Using Lispex Vouch

Before you start

The running example is a refund-window rule. Prepare these independently — none of them may come from the artifact you are about to verify:

• the reviewed rule as refund-window.lspx.png or refund-window.lspx;
• the exact checked input file INPUT;
• an Ed25519 public key issuer.spki.der and an absolute local PKCS#8 key URI;
• the reviewed digest of the exact Native executable; and
• new paths for POLICY, OUTPUT, and each report.

The trust policy belongs to the consumer. Do not derive trust from the bundle you are about to verify.

The six-stage path

Each stage answers one question and hands its result to the next. Success at one stage never implies the next.

Read the results in order

1. A valid policy is configuration, not authentication.
2. Verifying a bundle without pins authenticates the bundle's own context only.
3. Pinned verification adds exact byte equality with the caller's external source and input; both files are mandatory for every authority-bearing Native step.
4. Re-execution is a new observation by the current Native build. It is not a claim about a past run and not an independent implementation.
5. A gate exit of 0 is one local decision match. Exit 10 means no grant. The report itself cannot be replayed as a grant.
6. Any payment, deployment, refund, or other action remains a separate application decision with its own freshness and replay controls.

What each step establishes — and what it still lacks

Commands you can copy

1. Derive the exact key identity

lispex vouch key-id --public-key issuer.spki.der

2. Derive the exact engine identity

lispex vouch engine-id --executable /exact/path/to/lispex

3. Derive the exact source identity

lispex vouch source-id --source-image refund-window.lspx.png

4. Derive the exact input identity

lispex vouch input-id --input INPUT

5. Native issue and emit the bundle

lispex vouch issue \
  --source-image refund-window.lspx.png --input INPUT \
  --profile csk.checked-profile/v1 \
  --key-handle pkcs8-file:///ABSOLUTE/issuer.pk8 \
  --out-dir OUTPUT --emit-bundle

6. Create policy from independently reviewed public inputs

lispex vouch policy create \
  --public-key issuer.spki.der \
  --engine-sha256 sha256:<reviewed-engine-digest> \
  --source-image refund-window.lspx.png --out POLICY

7. Check the exact canonical policy bytes

lispex vouch policy check --trust-policy POLICY

8. Native or npm authenticate the bundle-owned context

lispex vouch verify \
  --bundle OUTPUT/vouch-input-bundle.json \
  --trust-policy POLICY --profile csk.checked-profile/v1 \
  --report-out AUTH-REPORT

9. Native or npm pin the bundle to the intended request

lispex vouch verify \
  --bundle OUTPUT/vouch-input-bundle.json \
  --trust-policy POLICY --source-image refund-window.lspx.png --input INPUT \
  --profile csk.checked-profile/v1 --report-out PINNED-REPORT

10. Native bind the exact request and re-execute

lispex vouch verify \
  --bundle OUTPUT/vouch-input-bundle.json \
  --trust-policy POLICY --source-image refund-window.lspx.png --input INPUT \
  --profile csk.checked-profile/v1 --reexecute \
  --report-out REEXECUTION-REPORT

11. Native local decision gate

lispex vouch gate \
  --bundle OUTPUT/vouch-input-bundle.json \
  --trust-policy POLICY --source-image refund-window.lspx.png --input INPUT \
  --profile csk.checked-profile/v1 --require-decision approve \
  --report-out GATE-REPORT

12. Optionally require verified VM agreement

Build the Vouch-specific compiled container from the same exact source. Building, inspecting, and validating do not authenticate, execute, or grant anything:

lispex vouch compiled build \
  --source-image refund-window.lspx.png \
  --out refund-window.lpxvca

lispex vouch compiled inspect \
  --artifact refund-window.lpxvca

lispex vouch compiled validate \
  --artifact refund-window.lpxvca \
  --source-image refund-window.lspx.png

Then opt into the compiled path without removing any earlier pin or check:

lispex vouch verify \
  --bundle OUTPUT/vouch-input-bundle.json \
  --trust-policy POLICY --source-image refund-window.lspx.png --input INPUT \
  --profile csk.checked-profile/v1 --reexecute \
  --compiled-artifact refund-window.lpxvca \
  --report-out COMPILED-REEXECUTION-REPORT

lispex vouch gate \
  --bundle OUTPUT/vouch-input-bundle.json \
  --trust-policy POLICY --source-image refund-window.lspx.png --input INPUT \
  --profile csk.checked-profile/v1 --require-decision approve \
  --compiled-artifact refund-window.lpxvca \
  --report-out COMPILED-GATE-REPORT

The container must be canonical, pass the strict bytecode verifier, and match an exact source-to-Core-IR-to-bytecode derivation before any VM state is created. The current tree/Meaning execution must still agree first. A producer mutation, different source byte, VM disagreement, or required-decision mismatch fails closed; the command never retries through the source-only gate.

13. Raw compatibility with the same policy

lispex vouch verify \
  --envelope OUTPUT/envelope.dsse.json \
  --trust-policy POLICY --source-image refund-window.lspx.png --input INPUT \
  --profile csk.checked-profile/v1 --report-out AUTH-REPORT

A common mistake

The gate does not execute an external action, and its report is not a transferable authorization. The calling application still owns freshness, replay handling, identity, deployment controls, and the judgment of whether requiring that decision is safe and correct.

Current boundaries

• Policy creation accepts only the reviewed public inputs. It never accepts a private key, stdin, an envelope, bundle, receipt, or report, an inferred running engine, a network resource, or an existing policy to merge. Reviewing where the public key and engine came from — and distributing, replacing, and retiring the policy — remains the consumer's job; browser WASM and the Playground expose no policy API.
• Identity commands read the named files only and infer nothing from artifacts. source-id and input-id are domain-separated hashes rather than ordinary SHA-256; neither decodes or normalizes text, and input-id does not parse checked-input JSON. An identity is a name for exact bytes — it establishes no provenance, approval, policy, trust, authentication, evidence, freshness, replay control, or authority.
• A bundle is untrusted transport — not a receipt, signature, report, capability, source approval, or transferable authorization. It adds no encryption or confidentiality, and it provides no freshness, nonce enforcement, expiry, revocation, replay prevention, identity, independent witnessing, policy correctness, provenance before the supplied bytes, deployment safety, or permission for an external action.
• Request pinning is exact byte equality and nothing else: it provides no freshness, nonce uniqueness, expiry, revocation, replay prevention, or proof of human intent, and no permission for an external action. An invalid signature or policy is rejected before any request mismatch is reported. With a bundle, --source and --input must be supplied together; a partial pair is usage exit 2 before any artifact is read.
• A compiled artifact is deterministic integrity material derived from exact source — not a trust root, signed request, independent witness, or portable capability. Its report cannot be used as evidence input. The compiled path does not establish organizational identity, policy or rule correctness, freshness, replay prevention, compiler correctness beyond the checked derivation, or permission for an external action.

Keep going

Keep the Vouch overview nearby: it separates authentication, request binding, current execution agreement, and a local grant.

Lispex Vouch overview · Choosing a Runtime Surface