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 data-shaped result, such as a refund approval. The party who ran the decision is the issuer; 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 invocation?

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. 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;
• the complete execution transcripts — Native evaluates the rule on its ordinary tree evaluator and through the lowered Meaning path, and keeps both full transcripts, not just the final value; and
• the issuer engine identity, a digest of the exact Native executable.

Issuance signs this context with the issuer's Ed25519 key as a DSSE envelope. With --emit-bundle, Native also packs the envelope together with the source and input bytes into one bounded transport file, 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, nothing more. lispex vouch inspect can confirm that a file is structurally consistent — schema, hashes, 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 canonical file the consumer creates from a public key, an engine digest, 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?” — never “did it sign the rule and input I mean?”.

For that second question, the request must arrive from outside the artifact: 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 reject a half-pinned invocation before reading the artifact.

A fully proved Lispex Image may supply the exact source bytes through --source-image. It changes the source representation only. 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:

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 invocation, the live re-executed result must exactly equal the decision the caller names with --require-decision. 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, engine, 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 invocation.

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 canonical lispex.vouch-compiled-artifact/v1 container 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 same-Rust-lineage evidence, 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 invocation.
• A gate grant is not a serializable authority token.
• 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.