Evaluate an Untrusted Rule

This page describes v1.13. Verify whether it is the current manual at /version.json

Choose the bounded product

Ordinary lispex rule.lspx remains the full-profile tree interpreter. Use lispex embed when the rule must run inside the smaller lispex/r7rs-rule-embedded-core/1 profile under deterministic work and logical-allocation limits.

The Native executable contains one exact import-free Wasm evaluator. You cannot supply a path, discover a replacement, download an engine, or request fallback.

The Downloads page also exposes the exact lispex-embed-evaluator.wasm, its component manifest, golden vectors, and SHA-256 sidecars for applications that consume the provider bytes directly.

1. Prepare the rule

Create prepare-limits.json:

{
  "raw_source_bytes": 4096,
  "prepare_work": 1000000,
  "logical_allocation": 1000000,
  "syntax_depth": 64
}

Then prepare the source:

lispex embed prepare \
  --source policy.lspx \
  --limits prepare-limits.json \
  --out policy.lpxembed

Preparation admits UTF-8, reads and normalizes the program, builds and verifies canonical bytecode, and checks the restricted profile. It records submitted source, canonical source, semantic rule, feature-set, bytecode, evaluator, and exact-limit identities. It does not evaluate the rule.

2. Evaluate the prepared rule

The input is one canonical lispex.embed-value/v1 value. Create evaluation-limits.json:

{
  "canonical_input_bytes": 4096,
  "eval_work": 1000000,
  "logical_allocation": 1000000,
  "semantic_frames": 1000,
  "traversal_depth": 256,
  "output_bytes": 1000000,
  "diagnostic_bytes": 1000000,
  "transcript_bytes": 1000000,
  "transcript_events": 100,
  "result_bytes": 1000000
}

Evaluate exactly that prepared artifact:

lispex embed evaluate \
  --prepared policy.lpxembed \
  --input input.lpxvalue \
  --limits evaluation-limits.json \
  --out result.lpxembed

Preparation usage never enters evaluation usage. Reusing a prepared artifact therefore cannot change the evaluation tariff or portable core.

3. Inspect and verify

lispex embed inspect --artifact result.lpxembed
lispex embed verify --artifact result.lpxembed

inspect gives a stable JSON projection. verify recomputes the envelope, exact hashes, category, limits, and portable core without running the rule. Neither command authenticates an issuer or grants Vouch authority.

Read the category first

Consumed work is useful local diagnostics, but it is not inside the portable core. The core binds the exact limits, profile, model, source, input, request, evaluator artifact, transcript, and result identities instead.

Boundaries

The first product uses one engine, not in-process agreement. Release-level differential courts qualify its bytes. The restricted profile is smaller than the full lispex-profile-1.5; unsupported forms and primitives are refused instead of being delegated elsewhere.

Native and the standalone evaluator bundle provide this surface. npm, the public browser WASM facade, the Playground, and browser embedding do not. Timing, cache, and microarchitectural side channels are outside the technical guarantee. Host-process survival is an operational goal of the first in-process release, not a security guarantee.

The artifact and core are inspection material. They are not a Vouch signature, authenticated evidence, a gate grant, rule correctness, or permission to perform an external action.

Keep going

Read the exact IDs, axes, categories, and bundle contract in Bounded Evaluator Contract.