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/CODE.md b/CODE.md index e07056e..9e25fe1 100644 --- a/CODE.md +++ b/CODE.md @@ -6,10 +6,13 @@ 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. +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. -3. **Core.** A pure function with a property worth proving gets its Lean spec first, green before any Rust. -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. +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.** 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 +31,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 outside tests 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 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` | -| 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 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 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, writes records. | | -| 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. | | -| 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` | +| 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` | +| 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 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` | +| 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. 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`, `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. | | +| 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`, `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. | | -| 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 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` | +| 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 @@ -108,7 +124,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. @@ -117,11 +133,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. 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/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.lean b/spec/Cead.lean new file mode 100644 index 0000000..5b2d2c3 --- /dev/null +++ b/spec/Cead.lean @@ -0,0 +1,5 @@ +import Cead.Codec +import Cead.Record +import Cead.Log +import Cead.Window +import Cead.Meter diff --git a/spec/Cead/Codec.lean b/spec/Cead/Codec.lean new file mode 100644 index 0000000..fcf87d5 --- /dev/null +++ b/spec/Cead/Codec.lean @@ -0,0 +1,212 @@ +/-! +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 + +/-- 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. -/ +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 + +/-- 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 + 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/Differential.lean b/spec/Cead/Differential.lean new file mode 100644 index 0000000..a9c3b8b --- /dev/null +++ b/spec/Cead/Differential.lean @@ -0,0 +1,195 @@ +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⟩ + +/-- 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 + 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 (← fixed32) (← u64) + | _ => return .recovery (← fixed32) (← 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 (← fixed32) (← 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 (← fixed32)) + | 1 => return .exit .meter + | 2 => return .exit .limit + | _ => return .exit .timeout + +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 + 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}" + +/-- 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 + 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 = 32 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 + | ["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 | log RUNS LEN SEED | meter RUNS OPS SEED | replay LOG BOOT PROC" + return 64 diff --git a/spec/Cead/Log.lean b/spec/Cead/Log.lean new file mode 100644 index 0000000..1d56971 --- /dev/null +++ b/spec/Cead/Log.lean @@ -0,0 +1,234 @@ +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 attestation is +verified by then too (attested) or accepted as `unattested` (trusted-host +mode). Everything that depends on the log is here. +-/ +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 Boot + | .report (.recovery b _) .. => some b + | _ => none + +section +variable (log : Log) + +def Logged (b : Boot) (s : UInt64) : Prop := ∃ r ∈ log, r.boot = b ∧ r.seq = s + +def Vouched (b : Boot) : Prop := Logged log b 1 + +def Exited (b : Boot) : Prop := ∃ r ∈ log, r.boot = b ∧ r.body.isExit + +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 +instance : Decidable (Exited log b) := by unfold Exited; infer_instance +instance : Decidable (Recovered log b) := by unfold Recovered; infer_instance +end + +/-- 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 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 ∧ 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 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 ∧ Admits log r then some (log ++ [r]) else none + +/-- The snapshot a fork or recovery booted from. -/ +def Body.source : Body → Option (Boot × 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 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 + /-- 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 + +theorem valid_nil : Valid [] := by + constructor <;> simp [Exited] + +section Proofs +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⟩ + +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 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 log r = some log') : log' = log ++ [r] := by + unfold accept at h; split at h <;> simp_all + +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, 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 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] + · 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 _ _ _ _ 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 + · exact logged_append hadm.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 _ _ _ _ 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 _ _ _ _ _) + · 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 _ _ _ _ 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 _ _ _ _ _) + · -- 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 + +/-- The logs `accept` builds from empty, one record at a time. -/ +inductive Accepted : Log → Prop + | nil : Accepted [] + | 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 log) : Valid log := by + induction h with + | nil => exact valid_nil + | cons _ ha ih => exact accept_valid ih ha + +end Proofs +end Cead 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/Record.lean b/spec/Cead/Record.lean new file mode 100644 index 0000000..13bda2f --- /dev/null +++ b/spec/Cead/Record.lean @@ -0,0 +1,201 @@ +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 + +/-- 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 : Boot) (last : UInt64) + | recovery (boot : Boot) (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 Attestation where + | unattested + | snp (report : Blob) +deriving DecidableEq + +/-- 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 (returned : Blob) + | allow + | spawn (child : UInt64) (query : Blob) +deriving DecidableEq + +/-- 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 and process with the call's other two. +Together they hold what the call added to its process's window. -/ +inductive Event where + /-- 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; `returned` what the + call returned to the model: the output if it fit the bound, else where it + spilled. -/ + | 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 : Digest) + | meter + | limit + | timeout +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) +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 : Boot + seq : UInt64 + body : Body +deriving DecidableEq + +namespace Codec + +def bootU64 : Codec (Boot × UInt64) := pair (fixed 32) u64 + +private def OriginT : Fin 3 → Type + | 0 => Unit | 1 => Boot × UInt64 | 2 => Boot × UInt64 + +def origin : Codec Origin := + 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) + (by intro o; cases o <;> rfl) + +private def AttestationT : Fin 2 → Type + | 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) + +private def DecisionT : Fin 3 → Type + | 0 => Blob | 1 => Unit | 2 => UInt64 × Blob + +def decision : Codec Decision := + 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 := + 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 WaitStatusT : Fin 2 → Type + | 0 => UInt8 | 1 => UInt8 + +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 × 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 (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⟩ + | .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 + | 0 => Digest | 1 => Unit | 2 => Unit | 3 => Unit + +def exit : Codec Exit := + 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) + (by intro e; cases e <;> rfl) + +private def BodyT : Fin 3 → Type + | 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 (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) + (by intro b; cases b <;> rfl) + +def record : Codec Record := + iso (pair (fixed 32) (pair u64 body)) + (fun (b, s, x) => ⟨b, s, x⟩) + (fun r => (r.boot, r.seq, 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/Cead/Window.lean b/spec/Cead/Window.lean new file mode 100644 index 0000000..2085b48 --- /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 : Boot) + +/-- 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.cfg b/spec/cead.cfg index 7e085b5..df69477 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 @@ -30,6 +31,8 @@ INVARIANTS WithinMeter Attenuated KillReach + BlockedWaits + ProcessTree PROPERTIES LogOnlyGrows diff --git a/spec/cead.tla b/spec/cead.tla index 0f14130..d41e3b4 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,34 +53,48 @@ 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 +\* 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 -\* record. A call's intent, decision and witness carry its id and command; -\* the exit record carries id 0 and why the boot ended. +\* 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. +\* 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, - from : Boots \cup {None}, last : 0..MaxSeq] + 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; -\* `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] @@ -90,18 +105,22 @@ 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 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] +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] + 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. @@ -148,6 +167,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 +183,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 +205,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 +213,39 @@ 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) == +\* 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" - /\ LET r == Rec(b, seq[b] + 1, 0, "exit", reason) + /\ ps[b, RootProc].state = "zombie" + /\ unwitnessed[b] = {} + /\ 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] /\ 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 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) == @@ -222,7 +253,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 +262,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 +276,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, @@ -255,7 +286,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 @@ -267,11 +298,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; 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. @@ -286,39 +317,56 @@ 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])] - /\ transit' = transit \cup - {Rec(b, s + 1, i, "decision", c), Rec(b, s + 2, i, "witness", c)} - /\ seq' = [seq EXCEPT ![b] = s + 2] + 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]}] /\ 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 + /\ 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' = Done(t) + IN /\ ps' = t /\ intent' = [CutOff(b, q) EXCEPT ![b, p] = NoRecord] - ELSE ps' = Done(ps) + /\ transit' = transit \cup {D(None)} + ELSE ps' = ps /\ transit' = transit \cup {D(None)} ELSE /\ executed' = executed - /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} - /\ seq' = [seq EXCEPT ![b] = s + 1] - /\ ps' = Done(ps) + /\ unwitnessed' = unwitnessed + /\ transit' = transit \cup {D(None)} + /\ 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 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, e.proc)} + /\ 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. -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,20 +376,18 @@ 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. +\* 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 - /\ UNCHANGED <> + IN ps' = IF ps[b, p].waits = q THEN [t EXCEPT ![b, p].waits = None] ELSE t + /\ UNCHANGED <> ----------------------------------------------------------------------------- (* Records in transit: outside the machine, so they go on after eviction *) @@ -352,7 +398,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) == @@ -366,7 +412,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 +431,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)) @@ -402,7 +449,8 @@ 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 /\ log \subseteq Record @@ -433,17 +481,18 @@ 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 -\* 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. @@ -492,4 +541,39 @@ 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"} + +\* 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/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..6ba4ee8 --- /dev/null +++ b/spec/lakefile.toml @@ -0,0 +1,9 @@ +name = "cead" +defaultTargets = ["Cead"] + +[[lean_lib]] +name = "Cead" + +[[lean_exe]] +name = "differential" +root = "Cead.Differential" 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 diff --git a/spec/tree.cfg b/spec/tree.cfg index 57f65df..32670e8 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 @@ -30,6 +31,8 @@ INVARIANTS WithinMeter Attenuated KillReach + BlockedWaits + ProcessTree PROPERTIES LogOnlyGrows diff --git a/src/host.rs b/src/host.rs new file mode 100644 index 0000000..faf9b06 --- /dev/null +++ b/src/host.rs @@ -0,0 +1,511 @@ +//! 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::{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; + + /// A record whose signature checked against its boot's key and, for a + /// 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, malformed, or attested in a way + /// this build cannot check. + #[derive(Debug)] + pub(crate) struct Forged; + + impl Verified { + 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 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, + } + + /// 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. + #[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 another record at or before + /// the report's place. + 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, + /// 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 { + 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, 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() + && 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"); + } + } +} + +/// 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 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 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, + } + + /// 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 { + 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 new file mode 100644 index 0000000..c670846 --- /dev/null +++ b/src/machine.rs @@ -0,0 +1,885 @@ +//! 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, 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 { + Boot::of(&self.0) + } + + pub(crate) fn sign(&self, bytes: &[u8]) -> Signature { + 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); + } + } + + /// 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, 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 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 { + 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 { + 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`. An + /// acknowledgment is a frame holding a place, big-endian. + pub(crate) fn acknowledged(&mut self, seq: u64) -> std::io::Result<()> { + 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(()) + } + } + + + /// 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!() + } + } + + #[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. +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 { + /// `to`, if every path it grants lies under one this grants for the + /// same right. + pub(crate) fn attenuate(&self, to: Rights) -> Result { + 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) + } + } + } + + + /// 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, + } + + #[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` +/// 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. + #[derive(Debug)] + struct Metered { + parent: Option, + cap: u64, + meter: u64, + calls: u64, + } + + /// 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 { + 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 { + 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> { + 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"); + } + } +} + +/// 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::{Body, Boot, Decision, Event, ProcId, Record}; + + #[derive(Debug, Clone, PartialEq, Eq)] + pub(crate) enum Role { + System, + User, + Assistant, + } + + /// 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 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 { + 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, its turn and what it returned, if both fit. + pub(crate) fn push(&mut self, turn: Vec, returned: Vec) -> Result<(), Full> { + 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] { + &self.spans + } + } + + /// 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> { + 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) + } + + #[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"); + } + } +} + +/// 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 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), + Spilled { path: PathBuf, size: u64 }, + } + + impl Bounded { + /// 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 && std::str::from_utf8(&output).is_ok() { + 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 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 { + 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"); + let binary = Bounded::admit(vec![0xff, 0xfe], 64, &spill).expect("admit"); + assert!(matches!(binary, Bounded::Spilled { size: 2, .. }), "bytes that are not text spill"); + } + } +} + +/// 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..df9b2a4 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1 +1,68 @@ -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 { + 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())), + } + } +} + +fn main() -> ExitCode { + todo!() +} + +#[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()); + } +} diff --git a/src/record.rs b/src/record.rs new file mode 100644 index 0000000..54e9d09 --- /dev/null +++ b/src/record.rs @@ -0,0 +1,597 @@ +//! 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. +#[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); + +// 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 { + 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); + + 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)] +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. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +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. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +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. +#[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. + Snp(Vec), +} + +/// 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 }, + 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. +#[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 }, + 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. +#[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 }, + Meter, + Limit, + Timeout, +} + +/// Bytes that are no record's encoding. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +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 seq(&self) -> u64 { + self.seq + } + + 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(); + self.write(&mut out); + out + } + + /// The record these bytes encode, if they encode exactly one. + pub(crate) fn decode(bytes: &[u8]) -> Result { + let mut r = Reader(bytes); + let record = Record::read(&mut r)?; + if r.0.is_empty() { Ok(record) } else { Err(Malformed) } + } +} + +/// 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. + +/// 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); + } + let (head, rest) = self.0.split_at(n); + self.0 = rest; + Ok(head) + } + + pub(crate) fn tag(&mut self) -> Result { + Ok(self.take(1)?[0]) + } + + 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)) + } + + pub(crate) 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)] +pub(crate) mod tests { + use super::Record; + use std::process::Command; + + /// Runs the Lean half of the differential test (`spec/Cead/Differential.lean`), + /// 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 = 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"); + 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() + } + + /// 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. + #[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"); + } +}