From 3512a4583ff802180df9ac54db8947cbc0cc555e Mon Sep 17 00:00:00 2001 From: Roone Date: Tue, 29 Sep 2026 00:06:56 -0600 Subject: [PATCH] Write down the method as practiced in #11, and let evidence outrank every artifact Co-Authored-By: Claude Opus 5.5 (1M context) --- AGENTS.md | 3 ++- CODE.md | 11 ++++++----- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index be810cb..0223ea3 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -26,6 +26,7 @@ When you hit a wall — a case that doesn't fit, a spec that breaks, an assumpti 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. Building around a blocker is failure and will always be rejected, sunk cost irrelevant. A blocker honestly reported is a desired outcome; a "working" deliverable built on duct tape is sabotage. +Evidence outranks every artifact: when code or a measurement disagrees with a spec, doc or decision, change it in that PR; never defend it. # GITHUB Pull Requests (PRs) are the units of work; only ever create PRs. No issues: the PR is the only record. @@ -44,7 +45,7 @@ Squash trades bisect granularity for readable history: the unsquashed commits st 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. 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 spec, when `CODE.md` says the seed's shape demands one; its checker is green before any code exists. +When a PR changes what the spec says, its first commit is that change, TLC green, before any code. 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. diff --git a/CODE.md b/CODE.md index f4412a5..e07056e 100644 --- a/CODE.md +++ b/CODE.md @@ -5,9 +5,8 @@ Push every invariant you can into the types, cover the rest with tests, and spen # Method 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.** -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. +1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable. 2. **Slice.** A PR takes a slice of the spec. Its dependencies are probed while scoping; findings go in a PR comment, the probe is never committed. 3. **Core.** A pure function with a property worth proving gets its Lean spec first, green before any Rust. 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. @@ -116,11 +115,13 @@ Everything else (fields, structs and enums, most traits, invariants like `len # TLA+ -- 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`). TLC is green before any Rust exists; the commit line records the TLA+ tools version and the bounds it passed at. +- 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. +- 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 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. +- Lean 4 via elan, toolchain pinned in `lean-toolchain`, one lake project in `spec/`. `lake build` green before the Rust it specifies. +- **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.