A receipt turns a private fact into public footing.

It binds a named semantic program to the exact committed state before and after. Unlike programs can therefore compose without pretending to share an instruction set.

The witness may stay hidden. The identity, authorized result, and state link remain available to anyone who must rely on the act.

The symbolic instruction

One envelope, six load-bearing claims.

SemanticReceiptpublic boundary

program_commitment_8   the exact semantic program
verification_key_8    the exact proof relation
old_state_root_8      the committed input world
new_state_root_8      the committed output world
public_result         only what this program authorizes revealing
session / index       where this step belongs
proof                 evidence that the relation holds

Identity

A proof for another relation cannot stand in. All eight verification-key limbs are bound.

Continuity

The next receipt must begin at this receipt’s output root and advance the index exactly once.

Meaning

The verifier learns the authorized result—not every private value used to establish it.

Why full identity matters

The verification key is part of the opcode.

Two relations can expose the same public fields while enforcing entirely different rules. Checking only the shape—or the first half of a key—would let an easier program impersonate the intended one.

dregg’s current custom carrier binds the full eight-limb program commitment and full eight-limb verification key alongside the state and application roots. Earlier four-limb carriers are retired and refused.

This is the symbolic equivalent of instruction decoding. The question is not merely “is this proof valid?” but “is it valid for exactly the semantic operation this cell installed?”

One real system receipt

The abstract boundary lands in an ordinary turn record.

This specimen is real output from the running system: one authorized state-field write to the number 42.

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
computrons_used        622
action_count           1
finality               Final

From knowledge to common knowledge

Common knowledge is manufactured.

step 0A → Bprogram P

step 1B → Cprogram P

step 2C → Dprogram Q

recursive foldA ⟹ Done succinct history proof

A ledger is a common-knowledge prosthesis.

A finality certificate is a shared, transferable witness. Instead of asking whether everyone knows, and knows that everyone knows, without end, a participant verifies one artifact under the agreed finality rule.

For graph rewriting, the formal history theorem already checks the exact boundary: same session and ruleset, contiguous index, equal adjacent roots. A hidden splice either denotes a real semantic chain or exposes a commitment collision.

What a receipt does not say

Small public output is a design decision.

revealed

The authorized result

A winner, clearing price, accepted/rejected bit, new graph root, or other deliberately public value.

hidden

The witness from consumers

Ballots, orders, graph openings, assignments, or cards can stay out of the proof consumer’s view.

not automatic

The witness from the prover

Tier-1 HidingFri still allows the trace-building process to see the witness. No-single-viewer production requires the separate FHE/MPC/distributed-prover path.

not automatic

Whether the rule was wise

A proof establishes the stated relation. It cannot rescue a badly authored policy or an incomplete model.