Use Lispex Vouch

Use Native and a new working directory. The commands use a POSIX shell, such as Git Bash on Windows. This exercise performs both issuer and recipient roles locally. For separate parties, the recipient independently reviews the issuer's public key, exact executable identifier, and rule source.

Prepare the rule and input

Save the complete program as print-handoff.lspx. The application measures the final file and supplies four boolean checks in the agreed order.

(define print-specs-pass?
  (and (car input)
       (car (cdr input))
       (car (cdr (cdr input)))
       (car (cdr (cdr (cdr input))))))

(if print-specs-pass?
    (decision-approve)
    (decision-deny))

Save input.checked.json exactly as follows. Save both files as UTF-8 without a BOM, with LF line endings and one final newline. Keep the input's two-space indentation.

{
  "input": "csk.checked-input/v1",
  "value": [
    true,
    true,
    true,
    true,
    "edition-final"
  ]
}

The first four values mean page size, margins, embedded fonts, and page count passed inspection, in that order. The fifth identifies the final file revision agreed by both parties. The application associates that revision with the exact production file and retains it. The rule reads the four booleans. The signature binds all five input values. This example returns approve. csk.checked-profile/v1 names the language profile used here.

Prepare a signing key

Generate a local Ed25519 key pair for this exercise and inspect the public key.

lispex key generate --out-dir issuer-key
lispex key inspect --public-key issuer-key/public.spki.der

Both commands exit with code 0. Generation prints JSON with "status": "generated" and creates issuer-key/private.pkcs8.der and issuer-key/public.spki.der. Inspection prints JSON with "status": "valid". The issuer uses the private key to sign. The recipient selects the public key for their policy and keeps the private key with the issuer.

Print the identifiers of the files you selected. Replace /absolute/path/to/lispex with your Native executable's absolute path. On Windows, a path such as D:/tools/lispex.exe works.

lispex vouch key-id --public-key issuer-key/public.spki.der
lispex vouch engine-id --executable /absolute/path/to/lispex
lispex vouch source-id --source print-handoff.lspx
lispex vouch input-id --input input.checked.json

Each command prints one identifier and exits with code 0. key-id depends on the generated key. engine-id starts with sha256: and identifies the exact executable. Review this value before using it in a policy. For the source and input above, the last two commands print these values.

3c60363413d708bed3b6c9cd0ae0fc440a89712c53aaa3eec8e5d4dcefe52423
9e1f420be1fc34992b76a0b1d88ea20e72243f6f4ca5a80210298e1693d006cf

1. Create the recipient's policy

Replace the placeholder in ENGINE_ID with the complete reviewed output of engine-id, including sha256:. Select the public key and source you reviewed.

ENGINE_ID="sha256:<reviewed-native-engine-digest>"
lispex vouch policy create \
  --public-key issuer-key/public.spki.der \
  --engine-sha256 "$ENGINE_ID" \
  --source print-handoff.lspx \
  --out policy.json

lispex vouch policy check --trust-policy policy.json

Creation writes policy.json. Both commands exit with code 0 and print nothing. The policy stores the allowed key, engine, language profile, and source identifier in one prescribed byte format. This step prepares trust settings. Next, the issuer signs an execution record.

2. Issue the signed record

Set ISSUER_KEY_URI to pkcs8-file:// followed by your private key's absolute path. A Linux or macOS path starts with pkcs8-file:///. On Windows, use a value such as pkcs8-file://D:/vouch-example/issuer-key/private.pkcs8.der. Replace the path below before running.

ISSUER_KEY_URI="pkcs8-file:///absolute/path/to/issuer-key/private.pkcs8.der"
lispex vouch issue \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --key-handle "$ISSUER_KEY_URI" \
  --out-dir issued \
  --emit-bundle

The command exits with code 0 and prints nothing. Native runs the source through Lispex Interpreter and the Meaning interpreter and signs both complete execution records. Lispex Interpreter reads and normalizes the source into core forms (CoreExpr), then evaluates them. Meaning evaluates a representation derived from that source.

The command creates these files under issued/. Choose a new output directory for each issuance.

The bundle has a byte limit. Next, check its signature against the recipient's policy.

3. Authenticate the bundle

lispex vouch verify \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --profile csk.checked-profile/v1 \
  --report-out authenticated.json

The command exits with code 0 and prints nothing. In authenticated.json, authentication_status is "authenticated" and primary_error is null. This confirms that a permitted key signed the context accepted by your policy.

The report's comparison_status: "agree" describes the signed execution record. The current run is checked in step 5. First, bind your own source and input.

4. Bind your request

Pass the source and input you selected separately from the bundle.

lispex vouch verify \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --report-out bound.json

The command exits with code 0 and prints nothing. It writes bound.json with authentication_status: "authenticated" after matching both files' exact bytes to the signed context. The report uses the same format as step 3. this command's external source and input establish the request binding.

A fully checked Lispex Image can replace --source with --source-image. Keep --input explicit. Native re-execution and the gate require both source and input paths, and reject an incomplete pair before reading files.

5. Check the current execution

lispex vouch verify \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --reexecute \
  --report-out current.json

The command exits with code 0 and prints nothing. It writes current.json with these results.

Native has now compared the current complete tree and Meaning execution records with the signed records. Next, require the decision your application needs.

6. Require the decision

lispex vouch gate \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --require-decision approve \
  --report-out gate.json

The command exits with code 0 and prints nothing. It writes gate.json. Its gate object is shown below.

{
  "basis": "csk.current-native-agreement/v0",
  "observed_decision": "approve",
  "reason": null,
  "required_decision": "approve",
  "status": "granted"
}

The gate authenticates, binds the request, reruns the rule, and compares the required decision within this call. It produces a local grant held inside the Native process. The report records that result for inspection and logging.

To see a refusal, repeat this command with --require-decision deny and --report-out denied.json. It exits with code 10, prints nothing, and writes gate.status: "denied" with gate.reason: "required-decision-mismatch". The observed decision remains "approve". After a refusal, inspect the report before deciding what the application should do.

The calling application checks caller identity, freshness, expiry, revocation, request reuse, business authorization, and transaction state. It controls external actions such as authorizing the print job.

Add compiled execution or connect an application

The compiled example adds Lispex VM agreement to the Lispex Interpreter and Meaning checks. Native derives Core IR, the intermediate representation with resolved name references, and bytecode again after authenticating the request.

Use What Your App Does After a Decision to connect the local gate result to an application. Use Records and Reports to read each output file.