Run one job end to end as a recursive language model

[1zeroone0]

The first end-to-end job, as a Recursive Language Model: Cloud Hypervisor boots one machine, unattested; its report is the first record; the root process drives a shell and fans work out to agent sub-processes; the root's reply ends the job and is signed into the log. Graded mechanically on the host. From Horizon #7 ("loop: one boot, one process, a reply" and "agent and meters", merged here because the RLM thesis is the harness: a loop without programmatic sub-calls is context offloading alone, which the RLM work shows breaks down over long horizons). Builds on the spec in #11 and the method in #12.

Spec slice: layers 1 and 3, one boot and its process tree (Boot, Start, Dispatch, Issue, Decide, Witness, Finish, Exhaust, Timeout, ReapChild, Reap, Leave, Arrive; properties 1–11 and 14–19).

What this PR does

• Spec first, matching the harness. Decide sends the decision and starts the command; the process stays blocked until Witness, when the command ends however it ends (a foreground agent ends when its child is reaped). Timeout ends the root process, killing the tree; Reap is the only exit and requires every command witnessed, so an exit record never hides a gap. The exit record carries the root's reply: the answer is signed. Call records name the process that ran them and a spawning decision names its child, so the log holds the process tree. Properties 18 (a live process is blocked exactly while it waits) and 19 (ProcessTree).
• RLM, in shell. Context is offloaded: the query is commit-sized argv, context arrives on stdin and is saved as a file, never put in a window. Sub-calls are programmatic: x=$(agent "…" < slice), agent … > a & wait; a child's answer is its stdout, in a file or variable until read.
• agent. A child process with its own shell, window, cgroup and PID namespace; its slice on stdin; rights ⊆ its parent's and depth − 1 set when spawned; its meter capped in argv, every call charged to each meter above it (KeyKOS). A process ends when the model replies without a command; its live descendants are killed. kill reaches only descendants.
• What a call returns. The exit code, and the command's stdout if it fits the output bound. If it does not, none of it enters the window: the model gets the exit code, the size and the path of a spill file holding it all (exit 0 · 48213 bytes → /spill/12), and queries that file like any other state. Domain-free by construction.
• The window appends each command and what it returned. When the next inference would exceed the window limit, the process ends with limit; no eviction. So each call's window begins with the previous call's bytes (prefix-stable).
• Custody of the key: init stays PID 1 for the whole boot, makes the key and signs every record; the harness asks it over a pipe. A compromised harness is a signing oracle for the boot's life, never a key thief. Harness death ends the boot with no exit record: unknown.
• Records: numbered from the report, each signed by the boot's key; the boot's public key names the boot. No hash chain: under KeySecret a signature already fixes author and place.
• Report, unattested: the same record; its attestation is SNP or none. The log accepts none only when configured for trusted-host mode.
• Log: one append-only file per boot, a line per record (its canonical encoding and signature, in hex: the format Lean's replay reads, so the log and the forensics tool share one), written by the operator's cead on the host from records over vsock, applying Arrive's checks. Trusted-host mode only: a report must be unattested until the confidential machine PR checks SNP reports.
• Dependencies: ed25519-dalek, sha2, rustix, and serde_json in the gateway only. Bedrock through an API key and curl on the host, if API keys cover Converse; otherwise aws-sigv4 returns as a question.
• The log replays every window. Records carry every byte a window holds: the report the pinned prompt and the root's query; a spawning decision the child's query; an intent the model's whole turn beside the command taken from it; the record ending a call (a deny, or the witness) what the call returned. The witness keeps the whole output's digest, so what was returned is checked against what was produced. Forensics runs from the log alone, and the gateway's record of each request to Bedrock is a second, independent reconstruction to check it against.
• Lean, by the scalpel "what must a skeptic trust", each green before its Rust and tied to it by a differential test (the differential executable runs the spec on random inputs and prints bytes and verdicts; cargo test compares):
  • record encoding: canonical and injective
  • log acceptance, for every log size
  • meters: no subtree outspends its root, for every tree and sequence of spawns and charges
  • windows: replayed from the log's records, prefix-stable
• Model: Claude Sonnet 5.5 on AWS Bedrock through a gateway on the host that holds the credentials and signs with SigV4 (aws-sigv4 plus a small HTTP client, each dependency approved at the fill that needs it).
• CLI contract: argv a commit-sized query; stdin optional context; stdout the answer only; stderr diagnostics; exit code the outcome (sysexits). Each call renders on stderr when it is a TTY. Plain lines.
• System prompt capped, rendered from what was mounted; per-call values in the shell prompt string ([call 12/100] $).
• Host: the Surface, Windows wiped, Linux x86_64 with KVM and vhost-vsock; driven over ssh from the Mac. Brought up in parallel with the skeleton. No Docker needed: grading is exact match.

What this PR does not do

• Fork, snapshot or recovery (Horizon: machine fork); attestation (Horizon: confidential machine). The report path is built; its attestation is none.

• The tracer (the witness here is the harness's view of the command's end), policy beyond permit-all, the core/task disk split (Horizon).

• Revoke a right from a running child: revocation is kill.

• Evict from a window.

• Split the crate.

• A leaderboard claim, or a file-tree task: CodeQA ships no tree, so the first job tests reaching one large context through a shell, not navigating a repository. Tree-shaped tasks (the SWE-bench family) are later evals.

• The task: CodeQA (LongBench v2's code repository understanding split, Apache-2.0): multiple-choice questions over a whole repository given as one concatenated text (0.1M–16.2M characters; no file paths or separators, so no tree). 20 of its 50 questions, chosen before any run, stratified by its difficulty and length labels. The answer is a letter: the root's reply; the grader is exact match on the host.

• Three-way comparison, one variable, the RLM paper's design in our terms: the same questions, model (Sonnet 5.5 on Bedrock) and sub-call model; only how the model reaches the context differs. Base: in the prompt, one call; a context that does not fit scores as a failure. RLM: the reference implementation (alexzhang13/rlm, MIT), the context as a REPL variable, with an adapter for Bedrock (its Anthropic client swapped for the SDK's AnthropicBedrock). cead: the context as a file in the machine, agent sub-calls in shell. Scored as accuracy and cost per question, inference vs everything else. The RLM paper reports CodeQA with GPT-5 at about 20–24% base and 60–62% RLM, depending on version.

Open, scoped before the skeleton

• From "agent and meters": a child's writes (copy-on-write scratch, committed or discarded on exit); exit codes per reason; context inheritance (a parent handing a child its window as a file); the cost of a child that replies without a command.

Merge requirements

• Spec change first: TLC green on both cfgs; each new guard and property has a mutation TLC catches.
• Specify cead as a system in TLA+ #11's mutations re-run against the current spec.
• tree.cfg receipt run at 3 processes, depth 2.
• Lean specs green before their Rust; differential tests in cargo test.
• cead run answers the 20 CodeQA questions end to end, a parent reading a child's answer from a file, graded on the host; base and RLM arms run on the same questions and model.
• Every call has its three records in the log, naming its process, after the boot's report, before its exit record; the exit record's reply digest matches stdout.
• No tree spends past its root's meter; kill reaches only descendants; no zombie after a job.
• Zero placeholders (CODE.md); cargo clippy --all-targets -- -D warnings and cargo test green.
• Measurements: cold boot to first command; the report's round trip; per-call log round trip and signature; init's signing hop; spawn latency; harness time per call; spill follow-up rate; cost per completed task, inference vs everything else.
• One honest limitation, stated here.

Record

• TLC 2.19: cead.cfg 315,202 distinct states, 25 s; tree.cfg 769,040, 48 s. A first cut that let a process run on before its command was witnessed was sound but unfaithful and cost 2,185,268 states, 2m18s; matching the harness removed both.
• Mutations caught: Reap without its witness guard → Complete; reply dropped → FinishHonest; witness with the wrong id → Complete; Decide readying on allow → BlockedWaits; Snapshot without its witness guard → BlockedWaits; Witness not waiting for the child → BlockedWaits; spawning decision without its child, and intent, decision or witness naming the root instead of the process → ProcessTree.
• Receipt: tree.cfg at 3 processes, depth 2 (every property, liveness included): 26,259,440 distinct states, depth 37, 38m01s, no error. The complete state space; Specify cead as a system in TLA+ #11 had stopped this bound past 11M.
• Specify cead as a system in TLA+ #11's mutations against the current spec, each with a cfg checking only its target: all 23 caught (IntentFirst, LogOnlyGrows, DenyNeverRuns, call limit via TypeOK, BootEnds, OnlyMachine ×2, ExecutedOnce, Unambiguous, FinishHonest, Complete, ReportFirst, Rooted, OneOutcome ×4, OnProcessors, WithinMeter, Attenuated ×2, KillReach). Two need larger bounds: rights attenuation needs 3 processes at depth 2, a second recovery needs 3 boots.
• Lean 4.34.1: record encoding canonical and injective; log acceptance valid for every log built from empty; every reachable meter tree balanced (meter + subtree calls = cap), so none outspends its root; windows prefix-stable. On propext and Quot.sound (the meter proof also Classical.choice), no sorry. Five meter mutations each break the proof. Each of the 9 acceptance guards replaced by True breaks a proof. The hash chain was dropped (Q21): under KeySecret a signature already fixes each record's author and place.

🤖 Generated with Claude Code

[1zeroone0]

e7a7de4: Witness a call when its command ends, and sign the answer

1. Built: Decide sends the decision and, on allow, appends to executed and to a new per-boot unwitnessed. The new action Witness(b, e) sends the witness and clears the call. Exit and Snapshot require unwitnessed[b] = {}. Finish(b, p, y) records the reply; Reap puts the root's reply on the exit record (new record field reply, new constant Replies). FinishHonest also checks the reply.

2. Why: the spec executed and witnessed in one step, but the real harness can't: the witness comes when the command ends. Without the guard, a timeout or a harness death between decision and witness yields a "complete" boot missing a witness. The reply was the one output that left the machine unsigned. The variable is named unwitnessed, not open, to avoid colliding with open(2).

   • Rejected: keeping the process blocked until its witness. That's more faithful, but it tangles foreground agent (whose witness is the child's end) with ReapChild. The chosen model admits a superset of real behaviours, so safety still carries over.

3. Bloat: Decide lost its second record. Witness is one action, independent of processes, so the kill and cut-off paths needed no new branches.

4. Drift: CODE.md Core now uses the scalpel ("what a skeptic has to trust"). CODE.md init, harness and record rows now say init is PID 1 for the whole boot, holds and signs, and forks the harness. README boot steps 2 and 5 and Observability updated to match. AGENTS.md's "next commit is typed stubs" no longer trips, since this PR does open with a spec commit.

5. Trust surface: TLC green on both cfgs (numbers in the description). Mutations caught:

   • no Exit guard → Complete
   • reply dropped → FinishHonest
   • witness with wrong id → Complete

   Not caught:

   • Witness never sent. The seq gap makes the boot unknown, not falsely complete. That's correct, but no property requires a well-behaved boot to be complete.
   • Snapshot without its unwitnessed guard. No property needs it; it encodes "between calls" only.

6. How it breaks:

   • tree.cfg tripled to 2m18s. The superset model interleaves witnesses with everything.
   • Replies = {y1} catches a dropped reply, but not one swapped between two replies. With {y1, y2}, cead.cfg was 865k states and 68 s; the mutation that needs two values wasn't run.

7. Not confident:

   • Whether the Snapshot guard should stay (meaning) or go (no property needs it).
   • Whether tree.cfg at 2m18s should be cut back with the faithful blocked-until-witnessed model.

8. Verify yourself:

   • Witness, and the Exit guard in spec/cead.tla.
   • FinishHonest's reply clause.
   • The CODE.md Core line (the scalpel wording).

9. Next steps: additional commits. Install Lean (elan is not on this machine), then Lean specs for encoding, acceptance, Bounded and window assembly; then the skeleton.

[1zeroone0]

8ea6b3b: Block a process until its command ends, as the harness does

1. Built:
   • Decide on allow leaves the process blocked.
   • Witness requires the process not to be waiting on a foreground child, sends the witness, and readies the process if it is still live. Entries in unwitnessed now name their process.
   • ReapChild only clears waits.
   • Timeout now ends the root process, which kills the tree, instead of exiting the boot.
   • Exit is folded into Reap, the single exit path, guarded by unwitnessed = {}.
   • New property 18, BlockedWaits: a live process is blocked exactly while it waits (on a decision, or on its command's end), and a process with waits set is blocked on a live or zombie child.
2. Why: the first cut let the model issue its next call before the previous command ended, which the harness can't do. A spec that allows behaviours the system can't have stops being a reference. Timeout as "exit now" couldn't coexist with "every command witnessed first"; as "end the root", it reuses Ended, and the witnesses follow.
3. Bloat: removed Exit as a separate action, Done, and ReapChild's readying branch. Timeout reuses Ended/CutOff.
4. Drift: PR description updated (slice, spec bullet, record). README and CODE.md unaffected beyond commit 1.
5. Trust surface: TLC green: cead.cfg 315,202 states in 24 s; tree.cfg 769,040 in 44 s. Six mutations, all caught (listed in the description).
   • Not re-run: Specify cead as a system in TLA+ #11's 26 mutations. The ones touching Exit, Timeout and ReapChild changed their target.
6. How it breaks: Snapshot now needs no process blocked, so no snapshot can be taken while any agent runs in the foreground. That is correct for "between calls", but the snapshot PR may find it too strict for tree-shaped jobs.
7. Not confident:
   • Whether a harness-level timeout, as distinct from the root's wall-time limit, will ever need its own reason.
   • The second clause of property 18 is only exercised by tree.cfg.
8. Verify yourself:
   • Witness.
   • Timeout → Reap.
   • BlockedWaits in spec/cead.tla.
9. Next steps: additional commits. Re-run Specify cead as a system in TLA+ #11's mutations on the changed actions; install elan; Lean specs; skeleton.

[1zeroone0]

7430236: Specify the record encoding in Lean: canonical, so a signature names one record

1. Built: a lake project in spec/, pinned to Lean 4.34.1.
   • Cead/Codec.lean: self-delimiting codecs with two laws. dec_enc means decoding an encoding gives the value back. enc_dec means whatever decodes was an encoding. Combinators unit, tag, u64 (big-endian), blob (u64 length plus bytes), pair, tagged (a tag byte picks the variant) and iso each prove both laws once.
   • Cead/Record.lean: the real record, built from the combinators, so its laws come by construction. It proves Record.dec_enc, Record.enc_dec (canonical) and Record.enc_injective.
   • Cead/Oracle.lean: the oracle record N SEED executable prints random valid and corrupted encodings, each with Lean's verdict.
2. Why:
   • The signature is only as sound as the encoding: a non-canonical encoding lets two byte strings claim one record. Self-delimiting codecs make canonicality compositional, so there's no per-type proof.
   • The record type makes invalid states unrepresentable:
     • only a call event carries an id
     • only finish carries a reply digest
     • only a fork or recovery names a snapshot
     • boot is the boot's public key, so a signature checks without the log
   • The bridge to Rust is bytes, not JSON: the interface itself, and Lean needs no parser.
   • Rejected: bv_decide for the u64 round trip. It proved in 1s, but it rests on native-code axioms, i.e. trusting Lean's compiler. Plain omega arithmetic is kernel-checked.
3. Bloat: none removed. New code only, and each codec proof exists once.
4. Drift: .gitignore ignores spec/.lake/. CODE.md's Lean section already names this layout.
5. Trust surface:
   • Proved: the three theorems, depending only on propext and Quot.sound. No sorry, no Classical.choice, no native code.
   • Not proved: that the Rust matches. That is the differential test, which lands with the Rust fill.
   • The oracle's 2,000-line sample: 795 valid, 1,197 rejected, 8 empty inputs. The Rust side must split each line on the space, not on whitespace, since an input can be empty.
6. How it breaks:
   • A field the fill discovers it needs (a timestamp, a duration) changes the record type and reruns the proofs. They're compositional, so that should be cheap.
   • Blob carries a length-bound proof, faithful to Vec<u8> on a 64-bit machine.
7. Not confident:
   • Witness content: Ended (exited or signaled) plus the whole output's digest. Is a byte count or a duration needed for the measurements?
   • Nested tags for enums versus one tag byte per variant: the same bytes either way here, since each type uses one tagged.
8. Verify yourself: the record type in Cead/Record.lean (lines 1–70): are these the nouns you want signed?
9. Next steps: additional commits. Log acceptance, then Bounded and window assembly, then the skeleton.

[1zeroone0]

a125521: Prove the log's acceptance for every log size

1. Built: Cead/Log.lean. accept log r keeps r iff three things hold:

   • its place in the chain is new (first-wins);
   • it links by hash to any neighbour already in the log;
   • Admits holds, the per-kind rule:
     • a report opens its chain (seq 1, empty prev); a fork or recovery names a logged record; a recovery only while its boot has neither an exit record nor another recovery;
     • any other record comes after seq 1, its boot is vouched, and its boot has no recovery (fencing).

   Valid bundles eight invariants: opens, firstWins, vouched, rooted, fenced, recoveredOnce, oneOutcome, linked. accept_valid shows accept preserves them, and accepted_valid covers every log built from empty. accept_grows: a kept record is appended.

2. Why:

   • TLC proves Arrive at 2 boots; this proves it for any log.
   • Signature and evidence checks stay at the crypto boundary, before accept. Because boot is the public key, they need no log.
   • hash is a parameter the proofs assume nothing about; collision resistance is what makes linked meaningful.
   • Rejected: nested ifs in accept. One Admits Prop made the proofs a single case split.

3. Bloat: mutation found seq ≠ 1 for non-reports redundant, and it admitted seq 0. Replaced with 1 < seq, and the new opens property makes both chain-head guards earn their place.

4. Drift: none. The TLA+ Arrive comment and this doc comment say the same thing. Keeping them aligned is review's job; nothing machine-checks it.

5. Trust surface:

   • Proved: accepted_valid and accept_grows, depending on propext and Quot.sound only.
   • Mutations: each of the 11 guards replaced by True breaks a proof. Replacing with True keeps the proof's structure intact, so each break shows the proof uses that fact. A broken proof is still not a counterexample.
   • Not covered: that the Lean accept matches TLA+'s Arrive, and that the Rust log matches Lean (the differential test, pending the hash question below).

6. How it breaks:

   • Log is a list, so every query is linear. That's fine for the spec; the Rust uses maps and the differential test ties the two.
   • linked only checks neighbours present at arrival. Gaps are allowed, which is correct: a boot with a gap is unknown, not invalid.

7. Not confident:

   • Whether the hash chain earns its place at all while every record is signed (question in the thread).
   • The oracle for accept needs a concrete hash, and Lean core has no SHA-256.

8. Verify yourself:

   • Admits and Origin.Admits against TLA+ Arrive.
   • The Valid fields against properties 2, 6, 8, 11, 12 and 13.

9. Next steps: blocked on the hash-chain decision for accept's oracle. Bounded and window decisions pending.

[1zeroone0]

e2a11de: Name each call's process in its records, so the log holds the process tree

1. Built:

   • Record gains proc (the process that made the call) and child (the process a decision spawned). Rec takes the process.
   • Decide builds one decision record D(q) per branch, so an agent spawn names its child.
   • executed entries record which process ran each command, the ground truth.
   • Property 19, ProcessTree: every logged call names the process that ran it, and a non-root process was spawned by a decision its parent made, earlier in its boot's records or those of the snapshot it booted from (Before).

2. Why: Q25. With a tree, the log must say who did what under whose meter. A first draft checked only the spawn chain, so a record misattributed to the root passed. Adding the ground truth to executed closes that gap.

   • Rejected: naming the child in the witness. A foreground agent's witness comes after the child's own calls, so the tree couldn't be checked from what the log holds at each point.

3. Bloat: Decide's decision record is built once as D(q), where there were two inline copies.

4. Drift:

   • Run one job end to end as a recursive language model #13's description is rewritten for Q24: the "agent and meters" Horizon comment is merged in and deleted.
   • Q21 (drop the hash chain), Q22 (all or nothing past the bound), Q23 (end with limit) and the open task question are written into the description.
   • Horizon comments pointing at "agent and meters" or "the loop" now point at Run one job end to end as a recursive language model #13.

5. Trust surface: TLC green, and the state counts didn't change (cead.cfg 315,202; tree.cfg 769,040), since the new fields are functions of existing state. Four mutations, all caught by ProcessTree on tree.cfg:

   • a spawning decision without its child
   • intent, decision or witness naming the root instead of the process that ran it

   Not covered: forks. tree.cfg has one boot, so Before's recursion into a snapshot's boot is never exercised.

6. How it breaks: Before picks a boot's report with CHOOSE among sent reports. Only one exists per boot under KeySecret, but a forged copy (key "path") is filtered out by hand; if that filter were wrong, CHOOSE could pick the forgery.

7. Not confident: Before is a helper operator, not a noun; it's named for plain reading under the OSTEP/ocap rule for terms.

8. Verify yourself: ProcessTree and Before at the end of spec/cead.tla; Decide's D(q).

9. Next steps: additional commits.

   • Q21 in Lean and docs, with the Lean renames (Decision, WaitStatus, Attestation).
   • Re-run Specify cead as a system in TLA+ #11's mutations.
   • The task round.
   • Lean for window assembly and meter charging.
   • The skeleton.

[1zeroone0]

Drop the hash chain: a signature already fixes each record's author and place

1. Built: prev removed from the Lean Record. Links, linked and the hash parameter removed from Log. opens now reads: a report at seq 1, everything else after. Call records carry proc. Decision = deny | allow | spawn child, so an agent decision names its child (mirrors ProcessTree, e2a11de). Renames under the OSTEP/ocap rule: Verdict → Decision (the vocabulary's noun), Ended → WaitStatus (wait(2)), Evidence → Attestation. The oracle generates the new shapes.
2. Why: Q21. Under KeySecret a record's signature already fixes who wrote it and its place; prev added a hash per record and a check, but no guarantee. spawn makes "allow with a child" a variant, not an optional field that a deny could carry.
3. Bloat: removed Links, linked, the neighbour cases of accept_valid, and the hash threaded through every theorem. Log.lean is 254 → ~225 lines, with one fewer guard.
4. Drift: CODE.md boot and integrity rows: records are numbered and each signed, no hash chain. TLA+ comments: "place in the boot's sequence". The description already carries Q21.
5. Trust surface: Record.enc_dec, dec_enc, enc_injective and accepted_valid depend on propext and Quot.sound only; accept_grows on propext only. Nine guard mutations, each breaking a proof. The oracle's 3,000-line sample has 1,271 valid encodings and 1,715 rejected.
6. How it breaks: with no chain, a verifier checks every record's signature, which the per-call measurement will price. If a compromised key ever becomes a threat, the answer is tlog-tiles over the whole log, not a per-boot chain.
7. Not confident:
   • Blob and Codec are proof-internal names with no OSTEP/ocap source; they never become Rust nouns (Rust uses Vec<u8> and plain functions).
   • proc : UInt64 as the process's number within its boot: is that the PID in its namespace, or the harness's own slot number? The skeleton decides; the record carries whichever.
8. Verify yourself: Decision and Body.call in spec/Cead/Record.lean; Admits in spec/Cead/Log.lean.
9. Next steps: additional commits. Re-run Specify cead as a system in TLA+ #11's mutations, then the task round.

[1zeroone0]

9aa3245: Make every window replayable from the log, and prove no tree outspends its root

1. Built:
   • Q29, records carry every byte a window holds. The report gains prompt and query. intent = the model's whole turn plus the command taken from it. Decision.deny carries what the call returned, and spawn the child's query. The witness adds returned beside the whole output's digest. The TLA+ comment says so; the abstraction is unchanged.
   • Cead/Window.lean: a window is a list of Spans: the pinned prompt, the query, then each call's turn and what it returned. replay log boot proc rebuilds any process's window from the log. window_prefix: each call's window begins with the previous one's.
   • Cead/Meter.lean: a tree of processes (a child's number is greater than its parent's). charge takes one unit from every meter up to the root, or refuses; spawn appends a child. Balanced: for every process, meter + calls in its subtree = cap. reachable_within_meter: in every tree a job can build, no subtree spends more than its root's cap. That's TLA+ property 15 for every size.
   • Cead/Differential.lean (was Oracle.lean) gains two modes: meter (random spawns and charges with verdicts) and replay (a log of hex records → a process's spans).
2. Why:
   • Q29 and your added intent: the mainline reconstructs from the log, and a second path (the gateway's request records) checks it independently.
   • Carrying both the turn and the command lets anyone re-run the extraction.
   • The equality invariant is stronger than TLA+'s inequality, and proves more easily.
3. Bloat: none removed. bump is one helper, used by charge and its proof alike.
4. Drift:
   • "Oracle" renamed to CODE.md's differential test.
   • Window elements are Spans (CODE.md evict: "window span"), not "messages" (consolidated in Specify cead as a system in TLA+ #11).
   • Fields are named returned, per CODE.md call: "text and exit code out".
5. Trust surface:
   • Proved: reachable_within_meter (propext, Classical.choice, Quot.sound) and window_prefix.
   • Five meter mutations, each breaking the proof:
     • no chargeable check
     • charging only the caller
     • not counting calls
     • a new child with calls
     • a new child with meter above cap
   • replay was checked by hand on an 8-record log, with records out of order, a spawn and a deny. The root's and the child's windows came out right, and an unknown process gets none.
   • Not proved: that replay is correct beyond its definition. Its value is as the executable reference the harness's assembly and the gateway's records are compared against, end to end.
6. How it breaks:
   • replay is one boot only. A forked boot's children were spawned in the snapshot's boot; replay would need Before's ancestry.
   • Records now grow by the returned text, bounded by the output bound, and the model's turn, which is unbounded unless the window limit caps it.
7. Not confident:
   • The root being process 0 is a convention stated only in Window.lean; the skeleton must make it the harness's.
   • Whether the model's turn needs its own bound in a record.
8. Verify yourself:
   • Event and Decision in Record.lean.
   • Balanced and bump in Meter.lean.
   • replay in Window.lean.
9. Next steps: additional commits. The skeleton. The 3-process receipt run is still going (16.6M distinct states, no violation).

[1zeroone0]

a06b1f7: Skeleton: one type per noun, one signature per action, every body todo!()

1. Built: one crate, one binary (Q31), one file per stack: record.rs (both sides), host.rs (job, log, vmm, gateway), machine.rs (init, harness, process, meter, window, bounded, shell, engine, agent). 48 todo!()s; cargo check has 0 errors. No dependencies: the skeleton names our nouns only.

   The tie to spec/cead.tla, which nothing machine-checks:

   Spec	Rust
   machine	vmm::Machine<Booting | Up>, a typestate; dropping it evicts
   ps	harness::Harness.procs: Vec<Process>; cap/meter in meter::Meters
   Proc.state	process::State = Ready | Running | Blocked(_) | Zombie(Status) | Reaped
   waits, intent, unwitnessed	process::Blocked = Deciding{call, seq, turn, command} | Running{call, turn} | Waiting{call, turn, child}, so property 18 holds by construction
   status, by, reply	process::Status = Finish(reply) | Meter | Limit | Timeout | Killed{by}
   ids, seq	Harness.next_call, Signer.next (numbered by construction, so no gaps)
   pending	Init::boot waits for the report's ack; Harness::reap, then init waits for the exit record's
   log, Arrive	log::Log::accept(Verified); Refused names each Admits case
   Boot, Start, Leave, Evict	Machine::boot, start, leave, evict
   Dispatch Issue Decide Witness Finish Exhaust Timeout ReapChild Reap	Harness::dispatch … reap, one each
   Deliver	the vsock loop inside job::run
   Snapshot, BootFrom, Forge	absent: out of this PR's slice (fork), or the adversary

   The tie to Lean: record::Record::{encode, decode} ↔ Record.lean; log::Log::accept ↔ accept; meter::Meters::{root, spawn, charge} ↔ Meter.lean; window::{Window, replay} ↔ Window.lean.

2. Why:

   • Process state is an enum in a table (Q30): the table holds every state at once.
   • accept takes Verified, so no unverified record reaches the log's logic.
   • Key lives only in init, and the harness is exec'd, so no copy of the key's memory reaches it.
   • Blocked carries each variant's data, which makes property 18 a type.
   • Bounded is Fits | Spilled (Q22): nothing is truncated.

3. Bloat: nothing to remove; main.rs was empty.

4. Drift: CODE.md homes and the bounded, init and cead rows are owed. That's the next commit, kept out of this one so it reads as the skeleton alone.

5. Trust surface: only the type gate. The skeleton claims shapes, not behaviour.

6. How it breaks:

   • Harness::run is one blocking cycle, but processes run concurrently (&, wait). The fill will need an event loop over the processes' commands and the engine. Its signature may move, and if so the fill commit will say why.
   • dispatch returns a Turn synchronously, which hides the model's processors (Processors in the spec).

7. Verify yourself:

   • process::Blocked and Status in src/machine.rs.
   • log::Refused against Admits.
   • init::Init::serve's doc, the key custody.

8. Not confident:

   • Some type names have no OSTEP or ocap source: Signer, Verified/Forged, Refused, Turn, Gateway, Spent, Ran. Amplification is ocap's; Blocked is OSTEP's.
   • Limits sits in host::job but is used by the machine: it crosses the boundary through the kernel command line.

9. Next steps: additional commits. Home the nouns in CODE.md, then fill in order: plain types (record), leaves (meter, window, bounded), then orchestration.

[1zeroone0]

07d6ca1: Give every noun its home in code, and write down the method as practiced here

1. Built:
   • Vocabulary is one table: noun, meaning, where it lives in code. Every type in src/ has a row; a type's errors and states sit in its row. New rows: agent, amplification, attestation, blocked, gateway, key, shell, signer, span, turn, verified, view, wait status.
   • Rewritten rows:
     • bounded: all or nothing, per Q22
     • cead: one binary, roles, per Q31
     • init: forks and execs the harness
     • log, record, report, window: replay, per Q29
     • model: holds no credential
   • Method:
     • step 0, Scope
     • Spec is never looser than the system (Q18)
     • Skeleton: shape agreed first; its comment carries the spec-to-code table
     • TLA+: one cfg per mutation
     • Lean: axioms, guard mutations, differential
2. Why: your ask, one table for vocabulary, meaning and types; and the playbook, so the next PR doesn't re-derive it.
3. Bloat: "crate and binary" collapsed into one binary; the "job-scoped token" clause dropped from model (the gateway holds credentials; the machine holds none).
4. Drift: checked by script: every struct/enum in src/ appears in the table.
5. Trust surface: prose. The type-to-row check is a one-off script, not in CI.
6. How it breaks: a type added in fill without a row. The same script catches it; I'll run it before ready.
7. Not confident: model lost "job-scoped token". That was Specify cead as a system in TLA+ #11's design for our own engine, and it's still true there. Restore it if you want it kept for later.
8. Verify yourself: the Method steps 0, 1 and 4; the rows for gateway, turn and verified.
9. Next steps: additional commits. Fill record.

[1zeroone0]

f5b34de: Fill record: the Lean codec byte for byte, held to it by the differential test

1. Built: Record::encode/decode implement spec/Cead/Record.lean's codec: a tag byte per variant, u64 big-endian, bytes as length plus data, keys and digests as their 32 bytes. decode refuses trailing bytes. Test codec_matches_lean runs lake build differential, then 5,000 Lean-generated inputs: every encoding Lean accepts, Rust decodes and re-encodes identically; every one Lean rejects, Rust rejects.
2. Why: fill order, plain types first. The spec moved: the skeleton typed keys and digests as [u8; 32], but Lean encoded them as variable-length blobs, so the two could never agree. Keeping the invariant in the type is the rule, so Lean gained Fixed n (its own codec with both laws proved), and Boot and Digest are Fixed 32 in the spec too.
3. Bloat: one Reader, and two writers (put_u64, put_bytes) shared by every type.
4. Drift: Log.lean and Window.lean now take Boot, not Blob. The vocabulary rows already say "key" and "digest".
5. Trust surface:
   • Proved: the Lean laws, still on propext and Quot.sound.
   • Tested: Rust equals Lean on 5,000 random inputs, about half valid encodings and half corruptions (a byte changed, cut short, extended).
   • Mutations: a wrong tag for Exit::Limit, and accepting trailing bytes. Both fail the test.
   • Not covered: lengths past what the generator makes (blobs ≤ 40 bytes; u64 values at both ends of the range).
6. How it breaks:
   • cargo test needs lake on PATH. It fails loudly if missing; it doesn't skip.
   • A blob longer than usize on a 32-bit host is refused as malformed, which is correct but untested.
7. Not confident: put_bytes uses len() as u64: lossless on 64-bit, the only target.
8. Verify yourself:
   • Record::decode's trailing-bytes check.
   • The fixed codec in spec/Cead/Codec.lean.
9. Next steps: additional commits. The leaves: meter, window, bounded.

[1zeroone0]

b3a35d6: Fill meter: the Lean definitions, held to them by the differential test

1. Built: Meters::{root, spawn, charge} and a private chain, each the definition in spec/Cead/Meter.lean. Test meters_match_lean replays 300 Lean runs of 40 random spawns and charges. After every operation, Rust's verdict and every meter must equal Lean's.
2. Why: fill order, leaves after plain types. ProcId gained ROOT, new and get; the record's fields stay private.
3. Bloat: chain is the one walk up the tree, used by the check and by the charge alike.
4. Drift: none.
5. Trust surface: Lean proves no subtree outspends its root, for every reachable tree. The test ties Rust to that definition on about 12,000 operations; the run asserts over 1,000 each of ok and refused. Mutation: charging only the caller fails the test.
6. How it breaks: chain walks parent links. The p < at filter mirrors Lean's termination guard, and spawn makes it hold by construction.
7. Not confident: Metered.cap is unread in Rust. It's kept because the invariant (meter + subtree calls = cap) is stated over it, and a stats readout will want it.
8. Verify yourself: Meters::charge.
9. Next steps: additional commits, window.

[1zeroone0]

c0252ab: Fill window: it only grows, and the log replays it as Lean does

1. Built: Window::{open, push, spans} and replay, definition for definition from spec/Cead/Window.lean. push refuses a call that would pass the limit and leaves the window as it was (Q23: the process then ends with limit). Record, Boot, CallId and Digest gained constructors and accessors. Tests:
   • window_grows_until_full: a push only appends; a refused push changes nothing.
   • replay_matches_lean: 200 random logs over 2 boots, 3 processes and 4 call ids (reports, spawns, intents, denies, witnesses, in any order). For every process, Rust's replay equals Lean's, and both refuse the same ones.
2. Why: replaying from the log is Q29's forensics path. The random logs include duplicates and out-of-order records on purpose, since replay must agree with Lean on any log, well-formed or not.
3. Bloat: differential() now builds Lean once per test run (OnceLock): 82 s → 1.6 s for all tests.
4. Drift: none.
5. Trust surface: Lean proves prefix-stability; the test ties Rust to the replay definition. Mutations, each failing the test: not sorting call ids; swapping the root's query for a child's.
   • Not covered: that the harness pushes what it logs. That's the end-to-end test: the harness's windows against the replay and against the gateway's record.
6. How it breaks: replay is linear scans per call, so quadratic in a boot's records. Fine for a job; a stats pass over many boots may want an index.
7. Not confident: the limit counts bytes. Bedrock's window counts tokens, so bytes is a proxy until the fill decides how the harness counts.
8. Verify yourself: replay against spec/Cead/Window.lean's replay.
9. Next steps: additional commits, bounded.

[1zeroone0]

093e0f5: Fill bounded: a call returns its output whole or not at all

1. Built: Bounded::admit: Fits when the output is within the bound; otherwise the output goes to the spill file and the result is Spilled { path, size }. returned:

   • when it fits: the output, a newline if one is missing, then exit N or signal N;
   • when it spilled: exit N · SIZE bytes → PATH.

   Test all_or_nothing covers the boundary (at the bound fits; one byte over spills and the file holds every byte), both status kinds, and empty output.

2. Why: Q22 and the RLM reading. The model never sees a cut it didn't choose, and the spill line has the same shape on every task.

3. Bloat: none.

4. Drift: none; the bounded row already says this.

5. Trust surface: the unit test is the whole claim. It's no Lean spec: the scalpel didn't pick it once truncation was gone.

6. How it breaks: admit does I/O (the spill write), the one leaf that does. A failed write fails the call; the harness must witness that as the call's end.

7. Not confident:

   • The exact text the model reads (exit 0, ·, →) is model-facing, and the prompt PR may want it in the man text.
   • The status line comes after the output rather than before it.

8. Verify yourself: Bounded::returned.

9. Next steps: orchestration, which needs dependencies (asked in the thread).

[1zeroone0]

f8a7d37: Fill log: keep and refuse as Lean's accept does, and verify signatures

1. Built:
   • Verified::verify: decode, refuse SNP reports (unverifiable until the confidential machine PR), strict Ed25519 check against the boot's key.
   • Log::accept: Admits from spec/Cead/Log.lean case by case, each refusal named in Refused, plus Unwritten for an I/O failure, where nothing is kept or acknowledged.
   • The log file: one per boot, a line per record, encoding and signature in hex.
   • Ed25519 lives only in record (sign, Boot::of, Boot::verifies), per CODE.md's boundary rule. init::Key is filled: 32 bytes from /dev/urandom, zeroed on drop.
   • Lean's differential gains log RUNS LEN SEED: random records aimed at the rules (three boots, low places, every kind), offered to accept from empty.
2. Why:
   • Two signatures moved. Mode is gone: attested mode can't check an SNP report yet, so rather than a variant that refuses everything, this build is trusted-host only and says so. And accept can fail to write.
   • The log format moved from JSON lines to hex lines (Q32). It's the same format Lean's replay reads.
3. Bloat: serde stays out of the log path. anyhow is dropped, and so is the clap preference in CODE.md: three roles don't need a parser.
4. Drift: CODE.md's log and verified rows and its dependency line; the PR description's log and dependency bullets.
5. Trust surface:
   • accept_matches_lean: 300 runs of 30 offers; Rust keeps and refuses exactly as Lean (about 2,000 kept, 7,000 refused). Mutations, each failing the test: no fence, no settled check, no rooted check, no vouching, no first-wins.
   • verify_refuses_forgeries: another boot's signature, a flipped byte, and an SNP report are all refused.
   • Not covered: Unwritten (disk full), and concurrent writers. There's one writer per boot by design.
6. How it breaks: state is in memory; restarting the host process loses seqs. The files are the truth, and a restart must replay them. Not built.
7. Not confident: /dev/urandom at early boot needs the VM's virtio-rng. To check on the Surface.
8. Verify yourself: Log::accept beside Admits; Verified::verify.
9. Next steps: additional commits.

(I amended this commit and force-pushed once, before anything referenced it. From now on I only add commits.)

[1zeroone0]

fe8a4ab: Spill output that is not text, so the window holds exactly what the log replays

1. Built: Bounded::admit admits output only if it fits and is UTF-8; otherwise it spills.
2. Why: Converse carries text only. Converting lossily would make what the model saw differ from what the log replays (Q29), so binary output becomes state the model reads with xxd or the like.
3. Bloat: none.
4. Drift: CODE.md's bounded row.
5. Trust surface: all_or_nothing adds a two-byte non-UTF-8 case, which spills.
6. How it breaks: output that's mostly text with one bad byte spills whole. That's measurable as the spill follow-up rate.
7. Not confident: whether the model needs a hint in the spill line that the file isn't text.
8. Verify yourself: Bounded::admit.
9. Next steps: additional commits.

[1zeroone0]

aab9953: Fill the gateway and the wire: frames, spans, and Converse through curl

1. Built:
   • record::{write_frame, read_frame}: u64 length plus bytes, capped at 64 MiB, since the host is untrusted.
   • window::{encode, decode}: spans on the wire, reusing the record codec's Reader.
   • gateway::Gateway::relay: decode spans, build the Converse body (the system span becomes the system prompt, the rest alternating messages), POST with curl, extract the turn and tokens, and record window turn inputTokens outputTokens per line.
   • The Bedrock API key goes in curl's config on stdin, never argv.
2. Why: Q32. Bedrock API keys authenticate Converse (verified in AWS's docs), so no SigV4 crate is needed, and curl needs no HTTP crate. The tokens are recorded because cost per question is a merge requirement.
3. Bloat: one reader shared by the record and span codecs.
4. Drift: CODE.md's gateway, span and record rows.
5. Trust surface:
   • Tested: frames round-trip, and the size cap refuses before allocating. The request and response shapes, and the config quoting.
   • Not verified: curl actually parsing that config (a local test server was denied here), and a real Bedrock call: the model ID for Sonnet 5.5, and whether Converse serves it. Both go to the host session.
6. How it breaks:
   • A curl process per inference, measured as harness time per call.
   • answer treats missing usage fields as 0.
7. Not confident:
   • Claude's docs split "Claude on Bedrock" (legacy) from "Claude in Amazon Bedrock" (Opus 4.7 and later). Newer models may be meant for a different API than Converse. To check first thing on the host.
   • No maxTokens is set, so Bedrock's default applies.
8. Verify yourself: curl_config and Gateway::send.
9. Next steps: additional commits.

[1zeroone0]

0bb9318 and 09aa4dc: Fill the signer, rights and roles; move test modules to the end

1. Built:
   • Signer: numbers from 2 (init sent the report at 1), writes each record as a frame to init, and waits for an acknowledgment of its place, in any order. Its one pipe became two (to_init, from_init).
   • Rights::attenuate: every granted path must lie under the parent's grant for the same right.
   • Role::parse: agent by the name it runs as; run QUERY, init and harness by subcommand.
   • 09aa4dc only moves test modules, per clippy's items_after_test_module.
2. Why: the host-independent pieces of orchestration, done before the Surface is up.
3. Bloat: none.
4. Drift: none.
5. Trust surface:
   • numbers_and_waits: over real pipes, records arrive numbered 2 and 3, and acknowledgments are honoured out of order.
   • attenuates_never_amplifies: /workshop isn't under /work, since Path::starts_with compares components, not strings.
   • roles.
6. How it breaks: acknowledged blocks forever if init never answers. That's init's death, which ends the boot anyway.
7. Not confident: Rights compares paths lexically. Symlinks and .. are Landlock's job at enforcement, not this check's.
8. Verify yourself: Signer::acknowledged.
9. Next steps: blocked on the host and three design questions (in the handoff). 29 placeholders left.

[1zeroone0]

2def4b3: Say what the three artifacts are for: a conversation that shows what cannot be stabilized

1. Built: one paragraph at the top of CODE.md's Method. TLA+, Lean and Rust argue; none is the source. Each stabilizes what it can, so what can't be stabilized shows (lossy translation, model-facing text, artifacts that agree only with themselves). Surfacing those to Roone is the work; a pipeline that runs without him is not the goal.
2. Why: a misreading this session, treating the method as a road to automation, was behind the momentum errors. Stated here, the next agent asks where it would otherwise assume.
3. Bloat: none.
4. Drift: also opened Horizon Horizon #7's "post-training: an open model trained on cead's logs" comment; the handoff's reading list already includes CODE.md's Method.
5. Trust surface: prose.
6. How it breaks: an agent reading only the numbered steps skips it. It sits above them for that reason.
7. Not confident: whether it also belongs in the /scope skill. Its question rounds are where the asking happens.
8. Verify yourself: the paragraph.
9. Next steps: none this session; the handoff takes over.