Lispex 2.0 specification · not released · Tested product not run · Examples not run

<a id="lispex.page.v2.sandbox-contract"></a>

# Sandbox contract

Run a rule with explicit data and finite limits. The same semantic request has the same outcome in every conforming product.

Canonical: /v2.0/en/docs/language/sandbox-contract

Document revision: 2.0-draft-1. Content locale: en. Translation: current.

- language: `lispex`
- languageVersion: `2.0`

<a id="lispex.section.v2.sandbox-contract.scope"></a>

## 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.

<a id="lispex.section.v2.sandbox-contract.sandbox-guarantees"></a>

## Sandbox guarantees

<a id="lispex.rule.v2.sandbox-contract.every-program"></a>

### 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.

<a id="lispex.claim.v2.sandbox-contract.every-program"></a>

Claim: `lispex.claim.v2.sandbox-contract.every-program` · structural · coverage partial · verification not-run

- language: `lispex`
- languageVersion: `2.0`

```json
{
  "predicate": {
    "kind": "public-program-execution",
    "programs": "all",
    "surfaces": "all-public-entrypoints"
  },
  "result": {
    "kind": "sandbox-contract",
    "guarantees": [
      "deterministic-outcome",
      "no-ambient-authority",
      "finite-execution"
    ]
  },
  "pendingCases": [
    "Every public entry point and supported engine requires direct product cases for all three guarantees."
  ]
}
```

<a id="lispex.example.v2.sandbox-contract.one-value"></a>

### One datum through each product

Mode: illustrative. Stage: semantic-request. Verification: not-run.

- language: `lispex`
- languageVersion: `2.0`

File: `source.scm`

```lispex
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      input))
)
```

File: `request.json`

```lispex
{
  "notation": "documentation-request",
  "source": "source.scm",
  "semantics": {
    "language": "Lispex 2.0",
    "standardLibrary": "one fixed library identity",
    "unicode": "one fixed Unicode semantics version",
    "resourceModel": "one fixed finite resource model"
  },
  "limits": {
    "prepare": "finite values sufficient to prepare this source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "42"
      }
    }
  ],
  "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 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.

<a id="lispex.section.v2.sandbox-contract.semantic-request"></a>

## Semantic request

A semantic request fixes the [canonical program](/v2.0/en/docs/tools/prepare#lispex.section.v2.prepare.resolved-program) and input [Datum](/v2.0/en/docs/language/values#lispex.section.v2.values.datum). It also fixes the language, library, Unicode semantics, resource model, and finite limits. Compare completed evaluations using their [canonical outcomes](/v2.0/en/docs/profiles/receipt-and-replay#lispex.section.v2.receipt-and-replay.canonical-outcome).

[Preparation](/v2.0/en/docs/tools/prepare#lispex.section.v2.prepare.resolved-program) defines the resolved program. [Identity domains](/v2.0/en/docs/profiles/receipt-and-replay#lispex.section.v2.receipt-and-replay.identities) 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.

<a id="lispex.rule.v2.sandbox-contract.same-request"></a>

### 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.

<a id="lispex.claim.v2.sandbox-contract.same-request"></a>

Claim: `lispex.claim.v2.sandbox-contract.same-request` · interaction · coverage partial · verification not-run

- language: `lispex`
- languageVersion: `2.0`

```json
{
  "predicate": {
    "kind": "semantic-request-repeat",
    "fixed": [
      "canonical-program",
      "language-semantics",
      "standard-library",
      "unicode-semantics",
      "canonical-input",
      "resource-model",
      "finite-limits"
    ]
  },
  "result": {
    "kind": "deterministic-outcome",
    "same": [
      "returned-datum-or-failure",
      "first-failure",
      "resource-axis-and-canonical-site"
    ],
    "cacheChangesEvaluationCharges": false
  },
  "pendingCases": [
    "Every supported engine and architecture requires repeated successful and failing requests with cold and warm caches."
  ]
}
```

The [independent phase budgets](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.separate-phases) and [cache preservation](/v2.0/en/docs/tools/prepare#lispex.rule.v2.prepare.cache-preservation) rules apply to every semantic request.

<a id="lispex.example.v2.sandbox-contract.repeat-request"></a>

### Repeat a request after preparation

Mode: illustrative. Stage: semantic-request. Verification: not-run.

- language: `lispex`
- languageVersion: `2.0`

File: `source.scm`

```lispex
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (+ input 1)))
)
```

File: `request.json`

```lispex
{
  "notation": "documentation-request",
  "source": "source.scm",
  "semantics": {
    "language": "Lispex 2.0",
    "standardLibrary": "one fixed library identity",
    "unicode": "one fixed Unicode semantics version",
    "resourceModel": "one fixed finite resource model"
  },
  "limits": {
    "prepare": "finite values sufficient to prepare this source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "41"
      }
    },
    {
      "input": {
        "kind": "integer",
        "value": "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"
    }
  ]
}
```

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 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.

<a id="lispex.section.v2.sandbox-contract.data-boundary"></a>

## Data boundary

The calling application gathers external facts before it invokes a rule. It supplies them through the [entry boundary](/v2.0/en/docs/language/procedures#lispex.section.v2.procedures.rule-entry) and presents the returned [Datum](/v2.0/en/docs/language/values#lispex.section.v2.values.datum).

The [closed-bundle rule](/v2.0/en/docs/tools/prepare#lispex.rule.v2.prepare.closed-bundle) governs dependencies supplied during preparation.

<a id="lispex.rule.v2.sandbox-contract.data-only"></a>

### 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.

<a id="lispex.claim.v2.sandbox-contract.data-only"></a>

Claim: `lispex.claim.v2.sandbox-contract.data-only` · boundary · coverage partial · verification not-run

- language: `lispex`
- languageVersion: `2.0`

```json
{
  "predicate": {
    "kind": "rule-host-boundary",
    "input": "Datum",
    "result": "Datum"
  },
  "result": {
    "kind": "value-only-boundary",
    "ambientAccess": false,
    "hostCallbacks": false,
    "guestIO": false,
    "displayOwner": "calling-application"
  },
  "pendingCases": [
    "Every admitted operation requires checks for external resource access and host capability injection."
  ]
}
```

<a id="lispex.example.v2.sandbox-contract.supplied-fact"></a>

### Supply a fact as an input 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)
      input))
)
```

File: `request.json`

```lispex
{
  "notation": "documentation-request",
  "source": "source.scm",
  "semantics": {
    "language": "Lispex 2.0",
    "standardLibrary": "one fixed library identity",
    "unicode": "one fixed Unicode semantics version",
    "resourceModel": "one fixed finite resource model"
  },
  "limits": {
    "prepare": "finite values sufficient to prepare this source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "42"
      }
    }
  ],
  "inputMeaning": "The calling application supplies the fact represented by 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": "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.

<a id="lispex.example.v2.sandbox-contract.external-clock"></a>

### Reject a request for the host clock

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)
      (current-second)))
)
```

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": "0"
      }
    }
  ],
  "operationUnderTest": "Attempt to obtain host time without a supplied time datum.",
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
```

Fixture inputs and environment:

```json
{
  "entry": "source.scm",
  "argv": [],
  "stdin": "",
  "cwd": ".",
  "environment": [],
  "wrapper": null,
  "packageRef": null,
  "lockRef": null,
  "generatedBindingRefs": {
    "knowledgeState": "not-applicable",
    "values": []
  }
}
```

#### Expected result

```json
{
  "status": "unspecified",
  "reason": "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](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.catalog) defines its fields.

<a id="lispex.example.v2.sandbox-contract.host-callback"></a>

### Reject a host callback as input

Mode: illustrative. Stage: semantic-request. Verification: not-run.

- language: `lispex`
- languageVersion: `2.0`

File: `source.scm`

```lispex
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      input))
)
```

File: `request.json`

```lispex
{
  "notation": "documentation-request",
  "source": "source.scm",
  "semantics": {
    "language": "Lispex 2.0",
    "standardLibrary": "one fixed library identity",
    "unicode": "one fixed Unicode semantics version",
    "resourceModel": "one fixed finite resource model"
  },
  "limits": {
    "prepare": "finite values sufficient to prepare this source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "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 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.

See [Concrete entry declaration and admission](/v2.0/en/docs/language/procedures#lispex.rule.v2.procedures.entry-declaration), [Module grammar and initialization](/v2.0/en/docs/tools/prepare#lispex.rule.v2.prepare.module-forms), [Diagnostic catalog and reports](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.catalog), [Concrete command forms](/v2.0/en/docs/tools/run#lispex.rule.v2.cli-and-diagnostics.command-forms), [Artifact and package formats](/v2.0/en/docs/tools/embedding#lispex.rule.v2.embedding.artifact-format).

<a id="lispex.section.v2.sandbox-contract.execution-limits"></a>

## Execution limits

<a id="lispex.rule.v2.sandbox-contract.finite-execution"></a>

### Finish within finite limits

Every public entry point applies the [finite-limit rule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.finite-entrypoints). [Separate phase budgets](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.separate-phases) 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.

<a id="lispex.claim.v2.sandbox-contract.finite-execution"></a>

Claim: `lispex.claim.v2.sandbox-contract.finite-execution` · boundary · coverage partial · verification not-run

- language: `lispex`
- languageVersion: `2.0`

```json
{
  "predicate": {
    "kind": "public-execution-limits",
    "phases": [
      "prepare",
      "evaluate"
    ],
    "default": "finite"
  },
  "result": {
    "kind": "finite-request",
    "outcomes": [
      "value",
      "defined-failure"
    ],
    "resourceStop": "terminal",
    "budgets": [
      "work",
      "logical-allocation",
      "frames",
      "channels"
    ]
  },
  "pendingCases": [
    "Preparation, value encoding, diagnostics, and each resource axis require separate cases below, at, and above the limit."
  ]
}
```

The [resource event order](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.event-order) determines the first failed reservation. [Channel budgets](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.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.

<a id="lispex.example.v2.sandbox-contract.unending-rule"></a>

### Stop an unending rule

Mode: illustrative. Stage: semantic-request. Verification: not-run.

- language: `lispex`
- languageVersion: `2.0`

File: `source.scm`

```lispex
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (let loop ()
        (loop))))
)
```

File: `request.json`

```lispex
{
  "notation": "documentation-request",
  "source": "source.scm",
  "semantics": {
    "language": "Lispex 2.0",
    "standardLibrary": "one fixed library identity",
    "unicode": "one fixed Unicode semantics version",
    "resourceModel": "one fixed finite resource model"
  },
  "limits": {
    "prepare": "finite values sufficient to prepare this source",
    "evaluate": "finite values sufficient to enter the loop"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "0"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
```

Fixture inputs and environment:

```json
{
  "entry": "source.scm",
  "argv": [],
  "stdin": "",
  "cwd": ".",
  "environment": [],
  "wrapper": null,
  "packageRef": null,
  "lockRef": null,
  "generatedBindingRefs": {
    "knowledgeState": "not-applicable",
    "values": []
  }
}
```

#### Expected result

```json
{
  "status": "unspecified",
  "reason": "Evaluation ends with a terminal resource stop and returns 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.

See [Resource model numbers](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers).

<a id="lispex.section.v2.sandbox-contract.profiles-products-engines"></a>

## 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.

<a id="lispex.rule.v2.sandbox-contract.profile-meaning"></a>

### Keep meaning when a profile admits a request

A profile applies its [admission requirements](/v2.0/en/docs/profiles/#lispex.rule.v2.profiles.admission-before-entry) and [evidence requirements](/v2.0/en/docs/profiles/#lispex.rule.v2.profiles.evidence-separation). Requests admitted by two profiles follow the [shared-meaning rule](/v2.0/en/docs/profiles/#lispex.rule.v2.profiles.shared-meaning).

**Why**

A profile adds a condition for admission. Preserving meaning lets callers compare a request across products and profiles.

<a id="lispex.claim.v2.sandbox-contract.profile-meaning"></a>

Claim: `lispex.claim.v2.sandbox-contract.profile-meaning` · interaction · coverage partial · verification not-run

- language: `lispex`
- languageVersion: `2.0`

```json
{
  "predicate": {
    "kind": "shared-profile-request",
    "admittedBy": "both-profiles",
    "request": "same-semantic-request"
  },
  "result": {
    "kind": "profile-preservation",
    "outcome": "same",
    "requestLimits": "unchanged",
    "evidenceRequirements": "may-differ"
  },
  "pendingCases": [
    "Each shipped profile requires cases for requests it shares with the base language and for its own admission conditions.",
    "Shared requests near a resource boundary must compare the resource stop under identical finite limits."
  ]
}
```

<a id="lispex.example.v2.sandbox-contract.admitted-profiles"></a>

### Compare an admitted request across 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)
      input))
)
```

File: `request.json`

```lispex
{
  "notation": "documentation-request",
  "source": "source.scm",
  "semantics": {
    "language": "Lispex 2.0",
    "standardLibrary": "one fixed library identity",
    "unicode": "one fixed Unicode semantics version",
    "resourceModel": "one fixed finite resource model"
  },
  "limits": {
    "prepare": "finite values sufficient to prepare this source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "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"
    }
  ]
}
```

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 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.

<a id="lispex.section.v2.sandbox-contract.related"></a>

## Related chapters

[Procedures](/v2.0/en/docs/language/procedures)

[Resources](/v2.0/en/docs/language/resources)

[Profiles and value interchange](/v2.0/en/docs/profiles)

[Embedding and packages](/v2.0/en/docs/tools/embedding)

[First rule](/v2.0/en/docs/tour/first-rule)

<a id="lispex.pending.v2.resources.model-numbers"></a>

### 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.

<a id="lispex.pending.v2.standard-library.kernel-and-cost-model"></a>

### 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

[Procedures](/v2.0/en/docs/language/procedures)

[Resources](/v2.0/en/docs/language/resources)

[Profiles and value interchange](/v2.0/en/docs/profiles)

[Embedding and packages](/v2.0/en/docs/tools/embedding)

[First rule](/v2.0/en/docs/tour/first-rule)