diff --git a/AGENTS.md b/AGENTS.md index bdd4293..be810cb 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -3,7 +3,7 @@ You build; I direct, review, approve, and answer for everything that ships. Public artifacts — commits, code, docs, descriptions — carry "Roone" only, never my last name. # CONTEXT -Read these root-level files: `README.md` (what this is), `CODE.md` (workflows, environments and vocabularies by language). +Read these root-level files: `README.md` (what this is), `CODE.md` (method, vocabulary, languages). Every time you create or discover a new AGENTS.md, paste its path here: # COMMUNICATION @@ -20,6 +20,7 @@ Code is the primary documentation surface; you are its steward. Every addition carries maintenance and trust cost: default to omission, delete when behavior is preserved, merge duplicates, and let an existing artifact absorb new work before adding one. Measure complexity by branch count, not lines; reduce it with better abstractions, never by minifying or code golfing. Label uncertainty as uncertainty; volunteer absences; find problems and opportunities, don't grade. +Prefer end-to-end tests; they prove the system works. Each ends in an artifact another person can check and re-run from the same initial state. Smaller tests only where an end-to-end test cannot reach an edge cheaply. When you hit a wall — a case that doesn't fit, a spec that breaks, an assumption that fails — the wall is information: the design is wrong somewhere. Stop the invalid path, re-derive the design from first principles until the wall doesn't exist, and return control only when meaning, evidence or authority must change. NEVER patch around a wall to comply with my words — no flags, special cases, shims, parallel paths, or tests rewritten to dodge a broken rule. @@ -30,7 +31,7 @@ A blocker honestly reported is a desired outcome; a "working" deliverable built Pull Requests (PRs) are the units of work; only ever create PRs. No issues: the PR is the only record. For new work, create a draft PR from the first commit, on a branch and worktree specific to that PR. One writer per branch; both are deleted upon merge. -Branches: short kebab-case topic — `ssh-inventory`, never `feature/…`. +Branches: short kebab-case, naming the change, not the thing changed — `initial-spec`, never `spec` or `feature/…`. Commits: one imperative line; the diff is the what, the message is the why. Every PR description has these sections, kept current: @@ -39,11 +40,12 @@ Every PR description has these sections, kept current: 3. **Merge requirements** — definition of done; think like a Software Engineer PR descriptions become the squash-commit body, so write them as records of truth with links to related PRs (#PR). +Squash trades bisect granularity for readable history: the unsquashed commits stay at `refs/pull/N/head`, and `gh land` keeps the comment thread as a note in `refs/notes/pr` (fetch `+refs/notes/*:refs/notes/*`). A leaning lives in the description of the PR that will settle it. Once code settles it, the why is a doc comment. No third document. -Until its PR exists, a leaning is a comment on #7 (Horizon), in the description template. Check #7 before opening a PR; update a comment as intent clarifies; when one is ready, open its PR and delete the comment. +Only #7 (Horizon) and PRs in progress are open. Until its PR exists, a leaning is a comment on #7, in the description template; scope it there, and when it is ready, open its PR and delete the comment. -The first commit is the model, when `CODE.md` says the seed's shape demands one; its checker is green before any code exists. -The next commit is typed stubs ONLY: types and signatures, placeholder bodies, the language's type gate green. The diff defines that PR's scope; one signature per action of the model. `CODE.md` names each language's stub and gate. +The first commit is the spec, when `CODE.md` says the seed's shape demands one; its checker is green before any code exists. +The next commit is typed stubs ONLY: types and signatures, placeholder bodies, the language's type gate green. The diff defines that PR's scope; one signature per action of the spec. `CODE.md` names each language's stub and gate. Subsequent commits fill those stubs. **Zero placeholders may remain at merge. This is always a hard requirement.** `CODE.md` names what counts as a placeholder and the lints that count them. @@ -58,9 +60,7 @@ For every subsequent commit, add a comment to the PR briefly describing: 8. **Verify yourself** — the 2–3 places most worth my direct attention before merging. 9. **Next steps** — choose one of these three: additional commits (briefly describe), blocked (explain what is needed), or finished (all merge requirements met, PR is ready for review) -Before marking a PR ready, fold what is durable from its comments (decisions, the measurement, the limitation) into the description; the description lands in git, the comments stay on GitHub. - -Every milestone yields one measurement and one honest limitation, in the PR. Nothing enters that the current milestone doesn't demand. +Before marking a PR ready, fold what is durable from its comments (decisions, measurements, limitations) into the description: the description is the record, the comments its receipts. You may freely commit and push to PR branches via their worktrees. I own ALL reviews and merges, with `gh land` (squash, delete the branch, evict the worktree), never by hand. `main` is protected. diff --git a/CODE.md b/CODE.md index edcae21..8b45aa9 100644 --- a/CODE.md +++ b/CODE.md @@ -1,129 +1,116 @@ -# cead's Workflows, Environments, and Vocabularies by Language +# How cead is built: method, vocabulary, languages -Nouns are types. A noun without a type is not in the domain. +Push every invariant you can into the types, cover the rest with tests, and spend review on what neither can express. -Which model a seed gets follows from its signature: interleaving across processes is a protocol and gets TLA+; a function is a core and gets Lean; neither means no model. The model commit precedes the skeleton. +# Method -# Rust +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. +**Unpracticed until `initial-spec`; confirm the approach for each PR.** -## PR Workflow -**NOTE: These are guidelines and are still being finalized; confirm approach for each PR.** +1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable: when code disagrees with it, the spec changes in that PR. +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. +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. -- `cargo check` on every edit. `cargo clippy` and `cargo test` green before a PR is marked ready. The lints are the rules. -- The skeleton commit is types and signatures with `todo!()` bodies, `cargo check` green. It is the spec of custody; the model, when there is one, is the spec of behaviour. Review diffs landed signatures against it. -- Every noun in Vocabulary is a struct or enum. No type without a noun, no noun without a type. -- States are enums, matched exhaustively. A lifecycle over a kernel object is a typestate — a sealed memfd, a booted machine, an evicted machine — and the invalid transition does not compile. -- A signature is a custody statement: by value moves, `&T` shares, `&mut T` claims, `Arc` confesses that ownership isn't a tree. One doc comment per item: what it owns, when it drops. Get these right in the skeleton; fill commits change bodies only and state why if a signature moves. -- When the borrow checker fights the skeleton, the custody is wrong: revise and re-declare, never wrap in `Rc`. -- A trait or a generic exists only where a second implementation exists. One impl is speculation. -- Each `todo!()` must be fillable from its own file plus the public types of what it imports. If more is required, move the boundary. +- Each placeholder is fillable from its own file plus the public types of what it imports. If more is required, move the boundary. - Fill order: plain types, then leaves (no I/O, no mutable state), then orchestration. -- Tests land in the same commit as the body they test. A test whose subject is still `todo!()` is `#[ignore = "todo"]`. -- Placeholders: `todo!()`, `unimplemented!()`, `unwrap`, `expect`, `#[allow]`, `#[ignore]`. A draft may carry them; a ready PR has zero. `clippy::todo` and `clippy::unimplemented` are denied at ready alongside the workspace lints. -- `pub(crate)` is the default; `pub` is an API promise. Modules are visibility boundaries; files lag the graph, one file per stack until it shows dense-inside, sparse-outside. -- Two failure modes: traits everywhere is Java in Rust; free functions passing `&mut world` is C in Rust. -- The call table is the single source. Builtins, exec policy, prompt lines and man text render from it; never a second list. Two calls; new capability arrives as state or a well-known CLI. -- The model's side of the boundary is untyped and GNU-flavoured. Types live between the shell and the kernel, never in the shell. -- For any new piece of code: which side of which contract is it on (model-facing, guest tool, harness, observer, host)? what is its source of stability (written spec, ABI promise, pinned version, none)? if below the ABI, what is the re-validation step when the pinned kernel changes? if it widens the model-facing surface, is it GNU-flavoured POSIX or a third call in disguise? - -## Environment +- Tests are end to end first (AGENTS.md). A leaf test lands in the commit that fills its subject. +- The checker counts two marks; review reads them: + - **frontier**: placeholders, the shape promised and not delivered. Zero at merge. + - **claim**: an assertion the checker cannot verify, each with its reason. Review reads every one. + +## Boundaries + +- Which side of which contract is new code on: model-facing, guest tool, harness, observer, host? What is its source of stability: written spec, ABI promise, pinned version, none? Below the ABI, what re-validates it when the pinned kernel changes? +- The model's side is untyped and GNU-flavoured. Types live between the shell and the kernel, never in the shell. Widening the model-facing surface is GNU-flavoured POSIX or a third call in disguise. +- The call table is the single source: builtins, exec policy, prompt lines and man text render from it, never a second list. Two calls; new capability arrives as state or a well-known CLI. +- A dependency's types stay inside the boundary module that wraps it. The skeleton names our nouns; swapping a dependency is a module change. + +# 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. + +| Noun | Meaning | Home | +|---|---|---| +| cead | The project, the operator's binary, and its shell over a declaration and its state. | crate and binary `cead` | +| operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | +| machine | The unit: pinned kernel, core, task image, descriptors, calls, policy and model endpoint, booted in a microVM by a backend. | | +| declaration | The one file that pins a machine. Equal declarations are the same experiment; its hashes are the version vector. | | +| backend | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same guest, same evidence. | | +| init | PID 1 in the guest. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | +| harness | The Rust program in the machine, its memory manager. Runs each process's cycle, installs kernel policy in the fork-exec gap, supplies the calls, writes receipts. | | +| process | One harness cycle with its own cgroup, window, shell, limits and budget. Started by `run` at depth 0 or by `rlm` below it. | | +| run | One machine, one root process and its tree, one log. From the operator shell or one-shot `cead run`; the machine ends with it. | | +| step | One command and its observation. The unit of budget and of measurement. | | +| window | The context the model can address now. A cache over state. | | +| pinned | The part of the window eviction never touches: the system prompt. | | +| bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | +| limit | A cap on one process: window size, bound, steps, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | +| budget | What a process tree may spend. A parent moves part of what remains into each child, never copies it. What it counts is declaration policy. | | +| slice | The bytes a child receives on stdin, sealed. | | +| descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | +| command | What the model writes: shell over the core plus the task image. | | +| core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | +| task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | +| query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | +| call | A command whose effect is on the harness: `rlm`, `finish`. | | +| call table | The single source; renders builtins, exec policy, prompt lines, man pages. | | +| membrane | The calls as boundary: untyped argv and stdin in, typed request inside, text and exit code out. | | +| rights | What a call may do to state: read, write. | | +| authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | +| 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. | | +| verdict | The adjudication of a command: permit or forbid. | | +| observer | eBPF keyed by cgroup, outside the model's reach. | | +| receipt | One record per command, three streams under one invocation id: intent, adjudication, witness. | | +| log | The append-only sequence of receipts, a flat file on the host. A finished run cites its hash. | | +| snapshot | The whole guest at an instant. The fork mechanism. | | +| model endpoint | Where inference is, reached only through the host proxy; keys never enter the guest. | | +| contract | One of the three lines everything else is swappable between. | | +| ring | A privilege layer: model processes; harness and observer; host. | | +| evict | Dispose at any tier: window span, KV block, process, machine. | | -- Stable toolchain, pinned in `rust-toolchain.toml`. -- Workspace lints, not prose: +# Rust - ```toml - [workspace.lints.rust] - unsafe_code = "forbid" - unreachable_pub = "warn" +## Types are the schema - [workspace.lints.clippy] - unwrap_used = "deny" - expect_used = "deny" - ``` +The language enforces, always: +1. Entity integrity: every value has exactly one owner. +2. Referential integrity: no reference outlives what it refers to. +3. Isolation: no write can falsify a live view. +4. Uniqueness: at most one impl per (type, trait) pair. +5. Encapsulation: invariants are established only by code with access to the fields. - Tests lift the unwrap lints with `#![cfg_attr(test, allow(...))]`. 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. -- One published crate, `cead`. When the workspace splits (core, guest, observer, host, backends) members are `publish = false`; `cead` stays the only public name. -- 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. Guest crates are `#![cfg(target_os = "linux")]` and use linux_raw and Linux-only crates freely. -- The core (brush, uutils, grep, git, sqlite3) is nix-built and static. - -## Vocabulary - -- **cead**: the project, the operator's binary, and its shell over a declaration and its state. -- **operator**: the human at depth 0. Types `cead` or `cead run`; never types a call. -- **machine**: the unit. A pinned kernel, core, task image, descriptors, calls, policy and model endpoint, booted in a microVM by a backend. -- **declaration**: the one file that pins a machine. Equal declarations are the same experiment. Its hashes are the version vector. -- **backend**: what boots a machine. Firecracker on Linux, Virtualization.framework on macOS. Same guest, same evidence. -- **init**: PID 1 in the guest. Assembles the view (task image as root, overlay, core first on PATH, descriptors mounted), applies policy, execs the harness. -- **harness**: the Rust program in the machine and its memory manager. Runs each process's cycle, installs kernel policy in the fork-exec gap, supplies the calls, writes receipts. -- **process**: one harness cycle with its own cgroup, window, shell, limits and budget. Started by `run` at depth 0 or by `rlm` below it. -- **run**: one machine, one root process and its tree, one log. Started from the operator shell or one-shot by `cead run`; the machine ends with it. -- **step**: one command and its observation. The unit of budget and of measurement. -- **window**: the context the model can address now. A cache over state. -- **pinned**: the part of the window eviction never touches: the system prompt. -- **bounded**: output admitted to the window; constructible only by truncation. The remainder **spills** to a file. -- **limit**: a cap on one process, whatever its place in the tree: window size, bound, steps, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. -- **budget**: what a process tree may spend. A parent moves part of what remains into each child, never copies it, so the tree never spends more than the root was given. Closest to a cgroup, but split rather than shared. What it counts is declaration policy. -- **slice**: the bytes a child receives on stdin, sealed. -- **descriptor**: state the model holds this session, bound to an object with rights. Minted by cead, never discovered. A capability. A child's is **attenuated**. -- **command**: what the model writes. Shell over the core plus the task image. -- **core**: the invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. -- **task image**: the tools one task brings. A read-only OCI image with a label declaring its tools, attached at boot. Postgres, a container engine, an interpreter: task tools. -- **query**: the argv of `run` or `rlm`: what the operator or a parent asks for, commit-message sized. Anything longer is context. The RLM paper's word. -- **call**: a command whose effect is on the harness. `rlm`, `done`. -- **call table**: the single source. Renders builtins, exec policy, prompt lines, man pages. -- **membrane**: the calls as boundary: untyped argv and stdin in, typed request inside, text and exit code out. -- **rights**: what a call may do to state: read, write. -- **authority**: how far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. -- **policy**: the rows of the call table, written in Cedar, compiled to seccomp and Landlock and installed in the kernel before exec. Permit-all is a declared policy, not an absence. -- **verdict**: the adjudication of a command: permit or forbid. -- **observer**: eBPF keyed by cgroup, outside the model's reach. -- **receipt**: one record per command, three streams under one invocation id: intent, adjudication, witness. -- **log**: the append-only sequence of receipts, a flat file on the host. A finished run cites its hash. -- **snapshot**: the whole guest at an instant. The fork mechanism. -- **model endpoint**: where inference is. An API, a local server, later the same box. Reached only through the host proxy; keys never enter the guest. -- **contract**: one of the three lines everything else is swappable between. -- **ring**: a privilege layer: model processes, harness and observer, host. -- **evict**: dispose at any tier: window span, KV block, process, machine. +Soundness: no sequence of safe operations commits a state that violates the schema. +Everything else (fields, structs and enums, most traits, invariants like `len ≤ capacity`) is a choice, held only by privacy, tests or proofs. To tell which: change the line and run `cargo check`. If it still compiles, it was a choice, yours or an agent's. -# TLA+ +## Idioms -## PR Workflow -**NOTE: Unpracticed; confirm approach for each PR.** - -- A seed whose signature interleaves across processes is a protocol and gets a TLA+ model before the skeleton. Candidates: the fork–exec gap, log/snapshot/fork, the budget tree. -- The model commit is `spec/.tla` with its `.cfg`, beside the crate it models. TLC is green before any Rust exists; the commit line records the bounds it passed at. -- Each action in the spec names one skeleton signature; the resolution commit for that signature names the action. Where model and code diverge, the commit says so. -- A PR that changes a protocol re-runs TLC. By hand until CI is demanded. +- States are enums, matched exhaustively. A lifecycle over a kernel object is a typestate (a sealed memfd, a booted machine) and the invalid transition does not compile. +- A signature is a custody statement: by value moves, `&T` shares, `&mut T` claims, `Arc` confesses that ownership isn't a tree. +- When the borrow checker fights the skeleton, the custody is wrong: revise and re-declare, never wrap in `Rc`. +- A trait or a generic exists only where a second implementation exists. +- `pub(crate)` is the default; `pub` is an API promise. Modules are visibility boundaries; files lag the graph, one file per stack until it shows dense-inside, sparse-outside. +- Two failure modes: traits everywhere is Java in Rust; free functions passing `&mut world` is C in Rust. +- Frontier: `todo!()`, `unimplemented!()`, `unwrap`, `expect`, `#[ignore]`. Claim: `unreachable!()` and `#[expect(lint, reason = "…")]`; `#[allow]` does not exist here. An `unreachable!()` is a state the types failed to make impossible: try that first. ## Environment -- TLA+ tools (SANY, TLC), Java. The tools version is recorded in the commit line with the bounds. +- 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. +- One published crate, `cead`. When the workspace splits (core, guest, observer, host, backends) 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. Guest crates are `#![cfg(target_os = "linux")]` and use linux_raw and Linux-only crates freely. +- The core is nix-built and static. -## Vocabulary +# TLA+ -- **spec**: a formula over behaviours of a state machine. -- **action**: one state transition. Maps to one signature. -- **invariant**: what every reachable state satisfies. What TLC checks. -- **instance**: the bounds TLC searched. A proof only up to them. +- Modules are `spec/.tla` with `.cfg`; the system spec is `spec/cead.tla`. TLC is green before any Rust exists; 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. +- **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 -## PR Workflow -**NOTE: Unpracticed; confirm approach for each PR.** - -- A seed whose signature is a pure function is a core and gets a Lean model before the skeleton. Candidates: `Budget::split`, eviction, the export schema round-trip, the pinned-prompt renderer. -- The model commit is a theory in the `model/` lake project: an executable definition plus theorems, `lake build` green before any Rust exists. -- A differential test feeds the same random inputs through the model and the Rust and compares outputs, in `cargo test`. It is the only thing that ties the two. How model outputs reach `cargo test` is open; the first Lean PR decides. -- First model: `Budget`, after the first loop ships. It measures the floor: toolchain cost and the differential bridge. - -## Environment - -- Lean 4 via elan, toolchain pinned in `lean-toolchain`, one lake project at `model/`. - -## Vocabulary - -- **model**: the executable Lean definition of a core function. -- **theorem**: a property proved of the model. -- **differential test**: random inputs through model and Rust, outputs compared. +- Lean 4 via elan, toolchain pinned in `lean-toolchain`, one lake project in `spec/`. `lake build` green before any Rust exists. +- **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. How spec outputs reach `cargo test` is for the first Lean PR. diff --git a/Cargo.toml b/Cargo.toml index 1a65eb3..d8b824d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -8,6 +8,11 @@ unreachable_pub = "warn" [workspace.lints.clippy] unwrap_used = "deny" expect_used = "deny" +todo = "warn" +unimplemented = "warn" +unreachable = "warn" +allow_attributes = "deny" +allow_attributes_without_reason = "deny" [package] name = "cead" diff --git a/README.md b/README.md index 684a576..349fd84 100644 --- a/README.md +++ b/README.md @@ -160,8 +160,8 @@ Rules beyond that come with the first release. It is a sub-agent, built from process structure rather than at the application layer. - Forking, of the machine. A snapshot of a running machine boots another machine that diverges from the same state. -- Done. - `done` ends a process with its answer; when the root process is done, the run is over and the machine is gone. +- Finish. + `finish` ends a process with its answer; when the root process finishes, the run is over and the machine is gone. ### Data diff --git a/clippy.toml b/clippy.toml new file mode 100644 index 0000000..0358cdb --- /dev/null +++ b/clippy.toml @@ -0,0 +1,2 @@ +allow-unwrap-in-tests = true +allow-expect-in-tests = true diff --git a/rust-toolchain.toml b/rust-toolchain.toml index b73c15e..13eb3e2 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,2 +1,3 @@ [toolchain] channel = "1.98.0" +components = ["clippy"]