Lispex 2.0 specification · not released · Tested product not run · Examples not run
# Embedding and packages
Call a prepared rule with canonical data and finite limits. Validate its artifacts and package before evaluation.
Canonical: /v2.0/en/docs/tools/embedding
Document revision: 2.0-draft-1. Content locale: en. Translation: current.
- language: `lispex`
- languageVersion: `2.0`
## Scope
Calling applications embed Lispex by supplying data to a prepared rule and receiving its canonical outcome. This chapter defines the host interface, artifact admission, packages, and the Topaz connection.
The examples pair rule source with a documentation request. The request names fixed semantics and symbolic finite limits. Artifact descriptions and limit defects describe cases for a future product adapter. They do not define public JSON fields, executable artifacts, or a byte encoding.
## Value interface
The host interface is the public surface through which a calling application prepares a rule and submits an input. The value-only ABI carries canonical data across that surface. Host objects and callable host functions are outside its data domain.
[Datum](/v2.0/en/docs/language/values#lispex.section.v2.values.datum) defines portable values. [Procedures](/v2.0/en/docs/language/procedures) defines the entry and its single result. [Profiles and value interchange](/v2.0/en/docs/profiles/) defines admission schemas and the canonical codec.
### Pass data across the host boundary
The calling application supplies one canonical Datum as input. Public embedding interfaces reject host callbacks and host object references. Guest code receives values without access to host services.
**Why**
A callable host function could read external state or perform work outside the language resource model. Passing captured values keeps authority with the calling application.
Claim: `lispex.claim.v2.embedding.value-only-call` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "embedding-input",
"inputDomain": "Datum",
"surface": "public"
},
"result": {
"kind": "value-only-host-boundary",
"hostCallbacks": false,
"hostObjectReferences": false,
"ambientAuthority": false
},
"pendingCases": [
"Native, npm, and WASM need cases for every portable datum kind, nested host references, callback injection routes, and supported architecture."
]
}
```
### Pass an exact value to a rule
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "41"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Evaluation returns the exact integer 42 as one canonical result datum. Product invocation awaits its 2.0 adapter."
}
```
The host supplies 41 as a value. The rule uses only that input and its fixed library. Datum and the canonical value codec are defined in Values and text and Profiles and value interchange.
### Reject a host callback as input
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "host-callback",
"behavior": "returns the exact integer 42"
}
}
],
"admission": "Attempt to supply a host function as the input datum.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Admission rejects the host callback as a non-Datum input. Neither the entry nor the callback is invoked. Product invocation awaits its 2.0 adapter."
}
```
A claim that the callback is pure does not change its input domain. The documentation request describes the attempted injection without installing a callable host service.
The public API separates prepare and evaluate. Preparation returns an opaque verified handle to an immutable rule. A product that transports versioned prepared bytes validates them before use. The caller supplies the canonical input and named evaluation limits for each call.
The caller can first select [record admission](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.record-input).
Record adaptation and its output encoding use the profile host account.
The evaluator then decodes the resulting canonical input under EvaluationLimits.
Its result encoding uses the same evaluation account.
The [boundary event schedule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.boundary-events) is the definition home for those events.
Identical canonical input gives identical evaluation events under the same program, fixed semantics, and limits.
The input construction path does not change those events.
[Preparation and modules](/v2.0/en/docs/tools/prepare) defines the closed source bundle, dependency resolution, and cache behavior. [Resources](/v2.0/en/docs/language/resources) defines work, logical allocation, frames, and channel budgets. Result encoding and diagnostic production follow those resource rules. A raw interpreter interface cannot bypass the public value and limit checks.
When a profile requires additional host checks, the caller supplies the separate finite [profile host budget](/v2.0/en/docs/profiles/#lispex.rule.v2.profiles.profile-work-separation). The host records [profile work identity](/v2.0/en/docs/profiles/receipt-and-replay#lispex.section.v2.receipt-and-replay.identities) without adding that budget to either base request.
The host returns an admission report for a refusal before entry. After evaluation it returns qualification and evidence results in a separate [profile work report](/v2.0/en/docs/profiles/receipt-and-replay#lispex.section.v2.receipt-and-replay.execution-evidence). That report preserves the completed canonical outcome and evaluation receipt eligibility.
### Prepare a rule and evaluate an input
Preparation accepts a closed source bundle and preparation limits. Evaluation accepts an immutable prepared rule, one canonical input, and evaluation limits. Success returns one canonical Datum. A convenience call performs the same two phases.
**Why**
A prepared rule fixes its program and dependencies before evaluation. Separate requests can reuse that rule while supplying independent inputs and evaluation budgets.
Claim: `lispex.claim.v2.embedding.typed-phases` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "typed-embedding-request",
"phases": [
"prepare",
"evaluate"
],
"preparedRule": "immutable"
},
"result": {
"kind": "typed-embedding-outcome",
"prepareBudget": "separate",
"evaluationBudget": "per-request",
"successValueCount": 1,
"successDomain": "Datum"
},
"pendingCases": [
"Native, npm, and WASM need direct and convenience API cases for fresh and reused prepared rules on every supported engine and architecture.",
"Boundary cases must cover zero results, multiple results, and nested procedures in otherwise portable data."
]
}
```
### Reuse one immutable prepared rule
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "41"
}
},
{
"input": {
"kind": "integer",
"value": "7"
}
}
],
"preparation": "Prepare this closed bundle once and keep its verified immutable handle.",
"execution": "Evaluate the two inputs as separate requests with independent copies of the same finite evaluation limits.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The two requests return the exact integers 42 and 8. Both use the same unchanged prepared rule and separate evaluation budgets. Product invocation awaits its 2.0 adapter."
}
```
The handle is opaque to the caller. Reuse preserves the prepared program and starts each evaluation with its own declared limits. The counters here count requests and do not assign resource tariffs.
### Reject a procedure at the result boundary
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(lambda (value) value)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Evaluation reaches the result boundary with a procedure. The boundary reports a language failure and returns no datum. Product invocation awaits its 2.0 adapter."
}
```
The inner procedure is a valid internal value. A public result must be portable data. The failure uses the [entry result diagnostic](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.catalog).
### Supply the complete bundle and root
SourceBundleBytes is one canonical `lispex.datum/2` packet containing the record below.
The [Datum codec](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.datum-byte-format) defines every tag, count, and UTF-8 octet.
A record is a proper association list of pairs from exact String keys to their field values.
Each entry has its key in car and its value in cdr.
Keys occur once in unsigned UTF-8 byte order.
Every listed field is required. Unknown fields are refused.
Vectors preserve the order shown by their schema.
| Record | Exact fields | Datum types |
| --- | --- | --- |
| SourceBundle | `format`, `modules`, `root` | String, Vector of ModuleSource, String |
| ModuleSource | `name`, `source` | String, Bytevector |
| SourceBundle format | `lispex.source-bundle/2` | Exact String |
`name` and `root` contain decoded Identifier scalars.
They may be empty. They preserve case and normalization.
The source token for a Unicode name uses the [barred identifier grammar](/v2.0/en/docs/language/source#lispex.rule.v2.source.reader-grammar).
The bars and escapes are absent from the name field.
The source field preserves all submitted source octets.
Paths, timestamps, and display labels are absent from this record.
ModuleSource records use nondecreasing unsigned UTF-8 name order.
Typed callers sort this vector before encoding it.
Equal adjacent names remain representable until the existing duplicate module check rejects them.
Every submitted source module participates in preparation.
The fixed package supplies the matching immutable library bytes as a separate dependency.
Preparation performs no dependency lookup or file access.
The [closed bundle checks](/v2.0/en/docs/tools/prepare#lispex.rule.v2.prepare.closed-bundle) retain their existing order.
Duplicate module names, missing root membership, and source declaration mismatches keep their existing preparation failures.
A root field is required even for one source module.
The root module's source declaration selects its entry under the [entry rule](/v2.0/en/docs/language/procedures#lispex.rule.v2.procedures.entry-selection).
There is no host entry override.
| Product operand | Exact submitted bytes | Selection |
| --- | --- | --- |
| CLI `--bundle FILE` | SourceBundleBytes | Required bundle root |
| CLI `--artifact FILE` | PreparedArtifactBytes | Validated prepared root and entry |
| Typed prepare | Canonical SourceBundleBytes from the typed record | Required bundle root |
| Typed load | Exact immutable PreparedArtifactBytes | Validated prepared root and entry |
The [CLI grammar](/v2.0/en/docs/tools/run#lispex.rule.v2.cli-and-diagnostics.command-forms) is unchanged.
The product reads these bytes before entering the value-only evaluator.
**Why**
One explicit root removes host naming conventions. Complete source bytes make preparation and source provenance reproducible.
Claim: `lispex.claim.v2.embedding.source-bundle` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "host-contract",
"operation": "source-bundle",
"language": "2.0"
},
"result": {
"kind": "canonical-source-bundle",
"format": "lispex.source-bundle/2",
"root": "required-decoded-identifier",
"fields": [
"format",
"modules",
"root"
],
"entryOverride": false
},
"pendingCases": [
"Native, npm, and WASM product adapters must exercise valid packets, first refusals, finite limits, ownership, and architecture boundaries."
]
}
```
### Keep the decoded Unicode root
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module |규칙|
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "규칙",
"moduleSources": [
{
"name": "규칙",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"bundleRoot": "규칙",
"moduleName": "규칙",
"inputInteger": "41"
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The bundle uses the raw Unicode name and its source uses barred syntax. Product invocation awaits its 2.0 adapter."
}
```
### Require root even for one module
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"mutation": "Remove only the required root field from a one-module bundle."
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "A missing bundle root is refused before source preparation. Product invocation awaits its 2.0 adapter."
}
```
### Use phase-specific typed calls
Native exposes Rust and C bindings. npm and browser WASM expose the TypeScript binding.
Every binding uses the same byte ABI below.
Datum input is supplied as canonical bytes.
Host functions, object references, implicit string conversion, and callable properties are refused.
| Shared type | Exact meaning |
| --- | --- |
| Bytes | Owned immutable octet sequence |
| Nat | Mathematical nonnegative integer |
| Identity | Complete canonical IdentityBytes from [Identity](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.identity-encoding) |
| FixedSelection | Required fields `language`, `library`, `resource-model`, `unicode` |
| FixedSelection field types | String `2.0`, Identity bytevector, Identity bytevector, Identity bytevector |
| PrepareLimits | The complete preparation record from [Resources](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.model-definition) |
| EvaluationLimits | The complete evaluation record from [Resources](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.model-definition) |
| CanonicalInputBytes | The complete input packet from [Profiles](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.datum-byte-format) |
| RecordInputBytes | The explicit [record input packet](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.record-input) |
| ProfileRequestBytes | The complete [profile request packet](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.profile-declarations) |
| ProfileSelection | The builtin String `base` or `vouch/2` from Profiles |
| ProfileHostBudget | The complete [host budget record](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.profile-work-contract) with its required host model metadata |
| ProfileHostBudgetBytes | The encoding owned by the same Profiles contract |
| PreparedFormat | Exact String `resolved/1` or `bytecode/1` |
| CommandResultBytes | The complete imported [command result](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.command-result-format) |
| PreparedRule | Private issuer-bound immutable verified program handle |
| PrepareReply | Complete command result and a handle only on successful sealing |
| TraceOptions | Closed Nat fields `allocation`, `capacity`, `work` under [Resources](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.trace-reservations) |
The following local byte names specify the C spans and the shared encoders.
D is the complete Datum packet encoding from [Identity](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.record-encoding).
Each local encoding imports its record meaning from the type table.
| Encoding | Exact packet |
| --- | --- |
| FixedSelectionBytes | D of FixedSelection |
| PrepareLimitsBytes | D of PrepareLimits |
| EvaluationLimitsBytes | D of EvaluationLimits |
| PreparedFormatBytes | D of the PreparedFormat String |
| TraceOptionsBytes | D of false or the TraceOptions record |
| ProfileSelectionBytes | D of the ProfileSelection String |
SourceBundleBytes and PreparedArtifactBytes retain their existing input contracts.
RecordInputBytes, ProfileRequestBytes, and ProfileHostBudgetBytes retain their Profiles definitions.
CanonicalInputBytes is a complete packet.
It is not an extra bytevector wrapper around that packet.
FixedSelection identifies the package's fixed Unicode 17.0.0 and library contracts.
Each identifier must equal the corresponding validated package dependency.
Limits are required for every performed phase.
Each Nat is a Datum integer with the integer tag and exact nonnegative value.
Nat fields are never decimal Strings or rational values.
Zero is finite and follows the inclusive limit rule.
Missing fields, unknown fields, negative values, nonintegers, and unlimited values fail admission.
An integer beyond the selected model's representation limit uses the existing overflow refusal.
The common preset expands to the same complete limit records before these calls.
The [cost freeze](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers) owns all numeric values.
The [signature fixture](/v2.0/en/docs/tools/embedding#lispex.example.v2.embedding.handle-independent-evaluations) defines the host signatures.
Its byte parameters use the complete packets named in the type table.
Rust Bytes owns a byte slice. Rust Nat has a private exact integer representation.
Rust `nat` returns BuildResult from canonical unsigned decimal text without a machine integer cast.
Its accepted text is `0` or a nonzero ASCII digit followed by ASCII digits.
Signs, whitespace, leading zeroes, and empty text are refused.
TypeScript Bytes is a copied Uint8Array. TypeScript Nat is a bigint validated before encoding.
TypeScript constructors take the validated Product and return BuildResult.
They issue privately branded records from primitive arguments and copied byte views.
Encoders read the private records without calling user properties or iterators.
Forged records and shared mutable backing storage are refused before encoding.
Byte copying uses typed array internal slots. It performs no numeric coercion or user callback.
The C binding uses opaque types and byte spans for the same records.
BuildResult contains either the constructed value or one complete CommandResultBytes with its admission report.
The [host result mapping](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.command-result-format) also defines Open, load, and export reports.
A constructor validates arguments from left to right under the Product ingress bounds.
A value, type, brand, or ownership failure uses `admission` and `request.invalid`.
The field is the parameter name and the reason is `invalid-value`.
The Rust Nat constructor uses field `text`.
Constructors check exact syntax and trusted ingress bounds.
The phase invocation checks its selected model's representation limits and uses reason `overflow` when needed.
No failed constructor enters a guest or creates an evaluation receipt.
TypeScript throws only TransportFailure for a transport failure.
Completed admission refusals and semantic failures remain command result data.
Rust drop, TypeScript dispose, and C destroy revoke the handle.
TypeScript disposal and C destruction are idempotent. A disposed, forged, or foreign handle returns `admission` and `request.invalid` before guest entry.
Its field is `rule` and its reason is `invalid-value`.
A C caller supplies valid live spans and writable output pointers. Invalid native pointers violate the transport precondition.
The wrapper associates each handle with its issuing Product.
It exposes no pointer, seal, numeric handle ID, or verified flag as portable data.
Export produces portable bytes. Load validates those bytes again under preparation limits.
Each evaluation initializes every admitted module under the [initialization rule](/v2.0/en/docs/tools/prepare#lispex.rule.v2.prepare.module-initialization).
Reuse retains only verified immutable program data.
It preserves the complete evaluation event sequence and canonical receipt.
A convenience run performs prepare or load followed by evaluate with both phase limits.
It returns the first phase failure and never evaluates after preparation refusal.
The explicit profile wrappers use the same private Product and PreparedRule types.
They keep the [profile host account](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.profile-work-separation) separate from evaluation.
| Wrapper | Rust | TypeScript | C |
| --- | --- | --- | --- |
| Record admission | admit_record | admitRecord | lispex_v2_admit_record |
| Profile evaluation | evaluate_profile | evaluateProfile | lispex_v2_evaluate_profile |
Record admission takes RecordInputBytes, an explicit ProfileSelection, and ProfileHostBudget.
It requires no program handle, library, declaration, schema, or evidence.
Its successful CommandResultBytes has payload kind input and the complete CanonicalInputBytes.
It has no canonical evaluation outcome or evaluation receipt.
Its command option is empty.
The [report envelope](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.command-result-format) owns this mapping.
Record admission remains a host operation.
It adds no evaluator operation or CLI command.
Profile evaluation takes a PreparedRule, CanonicalInputBytes, EvaluationLimits, ProfileRequestBytes, ProfileHostBudget, and the existing trace selection.
The profile request is required even for base.
It uses the canonical base declaration when base is selected.
The wrapper creates the ProfileEvaluation record defined in the byte ABI below.
The call decodes canonical input once under the evaluation account.
It checks the input schema under the host account.
It then resumes the same evaluation state for module initialization and entry.
Qualification and required evidence follow the existing Profiles schedule.
The result uses complete CommandResultBytes and preserves the canonical outcome and eligible receipt.
No callback, public continuation, or repeated decoder joins these stages.
The two wrappers create separate host operations and accounts.
Record admission does not transfer its remaining budget into profile evaluation.
Its returned canonical bytes are an explicit input to the later call.
Their different submissions have different profile work bindings.
Changing only the selected host model leaves the program and evaluation request unchanged.
The ProfileHostBudget type fixes its format to lispex.profile-host-budget/2.
Its resource_model field comes from the explicit IdentityBytes argument.
Its six numeric axes retain the exact meanings and order defined in Profiles.
The TypeScript profileHostBudget constructor requires that model argument.
The Rust record requires the resource_model field.
The C budget span contains complete ProfileHostBudgetBytes.
No binding substitutes the evaluation model for missing host metadata.
The selected host model must support the profile work contract before that account is used.
Construction uses the trusted Product ingress account.
The constructed budget selects only the subsequent profile host account.
**Why**
Named input packets preserve the same boundary across host languages.
Explicit record admission makes conversion and its budget visible.
The host model remains separate from evaluation semantics.
One coordinated call preserves input decoding charges and schema order.
Claim: `lispex.claim.v2.embedding.typed-interface` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "host-contract",
"operation": "typed-interface",
"language": "2.0"
},
"result": {
"kind": "typed-host-interface",
"hosts": [
"rust",
"c",
"typescript"
],
"phases": [
"prepare",
"load",
"evaluate",
"export",
"graph"
],
"opaqueHandle": true,
"numericLimits": "cost-model-freeze",
"hostWrappers": [
"admit_record",
"evaluate_profile"
],
"recordAdmissionNeedsProgram": false,
"recordAdmissionPayload": "input",
"recordAdmissionReceipt": false,
"hostBudgetEncoding": "ProfileHostBudgetBytes",
"hostModelMetadataRequired": true,
"laterProfileEvaluationAccount": "independent"
},
"pendingCases": [
"Native, npm, and WASM product adapters must exercise valid packets, first refusals, finite limits, ownership, and architecture boundaries."
]
}
```
### Refuse incomplete and inexact limits
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"cases": [
"Remove work from otherwise complete finite limits.",
"Set work to exact integer -1.",
"Add timeout to otherwise complete finite limits."
]
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "All products reject missing work, negative work, and an unknown timeout field. Product invocation awaits its 2.0 adapter."
}
```
### Reuse only the immutable program
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"sequence": [
"prepare",
"evaluate 41",
"release",
"evaluate 7",
"release",
"export resolved/1",
"load into a new instance",
"evaluate 41"
]
}
}
```
File: `rust-signatures.txt`
```lispex
pub struct Product { private: private::ProductState }
pub struct PreparedRule { private: private::SealedProgram }
pub struct Nat { private: private::ExactNatural }
pub type Bytes = Box<[u8]>;
pub type IdentityBytes = Bytes;
pub type CanonicalInputBytes = Bytes;
pub type RecordInputBytes = Bytes;
pub type ProfileRequestBytes = Bytes;
pub type PreparedArtifactBytes = Bytes;
pub type CommandResultBytes = Bytes;
pub type PackageBytes = Bytes;
pub type PackageMetadataBytes = Bytes;
pub struct ModuleSource { pub name: String, pub source: Bytes }
pub struct SourceBundle { pub modules: Vec, pub root: String }
pub struct FixedSelection {
pub language: String, pub library: IdentityBytes,
pub resource_model: IdentityBytes, pub unicode: IdentityBytes,
}
pub struct PrepareLimits {
pub allocation: Nat, pub diagnostic: Nat, pub frames: Nat,
pub input: Nat, pub result: Nat, pub work: Nat,
}
pub struct EvaluationLimits {
pub allocation: Nat, pub diagnostic: Nat, pub frames: Nat,
pub input: Nat, pub result: Nat, pub work: Nat,
}
pub struct ProfileHostBudget {
pub resource_model: IdentityBytes,
pub work: Nat, pub allocation: Nat, pub frames: Nat,
pub input: Nat, pub report: Nat, pub evidence: Nat,
}
pub enum ProfileSelection { Base, Vouch2 }
pub struct TraceOptions { pub allocation: Nat, pub capacity: Nat, pub work: Nat }
pub enum PreparedFormat { Resolved1, Bytecode1 }
pub enum PrepareReply {
Prepared { rule: PreparedRule, report: CommandResultBytes },
Refused { report: CommandResultBytes },
}
pub enum BuildResult { Value(T), Refused { report: CommandResultBytes } }
pub fn nat(product: &Product, text: &str) -> BuildResult;
pub enum TransportFailure { InvalidCall, HostFailure }
pub trait Host {
fn prepare(&self, bundle: SourceBundle, selection: FixedSelection,
limits: PrepareLimits) -> Result;
fn load(&self, artifact: PreparedArtifactBytes, selection: FixedSelection,
limits: PrepareLimits) -> Result;
fn evaluate(&self, rule: &PreparedRule, input: CanonicalInputBytes,
limits: EvaluationLimits, trace: Option)
-> Result;
fn admit_record(&self, record: RecordInputBytes, profile: ProfileSelection,
budget: ProfileHostBudget) -> Result;
fn evaluate_profile(&self, rule: &PreparedRule, input: CanonicalInputBytes,
limits: EvaluationLimits, profile_request: ProfileRequestBytes,
budget: ProfileHostBudget, trace: Option)
-> Result;
fn export(&self, rule: &PreparedRule, format: PreparedFormat,
limits: PrepareLimits) -> Result;
fn graph(&self, rule: &PreparedRule, limits: PrepareLimits)
-> Result;
}
// Product implements Host. nat uses canonical unsigned decimal text.
// Byte aliases denote complete packets from their owning contracts.
// ProfileHostBudget encoding writes its fixed format and explicit host model.
// Base evaluate writes profile false. evaluate_profile writes ProfileEvaluation.
// admit_record runs only the separate host record operation.
// Private fields and the private module are inaccessible to callers.
```
File: `typescript-signatures.d.ts`
```lispex
export type Bytes = Uint8Array;
export type IdentityBytes = Bytes;
export type CanonicalInputBytes = Bytes;
export type RecordInputBytes = Bytes;
export type ProfileRequestBytes = Bytes;
export type PreparedArtifactBytes = Bytes;
export type CommandResultBytes = Bytes;
export type PackageBytes = Bytes;
export type PackageMetadataBytes = Bytes;
export type Nat = bigint;
export type PreparedFormat = 'resolved/1' | 'bytecode/1';
export type ProfileSelection = 'base' | 'vouch/2';
export declare class Product { private constructor(); private readonly brand; }
export declare class PreparedRule { private constructor(); private readonly brand; }
export declare class ModuleSource { private constructor(); private readonly brand; }
export declare class SourceBundle { private constructor(); private readonly brand; }
export declare class FixedSelection { private constructor(); private readonly brand; }
export declare class PrepareLimits { private constructor(); private readonly brand; }
export declare class EvaluationLimits { private constructor(); private readonly brand; }
export declare class ProfileHostBudget { private constructor(); private readonly brand; }
export declare class TraceOptions { private constructor(); private readonly brand; }
export declare class TransportFailure extends Error {
readonly kind: 'invalid-call' | 'host-failure';
}
export type BuildResult =
| Readonly<{ kind: 'value'; value: T }>
| Readonly<{ kind: 'refused'; report: CommandResultBytes }>;
export type PrepareReply =
| Readonly<{ kind: 'prepared'; rule: PreparedRule; report: CommandResultBytes }>
| Readonly<{ kind: 'refused'; report: CommandResultBytes }>;
export declare function moduleSource(p: Product, name: string, source: Bytes): BuildResult;
export declare function sourceBundle(p: Product, root: string, ...modules: ModuleSource[]): BuildResult;
export declare function fixedSelection(p: Product, language: '2.0', library: IdentityBytes,
resourceModel: IdentityBytes, unicode: IdentityBytes): BuildResult;
export declare function prepareLimits(p: Product, allocation: Nat, diagnostic: Nat, frames: Nat,
input: Nat, result: Nat, work: Nat): BuildResult;
export declare function evaluationLimits(p: Product, allocation: Nat, diagnostic: Nat, frames: Nat,
input: Nat, result: Nat, work: Nat): BuildResult;
export declare function profileHostBudget(p: Product, resourceModel: IdentityBytes,
work: Nat, allocation: Nat, frames: Nat, input: Nat, report: Nat,
evidence: Nat): BuildResult;
export declare function traceOptions(p: Product, allocation: Nat, capacity: Nat, work: Nat): BuildResult;
export declare function prepare(p: Product, bundle: SourceBundle, selection: FixedSelection,
limits: PrepareLimits): PrepareReply;
export declare function load(p: Product, artifact: PreparedArtifactBytes, selection: FixedSelection,
limits: PrepareLimits): PrepareReply;
export declare function evaluate(rule: PreparedRule, input: CanonicalInputBytes,
limits: EvaluationLimits, trace: TraceOptions | null): CommandResultBytes;
export declare function admitRecord(p: Product, record: RecordInputBytes,
profile: ProfileSelection, budget: ProfileHostBudget): CommandResultBytes;
export declare function evaluateProfile(rule: PreparedRule, input: CanonicalInputBytes,
limits: EvaluationLimits, profileRequest: ProfileRequestBytes,
budget: ProfileHostBudget, trace: TraceOptions | null): CommandResultBytes;
export declare function exportPrepared(rule: PreparedRule, format: PreparedFormat,
limits: PrepareLimits): CommandResultBytes;
export declare function graph(rule: PreparedRule, limits: PrepareLimits): CommandResultBytes;
export declare function dispose(rule: PreparedRule): void;
```
File: `c-signatures.h`
```lispex
#include
#include
typedef struct lispex_v2_product lispex_v2_product;
typedef struct lispex_v2_prepared lispex_v2_prepared;
typedef struct { const uint8_t *data; size_t len; } lispex_v2_view;
typedef struct { uint8_t *data; size_t len; } lispex_v2_bytes;
enum lispex_v2_transport { LISPEX_V2_REPLY = 0, LISPEX_V2_INVALID_CALL = 1, LISPEX_V2_HOST_FAILURE = 2 };
uint32_t lispex_v2_prepare(const lispex_v2_product *product,
lispex_v2_view bundle, lispex_v2_view selection, lispex_v2_view limits,
lispex_v2_prepared **out_rule, lispex_v2_bytes *out_reply);
uint32_t lispex_v2_load(const lispex_v2_product *product,
lispex_v2_view artifact, lispex_v2_view selection, lispex_v2_view limits,
lispex_v2_prepared **out_rule, lispex_v2_bytes *out_reply);
uint32_t lispex_v2_evaluate(const lispex_v2_prepared *rule,
lispex_v2_view input, lispex_v2_view limits, lispex_v2_view trace,
lispex_v2_bytes *out_reply);
uint32_t lispex_v2_admit_record(const lispex_v2_product *product,
lispex_v2_view record, lispex_v2_view profile, lispex_v2_view budget,
lispex_v2_bytes *out_reply);
uint32_t lispex_v2_evaluate_profile(const lispex_v2_prepared *rule,
lispex_v2_view input, lispex_v2_view limits, lispex_v2_view profile_request,
lispex_v2_view budget, lispex_v2_view trace, lispex_v2_bytes *out_reply);
uint32_t lispex_v2_export(const lispex_v2_prepared *rule,
lispex_v2_view format, lispex_v2_view limits, lispex_v2_bytes *out_reply);
uint32_t lispex_v2_graph(const lispex_v2_prepared *rule,
lispex_v2_view limits, lispex_v2_bytes *out_reply);
void lispex_v2_prepared_destroy(lispex_v2_prepared **rule);
void lispex_v2_bytes_destroy(lispex_v2_bytes *bytes);
/* bundle contains SourceBundleBytes. artifact contains PreparedArtifactBytes.
* selection contains FixedSelectionBytes.
* prepare, load, export, and graph limits contain PrepareLimitsBytes.
* evaluate and evaluate_profile limits contain EvaluationLimitsBytes.
* input contains CanonicalInputBytes. record contains RecordInputBytes.
* profile contains ProfileSelectionBytes.
* profile_request contains ProfileRequestBytes.
* budget contains ProfileHostBudgetBytes with explicit resource_model.
* trace contains TraceOptionsBytes. format contains PreparedFormatBytes.
* out_reply contains complete CommandResultBytes.
* Base evaluate writes profile false. evaluate_profile writes ProfileEvaluation.
* admit_record never enters the raw evaluator ABI.
* Destroy sets the caller's pointer and length to zero.
* Nonzero transport status leaves outputs zero and exposes no receipt.
* A completed refusal has status zero, a report, and no prepared handle.
*/
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Independent evaluations reuse the program and preserve canonical outcomes and receipts. Product invocation awaits its 2.0 adapter."
}
```
### Admit a record before profile evaluation
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input)))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified fixed evaluation resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "one complete finite EvaluationLimits record sufficient for the case"
},
"fixtureParameterTypes": {
"W": "exact nonnegative integer",
"A": "exact nonnegative integer",
"F": "exact nonnegative integer",
"I": "exact nonnegative integer",
"R": "exact nonnegative integer",
"E": "exact nonnegative integer"
},
"budgetNotation": "Symbolic fields name finite fixture parameters. They are not public serialized strings.",
"operation": "typed record admission followed by typed profile evaluation",
"selectedProfile": "base",
"recordInput": {
"format": "lispex.record/2",
"value": [
"record",
[
[
"x",
[
"datum",
{
"kind": "integer",
"value": "7"
}
]
]
]
]
},
"recordBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified explicitly selected host model",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"evaluationProfileBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified explicitly selected host model",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"budgetConstraints": "Both complete budgets are finite and sufficient. Each call opens its own account.",
"profileRequest": "Complete ProfileRequestBytes for the canonical base declaration of the verified program",
"calls": [
"admit_record with the record packet, base selection, and recordBudget",
"evaluate_profile with the returned input payload bytes, verified rule, fixed evaluation limits, explicit profile request, evaluationProfileBudget, and trace false"
],
"apiBindings": {
"rust": [
"admit_record",
"evaluate_profile"
],
"typescript": [
"admitRecord",
"evaluateProfile"
],
"c": [
"lispex_v2_admit_record",
"lispex_v2_evaluate_profile"
]
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Record admission returns canonical input without an evaluation receipt. A later profile call uses its own host account and one evaluation decode. Product invocation awaits its 2.0 adapter."
}
```
### Select the host model explicitly
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input)))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified fixed evaluation resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "one complete finite EvaluationLimits record sufficient for the case"
},
"fixtureParameterTypes": {
"W": "exact nonnegative integer",
"A": "exact nonnegative integer",
"F": "exact nonnegative integer",
"I": "exact nonnegative integer",
"R": "exact nonnegative integer",
"E": "exact nonnegative integer"
},
"budgetNotation": "Symbolic fields name finite fixture parameters. They are not public serialized strings.",
"operation": "compare two evaluate_profile calls",
"canonicalInput": {
"kind": "integer",
"value": "7"
},
"profileRequest": "The same complete ProfileRequestBytes for the canonical base declaration",
"profileHostBudgets": [
{
"format": "lispex.profile-host-budget/2",
"resource_model": "verified supported host model A",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
{
"format": "lispex.profile-host-budget/2",
"resource_model": "verified supported host model B",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
}
],
"constraints": "A and B are distinct supported host model identities. All six numeric host limits are equal and sufficient in both calls. The program, input, evaluation model, evaluation limits, and profile declaration are identical.",
"trace": false
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Changing only the explicit host model changes the profile work binding and preserves the evaluation request and receipt. Product invocation awaits its 2.0 adapter."
}
```
### Encode one closed host request
The ABI identifier is `lispex.host/2`.
HostRequestBytes is one canonical `lispex.datum/2` packet containing a closed record.
It uses the record representation in [SourceBundle](/v2.0/en/docs/tools/embedding#lispex.rule.v2.embedding.source-bundle).
All nested records use the same representation.
`Bytes(T)` is a Bytevector containing one complete canonical T packet.
The outer packet adds no normalization or alternate encoding to imported bytes.
| Record | Required fields and values |
| --- | --- |
| HostRequest | `body` as the selected body record, `format` as String `lispex.host/2`, `operation` as the operation String |
| prepare body | `bundle` as Bytes(SourceBundleBytes), `limits` as PrepareLimits, `selection` as FixedSelection |
| load body | `artifact` as Bytes(PreparedArtifactBytes), `limits` as PrepareLimits, `selection` as FixedSelection |
| evaluate body | `input` as Bytes(CanonicalInputBytes), `limits` as EvaluationLimits, `profile` as false or ProfileEvaluation, `trace` as false or TraceOptions |
| export body | `format` as PreparedFormat, `limits` as PrepareLimits |
| graph body | `limits` as PrepareLimits |
| Nested record | Exact shape |
| --- | --- |
| ProfileEvaluation | `R{budget=ProfileHostBudget,request=Bytevector(ProfileRequestBytes)}` |
The profile field is required.
The base evaluate API supplies false.
The evaluate_profile wrapper supplies ProfileEvaluation.
Its budget retains the required host resource_model metadata from Profiles.
The nested profile request remains a complete imported packet.
The evaluator validates its host work contract before using that account.
It performs the authoritative input decode under EvaluationLimits.
Input schema work then uses the host account before module initialization.
The same charged evaluation state resumes after schema acceptance.
This coordination happens inside the existing evaluate call.
No host callback or public continuation participates.
The separate record admission wrapper never enters this byte ABI.
The operation Strings are exactly `prepare`, `load`, `evaluate`, `export`, and `graph`.
`false` uses the Datum false tag. Empty records use the empty list.
A reply is exactly one complete CommandResultBytes packet.
The [host result mapping](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.command-result-format) defines each operation and its empty CLI command option.
EmergencyTerminalBytes uses the final terminal report slot in that envelope.
The caller secures the complete outer emergency framing before normal work.
The reply carries the prepared artifact, graph, canonical outcome, or phase report for that operation.
Evaluation receipts and optional trace data use their named fields in that imported result contract.
No host handle enters either packet.
Evaluation projects the sealed program, canonical input, fixed semantics, and EvaluationLimits into the [semantic request](/v2.0/en/docs/language/sandbox-contract#lispex.rule.v2.sandbox-contract.same-request).
TraceOptions, ABI framing, transport bounds, product selection, local handles, and instance history are excluded.
The request identity never hashes HostRequestBytes as a whole.
The profile field contributes to its separate host work binding.
It contributes no field to the canonical evaluation RequestRecord.
An evaluate_profile refusal uses the existing run admission operation.
A successful explicit record admission uses the existing record-admission operation.
The [evaluator exports](/v2.0/en/docs/tools/embedding#lispex.rule.v2.embedding.evaluator-exports) transport these packets.
A new instance is empty. Successful prepare or load seals exactly one program.
Only prepare and load are allowed while empty.
Only evaluate, export, and graph are allowed while sealed.
There is at most one active call and one pending complete reply.
Release removes transfer buffers and leaves the program state unchanged.
Another program requires a new instance.
Preparation seals its private immutable snapshot and publishes its complete reply atomically.
Failure discards partial program state and leaves the instance empty.
Evaluation always starts with fresh guest state and fresh evaluation counters.
It never retains guest results, module values, or initialization state for the next call.
A trap invalidates the instance and returns transport host-failure.
The wrapper creates the existing operational attempt report under its reserved host envelope.
A trapped evaluator does not serialize its own report.
A new evaluation receipt is absent after that transport failure.
Previously delivered outcomes and receipts remain unchanged.
State misuse uses `admission` and `request.invalid` with field `operation` and reason `invalid-value`.
The admitted package establishes finite ingress and egress bounds before accepting transport bytes.
Logical transport exhaustion uses the package host.envelope refusal and a complete report when the emergency envelope remains available.
The caller's unvalidated fields cannot select those bounds.
The fixed resource model names their representation and work ceilings under the cost freeze.
Transport framing and host record checks follow [boundary events](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.boundary-events).
Source, prepared, and canonical Datum packets then use their existing phase accounts.
Canonical input decode charges evaluation even before request identity exists.
Malformed input produces its existing pre-entry refusal and no evaluation receipt.
The decoder first validates the outer Datum packet.
It checks that the root is a record before inspecting its fields.
For each record it visits the supplied entries in list order.
It checks the entry pair, String key, canonical key order, and membership in that order.
Only then does it check the field value's type.
After supplied fields it checks missing fields in unsigned UTF-8 key order.
The top-level body value is first checked only for record shape.
It then checks the exact format, operation, and instance state in that order.
Only then does it validate the selected body schema recursively in field order.
Every complete imported byte packet keeps its own decoder order.
An invalid outer packet or record uses the existing request.invalid admission diagnostic.
The field identifies the first failing path. The root path is the empty String.
Wrong format, duplicate keys, nonstring keys, and out-of-order keys use reason invalid-value.
Unsorted module names use field body/bundle/modules and reason invalid-value.
These checks never decode source bytes or enforce source module uniqueness.
Nested foreign packet contents stay opaque until their owning phase starts.
This preserves source preparation order and evaluation input decode order.
It snapshots every bytevector before validation reads.
Its successful reply becomes visible only after complete serialization.
| Failure | Existing diagnostic |
| --- | --- |
| Missing required host field | `admission`, `request.invalid`, field path, `missing-field` |
| Unknown host field | `admission`, `request.invalid`, field path, `unknown-field` |
| Wrong type or unsupported operation | `admission`, `request.invalid`, field path, `invalid-value` |
| Invalid nested prepared artifact | The existing prepared artifact refusal |
| Malformed canonical input | The existing canonical input decode refusal |
Field paths use exact record keys separated by `/`.
The root field path is the empty String.
Vector indices use minimal unsigned decimal text.
The [diagnostic catalog](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.catalog) owns payload fields and codes.
The [exit mapping](/v2.0/en/docs/tools/run#lispex.rule.v2.cli-and-diagnostics.exit-mapping) owns CLI status.
**Why**
A closed packet gives every product the same request bytes. An instance-owned seal keeps process identity out of portable data.
Claim: `lispex.claim.v2.embedding.host-byte-abi` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "host-contract",
"operation": "host-byte-abi",
"language": "2.0"
},
"result": {
"kind": "closed-host-byte-abi",
"abi": "lispex.host/2",
"codec": "lispex.datum/2",
"reply": "CommandResultBytes",
"serializedHandle": false,
"instanceStates": [
"empty",
"sealed"
],
"singlePendingReply": true,
"operations": [
"prepare",
"load",
"evaluate",
"export",
"graph"
],
"evaluateProfileField": "false-or-ProfileEvaluation",
"profileInputDecode": "once-under-evaluation-account",
"schemaBeforeInitialization": true,
"publicContinuation": false
},
"pendingCases": [
"Native, npm, and WASM product adapters must exercise valid packets, first refusals, finite limits, ownership, and architecture boundaries."
]
}
```
### Encode exact host request bytes
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"record": {
"body": {
"format": "resolved/1",
"limits": {
"allocation": 0,
"diagnostic": 0,
"frames": 0,
"input": 0,
"result": 0,
"work": 0
}
},
"format": "lispex.host/2",
"operation": "export"
},
"purpose": "Encoding only. Zero finite limits do not assert successful export execution."
}
}
```
File: `request.hex`
```lispex
6c69737065782e646174756d2f3200a60108080604626f647908080606666f726d6174060a7265736f6c7665642f31080806066c696d6974730808060a616c6c6f636174696f6e03000808060a646961676e6f737469630300080806066672616d6573030008080605696e707574030008080606726573756c74030008080604776f726b0300000008080606666f726d6174060d6c69737065782e686f73742f32080806096f7065726174696f6e06066578706f727400
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The closed export request has one exact packet on every product. Product invocation awaits its 2.0 adapter."
}
```
### Refuse evaluation before sealing
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"instance": "new empty admitted instance",
"operation": "evaluate",
"input": "canonical integer 41",
"limits": "complete sufficient finite evaluation limits"
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "An empty instance rejects evaluation without running guest code. Product invocation awaits its 2.0 adapter."
}
```
## Artifact admission
Artifact admission is the host check that determines whether a submitted or installed artifact can execute under the requested contracts. It checks identity, interface compatibility, dependencies, and the physical resources needed to honor finite limits. A host that cannot provide that envelope refuses admission.
A lexical source import selects a module from the closed submitted bundle. An evaluator artifact import links the evaluator to host functionality. Preparation resolves lexical imports before evaluation. The preferred evaluator artifact has no host imports. Host file discovery and network loading cannot supply a missing guest dependency during evaluation.
### Validate artifacts before execution
Artifact admission checks the evaluator interface, supported contracts, dependencies, and resource envelope before execution. A transported prepared artifact is validated before use. Admission rejects host capabilities that grant ambient authority. The preferred evaluator artifact has no host imports.
**Why**
An unverified artifact can carry behavior outside the submitted rule. Admission keeps the data interface and resource limits effective for every accepted artifact.
Claim: `lispex.claim.v2.embedding.artifact-admission` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "embedding-artifact",
"boundary": "before-evaluation"
},
"result": {
"kind": "artifact-admission",
"interfaceChecked": true,
"dependenciesChecked": true,
"resourceEnvelopeChecked": true,
"transportedPreparedBytes": "validated",
"ambientHostImports": "rejected",
"preferredHostImports": []
},
"pendingCases": [
"Native, npm, and WASM need shipped artifact checks for imports, exports, malformed bytes, dependency closure, and physical admission on every supported architecture.",
"Every supported prepared artifact format needs version, tampering, and interface mismatch cases before it can be admitted."
]
}
```
### Refuse an artifact that requests file access
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"artifactCandidate": {
"kind": "evaluator-artifact-description",
"hostImports": [
"file-read"
],
"otherAdmissionChecks": "satisfied"
},
"execution": "Attempt to admit an evaluator whose host import grants guest file access.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Artifact admission refuses the file access capability. The entry is not evaluated and the host import is not called. Product invocation awaits its 2.0 adapter."
}
```
This is an artifact admission case. A lexical import from a submitted source bundle is a different operation. The candidate description is documentation notation and contains no executable artifact.
### Revalidate transported prepared bytes
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"preparedCandidate": {
"kind": "transported-prepared-bytes-description",
"version": "one supported prepared artifact version",
"structure": "malformed",
"otherAdmissionChecks": "satisfied"
},
"execution": "Attempt evaluation after receiving malformed prepared bytes from a caller.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Admission rejects the malformed prepared artifact before evaluating the entry. Product invocation awaits its 2.0 adapter."
}
```
A caller supplied version label does not replace validation. [PreparedArtifactBytes](/v2.0/en/docs/tools/embedding#lispex.rule.v2.embedding.artifact-format) defines the complete packet and validation order. This fixture describes a claimed artifact in documentation notation. It remains not-run until the 2.0 products and observation adapter exist.
### Use closed artifact containers
Each container is one canonical `lispex.datum/2` record packet.
`PreparedArtifactBytes` encodes the complete PreparedArtifact packet.
`EvaluatorArtifactBytes` encodes the complete EvaluatorArtifact packet.
`PackageBytes` encodes the complete Package packet.
It uses the exact record representation in [the host ABI](/v2.0/en/docs/tools/embedding#lispex.rule.v2.embedding.host-byte-abi).
The following tables list every field in unsigned UTF-8 order.
Bytevectors contain exact octets. A false optional field uses the Datum false tag.
Unknown fields, duplicate fields, wrong types, and trailing bytes are refused.
| PreparedArtifact field | Exact type and value |
| --- | --- |
| `format` | String `lispex.prepared-artifact/2` |
| `payload` | Bytevector of one complete prepared program |
| `payload-format` | String `resolved/1` or `bytecode/1` |
| `program` | Bytevector of canonical program IdentityBytes |
| `source-map` | False or Bytevector of complete SourceMapBytes |
The [prepared grammar](/v2.0/en/docs/tools/prepare#lispex.rule.v2.prepare.prepared-format) defines the payload unchanged.
The payload header must agree with payload-format.
Its dependency identities, root, entry, lexical references, sites, and event roles retain their existing validation order.
The program field must equal the program identity computed by [Identity](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.identity-encoding).
It is outside the prepared payload and outside program-local site bytes.
A present source map must pass the [source map contract](/v2.0/en/docs/tools/meaning-graph#lispex.rule.v2.meaning-graph.source-map-records) against that program.
It never changes the program or evaluation request identity.
Every successful prepare or load reply emits resolved/1 with source-map false.
Load normalizes the reply format even when its input used bytecode/1 or carried a source map.
The CLI prepare command uses that same default.
Explicit typed export selects either supported payload format and emits source-map false.
Equal verified programs produce equal export bytes for the same selected format.
A source map travels as a separately constructed sidecar or an explicitly supplied container field.
Changing its source provenance can change container identity while preserving program identity.
| EvaluatorArtifact field | Exact type and value |
| --- | --- |
| `abi` | String `lispex.host/2` |
| `format` | String `lispex.evaluator-artifact/2` |
| `payload` | Bytevector of one complete admitted WebAssembly core module |
| `physical-envelope` | Bytevector of the installed physical envelope IdentityBytes |
Evaluator payload bytes pass the [export contract](/v2.0/en/docs/tools/embedding#lispex.rule.v2.embedding.evaluator-exports).
An evaluator artifact has no guest program entry or host callback field.
Its identity uses the external [artifact identity contract](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.identity-encoding).
No container contains its own artifact digest.
| Package field | Exact type and value |
| --- | --- |
| `evaluator` | Bytevector of complete EvaluatorArtifactBytes |
| `format` | String `lispex.package/2` |
| `library` | Bytevector of the exact fixed installed library image |
| `metadata` | Bytevector of complete PackageMetadataBytes |
The library image is an opaque immutable dependency of the admitted evaluator.
Its complete bytes and artifact identity must match the evaluator's installed supported library image.
The semantic LibraryIdentity remains the identity of resolved library meaning.
The separate library-image field pins exact image bytes without changing that semantic identity.
It supplies the fixed library module bytes and kernel bindings required by preparation.
It is not parsed as a source bundle with an invented root.
The [procedure catalog](/v2.0/en/docs/library#lispex.rule.v2.standard-library.procedure-catalog) determines the public library surface.
Final native membership remains under [kernel and cost model](/v2.0/en/docs/library#lispex.pending.v2.standard-library.kernel-and-cost-model).
Artifact admission first captures the immutable container under the trusted host envelope.
It validates the outer packet and exact record schema.
It then checks the container format and required field types in table order.
For a prepared artifact it checks payload-format and then runs the existing prepared validator.
The outer program field supplies the requested program identity at the prepared validator's existing identity check.
After that validator succeeds, the wrapper validates any source map.
A failed sidecar discards the private handle and exposes no sealed instance.
The wrapper publishes the complete reply and instance seal together.
For an evaluator artifact it checks ABI and physical envelope identity compatibility before module inspection.
It establishes actual physical capacity only after the package dependencies pass their checks.
For a package it validates metadata, evaluator, and library in that order after framing.
An enclosing bytevector count never admits an unchecked payload allocation.
Wrapper checks cannot reorder the checks inside a prepared payload.
| Refusal | Existing diagnostic |
| --- | --- |
| Malformed PreparedArtifact or EvaluatorArtifact, or mismatched payload format | `admission`, `artifact.invalid`, corresponding kind, `invalid-format` |
| Wrong supplied program identity | `admission`, `artifact.invalid`, `prepared`, `identity-mismatch` |
| Wrong evaluator or library bytes for the pinned identity | `admission`, `artifact.invalid`, `evaluator`, `invalid-integrity` |
| Unrecognized evaluator support evidence | `admission`, `artifact.invalid`, `evaluator`, `unverified-content` |
Package and metadata schema failures use the Open refusal table.
Preparation meters the raw selected prepared payload under [preparation events](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.preparation-events).
The host transport envelope meters container framing and command result framing separately.
Loading validates before sealing. Copying a verified flag or local handle is never an admission path.
**Why**
Closed containers preserve one payload interpretation and its exact dependencies. Keeping digests outside their own payloads prevents identity cycles.
Claim: `lispex.claim.v2.embedding.artifact-format` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "host-contract",
"operation": "artifact-format",
"language": "2.0"
},
"result": {
"kind": "artifact-containers",
"prepared": "lispex.prepared-artifact/2",
"evaluator": "lispex.evaluator-artifact/2",
"package": "lispex.package/2",
"defaultPreparedFormat": "resolved/1",
"payloadContracts": "unchanged",
"selfDigest": false
},
"pendingCases": [
"Native, npm, and WASM product adapters must exercise valid packets, first refusals, finite limits, ownership, and architecture boundaries."
]
}
```
### Emit one default prepared format
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"operations": [
"CLI prepare",
"typed prepare",
"export resolved/1",
"export bytecode/1"
],
"compare": "Same complete bundle and fixed dependencies."
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "All products emit the same resolved artifact by default and preserve program identity across explicit formats. Product invocation awaits its 2.0 adapter."
}
```
### Reject a mismatched prepared payload tag
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"containerMutation": {
"payload-format": "resolved/1",
"payload": "otherwise valid bytecode/1 bytes"
}
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "A bytecode payload under a resolved payload-format field is refused before use. Product invocation awaits its 2.0 adapter."
}
```
### Keep program identity outside local sites
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"mutation": "Change only the outer program identity to a different valid identity."
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "A wrong outer program identity is refused after the unchanged prepared payload is validated. Product invocation awaits its 2.0 adapter."
}
```
### Admit the exact evaluator exports
The standard evaluator is one WebAssembly core module with zero imports and no start section.
It has exactly the exports below and no others.
Its memory is one unshared memory32 with a declared finite maximum.
Tables and globals remain private. Shared memory, memory64, and additional memories are refused.
The physical envelope identity supplies memory and stack ceilings after implementation measurement.
This Rule assigns no page count or physical capacity.
| Export | WebAssembly kind and exact signature |
| --- | --- |
| `memory` | The single unshared memory32 |
| `lispex_v2_alloc` | Function `i32 -> i32` |
| `lispex_v2_call` | Function `i32 i32 -> i32` |
| `lispex_v2_response_ptr` | Function `() -> i32` |
| `lispex_v2_response_len` | Function `() -> i32` |
| `lispex_v2_release` | Function `() -> ()` |
The i32 length and address bit patterns are interpreted as unsigned integers.
Address zero is reserved as allocation failure.
Lengths must fit the installed finite transport envelope before allocation.
A zero request length is invalid transport input.
The caller may have one allocated request span at a time.
Alloc returns the span start or zero. It runs under the trusted host envelope.
Alloc while busy or while an input span or reply remains live returns zero without changing any state.
The wrapper checks lifecycle state and reserves the known span size under the trusted envelope before calling alloc.
Zero after that valid admitted allocation request is a host failure.
A known size or reservation refusal produces the existing host.envelope report before alloc.
The evaluator does not allocate from an unchecked count inside request bytes.
Call accepts exactly the start and length of that live span.
It checks nonwrapping end arithmetic and the whole span before reading any request octet.
It captures an immutable private snapshot before parsing.
Output storage never aliases input storage or the sealed program.
After call returns zero, both response getters expose the complete retained reply.
Repeated getters return the same span without evaluation or further semantic charge.
The response remains valid until release.
Getters before a complete reply return zero.
| Call status | Meaning | Reply |
| --- | --- | --- |
| `0` | One complete reply, including any admission or semantic failure | Complete CommandResultBytes |
| `1` | Invalid span, pending reply, reentry, or other transport lifecycle misuse | No new reply |
| `2` | Host allocation or infrastructure failure | None |
Status 1 preserves any existing live request, complete reply, and sealed program.
It never substitutes that old reply for a newly completed call.
These statuses are transport values. They never substitute for [CLI exit statuses](/v2.0/en/docs/tools/run#lispex.rule.v2.cli-and-diagnostics.exit-mapping).
A WebAssembly trap is handled as status 2 by the wrapper and revokes the instance.
The wrapper uses its reserved envelope for the existing operational attempt report.
It produces no new evaluation receipt for the failed attempt.
Earlier delivered reports stay unchanged.
Release frees the request and reply spans and resets their addresses and lengths to zero.
It preserves the private sealed program.
Release is idempotent when there is no pending call.
Calls and release are never reentrant.
After physical failure the wrapper destroys the instance instead of reusing partial state.
The typed wrapper keeps raw evaluator memory private.
It writes only its allocated request span and reads only the returned response span.
A JavaScript wrapper reacquires memory views after any export that can grow memory.
It copies the complete response before releasing it.
It never invokes guest code once to learn an output size and again to obtain output bytes.
The [host state contract](/v2.0/en/docs/tools/embedding#lispex.rule.v2.embedding.host-byte-abi) governs empty and sealed instances.
Admission checks the complete immutable module before instantiation.
It validates core module structure, imports, start section, export names and signatures, and memory shape in that order.
Each list uses binary section order. Missing exports are checked in the table order.
Duplicate or extra exports fail the same exact export check.
An import uses artifact.invalid with kind evaluator and reason host-import.
Other shape failures use kind evaluator and reason invalid-format.
Unsupported physical limits use the existing host.envelope diagnostic.
Only an explicitly installed supported evaluator identity can be instantiated.
Its conformance evidence and measured physical envelope must cover the admitted request.
Export shape and identity checks do not authorize an arbitrary uploaded evaluator.
A separate engine keeps the same public contract and requires its own conformance evidence.
**Why**
A small export set makes ownership and call state explicit. Supported identities and measured envelopes keep unchecked evaluator code outside admission.
Claim: `lispex.claim.v2.embedding.evaluator-exports` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "host-contract",
"operation": "evaluator-exports",
"language": "2.0"
},
"result": {
"kind": "evaluator-export-surface",
"imports": 0,
"startSection": false,
"memory": "single-unshared-memory32",
"exports": [
"memory",
"lispex_v2_alloc",
"lispex_v2_call",
"lispex_v2_response_ptr",
"lispex_v2_response_len",
"lispex_v2_release"
],
"transportStatuses": [
0,
1,
2
],
"evidenceRequired": true
},
"pendingCases": [
"Native, npm, and WASM product adapters must exercise valid packets, first refusals, finite limits, ownership, and architecture boundaries."
]
}
```
### Reject imports and extra exports
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"mutations": [
"Add one host import.",
"Add a start section.",
"Add one extra export."
],
"artifact": "otherwise matching candidate evaluator"
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Each mutated evaluator is refused before instantiation. Product invocation awaits its 2.0 adapter."
}
```
### Read one response without rerunning
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"sequence": [
"prepare and release",
"allocate one evaluation request",
"call once for input 41",
"read response pointer and length twice",
"release twice"
]
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Repeated response reads do not repeat evaluation or semantic charges. Product invocation awaits its 2.0 adapter."
}
```
### Require supported evaluator evidence
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"artifact": "A module has exactly the declared exports, zero imports, and no start section. Its identity has no installed support evidence."
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Correct exports do not admit an evaluator without installed conformance support. Product invocation awaits its 2.0 adapter."
}
```
## Topaz integration
Topaz will update its std.lispex adapter to follow this host interface. Topaz owns that adapter and its concrete calls. The interface carries a prepared immutable rule, canonical input, and finite limits, then returns the canonical outcome.
Topaz captures time, exchange rates, random results, and other external facts before evaluation when a rule needs them. Those captured values become part of the canonical input and the recorded request. A later live value becomes a new input. Topaz displays the result and applies its own policy before performing an external action.
[Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay) defines how the request, outcome, and execution evidence are recorded. The result is data for the host policy. Guest evaluation does not itself authorize or perform the host action.
### Keep external facts and actions with Topaz
Topaz supplies a prepared immutable rule, captured canonical input, and finite limits through its host interface. Lispex returns a canonical outcome. Topaz decides any external action separately from that outcome.
**Why**
Capturing time, rates, and other external facts as values makes them part of the replayable request. A returned decision gives Topaz data to assess under its own action policy.
Claim: `lispex.claim.v2.embedding.topaz-handoff` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "topaz-rule-call",
"facts": "captured-in-canonical-input"
},
"result": {
"kind": "topaz-value-handoff",
"guestHostQueries": false,
"outcome": "canonical",
"externalActionAuthority": "topaz-host-policy"
},
"pendingCases": [
"Native, npm, and WASM need captured time, rates, and random results replayed across every supported engine and architecture.",
"Topaz owns later std.lispex integration cases for host input capture, request evidence, and separate external action policy."
]
}
```
### Replay a fact captured by Topaz
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (facts)
(< (car facts) (car (cdr facts)))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "list",
"items": [
{
"kind": "integer",
"value": "9"
},
{
"kind": "integer",
"value": "10"
}
]
}
},
{
"input": {
"kind": "list",
"items": [
{
"kind": "integer",
"value": "9"
},
{
"kind": "integer",
"value": "10"
}
]
}
},
{
"input": {
"kind": "list",
"items": [
{
"kind": "integer",
"value": "11"
},
{
"kind": "integer",
"value": "10"
}
]
}
}
],
"hostContext": {
"adapter": "Topaz std.lispex",
"inputMeaning": "The list holds a captured time value followed by a cutoff value.",
"liveClockAcrossRequests": [
9,
11,
11
],
"actionPolicy": "Observe the returned values without performing an external action."
},
"execution": "Replay the first captured input after the host clock changes. Then submit a newly captured input as a different request.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The first two requests return true and the third returns false. Guest code reads no live clock and the calls perform no external action. Product invocation awaits its 2.0 adapter."
}
```
Topaz captures external facts before calling Lispex. The changed host clock is outside the first two requests. The new captured value belongs to a new request. Topaz owns the std.lispex adapter and any separate action policy.
## Packages
A package distributes an evaluator with its standard library and declared interface and semantic identities. Admission checks the evaluator, standard library, ABI, value codec, language and Unicode semantics, profile, and resource model. The installed components must match the package declaration and support the submitted request.
Native, npm, and WASM use the same language contract. A shared evaluator artifact is preferred for these products. An additional engine supplies its own conformance evidence. Package and engine identities attach to execution evidence. They do not permit a changed result for the same semantic request.
### Check the components of a package
A package verifies its evaluator, standard library, ABI, codec, semantics, profile, and resource model identities. A mismatched or unsupported component causes admission refusal. The package does not substitute another component silently.
**Why**
A package name alone does not identify the components that execute a rule. Component checks keep the installed product aligned with the requested semantics.
Claim: `lispex.claim.v2.embedding.package-identities` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "embedding-package",
"components": [
"evaluator",
"standard-library",
"abi",
"codec",
"semantics",
"profile",
"resource-model"
]
},
"result": {
"kind": "package-admission",
"identityChecks": "required",
"incompatibleComponent": "admission-failure",
"silentSubstitution": false
},
"pendingCases": [
"Native, npm, and WASM need installed package cases for each missing, mismatched, and unsupported component identity on every supported architecture.",
"Release and dependency evidence must identify the actual shipped evaluator and library components."
]
}
```
### Refuse mismatched package components
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
},
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"packageCandidates": [
{
"defect": "the installed standard library identity differs from the requested fixed library",
"otherAdmissionChecks": "satisfied"
},
{
"defect": "the installed value codec identity differs from the requested codec",
"otherAdmissionChecks": "satisfied"
}
],
"execution": "Submit each request to the described installed package without loading replacement components.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Each package is refused for its incompatible component. No entry runs and no replacement component is loaded silently. Product invocation awaits its 2.0 adapter."
}
```
The installed component identities are compared with the request and package contract. A different evaluator artifact may still implement the same semantics when its interface is compatible and its conformance evidence supports admission.
### Pin the complete package contract
PackageMetadataBytes is one canonical `lispex.datum/2` closed record.
Every field below is required and uses the host record representation.
Metadata declares exact installed contracts. It supplies no fallback or discovery instruction.
| Field | Exact value type |
| --- | --- |
| `abi` | String `lispex.host/2` |
| `datum-codec` | String `lispex.datum/2` |
| `engine` | Bytevector of engine IdentityBytes |
| `evaluator` | Bytevector of the supplied EvaluatorArtifactBytes identity |
| `format` | String `lispex.package-metadata/2` |
| `language` | String `2.0` |
| `library` | Bytevector of the semantic LibraryIdentity for resolved library meaning |
| `library-image` | Bytevector of the artifact identity of the complete fixed library image bytes |
| `physical-envelope` | Bytevector of the installed physical envelope identity |
| `prepared-formats` | Vector containing String `bytecode/1` then String `resolved/1` |
| `product` | String `native`, `npm`, or `wasm` |
| `product-version` | ReleaseVersion String |
| `profiles` | Vector of ProfileSupport records in unsigned UTF-8 name order |
| `resource-models` | Vector of resource model IdentityBytes bytevectors in unsigned byte order |
| `unicode` | Bytevector of the fixed Unicode 17.0.0 identity |
| Nested type | Exact shape |
| --- | --- |
| ProfileSupport | Record fields `identity` as an IdentityBytes bytevector and `name` as String `base` or `vouch/2` |
| ReleaseVersion | Three minimal unsigned decimal components separated by `.` |
| Minimal component | `0` or one ASCII digit from `1` through `9` followed by zero or more ASCII digits |
The support vectors are nonempty and have no duplicate elements or profile names.
The base profile is required. A vouch/2 entry requires its own admitted profile support.
Every identity passes its imported canonical decoder.
Resource model, profile, Unicode, and library identities refer to their existing contracts.
The metadata adds no new profile meaning or cost numbers.
It contains no package path, URL, time, host locale, account, license, signer, or publishing instruction.
Actual release names and ownership remain outside this format decision.
Open takes the complete package bytes and an expected metadata identity from the caller.
That expected identity uses the artifact domain over complete PackageMetadataBytes.
The installed product has an immutable supported component catalog before this operation.
That catalog supplies trusted finite ingress and egress bounds before any package field is decoded.
It also supplies the supported evaluator, library, and physical envelope identities.
The supplied metadata cannot enlarge that catalog or its bounds.
Open snapshots the package and validates its outer schema.
It decodes metadata and checks exact field types and canonical support order.
It compares the expected metadata identity before accepting any selected contract.
It checks the installed product and product version before checking the requested contract tuple.
It checks language, ABI, Datum codec, prepared formats, engine, Unicode, semantic library, library image, resource models, and profiles in that order.
The selected identities must form one supported installed compatibility tuple with the physical envelope.
Independent membership in separate support lists is insufficient.
Every declared profile and resource model pair must be covered with the same fixed engine, library, Unicode, and physical envelope.
It then validates the evaluator shape and supported identity, the supplied library bytes, and the physical envelope.
It returns a Product only after every check succeeds.
No guest preparation or evaluation runs during Open.
Failure returns an admission report and no Product.
| Existing refusal | Use |
| --- | --- |
| request.invalid with field `package` and reason invalid-value | Malformed package or metadata schema |
| artifact.invalid with kind evaluator and reason identity-mismatch | Expected metadata or selected component identity mismatch |
| artifact.invalid with kind evaluator and reason unverified-content | Unsupported evaluator conformance evidence |
| request.invalid with reason invalid-value | Installed product or release mismatch at field `package/metadata/product` or `package/metadata/product-version` |
| product.unsupported | Unsupported contract using only the existing ProductSubject enumeration |
| host.envelope with reason unsupported-limits | Trusted ingress or egress reservation cannot admit the work |
| host.envelope with reason physical-capacity | The host cannot establish the installed physical envelope |
The contract field of host.envelope is the trusted ingress, egress, or physical envelope identity that refused the operation.
Trusted egress admission uses bounds derived from the complete admitted phase and channel limits before guest entry.
It reserves the final report envelope before normal work.
Later report delivery cannot replace a completed canonical outcome with a new admission refusal.
A physical delivery failure follows the attempt report contract and preserves completed outcome and receipt eligibility.
An admission refusal before evaluation has no evaluation request identity or evaluation receipt.
A complete refusal report still uses transport status zero.
Actual physical failure during a call uses the separate operational failure path.
The [package signature fixture](/v2.0/en/docs/tools/embedding#lispex.example.v2.embedding.package-contract-fields) defines Open for every host.
It uses the same complete PackageBytes and IdentityBytes on each product.
The Product returned by Open issues every later private handle and checked constructor record.
Product labels and product versions remain execution evidence.
They never enter the prepared program, base semantic request, canonical outcome, or evaluation receipt.
**Why**
Exact metadata prevents silent substitutions across products. Independent installed support keeps untrusted metadata from authorizing itself.
Claim: `lispex.claim.v2.embedding.package-metadata` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "host-contract",
"operation": "package-metadata",
"language": "2.0"
},
"result": {
"kind": "closed-package-metadata",
"format": "lispex.package-metadata/2",
"fields": [
"abi",
"datum-codec",
"engine",
"evaluator",
"format",
"language",
"library",
"library-image",
"physical-envelope",
"prepared-formats",
"product",
"product-version",
"profiles",
"resource-models",
"unicode"
],
"selfAuthorization": false,
"guestCodeDuringOpen": false
},
"pendingCases": [
"Native, npm, and WASM product adapters must exercise valid packets, first refusals, finite limits, ownership, and architecture boundaries."
]
}
```
### Open a package with pinned contracts
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"package": "one complete matching package with supported fixed identities",
"expectedMetadata": "the exact independent metadata identity"
}
}
```
File: `open-signatures.txt`
```lispex
Rust
pub enum ProductReply {
Opened { product: Product, report: CommandResultBytes },
Refused { report: CommandResultBytes },
}
pub fn open(package: PackageBytes, expected_metadata: IdentityBytes)
-> Result;
TypeScript
export type ProductReply =
| Readonly<{ kind: 'opened'; product: Product; report: CommandResultBytes }>
| Readonly<{ kind: 'refused'; report: CommandResultBytes }>;
export declare function open(packageBytes: PackageBytes, expectedMetadata: IdentityBytes): ProductReply;
C
uint32_t lispex_v2_open(lispex_v2_view package_bytes,
lispex_v2_view expected_metadata, lispex_v2_product **out_product,
lispex_v2_bytes *out_reply);
void lispex_v2_product_destroy(lispex_v2_product **product);
All report bytes are complete CommandResultBytes.
The C package span contains PackageBytes.
The C expected_metadata span contains IdentityBytes for the expected metadata artifact.
The installed product catalog fixes transport bounds before Open starts.
Open uses no caller-supplied limits to authorize its own package decoder.
C destroy revokes owned records and handles and sets the pointer to zero.
Rust Product drop and TypeScript disposeProduct revoke owned records and handles.
TypeScript export declare function disposeProduct(product: Product): void;
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Exact supported metadata and dependency bytes expose one validated Product. Product invocation awaits its 2.0 adapter."
}
```
### Reject substituted library bytes
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite limits sufficient for these operations",
"evaluate": "finite limits sufficient for the stated evaluation"
},
"cases": {
"mutation": "Keep metadata and evaluator fixed but change one library image octet."
}
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "A package cannot substitute different bytes under a fixed library identity. Product invocation awaits its 2.0 adapter."
}
```
## Product contract
The [semantic request](/v2.0/en/docs/language/sandbox-contract#lispex.section.v2.sandbox-contract.semantic-request) fixes the program, input, semantics, model, and limits. Selecting a product changes the execution evidence while preserving the requested meaning. A profile may narrow admission without changing the accepted request.
A missing capability or unsupported contract produces an explicit admission refusal. Operational interruption and engine defect remain distinct outcomes for the host to handle. [Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay) defines their evidence and receipt eligibility. [CLI and diagnostics](/v2.0/en/docs/tools/run) defines product presentation and exit mapping.
### Resolve finite limits before entry
Every public execution entry applies the [finite-limit rule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.finite-entrypoints) to each phase it performs. Limits use named fields. An explicit limit record with a missing required field, an unknown field, or an overflow is refused before entry. Convenience defaults select the [common finite preset](/v2.0/en/docs/tools/run#lispex.rule.v2.cli-and-diagnostics.finite-preset-selection).
**Why**
Complete finite limits make a request comparable across products. Named fields prevent a changed field order from silently changing the resource budget.
Claim: `lispex.claim.v2.embedding.finite-limits` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "embedding-limits",
"surfaces": "all-public-entrypoints",
"representation": "named-fields"
},
"result": {
"kind": "finite-embedding-request",
"prepare": "finite",
"evaluate": "finite",
"defaultPreset": "common",
"invalidLimitRecord": "admission-failure",
"unmeteredPublicEntry": false
},
"pendingCases": [
"Native, npm, and WASM need all resource axes below, at, and above their limits on each supported engine and architecture.",
"Product cases must check preset resolution, explicit field validation, and physical admission before execution."
]
}
```
### Refuse malformed explicit limits
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
},
{
"input": {
"kind": "integer",
"value": "42"
}
},
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"limitSubmissions": [
{
"kind": "explicit-named-limits",
"defect": "one required field is missing after preset resolution"
},
{
"kind": "explicit-named-limits",
"defect": "one unknown field is supplied"
},
{
"kind": "explicit-named-limits",
"defect": "one value exceeds the supported contract range"
}
],
"execution": "Submit three independent requests. Each explicit limit record has only the stated defect.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Each request is refused for its malformed explicit limits. No entry is evaluated and no malformed value is replaced by a default. Product invocation awaits its 2.0 adapter."
}
```
Selecting a common preset is valid. These cases instead submit malformed explicit records after that selection. Field names, finite values, and representation bounds remain pending contracts.
### Return control from a nonterminating rule
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ()
(loop))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to enter the loop"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Evaluation ends with a terminal resource stop and returns control to the host without a result datum. Product invocation awaits its 2.0 adapter."
}
```
The language resource contract determines the stop. The example requires termination under finite limits without choosing a tariff coefficient, a default number, or an exact failure site.
See [Resource model numbers](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers).
### Preserve meaning across products
Every product preserves the outcome of the same admitted semantic request. This includes the first failure, exhausted resource axis, and canonical failure site. Each additional engine needs conformance evidence for the same contract.
**Why**
Selecting a package or engine must preserve what a rule means. Independent product evidence checks that the installed components satisfy the shared language contract.
Claim: `lispex.claim.v2.embedding.product-meaning` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "embedding-product-comparison",
"request": "same-admitted-semantic-request",
"products": [
"native",
"npm",
"wasm"
]
},
"result": {
"kind": "product-semantic-agreement",
"canonicalOutcome": "same",
"firstFailure": "same",
"resourceAxisAndSite": "same",
"additionalEngine": "requires-conformance-evidence"
},
"pendingCases": [
"Native, npm, and WASM need product comparisons across all supported engines and architectures, including resource boundaries and cold and warm preparation caches.",
"Different engine implementations require independent evidence for evaluation order, first failure, and resource event preservation."
]
}
```
### Compare a value and a domain failure across products
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (items)
(car items)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "list",
"items": [
{
"kind": "integer",
"value": "3"
},
{
"kind": "integer",
"value": "5"
}
]
}
},
{
"input": {
"kind": "list",
"items": []
}
}
],
"comparison": "Use the same canonical program, inputs, semantics, model, and limits for every supported product and engine.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Every product returns the exact integer 3 for the first input. Every product reports the same car domain failure for the empty list. Product invocation awaits its 2.0 adapter."
}
```
Native, npm, and WASM have separate product plans with the same authored outcomes. Engine and platform evidence attaches to the execution. The semantic request remains unchanged.
### Refuse unsupported requests explicitly
A product refuses an unsupported contract before guest evaluation. It preserves the requested semantics and limits when deciding admission. It does not retry the request with a different meaning or a reduced budget.
**Why**
A refusal tells the caller that the selected product cannot execute this request. A silent retry would answer a different question while appearing to preserve the original request.
Claim: `lispex.claim.v2.embedding.explicit-refusal` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "embedding-support-check",
"requestedContract": "unsupported"
},
"result": {
"kind": "explicit-admission-refusal",
"entryEvaluated": false,
"semanticFallback": false,
"limitReduction": false
},
"pendingCases": [
"Native, npm, and WASM need unsupported language, Unicode, library, codec, profile, and model cases for every supported engine and architecture.",
"Products must distinguish admission refusal from an operational interruption after admission."
]
}
```
### Refuse an unsupported resource model
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"productSupport": {
"requestedResourceModel": "unsupported by the selected product",
"otherResourceModel": "available but not requested",
"otherAdmissionChecks": "satisfied"
},
"execution": "Submit the request without authorizing a change to its resource model or limits.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The product refuses the unsupported resource model before entry. It performs no fallback evaluation under the available alternative. Product invocation awaits its 2.0 adapter."
}
```
The calling application may choose a different supported request explicitly. That later request has its own identity and evidence. Refusal does not itself create a substituted request.
See [Diagnostic catalog and reports](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.catalog), [Admission and profile work report formats](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.admission-report-format).
## Related chapters
[Sandbox contract](/v2.0/en/docs/language/sandbox-contract)
[Values and text](/v2.0/en/docs/language/values)
[Resources](/v2.0/en/docs/language/resources)
[Profiles and value interchange](/v2.0/en/docs/profiles)
[Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay)
[CLI and diagnostics](/v2.0/en/docs/tools/run)
[Procedures](/v2.0/en/docs/language/procedures)
[Preparation and modules](/v2.0/en/docs/tools/prepare)
### Pending · Resource model numbers
The 2.0 tariff coefficients, logical allocation units, bit-size accounting, detailed frame accounting, finite defaults, representation limits, and physical memory envelopes remain open. This includes preparation, calls, values, exact arithmetic, equality, text, record conversion, and canonical encoding.
Profile host budget coefficients and defaults remain separate from language preparation and evaluation budgets. Trace capacity, reservation sizes, and host memory requirements retain their separate reporting scope. Each budget retains its own identity and accounting boundary.
Implementation and attack tests must support these choices. [Resource event declarations](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.event-catalog) and [native kernel membership](/v2.0/en/docs/library#lispex.pending.v2.standard-library.kernel-and-cost-model) remain separate contracts.
### Pending · Native kernel membership
The final native kernel list and count remain open. Implementation and product attack tests must support these choices. [Tariff coefficients, allocation units, finite defaults, and physical envelopes](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers) are tracked once with the resource numbers.
## Related
[Sandbox contract](/v2.0/en/docs/language/sandbox-contract)
[Values and text](/v2.0/en/docs/language/values)
[Resources](/v2.0/en/docs/language/resources)
[Profiles and value interchange](/v2.0/en/docs/profiles)
[Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay)
[CLI and diagnostics](/v2.0/en/docs/tools/run)
[Procedures](/v2.0/en/docs/language/procedures)
[Preparation and modules](/v2.0/en/docs/tools/prepare)