Differential receipt
csk.differential-receipt/v0 records one decision-profile rule, exact input,
tree and lowered observations, hashes, and contract version. Native creates it
with lispex diff-receipt; Native and npm inspect it with lispex verify and
compare corpora with lispex replay.
Artifact roles
| Artifact | Records | Consumer |
|---|---|---|
csk.differential-receipt/v0 | exact rule, input, lowering, observations, versions, and hashes | structural verify and corpus replay |
csk.vouch-input-bundle/v0 | exact envelope, source, and input bytes | authenticated vouch verify |
| trust policy v1 | recipient-selected keys, engines, profiles, and source identities | authentication |
| authentication report | signature and policy result for the exact bound context | operator diagnostics and Native re-execution |
lispex.vouch-compiled-artifact/v1 | source identity, Core IR, verified bytecode, verifier, VM, and resource profile | compiled validation and Native compiled re-execution |
csk.native-reexecution-report/v0 | authentication plus current tree and Meaning agreement | local gate |
csk.native-compiled-reexecution-report/v1 | request-bound authentication, current tree and Meaning agreement, exact derivation, and current verified Rust VM agreement | compiled local gate |
| Topaz VM request, result, and comparison | installed-product lineage and exact bytecode observation | engineering inspection and comparison |
| Topaz AOT product and reports | installed executable lineage, source map, resource request, and observation | AOT inspect, validate, run, and route comparison |
| four-route report | one source, input, Core IR, bytecode, four observations, semantic axes, resource axes, and lineage | engineering inspection |
csk.native-gate-report/v0 | current local grant or denial for the required decision | host application |
csk.native-compiled-gate-report/v1 | current compiled local grant or denial | host application |
| Bridge report | external-engine artifact bindings, identities, and declared gates | lispex verify-bridge and recipient policy |
| replay report | agreement, mismatch, and comparison status for the selected corpus | rule review workflow |
Live decision chain
signed envelope
→ authentication under recipient policy
→ exact external request binding
→ current tree and Meaning re-execution
→ optional exact derivation and verified Rust VM agreement
→ required-decision local gate
→ host application actionEach transition consumes the typed result from the previous step in the same Native process. Reports record the transition for inspection and application logging.
Commands
SH
lispex diff-receipt --input input.datum rule.lspx > receipt.json
lispex verify receipt.json --source rule.lspx
lispex replay corpus --against receipts
lispex vouch verify ... --report-out authenticated.json
lispex vouch verify ... --reexecute --report-out current.json
lispex vouch gate ... --require-decision approve --report-out gate.json
lispex vouch compiled build --source rule.lspx --out rule.lpxvca
lispex vouch compiled validate --artifact rule.lpxvca --source rule.lspx
lispex vouch verify ... --reexecute --compiled-artifact rule.lpxvcaThe recipient policy owns accepted identity and source. Native owns current re-execution and the local gate. The host application owns actor, time, request uniqueness, transaction state, and external action.