Lispex manual
(Lispex)
( parens are punctuation, recursion is rhyme )
A small Lisp for decision rules, deliberately close to Scheme. Same input, same answer — and a run can leave a record exact enough to check later.
Structured input in, a printable verdict out.
Records are association lists, the boundary is an exact integer comparison, and every verdict — including refusal — is plain data you can print and compare. Nothing here is new notation: the surface belongs to Scheme. The Lispex character is in what stays fixed — a closed procedure surface, deterministic faults, one answer per input.
(define (field key record)
(let ((entry (assq key record)))
(if (pair? entry)
(cdr entry)
(error "missing field" key))))
(define (review-refund request)
(let ((days (field 'days request))
(opened (field 'opened request))
(cents (field 'cents request)))
(cond ((not (exact-integer? days)) '(reject malformed-days))
((>= days 15) '(deny outside-window))
(opened '(deny opened-item))
((> cents 50000) '(escalate manual-review))
(else '(allow within-policy)))))
(map review-refund
'(((days . 14) (opened . #f) (cents . 12900))
((days . 14) (opened . #f) (cents . 82000))
((days . 15) (opened . #f) (cents . 12900))))
; => ((allow within-policy)
; (escalate manual-review)
; (deny outside-window))Two on-ramps: a syntax map for Scheme readers, a guided path for everyone else.
The syntax map shows every everyday form with observed results, plus the places Lispex is stricter than the Scheme you know: a mandatory else arm on if, a closed 205-procedure surface, single-list higher-order procedures, and no user macro layer. The learning path takes the slower road and finishes with one complete, tested refund rule.
- 01Run a first program
- 02Name values and procedures
- 03Choose a data-shaped decision
- 04Test a complete refund rule
Lispex runs without a server. A reference interpreter, compiled to WebAssembly, evaluates code right in your browser.
One simple default, four explicit Native routes.
The default everywhere — browser, npm, Native — is the Rust tree interpreter. Native can additionally inspect and pin the built-in Rust VM or exactly installed Topaz VM and AOT products, as explicit routes rather than silent upgrades.
Rust and LIL cover all 205/205 current capability rows; LIT remains separately bounded at 84/205 and is reported that way. Native routes inventory, lock, doctor, measure, and run keep exact route identity and failure visible. Nothing is discovered, substituted, or retried behind your back: a missing product is a reported refusal, not a fallback.
Run the refund rule under exact limits. Keep what was checked.
Native lispex rule run prepares the reviewed rule, admits one strict JSON input, and evaluates it once on the bounded evaluator — a separate, import-free engine that must account for every unit of work and allocation inside limits you declare. What remains is a five-member decision directory: the prepared rule artifact, the canonical input, the deterministic result with its exact request binding, the eligible portable core, and a derived summary. The raw rule source is deliberately not among them.
- 01Reviewed rule
- 02Strict JSON input
- 03Decision: allow
- 04Checkable portable core
1. The rule
(let ((days (cdr (car input)))
(opened (cdr (car (cdr input)))))
(if (< days 15)
(if opened "deny" "allow")
"deny"))2. The input
{
"days": 14,
"opened": false
}3. One bounded run
lispex rule run \
--source refund-window.lspx \
--input day-14-unopened.json \
--prepare-limits prepare-limits.json \
--eval-limits evaluation-limits.json \
--out decision
lispex rule inspect --dir decision
lispex rule verify --dir decision
lispex rule replay --dir decisionFor the maintained day-14 unopened case, the bounded run returns allow.
rule inspect summarizes the directory without executing it; rule verify checks the exact member set, identities, hashes, and bindings, still without executing; rule replay evaluates the recorded request once, in a fresh evaluator instance, and requires the same result. None of the three confers authority.
What the portable core binds
The semantic rule, the canonical input, the exact limits, the exact evaluator artifact, and the deterministic outcome — enough to know precisely which question was answered, and under which ceilings. Consumed or remaining usage is never part of it.
What the record does not establish
Who ran it, whether it is fresh, whether the policy the rule encodes is fair or correct, whether the same decision was used twice, or any permission to act outside the process.
A decision rule can travel as a deterministic image.
An Image is a canonical picture file that carries a rule’s exact source bytes. This one carries a reviewed refund rule that returns a canonical Decision — the only kind of result Vouch can issue evidence for. Recover the source locally, run it only after the bytes prove canonical, or pin the proved image as the exact source in the Vouch workflow below. The pixels carry integrity, nothing more.
(define days-since-delivery (car input))
(define opened? (car (cdr input)))
(if (<= days-since-delivery 14)
(if opened?
(decision-deny)
(decision-approve))
(decision-deny))From here one path continues below: recover and prove this image, pin it as the exact source, and on Native issue signed Vouch evidence for one exact input. A recipient authenticates that evidence under a trust policy they own, re-executes the rule live on their own machine, and gates locally — and whether anything actually happens next is a separate decision their application makes. The image itself is none of this: not signed evidence, not trust, not authority. It only carries bytes exactly.
Every decision can keep a receipt.
Vouch turns one recorded decision into signed, portable evidence — and keeps evidence strictly separate from permission.
A receipt is a signed record of one run: which rule bytes ran, which input bytes went in, and which decision came out. On the Native release binary, lispex vouch issue produces one by running the reviewed rule itself — the receipt records what actually happened, not what anyone claims. Receipt, source, and input can travel together as a single file, the bundle. Anyone can authenticate a bundle with lispex vouch verify, on Native or npm, and it answers exactly one question: did a key you chose to trust sign these exact bytes? It deliberately answers nothing else.
A bundle cannot choose the request that your gate executes.
Re-execution starts from the request you pin, never from the bundle’s say-so.
Request binding is the rule that your machine only ever re-runs what you asked it to. A bundle proves what its issuer observed; it does not get to pick the rule or the input on your side. So before any re-execution you pin the request yourself: the rule source — a file you hold, or an image that passed the full canonical proof — and the exact input. Verification authenticates the signature first, then compares the bundle against your pins, and only an exact match continues into execution. Pin nothing and verification stays a signature check; it can never reach re-execution or a gate.
Re-execution is a comparison your own machine performs.
The gate succeeds only on exact live agreement, under a trust policy you composed yourself.
lispex vouch gate is a local check with a concrete question: run on this machine, right now, with the pinned request — does the rule still produce exactly the signed result, and is that decision the one I required? Evidence goes in, an exit status comes out. Above it sits the trust policy: a short configuration file you compose and audit yourself, naming the public key you reviewed, the exact evaluator, and the exact rule source or proved image you accept. A validly signed rule your policy does not list is rejected. The policy grants nothing by itself — it only narrows what you are willing to check.
What a passing gate does not give you.
Each boundary below is deliberate. Read a passing report as evidence for your next step — nothing more.
A passing verify or gate report is not a permission, a token, or authority for any external action — whether to actually refund, pay, or ship stays a separate decision your application makes. Request binding proves equality with the request you pinned, not freshness, uniqueness, or replay prevention. An image proves its recovered source bytes are intact, never that they are trusted. npm verifies and authenticates but cannot issue, re-execute, or gate; browser WASM and the Playground evaluate code, nothing more. And nothing from ordinary execution — route locks, measurements, run output — ever becomes Vouch authority.
Run the complete Vouch workflow생각의 원형을 담는 언어.
The language that captures the shape of thought.
Язык, воплощающий форму мысли.