Receipts & Q: history as evidence
A committed turn leaves Q — the receipt: the committed postcondition of the step, under one commitment scheme (a sorted-Poseidon2 Merkle commitment, all the way down). The witness proves Q; disclosure dials project Q; aggregation folds Q; the light client verifies only Q-chains. One object, every role.
The log is the truth; the database is a cache
Two coupled chains record a cell's history. The receipt chain (per
cell, prev → hash) is the append-only record of what was decided.
The witness bundle, bound into each receipt by its witness hash, is
the content that makes the decision replayable. Because the witness is bound,
checkpoint, restore, replay, and time-travel are theorems, not features: you
re-seed the execution from a recorded witness and the same receipts fall out. Any
state you can display is a projection of the chain; the chain is what is true.
A receipt binds the whole post-state
The receipt's commitment is determined by — and, under collision-resistance, recovers — every field of the post-state. There is no field a tamperer can edit while keeping the receipt valid: not a third cell's slots, not the capability list, not a nullifier, not the lifecycle. This is what separates a receipt from a checksum: it is a binding judgment about the entire state of the system after the step, including the parts the step did not touch (the frame is committed too).
The executor is a memory program
"Binds every field" is not a slogan bolted onto the commitment — it is a structural fact about how the executor moves state. Every state access the kernel makes — a register read or write, a heap get or set, a capability-membership check, a nullifier insert or freshness test — is one tuple in one memory multiset over a single domain-tagged address space. The whole post-state has a universal map: a total projection that lays all seventeen kernel fields, the heap, the c-list, the nullifiers, and the receipt log onto one address space, and the post-state's projection equals the fold of the verb's emitted memory trace over the pre-state's projection. Every field has a universal address; nothing is off the map, so nothing can be smuggled past the commitment.
This collapse pays out twice. First, it is what makes integrity constructive rather than asserted — the commitment binds the whole state because the whole state is the final column of one memory argument, and a single Blum multiset-balance check certifies every per-domain view at once (the domain tag keeps the views disjoint: a capability check cannot alias a nullifier cell). Second, it makes nullifier freshness Merkle-path-free inside a proof: a read that returns "absent" at a nullifier address, under the insert-only discipline, proves the nullifier was fresh — no per-access hashing, no in-proof Merkle path. Cross-proof persistence still rides the published sorted-tree root (the boundary view derived from the final memory cells equals today's root), so anyone holding the root learns absence; the path just stops being paid intra-proof.
One thing deliberately does not ride the memory multiset: conservation. Σδ = 0 is a correlated property of a paired write (value out of one balance, into another) and cannot be expressed by any per-address argument — so it stays an in-row paired constraint on the move row, exactly where rung 2's linear law lives.
Evidence is monotone
The receipt chain is the evidence substance from rung 2 doing its job: once a receipt exists it never un-exists, and the freshness ledgers it carries only grow. A committed spend inserts its nullifier; a second spend of the same nullifier fails closed — at the level of the term semantics itself, not an executor side table. Non-membership ("this nullifier is fresh") is itself a witnessed claim: a sorted-tree non-membership opening with a circuit gate, so freshness is checkable by anyone holding the root.
Grounding
Circuit/Argus/Receipt.lean—argus_commits_to_one_receipt(the circuit term commits to exactly one receipt, determined by the post-state) andargus_circuit_executor_receipts_agree(the circuit's receipt and the executor's receipt are the same judgment — one semantics, two readings).Circuit/CommitmentCrossBind.lean—runnable_binds_same_system_roots(equal commitment ⇒ equal full state) andchC_bad_not_bridge(a commitment that drops a field is rejected as a bridge — the binding has teeth).Circuit/Argus/Effects/NoteSpend.lean—noteSpendStmt_no_double_spend,noteSpendStmt_then_reject,noteSpendStmt_replay_rejected.Crypto/NonMembership.lean—nonmembership_sound/nonmembership_complete.Exec/UniversalBridge.lean—uproj(the universal map of the whole post-state) and{gwrite,move,create}_is_memory_program(the post-state projection equals the fold of the verb's memory trace, against the live executable steps).Crypto/UniversalMemory.lean—universal_memory_sound(one Blum balance certifies every per-domain view),nullifier_fresh_sound/nullifier_fresh_binds_root(intra-proof freshness with no Merkle path; the root pins absence at the boundary), andboundary_root_derived(the derived view equals today's map roots).
Live instance
Touch it: open any turn in the explorer and walk its witness; use the explorer's time-travel view to re-seed past state from receipts and watch it agree with the present chain.