Field note
LogUp Completeness: Proving Nothing Was Quietly Left Out
Suppose a proof contains ten resources and shows that every resource sent to a kind circuit was valid. A subtle question remains: did every one of the ten resources get sent somewhere? Independent per-kind checks can all pass while an inconvenient item is omitted.
This is the difference between local validity and completeness. The target vault treats completeness as its universal must-never-break invariant.
One signed multiset identity
The full Action set sends each resource fingerprint with multiplicity +1. Each kind partition receives the resources assigned to it with multiplicity −1. A LogUp argument compresses those multisets through randomized reciprocals in QM31. The global sum equals zero only when the received multiset equals the sent multiset, including multiplicities.
Informally:
all Action resources − all kind-partition resources = 0
That single identity proves two facts together: every resource appears in a partition, and no resource appears in more than one. Multiplicity itself is range-checked so arithmetic wraparound cannot fake cancellation.
Why fingerprints carry both kind and commitment
A resource fingerprint absorbs (kind_id, commitment). The kind identifier is the resource's logic field and is already bound into both its value reference and commitment. The partitioner cannot call an object one kind while its logic circuit sees another unless the commitment hash is broken.
Authority uses the same bus
Every consumed resource also needs evidence that its owner_kind validation ran. A second, domain-separated lane carries those authority assertions. Value completeness and authority completeness are therefore checked by the same algebraic pattern without confusing their meanings.
This is particularly useful for PayMoney escrow. The escrowed object's value logic is the selected FungibleV1, while its owner logic is the offer instance. It appears once in that asset's value partition and once in the offer authority lane. The domain tags keep those obligations distinct.
Why not use the same trick for all history
The per-Action resource set is bounded, so the complete partition can be represented in one proof at predictable cost. The lifetime nullifier set is unbounded. Rechecking its entire history per Action would make proving cost grow with system age, so freshness uses an indexed Merkle tree instead.
The architecture deliberately uses different arguments for bounded completeness and unbounded non-membership. The useful invariant is not “one primitive everywhere”; it is “the proof cost scales with the data each statement actually needs.”
Read indexed non-membership → · Read the architecture split →