:db/add rejected when equivalent to db.fn/call +

[moea]

(deftest scratch-passing
  (common/deployed-valid-invariant? backend schema)
  (let [txn [[:db.fn/call + 1 :account/balance -1]
             [:db.fn/call + 2 :account/balance +1]
             [:db/add 1 :transaction/signed-by 1]]]
    (is (not (common/balance-mismatch? backend txn schema)))))

(defn balance [u]
  (:account/balance (d/entity @conn u)))

(deftest scratch-failing
  (common/deployed-valid-invariant? backend schema)
  (let [txn [[:db/add 1 :account/balance (dec (balance 1))]
             [:db/add 2 :account/balance (inc (balance 2))]
             [:db/add 1 :transaction/signed-by 1]]]
    (is (not (common/balance-mismatch? backend txn schema)))))

@whilo It looks like ?balance-change is equivalent to ?balance-after in the second case, so the tx is rejected, though it's equivalent to the first (passing) tx. For commutativity etc. there's reasons why the first is preferable, and I may be missing something - but it seems like the second form ought to be acceptable?

[whilo]

Yes, scratch-failing should work. A big problem for me is that the debugging experience right now is not great. The invariant is not only checking the balance but also other things and I do not know where it fails just by looking at the code and what you say. It would be helpful to see what is happening in an inlined example playing around with Datalog as is done in the scratch pad for me. I can try to do so later this week; I think it would be good to have a general environment to test and explore incremental invariant building.

[moea]

@whilo The issue basically reduces to the clause [$empty+txs ?affected-entity :account/balance ?balance-change] - where $empty+txs is (d/db-with (db/empty-db) (concat schema tx)). In the + case, the balance change is always relative, so reading it from the tx makes sense. When we're using :db/add, the ?balance-change is just ?balance-after, as we're passing an absolute value. Changing the clause to [(- ?balance-after ?balance-before) ?balance-change] fixes the issue.

Here's some scratch code if you want to mess around with it:

(ns invariant.datahike-scratch
  (:refer-clojure :exclude [+])
  (:require [invariant.datahike
             :refer [+]]
            [invariant.test.util
             :refer [read-resource]]
            [datahike.api  :as d]
            [datahike.core :as dc]))

(defn query [q conn tx]
  (d/q q
       @conn
       (dc/db-with @conn tx)
       (dc/db-with (dc/empty-db) tx)
       tx))

(let [uri    "datahike:mem:///invariant-test-2"
      schema (read-resource "datahike_schema.edn")]
  (d/create-database uri)
  (let [conn (d/connect uri)]
    (d/transact conn schema)
    (d/transact conn common/example-txs)
    (let [q '[:find ?matches .
              :in $before $after $empty+txs $txs
              :where
              ;; run the sub-query
              [(subquery
                [:find (sum ?balance-before) (sum ?balance-after) (sum ?balance-change)
                 :with ?affected-entity
                 :in $before $after $empty+txs $txs
                 :where
                 ;; Unify data from databases and transactions with affected-entity
                 [$after      ?affected-entity         :account/balance    ?balance-after]
                 [(get-else $before ?affected-entity :account/balance 0) ?balance-before]
                 [(- ?balance-after ?balance-before) ?balance-change]

                 ;; 2. Positivity
                 [(>= ?balance-after 0)]

                 ;; 3. Sender spending
                 [$txs _ _ :transaction/signed-by ?sender]
                 [(= ?sender ?affected-entity) ?is-sender]
                 [(>= ?balance-change 0) ?pos-change]
                 [(or ?is-sender ?pos-change)]]
                $before $after $empty+txs $txs)
               [[?sum-before ?sum-after ?sum-change]]]
              [(= ?sum-before ?sum-after)]
              [(== ?sum-change 0) ?matches]]
          txn1 [[:db.fn/call + 1 :account/balance -1]
                [:db.fn/call + 2 :account/balance +1]
                [:db/add 1 :transaction/signed-by 1]]
          txn2 [[:db/add 1 :account/balance 4999M]
                [:db/add 2 :account/balance 101M]
                [:db/add 1 :transaction/signed-by 1]]]
      [(query q conn (concat schema txn1))
       (query q conn (concat schema txn2))])))