exact/semantics

Contract semantics

A formal semantics of the Contract language in Lean 4. The Rust runner is tested against it, differentially and at random.

Contract/Syntax.lean	The abstract syntax: a deep embedding of the expanded root component (every used component's declarations lifted into it), the file's shapes and fns. A statement may call an action (Stmt.call, LLP 1089 D9): by name, with its whole argument list, never the body the Rust compiler expanded.
Contract/Binary64.lean	Numbers: IEEE-754 binary64 as its bits (F64), every operation the exact result rounded once to nearest, ties to even, over Nat/Int — computable in the kernel.
Contract/Trig.lean	sin and cos: libm 0.2.16's kernels and argument reduction, including large arguments, over the exact F64 operations. No hardware floats or external oracle.
Contract/Binary64Facts.lean	That model proved: correct rounding, overflow, monotonicity, exactness (below).
Contract/Number.lean	max/min as JavaScript's Math.max/Math.min (NaN and signed zero included), and JavaScript's Number#toString over exact rationals.
Contract/Value.lean	Values, structural equality as the runner's compare::equal, and the roster's string functions.
Contract/Format.lean	The roster's formats (formatTime, formatDate, formatDay, formatNumber) and t(...)'s strings tables, as the runner computes them.
Contract/Route.lean	The router (LLP 1038): canonical locations, the route table's matching, path, launch, the six verbs and the reads.
Contract/Sort.lean	sortBy's order (LLP 1116.016 §5): a key per item (a number with NaN as +0, or a string's UTF-16 code units), core's List.mergeSort on the items decorated with their keys, ascending or descending.
Contract/SortFacts.lean	That order proved: a strict total order on keys, and the sort's answer a permutation, sorted by key, stable (below). Kept apart from Sort.lean, which the VM model imports and the extracted VM builds at another Lean.
Contract/Eval.lean	Operational semantics of expressions: the interpreter eval.
Contract/Tabs.lean	Navigation tab eligibility and selection, shared by the flat and component interpreters.
Contract/Runtime.lean	Operational semantics of programs: statements, actions as transactions, settlement of derives and resources, rendering with keyed rows, timers (gated by when and key=), queued sends, events.
Contract/Big.lean	The same semantics as inductive big-step relations, with proofs that the interpreter is sound and complete for them and that they are deterministic.
Contract/Axiomatic.lean	An axiomatic semantics: a Hoare logic for action bodies, proved sound against the operational semantics, plus the transaction laws (a refused action changes nothing, reads see the pre-state, the last write wins).
Contract/Invariant.lean	Invariants of runs: the configurations a program reaches from boot by any events (Reachable), and the rules that prove a property of all of them (Reachable.invariant, Reachable.slotIn).
Contract/Observe.lean	The canonical observation a differential run compares, and how an observed event is delivered (dispatchAt: the work due first, as every host's dispatch_at).
Contract/Vm.lean	A model of the expression VM (runner/src/vm.rs) for the opcodes expressions and action bodies use, over instructions with symbolic operands, and a decoder from the plan's bytes (plan/tables/format.json, opcodes).
Contract/Lower.lean	A compiler from the semantics' expressions and statements to VM code, mirroring contract/lower (expr.rs, stmts.rs) instruction for instruction.
Contract/VmFacts.lean, Lower{Types,Sim,Spec,Proof,Lists,Calls,Correct,Stmt}.lean	Its correctness proof (below).
Contract/VmRows.lean	Executable derive calls over the VM: fresh callee machines, owner-frame and owned-slot selection, shared call and callback-work counters, and caller restoration.
Contract/LowerCheck.lean	The Lean half of difftest lowering.
vm-extract/	The shipped VM machine (runner/src/machine.rs) extracted to Lean by Charon and Aeneas, and proved to refine Contract/Vm.lean step by step and run by run (vm-extract/README.md).
Contract/ValTy.lean	Types as sets of values (ValTy, conforms without finiteness), the order and join the checker's ? induces (Ty.le, Ty.unify), and that conforms at a complete type gives ValTy.
Contract/Types.lean	The type system: typing judgments for expressions, statements, views and programs (HasTy, StmtsTy, NodesTy, WellTyped), mirroring the Rust checker (contract/types).
Contract/TypeCheck.lean	The checker as a program (check), proved sound for the judgments.
Contract/Soundness.lean	Type soundness of expressions and statements against eval and exec.
Contract/TypeInvariant.lean	The slot invariant over every reachable configuration.
Contract/EnvSound.lean, SettleSound.lean, RenderSound.lean	Well-typed environments give EnvOK; settlement and rendering preserve typing and fail only legitimately.
Contract/StepSound.lean	Well-typed programs don't go wrong: every reachable configuration is well typed and every step from it is safe.
Contract/Components.lean	The unexpanded file: every component with its props, injects, provide section, slot, states, derives and actions, and a view whose uses are still uses.
Contract/CompSem.lean	The component-level semantics: the unexpanded file's meaning, instance by instance, without expanding it.
Contract/Expand.lean	The component expander, transcribing contract_syntax::inline (inline.rs, subst.rs, derives.rs, tail.rs).
Contract/ExpandCheck.lean	The Lean half of difftest expansion.
Contract/CompSemFacts.lean, ExpandSubst{,Rev}.lean, ExpandFrame.lean, ExpandInstance.lean, ExpandMap.lean	The expansion's correctness proofs (below).
Contract/EnvSound.lean, SettleSound.lean, SettleComplete.lean, RenderSound.lean	Well-typed environments give EnvOK; settlement and rendering preserve typing and fail only legitimately; a settlement that succeeds has settled everything.
Contract/StepSound.lean, BootSound.lean	Well-typed programs don't go wrong: boot and every step from a reachable configuration are safe, and every reachable configuration is well typed.
difftest/	The differential tester (Rust crate contract-difftest).
corpus/	Scripted programs: test blocks whose steps both sides run.
Apps/	Real apps' embeddings (generated, checked current by difftest apps) and, under Apps/Proofs/, invariants proved of them.

The pieces

Codegen. contract lean <file.contract> [--name <ident>] [-o <file.lean>] (contract/cli/src/lean.rs) emits any program the compiler accepts as a Contract.Program term. It runs after the whole compiler (a program the plan backend refuses is refused here too) and embeds the expanded root with the checker's types. Names stay names: the semantics does its own scoping. Its shapes are the ones the program reaches: those its types and records name, those of the roster entries it calls, the router's four when it has routes, and what their fields name — not every shape the checker knows, so a compiler shape the program never reaches (an event's) does not make an app embedding stale when it is added.

The embedding shares the plan lowerer's delete= expansion: an admitted list row includes its generated Delete button and suffixed testId, with disabled belonging to that button. Admission reads grouped-row layout before descending and keeps enum prop ascriptions as the plan does. Emission omits literal ascriptions that add no Lean type information; enums emit as strings. The plain embedding used to compare component expansion keeps the view before this lowering step.

Differential testing. For each case, difftest compiles the program to a plan and boots it on the runner, delivers the script's events, and prints a canonical observation after every step: the outcome, the commits attempted, every root slot, derive and resource, the commands issued to a host (hostCommands leaves out setMode and the seven-argument list-row form of scrollIntoView, which the runner consumes itself; the element form stays), and the text of every element with a testId. Then it emits the program with the Lean backend, and runs many cases in one generated Lean module whose main prints Contract.Observe.run for each. The two texts must match line for line. Data sources are a seeded oracle that answers any call with a value of the declared shape. The runner's transcript of that oracle becomes the Lean side's oracle, so if the semantics makes a call the runner didn't, that is a divergence. What the runner answers itself never reaches the oracle: its own sources (exactViewport, exactPage, …) and a native module's (LLP 1133.002 D13), which it answers from the module's substitute. Each such resource that answered at boot holds that answer as a host fact (fact in the oracle's text), and each module's source is named (module). Neither does a source the program declares (LLP 1162.001), whose HTTP request the runner makes itself: each is named (fetch), and a call to one is outside the semantics. A live time's text (LLP 1126 D6) is the runner's presentation too, and the observation leaves it out.

The observation starts with == <step> and outcome ok|refused|poisoned. Before the configuration, each attempted commit prints ran <kind> <action> <ok|refused|poisoned>, in execution order. The kind is handler, task, then, or queue; a queue names its mutation. A failed outcome or commit is followed by # <reason>. Reasons are the runner's Debug text and Lean's why, and are not compared; ran lines are compared. Boot and an event with no handler have no ran line. Curried arguments that refuse print ran handler <action> refused and a # reason saying the arguments refused. A due refusal and a successful handler print separate commit outcomes even when the step's outcome is refused.

Observe.runScript runs advance and dispatch beside their traced variants. The original supplies the configuration and outcome; the variant supplies only ran lines. A difference in either result replaces the configuration with trace disagrees, which always fails comparison. The guard compares derived structural representations of the entire configuration and outcome, including hidden scheduling state and the bits of every number. Projection equality is not proved. The new land has no earlier function to compare. ScriptEvent extends the harness vocabulary; the original Observe.Event, step and every existing theorem stay unchanged.

The runner also commits transport or MIDI answers, re-asks, wake deliveries and expiry, drop deadlines, transport ends, and the advance tail's presence, polls, live times and text-axis frames. These have no corresponding semantics branch. They print no ran line. For each step, observe.rs compares successful commit receipts with successful ran lines. Extra receipts mark it with # a commit the semantics has no branch for; the census prints steps with a commit the trace leaves out. Property checks must exclude marked steps from after. The work before the advance loop (module deadlines, listed due work and presence) has no receipt; tracing compares the configuration before and after it. A move prints untraced configuration moved as well as the marker, so comparison fails even if later work restores the old value. A step that moves without any successful ran line gets the same diagnostic. An extra receipt alone is counted; a differing configuration is a divergence named with the marker.

land drains armed thens and queued sends at the current clock, without firing a timer, even one due exactly now. It is Runner::land_then on the runner and Observe.land in Lean. An authored clock data emits it; an authored tap or type, and each explore tap, emits its input followed by land. Expectations read the observation after that pair and its automatic clock advances. after "a" reads the landing with old from before the input and commands from both steps. A refused input, another commit beside its handler, or an untraced commit makes the pair counted only. Its landing is not an after clock step. A timer due exactly now stands after land and fires at the next dispatch; that dispatch is counted only for after when it also runs a handler. A primitive clock +0 still fires due timers as well as continuations.

The device runner (scripts/agent-test.mjs, testMutationClock) advances one millisecond per mutation request, reading the runner's cumulative counter after each delivered operation and again after each advance, at most sixteen rounds. Delivery uses these device advances so a task armed for one millisecond by a mutation runs before the next authored expectation. An input lands before this clock runs, as it does on a device. Explore and walks use the same rule. Every advance is recorded as clock +N in the expansion's .events file and replayed on both evaluators; the matcher checks it as after clock. An expectation issues no requests, but still reads the counter. The receipt counts advances and bounds. Requests still issuing after sixteen advances stop the block or walk, as on the device; this differs from a settle bound, which lets the next step run. The shrinker keeps an input, its landing and these advances together; when a candidate's input reaches no handler, its landing and advances are removed. The harness retains their origin internally, so an authored clock data after the missing input is kept. Both kinds of landing still print land.

A typed value reaches an input handler when the target has one, otherwise its change handler. Both evaluators choose that event before advancing due work; the script label remains type. Oracle string enums draw from their declared members, including enum fields nested in resource answers.

An authored clock settle expands on a live runner: clock +0, then at most sixteen repetitions of clock +N to the latest task with now < due <= now + 1, where N is due - now, followed by another clock +0. Every task qualifies, including repeating tasks and tasks armed by earlier inputs or continuations. The expansion replaces the settle in the case and its expectation positions; Lean and JS replay those same events. A .events file under target/difftest/expansions/ keeps it, and the block reports settle expanded to k events once, totaling all its settles. A task still due within a millisecond after sixteen rounds increments the bound count; the next authored step still runs. The host's waits on motion, scrolling and hatches, its seek to a re-ask's due time (the oracle schedules no re-ask), and its advance to an animation's end have no image here; verify prints that limit on its world line. The census computes undeliverable kinds from the parser's step enum minus the delivered kinds and prints the supported forms of input and clock steps.

clock until state <path> == <literal> within <ms> emits one land, then reads the observation with the same matcher as expect state. A match lets the block continue. A miss stops it as clock until (not met), naming the path, observed value and literal. This is a stop of the world's: the oracle has already answered, no later answer is pending, and the wait never advances time to fire a timer. It is neither an app failure nor a property violation. Both evaluators replay the landing; a disagreement still fails verification. The .events file records its clock until origin and bound in a comment. The bound has no effect in this world. The usual mutation clock runs after a met step.

State expectations and waits resolve record fields and zero-based list indices through the compiled plan's shapes on either evaluator's observation. Paths such as session.phase and rows.0.name read the same positional values. Present options unwrap during traversal and at the resolved leaf. An existing none can match none; a missing root, field or index, or a path through none or a scalar, has no value and cannot match even none. Traversal and value scanning are bounded by the runner's value-depth limit. A wait on a missing path lands once, then stops as not met. The receipt counts met waits and not-met stops separately. A leading size WxH is consumed as a launch fact with no event: the harness has no layout. The test parser refuses a size after an input; a resize still stops the block.

An event is delivered as every host delivers one, at the current time: the work already due (a timer, a mutation's then, a queue's next send) fires first, then the event, which runs even when that work refused (Observe.dispatchAt, CompSem.cdispatchAt; the runner's dispatch_at; the web build's on()). The outcome is the event's when it failed, else the due work's. An event the target has no handler for reaches nothing and fires nothing, as a host attaches a listener only where one is declared. Such a step is at most two of Reachable's, an advance then a dispatch, so observe_step_sound (BootSound.lean) carries dont_go_wrong to it. The semantics names the target by its testId after the advance, where the runner keeps the view it picked before it: a due commit that renames the target's testId, or replaces it with another element of the same testId, is outside what an observed step models (the hosts differ there too: the web build's on() runs the listener it already holds).

cargo run -p contract-difftest -- corpus                    # every test block in corpus/
cargo run -p contract-difftest -- random --seed 7 --count 500
cargo run -p contract-difftest -- apps                      # app embeddings are current
cargo run -p contract-difftest -- types --seed 1 --count 200
cargo run --release -p contract-difftest -- arith --count 1000000

arith checks the number model against this machine's f64: for each operand pair (random bits; edge values and their neighbours; pairs that cancel or sit a few exponents apart; integers around 2^53; operands near overflow and underflow) and natural number, + - * / %, floor, max, min, trunc, negation, a natural number as a double, ceil, round (JavaScript's Math.round), sin, cos, sum([a, b, -a]), and < <= ==, as the runner computes them, compared by bits (every NaN one); and, for a numeral and two dates each case carries, parseNumber and calendarDiff in years and months (LLP 1102 §3.1, §3.4), the runner's stdlib against Contract.Value's; and, at a random digit count each, toFixed and formatDecimal (§3.2), the format capability against Contract.Format's. The trigonometric reference is exact_motion::math, the runner's pinned libm 0.2.16. Every run starts with both signs and the neighbours of zero, subnormals, tiny-input cutoffs, multiples of pi/2, argument-reduction cutoffs, large arguments through 1e300, the largest finite value, infinity and NaN. Random cases also sample pi/2 neighbourhoods. This checks the port's bits; it is not a proof that the port refines libm. JavaScript's Math.sin and Math.cos may differ in the last bits.

sum folds binary64 addition left to right from +0; an empty list returns +0. As with includes, the semantics omits the runner's list-budget limit (one list step per item), so a program exceeding that limit remains outside the comparison's resource-bound model. flat joins a list of lists one level, and range(n) lists 0 to n - 1: a count that is not a whole number at least 0 is a refusal, as the runner and the web runtime trap one, and a count past 65,536 is unsupported, outside the semantics, so no such list is built here.

sortBy(xs, x => key, direction) (LLP 1116.016 §5) is map's callback over the items, each key once, then Contract.sortByKeys: core's List.mergeSort on (item, key) pairs, numbers by F64.key with NaN read as +0, strings by Str.unitsLt, equal keys kept in input order in both directions. The runner and the JS target run a written-out bottom-up merge sort instead; SortFacts proves what makes every stable sort by this order give one answer:

• sortByKeys_spec: when sortByKeys xs ks desc = .ok v, the keys are ks.mapM sortKey = some keys with xs.length = keys.length, and v = .list (ps.map Prod.fst) for a list ps of (item, key) pairs with ps.Perm (xs.zip keys) (a permutation), ps.Pairwise (sortLe desc · ·) (sorted: no later key below an earlier one ascending, above it descending), and every sublist of xs.zip keys whose keys are all equal a sublist of ps (stable).
• sortByKeys_perm: sortByKeys xs ks desc = .ok (.list ys) → ys.Perm xs.
• sortByKeys_ok: keys of one kind (OneKind: all numbers or all strings), one per item, always sort; with type soundness (sortByKeys_good in Soundness), a well-typed sortBy never fails.

Like map, the semantics omits the runner's list budget (one step an item, taken by the Map that computes the keys; the comparisons take none).

numbers does the same for number printing.

types runs the Lean checker (Contract.check) against the Rust one: every corpus program and count generated ones, all accepted by the compiler, must be accepted; each also yields a mutant (a literal of another type, a field the shape lacks, an argument dropped, added or retyped, == across types, a condition that is not a bool), judged by the Rust checker, which the Lean checker must judge the same. A mutant the compiler refuses cannot pass contract lean, so its expansion is emitted with the types of the program it came from (contract::lean::emit_checked). Mutants touch only what the semantics evaluates (a view's presentation attributes are left alone) and what its checker judges (a host command's literal argument is not retyped: the command's signature is the Rust checker's). The embedding carries what the Rust checker judges at a use and at a source: every typed prop's and inject's argument is ascribed its declared type (.typed, from contract_syntax::expand_typed), and the program carries each data source's one signature (Program.sources), which every resource and send must meet. A disagreement is kept under target/difftest/types/.

A divergence is kept under target/difftest/failures/ (the program, the events, both observations); random failures have their scripts shrunk first. The async lane (scripts/async.mjs) runs this as four checks: lean builds the Lean project and checks the proofs (the app proofs among them); vm-extract checks the extracted VM (vm-extract/README.md); difftest checks the app embeddings are current and runs the corpus, the explored programs, a random sweep with fixed seeds, the lowering, number, type and expansion checks; difftest-js runs the web JS target (below). Each is skipped when its inputs are those of a run that passed: the binaries it runs, the Lean sources, every program and what compiling it reads, the tools and the environment (scripts/async-inputs.mjs). difftest runs with DIFFTEST_CACHE=1.

Using it day to day

None of this is a blocking check. Nothing needs Lean except these commands, and they say how to install it when it is missing (below, "Lean"). The first run builds the library (minutes, once per worktree); after that, Lean's observation of a case is kept under target/difftest/cache/, keyed by the case's embedding, oracle and events and by the semantics' sources and the harness that runs them (leanrun.rs), so a rerun only takes Lean time for what changed. Only verify and quick use the cache unless DIFFTEST_CACHE=1, which the async lane sets.

Writing an app. contract verify apps/<app>/app.contract runs the app's delivered test prefixes and explore script, plus 20 adaptive walks of at most 40 chosen primitive events each, plus automatic clock advances. --walks, --steps and --walk-seed set the search; the seed defaults to the app's path. Half the walks boot fresh; the others replay delivered test prefixes in turn before appending events. Each choice reads the live rendered controls. Inputs land before the next choice. Typed values come from that field's authored tests, then source literals, then the generator. Every script also runs from a seeded store when the app persists state, with the same oracle answers as its empty-store run.

State properties beside the test blocks in app.test.contract:

always "the phone is on one of its five screens"
  expect state screen in "lock" "home" "settings" "display" "messages"

after "increment" "increment adds one"
  expect state counter == old + 1

never refuses "reset"

Use blocks that name your app's states and actions; the properties recipe explains the literal forms and receipt. bun exact.mjs verify checks always on the device at boot, after inputs, reloads and every test-clock advance, then always runs contract verify. Either failure fails the command. Keep its receipt unchanged in the diary: the digests identify the sources, and the counts identify the scripts and world checked. “In the semantics' world” means the seeded oracle answers synchronously and never fails; it does not include a device's reloads, late replies or host inputs.

contract verify --js apps/<app>/app.contract replays every search script, including stored variants, and the shrunk findings on the web JS target. It checks always on the JS observation and compares configurations with the runner. The receipt's js: entry gives agreements, outside cases, errors and property line checks; without the flag it says not run. JS and device runs count after, its frames and commands, and never refuses as unchecked because they expose no commit trace.

The runner checks properties and classifies refusals on these scripts, then shrinks each distinct property-line or refusal-class/action finding in each script. Lean confirms the delivered tests and explore script, each shrunk finding, and --confirm N walks (default 2). A divergence is shrunk with both engines. Deletion tries large chunks before individual delivery groups; each retained candidate still satisfies the original predicate. The receipt counts candidates and times both halves. --runner-only, or an unavailable lake, skips the semantics and says why. A property failure or type refusal fails verification; app refusals are findings. clock data lands continuations; clock settle expands as described beside the observation format. Leading fixed epoch and time-zone lines set the runner's launch facts, using Bun's Date and Intl APIs for the date and offset; Lean receives the resulting host facts in its oracle. epoch now and other launch settings remain undelivered. A block runs up to its first undeliverable step, with its location, kind and reason printed. Only a block that stops at its first step is SKIP. Expectations before the stop still run. The summary counts whole, partial and skipped blocks.

Properties in the app's test files (always, after, never refuses; the grammar and example are in docs/contract-grammar.md, "Authored tests") apply to every delivered script, explore script, walk and stored variant. Before delivery, the compiler checks reads against the expanded root and follows derives and functions to reject dependencies on resources, mutation status, the clock or geometry. performanceNow is the roster's clock read; date formatters read arguments, and exactTime is a resource. Mutation result slots remain admissible: their values here are oracle answers.

property.rs matches the same observation on each side. always checks printed configurations; stays also reads the previous step. after "a" checks a successful handler-only input and its following land, from before the input through the landing. Extra commits on the input, commits other than then or queue on the landing, or an omitted-commit marker make the pair counted only. after clock checks clock +N and standalone land steps over all commits. Every changed root slot counts in a frame, including a queued mutation's slot. never refuses reads commit attribution, not the aggregate outcome. A poisoned step has no configuration and is counted only. Every line reports checks, counted-only steps and violations; an action never attempted is not exercised. A false property fails verify; if it holds on only one evaluator, it is also a divergence. These are observed-step checks under the seeded oracle, not proofs or device checks.

Suggestions print D1 blocks; they never edit test files. They use all observed runner scripts, including shrink candidates and confirmation replays. The receipt's script, step and property denominators count the search scripts once; shrink work is separate. Frames require at least two eligible input/landing pairs or clock advances and include changed queue slots. Sets, whole numbers, options and stays use the same cone as authored properties. Existing predicates are compared by scope and line, ignoring names.

Before printing, contract/analyze walks the expanded program's writes and callers. A frame includes every branch, called action and send continuation; the clock includes every task, sequence end, continuation and queued send. A larger finite write set widens the frame; a call or send cycle suppresses it. A set must contain the initializer and every possible written value, including arguments supplied by every caller. Literal choices and literal-list controls are understood. Unbounded values from inputs, module-event arguments, host answers or unsupported expressions suppress the set. A latch is suppressed if any assignment can reset it. Whole-number suggestions require whole initializers and writes: literals, increments or decrements by one, lengths, rounding of finite numbers, or callers that preserve whole values. A raw clock reading does not qualify. The walk follows pure functions and derives, but does not use branch guards to establish invariants, so it can lose true suggestions. The receipt counts drops by rule, names their reasons, counts frames widened by the code and times the pass. A suggestion is observed and code-consistent, not proved; persisted-store and oracle limits still apply.

The receipt records SHA-256 of the entry source, test files concatenated in filename order, and contract::lean::lean_path(file, "app"), plus the exact2 commit. It ends with the world and semantics boundaries. never reached names rendered test targets' actions that no walk attempted; declared actions and committed actions use the full plan. The receipt is the last output, so its command and seed can be kept with the app diary.

Corpus properties live in <program>.test.contract beside the program. The corpus loads these sidecars as tests rather than programs; a sidecar without scripts uses the explore script. A program may declare the test-only comment // # expect property false "name": corpus and quick require that named property to be falsified on both observations, and still compare the observations normally. // # expect property refused "reason fragment" requires the cone check to refuse before a script runs. These comments never exempt an app from verify. Unexpected violations, missing expected violations and missing expected refusals fail the corpus.

The refusal census classifies every failed outcome and commit line as world, limit, poisoned, cycle, value, app, type, or unclassified. Those counts include both the aggregate outcome and its commit line; findings use the refusing commit's line, without attributing due work to the event. A boot or curried-expression refusal has no commit line. At slot initializers and writes, derives and ordinary action arguments, a value that fails typed is class type and fails verification; one that is typed but fails conforms is non-finite, class value. Hidden @ parameters use typed alone. VM Trap::Arity is type; host-payload RunnerError::Arity is world. Coverage names actions committed and never run, clock actions fired against the declared tasks, steps with multiple commits, and poisoned steps.

A divergence names the step where the two first differ and the line of the test that step comes from, where the element it tapped is declared, and the slot, derive or element whose line differs:

DIVERGE apps/counter/app.contract: increments
  at step 2: tap "add" (apps/counter/app.contract:22:3)
  the element "add" is apps/counter/app.contract:17:7
  count is declared at apps/counter/app.contract:3:3
  runner: slot count 7
  lean:   slot count 8

OUTSIDE means the semantics doesn't model a construct the app uses ("What the semantics leaves out"), not that something is wrong. NOTE means a test's expect fails against the seeded oracle's data instead of the app's own, which is information and not a failure. --types also runs the Lean checker on the program. --prove <Module> regenerates Apps/<Module>.lean and builds Apps/Proofs/<Module>.lean (the next section). contract verify runs cargo run -p contract-difftest -- verify in the checkout it was built from. Warm on a small app it takes a few seconds.

An unsupported first difference remains OUTSIDE when an oracle reply is missing later in the script: the unsupported input can leave the two evaluators in different states. A missing reply before that boundary still diverges. The trace-twin and omitted-commit checks are unchanged.

Changing the compiler, runner or semantics. Before landing a change under contract/, runner/, plan/ or semantics/, run cargo run -p contract-difftest -- quick. From the files changed since the merge base with origin/main (--base <rev> picks another base), it runs the corpus directories the changed files' names point at, or the whole corpus when the names point at no area. It also runs 40 random programs and the lowering check on 8, seeded by the base, so a branch's reruns are warm. Warm, it takes about 10 s. Cold, with the semantics changed so Lean reruns everything, it takes one to three minutes depending on load. It prints a command that reproduces each divergence. The async lane's difftest check is still the full run.

The web JS target

The web build's JS target (host/web-js, LLP 1071) is a second implementation of Contract: the plan compiled ahead to one ES module over a small runtime. --js on corpus, explore and random checks every case a third way, against the runner (difftest/src/js.rs); --js-only skips the semantics (no Lean needed). The JS module exposes no commit trace, so js.rs strips ran lines from both observations before comparing them; this checks the step's outcome and configuration, without commit attribution.

cargo run -p contract-difftest -- corpus --js
cargo run -p contract-difftest -- explore contract/corpus apps/*/app.contract --js-only
cargo run -p contract-difftest -- random --seed 7 --count 2000 --js-only
cargo run -p contract-difftest -- verify --js apps/typetour/app.contract

These commands build exact-web-js locally with cargo build -p exact-web-js. The driver needs the repository's pinned Bun and installed dependencies; it downloads nothing. A build or driver failure fails verification and is named in the receipt.

difftest/js/drive.mjs is the headless driver. Each case's program is compiled by exact-web-js (the build's compiler), bundled with the runtime and run under Bun in a fresh VM context over the render DOM (host/web-js/dom.js) given event listeners, the clock the driver's (advance, as under the agent). It boots with the agent URL, so navigation tabs use the live runtime's deferred construction. It omits virtualized descendants by the collection attached to the element, including a list whose role is tabpanel. Its sources answer synchronously from the runner's oracle transcript, as the runner's do; resources whose boot answers bypassed the oracle become host facts (except transport and MIDI, which remain outside the model). Their sources answer what the runner answered at boot. A call the runner never made is noted (# js: the oracle has no answer…) and shows as the refusal it causes. It prints Contract.Observe's format from the module's own state (names.js) and the DOM: a testId's text is a text's, an inline run's, an option's or an SVG text's, as agent.js reads them. A tap goes to the element's press listener. A type prefers its input listener, falling back to change. An element without the listener is refused, as the runner refuses (NoHandler), and so is a value a browser could not deliver (a select's unknown or disabled option, a checkbox's text, a date outside HTML's format or its bounds). A press on a disabled control is outside the JS comparison: the runner's direct dispatch delivers it, while the browser's event handler declines it.

The JS target's sin and cos are the browser's Math.sin and Math.cos, held to the runner's pinned libm by value, not by bits (LLP 1003 §7); the semantics is held to the runner's bits. The driver replaces the two (roster.js's x_sin, x_cos) with the runner's bits for each input: an input it has no answer for is answered by Math and reported, the harness computes it with exact_motion::math, and the case is driven again until it asks for none, so a chain of trig results is answered link by link. Only a drive that asked for nothing is scored; a case still asking after 32 drives is a driver error (ERROR-JS). Every other number is compared by its bits, so the comparison stays exact; Math.sin and Math.cos themselves are not what it checks.

A program exact-web-js refuses is outside the JS target (OUTSIDE-JS), not a failure. A divergence prints DIVERGE-JS with whether the semantics agreed with the runner, and is kept under target/difftest/failures/ (*-js-*.{contract,events,rust.txt,js.txt}); random ones are shrunk first. The async lane's difftest-js check runs the corpus and the explored programs, and a random sweep of 500, with --js-only.

Verifying an app

An app is verified against its embedding, so the proofs are about the source as it is.

1. Generate. Add the app to APPS in difftest/src/main.rs and run cargo run -p contract-difftest -- apps --write: it writes Apps/<Module>.lean, def <name> : Contract.Program. Check that the semantics agrees with the runner on it (cargo run --release -p contract-difftest -- explore apps/<app>/app.contract) and that it is not refused (geometry reads are outside the semantics, below). From then on difftest apps, in the async lane, fails when the source moves and the embedding did not. After editing an app or its imports, regenerate the embeddings and run lake build Apps in semantics/ to recheck their proofs.
2. State. Write the property in Apps/Proofs/<Module>.lean over the embedding: of every reachable configuration (Reachable <name> c), of every event from any configuration (Event.step), or of one committed action (runAction … = (c', out) with out not a refusal). Slots are read with lookup; SlotIn x V slots says slot x has property V.
3. Prove. A reachability invariant of one slot is Reachable.slotIn: the values the slot starts with (SlotOrigin: unfold the program's states), and for every action a handler of the view, a task or a mutation's then names, the body keeps it (BodyKeeps). Queue mutation slots use the same rule: Reachable.slotInvariant also carries the waiting sends' answer property (QueuedIn) through drains. Queued sends describes the corresponding event and advance rules. An action body is unfolded by wp (BodyKeeps.of_wp); simp with the EvalR rules (EvalR.str_iff, EvalR.var_local, …) turns it into a statement about values. A body that never touches the slot is dismissed by decide (Stmt.noAssigns, BodyKeeps.untouched); a body that calls an action is not, since Stmt.noAssigns and Stmt.noSends answer false for a call rather than look into its callee. A fact about one action is runAction_commit (the body's ExecR outcome, the slots after it) plus wp_sound and applyWrites_last. Numbers are F64s whose arithmetic is defined over Nat and Int, so a numeric fact is proved from Contract.Binary64Facts (F64.add_ofNat: integer + is exact up to 2^53; F64.ofNat_le_ofNat; …) or computed by decide +kernel for given operands. native_decide is not used (it adds an axiom).

Type Tour declares routes for its six screens. Its generated embedding also contains the not-found route. The proof checks the names and the parent chains used by direct Display and conversation links:

def screens : List String := ["lock", "home", "messages", "thread", "settings", "display", "notfound"]

theorem route_names : ∀ r ∈ typeTour.routes, r.name ∈ screens := by decide

theorem display_parents :
    (Route.chain typeTour.routes "/settings/display").map (·.name) =
      ["lock", "home", "settings", "display"] := by decide +kernel

The proofs are in Apps/Proofs/TypeTour.lean. What is proved, by app:

App	Theorem	Says
Type Tour	TypeTour.route_names	Every declared route names one of the seven screens, including not-found.
Type Tour	TypeTour.display_parents, TypeTour.thread_parents	Direct Display and conversation links include Settings and Messages respectively.
Update Lab	UpdateLab.advance_keeps_user_state	Moving the clock (the 250 ms probe) never changes counter, note or live.
Update Lab	UpdateLab.results_shape	The three result slots always hold none or some answer.
Update Lab	UpdateLab.increment_adds_one	A committed increment leaves counter at its old value plus one.
Update Lab	UpdateLab.counter_always	counter is always exactly one of the doubles 1, 2, …, 2^53, however many increments: past 2^53 adding one rounds back.
Update Lab	UpdateLab.counter_pos	counter ≥ 1, in IEEE order.
Photo Editor	PhotoEditor.ready_stays	Once ready is true, no event makes it otherwise.
Photo Editor	PhotoEditor.rotate_only_turns	rotate changes no slot but turns.
Photo Editor	PhotoEditor.reset_spec	A committed reset sets turns to zero and adds one to resets.
Video Player	VideoPlayer.paused_bool	paused is always a bool.
Video Player	VideoPlayer.toggle_flips	A committed toggle negates paused.
Video Player	VideoPlayer.done_focuses	A committed done writes nothing and issues focus("done").

The lowering

The VM model. Contract.Vm steps as the runner's loop does: at a Map/Filter body's end it collects what the run left and starts the next item or pushes the list, else it runs the instruction at pc; every trap is an error. Operands stay symbolic (slot, derive, resource and mutation indices; a string is the pool's string; a Record is its shape's name and field count; a Call is the roster entry's name and arity), and a jump is a forward instruction offset: the decoder checks what Plan::check_code checks of what the model reads (framing, pool operands, forward and aligned jumps, a final Return) and refuses the rest. A Call means Contract.stdlib over the program's route table (the router verbs and reads).

The compiler. Contract.Lower.compile resolves names through a scope as contract/lower does through Scope and emits its instruction choices: and/or through BindLocal/LoadLocal/JumpIfFalse/DropLocal, match through JumpIfNone/Unwrap/BindLocal, templates through toString and Concat (one Str when every part is literal), records with a base bound as a local, a fn expanded inline with its arguments as locals, map/filter with the callback inline after the opcode, sortBy as the list bound as a local, a Map of its key and a Call sortBy, blocks whose lets are dropped where the block ends, and a call of an action as the Rust compiler expands it (LLP 1089 D8): each argument bound as the next local, the callee's body in a scope of those locals and the component's names alone, every local dropped at its end, no call opcode. It carries static types of its own (STy), proved sound, and refuses where it cannot know (+ of an operand not known to be a number or a string, a member of one not known to be a record, such as a router read) or where the semantics differs (path(…), which the Rust compiler expands into a template and the semantics evaluates by name).

The theorems (Contract.LowerStmt). In a machine state that corresponds to the semantics' environment (Ctx: every name the scope resolves reads, on the VM, what eval reads for it, of its static type; nothing in flight; the same clock and route table) — compileBody_correct: the compiled code of a derive, slot initializer or resource argument returns v exactly when eval answers v, and returns at all exactly when eval has a value; compileAction_correct: with writes admitting the body's writes (Writes), and the component's names agreeing with no locals bound (GlobalsAgree, which a callee's fresh scope needs), an action's code returns exactly the effects exec records, calls included, names resolved as the plan did (lowerFx), and returns at all exactly when exec has an outcome. Both rest on allOk/blockOk, one induction on the compiler's fuel proving, for every construct, that its code takes the VM from the state before it to eval's value on top (forward), and that a run through it that returns had a value (backward); map/filter by induction on the items through the VM's callback loop, and sortBy (case_sortBy) by that loop over the bound list, then the call.

Translation validation. difftest lowering checks the real pipeline: for each generated program it takes the plan contract::compile made, and in one Lean process per batch decodes every derive, root slot initializer, resource argument and action body, runs it on the VM model in every configuration the semantics reaches along the script, including after landings of mutation continuations and queued sends (actions with sample arguments, inside a row instance), and compares the result with eval's (or exec's effects); and compares the body with Contract.Lower's, instruction for instruction. A divergence or an undecodable body fails the run and keeps the program under target/difftest/failures/; a structural difference or a body Contract.Lower refuses is reported by category.

cargo run -p contract-difftest -- lowering --seed 7 --count 500
cargo run -p contract-difftest -- lowering-corpus             # semantics/corpus

Component expansion

Everything above is about the expanded root: contract lean embeds what contract_syntax::inline::expand makes of the file. This part stops trusting that expansion preserves meaning.

The unexpanded file. contract lean --components <file> emits the file before expansion as a Contract.Components.CProgram: every component with its props (declared type, whether action), injects, provide section, slot, states, derives, resources and actions (each with the checker's types: the root's from the expanded root, a child's from the checker's standalone pass), and a view whose Use and children nodes are still there, each region, use and children node numbered within its component.

Its meaning (Contract.CompSem) is given directly, not by expanding. A use is an instance, identified by its path from the root: every use, region arm (if/match arm, for row by key and duplicate count) and children node on the way. Its states live in a store under that path, initialized in the instance's frame the first time it renders, kept while it renders, dropped when a render leaves it out. Names are read in a frame: the root's reads the root's declarations as Contract.Eval does; an instance's reads its derives (the body, at every read), its states (the store), its injects and props, each a thunk (the expression the use or the provider wrote, with the frame and locals where it was written, evaluated at each read). A fill renders where children stands, in the use site's frame, locals, providers and fill; a provide covers the providing component's view. A handler names an action or an action prop, resolved through the props to the action it names with the curried arguments; its arguments are evaluated at dispatch. A child's action writes its instance's states; an action prop called last (LLP 1017 §11) runs the named action's statements in its own frame in the same commit. The root's own slots, settlement, actions and timers are Contract.Runtime's (rootProgram). Each child's exactViewport() and exactPage() resources live in that root environment under name@Component, shared by all its instances. Reads, status queries and refreshes in the child's frame resolve to those resources.

The expander (Contract.Expand) transcribes inline.rs and its submodules step for step, numbering and spelling included: capture-avoiding substitution renaming a binder x@k when a replacement mentions it, view binders x#viewN (0 for the root), derive resolution (freshened binders x@bk, a dependency read twice on every path bound once by a let), lifted states and actions x#n with their owners, a slot's fill inlined afresh at each children node under that node's region arms, props and injects captured as hidden parameters @capture:n:i, tail calls resolved (p@ck, x@bk, p@tailk; the @check: statement the flat embedding drops is not emitted). Device resources are hoisted once per declaration, including unused components, in file order. Their value reads and refresh targets are renamed; same-named function calls keep their heads. Style names, surface names and positional syntax words stay unchanged; only a conditional class's condition and a surface's arguments are substituted.

difftest expansion checks the real expander on each program:

cargo run -p contract-difftest -- expansion                          # semantics/corpus
cargo run -p contract-difftest -- expansion contract/corpus apps/*/app.contract
cargo run -p contract-difftest -- expansion --seed 1 --count 500     # generated

(a) the Lean expander's output on the component-level embedding against Rust's expansion (the flat embedding of the expansion the plan compiler makes, contract::lean::lean_plain: its uses' arguments not ascribed as contract lean's are for the checker), declaration by declaration and node by node, types apart (a lifted type that differs is reported, not failed: a child's declarations carry the standalone checker's types; a curried argument's hidden parameter, ? in both expansions until the checker types it from its handler, need only be at least the expansion's, Ty.le); (b) the component-level semantics of the unexpanded file against the flat semantics of Rust's expansion over the case's script, the oracle the runner's transcript. It compares outcomes and configurations, omitting commit traces (ran …), which the component-level semantics does not emit, and the slots the expansion lifts out of children (slot name#n …), which it keeps per instance. A disagreement is kept under target/difftest/expansion/, its script shrunk.

What is proved (no sorry, no axioms beyond Lean's own):

• ExpandSubst.subst_iff: the expander's substitution commutes with evaluation. For an expression of the fragment (Plain: no pending/failed/failure/current, no sortBy (not yet carried through these proofs; difftest expansion checks it), callbacks of at most two parameters, no binder named like a call in its scope), a substitution whose replacements are callbacks of at most two parameters and never a callback, and no call head replaced: if every free name reads in the source environment what its replacement reads in the target (Agree), the expression has value v in the source exactly when its substitution has value v in the target. The binder cases are agree_enter: a binder is renamed exactly when a replacement mentions it, to a name the scope, the replacements and the enclosing binders do not write, so nothing is captured either way. Weakening (wk_iff: only free names' locals matter) and environment transfer for fn bodies (xferE) are proved on the way.
• CompSemFacts.ceval_mono, ceval_det: more fuel never changes the component-level evaluator's answer; a name has one value in a frame.
• ExpandFrame.frame_iff: an instance's frame is an environment. An expression of the fragment whose free names are locals or the frame's has value v in the frame (at some fuel) exactly when it has value v in frameEnv — the flat semantics over the frame's names as values.
• ExpandInstance.instance_iff: an instance's expression means what its expansion means. When the frame's names correspond to their replacements (Corr), a component-level expression has value v in the instance exactly when the expander's substitution of it has value v in the flat environment. prop_reads, state_reads and derive_reads discharge Corr name by name: a prop when its argument corresponds at the use site (the same theorem one level up, so it composes through nesting), a state when its lifted slot x#n holds the store's value, a derive when its resolved body means its body.
• ExpandMap.use_prop, use_state: the same of the expander's own substitution for a use (Expand.baseMap, withDerives, which inlineNode builds it with), for a component whose props, injects, states, actions, derives and device resources have distinct names: a prop's replacement is its argument substituted at the use site (map_prop), a state's its lifted name (map_state).

What is left. The theorem stops at expressions in an instance's frame. Not proved, and covered only by difftest expansion: that derive resolution (resolvedDerives: freshening, let placement) keeps a body's meaning; that the expander's view is the component-level view node for node (regions and their tags, fills placed at children, the instance store against lifted root and row slots); handler resolution and a child action's body (captured props as hidden parameters, writes to x#n); tail calls; provide/inject scoping in a render; and their composition into a run, where both semantics take a fixed fuel the expansion spends differently.

Findings, fixed. The first run found four disagreements, each a bug in inline.rs (the rule: a child's state lives exactly as long as its instance, owned by the innermost region arm around the instance, or the root). Each is now a case in corpus/components/ and a runner test in contract/cli/tests/it/child_state_lifetime.rs.

1. A stateful child in a slot fill, the slot component showing children under an if, kept its state across hide and show: the fill was inlined before the slot component's view, so its uses were owned by the use site's region. The fill is now inlined at children, under the arms around it (fill-state-when).
2. A slot component showing children twice shared one instance's state and region tags between the copies (the fill was inlined once and copied). Each children now inlines the fill afresh: its own instances, numbers and tags (fill-twice).
3. A slot component repeating children per for row shared one instance across the rows, for the same reason; each row now owns its copy (fill-per-row).
4. A child whose prop held a number that is not finite had all its actions refused (ArgumentType on @capture:n:i), even those that never read the prop. A hidden parameter (one whose name begins with @, which no authored name can) is the compiler's argument, not the host's, so its argument is held to its type but not to finiteness (Runtime.argOk, typed; the runner's Value::typed; the JS target's N type code), as the prop read in place is (nonfinite-prop-action).

Lean

The Lean toolchain is pinned in lean-toolchain. To install it: curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y. Build and check every proof with lake build. The library has no dependencies.

What is proven

All without sorry or axioms beyond Lean's own (propext, Classical.choice, Quot.sound).

• eval_sound_ty (preservation and progress): if HasTy p G Γ e τ, the program is fit to evaluate (ProgOK: the fns are well typed and the router shapes are Contract.Route's), the component names G reads hold values of their types or fail legitimately in env (EnvOK) and the locals match Γ (LocalsOK), then eval n env false ls e is a value v with ValTy p v τ, or an error that is pending, unsupported or refused — never a type error, never an unbound name. ValTy has no finiteness: 1 / 0 is a value inside an evaluation. eval_sound_E, exec_sound_E: the same for any kind of failure E the environment keeps to (EnvOKE); with E excluding pending, an evaluation where every name it reads has settled never answers pending (no roster entry or operator does: stdlib_notPending, binop_notPending).
• exec_sound_ty: a well-typed action body run the same way asks only for writes of values of the target slots' types (root and row writes), sends to mutations, or fails legitimately. With calls (LLP 1089 D9) it takes every action's body typed under its parameters, which WellTyped gives: a callee runs as the action it is.
• check_sound: check p = true → WellTyped p. Beyond types, both ask what the Rust analyzer asks of a task (analyze-unknown-action, analyze-handler-arity): it names an action of no parameters, else a timer would fire an unbound name; and what the compiler asks of a task's interval (lower-timer-literal: a number literal). A derive's body and a resource's arguments are typed in settleScope, the component scope without the states lifted from children (lifted: late or arm-owned), whose names (x#N) the root's source cannot write; pending(x)/failed(x) name a resource in scope (the checker's scope.lookup), so a root initializer cannot ask after one; current(x) names a resource, never a mutation; a resource's when is typed where its arguments are, and a resource over a list has none.
• reachable_slotsOK and reachable_valTy (TypeInvariant.lean, over Contract.Reachable): in every configuration a well-typed program reaches, each root slot is a state or mutation holding a value of its declared type. Most of this is the runtime's checks (conforms at boot and at every commit, which also makes numbers finite: that is the runtime's refusal, not typing); typing supplies that names are distinct and that a send targets a mutation, so every check is made at the slot's own type. The router slot's boot value is no check's: it is the launch of /, and routerValue_ty gives its type.
• conforms_valTy: what the runtime check admits at a complete type is a value of that type; conforms_of_valTy: a value of a type whose numbers are finite passes the check. Finiteness is all that separates them.
• VmExtract.step_ok, VmExtract.machine_run_ok (vm-extract/, checked by its own check.sh under Aeneas's Lean): the runner's VM machine as shipped, translated by Charon and Aeneas, refines Contract.Vm: whatever a step or a run of it returns, the model's step or interpreter returns too, or traps correspondingly. The trusted base (the translation, a few standard functions, the runner's Val and Host instances against the model's) is in vm-extract/README.md.
• EnvGood.envOK (EnvSound.lean): an environment whose root slots are present and of their types, whose row slots in force are of theirs and whose settled derives and resources are declared ones of theirs (EnvGood) satisfies EnvOK for the component scope.
• settle_good (SettleSound.lean): settlement from well-typed previous values returns derives and resources of their declared types (SettledOK; the runtime checks each, and a kept resource was checked when it was asked), and, when the slots are well typed for the scope the bodies are typed in, fails only legitimately — by induction over settle's passes and its two loops, each derive evaluated by eval_sound_ty under the derives settled so far; and it never fails pending (settle_strict: it waits on those).
• settle_complete (SettleComplete.lean): a settlement that succeeds has settled every derive and every resource.
• render_good (RenderSound.lean): a well-typed view (NodesTy) rendered in a well-typed environment and row store fails only legitimately (a non-finite row key or row slot initializer, an expression's refusal other than an attribute's), keeps every live row's slots of their types (StoreOK), and records only handlers naming an existing action with curried arguments typed, in the element's own scope, at most the action's leading parameters (VNodeOK).
• reachable_configOK (StepSound.lean): every configuration a well-typed program reaches is ConfigOK — root slots present and of their types, settled values of theirs, live rows' slots of theirs, every rendered handler VNodeOK, every timer running an action of no parameters, its gate and key well typed.
• runAction_sound, nextCommit_sound, dispatch_sound, advance_sound, step_sound: from a ConfigOK configuration every action that exists, every dispatch and every advance, whatever the oracle answers, lands in a ConfigOK configuration and commits, or refuses or poisons for a Legitimate reason (refused: the data seam, a non-finite number at a boundary, the host's input, the router, a row slot outside its row, a settlement cycle, fuel or the timer fire limit, a full queue, a task's key that is no key, an earlier poison; unsupported) — never pending: ConfigOK carries that every derive and resource has settled, so actions, handlers and rendering read settled values. handler_args_good and curried_conform: a handler's curried arguments evaluate to values of its action's leading parameter types, so the action's argument check refuses them only for a non-finite number; the rest of that check is about the host's payload.
• boot_sound (BootSound.lean): boot commits or is refused for a Legitimate reason. Each root initializer reads only the slots before it (rootScope), the intervals are literals, settlement reads no late slot (settleScope; the late slots still hold ()), and each late initializer reads the settled values and the late slots before it (lateScope, lateScope_not_late).
• dont_go_wrong, never_wrong: for check p = true, boot and every event from a reachable configuration, whatever the oracle answers, commit or fail for a Legitimate reason — never a type error, an unbound name or a pending read — and every reachable configuration is well typed. The checks at a derive, a slot written and a slot initialized report a value of another type as a type error (unfit), so the theorem says they refuse only a number that is not finite.
• Numbers (Binary64Facts.lean). A finite double y is the integer y.scaled times 2^-1074, and an operation's exact result ±a / (d * 2^1074), so distances are compared in integers. round_nearest: the rounding is a finite double nearest the exact value among all finite doubles; round_tie_even: another as near makes its significand even; roundMag_eq_none_iff: it overflows to infinity exactly from 2^1024 - 2^970; round_mono: it is monotone; roundMag_scale: it depends on the value alone; round_exact: a representable value rounds to itself. add_nearest, sub_nearest, mul_nearest, div_nearest: + - * / on finite operands are their exact results so rounded. ofNat_spec: every natural number up to 2^53 is a double exactly; add_ofNat, sub_ofNat: integer arithmetic there is exact; add_one_saturates: 2^53 + 1 = 2^53; ofNat_le_ofNat, ofNat_lt_ofNat: those integers compare as integers. Not proved but tested (difftest arith): NaN and infinity cases, signed zeros, %, floor, trunc, max, min.

Routes are typed: Router and Entry values, the verbs and reads at the roster's types (routerTy), path("route", …) with one string or number per parameter of a declared route, and the router slot, whose initializer is never evaluated. A value of the shape Router need not be a valid router (a source can answer one): a verb or read of it traps, which the semantics gives as a refusal (Route.verb, Route.read; likewise searchParam of an invalid entry), not a type error.

Left out: the judgments accept a ? operand where the Rust checker defers it (no value has type ?), check only what the semantics evaluates of a view (a text's text, testId, handlers, regions), type a command's arguments without its host signature, and check the expanded root, so a component nothing uses is not checked. Rust refuses more: let shadowing, host command signatures, presentation attributes, placeholders, t(...)'s key and placeholder names against the tables, and a prop's declared type where the expansion reads its argument only in presentation or not at all (the ascription is judged where the semantics evaluates it). A data source's signature is carried as the Rust checker unified it across its uses, and checked per use (sourceOk: as many arguments, each meeting its parameter, the answer meeting the source's).

The clock

advance moves the clock as the runner's advance_within does. Timers fire in order of due time, ties by declaration order. A mutation's then is armed, due at the commit's time, by every commit that stood in which a send into the mutation was answered (here every answer is synchronous, armThens; arming again moves the due time); it runs as its own commit at the next advance or land, before any timer due at or after its time, ties by the mutations' order. A frame task is the runner's virtual display while the host presents no frames (the harness never does): due at virtualFrame 0 k = k·1000/60 for k = 1, 2, …; presented frames (Runner::frame) are not modelled. One advance makes at most 4096 fires, thens and queues' nexts counted. The actions the clock runs are clockActions: the tasks' and the mutations' thens (and, by nextCommit, queued sends).

Formatting and localized text

formatTime, formatDate, formatDay and formatNumber (Contract/Format.lean) are the runner's (runner/src/stdlib.rs, runner/src/format/) transcribed: en-US at the fixed UTC offset the call names, the wall time truncated then shifted and held to years 1–9999 (else ""), the calendar by Hinnant's civil_from_days over integers. formatDate also takes a strict ASCII YYYY-MM-DD Gregorian day key in years 0001–9999, validated by Str.isoDate and formatted without shifting its day; invalid keys or offsets print "". Compact numbers come from the shortest digits Rust's {} prints (of two equally near shortest forms the upper, where toString takes the even). t(...) reads the strings tables (strings/<locale>.json beside the source), which the embedding carries (Program.strings, the base first) with the resolved locale's slot (Program.locale, the plan's #locale, initialized to the base before every other slot and left out of the observation, as the runner's is). The embedding writes t("key", name=value) as the compiler lowers it: the locale slot, the key, then each name and its value through toString; Plan::localized falls back to the base table and strings::fill fills {$name}/{name} and the \{, \}, \\ escapes. The host's place event (a viewer locale other than the base) is not delivered by the harness, so only the base table is read there.

Each takes the format locale last (LLP 1054.000.003 D6), as the embedding writes the call: "" in a program whose tables all format as en does, which is the en-US above, else the format slot (#format, initialized to the base table's name after the locale slot and left out of the observation, as the runner's and the JS target's are). Its table's record (contract/lower/src/formats.rs) rides in that table's (key, text) pairs under Format.formatKey, a key no table can hold, and Format.recordOf, styledIn, compactIn, dateIn, timeIn and dayIn are runner/src/format/locale.rs transcribed over it. The corpus's localized-formats reads a German base, and localized-formats-at a base named with an extension (de-AT-u-nu-latn) whose money has its own symbols. Outside the semantics: a localized formatter in a fn, whose body the compiler expands where it is called and so reads the format slot there, while the semantics evaluates a fn closed over its parameters (as it does t there, which reads the locale slot).

Queued sends and gated tasks (LLP 1092)

Contract/Runtime.lean carries both. A queue mutation's send that may not be asked now (it is not free — its then or its next armed, or it is stalled — one of it already waits, or it was sent earlier in the commit) joins Config.queued; dispatch never drains it. After every commit concludes, a scan (Config.armNexts, the runner's arm_next) arms the next of each free queue mutation with a send waiting, due at the commit's time (Config.nexts, the runner's next_due), so a queue's drain waits while its then is armed and then runs once per reply, in send order. advance runs an armed next (clockPick) before a then due at or after its time and before a timer due after it, as the runner's advance_within orders them; nextCommit (D3's next commit) asks the oldest waiting send, arms the mutation's then when it lands, and scans: its own ask's refusal drops it and stops the advance; any other refusal keeps it, records the state it saw in Config.stalled, and stops the advance, and no next is armed for it until a commit that stood changed a slot, a derive or a resource from that state. A gated task's timer is idle (an infinite deadline) until the gate step (gateStep, D8), run inside every commit after its settlement and at boot after the late slots, finds its gate true; a changed key (rowKey's reading) re-arms it from the commit's time — a frame task's virtual frames start again there, virtualFrame now k — and a key that is no key refuses the commit. The observation prints queued <mutation> <count> for each queue mutation, on both sides. The corpus has mutations/queue-* (queue-then: a queue with a then beside a timer) and timers/gated-* (gated-frame), and the generator writes queue mutations (sent more than once on a path) and gated tasks over the states alone.

The one-slot invariants include queue mutation slots. SlotInvariant x V c combines SlotIn x V c.slots with QueuedIn x V c.queued: ∀ q ∈ c.queued, q.1 = x → ∀ v, V (.some v). Boot has no waiting sends; BodyKeeps supplies the answer property for new sends, and a drain either lands such an answer, removes a refused send, or keeps it stalled. Poisoning clears the waiting sends. Reachable.slotIn projects the slot property; Reachable.slotInvariant, Event.step_slotInvariant and Reachable.advance_slotInvariant carry both. Contract/Invariant.lean has a checked example with two sends to one queue, a drain, refusal and poisoning. The equality rule Reachable.advance_untouched and the slot-only event rule Event.step_slotIn still require a slot no drain writes: waiting answers can change a queue mutation's slot even when no clock action touches it.

What it does not carry, as restrictions:

• pending(m) is false for a queue mutation whose send waits (the oracle answers at once, so nothing is ever in flight here; the runner's is true). The generator never reads pending of a mutation.
• A send behind one in flight (every answer here is synchronous) is the runner's and the conformance plans' tests (contract/cli/tests/it/queue.rs, host/web-js/conformance/queue.contract).
• The component-level semantics (Contract.CompSem) refuses both, so difftest expansion writes and reads programs without them.

Whether an answer is current, and a resource's when (LLP 1161.001, 1161.002)

A resource may carry a gate (ResourceDecl.gate, resource r = s(args) when cond). settle reads it before the arguments (gateOpen; a value other than true closes it, as the runner reads it). Closed, the resource is idle: its arguments are not read, nothing is asked even when the commit refreshes it, it keeps its previous value (idleValue; before any value, its type's zero, zeroOf), it has no Settled.args entry, and its name is in Settled.idle. With no arguments kept, the settlement that opens the gate asks again, at the same arguments or new ones. current(r) reads Env.idle: every settled answer here answers its arguments, so it is true unless r is idle; the VM reads the runner's flag (Vm.Env.currentResources, CurrentResource), and the lowering proof takes the two to agree (RefOk). The corpus has resources/current and resources/gate.

What it does not carry:

• A placeholder: a resource idle before its first answer holds its type's zero, where the runner shows its else. A program that gates a resource with an else placeholder disagrees until the first answer, and a string enum's zero here is "" (the embedding types an enum string) where the runner's is its first member.
• A request in flight when the gate closes, an upload's or a stream's, and the window between waking and the forced ask's answer, when the runner's current is false: answers here are synchronous. The runner's tests (contract/cli/tests/it/when.rs, current.rs) and the conformance plan (host/web-js/conformance/gate.contract) check these.

Persisted state (LLP 1116 D5)

A root state … persist starts from the device's store: Oracle.stored, each persisted state's kept value by name, which restore (Runtime.lean) takes at boot where it conforms to the state's type, else the initializer's value stands. The store is part of the oracle because it is the device's, as every answer there is: Reachable quantifies over it, so every theorem holds whatever a device kept, and SlotOrigin gains the stored value of its type as a third origin of a persisted state's boot value (restore_cases, restore_conforms). Each step's observation adds a store <name> <value> line per persisted state after the slots: what the runner's store keeps for it, decoded (Runner::persisted), against the slot's value in the semantics, since after every commit that stands the store holds the slot's value. The oracle text carries the store as stored <name> <value> lines.

A corpus test starts from an empty store, as an authored test does. Each corpus case whose program persists a state runs again as <name> (stored) on a store the oracle fills from its seed: per state nothing, a value of its type, or one of another kind (Oracle::with_store), with the case's events and no expects. Random programs mark about a third of the root states of a persistable type persist (drawn apart from the program's own generator) and always run on a filled store. --js hands the JS target the same store as its localStorage (persist.js) and compares its store lines too.

The store's text, its 16 KB bound, and the compiler's refusal of persist on other types (type-persist-type, type-persist-child) are the runner's and the compiler's: the semantics takes decoded values and any type.

What the semantics leaves out

Geometry reads (frame(id), measure(id): where layout put a node) are refused as unsupported rather than given a meaning: layout is out of scope. So are resources reading exactTransport and exactMIDI (LLP 1125), which the runner answers from its transport and its MIDI ports and answers again as they play; the semantics models neither. A native module's state (a permission, a preferred value, what a send to it answered) is the runner's: the semantics holds a module read's boot answer, a call it has no fact for (a send, one per element, or a read with no answer at boot: closed, held or failed, whose placeholder is no answer) is unsupported, and a step where a read no longer holds its boot answer carries # outside: a module's answer moved, from which a first difference is OUTSIDE, a poll the trace leaves out included. sendMIDI and requestMIDIAccess are in, as commands. toLowerCase and toUpperCase (LLP 1088 D2) are typed but left out: their mappings are Unicode's case tables, which the semantics does not carry, and the generator writes neither. The corpus checks them against the values Bun gives (corpus/typescript/lowercase.contract, uppercase.contract), the runner and the web runtime agreeing. Routes are in (Contract/Route.lean, the exact_route crate and the runner's plan boundary transcribed): the router slot starts at the launch of /, as the harness boots the runner, and a commit that leaves it holding an invalid router is refused; the host's navigate event, which the harness does not deliver, is not modelled, nor a router carried across a reload, nor the change the runner publishes to a host after a commit. A refused verb answers its input, and the runner journals the refusal in its log, which no observation shows. The router slot is observed like any other root slot.

Navigation tabs are in (Contract/Tabs.lean, LLP 1075.003 §9.14): a literal role="tabpanel" below a navigation root waits for its first selection. Selection opens panels until a route holds the root's key, preferring an aria-selected tab, then tab order; a panel no tab names opens at once. Visited panels retain their contents and state until removed. The expander puts a panel's contents in one arm, so component state initializes when that panel first opens; a virtualized panel keeps its for as the owner. Both interpreters leave an unopened panel's descendants out of the tree, so they cannot be observed or receive events. A prerendered page's host builds every panel from boot on (Runner::build_every_tab): the oracle's everyTab (every-tab in its text) opens every panel as it is made, and each corpus case with a "tabpanel" runs again as <name> (prerendered) on such a host, with its events and no expects (the JS driver boots the agent's way, so the variant is outside the JS target). A reload, and the panel state it carries (carry_panels), are not modelled: the semantics has no reload.

Presentation attributes are carried in the embedding but not evaluated, except the six attributes tab selection reads (role, id, navigationKey, navigationBack, aria-controls, aria-selected). An attribute whose expression is refused (other than for fuel) has no value and the render goes on (unsetRefused), as the runner unsets a prop or style binding that traps (LLP 1017.003 D3); a refused subject, key or row initializer still fails the render. Only a text's text and an element's testId are observed, and nothing inside a virtualized list: the runner builds only the rows its window lays out, which is layout, so both sides leave a virtualized list's descendants out of the observation (the list's own line stays). The runner's evaluation bounds (list steps, derive calls and call depth, string length, value size and depth) are a refinement the semantics doesn't model (LLP 1090 D8): a step the runner refuses for one (IterationLimit, CallLimit, CallDepth, StringTooLong as a trap or an argument's or write's refusal, ValueTooLarge, ValueTooDeep) is UNSUPPORTED, outside the semantics, not a divergence, and so is a step after the runner unset a binding for one (its journal line is a # note in the runner's observation). The web's JS target refuses the same steps (host/web-js/conform.mjs). The checker's two type refusals that bound a value (type-option-option, type-too-deep) are in Contract.check too (checkBounds, and where infer grows a type: some, map, the roster).

Executable instance expressions share plan rows during lowering. Source expansion and instance_iff still use substitution. VmRows runs these calls over Vm.step: a fresh callee machine, empty parameters and writable slots, frames cut to the owner, and the caller restored with the returned value. Calls share a 65,536-call counter and a depth bound of 64. Callback work shares a 65,536-step counter. owner_frames_cut proves selection of the nearest owner; frame_read_rebase relates item, index and bound reads across the cut. Its checked examples exercise owner selection, local isolation, depth, sibling calls and caller-spent callback work. Instance frames carry owned-slot stores. A call reselects slots from the retained frames, taking only the nearest instance of each owning region; return restores the caller's slots and frames. Checked examples cover a retained owner, an inaccessible inner slot, a root call and a missing slot in the nearest instance. These stores are modeled but are not yet supplied by LowerCheck's contextual validation.

LowerCheck receives row bytecode, owner regions and the checked substituted expressions that lowering shares. It decodes every body and compares root-owned rows with source evaluation, including transitive row calls. A mutation test changes an executable body and requires a divergence. Arm-owned rows are reported as needing an instance environment and counted as refused by this check; they are not claimed as validated.

Still owed: the general correspondence between shared loads and substitution, including the matcher's scope and binder conditions; contextual validation of arm-owned bodies and their view readers; and refinement of VmRows to the runner's row-call implementation. The model does not yet carry the roster's list-step, string and extent accounting. The existing lowering theorems cover Vm without this sharing transformation. The call model and its local invariants do not extend those theorems.