wek/ — the R2 bounded executable model

R2 CLOSED 2026-09-13 under the four-register checklist (WEK_R2_CLOSED.md). These bytes are the closed model; WEK_R3_ADMISSION_PROPOSAL.md is what comes next, and is not authorized.

Round: R2, slice 4 (boundary ownership and the reserved journal, authorized by WEK_R2_SLICE3_ADJUDICATED.md §5) Status: a model, not an implementation. Nothing here runs in production, talks to a network, or touches super/. It exists so that R1's refusals can be executed instead of asserted. Run it: node wek/run.mjs — exits non-zero if any guard, law, mutation control or oracle comparison is off. About three minutes on this machine: each mutant runs its law suite in its own process, in a pool.

node wek/run.mjs                          full run; derives wek/COVERAGE.md and wek/RECEIPT.json
node wek/run.mjs --quiet                  verdict line only
bash scripts/check-wek-model-digests.sh   reproduce all four receipt digests outside this program
node scripts/wek-slice3-probes.mjs wek    the slice-2 adjudicator's bypasses, against this tree
node scripts/wek-slice4-probes.mjs wek    the slice-3 adjudicator's bypasses, against this tree

WEK R2.4 GREEN · 47/47 laws · 50/50 behavioural mutants · clean-copy control held · 5/5 guards · 50625+21696+729 sequences/0 mismatches

Those are separate figures (ruled 2026-09-12): 47 executable invariants; 50 behavioural mutants; 1 clean-copy control; 5 shallow source guards; and three bounded explorations against hand-written oracles — 50,625 lifecycle sequences (depth 4 over 15 op instances), 21,696 attack sequences (every prefix of depth ≤ 3, then one attack, then one probe; max depth 5), and 729 store sequences (depth 3 over 9 ops). COVERAGE.md reports 43 distinct failure signatures under this mutant set — which laws only ever move together — and any law no mutant exercises (none). A signature count is not a dimension count and is not assurance.

What it models, and why only this much

Not modelled, by ruling: a WCI transport, atomicity claims, plateau results, a production backend, substrate authorization of administrative operations, anything implementation-shaped.

Zero dependencies

node:crypto only. Ed25519 with keys from a fixed seed, so the model stays deterministic.

Files

model.mjs                     canonical bytes · declared refusal classes · Σ.P · Σ.A · Σ.H with
                              RETENTION modes (BR-*) and ORDER modes (ORD-*), every record copied in
                              and DETACHED out · place() · W-7 commit classes · the W-7.2 store set:
                              ONE commitIntent() with validation, an opaque handle, PRIVATE scope, a
                              RESERVED journal, journal copies, an optional audit sink · recovery that
                              NAMES corruption
classify.mjs                  the VERIFIER. Receives an assertion, opaque basis identities, and
                              verifier-owned trust state (public keys, copied at construction). Holds
                              no signing key.
fixtures/agent-invariants.mjs the CLASSIFIER FIXTURE. Stands in for Agent-Invariants; the only file
                              with a signing key. Never imported by the verifier (guard G1).
authority.mjs                 the MONITOR. Built once from trust + profile (copied); owns history,
                              capability and grant state; names ADMINISTRATIVE vs ORDINARY operations;
                              exports monitor() and its tables, nothing that takes trust/history/grants
                              as a call argument (guard G4). Every response and read is detached.
oracle.mjs                    the INDEPENDENT oracles: the lifecycle (with the duplicate rule and the
                              three attack families, ruled ABSORBED) and the mediated store. Imports
                              nothing from the monitor (guard G5).
vectors.mjs                   #27 (4 modes) · #27b · #27c · W-7.1 · W-7.2 (8 bypass attempts, crash,
                              audit-sink-down, reserved journal, invalid declarations, malformed
                              journal) · the REQ-1 matrix · the attacker set · revalidation · the
                              lifecycle table · the alias attacks · three explorations. Deterministic.
laws.mjs                      47 executable invariants, taking the modules as an argument
mutations.mjs                 50 behavioural mutants + the clean-copy control, each evaluated in its
                              own process by mutant-worker.mjs; a mutant may name laws it must EVADE.
                              The WORKER BOUNDARY: every worker outcome is classified with a name
                              (WORKER_FAILURES) and recorded; a failure is never a caught mutant
mutant-worker.mjs             one mutant, one process: runs the laws from its directory, writes the
                              result to result.json (written whole, renamed into place) and a sha256
                              trailer on stdout; the parent requires both
fault-worker.mjs              the FAULT worker: misbehaves in one named way (fault-modes.mjs) and runs
                              no laws; stands in for the mutant worker under the harness controls
harness-controls.mjs          17 harness controls, two of them POSITIVE: 12 named faults + 2 positive
                              (a well-formed result must be ADMITTED) through runWorker, and 3 through
                              the real pool path, where the control must FAIL and the mutant must be a
                              harness failure, not a law gap
run.mjs                       the guard; stamps RECEIPT.json INCOMPLETE first, ABORTED on a handled failure
                              (INCOMPLETE stays after an uncatchable termination),
                              and writes RECEIPT.json + COVERAGE.md + a run log at the end
history/                      slice-2, slice-3 and slice-4 receipts and coverage, preserved as delivered
r3/                           the E3-1 CONTRACT, executable (R3, 2026-09-14): contract.mjs (authorize · classify ·
                              checkTrace · acceptCase · validateIntent · categorize, tables as data), fixtures.mjs
                              (32 synthetic traces: the walkthroughs, the review discrepancies, malformed evidence,
                              must-fail cases), check.mjs (replay, 8 contract mutants, generated CONTRACT_TABLES.md,
                              RECEIPT.json). `node wek/r3/check.mjs` — SYNTHETIC; establishes NO substrate conformance

Administrative and ordinary operations

ADMINISTRATIVE  construct · establish · reconfigure · issueGrant · revoke
                configuration authority — WEK SPECIFIES the requirement, the substrate DISCHARGES it;
                this model names the split and does not implement substrate authorization
ORDINARY        applyEmbodimentChange · check · revalidate
                requests — WEK's to refuse; a request carrying its own trust, history, grants,
                capability snapshot or target basis is not honoured (L38)
READ-ONLY       state · grant · liveBasis · records · trustIssuers — every read is a detached copy

The constructor's caller is trusted by stated assumption. That trust does not let a mutable alias escape afterwards: accepted profiles are copied in, and every committed record, history read, retained envelope, state snapshot and grant read is a deep-frozen deep copy (L39–L41).

The ownership boundary — what holds it, and what does not

Agent-Invariants   owns the FACTUAL classification of an embodiment change
WEK                owns its AUTHORITY CONSEQUENCE, and enforces that
WEK MUST NOT       invent the underlying classification theory

What holds it: the fixture signs; the verifier owns public material only; L21 re-verifies every admitted class against the fixture's public key, independently of the verifier, and requires it to equal the class WEK committed. L13 is a shallow two-argument probe and says so; three mutants derive a class inside admit() and are recorded as evading L13 while L21 catches them.

Six results the model produces

1 — Basis adjudicability is RETAIN + ORDER, and the order needed is per-basis.

BR-NONE             A=INDETERMINATE  B=INDETERMINATE  discriminates=false
BR-LOCAL-NO-ORDER   A=LEGAL          B=INDETERMINATE  discriminates=false
BR-LOCAL            A=LEGAL          B=ILLEGAL        discriminates=true     (total order: one implementation)
BR-LOCAL-PER-BASIS  A=LEGAL          B=ILLEGAL        discriminates=true     (the weakest sufficient relation)

2 — W-7.2: an undeclared write never lands, the journal is reserved, and corruption is named.

Eight bypass attempts refuse with the store unchanged. Declaring _intent is INTENT_INVALID and journals nothing; writing there under a real handle is refused; six invalid declarations refuse before any mutation. A journal holding malformed durable records recovers to a named corruption outcome — not a throw, not "clean" — that still lists the gaps of the records that parsed. With the audit sink down, the write is still refused. No journaled backend is reported W-7 conformant.

3 — Freshness is validated issuance against a current suspension; replay is not usability.

A revalidation grant is issued for a capability's current suspension (a LIVE capability: SUSPENSION_UNKNOWN) and bound to capability, generation, target basis and fact-set version. Stale in any one dimension is AUTHORITY_NOT_FRESH. A retry of a consumed grant returns the current state as its value and the prior outcome separately, creating no transition — after a further suspension the value is SUSPENDED while the prior outcome was LIVE.

4 — The lifecycle is a table, resolved from current state, with no generation churn.

LIVE         STILL→LIVE · REQUIRES→SUSPENDED(gen+1) · INVALIDATED→WITHDRAWN · UNAVAILABLE→UNAVAILABLE
SUSPENDED    STILL→TRANSITION_REFUSED · REQUIRES(distinct transition)→SUSPENDED(gen+1) · INVALIDATED→WITHDRAWN · UNAVAILABLE→UNAVAILABLE
WITHDRAWN    every class TRANSITION_REFUSED
UNAVAILABLE  every class TRANSITION_REFUSED   (terminal for this capability instance in this model — ruled)
identical classification again  → CLASSIFICATION_DUPLICATE, no transition, no new generation

5 — Nothing that crosses the boundary carries authority.

Editing a returned issue response's binding (committed and value) throws, changes neither the grant record nor the history, and leaves a refused revalidation refused. Editing a supplied profile after construction or reconfiguration moves nothing. Editing a history read, a state snapshot, a grant read, a retained envelope, or the registry's entry array changes nothing held. The slice-3 model failed all of these.

6 — Every sequence in three bounded universes agrees with its oracle.

Lifecycle: 15 op instances, depth 4, 50,625 sequences. Attacks: every prefix of depth ≤ 3, then one of three attack families (edit a returned binding, edit a supplied profile, edit a history read — ruled ABSORBED), then one of two probes: 21,696 sequences. Store: 9 ops incl. a reserved declaration and a journal write, depth 3, 729 sequences. 0 mismatches. What is claimed is exactly those universes and depths; nothing outside them.

The worker boundary (R2 closure repair, 2026-09-13)

The adjudicator's two pooled reruns of slice 4 each died with SyntaxError: Unexpected end of JSON input at mutations.mjs:286: a worker had exited 0 with empty stdout, and the parent parsed that inside a bare execFile callback, so the throw escaped the promise, the run ended with no receipt, and the previous GREEN receipt stayed on disk looking current. The repair treats a worker's output as data from another process:

• Transport. The worker writes its result to result.json.partial synchronously and renames

it to result.json (a partial file is never a result), then prints one trailer line naming the file's sha256 and byte length. On this Linux/Node 25 a piped stdout is asynchronous (a large write followed by process.exit delivers one pipe buffer), which is why the result no longer rides the pipe. The parent requires both channels and names which one failed — file absent means the worker never completed; file complete with no trailer means the stdio channel.

• Validation. Termination by signal or non-zero exit, no result, malformed JSON, a wrong

shape, an empty law list, duplicate, missing or undeclared law IDs, a missing or mismatched trailer — each is a named WORKER_* harness failure. None counts as a caught mutant; on the clean copy each is a FAILED control (the old control computed [].every(...) and would have held over an empty list).

• Records. Every worker leaves a record — pid, exit, signal, stdout bytes, a stderr tail,

timing, result bytes and digest, and what it reported about itself (node version, platform, execPath) — in the run log run.mjs names at the end. A RED receipt carries its failures.

• Settings. WEK_WORKERS=N or --workers=N bounds the pool; WEK_SCRATCH_DIR moves the

mutant copies off the OS temp dir. --inject-worker-fault=<mode> substitutes the fault worker for MUT-1 in a full run, which must then end RED with exit 1.

• No stale GREEN. RECEIPT.json is stamped INCOMPLETE before anything runs and ABORTED

(with the error) on a handled failure — an uncaught exception, an unhandled rejection, an exit before the verdict. An uncatchable termination leaves INCOMPLETE, which is the right reading: a run started and no verdict was written. Only a finished run writes a verdict.

Four digests, ruled apart

RECEIPT.json carries evidence_digest (over what the model produced), source_digest (over all thirteen files), and the same listing split into model_source_digest and harness_digest — the harness half binds mutations.mjs, the file that decides the mutants and their expected failures, and since the closure repair the worker, the fault worker and the harness controls, so the recorded verdict is bound to the harness that produced it. scripts/check-wek-model-digests.sh reproduces the three source digests with coreutils and the evidence digest with two runs.

Mutations and vectors that found their own defects

Slice 1: MUT-1 → L20. Slice 2: MUT-16 walked past an L21 that compared the input against its own label. Slice 3: a grant-name collision hid the positive case; every stale-generation grant was also stale in target. Slice 4: the alias vector expected the wrong first history record; the duplicate rule masked MUT-35 from L35 until a wrong-source-live-target case existed; and the exploration cannot see a construction-time alias because its universe reconfigures in setup — recorded on MUT-41, with MUT-51 (the reconfigure-time alias) as the one it does see.