Lispex Vouch

The decision being checked

Every Vouch workflow protects one concrete, repeatable decision. A reviewed Lispex rule reads one exact input and returns one result that is ordinary data, such as a refund approval. The party who ran the decision is the issuer, and the party who wants to check it later is the consumer. Vouch exists for the moment those two are not the same person, machine, or point in time.

Instead of answering the broad question “should I trust this JSON?”, Vouch asks four smaller questions, each with its own check and its own failure.

1. Authentication. Did an allowed key sign these exact bytes?
2. Request binding. Do those bytes describe the exact source and input chosen by this consumer?
3. Current execution agreement. Does the current Native interpreter reproduce the same complete result?
4. Local decision. Does that live result exactly match the decision required by this call?

Passing an earlier question never silently passes a later one. That separation is the core of Vouch.

The evidence a decision leaves behind

When the issuer runs Native vouch issue, the run is captured as evidence rather than as a bare answer. Here is what the signed context pins.

• the exact rule source bytes
• the exact input bytes the rule read
• the fixed checked profile (csk.checked-profile/v1) under which the rule ran, which is the smaller part of the language a rule has to stay inside to take part in Vouch at all
• the complete execution transcripts. Native evaluates the rule twice, once on the built-in interpreter that reads your source directly and once through the Meaning path, the lowered form that same source is first converted into. These docs write that pair as tree/Meaning, and issuance keeps both full transcripts, not just the final value
• the issuer engine identity, a short fingerprint of the bytes of the exact Native executable

Issuance signs this context with the issuer's Ed25519 key, producing a signed container in the DSSE format called the envelope. With --emit-bundle, Native also packs the envelope together with the source and input bytes into one transport file that has a fixed size limit, the bundle.

What the portable artifacts prove

A bundle is one file you can move between machines, and it is deliberately weak. It is untrusted transport and nothing more. lispex vouch inspect can confirm that a file is structurally consistent, checking its schema, its hashes, and its internal bindings, without making any trust claim.

The first real claim is authentication. lispex vouch verify checks the envelope against a trust policy, a small file written the same way every time, which the consumer creates from a public key, a short fingerprint of the exact program that runs the rule, and rule source they reviewed independently. A successful verify means precisely this. A key allowed by my policy signed exactly this context. It does not mean the context is the one you care about, that the rule still behaves the same way today, or that anything is approved.

Why the request must come from you

A bundle may carry source and input, but the issuer chose them. Verifying only the bundle answers “did an allowed key sign something?” and never “did it sign the rule and input I mean?”.

For that second question, the request must arrive from outside the bundle. You supply your own --source and --input, and Vouch checks that the signed context is byte-for-byte equal to them. Without that separately supplied pair, the bundle is an authentication target, not permission to select what re-execution or a gate will run. Native re-execution and gate require both external paths, and a call that supplies only one of them is rejected before the file is read.

A fully proved Lispex Image may supply the exact source bytes through --source-image. It changes only how the source is carried. Input choice, trust policy, re-execution, and gate remain separate.

How each tool consumes the evidence

Choose the operation by the question you actually need answered. The table also names the verified Rust VM, a virtual machine that runs compiled instructions instead of reading your source directly.

Re-execution answers the third question. Native runs the rule again now and compares the current complete transcripts with the signed ones. The gate answers the fourth. Within one Native call, the live re-executed result must exactly equal the decision the caller names with --require-decision. That local pass, the grant, exists only inside that process. The gate report is diagnostic output, not a token.

The safe default journey uses the pieces in this order.

1. Build a trust policy from a public key, the exact program that runs the rule, and rule source that the consumer reviewed independently.
2. Let the issuer create a bundle for exact source and input bytes with Native.
3. Do not let the bundle choose the request. Supply the consumer's own --source and --input.
4. Authenticate with Native or npm.
5. Add Native re-execution only when current execution agreement matters.
6. If you also require the verified Rust VM, build and validate a compiled artifact from that exact source, then add --compiled-artifact.
7. Use the Native gate only when the application requires one exact decision in that same call.

The end-to-end Vouch workflow gives the commands in that order.

The optional compiled route

Vouch can additionally require agreement from the verified Rust VM, but ordinary bytecode and VM output cannot enter the chain. The compiled route starts from the same externally supplied exact source and input, then requires a lispex.vouch-compiled-artifact/v1 container, written the same way every time, to be re-derived from that source before the verified Rust VM runs. A .lpxbc file, hash, verifier result, inspection report, VM observation, or tree/VM comparison report cannot replace the source request, authentication, current tree/Meaning agreement, or live gate transition.

The optional Topaz bytecode VM is a separate diagnostic route, not another Vouch verifier. Its installed product, request/result JSON, execution output, resource observation, and compare-vms receipt cannot be supplied to vouch verify, compiled re-execution, or vouch gate. Agreement with Topaz does not create or strengthen a grant.

What Vouch does not authorize or guarantee

• A valid signature does not prove a person or organization, signing time, or honest deployment.
• Exact request equality does not provide freshness, expiry, revocation, or replay prevention.
• Tree/Meaning and VM agreement is evidence from one shared Rust lineage, not an independent implementation witness or whole-language equivalence proof.
• Compiled agreement does not prove compiler correctness outside the exact artifact, source, input, transcript, and limits checked by this call.
• A gate grant is not an authority token you can save and hand to another program.
• Reports, bundles, images, bytecode, VM results, and Bridge artifacts cannot promote themselves into a grant.
• The calling application still owns approval and side-effect control for payments, refunds, deployments, or any other external action.

Keep going

Run the end-to-end workflow, or use Artifacts and Reports to look up what each file establishes and excludes.