Lispex 2.0 specification · not released · Tested product not run · Examples not run
# Profiles and value interchange
Select profile admission and evidence requirements while preserving Lispex meaning. Exchange exact data through a canonical codec.
Canonical: /v2.0/en/docs/profiles
Document revision: 2.0-draft-1. Content locale: en. Translation: current.
- language: `lispex`
- languageVersion: `2.0`
## Scope
The calling application selects a profile and supplies canonical input data. An admitted rule keeps the language meaning and resource limits of its semantic request.
This chapter defines admission, base, vouch/2, schemas, and canonical value interchange. [Sandbox contract](/v2.0/en/docs/language/sandbox-contract) defines language, profile, product, and engine. [Values and text](/v2.0/en/docs/language/values#lispex.section.v2.values.datum) defines Datum.
## Admission
Admission checks whether the selected product and profile can accept a proposed execution. It accepts the submitted request or refuses it before guest entry. A refusal preserves the declared program, input, semantics, and limits.
Engine support and library permission are explicit checks. A product reports missing support instead of changing execution meaning. [Preparation and modules](/v2.0/en/docs/tools/prepare) defines the closed program that admission inspects.
### Refuse unsupported requests before entry
Admission checks the selected profile and the product’s supported semantics before guest entry. Unsupported engine features or excluded library operations cause admission refusal. A product cannot repair refusal by changing semantics or silently selecting another engine.
**Why**
An accepted request has one declared meaning. Refusal identifies an unsupported request before a different implementation can produce a different result.
Claim: `lispex.claim.v2.profiles.admission-before-entry` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "execution-admission",
"checks": [
"profile",
"engine-support",
"library-permission"
]
},
"result": {
"kind": "explicit-admission",
"unsupportedRequest": "admission-failure",
"entryBeforeAcceptance": false,
"semanticFallback": false
},
"pendingCases": [
"Every installed product needs direct unsupported engine, excluded library, incompatible semantics, and finite limit admission cases.",
"The concrete base and vouch/2 declarations must enumerate accepted libraries and required evidence."
]
}
```
### Reject missing engine support
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 3)))
)
```
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
},
"profileRole": "base"
}
],
"engineAdmissionFixture": {
"requiredOperation": "exact rational division",
"supportsRequiredOperation": false
},
"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 refuses an engine that lacks the required exact rational operation. No alternate engine or approximate result is selected. Product invocation awaits its 2.0 adapter."
}
```
The fixture describes a deliberately unsupported engine capability. A conforming product reports the refusal before invoking the rule.
### Reject an excluded library operation
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "41"
},
"selectedProfile": "vouch/2"
}
],
"engineAdmissionFixture": {
"supportsRequiredOperation": true
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope and statement. This fixture refuses admission before receipt binding or signature verification is reached."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
},
"libraryExclusion": {
"name": "+",
"resolvedOwner": "fixed standard library",
"presentInAllowedBindings": false,
"checkOrder": "before evidence prerequisites and canonical input decoding"
}
}
```
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 selected profile refuses the excluded library operation before entry. It does not switch to base admission. Product invocation awaits its 2.0 adapter."
}
```
The exclusion is a property of this documented profile declaration. The final vouch/2 library inventory remains a pending contract.
The profile host budget bounds additional profile admission, schema checks, output qualification, and evidence work. It is finite and separate from the language preparation and evaluation budgets. Canonical input decoding and canonical result or failure encoding remain evaluation work.
An early host refusal prevents guest entry. A later qualification or evidence refusal preserves the completed canonical outcome. Profile work cannot reduce the evaluation budget, move the first language failure, or rerun guest code.
[Profile work identity and reports](/v2.0/en/docs/profiles/receipt-and-replay#lispex.section.v2.receipt-and-replay.identities) identify these checks separately from the semantic request. Before entry, a refusal uses an admission report. After evaluation, qualification or evidence refusal uses a profile work report tied to the completed canonical outcome.
### Keep profile work separate
Additional profile admission, schema checks, qualification, and evidence work use the separate finite profile host budget. Canonical input decoding and canonical result or failure encoding remain evaluation work. Profile checks preserve the semantic request and cannot debit its budgets or change its first language failure. A host check can refuse admission before entry or qualification after evaluation. A completed canonical outcome remains unchanged.
**Why**
A narrower profile may perform more checks than base. Accounting for those checks separately preserves the evaluation meaning and limits of requests accepted by both.
Claim: `lispex.claim.v2.profiles.profile-work-separation` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "profile-work-accounting",
"work": [
"profile-admission",
"input-schema",
"output-schema",
"evidence"
]
},
"result": {
"kind": "separate-finite-profile-work",
"hostBudgets": "separately-declared-finite",
"canonicalInputDecoding": "evaluation",
"canonicalResultAndFailureEncoding": "evaluation",
"semanticRequest": "unchanged",
"evaluationCharges": "unchanged",
"firstLanguageFailure": "unchanged"
},
"pendingCases": [
"Each profile needs finite admission, input schema, output schema, and evidence work cases on every product.",
"Products must compare accepted requests with different profile check workloads and unchanged evaluation charges and first stops."
]
}
```
### Stop a finite input schema check before entry
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
},
"selectedProfile": "vouch/2"
}
],
"canonicalCodecResources": "finite evaluation resources sufficient to decode the input datum",
"profileWork": {
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"identity": "submitted-profile-work",
"contract": "lispex.profile-work/2",
"evidenceRequirement": "signed-execution",
"evidenceOperation": "verify the explicitly supplied envelope after output qualification"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "The finite W covers setup, snapshot, declaration, library checks, evidence prerequisites, and all preceding host events. The next input schema reservation exceeds the remaining W. A, F, I, R, and E are sufficient. Authoritative input decoding has completed under EvaluationLimits.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope and statement. This fixture refuses admission before receipt binding or signature verification is reached."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
}
}
```
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 profile host budget stops the input schema check. Admission refuses the request before guest entry without changing its declared evaluation limits. Product invocation awaits its 2.0 adapter."
}
```
Canonical input decoding has sufficient evaluation resources. The additional input schema check uses the separate finite profile host budget.
### Bound all profile host work
The profile host budget has every field below. Each of its six budget axes is an exact nonnegative integer. The `format` and `resource_model` fields are metadata. Zero is finite. Missing fields, unknown fields, nonintegers, unlimited values, and values outside the selected model's admitted range fail admission. Host integer width does not choose that range.
One account covers all performed profile stages. It starts before profile operand checks and continues through qualification and evidence. Stage changes do not refill it. Committed work, allocation, input, report, and evidence charges are never refunded. Logical traversal frames are released only when their traversal returns.
Every event reserves all required fields before its check or effect. Simultaneous shortages choose work, allocation, frames, input, report, then evidence. A refused reservation changes no charged total and performs no partial effect. The first committed failure ends later profile work.
Profile wrapper decoding, record conversion, schema checks, declaration checks, library inspection, hashing, evidence verification, and report construction use this account. Canonical input decoding runs once under EvaluationLimits. Schema checks then inspect that immutable decoded Datum under the host account. After admission, evaluation continues with its existing decoding charges and state. It initializes modules and invokes the entry only after input schema acceptance. Canonical result encoding remains evaluation work.
Before evaluation, the host secures the terminal report capacity required by the selected finite limits and model. The reservation covers a complete refusal diagnostic and the largest eligible receipt and profile report permitted by those limits. The model names that bound. A shortage refuses admission. Its numeric bound remains under the cost model freeze.
After evaluation, the canonical outcome and eligible receipt remain immutable. A later schema, budget, or evidence failure produces its separate report. It does not rerun the guest, replace a language failure, or revoke receipt eligibility. Later report transport failure cannot change the committed first cause.
The resource_model metadata selects the host model independently of the evaluation model. Only the six numeric limit fields are budget axes. Operations without a declaration skip profile schema and qualification stages. Their separate command contracts retain the same finite host account.
**Why**
A finite shared host account bounds every additional check. A fixed reservation order gives the same first refusal across products. Reserved reporting capacity protects a completed result while profile work is refused.
Claim: `lispex.claim.v2.profiles.profile-work-contract` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "profile-work-contract",
"languageVersion": "2.0",
"contract": "lispex.profile-work/2"
},
"result": {
"kind": "portable-profile-contract",
"closedFields": true,
"orderedChecks": true,
"ambientAuthority": false,
"evaluationMeaningPreserved": true
},
"pendingCases": [
"Installed 2.0 products and engines must execute these cases.",
"Each finite boundary requires cases below, at, and above its selected limit."
]
}
```
| Operation | Complete terminal capacity bound |
| --- | --- |
| `run` | The requested finite evaluation result and diagnostic limits, eligible receipt framing, and complete profile report |
| `verify` | The captured receipt and evidence operand sizes and the complete verification report |
| `replay` | The expected receipt size, recorded finite evaluation result and diagnostic limits, actual eligible receipt, and complete comparison report |
| `record-admission` | The finite captured input bound, canonical converted input packet, and complete admission refusal report |
The host secures its terminal reporting slot before work can publish a result.
Run and replay reserve the complete eligible receipt capacity before guest evaluation.
Record admission reserves complete conversion output capacity before conversion.
The selected host model defines the required finite reservation from these inputs.
The reservation uses report capacity and its required work and logical allocation.
A shortage refuses the operation before its unprotected stage begins.
The committed first cause stays fixed.
Later physical delivery failure leaves every completed immutable outcome and receipt available.
The model's numeric bounds and physical capacity proof remain under the cost model freeze.
The [command result contract](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.command-result-format) imports the complete outer emergency framing and separate trace state.
Those fields are covered before normal work begins.
| Host operation | Profile contract | Declaration | Schema and evidence work |
| --- | --- | --- | --- |
| `run` | The selected base or vouch/2 builtin | The generated base declaration or explicit vouch/2 declaration | The complete admission, qualification, and required evidence schedule |
| `verify` | Absent | Absent | Receipt comparison and explicitly requested evidence under the command contract |
| `replay` | Absent | Absent | Recorded-request binding and explicitly requested expected-receipt evidence before authoritative input decoding |
| `record-admission` | The explicitly selected base or vouch/2 builtin | Absent | Record key admission and canonical conversion only |
Record admission requires no program, library, input schema, output schema, or evidence.
Both builtin profiles use the same record key policy.
Conversion ends with CanonicalInputBytes.
Later evaluation admission checks its selected schema against a verified program.
That later operation has its own host work identity and account.
Record admission produces no canonical evaluation outcome or evaluation receipt.
Standalone verify and replay do not synthesize a base declaration.
They skip profile schema membership and output qualification.
Their host work still uses the complete finite ProfileHostBudget.
The profile and declaration options in ProfileWorkInput are absent.
For record admission only the profile option is present.
For run both options are present.
Prepare and graph use their existing preparation and tool contracts.
They do not acquire profile arguments or a ProfileWorkIdentity through this rule.
| Form | Exact shape |
| --- | --- |
| `ProfileWorkContractDefinition` | `R{format="lispex.profile-work/2",schema_language="lispex.schema/2",resource_model=ProfileHostBudget.resource_model}` |
| `ProfileWorkContractIdentity` | `ContractIdentity(kind="profile-work",name="lispex.profile-work/2",definition=ProfileWorkContractDefinition)` |
This exact descriptor denotes the complete check schedule and schema traversal in this chapter.
Its resource model supplies host tariff and allocation parameters.
The definition resource_model equals the validated budget metadata.
The schema language and format strings are fixed.
Extra fields and alternate schedules are invalid.
The product verifies the complete descriptor against its supported version before marking the contract identity verified.
The [identity contract](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.identity-encoding) encodes and hashes this declarative value.
The definition is independent of document prose and product implementation bytes.
The numeric model choices remain frozen until implementation and product evidence support them.
### Inspect schemas in a fixed order
Schema validation visits each finite tree occurrence in depth-first order. It checks a node's tag and exact shape before its children. Pair children use car then cdr order. Vectors use ascending index order. A record node checks all field names, field shapes, ordering, and required markers before validating any child schema. It then validates child schemas in key order. Enum canonical order and duplicates are checked before membership.
Membership follows the table below. Each entered schema and data occurrence reserves its work and logical frame before inspection. A completed child releases its frame before its next sibling begins. Shared physical storage never skips an occurrence.
Complete the prescribed shape checks before testing child membership. Stop at the first failed shape, key, membership test, or earlier reservation. A successful earlier comparison cannot suppress required later checks. No remaining child is visited after a committed failure.
A mismatch is reported by the schema boundary diagnostic. It does not invoke a guest Condition or a handler. The semantic request and completed outcome remain unchanged.
**Why**
Membership order can decide whether a schema mismatch or a host budget refusal happens first. A fixed traversal preserves that choice across recursive and iterative implementations. Structural prechecks avoid partial acceptance of malformed data.
Claim: `lispex.claim.v2.profiles.schema-traversal` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "schema-traversal",
"languageVersion": "2.0",
"contract": "lispex.profile-work/2"
},
"result": {
"kind": "portable-profile-contract",
"closedFields": true,
"orderedChecks": true,
"ambientAuthority": false,
"evaluationMeaningPreserved": true
},
"pendingCases": [
"Installed 2.0 products and engines must execute these cases.",
"Each finite boundary requires cases below, at, and above its selected limit."
]
}
```
| Form | Exact shape |
| --- | --- |
| `ProfileHostBudget` | `R{format="lispex.profile-host-budget/2",resource_model=ResourceModelIdentity,work=HostNat,allocation=HostNat,frames=HostNat,input=HostNat,report=HostNat,evidence=HostNat}` |
| `ProfileHostBudgetBytes` | `D(ProfileHostBudget)` |
| `HostNat` | An exact nonnegative Datum integer |
| `HostBudgetFieldName` | `work`, `allocation`, `frames`, `input`, `report`, `evidence` |
The resource_model field selects the explicit host work model.
It is required metadata and is not a budget axis.
The format field is required metadata.
The host model may differ from the evaluation resource model.
It does not change evaluation charges or RequestIdentity.
A change to either host model or host limits changes ProfileWorkIdentity.
The selected common-default preset resolves this complete record.
An explicit profile-limits operand supplies the complete record.
No product fills missing metadata from its engine or another operand.
A supported model is verified from the complete [model definition](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.model-definition).
Default host axis data is known before the model identity.
Preset resolution adds resource_model only after that identity is verified.
No network or registry discovery supplies that declaration.
| Field | Quantity bounded |
| --- | --- |
| `work` | Cumulative normative host work |
| `allocation` | Cumulative logical host allocation |
| `frames` | Simultaneously active logical host traversal frames |
| `input` | Total captured operand packet bytes used by this host operation |
| `report` | Complete host report and conversion output capacity |
| `evidence` | Total complete evidence packet bytes processed by this operation |
| Operation | Captured packet operands counted by input |
| --- | --- |
| `run` | The explicit profile request and canonical input packets, plus every other submitted packet read by its host checks |
| `verify` | Expected receipt, actual receipt, supplied evidence, and supplied trust policy packets |
| `replay` | Recorded request, expected receipt, supplied evidence, and supplied trust policy packets, plus every submitted packet read by its host checks |
| `record-admission` | The complete explicit record input packet |
Each submitted operand occurrence contributes its complete byte length once.
Repeated inspection does not add another input charge.
It retains the required work and allocation events.
Nested evidence and trust packets already contained in a profile request do not add another input occurrence when extracted.
An independently supplied operand is a new occurrence even when it reuses the same physical buffer.
The evidence field also bounds evidence packet bytes contained in an input operand.
Host checks that read source or prepared operands include those bytes in input.
Preparation retains its separate resource account.
Malformed metadata or budget values use request.invalid under the existing catalog.
An unsupported host model uses product.unsupported with subject resource-model.
No fallback model is selected.
Tariffs, allocation units, numeric range bounds, defaults, terminal capacity bounds, physical capacity values, and the final native kernel inventory remain under [cost model freeze](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers).
The field names, exact types, occurrence rules, reservation order, and traversal schedule are fixed here.
| Stage | Ordered work | Result boundary |
| --- | --- | --- |
| Host setup | Validate the complete budget and acquire the finite physical safety envelope. Reserve terminal report capacity | A refusal precedes guest entry |
| Snapshot | Bind the complete explicit operand snapshot and charge its input and evidence bytes | No issuer or configuration lookup |
| Declaration | Decode the profile request, validate its wrapper, validate the declaration, then validate input and output schemas | Unknown or malformed data is refused |
| Library | Verify the selected fixed library identity, validate allowed names, then inspect resolved source references in canonical order | The first excluded binding refuses admission |
| Prerequisites | Check supported engine semantics, explicit evidence and trust presence, and their supported structure | Missing prerequisites refuse admission |
| Canonical input | Decode the canonical packet exactly once under EvaluationLimits | Malformed data or decoding exhaustion follows the existing input diagnostic contract |
| Input schema | Apply the schema to the immutable decoded Datum under the host account | No guest entry on schema refusal |
| Evaluation | Continue the admitted evaluation state with module initialization and entry. Retain the input decoding charges | Complete the canonical outcome and eligible receipt |
| Qualification | Apply the output schema to the immutable returned Datum. Skip membership for language failure and resource stop | A refusal preserves the completed outcome and receipt |
| Evidence | Check the declared requirement against the completed actual receipt in the evidence contract order | No evidence work after an earlier profile refusal |
| Report | Commit the complete separate host report in its reserved capacity | Preserve the first cause and the receipt bytes |
Standalone verify and replay use the same host fields. Their [command order](/v2.0/en/docs/tools/run#lispex.rule.v2.cli-and-diagnostics.command-forms) chooses when evidence is checked. Replay evaluation retains its separate account.
| Event family | Required logical work |
| --- | --- |
| `profile-input` | Account for an explicit operand occurrence before inspecting it |
| `profile-declaration` | Visit the next declaration component in its prescribed order |
| `profile-library` | Check the next allowed binding or resolved source reference |
| `profile-schema` | Enter, inspect, or leave the next schema and data occurrence |
| `profile-compare` | Compare canonical names or enum bytes in their declared order |
| `profile-hash` | Hash the next required byte sequence under the identity contract |
| `profile-signature` | Perform the next required canonical key or signature check |
| `profile-report` | Reserve and encode a complete report before publication |
Record admission uses the codec and record events from the [boundary event schedule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.boundary-events).
Wrapper decoding, record adaptation, and encoding the converted packet all charge the host account.
Reserve that complete packet against report before emitting its octets.
The evaluator later performs its complete input decode and result encode in the evaluation account.
The selected host resource model supplies each host reservation size.
Product caching and pointer sharing preserve every required logical event.
| Node | Shape checks | Child or comparison order |
| --- | --- | --- |
| `datum` | The value has completed canonical Datum validation | No child schema |
| `kind` | Compare the current Datum kind | No child schema |
| `enum` | Use the complete canonical Datum bytes of the value | Members in declared byte order. Compare unsigned octets from zero. Stop on equality or after the final member |
| `pair` | Require a pair | Complete car membership, then cdr membership |
| `list` | Inspect the complete spine and require the empty final tail | Element schemas from the head |
| `vector` | Require a vector | Elements from index zero |
| `tuple` | Require a vector and exact declared length | Corresponding schemas from index zero |
| `record` | Require a proper list. Inspect all entry pair shapes and string keys in list order. Require strictly increasing keys. Merge actual and schema keys in UTF-8 order to check required and unknown names | After all key checks, visit present values in key order |
The first absent required or unknown supplied key in the merged order fails before any field value check. Absent optional fields have no child value to inspect. Required and optional markers change membership only. They never insert data.
The logical frame count includes the current traversal occurrence and its unfinished ancestors. Implementation call stacks, iterators, cached hashes, and shared objects do not change that count.
Input decoding has one authoritative result. It uses EvaluationLimits before schema membership. A malformed packet uses admission and input.codec. An exhausted decode uses admission and input.resource. Host schema work cannot replace either failure. Successful decoding supplies an immutable Datum and preserves the charged evaluation state. Schema acceptance resumes that state without decoding again.
A replay command can compare outer recorded-request bytes before this step. That comparison does not mark the canonical input or evaluation request verified. The [replay contract](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.replay-request) completes expected evidence checks before the authoritative decode. The corresponding verified markers appear only after decoding succeeds.
### Keep the first simultaneous host shortage
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "17"
},
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"profileHostBudgetConstraints": {
"setup": "finite fields sufficient for all preceding reservations",
"boundary": "the next admission schema event needs both work and allocation beyond their remaining limits",
"otherFields": "finite and sufficient"
},
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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": "Work precedes allocation when the same required reservation exceeds both fields. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Reserve a complete terminal report before 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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "base",
"input": {
"kind": "integer",
"value": "17"
},
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"evaluationLimits": "finite limits with the model-defined complete receipt bound",
"profileHostBudgetConstraints": {
"report": "finite capacity below the named terminal report reserve for the requested evaluation limits",
"otherFields": "finite and sufficient"
},
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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": "Insufficient terminal report capacity is refused before evaluation can create a result that the report cannot preserve. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Retain host charges through output qualification
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "42"
},
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"terminalReportReserve": "complete before evaluation",
"profileHostBudgetConstraints": {
"work": "finite work sufficient for admission but below cumulative admission work plus the next qualification reservation",
"otherFields": "finite and sufficient",
"resetCounterWouldPass": true
},
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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 account is not refilled after evaluation. The qualification refusal keeps the completed value and receipt. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Check a complete list spine before its members
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"list",
[
"kind",
"integer"
]
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "pair",
"car": {
"kind": "string",
"value": "wrong"
},
"cdr": {
"kind": "integer",
"value": "5"
}
},
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"profileHostBudgetConstraints": {
"work": "finite work sufficient through the improper-tail check but below the next element-schema reservation",
"otherFields": "finite and sufficient"
},
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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 improper final tail fails before element membership or its reservation begins. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Complete record keys before field membership
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"record",
[
[
"a",
true,
[
"kind",
"integer"
]
],
[
"b",
true,
[
"kind",
"integer"
]
]
]
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "list",
"items": [
{
"kind": "pair",
"car": {
"kind": "string",
"value": "a"
},
"cdr": {
"kind": "string",
"value": "wrong"
}
},
{
"kind": "pair",
"car": {
"kind": "string",
"value": "z"
},
"cdr": {
"kind": "integer",
"value": "1"
}
}
]
},
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"profileHostBudgetConstraints": {
"work": "finite work sufficient through the missing b check but below the first value-schema reservation",
"otherFields": "finite and sufficient"
},
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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 merged key order finds missing b before unknown z and before the mismatched value at a. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Charge every repeated schema occurrence
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"tuple",
[
[
"list",
[
"kind",
"integer"
]
],
[
"list",
[
"kind",
"integer"
]
]
]
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "vector",
"items": [
{
"kind": "list",
"items": [
{
"kind": "integer",
"value": "1"
}
]
},
{
"kind": "list",
"items": [
{
"kind": "integer",
"value": "1"
}
]
}
]
},
"materializationCases": [
"two distinct immutable list objects",
"shared immutable list storage"
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"profileHostBudgetConstraints": {
"work": "finite work sufficient for the first list occurrence but below the next required visit of the second occurrence",
"otherFields": "finite and sufficient"
},
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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": "Both materializations visit the second occurrence and refuse its same required reservation. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Preserve the receipt when evidence work exhausts its budget
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "42"
},
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"terminalReportReserve": "complete before evaluation",
"profileHostBudgetConstraints": {
"work": "finite work sufficient through output qualification but below the next required evidence verification reservation",
"otherFields": "finite and sufficient"
},
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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 next evidence reservation refuses profile acceptance while the immutable canonical receipt remains available. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Keep authoritative input decoding before schema membership
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"selectedProfile": "base",
"canonicalInputHex": "6c69737065782e646174756d2f320001ff",
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"cases": [
{
"case": "decode-reservation-first",
"evaluationLimits": "finite work below the next authoritative decode reservation"
},
{
"case": "malformed-tag",
"evaluationLimits": "finite and sufficient through the invalid tag check"
}
],
"profileHostBudgetConstraints": "finite and sufficient for all profile work",
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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": "EvaluationLimits determine the first authoritative input failure before any schema membership. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
## Base language
Base names the common Lispex 2.0 language contract. Its programs use exact data, the shared condition rules, and finite resources. Every admitted program has the sandbox guarantees defined in [Sandbox contract](/v2.0/en/docs/language/sandbox-contract).
A narrower profile can accept fewer inputs or libraries and require additional evidence. It preserves the meaning of the requests it accepts.
### Use one base language
Base applies the [default sandbox contract](/v2.0/en/docs/language/sandbox-contract#lispex.rule.v2.sandbox-contract.every-program) to every program. A narrower profile applies those same guarantees to its admitted requests. Selecting a product or engine follows the [same-request rule](/v2.0/en/docs/language/sandbox-contract#lispex.rule.v2.sandbox-contract.same-request).
**Why**
Every accepted program begins with the same sandbox contract. Profile admission can express application requirements without becoming a second language.
Claim: `lispex.claim.v2.profiles.base-contract` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "base-language-contract",
"languageVersion": "2.0",
"programs": "all"
},
"result": {
"kind": "shared-language-guarantees",
"deterministicOutcome": true,
"ambientAuthority": false,
"finiteExecution": true
},
"pendingCases": [
"Each product and engine needs direct base language cases for values, language failures, and terminal resource stops.",
"The 2.0 product observations must identify their exact language and profile scope."
]
}
```
### Return a value in the base language
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "17"
},
"profileRole": "base"
}
],
"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 base language request returns the exact integer 17 as its sole result datum. Product invocation awaits its 2.0 adapter."
}
```
The request uses finite preparation and evaluation limits. The base contract applies before any narrower profile requirements are selected.
## Vouch
The vouch/2 profile adds declared admission and evidence requirements to the base language. A declaration fixes its accepted input and output schemas, allowed library set, and required evidence.
Use the [language, profile, product, and engine definitions](/v2.0/en/docs/language/sandbox-contract#lispex.section.v2.sandbox-contract.profiles-products-engines) when selecting Native, npm, or WASM. Their execution evidence identifies the product and engine that supplied the observation.
[Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay#lispex.section.v2.receipt-and-replay.execution-evidence) defines how canonical outcomes and attached evidence are recorded.
### Preserve meaning after admission
Base and vouch/2 produce the same canonical outcome when both admit the same semantic request. Their evaluation limits and charges remain unchanged. A profile cannot replace a language failure or resource stop with a decision datum.
**Why**
Profiles can narrow admission and require evidence. Accepted evaluation still follows the same program, input, semantics, resource model, and limits.
Claim: `lispex.claim.v2.profiles.shared-meaning` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "shared-profile-request",
"profiles": [
"base",
"vouch/2"
],
"admittedBy": "both",
"request": "same-semantic-request"
},
"result": {
"kind": "profile-meaning-preservation",
"canonicalOutcome": "equal",
"evaluationLimits": "unchanged",
"evaluationCharges": "equal",
"failureCoercion": false
},
"pendingCases": [
"Each product needs shared base and vouch/2 cases for runtime conditions and every resource axis.",
"Every supported engine and architecture must compare the first failure and canonical site under identical limits."
]
}
```
### Return the same decision datum in both profiles
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)
(if (< input 0) 'deny 'allow)))
)
```
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "-1"
},
"selectedProfile": "base"
},
{
"input": {
"kind": "integer",
"value": "-1"
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"enum",
[
{
"kind": "symbol",
"value": "deny"
},
{
"kind": "symbol",
"value": "allow"
}
]
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence1"
],
"trust": [
"Trust1"
]
}
}
],
"comparison": "Hold the canonical program, input, fixed semantics, resource model, and evaluation limits constant.",
"profileWorkContexts": [
"base admission under sufficient finite host budgets",
"additional vouch/2 schema and evidence checks under sufficient separate finite host budgets"
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence1": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request."
},
"Trust1": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
}
}
```
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": "Both admitted requests return the symbol deny as one successful datum. Their evaluation limits and charges are equal. Product invocation awaits its 2.0 adapter."
}
```
The documented profile declaration accepts this program, its input, and the returned symbol. The label deny has no special language control effect.
### Preserve a terminal stop in both profiles
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 the rule",
"evaluate": "finite work that fails at one loop reservation with all other finite budgets sufficient through that event"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
},
"selectedProfile": "base"
},
{
"input": {
"kind": "integer",
"value": "0"
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence1"
],
"trust": [
"Trust1"
]
}
}
],
"comparison": "Use the same semantic request and first unsatisfied work reservation.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence1": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request."
},
"Trust1": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"evidenceTarget": "the complete resource-stop receipt for the same program, canonical input, resource model, and 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": "Both admitted requests stop at the same work reservation and canonical site. Neither profile substitutes a decision datum for the stop. Product invocation awaits its 2.0 adapter."
}
```
The profile declarations admit the program and input. Finite symbolic limits make work the first exhausted axis in both evaluations.
### Attach evidence to the same outcome
The vouch/2 profile applies the [execution evidence rule](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.execution-evidence). Its declaration determines the evidence required for a Vouch result. Evidence work uses the profile host budget and preserves the canonical outcome and evaluation charges.
**Why**
An execution record identifies how a result was obtained. Keeping that record separate preserves the meaning compared across profiles and products.
Finite host work stays separate from language evaluation.
Claim: `lispex.claim.v2.profiles.evidence-separation` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "vouch-evidence-requirement",
"profileRole": "vouch/2"
},
"result": {
"kind": "outcome-evidence-separation",
"canonicalOutcome": "preserved",
"productAndEngine": "identified-by-evidence",
"requirements": "declared-profile",
"evidenceWorkResources": "separate-finite-host-resources"
},
"pendingCases": [
"Concrete vouch/2 evidence requirements need missing, stale, incompatible, and invalid evidence cases.",
"Installed distribution observations, replay evidence, and signatures need distinct product cases."
]
}
```
### Attach distinct evidence to one language outcome
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "17"
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
}
},
{
"input": {
"kind": "integer",
"value": "17"
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence1"
],
"trust": [
"Trust1"
]
}
}
],
"evidenceContexts": [
"one admitted engine artifact",
"another admitted engine artifact"
],
"comparison": "Keep the semantic request fixed and compare canonical outcomes separately from execution evidence.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request. Its statement names the first admitted execution artifact tuple."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
},
"Evidence1": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request. Its statement names the second admitted execution artifact tuple."
},
"Trust1": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
}
}
```
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": "Both admitted executions return the exact integer 17 with equal evaluation charges. Their execution evidence differs while the canonical outcome remains equal. Product invocation awaits its 2.0 adapter."
}
```
The evidence contexts identify distinct admitted engine artifacts. Concrete evidence formats and verification belong to Identity, receipt, replay.
### Stop finite evidence work after 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",
"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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
},
"selectedProfile": "vouch/2"
}
],
"canonicalCodecResources": "finite evaluation resources sufficient to encode the canonical outcome",
"profileWork": {
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"identity": "submitted-profile-work",
"contract": "lispex.profile-work/2",
"evidenceRequirement": "signed-execution",
"evidenceOperation": "verify the explicitly supplied envelope after output qualification"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "The finite W covers admission and output qualification. The next required evidence verification reservation exceeds the remaining W. A, F, I, R, and E are sufficient. The supplied evidence bytes and complete terminal report capacity were reserved before evaluation.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
}
}
```
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. The profile host budget stops required evidence work before a profile result can be issued and preserves that canonical outcome. Product invocation awaits its 2.0 adapter."
}
```
Canonical result encoding has sufficient evaluation resources. Evidence work cannot replace the result with a language resource stop or run the rule again.
### Declare the complete profile contract
A profile declaration uses the exact fields below. Every field is required. The selected profile name must match the declaration. Unknown formats, fields, and values fail admission. An explicit declaration supplies no defaults.
Base is the fixed declaration generated from the request's verified library identity. Its input and output schemas accept every Datum. Its library entry contains the complete public catalog. Its evidence requirement is none. A declaration with narrower fields cannot use the base name.
A vouch/2 declaration supplies its complete input schema, output schema, and allowed public bindings. Its evidence requirement is signed-execution. It preserves the request's fixed library identity. An empty binding list admits source that uses no public library binding.
The sole allowed library identity is the fixed Lispex 2.0 library selected by the semantic request. Each binding name must appear in the [public catalog](/v2.0/en/docs/library#lispex.rule.v2.standard-library.procedure-catalog). The vector is strictly increasing by unsigned UTF-8 name bytes. Internal library dependencies keep their fixed meaning. Source modules and source-defined bindings are outside this allowlist.
Admission checks resolved library references in every supplied source module. It follows canonical module and node order. An alias retains the identity of its resolved binding. Unused definitions and unselected branches still take part in this check. The first excluded reference refuses admission. No library procedure runs during this inspection.
The request wrapper carries the explicit declaration and its evidence operands. Base uses empty evidence and trust options. Vouch/2 requires both options. Missing operands refuse admission. Evidence verification follows output qualification and binds the completed actual receipt.
The profile host budget is a separate request input. The command's profile-limits operand or selected finite preset supplies it. The declaration wrapper cannot replace that budget.
**Why**
A complete declaration makes acceptance reproducible. A fixed base declaration preserves the common language. A narrower declaration records each additional restriction. Resolved references keep aliases and source shadowing precise. Explicit evidence operands keep trust outside ambient host state.
Claim: `lispex.claim.v2.profiles.profile-declarations` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "profile-declarations",
"languageVersion": "2.0",
"contract": "lispex.profile/2"
},
"result": {
"kind": "portable-profile-contract",
"closedFields": true,
"orderedChecks": true,
"ambientAuthority": false,
"evaluationMeaningPreserved": true
},
"pendingCases": [
"Installed 2.0 products and engines must execute these cases.",
"Each finite boundary requires cases below, at, and above its selected limit."
]
}
```
### Use finite structural schemas
A schema is a finite tree in the grammar below. Each vector has its exact declared length. Schema validation completes before the schema is applied. Unknown nodes, extra fields, and invalid field types refuse admission. There are no references or implicit schema imports.
Membership inspects an already validated Datum. It preserves every value and raw scalar. It never coerces a number, normalizes text, inserts a field, or invokes guest or host code. The schema contract contains no executable predicate.
An enum contains at least one Datum. Its members are strictly increasing by their complete canonical Datum bytes. Repeated members are invalid. A record schema has exact string names in unsigned UTF-8 order. Each field appears once. Its Boolean marks whether the field is required. A false value allows absence without supplying a replacement.
A record schema accepts only a proper association list of string-keyed pairs in canonical key order. Its keys are unique. Every supplied key must occur in the schema. An ordinary association list keeps its original Datum meaning outside a record schema.
The [schema traversal rule](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.schema-traversal) fixes validation and membership order. A mismatch uses profile.admission before entry or profile.qualification after evaluation. The profile field identifies the selected builtin profile contract. The rule field identifies the verified canonical program.
**Why**
Structural schemas express finite data restrictions without a second evaluator. Canonical set and field order remove host ordering choices. Explicit optional fields preserve absence as input data.
Claim: `lispex.claim.v2.profiles.schema-language` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "schema-language",
"languageVersion": "2.0",
"contract": "lispex.profile/2"
},
"result": {
"kind": "portable-profile-contract",
"closedFields": true,
"orderedChecks": true,
"ambientAuthority": false,
"evaluationMeaningPreserved": true
},
"pendingCases": [
"Installed 2.0 products and engines must execute these cases.",
"Each finite boundary requires cases below, at, and above its selected limit."
]
}
```
### Admit explicit records with string keys
Base and vouch/2 admit the named record input below. The caller selects record conversion explicitly. A field key is an exact Unicode string. Empty strings and all Unicode scalar strings are admitted. Symbols, numbers, bytevectors, and host object keys are not field names. No coercion or normalization supplies a name.
Each field vector has a name and one child. The complete name collection is checked before any child value is converted. The adopted [record conversion rule](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.host-record-conversion) sorts names, rejects duplicates, and converts values in that order. Nested records use the same rule. A datum node preserves its enclosed Datum. A record node becomes ordinary association data with each unchanged name as a string key.
The record packet is a finite value tree. It contains no callback, accessor, identity-bearing object, cycle, or live host reference. A typed host adapter rejects such values without invoking them.
Record adaptation, wrapper decoding, and conversion output encoding use the profile host budget.
The result is one complete canonical input packet.
The [evaluation boundary](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.boundary-events) then decodes that packet under EvaluationLimits.
Direct input and converted input with identical bytes have identical evaluation events.
Evaluation also encodes its result under EvaluationLimits.
A cached conversion does not remove evaluation events.
The command input operand still takes canonical Datum bytes. A record wrapper supplied as an ordinary Datum remains that Datum. The format name never selects conversion by inspecting guest data.
**Why**
Explicit conversion keeps host records distinct from ordinary lists. String keys preserve the adopted Unicode and codec contracts. Lowering before evaluation gives identical association data the same evaluation request and charges.
Claim: `lispex.claim.v2.profiles.record-input` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "record-input",
"languageVersion": "2.0",
"contract": "lispex.profile/2"
},
"result": {
"kind": "portable-profile-contract",
"closedFields": true,
"orderedChecks": true,
"ambientAuthority": false,
"evaluationMeaningPreserved": true
},
"pendingCases": [
"Installed 2.0 products and engines must execute these cases.",
"Each finite boundary requires cases below, at, and above its selected limit."
]
}
```
D encodes one complete lispex.datum/2 packet. R is a proper association list with exact string keys in unsigned UTF-8 order. The shared [wire notation](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.identity-encoding) defines these forms.
| Form | Exact shape |
| --- | --- |
| `ProfileDeclaration` | `R{ format = "lispex.profile/2", profile = "base" | "vouch/2", schema_language = "lispex.schema/2", input_schema = Schema, output_schema = Schema, libraries = #(LibraryPermission), evidence_requirement = "none" | "signed-execution", work_contract = "lispex.profile-work/2" }` |
| `LibraryPermission` | `R{identity = LibraryIdentity, bindings = #(Text...)}` |
| `ProfileDeclarationBytes` | `D(ProfileDeclaration)` |
| `ProfileRequest` | `R{ format = "lispex.profile-request/2", declaration = ProfileDeclaration, evidence = Option(Bytevector), trust = Option(Bytevector) }` |
| `ProfileRequestBytes` | `D(ProfileRequest)` |
| `Option(T)` | `#() | #(T)` |
| Profile | Input schema | Output schema | Bindings | Evidence requirement |
| --- | --- | --- | --- | --- |
| `base` | `#("datum")` | `#("datum")` | Every public catalog name exactly once | `none` |
| `vouch/2` | One explicit Schema | One explicit Schema | An explicit sorted subset of the public catalog | `signed-execution` |
The evidence option contains the complete named evidence packet. The trust option contains the complete named trust policy packet. The [evidence envelope contract](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.evidence-envelope) defines those bytes.
The profile-declaration command operand contains ProfileRequestBytes. An omitted base operand selects the generated base declaration and empty options. Vouch/2 requires this operand. An explicit base operand must equal the generated base declaration and its empty options.
| Failure | Diagnostic | Field |
| --- | --- | --- |
| Missing declaration field | `request.invalid` with `missing-field` | `profile-declaration.` followed by the exact missing name |
| Unknown declaration field | `request.invalid` with `unknown-field` | `profile-declaration.` followed by the exact supplied name |
| Invalid declaration value | `request.invalid` with `invalid-value` | `profile-declaration.` followed by its top-level field name |
| Invalid input schema subtree | `request.invalid` with `invalid-value` | `profile-declaration.input_schema` |
| Invalid output schema subtree | `request.invalid` with `invalid-value` | `profile-declaration.output_schema` |
| Malformed declaration record or packet | `request.invalid` with `invalid-value` | `profile-declaration` |
| Excluded resolved library binding | `profile.admission` with `library-exclusion` | The catalog payload names the builtin profile contract and verified program identities |
| Missing required evidence or trust | `profile.admission` with `evidence-prerequisite` | The catalog payload names the builtin profile contract and verified program identities |
Check record shape first. Then merge the required and supplied field names in unsigned UTF-8 order. The first missing or unknown name wins before field values are checked. Validate field values in unsigned UTF-8 name order. Validate input_schema before output_schema. Malformed wrapper fields use the same rule with profile-request as their field prefix. Budget shortages use the phase and field from the host work contract.
A declaration packet has no verified declaration identity until all declaration checks succeed. The selected builtin profile contract is verified before parsing. Profile budget diagnostics use that builtin identity. The report keeps declaration verification separate.
| Form | Exact shape |
| --- | --- |
| `SchemaBytes` | `D(R{format = "lispex.schema/2", schema = Schema})` |
| `Schema` | `#("datum") | #("kind" Kind) | #("enum" #(Datum...)) | #("pair" Schema Schema) | #("list" Schema) | #("vector" Schema) | #("tuple" #(Schema...)) | #("record" #(Field...))` |
| `Field` | `#(Text Boolean Schema)` |
| `Kind` | `"boolean" | "integer" | "rational" | "number" | "character" | "symbol" | "empty-list" | "pair" | "string" | "vector" | "bytevector"` |
| Schema | Membership |
| --- | --- |
| `datum` | Every already validated Datum |
| `kind` | The exact Datum kind. Number admits integers and reduced nonintegral rationals |
| `enum` | One exact canonical member |
| `pair` | A pair whose car and cdr satisfy the two child schemas |
| `list` | A proper list whose elements satisfy the child schema |
| `vector` | A vector whose elements satisfy the child schema |
| `tuple` | A vector with the declared length and corresponding child schemas |
| `record` | Closed canonical association data with the declared required and optional fields |
Rational selects the nonintegral rational kind. Integer selects the integer kind. Empty record schemas accept only the empty list. Empty tuple schemas accept only an empty vector.
| Form | Exact shape |
| --- | --- |
| `RecordInputBytes` | `D(R{format = "lispex.record/2", value = RecordNode})` |
| `RecordNode` | `#("record" #(RecordField...))` |
| `RecordField` | `#(Text InputNode)` |
| `InputNode` | `#("datum" Datum) | RecordNode` |
| Check | Required result |
| --- | --- |
| Wrapper and node shape | Exact tags and vector lengths |
| Field shape and key type | Inspect field positions from zero before ordering names |
| Key type failure | `record.key` with the first invalid submitted field position |
| Name collection | Apply the existing UTF-8 order and duplicate check |
| Duplicate positions | `first` and `second` are the adjacent positions of the first equal name in the sorted name sequence |
| Key Datum | The unchanged name as a string |
| Field value | Recursively convert in canonical name order |
| Converted input | D of the resulting association Datum |
A missing or malformed structural slot uses request.invalid with invalid-value. A nonstring field name uses record.key. Duplicate keys use record.duplicate. Conversion ends with CanonicalInputBytes. Later evaluation admission checks its selected schema against a verified program. Record admission performs no evidence work.
The builtin profile contract is fixed before the request declaration is parsed. Its identity selects the contract applied by every profile diagnostic. The declaration has its own identity and verification marker.
| Form | Exact shape |
| --- | --- |
| `ProfileContractDefinition` | `R{ format = "lispex.profile-contract/2", profile = "base" | "vouch/2", declaration_format = "lispex.profile/2", schema_format = "lispex.schema/2", work_contract = "lispex.profile-work/2" }` |
| `ContractName("base")` | `"base/2"` |
| `ContractName("vouch/2")` | `"vouch/2"` |
| `ProfileContractIdentity` | `ContractIdentity( kind = "profile", name = ContractName(selected profile), definition = ProfileContractDefinition )` |
An unrecognized selector cannot produce a builtin identity. It uses the existing request or unsupported-product diagnostic. No profile declaration identity is inferred from an unchecked packet.
### Use the fixed base declaration
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "base",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "base",
"schema_language": "lispex.schema/2",
"input_schema": [
"datum"
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "none",
"work_contract": "lispex.profile-work/2"
},
"evidence": [],
"trust": []
},
"input": {
"kind": "integer",
"value": "17"
},
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"profileHostBudgetConstraints": "all finite fields sufficient for the specified host work",
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record."
}
```
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 exact base declaration accepts the Datum and adds no evidence requirement. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Reject a narrowed declaration named base
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "base",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "base",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "none",
"work_contract": "lispex.profile-work/2"
},
"evidence": [],
"trust": []
},
"input": {
"kind": "integer",
"value": "17"
}
}
```
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 base name requires the exact universal schema even when this input would satisfy the narrower schema. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Qualify the same receipt with explicit 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)))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "17"
},
"evidenceFixture": {
"order": [
"complete the same semantic request under base",
"sign that immutable receipt outside guest execution",
"supply the envelope and policy in the vouch request"
],
"signatureStatus": "valid for the exact receipt",
"originalAttestationProfileWork": "different from this vouch work 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": "The explicit signed envelope qualifies the same completed receipt. A new profile work identity does not change the evaluation request. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Inspect an excluded binding in an unselected branch
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) (if #t input (+ input 1)))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "41"
},
"preparedGraph": "the source reference to + resolves to the fixed library binding"
}
```
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 resolved library reference before branch selection can hide it. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Keep a source binding outside the library allowlist
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 + (lambda (a b) a))
(define rule (lambda (input) (+ input 99))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "17"
},
"preparedGraph": "the source use of + resolves to the local source definition"
}
```
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 empty library allowlist does not exclude a source-defined binding with the same spelling. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Accept an exact enum result without coercion
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) 'allow)))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"enum",
[
{
"kind": "symbol",
"value": "allow"
}
]
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "17"
}
}
```
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 symbol matches the same canonical enum member. The schema invokes no predicate and supplies no replacement value. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Reject an executable schema node
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"predicate",
"host-validator"
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": []
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"complete explicit valid evidence bytes for this fixture receipt"
],
"trust": [
"complete explicit trust policy bytes accepting the fixture issuer and execution tuple"
]
},
"input": {
"kind": "integer",
"value": "17"
}
}
```
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 schema grammar rejects a predicate node before membership and without invoking host code. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Lower explicit records to the same canonical 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",
"rootModule": "main",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"operation": "compare record admission followed by evaluation with direct canonical input evaluation",
"selectedProfile": "base",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "base",
"schema_language": "lispex.schema/2",
"input_schema": [
"datum"
],
"output_schema": [
"datum"
],
"libraries": [
{
"identity": "verified fixture LibraryIdentity",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "none",
"work_contract": "lispex.profile-work/2"
},
"evidence": [],
"trust": []
},
"records": [
{
"format": "lispex.record/2",
"value": [
"record",
[
[
"é",
[
"datum",
{
"kind": "integer",
"value": "1"
}
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "3"
}
]
],
[
"é",
[
"datum",
{
"kind": "integer",
"value": "2"
}
]
]
]
]
},
{
"format": "lispex.record/2",
"value": [
"record",
[
[
"é",
[
"datum",
{
"kind": "integer",
"value": "2"
}
]
],
[
"é",
[
"datum",
{
"kind": "integer",
"value": "1"
}
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "3"
}
]
]
]
]
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"profileHostBudgetConstraints": "finite fields sufficient for conversion and schema work",
"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": "The named W A F I R E parameters stand for finite exact integers that satisfy the separately stated fixture constraints. They are not serialized strings in a public budget record.",
"inputPaths": [
{
"case": "first-order",
"recordIndex": 0
},
{
"case": "second-order",
"recordIndex": 1
},
{
"case": "direct-canonical-input",
"canonicalInputHex": "6c69737065782e646174756d2f320019080806016103060808060365cc81030408080602c3a9030200"
}
],
"evaluationComparison": "Use the same verified program, evaluation limits, and fixed semantics for all three paths. Record admission has its own host operation and account."
}
```
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": "Both record orders and direct canonical input produce the same evaluation events, result, and receipt. Record adaptation and its encoding use the separate host account. Product invocation awaits its 2.0 adapter."
}
```
The two record inputs differ only in field order. A third call supplies their canonical input bytes directly. Compare the complete evaluation event streams and receipt bytes. Record conversion and output encoding remain separate host work.
### Refuse a symbol as a host record key
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"operation": "explicit record conversion",
"record": {
"format": "lispex.record/2",
"value": [
"record",
[
[
{
"kind": "symbol",
"value": "a"
},
[
"datum",
{
"kind": "integer",
"value": "1"
}
]
]
]
]
}
}
```
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 admitted key kind is string even when a symbol has the same scalar spelling. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Reject duplicate record names before nested values
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",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"operation": "explicit record conversion",
"record": {
"format": "lispex.record/2",
"value": [
"record",
[
[
"z",
[
"unknown-node"
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "1"
}
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "2"
}
]
]
]
]
}
}
```
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 duplicate in canonical name order wins before the invalid nested value is visited. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
### Keep a record wrapper ordinary at the Datum 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) input)))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one verified fixed library identity",
"unicode": "one verified fixed Unicode contract identity",
"resourceModel": "one verified finite resource model"
},
"limits": {
"prepare": "finite values sufficient for preparation",
"evaluate": "finite values sufficient for the case",
"profile": "finite values for the declared host work case"
},
"entry": "rule",
"schemaNotation": "JSON arrays in schemaNode fields denote Datum vectors. Identity and finite budget labels name fixture parameters.",
"operation": "ordinary evaluate",
"input": {
"kind": "list",
"items": [
{
"kind": "pair",
"car": {
"kind": "string",
"value": "format"
},
"cdr": {
"kind": "string",
"value": "lispex.record/2"
}
},
{
"kind": "pair",
"car": {
"kind": "string",
"value": "value"
},
"cdr": {
"kind": "vector",
"items": [
{
"kind": "string",
"value": "record"
},
{
"kind": "vector",
"items": []
}
]
}
}
]
},
"selectedProfile": "base"
}
```
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 canonical input boundary does not dispatch on a format-looking Datum value. Product invocation awaits its 2.0 adapter."
}
```
The fixture uses the declared 2.0 byte contract and symbolic finite limits. The product plans remain not-run.
## Input and output schemas
A schema describes accepted data. An input schema chooses which input data the rule may receive. An output schema describes the result data accepted by a profile.
A decision label such as allow or deny is ordinary returned data. The calling application chooses any external action. The language does not turn the label into a host command.
Input schema checks inspect decoded input before guest entry. Canonical input decoding remains evaluation work. The additional schema check uses the profile host budget.
After evaluation, host qualification checks a returned datum against the output schema. It records profile acceptance separately from the canonical outcome. Canonical result or failure encoding remains evaluation work.
### Validate data without coercion
A schema specifies accepted input and output data. An input outside the selected schema is refused before guest entry. Validation preserves exact values and text. Decision labels remain ordinary data. Profile schema checks use the [profile host budget](/v2.0/en/docs/profiles/#lispex.rule.v2.profiles.profile-work-separation).
**Why**
Schema membership describes which data the application accepts. Coercing an input or interpreting a label as an engine command would change the rule request.
Finite host work stays separate from language evaluation.
Claim: `lispex.claim.v2.profiles.schema-values` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "profile-schema-validation",
"values": [
"input",
"output"
]
},
"result": {
"kind": "value-preserving-validation",
"inputMismatch": "admission-failure",
"implicitCoercion": false,
"decisionLabels": "ordinary-data",
"profileCheckResources": "separate-finite-host-resources"
},
"pendingCases": [
"The settled schema language needs valid and invalid cases for every supported datum shape, depth, and size.",
"Output qualification needs concrete schema traversal, reporting, and finite host resource cases."
]
}
```
### Reject a numeric string for an integer schema
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "string",
"value": "41"
},
"selectedProfile": "vouch/2"
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope and statement. This fixture refuses admission before receipt binding or signature verification is reached."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
}
}
```
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 refuses the string input before entry. It does not convert the text 41 into an integer. Product invocation awaits its 2.0 adapter."
}
```
The input is a valid string datum but does not belong to the selected input schema. The schema declaration is documentation notation.
### Qualify output separately
After evaluation, a profile checks the returned Datum against its output schema. A mismatch refuses qualification as a profile result and preserves the canonical outcome. Qualification uses the profile host budget under the [profile work rule](/v2.0/en/docs/profiles/#lispex.rule.v2.profiles.profile-work-separation). It does not rerun guest code. A language failure or resource stop keeps its original outcome.
**Why**
A returned datum already has language meaning. Separate qualification expresses application acceptance without changing that meaning or moving the first evaluation stop.
Claim: `lispex.claim.v2.profiles.output-qualification` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "profile-output-qualification",
"input": "completed-language-outcome",
"schema": "declared-output-schema"
},
"result": {
"kind": "separate-profile-qualification",
"canonicalOutcome": "preserved",
"schemaMismatch": "unqualified-profile-result",
"guestReevaluation": false,
"semanticRequest": "unchanged",
"qualificationResources": "separate-finite-host-resources",
"failureCoercion": false
},
"pendingCases": [
"Each installed product needs output qualification cases with the settled schemas and evidence requirements.",
"Every host qualification resource axis needs cases below, at, and above its finite reservation boundary."
]
}
```
### Qualify a matching output datum
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)
'allow))
)
```
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
},
"selectedProfile": "vouch/2"
}
],
"profileWork": {
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"identity": "submitted-profile-work",
"contract": "lispex.profile-work/2",
"evidenceRequirement": "signed-execution",
"evidenceOperation": "verify the explicitly supplied envelope after output qualification"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"enum",
[
{
"kind": "symbol",
"value": "deny"
},
{
"kind": "symbol",
"value": "allow"
}
]
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
}
}
```
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 symbol allow. Separate qualification accepts that datum and delivers the profile result with its required evidence. Product invocation awaits its 2.0 adapter."
}
```
The declared output schema accepts allow and deny. Qualification uses the separate finite profile host budget.
### Preserve a datum that fails output qualification
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
},
"selectedProfile": "vouch/2"
}
],
"profileWork": {
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"identity": "submitted-profile-work",
"contract": "lispex.profile-work/2",
"evidenceRequirement": "signed-execution",
"evidenceOperation": "verify the explicitly supplied envelope after output qualification"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"enum",
[
{
"kind": "symbol",
"value": "deny"
},
{
"kind": "symbol",
"value": "allow"
}
]
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
}
}
```
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. The output schema refuses profile qualification while the canonical outcome remains that value. Product invocation awaits its 2.0 adapter."
}
```
Input admission accepts the integer. The output schema accepts only the declared decision symbols. Qualification does not rerun or rewrite the rule.
### Keep a language stop during qualification
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 the rule",
"evaluate": "finite work that fails at one loop reservation with all other finite budgets sufficient through that event"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
},
"selectedProfile": "vouch/2"
}
],
"profileWork": {
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"identity": "submitted-profile-work",
"contract": "lispex.profile-work/2",
"evidenceRequirement": "signed-execution",
"evidenceOperation": "verify the explicitly supplied envelope after output qualification"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"enum",
[
{
"kind": "symbol",
"value": "deny"
},
{
"kind": "symbol",
"value": "allow"
}
]
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
},
"evidenceTarget": "the complete resource-stop receipt for the same program, canonical input, resource model, and 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": "Evaluation ends with its original work stop. No datum is available for output qualification and no decision datum is substituted. Product invocation awaits its 2.0 adapter."
}
```
The profile admits the program and input. The first unsatisfied evaluation reservation remains the canonical language failure.
### Stop host qualification without changing 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",
"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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
},
"selectedProfile": "vouch/2"
}
],
"profileWork": {
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"identity": "submitted-profile-work",
"contract": "lispex.profile-work/2",
"evidenceRequirement": "signed-execution",
"evidenceOperation": "verify the explicitly supplied envelope after output qualification"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "The finite W covers all admission host work. The next output qualification reservation exceeds the remaining W. A, F, I, R, and E are sufficient. The evaluation outcome and receipt are complete.",
"fixtureParameters": {
"Evidence0": {
"type": "Bytevector",
"format": "lispex.evidence/2",
"constraint": "One complete supported Ed25519 envelope for the exact canonical receipt of the corresponding base request. The external issuer creates it before the vouch request."
},
"Trust0": {
"type": "Bytevector",
"format": "lispex.trust-policy/2",
"constraint": "One complete supported explicit policy that admits the envelope issuer key and its exact product and artifact tuple."
}
},
"selectedProfile": "vouch/2",
"profileRequest": {
"format": "lispex.profile-request/2",
"declaration": {
"format": "lispex.profile/2",
"profile": "vouch/2",
"schema_language": "lispex.schema/2",
"input_schema": [
"kind",
"integer"
],
"output_schema": [
"kind",
"integer"
],
"libraries": [
{
"identity": "the verified fixed LibraryIdentity from semantics.standardLibrary",
"bindings": [
"*",
"+",
"-",
"/",
"<",
"<=",
"=",
">",
">=",
"abs",
"any",
"append",
"apply",
"assoc",
"boolean=?",
"boolean?",
"bytevector",
"bytevector->list",
"bytevector-append",
"bytevector-length",
"bytevector-slice",
"bytevector-u8-ref",
"bytevector?",
"caar",
"cadr",
"call-with-values",
"car",
"cdar",
"cddr",
"cdr",
"ceiling",
"char->integer",
"char-alphabetic?",
"char-ci<=?",
"char-ci=?",
"char-ci>?",
"char-downcase",
"char-foldcase",
"char-lower-case?",
"char-numeric?",
"char-upcase",
"char-upper-case?",
"char-whitespace?",
"char<=?",
"char=?",
"char>?",
"char?",
"condition-code",
"condition-data",
"condition-phase",
"condition?",
"cons",
"datum?",
"denominator",
"digit-value",
"eq?",
"equal?",
"eqv?",
"even?",
"every",
"expt",
"filter",
"find",
"floor",
"fold-left",
"fold-right",
"for-each",
"gcd",
"integer->char",
"integer?",
"lcm",
"length",
"list",
"list->bytevector",
"list->string",
"list->vector",
"list-ref",
"list-tail",
"list?",
"make-bytevector",
"make-condition",
"make-list",
"make-string",
"make-vector",
"map",
"max",
"member",
"min",
"modulo",
"negative?",
"not",
"null?",
"number->string",
"number?",
"numerator",
"odd?",
"pair?",
"positive?",
"procedure?",
"quantize",
"quotient",
"raise",
"remainder",
"reverse",
"scalar?",
"string",
"string->list",
"string->symbol",
"string->utf8",
"string-append",
"string-ci<=?",
"string-ci=?",
"string-ci>?",
"string-downcase",
"string-foldcase",
"string-length",
"string-normalize-nfc",
"string-normalize-nfd",
"string-normalize-nfkc",
"string-normalize-nfkd",
"string-ref",
"string-upcase",
"string<=?",
"string=?",
"string>?",
"string?",
"substring",
"symbol->string",
"symbol=?",
"symbol?",
"truncate",
"utf8->string",
"values",
"vector",
"vector->list",
"vector-append",
"vector-length",
"vector-ref",
"vector-slice",
"vector?",
"zero?"
]
}
],
"evidence_requirement": "signed-execution",
"work_contract": "lispex.profile-work/2"
},
"evidence": [
"Evidence0"
],
"trust": [
"Trust0"
]
}
}
```
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. The profile host budget prevents a profile result from being issued and preserves the canonical outcome. Product invocation awaits its 2.0 adapter."
}
```
The profile host budget is below the next required qualification reservation. Its numeric value remains part of the pending tariff contract.
See [Profile host budget fields and check schedule](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.profile-work-contract), [Identity domains and encoded inputs](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.identity-encoding), [Admission and profile work report formats](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.admission-report-format), [Resource model numbers](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers).
## Canonical codec
The canonical Datum codec `lispex.datum/2` defines the byte representation used for interchange. It preserves the values defined in [Values and text](/v2.0/en/docs/language/values#lispex.section.v2.values.datum). Exact numeric forms follow [Exact numbers](/v2.0/en/docs/language/numbers).
Text retains its scalar sequence. Admitted host records become immutable association data under the conversion rule below. A host object does not become a guest capability.
Canonical decoding and encoding use the [evaluation resource account](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.separate-phases). Additional schema traversal uses the [profile host budget](/v2.0/en/docs/profiles/#lispex.rule.v2.profiles.profile-work-separation). Input and result channels follow the [channel budget rules](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.channel-budgets). Numeric costs and physical envelopes remain with the resource model.
### Exchange exact canonical data
Use the [canonical Datum byte format](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.datum-byte-format).
Its packet preserves exact values and text scalars.
The [record input contract](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.record-input) defines explicit host adaptation.
The [boundary event schedule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.boundary-events) assigns codec work to its phase account.
**Why**
Canonical interchange lets products compare the same data across platforms. Exact numbers and text remain independent of host numeric width and locale.
Claim: `lispex.claim.v2.profiles.canonical-codec` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "canonical-datum-interchange",
"fixed": "codec-version",
"boundary": "Datum"
},
"result": {
"kind": "exact-value-interchange",
"representationPerDatum": "one",
"exactRoundTrip": true,
"implicitNormalization": false,
"hostCapabilities": false,
"inexactInput": false,
"finiteResources": true
},
"pendingCases": [
"The byte, rejection, and record examples below need product execution.",
"Each product needs exact numeric, Unicode, nesting, and channel boundary cases on supported architectures."
]
}
```
### Preserve exact numbers and text scalars
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "9007199254740993"
}
},
{
"input": {
"kind": "rational",
"numerator": "1",
"denominator": "3"
}
},
{
"input": {
"kind": "string",
"value": "é"
}
},
{
"input": {
"kind": "string",
"value": "é"
}
}
],
"codecOperation": "Encode each typed datum, decode it as input, evaluate, then decode the canonical result.",
"codecVersion": "lispex.datum/2",
"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 input returns unchanged. The large integer and rational stay exact. The two strings retain different scalar sequences and result encodings. Product invocation awaits its 2.0 adapter."
}
```
The request notation uses typed exact data. The byte examples below fix their canonical representation under `lispex.datum/2`.
### Encode equal rational results identically
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)
(/ 2 6)))
)
```
File: `reduced.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(/ 1 3)))
)
```
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"source": "source.scm",
"input": {
"kind": "integer",
"value": "0"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
},
{
"source": "reduced.scm",
"input": {
"kind": "integer",
"value": "0"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "reduced.scm"
}
]
}
],
"codecVersion": "lispex.datum/2",
"comparison": "Encode both returned rational data with the same codec version.",
"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": "Both programs return the exact rational one third. The fixed codec gives their equal result data the same encoding. Product invocation awaits its 2.0 adapter."
}
```
Equal reduced numeric values use the same `lispex.datum/2` packet. Source spelling and decimal scale do not change it.
### Reject a host callback at the codec 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)
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"fixtureValue": "host callback from hostSetup"
}
}
],
"hostSetup": {
"inputKind": "host-callback",
"callbackResult": {
"kind": "integer",
"value": "42"
}
},
"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 callback as a non-Datum input. Neither the callback nor the rule entry is invoked. Product invocation awaits its 2.0 adapter."
}
```
The calling application can supply the result of an external computation as data. It cannot supply a procedure that the guest can invoke.
### Reject an inexact host number
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 finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"fixtureValue": "inexact host number from hostSetup"
}
}
],
"hostSetup": {
"inputKind": "inexact-number",
"description": "a host floating point value"
},
"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 refuses the inexact host number. It does not round the number or convert it to an exact datum. Product invocation awaits its 2.0 adapter."
}
```
The fixture supplies an inexact host value as a rejected input. Lispex exact numeric input must use the canonical exact value contract.
### Use one framed Datum format
The codec identifier is `lispex.datum/2`. A packet contains the fixed magic, a minimal payload length, and one Datum. The byte grammar and tag table below define every accepted representation. Strings and symbols use strict UTF-8. Pairs preserve both components. Vectors preserve element order. Sharing has no byte representation.
CanonicalDatumBytes names one complete packet for a Datum.
CanonicalInputBytes names those same complete bytes when supplied as evaluation input.
Both names include the magic, length, and payload.
A record field that carries either packet uses an explicit bytevector.
A record wrapper is not part of those packet bytes.
**Why**
A small closed grammar assigns one representation to every portable value. Distinct tags keep text, symbols, and characters distinct. One frame gives later identity and receipt formats an exact byte boundary.
Claim: `lispex.claim.v2.profiles.datum-byte-format` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "datum-byte-format",
"codec": "lispex.datum/2",
"input": "finite-Datum"
},
"result": {
"kind": "canonical-framed-datum",
"magicHex": "6c69737065782e646174756d2f3200",
"length": "minimal-unsigned-base128",
"singleRoot": true,
"trailingBytes": false,
"text": "strict-UTF-8",
"sharingReferences": false,
"recordTag": false
},
"pendingCases": [
"Every scalar boundary and every tag combination needs product execution.",
"Deep data and exact channel boundaries need product and architecture cases."
]
}
```
The byte grammar uses hexadecimal octets and scalar bounds. Arithmetic constants are decimal. `U` encodes an exact natural number. `Z` encodes an exact integer.
| Field | Encoding equation |
| --- | --- |
| Packet | `magic U(payload-byte-length) value EOF` |
| Magic | `6c 69 73 70 65 78 2e 64 61 74 75 6d 2f 32 00` |
| Unsigned integer | `U(n) = b[0] ... b[k-1]`, `k >= 1` |
| Integer value | `n = sum((b[i] & 0x7f) * 128^i)` |
| Continuation octet | `b[i] in 0x80..0xff` for `i < k-1` |
| Final octet | `b[k-1] in 0x00..0x7f` |
| Minimal form | `k > 1` requires `b[k-1] != 0x00` |
| Nonnegative integer | `Z(n) = U(2*n)` for `n >= 0` |
| Negative integer | `Z(n) = U(-2*n-1)` for `n < 0` |
| Text payload | `U(byte-length) UTF8[byte-length]` |
| Pair | `08 value value` |
| Vector | `09 U(element-count) value[element-count]` |
| Bytevector | `0a U(byte-length) octet[byte-length]` |
| Datum | Tag | Payload | Required form |
| --- | --- | --- | --- |
| Empty list | `00` | Empty | One empty list value |
| False | `01` | Empty | Boolean false |
| True | `02` | Empty | Boolean true |
| Integer | `03` | `Z(n)` | Exact integer |
| Rational | `04` | `Z(n) U(d)` | `n != 0`, `d > 1`, `gcd(abs(n), d) = 1` |
| Character | `05` | `U(scalar)` | `0000..d7ff` or `e000..10ffff` |
| String | `06` | `text` | Exact scalar sequence |
| Symbol | `07` | `text` | Exact scalar sequence |
| Pair | `08` | `value value` | Car then cdr |
| Vector | `09` | `U(count) value[count]` | Index order |
| Bytevector | `0a` | `U(length) octet[length]` | Byte order |
All other tag octets are invalid. A list uses pair tags ending in the empty list tag. An improper pair remains valid Datum.
Lengths count octets except the vector count. A text length counts its UTF-8 payload, not its scalars. Empty strings and symbols are valid.
Unsigned integers have no machine width limit. The signed mapping gives zero one representation. It has no negative zero code.
Strict UTF-8 uses the shortest encoding of each Unicode scalar. Surrogate values and values above U+10FFFF are invalid.
Unassigned scalars, noncharacters, and U+FEFF inside text remain data. The codec performs no normalization or case conversion.
The outer length covers only the encoded value. Every packet includes the magic and length. Nested values include neither.
Repeated equal subvalues are encoded in full. Reference tags, cycles, extension tags, and implicit record conversion are invalid.
### Encode scalar values with distinct tags
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "empty-list",
"input": {
"kind": "list",
"items": []
},
"encodedInputHex": "6c69737065782e646174756d2f32000100"
},
{
"case": "false",
"input": {
"kind": "boolean",
"value": false
},
"encodedInputHex": "6c69737065782e646174756d2f32000101"
},
{
"case": "true",
"input": {
"kind": "boolean",
"value": true
},
"encodedInputHex": "6c69737065782e646174756d2f32000102"
},
{
"case": "zero",
"input": {
"kind": "integer",
"value": "0"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020300"
},
{
"case": "minus-one",
"input": {
"kind": "integer",
"value": "-1"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020301"
},
{
"case": "one",
"input": {
"kind": "integer",
"value": "1"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020302"
},
{
"case": "positive-varint-boundary",
"input": {
"kind": "integer",
"value": "64"
},
"encodedInputHex": "6c69737065782e646174756d2f320003038001"
},
{
"case": "negative-varint-boundary",
"input": {
"kind": "integer",
"value": "-65"
},
"encodedInputHex": "6c69737065782e646174756d2f320003038101"
},
{
"case": "nul-character",
"input": {
"kind": "character",
"value": "\u0000"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020500"
},
{
"case": "last-scalar",
"input": {
"kind": "character",
"value": ""
},
"encodedInputHex": "6c69737065782e646174756d2f32000405ffff43"
},
{
"case": "empty-string",
"input": {
"kind": "string",
"value": ""
},
"encodedInputHex": "6c69737065782e646174756d2f3200020600"
},
{
"case": "empty-symbol",
"input": {
"kind": "symbol",
"value": ""
},
"encodedInputHex": "6c69737065782e646174756d2f3200020700"
},
{
"case": "string-a",
"input": {
"kind": "string",
"value": "a"
},
"encodedInputHex": "6c69737065782e646174756d2f320003060161"
},
{
"case": "symbol-a",
"input": {
"kind": "symbol",
"value": "a"
},
"encodedInputHex": "6c69737065782e646174756d2f320003070161"
}
],
"codecOperation": "Encode the typed input and compare it with encodedInputHex. Decode those bytes, evaluate identity, and compare the result packet.",
"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 scalar has the stated complete packet. Empty list, empty text, and empty symbol remain distinct. Product invocation awaits its 2.0 adapter."
}
```
Hex strings contain complete packets. Whitespace in displayed hex is only presentation. Fixture JSON is documentation notation.
### Preserve structure and raw text 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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "improper-pair",
"input": {
"kind": "pair",
"car": {
"kind": "integer",
"value": "1"
},
"cdr": {
"kind": "integer",
"value": "2"
}
},
"encodedInputHex": "6c69737065782e646174756d2f3200050803020304"
},
{
"case": "proper-list",
"input": {
"kind": "list",
"items": [
{
"kind": "integer",
"value": "1"
},
{
"kind": "integer",
"value": "2"
}
]
},
"encodedInputHex": "6c69737065782e646174756d2f32000708030208030400"
},
{
"case": "empty-vector",
"input": {
"kind": "vector",
"items": []
},
"encodedInputHex": "6c69737065782e646174756d2f3200020900"
},
{
"case": "empty-bytevector",
"input": {
"kind": "bytevector",
"bytes": []
},
"encodedInputHex": "6c69737065782e646174756d2f3200020a00"
},
{
"case": "bytevector",
"input": {
"kind": "bytevector",
"bytes": [
0,
127,
128,
255
]
},
"encodedInputHex": "6c69737065782e646174756d2f3200060a04007f80ff"
},
{
"case": "raw-decomposed",
"input": {
"kind": "string",
"value": "é"
},
"encodedInputHex": "6c69737065782e646174756d2f320005060365cc81"
},
{
"case": "raw-composed",
"input": {
"kind": "string",
"value": "é"
},
"encodedInputHex": "6c69737065782e646174756d2f3200040602c3a9"
},
{
"case": "repeated-data",
"input": {
"kind": "vector",
"items": [
{
"kind": "pair",
"car": {
"kind": "integer",
"value": "1"
},
"cdr": {
"kind": "list",
"items": []
}
},
{
"kind": "pair",
"car": {
"kind": "integer",
"value": "1"
},
"cdr": {
"kind": "list",
"items": []
}
}
]
},
"encodedInputHex": "6c69737065782e646174756d2f32000a09020803020008030200"
},
{
"case": "text-length-varint",
"input": {
"kind": "string",
"value": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"
},
"encodedInputHex": "6c69737065782e646174756d2f320083010680016161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161"
}
],
"codecOperation": "Encode each typed value. Decode the stated packet as identity input and compare the complete result packet.",
"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": "Pairs, lists, vectors, and bytevectors retain their structure. The two Unicode spellings have different packets. Repeated data is encoded twice. Product invocation awaits its 2.0 adapter."
}
```
The long string crosses a varint boundary. Its length counts UTF-8 octets. No product execution is recorded.
### Encode mathematical numbers exactly
An integer uses the integer tag and the signed mapping in the grammar. A nonintegral rational uses the rational tag. Its numerator is nonzero. Its denominator exceeds one. Their greatest common divisor is one. Equal decimal, rational, and integer values receive equal bytes. The codec stores no decimal scale or signed zero.
**Why**
Numeric spelling does not change a Lispex value. Encoding the reduced value keeps input identities and result bytes independent of presentation. Exact integers avoid a host numeric width or floating point conversion.
Claim: `lispex.claim.v2.profiles.codec-numeric-values` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "canonical-exact-number",
"codec": "lispex.datum/2",
"number": "exact-integer-or-rational"
},
"result": {
"kind": "value-canonical-number-bytes",
"signedMapping": "zigzag",
"integerWidth": "unbounded-exact",
"rationalNumerator": "nonzero",
"rationalDenominator": "greater-than-one",
"reduced": true,
"decimalScale": false,
"negativeZero": false
},
"pendingCases": [
"Large numerator and denominator bit lengths need product boundary cases.",
"Numeric work and allocation stops await the fixed resource model."
]
}
```
### Give equal numeric values equal packets
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "integer-spelling",
"input": {
"kind": "integer",
"value": "1"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020302",
"sourceValueSpelling": "1"
},
{
"case": "rational-spelling",
"input": {
"kind": "integer",
"value": "1"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020302",
"sourceValueSpelling": "1/1"
},
{
"case": "decimal-spelling",
"input": {
"kind": "integer",
"value": "1"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020302",
"sourceValueSpelling": "1.00"
},
{
"case": "decimal-negative-zero",
"input": {
"kind": "integer",
"value": "0"
},
"encodedInputHex": "6c69737065782e646174756d2f3200020300",
"sourceValueSpelling": "-0.00"
},
{
"case": "one-half",
"input": {
"kind": "rational",
"numerator": "1",
"denominator": "2"
},
"encodedInputHex": "6c69737065782e646174756d2f320003040202"
},
{
"case": "minus-one-third",
"input": {
"kind": "rational",
"numerator": "-1",
"denominator": "3"
},
"encodedInputHex": "6c69737065782e646174756d2f320003040103"
},
{
"case": "wide-positive",
"input": {
"kind": "integer",
"value": "1180591620717411303424"
},
"encodedInputHex": "6c69737065782e646174756d2f32000c038080808080808080808002"
},
{
"case": "wide-negative",
"input": {
"kind": "integer",
"value": "-1180591620717411303424"
},
"encodedInputHex": "6c69737065782e646174756d2f32000c03ffffffffffffffffffff01"
}
],
"codecOperation": "Use each exact value or sourceValueSpelling to encode input, decode identity input, and encode its exact result.",
"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 three spellings encode integer one identically. Negative zero encodes zero. Large integers retain all bits. Product invocation awaits its 2.0 adapter."
}
```
The source spellings name exact values in documentation notation. They do not authorize a host floating point conversion.
### Reject alternate number encodings
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "overlong-zero",
"encodedInputHex": "6c69737065782e646174756d2f320003038000"
},
{
"case": "overlong-one",
"encodedInputHex": "6c69737065782e646174756d2f320003038200"
},
{
"case": "unterminated-integer",
"encodedInputHex": "6c69737065782e646174756d2f3200020380"
},
{
"case": "zero-denominator",
"encodedInputHex": "6c69737065782e646174756d2f320003040200"
},
{
"case": "unit-denominator",
"encodedInputHex": "6c69737065782e646174756d2f320003040201"
},
{
"case": "rational-zero",
"encodedInputHex": "6c69737065782e646174756d2f320003040002"
},
{
"case": "unreduced-rational",
"encodedInputHex": "6c69737065782e646174756d2f320003040406"
},
{
"case": "overlong-denominator",
"encodedInputHex": "6c69737065782e646174756d2f32000404028200"
}
],
"codecOperation": "Decode the exact submitted bytes as input to the identity rule.",
"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": "Nonminimal integer fields and noncanonical rational values are refused. The decoder does not reduce or retag them. Product invocation awaits its 2.0 adapter."
}
```
Every hex string is submitted unchanged. The decoder must refuse it without repair or entry evaluation.
### Reject malformed and alternate encodings
Decode the frame before its Datum. Within a Datum, follow the field order in the grammar. Visit a pair car before its cdr and vector elements in index order. Reject the first malformed or noncanonical field. Reject unknown tags, excess bytes, invalid scalars, and every alternate integer or rational encoding. Decoding never repairs input. Complete structural and canonical validation precedes result Datum materialization. An unchecked length or count cannot trigger a bulk result reservation. A rejected input does not invoke entry or produce an evaluation receipt.
**Why**
Accepting alternate spellings would give one value several input byte identities. A fixed validation order also preserves the first failure. Rejecting a packet as a whole prevents a partial value from crossing the input boundary.
Claim: `lispex.claim.v2.profiles.strict-codec-decoding` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "canonical-decode-validation",
"codec": "lispex.datum/2",
"input": "submitted-packet"
},
"result": {
"kind": "strict-first-failure",
"order": [
"magic",
"frame-length",
"frame-boundary",
"payload",
"root-end",
"materialize"
],
"childOrder": "depth-first-car-before-cdr-and-index-order",
"repair": false,
"entryOnInvalidInput": false,
"receiptOnInvalidInput": false,
"validationBeforeMaterialization": true,
"uncheckedAggregateReservation": false,
"validationWorkMetered": true,
"materializationOrder": "depth-first-car-before-cdr-and-index-order"
},
"pendingCases": [
"Product executions must cover combinations of malformed fields and finite resource stops.",
"Future diagnostic codes map these causes without changing the validation order."
]
}
```
The decoder follows this order. Resource reservations use the shared event rules before the corresponding work or allocation.
| Step | Validation | Rejection cause |
| --- | --- | --- |
| Magic | Compare each magic octet from the start | `magic` at the first mismatch or missing octet |
| Frame length | Read one terminating minimal `U` | `unterminated-integer` or `nonminimal-integer` |
| Frame boundary | Compare the declared payload length with all remaining octets | `truncated-frame` or `trailing-frame-data` |
| Value tag | Read the next tag in traversal order | `missing-value` or `unknown-tag` |
| Integer field | Read a terminating minimal `U` before interpreting it | `unterminated-integer` or `nonminimal-integer` |
| Rational fields | Read numerator then denominator, then check denominator, numerator, and reduction | `rational-denominator`, `rational-zero`, or `unreduced-rational` |
| Character | Check the scalar after decoding `U` | `invalid-scalar` |
| Text or bytes | Read the length, check remaining bytes, then consume that exact slice | `truncated-sequence` |
| Text scalar | Check UTF-8 from the start of the declared slice | `invalid-utf8` at the first invalid sequence |
| Pair | Decode car completely, then cdr completely | The first child failure |
| Vector | Read the count, then decode that many children | The first child failure |
| Root end | Require the root to consume the payload exactly | `trailing-value-data` |
| Materialization | Reserve and construct the validated Datum in depth-first car, cdr, and index order | A resource stop |
The decoder completes structural and canonical validation before materializing its result Datum. It does not reserve or allocate a result container from an unchecked length or count. Validation workspace, traversal, and exact numeric checks still consume metered work and storage. Every event reserves its resources before the corresponding check or effect. After validation, result reservations and materialization follow depth-first car, cdr, and index order.
Text validation rejects overlong encodings, isolated continuation bytes, truncated sequences, surrogates, and out-of-range scalars.
It does not substitute replacement characters. A missing UTF-8 continuation fails within the declared text slice.
The cause names describe codec failures. The [diagnostic catalog](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.catalog) supplies public codes and reports.
Every malformed input is refused before entry. It produces no canonical evaluation outcome or evaluation receipt.
Canonical decoding still uses the evaluation resource account. A resource stop follows the shared resource rules.
| Event name | Required work |
| --- | --- |
| `codec-frame` | Open or finish one packet |
| `codec-byte` | Consume or emit an octet in byte order |
| `codec-value` | Visit a Datum in depth-first order |
| `codec-integer` | Interpret or size an exact integer field |
| `codec-scalar` | Validate or encode one text scalar |
| `codec-rational-check` | Check a rational in the stated field order |
| `codec-allocation` | Reserve logical data and buffer allocation before materialization |
| `record-order` | Establish canonical field order from the complete name collection |
| `record-key` | Check the next name in canonical order |
| `record-field` | Convert the next value in canonical order |
Encoding validates the Datum and determines its payload length before emitting a packet.
It follows the same value and field order as decoding. Result bytes become available only when the complete packet succeeds.
Host widths, caching, sharing, and allocation strategies do not change semantic events.
The [resource event catalog](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.event-catalog) owns their accounting details.
Tariffs, allocation units, finite defaults, and physical envelopes remain under the [cost model freeze](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers).
### Reject malformed packet frames
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "wrong-magic",
"encodedInputHex": "0069737065782e646174756d2f32000100"
},
{
"case": "truncated-magic",
"encodedInputHex": "6c69737065782e646174756d2f32"
},
{
"case": "missing-length",
"encodedInputHex": "6c69737065782e646174756d2f3200"
},
{
"case": "overlong-length",
"encodedInputHex": "6c69737065782e646174756d2f3200810000"
},
{
"case": "short-payload",
"encodedInputHex": "6c69737065782e646174756d2f32000200"
},
{
"case": "extra-octet",
"encodedInputHex": "6c69737065782e646174756d2f3200010000"
},
{
"case": "concatenated-packets",
"encodedInputHex": "6c69737065782e646174756d2f320001006c69737065782e646174756d2f32000100"
},
{
"case": "empty-payload",
"encodedInputHex": "6c69737065782e646174756d2f320000"
},
{
"case": "unknown-tag",
"encodedInputHex": "6c69737065782e646174756d2f320001ff"
},
{
"case": "second-root",
"encodedInputHex": "6c69737065782e646174756d2f3200020000"
}
],
"codecOperation": "Decode the exact submitted bytes as input to the identity rule.",
"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": "All frames are refused. Framing checks precede payload interpretation. Product invocation awaits its 2.0 adapter."
}
```
Every hex string is submitted unchanged. The decoder must refuse it without repair or entry evaluation.
### Reject invalid Unicode encodings
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "overlong-utf8",
"encodedInputHex": "6c69737065782e646174756d2f3200040602c080"
},
{
"case": "isolated-continuation",
"encodedInputHex": "6c69737065782e646174756d2f320003060180"
},
{
"case": "surrogate-utf8",
"encodedInputHex": "6c69737065782e646174756d2f3200050703eda080"
},
{
"case": "out-of-range-utf8",
"encodedInputHex": "6c69737065782e646174756d2f3200060604f4908080"
},
{
"case": "truncated-scalar-in-slice",
"encodedInputHex": "6c69737065782e646174756d2f3200030601c3"
},
{
"case": "truncated-text-payload",
"encodedInputHex": "6c69737065782e646174756d2f3200030602c3"
},
{
"case": "surrogate-character",
"encodedInputHex": "6c69737065782e646174756d2f3200040580b003"
},
{
"case": "out-of-range-character",
"encodedInputHex": "6c69737065782e646174756d2f32000405808044"
},
{
"case": "overlong-character",
"encodedInputHex": "6c69737065782e646174756d2f320003058000"
}
],
"codecOperation": "Decode the exact submitted bytes as input to the identity rule.",
"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": "Invalid UTF-8 and invalid character scalars are refused without replacement. Declared text slices define sequence boundaries. Product invocation awaits its 2.0 adapter."
}
```
Every hex string is submitted unchanged. The decoder must refuse it without repair or entry evaluation.
### Reject incomplete aggregate payloads
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for all structural and numeric validation in these packets, below the reservation needed for the huge declared vector"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "missing-pair-cdr",
"encodedInputHex": "6c69737065782e646174756d2f320003080302"
},
{
"case": "missing-vector-element",
"encodedInputHex": "6c69737065782e646174756d2f320003090200"
},
{
"case": "truncated-bytevector",
"encodedInputHex": "6c69737065782e646174756d2f3200030a0200"
},
{
"case": "overlong-vector-count",
"encodedInputHex": "6c69737065782e646174756d2f320003098000"
},
{
"case": "overlong-text-length",
"encodedInputHex": "6c69737065782e646174756d2f320003068000"
},
{
"case": "reference-tag",
"encodedInputHex": "6c69737065782e646174756d2f3200010b"
},
{
"case": "huge-vector-count-without-elements",
"encodedInputHex": "6c69737065782e646174756d2f32000c098080808080808080808001"
}
],
"codecOperation": "Decode the exact submitted bytes as input to the identity rule.",
"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 pair and vector must contain its full declared children. Byte lengths are exact. The huge vector count fails at its missing first child before any result container reservation. Product invocation awaits its 2.0 adapter."
}
```
Every packet is submitted unchanged. The last count exceeds a host word. Its symbolic budget permits complete validation but not a vector reservation of that count. The decoder refuses missing structure before result materialization.
### Keep the first codec failure stable
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "frame-before-tag",
"encodedInputHex": "6c69737065782e646174756d2f320002ff"
},
{
"case": "numerator-before-denominator",
"encodedInputHex": "6c69737065782e646174756d2f32000404800000"
},
{
"case": "denominator-before-zero",
"encodedInputHex": "6c69737065782e646174756d2f320003040000"
},
{
"case": "car-before-cdr",
"encodedInputHex": "6c69737065782e646174756d2f320006080602c080ff"
},
{
"case": "vector-index-order",
"encodedInputHex": "6c69737065782e646174756d2f3200060902040406ff"
}
],
"codecOperation": "Decode the exact submitted bytes as input to the identity rule.",
"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": "Frame length wins before an unknown payload tag. Numerator syntax wins before denominator value. Car and earlier vector elements fail first. Product invocation awaits its 2.0 adapter."
}
```
Every hex string is submitted unchanged. The decoder must refuse it without repair or entry evaluation.
### Convert admitted records into ordered association data
The [record input contract](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.record-input) supplies fields with exact Unicode string names.
Each key Datum is that unchanged string. Order fields by unsigned UTF-8 name bytes. Reject duplicate names before visiting any value. Then convert values in that order. Emit a proper list of pairs with the key in car and the value in cdr. An empty record becomes the empty list. Encoding an ordinary association list preserves its existing order.
**Why**
Records need deterministic conversion without adding a guest map kind. Sorting exact names makes host enumeration irrelevant. Checking all keys first gives duplicate keys priority over failures in field values. Keeping ordinary lists ordered preserves their existing Datum meaning.
Claim: `lispex.claim.v2.profiles.host-record-conversion` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "admitted-host-record-conversion",
"keyPolicy": "profile-selected-exact-name-preserving",
"destination": "Datum"
},
"result": {
"kind": "canonical-association-list",
"order": "unsigned-UTF-8-name-bytes",
"duplicates": "reject-before-values",
"valueOrder": "sorted-name-order",
"pairShape": [
"key",
"value"
],
"emptyRecord": "empty-list",
"ordinaryAssociationListReordered": false,
"hostEnumerationObserved": false
},
"pendingCases": [
"Each admitted host input form and key kind needs cases after profile declarations settle admission.",
"Product executions must verify nested record and finite conversion budget boundaries."
]
}
```
The [record input contract](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.record-input) admits the explicit packet and its string keys.
The codec applies this conversion after that admission.
| Stage | Required behavior |
| --- | --- |
| Name view | Use the complete finite collection of exact Unicode string field names |
| Order | Compare unsigned UTF-8 bytes lexicographically, with the shorter prefix first |
| Key check | Reject the first duplicate name in sorted order before inspecting any field value |
| Value conversion | Visit field values in sorted name order and convert nested admitted records by the same rule |
| Association data | Construct one dotted pair per field and a proper list containing those pairs |
| Encoding | Encode that ordinary Datum with `lispex.datum/2` |
The key policy preserves names without normalization, case folding, or string coercion.
An inadmissible name or nonpreserving key policy fails profile admission. Field values must become Datum.
Callbacks, accessors, cycles, inexact numbers, and other host capabilities are refused without invocation.
The `record-order` reservation covers ordering work for the whole name collection.
Its event parameters depend on the collection, not host enumeration. Key checks and value conversion follow the resulting order.
Different source enumerations produce the same association data and host conversion events.
The mapping uses no record byte tag. Decoding the resulting packet returns association data.
An ordinary list can contain repeated keys or any element order. The Datum decoder preserves that list without record checks.
[Profile declarations](/v2.0/en/docs/profiles#lispex.rule.v2.profiles.profile-declarations) select the public host forms and admitted key kinds.
Record adaptation and its complete output encoding use the profile host budget.
The report axis covers the converted input packet.
The [boundary event schedule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.boundary-events) selects the account for each codec operation.
The evaluator decodes that packet under EvaluationLimits.
It uses the same evaluation events as a caller that supplies those canonical bytes directly.
Schema work remains in the profile host budget.
### Give admitted record permutations equal 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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "record-permutation-one",
"input": {
"kind": "host-record",
"fields": [
{
"key": "é",
"value": {
"kind": "integer",
"value": "1"
}
},
{
"key": "a",
"value": {
"kind": "integer",
"value": "3"
}
},
{
"key": "é",
"value": {
"kind": "integer",
"value": "2"
}
}
]
},
"operation": "explicit typed record admission followed by base evaluation of its canonical output"
},
{
"case": "record-permutation-two",
"input": {
"kind": "host-record",
"fields": [
{
"key": "é",
"value": {
"kind": "integer",
"value": "2"
}
},
{
"key": "a",
"value": {
"kind": "integer",
"value": "3"
}
},
{
"key": "é",
"value": {
"kind": "integer",
"value": "1"
}
}
]
},
"operation": "explicit typed record admission followed by base evaluation of its canonical output"
},
{
"case": "empty-record",
"input": {
"kind": "host-record",
"fields": []
},
"operation": "explicit typed record admission followed by base evaluation of its canonical output"
},
{
"case": "ordinary-unsorted-list",
"input": {
"kind": "list",
"items": [
{
"kind": "pair",
"car": {
"kind": "string",
"value": "b"
},
"cdr": {
"kind": "integer",
"value": "2"
}
},
{
"kind": "pair",
"car": {
"kind": "string",
"value": "a"
},
"cdr": {
"kind": "integer",
"value": "1"
}
}
]
},
"operation": "ordinary base evaluation"
},
{
"case": "ordinary-repeated-keys",
"input": {
"kind": "list",
"items": [
{
"kind": "pair",
"car": {
"kind": "string",
"value": "a"
},
"cdr": {
"kind": "integer",
"value": "1"
}
},
{
"kind": "pair",
"car": {
"kind": "string",
"value": "a"
},
"cdr": {
"kind": "integer",
"value": "2"
}
}
]
},
"operation": "ordinary base evaluation"
}
],
"recordMapping": {
"admission": "The caller explicitly selects record admission with the verified base builtin contract. The operation takes no program, declaration, schema, or evidence. Successful conversion returns CanonicalInputBytes for later evaluation.",
"keyDatum": "the unchanged field name as a string",
"keyOrder": "ascending unsigned UTF-8 name bytes",
"duplicates": "reject before visiting values",
"datumRepresentation": "proper list of pairs with key in car and value in cdr",
"invalidHostValues": "Live host values remain typed rejection fixtures. They are never encoded into a lispex.record/2 packet and are never invoked."
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"recordAdmissionProfile": "base",
"recordAdmissionHasProgram": false,
"recordAdmissionHasDeclaration": false,
"recordAdmissionPerformsSchemaOrEvidence": 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": "The two records produce equal ordered association data and equal packets. Empty records become the empty list. Ordinary lists retain order and repeated keys. Product invocation awaits its 2.0 adapter."
}
```
The fixture selects string keys for these cases. Public host input forms and other admitted key kinds belong to profile declarations.
### Check record keys before field values
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": "the fixed Unicode semantics from Values and text",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to reach the stated codec result"
},
"codecVersion": "lispex.datum/2",
"requests": [
{
"case": "duplicate-before-malformed-child",
"operation": "explicit typed record admission from RecordInputBytes",
"recordInput": {
"format": "lispex.record/2",
"value": [
"record",
[
[
"z",
[
"unknown-z"
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "1"
}
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "2"
}
]
]
]
]
}
},
{
"case": "first-duplicate-in-key-order",
"operation": "explicit typed record admission from RecordInputBytes",
"recordInput": {
"format": "lispex.record/2",
"value": [
"record",
[
[
"b",
[
"datum",
{
"kind": "integer",
"value": "1"
}
]
],
[
"b",
[
"datum",
{
"kind": "integer",
"value": "2"
}
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "1"
}
]
],
[
"a",
[
"datum",
{
"kind": "integer",
"value": "2"
}
]
]
]
]
}
},
{
"case": "malformed-children-in-key-order",
"operation": "explicit typed record admission from RecordInputBytes",
"recordInput": {
"format": "lispex.record/2",
"value": [
"record",
[
[
"z",
[
"unknown-z"
]
],
[
"a",
[
"unknown-a"
]
]
]
]
}
}
],
"recordMapping": {
"admission": "The caller explicitly selects record admission with the verified base builtin contract. The operation takes no program, declaration, schema, or evidence. Successful conversion returns CanonicalInputBytes for later evaluation.",
"keyDatum": "the unchanged field name as a string",
"keyOrder": "ascending unsigned UTF-8 name bytes",
"duplicates": "reject before visiting values",
"datumRepresentation": "proper list of pairs with key in car and value in cdr"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"profileHostBudget": {
"format": "lispex.profile-host-budget/2",
"resource_model": "verified fixture host ResourceModelIdentity",
"work": "W",
"allocation": "A",
"frames": "F",
"input": "I",
"report": "R",
"evidence": "E"
},
"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"
},
"profileNotation": "This is documentation notation. Schema arrays denote Datum vectors. Identity labels and the named budget, evidence, and trust parameters stand for concrete values of their declared types.",
"hostBudgetConditions": "All six finite host fields satisfy the selected host model and cover the stated stages. The terminal report reservation completes before evaluation.",
"recordAdmissionProfile": "base",
"recordAdmissionHasProgram": false,
"recordAdmissionHasDeclaration": false,
"recordAdmissionPerformsSchemaOrEvidence": false,
"recordNotation": "JSON arrays in value denote InputNode vectors. Malformed tags are ordinary encoded Datum. They are not live host values."
}
```
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": "Duplicate a is rejected before any child node. Without duplicates, malformed child a is inspected before z. Product invocation awaits its 2.0 adapter."
}
```
Each malformed child is an ordinary Datum vector inside RecordInputBytes.
Duplicate names are rejected before child conversion.
Child conversion follows canonical name order.
The diagnosticIdentity and diagnosticDataProjection fields are documentation projections.
A complete report retains every required catalog field.
These examples remain not-run.
See [Resource model numbers](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers).
## Related chapters
[Sandbox contract](/v2.0/en/docs/language/sandbox-contract)
[Values and text](/v2.0/en/docs/language/values)
[Preparation and modules](/v2.0/en/docs/tools/prepare)
[Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay)
[Embedding and packages](/v2.0/en/docs/tools/embedding)
### 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)
[Preparation and modules](/v2.0/en/docs/tools/prepare)
[Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay)
[Embedding and packages](/v2.0/en/docs/tools/embedding)