From e7a7de43b519cc81c0c47e43984c52ca97337a6c Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 10:08:40 -0600 Subject: [PATCH 01/19] Witness a call when its command ends, and sign the answer An exit record could close a boot as complete while an executed command had no witness yet; the reply left the machine unsigned. TLC 2.19: cead.cfg 473,888 distinct states, 36 s; tree.cfg 2,185,268, 2m18s. Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 8 ++-- README.md | 6 +-- spec/cead.cfg | 1 + spec/cead.tla | 111 ++++++++++++++++++++++++++++++++------------------ spec/tree.cfg | 1 + 5 files changed, 80 insertions(+), 47 deletions(-) diff --git a/CODE.md b/CODE.md index e07056e..6c0ade1 100644 --- a/CODE.md +++ b/CODE.md @@ -8,7 +8,7 @@ Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TL 1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable. 2. **Slice.** A PR takes a slice of the spec. Its dependencies are probed while scoping; findings go in a PR comment, the probe is never committed. -3. **Core.** A pure function with a property worth proving gets its Lean spec first, green before any Rust. +3. **Core.** Ask what a skeptic has to trust. Every pure function on that path (what signs, verifies, admits or renders) gets its Lean spec first, green before any Rust, and a differential test; elsewhere, a pure function gets one when a property is stated. 4. **Skeleton.** One commit of types, signatures, private fields and one doc comment per item (what it owns, when it drops); bodies are `todo!()`; the type gate is green. It is the spec of custody. It mirrors the spec: variables become fields, states become variants or typestates, each action becomes one signature. 5. **Fill.** Later commits change bodies. A signature that moves is learning: say why in the commit comment. A new capability is drift: it belongs to another PR. A fill commit names the action it implements. @@ -48,9 +48,9 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | engine | Executes the weights and signs what it produces: the model's counterpart to the machine. vLLM by default. | | | evict | Dispose at any tier: window span, KV block, process, machine. | | | executed | What the kernel ran: the truth the records record. | `spec/cead.tla` | -| harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, writes records. | | +| harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, sequences records for init to sign. | | | host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | | -| init | PID 1 in the machine. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | +| init | PID 1 in the machine, for the whole boot. Makes the boot's key and never lets it go; signs every record. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, forks the harness. If the harness dies, the boot ends with no exit record: unknown. | | | integrity | The log says only what the machine signed, in the machine's order. Guaranteed by each boot's signature and hash chain, rooted in its report. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | | job | One query's work: a root process and its tree. Started by `cead run`. Spans one boot, or more through recovery. | | @@ -67,7 +67,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. A boot sees the model's processors as virtual, like vCPUs; how the engine shares its GPU among them (batching) is its scheduler's. | | | query | The argv of `run` or `agent`, commit-message sized. Anything longer is context. | | | report | A boot's first record: the processor's signed statement binding the boot's key, and for a fork or recovery the snapshot it booted from (that boot and its last record), to the manifest's measurement. Unsigned in trusted-host mode. Linux's TSM report. | `spec/cead.tla` | -| record | One entry the machine signs for the log, Linux audit's unit. Types: report, intent, decision, witness, exit. A call's intent, decision and witness share its id, as Linux audit's records share an event. | `spec/cead.tla` | +| record | One entry the machine signs for the log, Linux audit's unit. Types: report, intent, decision, witness, exit; the exit record carries the root process's reply. A call's intent, decision and witness share its id, as Linux audit's records share an event. | `spec/cead.tla` | | rights | What a call may do to state: read, write. | | | ring | A privilege layer: model processes; harness and tracer; host. | | | scheduler | Decides what runs where: machines on hosts (Kubernetes), requests on engines (Dynamo). Trusted for availability only; needs consensus once there is more than one. | | diff --git a/README.md b/README.md index 2ac215f..414e5b5 100644 --- a/README.md +++ b/README.md @@ -70,10 +70,10 @@ A **manifest** is one file that names a machine: kernel, task image, policy, VMM What a job does, from manifest to first command: 1. The VMM boots the kernel with two read-only disks: the core (built by nix) and the task image. -2. The machine makes its key and sends its report; nothing runs until the log holds it. +2. init makes the boot's key, which never leaves it, and sends the report; nothing runs until the log holds it. 3. init, as root, loads the eBPF programs and compiles the policy into seccomp and Landlock. 4. init mounts the view: the task image as root, the core first on PATH, one descriptor per grant. -5. The harness spawns the root process: policy attached, an unprivileged uid, the shell. +5. init forks the harness, which spawns the root process: policy attached, an unprivileged uid, the shell. Every child inherits the policy; no syscall loosens it, and no model process holds CAP_BPF. 6. The harness sends the engine the query and a system prompt rendered from what it mounted. 7. The model writes its first command. @@ -158,5 +158,5 @@ The machine is the unit of scale. Work fans out three ways: - eBPF records which programs start, which files are read, and each request to the engine. - Keyed by cgroup: each action is traced to the command that caused it, however many processes it spawned. - The log holds each boot's records, in order: - its report; per call an intent, a decision, and a witness if allowed; its exit. + its report; per call an intent, a decision, and a witness if allowed; its exit, carrying the answer. - The console reads it live, during a job and after. diff --git a/spec/cead.cfg b/spec/cead.cfg index 7e085b5..5351483 100644 --- a/spec/cead.cfg +++ b/spec/cead.cfg @@ -8,6 +8,7 @@ CONSTANTS Processors = 1 Procs = {p1} RootProc = p1 + Replies = {y1} Boots = {b1, b2} Root = b1 NoRecord = NoRecord diff --git a/spec/cead.tla b/spec/cead.tla index 0f14130..68bf513 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -35,6 +35,7 @@ CONSTANTS Processors, \* how many of a boot's processes the model can run at once Procs, \* model values: process slots in a boot RootProc, \* the process `cead run` starts + Replies, \* what the model can reply without a command Boots, \* model values: each boot, which is also its key Root, \* the boot `cead run` starts NoRecord \* a model value: no record awaiting acknowledgment @@ -52,7 +53,7 @@ Origins == {"run", "fork", "recovery"} \* what a report says st Signers == Boots \cup {"path", "processor"} \* the processor signs only reports MaxId == Cardinality(Procs) * CallLimit \* every call of every process MaxSeq == 3 * MaxId + 2 \* the report, every call's records, the exit -None == "none" \* no process, or no snapshot +None == "none" \* no process, snapshot or reply Live == {"ready", "running", "blocked"} \* One record of a boot. `seq` is its place in the boot's hash chain: the @@ -60,26 +61,31 @@ Live == {"ready", "running", "blocked"} \* id 0) names its boot, whose key signs the rest, what started it, and for \* a fork or recovery the snapshot it booted from: that boot and its last \* record. A call's intent, decision and witness carry its id and command; -\* the exit record carries id 0 and why the boot ended. +\* the exit record carries id 0, why the boot ended, and the root process's +\* reply if it finished: the answer, signed. Record == [boot : Boots, seq : 1..MaxSeq, id : 0..MaxId, type : CallTypes \cup {"report", "exit"}, body : Commands \cup Reasons \cup Origins, key : Signers, - from : Boots \cup {None}, last : 0..MaxSeq] + from : Boots \cup {None}, last : 0..MaxSeq, reply : Replies \cup {None}] \* One process, as the harness holds it. `cap` is the meter it was given, \* `meter` what remains; `waits` is the child it waits for in the foreground; -\* `status` is why it ended, and `by` the process that killed it. +\* `status` is why it ended, `by` the process that killed it, and `reply` +\* what it replied if it finished. Proc == [state : {"unused", "zombie", "reaped"} \cup Live, parent : Procs \cup {None}, calls : 0..CallLimit, cap : 0..MeterCap, meter : 0..MeterCap, depth : 0..Depth, rights : SUBSET Rights, waits : Procs \cup {None}, - status : Reasons \cup {"killed", None}, by : Procs \cup {None}] + status : Reasons \cup {"killed", None}, by : Procs \cup {None}, + reply : Replies \cup {None}] Unused == [state |-> "unused", parent |-> None, calls |-> 0, cap |-> 0, meter |-> 0, - depth |-> 0, rights |-> {}, waits |-> None, status |-> None, by |-> None] + depth |-> 0, rights |-> {}, waits |-> None, status |-> None, by |-> None, + reply |-> None] Spawned(parent, cap, depth, rights) == [state |-> "ready", parent |-> parent, calls |-> 0, cap |-> cap, meter |-> cap, - depth |-> depth, rights |-> rights, waits |-> None, status |-> None, by |-> None] + depth |-> depth, rights |-> rights, waits |-> None, status |-> None, by |-> None, + reply |-> None] RootTable == [p \in Procs |-> IF p = RootProc THEN Spawned(None, MeterCap, Depth, Rights) ELSE Unused] @@ -91,17 +97,19 @@ VARIABLES seq, \* per boot: the machine's last sequence number pending, \* per boot: the report or exit record awaiting acknowledgment, or NoRecord executed, \* per boot: what the kernel ran, in order: the truth + unwitnessed, \* per boot: calls executed whose witness is not yet sent job, \* per boot: the boot that started its job snapshots, \* every snapshot taken: a boot, its last record, its processes transit, \* every record sent: each can be lost, delayed, reordered, duplicated log \* held outside the machine: a set of records -vars == <> +vars == <> Rec(b, s, i, t, x) == [boot |-> b, seq |-> s, id |-> i, type |-> t, body |-> x, - key |-> b, from |-> None, last |-> 0] + key |-> b, from |-> None, last |-> 0, reply |-> None] Report(b, o, f, l) == [boot |-> b, seq |-> 1, id |-> 0, type |-> "report", body |-> o, - key |-> "processor", from |-> f, last |-> l] + key |-> "processor", from |-> f, last |-> l, reply |-> None] Logged(b, s) == \E r \in log : r.boot = b /\ r.seq = s LoggedType(b, i, t) == \E r \in log : r.boot = b /\ r.id = i /\ r.type = t \* The log holds boot b's report: b's key is vouched for. @@ -148,6 +156,7 @@ Init == /\ seq = [b \in Boots |-> 0] /\ pending = [b \in Boots |-> NoRecord] /\ executed = [b \in Boots |-> <<>>] + /\ unwitnessed = [b \in Boots |-> {}] /\ job = [b \in Boots |-> b] /\ snapshots = {} /\ transit = {} @@ -163,6 +172,7 @@ Begin(b, r, t, i, j) == /\ pending' = [pending EXCEPT ![b] = r] /\ job' = [job EXCEPT ![b] = j] /\ transit' = transit \cup {r} + /\ unwitnessed' = [unwitnessed EXCEPT ![b] = {}] /\ UNCHANGED <> \* `cead run` boots the root. @@ -184,7 +194,7 @@ Start(b) == /\ Logged(b, 1) /\ machine' = [machine EXCEPT ![b] = "up"] /\ pending' = [pending EXCEPT ![b] = NoRecord] - /\ UNCHANGED <> + /\ UNCHANGED <> \* The whole machine at an instant: no call in progress, and the log holds \* every record so far. A process that was running is ready: its inference @@ -192,29 +202,34 @@ Start(b) == Snapshot(b) == /\ machine[b] = "up" /\ \A p \in Procs : intent[b, p] = NoRecord + /\ unwitnessed[b] = {} /\ \A s \in 1..seq[b] : Logged(b, s) /\ snapshots' = snapshots \cup {[boot |-> b, last |-> seq[b], ids |-> ids[b], procs |-> [p \in Procs |-> IF ps[b, p].state = "running" THEN [ps[b, p] EXCEPT !.state = "ready"] ELSE ps[b, p]]]} - /\ UNCHANGED <> + /\ UNCHANGED <> \* The machine signs its exit record, its last record, and waits for the log -\* to acknowledge it. Any call in progress is cut off. -Exit(b, reason) == +\* to acknowledge it. A call awaiting its decision is cut off; every executed +\* call has been witnessed first, so the exit record never hides a gap. +Exit(b, reason, reply) == /\ machine[b] = "up" - /\ LET r == Rec(b, seq[b] + 1, 0, "exit", reason) + /\ unwitnessed[b] = {} + /\ LET r == [Rec(b, seq[b] + 1, 0, "exit", reason) EXCEPT !.reply = reply] IN /\ machine' = [machine EXCEPT ![b] = "exiting"] /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] /\ pending' = [pending EXCEPT ![b] = r] /\ transit' = transit \cup {r} - /\ UNCHANGED <> + /\ UNCHANGED <> -\* The root process has ended: the boot exits with its reason. -Reap(b) == ps[b, RootProc].state = "zombie" /\ Exit(b, ps[b, RootProc].status) -\* The machine's own wall-time limit fires. -Timeout(b) == Exit(b, "timeout") +\* The root process has ended: the boot exits with its reason and reply. +Reap(b) == ps[b, RootProc].state = "zombie" /\ + Exit(b, ps[b, RootProc].status, ps[b, RootProc].reply) +\* The machine's own wall-time limit fires. The harness kills running +\* commands first; each is still witnessed (Witness), then the boot exits. +Timeout(b) == Exit(b, "timeout", None) \* The log has the exit record: the machine is gone. Leave(b) == @@ -222,7 +237,7 @@ Leave(b) == /\ Logged(b, pending[b].seq) /\ machine' = [machine EXCEPT ![b] = "evicted"] /\ pending' = [pending EXCEPT ![b] = NoRecord] - /\ UNCHANGED <> + /\ UNCHANGED <> \* The machine ends without an acknowledged exit record. A crash can happen \* at any point. The host's hard kill is the same event, but it is assumed @@ -231,7 +246,7 @@ Evict(b) == /\ machine[b] \in {"booting", "up", "exiting"} /\ machine' = [machine EXCEPT ![b] = "evicted"] /\ pending' = [pending EXCEPT ![b] = NoRecord] - /\ UNCHANGED <> + /\ UNCHANGED <> Crash(b) == Evict(b) HostKill(b) == Evict(b) @@ -245,7 +260,7 @@ Dispatch(b, p) == /\ ps[b, p].state = "ready" /\ Cardinality(Running(b)) < Processors /\ ps' = [ps EXCEPT ![b, p].state = "running"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* The processor returns a command. Its unit is charged to every meter from \* the process up to the root; the process releases the processor, blocks, @@ -267,11 +282,11 @@ Issue(b, p, c) == /\ ids' = [ids EXCEPT ![b] = ids[b] + 1] /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] /\ transit' = transit \cup {r} - /\ UNCHANGED <> + /\ UNCHANGED <> \* The log has acknowledged the intent: the harness checks the call against -\* policy. Deny returns to the model. Allow runs the command, and the tracer -\* witnesses it; both records go through the harness, which sequences them. +\* policy and sends the decision. Deny returns to the model. Allow starts +\* the command, whose witness is sent when it ends (Witness). \* `agent` spawns a child in the foreground (the caller waits) or the \* background; it fails if the caller's depth is spent or no slot is free. \* `kill` ends one of the caller's live children and its descendants. @@ -289,9 +304,9 @@ Decide(b, p) == Done(t) == [t EXCEPT ![b, p].state = "ready"] IN /\ IF Decision(c) = "allow" THEN /\ executed' = [executed EXCEPT ![b] = Append(@, [id |-> i, cmd |-> c])] - /\ transit' = transit \cup - {Rec(b, s + 1, i, "decision", c), Rec(b, s + 2, i, "witness", c)} - /\ seq' = [seq EXCEPT ![b] = s + 2] + /\ unwitnessed' = [unwitnessed EXCEPT ![b] = @ \cup {[id |-> i, cmd |-> c]}] + /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} + /\ seq' = [seq EXCEPT ![b] = s + 1] /\ IF c = "agent" /\ me.depth > 0 /\ Free # {} THEN \E q \in Free, m \in 1..MeterCap, R \in SUBSET me.rights, fg \in BOOLEAN : @@ -304,6 +319,7 @@ Decide(b, p) == /\ intent' = [CutOff(b, q) EXCEPT ![b, p] = NoRecord] ELSE ps' = Done(ps) ELSE /\ executed' = executed + /\ unwitnessed' = unwitnessed /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} /\ seq' = [seq EXCEPT ![b] = s + 1] /\ ps' = Done(ps) @@ -311,14 +327,26 @@ Decide(b, p) == intent' = [intent EXCEPT ![b, p] = NoRecord] /\ UNCHANGED <> +\* A command ends, however it ends (exit, signal, a kill from its process's +\* ancestor or the harness): the tracer's witness goes through the harness, +\* which sequences it. A process's calls are witnessed whatever becomes of +\* the process. +Witness(b, e) == + /\ machine[b] = "up" + /\ e \in unwitnessed[b] + /\ unwitnessed' = [unwitnessed EXCEPT ![b] = @ \ {e}] + /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] + /\ transit' = transit \cup {Rec(b, seq[b] + 1, e.id, "witness", e.cmd)} + /\ UNCHANGED <> + \* The model replies without a command: the process ends, and its running \* descendants are killed. The reply is its stdout. -Finish(b, p) == +Finish(b, p, y) == /\ machine[b] = "up" /\ ps[b, p].state = "running" - /\ ps' = Ended(b, p, "finish") + /\ ps' = [Ended(b, p, "finish") EXCEPT ![b, p].reply = y] /\ intent' = CutOff(b, p) - /\ UNCHANGED <> + /\ UNCHANGED <> \* The processor returns a command the process cannot pay for, or its call \* limit is reached: it ends, and its descendants are killed. @@ -328,7 +356,7 @@ Exhaust(b, p) == /\ \/ ~Chargeable(b, p) /\ ps' = Ended(b, p, "meter") \/ ps[b, p].calls = CallLimit /\ ps' = Ended(b, p, "limit") /\ intent' = CutOff(b, p) - /\ UNCHANGED <> + /\ UNCHANGED <> \* The harness reaps an ended child; a parent waiting on it in the \* foreground is ready again. @@ -341,7 +369,7 @@ ReapChild(b, q) == IN ps' = IF ps[b, p].waits = q /\ ps[b, p].state = "blocked" THEN [t EXCEPT ![b, p].state = "ready", ![b, p].waits = None] ELSE t - /\ UNCHANGED <> + /\ UNCHANGED <> ----------------------------------------------------------------------------- (* Records in transit: outside the machine, so they go on after eviction *) @@ -366,7 +394,7 @@ Arrive(r) == /\ ~Recovered(r.boot) /\ ~Logged(r.boot, r.seq) /\ log' = log \cup {r} - /\ UNCHANGED <> + /\ UNCHANGED <> Deliver(r) == r \in transit /\ Arrive(r) @@ -385,9 +413,10 @@ Next == \/ Start(b) \/ Snapshot(b) \/ Reap(b) \/ Timeout(b) \/ Leave(b) \/ Crash(b) \/ HostKill(b) \/ \E p \in Procs : - \/ Dispatch(b, p) \/ Decide(b, p) \/ Finish(b, p) \/ Exhaust(b, p) - \/ ReapChild(b, p) + \/ Dispatch(b, p) \/ Decide(b, p) \/ Exhaust(b, p) \/ ReapChild(b, p) \/ \E c \in Commands : Issue(b, p, c) + \/ \E y \in Replies : Finish(b, p, y) + \/ \E e \in unwitnessed[b] : Witness(b, e) \/ \E r \in transit : Deliver(r) \/ Forge(r) Spec == Init /\ [][Next]_vars /\ \A b \in Boots : WF_vars(HostKill(b)) @@ -403,6 +432,7 @@ TypeOK == /\ seq \in [Boots -> 0..MaxSeq] /\ pending \in [Boots -> Record \cup {NoRecord}] /\ \A b \in Boots : executed[b] \in Seq([id : 1..MaxId, cmd : Commands]) + /\ unwitnessed \in [Boots -> SUBSET [id : 1..MaxId, cmd : Commands]] /\ job \in [Boots -> Boots] /\ transit \subseteq Record /\ log \subseteq Record @@ -439,11 +469,12 @@ Unambiguous == LET Seen == {r \in transit : r.key # "path"} \cup log IN \A r1, r2 \in Seen : (r1.boot = r2.boot /\ r1.seq = r2.seq) => r1 = r2 -\* 9. An exit record saying `finish` means the root process ended its turn: -\* it was not cut off. +\* 9. An exit record saying `finish` means the root process ended its turn, +\* was not cut off, and replied what the record says. FinishHonest == \A r \in log : (r.type = "exit" /\ r.body = "finish") => - ps[r.boot, RootProc].status = "finish" + /\ ps[r.boot, RootProc].status = "finish" + /\ r.reply = ps[r.boot, RootProc].reply \* 10. A boot is complete when the log holds its exit record with no gap \* before it: then every call it executed has all three records logged. diff --git a/spec/tree.cfg b/spec/tree.cfg index 57f65df..4343c07 100644 --- a/spec/tree.cfg +++ b/spec/tree.cfg @@ -8,6 +8,7 @@ CONSTANTS Processors = 1 Procs = {p1, p2} RootProc = p1 + Replies = {y1} Boots = {b1} Root = b1 NoRecord = NoRecord From 8ea6b3b662bd482fb2d0e02f2fd8f84f5f1703ba Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 10:19:43 -0600 Subject: [PATCH 02/19] Block a process until its command ends, as the harness does Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/cead.cfg | 1 + spec/cead.tla | 76 +++++++++++++++++++++++++++++++-------------------- spec/tree.cfg | 1 + 3 files changed, 48 insertions(+), 30 deletions(-) diff --git a/spec/cead.cfg b/spec/cead.cfg index 5351483..47cef0a 100644 --- a/spec/cead.cfg +++ b/spec/cead.cfg @@ -31,6 +31,7 @@ INVARIANTS WithinMeter Attenuated KillReach + BlockedWaits PROPERTIES LogOnlyGrows diff --git a/spec/cead.tla b/spec/cead.tla index 68bf513..b8eb264 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -97,7 +97,7 @@ VARIABLES seq, \* per boot: the machine's last sequence number pending, \* per boot: the report or exit record awaiting acknowledgment, or NoRecord executed, \* per boot: what the kernel ran, in order: the truth - unwitnessed, \* per boot: calls executed whose witness is not yet sent + unwitnessed, \* per boot: calls executed whose command has not yet ended job, \* per boot: the boot that started its job snapshots, \* every snapshot taken: a boot, its last record, its processes transit, \* every record sent: each can be lost, delayed, reordered, duplicated @@ -211,25 +211,30 @@ Snapshot(b) == ELSE ps[b, p]]]} /\ UNCHANGED <> -\* The machine signs its exit record, its last record, and waits for the log -\* to acknowledge it. A call awaiting its decision is cut off; every executed -\* call has been witnessed first, so the exit record never hides a gap. -Exit(b, reason, reply) == +\* The root process has ended and every command has ended and been +\* witnessed: the machine signs its exit record, its last record, with the +\* root's reason and reply, and waits for the log to acknowledge it. The exit +\* record never hides a gap. +Reap(b) == /\ machine[b] = "up" + /\ ps[b, RootProc].state = "zombie" /\ unwitnessed[b] = {} - /\ LET r == [Rec(b, seq[b] + 1, 0, "exit", reason) EXCEPT !.reply = reply] + /\ LET r == [Rec(b, seq[b] + 1, 0, "exit", ps[b, RootProc].status) EXCEPT + !.reply = ps[b, RootProc].reply] IN /\ machine' = [machine EXCEPT ![b] = "exiting"] /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] /\ pending' = [pending EXCEPT ![b] = r] /\ transit' = transit \cup {r} /\ UNCHANGED <> -\* The root process has ended: the boot exits with its reason and reply. -Reap(b) == ps[b, RootProc].state = "zombie" /\ - Exit(b, ps[b, RootProc].status, ps[b, RootProc].reply) -\* The machine's own wall-time limit fires. The harness kills running -\* commands first; each is still witnessed (Witness), then the boot exits. -Timeout(b) == Exit(b, "timeout", None) +\* The job's wall-time limit fires: the root process ends, killing every +\* process below it. Their commands end and are witnessed; then Reap. +Timeout(b) == + /\ machine[b] = "up" + /\ ps[b, RootProc].state \in Live + /\ ps' = Ended(b, RootProc, "timeout") + /\ intent' = CutOff(b, RootProc) + /\ UNCHANGED <> \* The log has the exit record: the machine is gone. Leave(b) == @@ -286,7 +291,7 @@ Issue(b, p, c) == \* The log has acknowledged the intent: the harness checks the call against \* policy and sends the decision. Deny returns to the model. Allow starts -\* the command, whose witness is sent when it ends (Witness). +\* the command; the process stays blocked until it ends (Witness). \* `agent` spawns a child in the foreground (the caller waits) or the \* background; it fails if the caller's depth is spent or no slot is free. \* `kill` ends one of the caller's live children and its descendants. @@ -301,43 +306,46 @@ Decide(b, p) == me == ps[b, p] Free == {q \in Procs : ps[b, q].state = "unused"} Kids == {q \in Procs : ps[b, q].parent = p /\ ps[b, q].state \in Live} - Done(t) == [t EXCEPT ![b, p].state = "ready"] IN /\ IF Decision(c) = "allow" THEN /\ executed' = [executed EXCEPT ![b] = Append(@, [id |-> i, cmd |-> c])] - /\ unwitnessed' = [unwitnessed EXCEPT ![b] = @ \cup {[id |-> i, cmd |-> c]}] + /\ unwitnessed' = [unwitnessed EXCEPT ![b] = @ \cup {[id |-> i, cmd |-> c, proc |-> p]}] /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} /\ seq' = [seq EXCEPT ![b] = s + 1] /\ IF c = "agent" /\ me.depth > 0 /\ Free # {} THEN \E q \in Free, m \in 1..MeterCap, R \in SUBSET me.rights, fg \in BOOLEAN : LET t == [ps EXCEPT ![b, q] = Spawned(p, m, me.depth - 1, R)] - IN ps' = IF fg THEN [t EXCEPT ![b, p].waits = q] ELSE Done(t) + IN ps' = IF fg THEN [t EXCEPT ![b, p].waits = q] ELSE t ELSE IF c = "kill" /\ Kids # {} THEN \E q \in Kids : LET t == [Ended(b, q, "killed") EXCEPT ![b, q].by = p] - IN /\ ps' = Done(t) + IN /\ ps' = t /\ intent' = [CutOff(b, q) EXCEPT ![b, p] = NoRecord] - ELSE ps' = Done(ps) + ELSE ps' = ps ELSE /\ executed' = executed /\ unwitnessed' = unwitnessed /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} /\ seq' = [seq EXCEPT ![b] = s + 1] - /\ ps' = Done(ps) + /\ ps' = [ps EXCEPT ![b, p].state = "ready"] /\ (c # "kill" \/ Decision(c) = "deny" \/ Kids = {}) => intent' = [intent EXCEPT ![b, p] = NoRecord] /\ UNCHANGED <> -\* A command ends, however it ends (exit, signal, a kill from its process's -\* ancestor or the harness): the tracer's witness goes through the harness, -\* which sequences it. A process's calls are witnessed whatever becomes of -\* the process. +\* A command ends, however it ends (exit, signal, a kill from an ancestor +\* or the harness); a foreground `agent` ends when its child is reaped. The +\* tracer's witness goes through the harness, which sequences it, and the +\* process, if still live, is ready again. A killed process's commands are +\* witnessed too. Witness(b, e) == /\ machine[b] = "up" /\ e \in unwitnessed[b] + /\ ps[b, e.proc].waits = None /\ unwitnessed' = [unwitnessed EXCEPT ![b] = @ \ {e}] /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] /\ transit' = transit \cup {Rec(b, seq[b] + 1, e.id, "witness", e.cmd)} - /\ UNCHANGED <> + /\ ps' = IF ps[b, e.proc].state = "blocked" + THEN [ps EXCEPT ![b, e.proc].state = "ready"] ELSE ps + /\ UNCHANGED <> \* The model replies without a command: the process ends, and its running \* descendants are killed. The reply is its stdout. @@ -358,17 +366,15 @@ Exhaust(b, p) == /\ intent' = CutOff(b, p) /\ UNCHANGED <> -\* The harness reaps an ended child; a parent waiting on it in the -\* foreground is ready again. +\* The harness reaps an ended child; a parent's foreground `agent` waiting +\* on it can now end (Witness). ReapChild(b, q) == /\ machine[b] = "up" /\ q # RootProc /\ ps[b, q].state = "zombie" /\ LET p == ps[b, q].parent t == [ps EXCEPT ![b, q].state = "reaped"] - IN ps' = IF ps[b, p].waits = q /\ ps[b, p].state = "blocked" - THEN [t EXCEPT ![b, p].state = "ready", ![b, p].waits = None] - ELSE t + IN ps' = IF ps[b, p].waits = q THEN [t EXCEPT ![b, p].waits = None] ELSE t /\ UNCHANGED <> ----------------------------------------------------------------------------- @@ -432,7 +438,7 @@ TypeOK == /\ seq \in [Boots -> 0..MaxSeq] /\ pending \in [Boots -> Record \cup {NoRecord}] /\ \A b \in Boots : executed[b] \in Seq([id : 1..MaxId, cmd : Commands]) - /\ unwitnessed \in [Boots -> SUBSET [id : 1..MaxId, cmd : Commands]] + /\ unwitnessed \in [Boots -> SUBSET [id : 1..MaxId, cmd : Commands, proc : Procs]] /\ job \in [Boots -> Boots] /\ transit \subseteq Record /\ log \subseteq Record @@ -523,4 +529,14 @@ KillReach == \A b \in Boots, p \in Procs : ps[b, p].status = "killed" => ps[b, p].by \in Ancestors(b, p) +\* 18. A live process is blocked exactly while it waits: on its intent's +\* decision, or on its command's end, a foreground `agent` on its child. +BlockedWaits == + \A b \in Boots, p \in Procs : + ps[b, p].state \in Live => + /\ ps[b, p].state = "blocked" <=> + intent[b, p] # NoRecord \/ \E e \in unwitnessed[b] : e.proc = p + /\ ps[b, p].waits # None => + ps[b, p].state = "blocked" /\ ps[b, ps[b, p].waits].state \in Live \cup {"zombie"} + ============================================================================= diff --git a/spec/tree.cfg b/spec/tree.cfg index 4343c07..0e83733 100644 --- a/spec/tree.cfg +++ b/spec/tree.cfg @@ -31,6 +31,7 @@ INVARIANTS WithinMeter Attenuated KillReach + BlockedWaits PROPERTIES LogOnlyGrows From 7430236c7f1c68a990cde5fa0d7806aa6fe2c8cc Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 10:34:33 -0600 Subject: [PATCH 03/19] Specify the record encoding in Lean: canonical, so a signature names one record Co-Authored-By: Claude Opus 5.5 (1M context) --- .gitignore | 1 + spec/Cead.lean | 2 + spec/Cead/Codec.lean | 194 ++++++++++++++++++++++++++++++++++++++++ spec/Cead/Oracle.lean | 88 ++++++++++++++++++ spec/Cead/Record.lean | 172 +++++++++++++++++++++++++++++++++++ spec/lake-manifest.json | 6 ++ spec/lakefile.toml | 9 ++ spec/lean-toolchain | 1 + 8 files changed, 473 insertions(+) create mode 100644 spec/Cead.lean create mode 100644 spec/Cead/Codec.lean create mode 100644 spec/Cead/Oracle.lean create mode 100644 spec/Cead/Record.lean create mode 100644 spec/lake-manifest.json create mode 100644 spec/lakefile.toml create mode 100644 spec/lean-toolchain diff --git a/.gitignore b/.gitignore index 8106cf5..955f4b0 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ .DS_Store target/ .claude/ +spec/.lake/ diff --git a/spec/Cead.lean b/spec/Cead.lean new file mode 100644 index 0000000..29310ab --- /dev/null +++ b/spec/Cead.lean @@ -0,0 +1,2 @@ +import Cead.Codec +import Cead.Record diff --git a/spec/Cead/Codec.lean b/spec/Cead/Codec.lean new file mode 100644 index 0000000..17af16b --- /dev/null +++ b/spec/Cead/Codec.lean @@ -0,0 +1,194 @@ +/-! +A codec is a self-delimiting encoding: a value's bytes say where they end, so +encodings laid end to end parse back with no separator. Each combinator +proves its two laws once; anything built from them inherits both. +-/ +namespace Cead + +abbrev Bytes := List UInt8 + +structure Codec (α : Type) where + enc : α → Bytes + dec : Bytes → Option (α × Bytes) + /-- Decoding an encoding gives the value back, and leaves what follows. -/ + dec_enc : ∀ a rest, dec (enc a ++ rest) = some (a, rest) + /-- Whatever decodes was an encoding, so no two byte strings decode to one value. -/ + enc_dec : ∀ b a rest, dec b = some (a, rest) → enc a ++ rest = b + +/-- Bytes whose length fits a u64: every Rust `Vec` on a 64-bit host. -/ +structure Blob where + data : Bytes + fits : data.length < UInt64.size +deriving DecidableEq + +namespace Codec + +/-- Equal encodings mean equal values. -/ +theorem enc_injective (c : Codec α) {a b : α} (h : c.enc a = c.enc b) : a = b := by + have ha := c.dec_enc a [] + rw [h, c.dec_enc] at ha + cases ha; rfl + +/-- A whole message: one value, nothing after it. -/ +def decAll (c : Codec α) (b : Bytes) : Option α := + match c.dec b with + | some (a, []) => some a + | _ => none + +theorem decAll_enc (c : Codec α) (a : α) : c.decAll (c.enc a) = some a := by + have h := c.dec_enc a [] + rw [List.append_nil] at h + simp [decAll, h] + +/-- Canonical: the only bytes that decode to a value are its encoding. -/ +theorem enc_decAll (c : Codec α) {b : Bytes} {a : α} (h : c.decAll b = some a) : c.enc a = b := by + unfold decAll at h + split at h + · rename_i hd; cases h + simpa using c.enc_dec _ _ _ hd + · cases h + +def unit : Codec Unit where + enc _ := [] + dec b := some ((), b) + dec_enc _ _ := rfl + enc_dec _ _ _ h := by cases h; rfl + +/-- One tag byte, below `n`. -/ +def tag (n : Nat) (hn : n ≤ 256) : Codec (Fin n) where + enc i := [i.val.toUInt8] + dec + | t :: rest => if h : t.toNat < n then some (⟨t.toNat, h⟩, rest) else none + | [] => none + dec_enc i rest := by + have : i.val < 256 := by omega + simp [Nat.toUInt8, Nat.mod_eq_of_lt this] + enc_dec b i rest h := by + match b, h with + | t :: r, h => + simp only at h + split at h + · cases h; simp [Nat.toUInt8] + · cases h + +private def be (n : UInt64) : List UInt8 := + [(n.toNat / 2^56 % 256).toUInt8, (n.toNat / 2^48 % 256).toUInt8, + (n.toNat / 2^40 % 256).toUInt8, (n.toNat / 2^32 % 256).toUInt8, + (n.toNat / 2^24 % 256).toUInt8, (n.toNat / 2^16 % 256).toUInt8, + (n.toNat / 2^8 % 256).toUInt8, (n.toNat % 256).toUInt8] + +private def unbe (a b c d e f g h : UInt8) : UInt64 := + (a.toNat * 2^56 + b.toNat * 2^48 + c.toNat * 2^40 + d.toNat * 2^32 + + e.toNat * 2^24 + f.toNat * 2^16 + g.toNat * 2^8 + h.toNat).toUInt64 + +private theorem digits (x : Nat) (hx : x < 2^64) : + x / 2^56 % 256 * 2^56 + x / 2^48 % 256 * 2^48 + x / 2^40 % 256 * 2^40 + + x / 2^32 % 256 * 2^32 + x / 2^24 % 256 * 2^24 + x / 2^16 % 256 * 2^16 + + x / 2^8 % 256 * 2^8 + x % 256 = x := by + omega + +private theorem unbe_be (n : UInt64) : + unbe (n.toNat / 2^56 % 256).toUInt8 (n.toNat / 2^48 % 256).toUInt8 + (n.toNat / 2^40 % 256).toUInt8 (n.toNat / 2^32 % 256).toUInt8 + (n.toNat / 2^24 % 256).toUInt8 (n.toNat / 2^16 % 256).toUInt8 + (n.toNat / 2^8 % 256).toUInt8 (n.toNat % 256).toUInt8 = n := by + apply UInt64.toNat_inj.mp + simp only [unbe, Nat.toUInt8, UInt8.toNat_ofNat', Nat.mod_mod, Nat.toUInt64, UInt64.toNat_ofNat'] + rw [digits _ n.toNat_lt_size, Nat.mod_eq_of_lt n.toNat_lt_size] + +private theorem be_unbe (a b c d e f g h : UInt8) : + be (unbe a b c d e f g h) = [a, b, c, d, e, f, g, h] := by + have := a.toNat_lt; have := b.toNat_lt; have := c.toNat_lt; have := d.toNat_lt + have := e.toNat_lt; have := f.toNat_lt; have := g.toNat_lt; have := h.toNat_lt + simp only [be, unbe, List.cons.injEq, and_true, Nat.toUInt64, UInt64.toNat_ofNat', Nat.reducePow] + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> + simp only [Nat.toUInt8, UInt8.toNat_ofNat', Nat.reducePow] <;> omega + +/-- Eight bytes, big-endian. -/ +def u64 : Codec UInt64 where + enc := be + dec + | a :: b :: c :: d :: e :: f :: g :: h :: rest => some (unbe a b c d e f g h, rest) + | _ => none + dec_enc n rest := by simp only [be, List.cons_append, List.nil_append, unbe_be] + enc_dec bs n rest hd := by + match bs, hd with + | a :: b :: c :: d :: e :: f :: g :: h :: r, hd => + cases hd; simp [be_unbe] + +/-- A u64 length, then the bytes. -/ +def blob : Codec Blob where + enc b := u64.enc (UInt64.ofNat b.data.length) ++ b.data + dec bs := do + let (n, r) ← u64.dec bs + if h : n.toNat ≤ r.length then + some (⟨r.take n.toNat, by have := n.toNat_lt_size; simp; omega⟩, r.drop n.toNat) + else none + dec_enc b rest := by + have hn : (UInt64.ofNat b.data.length).toNat = b.data.length := + UInt64.toNat_ofNat_of_lt b.fits + simp [List.append_assoc, u64.dec_enc, hn] + enc_dec bs b rest hd := by + simp only [Option.bind_eq_bind] at hd + match hn : u64.dec bs, hd with + | some (n, r), hd => + simp only [Option.bind_some] at hd + split at hd + · cases hd + have := u64.enc_dec _ _ _ hn + simp [List.length_take, Nat.min_eq_left ‹n.toNat ≤ r.length›, List.append_assoc, this] + · cases hd + +def pair (ca : Codec α) (cb : Codec β) : Codec (α × β) where + enc p := ca.enc p.1 ++ cb.enc p.2 + dec bs := do + let (a, r) ← ca.dec bs + let (b, r) ← cb.dec r + pure ((a, b), r) + dec_enc p rest := by simp [List.append_assoc, ca.dec_enc, cb.dec_enc] + enc_dec bs p rest hd := by + match ha : ca.dec bs, hd with + | some (a, r), hd => + simp only [Option.bind_eq_bind, Option.bind_some] at hd + match hb : cb.dec r, hd with + | some (b, r'), hd => + simp only [Option.bind_some, Option.pure_def, Option.some.injEq] at hd + cases hd + simp [List.append_assoc, cb.enc_dec _ _ _ hb, ca.enc_dec _ _ _ ha] + +/-- A tag byte picks the variant; the variant's codec follows. -/ +def tagged (n : Nat) (hn : n ≤ 256) (T : Fin n → Type) (cs : (i : Fin n) → Codec (T i)) : + Codec ((i : Fin n) × T i) where + enc x := (tag n hn).enc x.1 ++ (cs x.1).enc x.2 + dec bs := do + let (i, r) ← (tag n hn).dec bs + let (x, r) ← (cs i).dec r + pure (⟨i, x⟩, r) + dec_enc x rest := by + obtain ⟨i, x⟩ := x + simp [List.append_assoc, (tag n hn).dec_enc, (cs i).dec_enc] + enc_dec bs x rest hd := by + match hi : (tag n hn).dec bs, hd with + | some (i, r), hd => + simp only [Option.bind_eq_bind, Option.bind_some] at hd + match hx : (cs i).dec r, hd with + | some (y, r'), hd => + simp only [Option.bind_some, Option.pure_def, Option.some.injEq] at hd + cases hd + simp [List.append_assoc, (cs i).enc_dec _ _ _ hx, (tag n hn).enc_dec _ _ _ hi] + +/-- A codec for `β` through a bijection with `α`. -/ +def iso (c : Codec α) (f : α → β) (g : β → α) (gf : ∀ a, g (f a) = a) (fg : ∀ b, f (g b) = b) : + Codec β where + enc b := c.enc (g b) + dec bs := (c.dec bs).map fun (a, r) => (f a, r) + dec_enc b rest := by simp [c.dec_enc, fg] + enc_dec bs b rest hd := by + match ha : c.dec bs, hd with + | some (a, r), hd => + simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at hd + obtain ⟨rfl, rfl⟩ := hd + rw [gf]; exact c.enc_dec _ _ _ ha + +end Codec +end Cead diff --git a/spec/Cead/Oracle.lean b/spec/Cead/Oracle.lean new file mode 100644 index 0000000..e020c46 --- /dev/null +++ b/spec/Cead/Oracle.lean @@ -0,0 +1,88 @@ +import Cead.Record + +/-! +The differential oracle: random inputs through the Lean spec, printed one +per line for `cargo test` to run through the Rust and compare. The bridge is +bytes, the interface itself. +-/ +namespace Cead.Oracle + +def hex (b : Bytes) : String := + String.join (b.map fun x => + let s := String.ofList (Nat.toDigits 16 x.toNat) + if s.length = 1 then "0" ++ s else s) + +def byte : IO UInt8 := return (← IO.rand 0 255).toUInt8 + +def blob : IO Blob := do + let n ← IO.rand 0 40 + let data ← (List.range n).mapM fun _ => byte + if h : data.length < UInt64.size then return ⟨data, h⟩ else return ⟨[], by decide⟩ + +def u64 : IO UInt64 := do + -- small values exercise the low bytes, large ones the high + if (← IO.rand 0 1) = 0 then return (← IO.rand 0 1000).toUInt64 + else return (← IO.rand 0 (2^64 - 1)).toUInt64 + +def origin : IO Origin := do + match ← IO.rand 0 2 with + | 0 => return .run + | 1 => return .fork (← blob) (← u64) + | _ => return .recovery (← blob) (← u64) + +def event : IO Event := do + match ← IO.rand 0 2 with + | 0 => return .intent (← blob) + | 1 => return .decision (if (← IO.rand 0 1) = 0 then .allow else .deny) + | _ => + let code ← byte + let ended := if (← IO.rand 0 1) = 0 then Ended.exited code else .signaled code + return .witness ended (← blob) + +def body : IO Body := do + match ← IO.rand 0 2 with + | 0 => + let report ← blob + let evidence := if (← IO.rand 0 1) = 0 then Evidence.unattested else .snp report + return .report (← origin) (← blob) evidence + | 1 => return .call (← u64) (← event) + | _ => + match ← IO.rand 0 3 with + | 0 => return .exit (.finish (← blob)) + | 1 => return .exit .meter + | 2 => return .exit .limit + | _ => return .exit .timeout + +def record : IO Record := return ⟨← blob, ← u64, ← blob, ← body⟩ + +/-- A valid encoding, or one corrupted: a byte changed, cut short, or extended. -/ +def recordBytes : IO Bytes := do + let b := (← record).enc + match ← IO.rand 0 3 with + | 0 => return b + | 1 => + let i ← IO.rand 0 (b.length - 1) + return b.set i (← byte) + | 2 => return b.take (← IO.rand 0 (b.length - 1)) + | _ => return b ++ [← byte] + +/-- Each line: the input, then the encoding of what it decodes to, or `-`. -/ +def records (n : Nat) : IO Unit := do + for _ in [0:n] do + let b ← recordBytes + let out := match Record.dec b with + | some r => hex r.enc + | none => "-" + IO.println s!"{hex b} {out}" + +end Cead.Oracle + +def main (args : List String) : IO UInt32 := do + match args with + | ["record", n, seed] => + IO.setRandSeed seed.toNat! + Cead.Oracle.records n.toNat! + return 0 + | _ => + IO.eprintln "usage: oracle record COUNT SEED" + return 64 diff --git a/spec/Cead/Record.lean b/spec/Cead/Record.lean new file mode 100644 index 0000000..c5117b1 --- /dev/null +++ b/spec/Cead/Record.lean @@ -0,0 +1,172 @@ +import Cead.Codec + +/-! +A record, as the machine signs it: `spec/cead.tla`'s `Record` with each +field's real content. The signature covers `record.enc r`; the codec's laws +make that encoding canonical, so a signature names exactly one record. +-/ +namespace Cead + +open Codec + +/-- What started a boot. A fork or recovery names its snapshot: that boot +and its last record. -/ +inductive Origin where + | run + | fork (boot : Blob) (last : UInt64) + | recovery (boot : Blob) (last : UInt64) +deriving DecidableEq + +/-- What the processor signed about a boot. `unattested` is what trusted-host +mode sends: the host, not the processor, vouches for the key. -/ +inductive Evidence where + | unattested + | snp (report : Blob) +deriving DecidableEq + +inductive Verdict where + | allow + | deny +deriving DecidableEq + +/-- How a command ended. -/ +inductive Ended where + | exited (code : UInt8) + | signaled (signal : UInt8) +deriving DecidableEq + +/-- One call's record, sharing its id with the call's other two. -/ +inductive Event where + | intent (command : Blob) + | decision (verdict : Verdict) + /-- `output` is the digest of the command's whole output, before truncation. -/ + | witness (ended : Ended) (output : Blob) +deriving DecidableEq + +/-- Why a boot ended: the root process's status. Only `finish` has a reply, +and the record carries its digest. -/ +inductive Exit where + | finish (reply : Blob) + | meter + | limit + | timeout +deriving DecidableEq + +inductive Body where + | report (origin : Origin) (measurement : Blob) (evidence : Evidence) + | call (id : UInt64) (event : Event) + | exit (exit : Exit) +deriving DecidableEq + +/-- `boot` is the boot's public key; `prev` the digest of the previous +record's encoding, empty for the report. -/ +structure Record where + boot : Blob + seq : UInt64 + prev : Blob + body : Body +deriving DecidableEq + +namespace Codec + +def blobU64 : Codec (Blob × UInt64) := pair blob u64 + +private def OriginT : Fin 3 → Type + | 0 => Unit | 1 => Blob × UInt64 | 2 => Blob × UInt64 + +def origin : Codec Origin := + iso (tagged 3 (by decide) OriginT fun | 0 => unit | 1 => blobU64 | 2 => blobU64) + (fun | ⟨0, _⟩ => .run | ⟨1, (b, l)⟩ => .fork b l | ⟨2, (b, l)⟩ => .recovery b l) + (fun | .run => ⟨0, ()⟩ | .fork b l => ⟨1, (b, l)⟩ | .recovery b l => ⟨2, (b, l)⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, () => rfl | 1, (_, _) => rfl | 2, (_, _) => rfl) + (by intro o; cases o <;> rfl) + +private def EvidenceT : Fin 2 → Type + | 0 => Unit | 1 => Blob + +def evidence : Codec Evidence := + iso (tagged 2 (by decide) EvidenceT fun | 0 => unit | 1 => blob) + (fun | ⟨0, _⟩ => .unattested | ⟨1, r⟩ => .snp r) + (fun | .unattested => ⟨0, ()⟩ | .snp r => ⟨1, r⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, () => rfl | 1, _ => rfl) + (by intro e; cases e <;> rfl) + +def verdict : Codec Verdict := + iso (tag 2 (by decide)) + (fun | 0 => .allow | 1 => .deny) + (fun | .allow => 0 | .deny => 1) + (by intro i; match i with | 0 => rfl | 1 => rfl) + (by intro v; cases v <;> rfl) + +private def u8 : Codec UInt8 := + iso (tag 256 (by decide)) (fun i => i.val.toUInt8) (fun b => ⟨b.toNat, b.toNat_lt⟩) + (by intro i; apply Fin.ext; simp [Nat.toUInt8]) + (by intro b; simp [Nat.toUInt8]) + +private def EndedT : Fin 2 → Type + | 0 => UInt8 | 1 => UInt8 + +def ended : Codec Ended := + iso (tagged 2 (by decide) EndedT fun | 0 => u8 | 1 => u8) + (fun | ⟨0, c⟩ => .exited c | ⟨1, s⟩ => .signaled s) + (fun | .exited c => ⟨0, c⟩ | .signaled s => ⟨1, s⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, _ => rfl) + (by intro e; cases e <;> rfl) + +private def EventT : Fin 3 → Type + | 0 => Blob | 1 => Verdict | 2 => Ended × Blob + +def event : Codec Event := + iso (tagged 3 (by decide) EventT fun | 0 => blob | 1 => verdict | 2 => pair ended blob) + (fun | ⟨0, c⟩ => .intent c | ⟨1, v⟩ => .decision v | ⟨2, (e, o)⟩ => .witness e o) + (fun | .intent c => ⟨0, c⟩ | .decision v => ⟨1, v⟩ | .witness e o => ⟨2, (e, o)⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, _ => rfl | 2, (_, _) => rfl) + (by intro e; cases e <;> rfl) + +private def ExitT : Fin 4 → Type + | 0 => Blob | 1 => Unit | 2 => Unit | 3 => Unit + +def exit : Codec Exit := + iso (tagged 4 (by decide) ExitT fun | 0 => blob | 1 => unit | 2 => unit | 3 => unit) + (fun | ⟨0, r⟩ => .finish r | ⟨1, _⟩ => .meter | ⟨2, _⟩ => .limit | ⟨3, _⟩ => .timeout) + (fun | .finish r => ⟨0, r⟩ | .meter => ⟨1, ()⟩ | .limit => ⟨2, ()⟩ | .timeout => ⟨3, ()⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, () => rfl | 2, () => rfl | 3, () => rfl) + (by intro e; cases e <;> rfl) + +private def BodyT : Fin 3 → Type + | 0 => Origin × Blob × Evidence | 1 => UInt64 × Event | 2 => Exit + +def body : Codec Body := + iso (tagged 3 (by decide) BodyT + fun | 0 => pair origin (pair blob evidence) | 1 => pair u64 event | 2 => exit) + (fun | ⟨0, (o, m, e)⟩ => .report o m e | ⟨1, (i, e)⟩ => .call i e | ⟨2, x⟩ => .exit x) + (fun | .report o m e => ⟨0, (o, m, e)⟩ | .call i e => ⟨1, (i, e)⟩ | .exit x => ⟨2, x⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, (_, _, _) => rfl | 1, (_, _) => rfl | 2, _ => rfl) + (by intro b; cases b <;> rfl) + +def record : Codec Record := + iso (pair blob (pair u64 (pair blob body))) + (fun (b, s, p, x) => ⟨b, s, p, x⟩) + (fun r => (r.boot, r.seq, r.prev, r.body)) + (fun _ => rfl) + (fun _ => rfl) + +end Codec + +/-- The bytes a boot's key signs. -/ +def Record.enc (r : Record) : Bytes := Codec.record.enc r + +def Record.dec (b : Bytes) : Option Record := Codec.record.decAll b + +theorem Record.dec_enc (r : Record) : Record.dec r.enc = some r := + Codec.record.decAll_enc r + +/-- Canonical: the only bytes that decode to a record are its encoding. -/ +theorem Record.enc_dec {b : Bytes} {r : Record} (h : Record.dec b = some r) : r.enc = b := + Codec.record.enc_decAll h + +/-- Two records sign the same bytes only if they are the same record. -/ +theorem Record.enc_injective {r s : Record} (h : r.enc = s.enc) : r = s := + Codec.record.enc_injective h + +end Cead diff --git a/spec/lake-manifest.json b/spec/lake-manifest.json new file mode 100644 index 0000000..2df766a --- /dev/null +++ b/spec/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "cead", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/spec/lakefile.toml b/spec/lakefile.toml new file mode 100644 index 0000000..6e1bc5b --- /dev/null +++ b/spec/lakefile.toml @@ -0,0 +1,9 @@ +name = "cead" +defaultTargets = ["Cead"] + +[[lean_lib]] +name = "Cead" + +[[lean_exe]] +name = "oracle" +root = "Cead.Oracle" diff --git a/spec/lean-toolchain b/spec/lean-toolchain new file mode 100644 index 0000000..ba8ebf2 --- /dev/null +++ b/spec/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1 From a125521fd9b0250eed48d61c05906b1f130aed71 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 10:38:57 -0600 Subject: [PATCH 04/19] Prove the log's acceptance for every log size Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/Cead.lean | 1 + spec/Cead/Log.lean | 254 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 255 insertions(+) create mode 100644 spec/Cead/Log.lean diff --git a/spec/Cead.lean b/spec/Cead.lean index 29310ab..1e7ff45 100644 --- a/spec/Cead.lean +++ b/spec/Cead.lean @@ -1,2 +1,3 @@ import Cead.Codec import Cead.Record +import Cead.Log diff --git a/spec/Cead/Log.lean b/spec/Cead/Log.lean new file mode 100644 index 0000000..e050f4d --- /dev/null +++ b/spec/Cead/Log.lean @@ -0,0 +1,254 @@ +import Cead.Record + +/-! +The log's acceptance, `spec/cead.tla`'s `Arrive` over real records, proved +for every log size (TLC checks it up to its bounds). + +`accept` sees only records whose signature already verified: `boot` is the +boot's public key, so the check needs no log. A report's evidence is +verified by then too (attested) or accepted as `unattested` (trusted-host +mode). Everything that depends on the log is here. `hash` is any function: +the proofs assume nothing of it; collision resistance is what makes +`Linked` mean what it says. +-/ +namespace Cead + +abbrev Log := List Record + +def Body.isReport : Body → Bool + | .report .. => true + | _ => false + +def Body.isExit : Body → Bool + | .exit _ => true + | _ => false + +/-- The boot a report recovers, if it is a recovery. -/ +def Body.recovers : Body → Option Blob + | .report (.recovery b _) _ _ => some b + | _ => none + +section +variable (log : Log) + +def Logged (b : Blob) (s : UInt64) : Prop := ∃ r ∈ log, r.boot = b ∧ r.seq = s + +def Vouched (b : Blob) : Prop := Logged log b 1 + +def Exited (b : Blob) : Prop := ∃ r ∈ log, r.boot = b ∧ r.body.isExit + +def Recovered (b : Blob) : Prop := ∃ r ∈ log, r.body.recovers = some b + +instance : Decidable (Logged log b s) := by unfold Logged; infer_instance +instance : Decidable (Vouched log b) := by unfold Vouched; infer_instance +instance : Decidable (Exited log b) := by unfold Exited; infer_instance +instance : Decidable (Recovered log b) := by unfold Recovered; infer_instance +end + +variable (hash : Bytes → Blob) + +/-- `r`'s neighbours already in the log agree with it on the hash chain. -/ +def Links (log : Log) (r : Record) : Prop := + (∀ p ∈ log, p.boot = r.boot → p.seq.toNat + 1 = r.seq.toNat → r.prev = hash p.enc) ∧ + (∀ s ∈ log, s.boot = r.boot → r.seq.toNat + 1 = s.seq.toNat → s.prev = hash r.enc) + +instance : Decidable (Links hash log r) := by unfold Links; infer_instance + +/-- What a report's origin demands: a fork or recovery names a record the +log holds; a recovery only while its boot has no exit record and no other +recovery. -/ +def Origin.Admits (log : Log) : Origin → Prop + | .run => True + | .fork b l => Logged log b l + | .recovery b l => Logged log b l ∧ ¬ Exited log b ∧ ¬ Recovered log b + +instance : Decidable (Origin.Admits log o) := by cases o <;> unfold Origin.Admits <;> infer_instance + +/-- What a record's kind demands of the log. A report opens its chain: +first, with no predecessor. Any other record needs its boot's report, and no recovery of its +boot: a recovery fences the boot it recovers. -/ +def Admits (log : Log) (r : Record) : Prop := + match r.body with + | .report o _ _ => r.seq = 1 ∧ r.prev.data = [] ∧ o.Admits log + | _ => 1 < r.seq ∧ Vouched log r.boot ∧ ¬ Recovered log r.boot + +instance : Decidable (Admits log r) := by unfold Admits; split <;> infer_instance + +/-- The log keeps a record, or refuses it. It keeps the first record for each +place in a boot's chain, so a duplicate or resend is refused and changes +nothing. -/ +def accept (log : Log) (r : Record) : Option Log := + if ¬ Logged log r.boot r.seq ∧ Links hash log r ∧ Admits log r then some (log ++ [r]) else none + +/-- The snapshot a fork or recovery booted from. -/ +def Body.source : Body → Option (Blob × UInt64) + | .report (.fork b l) _ _ | .report (.recovery b l) _ _ => some (b, l) + | _ => none + +/-- What every log `accept` builds from empty satisfies. -/ +structure Valid (log : Log) : Prop where + /-- A report opens each chain; every other record comes after it. -/ + opens : ∀ r ∈ log, if r.body.isReport then r.seq = 1 ∧ r.prev.data = [] else 1 < r.seq + /-- One record per place in a boot's chain. -/ + firstWins : log.Pairwise fun r s => ¬ (r.boot = s.boot ∧ r.seq = s.seq) + /-- Every record's boot has its report in the log. -/ + vouched : ∀ r ∈ log, Vouched log r.boot + /-- A fork or recovery names a record the log holds. -/ + rooted : ∀ r ∈ log, ∀ b l, r.body.source = some (b, l) → Logged log b l + /-- Nothing of a boot follows its recovery. -/ + fenced : log.Pairwise fun r s => r.body.recovers ≠ some s.boot + /-- At most one recovery per boot. -/ + recoveredOnce : log.Pairwise fun r s => ∀ b, r.body.recovers = some b → s.body.recovers ≠ some b + /-- A job has one outcome: no boot both exits and is recovered. -/ + oneOutcome : ∀ b, Exited log b → ¬ Recovered log b + /-- Neighbours in a chain link by hash. -/ + linked : ∀ p ∈ log, ∀ s ∈ log, p.boot = s.boot → p.seq.toNat + 1 = s.seq.toNat → + s.prev = hash p.enc + +theorem valid_nil : Valid hash [] := by + constructor <;> simp [Exited] + +section Proofs +variable {log : Log} {r : Record} {b : Blob} {s : UInt64} + +private theorem logged_append (h : Logged log b s) : Logged (log ++ [r]) b s := by + obtain ⟨x, hx, h⟩ := h; exact ⟨x, by simp [hx], h⟩ + +private theorem recovers_source {x : Record} (h : x.body.recovers = some b) : + ∃ l, x.body.source = some (b, l) := by + match hb : x.body, h with + | .report (.recovery b' l) _ _, h => + simp only [Body.recovers, Option.some.injEq] at h; subst h; exact ⟨l, rfl⟩ + +/-- A recovered boot's report is in the log: the recovery names one of its records. -/ +private theorem recovered_vouched (hv : Valid hash log) (h : Recovered log b) : Logged log b 1 := by + obtain ⟨x, hx, hr⟩ := h + obtain ⟨l, hs⟩ := recovers_source hr + obtain ⟨y, hy, rfl, -⟩ := hv.rooted x hx b l hs + exact hv.vouched y hy + +/-- `accept` keeps the record and refuses nothing it should keep: the log only grows. -/ +theorem accept_grows {log' : Log} (h : accept hash log r = some log') : log' = log ++ [r] := by + unfold accept at h; split at h <;> simp_all + +theorem accept_valid {log' : Log} (hv : Valid hash log) (h : accept hash log r = some log') : + Valid hash log' := by + unfold accept at h + split at h + case isFalse => cases h + rename_i hc + obtain ⟨hnew, ⟨hprev, hnext⟩, hadm⟩ := hc + cases h + -- No recovery of r's boot is in the log. + have hfresh : ¬ Recovered log r.boot := by + unfold Admits at hadm + split at hadm + · intro hr + exact hnew (hadm.1 ▸ recovered_vouched hash hv hr) + · exact hadm.2.2 + constructor + · intro x hx + rcases List.mem_append.mp hx with hx | hx + · exact hv.opens x hx + · simp only [List.mem_singleton] at hx; subst hx + unfold Admits at hadm + split at hadm + · rename_i hb; simp [Body.isReport, hb, hadm.1, hadm.2.1] + · rename_i hb + have : x.body.isReport = false := by + unfold Body.isReport; split + · rename_i h; exact absurd h (hb _ _ _) + · rfl + simp [this, hadm.1] + · rw [List.pairwise_append] + refine ⟨hv.firstWins, by simp, ?_⟩ + intro x hx y hy ⟨hb, hs⟩ + simp only [List.mem_singleton] at hy; subst hy + exact hnew ⟨x, hx, hb, hs⟩ + · intro x hx + rcases List.mem_append.mp hx with hx | hx + · exact logged_append (hv.vouched x hx) + · simp only [List.mem_singleton] at hx; subst hx + unfold Admits at hadm + split at hadm + · exact ⟨x, by simp, rfl, hadm.1⟩ + · exact logged_append hadm.2.1 + · intro x hx b l hs + rcases List.mem_append.mp hx with hx | hx + · exact logged_append (hv.rooted x hx b l hs) + · simp only [List.mem_singleton] at hx; subst hx + unfold Admits at hadm + split at hadm + · rename_i o m e hb + rw [hb] at hs + cases o <;> simp only [Body.source, Option.some.injEq, Prod.mk.injEq, reduceCtorEq] at hs + all_goals + obtain ⟨rfl, rfl⟩ := hs + simp only [Origin.Admits] at hadm + · exact logged_append hadm.2.2 + · exact logged_append hadm.2.2.1 + · rename_i hb + match hx : x.body, hs with + | .report (.fork _ _) _ _, _ | .report (.recovery _ _) _ _, _ => + exact absurd hx (hb _ _ _) + · rw [List.pairwise_append] + refine ⟨hv.fenced, by simp, ?_⟩ + intro x hx y hy h + simp only [List.mem_singleton] at hy; subst hy + exact hfresh ⟨x, hx, h⟩ + · rw [List.pairwise_append] + refine ⟨hv.recoveredOnce, by simp, ?_⟩ + intro x hx y hy b hxb hyb + simp only [List.mem_singleton] at hy; subst hy + unfold Admits at hadm + split at hadm + · rename_i o m e hb + cases o <;> simp [Body.recovers, hb] at hyb + subst hyb + exact hadm.2.2.2.2 ⟨x, hx, hxb⟩ + · rename_i hb + match hy : y.body, hyb with + | .report (.recovery _ _) _ _, _ => exact absurd hy (hb _ _ _) + · intro b hex hrec + obtain ⟨x, hx, hxb, hxe⟩ := hex + obtain ⟨y, hy, hyr⟩ := hrec + rcases List.mem_append.mp hx with hxo | hxr <;> rcases List.mem_append.mp hy with hyo | hyr' + · exact hv.oneOutcome b ⟨x, hxo, hxb, hxe⟩ ⟨y, hyo, hyr⟩ + · -- r recovers b, which already has an exit record + simp only [List.mem_singleton] at hyr'; subst hyr' + unfold Admits at hadm + split at hadm + · rename_i o m e hb + cases o <;> simp [Body.recovers, hb] at hyr + subst hyr + exact hadm.2.2.2.1 ⟨x, hxo, hxb, hxe⟩ + · rename_i hb + match hyb : y.body, hyr with + | .report (.recovery _ _) _ _, _ => exact absurd hyb (hb _ _ _) + · -- r is b's exit record, and b is already recovered + simp only [List.mem_singleton] at hxr; subst hxr + exact hfresh (hxb ▸ ⟨y, hyo, hyr⟩) + · simp only [List.mem_singleton] at hxr hyr' + rw [hxr] at hxe; rw [hyr'] at hyr + match hb : r.body, hxe, hyr with + | .report (.recovery _ _) _ _, hxe, _ => simp [Body.isExit] at hxe + · intro p hp q hq hb hs + rcases List.mem_append.mp hp with hpo | hpr <;> rcases List.mem_append.mp hq with hqo | hqr + · exact hv.linked p hpo q hqo hb hs + · simp only [List.mem_singleton] at hqr; subst hqr; exact hprev p hpo hb hs + · simp only [List.mem_singleton] at hpr; subst hpr; exact hnext q hqo hb.symm hs + · simp only [List.mem_singleton] at hpr hqr; subst hpr; subst hqr; omega + +/-- The logs `accept` builds from empty, one record at a time. -/ +inductive Accepted : Log → Prop + | nil : Accepted [] + | cons {log log' r} : Accepted log → accept hash log r = some log' → Accepted log' + +/-- Every log built by `accept` from empty is valid. -/ +theorem accepted_valid (h : Accepted hash log) : Valid hash log := by + induction h with + | nil => exact valid_nil hash + | cons _ ha ih => exact accept_valid hash ih ha + +end Proofs +end Cead From e2a11de854676ee115165f09af8bd416e760dac5 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:08:09 -0600 Subject: [PATCH 05/19] Name each call's process in its records, so the log holds the process tree Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/cead.cfg | 1 + spec/cead.tla | 71 ++++++++++++++++++++++++++++++++++++--------------- spec/tree.cfg | 1 + 3 files changed, 53 insertions(+), 20 deletions(-) diff --git a/spec/cead.cfg b/spec/cead.cfg index 47cef0a..df69477 100644 --- a/spec/cead.cfg +++ b/spec/cead.cfg @@ -32,6 +32,7 @@ INVARIANTS Attenuated KillReach BlockedWaits + ProcessTree PROPERTIES LogOnlyGrows diff --git a/spec/cead.tla b/spec/cead.tla index b8eb264..29ca777 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -60,13 +60,16 @@ Live == {"ready", "running", "blocked"} \* order the machine sent it, whatever order it arrives in. A report (seq 1, \* id 0) names its boot, whose key signs the rest, what started it, and for \* a fork or recovery the snapshot it booted from: that boot and its last -\* record. A call's intent, decision and witness carry its id and command; -\* the exit record carries id 0, why the boot ended, and the root process's -\* reply if it finished: the answer, signed. +\* record. A call's intent, decision and witness carry its id, its command +\* and the process that made it; a decision that spawns a process names it +\* as `child`, so the log holds the process tree. The exit record carries +\* id 0, why the boot ended, and the root process's reply if it finished: +\* the answer, signed. Record == [boot : Boots, seq : 1..MaxSeq, id : 0..MaxId, type : CallTypes \cup {"report", "exit"}, body : Commands \cup Reasons \cup Origins, key : Signers, - from : Boots \cup {None}, last : 0..MaxSeq, reply : Replies \cup {None}] + from : Boots \cup {None}, last : 0..MaxSeq, reply : Replies \cup {None}, + proc : Procs \cup {None}, child : Procs \cup {None}] \* One process, as the harness holds it. `cap` is the meter it was given, \* `meter` what remains; `waits` is the child it waits for in the foreground; @@ -96,7 +99,7 @@ VARIABLES ids, \* per boot: the last call id seq, \* per boot: the machine's last sequence number pending, \* per boot: the report or exit record awaiting acknowledgment, or NoRecord - executed, \* per boot: what the kernel ran, in order: the truth + executed, \* per boot: what the kernel ran, in order, and in which process: the truth unwitnessed, \* per boot: calls executed whose command has not yet ended job, \* per boot: the boot that started its job snapshots, \* every snapshot taken: a boot, its last record, its processes @@ -106,10 +109,12 @@ VARIABLES vars == <> -Rec(b, s, i, t, x) == [boot |-> b, seq |-> s, id |-> i, type |-> t, body |-> x, - key |-> b, from |-> None, last |-> 0, reply |-> None] +Rec(b, s, i, t, x, p) == [boot |-> b, seq |-> s, id |-> i, type |-> t, body |-> x, + key |-> b, from |-> None, last |-> 0, reply |-> None, + proc |-> p, child |-> None] Report(b, o, f, l) == [boot |-> b, seq |-> 1, id |-> 0, type |-> "report", body |-> o, - key |-> "processor", from |-> f, last |-> l, reply |-> None] + key |-> "processor", from |-> f, last |-> l, reply |-> None, + proc |-> None, child |-> None] Logged(b, s) == \E r \in log : r.boot = b /\ r.seq = s LoggedType(b, i, t) == \E r \in log : r.boot = b /\ r.id = i /\ r.type = t \* The log holds boot b's report: b's key is vouched for. @@ -219,7 +224,7 @@ Reap(b) == /\ machine[b] = "up" /\ ps[b, RootProc].state = "zombie" /\ unwitnessed[b] = {} - /\ LET r == [Rec(b, seq[b] + 1, 0, "exit", ps[b, RootProc].status) EXCEPT + /\ LET r == [Rec(b, seq[b] + 1, 0, "exit", ps[b, RootProc].status, None) EXCEPT !.reply = ps[b, RootProc].reply] IN /\ machine' = [machine EXCEPT ![b] = "exiting"] /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] @@ -275,7 +280,7 @@ Issue(b, p, c) == /\ ps[b, p].state = "running" /\ ps[b, p].calls < CallLimit /\ Chargeable(b, p) - /\ LET r == Rec(b, seq[b] + 1, ids[b] + 1, "intent", c) + /\ LET r == Rec(b, seq[b] + 1, ids[b] + 1, "intent", c, p) A == {p} \cup Ancestors(b, p) IN /\ ps' = [x \in Boots \X Procs |-> IF x[1] = b /\ x[2] \in A @@ -306,26 +311,27 @@ Decide(b, p) == me == ps[b, p] Free == {q \in Procs : ps[b, q].state = "unused"} Kids == {q \in Procs : ps[b, q].parent = p /\ ps[b, q].state \in Live} - IN /\ IF Decision(c) = "allow" - THEN /\ executed' = [executed EXCEPT ![b] = Append(@, [id |-> i, cmd |-> c])] + D(q) == [Rec(b, s + 1, i, "decision", c, p) EXCEPT !.child = q] + IN /\ seq' = [seq EXCEPT ![b] = s + 1] + /\ IF Decision(c) = "allow" + THEN /\ executed' = [executed EXCEPT ![b] = Append(@, [id |-> i, cmd |-> c, proc |-> p])] /\ unwitnessed' = [unwitnessed EXCEPT ![b] = @ \cup {[id |-> i, cmd |-> c, proc |-> p]}] - /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} - /\ seq' = [seq EXCEPT ![b] = s + 1] /\ IF c = "agent" /\ me.depth > 0 /\ Free # {} THEN \E q \in Free, m \in 1..MeterCap, R \in SUBSET me.rights, fg \in BOOLEAN : LET t == [ps EXCEPT ![b, q] = Spawned(p, m, me.depth - 1, R)] - IN ps' = IF fg THEN [t EXCEPT ![b, p].waits = q] ELSE t + IN /\ ps' = IF fg THEN [t EXCEPT ![b, p].waits = q] ELSE t + /\ transit' = transit \cup {D(q)} ELSE IF c = "kill" /\ Kids # {} THEN \E q \in Kids : LET t == [Ended(b, q, "killed") EXCEPT ![b, q].by = p] IN /\ ps' = t /\ intent' = [CutOff(b, q) EXCEPT ![b, p] = NoRecord] - ELSE ps' = ps + /\ transit' = transit \cup {D(None)} + ELSE ps' = ps /\ transit' = transit \cup {D(None)} ELSE /\ executed' = executed /\ unwitnessed' = unwitnessed - /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} - /\ seq' = [seq EXCEPT ![b] = s + 1] + /\ transit' = transit \cup {D(None)} /\ ps' = [ps EXCEPT ![b, p].state = "ready"] /\ (c # "kill" \/ Decision(c) = "deny" \/ Kids = {}) => intent' = [intent EXCEPT ![b, p] = NoRecord] @@ -342,7 +348,7 @@ Witness(b, e) == /\ ps[b, e.proc].waits = None /\ unwitnessed' = [unwitnessed EXCEPT ![b] = @ \ {e}] /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] - /\ transit' = transit \cup {Rec(b, seq[b] + 1, e.id, "witness", e.cmd)} + /\ transit' = transit \cup {Rec(b, seq[b] + 1, e.id, "witness", e.cmd, e.proc)} /\ ps' = IF ps[b, e.proc].state = "blocked" THEN [ps EXCEPT ![b, e.proc].state = "ready"] ELSE ps /\ UNCHANGED <> @@ -437,7 +443,7 @@ TypeOK == /\ ids \in [Boots -> 0..MaxId] /\ seq \in [Boots -> 0..MaxSeq] /\ pending \in [Boots -> Record \cup {NoRecord}] - /\ \A b \in Boots : executed[b] \in Seq([id : 1..MaxId, cmd : Commands]) + /\ \A b \in Boots : executed[b] \in Seq([id : 1..MaxId, cmd : Commands, proc : Procs]) /\ unwitnessed \in [Boots -> SUBSET [id : 1..MaxId, cmd : Commands, proc : Procs]] /\ job \in [Boots -> Boots] /\ transit \subseteq Record @@ -539,4 +545,29 @@ BlockedWaits == /\ ps[b, p].waits # None => ps[b, p].state = "blocked" /\ ps[b, ps[b, p].waits].state \in Live \cup {"zombie"} +\* The records boot b sent through its record n, and, if it booted from a +\* snapshot, that boot's records through the snapshot's last record. +RECURSIVE Before(_, _) +Before(b, n) == + LET Sent == {r \in transit \cup log : r.key # "path"} + R == {r \in Sent : r.boot = b /\ r.type = "report"} + Mine == {r \in Sent : r.boot = b /\ r.seq <= n} + IN IF R = {} THEN Mine + ELSE LET x == CHOOSE x \in R : TRUE + IN IF x.from = None THEN Mine ELSE Mine \cup Before(x.from, x.last) + +\* 19. Every logged call names the process that ran it, and a process other +\* than the root was spawned earlier in its boot's records, by a +\* decision its parent made: the log holds the process tree. +ProcessTree == + \A r \in log : + r.type \in CallTypes => + /\ r.proc \in Procs + /\ \A k \in 1..Len(executed[r.boot]) : + executed[r.boot][k].id = r.id => executed[r.boot][k].proc = r.proc + /\ r.proc # RootProc => + \E d \in Before(r.boot, r.seq - 1) : + /\ d.type = "decision" /\ d.child = r.proc + /\ d.proc = ps[r.boot, r.proc].parent + ============================================================================= diff --git a/spec/tree.cfg b/spec/tree.cfg index 0e83733..32670e8 100644 --- a/spec/tree.cfg +++ b/spec/tree.cfg @@ -32,6 +32,7 @@ INVARIANTS Attenuated KillReach BlockedWaits + ProcessTree PROPERTIES LogOnlyGrows From fbeb1b197ca3c4e41ce8c944ba5729a62472009f Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:11:09 -0600 Subject: [PATCH 06/19] Drop the hash chain: a signature already fixes each record's author and place Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 4 +-- spec/Cead/Log.lean | 72 ++++++++++++++----------------------- spec/Cead/Oracle.lean | 18 ++++++---- spec/Cead/Record.lean | 84 +++++++++++++++++++++++-------------------- spec/cead.tla | 8 ++--- 5 files changed, 89 insertions(+), 97 deletions(-) diff --git a/CODE.md b/CODE.md index 6c0ade1..f6d94b5 100644 --- a/CODE.md +++ b/CODE.md @@ -34,7 +34,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun |---|---|---| | authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | | availability | The job runs and ends. The host guarantees it, and can always deny it. | `spec/cead.tla` | -| boot | One life of a machine's kernel, from the VMM starting it to eviction, with one key. Its records form one hash chain signed with that key, its report first. **Complete** when the log holds its records through its exit record with no gap; otherwise **unknown** (crash, host kill, lost report). Linux's `boot_id`. | `spec/cead.tla` | +| boot | One life of a machine's kernel, from the VMM starting it to eviction, with one key. Its records are numbered from its report, each signed with that key. **Complete** when the log holds its records through its exit record with no gap; otherwise **unknown** (crash, host kill, lost report). Linux's `boot_id`. | `spec/cead.tla` | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | | call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `agent`; every other call is a well-known CLI. | | | call table | The system call table: the toolset. | | @@ -51,7 +51,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, sequences records for init to sign. | | | host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | | | init | PID 1 in the machine, for the whole boot. Makes the boot's key and never lets it go; signs every record. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, forks the harness. If the harness dies, the boot ends with no exit record: unknown. | | -| integrity | The log says only what the machine signed, in the machine's order. Guaranteed by each boot's signature and hash chain, rooted in its report. | `spec/cead.tla` | +| integrity | The log says only what the machine signed, in the machine's order. Guaranteed by each boot's key signing every record, in a numbered sequence rooted in its report. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | | job | One query's work: a root process and its tree. Started by `cead run`. Spans one boot, or more through recovery. | | | limit | A cap on one process: window size, bound, calls, wall time, depth. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | diff --git a/spec/Cead/Log.lean b/spec/Cead/Log.lean index e050f4d..49017d7 100644 --- a/spec/Cead/Log.lean +++ b/spec/Cead/Log.lean @@ -5,11 +5,9 @@ The log's acceptance, `spec/cead.tla`'s `Arrive` over real records, proved for every log size (TLC checks it up to its bounds). `accept` sees only records whose signature already verified: `boot` is the -boot's public key, so the check needs no log. A report's evidence is +boot's public key, so the check needs no log. A report's attestation is verified by then too (attested) or accepted as `unattested` (trusted-host -mode). Everything that depends on the log is here. `hash` is any function: -the proofs assume nothing of it; collision resistance is what makes -`Linked` mean what it says. +mode). Everything that depends on the log is here. -/ namespace Cead @@ -45,15 +43,6 @@ instance : Decidable (Exited log b) := by unfold Exited; infer_instance instance : Decidable (Recovered log b) := by unfold Recovered; infer_instance end -variable (hash : Bytes → Blob) - -/-- `r`'s neighbours already in the log agree with it on the hash chain. -/ -def Links (log : Log) (r : Record) : Prop := - (∀ p ∈ log, p.boot = r.boot → p.seq.toNat + 1 = r.seq.toNat → r.prev = hash p.enc) ∧ - (∀ s ∈ log, s.boot = r.boot → r.seq.toNat + 1 = s.seq.toNat → s.prev = hash r.enc) - -instance : Decidable (Links hash log r) := by unfold Links; infer_instance - /-- What a report's origin demands: a fork or recovery names a record the log holds; a recovery only while its boot has no exit record and no other recovery. -/ @@ -64,21 +53,21 @@ def Origin.Admits (log : Log) : Origin → Prop instance : Decidable (Origin.Admits log o) := by cases o <;> unfold Origin.Admits <;> infer_instance -/-- What a record's kind demands of the log. A report opens its chain: -first, with no predecessor. Any other record needs its boot's report, and no recovery of its +/-- What a record's kind demands of the log. A report opens its boot's +sequence. Any other record needs its boot's report, and no recovery of its boot: a recovery fences the boot it recovers. -/ def Admits (log : Log) (r : Record) : Prop := match r.body with - | .report o _ _ => r.seq = 1 ∧ r.prev.data = [] ∧ o.Admits log + | .report o _ _ => r.seq = 1 ∧ o.Admits log | _ => 1 < r.seq ∧ Vouched log r.boot ∧ ¬ Recovered log r.boot instance : Decidable (Admits log r) := by unfold Admits; split <;> infer_instance /-- The log keeps a record, or refuses it. It keeps the first record for each -place in a boot's chain, so a duplicate or resend is refused and changes +place in a boot's sequence, so a duplicate or resend is refused and changes nothing. -/ def accept (log : Log) (r : Record) : Option Log := - if ¬ Logged log r.boot r.seq ∧ Links hash log r ∧ Admits log r then some (log ++ [r]) else none + if ¬ Logged log r.boot r.seq ∧ Admits log r then some (log ++ [r]) else none /-- The snapshot a fork or recovery booted from. -/ def Body.source : Body → Option (Blob × UInt64) @@ -87,9 +76,9 @@ def Body.source : Body → Option (Blob × UInt64) /-- What every log `accept` builds from empty satisfies. -/ structure Valid (log : Log) : Prop where - /-- A report opens each chain; every other record comes after it. -/ - opens : ∀ r ∈ log, if r.body.isReport then r.seq = 1 ∧ r.prev.data = [] else 1 < r.seq - /-- One record per place in a boot's chain. -/ + /-- A report opens each boot's sequence; every other record comes after it. -/ + opens : ∀ r ∈ log, if r.body.isReport then r.seq = 1 else 1 < r.seq + /-- One record per place in a boot's sequence. -/ firstWins : log.Pairwise fun r s => ¬ (r.boot = s.boot ∧ r.seq = s.seq) /-- Every record's boot has its report in the log. -/ vouched : ∀ r ∈ log, Vouched log r.boot @@ -101,11 +90,8 @@ structure Valid (log : Log) : Prop where recoveredOnce : log.Pairwise fun r s => ∀ b, r.body.recovers = some b → s.body.recovers ≠ some b /-- A job has one outcome: no boot both exits and is recovered. -/ oneOutcome : ∀ b, Exited log b → ¬ Recovered log b - /-- Neighbours in a chain link by hash. -/ - linked : ∀ p ∈ log, ∀ s ∈ log, p.boot = s.boot → p.seq.toNat + 1 = s.seq.toNat → - s.prev = hash p.enc -theorem valid_nil : Valid hash [] := by +theorem valid_nil : Valid [] := by constructor <;> simp [Exited] section Proofs @@ -121,30 +107,30 @@ private theorem recovers_source {x : Record} (h : x.body.recovers = some b) : simp only [Body.recovers, Option.some.injEq] at h; subst h; exact ⟨l, rfl⟩ /-- A recovered boot's report is in the log: the recovery names one of its records. -/ -private theorem recovered_vouched (hv : Valid hash log) (h : Recovered log b) : Logged log b 1 := by +private theorem recovered_vouched (hv : Valid log) (h : Recovered log b) : Logged log b 1 := by obtain ⟨x, hx, hr⟩ := h obtain ⟨l, hs⟩ := recovers_source hr obtain ⟨y, hy, rfl, -⟩ := hv.rooted x hx b l hs exact hv.vouched y hy /-- `accept` keeps the record and refuses nothing it should keep: the log only grows. -/ -theorem accept_grows {log' : Log} (h : accept hash log r = some log') : log' = log ++ [r] := by +theorem accept_grows {log' : Log} (h : accept log r = some log') : log' = log ++ [r] := by unfold accept at h; split at h <;> simp_all -theorem accept_valid {log' : Log} (hv : Valid hash log) (h : accept hash log r = some log') : - Valid hash log' := by +theorem accept_valid {log' : Log} (hv : Valid log) (h : accept log r = some log') : + Valid log' := by unfold accept at h split at h case isFalse => cases h rename_i hc - obtain ⟨hnew, ⟨hprev, hnext⟩, hadm⟩ := hc + obtain ⟨hnew, hadm⟩ := hc cases h -- No recovery of r's boot is in the log. have hfresh : ¬ Recovered log r.boot := by unfold Admits at hadm split at hadm · intro hr - exact hnew (hadm.1 ▸ recovered_vouched hash hv hr) + exact hnew (hadm.1 ▸ recovered_vouched hv hr) · exact hadm.2.2 constructor · intro x hx @@ -153,7 +139,7 @@ theorem accept_valid {log' : Log} (hv : Valid hash log) (h : accept hash log r = · simp only [List.mem_singleton] at hx; subst hx unfold Admits at hadm split at hadm - · rename_i hb; simp [Body.isReport, hb, hadm.1, hadm.2.1] + · rename_i hb; simp [Body.isReport, hb, hadm.1] · rename_i hb have : x.body.isReport = false := by unfold Body.isReport; split @@ -185,8 +171,8 @@ theorem accept_valid {log' : Log} (hv : Valid hash log) (h : accept hash log r = all_goals obtain ⟨rfl, rfl⟩ := hs simp only [Origin.Admits] at hadm - · exact logged_append hadm.2.2 - · exact logged_append hadm.2.2.1 + · exact logged_append hadm.2 + · exact logged_append hadm.2.1 · rename_i hb match hx : x.body, hs with | .report (.fork _ _) _ _, _ | .report (.recovery _ _) _ _, _ => @@ -205,7 +191,7 @@ theorem accept_valid {log' : Log} (hv : Valid hash log) (h : accept hash log r = · rename_i o m e hb cases o <;> simp [Body.recovers, hb] at hyb subst hyb - exact hadm.2.2.2.2 ⟨x, hx, hxb⟩ + exact hadm.2.2.2 ⟨x, hx, hxb⟩ · rename_i hb match hy : y.body, hyb with | .report (.recovery _ _) _ _, _ => exact absurd hy (hb _ _ _) @@ -221,7 +207,7 @@ theorem accept_valid {log' : Log} (hv : Valid hash log) (h : accept hash log r = · rename_i o m e hb cases o <;> simp [Body.recovers, hb] at hyr subst hyr - exact hadm.2.2.2.1 ⟨x, hxo, hxb, hxe⟩ + exact hadm.2.2.1 ⟨x, hxo, hxb, hxe⟩ · rename_i hb match hyb : y.body, hyr with | .report (.recovery _ _) _ _, _ => exact absurd hyb (hb _ _ _) @@ -232,23 +218,17 @@ theorem accept_valid {log' : Log} (hv : Valid hash log) (h : accept hash log r = rw [hxr] at hxe; rw [hyr'] at hyr match hb : r.body, hxe, hyr with | .report (.recovery _ _) _ _, hxe, _ => simp [Body.isExit] at hxe - · intro p hp q hq hb hs - rcases List.mem_append.mp hp with hpo | hpr <;> rcases List.mem_append.mp hq with hqo | hqr - · exact hv.linked p hpo q hqo hb hs - · simp only [List.mem_singleton] at hqr; subst hqr; exact hprev p hpo hb hs - · simp only [List.mem_singleton] at hpr; subst hpr; exact hnext q hqo hb.symm hs - · simp only [List.mem_singleton] at hpr hqr; subst hpr; subst hqr; omega /-- The logs `accept` builds from empty, one record at a time. -/ inductive Accepted : Log → Prop | nil : Accepted [] - | cons {log log' r} : Accepted log → accept hash log r = some log' → Accepted log' + | cons {log log' r} : Accepted log → accept log r = some log' → Accepted log' /-- Every log built by `accept` from empty is valid. -/ -theorem accepted_valid (h : Accepted hash log) : Valid hash log := by +theorem accepted_valid (h : Accepted log) : Valid log := by induction h with - | nil => exact valid_nil hash - | cons _ ha ih => exact accept_valid hash ih ha + | nil => exact valid_nil + | cons _ ha ih => exact accept_valid ih ha end Proofs end Cead diff --git a/spec/Cead/Oracle.lean b/spec/Cead/Oracle.lean index e020c46..3cab39e 100644 --- a/spec/Cead/Oracle.lean +++ b/spec/Cead/Oracle.lean @@ -33,19 +33,23 @@ def origin : IO Origin := do def event : IO Event := do match ← IO.rand 0 2 with | 0 => return .intent (← blob) - | 1 => return .decision (if (← IO.rand 0 1) = 0 then .allow else .deny) + | 1 => + match ← IO.rand 0 2 with + | 0 => return .decision .deny + | 1 => return .decision .allow + | _ => return .decision (.spawn (← u64)) | _ => let code ← byte - let ended := if (← IO.rand 0 1) = 0 then Ended.exited code else .signaled code - return .witness ended (← blob) + let status := if (← IO.rand 0 1) = 0 then WaitStatus.exited code else .signaled code + return .witness status (← blob) def body : IO Body := do match ← IO.rand 0 2 with | 0 => let report ← blob - let evidence := if (← IO.rand 0 1) = 0 then Evidence.unattested else .snp report - return .report (← origin) (← blob) evidence - | 1 => return .call (← u64) (← event) + let attestation := if (← IO.rand 0 1) = 0 then Attestation.unattested else .snp report + return .report (← origin) (← blob) attestation + | 1 => return .call (← u64) (← u64) (← event) | _ => match ← IO.rand 0 3 with | 0 => return .exit (.finish (← blob)) @@ -53,7 +57,7 @@ def body : IO Body := do | 2 => return .exit .limit | _ => return .exit .timeout -def record : IO Record := return ⟨← blob, ← u64, ← blob, ← body⟩ +def record : IO Record := return ⟨← blob, ← u64, ← body⟩ /-- A valid encoding, or one corrupted: a byte changed, cut short, or extended. -/ def recordBytes : IO Bytes := do diff --git a/spec/Cead/Record.lean b/spec/Cead/Record.lean index c5117b1..2fa3e79 100644 --- a/spec/Cead/Record.lean +++ b/spec/Cead/Record.lean @@ -19,28 +19,31 @@ deriving DecidableEq /-- What the processor signed about a boot. `unattested` is what trusted-host mode sends: the host, not the processor, vouches for the key. -/ -inductive Evidence where +inductive Attestation where | unattested | snp (report : Blob) deriving DecidableEq -inductive Verdict where - | allow +/-- The outcome of checking a call against policy. `spawn` allows an `agent` +call and names the process it starts. -/ +inductive Decision where | deny + | allow + | spawn (child : UInt64) deriving DecidableEq -/-- How a command ended. -/ -inductive Ended where +/-- How a command ended, as `wait(2)` reports it. -/ +inductive WaitStatus where | exited (code : UInt8) | signaled (signal : UInt8) deriving DecidableEq -/-- One call's record, sharing its id with the call's other two. -/ +/-- One call's record, sharing its id and process with the call's other two. -/ inductive Event where | intent (command : Blob) - | decision (verdict : Verdict) - /-- `output` is the digest of the command's whole output, before truncation. -/ - | witness (ended : Ended) (output : Blob) + | decision (decision : Decision) + /-- `output` is the digest of the command's whole output. -/ + | witness (status : WaitStatus) (output : Blob) deriving DecidableEq /-- Why a boot ended: the root process's status. Only `finish` has a reply, @@ -53,17 +56,17 @@ inductive Exit where deriving DecidableEq inductive Body where - | report (origin : Origin) (measurement : Blob) (evidence : Evidence) - | call (id : UInt64) (event : Event) + | report (origin : Origin) (measurement : Blob) (attestation : Attestation) + /-- `proc` is the boot's number for the process that made the call. -/ + | call (id : UInt64) (proc : UInt64) (event : Event) | exit (exit : Exit) deriving DecidableEq -/-- `boot` is the boot's public key; `prev` the digest of the previous -record's encoding, empty for the report. -/ +/-- `boot` is the boot's public key, which signs the record; `seq` its place +in the boot's sequence, the report first. -/ structure Record where boot : Blob seq : UInt64 - prev : Blob body : Body deriving DecidableEq @@ -81,45 +84,48 @@ def origin : Codec Origin := (by rintro ⟨i, x⟩; match i, x with | 0, () => rfl | 1, (_, _) => rfl | 2, (_, _) => rfl) (by intro o; cases o <;> rfl) -private def EvidenceT : Fin 2 → Type +private def AttestationT : Fin 2 → Type | 0 => Unit | 1 => Blob -def evidence : Codec Evidence := - iso (tagged 2 (by decide) EvidenceT fun | 0 => unit | 1 => blob) +def attestation : Codec Attestation := + iso (tagged 2 (by decide) AttestationT fun | 0 => unit | 1 => blob) (fun | ⟨0, _⟩ => .unattested | ⟨1, r⟩ => .snp r) (fun | .unattested => ⟨0, ()⟩ | .snp r => ⟨1, r⟩) (by rintro ⟨i, x⟩; match i, x with | 0, () => rfl | 1, _ => rfl) (by intro e; cases e <;> rfl) -def verdict : Codec Verdict := - iso (tag 2 (by decide)) - (fun | 0 => .allow | 1 => .deny) - (fun | .allow => 0 | .deny => 1) - (by intro i; match i with | 0 => rfl | 1 => rfl) - (by intro v; cases v <;> rfl) +private def DecisionT : Fin 3 → Type + | 0 => Unit | 1 => Unit | 2 => UInt64 + +def decision : Codec Decision := + iso (tagged 3 (by decide) DecisionT fun | 0 => unit | 1 => unit | 2 => u64) + (fun | ⟨0, _⟩ => .deny | ⟨1, _⟩ => .allow | ⟨2, c⟩ => .spawn c) + (fun | .deny => ⟨0, ()⟩ | .allow => ⟨1, ()⟩ | .spawn c => ⟨2, c⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, () => rfl | 1, () => rfl | 2, _ => rfl) + (by intro d; cases d <;> rfl) private def u8 : Codec UInt8 := iso (tag 256 (by decide)) (fun i => i.val.toUInt8) (fun b => ⟨b.toNat, b.toNat_lt⟩) (by intro i; apply Fin.ext; simp [Nat.toUInt8]) (by intro b; simp [Nat.toUInt8]) -private def EndedT : Fin 2 → Type +private def WaitStatusT : Fin 2 → Type | 0 => UInt8 | 1 => UInt8 -def ended : Codec Ended := - iso (tagged 2 (by decide) EndedT fun | 0 => u8 | 1 => u8) +def waitStatus : Codec WaitStatus := + iso (tagged 2 (by decide) WaitStatusT fun | 0 => u8 | 1 => u8) (fun | ⟨0, c⟩ => .exited c | ⟨1, s⟩ => .signaled s) (fun | .exited c => ⟨0, c⟩ | .signaled s => ⟨1, s⟩) (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, _ => rfl) (by intro e; cases e <;> rfl) private def EventT : Fin 3 → Type - | 0 => Blob | 1 => Verdict | 2 => Ended × Blob + | 0 => Blob | 1 => Decision | 2 => WaitStatus × Blob def event : Codec Event := - iso (tagged 3 (by decide) EventT fun | 0 => blob | 1 => verdict | 2 => pair ended blob) - (fun | ⟨0, c⟩ => .intent c | ⟨1, v⟩ => .decision v | ⟨2, (e, o)⟩ => .witness e o) - (fun | .intent c => ⟨0, c⟩ | .decision v => ⟨1, v⟩ | .witness e o => ⟨2, (e, o)⟩) + iso (tagged 3 (by decide) EventT fun | 0 => blob | 1 => decision | 2 => pair waitStatus blob) + (fun | ⟨0, c⟩ => .intent c | ⟨1, d⟩ => .decision d | ⟨2, (w, o)⟩ => .witness w o) + (fun | .intent c => ⟨0, c⟩ | .decision d => ⟨1, d⟩ | .witness w o => ⟨2, (w, o)⟩) (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, _ => rfl | 2, (_, _) => rfl) (by intro e; cases e <;> rfl) @@ -134,20 +140,22 @@ def exit : Codec Exit := (by intro e; cases e <;> rfl) private def BodyT : Fin 3 → Type - | 0 => Origin × Blob × Evidence | 1 => UInt64 × Event | 2 => Exit + | 0 => Origin × Blob × Attestation | 1 => UInt64 × UInt64 × Event | 2 => Exit def body : Codec Body := iso (tagged 3 (by decide) BodyT - fun | 0 => pair origin (pair blob evidence) | 1 => pair u64 event | 2 => exit) - (fun | ⟨0, (o, m, e)⟩ => .report o m e | ⟨1, (i, e)⟩ => .call i e | ⟨2, x⟩ => .exit x) - (fun | .report o m e => ⟨0, (o, m, e)⟩ | .call i e => ⟨1, (i, e)⟩ | .exit x => ⟨2, x⟩) - (by rintro ⟨i, x⟩; match i, x with | 0, (_, _, _) => rfl | 1, (_, _) => rfl | 2, _ => rfl) + fun | 0 => pair origin (pair blob attestation) | 1 => pair u64 (pair u64 event) + | 2 => exit) + (fun | ⟨0, (o, m, a)⟩ => .report o m a | ⟨1, (i, p, e)⟩ => .call i p e | ⟨2, x⟩ => .exit x) + (fun | .report o m a => ⟨0, (o, m, a)⟩ | .call i p e => ⟨1, (i, p, e)⟩ | .exit x => ⟨2, x⟩) + (by rintro ⟨i, x⟩ + match i, x with | 0, (_, _, _) => rfl | 1, (_, _, _) => rfl | 2, _ => rfl) (by intro b; cases b <;> rfl) def record : Codec Record := - iso (pair blob (pair u64 (pair blob body))) - (fun (b, s, p, x) => ⟨b, s, p, x⟩) - (fun r => (r.boot, r.seq, r.prev, r.body)) + iso (pair blob (pair u64 body)) + (fun (b, s, x) => ⟨b, s, x⟩) + (fun r => (r.boot, r.seq, r.body)) (fun _ => rfl) (fun _ => rfl) diff --git a/spec/cead.tla b/spec/cead.tla index 29ca777..3b4c2b9 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -56,7 +56,7 @@ MaxSeq == 3 * MaxId + 2 \* the report, every cal None == "none" \* no process, snapshot or reply Live == {"ready", "running", "blocked"} -\* One record of a boot. `seq` is its place in the boot's hash chain: the +\* One record of a boot. `seq` is its place in the boot's sequence: the \* order the machine sent it, whatever order it arrives in. A report (seq 1, \* id 0) names its boot, whose key signs the rest, what started it, and for \* a fork or recovery the snapshot it booted from: that boot and its last @@ -392,7 +392,7 @@ ReapChild(b, q) == \* while the boot it recovers is not complete, and only the first for that \* boot. It keeps any other record only if its boot's key signed it, the log \* holds that boot's report, and no recovery has taken the boot's place. It -\* keeps the first record for each place in a boot's hash chain; a +\* keeps the first record for each place in a boot's sequence; a \* duplicate or resend changes nothing. First-wins matters only if \* KeySecret fails, so TLC never exercises it. Arrive(r) == @@ -475,8 +475,8 @@ ExecutedOnce == \A b \in Boots : \A j, k \in 1..Len(executed[b]) : j # k => executed[b][j].id # executed[b][k].id -\* 8. No boot signs two different records for one place in its hash chain, -\* so each chain gives one order. +\* 8. No boot signs two different records for one place in its sequence, +\* so each boot gives one order. Unambiguous == LET Seen == {r \in transit : r.key # "path"} \cup log IN \A r1, r2 \in Seen : (r1.boot = r2.boot /\ r1.seq = r2.seq) => r1 = r2 From 9aa32454e83da1c0e9287e73848779af1881d897 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:31:59 -0600 Subject: [PATCH 07/19] Make every window replayable from the log, and prove no tree outspends its root Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/Cead.lean | 2 + spec/Cead/Differential.lean | 151 ++++++++++++++++++++++++ spec/Cead/Log.lean | 26 ++--- spec/Cead/Meter.lean | 224 ++++++++++++++++++++++++++++++++++++ spec/Cead/Oracle.lean | 92 --------------- spec/Cead/Record.lean | 63 ++++++---- spec/Cead/Window.lean | 98 ++++++++++++++++ spec/cead.tla | 6 + spec/lakefile.toml | 4 +- 9 files changed, 535 insertions(+), 131 deletions(-) create mode 100644 spec/Cead/Differential.lean create mode 100644 spec/Cead/Meter.lean delete mode 100644 spec/Cead/Oracle.lean create mode 100644 spec/Cead/Window.lean diff --git a/spec/Cead.lean b/spec/Cead.lean index 1e7ff45..5b2d2c3 100644 --- a/spec/Cead.lean +++ b/spec/Cead.lean @@ -1,3 +1,5 @@ import Cead.Codec import Cead.Record import Cead.Log +import Cead.Window +import Cead.Meter diff --git a/spec/Cead/Differential.lean b/spec/Cead/Differential.lean new file mode 100644 index 0000000..8055a76 --- /dev/null +++ b/spec/Cead/Differential.lean @@ -0,0 +1,151 @@ +import Cead.Window +import Cead.Meter + +/-! +The Lean half of the differential test: random inputs through the spec, +printed one per line for `cargo test` to run through the Rust and compare. +The bridge is bytes, the interface itself. +-/ +namespace Cead.Differential + +def hex (b : Bytes) : String := + String.join (b.map fun x => + let s := String.ofList (Nat.toDigits 16 x.toNat) + if s.length = 1 then "0" ++ s else s) + +def byte : IO UInt8 := return (← IO.rand 0 255).toUInt8 + +def blob : IO Blob := do + let n ← IO.rand 0 40 + let data ← (List.range n).mapM fun _ => byte + if h : data.length < UInt64.size then return ⟨data, h⟩ else return ⟨[], by decide⟩ + +def u64 : IO UInt64 := do + -- small values exercise the low bytes, large ones the high + if (← IO.rand 0 1) = 0 then return (← IO.rand 0 1000).toUInt64 + else return (← IO.rand 0 (2^64 - 1)).toUInt64 + +def origin : IO Origin := do + match ← IO.rand 0 2 with + | 0 => return .run + | 1 => return .fork (← blob) (← u64) + | _ => return .recovery (← blob) (← u64) + +def event : IO Event := do + match ← IO.rand 0 2 with + | 0 => return .intent (← blob) (← blob) + | 1 => + match ← IO.rand 0 2 with + | 0 => return .decision (.deny (← blob)) + | 1 => return .decision .allow + | _ => return .decision (.spawn (← u64) (← blob)) + | _ => + let code ← byte + let status := if (← IO.rand 0 1) = 0 then WaitStatus.exited code else .signaled code + return .witness status (← blob) (← blob) + +def body : IO Body := do + match ← IO.rand 0 2 with + | 0 => + let report ← blob + let attestation := if (← IO.rand 0 1) = 0 then Attestation.unattested else .snp report + return .report (← origin) (← blob) attestation (← blob) (← blob) + | 1 => return .call (← u64) (← u64) (← event) + | _ => + match ← IO.rand 0 3 with + | 0 => return .exit (.finish (← blob)) + | 1 => return .exit .meter + | 2 => return .exit .limit + | _ => return .exit .timeout + +def record : IO Record := return ⟨← blob, ← u64, ← body⟩ + +/-- A valid encoding, or one corrupted: a byte changed, cut short, or extended. -/ +def recordBytes : IO Bytes := do + let b := (← record).enc + match ← IO.rand 0 3 with + | 0 => return b + | 1 => + let i ← IO.rand 0 (b.length - 1) + return b.set i (← byte) + | 2 => return b.take (← IO.rand 0 (b.length - 1)) + | _ => return b ++ [← byte] + +/-- Each line: the input, then the encoding of what it decodes to, or `-`. -/ +def records (n : Nat) : IO Unit := do + for _ in [0:n] do + let b ← recordBytes + let out := match Record.dec b with + | some r => hex r.enc + | none => "-" + IO.println s!"{hex b} {out}" + +/-- Random spawns and charges from a root. Each line: the operation, Lean's +verdict, then every meter. -/ +def meters (runs ops : Nat) : IO Unit := do + for _ in [0:runs] do + let cap ← IO.rand 1 10 + let mut t := Meter.root cap + IO.println s!"root {cap}" + for _ in [0:ops] do + let (op, next) ← do + if (← IO.rand 0 3) = 0 then + let pa ← IO.rand 0 t.length + let c ← IO.rand 1 10 + pure (s!"spawn {pa} {c}", Meter.spawn t pa c) + else + let q ← IO.rand 0 t.length + pure (s!"charge {q}", Meter.charge t q) + match next with + | some t' => + t := t' + IO.println s!"{op} ok {t.map (·.meter)}" + | none => IO.println s!"{op} refused {t.map (·.meter)}" + +def unhex (s : String) : Option Bytes := + let digit (c : Char) : Option Nat := + if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat) + else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10) else none + let rec go : List Char → Option Bytes + | [] => some [] + | a :: b :: rest => do + let x ← digit a; let y ← digit b + return (x * 16 + y).toUInt8 :: (← go rest) + | [_] => none + go s.toList + +/-- Process `proc`'s window replayed from a log of hex-encoded records, one per +line. Each line out: the span's role, then its text in hex. -/ +def replay (path : String) (boot : String) (proc : Nat) : IO UInt32 := do + let lines := (← IO.FS.readFile path).splitOn "\n" |>.filter (· ≠ "") + let some log := lines.mapM fun l => unhex l >>= Record.dec + | IO.eprintln "a line is not a record"; return 65 + let some b := unhex boot + | IO.eprintln "boot is not hex"; return 64 + if h : b.length < UInt64.size then + match Cead.replay log ⟨b, h⟩ proc.toUInt64 with + | some spans => + for sp in spans do + let role := match sp.role with + | .system => "system" | .user => "user" | .assistant => "assistant" + IO.println s!"{role} {hex sp.text.data}" + return 0 + | none => IO.eprintln "no window for that process"; return 66 + else return 64 + +end Cead.Differential + +def main (args : List String) : IO UInt32 := do + match args with + | ["record", n, seed] => + IO.setRandSeed seed.toNat! + Cead.Differential.records n.toNat! + return 0 + | ["meter", runs, ops, seed] => + IO.setRandSeed seed.toNat! + Cead.Differential.meters runs.toNat! ops.toNat! + return 0 + | ["replay", log, boot, proc] => Cead.Differential.replay log boot proc.toNat! + | _ => + IO.eprintln "usage: differential record COUNT SEED | meter RUNS OPS SEED | replay LOG BOOT PROC" + return 64 diff --git a/spec/Cead/Log.lean b/spec/Cead/Log.lean index 49017d7..93ef860 100644 --- a/spec/Cead/Log.lean +++ b/spec/Cead/Log.lean @@ -23,7 +23,7 @@ def Body.isExit : Body → Bool /-- The boot a report recovers, if it is a recovery. -/ def Body.recovers : Body → Option Blob - | .report (.recovery b _) _ _ => some b + | .report (.recovery b _) .. => some b | _ => none section @@ -58,7 +58,7 @@ sequence. Any other record needs its boot's report, and no recovery of its boot: a recovery fences the boot it recovers. -/ def Admits (log : Log) (r : Record) : Prop := match r.body with - | .report o _ _ => r.seq = 1 ∧ o.Admits log + | .report o .. => r.seq = 1 ∧ o.Admits log | _ => 1 < r.seq ∧ Vouched log r.boot ∧ ¬ Recovered log r.boot instance : Decidable (Admits log r) := by unfold Admits; split <;> infer_instance @@ -71,7 +71,7 @@ def accept (log : Log) (r : Record) : Option Log := /-- The snapshot a fork or recovery booted from. -/ def Body.source : Body → Option (Blob × UInt64) - | .report (.fork b l) _ _ | .report (.recovery b l) _ _ => some (b, l) + | .report (.fork b l) .. | .report (.recovery b l) .. => some (b, l) | _ => none /-- What every log `accept` builds from empty satisfies. -/ @@ -103,7 +103,7 @@ private theorem logged_append (h : Logged log b s) : Logged (log ++ [r]) b s := private theorem recovers_source {x : Record} (h : x.body.recovers = some b) : ∃ l, x.body.source = some (b, l) := by match hb : x.body, h with - | .report (.recovery b' l) _ _, h => + | .report (.recovery b' l) .., h => simp only [Body.recovers, Option.some.injEq] at h; subst h; exact ⟨l, rfl⟩ /-- A recovered boot's report is in the log: the recovery names one of its records. -/ @@ -143,7 +143,7 @@ theorem accept_valid {log' : Log} (hv : Valid log) (h : accept log r = some log' · rename_i hb have : x.body.isReport = false := by unfold Body.isReport; split - · rename_i h; exact absurd h (hb _ _ _) + · rename_i h; exact absurd h (hb _ _ _ _ _) · rfl simp [this, hadm.1] · rw [List.pairwise_append] @@ -165,7 +165,7 @@ theorem accept_valid {log' : Log} (hv : Valid log) (h : accept log r = some log' · simp only [List.mem_singleton] at hx; subst hx unfold Admits at hadm split at hadm - · rename_i o m e hb + · rename_i o _ _ _ _ hb rw [hb] at hs cases o <;> simp only [Body.source, Option.some.injEq, Prod.mk.injEq, reduceCtorEq] at hs all_goals @@ -175,8 +175,8 @@ theorem accept_valid {log' : Log} (hv : Valid log) (h : accept log r = some log' · exact logged_append hadm.2.1 · rename_i hb match hx : x.body, hs with - | .report (.fork _ _) _ _, _ | .report (.recovery _ _) _ _, _ => - exact absurd hx (hb _ _ _) + | .report (.fork _ _) .., _ | .report (.recovery _ _) .., _ => + exact absurd hx (hb _ _ _ _ _) · rw [List.pairwise_append] refine ⟨hv.fenced, by simp, ?_⟩ intro x hx y hy h @@ -188,13 +188,13 @@ theorem accept_valid {log' : Log} (hv : Valid log) (h : accept log r = some log' simp only [List.mem_singleton] at hy; subst hy unfold Admits at hadm split at hadm - · rename_i o m e hb + · rename_i o _ _ _ _ hb cases o <;> simp [Body.recovers, hb] at hyb subst hyb exact hadm.2.2.2 ⟨x, hx, hxb⟩ · rename_i hb match hy : y.body, hyb with - | .report (.recovery _ _) _ _, _ => exact absurd hy (hb _ _ _) + | .report (.recovery _ _) .., _ => exact absurd hy (hb _ _ _ _ _) · intro b hex hrec obtain ⟨x, hx, hxb, hxe⟩ := hex obtain ⟨y, hy, hyr⟩ := hrec @@ -204,20 +204,20 @@ theorem accept_valid {log' : Log} (hv : Valid log) (h : accept log r = some log' simp only [List.mem_singleton] at hyr'; subst hyr' unfold Admits at hadm split at hadm - · rename_i o m e hb + · rename_i o _ _ _ _ hb cases o <;> simp [Body.recovers, hb] at hyr subst hyr exact hadm.2.2.1 ⟨x, hxo, hxb, hxe⟩ · rename_i hb match hyb : y.body, hyr with - | .report (.recovery _ _) _ _, _ => exact absurd hyb (hb _ _ _) + | .report (.recovery _ _) .., _ => exact absurd hyb (hb _ _ _ _ _) · -- r is b's exit record, and b is already recovered simp only [List.mem_singleton] at hxr; subst hxr exact hfresh (hxb ▸ ⟨y, hyo, hyr⟩) · simp only [List.mem_singleton] at hxr hyr' rw [hxr] at hxe; rw [hyr'] at hyr match hb : r.body, hxe, hyr with - | .report (.recovery _ _) _ _, hxe, _ => simp [Body.isExit] at hxe + | .report (.recovery _ _) .., hxe, _ => simp [Body.isExit] at hxe /-- The logs `accept` builds from empty, one record at a time. -/ inductive Accepted : Log → Prop diff --git a/spec/Cead/Meter.lean b/spec/Cead/Meter.lean new file mode 100644 index 0000000..0cfb02a --- /dev/null +++ b/spec/Cead/Meter.lean @@ -0,0 +1,224 @@ +/-! +Meters, from KeyKOS: what a process tree may spend. `spec/cead.tla`'s +`Chargeable`, `Issue`'s charge and property 15 (`WithinMeter`), proved for +every tree and every sequence of spawns and charges. + +A process's number is its index; a child is appended, so its parent's number +is smaller. Every call is charged to each meter from its process up to the +root. +-/ +namespace Cead.Meter + +structure Proc where + parent : Option Nat + /-- The meter it was given. -/ + cap : Nat + /-- What remains of it. -/ + meter : Nat + /-- The calls it made. -/ + calls : Nat + +abbrev Tree := List Proc + +def root (cap : Nat) : Tree := [⟨none, cap, cap, 0⟩] + +/-- `q`, its parent, and so on up to the root. -/ +def chain (t : Tree) (q : Nat) : List Nat := + q :: match t[q]?.bind (·.parent) with + | some pa => if pa < q then chain t pa else [] + | none => [] +termination_by q +decreasing_by omega + +theorem chain_le (t : Tree) (q : Nat) : ∀ a ∈ chain t q, a ≤ q := by + induction q using Nat.strongRecOn with + | _ q ih => + intro a ha + rw [chain] at ha + simp only [List.mem_cons] at ha + rcases ha with rfl | ha + · exact Nat.le_refl _ + · split at ha + · split at ha + · rename_i pa _ hlt; exact Nat.le_of_lt (Nat.lt_of_le_of_lt (ih pa hlt a ha) hlt) + · simp at ha + · simp at ha + +/-- `chain` reads only parents at indices up to `q`: trees agreeing there agree on it. -/ +theorem chain_congr (t t' : Tree) (q : Nat) + (h : ∀ i ≤ q, t'[i]?.bind (·.parent) = t[i]?.bind (·.parent)) : chain t' q = chain t q := by + induction q using Nat.strongRecOn with + | _ q ih => + rw [chain, chain, h q (Nat.le_refl _)] + split + · rename_i pa _ + split + · rename_i hlt + rw [ih pa hlt (fun i hi => h i (by omega))] + · rfl + · rfl + +/-- Every meter from `q` up to the root has a unit left. -/ +def Chargeable (t : Tree) (q : Nat) : Prop := + q < t.length ∧ ∀ a ∈ chain t q, 0 < (t[a]?.map (·.meter)).getD 0 + +instance : Decidable (Chargeable t q) := by unfold Chargeable; infer_instance + +/-- Process `a` after a call by `q`: one unit off its meter if the call is +charged to it, and one more call if it made it. -/ +def bump (t : Tree) (q a : Nat) (x : Proc) : Proc := + { x with meter := if a ∈ chain t q then x.meter - 1 else x.meter, + calls := if a = q then x.calls + 1 else x.calls } + +/-- A call by `q`: one unit from each meter up to the root, or refused. -/ +def charge (t : Tree) (q : Nat) : Option Tree := + if Chargeable t q then some (t.mapIdx (bump t q)) else none + +/-- `agent`: a child of `pa` with meter `cap`. -/ +def spawn (t : Tree) (pa cap : Nat) : Option Tree := + if pa < t.length then some (t ++ [⟨some pa, cap, cap, 0⟩]) else none + +/-- The calls made anywhere in `p`'s subtree: by every process whose chain +passes through `p`. -/ +def spent (t : Tree) (p : Nat) : Nat := + (((List.range t.length).filter fun q => p ∈ chain t q).map + fun q => (t[q]?.map (·.calls)).getD 0).sum + +/-- Every process's remaining meter and its subtree's calls add up to what it +was given. -/ +def Balanced (t : Tree) : Prop := + ∀ p x, t[p]? = some x → x.meter + spent t p = x.cap + +/-- No subtree spends more than its root's meter. -/ +theorem within_meter (h : Balanced t) (hp : t[p]? = some x) : spent t p ≤ x.cap := by + have := h p x hp; omega + +theorem balanced_root (cap : Nat) : Balanced (root cap) := by + intro p x hp + match p, hp with + | 0, hp => + simp only [root, List.getElem?_cons_zero, Option.some.injEq] at hp; subst hp + unfold spent + simp only [root, List.length_singleton, List.range_one, List.filter_cons, List.filter_nil] + split <;> simp + +private theorem sum_bump (l : List Nat) (hl : l.Nodup) (f : Nat → Nat) (q : Nat) : + (l.map fun i => f i + if i = q then 1 else 0).sum = (l.map f).sum + if q ∈ l then 1 else 0 := by + induction l with + | nil => simp + | cons a l ih => + simp only [List.nodup_cons] at hl + simp only [List.map_cons, List.sum_cons, ih hl.2, List.mem_cons] + by_cases ha : a = q + · subst ha; simp [hl.1]; omega + · simp [ha, Ne.symm ha]; omega + +theorem charge_balanced (h : Balanced t) (hc : charge t q = some t') : Balanced t' := by + unfold charge at hc + split at hc + case isFalse => cases hc + rename_i hq + cases hc + have hget : ∀ i, (t.mapIdx (bump t q))[i]? = t[i]?.map (bump t q i) := by + intro i; simp [List.getElem?_mapIdx] + have hchain : ∀ i, chain (t.mapIdx (bump t q)) i = chain t i := by + intro i; apply chain_congr; intro j _; rw [hget j]; cases t[j]? <;> rfl + have hspent : ∀ p, spent (t.mapIdx (bump t q)) p = spent t p + if p ∈ chain t q then 1 else 0 := by + intro p + unfold spent + simp only [List.length_mapIdx, hchain, hget] + have : ∀ i, ((t[i]?.map (bump t q i)).map (·.calls)).getD 0 = + (t[i]?.map (·.calls)).getD 0 + if i = q then 1 else 0 := by + intro i + cases hi : t[i]? with + | none => + simp only [Option.map_none, Option.getD_none] + split + · subst_vars; have := hq.1; simp at hi; omega + · rfl + | some z => simp only [Option.map_some, Option.getD_some, bump]; split <;> simp + simp only [this] + rw [sum_bump _ ((List.nodup_range).filter _)] + congr 1 + simp [hq.1] + intro p x hp + rw [hget p] at hp + cases hy : t[p]? with + | none => rw [hy] at hp; cases hp + | some y => + rw [hy] at hp + simp only [Option.map_some, Option.some.injEq] at hp + subst hp + have hb := h p y hy + rw [hspent p] + by_cases hpq : p ∈ chain t q + · have hm := hq.2 p hpq + simp [hy] at hm + simp [bump, hpq]; omega + · simp [bump, hpq]; omega + +theorem spawn_balanced (h : Balanced t) (hs : spawn t pa cap = some t') : Balanced t' := by + unfold spawn at hs + split at hs + case isFalse => cases hs + rename_i hpa + cases hs + let c : Proc := ⟨some pa, cap, cap, 0⟩ + have hold : ∀ i < t.length, (t ++ [c])[i]? = t[i]? := fun i hi => List.getElem?_append_left hi + have hchain : ∀ i < t.length, chain (t ++ [c]) i = chain t i := by + intro i hi; apply chain_congr; intro j hj; rw [hold j (by omega)] + -- A new process adds no calls, so no subtree's spending changes. + have hspent : ∀ p, spent (t ++ [c]) p = spent t p := by + intro p + unfold spent + rw [List.length_append, List.length_singleton, List.range_succ, List.filter_append, + List.map_append, List.sum_append] + have hnew : ((([t.length].filter fun q => decide (p ∈ chain (t ++ [c]) q)).map + fun q => ((t ++ [c])[q]?.map (·.calls)).getD 0)).sum = 0 := by + simp only [List.filter_cons, List.filter_nil] + split <;> simp [c] + rw [hnew, Nat.add_zero] + congr 1 + rw [List.filter_congr (fun i hi => by rw [hchain i (List.mem_range.mp hi)])] + apply List.map_congr_left + intro i hi + rw [hold i (List.mem_range.mp (List.mem_filter.mp hi).1)] + intro p x hp + rw [hspent p] + by_cases hlt : p < t.length + · rw [hold p hlt] at hp; exact h p x hp + · have hpn : p = t.length := by + have := (List.getElem?_eq_some_iff.mp hp).1; simp at this; omega + subst hpn + rw [List.getElem?_append_right (Nat.le_refl _)] at hp + simp only [Nat.sub_self, List.getElem?_cons_zero, Option.some.injEq] at hp + subst hp + -- Nothing in `t` has the new process in its chain. + have : spent t t.length = 0 := by + unfold spent + rw [List.filter_eq_nil_iff.mpr] + · rfl + · intro i hi hm + have := chain_le t i _ (of_decide_eq_true hm) + have := List.mem_range.mp hi + omega + simp [this] + +/-- The trees a job builds from its root, one spawn or charge at a time. -/ +inductive Reachable : Tree → Prop + | root (cap : Nat) : Reachable (root cap) + | spawn {t t' pa cap} : Reachable t → spawn t pa cap = some t' → Reachable t' + | charge {t t' q} : Reachable t → charge t q = some t' → Reachable t' + +theorem reachable_balanced (hr : Reachable t) : Balanced t := by + induction hr with + | root cap => exact balanced_root cap + | spawn _ hs ih => exact spawn_balanced ih hs + | charge _ hc ih => exact charge_balanced ih hc + +/-- In every tree a job can build, no subtree spends more than its root's +meter: property 15, `WithinMeter`, for every tree size. -/ +theorem reachable_within_meter (hr : Reachable t) (hp : t[p]? = some x) : spent t p ≤ x.cap := + within_meter (reachable_balanced hr) hp + +end Cead.Meter diff --git a/spec/Cead/Oracle.lean b/spec/Cead/Oracle.lean deleted file mode 100644 index 3cab39e..0000000 --- a/spec/Cead/Oracle.lean +++ /dev/null @@ -1,92 +0,0 @@ -import Cead.Record - -/-! -The differential oracle: random inputs through the Lean spec, printed one -per line for `cargo test` to run through the Rust and compare. The bridge is -bytes, the interface itself. --/ -namespace Cead.Oracle - -def hex (b : Bytes) : String := - String.join (b.map fun x => - let s := String.ofList (Nat.toDigits 16 x.toNat) - if s.length = 1 then "0" ++ s else s) - -def byte : IO UInt8 := return (← IO.rand 0 255).toUInt8 - -def blob : IO Blob := do - let n ← IO.rand 0 40 - let data ← (List.range n).mapM fun _ => byte - if h : data.length < UInt64.size then return ⟨data, h⟩ else return ⟨[], by decide⟩ - -def u64 : IO UInt64 := do - -- small values exercise the low bytes, large ones the high - if (← IO.rand 0 1) = 0 then return (← IO.rand 0 1000).toUInt64 - else return (← IO.rand 0 (2^64 - 1)).toUInt64 - -def origin : IO Origin := do - match ← IO.rand 0 2 with - | 0 => return .run - | 1 => return .fork (← blob) (← u64) - | _ => return .recovery (← blob) (← u64) - -def event : IO Event := do - match ← IO.rand 0 2 with - | 0 => return .intent (← blob) - | 1 => - match ← IO.rand 0 2 with - | 0 => return .decision .deny - | 1 => return .decision .allow - | _ => return .decision (.spawn (← u64)) - | _ => - let code ← byte - let status := if (← IO.rand 0 1) = 0 then WaitStatus.exited code else .signaled code - return .witness status (← blob) - -def body : IO Body := do - match ← IO.rand 0 2 with - | 0 => - let report ← blob - let attestation := if (← IO.rand 0 1) = 0 then Attestation.unattested else .snp report - return .report (← origin) (← blob) attestation - | 1 => return .call (← u64) (← u64) (← event) - | _ => - match ← IO.rand 0 3 with - | 0 => return .exit (.finish (← blob)) - | 1 => return .exit .meter - | 2 => return .exit .limit - | _ => return .exit .timeout - -def record : IO Record := return ⟨← blob, ← u64, ← body⟩ - -/-- A valid encoding, or one corrupted: a byte changed, cut short, or extended. -/ -def recordBytes : IO Bytes := do - let b := (← record).enc - match ← IO.rand 0 3 with - | 0 => return b - | 1 => - let i ← IO.rand 0 (b.length - 1) - return b.set i (← byte) - | 2 => return b.take (← IO.rand 0 (b.length - 1)) - | _ => return b ++ [← byte] - -/-- Each line: the input, then the encoding of what it decodes to, or `-`. -/ -def records (n : Nat) : IO Unit := do - for _ in [0:n] do - let b ← recordBytes - let out := match Record.dec b with - | some r => hex r.enc - | none => "-" - IO.println s!"{hex b} {out}" - -end Cead.Oracle - -def main (args : List String) : IO UInt32 := do - match args with - | ["record", n, seed] => - IO.setRandSeed seed.toNat! - Cead.Oracle.records n.toNat! - return 0 - | _ => - IO.eprintln "usage: oracle record COUNT SEED" - return 64 diff --git a/spec/Cead/Record.lean b/spec/Cead/Record.lean index 2fa3e79..6fea472 100644 --- a/spec/Cead/Record.lean +++ b/spec/Cead/Record.lean @@ -24,12 +24,14 @@ inductive Attestation where | snp (report : Blob) deriving DecidableEq -/-- The outcome of checking a call against policy. `spawn` allows an `agent` -call and names the process it starts. -/ +/-- The outcome of checking a call against policy. A deny carries what the +call returned to the model, which ends the call. `spawn` allows an `agent` call and +names the process it starts and that process's query, which opens its +window. -/ inductive Decision where - | deny + | deny (returned : Blob) | allow - | spawn (child : UInt64) + | spawn (child : UInt64) (query : Blob) deriving DecidableEq /-- How a command ended, as `wait(2)` reports it. -/ @@ -38,12 +40,16 @@ inductive WaitStatus where | signaled (signal : UInt8) deriving DecidableEq -/-- One call's record, sharing its id and process with the call's other two. -/ +/-- One call's record, sharing its id and process with the call's other two. +Together they hold what the call added to its process's window. -/ inductive Event where - | intent (command : Blob) + /-- The model's whole turn, and the command the harness took from it. -/ + | intent (turn : Blob) (command : Blob) | decision (decision : Decision) - /-- `output` is the digest of the command's whole output. -/ - | witness (status : WaitStatus) (output : Blob) + /-- `output` is the digest of the command's whole output; `returned` what the + call returned to the model: the output if it fit the bound, else where it + spilled. -/ + | witness (status : WaitStatus) (output : Blob) (returned : Blob) deriving DecidableEq /-- Why a boot ended: the root process's status. Only `finish` has a reply, @@ -56,7 +62,10 @@ inductive Exit where deriving DecidableEq inductive Body where + /-- `prompt` is the pinned prompt and `query` the root's: its window opens + with them. -/ | report (origin : Origin) (measurement : Blob) (attestation : Attestation) + (prompt : Blob) (query : Blob) /-- `proc` is the boot's number for the process that made the call. -/ | call (id : UInt64) (proc : UInt64) (event : Event) | exit (exit : Exit) @@ -95,13 +104,13 @@ def attestation : Codec Attestation := (by intro e; cases e <;> rfl) private def DecisionT : Fin 3 → Type - | 0 => Unit | 1 => Unit | 2 => UInt64 + | 0 => Blob | 1 => Unit | 2 => UInt64 × Blob def decision : Codec Decision := - iso (tagged 3 (by decide) DecisionT fun | 0 => unit | 1 => unit | 2 => u64) - (fun | ⟨0, _⟩ => .deny | ⟨1, _⟩ => .allow | ⟨2, c⟩ => .spawn c) - (fun | .deny => ⟨0, ()⟩ | .allow => ⟨1, ()⟩ | .spawn c => ⟨2, c⟩) - (by rintro ⟨i, x⟩; match i, x with | 0, () => rfl | 1, () => rfl | 2, _ => rfl) + iso (tagged 3 (by decide) DecisionT fun | 0 => blob | 1 => unit | 2 => pair u64 blob) + (fun | ⟨0, m⟩ => .deny m | ⟨1, _⟩ => .allow | ⟨2, (c, q)⟩ => .spawn c q) + (fun | .deny m => ⟨0, m⟩ | .allow => ⟨1, ()⟩ | .spawn c q => ⟨2, (c, q)⟩) + (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, () => rfl | 2, (_, _) => rfl) (by intro d; cases d <;> rfl) private def u8 : Codec UInt8 := @@ -120,13 +129,17 @@ def waitStatus : Codec WaitStatus := (by intro e; cases e <;> rfl) private def EventT : Fin 3 → Type - | 0 => Blob | 1 => Decision | 2 => WaitStatus × Blob + | 0 => Blob × Blob | 1 => Decision | 2 => WaitStatus × Blob × Blob def event : Codec Event := - iso (tagged 3 (by decide) EventT fun | 0 => blob | 1 => decision | 2 => pair waitStatus blob) - (fun | ⟨0, c⟩ => .intent c | ⟨1, d⟩ => .decision d | ⟨2, (w, o)⟩ => .witness w o) - (fun | .intent c => ⟨0, c⟩ | .decision d => ⟨1, d⟩ | .witness w o => ⟨2, (w, o)⟩) - (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, _ => rfl | 2, (_, _) => rfl) + iso (tagged 3 (by decide) EventT + fun | 0 => pair blob blob | 1 => decision | 2 => pair waitStatus (pair blob blob)) + (fun | ⟨0, (t, c)⟩ => .intent t c | ⟨1, d⟩ => .decision d + | ⟨2, (w, o, m)⟩ => .witness w o m) + (fun | .intent t c => ⟨0, (t, c)⟩ | .decision d => ⟨1, d⟩ + | .witness w o m => ⟨2, (w, o, m)⟩) + (by rintro ⟨i, x⟩ + match i, x with | 0, (_, _) => rfl | 1, _ => rfl | 2, (_, _, _) => rfl) (by intro e; cases e <;> rfl) private def ExitT : Fin 4 → Type @@ -140,16 +153,18 @@ def exit : Codec Exit := (by intro e; cases e <;> rfl) private def BodyT : Fin 3 → Type - | 0 => Origin × Blob × Attestation | 1 => UInt64 × UInt64 × Event | 2 => Exit + | 0 => Origin × Blob × Attestation × Blob × Blob | 1 => UInt64 × UInt64 × Event | 2 => Exit def body : Codec Body := iso (tagged 3 (by decide) BodyT - fun | 0 => pair origin (pair blob attestation) | 1 => pair u64 (pair u64 event) - | 2 => exit) - (fun | ⟨0, (o, m, a)⟩ => .report o m a | ⟨1, (i, p, e)⟩ => .call i p e | ⟨2, x⟩ => .exit x) - (fun | .report o m a => ⟨0, (o, m, a)⟩ | .call i p e => ⟨1, (i, p, e)⟩ | .exit x => ⟨2, x⟩) + fun | 0 => pair origin (pair blob (pair attestation (pair blob blob))) + | 1 => pair u64 (pair u64 event) | 2 => exit) + (fun | ⟨0, (o, m, a, p, q)⟩ => .report o m a p q | ⟨1, (i, p, e)⟩ => .call i p e + | ⟨2, x⟩ => .exit x) + (fun | .report o m a p q => ⟨0, (o, m, a, p, q)⟩ | .call i p e => ⟨1, (i, p, e)⟩ + | .exit x => ⟨2, x⟩) (by rintro ⟨i, x⟩ - match i, x with | 0, (_, _, _) => rfl | 1, (_, _, _) => rfl | 2, _ => rfl) + match i, x with | 0, (_, _, _, _, _) => rfl | 1, (_, _, _) => rfl | 2, _ => rfl) (by intro b; cases b <;> rfl) def record : Codec Record := diff --git a/spec/Cead/Window.lean b/spec/Cead/Window.lean new file mode 100644 index 0000000..4aa9175 --- /dev/null +++ b/spec/Cead/Window.lean @@ -0,0 +1,98 @@ +import Cead.Log + +/-! +A process's window, replayed from the log. The log holds every byte a window +holds (the pinned prompt and query to open it, each call's turn and what it +returned), so what the model saw on any call is a function of the records. +The harness assembles its windows by the same definition; the differential +test compares them, and the gateway's own record of each request is a +second, independent check. +-/ +namespace Cead + +inductive Role where + | system + | user + | assistant +deriving DecidableEq + +/-- One span of a window. -/ +structure Span where + role : Role + text : Blob +deriving DecidableEq + +/-- The pinned prompt, then the query, then each completed call: the model's +turn and what it returned. -/ +def window (prompt query : Blob) (calls : List (Blob × Blob)) : List Span := + ⟨.system, prompt⟩ :: ⟨.user, query⟩ :: + calls.flatMap fun (turn, returned) => [⟨.assistant, turn⟩, ⟨.user, returned⟩] + +/-- A window only grows at its end: each call's window begins with the +previous call's, byte for byte. -/ +theorem window_prefix (prompt query : Blob) (calls more : List (Blob × Blob)) : + window prompt query calls <+: window prompt query (calls ++ more) := by + simp [window, List.flatMap_append] + +/-- The root is process 0; a spawning decision numbers the rest. -/ +def Root : UInt64 := 0 + +section Replay +variable (log : Log) (b : Blob) + +/-- The pinned prompt and the root's query, from boot `b`'s report. -/ +def reportOf : Option (Blob × Blob) := + log.findSome? fun r => + if r.boot = b then + match r.body with + | .report _ _ _ prompt query => some (prompt, query) + | _ => none + else none + +/-- Process `p`'s query: the root's from the report, any other's from the +decision that spawned it. -/ +def queryOf (p : UInt64) : Option Blob := + if p = Root then (reportOf log b).map (·.2) + else log.findSome? fun r => + if r.boot = b then + match r.body with + | .call _ _ (.decision (.spawn c q)) => if c = p then some q else none + | _ => none + else none + +/-- Call `i`'s turn and what it returned, once the log holds both. -/ +def callOf (i : UInt64) : Option (Blob × Blob) := do + let turn ← log.findSome? fun r => + if r.boot = b then + match r.body with + | .call j _ (.intent t _) => if j = i then some t else none + | _ => none + else none + let returned ← log.findSome? fun r => + if r.boot = b then + match r.body with + | .call j _ (.decision (.deny x)) | .call j _ (.witness _ _ x) => + if j = i then some x else none + | _ => none + else none + pure (turn, returned) + +/-- The ids of process `p`'s calls, in the order it made them. -/ +def callIds (p : UInt64) : List UInt64 := + let ids := log.filterMap fun r => + if r.boot = b then + match r.body with + | .call i q (.intent ..) => if q = p then some i else none + | _ => none + else none + ids.mergeSort (· ≤ ·) + +/-- Process `p`'s window as the log replays it: its opening, then its +completed calls in order. -/ +def replay (p : UInt64) : Option (List Span) := do + let (prompt, _) ← reportOf log b + let query ← queryOf log b p + pure (window prompt query ((callIds log b p).filterMap (callOf log b))) + +end Replay +end Cead diff --git a/spec/cead.tla b/spec/cead.tla index 3b4c2b9..d41e3b4 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -65,6 +65,12 @@ Live == {"ready", "running", "blocked"} \* as `child`, so the log holds the process tree. The exit record carries \* id 0, why the boot ended, and the root process's reply if it finished: \* the answer, signed. +\* The records also carry every byte a window holds, so the log alone +\* replays what the model saw on each call: 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; and the record that +\* ends a call (a deny, or the witness) what the call returned to it. The +\* spec abstracts all of these as `body`. Record == [boot : Boots, seq : 1..MaxSeq, id : 0..MaxId, type : CallTypes \cup {"report", "exit"}, body : Commands \cup Reasons \cup Origins, key : Signers, diff --git a/spec/lakefile.toml b/spec/lakefile.toml index 6e1bc5b..6ba4ee8 100644 --- a/spec/lakefile.toml +++ b/spec/lakefile.toml @@ -5,5 +5,5 @@ defaultTargets = ["Cead"] name = "Cead" [[lean_exe]] -name = "oracle" -root = "Cead.Oracle" +name = "differential" +root = "Cead.Differential" From a06b1f7d8cc2ec0e40c360a886bfdc61f143f42f Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:39:06 -0600 Subject: [PATCH 08/19] Skeleton: one type per noun, one signature per action, every body todo!() Co-Authored-By: Claude Opus 5.5 (1M context) --- src/host.rs | 197 +++++++++++++++++++++ src/machine.rs | 460 +++++++++++++++++++++++++++++++++++++++++++++++++ src/main.rs | 37 +++- src/record.rs | 122 +++++++++++++ 4 files changed, 815 insertions(+), 1 deletion(-) create mode 100644 src/host.rs create mode 100644 src/machine.rs create mode 100644 src/record.rs diff --git a/src/host.rs b/src/host.rs new file mode 100644 index 0000000..44340e7 --- /dev/null +++ b/src/host.rs @@ -0,0 +1,197 @@ +//! The host: the operator's side. Boots machines, keeps the log, relays +//! inference. Trusted for availability only. + +/// `cead run`: one job, from manifest to answer. +pub(crate) mod job { + use std::path::PathBuf; + use std::process::ExitCode; + + /// The one file that pins a machine by content. Owned by the job; dropped + /// when it ends. + pub(crate) struct Manifest { + kernel: PathBuf, + image: PathBuf, + model: String, + limits: Limits, + } + + /// Caps on one process, set when it is spawned and inherited as a copy. + pub(crate) struct Limits { + calls: u32, + window: usize, + bound: usize, + wall: std::time::Duration, + depth: u32, + meter: u64, + } + + /// A manifest that does not load. + pub(crate) struct BadManifest(String); + + impl Manifest { + pub(crate) fn load(path: &std::path::Path) -> Result { + todo!() + } + } + + /// Boots the machine, keeps its records, relays its inference, and returns + /// the root's reply on stdout once the log holds the exit record. The exit + /// code is the outcome. + pub(crate) fn run(manifest: Manifest, query: Vec, context: Vec) -> ExitCode { + todo!() + } +} + +/// The log: every boot's records, held outside the machine. `spec/cead.tla`'s +/// `Arrive` and `spec/Cead/Log.lean`'s `accept`. +pub(crate) mod log { + use crate::record::{Boot, Record, Signature, Signed}; + use std::collections::{BTreeSet, HashMap}; + use std::fs::File; + use std::path::PathBuf; + + /// Who guarantees the header's assumptions: the processor, or the host. + pub(crate) enum Mode { + Attested, + TrustedHost, + } + + /// A record whose signature checked against its boot's key and, for a + /// report, whose attestation checked for the mode. The only kind `accept` + /// takes. + pub(crate) struct Verified { + record: Record, + bytes: Vec, + signature: Signature, + } + + /// A record signed by no one it names, or attested wrongly for the mode. + pub(crate) struct Forged; + + impl Verified { + pub(crate) fn verify(signed: Signed, mode: &Mode) -> Result { + todo!() + } + } + + /// One JSON-lines file per boot, append-only. Owned by the operator's `cead` + /// for the life of the job. + pub(crate) struct Log { + dir: PathBuf, + boots: HashMap, + } + + /// What the log knows of one boot: its file and the facts `accept` asks. + struct BootLog { + file: File, + seqs: BTreeSet, + exited: bool, + recovered: bool, + } + + /// Why the log kept nothing: `Admits` in `spec/Cead/Log.lean`, case by case. + pub(crate) enum Refused { + /// Its place in the boot's sequence is taken: first wins. + Taken, + /// A report not first in its sequence, or a record before its report. + OutOfPlace, + /// A record whose boot's report the log does not hold. + Unvouched, + /// A fork or recovery naming a record the log does not hold. + Unrooted, + /// A recovery of a boot that exited or is already recovered. + Settled, + /// A record of a boot a recovery has fenced. + Fenced, + } + + impl Log { + pub(crate) fn open(dir: PathBuf) -> std::io::Result { + todo!() + } + + /// Keeps the record, or says why not. Keeping it acknowledges it. + pub(crate) fn accept(&mut self, record: Verified) -> Result<(), Refused> { + todo!() + } + } +} + +/// The VMM: Cloud Hypervisor, driven as a child process. +pub(crate) mod vmm { + use std::path::PathBuf; + use std::process::Child; + + /// Booted, report not yet in the log. + pub(crate) struct Booting; + /// The log holds the report: init runs the harness. + pub(crate) struct Up; + + /// One boot of one machine, from the VMM starting it to eviction. Owns the + /// VMM process; dropping it evicts the machine. + pub(crate) struct Machine { + vmm: Child, + vsock: PathBuf, + state: S, + } + + impl Machine { + /// `Boot`: the VMM starts the kernel with the task image, the query and + /// the context. + pub(crate) fn boot( + manifest: &super::job::Manifest, + query: &[u8], + context: &[u8], + ) -> std::io::Result> { + todo!() + } + + /// `Start`: the log holds the report. + pub(crate) fn start(self) -> Machine { + todo!() + } + } + + impl Machine { + /// `Evict`: the host's hard kill, whatever state the boot is in. + pub(crate) fn evict(self) { + todo!() + } + } + + impl Machine { + /// `Leave`: the log holds the exit record; the machine is gone. + pub(crate) fn leave(self) { + todo!() + } + } +} + +/// The gateway: holds the model's credentials, which never enter the machine, +/// and relays each inference to Bedrock. +pub(crate) mod gateway { + use std::fs::File; + + /// Owns the AWS credentials and the record of every request it relays: a + /// second account of each window, independent of the log. + pub(crate) struct Gateway { + credentials: Credentials, + requests: File, + } + + /// AWS credentials, read on the host. Never serialized, never sent. + pub(crate) struct Credentials { + access_key: String, + secret_key: String, + session_token: Option, + region: String, + } + + impl Gateway { + /// Signs a request from the machine with SigV4, sends it, records it, + /// and returns the response. + pub(crate) fn relay(&mut self, request: &[u8]) -> std::io::Result> { + todo!() + } + } +} diff --git a/src/machine.rs b/src/machine.rs new file mode 100644 index 0000000..f0de7ff --- /dev/null +++ b/src/machine.rs @@ -0,0 +1,460 @@ +//! The machine: init, the harness and the model's processes, inside one boot. + +/// init: PID 1 for the whole boot. The boot's key is made here and never +/// leaves this process. +pub(crate) mod init { + use crate::record::{Boot, Signature}; + use std::fs::File; + use std::path::PathBuf; + use std::process::Child; + + /// The boot's signing key. Owned by init alone: never cloned, never sent, + /// never in the harness, which init starts by exec so no copy of this + /// memory reaches it. Dropped, and zeroed, when the boot ends. + pub(crate) struct Key([u8; 32]); + + impl Key { + /// A fresh key for a fresh boot. + pub(crate) fn generate() -> Key { + todo!() + } + + /// The public half, which names the boot. + pub(crate) fn boot(&self) -> Boot { + todo!() + } + + pub(crate) fn sign(&self, bytes: &[u8]) -> Signature { + todo!() + } + } + + /// What init mounts for the model: the task image as root, the context as + /// a file, a directory for spills. Owned by init; the harness gets paths. + pub(crate) struct View { + root: PathBuf, + context: PathBuf, + spill: PathBuf, + } + + /// init's state: the key, the stream to the log over vsock, and the + /// harness once started. + pub(crate) struct Init { + key: Key, + log: File, + harness: Option, + } + + impl Init { + /// Makes the key, signs and sends the report, and waits for the log to + /// acknowledge it: nothing runs before the log holds the report. + pub(crate) fn boot() -> std::io::Result { + todo!() + } + + /// Assembles the view (mounts, policy, the context file). + pub(crate) fn assemble(&mut self) -> std::io::Result { + todo!() + } + + /// Forks and execs `/proc/self/exe harness`, then signs what it sends + /// and forwards the log's acknowledgments, until it exits. If it exits + /// without its exit record acknowledged, the machine powers off with + /// none: the boot is unknown. + pub(crate) fn serve(self, view: View) -> ! { + todo!() + } + } + + /// The pinned prompt, rendered from what was mounted. + pub(crate) fn prompt(view: &View) -> Vec { + todo!() + } +} + +/// The harness: the model's kernel. One signature per action of +/// `spec/cead.tla`'s layers 1 and 3. +pub(crate) mod harness { + use super::engine::{Engine, Turn}; + use super::meter::Meters; + use super::process::{Process, Status}; + use super::shell::Ran; + use crate::host::job::Limits; + use crate::record::{Body, Boot, CallId, ProcId}; + use std::fs::File; + use std::time::Instant; + + /// The harness's end of init's signing pipe. Numbers each record, so a + /// boot's sequence has no gaps by construction. Owned by the harness. + pub(crate) struct Signer { + pipe: File, + boot: Boot, + next: u64, + } + + impl Signer { + /// Numbers the body and hands it to init to sign and send; returns + /// its place in the sequence. + pub(crate) fn send(&mut self, body: Body) -> std::io::Result { + todo!() + } + + /// Blocks until the log has acknowledged the record at `seq`. + pub(crate) fn acknowledged(&mut self, seq: u64) -> std::io::Result<()> { + todo!() + } + } + + /// Why a live process was ended by the harness rather than by its reply. + pub(crate) enum Exhausted { + Meter, + Limit, + } + + /// Every process of the boot, their meters, and the channels to init and + /// the engine. Owned by the harness process; dropped when the boot exits. + pub(crate) struct Harness { + signer: Signer, + engine: Engine, + procs: Vec, + meters: Meters, + next_call: u64, + limits: Limits, + started: Instant, + } + + impl Harness { + /// Starts the root process over the view init assembled. + pub(crate) fn start(signer: Signer, engine: Engine, limits: Limits) -> Harness { + todo!() + } + + /// `Dispatch`: a ready process gets a processor; its window goes to + /// the engine, and its turn comes back. + pub(crate) fn dispatch(&mut self, p: ProcId) -> std::io::Result { + todo!() + } + + /// `Issue`: the turn has a command. Charges every meter up to the + /// root, sends the intent, and blocks the process on its decision. + pub(crate) fn issue( + &mut self, + p: ProcId, + turn: Vec, + command: Vec, + ) -> Result { + todo!() + } + + /// `Decide`: once the log holds the intent, checks the call against + /// policy and sends the decision. Deny returns to the model; allow + /// starts the command (`agent` spawns, `kill` ends a child's tree). + pub(crate) fn decide(&mut self, call: CallId) -> std::io::Result<()> { + todo!() + } + + /// `Witness`: the command ended; sends the witness with what the call + /// returned, and the process is ready again. + pub(crate) fn witness(&mut self, call: CallId, ran: Ran) -> std::io::Result<()> { + todo!() + } + + /// `Finish`: the turn has no command. The process ends; its reply is + /// its stdout; its live descendants are killed. + pub(crate) fn finish(&mut self, p: ProcId, reply: Vec) { + todo!() + } + + /// `Exhaust`: the process cannot pay for its call, or hit a limit. + pub(crate) fn exhaust(&mut self, p: ProcId, why: Exhausted) { + todo!() + } + + /// `Timeout`: the job's wall time is spent; the root ends, killing the + /// tree. + pub(crate) fn timeout(&mut self) { + todo!() + } + + /// `ReapChild`: an ended child is reaped; a parent's foreground + /// `agent` waiting on it can end. + pub(crate) fn reap_child(&mut self, q: ProcId) { + todo!() + } + + /// `Reap`: the root has ended and every command is witnessed. Sends + /// the exit record; the harness is done. + pub(crate) fn reap(self) -> std::io::Result { + todo!() + } + + /// The cycle: dispatch, then issue, finish or exhaust, until `reap`. + pub(crate) fn run(self) -> std::io::Result { + todo!() + } + } +} + +/// A model's process, as the harness holds it. +pub(crate) mod process { + use super::shell::Shell; + use super::window::Window; + use crate::record::{CallId, ProcId}; + use std::path::PathBuf; + + /// What a process may do to state. A child's rights never exceed its + /// parent's. + pub(crate) struct Rights { + read: Vec, + write: Vec, + } + + /// A child asked for more than its parent holds: rights amplification, + /// which attenuation forbids. + pub(crate) struct Amplification; + + impl Rights { + pub(crate) fn attenuate(&self, to: Rights) -> Result { + todo!() + } + } + + /// What a blocked process waits on: property 18 of the spec, by + /// construction. Each holds the model's turn, which enters the window + /// with what the call returns. + pub(crate) enum Blocked { + /// Its intent, until the log holds the record at `seq` and the + /// harness decides on `command`. + Deciding { + call: CallId, + seq: u64, + turn: Vec, + command: Vec, + }, + /// Its command, until it ends. + Running { call: CallId, turn: Vec }, + /// Its foreground `agent`, until the child it spawned is reaped. + Waiting { + call: CallId, + turn: Vec, + child: ProcId, + }, + } + + /// Why a process ended. + pub(crate) enum Status { + /// It replied without a command; the reply is its stdout. + Finish(Vec), + Meter, + Limit, + Timeout, + /// Killed by an ancestor, or when one ended. + Killed { by: ProcId }, + } + + pub(crate) enum State { + Ready, + Running, + Blocked(Blocked), + Zombie(Status), + Reaped, + } + + /// One process: its place in the tree, its limits' counters, its window + /// and shell. Owned by the harness's table; its shell and cgroup go when + /// it is reaped. + pub(crate) struct Process { + id: ProcId, + parent: Option, + depth: u32, + calls: u32, + rights: Rights, + state: State, + window: Window, + shell: Shell, + } +} + +/// Meters, from KeyKOS. Mirrors `spec/Cead/Meter.lean`: `charge` and `spawn` +/// are its definitions, and the differential test holds them to it. +pub(crate) mod meter { + use crate::record::ProcId; + + /// One process's meter: what it was given, what remains, what it spent. + struct Metered { + parent: Option, + cap: u64, + meter: u64, + calls: u64, + } + + /// Every process's meter, indexed by process number. Owned by the harness. + pub(crate) struct Meters(Vec); + + /// Some meter from the process up to the root is spent. + pub(crate) struct Spent; + + /// A spawn under a process that does not exist. + pub(crate) struct NoParent; + + impl Meters { + pub(crate) fn root(cap: u64) -> Meters { + todo!() + } + + /// A child of `parent` with meter `cap`, numbered next. + pub(crate) fn spawn(&mut self, parent: ProcId, cap: u64) -> Result { + todo!() + } + + /// A call by `q`: one unit from every meter up to the root, or none. + pub(crate) fn charge(&mut self, q: ProcId) -> Result<(), Spent> { + todo!() + } + } +} + +/// A process's window. Mirrors `spec/Cead/Window.lean`: it only grows at its +/// end, and the log replays it. +pub(crate) mod window { + use crate::record::{Boot, ProcId, Record}; + + pub(crate) enum Role { + System, + User, + Assistant, + } + + /// One span of a window. + pub(crate) struct Span { + role: Role, + text: Vec, + } + + /// The pinned prompt, the query, then each call's turn and what it + /// returned. Owned by its process; dropped when the process is reaped. + pub(crate) struct Window { + spans: Vec, + len: usize, + limit: usize, + } + + /// The next span would pass the window limit: the process ends with + /// `limit`. + pub(crate) struct Full; + + impl Window { + pub(crate) fn open(prompt: Vec, query: Vec, limit: usize) -> Window { + todo!() + } + + /// Appends one call: the model's turn and what the call returned. + pub(crate) fn push(&mut self, turn: Vec, returned: Vec) -> Result<(), Full> { + todo!() + } + + pub(crate) fn spans(&self) -> &[Span] { + todo!() + } + } + + /// Process `proc`'s window as the log's records replay it. + pub(crate) fn replay(records: &[Record], boot: &Boot, proc: ProcId) -> Option> { + todo!() + } +} + +/// What a call returns to the model: the output whole, or where it spilled. +pub(crate) mod bounded { + use crate::record::WaitStatus; + use std::path::{Path, PathBuf}; + + /// Output admitted to the window only if it fits the bound; otherwise + /// none of it, and the model reads the spill file like any other state. + pub(crate) enum Bounded { + Fits(Vec), + Spilled { path: PathBuf, size: u64 }, + } + + impl Bounded { + /// Admits `output` whole if it fits `bound`, else writes it under + /// `spill`. + pub(crate) fn admit(output: Vec, bound: usize, spill: &Path) -> std::io::Result { + todo!() + } + + /// The bytes the call returns: the exit status, then the output or + /// the spill's path and size. + pub(crate) fn returned(&self, status: &WaitStatus) -> Vec { + todo!() + } + } +} + +/// A process's shell: the model's interface to the kernel. +pub(crate) mod shell { + use crate::record::WaitStatus; + use std::process::Child; + + /// A command that ended: how, and everything it wrote. + pub(crate) struct Ran { + status: WaitStatus, + output: Vec, + } + + /// One shell per process, persistent across its calls. Owned by the + /// process; killed with it. + pub(crate) struct Shell { + child: Child, + } + + impl Shell { + pub(crate) fn spawn() -> std::io::Result { + todo!() + } + + /// Runs one command to its end. + pub(crate) fn run(&mut self, command: &[u8]) -> std::io::Result { + todo!() + } + } +} + +/// The engine as the machine reaches it: over vsock, through the host's +/// gateway. +pub(crate) mod engine { + use super::window::Window; + use std::fs::File; + + /// What the model wrote. + pub(crate) enum Turn { + /// The whole turn, and the command taken from it. + Command { turn: Vec, command: Vec }, + /// No command: the process's reply. + Reply(Vec), + } + + /// The machine's stream to the gateway. Holds no credential. + pub(crate) struct Engine { + vsock: File, + } + + impl Engine { + /// Sends the window, returns the model's turn. + pub(crate) fn infer(&mut self, window: &Window) -> std::io::Result { + todo!() + } + } +} + +/// `agent`: the call cead adds, run by a model's shell. +pub(crate) mod agent { + use std::process::ExitCode; + + /// Asks the harness, over a descriptor it inherited, to spawn a child with + /// this query and stdin as its slice; writes the child's reply to stdout. + /// The exit code says how the child ended. + pub(crate) fn agent(query: Vec) -> ExitCode { + todo!() + } +} diff --git a/src/main.rs b/src/main.rs index f328e4d..25246be 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1 +1,36 @@ -fn main() {} +//! cead: one binary, its role chosen at start. On the host, the operator's +//! `cead run`. In the machine, `cead init` as PID 1, the harness it execs, +//! and `agent`, the call cead adds, reached by its name on PATH. + +mod host; +mod machine; +mod record; + +use std::process::ExitCode; + +/// What this process is, from its argv. Owns nothing; dropped once dispatched. +enum Role { + /// `cead run QUERY`: one job, context on stdin, the answer on stdout. + Run { query: Vec }, + /// `cead init`: PID 1 in the machine, for the whole boot. + Init, + /// `cead harness`: exec'd by init, so it starts without init's key. + Harness, + /// `agent QUERY`: a model's process asking the harness for a child. + Agent { query: Vec }, +} + +/// argv that names no role, or names one wrongly. Owns the message for stderr. +struct Usage(String); + +impl Role { + /// Chooses the role from argv: `agent` by the name it was run as, the rest + /// by subcommand. + fn parse(args: Vec) -> Result { + todo!() + } +} + +fn main() -> ExitCode { + todo!() +} diff --git a/src/record.rs b/src/record.rs new file mode 100644 index 0000000..f88dc75 --- /dev/null +++ b/src/record.rs @@ -0,0 +1,122 @@ +//! Records: what the machine signs and the log keeps. Mirrors `spec/cead.tla`'s +//! `Record` and `spec/Cead/Record.lean`; the encoding is the Lean codec's, byte +//! for byte, which the differential test checks. + +/// A boot, named by its public key: the key that signs its records. +pub(crate) struct Boot([u8; 32]); + +/// A SHA-256 digest. +pub(crate) struct Digest([u8; 32]); + +/// An Ed25519 signature over a record's encoding. +pub(crate) struct Signature([u8; 64]); + +/// A call's number within its boot, shared by its intent, decision and witness. +pub(crate) struct CallId(u64); + +/// A process's number within its boot; the root is 0, a spawn numbers the rest. +pub(crate) struct ProcId(u64); + +/// One record: its boot, its place in the boot's sequence, what it says. +/// Owned by whoever holds it: the harness until sent, then the log. +pub(crate) struct Record { + boot: Boot, + seq: u64, + body: Body, +} + +/// What a record says. Together a boot's records hold every byte its windows +/// held, so the log replays them. +pub(crate) enum Body { + /// The boot's first record. `prompt` and `query` open the root's window. + Report { + origin: Origin, + measurement: Vec, + attestation: Attestation, + prompt: Vec, + query: Vec, + }, + /// One of a call's three records, naming the process that made it. + Call { + id: CallId, + proc: ProcId, + event: Event, + }, + /// The boot's last record: why it ended. + Exit(Exit), +} + +/// What started a boot. A fork or recovery names its snapshot: that boot and +/// its last record. +pub(crate) enum Origin { + Run, + Fork { boot: Boot, last: u64 }, + Recovery { boot: Boot, last: u64 }, +} + +/// What the processor signed about a boot; `Unattested` in trusted-host mode. +pub(crate) enum Attestation { + Unattested, + /// A TSM report from SEV-SNP, binding the boot's key to the measurement. + Snp(Vec), +} + +/// A call's record. +pub(crate) enum Event { + /// The model's whole turn, and the command the harness took from it. + Intent { turn: Vec, command: Vec }, + Decision(Decision), + /// The command ended: how, the digest of its whole output, and what the + /// call returned to the model. + Witness { + status: WaitStatus, + output: Digest, + returned: Vec, + }, +} + +/// The outcome of checking a call against policy. +pub(crate) enum Decision { + /// Refused; `returned` is what the model gets back, which ends the call. + Deny { returned: Vec }, + Allow, + /// Allowed `agent`: the process it starts and that process's query. + Spawn { child: ProcId, query: Vec }, +} + +/// How a command ended, as `wait(2)` reports it. +pub(crate) enum WaitStatus { + Exited(u8), + Signaled(u8), +} + +/// Why a boot ended: its root process's status. Only a finish has a reply. +pub(crate) enum Exit { + /// The root replied without a command; the digest of its reply, the answer. + Finish { reply: Digest }, + Meter, + Limit, + Timeout, +} + +/// Bytes that are no record's encoding. +pub(crate) struct Malformed; + +impl Record { + /// The bytes a boot's key signs: canonical, so a signature names one record. + pub(crate) fn encode(&self) -> Vec { + todo!() + } + + /// The record these bytes encode, if they encode exactly one. + pub(crate) fn decode(bytes: &[u8]) -> Result { + todo!() + } +} + +/// A record's encoding and its boot's signature over it, as it travels from +/// the machine to the log. +pub(crate) struct Signed { + bytes: Vec, + signature: Signature, +} From 07d6ca165bf2e9e7ec7fb7936515c9e1e6a243ae Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:43:07 -0600 Subject: [PATCH 09/19] Give every noun its home in code, and write down the method as practiced here Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 91 ++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 54 insertions(+), 37 deletions(-) diff --git a/CODE.md b/CODE.md index f6d94b5..87824cb 100644 --- a/CODE.md +++ b/CODE.md @@ -6,10 +6,11 @@ Push every invariant you can into the types, cover the rest with tests, and spen Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TLA+ specifies the system (processes and how they interleave), Lean specifies a core (a pure function and its properties), Rust is the system. -1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable. +0. **Scope.** Numbered questions, one recommendation each; facts fetched before asking; each decision written into the PR description. +1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable, never looser than the system: a behaviour the spec allows and the system cannot have is a wall, so the spec changes. 2. **Slice.** A PR takes a slice of the spec. Its dependencies are probed while scoping; findings go in a PR comment, the probe is never committed. 3. **Core.** Ask what a skeptic has to trust. Every pure function on that path (what signs, verifies, admits or renders) gets its Lean spec first, green before any Rust, and a differential test; elsewhere, a pure function gets one when a property is stated. -4. **Skeleton.** One commit of types, signatures, private fields and one doc comment per item (what it owns, when it drops); bodies are `todo!()`; the type gate is green. It is the spec of custody. It mirrors the spec: variables become fields, states become variants or typestates, each action becomes one signature. +4. **Skeleton.** Its shape (modules, types, custody) is agreed first. Then one commit of types, signatures, private fields and one doc comment per item (what it owns, when it drops); bodies are `todo!()`; the type gate is green. It is the spec of custody. It mirrors the spec: variables become fields, states become variants or typestates, each action becomes one signature. Its commit comment carries the table from spec to code, the tie nothing checks; every type gets a row in Vocabulary. 5. **Fill.** Later commits change bodies. A signature that moves is learning: say why in the commit comment. A new capability is drift: it belongs to another PR. A fill commit names the action it implements. - Each placeholder is fillable from its own file plus the public types of what it imports. If more is required, move the boundary. @@ -28,56 +29,69 @@ Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TL # Vocabulary -Every noun has one home in code: a type, a module or crate, or a binary. A noun may precede its home; the PR that first needs it builds it. No home without a noun. +Every noun has one home in code: a type, a module, or a subcommand. A noun may precede its home; the PR that first needs it builds it. No home without a noun, and no type without a row here. Paths are from `src/`; a type's errors and states sit in its row. -| Noun | Meaning | Home | +| Noun | Meaning | In code | |---|---|---| +| agent | The call cead adds: spawns a child process with a query and a slice. | `machine::agent::agent`, run as `agent` | +| amplification | A child asking for more rights than its parent holds; attenuation forbids it (ocap). | `machine::process::Amplification` | +| attestation | What the processor signs about a boot: SNP's TSM report, or none in trusted-host mode. | `record::Attestation` | | authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | | availability | The job runs and ends. The host guarantees it, and can always deny it. | `spec/cead.tla` | -| boot | One life of a machine's kernel, from the VMM starting it to eviction, with one key. Its records are numbered from its report, each signed with that key. **Complete** when the log holds its records through its exit record with no gap; otherwise **unknown** (crash, host kill, lost report). Linux's `boot_id`. | `spec/cead.tla` | -| bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | -| call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `agent`; every other call is a well-known CLI. | | +| blocked | A process waiting: on its intent's decision, its command's end, or a foreground child. Holds the model's turn until the call returns. | `machine::process::Blocked` | +| boot | One life of a machine's kernel, from the VMM starting it to eviction, with one key, which names it. Its records are numbered from its report, each signed with that key. **Complete** when the log holds its records through its exit record with no gap; otherwise **unknown** (crash, host kill, lost report). Linux's `boot_id`. | `record::Boot`; `spec/cead.tla` | +| bounded | What a call returns: the output whole if it fits the bound, else none of it and where it **spilled**, a file the model reads like any other state. Nothing is truncated. | `machine::bounded::Bounded` | +| call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. Its intent, decision and witness share its id. | `record::CallId` | | call table | The system call table: the toolset. | | -| cead | The project and the operator's binary. | crate and binary `cead` | -| command | What the model writes: shell over the core plus the task image. | | -| confidentiality | No one outside the machine can read it. Guaranteed by the processor on an attested boot; claimed by no one in trusted-host mode. | | -| console | The operator's interface to manifests, machines and their state: `cead` with no verb. Its verbs drive the scheduler. | | +| cead | The project and its one binary, its role chosen at start: `run` on the host; `init`, `harness` and `agent` in the machine. | crate and binary `cead`; `main::Role`, `Usage` | +| command | What the model writes: shell over the core plus the task image. The harness takes it from the model's turn. | bytes in `record::Event::Intent` | +| confidentiality | No one outside the machine can read it. Guaranteed by the processor on an attested boot; claimed by no one in trusted-host mode. | | +| console | The operator's interface to manifests, machines and their state: `cead` with no verb. Its verbs drive the scheduler. | | | core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | -| decision | The outcome of checking a call against policy: allow or deny. | | +| decision | The outcome of checking a call against policy: deny (with what the call returns), allow, or spawn (allowed `agent`, naming the child and its query). | `record::Decision` | | descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child process's is **attenuated** when it is spawned, and never grows; revoking it is `kill`. | | -| engine | Executes the weights and signs what it produces: the model's counterpart to the machine. vLLM by default. | | -| evict | Dispose at any tier: window span, KV block, process, machine. | | +| engine | Executes the weights and signs what it produces: the model's counterpart to the machine. Reached from the machine over vsock, through the gateway. | `machine::engine::Engine` | +| evict | Dispose at any tier: window span, KV block, process, machine. | `host::vmm::Machine::evict` | | executed | What the kernel ran: the truth the records record. | `spec/cead.tla` | -| harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, sequences records for init to sign. | | -| host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | | -| init | PID 1 in the machine, for the whole boot. Makes the boot's key and never lets it go; signs every record. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, forks the harness. If the harness dies, the boot ends with no exit record: unknown. | | +| gateway | The host's relay to a hosted engine: holds the credentials the machine never sees, signs each request, and records it, a second account of every window. | `host::gateway::Gateway`, `Credentials` | +| harness | The model's kernel, exec'd by init so it starts without the key. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, numbers records for init to sign. One method per spec action. | `machine::harness::Harness`; `cead harness` | +| host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | `host` | +| init | PID 1 in the machine, for the whole boot. Makes the boot's key and never lets it go; signs every record. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, forks and execs the harness. If the harness dies, the boot ends with no exit record: unknown. | `machine::init::Init`; `cead init` | | integrity | The log says only what the machine signed, in the machine's order. Guaranteed by each boot's key signing every record, in a numbered sequence rooted in its report. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | -| job | One query's work: a root process and its tree. Started by `cead run`. Spans one boot, or more through recovery. | | -| limit | A cap on one process: window size, bound, calls, wall time, depth. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | -| log | Every boot's records, held outside the machine. Records in transit can be lost, delayed, replayed or forged; the log keeps only what the processor or a boot's key signed. A complete boot's records are all it did; an unknown boot's are true but may be partial. A job's boots link through their reports. One writer per boot: never consensus. | `spec/cead.tla` | -| machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model, booted in a microVM by a VMM. | | -| manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | -| meter | What a process tree may spend, from KeyKOS. A child process's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent caps a child's meter in `agent`'s argv and revokes it with `kill`. What it counts is manifest policy. | | -| model | The machine's user: weights running on an engine, reached by the harness over TLS that every host between only relays. The machine holds only a job-scoped token, never a long-lived key. | | +| job | One query's work: a root process and its tree. Started by `cead run`. Spans one boot, or more through recovery. | `host::job::run` | +| key | A boot's signing key: made by init, never copied out of it. | `machine::init::Key` | +| limit | A cap on one process: calls, window, bound, wall time, depth. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | `host::job::Limits`; `machine::harness::Exhausted` | +| log | Every boot's records, held outside the machine: one append-only JSON-lines file per boot. Records in transit can be lost, delayed, replayed or forged; the log keeps only what the processor or a boot's key signed, and says why it refuses the rest. A complete boot's records are all it did, and replay its every window; an unknown boot's are true but may be partial. A job's boots link through their reports. One writer per boot: never consensus. | `host::log::Log`, `BootLog`, `Refused`; `spec/Cead/Log.lean` | +| machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model, booted in a microVM by a VMM. Booting until the log holds its report, then up. | `host::vmm::Machine`; `machine` | +| manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | `host::job::Manifest`, `BadManifest` | +| meter | What a process tree may spend, from KeyKOS. A child process's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent caps a child's meter in `agent`'s argv and revokes it with `kill`. What it counts is manifest policy. | `machine::meter::Meters`, `Metered`, `Spent`, `NoParent`; `spec/Cead/Meter.lean` | +| model | The machine's user: weights running on an engine, reached by the harness over TLS that every host between only relays. The machine holds no credential. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | -| pinned | The part of the window eviction never touches: the system prompt. | | +| pinned | The part of the window eviction never touches: the system prompt, rendered from what was mounted. | `machine::init::prompt` | | policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | -| process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `agent` below. It ends when the model replies without a command; its reply is its stdout. Each `agent` child is spawned in its own PID namespace, so `kill` reaches only its descendants. | | -| processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. A boot sees the model's processors as virtual, like vCPUs; how the engine shares its GPU among them (batching) is its scheduler's. | | -| query | The argv of `run` or `agent`, commit-message sized. Anything longer is context. | | -| report | A boot's first record: the processor's signed statement binding the boot's key, and for a fork or recovery the snapshot it booted from (that boot and its last record), to the manifest's measurement. Unsigned in trusted-host mode. Linux's TSM report. | `spec/cead.tla` | -| record | One entry the machine signs for the log, Linux audit's unit. Types: report, intent, decision, witness, exit; the exit record carries the root process's reply. A call's intent, decision and witness share its id, as Linux audit's records share an event. | `spec/cead.tla` | -| rights | What a call may do to state: read, write. | | +| process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Ready, running, blocked, zombie, reaped. Started by `run` at depth 0 (process 0), `agent` below. It ends when the model replies without a command; its reply is its stdout. Each `agent` child is spawned in its own PID namespace, so `kill` reaches only its descendants. | `machine::process::Process`, `State`, `Status`; `record::ProcId` | +| processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. A boot sees the model's processors as virtual, like vCPUs; how the engine shares its GPU among them (batching) is its scheduler's. | | +| query | The argv of `run` or `agent`, commit-message sized; it opens its process's window. Anything longer is context, a file. | bytes in `record::Body::Report`, `Decision::Spawn` | +| report | A boot's first record: binds the boot's key to the manifest's measurement, names what started it (run, or the snapshot a fork or recovery booted from), and carries the pinned prompt and the root's query. Signed by the processor on an attested boot. Linux's TSM report. | `record::Body::Report`, `Origin`; `spec/cead.tla` | +| record | One entry the machine signs for the log, Linux audit's unit, canonically encoded. Types: report, intent (the model's turn and its command), decision, witness (how the command ended, its output's digest, what the call returned), exit (why the boot ended; the root's reply digest on a finish). A call's three share its id and process. | `record::Record`, `Body`, `Event`, `Exit`, `Signed`, `Signature`, `Digest`, `Malformed`; `spec/Cead/Record.lean` | +| rights | What a call may do to state: read, write. | `machine::process::Rights` | | ring | A privilege layer: model processes; harness and tracer; host. | | -| scheduler | Decides what runs where: machines on hosts (Kubernetes), requests on engines (Dynamo). Trusted for availability only; needs consensus once there is more than one. | | +| scheduler | Decides what runs where: machines on hosts (Kubernetes), requests on engines (Dynamo). Trusted for availability only; needs consensus once there is more than one. | | +| shell | A process's interface to the kernel: one per process, persistent across its calls. | `machine::shell::Shell`, `Ran` | +| signer | The harness's end of init's signing pipe: numbers each record, so a boot's sequence has no gaps. | `machine::harness::Signer` | | slice | The bytes a child receives on stdin, sealed. | | -| snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). A recovery **fences** the boot it recovers: the log keeps none of that boot's records after it. | | +| snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). A recovery **fences** the boot it recovers: the log keeps none of that boot's records after it. | `record::Origin` | +| span | One piece of a window: system, user or assistant text. | `machine::window::Span`, `Role` | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | -| VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same records; only an attested boot's report is signed. | | -| weights | The model's program text, pinned by hash in the manifest. Part of the version vector. | | -| window | The context the model can address now. A cache over state. | | +| turn | What the model writes on one call: a command, or a reply without one. Logged whole. | `machine::engine::Turn` | +| verified | A record whose signature checked against its boot's key, and whose attestation checked for the mode: the only kind the log accepts. | `host::log::Verified`, `Forged`, `Mode` | +| view | What init mounts for the model: the task image as root, the context as a file, a directory for spills. | `machine::init::View` | +| VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same records; only an attested boot's report is signed. | `host::vmm` | +| wait status | How a command ended, as `wait(2)` reports it: exited with a code, or signaled. | `record::WaitStatus` | +| weights | The model's program text, pinned by hash in the manifest. Part of the version vector. | | +| window | The context the model can address now: the pinned prompt, the query, then each call's turn and what it returned. Only grows; ending the process when full. The log replays it. A cache over state. | `machine::window::Window`, `Full`; `spec/Cead/Window.lean` | # Rust @@ -117,11 +131,14 @@ Everything else (fields, structs and enums, most traits, invariants like `len - Modules are `spec/.tla` with `.cfg`; the system spec is `spec/cead.tla`. A layer whose state multiplies another's gets its own cfg over the same module (`spec/tree.cfg`). The commit line records the TLA+ tools version and the bounds it passed at. - A PR that changes a protocol re-runs TLC, by hand until CI is demanded. -- Every property has a mutation TLC catches. +- Every property has a mutation TLC catches, run with a cfg holding only that property so the catch is its own. - Committed cfgs run in about a minute; larger bounds are one-off runs recorded in the PR. - **spec**: a formula over behaviours of a state machine. **action**: one transition; one signature. **invariant**: what every reachable state satisfies; what TLC checks. **instance**: the bounds TLC searched; a proof only up to them. # Lean - Lean 4 via elan, toolchain pinned in `lean-toolchain`, one lake project in `spec/`. `lake build` green before the Rust it specifies. +- No `sorry`. Proofs rest on `propext`, `Quot.sound` and `Classical.choice` only, checked with `#print axioms`: no native code (`bv_decide`, `native_decide`), so the kernel checks everything. +- Every guard has a mutation: replaced by `True`, it breaks a proof. +- `spec/Cead/Differential.lean` builds `differential`, the Lean half of every differential test. - **spec**: an executable definition. **theorem**: a property proved of it. **differential test**: random inputs through spec and Rust, outputs compared in `cargo test`; the only tie between them. From f5b34dead7f58120a999cce9dd83e69904b1245e Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:45:30 -0600 Subject: [PATCH 10/19] Fill record: the Lean codec byte for byte, held to it by the differential test Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/Cead/Codec.lean | 18 ++ spec/Cead/Differential.lean | 17 +- spec/Cead/Log.lean | 14 +- spec/Cead/Record.lean | 32 ++-- spec/Cead/Window.lean | 2 +- src/record.rs | 320 +++++++++++++++++++++++++++++++++++- 6 files changed, 374 insertions(+), 29 deletions(-) diff --git a/spec/Cead/Codec.lean b/spec/Cead/Codec.lean index 17af16b..fcf87d5 100644 --- a/spec/Cead/Codec.lean +++ b/spec/Cead/Codec.lean @@ -21,6 +21,12 @@ structure Blob where fits : data.length < UInt64.size deriving DecidableEq +/-- Exactly `n` bytes: a key or a digest. -/ +structure Fixed (n : Nat) where + data : Bytes + len : data.length = n +deriving DecidableEq + namespace Codec /-- Equal encodings mean equal values. -/ @@ -139,6 +145,18 @@ def blob : Codec Blob where simp [List.length_take, Nat.min_eq_left ‹n.toNat ≤ r.length›, List.append_assoc, this] · cases hd +/-- The `n` bytes as they are: their length says where they end. -/ +def fixed (n : Nat) : Codec (Fixed n) where + enc b := b.data + dec bs := if h : n ≤ bs.length then some (⟨bs.take n, by simp; omega⟩, bs.drop n) else none + dec_enc b rest := by + have := b.len + simp [this, List.take_left', List.drop_left'] + enc_dec bs b rest hd := by + split at hd + · cases hd; simp + · cases hd + def pair (ca : Codec α) (cb : Codec β) : Codec (α × β) where enc p := ca.enc p.1 ++ cb.enc p.2 dec bs := do diff --git a/spec/Cead/Differential.lean b/spec/Cead/Differential.lean index 8055a76..d27bd88 100644 --- a/spec/Cead/Differential.lean +++ b/spec/Cead/Differential.lean @@ -20,6 +20,11 @@ def blob : IO Blob := do let data ← (List.range n).mapM fun _ => byte if h : data.length < UInt64.size then return ⟨data, h⟩ else return ⟨[], by decide⟩ +/-- A key or digest: 32 random bytes. -/ +def fixed32 : IO (Fixed 32) := do + let data ← (List.range 32).mapM fun _ => byte + if h : data.length = 32 then return ⟨data, h⟩ else return ⟨List.replicate 32 0, by simp⟩ + def u64 : IO UInt64 := do -- small values exercise the low bytes, large ones the high if (← IO.rand 0 1) = 0 then return (← IO.rand 0 1000).toUInt64 @@ -28,8 +33,8 @@ def u64 : IO UInt64 := do def origin : IO Origin := do match ← IO.rand 0 2 with | 0 => return .run - | 1 => return .fork (← blob) (← u64) - | _ => return .recovery (← blob) (← u64) + | 1 => return .fork (← fixed32) (← u64) + | _ => return .recovery (← fixed32) (← u64) def event : IO Event := do match ← IO.rand 0 2 with @@ -42,7 +47,7 @@ def event : IO Event := do | _ => let code ← byte let status := if (← IO.rand 0 1) = 0 then WaitStatus.exited code else .signaled code - return .witness status (← blob) (← blob) + return .witness status (← fixed32) (← blob) def body : IO Body := do match ← IO.rand 0 2 with @@ -53,12 +58,12 @@ def body : IO Body := do | 1 => return .call (← u64) (← u64) (← event) | _ => match ← IO.rand 0 3 with - | 0 => return .exit (.finish (← blob)) + | 0 => return .exit (.finish (← fixed32)) | 1 => return .exit .meter | 2 => return .exit .limit | _ => return .exit .timeout -def record : IO Record := return ⟨← blob, ← u64, ← body⟩ +def record : IO Record := return ⟨← fixed32, ← u64, ← body⟩ /-- A valid encoding, or one corrupted: a byte changed, cut short, or extended. -/ def recordBytes : IO Bytes := do @@ -122,7 +127,7 @@ def replay (path : String) (boot : String) (proc : Nat) : IO UInt32 := do | IO.eprintln "a line is not a record"; return 65 let some b := unhex boot | IO.eprintln "boot is not hex"; return 64 - if h : b.length < UInt64.size then + if h : b.length = 32 then match Cead.replay log ⟨b, h⟩ proc.toUInt64 with | some spans => for sp in spans do diff --git a/spec/Cead/Log.lean b/spec/Cead/Log.lean index 93ef860..1d56971 100644 --- a/spec/Cead/Log.lean +++ b/spec/Cead/Log.lean @@ -22,20 +22,20 @@ def Body.isExit : Body → Bool | _ => false /-- The boot a report recovers, if it is a recovery. -/ -def Body.recovers : Body → Option Blob +def Body.recovers : Body → Option Boot | .report (.recovery b _) .. => some b | _ => none section variable (log : Log) -def Logged (b : Blob) (s : UInt64) : Prop := ∃ r ∈ log, r.boot = b ∧ r.seq = s +def Logged (b : Boot) (s : UInt64) : Prop := ∃ r ∈ log, r.boot = b ∧ r.seq = s -def Vouched (b : Blob) : Prop := Logged log b 1 +def Vouched (b : Boot) : Prop := Logged log b 1 -def Exited (b : Blob) : Prop := ∃ r ∈ log, r.boot = b ∧ r.body.isExit +def Exited (b : Boot) : Prop := ∃ r ∈ log, r.boot = b ∧ r.body.isExit -def Recovered (b : Blob) : Prop := ∃ r ∈ log, r.body.recovers = some b +def Recovered (b : Boot) : Prop := ∃ r ∈ log, r.body.recovers = some b instance : Decidable (Logged log b s) := by unfold Logged; infer_instance instance : Decidable (Vouched log b) := by unfold Vouched; infer_instance @@ -70,7 +70,7 @@ def accept (log : Log) (r : Record) : Option Log := if ¬ Logged log r.boot r.seq ∧ Admits log r then some (log ++ [r]) else none /-- The snapshot a fork or recovery booted from. -/ -def Body.source : Body → Option (Blob × UInt64) +def Body.source : Body → Option (Boot × UInt64) | .report (.fork b l) .. | .report (.recovery b l) .. => some (b, l) | _ => none @@ -95,7 +95,7 @@ theorem valid_nil : Valid [] := by constructor <;> simp [Exited] section Proofs -variable {log : Log} {r : Record} {b : Blob} {s : UInt64} +variable {log : Log} {r : Record} {b : Boot} {s : UInt64} private theorem logged_append (h : Logged log b s) : Logged (log ++ [r]) b s := by obtain ⟨x, hx, h⟩ := h; exact ⟨x, by simp [hx], h⟩ diff --git a/spec/Cead/Record.lean b/spec/Cead/Record.lean index 6fea472..13bda2f 100644 --- a/spec/Cead/Record.lean +++ b/spec/Cead/Record.lean @@ -9,12 +9,18 @@ namespace Cead open Codec +/-- A boot, named by its public key, which signs its records. -/ +abbrev Boot := Fixed 32 + +/-- A SHA-256 digest. -/ +abbrev Digest := Fixed 32 + /-- What started a boot. A fork or recovery names its snapshot: that boot and its last record. -/ inductive Origin where | run - | fork (boot : Blob) (last : UInt64) - | recovery (boot : Blob) (last : UInt64) + | fork (boot : Boot) (last : UInt64) + | recovery (boot : Boot) (last : UInt64) deriving DecidableEq /-- What the processor signed about a boot. `unattested` is what trusted-host @@ -49,13 +55,13 @@ inductive Event where /-- `output` is the digest of the command's whole output; `returned` what the call returned to the model: the output if it fit the bound, else where it spilled. -/ - | witness (status : WaitStatus) (output : Blob) (returned : Blob) + | witness (status : WaitStatus) (output : Digest) (returned : Blob) deriving DecidableEq /-- Why a boot ended: the root process's status. Only `finish` has a reply, and the record carries its digest. -/ inductive Exit where - | finish (reply : Blob) + | finish (reply : Digest) | meter | limit | timeout @@ -74,20 +80,20 @@ deriving DecidableEq /-- `boot` is the boot's public key, which signs the record; `seq` its place in the boot's sequence, the report first. -/ structure Record where - boot : Blob + boot : Boot seq : UInt64 body : Body deriving DecidableEq namespace Codec -def blobU64 : Codec (Blob × UInt64) := pair blob u64 +def bootU64 : Codec (Boot × UInt64) := pair (fixed 32) u64 private def OriginT : Fin 3 → Type - | 0 => Unit | 1 => Blob × UInt64 | 2 => Blob × UInt64 + | 0 => Unit | 1 => Boot × UInt64 | 2 => Boot × UInt64 def origin : Codec Origin := - iso (tagged 3 (by decide) OriginT fun | 0 => unit | 1 => blobU64 | 2 => blobU64) + iso (tagged 3 (by decide) OriginT fun | 0 => unit | 1 => bootU64 | 2 => bootU64) (fun | ⟨0, _⟩ => .run | ⟨1, (b, l)⟩ => .fork b l | ⟨2, (b, l)⟩ => .recovery b l) (fun | .run => ⟨0, ()⟩ | .fork b l => ⟨1, (b, l)⟩ | .recovery b l => ⟨2, (b, l)⟩) (by rintro ⟨i, x⟩; match i, x with | 0, () => rfl | 1, (_, _) => rfl | 2, (_, _) => rfl) @@ -129,11 +135,11 @@ def waitStatus : Codec WaitStatus := (by intro e; cases e <;> rfl) private def EventT : Fin 3 → Type - | 0 => Blob × Blob | 1 => Decision | 2 => WaitStatus × Blob × Blob + | 0 => Blob × Blob | 1 => Decision | 2 => WaitStatus × Digest × Blob def event : Codec Event := iso (tagged 3 (by decide) EventT - fun | 0 => pair blob blob | 1 => decision | 2 => pair waitStatus (pair blob blob)) + fun | 0 => pair blob blob | 1 => decision | 2 => pair waitStatus (pair (fixed 32) blob)) (fun | ⟨0, (t, c)⟩ => .intent t c | ⟨1, d⟩ => .decision d | ⟨2, (w, o, m)⟩ => .witness w o m) (fun | .intent t c => ⟨0, (t, c)⟩ | .decision d => ⟨1, d⟩ @@ -143,10 +149,10 @@ def event : Codec Event := (by intro e; cases e <;> rfl) private def ExitT : Fin 4 → Type - | 0 => Blob | 1 => Unit | 2 => Unit | 3 => Unit + | 0 => Digest | 1 => Unit | 2 => Unit | 3 => Unit def exit : Codec Exit := - iso (tagged 4 (by decide) ExitT fun | 0 => blob | 1 => unit | 2 => unit | 3 => unit) + iso (tagged 4 (by decide) ExitT fun | 0 => fixed 32 | 1 => unit | 2 => unit | 3 => unit) (fun | ⟨0, r⟩ => .finish r | ⟨1, _⟩ => .meter | ⟨2, _⟩ => .limit | ⟨3, _⟩ => .timeout) (fun | .finish r => ⟨0, r⟩ | .meter => ⟨1, ()⟩ | .limit => ⟨2, ()⟩ | .timeout => ⟨3, ()⟩) (by rintro ⟨i, x⟩; match i, x with | 0, _ => rfl | 1, () => rfl | 2, () => rfl | 3, () => rfl) @@ -168,7 +174,7 @@ def body : Codec Body := (by intro b; cases b <;> rfl) def record : Codec Record := - iso (pair blob (pair u64 body)) + iso (pair (fixed 32) (pair u64 body)) (fun (b, s, x) => ⟨b, s, x⟩) (fun r => (r.boot, r.seq, r.body)) (fun _ => rfl) diff --git a/spec/Cead/Window.lean b/spec/Cead/Window.lean index 4aa9175..2085b48 100644 --- a/spec/Cead/Window.lean +++ b/spec/Cead/Window.lean @@ -38,7 +38,7 @@ theorem window_prefix (prompt query : Blob) (calls more : List (Blob × Blob)) : def Root : UInt64 := 0 section Replay -variable (log : Log) (b : Blob) +variable (log : Log) (b : Boot) /-- The pinned prompt and the root's query, from boot `b`'s report. -/ def reportOf : Option (Blob × Blob) := diff --git a/src/record.rs b/src/record.rs index f88dc75..cc8ab61 100644 --- a/src/record.rs +++ b/src/record.rs @@ -3,22 +3,28 @@ //! for byte, which the differential test checks. /// A boot, named by its public key: the key that signs its records. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct Boot([u8; 32]); /// A SHA-256 digest. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct Digest([u8; 32]); /// An Ed25519 signature over a record's encoding. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct Signature([u8; 64]); /// A call's number within its boot, shared by its intent, decision and witness. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct CallId(u64); /// A process's number within its boot; the root is 0, a spawn numbers the rest. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct ProcId(u64); /// One record: its boot, its place in the boot's sequence, what it says. /// Owned by whoever holds it: the harness until sent, then the log. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct Record { boot: Boot, seq: u64, @@ -27,6 +33,7 @@ pub(crate) struct Record { /// What a record says. Together a boot's records hold every byte its windows /// held, so the log replays them. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) enum Body { /// The boot's first record. `prompt` and `query` open the root's window. Report { @@ -48,6 +55,7 @@ pub(crate) enum Body { /// What started a boot. A fork or recovery names its snapshot: that boot and /// its last record. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) enum Origin { Run, Fork { boot: Boot, last: u64 }, @@ -55,6 +63,7 @@ pub(crate) enum Origin { } /// What the processor signed about a boot; `Unattested` in trusted-host mode. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) enum Attestation { Unattested, /// A TSM report from SEV-SNP, binding the boot's key to the measurement. @@ -62,6 +71,7 @@ pub(crate) enum Attestation { } /// A call's record. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) enum Event { /// The model's whole turn, and the command the harness took from it. Intent { turn: Vec, command: Vec }, @@ -76,6 +86,7 @@ pub(crate) enum Event { } /// The outcome of checking a call against policy. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) enum Decision { /// Refused; `returned` is what the model gets back, which ends the call. Deny { returned: Vec }, @@ -85,12 +96,14 @@ pub(crate) enum Decision { } /// How a command ended, as `wait(2)` reports it. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) enum WaitStatus { Exited(u8), Signaled(u8), } /// Why a boot ended: its root process's status. Only a finish has a reply. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) enum Exit { /// The root replied without a command; the digest of its reply, the answer. Finish { reply: Digest }, @@ -100,23 +113,326 @@ pub(crate) enum Exit { } /// Bytes that are no record's encoding. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct Malformed; impl Record { /// The bytes a boot's key signs: canonical, so a signature names one record. pub(crate) fn encode(&self) -> Vec { - todo!() + let mut out = Vec::new(); + self.write(&mut out); + out } /// The record these bytes encode, if they encode exactly one. pub(crate) fn decode(bytes: &[u8]) -> Result { - todo!() + let mut r = Reader(bytes); + let record = Record::read(&mut r)?; + if r.0.is_empty() { Ok(record) } else { Err(Malformed) } + } +} + +// The codec of `spec/Cead/Record.lean`: every value is self-delimiting. A +// variant is a tag byte, then its fields in order; a u64 is eight bytes +// big-endian; bytes are a u64 length, then the bytes; a key or digest is its +// 32 bytes. + +struct Reader<'a>(&'a [u8]); + +impl<'a> Reader<'a> { + fn take(&mut self, n: usize) -> Result<&'a [u8], Malformed> { + if self.0.len() < n { + return Err(Malformed); + } + let (head, rest) = self.0.split_at(n); + self.0 = rest; + Ok(head) + } + + fn tag(&mut self) -> Result { + Ok(self.take(1)?[0]) + } + + fn u64(&mut self) -> Result { + let mut b = [0; 8]; + b.copy_from_slice(self.take(8)?); + Ok(u64::from_be_bytes(b)) + } + + fn bytes(&mut self) -> Result, Malformed> { + let n = usize::try_from(self.u64()?).map_err(|_| Malformed)?; + Ok(self.take(n)?.to_vec()) + } + + fn fixed(&mut self) -> Result<[u8; 32], Malformed> { + let mut b = [0; 32]; + b.copy_from_slice(self.take(32)?); + Ok(b) + } +} + +fn put_u64(out: &mut Vec, n: u64) { + out.extend_from_slice(&n.to_be_bytes()); +} + +fn put_bytes(out: &mut Vec, b: &[u8]) { + put_u64(out, b.len() as u64); + out.extend_from_slice(b); +} + +impl Record { + fn write(&self, out: &mut Vec) { + out.extend_from_slice(&self.boot.0); + put_u64(out, self.seq); + self.body.write(out); + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(Record { boot: Boot(r.fixed()?), seq: r.u64()?, body: Body::read(r)? }) + } +} + +impl Body { + fn write(&self, out: &mut Vec) { + match self { + Body::Report { origin, measurement, attestation, prompt, query } => { + out.push(0); + origin.write(out); + put_bytes(out, measurement); + attestation.write(out); + put_bytes(out, prompt); + put_bytes(out, query); + } + Body::Call { id, proc, event } => { + out.push(1); + put_u64(out, id.0); + put_u64(out, proc.0); + event.write(out); + } + Body::Exit(exit) => { + out.push(2); + exit.write(out); + } + } + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(match r.tag()? { + 0 => Body::Report { + origin: Origin::read(r)?, + measurement: r.bytes()?, + attestation: Attestation::read(r)?, + prompt: r.bytes()?, + query: r.bytes()?, + }, + 1 => Body::Call { id: CallId(r.u64()?), proc: ProcId(r.u64()?), event: Event::read(r)? }, + 2 => Body::Exit(Exit::read(r)?), + _ => return Err(Malformed), + }) + } +} + +impl Origin { + fn write(&self, out: &mut Vec) { + let (tag, snapshot) = match self { + Origin::Run => (0, None), + Origin::Fork { boot, last } => (1, Some((boot, last))), + Origin::Recovery { boot, last } => (2, Some((boot, last))), + }; + out.push(tag); + if let Some((boot, last)) = snapshot { + out.extend_from_slice(&boot.0); + put_u64(out, *last); + } + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(match r.tag()? { + 0 => Origin::Run, + 1 => Origin::Fork { boot: Boot(r.fixed()?), last: r.u64()? }, + 2 => Origin::Recovery { boot: Boot(r.fixed()?), last: r.u64()? }, + _ => return Err(Malformed), + }) + } +} + +impl Attestation { + fn write(&self, out: &mut Vec) { + match self { + Attestation::Unattested => out.push(0), + Attestation::Snp(report) => { + out.push(1); + put_bytes(out, report); + } + } + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(match r.tag()? { + 0 => Attestation::Unattested, + 1 => Attestation::Snp(r.bytes()?), + _ => return Err(Malformed), + }) + } +} + +impl Event { + fn write(&self, out: &mut Vec) { + match self { + Event::Intent { turn, command } => { + out.push(0); + put_bytes(out, turn); + put_bytes(out, command); + } + Event::Decision(decision) => { + out.push(1); + decision.write(out); + } + Event::Witness { status, output, returned } => { + out.push(2); + status.write(out); + out.extend_from_slice(&output.0); + put_bytes(out, returned); + } + } + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(match r.tag()? { + 0 => Event::Intent { turn: r.bytes()?, command: r.bytes()? }, + 1 => Event::Decision(Decision::read(r)?), + 2 => Event::Witness { + status: WaitStatus::read(r)?, + output: Digest(r.fixed()?), + returned: r.bytes()?, + }, + _ => return Err(Malformed), + }) + } +} + +impl Decision { + fn write(&self, out: &mut Vec) { + match self { + Decision::Deny { returned } => { + out.push(0); + put_bytes(out, returned); + } + Decision::Allow => out.push(1), + Decision::Spawn { child, query } => { + out.push(2); + put_u64(out, child.0); + put_bytes(out, query); + } + } + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(match r.tag()? { + 0 => Decision::Deny { returned: r.bytes()? }, + 1 => Decision::Allow, + 2 => Decision::Spawn { child: ProcId(r.u64()?), query: r.bytes()? }, + _ => return Err(Malformed), + }) + } +} + +impl WaitStatus { + fn write(&self, out: &mut Vec) { + let (tag, n) = match self { + WaitStatus::Exited(code) => (0, code), + WaitStatus::Signaled(signal) => (1, signal), + }; + out.extend_from_slice(&[tag, *n]); + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(match r.tag()? { + 0 => WaitStatus::Exited(r.tag()?), + 1 => WaitStatus::Signaled(r.tag()?), + _ => return Err(Malformed), + }) + } +} + +impl Exit { + fn write(&self, out: &mut Vec) { + match self { + Exit::Finish { reply } => { + out.push(0); + out.extend_from_slice(&reply.0); + } + Exit::Meter => out.push(1), + Exit::Limit => out.push(2), + Exit::Timeout => out.push(3), + } + } + + fn read(r: &mut Reader<'_>) -> Result { + Ok(match r.tag()? { + 0 => Exit::Finish { reply: Digest(r.fixed()?) }, + 1 => Exit::Meter, + 2 => Exit::Limit, + 3 => Exit::Timeout, + _ => return Err(Malformed), + }) } } /// A record's encoding and its boot's signature over it, as it travels from /// the machine to the log. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct Signed { bytes: Vec, signature: Signature, } + +#[cfg(test)] +mod tests { + use super::Record; + use std::process::Command; + + /// Runs the Lean half of the differential test (`spec/Cead/Differential.lean`), + /// building it first. Needs `lake` on PATH (elan's `~/.elan/bin`). + pub(crate) fn differential(args: &[&str]) -> String { + let spec = concat!(env!("CARGO_MANIFEST_DIR"), "/spec"); + let built = Command::new("lake").args(["build", "differential"]).current_dir(spec).status(); + assert!(built.expect("lake runs").success(), "lake build differential"); + let out = Command::new(format!("{spec}/.lake/build/bin/differential")) + .args(args) + .output() + .expect("differential runs"); + assert!(out.status.success()); + String::from_utf8(out.stdout).expect("differential prints text") + } + + pub(crate) fn unhex(s: &str) -> Vec { + (0..s.len()) + .step_by(2) + .map(|i| u8::from_str_radix(&s[i..i + 2], 16).expect("hex")) + .collect() + } + + /// Every encoding Lean accepts, Rust decodes and re-encodes to the same + /// bytes; every one Lean rejects (a byte changed, cut short, extended), Rust + /// rejects too. + #[test] + fn codec_matches_lean() { + let lines = differential(&["record", "5000", "1"]); + let (mut valid, mut rejected) = (0, 0); + for line in lines.lines() { + let (input, lean) = line.split_once(' ').expect("two fields"); + let bytes = unhex(input); + match (Record::decode(&bytes), lean) { + (Err(_), "-") => rejected += 1, + (Ok(_), "-") => panic!("Rust decodes what Lean rejects: {line}"), + (Ok(r), expected) => { + assert_eq!(r.encode(), unhex(expected), "{line}"); + valid += 1; + } + (Err(_), _) => panic!("Lean decodes what Rust rejects: {line}"), + } + } + assert!(valid > 1000 && rejected > 1000, "{valid} valid, {rejected} rejected"); + } +} From b3a35d666bbcf5feff148de61b615a167f8e18a9 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:46:53 -0600 Subject: [PATCH 11/19] Fill meter: the Lean definitions, held to them by the differential test Co-Authored-By: Claude Opus 5.5 (1M context) --- src/machine.rs | 90 ++++++++++++++++++++++++++++++++++++++++++++++---- src/record.rs | 15 ++++++++- 2 files changed, 97 insertions(+), 8 deletions(-) diff --git a/src/machine.rs b/src/machine.rs index f0de7ff..73bcf34 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -281,35 +281,111 @@ pub(crate) mod meter { use crate::record::ProcId; /// One process's meter: what it was given, what remains, what it spent. + #[derive(Debug)] struct Metered { - parent: Option, + parent: Option, cap: u64, meter: u64, calls: u64, } - /// Every process's meter, indexed by process number. Owned by the harness. + /// Every process's meter, indexed by process number. A child is appended, + /// so its parent's number is smaller. Owned by the harness. + #[derive(Debug)] pub(crate) struct Meters(Vec); /// Some meter from the process up to the root is spent. + #[derive(Debug)] pub(crate) struct Spent; /// A spawn under a process that does not exist. + #[derive(Debug)] pub(crate) struct NoParent; impl Meters { pub(crate) fn root(cap: u64) -> Meters { - todo!() + Meters(vec![Metered { parent: None, cap, meter: cap, calls: 0 }]) } /// A child of `parent` with meter `cap`, numbered next. - pub(crate) fn spawn(&mut self, parent: ProcId, cap: u64) -> Result { - todo!() + pub(crate) fn spawn(&mut self, parent: &ProcId, cap: u64) -> Result { + let parent = usize::try_from(parent.get()).map_err(|_| NoParent)?; + if parent >= self.0.len() { + return Err(NoParent); + } + self.0.push(Metered { parent: Some(parent), cap, meter: cap, calls: 0 }); + Ok(ProcId::new(self.0.len() as u64 - 1)) } /// A call by `q`: one unit from every meter up to the root, or none. - pub(crate) fn charge(&mut self, q: ProcId) -> Result<(), Spent> { - todo!() + pub(crate) fn charge(&mut self, q: &ProcId) -> Result<(), Spent> { + let q = usize::try_from(q.get()).map_err(|_| Spent)?; + if q >= self.0.len() { + return Err(Spent); + } + let chain = self.chain(q); + if chain.iter().any(|&a| self.0[a].meter == 0) { + return Err(Spent); + } + for a in chain { + self.0[a].meter -= 1; + } + self.0[q].calls += 1; + Ok(()) + } + + /// `q`, its parent, and so on up to the root. + fn chain(&self, q: usize) -> Vec { + let mut chain = vec![q]; + let mut at = q; + while let Some(parent) = self.0[at].parent.filter(|&p| p < at) { + chain.push(parent); + at = parent; + } + chain + } + } + + #[cfg(test)] + mod tests { + use super::Meters; + use crate::record::ProcId; + use crate::record::tests::differential; + + /// Lean's random spawns and charges, replayed: every verdict and every + /// meter after it agree. + #[test] + fn meters_match_lean() { + let lines = differential(&["meter", "300", "40", "2"]); + let mut meters = Meters::root(0); + let (mut ok, mut refused) = (0, 0); + for line in lines.lines() { + // `spawn PA CAP VERDICT [METERS]`, `charge Q VERDICT [METERS]`, `root CAP` + let words: Vec<&str> = line.splitn(4, ' ').collect(); + let n = |i: usize| words[i].parse::().expect("a number"); + let (verdict, expected) = match words[0] { + "root" => { + meters = Meters::root(n(1)); + continue; + } + "spawn" => { + let rest: Vec<&str> = words[3].splitn(2, ' ').collect(); + let got = meters.spawn(&ProcId::new(n(1)), n(2)).is_ok(); + (got == (rest[0] == "ok"), rest[1]) + } + "charge" => { + let rest: Vec<&str> = line.splitn(4, ' ').skip(2).collect(); + let got = meters.charge(&ProcId::new(n(1))).is_ok(); + (got == (rest[0] == "ok"), rest[1]) + } + other => panic!("unknown operation {other}"), + }; + assert!(verdict, "verdict differs: {line}"); + let now: Vec = meters.0.iter().map(|m| m.meter.to_string()).collect(); + assert_eq!(format!("[{}]", now.join(", ")), expected, "{line}"); + if line.contains(" ok ") { ok += 1 } else { refused += 1 } + } + assert!(ok > 1000 && refused > 1000, "{ok} ok, {refused} refused"); } } } diff --git a/src/record.rs b/src/record.rs index cc8ab61..141cf7b 100644 --- a/src/record.rs +++ b/src/record.rs @@ -22,6 +22,19 @@ pub(crate) struct CallId(u64); #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct ProcId(u64); +impl ProcId { + /// The root process: the one `cead run` starts. + pub(crate) const ROOT: ProcId = ProcId(0); + + pub(crate) fn new(n: u64) -> ProcId { + ProcId(n) + } + + pub(crate) fn get(&self) -> u64 { + self.0 + } +} + /// One record: its boot, its place in the boot's sequence, what it says. /// Owned by whoever holds it: the harness until sent, then the log. #[derive(Debug, Clone, PartialEq, Eq, Hash)] @@ -388,7 +401,7 @@ pub(crate) struct Signed { } #[cfg(test)] -mod tests { +pub(crate) mod tests { use super::Record; use std::process::Command; From c0252ab7e8ec506856056561eecc4cdf4203e00a Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:49:22 -0600 Subject: [PATCH 12/19] Fill window: it only grows, and the log replays it as Lean does Co-Authored-By: Claude Opus 5.5 (1M context) --- src/machine.rs | 195 ++++++++++++++++++++++++++++++++++++++++++++++--- src/record.rs | 51 ++++++++++++- 2 files changed, 232 insertions(+), 14 deletions(-) diff --git a/src/machine.rs b/src/machine.rs index 73bcf34..8133afb 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -393,8 +393,9 @@ pub(crate) mod meter { /// A process's window. Mirrors `spec/Cead/Window.lean`: it only grows at its /// end, and the log replays it. pub(crate) mod window { - use crate::record::{Boot, ProcId, Record}; + use crate::record::{Body, Boot, Decision, Event, ProcId, Record}; + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum Role { System, User, @@ -402,41 +403,215 @@ pub(crate) mod window { } /// One span of a window. + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct Span { role: Role, text: Vec, } + impl Span { + pub(crate) fn role(&self) -> &Role { + &self.role + } + + pub(crate) fn text(&self) -> &[u8] { + &self.text + } + } + /// The pinned prompt, the query, then each call's turn and what it /// returned. Owned by its process; dropped when the process is reaped. + #[derive(Debug)] pub(crate) struct Window { spans: Vec, len: usize, limit: usize, } - /// The next span would pass the window limit: the process ends with + /// The next call would pass the window limit: the process ends with /// `limit`. + #[derive(Debug)] pub(crate) struct Full; impl Window { pub(crate) fn open(prompt: Vec, query: Vec, limit: usize) -> Window { - todo!() + let len = prompt.len() + query.len(); + let spans = vec![Span { role: Role::System, text: prompt }, Span { role: Role::User, text: query }]; + Window { spans, len, limit } } - /// Appends one call: the model's turn and what the call returned. + /// Appends one call, its turn and what it returned, if both fit. pub(crate) fn push(&mut self, turn: Vec, returned: Vec) -> Result<(), Full> { - todo!() + let len = self.len + turn.len() + returned.len(); + if len > self.limit { + return Err(Full); + } + self.len = len; + self.spans.push(Span { role: Role::Assistant, text: turn }); + self.spans.push(Span { role: Role::User, text: returned }); + Ok(()) } pub(crate) fn spans(&self) -> &[Span] { - todo!() - } + &self.spans + } + } + + /// Process `proc`'s window as the log's records replay it: `replay` in + /// `spec/Cead/Window.lean`, definition for definition. + pub(crate) fn replay(records: &[Record], boot: &Boot, proc: &ProcId) -> Option> { + let mine = || records.iter().filter(|r| r.boot() == boot).map(Record::body); + let (prompt, root_query) = mine().find_map(|b| match b { + Body::Report { prompt, query, .. } => Some((prompt, query)), + _ => None, + })?; + let query = if *proc == ProcId::ROOT { + root_query + } else { + mine().find_map(|b| match b { + Body::Call { event: Event::Decision(Decision::Spawn { child, query }), .. } + if child == proc => + { + Some(query) + } + _ => None, + })? + }; + let mut ids: Vec = mine() + .filter_map(|b| match b { + Body::Call { id, proc: p, event: Event::Intent { .. } } if p == proc => Some(id.get()), + _ => None, + }) + .collect(); + ids.sort(); + let call = |i: u64| { + let turn = mine().find_map(|b| match b { + Body::Call { id, event: Event::Intent { turn, .. }, .. } if id.get() == i => Some(turn), + _ => None, + })?; + let returned = mine().find_map(|b| match b { + Body::Call { id, event: Event::Decision(Decision::Deny { returned }), .. } + | Body::Call { id, event: Event::Witness { returned, .. }, .. } + if id.get() == i => + { + Some(returned) + } + _ => None, + })?; + Some((turn.clone(), returned.clone())) + }; + let mut spans = vec![ + Span { role: Role::System, text: prompt.clone() }, + Span { role: Role::User, text: query.clone() }, + ]; + for (turn, returned) in ids.into_iter().filter_map(call) { + spans.push(Span { role: Role::Assistant, text: turn }); + spans.push(Span { role: Role::User, text: returned }); + } + Some(spans) } - /// Process `proc`'s window as the log's records replay it. - pub(crate) fn replay(records: &[Record], boot: &Boot, proc: ProcId) -> Option> { - todo!() + #[cfg(test)] + mod tests { + use super::{Role, replay}; + use crate::record::tests::differential; + use crate::record::{ + Attestation, Body, Boot, CallId, Decision, Digest, Event, Origin, ProcId, Record, WaitStatus, + }; + + /// xorshift64: a seeded source of small random choices, no dependency. + struct Rng(u64); + impl Rng { + fn below(&mut self, n: u64) -> u64 { + self.0 ^= self.0 << 13; + self.0 ^= self.0 >> 7; + self.0 ^= self.0 << 17; + self.0 % n + } + fn bytes(&mut self) -> Vec { + let n = self.below(4); + (0..n).map(|_| b'a' + self.below(26) as u8).collect() + } + } + + /// A random log over two boots, three processes and a few call ids: + /// reports, spawns, intents, denies and witnesses, in any order. + fn log(rng: &mut Rng, boots: &[Boot]) -> Vec { + (0..rng.below(24)) + .map(|seq| { + let boot = boots[rng.below(2) as usize].clone(); + let (id, proc) = (CallId::new(rng.below(4)), ProcId::new(rng.below(3))); + let event = match rng.below(5) { + 0 => Event::Intent { turn: rng.bytes(), command: rng.bytes() }, + 1 => Event::Decision(Decision::Deny { returned: rng.bytes() }), + 2 => Event::Decision(Decision::Spawn { child: ProcId::new(rng.below(3)), query: rng.bytes() }), + 3 => Event::Witness { status: WaitStatus::Exited(0), output: Digest::new([0; 32]), returned: rng.bytes() }, + _ => { + let body = Body::Report { + origin: Origin::Run, + measurement: vec![], + attestation: Attestation::Unattested, + prompt: rng.bytes(), + query: rng.bytes(), + }; + return Record::new(boot, seq, body); + } + }; + Record::new(boot, seq, Body::Call { id, proc, event }) + }) + .collect() + } + + /// A window only grows at its end, and refuses the call that would pass + /// its limit, leaving itself as it was. + #[test] + fn window_grows_until_full() { + let mut w = super::Window::open(b"pinned".to_vec(), b"query".to_vec(), 20); + let before = w.spans().to_vec(); + w.push(b"ls".to_vec(), b"a b".to_vec()).expect("fits"); + assert_eq!(&w.spans()[..before.len()], &before[..]); + let full = w.spans().to_vec(); + assert!(w.push(b"cat big".to_vec(), b"x".to_vec()).is_err()); + assert_eq!(w.spans(), &full[..]); + } + + /// Lean's `replay` and Rust's agree on every process of random logs. + #[test] + fn replay_matches_lean() { + let dir = std::env::temp_dir().join(format!("cead-replay-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("temp dir"); + let boots = [Boot::new([1; 32]), Boot::new([2; 32])]; + let mut rng = Rng(0x9e37_79b9_7f4a_7c15); + let mut windows = 0; + for n in 0..200 { + let records = log(&mut rng, &boots); + let path = dir.join(format!("{n}.hex")); + let hex = |b: &[u8]| b.iter().map(|x| format!("{x:02x}")).collect::(); + let lines: Vec = records.iter().map(|r| hex(&r.encode())).collect(); + std::fs::write(&path, lines.join("\n") + "\n").expect("write log"); + for proc in 0..3 { + let lean = differential(&["replay", path.to_str().expect("utf-8"), &hex(boots[0].bytes()), &proc.to_string()]); + let rust = replay(&records, &boots[0], &ProcId::new(proc)); + let rendered = rust.map(|spans| { + spans + .iter() + .map(|s| { + let role = match s.role() { Role::System => "system", Role::User => "user", Role::Assistant => "assistant" }; + format!("{role} {}\n", hex(s.text())) + }) + .collect::() + }); + match rendered { + Some(r) => { + windows += 1; + assert_eq!(r, lean, "log {n}, process {proc}"); + } + None => assert_eq!(lean, "", "log {n}, process {proc}: Lean replays, Rust does not"), + } + } + } + assert!(windows > 100, "{windows} windows replayed"); + } } } diff --git a/src/record.rs b/src/record.rs index 141cf7b..70b8d37 100644 --- a/src/record.rs +++ b/src/record.rs @@ -22,6 +22,32 @@ pub(crate) struct CallId(u64); #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct ProcId(u64); +impl Boot { + pub(crate) fn new(key: [u8; 32]) -> Boot { + Boot(key) + } + + pub(crate) fn bytes(&self) -> &[u8; 32] { + &self.0 + } +} + +impl CallId { + pub(crate) fn new(n: u64) -> CallId { + CallId(n) + } + + pub(crate) fn get(&self) -> u64 { + self.0 + } +} + +impl Digest { + pub(crate) fn new(d: [u8; 32]) -> Digest { + Digest(d) + } +} + impl ProcId { /// The root process: the one `cead run` starts. pub(crate) const ROOT: ProcId = ProcId(0); @@ -130,6 +156,18 @@ pub(crate) enum Exit { pub(crate) struct Malformed; impl Record { + pub(crate) fn new(boot: Boot, seq: u64, body: Body) -> Record { + Record { boot, seq, body } + } + + pub(crate) fn boot(&self) -> &Boot { + &self.boot + } + + pub(crate) fn body(&self) -> &Body { + &self.body + } + /// The bytes a boot's key signs: canonical, so a signature names one record. pub(crate) fn encode(&self) -> Vec { let mut out = Vec::new(); @@ -406,16 +444,21 @@ pub(crate) mod tests { use std::process::Command; /// Runs the Lean half of the differential test (`spec/Cead/Differential.lean`), - /// building it first. Needs `lake` on PATH (elan's `~/.elan/bin`). + /// building it first, and returns what it prints. Needs `lake` on PATH + /// (elan's `~/.elan/bin`). A refusal (`replay` of a process with no window) + /// prints nothing. pub(crate) fn differential(args: &[&str]) -> String { + static BUILT: std::sync::OnceLock = std::sync::OnceLock::new(); let spec = concat!(env!("CARGO_MANIFEST_DIR"), "/spec"); - let built = Command::new("lake").args(["build", "differential"]).current_dir(spec).status(); - assert!(built.expect("lake runs").success(), "lake build differential"); + let built = BUILT.get_or_init(|| { + let status = Command::new("lake").args(["build", "differential"]).current_dir(spec).status(); + status.expect("lake runs").success() + }); + assert!(built, "lake build differential"); let out = Command::new(format!("{spec}/.lake/build/bin/differential")) .args(args) .output() .expect("differential runs"); - assert!(out.status.success()); String::from_utf8(out.stdout).expect("differential prints text") } From 093e0f5e375f44e10e2357a25d0fbc8679ba4349 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 11:49:45 -0600 Subject: [PATCH 13/19] Fill bounded: a call returns its output whole or not at all Co-Authored-By: Claude Opus 5.5 (1M context) --- src/machine.rs | 53 ++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 47 insertions(+), 6 deletions(-) diff --git a/src/machine.rs b/src/machine.rs index 8133afb..f147b14 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -622,22 +622,63 @@ pub(crate) mod bounded { /// Output admitted to the window only if it fits the bound; otherwise /// none of it, and the model reads the spill file like any other state. + #[derive(Debug, PartialEq, Eq)] pub(crate) enum Bounded { Fits(Vec), Spilled { path: PathBuf, size: u64 }, } impl Bounded { - /// Admits `output` whole if it fits `bound`, else writes it under - /// `spill`. + /// Admits `output` whole if it fits `bound`, else writes it to `spill`. pub(crate) fn admit(output: Vec, bound: usize, spill: &Path) -> std::io::Result { - todo!() + if output.len() <= bound { + return Ok(Bounded::Fits(output)); + } + std::fs::write(spill, &output)?; + Ok(Bounded::Spilled { path: spill.to_path_buf(), size: output.len() as u64 }) } - /// The bytes the call returns: the exit status, then the output or - /// the spill's path and size. + /// The bytes the call returns: the output then its exit status, or the + /// exit status with the spill's size and path. The same shape on every + /// task. pub(crate) fn returned(&self, status: &WaitStatus) -> Vec { - todo!() + let status = match status { + WaitStatus::Exited(code) => format!("exit {code}"), + WaitStatus::Signaled(signal) => format!("signal {signal}"), + }; + match self { + Bounded::Fits(output) => { + let mut out = output.clone(); + if !out.is_empty() && !out.ends_with(b"\n") { + out.push(b'\n'); + } + out.extend_from_slice(status.as_bytes()); + out + } + Bounded::Spilled { path, size } => { + format!("{status} · {size} bytes → {}", path.display()).into_bytes() + } + } + } + } + + #[cfg(test)] + mod tests { + use super::Bounded; + use crate::record::WaitStatus; + + /// Output at the bound enters whole; one byte more enters not at all, + /// and the spill file holds every byte. + #[test] + fn all_or_nothing() { + let spill = std::env::temp_dir().join(format!("cead-spill-{}", std::process::id())); + let fits = Bounded::admit(b"abcd".to_vec(), 4, &spill).expect("admit"); + assert_eq!(fits.returned(&WaitStatus::Exited(0)), b"abcd\nexit 0"); + let over = Bounded::admit(b"abcde".to_vec(), 4, &spill).expect("admit"); + assert_eq!(std::fs::read(&spill).expect("spilled"), b"abcde"); + let returned = String::from_utf8(over.returned(&WaitStatus::Signaled(9))).expect("utf-8"); + assert_eq!(returned, format!("signal 9 · 5 bytes → {}", spill.display())); + assert_eq!(Bounded::admit(vec![], 0, &spill).expect("admit").returned(&WaitStatus::Exited(1)), b"exit 1"); } } } From f8a7d3788643e3bc2562d71ba598c312748ec249 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 12:00:37 -0600 Subject: [PATCH 14/19] Fill log: keep and refuse as Lean's accept does, and verify signatures Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 6 +- Cargo.lock | 281 ++++++++++++++++++++++++++++++++++++ Cargo.toml | 5 + spec/Cead/Differential.lean | 41 +++++- src/host.rs | 181 ++++++++++++++++++++--- src/machine.rs | 20 ++- src/record.rs | 55 +++++++ 7 files changed, 562 insertions(+), 27 deletions(-) diff --git a/CODE.md b/CODE.md index 87824cb..4b7bd58 100644 --- a/CODE.md +++ b/CODE.md @@ -62,7 +62,7 @@ Every noun has one home in code: a type, a module, or a subcommand. A noun may p | job | One query's work: a root process and its tree. Started by `cead run`. Spans one boot, or more through recovery. | `host::job::run` | | key | A boot's signing key: made by init, never copied out of it. | `machine::init::Key` | | limit | A cap on one process: calls, window, bound, wall time, depth. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | `host::job::Limits`; `machine::harness::Exhausted` | -| log | Every boot's records, held outside the machine: one append-only JSON-lines file per boot. Records in transit can be lost, delayed, replayed or forged; the log keeps only what the processor or a boot's key signed, and says why it refuses the rest. A complete boot's records are all it did, and replay its every window; an unknown boot's are true but may be partial. A job's boots link through their reports. One writer per boot: never consensus. | `host::log::Log`, `BootLog`, `Refused`; `spec/Cead/Log.lean` | +| log | Every boot's records, held outside the machine: one append-only file per boot, a line per record, its encoding and signature in hex. Records in transit can be lost, delayed, replayed or forged; the log keeps only what the processor or a boot's key signed, and says why it refuses the rest. A complete boot's records are all it did, and replay its every window; an unknown boot's are true but may be partial. A job's boots link through their reports. One writer per boot: never consensus. | `host::log::Log`, `BootLog`, `Refused`; `spec/Cead/Log.lean` | | machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model, booted in a microVM by a VMM. Booting until the log holds its report, then up. | `host::vmm::Machine`; `machine` | | manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | `host::job::Manifest`, `BadManifest` | | meter | What a process tree may spend, from KeyKOS. A child process's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent caps a child's meter in `agent`'s argv and revokes it with `kill`. What it counts is manifest policy. | `machine::meter::Meters`, `Metered`, `Spent`, `NoParent`; `spec/Cead/Meter.lean` | @@ -86,7 +86,7 @@ Every noun has one home in code: a type, a module, or a subcommand. A noun may p | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | | turn | What the model writes on one call: a command, or a reply without one. Logged whole. | `machine::engine::Turn` | -| verified | A record whose signature checked against its boot's key, and whose attestation checked for the mode: the only kind the log accepts. | `host::log::Verified`, `Forged`, `Mode` | +| verified | A record whose signature checked against its boot's key, and whose attestation this build can vouch for (trusted-host mode: unattested only): the only kind the log accepts. | `host::log::Verified`, `Forged` | | view | What init mounts for the model: the task image as root, the context as a file, a directory for spills. | `machine::init::View` | | VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same records; only an attested boot's report is signed. | `host::vmm` | | wait status | How a command ended, as `wait(2)` reports it: exited with a code, or signaled. | `record::WaitStatus` | @@ -122,7 +122,7 @@ Everything else (fields, structs and enums, most traits, invariants like `len - Stable toolchain with clippy, pinned in `rust-toolchain.toml`. - `Cargo.toml` and `clippy.toml` lints are the rules. `cargo check` on every edit; `cargo clippy --all-targets -- -D warnings` and `cargo test` green before ready. Frontier lints warn, so a draft compiles and a ready PR cannot. - eBPF program crates alone lift `unsafe_code`, in their own `Cargo.toml`, visibly. -- `Cargo.toml` is the allowlist: no new dependency without approval. Preferences: rustix, never libc directly; clap derive; anyhow in binaries, thiserror in libraries; serde. Boundary crates: rustix, aya, seccompiler, landlock. +- `Cargo.toml` is the allowlist: no new dependency without approval. Preferences: rustix, never libc directly; std and typed errors until a need appears; `serde_json` only where a wire format is JSON (Bedrock). Approved: `ed25519-dalek`, `sha2`, `serde_json`, `rustix`. Boundary crates: rustix, aya, seccompiler, landlock. - One published crate, `cead`. When the workspace splits (core, machine, tracer, host, VMMs) members are `publish = false`. - Host crates build on macOS: rustix with its libc backend, std, nothing Linux-specific. A Linux-only crate in the host tree is the axis being violated. Machine crates are `#![cfg(target_os = "linux")]` and use linux_raw and Linux-only crates freely. - The core is nix-built and static. diff --git a/Cargo.lock b/Cargo.lock index 8d11ddb..1d5331f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,287 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "block-buffer" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2f6c7dbe95a6ed67ad9f18e57daf93a2f034c524b99fd2b76d18fdfeb6660aa" +dependencies = [ + "hybrid-array", +] + [[package]] name = "cead" version = "0.0.1" +dependencies = [ + "ed25519-dalek", + "serde_json", + "sha2", +] + +[[package]] +name = "cfg-if" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4e7648175b45a9a48536d676f68d918270699102aa8dab5496df06904c914600" + +[[package]] +name = "const-oid" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a6ef517f0926dd24a1582492c791b6a4818a4d94e789a334894aa15b0d12f55c" + +[[package]] +name = "cpufeatures" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ca28b0ae3115b884660db4118d803791fd6756b6e88f39c0f3f7859060d7566" +dependencies = [ + "libc", +] + +[[package]] +name = "crypto-common" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ce6e4c961d6cd6c9a86db418387425e8bdeaf05b3c8bc1411e6dca4c252f1453" +dependencies = [ + "hybrid-array", +] + +[[package]] +name = "curve25519-dalek" +version = "5.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5eed333089e2e1c1ac8c6c0398e5e2497b4c9926ca6d0365ed1e099afa5bc23" +dependencies = [ + "cfg-if", + "cpufeatures", + "curve25519-dalek-derive", + "digest", + "fiat-crypto", + "rustc_version", + "subtle", + "zeroize", +] + +[[package]] +name = "curve25519-dalek-derive" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f46882e17999c6cc590af592290432be3bce0428cb0d5f8b6715e4dc7b383eb3" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "digest" +version = "0.11.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1dd6dbb5841937940781866fa1281a1ff7bd3bf827091440879f9994983d5c2" +dependencies = [ + "block-buffer", + "const-oid", + "crypto-common", +] + +[[package]] +name = "ed25519" +version = "3.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29fcf32e6c73d1079f83ab4d782de2d81620346a5f38c6237a86a22f8368980a" +dependencies = [ + "signature", +] + +[[package]] +name = "ed25519-dalek" +version = "3.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ebaa1a2bf1290ab3bfe5a7b771d050ebffab2711c19a81691c683a5144a25de" +dependencies = [ + "curve25519-dalek", + "ed25519", + "sha2", + "subtle", + "zeroize", +] + +[[package]] +name = "fiat-crypto" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "64cd1e32ddd350061ae6edb1b082d7c54915b5c672c389143b9a63403a109f24" + +[[package]] +name = "hybrid-array" +version = "0.4.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "27f864f10dfb56725ce5ce5472bc52252c8f93a4ab86327122cebf62c5f59a17" +dependencies = [ + "typenum", +] + +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + +[[package]] +name = "libc" +version = "0.2.189" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2" + +[[package]] +name = "memchr" +version = "2.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rustc_version" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92" +dependencies = [ + "semver", +] + +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "serde" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba" +dependencies = [ + "serde_core", +] + +[[package]] +name = "serde_core" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.6", +] + +[[package]] +name = "serde_json" +version = "1.0.151" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + +[[package]] +name = "sha2" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "446ba717509524cb3f22f17ecc096f10f4822d76ab5c0b9822c5f9c284e825f4" +dependencies = [ + "cfg-if", + "cpufeatures", + "digest", +] + +[[package]] +name = "signature" +version = "3.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "28d567dcbaf0049cb8ac2608a76cd95ff9e4412e1899d389ee400918ca7537f5" + +[[package]] +name = "subtle" +version = "2.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292" + +[[package]] +name = "syn" +version = "2.0.119" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "3.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8593e8e72159ed2257d083c7a454a85cbf854f37a0966d8d483aff8c8a3ebcee" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "typenum" +version = "1.20.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6f5e870be6c3b371b77fe0ee0bafb859fa4964b4404c27de1d380043c4dda20" + +[[package]] +name = "unicode-ident" +version = "1.0.26" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d245f478577f809a851594d02313b640fb437e0bb33866753cff937863096954" + +[[package]] +name = "zeroize" +version = "1.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e13c156562582aa81c60cb29407084cdb54c4164760106ab78e6c5b0858cf64e" + +[[package]] +name = "zmij" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b" diff --git a/Cargo.toml b/Cargo.toml index d8b824d..4e98e66 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -24,3 +24,8 @@ license = "Apache-2.0" [lints] workspace = true + +[dependencies] +ed25519-dalek = "3.0.0" +serde_json = "1.0.151" +sha2 = "0.11.0" diff --git a/spec/Cead/Differential.lean b/spec/Cead/Differential.lean index d27bd88..a9c3b8b 100644 --- a/spec/Cead/Differential.lean +++ b/spec/Cead/Differential.lean @@ -85,6 +85,41 @@ def records (n : Nat) : IO Unit := do | none => "-" IO.println s!"{hex b} {out}" +/-- One of three boots, so records collide on boots and places. -/ +def poolBoot : IO Boot := do + let k := (← IO.rand 1 3).toUInt8 + return ⟨List.replicate 32 k, by simp⟩ + +/-- A record aimed at the log's rules: few boots, low places, every kind. -/ +def logRecord : IO Record := do + let boot ← poolBoot + let body ← match ← IO.rand 0 5 with + | 0 => pure (Body.report .run (← blob) .unattested (← blob) (← blob)) + | 1 => pure (Body.report (.fork (← poolBoot) (← IO.rand 0 4).toUInt64) (← blob) .unattested (← blob) (← blob)) + | 2 => pure (Body.report (.recovery (← poolBoot) (← IO.rand 0 4).toUInt64) (← blob) .unattested (← blob) (← blob)) + | 3 => pure (Body.exit .timeout) + | _ => pure (Body.call (← u64) (← u64) (← event)) + -- mostly where each kind belongs, sometimes anywhere + let later ← IO.rand 2 4 + let anywhere ← IO.rand 0 4 + let usual := if body.isReport then 1 else later + let seq := if (← IO.rand 0 3) = 0 then anywhere else usual + return ⟨boot, seq.toUInt64, body⟩ + +/-- Random records offered to `accept` in turn, from an empty log. Each line: +the record, then `kept` or `refused`; `---` between runs. -/ +def logs (runs len : Nat) : IO Unit := do + for _ in [0:runs] do + let mut log : Log := [] + for _ in [0:len] do + let r ← logRecord + match accept log r with + | some log' => + log := log' + IO.println s!"{hex r.enc} kept" + | none => IO.println s!"{hex r.enc} refused" + IO.println "---" + /-- Random spawns and charges from a root. Each line: the operation, Lean's verdict, then every meter. -/ def meters (runs ops : Nat) : IO Unit := do @@ -150,7 +185,11 @@ def main (args : List String) : IO UInt32 := do IO.setRandSeed seed.toNat! Cead.Differential.meters runs.toNat! ops.toNat! return 0 + | ["log", runs, len, seed] => + IO.setRandSeed seed.toNat! + Cead.Differential.logs runs.toNat! len.toNat! + return 0 | ["replay", log, boot, proc] => Cead.Differential.replay log boot proc.toNat! | _ => - IO.eprintln "usage: differential record COUNT SEED | meter RUNS OPS SEED | replay LOG BOOT PROC" + IO.eprintln "usage: differential record COUNT SEED | log RUNS LEN SEED | meter RUNS OPS SEED | replay LOG BOOT PROC" return 64 diff --git a/src/host.rs b/src/host.rs index 44340e7..f9d01ad 100644 --- a/src/host.rs +++ b/src/host.rs @@ -45,37 +45,53 @@ pub(crate) mod job { /// The log: every boot's records, held outside the machine. `spec/cead.tla`'s /// `Arrive` and `spec/Cead/Log.lean`'s `accept`. pub(crate) mod log { - use crate::record::{Boot, Record, Signature, Signed}; + use crate::record::{Attestation, Body, Boot, Exit, Origin, Record, Signature, Signed}; use std::collections::{BTreeSet, HashMap}; use std::fs::File; + use std::io::Write; use std::path::PathBuf; - /// Who guarantees the header's assumptions: the processor, or the host. - pub(crate) enum Mode { - Attested, - TrustedHost, - } - /// A record whose signature checked against its boot's key and, for a - /// report, whose attestation checked for the mode. The only kind `accept` - /// takes. + /// report, whose attestation this build can vouch for: the only kind + /// `accept` takes. Trusted-host mode only: a report must say + /// `Unattested`, since checking an SNP report is the confidential + /// machine's PR. + #[derive(Debug)] pub(crate) struct Verified { record: Record, bytes: Vec, signature: Signature, } - /// A record signed by no one it names, or attested wrongly for the mode. + /// A record signed by no one it names, malformed, or attested in a way + /// this build cannot check. + #[derive(Debug)] pub(crate) struct Forged; impl Verified { - pub(crate) fn verify(signed: Signed, mode: &Mode) -> Result { - todo!() + pub(crate) fn verify(signed: Signed) -> Result { + let record = Record::decode(signed.bytes()).map_err(|_| Forged)?; + if let Body::Report { attestation: Attestation::Snp(_), .. } = record.body() { + return Err(Forged); + } + if !record.boot().verifies(signed.bytes(), signed.signature()) { + return Err(Forged); + } + let (bytes, signature) = signed.into_parts(); + Ok(Verified { record, bytes, signature }) + } + + /// A record taken as verified, for tests of what follows verification. + #[cfg(test)] + pub(crate) fn assume(record: Record) -> Verified { + let bytes = record.encode(); + Verified { record, bytes, signature: Signature::new([0; 64]) } } } - /// One JSON-lines file per boot, append-only. Owned by the operator's `cead` - /// for the life of the job. + /// One file per boot, a line per kept record: its encoding and signature, + /// in hex. The format `spec/Cead/Differential.lean`'s `replay` reads. + /// Owned by the operator's `cead` for the life of the job. pub(crate) struct Log { dir: PathBuf, boots: HashMap, @@ -90,10 +106,12 @@ pub(crate) mod log { } /// Why the log kept nothing: `Admits` in `spec/Cead/Log.lean`, case by case. + #[derive(Debug, PartialEq, Eq)] pub(crate) enum Refused { /// Its place in the boot's sequence is taken: first wins. Taken, - /// A report not first in its sequence, or a record before its report. + /// A report not first in its sequence, or another record at or before + /// the report's place. OutOfPlace, /// A record whose boot's report the log does not hold. Unvouched, @@ -103,16 +121,143 @@ pub(crate) mod log { Settled, /// A record of a boot a recovery has fenced. Fenced, + /// The log could not write it: nothing kept, nothing acknowledged, so + /// the machine sends it again. + Unwritten, } impl Log { pub(crate) fn open(dir: PathBuf) -> std::io::Result { - todo!() + std::fs::create_dir_all(&dir)?; + Ok(Log { dir, boots: HashMap::new() }) + } + + fn logged(&self, boot: &Boot, seq: u64) -> bool { + self.boots.get(boot).is_some_and(|b| b.seqs.contains(&seq)) + } + + fn settled(&self, boot: &Boot) -> bool { + self.boots.get(boot).is_some_and(|b| b.exited || b.recovered) } /// Keeps the record, or says why not. Keeping it acknowledges it. - pub(crate) fn accept(&mut self, record: Verified) -> Result<(), Refused> { - todo!() + pub(crate) fn accept(&mut self, v: Verified) -> Result<(), Refused> { + let (boot, seq) = (v.record.boot(), v.record.seq()); + if self.logged(boot, seq) { + return Err(Refused::Taken); + } + match v.record.body() { + Body::Report { origin, .. } => { + if seq != 1 { + return Err(Refused::OutOfPlace); + } + match origin { + Origin::Run => {} + Origin::Fork { boot: from, last } => { + if !self.logged(from, *last) { + return Err(Refused::Unrooted); + } + } + Origin::Recovery { boot: from, last } => { + if !self.logged(from, *last) { + return Err(Refused::Unrooted); + } + if self.settled(from) { + return Err(Refused::Settled); + } + } + } + } + _ => { + if seq <= 1 { + return Err(Refused::OutOfPlace); + } + if !self.logged(boot, 1) { + return Err(Refused::Unvouched); + } + if self.boots.get(boot).is_some_and(|b| b.recovered) { + return Err(Refused::Fenced); + } + } + } + self.keep(v).map_err(|_| Refused::Unwritten) + } + + /// Appends the record to its boot's file, then to what `accept` asks. + fn keep(&mut self, v: Verified) -> std::io::Result<()> { + let hex = |b: &[u8]| b.iter().map(|x| format!("{x:02x}")).collect::(); + let boot = v.record.boot().clone(); + if !self.boots.contains_key(&boot) { + let path = self.dir.join(format!("{}.log", hex(boot.bytes()))); + let file = File::options().create(true).append(true).open(path)?; + self.boots.insert(boot.clone(), BootLog { file, seqs: BTreeSet::new(), exited: false, recovered: false }); + } + let line = format!("{} {}\n", hex(&v.bytes), hex(v.signature.bytes())); + let entry = self.boots.get_mut(&boot).ok_or_else(|| std::io::Error::other("boot vanished"))?; + entry.file.write_all(line.as_bytes())?; + entry.seqs.insert(v.record.seq()); + if let Body::Exit(_) = v.record.body() { + entry.exited = true; + } + if let Body::Report { origin: Origin::Recovery { boot: from, .. }, .. } = v.record.body() { + if let Some(recovered) = self.boots.get_mut(from) { + recovered.recovered = true; + } + } + Ok(()) + } + } + + #[cfg(test)] + mod tests { + use super::{Log, Verified}; + use crate::record::Record; + use crate::record::tests::{differential, unhex}; + + /// Only a record its own boot's key signed gets through, and no SNP + /// report yet. + #[test] + fn verify_refuses_forgeries() { + use crate::machine::init::Key; + use crate::record::{Attestation, Body, Origin, Signed}; + let report = |attestation| Body::Report { + origin: Origin::Run, + measurement: vec![], + attestation, + prompt: vec![], + query: vec![], + }; + let (key, other) = (Key::generate().expect("key"), Key::generate().expect("key")); + let bytes = Record::new(key.boot(), 1, report(Attestation::Unattested)).encode(); + assert!(Verified::verify(Signed::new(bytes.clone(), key.sign(&bytes))).is_ok()); + assert!(Verified::verify(Signed::new(bytes.clone(), other.sign(&bytes))).is_err()); + let mut flipped = bytes.clone(); + flipped[40] ^= 1; + assert!(Verified::verify(Signed::new(flipped, key.sign(&bytes))).is_err()); + let snp = Record::new(key.boot(), 1, report(Attestation::Snp(vec![1]))).encode(); + assert!(Verified::verify(Signed::new(snp.clone(), key.sign(&snp))).is_err()); + } + + /// Lean's `accept` and Rust's keep and refuse the same records, run + /// after run from an empty log. + #[test] + fn accept_matches_lean() { + let base = std::env::temp_dir().join(format!("cead-log-{}", std::process::id())); + let (mut kept, mut refused, mut run) = (0, 0, 0); + let mut log = Log::open(base.join("0")).expect("log"); + for line in differential(&["log", "300", "30", "4"]).lines() { + if line == "---" { + run += 1; + log = Log::open(base.join(run.to_string())).expect("log"); + continue; + } + let (hex, lean) = line.split_once(' ').expect("two fields"); + let record = Record::decode(&unhex(hex)).expect("Lean encodes records"); + let rust = log.accept(Verified::assume(record)); + assert_eq!(rust.is_ok(), lean == "kept", "run {run}: {line}: {rust:?}"); + if rust.is_ok() { kept += 1 } else { refused += 1 } + } + assert!(kept > 1000 && refused > 1000, "{kept} kept, {refused} refused"); } } } diff --git a/src/machine.rs b/src/machine.rs index f147b14..c8908cd 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -14,18 +14,28 @@ pub(crate) mod init { pub(crate) struct Key([u8; 32]); impl Key { - /// A fresh key for a fresh boot. - pub(crate) fn generate() -> Key { - todo!() + /// A fresh key for a fresh boot, from the kernel's random source. + pub(crate) fn generate() -> std::io::Result { + use std::io::Read; + let mut secret = [0; 32]; + File::open("/dev/urandom")?.read_exact(&mut secret)?; + Ok(Key(secret)) } /// The public half, which names the boot. pub(crate) fn boot(&self) -> Boot { - todo!() + Boot::of(&self.0) } pub(crate) fn sign(&self, bytes: &[u8]) -> Signature { - todo!() + crate::record::sign(&self.0, bytes) + } + } + + impl Drop for Key { + /// The secret does not outlive the boot's init. + fn drop(&mut self) { + self.0.fill(0); } } diff --git a/src/record.rs b/src/record.rs index 70b8d37..6eab0e1 100644 --- a/src/record.rs +++ b/src/record.rs @@ -22,14 +22,65 @@ pub(crate) struct CallId(u64); #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct ProcId(u64); +// Ed25519 lives here and nowhere else: `sign` for init's key, `verifies` for +// the log. + +/// Signs `bytes` with the secret half of a boot's key. +pub(crate) fn sign(secret: &[u8; 32], bytes: &[u8]) -> Signature { + use ed25519_dalek::Signer; + Signature(ed25519_dalek::SigningKey::from_bytes(secret).sign(bytes).to_bytes()) +} + impl Boot { pub(crate) fn new(key: [u8; 32]) -> Boot { Boot(key) } + /// The boot whose key has this secret half. + pub(crate) fn of(secret: &[u8; 32]) -> Boot { + Boot(ed25519_dalek::SigningKey::from_bytes(secret).verifying_key().to_bytes()) + } + pub(crate) fn bytes(&self) -> &[u8; 32] { &self.0 } + + /// This boot's key signed `bytes`. Strict: no malleable or small-order + /// signatures. + pub(crate) fn verifies(&self, bytes: &[u8], signature: &Signature) -> bool { + let Ok(key) = ed25519_dalek::VerifyingKey::from_bytes(&self.0) else { + return false; + }; + key.verify_strict(bytes, &ed25519_dalek::Signature::from_bytes(&signature.0)).is_ok() + } +} + +impl Signature { + pub(crate) fn new(s: [u8; 64]) -> Signature { + Signature(s) + } + + pub(crate) fn bytes(&self) -> &[u8; 64] { + &self.0 + } +} + +impl Signed { + pub(crate) fn new(bytes: Vec, signature: Signature) -> Signed { + Signed { bytes, signature } + } + + pub(crate) fn bytes(&self) -> &[u8] { + &self.bytes + } + + pub(crate) fn signature(&self) -> &Signature { + &self.signature + } + + pub(crate) fn into_parts(self) -> (Vec, Signature) { + (self.bytes, self.signature) + } } impl CallId { @@ -164,6 +215,10 @@ impl Record { &self.boot } + pub(crate) fn seq(&self) -> u64 { + self.seq + } + pub(crate) fn body(&self) -> &Body { &self.body } From fe8a4ab7f0b31beced7dd91f8d11da348bb4d809 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 12:01:41 -0600 Subject: [PATCH 15/19] Spill output that is not text, so the window holds exactly what the log replays Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 6 +++--- src/machine.rs | 13 +++++++++---- 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/CODE.md b/CODE.md index 4b7bd58..7e062d1 100644 --- a/CODE.md +++ b/CODE.md @@ -29,7 +29,7 @@ Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TL # Vocabulary -Every noun has one home in code: a type, a module, or a subcommand. A noun may precede its home; the PR that first needs it builds it. No home without a noun, and no type without a row here. Paths are from `src/`; a type's errors and states sit in its row. +Every noun has one home in code: a type, a module, or a subcommand. A noun may precede its home; the PR that first needs it builds it. No home without a noun, and no type outside tests without a row here. Paths are from `src/`; a type's errors and states sit in its row. | Noun | Meaning | In code | |---|---|---| @@ -40,7 +40,7 @@ Every noun has one home in code: a type, a module, or a subcommand. A noun may p | availability | The job runs and ends. The host guarantees it, and can always deny it. | `spec/cead.tla` | | blocked | A process waiting: on its intent's decision, its command's end, or a foreground child. Holds the model's turn until the call returns. | `machine::process::Blocked` | | boot | One life of a machine's kernel, from the VMM starting it to eviction, with one key, which names it. Its records are numbered from its report, each signed with that key. **Complete** when the log holds its records through its exit record with no gap; otherwise **unknown** (crash, host kill, lost report). Linux's `boot_id`. | `record::Boot`; `spec/cead.tla` | -| bounded | What a call returns: the output whole if it fits the bound, else none of it and where it **spilled**, a file the model reads like any other state. Nothing is truncated. | `machine::bounded::Bounded` | +| bounded | What a call returns: the output whole if it fits the bound and is text, else none of it and where it **spilled**, a file the model reads like any other state. Nothing is truncated or re-encoded, so the window holds exactly what the log replays. | `machine::bounded::Bounded` | | call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. Its intent, decision and witness share its id. | `record::CallId` | | call table | The system call table: the toolset. | | | cead | The project and its one binary, its role chosen at start: `run` on the host; `init`, `harness` and `agent` in the machine. | crate and binary `cead`; `main::Role`, `Usage` | @@ -74,7 +74,7 @@ Every noun has one home in code: a type, a module, or a subcommand. A noun may p | processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. A boot sees the model's processors as virtual, like vCPUs; how the engine shares its GPU among them (batching) is its scheduler's. | | | query | The argv of `run` or `agent`, commit-message sized; it opens its process's window. Anything longer is context, a file. | bytes in `record::Body::Report`, `Decision::Spawn` | | report | A boot's first record: binds the boot's key to the manifest's measurement, names what started it (run, or the snapshot a fork or recovery booted from), and carries the pinned prompt and the root's query. Signed by the processor on an attested boot. Linux's TSM report. | `record::Body::Report`, `Origin`; `spec/cead.tla` | -| record | One entry the machine signs for the log, Linux audit's unit, canonically encoded. Types: report, intent (the model's turn and its command), decision, witness (how the command ended, its output's digest, what the call returned), exit (why the boot ended; the root's reply digest on a finish). A call's three share its id and process. | `record::Record`, `Body`, `Event`, `Exit`, `Signed`, `Signature`, `Digest`, `Malformed`; `spec/Cead/Record.lean` | +| record | One entry the machine signs for the log, Linux audit's unit, canonically encoded. Types: report, intent (the model's turn and its command), decision, witness (how the command ended, its output's digest, what the call returned), exit (why the boot ended; the root's reply digest on a finish). A call's three share its id and process. | `record::Record`, `Body`, `Event`, `Exit`, `Signed`, `Signature`, `Digest`, `Malformed`, `Reader`; `spec/Cead/Record.lean` | | rights | What a call may do to state: read, write. | `machine::process::Rights` | | ring | A privilege layer: model processes; harness and tracer; host. | | | scheduler | Decides what runs where: machines on hosts (Kubernetes), requests on engines (Dynamo). Trusted for availability only; needs consensus once there is more than one. | | diff --git a/src/machine.rs b/src/machine.rs index c8908cd..7106849 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -630,8 +630,10 @@ pub(crate) mod bounded { use crate::record::WaitStatus; use std::path::{Path, PathBuf}; - /// Output admitted to the window only if it fits the bound; otherwise - /// none of it, and the model reads the spill file like any other state. + /// Output admitted to the window only if it fits the bound and is text + /// (UTF-8, as the engine's API requires, so the window holds exactly the + /// bytes the log replays); otherwise none of it, and the model reads the + /// spill file like any other state. #[derive(Debug, PartialEq, Eq)] pub(crate) enum Bounded { Fits(Vec), @@ -639,9 +641,10 @@ pub(crate) mod bounded { } impl Bounded { - /// Admits `output` whole if it fits `bound`, else writes it to `spill`. + /// Admits `output` whole if it fits `bound` and is text, else writes it + /// to `spill`. pub(crate) fn admit(output: Vec, bound: usize, spill: &Path) -> std::io::Result { - if output.len() <= bound { + if output.len() <= bound && std::str::from_utf8(&output).is_ok() { return Ok(Bounded::Fits(output)); } std::fs::write(spill, &output)?; @@ -689,6 +692,8 @@ pub(crate) mod bounded { let returned = String::from_utf8(over.returned(&WaitStatus::Signaled(9))).expect("utf-8"); assert_eq!(returned, format!("signal 9 · 5 bytes → {}", spill.display())); assert_eq!(Bounded::admit(vec![], 0, &spill).expect("admit").returned(&WaitStatus::Exited(1)), b"exit 1"); + let binary = Bounded::admit(vec![0xff, 0xfe], 64, &spill).expect("admit"); + assert!(matches!(binary, Bounded::Spilled { size: 2, .. }), "bytes that are not text spill"); } } } From aab9953bec2ce5e34704dd515fb3e41688417a88 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 12:03:29 -0600 Subject: [PATCH 16/19] Fill the gateway and the wire: frames, spans, and Converse through curl Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 6 +- src/host.rs | 205 ++++++++++++++++++++++++++++++++++++++++++++----- src/machine.rs | 36 +++++++++ src/record.rs | 56 +++++++++++++- 4 files changed, 278 insertions(+), 25 deletions(-) diff --git a/CODE.md b/CODE.md index 7e062d1..f494a77 100644 --- a/CODE.md +++ b/CODE.md @@ -53,7 +53,7 @@ Every noun has one home in code: a type, a module, or a subcommand. A noun may p | engine | Executes the weights and signs what it produces: the model's counterpart to the machine. Reached from the machine over vsock, through the gateway. | `machine::engine::Engine` | | evict | Dispose at any tier: window span, KV block, process, machine. | `host::vmm::Machine::evict` | | executed | What the kernel ran: the truth the records record. | `spec/cead.tla` | -| gateway | The host's relay to a hosted engine: holds the credentials the machine never sees, signs each request, and records it, a second account of every window. | `host::gateway::Gateway`, `Credentials` | +| gateway | The host's relay to a hosted engine: holds the credential the machine never sees (a Bedrock API key), sends each window through `curl`, and records it with its turn and tokens, a second account of every window. | `host::gateway::Gateway`, `Credentials`, `Answer`, `Failed` | | harness | The model's kernel, exec'd by init so it starts without the key. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, numbers records for init to sign. One method per spec action. | `machine::harness::Harness`; `cead harness` | | host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | `host` | | init | PID 1 in the machine, for the whole boot. Makes the boot's key and never lets it go; signs every record. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, forks and execs the harness. If the harness dies, the boot ends with no exit record: unknown. | `machine::init::Init`; `cead init` | @@ -74,7 +74,7 @@ Every noun has one home in code: a type, a module, or a subcommand. A noun may p | processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. A boot sees the model's processors as virtual, like vCPUs; how the engine shares its GPU among them (batching) is its scheduler's. | | | query | The argv of `run` or `agent`, commit-message sized; it opens its process's window. Anything longer is context, a file. | bytes in `record::Body::Report`, `Decision::Spawn` | | report | A boot's first record: binds the boot's key to the manifest's measurement, names what started it (run, or the snapshot a fork or recovery booted from), and carries the pinned prompt and the root's query. Signed by the processor on an attested boot. Linux's TSM report. | `record::Body::Report`, `Origin`; `spec/cead.tla` | -| record | One entry the machine signs for the log, Linux audit's unit, canonically encoded. Types: report, intent (the model's turn and its command), decision, witness (how the command ended, its output's digest, what the call returned), exit (why the boot ended; the root's reply digest on a finish). A call's three share its id and process. | `record::Record`, `Body`, `Event`, `Exit`, `Signed`, `Signature`, `Digest`, `Malformed`, `Reader`; `spec/Cead/Record.lean` | +| record | One entry the machine signs for the log, Linux audit's unit, canonically encoded. Types: report, intent (the model's turn and its command), decision, witness (how the command ended, its output's digest, what the call returned), exit (why the boot ended; the root's reply digest on a finish). A call's three share its id and process. | `record::Record`, `Body`, `Event`, `Exit`, `Signed`, `Signature`, `Digest`, `Malformed`, `Reader`, `write_frame`, `read_frame`; `spec/Cead/Record.lean` | | rights | What a call may do to state: read, write. | `machine::process::Rights` | | ring | A privilege layer: model processes; harness and tracer; host. | | | scheduler | Decides what runs where: machines on hosts (Kubernetes), requests on engines (Dynamo). Trusted for availability only; needs consensus once there is more than one. | | @@ -82,7 +82,7 @@ Every noun has one home in code: a type, a module, or a subcommand. A noun may p | signer | The harness's end of init's signing pipe: numbers each record, so a boot's sequence has no gaps. | `machine::harness::Signer` | | slice | The bytes a child receives on stdin, sealed. | | | snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). A recovery **fences** the boot it recovers: the log keeps none of that boot's records after it. | `record::Origin` | -| span | One piece of a window: system, user or assistant text. | `machine::window::Span`, `Role` | +| span | One piece of a window: system, user or assistant text. | `machine::window::Span`, `Role`, `encode`, `decode`, `NotSpans` | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | | turn | What the model writes on one call: a command, or a reply without one. Logged whole. | `machine::engine::Turn` | diff --git a/src/host.rs b/src/host.rs index f9d01ad..faf9b06 100644 --- a/src/host.rs +++ b/src/host.rs @@ -199,10 +199,10 @@ pub(crate) mod log { if let Body::Exit(_) = v.record.body() { entry.exited = true; } - if let Body::Report { origin: Origin::Recovery { boot: from, .. }, .. } = v.record.body() { - if let Some(recovered) = self.boots.get_mut(from) { - recovered.recovered = true; - } + if let Body::Report { origin: Origin::Recovery { boot: from, .. }, .. } = v.record.body() + && let Some(recovered) = self.boots.get_mut(from) + { + recovered.recovered = true; } Ok(()) } @@ -312,31 +312,200 @@ pub(crate) mod vmm { } } -/// The gateway: holds the model's credentials, which never enter the machine, -/// and relays each inference to Bedrock. +/// The gateway: holds the model's credential, which never enters the machine, +/// and relays each inference to Bedrock's Converse API. pub(crate) mod gateway { + use crate::machine::window::{self, Role, Span}; + use serde_json::{Value, json}; use std::fs::File; + use std::io::Write; + use std::process::{Command, Stdio}; + + /// A Bedrock API key: a bearer token, read on the host. Never serialized, + /// never sent anywhere but Bedrock, never on a command line. + pub(crate) struct Credentials(String); + + impl Credentials { + pub(crate) fn new(token: String) -> Credentials { + Credentials(token) + } + } - /// Owns the AWS credentials and the record of every request it relays: a - /// second account of each window, independent of the log. + /// Owns the credential and the record of every request it relays: a second + /// account of each window, independent of the log. pub(crate) struct Gateway { credentials: Credentials, + region: String, + model: String, requests: File, } - /// AWS credentials, read on the host. Never serialized, never sent. - pub(crate) struct Credentials { - access_key: String, - secret_key: String, - session_token: Option, - region: String, + /// What Bedrock answered, or why there is no answer. + #[derive(Debug)] + pub(crate) enum Failed { + /// The machine sent something that is not a window of text. + BadWindow, + /// `curl` could not run, or Bedrock refused; its words. + Relay(String), + /// Bedrock answered with no text. + NoTurn, + } + + /// One answer: the model's turn and the tokens it cost. + #[derive(Debug, PartialEq)] + pub(crate) struct Answer { + turn: Vec, + input_tokens: u64, + output_tokens: u64, } impl Gateway { - /// Signs a request from the machine with SigV4, sends it, records it, - /// and returns the response. - pub(crate) fn relay(&mut self, request: &[u8]) -> std::io::Result> { - todo!() + pub(crate) fn new(credentials: Credentials, region: String, model: String, requests: File) -> Gateway { + Gateway { credentials, region, model, requests } + } + + /// Takes a window as the machine encodes it, asks Bedrock, records the + /// exchange (window, turn, tokens, in that order), and returns the turn. + pub(crate) fn relay(&mut self, request: &[u8]) -> Result, Failed> { + let spans = window::decode(request).map_err(|_| Failed::BadWindow)?; + let body = body(&spans).ok_or(Failed::BadWindow)?; + let answer = answer(&self.send(&body)?)?; + let hex = |b: &[u8]| b.iter().map(|x| format!("{x:02x}")).collect::(); + let line = format!( + "{} {} {} {}\n", + hex(request), + hex(&answer.turn), + answer.input_tokens, + answer.output_tokens + ); + self.requests.write_all(line.as_bytes()).map_err(|e| Failed::Relay(e.to_string()))?; + Ok(answer.turn) + } + + /// POSTs the body with `curl`. Its configuration, the token included, + /// goes on stdin, so neither shows in the host's process list. + fn send(&self, body: &Value) -> Result, Failed> { + let url = format!( + "https://bedrock-runtime.{}.amazonaws.com/model/{}/converse", + self.region, self.model + ); + let config = curl_config(&url, &self.credentials.0, &body.to_string()); + let mut curl = Command::new("curl") + .args(["--config", "-"]) + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn() + .map_err(|e| Failed::Relay(e.to_string()))?; + curl.stdin + .take() + .ok_or_else(|| Failed::Relay("no stdin".into()))? + .write_all(config.as_bytes()) + .map_err(|e| Failed::Relay(e.to_string()))?; + let out = curl.wait_with_output().map_err(|e| Failed::Relay(e.to_string()))?; + if !out.status.success() { + let words = [out.stderr, out.stdout].concat(); + return Err(Failed::Relay(String::from_utf8_lossy(&words).into_owned())); + } + Ok(out.stdout) + } + } + + /// A curl configuration, one option per line, values quoted with `"` and + /// `\` escaped. + fn curl_config(url: &str, token: &str, body: &str) -> String { + let q = |v: &str| format!("\"{}\"", v.replace('\\', "\\\\").replace('"', "\\\"")); + [ + format!("url = {}", q(url)), + "request = \"POST\"".into(), + "silent".into(), + "show-error".into(), + "fail-with-body".into(), + format!("header = {}", q(&format!("Authorization: Bearer {token}"))), + format!("header = {}", q("Content-Type: application/json")), + format!("data-raw = {}", q(body)), + ] + .join("\n") + + "\n" + } + + /// The Converse request for a window: its system span as the system + /// prompt, the rest as alternating messages. None if any span is not text. + fn body(spans: &[Span]) -> Option { + let text = |s: &Span| std::str::from_utf8(s.text()).ok().map(str::to_owned); + let mut system = Vec::new(); + let mut messages = Vec::new(); + for span in spans { + let t = text(span)?; + match span.role() { + Role::System => system.push(json!({ "text": t })), + Role::User => messages.push(json!({ "role": "user", "content": [{ "text": t }] })), + Role::Assistant => messages.push(json!({ "role": "assistant", "content": [{ "text": t }] })), + } + } + Some(json!({ "system": system, "messages": messages })) + } + + /// The model's turn and its token counts from a Converse response. + fn answer(response: &[u8]) -> Result { + let v: Value = serde_json::from_slice(response).map_err(|e| Failed::Relay(e.to_string()))?; + let turn: String = v["output"]["message"]["content"] + .as_array() + .ok_or(Failed::NoTurn)? + .iter() + .filter_map(|c| c["text"].as_str()) + .collect(); + if turn.is_empty() { + return Err(Failed::NoTurn); + } + let tokens = |k: &str| v["usage"][k].as_u64().unwrap_or(0); + Ok(Answer { turn: turn.into_bytes(), input_tokens: tokens("inputTokens"), output_tokens: tokens("outputTokens") }) + } + + #[cfg(test)] + mod tests { + use super::{Answer, answer, body, curl_config}; + use crate::machine::window::Window; + use serde_json::json; + + /// A window becomes Converse's system prompt and alternating messages. + #[test] + fn request_shape() { + let mut w = Window::open(b"pinned".to_vec(), b"query".to_vec(), 100); + w.push(b"ls".to_vec(), b"a\nexit 0".to_vec()).expect("fits"); + let spans = crate::machine::window::decode(&crate::machine::window::encode(w.spans())).expect("spans"); + assert_eq!( + body(&spans).expect("text"), + json!({ + "system": [{ "text": "pinned" }], + "messages": [ + { "role": "user", "content": [{ "text": "query" }] }, + { "role": "assistant", "content": [{ "text": "ls" }] }, + { "role": "user", "content": [{ "text": "a\nexit 0" }] }, + ] + }) + ); + } + + /// The turn is the response's text, joined; its tokens are counted. + #[test] + fn response_shape() { + let response = json!({ + "output": { "message": { "role": "assistant", "content": [{ "text": "cat " }, { "text": "f" }] } }, + "usage": { "inputTokens": 12, "outputTokens": 3 }, + "stopReason": "end_turn" + }); + let got = answer(response.to_string().as_bytes()).expect("answer"); + assert_eq!(got, Answer { turn: b"cat f".to_vec(), input_tokens: 12, output_tokens: 3 }); + assert!(answer(br#"{"output":{"message":{"content":[]}}}"#).is_err()); + } + + /// Quotes and backslashes in the body cannot end a config value early. + #[test] + fn config_quotes() { + let c = curl_config("https://x", "t", r#"{"a":"b\"c"}"#); + assert!(c.contains(r#"data-raw = "{\"a\":\"b\\\"c\"}""#), "{c}"); + assert!(c.contains(r#"header = "Authorization: Bearer t""#)); } } } diff --git a/src/machine.rs b/src/machine.rs index 7106849..178a8a7 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -467,6 +467,42 @@ pub(crate) mod window { } } + /// Spans as they cross to the gateway: a u64 count, then each span's role + /// tag (0 system, 1 user, 2 assistant) and its text as u64 length and bytes. + pub(crate) fn encode(spans: &[Span]) -> Vec { + let mut out = (spans.len() as u64).to_be_bytes().to_vec(); + for span in spans { + out.push(match span.role { + Role::System => 0, + Role::User => 1, + Role::Assistant => 2, + }); + out.extend_from_slice(&(span.text.len() as u64).to_be_bytes()); + out.extend_from_slice(&span.text); + } + out + } + + /// Bytes that are no spans' encoding. + #[derive(Debug)] + pub(crate) struct NotSpans; + + pub(crate) fn decode(bytes: &[u8]) -> Result, NotSpans> { + let mut r = crate::record::Reader::new(bytes); + let count = r.u64().map_err(|_| NotSpans)?; + let mut spans = Vec::new(); + for _ in 0..count { + let role = match r.tag().map_err(|_| NotSpans)? { + 0 => Role::System, + 1 => Role::User, + 2 => Role::Assistant, + _ => return Err(NotSpans), + }; + spans.push(Span { role, text: r.bytes().map_err(|_| NotSpans)? }); + } + if r.is_empty() { Ok(spans) } else { Err(NotSpans) } + } + /// Process `proc`'s window as the log's records replay it: `replay` in /// `spec/Cead/Window.lean`, definition for definition. pub(crate) fn replay(records: &[Record], boot: &Boot, proc: &ProcId) -> Option> { diff --git a/src/record.rs b/src/record.rs index 6eab0e1..54e9d09 100644 --- a/src/record.rs +++ b/src/record.rs @@ -238,14 +238,48 @@ impl Record { } } +/// The most a frame may carry. The host is untrusted: a length it sends +/// cannot make the machine allocate without bound. +pub(crate) const MAX_FRAME: u64 = 64 << 20; + +/// Writes one frame: a u64 length, big-endian, then the bytes. How records, +/// acknowledgments and inference cross a pipe or vsock. +pub(crate) fn write_frame(w: &mut impl std::io::Write, bytes: &[u8]) -> std::io::Result<()> { + w.write_all(&(bytes.len() as u64).to_be_bytes())?; + w.write_all(bytes)?; + w.flush() +} + +/// Reads one frame, refusing one longer than `MAX_FRAME`. +pub(crate) fn read_frame(r: &mut impl std::io::Read) -> std::io::Result> { + let mut len = [0; 8]; + r.read_exact(&mut len)?; + let len = u64::from_be_bytes(len); + if len > MAX_FRAME { + return Err(std::io::Error::other(format!("frame of {len} bytes"))); + } + let mut bytes = vec![0; len as usize]; + r.read_exact(&mut bytes)?; + Ok(bytes) +} + // The codec of `spec/Cead/Record.lean`: every value is self-delimiting. A // variant is a tag byte, then its fields in order; a u64 is eight bytes // big-endian; bytes are a u64 length, then the bytes; a key or digest is its // 32 bytes. -struct Reader<'a>(&'a [u8]); +/// Reads the codec's primitives from the front of a byte slice. +pub(crate) struct Reader<'a>(&'a [u8]); impl<'a> Reader<'a> { + pub(crate) fn new(bytes: &'a [u8]) -> Reader<'a> { + Reader(bytes) + } + + pub(crate) fn is_empty(&self) -> bool { + self.0.is_empty() + } + fn take(&mut self, n: usize) -> Result<&'a [u8], Malformed> { if self.0.len() < n { return Err(Malformed); @@ -255,17 +289,17 @@ impl<'a> Reader<'a> { Ok(head) } - fn tag(&mut self) -> Result { + pub(crate) fn tag(&mut self) -> Result { Ok(self.take(1)?[0]) } - fn u64(&mut self) -> Result { + pub(crate) fn u64(&mut self) -> Result { let mut b = [0; 8]; b.copy_from_slice(self.take(8)?); Ok(u64::from_be_bytes(b)) } - fn bytes(&mut self) -> Result, Malformed> { + pub(crate) fn bytes(&mut self) -> Result, Malformed> { let n = usize::try_from(self.u64()?).map_err(|_| Malformed)?; Ok(self.take(n)?.to_vec()) } @@ -524,6 +558,20 @@ pub(crate) mod tests { .collect() } + /// A frame carries its bytes exactly; an oversized length is refused + /// before anything is allocated. + #[test] + fn frames() { + let mut wire = Vec::new(); + super::write_frame(&mut wire, b"abc").expect("write"); + super::write_frame(&mut wire, b"").expect("write"); + let mut r = &wire[..]; + assert_eq!(super::read_frame(&mut r).expect("read"), b"abc"); + assert_eq!(super::read_frame(&mut r).expect("read"), b""); + let huge = (super::MAX_FRAME + 1).to_be_bytes(); + assert!(super::read_frame(&mut &huge[..]).is_err()); + } + /// Every encoding Lean accepts, Rust decodes and re-encodes to the same /// bytes; every one Lean rejects (a byte changed, cut short, extended), Rust /// rejects too. From 0bb9318ab3c76301130c1311d5799069831f8299 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 12:04:18 -0600 Subject: [PATCH 17/19] Fill the signer, rights and roles: numbered records, attenuation, argv Co-Authored-By: Claude Opus 5.5 (1M context) --- src/machine.rs | 96 +++++++++++++++++++++++++++++++++++++++++++++----- src/main.rs | 34 +++++++++++++++++- 2 files changed, 121 insertions(+), 9 deletions(-) diff --git a/src/machine.rs b/src/machine.rs index 178a8a7..231a8c9 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -90,28 +90,77 @@ pub(crate) mod harness { use super::process::{Process, Status}; use super::shell::Ran; use crate::host::job::Limits; - use crate::record::{Body, Boot, CallId, ProcId}; + use crate::record::{Body, Boot, CallId, ProcId, Record, read_frame, write_frame}; + use std::collections::BTreeSet; use std::fs::File; use std::time::Instant; - /// The harness's end of init's signing pipe. Numbers each record, so a - /// boot's sequence has no gaps by construction. Owned by the harness. + /// The harness's end of init's signing pipes: records out, the log's + /// acknowledgments back, each a frame. Numbers each record, so a boot's + /// sequence has no gaps by construction; init sent the report at 1, so the + /// harness starts at 2. Owned by the harness. pub(crate) struct Signer { - pipe: File, + to_init: File, + from_init: File, boot: Boot, next: u64, + acked: BTreeSet, } impl Signer { + pub(crate) fn new(to_init: File, from_init: File, boot: Boot) -> Signer { + Signer { to_init, from_init, boot, next: 2, acked: BTreeSet::new() } + } + /// Numbers the body and hands it to init to sign and send; returns /// its place in the sequence. pub(crate) fn send(&mut self, body: Body) -> std::io::Result { - todo!() + let seq = self.next; + write_frame(&mut self.to_init, &Record::new(self.boot.clone(), seq, body).encode())?; + self.next += 1; + Ok(seq) } - /// Blocks until the log has acknowledged the record at `seq`. + /// Blocks until the log has acknowledged the record at `seq`. An + /// acknowledgment is a frame holding a place, big-endian. pub(crate) fn acknowledged(&mut self, seq: u64) -> std::io::Result<()> { - todo!() + while !self.acked.contains(&seq) { + let frame = read_frame(&mut self.from_init)?; + let place: [u8; 8] = frame.try_into().map_err(|_| std::io::Error::other("not an acknowledgment"))?; + self.acked.insert(u64::from_be_bytes(place)); + } + Ok(()) + } + } + + #[cfg(test)] + mod tests { + use super::Signer; + use crate::record::{Body, Boot, Exit, Record, read_frame, write_frame}; + use std::fs::File; + use std::os::fd::OwnedFd; + + fn pipe() -> (File, File) { + let (r, w) = std::io::pipe().expect("pipe"); + (File::from(OwnedFd::from(r)), File::from(OwnedFd::from(w))) + } + + /// Records leave numbered from 2 without a gap; `acknowledged` waits + /// for its place whatever order acknowledgments come in. + #[test] + fn numbers_and_waits() { + let ((mut init_reads, harness_writes), (harness_reads, mut init_writes)) = (pipe(), pipe()); + let boot = Boot::new([7; 32]); + let mut signer = Signer::new(harness_writes, harness_reads, boot.clone()); + assert_eq!(signer.send(Body::Exit(Exit::Meter)).expect("send"), 2); + assert_eq!(signer.send(Body::Exit(Exit::Limit)).expect("send"), 3); + let first = Record::decode(&read_frame(&mut init_reads).expect("frame")).expect("record"); + assert_eq!(first, Record::new(boot, 2, Body::Exit(Exit::Meter))); + for place in [3u64, 2] { + write_frame(&mut init_writes, &place.to_be_bytes()).expect("ack"); + } + signer.acknowledged(2).expect("acked"); + signer.acknowledged(3).expect("acked"); } } @@ -224,8 +273,39 @@ pub(crate) mod process { pub(crate) struct Amplification; impl Rights { + /// `to`, if every path it grants lies under one this grants for the + /// same right. pub(crate) fn attenuate(&self, to: Rights) -> Result { - todo!() + let within = |mine: &[PathBuf], theirs: &[PathBuf]| { + theirs.iter().all(|t| mine.iter().any(|m| t.starts_with(m))) + }; + if within(&self.read, &to.read) && within(&self.write, &to.write) { + Ok(to) + } else { + Err(Amplification) + } + } + } + + #[cfg(test)] + mod tests { + use super::Rights; + use std::path::PathBuf; + + fn rights(read: &[&str], write: &[&str]) -> Rights { + let paths = |ps: &[&str]| ps.iter().map(PathBuf::from).collect(); + Rights { read: paths(read), write: paths(write) } + } + + /// A child gets its parent's rights or fewer, never more. + #[test] + fn attenuates_never_amplifies() { + let parent = rights(&["/work"], &["/work/out"]); + assert!(parent.attenuate(rights(&["/work/src"], &["/work/out/a"])).is_ok()); + assert!(parent.attenuate(rights(&[], &[])).is_ok()); + assert!(parent.attenuate(rights(&["/etc"], &[])).is_err()); + assert!(parent.attenuate(rights(&[], &["/work/src"])).is_err()); + assert!(parent.attenuate(rights(&["/workshop"], &[])).is_err()); } } diff --git a/src/main.rs b/src/main.rs index 25246be..57f9a83 100644 --- a/src/main.rs +++ b/src/main.rs @@ -27,7 +27,39 @@ impl Role { /// Chooses the role from argv: `agent` by the name it was run as, the rest /// by subcommand. fn parse(args: Vec) -> Result { - todo!() + use std::os::unix::ffi::OsStrExt; + let bytes = |a: &std::ffi::OsString| a.as_bytes().to_vec(); + let name = args.first().and_then(|a| std::path::Path::new(a).file_name()); + let rest = args.get(1..).unwrap_or_default(); + match (name.map(|n| n.as_bytes()), rest) { + (Some(b"agent"), [query]) => Ok(Role::Agent { query: bytes(query) }), + (Some(b"agent"), _) => Err(Usage("usage: agent QUERY < slice".into())), + (_, [verb, query]) if verb == "run" => Ok(Role::Run { query: bytes(query) }), + (_, [verb]) if verb == "init" => Ok(Role::Init), + (_, [verb]) if verb == "harness" => Ok(Role::Harness), + _ => Err(Usage("usage: cead run QUERY < context > answer".into())), + } + } +} + +#[cfg(test)] +mod tests { + use super::Role; + + fn parse(args: &[&str]) -> Option { + Role::parse(args.iter().map(std::ffi::OsString::from).collect()).ok() + } + + /// `agent` by the name it runs as; the rest by subcommand; nothing else. + #[test] + fn roles() { + assert!(matches!(parse(&["/core/bin/agent", "find x"]), Some(Role::Agent { query }) if query == b"find x")); + assert!(matches!(parse(&["cead", "run", "q"]), Some(Role::Run { query }) if query == b"q")); + assert!(matches!(parse(&["/cead", "init"]), Some(Role::Init))); + assert!(matches!(parse(&["/proc/self/exe", "harness"]), Some(Role::Harness))); + assert!(parse(&["agent"]).is_none()); + assert!(parse(&["cead", "run"]).is_none()); + assert!(parse(&["cead"]).is_none()); } } From 09aa4dc933e7eb6f2c3ff1f1a7ff5d125fe4959c Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 12:04:36 -0600 Subject: [PATCH 18/19] Move test modules to the end of theirs, as clippy asks Co-Authored-By: Claude Opus 5.5 (1M context) --- src/machine.rs | 104 +++++++++++++++++++++++++------------------------ src/main.rs | 8 ++-- 2 files changed, 57 insertions(+), 55 deletions(-) diff --git a/src/machine.rs b/src/machine.rs index 231a8c9..c670846 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -133,36 +133,6 @@ pub(crate) mod harness { } } - #[cfg(test)] - mod tests { - use super::Signer; - use crate::record::{Body, Boot, Exit, Record, read_frame, write_frame}; - use std::fs::File; - use std::os::fd::OwnedFd; - - fn pipe() -> (File, File) { - let (r, w) = std::io::pipe().expect("pipe"); - (File::from(OwnedFd::from(r)), File::from(OwnedFd::from(w))) - } - - /// Records leave numbered from 2 without a gap; `acknowledged` waits - /// for its place whatever order acknowledgments come in. - #[test] - fn numbers_and_waits() { - let ((mut init_reads, harness_writes), (harness_reads, mut init_writes)) = (pipe(), pipe()); - let boot = Boot::new([7; 32]); - let mut signer = Signer::new(harness_writes, harness_reads, boot.clone()); - assert_eq!(signer.send(Body::Exit(Exit::Meter)).expect("send"), 2); - assert_eq!(signer.send(Body::Exit(Exit::Limit)).expect("send"), 3); - let first = Record::decode(&read_frame(&mut init_reads).expect("frame")).expect("record"); - assert_eq!(first, Record::new(boot, 2, Body::Exit(Exit::Meter))); - for place in [3u64, 2] { - write_frame(&mut init_writes, &place.to_be_bytes()).expect("ack"); - } - signer.acknowledged(2).expect("acked"); - signer.acknowledged(3).expect("acked"); - } - } /// Why a live process was ended by the harness rather than by its reply. pub(crate) enum Exhausted { @@ -252,6 +222,37 @@ pub(crate) mod harness { todo!() } } + + #[cfg(test)] + mod tests { + use super::Signer; + use crate::record::{Body, Boot, Exit, Record, read_frame, write_frame}; + use std::fs::File; + use std::os::fd::OwnedFd; + + fn pipe() -> (File, File) { + let (r, w) = std::io::pipe().expect("pipe"); + (File::from(OwnedFd::from(r)), File::from(OwnedFd::from(w))) + } + + /// Records leave numbered from 2 without a gap; `acknowledged` waits + /// for its place whatever order acknowledgments come in. + #[test] + fn numbers_and_waits() { + let ((mut init_reads, harness_writes), (harness_reads, mut init_writes)) = (pipe(), pipe()); + let boot = Boot::new([7; 32]); + let mut signer = Signer::new(harness_writes, harness_reads, boot.clone()); + assert_eq!(signer.send(Body::Exit(Exit::Meter)).expect("send"), 2); + assert_eq!(signer.send(Body::Exit(Exit::Limit)).expect("send"), 3); + let first = Record::decode(&read_frame(&mut init_reads).expect("frame")).expect("record"); + assert_eq!(first, Record::new(boot, 2, Body::Exit(Exit::Meter))); + for place in [3u64, 2] { + write_frame(&mut init_writes, &place.to_be_bytes()).expect("ack"); + } + signer.acknowledged(2).expect("acked"); + signer.acknowledged(3).expect("acked"); + } + } } /// A model's process, as the harness holds it. @@ -287,27 +288,6 @@ pub(crate) mod process { } } - #[cfg(test)] - mod tests { - use super::Rights; - use std::path::PathBuf; - - fn rights(read: &[&str], write: &[&str]) -> Rights { - let paths = |ps: &[&str]| ps.iter().map(PathBuf::from).collect(); - Rights { read: paths(read), write: paths(write) } - } - - /// A child gets its parent's rights or fewer, never more. - #[test] - fn attenuates_never_amplifies() { - let parent = rights(&["/work"], &["/work/out"]); - assert!(parent.attenuate(rights(&["/work/src"], &["/work/out/a"])).is_ok()); - assert!(parent.attenuate(rights(&[], &[])).is_ok()); - assert!(parent.attenuate(rights(&["/etc"], &[])).is_err()); - assert!(parent.attenuate(rights(&[], &["/work/src"])).is_err()); - assert!(parent.attenuate(rights(&["/workshop"], &[])).is_err()); - } - } /// What a blocked process waits on: property 18 of the spec, by /// construction. Each holds the model's turn, which enters the window @@ -363,6 +343,28 @@ pub(crate) mod process { window: Window, shell: Shell, } + + #[cfg(test)] + mod tests { + use super::Rights; + use std::path::PathBuf; + + fn rights(read: &[&str], write: &[&str]) -> Rights { + let paths = |ps: &[&str]| ps.iter().map(PathBuf::from).collect(); + Rights { read: paths(read), write: paths(write) } + } + + /// A child gets its parent's rights or fewer, never more. + #[test] + fn attenuates_never_amplifies() { + let parent = rights(&["/work"], &["/work/out"]); + assert!(parent.attenuate(rights(&["/work/src"], &["/work/out/a"])).is_ok()); + assert!(parent.attenuate(rights(&[], &[])).is_ok()); + assert!(parent.attenuate(rights(&["/etc"], &[])).is_err()); + assert!(parent.attenuate(rights(&[], &["/work/src"])).is_err()); + assert!(parent.attenuate(rights(&["/workshop"], &[])).is_err()); + } + } } /// Meters, from KeyKOS. Mirrors `spec/Cead/Meter.lean`: `charge` and `spawn` diff --git a/src/main.rs b/src/main.rs index 57f9a83..df9b2a4 100644 --- a/src/main.rs +++ b/src/main.rs @@ -42,6 +42,10 @@ impl Role { } } +fn main() -> ExitCode { + todo!() +} + #[cfg(test)] mod tests { use super::Role; @@ -62,7 +66,3 @@ mod tests { assert!(parse(&["cead"]).is_none()); } } - -fn main() -> ExitCode { - todo!() -} From 2def4b322d8f2ae482603c85a789f702310c9772 Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 12:19:07 -0600 Subject: [PATCH 19/19] Say what the three artifacts are for: a conversation that shows what cannot be stabilized Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CODE.md b/CODE.md index f494a77..9e25fe1 100644 --- a/CODE.md +++ b/CODE.md @@ -6,6 +6,8 @@ Push every invariant you can into the types, cover the rest with tests, and spen Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TLA+ specifies the system (processes and how they interleave), Lean specifies a core (a pure function and its properties), Rust is the system. +They are a conversation about the theory of the problem, not a factory. None is the source the others derive from: each stabilizes what it can (vocabulary, states, custody, proofs), so what cannot be stabilized becomes visible, such as a translation that loses something, model-facing text, or two artifacts that each agree with themselves but not with each other. Finding those places and bringing them to Roone is the work; building toward a pipeline that runs without him is not. When in doubt, ask. + 0. **Scope.** Numbered questions, one recommendation each; facts fetched before asking; each decision written into the PR description. 1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable, never looser than the system: a behaviour the spec allows and the system cannot have is a wall, so the spec changes. 2. **Slice.** A PR takes a slice of the spec. Its dependencies are probed while scoping; findings go in a PR comment, the probe is never committed.