The stable center
Lispex is a small deterministic language for decision rules, which means one input always gives one answer. Rust is the reference implementation and supports all 205 tracked rows of built-in capability. Exact Lispex Images carry the original source bytes and give them back unchanged. Request-Bound Vouch can authenticate a context that a bundle declares, and only on Native, and only with an exact request supplied from outside, can it re-execute the rule and reach a local decision gate. That Native path can explicitly add a compiled artifact derived from the same exact source and require agreement from the verified Rust virtual machine (VM), a program that runs prepared instructions instead of reading your source. The existing tree and Meaning checks still have to pass, where tree means the built-in interpreter that reads your source directly.
The hosted interpreters keep explicit boundaries. Lispex-in-Lispex (LIL), the hosted interpreter written in Lispex, supports all 205 primitive rows counted today. Lispex-in-Topaz (LIT) supports 84 of 205. Rows that LIT does not support refuse to run instead of borrowing behavior from the host. Complete LIL capability coverage is not a claim of whole-language equivalence.
How to read the direction
| Direction | Why it matters | A real completion signal | Not promised |
|---|---|---|---|
| Learnability | a capable language is useless if a new reader cannot write a first rule | runnable lessons, exact results, natural English/Korean/Russian, and tested navigation | a large language, classroom platform, or hidden tutorial state |
| Deterministic product ergonomics | one fixed meaning of the language should be easy to install, inspect, and automate | exact local products, stable diagnostics, and task-first guidance for Native, npm, WebAssembly, and the Playground | identical resource limits everywhere Lispex runs |
| Exact-source workflows | reviewed source should survive travel as a picture byte for byte | proof that the bytes are exactly the ones that went in, exact recovery, explicit execution, and clear failures when a file is damaged | secrecy, signature, a record of where it came from, or authority from how an image looks |
| Request-bound evidence | authentication must not silently become permission | the consumer pinning the source and the input before Native re-runs the rule and checks the gate | freshness, replay prevention, policy correctness, or permission for an external action |
| Checkable decision exchange | a recipient should be able to check an exact decision record and its allowed issuer without learning how the runtime is built | one engine that always gives the same answer, optional checking of who issued the record, an explicit request the recipient pins, and a fresh re-run reported as separate conclusions | signature as freshness, correctness, or permission to act |
| Backend growth with stated limits | another implementation is useful only when you can measure how much of the language it covers | an explicit capability row, a negative control, a record of where it came from, and a receipt | silent fallback or a whole-language equivalence claim |
| Research evidence | comparisons should say what they counted and what they assumed | named corpora, runners, observations, mismatches, and not-comparable cases | proof by test count or a release-date commitment |
Ordered portable-execution direction
The architectural outcomes are deliberately ordered. The stable profile now has complete LIL capability coverage, and Native can lower the complete normalized Core to Core IR, a checked internal form of a rule that is written the same way every time, carrying resolved cells, explicit tail positions, primitive IDs, source anchors, cost identity, and one strict JSON byte representation. The public commands build, validate, and inspect that artifact without executing it or granting authority.
Native now compiles strict Core IR to lispex.bytecode/v1, a bytecode written
the same way every time, rejects malformed structure before execution, and
runs the verified artifact in lispex-rust-vm/v1, the Rust VM with explicit
control. The route that starts from source can select --engine vm. Tree
remains the default and the VM never falls back. The focused tree and VM
comparison records exact intermediate identities and semantic axes, while
honestly labelling both routes as the same Rust lineage.
Compiled execution bound to Vouch is now the limited result of this sequence.
Only lispex.vouch-compiled-artifact/v1, derived again from the consumer's
exact source after authentication and after the request is pinned, can add
current verified Rust VM agreement to the existing tree and Meaning chain.
Ordinary bytecode, the record of which compiler produced an artifact,
artifacts, and reports cannot promote themselves into authority.
Native now also admits the exact separately installed Topaz 5.11
lispex-topaz-vm/v1 product on macOS ARM64. The explicit Topaz bytecode route
and compare-vms bind the provider product, request, result, exact bytecode and
input identities, full-width u64 resources, and zero fallback. Rust remains
the default, no Topaz request, result, or comparison can be supplied to any
Vouch command, and the comparison is evidence with stated limits rather than a
proof of independent equivalence.
Native macOS ARM64 now also has the explicit correctness-first Lispex-to-Topaz route built on ahead-of-time compilation (AOT), which turns a rule into a program before anyone runs it. It emits readable Topaz and a source map from the verified static control graph, consumes only the exact installed Topaz 5.11 compiler, and installs a product that ships without source, while the identities of the source, Core IR, bytecode, generated bundle, artifact, executable, resources, and the zero fallbacks all stay bound. It is execution material outside Vouch, not a new backend family or an equivalence proof. Native can now derive one request and issue a diagnostic receipt that never overwrites an existing one, covering tree, Rust VM, exact Topaz VM, and the matching AOT product. Semantic and comparable-resource axes, lineage, and every fallback remain visible. The receipt grants no authority and does not turn four routes into four independent witnesses.
The stable multi-route product is now public. Native can list four honest routes, write selection locks that record no local path, diagnose exact installations, collect measurements that stay inside stated limits, and run a locked route. A selection lock is a small file that records which route you chose without recording where that product sits on your machine. Rust tree remains the default. There is no discovery, retry, fallback, or Vouch authority derived from Topaz.
Distribution of the portable routes now has a catalog written the same way every time, an installation receipt that records no local path, an offline archive installer with stated limits, and a restricted official fetch path. Native fetches only an exact entry embedded in the binary. The current catalog contains the macOS ARM64 Topaz VM backed by evidence from an installed run and the exact AOT compiler companion, and it omits unsupported targets. Installation stays separate from execution, and the compiler companion still requires a separately selected Rust toolchain at build time. Python, browser, direct WebAssembly, optimization, cross-compilation, and other companion targets remain directions rather than promised dates.
The installed journey is now closed end to end. The same explicit products
survive inventory, selection that records no local path, the doctor
diagnostic, comparison with stated limits, locked execution, and relocation
with unchanged locks. It does not discover another product route or widen the
claim about supported targets.
Native also exposes one local authoring channel that an assistant talks to over standard input and output. An assistant can query the exact installed forms and procedures, run a trusted-source Rust tree example under a size and time cap, resolve a diagnostic, or request one fixed comparison run over tree and Rust, Rust and Topaz, or all four routes. This channel is not a sandbox for hostile source and it does not count all guest work or logical allocation. A maintained journey over the installed product, which keeps no source tree, checks the four tools, exact matching of CLI diagnostics, denied host capabilities, resource termination and recovery, agreement, honest disagreement or unavailability, and cleanup. It does not discover a route, choose an answer, retain source, open a remote service, or create Vouch authority.
The exact evaluator that runs under a fixed limit on work and memory is now public as a separately retained WebAssembly component with no imports. The evaluator is the program that runs the rule. Native embeds those exact bytes and separates preparation from evaluation, deterministic work and logical-allocation limits, semantic outcomes and request refusals, and operational or engine failures. Only eligible deterministic results carry the frozen portable core, the small record that binds the rule, the input, the limits, and the outcome of one run. The evaluator has no host capability, discovery, fallback, or remote transport, and nothing it produces can be promoted into Vouch evidence.
The evaluator for the complete current profile is also public as a second,
separately identified component under the same kind of fixed limit. One
generated authority, closed to anything it does not list, covers all 205
primitive rows, and its full counter of work keeps preparation and evaluation
resources separate, charging before the work and refunding nothing. Native
exposes it only through explicit embed full commands and creates a fresh
instance for every operation. This
does not rename or widen the restricted component, and it adds no discovery,
fallback, host capability, promotion into Vouch evidence, or Topaz admission.
The checkable decision workflow is also public. Native rule run accepts one
reviewed rule, strict JSON input, and exact limits, then creates a five-member
decision directory that holds no source, either completely or not at all. The
inspect and verify commands do not execute the rule. The replay command
uses a fresh instance of the exact evaluator and requires the result and the
portable core to match. This record is checkable and never grants permission
for an external action.
Authenticated decision exchange is now public. One task-first refund path and
exact Native handoff lead to an optional issuer envelope outside the unchanged
evaluator and portable core. Recipient policy, signature validity, request
binding, replay, replay prevention, and external authority stay separate. One
seven-member .lpxdecision bundle with stated size limits and one fixed way of
writing it supports the full Native lifecycle and npm inspection and
authentication, which can verify but never issue. The installed Native and npm
check run, which keeps no source, proves relocation and fresh replay without
turning the bundle into Vouch evidence or permission to act.
What does not move casually
Language semantics do not change just to make a tutorial, backend, or artifact easier to implement. A genuine semantic change must update the runtime specification, Rust implementation, tests, receipts, and public explanation together. Exact Images remain a way of representing source. They are not a new datum and not a compiler. Vouch artifacts remain evidence, not transferable authority.
Current boundaries
- Roadmap directions are not assigned versions, dates, or staffing promises.
- Rust, LIL, and LIT are separately labelled execution families. Generated or packaged variants do not become independent witnesses.
- The historical three-family receipt records 59 agreements across its 144 checked cases. That count of 144 must not be enlarged in prose.
- A future backend or mechanized model closes only the part of the language and the assumptions it explicitly names.
Keep going
Read Philosophy for the decisions behind these limits. Use History when you want the exact chronology of shipped capabilities.