I.1장
Sandbox contract
Run a rule with explicit data and finite limits. The same semantic request has the same outcome in every conforming product.
번역이 없는 문장은 영어 원문으로 보입니다
Scope
Lispex is a sandboxed rule language. Every program follows the same three guarantees.
The same semantic request produces the same outcome. A program receives outside information through supplied data. Finite limits end execution when the request cannot finish.
These are Lispex 2.0 rules. The product plans remain not run until a suitable 2.0 product and observation adapter are available.
Sandbox guarantees
1.1 Every program uses the sandbox contract
Every Lispex program has deterministic outcomes, no access to external resources, and finite execution limits. Every public product applies this contract.
Why
A caller needs the same safety contract when choosing a product or profile. Making it the default removes a route around the rule boundary.
One datum through each product
lispex.example.v2.sandbox-contract.one-value · 1판
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
요청과 파일
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
42결과 상세
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.
제품 실행
예상 결과
The rule returns the exact integer 42 as one result datum. Product invocation awaits its 2.0 adapter.
The rule returns the input datum 42. Separate Native, npm, and WASM plans check the same result under finite limits.
Semantic request
A semantic request fixes the canonical program and input Datum. It also fixes the language, library, Unicode semantics, resource model, and finite limits. Compare completed evaluations using their canonical outcomes.
Preparation defines the resolved program. Identity domains distinguish that program from exact source bytes and engine artifact bytes.
Two different programs can compute the same value and use different resources. Determinism compares the same semantic request.
The examples use request.json as documentation notation. The CLI and value interchange chapters define the concrete product forms.
1.2 Repeat the same semantic request
Every conforming execution of the same semantic request produces the same outcome. This includes the first semantic failure and any resource stop.
Why
A caller can repeat a decision only when every part of the request is fixed. Hidden implementation choices must leave that decision unchanged.
The independent phase budgets and cache preservation rules apply to every semantic request.
Repeat a request after preparation
lispex.example.v2.sandbox-contract.repeat-request · 1판
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(+ input 1)))
)
요청과 파일
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "41"
}
},
{
"input": {
"kind": "integer",
"value": "41"
}
}
],
"executionContexts": [
"cold preparation cache",
"warm preparation cache"
],
"comparison": "Use the same semantic request for both evaluations.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
42결과 상세
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}42결과 상세
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.
의미 상세
{
"comparison": {
"canonicalOutcomeEqual": true,
"evaluationChargesEqual": true
}
}제품 실행
예상 결과
Both evaluations return the exact integer 42. Their canonical outcomes and evaluation charges are equal. Product invocation awaits its 2.0 adapter.
The program and input stay fixed. Preparation may use a cold or warm cache. The product plan compares the outcomes and evaluation charges.
Data boundary
The calling application gathers external facts before it invokes a rule. It supplies them through the entry boundary and presents the returned Datum.
The closed-bundle rule governs dependencies supplied during preparation.
1.3 Pass outside facts as data
A rule receives outside information through its input datum. Guest code cannot perform file, network, clock, random, or display operations. Host callbacks cannot cross the input boundary.
Why
Explicit input makes the facts used by a rule visible. It also keeps changes in the host environment outside the rule.
Supply a fact as an input datum
lispex.example.v2.sandbox-contract.supplied-fact · 1판
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
요청과 파일
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"inputMeaning": "The calling application supplies the fact represented by 42.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
42결과 상세
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.
제품 실행
예상 결과
The supplied datum 42 returns as the sole result datum. Product invocation awaits its 2.0 adapter.
The calling application supplies the outside fact as data. The rule returns that datum. The product plan checks the value boundary.
Reject a request for the host clock
lispex.example.v2.sandbox-contract.external-clock · 3판
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(current-second)))
)
요청과 파일
{
"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": "0"
}
}
],
"operationUnderTest": "Attempt to obtain host time without a supplied time datum.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
library.reference결과 상세
{
"kind": "failure",
"valueCount": 0,
"diagnostic": {
"phase": "resolve",
"code": "library.reference",
"data": {
"name": "current-second",
"reason": "removed-operation"
}
}
}명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.
의미 상세
{
"externalAccess": {
"clock": false
},
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}제품 실행
예상 결과
The request fails and returns no datum. Guest code does not read the host clock. Product invocation awaits its 2.0 adapter.
The source attempts to read the host clock. The product plan checks failure and verifies that guest code receives no clock access. Host timing for execution evidence remains separate. Resolution reports library.reference with removed-operation. The diagnostic catalog defines its fields.
Reject a host callback as input
lispex.example.v2.sandbox-contract.host-callback · 3판
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
요청과 파일
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"fixtureValue": "host callback from hostSetup"
}
}
],
"hostSetup": {
"inputKind": "host-callback",
"callbackResult": {
"kind": "integer",
"value": "42"
}
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
input.value결과 상세
{
"kind": "admission-failure",
"valueCount": 0,
"diagnostic": {
"phase": "admission",
"code": "input.value",
"data": {
"actual": "host-capability",
"path": []
}
}
}명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.
의미 상세
{
"entryEvaluated": false,
"callbackInvocations": 0,
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}제품 실행
예상 결과
Admission rejects the host callback as a non-Datum input. The entry and callback are not invoked. Product invocation awaits its 2.0 adapter.
The request describes a host value that is a callback. The product plan submits that value at the host boundary and checks rejection before evaluation.
Execution limits
1.4 Finish within finite limits
Every public entry point applies the finite-limit rule. Separate phase budgets govern preparation and evaluation. These limits end uncompleted requests with a defined failure.
Why
A caller must regain control after each request. Finite budgets turn unending work into a defined failure.
The resource event order determines the first failed reservation. Channel budgets apply to input, results, and diagnostics.
The symbolic limits in these examples stand for finite values. The tariff and default numeric limits will be fixed after implementation and attack tests.
Stop an unending rule
lispex.example.v2.sandbox-contract.unending-rule · 2판
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ()
(loop))))
)
요청과 파일
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient to enter the loop"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop결과 상세
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"diagnosticIdentity": {
"phase": "evaluate",
"code": "resource.exhausted"
}
}명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.
의미 상세
{
"returnedControl": true
}제품 실행
예상 결과
Evaluation ends with a terminal resource stop and returns no datum. Product invocation awaits its 2.0 adapter.
The loop has no successful return path. The product plan checks that finite limits end evaluation and return control to the calling application.
Profiles, products, and engines
A profile chooses which programs and data it accepts. A product packages an implementation. An engine evaluates the accepted program.
Native, npm, and WASM have separate product plans. Every supported engine must meet the same request contract. A recorded observation identifies the product and engine that supplied it.
1.5 Keep meaning when a profile admits a request
A profile applies its admission requirements and evidence requirements. Requests admitted by two profiles follow the shared-meaning rule.
Why
A profile adds a condition for admission. Preserving meaning lets callers compare a request across products and profiles.
Compare an admitted request across profiles
lispex.example.v2.sandbox-contract.admitted-profiles · 1판
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
요청과 파일
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "17"
},
"profileRole": "base language"
},
{
"input": {
"kind": "integer",
"value": "17"
},
"profileRole": "narrower admission that accepts this source and input"
}
],
"comparison": "Both profiles admit the same canonical program, input, semantics, resource model, and limits.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
17결과 상세
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "17"
}
}17결과 상세
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "17"
}
}명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.
의미 상세
{
"comparison": {
"canonicalOutcomeEqual": true
}
}제품 실행
예상 결과
Both admitted requests return the exact integer 17. Their canonical outcomes are equal. Product invocation awaits its 2.0 adapter.
The profile roles describe two admissions of the same request. The product plan compares their outcomes. Concrete profile identifiers belong to Profiles and value interchange.