Bounded Evaluator Contract

Frozen contract set

The portable core is the part of the record that can travel on its own. What it binds is listed under Identity and core below.

The provider is the exact WebAssembly bytes named by the bundle manifest, not an arbitrary rebuild or a Lispex version label. A rebuild inherits the guarantee only when its SHA-256 is identical.

Separate complete current-profile component

The public full component is not a renamed restricted profile. It adds the separate lispex/r7rs-rule-current-profile-bounded/1 semantic profile, the lispex-full-vm-meter/1 model that counts work, and the lispex-evaluator/rust-vm-current-profile/1 component identity over all 205 generated primitive rows with zero Deferred rows. The existing interface, value codec, transcript, and portable-core schemas were audited as sufficient and retain their exact v1 meanings. Full artifacts use the distinct LPXFAR01 envelope while restricted LPXART01 artifacts and historical receipts remain unchanged.

Interface and lifecycle

The interface is the fixed set of functions the module offers and the fixed way data is passed in and out. The module has zero imports, one memory with 18 initial and 256 maximum pages, and only the allocation, deallocation, interface-version, prepare, and evaluate functions plus standard memory boundary globals. Requests are size-limited, length-delimited, big-endian values.

Every operation gets a fresh Wasmtime Store, Instance, memory, allocator, guest heap, interner, cells, continuations, work counter, transcript, and result buffer. An immutable compiled Module may be shared only under the exact WebAssembly SHA-256. Instance pooling is not admitted.

Separate resource domains

Preparation owns raw_source_bytes, prepare_work, prepare_logical_allocation, and syntax_depth. Evaluation owns canonical_input_bytes, eval_work, eval_logical_allocation, semantic_frames, traversal_depth, output_bytes, diagnostic_bytes, transcript_bytes, transcript_events, and result_bytes.

Work is a versioned deterministic tariff, not CPU time. Logical allocation is defined by the model, not Rust object size, allocator capacity, or pointer width. Charges occur before effects, never refund, use full u64, and fail on the first reservation that would exceed its named limit. Proper tail calls do not consume semantic non-tail frames.

Consumed or remaining usage is never part of the portable core. A tariff, axis, unit, ordering, overflow, depth, or failure-rule change creates a new model ID, and budgets are not converted between models.

Identity and core

The core separates the identities of the exact submitted source bytes, the source in its one fixed form, the semantic rule, the input in its one fixed form, the resource contract, the request, the artifact that ran the rule, the evaluation, the transcript, and the result. Hash framing is the normative lispex.evaluation-identity/v1 length-delimited SHA-256 construction.

Only deterministic semantic outcomes and deterministic request refusals carry a core. Operational interruptions and engine faults cannot carry one. An issuer may sign completed core bytes outside the program that ran the rule, but that envelope does not change their category.

Restricted profile

The first profile admits the closed operation set qualified by the bundle. The ordinary full lispex-profile-1.5 tree interpreter remains separate. Unsupported forms or primitives fail closed before the virtual machine runs anything. The provider does not invoke tree, Rust route products, Topaz, the ahead-of-time compiled product, an older program that runs rules, or any fallback.

Native decision-directory contract

The Native rule wrapper exposes this limited runner as one atomic local workflow.

rule run -> inspect -> verify -> replay

rule run accepts exact source and strict JSON files plus separate preparation and evaluation limits. JSON objects become records, arrays become vectors, strings, booleans, and exact integers keep their value kinds, and null becomes the empty list. Duplicate object keys, inexact numbers, unsupported values, or trailing data are deterministic request refusals.

A successful run creates exactly five ordinary files.

The output directory is created without overwriting an existing path. inspect and verify never evaluate. replay uses a fresh instance of the runner and requires the reproduced result and portable core to match. Missing, tampered, extra, or symbolic-link members fail closed.

This workflow is provided by the Native product. It does not reconstruct or retain submitted source, discover another program to run the rule, invoke fallback, access a host capability, contact a remote service, create or upgrade Vouch evidence, or authorize an external action.

Distribution and retention

Native contains the exact provider bytes. The release also publishes the WebAssembly bundle, manifest, golden vectors, verifier material, the software bill of materials and dependency dispositions, safety evidence, and append-only release-DAG records. A security update creates a new artifact identity and admission. Old receipts remain verifiable with retained old bytes and contracts but may be refused for new adversarial evaluation.

This component has no Topaz build dependency. The separate ahead-of-time compiled component keeps its own exact Topaz compiler pin. A Topaz consumer must pin this component by its exact hash in a later, separately admitted release.

Non-guarantees

The contract does not provide confidentiality, issuer authentication, Vouch authority, rule correctness, provenance, freshness, external-action authorization, timing secrecy, cache isolation, or microarchitectural side-channel resistance. Browser support is not part of this release.

Keep going

Use Evaluate an Untrusted Rule for the Native workflow.