Choose the fixed workspace
Start from the practical decision workspace listed on
Downloads, or use
examples/refund-workspace in the Lispex repository. The archive and the
repository directory have the same fixed member inventory. Keep every key and
generated artifact outside that immutable directory.
The workspace contains two different refund rules.
| Lane | Source | Input shape | Result |
|---|---|---|---|
| Decision exchange | generated/exchange/refund-window.lspx | ordinary JSON records | allow or deny |
| Vouch | generated/vouch/refund-window-native.lspx.png | checked input values | approve or deny |
The exchange result is not Vouch evidence. The Vouch result is not an exchange result. They share a business example without sharing an identity, receipt, policy, or authority.
Check the workspace before doing any work
Enter the extracted workspace root or the repository directory. Create one separate caller-owned work root and ask Native to check the fixed inventory.
mkdir -p ../refund-work
lispex workspace status --dir . --work-dir ../refund-workworkspace status checks the exact workspace members before it reports any
work slot. A reported present-unchecked slot is only present. It is not
verified, trusted, fresh, or authorized.
Run the bounded decision exchange
The exchange lane uses separate preparation and evaluation limits. It writes a five-member decision directory without storing the raw rule source.
mkdir -p ../refund-work/exchange
lispex rule run \
--source ./generated/exchange/refund-window.lspx \
--input ./generated/exchange/inputs/day-14-unopened.json \
--prepare-limits ./generated/exchange/prepare-limits.json \
--eval-limits ./generated/exchange/evaluation-limits.json \
--out ../refund-work/exchange/decision
lispex rule inspect --dir ../refund-work/exchange/decision
lispex rule verify --dir ../refund-work/exchange/decision
lispex rule replay --dir ../refund-work/exchange/decisionInspect and verify do not execute the rule. Replay creates one fresh built-in
evaluator instance and requires the same result. The portable result remains
vouch_eligible false.
Prepare a local issuer and an independent recipient
Generate the private key under a caller-owned directory outside both the workspace and the work root.
mkdir -p ../refund-issuer ../refund-recipient
lispex key generate --out-dir ../refund-issuer/key
lispex key inspect --public-key ../refund-issuer/key/public.spki.derFor this one-machine exercise, copy only the reviewed public SPKI into the recipient directory and inspect the copied bytes again.
cp ../refund-issuer/key/public.spki.der \
../refund-recipient/reviewed-issuer.spki.der
lispex key inspect \
--public-key ../refund-recipient/reviewed-issuer.spki.derA real issuer and recipient need a separately chosen transfer and review
channel. A local copy is a walkthrough convenience, not a trust procedure.
Never place private.pkcs8.der in the workspace, work root, recipient
directory, source control, or a bundle.
The recipient now creates a decision policy from four independently reviewed facts. None of them comes from the bundle that will be authenticated.
lispex decision policy create \
--public-key ../refund-recipient/reviewed-issuer.spki.der \
--semantic-rule-sha256 14bb6f2e43cee011aedbeafc71d3716789bea8117e8331cd6a7feb1858d7418f \
--semantic-profile-id lispex/r7rs-rule-embedded-core/1 \
--engine-artifact-sha256 fa6e52559e1f5a43e50a3b7ac0cc5add6930cff0aed8aaff462cff4609362870 \
--portable-core-schema lispex.embed-receipt-core/v1 \
--consumer-label refund-recipient \
--out ../refund-recipient/decision-policy.json
lispex decision policy check \
--policy ../refund-recipient/decision-policy.jsonPolicy creation records configuration. It does not authenticate an issuer organization and does not grant repeated-use or action authority.
Issue and authenticate the portable decision
The issuer signs the already verified portable core and writes one bounded
.lpxdecision file.
lispex decision issue \
--dir ../refund-work/exchange/decision \
--private-key ../refund-issuer/key/private.pkcs8.der \
--issuer-label refund-issuer \
--out ../refund-work/exchange/refund.lpxdecisionThe recipient uses its own policy and names the received bundle explicitly.
lispex decision inspect \
--bundle ../refund-work/exchange/refund.lpxdecision
lispex decision authenticate \
--bundle ../refund-work/exchange/refund.lpxdecision \
--policy ../refund-recipient/decision-policy.json
lispex decision replay \
--bundle ../refund-work/exchange/refund.lpxdecision \
--policy ../refund-recipient/decision-policy.jsonAuthentication proves that an admitted exact key signed the exact decision material. Replay adds a fresh evaluation. Neither one supplies freshness, replay prevention, organizational identity, or permission for an external action.
The files under samples/recipient are permanently marked
sample-do-not-trust. They are useful for command practice only and must not
become a real recipient policy or trust root.
Start the separate Image-backed Vouch lane
This lane starts again from the checked input and exact Lispex Image. It does
not consume the exchange result, decision directory, decision policy, or
.lpxdecision bundle.
Inspect the four Vouch identity inputs first.
mkdir -p ../refund-work/vouch
lispex vouch source-id \
--source-image ./generated/vouch/refund-window-native.lspx.png
lispex vouch input-id \
--input ./generated/vouch/inputs/day-14-unopened.checked.json
lispex vouch key-id \
--public-key ../refund-recipient/reviewed-issuer.spki.der
lispex vouch engine-id \
--executable /absolute/path/to/lispexReview the exact engine output, then use that complete printed value as
ENGINE_ID. The Vouch policy is separate from the decision policy even when
both refer to the same reviewed public key.
ENGINE_ID="sha256:<reviewed-native-engine-digest>"
lispex vouch policy create \
--public-key ../refund-recipient/reviewed-issuer.spki.der \
--engine-sha256 "$ENGINE_ID" \
--source-image ./generated/vouch/refund-window-native.lspx.png \
--out ../refund-work/vouch/policy.json
lispex vouch policy check \
--trust-policy ../refund-work/vouch/policy.jsonIssue the retained walkthrough input from the exact Image.
ISSUER_KEY_URI="pkcs8-file:///absolute/path/outside-workspace/refund-issuer/key/private.pkcs8.der"
lispex vouch issue \
--source-image ./generated/vouch/refund-window-native.lspx.png \
--input ./generated/vouch/inputs/day-14-unopened.checked.json \
--profile csk.checked-profile/v1 \
--key-handle "$ISSUER_KEY_URI" \
--out-dir ../refund-work/vouch/issued \
--emit-bundleThe retained checked input contains only [14, false]. Its issued bundle is a
walkthrough bundle only. It cannot be reused by the application handoff
because it does not bind a request ID, actor, action, or expiry.
Issue a dedicated six-value current-request bundle
Create a caller-owned file with these exact canonical bytes and one final line feed.
{
"input": "csk.checked-input/v1",
"value": [
14,
false,
"request-123",
"operator-7",
"refund",
1785600000
]
}Store it as ../refund-work/app/current-request.checked.json. Issue a new
bundle that binds all six values.
mkdir -p ../refund-work/app
lispex vouch issue \
--source-image ./generated/vouch/refund-window-native.lspx.png \
--input ../refund-work/app/current-request.checked.json \
--profile csk.checked-profile/v1 \
--key-handle "$ISSUER_KEY_URI" \
--out-dir ../refund-work/app/current-request-issued \
--emit-bundleThe refund rule reads the first two values. The Vouch input identity and signed context still bind all six exact values. Extra binding does not prove that the actor was authenticated or that the request is unique. The surrounding application must establish those facts from its own trusted state.
Run a fresh gate for that exact request
The recipient supplies the dedicated bundle, its policy, the exact Image, and
the same six-value checked input independently. The gate creates a fresh local
execution observation and requires approve.
lispex vouch gate \
--bundle ../refund-work/app/current-request-issued/vouch-input-bundle.json \
--trust-policy ../refund-work/vouch/policy.json \
--source-image ./generated/vouch/refund-window-native.lspx.png \
--input ../refund-work/app/current-request.checked.json \
--profile csk.checked-profile/v1 \
--require-decision approve \
--report-out ../refund-work/app/current-request-gate.jsonA stored verification or gate report is diagnostic output. It cannot replace a fresh gate for another request and cannot become evidence input to a later gate.
Stop at the authority boundary
An exit-zero gate establishes one local match between live authenticated current execution and the required decision. It does not authenticate the application caller, authorize an actor or action, check server time, reserve a request ID, perform a refund, or make an external transaction exactly once.
The application handoff example shows how a surrounding application can bind
those server-owned facts and publish an informative no-clobber would_act
record. It still performs no external action.