Anatomy of a receipt.

Every action in dregg leaves a receipt—a small record that pins exactly what happened. Here is what one is made of, and what a machine has proven about it.

Nothing below is a mock-up. The receipt is real output from the running system; the field names are the real ones; the theorems are the real statements, checked by machine.

One real action

The action, then the receipt.

A single turn: set one cell's state field to the number 42, authorized by a hybrid Ed25519 + post-quantum (ML-DSA-65) signature. This is what the system produced.

TurnReceiptreal output · finality: Final

turn_hash              ef98305e2a8fd373beb4e91b3c58b8dfb9dc5d00c6e754eac5d7b7de4269c9da
forest_hash            96cdbbd016ad23740f87151c901f866c730f5b7ec66e0101950b3847f51498a1
pre_state_hash         edbf0739c53d59f46d0ce32d1b3d04e9768b074fdab39d4efc6ebdb95397e012
post_state_hash        0803a53daf67b2387748167a49f19255bef4f5c8ae13e557ea316f0b1c7bc1a3
effects_hash           61a7cc5301a13e03f2d77626a75dff9c792e55caa50c69862f5cea183d9942a6
agent                  4503c7b6ced06c09c2b9ca66afe04869c8f2aa69fa73d835379937e8eb2c507e
previous_receipt_hash  null            (this is the first receipt in the chain)
computrons_used        622
action_count           1
finality               Final

A receipt carries more than this—links for capabilities it created, events it emitted, an optional executor signature. These are the load-bearing few.

Field by field

What each line means.

turn_hash

A fingerprint of the exact action this receipt answers for. Change what was requested, and this no longer matches.

pre_state_hash / post_state_hash

The world's fingerprint before and after. A receipt is a claim: "I moved the world from here, to there." One 32-byte value fixes every balance, every stored field, every permission, every spent coin.

effects_hash

A fingerprint of every concrete change the turn made—each balance moved, each value written. Nudge one delta and this value moves.

agent

The cell that authorized the turn. Authority here means holding a key that produces an accepted witness—not merely being named in a table.

previous_receipt_hash

The link to the receipt before it. Receipts form an unbroken chain; here it is null because this is the very first one.

computrons_used

The metered work the turn cost—622 here. Work is counted, not estimated.

finality

Final means a quorum has committed it; Tentative means it is provable but not yet quorum-final.

The property that matters

You cannot forge a field.

Here is what makes a receipt more than a log line. The post-state fingerprint is not written down and trusted—it is bound, inside the proof, to the actual output of the run. Change one field the action did not legitimately write—nudge a balance, mint a coin, widen a permission—and the fingerprint no longer matches what the machine computed.

So the proof does not merely fail to be found. It cannot exist. The turn becomes unprovable. Not "a server catches you"—there is no server, and nothing to catch. A ghost leaves no receipt.

In the engine, the claimed post-state is tied to the trace's committed output by the circuit's binding; the state fingerprint folds every balance, field, permission, and spent-coin ledger together, so moving any one of them moves the whole root. A tampered claim makes the proof's constraints unsatisfiable.

What is proven about it

The rules are theorems.

A receipt is only as good as the rules it must obey. In dregg those rules are theorems—written as mathematics and checked, every build, by the Lean proof checker. Four of them, in the system's own words, each with a plain reading.

proven

Conservation

∀ a : AssetId, recTotalAsset s.kernel a = 0

On every state the system can reach, every asset's books sum to exactly zero. Nothing is ever created or destroyed.

metatheory · AssuranceCase.lean · conservation_guarantee

proven

No amplification

∀ e ∈ forestEdgesG f,
  capAuthConferred (attenuate e.1 e.2) ⊆ capAuthConferred e.2

Every time authority is handed off, it can only narrow. No one can pass on more power than they hold.

metatheory · FullForestAuth.lean · execFullForestG_no_amplify

proven

No double-spend

interp (noteSpendStmt nf) k = some k' → nf ∉ k.nullifiers

If a coin is spent, it was provably unspent before—and spending it a second time simply fails.

metatheory · Argus/Effects/NoteSpend.lean · noteSpendStmt_no_double_spend

proven

The circuit is the machine

satisfiesConstraints applyEff old new s rest →
  isVmExecution applyEff old new s rest

Any trace that passes the circuit's checks really is a faithful run of the machine—it starts where it claims and ends exactly at the computed result.

metatheory · Circuit/AirSoundness.lean · air_sound

One theorem holds them together. A single statement, deployed_system_secure, composes all of these over one turn—no amplification, conservation, whole-post-state binding, no double-spend, and light-client provability, at once. Assuming standard cryptography—the same collision-resistance every modern system rests on—it holds.