From 44a703957167a701410545267b1a0107ae0a26f1 Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 00:38:16 -0700 Subject: [PATCH 1/7] RFC-5: an RFC process, and RFCs as files MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Proposals live in the issue tracker, documents live in `.design/`, and requirements live in the registry, and none of the three references the others. An issue is a report — one author, one body, open or closed — so an amendment becomes a comment and the document a reader sees first is its stalest version. This makes an RFC a file with front matter, one PR per RFC, always merged so a rejection keeps its reasoning, and `introduces:` linking an RFC to the requirements it creates. Implementation status is then derived from the registry rather than declared, and a version is derived from git rather than written down. Ships with its gate (`tooling/rfc-check.py`, wired into CI) and its own three requirements, so the proposal is checked by the mechanism it proposes. --- .design/reqs/registry.toml | 60 ++++++++ .design/rfcs/0005-rfc-process.md | 227 +++++++++++++++++++++++++++++++ .github/workflows/ci.yml | 2 + tooling/rfc-check.py | 226 ++++++++++++++++++++++++++++++ 4 files changed, 515 insertions(+) create mode 100644 .design/rfcs/0005-rfc-process.md create mode 100755 tooling/rfc-check.py diff --git a/.design/reqs/registry.toml b/.design/reqs/registry.toml index 2073e863..8ea9f417 100644 --- a/.design/reqs/registry.toml +++ b/.design/reqs/registry.toml @@ -17692,3 +17692,63 @@ note = "The kernel-image job builds a fresh tracked-source image, verifies deter kind = "file" target = "platform/x86_64-pc-uefi-smp-v1/test-qemu.py" note = "Fail-closed serial protocol validator for the complete release matrix and terminal power actions." + +[[requirement]] +id = "REQ-RFC-FRONTMATTER" +title = "RFC front-matter schema" +owner = ".design/rfcs" +status = "shipped" +scope = "docs" +summary = "Every RFC is a file under .design/rfcs/ carrying rfc/title/status front matter, with optional supersedes, introduces and discussion fields." +contributors = [".design/rfcs/0005-rfc-process.md", "tooling/rfc-check.py"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "file" +target = ".design/rfcs/0005-rfc-process.md" +note = "the schema, and the RFC that defines it" + +[[requirement.evidence]] +kind = "symbol" +target = "parse_front_matter" +note = "front-matter reader" + +[[requirement]] +id = "REQ-RFC-GATE" +title = "RFC front-matter gate" +owner = "tooling/rfc-check.py" +status = "shipped" +scope = "docs" +summary = "CI rejects an RFC with missing or malformed front matter, a status outside the enum, a number disagreeing with its filename, or a number colliding with a non-draft RFC." +contributors = [".design/rfcs/0005-rfc-process.md", ".github/workflows/ci.yml"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "symbol" +target = "check" +note = "the gate" + +[[requirement.evidence]] +kind = "command" +target = "python3 tooling/rfc-check.py" +note = "CI step" + +[[requirement]] +id = "REQ-RFC-REGISTRY-LINK" +title = "RFC to REQ registry link" +owner = "tooling/rfc-check.py" +status = "shipped" +scope = "docs" +summary = "An RFC declares the requirements it introduces, and the gate rejects a name absent from the registry, so implementation status is derived from the registry rather than declared in the RFC." +contributors = [".design/reqs/registry.toml", ".design/rfcs/0005-rfc-process.md"] +generated_to = ["status"] + +[[requirement.evidence]] +kind = "symbol" +target = "known_reqs" +note = "registry reader" + +[[requirement.evidence]] +kind = "file" +target = ".design/reqs/registry.toml" +note = "the registry the link resolves against" diff --git a/.design/rfcs/0005-rfc-process.md b/.design/rfcs/0005-rfc-process.md new file mode 100644 index 00000000..05f64a63 --- /dev/null +++ b/.design/rfcs/0005-rfc-process.md @@ -0,0 +1,227 @@ +--- +rfc: 5 +title: An RFC process, and RFCs as files +status: draft +supersedes: [] +introduces: + - REQ-RFC-FRONTMATTER + - REQ-RFC-GATE + - REQ-RFC-REGISTRY-LINK +--- + +# An RFC process, and RFCs as files + +This RFC proposes the process it is being submitted through, so its own PR is the +worked example. + +## The problem + +Three things that should reference each other live in three places that do not. + +| | where it lives today | +|---|---| +| the **proposal** | a GitHub issue — RFC-1 is #2, RFC-2 is #119, RFC-3 is #120, and one is unnumbered | +| the **document** | `.design/` — `stage1-forge-tier.md`, `stage3-bv-reconstruction.md`, and the rest | +| the **requirements** | `.design/reqs/registry.toml`, generating a status table with evidence links | + +An issue is the wrong primitive for the first of those. An issue is a **report**: +one author, one body, open or closed. A proposal needs versions, a status that is +not binary, and amendment history. On an issue, amendments become comments, so +the document a reader sees first is the stalest version of it. + +The registry is the hard half and it already exists, from #17. What is missing is +the link in both directions: an RFC has no path to becoming tracked work, and a +REQ has no path back to the proposal that motivated it. + +**#17 is the worked example of the whole problem.** It is an RFC that proposed +the canonical REQ registry, it shipped, and it never got a number — so it does +not appear in any sequence, its document is an issue body, and nothing connects +it to the requirements it created. An RFC that built the requirement-tracking +system is itself untracked. + +## Proposal + +RFCs become files. + +``` +.design/rfcs/0004-verified-effect-rows.md +``` + +```yaml +--- +rfc: 4 +title: Verified effect rows +status: draft | accepted | rejected | superseded +supersedes: [] +introduces: [REQ-EFFECT-ROW-REGIONS, REQ-EFFECT-ROW-CONFLICT] +discussion: https://github.com/dollspace-gay/Thermite/issues/119 +--- +``` + +### One PR per RFC + +Review happens line by line on the document rather than in a thread about a first +post that has since been superseded. The PR is the discussion until the RFC +lands. + +### A draft's number is provisional; merging makes it canonical + +Take the next free number when you write it, so the RFC is citable while it is +being argued about — "RFC-6" beats "the one in PR 214". The file is +`0006-slug.md` from the first commit. + +**While `status: draft`, that number is provisional.** No extra field says so; +`draft` already means it. If two RFCs are drafted concurrently and collide, or a +reviewer wants a different slot, the number moves at merge and the file is +renamed in the merge commit. Once the status leaves `draft`, the number is +canonical and never moves again. + +That is where the flexibility belongs. A number that is fixed the moment someone +opens a PR turns an ordering question into a race; a number that does not exist +until merge cannot be cited during the review that decides it. + +The gate enforces the distinction rather than the etiquette: + +| | | +|---|---| +| two non-draft RFCs share a number | **error** | +| a draft collides with a non-draft | **error** — the draft moves | +| two drafts share a number | reported, not fatal — merge resolves it | + +Using the PR number instead was considered and rejected: it would jump the +sequence to a large sparse number interleaved with every other PR. + +### Always merge, never close + +A rejected RFC merges with `status: rejected`. Closing the PR instead would +discard the reasoning, which is the part worth keeping — the argument for why +something was *not* done is the expensive thing to reconstruct later. + +### `introduces:` feeds the registry + +The RFC declares the REQs it creates. The registry tracks whether they shipped. +The generated status table becomes the RFC's progress view without anyone +maintaining one. + +So there is deliberately **no `implemented` status**. Whether an RFC is +implemented is computable — all of its REQs shipped — and a hand-maintained field +would drift from the registry, which is the failure the registry exists to +prevent. + +### Versions are derived, not declared + +One commit per edit of an RFC file, and a version is cited as: + +``` +RFC-4 r3 @ a1b2c3d +``` + +`r3` is the number of commits that have touched that file; `a1b2c3d` pins the +exact content. Both are computed: + +```sh +git log --oneline -- .design/rfcs/0004-*.md | wc -l +``` + +So there is no `version:` field, for the same reason there is no `implemented` +status: a declared version drifts from the file it describes, and a derived one +cannot. + +**`git log` on the file is the amendment history**, which is the thing an issue +cannot provide. An RFC that changed three times shows three diffs, each with a +message saying why. On an issue, an amendment is a comment and the reader has to +reconstruct the document's state at each point by hand. + +One consequence to state rather than discover: **an RFC PR should not be +squash-merged**, or its review history collapses into one commit. The natural +reading is that r1 is the RFC as merged and later revisions are amendments, with +pre-merge iteration living in the PR — which works either way, but only if the +merge is not a squash when the iteration is worth keeping. + +### `discussion:` names where the argument lives, when it is not here + +Omitted for a new RFC, because its PR is the discussion and `git log` links the +two. Present on a migrated one, pointing at the issue it came from, so a +conversation in flight is not orphaned by the move. + +## Migration + +All three existing RFCs move, and the two live ones are the point. + +| RFC | issue | state | what the move looks like | +|---|---|---|---| +| RFC-1 | #2 | closed | the terminal case: a document with a resolved status and an archived discussion | +| RFC-2 | #119 | open | a document now, its discussion still at #119 | +| RFC-3 | #120 | open | same | +and the sequence is renumbered so it is chronological: + +| RFC | issue | filed | was | is | +|---|---|---|---|---| +| Thermite 2 | #2 | first | RFC-1 | RFC-1 | +| Canonical REQ registry | #17 | second | *unnumbered* | **RFC-2** | +| The certification surface | #119 | third | RFC-2 | **RFC-3** | +| Versioning | #120 | fourth | RFC-3 | **RFC-4** | + +**Renumbering is done once, here, and never again.** It is possible now because +the cost is two issue titles: nothing in the tree references RFC-2 or RFC-3, and +no issue or PR body does either — checked. At any larger size it would not be +worth doing, and the convention from here is: + +> **A number is identity.** Never reused, never reassigned. Chronology is visible +> from the git history and the linked issue. + +Fixing the sequence before adopting that rule is cheaper than carrying an +anomaly under it forever. + +**The migration is a text move, not an edit.** Issue bodies are copied verbatim +and front matter is added above them. Nothing is rewritten, reordered, or +summarised — an editorial pass would put words under an author's name that they +did not write. + +**Comments stay in the issue.** The file is the document; the issue is the +discussion. That separation is the whole proposal, so applying it to the +migration is the consistent move rather than an omission. `discussion:` links +the two, and the issue links back. + +An open RFC keeps its issue open. When its discussion resolves, the issue closes +pointing at the file and `status` moves off `draft`. Nobody has to move a thread +mid-argument. + +## The gate + +`tooling/rfc-check.py`, in the style of the existing gates: stdlib only, exit +non-zero with a specific message. + +- every file in `.design/rfcs/` has valid front matter with the required fields +- `status` is one of the four values +- `rfc:` is unique, and matches the filename's numeric prefix +- every REQ in `introduces:` exists in `registry.toml` +- every `supersedes:` target exists + +The script ships with this RFC. A process proposal that asks the maintainer to +write its own enforcement is one that does not land. + +## What this does not change + +**Issues stay defect reports**, which is what they are good at. #122–#126 are +right where they belong. + +**`.design/` documents stay.** An RFC proposes a change; a design document +governs a component. They are different artifacts, and the RFC can reference the +document it will produce or amend. + +**No approval ceremony is added.** There is no review period, no shepherd, no +FCP. The proposal is a file and a PR, and the existing review is the review. + +## Why files, beyond the immediate + +A file with front matter is a record with fields. Whatever this eventually +federates to — an atproto lexicon, a static site, a generated index — reads a +directory of documents. An issue thread has no such shape, and a migration +later is strictly harder than starting here. + +## Self-hosting + +This RFC is `.design/rfcs/0005-rfc-process.md`, numbered like any other, in a PR +that is its own discussion. If the process is wrong, the artifact demonstrating it is the thing +being reviewed, which is the cheapest possible way to find out. diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f4848067..df3c8376 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -68,6 +68,8 @@ jobs: run: python3 tooling/req-status.py - name: req-registry gate (canonical status inventory) run: tooling/reqs check + - name: rfc gate (front matter, numbering, registry link) + run: python3 tooling/rfc-check.py - name: Rust build cache uses: Swatinem/rust-cache@v2 diff --git a/tooling/rfc-check.py b/tooling/rfc-check.py new file mode 100755 index 00000000..a47e4bfd --- /dev/null +++ b/tooling/rfc-check.py @@ -0,0 +1,226 @@ +#!/usr/bin/env python3 +""" +RFC front-matter gate for `.design/rfcs/`. + +RFCs are files with front matter (RFC-4). This gate keeps the directory +mechanically readable, so the generated index and the registry link cannot drift +from the documents: + + * every RFC has front matter with the required fields; + * `status` is one of draft/accepted/rejected/superseded — there is no + `implemented`, because implementation is derived from the REQ registry; + * `rfc:` agrees with the filename prefix, and is unique — except that two + *drafts* may share a number, since a draft's number is provisional until + merge and the collision is resolved there; + * every REQ named in `introduces:` exists in `.design/reqs/registry.toml`; + * every RFC named in `supersedes:` exists. + +Usage: + + python3 tooling/rfc-check.py [--root ] [--json] +""" + +from __future__ import annotations + +import argparse +import json +import re +import subprocess +import sys +from pathlib import Path + +REQUIRED = ("rfc", "title", "status") +STATUSES = ("draft", "accepted", "rejected", "superseded") +FILENAME = re.compile(r"^(\d{4})-[a-z0-9-]+\.md$") + + +def parse_front_matter(text: str) -> tuple[dict, str | None]: + """Return (fields, error). Deliberately small: a flat `key: value` block plus + `[a, b]` and `- item` lists. A full YAML parser is not a dependency worth + taking for five fields.""" + if not text.startswith("---\n"): + return {}, "no front matter (the file must open with `---`)" + end = text.find("\n---\n", 3) + if end == -1: + return {}, "front matter is not closed with `---`" + + fields: dict[str, object] = {} + key = None + for raw in text[4:end].splitlines(): + line = raw.rstrip() + if not line.strip(): + continue + if line.startswith(" - ") and key: + fields.setdefault(key, []) + if isinstance(fields[key], list): + fields[key].append(line[4:].strip()) + continue + if ":" not in line: + return {}, f"malformed front-matter line: {line!r}" + key, _, value = line.partition(":") + key, value = key.strip(), value.strip() + if value.startswith("[") and value.endswith("]"): + inner = value[1:-1].strip() + fields[key] = [v.strip() for v in inner.split(",") if v.strip()] + elif value: + fields[key] = value + else: + fields[key] = [] + return fields, None + + +def known_reqs(root: Path) -> set[str]: + registry = root / ".design" / "reqs" / "registry.toml" + if not registry.is_file(): + return set() + return set(re.findall(r"\bREQ-[A-Z0-9-]+\b", registry.read_text(encoding="utf-8"))) + + +def revision(root: Path, path: Path) -> tuple[int, str]: + """(revision number, short hash) for an RFC file — the count of commits that + touched it, and the newest. Derived rather than declared, so it cannot drift + from the file it describes. Returns (0, "") outside a git tree.""" + try: + log = subprocess.run( + ["git", "log", "--format=%h", "--", str(path.relative_to(root))], + cwd=root, capture_output=True, text=True, check=True).stdout.split() + except (subprocess.CalledProcessError, OSError, ValueError): + return 0, "" + return len(log), (log[0] if log else "") + + +def index(root: Path) -> list[dict]: + """The generated RFC index: number, title, status, and derived version.""" + rows = [] + for path in sorted((root / ".design" / "rfcs").glob("*.md")): + fields, err = parse_front_matter(path.read_text(encoding="utf-8")) + if err: + continue + rev, sha = revision(root, path) + rows.append({ + "rfc": fields.get("rfc"), + "title": fields.get("title"), + "status": fields.get("status"), + "revision": rev, + "commit": sha, + "file": path.name, + }) + return rows + + +def check(root: Path) -> list[str]: + rfc_dir = root / ".design" / "rfcs" + if not rfc_dir.is_dir(): + return [f"{rfc_dir} does not exist"] + + problems: list[str] = [] + notes: list[str] = [] + reqs = known_reqs(root) + seen: dict[int, tuple[str, str]] = {} # number -> (filename, status) + titles: dict[str, str] = {} + + for path in sorted(rfc_dir.glob("*.md")): + rel = path.relative_to(root) + name_match = FILENAME.match(path.name) + if not name_match: + problems.append(f"{rel}: filename must be NNNN-slug.md") + continue + + fields, err = parse_front_matter(path.read_text(encoding="utf-8")) + if err: + problems.append(f"{rel}: {err}") + continue + + for field in REQUIRED: + if field not in fields: + problems.append(f"{rel}: front matter is missing `{field}`") + + status = fields.get("status") + if status is not None and status not in STATUSES: + problems.append( + f"{rel}: status {status!r} is not one of {'/'.join(STATUSES)}" + " (implementation is derived from the REQ registry, not declared)" + ) + + try: + number = int(str(fields.get("rfc", "")).strip()) + except ValueError: + problems.append(f"{rel}: `rfc:` must be an integer") + continue + + if number != int(name_match.group(1)): + problems.append( + f"{rel}: `rfc: {number}` disagrees with the filename prefix" + f" {name_match.group(1)}" + ) + if number in seen: + other_name, other_status = seen[number] + if status == "draft" and other_status == "draft": + notes.append( + f"{rel}: rfc {number} is also used by {other_name};" + " both are drafts, so the number is provisional until merge" + ) + else: + problems.append( + f"{rel}: rfc {number} is already used by {other_name}" + f" (status {other_status})" + ) + seen[number] = (path.name, str(status)) + titles[path.name] = str(fields.get("title", "")) + + for req in fields.get("introduces", []) or []: + if reqs and req not in reqs: + problems.append( + f"{rel}: introduces {req}, which is not in registry.toml" + ) + + for target in fields.get("supersedes", []) or []: + try: + target_n = int(str(target).strip()) + except ValueError: + problems.append(f"{rel}: supersedes {target!r} is not an RFC number") + continue + if not any(p.name.startswith(f"{target_n:04d}-") for p in rfc_dir.glob("*.md")): + problems.append(f"{rel}: supersedes RFC-{target_n}, which does not exist") + + for note in notes: + print(f"rfc-check: note: {note}", file=sys.stderr) + return problems + + +def main(argv: list[str]) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", default=".", help="repository root") + parser.add_argument("--json", action="store_true", help="machine-readable output") + parser.add_argument("--index", action="store_true", help="print the RFC index") + args = parser.parse_args(argv) + + root = Path(args.root).resolve() + + if args.index: + rows = index(root) + if args.json: + print(json.dumps(rows, indent=2)) + else: + print("| RFC | title | status | version |") + print("|---|---|---|---|") + for r in rows: + v = f"r{r['revision']} @ {r['commit']}" if r["commit"] else "unversioned" + print(f"| {r['rfc']} | {r['title']} | {r['status']} | {v} |") + return 0 + + problems = check(root) + + if args.json: + print(json.dumps({"ok": not problems, "problems": problems}, indent=2)) + elif problems: + for p in problems: + print(f"rfc-check: {p}", file=sys.stderr) + else: + print("rfc-check: ok") + + return 1 if problems else 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) From 0639cf1fde8df72b6e466d1218c4ce4984e9c326 Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 00:38:16 -0700 Subject: [PATCH 2/7] Migrate RFC-1 from #2 Body copied verbatim; front matter added above it. Comments stay in the issue, which `discussion:` links, because the file is the document and the issue is the discussion. --- .design/rfcs/0001-thermite-2.md | 490 ++++++++++++++++++++++++++++++++ 1 file changed, 490 insertions(+) create mode 100644 .design/rfcs/0001-thermite-2.md diff --git a/.design/rfcs/0001-thermite-2.md b/.design/rfcs/0001-thermite-2.md new file mode 100644 index 00000000..5a3aac68 --- /dev/null +++ b/.design/rfcs/0001-thermite-2.md @@ -0,0 +1,490 @@ +--- +rfc: 1 +title: Thermite 2 — a dependent-type tier, a stratified cage, and new ladder boundaries +status: accepted +supersedes: [] +introduces: [] +discussion: https://github.com/dollspace-gay/Thermite/issues/2 +--- + +# RFC-1: Thermite 2 — a dependent-type tier, a stratified cage, and new ladder boundaries + +| | | +|---|---| +| **Status** | Design sketch — not shipped software | +| **Supersedes** | RFC-1-draft1, RFC-1-draft2 | +| **Baseline** | `dollspace-gay/Thermite @ 93d3cbc0` | +| **Configuration** | C3′ (decision record in §12) | +| **Follow-up** | Stage-2 metatheory sketch (stratified-FOL spine extension) | + +This document is **self-contained**: it specifies the full Thermite 2 design, not a delta against prior RFCs. + +**Contents:** [§0 Abstract](#0-abstract) · [§1 Background](#1-background-thermite-1-in-five-sentences) · [§2 Ladder + verdicts](#2-the-ladder-and-the-verdicts) · [§3 The cage (L4)](#3-the-cage-l4) · [§4 Numeric routing + @bv](#4-numeric-routing) · [§5 The forge (L3)](#5-the-forge-l3) · [§6 Syntax summary](#6-syntax-summary) · [§7 Six programs](#7-six-programs) · [§8 The agent loop](#8-the-agent-loop) · [§9 Certificates](#9-certificates) · [§10 Anti-Goodhart](#10-anti-goodhart) · [§11 Trust base](#11-the-trust-base) · [§12 Staging + decision record](#12-staging-and-the-decision-record) · [§13 Limits](#13-limits-by-theorem) + +--- + +## 0. Abstract + +Thermite 2 is a verification-mandatory programming language for AI agents. Every function carries an enforced contract; every contract clause is proven, and the proof is graded on a five-rung ladder where **rank means refutation quality**. Three proof mechanisms serve the ladder: + +- a **stratified SMT cage** (L4) — decidable by an admission test, push-button, every failure a concrete countermodel; +- a **kernel forge** (L3) — full dependent-type-theoretic propositions, proven by agent-authored proof terms checked by the Lean 4 kernel, paid in tokens, falsified by covenant; +- a **machine-semantics clause mode** (`@bv`) for bit-exact arithmetic, where everything — multiplication included — is decidable. + +Obligations the cage cannot hold escalate **up** to the forge — never down the ladder. The thesis is unchanged from Thermite 1: burn the cheap resource (compute, tokens, patience) to buy the expensive one (trust). + +## 1. Background: Thermite 1 in five sentences + +Every Thermite function makes three promises as enforced syntax — `req` (what must hold before the call), `ens` (what the result guarantees), `fx` (everything the function may touch); omitting one is a compile error, and `fx` is additionally enforced at runtime by a kernel seccomp filter derived from it. Loops carry `inv` (why the loop is right) and `dec` (why it ends). The toolchain, `forge`, proves the promises through Verus/Z3 over a deliberately small contract language and grades each item on a ladder; a contract too weak to catch sabotage is rejected by an anti-gaming battery (vacuity detection plus mutation testing). A machine-checked Lean 4 soundness spine ties the production translation to a proven reference encoder via per-run translation validation, so the whole chain re-derives on a skeptic's machine. Agents write Thermite the way they converse: declare the contract with typed holes, read the goals, fill, re-check, repeat until *all goals discharged*. + +**The problem Thermite 2 fixes.** In Thermite 1, the decidable contract fragment is a fixed menu (eight quantifier combinators with frozen SMT triggers), and a clause outside the menu slides *down* the ladder — to bounded checking or runtime monitoring. Expressiveness was paid for with assurance. The structural-limits analysis behind this RFC showed the menu's walls are theorems (undecidability of nonlinear integer arithmetic, of unrestricted quantification, of general inductive reasoning) — but also that the walls sit much further out than the menu does, and that a kernel-checked proof tier dissolves the expressiveness walls entirely at the price of a weaker refutation story. Thermite 2 therefore does two things: it pushes the decidable cage out to its principled boundary, and it adds a proof tier *above the slide* for everything past that boundary. + +## 2. The ladder and the verdicts + +Both top rungs mean *proven for every input*. They differ in what failure looks like: the cage's refutations are mechanically complete inside its fragment (a failed obligation always yields a countermodel), while the forge's refutation channel is a covenant — empirical, mandatory, but not complete. **That asymmetry decides the order, not expressiveness.** + +| rung | name | mechanism | on failure | +|---|---|---|---| +| **L4** | caged | Stratified-FOL admission (§3) + linear arithmetic + relaxed nonlinear universals (§4) + machine-width clauses (§4). Discharged by Z3/Verus; tied to source meaning by per-run translation validation against the kernel-proven reference encoder. | A countermodel: a finite structure, an integer point, or a bit pattern. Mechanically complete in-fragment. Never degraded. | +| **L3** | forged *(new)* | Full propositions in Lean 4 CIC (§5); proofs authored by the agent, checked by the kernel, axiom-gated. Receives only what the cage genuinely cannot hold — and the classifier must name *why* (a routing reason from a frozen vocabulary, never a bare refusal). | The covenant runs first — a typed generator attempts refutation before any proof search; a hit is a hard fail. Past that: a stuck goal with hypotheses and a battery hint. | +| **L2** | bounded | Kani/CBMC: proven for all inputs up to a stated size. | A concrete trace within the bound. | +| **L1** | watched | Runtime contract monitoring; violations abort. The honest seam for syscall boundaries and `fx diverge` event loops. | An abort at the violating call, in production. | +| **L0** | slag | `#[slag]` — trusted by fiat, deliberately ugly, greppable; the complete inventory of faith. | Nothing. That is what the name is for. | + +**Per-clause grading:** forge classifies each `req`/`ens`/`inv` individually; a function's level is the minimum over its clauses. An open hole — body (`?0`) or proof (`?p0`) — means the item cannot certify or build at all. + +### The seven verdicts (a closed set) + +Every obligation's outcome is one of seven verdicts — closed like the combinator registry was closed, for the same anti-laundering reason. No verdict ever converts into another silently; in particular, nothing on this list ever becomes `Proved` except `Proved`. + +| verdict | channel | meaning | the agent's move | +|---|---|---|---| +| `Proved` | any | Obligation discharged; engine + trust base recorded in the certificate | continue | +| `Counterexample` | cage | A model of the negation. Hard fail; never softened into a lower grade | fix the code or the contract — the model says which | +| `RealWitness` | nonlinear route | Refuted over the reals, but no integer counterexample found; the claim may still hold over the integers | escalate to the forge; the real point seeds the proof attempt | +| `CovenantRefuted` | forge pre-pass | The falsifier found a concrete refutation before proof search began | same as `Counterexample` — it is one | +| `Stuck(goals)` | forge | Goals remain after the tactic battery; residual goals + hypotheses returned | burn: a lemma, a restatement, or a restratification upstream | +| `KernelBudget` | forge | Elaboration or normalization exceeded its budget. Not a failure, not a pass | split the goal, raise the budget, or restructure the term | +| `Timeout` | cage | Solver resource limit — the in-fragment cost cliff, named | a profile hint follows; restructure or re-route | + +Two verdicts encode theorems. `RealWitness` exists because refutation over ℝ does not imply refutation over ℤ for universal claims. `KernelBudget` exists because kernel conversion checking is decidable but non-elementary in cost. Both follow the rule the rest of the toolchain already lives by: a resource exhaustion degrades loudly and is never fabricated into a finding or a pass. + +## 3. The cage (L4) + +### From a menu of combinators to an admission test + +Thermite 1's eight combinators were the eight quantified shapes whose decidability its spine could prove. Thermite 2 generalizes the principle behind them: a quantified contract formula is **admitted to the cage** when its quantifier-alternation graph over sorts is acyclic — the criterion from the Ivy line of work, under which the formula lies in an essentially-finite fragment (EPR-reducible) where Z3's model-based quantifier instantiation (MBQI) is a genuine decision procedure. Index arithmetic inside admitted formulas is confined to array-property shapes; the precise admitted arithmetic–quantifier mix is the stage-2 metatheory deliverable (§12). + +Three consequences: + +1. **Membership is decidable.** The classifier builds the graph and checks acyclicity — no judgment calls, no heuristics, and a rejection always names the cycle. +2. **Failures are finite models.** A wrong quantified spec dies with a concrete small structure — an actual array, an actual map. +3. **The trigger layer is gone, not frozen.** Admitted formulas need no trigger annotations and cannot matching-loop; the entire heuristic apparatus the frozen triggers existed to tame is absent for them. The cost moved to model search — EPR is NEXPTIME-complete, so the cliff exists — but it terminates with a verdict either way, and exhaustion is the `Timeout` verdict, never an *unknown*. + +The eight v1 combinators remain valid syntax and become *derived lemmas* over the admitted fragment. Every Thermite 1 program certifies unchanged, as a special case. + +**The graph:** one node per sort; an edge `S → T` whenever a universally bound variable of sort S has an existentially bound (or Skolemized) variable of sort T inside its scope. + +```mermaid +flowchart LR + subgraph admitted ["admitted — acyclic"] + direction LR + A[usize] --> B[u32] --> C[Key] + end + subgraph routed ["forge-routed — cycle named"] + direction LR + K[Key] --> V[Value] --> K + end +``` + +Left: `forall i: usize . exists v: u32 . …` — indices quantify over values, values over keys, nothing returns. Decidable; finite countermodels. Right: `forall k . exists v …` together with `forall v . exists k …` — Key and Value form a loop; the classifier reports the cycle, and the repair is mechanical. + +### The repair verb: restratify + +A cycle is broken by **naming the witness**: replace `exists v . maps(m, k, v)` with a derived `spec fn lookup(m, k)` and state `maps(m, k, lookup(m, k))`. The existential disappears, the edge disappears, the formula is admitted. The rewrite is checked, not trusted: forge automatically emits the in-cage side obligation that the restratified formula implies the original under the new definition — restratification can strengthen a spec, never weaken one. This is a purely syntactic, fully mechanical transformation whose error message contains everything needed to perform it: exactly the kind of repair an agent loop excels at. **Restratify joins fix-the-code and weaken-the-claim as the language's third repair verb.** + +## 4. Numeric routing + +### Real-relaxation: pure routing, zero new syntax + +Nonlinear *integer* validity is undecidable (Matiyasevich); nonlinear *real* validity is decidable (Tarski; Z3's nlsat). And for universally quantified claims with polynomial atoms, validity over the reals implies validity over the integers. So: any universally quantified nonlinear goal over `nat`/`int` containing only polynomial atoms — no integer division, no modulo, no shifts — is routed to nlsat first. The source is untouched; only the certificate shows the engine. + +```mermaid +flowchart LR + G["nonlinear ∀-goal
(polynomial · no ÷ % ≪)"] --> N["nlsat over ℝ
(complete: CAD)"] + N -- "valid" --> P["Proved · L4
trust: solver(nlsat) + ℝ⊇ℤ lemma"] + N -- "real cex p" --> I["integrality check on p
(round / search near p in ℤⁿ)"] + N -- "unknown" --> F["→ forge
(covenant, then burn)"] + I -- "ℤ hit" --> C["Counterexample"] + I -- "none" --> R["RealWitness
→ forge, seeded with p"] +``` + +The asymmetry is deliberate and sound: *proof* over ℝ is conclusive for ℤ; *refutation* over ℝ is not — so a real-only witness escalates instead of failing, and the witness point travels with the goal as proof-search guidance. One-sided completeness, honestly labeled, with the soundness lemma (`r_relax_sound`) stated and proven in the spine. + +### `@bv` — the machine-semantics clause tag + +A clause tagged `ens@bv64` (or `@bv32`, …) is interpreted over fixed-width wraparound semantics, where *everything* is decidable — multiplication, xor-rotate chains, hash mixers, modular identities — with bit-level countermodels (QF_BV; the backend is Verus's `by(bit_vector)` mode, nearly free). + +The tag is loud on purpose: it is a **semantic fork**. Wraparound truth is not unbounded truth, and a clause moved to `@bv` where wrap makes it weaker is the design's one new gaming vector. Three locks, all mandatory: + +1. every tagged clause carries a `bv_shadow` flag in its certificate — greppable at every layer slag is greppable at; +2. the mutation battery runs against bv semantics for tagged clauses; +3. the variant `@bv64(nowrap)` additionally emits a no-overflow side obligation — for when machine width is the domain but wrap is *not* the intent. + +## 5. The forge (L3) + +The forge is where a clause goes when no decision procedure can hold it: inductive structure, multiset equalities, ordinal termination, cyclic-quantifier specs the author chooses not to restratify. The contract is proved by a **proof term** the agent authors, elaborated and checked by the Lean 4 kernel against the same mechanized semantics the soundness spine already defines. The kernel is small (the de Bruijn criterion); the axioms are gated per item to exactly `{propext, Classical.choice, Quot.sound}` — the set the existing spine passes — and a `sorry` is a hole, and holes do not certify. + +### The logic, fixed + +| axis | choice | why (the losing alternative) | +|---|---|---| +| Type theory | Intensional CIC — Lean 4, the spine's own kernel | Extensional TT has undecidable type-checking (Hofmann). A wall, not a preference. | +| Axioms | `{propext, Classical.choice, Quot.sound}`, gated per item | The audit's existing axiom probe applies verbatim. | +| Quotients | Permitted in `prop fn` | Kernel-native; buys `Multiset`, so permutation is an equality rather than a counting trick. | +| Proof irrelevance | Definitional (native `Prop`) | Refinement payloads erase for free; codegen sees only the value. | +| Elaboration | Generated proofs restricted to Miller-pattern implicits | Full higher-order unification is undecidable (Goldfarb); the pattern fragment is the decidable island. Predictable elaboration beats expressive elaboration for an agent loop. | +| Tactics | Frozen battery + **frozen simp set** | An open simp set is the matching-loop hazard reborn. The trigger-freezing philosophy, applied to tactics. | +| Termination | `dec lex(…)` built-in; `dec wf ⟨rel⟩` with an accessibility proof | Sized-types conveniences have a soundness-bug history; accessibility recursion has the same reach, conservatively. | + +### The surface: four constructs + +- **`prop fn`** — the uncaged sibling of `spec fn`: unbounded quantifiers, inductive predicates, quotient types, real implication, over the same value vocabulary. Any clause mentioning one is forge-routed. +- **`lemma`** — a named, proved proposition; the reusable currency of the tier (burned once, cited forever). +- **`proof` blocks** — attached to a function, discharging its forge-routed clauses goal by goal through the frozen battery (`omega`, `simp`, `nlinarith`, `induction`, `decide`, `calc`, `exact`, `from`, `push_neg`); unproven goals are typed proof holes `?p0`, mirroring body holes. +- **Refinement types** — sugar that moves contracts into signatures: `n: u64{n > 0}` desugars to a `req`, a refined return to an `ens`, and a refined `type` alias makes the obligation portable to call sites, where it is discharged in whichever tier the caller's evidence lives (most often the cage, for free). + +### The falsification covenant + +Type theory's structural weakness is that a failed proof search is a stuck goal, not a disproof. The covenant is the design's answer, and it is mandatory: before any proof search, every forge-routed clause owes + +- **`inhabit` witnesses** — concrete inputs satisfying `req`, required *by exhibition* because inhabitation is undecidable to check; and +- a **`falsify` budget** — a deterministic typed generator (seeded, reproducible) attacks the claim on the executable semantics. + +A refutation found here is the verdict `CovenantRefuted` — a concrete counterexample and a hard fail, the cage's rule recovered. Only past a clean falsifier does token burn begin, which means a *false* forge claim almost always dies as a counterexample rather than as an unfalsifiable stuck state. + +### The meaning audit + +Expressive specs widen the gap between what was proved and what was meant. Two quotas keep it auditable: a **definition-tower budget** — a depth/size cap on the `prop fn` definitions a contract may stand on — and `forge audit --meaning`, which prints the fully unfolded tower for human sign-off and pins its hash in the certificate. The cage's legibility, re-imposed as a quota where it can no longer hold by construction. + +## 6. Syntax summary + +| form | tier | meaning | +|---|---|---| +| `forall x: T . P` / `exists x: T . P` | cage if stratified | Raw quantifiers in contract position; admitted when the sort graph is acyclic, forge-routed (cycle named) otherwise | +| `x: T{P(x)}` | either | Refinement type; desugars to `req`/`ens`, classified per the refinement | +| `type name(args) = x: T{P}` | either | Refined alias; the obligation travels to call sites | +| `ens@bvN P` / `@bvN(nowrap)` | cage (bv) | Clause interpreted at machine width; shadow-flagged; `nowrap` adds the no-overflow side obligation | +| `prop fn` | forge | Uncaged specification function: full propositions, quotients | +| `lemma name(args) req … ens … proof { … }` | forge | Named proved proposition; citable in proof blocks | +| `proof for f { ens#k by { … } }` | forge | Discharges f's forge-routed clauses via the frozen battery; `?pN` are proof holes | +| `witness { inhabit (…); falsify N; }` | forge | The covenant: mandatory for any item with forge-routed clauses | +| `dec lex(a, b, …)` / `dec wf rel proof { … }` | either / forge | Lexicographic measures; arbitrary well-founded relations with an accessibility proof | + +**Unchanged from Thermite 1:** `req`/`ens`/`fx` mandatory on every fn; `inv`/`dec` on loops; `spec fn`; `#[slag]` and `#[boundary]`; typed body holes `?N`; the seccomp cage derived from `fx`; the certificate-per-item model. Every Thermite 1 program is a Thermite 2 program with the same or better grade. + +## 7. Six programs + +### A — Thermite 1 compatibility: the cage keeps everything it had + +```rust +fn sum(xs: &[u32]) -> u64 + req xs.len() <= 1_000_000 // → L4 + ens result == spec_sum(xs) // → L4 + fx pure +{ + let mut acc: u64 = 0; + let mut i: usize = 0; + while i < xs.len() + inv acc == spec_sum(&xs[..i]) + dec xs.len() - i + { + acc = acc + xs[i] as u64; + i = i + 1; + } + acc +} +``` + +### B — Raw quantifiers in-cage: binary search without combinators + +Sortedness and not-found are plain ∀-formulas. The classifier admits both (index sorts quantify over element values — acyclic; array-property shape), MBQI decides them, and a wrong program dies with a finite model: a concrete array. + +```rust +fn binary_search(xs: &[u32], needle: u32) -> (r: Option) + req forall i: usize, j: usize . + i <= j && j < xs.len() ==> xs[i] <= xs[j] // raw forall — strat: usize ≻ u32, acyclic → L4 + ens match r { + Some(i) => i < xs.len() && xs[i] == needle, + None => forall i: usize . + i < xs.len() ==> xs[i] != needle, // raw forall — admitted, no trigger → L4 + } + fx pure +{ + // body as in v1 — loop inv/dec unchanged +} +``` + +### C — Nonlinear arithmetic, push-button: the real-relaxation route + +Integer square root. Both postconditions multiply a variable by itself — classically the point where SMT becomes heuristic and old Thermite capped at runtime checks. Here both are universally quantified polynomial claims: nlsat decides them over ℝ, the ℝ→ℤ lemma carries the result, and the item is push-button L4 — no proof block, no covenant. + +```rust +fn isqrt(n: u64) -> (r: u64) + req n <= 1_000_000_000_000 + ens r * r <= n // nonlinear ∀-goal, polynomial: ℝ-relax route → L4 (engine: nlsat) + ens n < (r + 1) * (r + 1) // same route → L4 + fx pure +{ + let mut r: u64 = 0; + while (r + 1) * (r + 1) <= n + inv r * r <= n + dec n - r * r + { r = r + 1; } + r +} +// no proof block, no witness block: nothing here routes to the forge. +// covenant and burn are forge obligations only. +``` + +### D — Hash mixing at machine width: the @bv clause + +The SplitMix64 finalizer. Its avalanche identity and its *injectivity* — a 64-bit bijection claim, hopeless over unbounded integers — are decidable at `@bv64`. The zero-fixpoint clause stays in unbounded semantics: one function, three labeled mechanisms. (Decidable is not cheap: bit-blasting two 64-bit multiplies is the in-fragment cost cliff; the budget verdicts apply.) + +```rust +fn mix64(z: u64) -> (r: u64) + ens@bv64 r == (z ^ (z >> 30)) * 0xBF58_476D_1CE4_E5B9 // wrap intended → L4 @bv64 + ens z == 0 ==> r == 0 // unbounded semantics → L4 + fx pure +{ /* ... */ } + +lemma mix64_injective(a: u64, b: u64) + ens@bv64 mix64(a) == mix64(b) ==> a == b // a 64-bit bijection claim — decidable at @bv64 +// no proof block: QF_BV decides it. expensive (two 64-bit multiplies, bit-blasted) — +// budgeted, never unknown. +``` + +### E — The forge keeps what is genuinely its own: merge + +Sortedness: raw quantifiers, admitted — L4. Length: linear — L4. Permutation: a *quotient multiset equality*, which no decision procedure holds and none should — L3, with a four-line inductive proof citing two library lemmas. This is the shape of every remaining forge obligation: structural, reusable, compounding. + +```rust +prop fn melems(s: Seq) -> Multiset { // quotient type: List modulo permutation + fold s with insert into Multiset.empty +} + +fn merge(a: &[u32], b: &[u32]) -> (out: Vec) + req forall i, j: usize . i <= j && j < a.len() ==> a[i] <= a[j] // strat ✓ → L4 + req forall i, j: usize . i <= j && j < b.len() ==> b[i] <= b[j] // strat ✓ → L4 + req a.len() + b.len() <= 1_000_000 // → L4 + ens forall i, j: usize . i <= j && j < out.len() ==> out[i] <= out[j] // → L4 + ens out.len() == a.len() + b.len() // → L4 + ens melems(out) == melems(a) + melems(b) // multiset equality — the forge → L3 + fx alloc + witness { + inhabit (a = [1, 3], b = [2]); + inhabit (a = [], b = []); + falsify 50_000; // refutation budget, runs before proof search + } +{ /* two-pointer merge; loop inv/dec elided for the sketch */ } + +proof for merge { + ens#3 by { + induction merge_step; + simp [melems_cons, melems_append]; // library lemmas: burned once, cited forever + } +} +``` + +Item level = min over clauses = **L3**. + +### F — Restratification, end to end + +A bidirectional key/value invariant creates a Key ⇄ Value cycle. The fix is the named-witness move — and the result is a *stronger*, more explicit contract. The repair verb improves specs as a side effect. + +**Before (cycle):** + +```rust +struct Store { m: Map } + inv forall k: Key . has_key(m, k) ==> exists v: Value . maps(m, k, v) // Key ≻ Value → L3 + inv forall v: Value . in_range(m, v) ==> exists k: Key . maps(m, k, v) // Value ≻ Key → L3 +// classifier: alternation cycle Key ⇄ Value — forge-routed unless restratified +``` + +**After (restratified):** + +```rust +spec fn lookup(m: Map, k: Key) -> Value // the witness, named +spec fn owner(m: Map, v: Value) -> Key // its dual + +struct Store { m: Map } + inv forall k: Key . has_key(m, k) ==> maps(m, k, lookup(m, k)) // Key ≻ Value only → L4 + inv forall v: Value . in_range(m, v) ==> maps(m, owner(m, v), v) // Value ≻ Key only — no loop closes → L4 +// both edges exist but no existential closes a cycle: graph acyclic — admitted +// forge also emits the side obligation: restratified ==> original (checked in-cage) +``` + +## 8. The agent loop + +The loop's quality lives in its failure messages: every routing decision and every verdict comes from a frozen vocabulary, so the agent's next move is a lookup, not a guess. Four sessions, four repair verbs: + +```text +$ forge check kv.th + classify : inv#1 forge-routed — alternation cycle: Key ⇄ Value + edges: forall k:Key ≻ exists v:Value (inv#1) · forall v:Value ≻ exists k:Key (inv#2) + repair: name the witness — replace the existential with a derived spec fn (restratify) + +$ forge edit kv.th --restratify inv#1 --witness lookup + rewrote : exists v . maps(m,k,v) → maps(m, k, lookup(m, k)) + spec fn lookup added + emitted : side obligation: restratified ==> original [cage] · Proved + +$ forge check kv.th + classify : inv#1 cage (strat: Key ≻ Value, acyclic) · inv#2 cage + solve : MBQI · Proved · Proved trust: solver(z3-epr) + item kv certified L4 — no triggers, no covenant, no burn + +$ forge check mix64.th + classify : ens#1 cage@bv64 · ens#2 cage@bv64 · ens#3 cage + solve : ens#1 Proved (0.8s) · ens#2 Counterexample + model: z = 0x8000_0000_0000_0001 — the truncated rotate is not injective; bit pattern attached + …agent fixes the rotate width, re-checks: Proved (41s — the bv cost cliff, within budget) + +$ forge check merge.th + classify : ens#1 cage · ens#2 cage · ens#3 forge (prop fn melems: quotient type) + covenant : inhabit ✓ (2 witnesses) · falsify 50,000 generated · 0 refuted + goals : ?p0 : melems(out) == melems(a) + melems(b) + +$ forge fill merge ?p0 "induction merge_step; simp" + kernel: stuck — residual: melems(push(out, x)) == insert(x, melems(out)) + hint: the frozen simp set lacks a push/insert bridge — state it as a lemma + +$ forge fill merge ?p0 "induction merge_step; simp [melems_cons, melems_append]" + kernel: goal closed · axioms ⊆ {propext, Classical.choice, Quot.sound} · proof 287 tokens + item merge certified L3 (clauses: L4, L4, L3) +``` + +The four verbs in order: **restratify** (kv — re-routed to push-button, with the strengthening side obligation auto-checked), **fix the code** (mix64 — a bit-level model said exactly what), **burn** (merge — including one honest `Stuck` with a battery hint, the forge's characteristic failure mode), and the always-available fourth verb, **weaken the claim**. Note the merge covenant ran before any proof search: a false permutation claim would have died there as a concrete refutation. + +## 9. Certificates + +The certificate model is Thermite 1's (a JSON manifest per item, oracle-stable, cache-keyed), extended per clause: the `engine` block names the mechanism, and a new `trust:` field names exactly what discharging this clause asked you to believe. The ladder stays one-dimensional in the product; the trust dimension lives here and is aggregated by the audit into the residual-trust statement. Forge-tier certificates additionally carry the covenant evidence, the burn receipt (the spent tokens, recorded — the thesis, kept honest), and the meaning-audit pin. + +**isqrt — relaxed L4:** + +```json +{ + "item": "isqrt", "clause": "ens#1", + "level": "L4", + "engine": { "kind": "nlsat", "route": "real-relaxation", + "soundness": "forall-polynomial: valid(R) implies valid(Z) [spine lemma r_relax_sound]" }, + "trust": "solver(nlsat) + spine-lemma(kernel)", + "tv": { "verdict": "Faithful", "reference": "ref_encode (stage-2 stratified ext)" }, + "falsification_channel": "integer countermodel (integrality-checked); RealWitness escalates" +} +``` + +**mix64 — @bv64 L4:** + +```json +{ + "item": "mix64", "clause": "ens#1", + "level": "L4", + "engine": { "kind": "verus-z3", "mode": "bit_vector", "width": 64 }, + "trust": "solver(z3-qfbv)", + "bv_shadow": { "flagged": true, "semantics": "wraparound", + "nowrap_obligation": null, + "note": "clause meaning differs from unbounded semantics — greppable, like slag" }, + "mutation": { "semantics": "bv64", "killed": 9, "scored": 10 }, + "falsification_channel": "bit-level model (mechanically complete)" +} +``` + +**merge — forge L3:** + +```json +{ + "item": "merge", "clause": "ens#3", + "level": "L3", + "engine": { "kind": "lean-kernel", "version": "4.29.0", + "axioms": ["propext", "Classical.choice", "Quot.sound"], + "quotients": ["Multiset"] }, + "trust": "kernel + exporter(inspection, drift-pinned)", + "covenant": { "inhabit": 2, "falsify": { "generated": 50000, "refuted": 0, "seed": 4096 } }, + "mutation": { "mode": "re-elaboration", "killed": 15, "scored": 16 }, + "meaning_audit": { "tower_depth": 2, "tower_budget": 4, "unfolded_hash": "c41a…", "human_ack": true }, + "burn": { "proof_tokens": 287, "lemmas_cited": ["melems_cons", "melems_append"] } +} +``` + +## 10. Anti-Goodhart + +A passing grade must be hard to fake, per tier. The cage battery is Thermite 1's, unchanged; the forge battery is its counterpart against a larger gaming surface; the bv locks close the one vector this design adds. + +| defense | cage (L4) | forge (L3) | +|---|---|---| +| Vacuous precondition | The solver proves `false` under `req` → reject | Undecidable to check — so **required by exhibition**: `inhabit` witnesses are mandatory; no witness, no certificate | +| Tautology (ens ignores the body) | Empty-body harness proves `ens` from types alone → reject | **Arbitrary-result re-elaboration**: substitute an opaque result into the proof term; if it still elaborates, the `ens` said nothing → reject | +| Weak contract | Mutation battery; kill-ratio floor; prover-proved equivalent-mutant exclusion | **Re-elaboration mutation** — strictly sharper: each mutant body is substituted under the existing proof term, and "the proof breaks" is decidable per mutant, kernel-guaranteed. (Deciding a survivor is *equivalent* stays undecidable — Budd–Angluin — so survivors keep counting against the floor.) | +| Wrong theorem proved | Cage poverty keeps contracts legible by construction | Definition-tower budget + the meaning audit (§5), hash-pinned in the certificate | +| Proof-cheat escapes | No `assume`, no external-body outside slag | Per-item axiom gate; `sorry` is a hole; holes never certify | + +Two cross-tier vectors, with their locks: + +- **@bv weakening** — tagging a clause `@bv64` so wraparound makes it vacuously easier. Locks: the `bv_shadow` flag (greppable like slag), bv-semantics mutation for tagged clauses, and the `nowrap` side obligation when wrap is not intended. +- **Restratify laundering** — could naming a witness weaken the spec? Impossible by construction: the rewrite emits the implication side obligation (restratified ⟹ original), checked in-cage; the move can strengthen a spec, never weaken one. + +**The one place the forge beats the cage:** re-elaboration mutation is cheaper, deterministic, and more meaningful than per-mutant solver runs — a proof term that survives a body mutation has measured the contract's blind spot exactly. The anti-gaming layer is the unexpected beneficiary of the kernel tier. + +## 11. The trust base + +| you are trusting… | L4 clauses | L3 clauses | +|---|---|---| +| Lean kernel + {propext, Classical.choice, Quot.sound} | yes (via the soundness spine and TV) | yes (directly — the proofs live here) | +| Z3 / Verus solver soundness | yes (per query; ~500 kLOC of solver; proof reconstruction migrates this to the kernel where the fragment allows — §12 stage 3) | **no** | +| S = the intended meaning of the spec | yes | yes, **and harder** — hence the meaning audit; irreducible on every tier | +| Rust↔Lean correspondence (inspection tier) | yes (the reference encoders; SHA-pinned + drift-tripwired) | mostly no — obligations export straight into the proven semantics; the exporter itself stays inspected | +| Erasure / extraction to the running binary | n/a — Verus verifies the Rust that compiles | **yes — new**: refinements and proof terms vanish at codegen; the proven term and the compiled body are tied by the lowering once, not per query | +| rustc / LLVM | yes | yes | + +**The floor (Gödel II), permanent on both tiers:** no tier proves its own checker sound. The residual list shrinks and changes shape; it never empties — which is why the residual statement remains the last thing the audit prints. + +The trade in one line: L4 trusts a large heuristic solver on every query; L3 trusts a small kernel on every query plus one erasure link amortized across all of them. A good trade, probably — and "probably" is why L3 ranks below the rung whose refutations are mechanically complete. + +## 12. Staging and the decision record + +This configuration (**C3′**) was selected from four candidate packages: + +| package | verdict | reason | +|---|---|---| +| C1 — conservative core (forge under the v1 menu) | rejected | The cage is too small, so burn dominates and the covenant becomes the primary refutation channel for most of the language. A proof assistant wearing an SMT hat. | +| C2 — stratified cage | adopted as base | Best failure actionability (the restratify repair verb); loses only on numeric coverage. | +| **C3′ — wide-spectrum, staged** | **chosen** | C2 + ℝ-relaxation (pure routing, near-zero metatheory, large coverage win) + @bv as an explicitly tagged, shadow-flagged, last-staged opt-in — the one risky piece, isolated. | +| C4 — grid ladder (refutation × trust as product surface) | demoted to metadata | The 2-D decomposition is true and lives in the `trust:` field and `make audit`; the ladder keeps the product's legibility. | + +Rollout is ordered by risk isolation, not demo value; each stage states what is proven while it ships, and the system never claims the next stage's trust story early. + +**Stage 1 — the forge tier + real-relaxation routing.** The kernel tier (export bridge grown from the existing obligation exporter; covenant; battery; the verdicts `Stuck`/`KernelBudget`/`CovenantRefuted`) plus nlsat routing with `RealWitness`. No spine change; the cage is still the v1 combinators. +> *Honest residual during stage 1:* the ℝ→ℤ soundness lemma is stated and proven in the spine (one page). Forge obligations trust the kernel plus the exporter (inspection tier, drift-pinned). The headline lands here: out-of-cage no longer degrades. + +**Stage 2 — the stratified cage + the spine extension.** The admission classifier (sort-graph construction, cycle reporting, the restratify rewrite + its implication side obligation) ships against a stratified-FOL extension of the Lean spine: denotation for the admitted fragment, reference encoder, soundness theorem, TV obligation shapes. The combinators become derived lemmas. +> *Honest residual during stage 2:* until the spine extension is green, stratified formulas run under per-run TV against an unproven reference — existential evidence, labeled as such in the certificate's `trust:` field. The system admits them but does not claim the universal theorem over them. This is the months-not-weekend stage and the subject of the follow-up metatheory document. + +**Stage 3 — @bv clause mode + reconstruction by default.** `@bv` with all three locks, riding the bit-vector solver mode; SMT proof reconstruction (the cvc5/kernel-replay path) flipped to default-on where the fragment supports it, migrating cage clauses' trust base from solver to kernel without touching their rung. +> *Honest residual during stage 3:* the bv semantic fork exists from day one of this stage — the locks ship with the feature, not after. A build without the shadow-flag plumbing does not get the tag. + +## 13. Limits, by theorem + +Every item below is a theorem, not an engineering gap. The design's posture toward each is the same as Thermite's everywhere: degrade loudly, never launder. + +- **Cost cliffs inside decidable land** (Fischer–Rabin; CAD lower bounds; EPR is NEXPTIME-complete; 64-bit bv multiplication is brutal for SAT). Every cage enlargement trades *unknown* for *expensive* — the right trade, since expensive gets a budget verdict and a profile — but L4's growth is bounded by feasibility, not logic. **The practical admission test is decidable-and-affordable.** +- **The real-relaxation gap has a name** (Matiyasevich). Integer-essential claims — divisibility, exact division and modulo, claims true over ℤ but false over ℝ — stay forge-bound. `RealWitness` is the honest marker of exactly this gap. +- **@bv is two truths, permanently.** Wraparound and unbounded semantics will never agree, and no lock changes that — the locks keep the fork *visible*. A certificate on a bv-heavy module must keep saying "this is modular arithmetic" forever. +- **The covenant is empirical, not complete.** A falsifier-clean false claim still dies as wasted tokens, not as a model. This is the structural reason the forge ranks below the cage, and no amount of generator engineering closes it — only narrows it. +- **The forge's walls stand** (Goldfarb; Pollack-consistency; Budd–Angluin). Elaboration outside the pattern fragment, the proved-vs-meant gap, and surviving equivalent mutants — each undecidable, each managed by quota or exhibition rather than solved. The forge shrank in docket, not in difficulty per item. +- **The floor and the residue are permanent** (Gödel II; Rice). No tier proves its own checker; some true obligations stay out of reach at every rung forever. The roadmap question is never "when does everything reach the top" but **"which decidable islands next, at what cost, with the honest-degradation machinery scaling alongside."** + +--- + +*Next document: the stage-2 metatheory sketch — the stratified-FOL spine (denotation for the admitted fragment, the reference encoder, the soundness theorem, the TV obligation shapes, and the proof that the admission classifier and the proven fragment coincide).* + +*RFC-1 · Thermite 2 · design sketch — not shipped software · supersedes RFC-1-draft1 and RFC-1-draft2 · baseline `dollspace-gay/Thermite @ 93d3cbc0`.* From a25231f54e38c2c83fb8b76ceae66065774aafb8 Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 00:38:16 -0700 Subject: [PATCH 3/7] Migrate the unnumbered RFC from #17, as RFC-2 Body copied verbatim; front matter added above it. Comments stay in the issue, which `discussion:` links, because the file is the document and the issue is the discussion. --- .design/rfcs/0002-canonical-req-registry.md | 96 +++++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 .design/rfcs/0002-canonical-req-registry.md diff --git a/.design/rfcs/0002-canonical-req-registry.md b/.design/rfcs/0002-canonical-req-registry.md new file mode 100644 index 00000000..d45f911a --- /dev/null +++ b/.design/rfcs/0002-canonical-req-registry.md @@ -0,0 +1,96 @@ +--- +rfc: 2 +title: Canonical REQ registry and generated status tables +status: accepted +supersedes: [] +introduces: [] +discussion: https://github.com/dollspace-gay/Thermite/issues/17 +--- + +## Context + +The current doc-drift gate catches routed design documents that are stale relative to audited file SHA pins. That is useful, but it does not catch semantic drift inside long source comments. The recent `REQ-5 (forge plug-in point)` mismatch is the concrete example: one module documented the forge TV plug-in point as `NOT-STARTED` while the forge side documented and implemented it as `SHIPPED`. + +The new `tooling/req-status.py` lint is a pragmatic tripwire for this class of mistake. It scans `//! | REQ ... | SHIPPED/NOT-STARTED | ... |` source-comment rows and fails when exact labels disagree, `NOT-STARTED` rows do not cite future/deferred scope, or `SHIPPED` rows lack at least one resolving backtick file/symbol citation. + +That guard is intentionally mechanical. It reduces obvious contradictions, but it should not become the long-term source of truth. + +## Problem + +REQ status is currently repeated in multiple long source comments. That creates several failure modes: + +- The same requirement can be renamed slightly and evade exact-label matching. +- A real symbol/file citation can exist without actually proving the status claim. +- Future/blocker wording is keyword-based and does not prove that an issue exists or is the correct blocker. +- Source comments mix stable implementation invariants with volatile project status and history. +- Ownership is implicit, so there is no machine-readable answer to which module owns a requirement. + +## Proposal + +Introduce a canonical machine-readable REQ registry and generate status tables from it instead of hand-maintaining them in source comments. + +The registry should assign each requirement a stable ID and explicit ownership, for example: + +- `id`: stable requirement ID, e.g. `REQ-5` +- `title`: human-readable name +- `owner`: owning crate/module/doc +- `status`: accepted enum such as `shipped`, `not_started`, `partial`, `blocked`, `deferred` +- `scope`: contract/exec/forge/spec/docs/etc. +- `evidence`: typed entries, not prose-only citations +- `blockers`: issue/PR IDs required for non-shipped work +- `generated_to`: source/doc locations where rendered tables should appear +- `last_reviewed`: optional review marker for high-risk requirements + +Evidence should be typed so the gate can validate more than string existence: + +- `symbol`: resolves to a real Rust path or item where practical +- `file`: resolves to a repo path +- `test`: resolves to a test file/name and preferably a CI job target +- `issue`: resolves to an open/closed GitHub issue depending on status +- `doc`: resolves to a design doc section or routed doc pin +- `command`: names the verification command expected to cover the requirement + +## Generated Output + +Generate markdown tables for source comments and design docs from the registry. Source comments should keep durable invariants and non-obvious mechanisms. Volatile status, shipped evidence, blockers, and history should be generated into a small number of status views or inserted into marked generated regions. + +Possible generated views: + +- full REQ inventory +- per-crate REQ status +- not-started/blocked work queue +- shipped evidence index +- requirements with weak or missing verification commands + +## Enforcement Plan + +1. Keep `tooling/req-status.py` as the short-term contradiction lint. +2. Add a registry file, likely under `.design/reqs/` or `tooling/reqs/`. +3. Add a generator that renders tables from the registry. +4. Add a check that generated tables are up to date. +5. Replace hand-written source-comment status rows with generated rows or links to generated status docs. +6. Tighten validation once evidence is typed: + - `shipped` requires test/symbol/file evidence. + - `not_started` requires blocker or deferred scope. + - `blocked` requires an open issue. + - `partial` requires explicit remaining scope. + - generated table diffs fail CI. + +## Known Edge Cases To Design For + +- Requirement aliases and renamed titles should still map to stable IDs. +- Requirements spanning multiple crates need one owner plus contributors, not multiple conflicting owners. +- Generated regions should be easy to review and should avoid excessive churn. +- Evidence may be valid only under features or external tools such as Verus; the schema should capture that. +- Test files can exist while tests are skipped, ignored, or not run in CI; evidence should eventually link to commands/jobs. +- Some requirements are intentionally aspirational or roadmap-level; those need an explicit status instead of being forced into `NOT-STARTED` prose. + +## Acceptance Criteria + +- A canonical registry exists with stable IDs, owners, statuses, and typed evidence. +- Generated status views replace duplicated hand-written REQ status tables. +- CI fails when generated output is stale. +- CI fails when registry entries have invalid statuses, unresolved evidence, or missing blockers. +- Existing source comments retain durable design invariants while volatile status moves to generated output. + +This should make doc drift a data consistency problem instead of a prose archaeology problem. From 7987246a4c442169669bf07d73475a311ed24356 Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 00:38:16 -0700 Subject: [PATCH 4/7] Migrate RFC-2 from #119, as RFC-3 Body copied verbatim; front matter added above it. Comments stay in the issue, which `discussion:` links, because the file is the document and the issue is the discussion. --- .design/rfcs/0003-certification-surface.md | 353 +++++++++++++++++++++ 1 file changed, 353 insertions(+) create mode 100644 .design/rfcs/0003-certification-surface.md diff --git a/.design/rfcs/0003-certification-surface.md b/.design/rfcs/0003-certification-surface.md new file mode 100644 index 00000000..e29e92ec --- /dev/null +++ b/.design/rfcs/0003-certification-surface.md @@ -0,0 +1,353 @@ +--- +rfc: 3 +title: The certification surface — from a ladder to a coordinate system +status: draft +supersedes: [] +introduces: [] +discussion: https://github.com/dollspace-gay/Thermite/issues/119 +--- + +# RFC-2: The certification surface — from a ladder to a coordinate system + +| | | +|---|---| +| **Status** | Draft for discussion — not routed, not content-pinned | +| **Supersedes** | RFC-1 §2 (the ladder), §9 (certificates), §11 (the trust base) — *presentation only* | +| **Preserves** | RFC-1 §3–§5, §10, §13 unchanged. No mechanism, engine, or admission rule changes. | +| **Baseline** | `dollspace-gay/Thermite @ 84d276e7` (gates G1–G4 shipped) | +| **Companion** | The assurance-order metatheory (§4) — a separate document, per the RFC-1 pattern | + +**Contents:** [§0 Problem](#0-the-problem) · [§1 Coordinates](#1-the-four-coordinates) · [§2 Rendering](#2-the-rendering) · [§3 The lattice](#3-the-lattice) · [§4 Aggregation is deferred](#4-aggregation-is-deferred) · [§5 Dual labels](#5-dual-labels-and-the-collapse-policy) · [§6 Removing Lx](#6-removing-lx) · [§7 Increments](#7-increments) · [§8 Unchanged](#8-what-rfc-2-does-not-change) · [§9 Open questions](#9-open-questions) + +--- + +## 0. The problem + +RFC-1 graded every obligation on a five-rung scalar ladder and stated the rungs mean **refutation quality** ("rank means refutation quality", §2). That was true when written, and it stopped being true the moment two mechanisms shared a rung. + +Today `Level::L3` denotes both: + +- a general Verus/Z3 result — proven for all inputs, refutation *incomplete* (Z3 may return `unknown`), trust base ~500 kLOC of solver; and +- a Lean forge result — proven for all inputs, refutation *absent* (a failed proof is a stuck goal; the covenant is empirical), trust base a small kernel plus a per-item axiom gate. + +These differ on both axes RFC-1 cares about, and they differ in *opposite directions*. Verus refutes better; Lean is trusted less. A scalar cannot carry that, so the scalar silently stopped meaning what §2 said it meant. + +This is not a defect introduced by any one change — it is what a lossy projection does under load, and the collision predates any recent work. RFC-1 even anticipated it: §12 lists configuration **C4 ("grid ladder — refutation × trust as a product surface")** and *demotes it to metadata* on legibility grounds: + +> The 2-D decomposition is true and lives in the `trust:` field and `make audit`; +> the ladder keeps the product's legibility. + +RFC-2 revisits that call with the metatheory that did not exist then: the S₂.0 classifier, checked reconstruction at QF_LIA/QF_BV/EPR, the covenant, per-run translation validation, and boundary-closure classification. The decomposition is no longer theoretical — **every coordinate is already computed and stored. Only one of them is rendered.** + +**RFC-2's claim: the decomposition won. Render it.** + +## 1. The four coordinates + +Each already exists in the implementation. None is new work to *compute*. + +### 1.1 Scope — what the claim quantifies over + +| value | meaning | source | +|---|---|---| +| `all` | holds for every input | Verus/Z3, Lean, cage routes | +| `bounded(n)` | holds for every input up to size *n* | Kani/CBMC | +| `per-exec` | checked at the call site, this execution | runtime contracts | +| `none` | nothing is claimed about the body | `#[slag]` | + +### 1.2 Refutation — what a *false* clause yields + +This is RFC-1 §9's `falsification_channel`. **It was specified and never shipped** — `manifest.rs` carries `trust` but no falsification field. + +| value | meaning | witness | +|---|---|---| +| `complete` | mechanically complete in-fragment | real point · bit pattern · finite structure | +| `incomplete` | a countermodel *when the solver finds one*; `unknown` possible | Verus counterexample | +| `empirical` | no mechanical refutation; a seeded generator attacks the claim | covenant `CovenantRefuted` | +| `trace(n)` | a concrete trace within the bound | Kani trace | +| `abort` | detected in production, at the violating call | L1 abort | +| `none` | — | `#[slag]` | + +**Refutation is a property of the fragment, not of the proof.** It classifies the *question*, not the *answer*. A successful `complete` certificate and a successful `empirical` certificate establish the same proposition; they differ in what the system can tell you when the claim is false, or when the code changes. Lx obscured this by looking like a quality score on the artifact. + +What decidability buys is precisely the model-finding direction: + +> **¬φ satisfiable ⟺ the procedure exhibits a model of ¬φ.** + +That biconditional is why `complete` means something: a `valid` answer carries the information *no countermodel exists, because the procedure would have found one*. Outside a decidable fragment there is no such guarantee, and three situations collapse into one observable stuck goal — φ is false, φ is true but unproven, φ is true but unprovable here. + +### 1.3 Trust — what discharging this clause asks you to believe + +Already shipped as `Certificate::trust` (`forge/src/manifest.rs:266`). Trust is a **set**, not a scalar. + +| value | meaning | +|---|---| +| `lean-checked` | Lean re-checked the actual `req → clause` theorem; the solver is a proof *producer* and **leaves** the trusted base | +| `lean-lemma` | Lean proved a *bridge lemma* licensing the route (e.g. `r_relax_sound`); the solver **remains** trusted | +| `solver` | Z3/Verus soundness, per query | +| `fiat` | trusted by declaration | + +`inspection` is a **modifier, not a value** (resolving OQ-3): the Rust↔Lean renderers stay inspection-tier *even after* reconstruction — `bv_kernel_checked_trust_profile` carries a residual "renderer correspondence remains inspection-tier" item alongside its `lean-checked` claim. + +**Trust splits into residual and discharged.** A naive union is wrong: it makes the relax route `{solver, lean-lemma}` a superset of plain cage `{solver}`, and therefore "worse," when the bridge lemma is not a liability but a *discharged obligation*. Ordering by **residual risk under set inclusion** gives the right answer for free: + +| position | residual | +|---|---| +| `lean-checked` | `{inspection, rustc}` | +| `solver`, `solver + lean-lemma` | `{solver, inspection, rustc}` | + +`{inspection, rustc} ⊂ {solver, inspection, rustc}`, so **trust is a two-element chain and `lean-checked` strictly dominates** — with no metatheory required. And the relax route comes out *equal* to the unreconstructed cage rather than worse, which matches RFC-1 §12's own characterization of ℝ-relaxation as a **coverage** win rather than an assurance-rank win. + +Note the deliberate absence of the word *kernel*: it is claimed by the Lean kernel, the seccomp filter, the OS-kernel target, and the "kernel-grounded" descriptor. See the nomenclature issue. + +**The distinction this axis exists to preserve.** Reconstruction is `{lean-checked}` — Z3 is gone entirely (`engine.rs:130`: "the SAT solver and LRAT converter are proof producers only: neither remains in the trusted base"). The relax route keeps Z3. Today the audit **cannot tell them apart**: `KERNEL_CHECKED_TRUST_MARKER` is the substring `"kernel-checked"`, and `r_relax_sound`'s description ends in that substring, so the marker fires for both. That is the same scalar-collapse pathology as the L3 blur, one layer down. (Filed separately per §7.) + +### 1.4 Boundary — how far the claim closes + +Already shipped (`f78dd664`, 2026-06-05, "end-to-end vs to-the-boundary classification"), typed as `AssuranceScope`. + +| value | meaning | +|---|---| +| `e2e` | the claim closes over the item's whole call graph | +| `to_boundary` | closes to declared `#[boundary]` contracts, which are assumed | +| `to_platform(p)` | closes to a named frozen platform registry `p` | + +Boundary is **orthogonal to the ladder and always has been**: a clause can be fully proven *and* to-the-boundary — its own contract verified, the whole-program guarantee still resting on a foreign body. Level and boundary answer different questions: *how well is this proven* versus *how far does the proof reach*. + +## 2. The rendering + +``` +scope/refutation/trust@boundary +``` + +| rendered | what it is | +|---|---| +| `all/complete/lean-checked@e2e` | caged and reconstructed — the strongest position available | +| `all/complete/{solver,lean-lemma}@e2e` | the nlsat relax route | +| `all/complete/solver@e2e` | caged, reconstruction not yet available for the fragment | +| `all/incomplete/solver@e2e` | general Verus/Z3 | +| `all/empirical/lean-checked@e2e` | the Lean forge | +| `all/incomplete/solver@to_platform(x86_64-pc-uefi-smp-v1)` | a kernel core, stated honestly | +| `bounded(8)/trace(8)/solver@e2e` | Kani | +| `per-exec/abort/fiat@e2e` | runtime contracts | +| `none/none/fiat@e2e` | `#[slag]` | + +The two rows that render identically as `L3` today — general Verus/Z3 and the Lean forge — are now visibly different objects. + +## 3. The lattice + +### 3.1 Coherent cells + +The coordinate product is mostly empty, and the emptiness is structural. **Refutation is functionally determined by scope everywhere except `all`:** + +| scope | admissible refutation | why | +|---|---|---| +| `none` | `none` | nothing is claimed, so nothing to refute | +| `per-exec` | `abort` | a runtime check can only fail at the violating call | +| `bounded(n)` | `trace(n)` | which *is* "complete, relative to the bound" | +| `all` | `complete` · `incomplete` · `empirical` | the only free choice | + +Further constraints: `fiat` ⟹ `scope ∈ {none, per-exec}` (claiming all inputs by declaration just *is* `#[slag]`); `incomplete` ⟹ `solver ∈ residual` (if Lean re-checked it, the route was decidable, hence `complete`); `empirical` ⟹ `lean-checked` (empirical refutation is the covenant, a forge construct). + +**Incoherent a priori** — a certificate landing in one of these is a schema violation and a real bug detector: + +``` +all/*/fiat none/{≠none}/* bounded(n)/complete/* +per-exec/{complete,incomplete,empirical}/* +all/incomplete/lean-checked all/empirical/solver +``` + +**Eight coherent cells**, five of them in `all`: + +``` +none/none/fiat (slag) +per-exec/abort/fiat (runtime) +bounded(n)/trace(n)/solver (Kani) +all/complete/lean-checked (reconstructed cage) +all/complete/{solver, lean-lemma} (relax route) +all/complete/solver (cage, unreconstructed) +all/incomplete/solver (general Verus) +all/empirical/lean-checked (the forge) +``` + +### 3.2 Seven order-elements + +The relax route and the unreconstructed cage have identical residual, refutation, and scope — they are **order-equivalent**, different routes to one position. So eight cells collapse to **seven distinct elements**. + +``` + A all / complete / lean-checked + / \ + / \ + B \ all / complete / solver [≡ relax route] + | \ + C D all / incomplete / solver + \ / all / empirical / lean-checked + \ / + K bounded(n) / trace(n) / solver + | + R per-exec / abort / fiat + | + S none / none / fiat +``` + +**This is a bounded lattice.** Top `A`, bottom `S`, and both non-trivial pairs have meets and joins: + +| pair | join | meet | +|---|---|---| +| `B ∨ D` | `A` | `K` | +| `C ∨ D` | `A` | `K` | + +The meets are worth reading: **the greatest common assurance of the forge and any solver route is Kani.** That is the honest answer to "what can I claim about a module mixing forge and cage clauses without appealing to either's distinctive strength." + +### 3.3 The obstruction is exactly N₅ + +The sublattice `{K, C, B, D, A}` is the **pentagon**: + +``` + A + / \ + B \ K < C < B < A (chain of length 3) + | D K < D < A (chain of length 2) + C / D ∥ C, D ∥ B + \ / + K +``` + +N₅ is the forbidden sublattice for modularity, so **the assurance order is non-modular, hence non-distributive.** That is the formal statement of a fact the implementation kept rediscovering: the axes genuinely interact, and no amount of per-axis reasoning recovers the whole structure. + +Two consequences the documents should carry: + +**Any total order must invent a comparison.** A linear extension always exists, so RFC-1's scalar ladder was not wrong to be totally ordered — it was wrong to be *silent* about which relation it added. The fiat is `B ∥ D` and `C ∥ D` being forcibly ordered. The L3 blur is `C ∥ D` being forcibly *identified*, which is strictly worse: an invented equality rather than an invented inequality. + +**The pentagon names the companion's subject.** `{Kani, general-Verus, cage-solver, forge, reconstructed-cage}`. The companion document's job is to characterize that one obstruction — prove the cell inventory complete, prove N₅ is the only non-modular sublattice, and decide whether the `forge ∥ solver` edge stays incomparable or earns a principled orientation. + +### 3.4 Comparison and floors + +- Certificates compare by **product order**. Incomparable pairs are reported incomparable, never silently ordered. +- Acceptance gates compare against a **declared set of floor tuples**, accepted on dominance over any member. For a single floor this is identical to per-axis minimums, so the set form costs nothing until needed — and it is already needed: the strict artifact path requires `@e2e` while a platform-image path requires `@to_platform(p)`. Two acceptable positions, not one floor. +- The floor set is **declared in-repo**, versioned under RFC-3's contract, not computed per command. Scattered acceptance constants are how a build path comes to invent its own criterion privately. +- `make audit` reports the **Pareto frontier** plus the weakest link per axis, and the residual-trust statement stays the last thing it prints. + +## 4. Aggregation is deferred + +Composing clause tuples into item tuples, and item tuples into artifact tuples, is **not** per-axis minimum, and RFC-2 deliberately does not specify it. Three known failures of the naive rule: + +1. **Refutation is fibered over scope.** `complete` means complete *relative to the scope claimed*. `bounded(8)/trace(8)` and `all/complete` both say "complete" and mean different strengths; comparing across fibers without normalizing is a category error. +2. **Boundary acts on refutation.** A clause completely refutable `@to_boundary` is completely refutable *modulo the assumption* — a counterexample to the whole-program property can live inside the foreign body, where no channel observes it. Boundary acts *on* the other axes rather than beside them. +3. **Trust is not flat** (§1.3): residual composes, discharged does not. + +This follows RFC-1's own precedent. §3 shipped the admission test while deferring its characterization: + +> the precise admitted arithmetic–quantifier mix is the stage-2 metatheory +> deliverable (§12) + +Same move: ship the surface, name the deferred characterization, make it a numbered deliverable rather than an unstated gap. **Until the companion lands, `forge` reports per-clause tuples and the weakest link on each axis separately, and computes no single composite claim.** The existing aggregation sites keep computing exactly what they compute today. + +The companion must also prove its operator *agrees with what `forge check` computes* — the same discipline as `classifier_correct`. Metatheory that merely coexists with the implementation is how drift starts. + +## 5. Dual labels and the collapse policy + +Every claim is validity **relative to a frame**, and the fragment plus decision procedure are what fix the frame. Different audiences need different amounts of that frame. + +So a certificate carries **two labels, both stored, neither derived at read time**: + +- **engineer label** — what changes a decision: *"proven for all inputs; a false clause gives you a concrete failing input."* +- **formal label** — the tuple plus frame: fragment, procedure, axioms, residual. + +Presentation is progressive disclosure: the engineer label on the front page, the frame behind `--explain`, the lattice position in the audit. + +**The rule that makes this safe:** + +> Collapsing two formal positions into one engineer label is permitted, and is +> governed by an explicit, versioned **collapse policy**. Collapsing them +> *silently* is a schema violation. + +This is the piece that prevents the L3 blur recurring. The blur was never wrong because two mechanisms shared a label — it was wrong because **nothing declared the collapse, on what grounds, for which audience.** A declared collapse is a reviewable design decision. An undeclared one is drift that looks like a decision. + +## 6. Removing Lx + +**Lx is removed, not retained** — deleted from the certificate schema, audit output, skill, and README during the `2.0.0-beta` line. The tuple becomes the sole certification surface. + +A lossy projection kept "for skimming" is a projection someone will eventually gate on, guaranteeing a second source of truth and slow drift back to the collision this RFC exists to fix. + +The migration table is a **translation aid for readers of historical certificates**, not a live projection: + +| historical Lx | tuple | +|---|---| +| L4 | `all/complete/*` | +| L3 | `all/incomplete/*` **or** `all/empirical/*` — *ambiguous; the collision class* | +| L2 | `bounded(n)/*` | +| L1 | `per-exec/*` | +| L0 | `none/*` | + +The L3 row is the point: historical L3 certificates **cannot be mechanically migrated**, because the number never carried enough information to tell the two cases apart. That is the clearest argument for the change, and why removal is cheaper now than later. + +**Migration cost, measured.** The checked-in oracle corpus is **12 `.cert.json` files** (10 at L3, 2 at L0), hand-authored and compared as *subsets*. Subset comparison means R2-1…R2-5 do not break them at all — only removing Lx does, and that is 12 files to re-cut by hand. There are no external consumers to migrate: version `0.0.1`, two tags, no releases. + +Per RFC-3, removing Lx breaks *both* the certificate schema and the assurance semantics — permitted within the beta line, and the reason `2.0.0-beta` is where it lands. + +## 7. Increments + +| # | increment | surface | risk | +|---|---|---|---| +| R2-1 | Ship `falsification_channel` per RFC-1 §9 | `manifest.rs`, cert schema v3 | low — additive | +| R2-2 | `trust` as a set; split `lean-checked`/`lean-lemma`; order by residual inclusion | `manifest.rs`, `engine.rs` | low — already the semantics | +| R2-3 | Surface `boundary` in the per-clause record | `manifest.rs` | low — exists at item level | +| R2-4 | Coherence validation: reject certificates in incoherent cells (§3.1) | `manifest.rs` | low — additive, and a bug detector | +| R2-5 | Render the tuple; dual labels + declared collapse policy (§5) | `manifest.rs`, `audit.rs` | medium | +| R2-6 | Product-order comparison, declared floor set, Pareto frontier | `audit.rs`, new policy file | medium | +| R2-7 | Retire the level-as-verdict idiom | 10 call sites | low — arguably a bug fix | +| R2-8 | **Classification certificate** — emit the fragment verdict pre-discharge | `manifest.rs`, `check.rs` | medium | +| R2-9 | **Remove `Lx`** from schema, audit, skill, README | everywhere | **high** — breaking; requires R2-1…R2-8 | + +No engine, admission-rule, or solver path is touched by any increment. + +### R2-7, sized + +`Level` is mentioned 288 times across `forge/src` and `thermite-*/src`, but only **23 are real comparisons**, in five shapes: + +| shape | count | what it actually is | +|---|---|---| +| verdict proxy | 10 | `cert.level == Level::L3 && cert.reject.is_none()` — asking *did it prove*, not *where does it sit*. Should read `CertVerdict::Proved`. | +| floor | 4 | `< Level::L3` in the build/image path — the only true floors | +| aggregation | 6 | min-over-clauses; unchanged pending §4 | +| downgrade clamp | 1 | `check.rs:2158` | +| bounded check | 1 | `kani.rs:370` | + +**Correction to an earlier assumption:** `G2Checks.g2_flip_permitted` does *not* read a level. It is `declared && checks.all_green()` over four booleans (`axiom_probe`, `doc_drift`, `differential`, `two_phase_tv`). Removing Lx does not touch it. + +The verdict-proxy shape is the same scalar-overload pathology one level further down — it is why `L3` kept accreting meanings — and fixing it is arguably a bug fix independent of this RFC. + +### R2-8, the classification certificate + +The S₂.0 classifier returns `Admitted | Rejected(reason) | Unknown` and drives routing, but **nothing about the fragment is persisted**: `thermite_spec::classifier::classify` is referenced once outside its own crate (`cli.rs:2001`), and `manifest.rs` has no admission field. The frozen `RejectReason` vocabulary dies at the CLI boundary. + +Map that onto §3 and the structure is exact: + +> **classification determines the refutation coordinate** (which fiber) · +> **discharge determines the trust coordinate** (position within it) + +Two phases, two coordinates — and only the second is recorded. Consequences: + +- The best achievable rung for a clause is statically computable and cheap, yet cannot be answered without running the whole pipeline. +- **"Escalate UP, never degrade down" is not independently auditable.** You cannot verify a clause reached the forge because the cage genuinely could not hold it, versus because a cage attempt timed out. RFC-1 §2 requires the classifier "name *why* — a routing reason from a frozen vocabulary, never a bare refusal." That vocabulary exists and is discarded. +- Pre-discharge code has no artifact describing what it logically *is*. + +Today's certificate is a **post-mortem**. R2-8 adds the **prognosis**, which is the more fundamental of the two: it determines the coordinate the post-mortem later fills in. + +### Out of scope, filed separately + +Per the presentation-only boundary: the `KERNEL_CHECKED_TRUST_MARKER` substring conflation; the dual closure classifier (`verified_closure` vs the legacy one); `to_platform_boundary` as a raw string outside `AssuranceScope`. Each is a defect *against* the axes RFC-2 defines, not a change to them. + +## 8. What RFC-2 does not change + +RFC-1 §3 (cage admission), §4 (numeric routing, `@bv` and the three locks), §5 (the forge, the covenant, the meaning audit), §10 (anti-Goodhart), and §13 (limits) stand unmodified. The seven verdicts stay closed. Covenant-before-burn stays structural. This RFC is about how the system *reports* what it already does. + +## 9. Open questions + +- **OQ-1** — Does `refutation` need a `reconstructed` value distinct from `complete`? Current view: no — `trust` carries it, and a reconstructed and a solver-trusted cage clause refute identically. +- **OQ-2** — Should the covenant's `falsify` budget appear in the refutation coordinate (`empirical(50000)`)? Argues for; costs schema churn. +- **OQ-3** — ~~Is `inspection` a trust value or a modifier?~~ **Resolved:** a modifier (§1.3). +- **OQ-4** — ~~Does the partial order break `g2_flip_permitted`?~~ **Resolved:** no — it reads four booleans, not a level (§7). The floor question is settled at §3.4: a declared set of floor tuples, dominance over any member. +- **OQ-5** — ~~How do historical L3 certificates migrate?~~ **Resolved:** they do not need to. 12 hand-authored oracles compared as subsets; re-cutting them is a chore, not a design question (§6). +- **OQ-6** — Does the boundary modality preserve the lattice, or does it fail to distribute over the pentagon? Expectation: it does not distribute, which would make it a second obstruction. Companion question. +- **OQ-7** — Who owns the collapse policy (§5), and what is the review bar for changing it? A collapse policy nobody reviews is an undeclared collapse with extra steps. From bc7d8bebfee5dec60c5b750cdb7ab86ad0b4681d Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 00:38:16 -0700 Subject: [PATCH 5/7] Migrate RFC-3 from #120, as RFC-4 Body copied verbatim; front matter added above it. Comments stay in the issue, which `discussion:` links, because the file is the document and the issue is the discussion. --- .design/rfcs/0004-versioning.md | 151 ++++++++++++++++++++++++++++++++ 1 file changed, 151 insertions(+) create mode 100644 .design/rfcs/0004-versioning.md diff --git a/.design/rfcs/0004-versioning.md b/.design/rfcs/0004-versioning.md new file mode 100644 index 00000000..9264fe77 --- /dev/null +++ b/.design/rfcs/0004-versioning.md @@ -0,0 +1,151 @@ +--- +rfc: 4 +title: Versioning — what a Thermite version number promises +status: draft +supersedes: [] +introduces: [] +discussion: https://github.com/dollspace-gay/Thermite/issues/120 +--- + +# RFC-3: Versioning — what a Thermite version number promises + +| | | +|---|---| +| **Status** | Draft for discussion — not routed, not content-pinned | +| **Companion** | [RFC-2](https://github.com/dollspace-gay/Thermite/issues/119) — coupled; the Lx removal is a beta-line break under this contract | +| **Baseline** | `dollspace-gay/Thermite @ 84d276e7` (gates G1–G4 shipped) | + +--- + +## 0. Where we are + +| | | +|---|---| +| `workspace.package.version` | **`0.0.1`** | +| git tags, entire repository | **two** — `v0.0.1`, `v0.0.2` | +| gates shipped under `0.0.1` | **four** — G1, G2, G3, G4 | +| `CHANGELOG.md` sections | `[Unreleased]`, G3, G2, G1, `v0.1 — baseline architecture` | +| occurrences of "G4" in the changelog | **zero** | + +The changelog states the current position explicitly: + +> Because Thermite is a verification toolchain developed against the RFC-1 +> program (GH issue #2) rather than a semver-released library, entries are +> organized by the program's **stage gates** (G1, G2, G3). + +That was a reasonable call for a research program with one consumer. It has two consequences that are now costing something: + +1. **A four-gate program, including a trust-base migration, shipped entirely under `0.0.1`.** Nothing in the version stream distinguishes the toolchain before and after checked reconstruction. +2. **The changelog still says "Stage 3 completes the RFC-1 program,"** written before Stage 4 existed, and has no G4 entry. The gate vocabulary drifted because gates were doing a job — marking releases — that they are not shaped for. + +There is also now a second consumer. A downstream repository pins Thermite at a commit SHA, because a commit SHA is the only thing precise enough to pin. + +## 1. What a version contracts over + +Thermite is not a library, so "the public API" needs saying explicitly. The version makes promises about **four surfaces**: + +| surface | what breaks | who notices | +|---|---|---| +| **Certificate schema** | the per-clause record: level/tuple, engine, trust, verdict, evidence blocks | anyone consuming or archiving certificates | +| **Assurance semantics** | *what a given certification claims* — even with the schema byte-identical | anyone relying on a certificate to mean something | +| **Language surface** | `.th` grammar: clause forms, tags, effects, refinement sugar | every program | +| **Forge CLI / method surface** | command names, flags, exit codes, JSON shapes | every script and CI pipeline | + +The second is the one conventional semver has no vocabulary for, and it is the one that has already bitten. + +## 2. The motivating example + +`Level::L3` came to denote two mechanisms with materially different trust bases and refutation stories — general Verus/Z3, and the Lean forge. No schema field changed. No CLI flag changed. No `.th` program changed. + +**But what an `L3` certificate claimed became strictly weaker**, and every archived `L3` certificate became ambiguous retroactively: the number never carried enough information to say which mechanism produced it (see [RFC-2](https://github.com/dollspace-gay/Thermite/issues/119) §6). + +Under this RFC that is a **breaking change to assurance semantics** — and it shipped silently, under `0.0.1`, with no release boundary marking it. + +That is the argument for putting assurance semantics inside the version contract. A change that alters what your evidence means is breaking even when every byte of the schema is identical. + +## 3. Gates and versions are different vocabularies + +**Gates are milestones. Versions are contracts.** They answer different questions and should not be made to substitute for each other: + +- a gate says *this stage's headline claim is now defensible* +- a version says *here is what I promise about the four surfaces* + +A release may contain zero gates, one, or several. A gate may land mid-release without changing any contract. + +**Rule.** Gate headings are nested **inside** semver release sections in the changelog, never in place of them. The gate vocabulary stays; it stops being the shipping unit. + +## 4. Pre-release semantics + +**`2.0.0-beta.N` means the certification surface is still moving.** Specifically: + +- The certificate schema **may break between betas.** Consumers pin an exact beta, and the changelog says what moved. +- Assurance semantics may be refined between betas, and **any such change must be called out explicitly** — that is the class of change §2 shows is otherwise invisible. +- Language surface and CLI changes follow ordinary semver intuitions within the beta line: additive freely, removals called out. + +**`2.0.0` is the point the certificate schema freezes.** After it, a schema break requires a major bump, and assurance-semantics changes require one too. + +This is what lets RFC-2 and RFC-3 land in parallel: removing Lx breaks both the schema and the assurance semantics, which is permitted inside the beta line and is exactly what the beta line is for. + +## 5. Schema sprawl — govern the relationship, not the numbers + +Six things are independently versioned today, with no stated relationship between any of them: + +| | where | +|---|---| +| `workspace.package.version = "0.0.1"` | `Cargo.toml` | +| `CHECK_SCHEMA_VERSION: u32 = 7` | `forge/src/cache.rs:126` — **private**, a cache-key input | +| `ThermiteBootableKernelReceiptV1` | kernel image receipt | +| `ThermiteBootableKernelValidationV1` | kernel image validation report | +| `ThermiteKernelPlatformProfileV1` | `platform/*/profile.toml` | +| `ThermitePlatformRegistryBindingV1` | `platform/*/registry.toml` | + +RFC-3 does **not** unify these. Coupling unrelated artifacts means a kernel receipt tweak bumps the toolchain, which is worse than the current situation. + +Instead: **every schema that crosses a repository boundary must declare, in one published place, its compatibility relationship to the project version.** Is it frozen? Does it track minor releases? Does a break in it require a project major? Independent numbering survives; it stops being arbitrary. + +Schemas that do not cross a boundary — `CHECK_SCHEMA_VERSION` is internal to the proof cache — are explicitly *not* public contract, and should be marked as such so nobody pins to them. + +## 6. The prerequisite: certificates carry no version marker + +`forge/src/manifest.rs:489` — the `Certificate` struct has **no schema version field**. `CHECK_SCHEMA_VERSION` is a private constant in `cache.rs` used as a cache-key input, not a certificate field, and no `schema_version` field exists anywhere in the codebase. + +So a consumer holding a certificate cannot determine which schema produced it. The 12 checked-in oracle files are pre-RFC-2 schema and are indistinguishable from post-RFC-2 ones except by inspecting which fields happen to be present. + +**This is a prerequisite for RFC-2's R2-9** (removing Lx) and arguably for any schema change at all. It should land first, and it is small: one additive field, set at emit time. + +## 7. The cut + +| | | +|---|---| +| **`2.0.0-beta.1`** at `84d276e7` | Thermite 2, gates G1–G4 complete. Set `workspace.package.version` to match. | +| `2.0.0-beta.N` | per RFC-2 increment or gate | +| `2.0.0-rc.1` | when certificate schema v3 is stable | +| `2.0.0` | when the schema freezes and the assurance vocabulary is final | + +Changelog work that comes with it: backfill a G4 section, strike "Stage 3 completes the RFC-1 program," and re-nest the existing G1–G3 headings under release sections. + +Why `2.x` rather than continuing `0.x`: the product is called **Thermite 2**, the RFC-1 program that defines it is complete through G4, and the artifacts say `0.0.1`. The mismatch is not cosmetic — it is the same class of error the rest of this document is about, where the record does not say what happened. + +## 8. Identifier convention + +While we are here, because there will be more of these: + +**RFC numbers are identifiers assigned at draft time, not queue positions.** Acceptance and posting order routinely differ from numeric order — as with PEPs and Rust RFCs — and nothing is renumbered to compensate. RFC-3 may land before RFC-2 without either being wrong. + +The same principle is the subject of this RFC: an identifier's job is to name a thing unambiguously, not to encode its position in a sequence. + +## 9. Increments + +| # | increment | risk | +|---|---|---| +| R3-1 | Add a schema version field to `Certificate` (§6) | low — additive, prerequisite for RFC-2 | +| R3-2 | Cut `2.0.0-beta.1`; set `workspace.package.version` | low | +| R3-3 | Restructure `CHANGELOG.md`: gates nested inside releases; backfill G4; strike the stale completion claim | low | +| R3-4 | Publish the four-surface contract and the pre-release semantics | low — documentation | +| R3-5 | Declare each public schema's compatibility relationship; mark internal ones non-contract | low | + +## 10. Open questions + +- **OQ-1** — Does a downstream consumer pin a version or a commit SHA? Today only a SHA is precise enough. If versions are to be pinnable, tags must be cut at a cadence that makes that practical. +- **OQ-2** — Should assurance-semantics changes get their own changelog section, separate from Added/Changed/Fixed? They are the class most easily missed, and §2 is the evidence. +- **OQ-3** — What is the deprecation window inside a beta line? "May break between betas" is permissive; a stated minimum notice may be worth more than the freedom. From a649d403d12e2680017e89fcae75eded27a907d0 Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 00:40:41 -0700 Subject: [PATCH 6/7] Declare the interpreter these gates need, and re-pin what CI touched MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `rfc-check.py`, `req-registry.py` and `reqs` carry a PEP 723 header so `uv run` fetches a matching interpreter instead of inheriting whatever `python3` is on PATH. `req-registry.py` parses the registry with `tomllib`, standard library from 3.11. On an older interpreter it reports "REQ registry inconclusive" and exits 3 — it fails rather than passes, which is right — but the environment error stands in front of the verdict. In this branch the verdict was a fault of mine: three requirements added to the registry without regenerating the status view they appear in. It surfaced only once the gate ran on an interpreter that could parse the file. `.design/reqs/status.md` is regenerated here, and three design-doc pins are refreshed: `.design/tooling/req-registry.md` because this changes files it governs, and `.design/build/bootable-multicore-kernel.md` plus `.design/stage4-epr-reconstruction.md` because `ci.yml` gains one step and both govern it. Neither pipeline they describe is otherwise affected. --- .design/build/bootable-multicore-kernel.md | 2 +- .design/reqs/status.md | 3 +++ .design/rfcs/0005-rfc-process.md | 23 ++++++++++++++++++++++ .design/stage4-epr-reconstruction.md | 2 +- .design/tooling/req-registry.md | 22 ++++++++++++++++++++- tooling/req-registry.py | 4 ++++ tooling/reqs | 4 ++++ tooling/rfc-check.py | 13 +++++++++++- 8 files changed, 69 insertions(+), 4 deletions(-) diff --git a/.design/build/bootable-multicore-kernel.md b/.design/build/bootable-multicore-kernel.md index 1689f1df..ba6f2bf6 100644 --- a/.design/build/bootable-multicore-kernel.md +++ b/.design/build/bootable-multicore-kernel.md @@ -35,7 +35,7 @@ governs: - platform/x86_64-pc-uefi-smp-v1/runtime/Cargo.* - platform/x86_64-pc-uefi-smp-v1/runtime/src/* - .github/workflows/ci.yml -audited-content-sha256: 57214a2c4c466cb21e007a6e4c0d3f7943a8a63d71f944f265f2c14169025a9c +audited-content-sha256: dc0cbb1ef5f1f1cdf2c92a3013cec0626dee0d83378927657cdd772e7445342c (re-pinned 2026-08-06: `.github/workflows/ci.yml` gains one step, the RFC front-matter gate (#127). Nothing else this document governs changed, and the pipeline it describes is unaffected) extends: - .design/build/kernel-target.md - .design/build/l3-rich-composition.md diff --git a/.design/reqs/status.md b/.design/reqs/status.md index 6d6cb814..a4a90167 100644 --- a/.design/reqs/status.md +++ b/.design/reqs/status.md @@ -338,6 +338,9 @@ Source: `.design/reqs/registry.toml` | REQ-REG-4 | shipped | `tooling/req-registry.py` | | tooling | Generated status views | symbol: `render_full_inventory` - status view renderer
test: `tooling/tests/test_req_registry.py::ReqRegistryOracleTest.test_check_detects_stale_generated_view` - stale generated output is a failing condition
command: `tooling/reqs check` - CI-facing generated-view check | | | REQ-REG-5 | shipped | `tooling/req-status.py` | `tooling/req-registry.py` | tooling | Legacy source-comment bridge | file: `tooling/req-status.py` - short-term contradiction tripwire
command: `python3 tooling/req-status.py` - legacy row lint stays green during migration | | | REQ-REG-6 | shipped | `tooling/req-registry.py` | | tooling | Generated-region migration | symbol: `render_reference_list_body` - generated source-comment reference-list view
issue: `github:dollspace-gay/Thermite#17` - RFC tracking the full migration plan | | +| REQ-RFC-FRONTMATTER | shipped | `.design/rfcs` | `.design/rfcs/0005-rfc-process.md`, `tooling/rfc-check.py` | docs | RFC front-matter schema | file: `.design/rfcs/0005-rfc-process.md` - the schema, and the RFC that defines it
symbol: `parse_front_matter` - front-matter reader | | +| REQ-RFC-GATE | shipped | `tooling/rfc-check.py` | `.design/rfcs/0005-rfc-process.md`, `.github/workflows/ci.yml` | docs | RFC front-matter gate | symbol: `check` - the gate
command: `python3 tooling/rfc-check.py` - CI step | | +| REQ-RFC-REGISTRY-LINK | shipped | `tooling/rfc-check.py` | `.design/reqs/registry.toml`, `.design/rfcs/0005-rfc-process.md` | docs | RFC to REQ registry link | symbol: `known_reqs` - registry reader
file: `.design/reqs/registry.toml` - the registry the link resolves against | | | REQ-S1-1 | shipped | `.design/stage1-forge-tier.md` | | forge | Seven-verdict certificate vocabulary | file: `forge/src/verdict.rs` - the cert-level verdict enum + construction sites
symbol: `CertVerdict`
symbol: `from_engine_verdict` - the total, exhaustive, wildcard-free map from engine::Verdict
symbol: `is_kernel_budget_signal` - the Q-KBSIGNAL kernel/elaboration-budget discriminator
symbol: `all_seven_variants_round_trip` - serde round-trip test over all seven variants | | | REQ-S1-10 | partial | `.design/stage1-forge-tier.md` | | forge | G1 gate artifact — the isqrt_class example, the golden cert, the seven-verdict hermetic suite | file: `conformance/forge/isqrt_class.th` - (1) the isqrt_class example: a single fn keyed on the integer-sqrt characterization (req r*r<=n && n<(r+1)^2) with two NON-TRIVIAL nlsat-earned L4 consequences (2*r<=n+1, n<2*r*r+2*r+1 — not req restatements) + one non-relaxable `%` L3 clause, a witness covenant, and the `proof for isqrt_class { ens#2 }` author proof
file: `conformance/forge/isqrt_class.cert.json` - (3) the golden certificate: item L3, per-clause engine nlsat/nlsat/lean, all four evidence blocks (covenant_evidence, engine_attribution, mutants_killed 7/7, burn) + the meaning audit — the AC-14 oracle
symbol: `forge_gate_check` - (2) the `--engine forge` G1 gate pass (check.rs): per-fn dispatch to the per-clause hybrid certificate builder
symbol: `forge_gate_item_cert` - (2) the per-clause hybrid assembly: classify each ens (synthetic single-ens fn), nlsat L4 vs author-proof Lean L3 + burn, covenant-before-burn, meaning audit, re-elaboration mutation, min-level cert with all four evidence blocks
symbol: `EngineSelection` - (2) the `EngineSelection::Forge` variant + the `--engine forge` CLI surface (cli.rs) — additive, returns early in check_file_with_engine; the v1 Verus/lean/auto/nlsat paths are unchanged
test: `forge/tests/g1_gate.rs` - (3) AC-14 cert-oracle (verus+lake-guarded): isqrt_class certifies L3 with clauses L4/L4/L3 (engine nlsat/nlsat/lean) and all four evidence blocks present + populated, == the golden
test: `forge/src/seven_verdicts.rs` - (4) the seven-verdict hermetic suite: verdict_proved / verdict_counterexample / verdict_real_witness / verdict_covenant_refuted / verdict_stuck / verdict_kernel_budget / verdict_timeout — one named test per CertVerdict, all run under cargo test -p forge (the CI lean job)
test: `forge/src/engine.rs` - (4) the UNGATED structural RealWitness producer (classify_sat_real_only_model_is_real_witness): feeds classify_sat the √2 real countermodel directly → RealWitness, never a Counterexample — the AC-14 RealWitness-producer coverage that does not depend on z3 | Gate DECLARATION only — the artifact is shipped, but the G1 gate (REQ-10) is not declared closed here: flipping the README/docs headline ("out-of-cage no longer degrades") is the separate R-GATE-1 step (changes at gate time, not merge time), and the thermite2 governance docs (thermite2-semantics.md / the R-rules / skill v2) are separate authoring steps. This entry covers ONLY the isqrt_class example + golden cert + the seven-verdict suite + zero-v1-regression; it does NOT mark the headline flipped. | | REQ-S1-2 | shipped | `.design/stage1-forge-tier.md` | | forge | Exporter hardening — certify-time axiom gate + correspondence table | symbol: `certify_lean_axioms` - the shared certify-time axiom gate, run on every Lean discharge path
symbol: `STANDARD_AXIOM_ALLOWLIST`
doc: `.design/verified/exporter-surface-correspondence.md` - the inspection-tier exporter-surface correspondence table | | diff --git a/.design/rfcs/0005-rfc-process.md b/.design/rfcs/0005-rfc-process.md index 05f64a63..c4165d59 100644 --- a/.design/rfcs/0005-rfc-process.md +++ b/.design/rfcs/0005-rfc-process.md @@ -201,6 +201,29 @@ non-zero with a specific message. The script ships with this RFC. A process proposal that asks the maintainer to write its own enforcement is one that does not land. +### The gate declares its interpreter + +`rfc-check.py` carries a PEP 723 header, so `uv run tooling/rfc-check.py` fetches +a matching interpreter rather than inheriting whichever `python3` is on PATH. +`req-registry.py` and `reqs` get the same header, for a reason this PR ran into. + +Those two parse the registry with `tomllib`, standard library from Python 3.11. +On an older interpreter they report + +``` +REQ registry inconclusive: tomllib is unavailable (Python < 3.11) +``` + +and exit **3** — so they fail rather than pass, which is right. What they do not +do is tell you anything about the registry, and the environment error stands in +front of whatever the real finding was. In this PR the real finding was a fault +of mine: three requirements added to the registry without regenerating the +status view they appear in. It was invisible until the gate ran on an +interpreter that could parse the file. + +An inconclusive gate is not a lie, but it is a result nobody can act on. The +header makes `uv run tooling/reqs check` produce the actual verdict. + ## What this does not change **Issues stay defect reports**, which is what they are good at. #122–#126 are diff --git a/.design/stage4-epr-reconstruction.md b/.design/stage4-epr-reconstruction.md index e795a1fb..3ad4c3f2 100644 --- a/.design/stage4-epr-reconstruction.md +++ b/.design/stage4-epr-reconstruction.md @@ -3,7 +3,7 @@ diff --git a/.design/tooling/req-registry.md b/.design/tooling/req-registry.md index 50ad58d6..b3ce4e76 100644 --- a/.design/tooling/req-registry.md +++ b/.design/tooling/req-registry.md @@ -4,7 +4,7 @@ tier: 3-component status: draft audited-sha: f09f8ca376257cc1e2543b8ebc9fb771bffd04df (content-sha256 re-pinned 2026-07-29 for stage-3 REQ-1..REQ-9 / gate G3 (#80, crosslink #351): the registry and generated status view carry the fixed-width reconstruction requirements and verified evidence; req-registry.py --check is clean (462 requirements, 119 views). The legacy commit pin remains the f09f8ca3 stable-main ancestor; the active content digest tracks the governed files. prior: 2026-06-21 stage-2 REQ-10 / AC-10 (#332), the pin battery and final gate G2 increment) -audited-content-sha256: 1106ab1e5817d4cbb5928f93b40fce3d262c9482e62e5c7ef86434ef2dc673c2 (re-pinned 2026-08-01 after replacing generated-image evidence with the tracked kernel-image CI gate) +audited-content-sha256: 16a9da4d652be060b86aa36e0d54e08c7b09425762c1c9e100a14f764ff63ff2 (re-pinned 2026-08-06 for the RFC process (#127): three RFC requirements join the registry and the generated status view, and the tools declare their interpreter floor, described under Interpreter floor. req-registry.py --check is clean (527 requirements, 125 views). prior: 2026-08-01 after replacing generated-image evidence with the tracked kernel-image CI gate) governs: - .design/reqs/registry.toml - .design/reqs/status.md @@ -245,6 +245,26 @@ scripts that have not switched to the facade. hand-maintained source status row should be treated as a regression to map or remove. +## Interpreter floor + +`req-registry.py` parses the registry with `tomllib`, which is standard library +from Python 3.11. On an older interpreter it reports + +``` +REQ registry inconclusive: tomllib is unavailable (Python < 3.11) +``` + +and exits **3**. That is correct behaviour — it fails rather than passing — but +the environment error stands in front of the verdict, so a real finding waits +behind it. In #127 the finding was requirements added to the registry without +regenerating the status view they appear in, and it surfaced only once the gate +ran on an interpreter that could parse the file. + +`req-registry.py` and `reqs` therefore carry a PEP 723 header declaring the +floor, so `uv run tooling/reqs check` fetches a matching interpreter rather than +inheriting whichever `python3` is on PATH, and returns a verdict instead of an +excuse. + ## Known Limits This registry does not prove semantic adequacy. A symbol can exist without being diff --git a/tooling/req-registry.py b/tooling/req-registry.py index 853b2b0f..e39a0cc3 100644 --- a/tooling/req-registry.py +++ b/tooling/req-registry.py @@ -1,4 +1,8 @@ #!/usr/bin/env python3 +# /// script +# requires-python = ">=3.11" +# dependencies = [] +# /// """ Canonical REQ registry validator and generated-view writer. diff --git a/tooling/reqs b/tooling/reqs index fb2416b3..15ab3408 100755 --- a/tooling/reqs +++ b/tooling/reqs @@ -1,4 +1,8 @@ #!/usr/bin/env python3 +# /// script +# requires-python = ">=3.11" +# dependencies = [] +# /// """Small command facade for the canonical REQ registry tool.""" from __future__ import annotations diff --git a/tooling/rfc-check.py b/tooling/rfc-check.py index a47e4bfd..e9771e77 100755 --- a/tooling/rfc-check.py +++ b/tooling/rfc-check.py @@ -1,4 +1,8 @@ #!/usr/bin/env python3 +# /// script +# requires-python = ">=3.9" +# dependencies = [] +# /// """ RFC front-matter gate for `.design/rfcs/`. @@ -17,7 +21,14 @@ Usage: - python3 tooling/rfc-check.py [--root ] [--json] + python3 tooling/rfc-check.py [--root ] [--json] [--index] + uv run tooling/rfc-check.py [--root ] [--json] [--index] + +The PEP 723 header above pins the interpreter this needs, so `uv run` fetches a +matching one rather than inheriting whatever `python3` happens to be. This gate +is stdlib-only and works on 3.9, so the header is a statement rather than a +requirement — but a gate that skips silently on the wrong interpreter is worse +than one that fails, and declaring the floor is how that is avoided. """ from __future__ import annotations From 112b2deeccdd306262c12c85a11f351e6d0b9fc2 Mon Sep 17 00:00:00 2001 From: Maxine Levesque <170461181+maxinelevesque@users.noreply.github.com> Date: Thu, 6 Aug 2026 01:00:23 -0700 Subject: [PATCH 7/7] Oracle tests for the RFC gate Fifteen tests under `tooling/tests/`, where CI already discovers them. Each asserts on the reported message rather than only the exit code: a gate that fails for the wrong reason sends the next reader to the wrong place, and an exit-code-only test cannot tell those apart. They cover the front-matter reader, the status enum including the rejection of `implemented`, filename and number agreement, the registry link in both directions, and `supersedes` resolution. Three of them pin the provisional-number rule, which is the part most likely to be mis-implemented later: two drafts may share a number and the gate says so without failing, a draft may not take a canonical one, and two canonical RFCs may never collide. One more derives a revision from real git history rather than a declared field, which is the property the version scheme rests on. `REQ-RFC-GATE` gains test evidence, which is the kind the registry schema prefers for a shipped requirement, and `.design/tooling/req-registry.md` is re-pinned because its governed files changed again. --- .design/reqs/registry.toml | 5 + .design/reqs/status.md | 2 +- .design/tooling/req-registry.md | 2 +- tooling/tests/test_rfc_check.py | 165 ++++++++++++++++++++++++++++++++ 4 files changed, 172 insertions(+), 2 deletions(-) create mode 100644 tooling/tests/test_rfc_check.py diff --git a/.design/reqs/registry.toml b/.design/reqs/registry.toml index 8ea9f417..88854549 100644 --- a/.design/reqs/registry.toml +++ b/.design/reqs/registry.toml @@ -17733,6 +17733,11 @@ kind = "command" target = "python3 tooling/rfc-check.py" note = "CI step" +[[requirement.evidence]] +kind = "test" +target = "tooling/tests/test_rfc_check.py" +note = "15 oracle tests, asserting on the reported message rather than the exit code" + [[requirement]] id = "REQ-RFC-REGISTRY-LINK" title = "RFC to REQ registry link" diff --git a/.design/reqs/status.md b/.design/reqs/status.md index a4a90167..a02da26e 100644 --- a/.design/reqs/status.md +++ b/.design/reqs/status.md @@ -339,7 +339,7 @@ Source: `.design/reqs/registry.toml` | REQ-REG-5 | shipped | `tooling/req-status.py` | `tooling/req-registry.py` | tooling | Legacy source-comment bridge | file: `tooling/req-status.py` - short-term contradiction tripwire
command: `python3 tooling/req-status.py` - legacy row lint stays green during migration | | | REQ-REG-6 | shipped | `tooling/req-registry.py` | | tooling | Generated-region migration | symbol: `render_reference_list_body` - generated source-comment reference-list view
issue: `github:dollspace-gay/Thermite#17` - RFC tracking the full migration plan | | | REQ-RFC-FRONTMATTER | shipped | `.design/rfcs` | `.design/rfcs/0005-rfc-process.md`, `tooling/rfc-check.py` | docs | RFC front-matter schema | file: `.design/rfcs/0005-rfc-process.md` - the schema, and the RFC that defines it
symbol: `parse_front_matter` - front-matter reader | | -| REQ-RFC-GATE | shipped | `tooling/rfc-check.py` | `.design/rfcs/0005-rfc-process.md`, `.github/workflows/ci.yml` | docs | RFC front-matter gate | symbol: `check` - the gate
command: `python3 tooling/rfc-check.py` - CI step | | +| REQ-RFC-GATE | shipped | `tooling/rfc-check.py` | `.design/rfcs/0005-rfc-process.md`, `.github/workflows/ci.yml` | docs | RFC front-matter gate | symbol: `check` - the gate
command: `python3 tooling/rfc-check.py` - CI step
test: `tooling/tests/test_rfc_check.py` - 15 oracle tests, asserting on the reported message rather than the exit code | | | REQ-RFC-REGISTRY-LINK | shipped | `tooling/rfc-check.py` | `.design/reqs/registry.toml`, `.design/rfcs/0005-rfc-process.md` | docs | RFC to REQ registry link | symbol: `known_reqs` - registry reader
file: `.design/reqs/registry.toml` - the registry the link resolves against | | | REQ-S1-1 | shipped | `.design/stage1-forge-tier.md` | | forge | Seven-verdict certificate vocabulary | file: `forge/src/verdict.rs` - the cert-level verdict enum + construction sites
symbol: `CertVerdict`
symbol: `from_engine_verdict` - the total, exhaustive, wildcard-free map from engine::Verdict
symbol: `is_kernel_budget_signal` - the Q-KBSIGNAL kernel/elaboration-budget discriminator
symbol: `all_seven_variants_round_trip` - serde round-trip test over all seven variants | | | REQ-S1-10 | partial | `.design/stage1-forge-tier.md` | | forge | G1 gate artifact — the isqrt_class example, the golden cert, the seven-verdict hermetic suite | file: `conformance/forge/isqrt_class.th` - (1) the isqrt_class example: a single fn keyed on the integer-sqrt characterization (req r*r<=n && n<(r+1)^2) with two NON-TRIVIAL nlsat-earned L4 consequences (2*r<=n+1, n<2*r*r+2*r+1 — not req restatements) + one non-relaxable `%` L3 clause, a witness covenant, and the `proof for isqrt_class { ens#2 }` author proof
file: `conformance/forge/isqrt_class.cert.json` - (3) the golden certificate: item L3, per-clause engine nlsat/nlsat/lean, all four evidence blocks (covenant_evidence, engine_attribution, mutants_killed 7/7, burn) + the meaning audit — the AC-14 oracle
symbol: `forge_gate_check` - (2) the `--engine forge` G1 gate pass (check.rs): per-fn dispatch to the per-clause hybrid certificate builder
symbol: `forge_gate_item_cert` - (2) the per-clause hybrid assembly: classify each ens (synthetic single-ens fn), nlsat L4 vs author-proof Lean L3 + burn, covenant-before-burn, meaning audit, re-elaboration mutation, min-level cert with all four evidence blocks
symbol: `EngineSelection` - (2) the `EngineSelection::Forge` variant + the `--engine forge` CLI surface (cli.rs) — additive, returns early in check_file_with_engine; the v1 Verus/lean/auto/nlsat paths are unchanged
test: `forge/tests/g1_gate.rs` - (3) AC-14 cert-oracle (verus+lake-guarded): isqrt_class certifies L3 with clauses L4/L4/L3 (engine nlsat/nlsat/lean) and all four evidence blocks present + populated, == the golden
test: `forge/src/seven_verdicts.rs` - (4) the seven-verdict hermetic suite: verdict_proved / verdict_counterexample / verdict_real_witness / verdict_covenant_refuted / verdict_stuck / verdict_kernel_budget / verdict_timeout — one named test per CertVerdict, all run under cargo test -p forge (the CI lean job)
test: `forge/src/engine.rs` - (4) the UNGATED structural RealWitness producer (classify_sat_real_only_model_is_real_witness): feeds classify_sat the √2 real countermodel directly → RealWitness, never a Counterexample — the AC-14 RealWitness-producer coverage that does not depend on z3 | Gate DECLARATION only — the artifact is shipped, but the G1 gate (REQ-10) is not declared closed here: flipping the README/docs headline ("out-of-cage no longer degrades") is the separate R-GATE-1 step (changes at gate time, not merge time), and the thermite2 governance docs (thermite2-semantics.md / the R-rules / skill v2) are separate authoring steps. This entry covers ONLY the isqrt_class example + golden cert + the seven-verdict suite + zero-v1-regression; it does NOT mark the headline flipped. | diff --git a/.design/tooling/req-registry.md b/.design/tooling/req-registry.md index b3ce4e76..b0d783e1 100644 --- a/.design/tooling/req-registry.md +++ b/.design/tooling/req-registry.md @@ -4,7 +4,7 @@ tier: 3-component status: draft audited-sha: f09f8ca376257cc1e2543b8ebc9fb771bffd04df (content-sha256 re-pinned 2026-07-29 for stage-3 REQ-1..REQ-9 / gate G3 (#80, crosslink #351): the registry and generated status view carry the fixed-width reconstruction requirements and verified evidence; req-registry.py --check is clean (462 requirements, 119 views). The legacy commit pin remains the f09f8ca3 stable-main ancestor; the active content digest tracks the governed files. prior: 2026-06-21 stage-2 REQ-10 / AC-10 (#332), the pin battery and final gate G2 increment) -audited-content-sha256: 16a9da4d652be060b86aa36e0d54e08c7b09425762c1c9e100a14f764ff63ff2 (re-pinned 2026-08-06 for the RFC process (#127): three RFC requirements join the registry and the generated status view, and the tools declare their interpreter floor, described under Interpreter floor. req-registry.py --check is clean (527 requirements, 125 views). prior: 2026-08-01 after replacing generated-image evidence with the tracked kernel-image CI gate) +audited-content-sha256: 68d2b71dc3764885450afa985b710f40840a6fe7c48b35c7e8d1bab8474f3505 (re-pinned 2026-08-06 for the RFC process (#127): three RFC requirements join the registry and the generated status view, and the tools declare their interpreter floor, described under Interpreter floor. req-registry.py --check is clean (527 requirements, 125 views); the RFC gate carries test evidence. prior: 2026-08-01 after replacing generated-image evidence with the tracked kernel-image CI gate) governs: - .design/reqs/registry.toml - .design/reqs/status.md diff --git a/tooling/tests/test_rfc_check.py b/tooling/tests/test_rfc_check.py new file mode 100644 index 00000000..b67c6e72 --- /dev/null +++ b/tooling/tests/test_rfc_check.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""Oracle tests for tooling/rfc-check.py. + +Each test asserts on the reported message rather than only the exit code. A gate +that fails for the wrong reason is a gate that sends the next reader to the wrong +place, and an exit-code-only test cannot tell the two apart. +""" + +import subprocess +import sys +import tempfile +import textwrap +import unittest +from pathlib import Path + + +GATE = Path(__file__).resolve().parents[1] / "rfc-check.py" + + +class Fixture: + def __init__(self, root: Path): + self.root = root + (root / ".design" / "rfcs").mkdir(parents=True, exist_ok=True) + (root / ".design" / "reqs").mkdir(parents=True, exist_ok=True) + (root / ".design" / "reqs" / "registry.toml").write_text( + 'id = "REQ-KNOWN"\n', encoding="utf-8" + ) + + def rfc(self, name: str, body: str): + p = self.root / ".design" / "rfcs" / name + p.write_text(textwrap.dedent(body).lstrip(), encoding="utf-8") + return p + + def run(self, *args): + return subprocess.run( + [sys.executable, str(GATE), "--root", str(self.root), *args], + capture_output=True, + text=True, + ) + + +def front(rfc: int, status: str = "draft", title: str = "A title", extra: str = "") -> str: + return f"---\nrfc: {rfc}\ntitle: {title}\nstatus: {status}\n{extra}---\n\nbody\n" + + +class RfcCheckTests(unittest.TestCase): + def setUp(self): + self._tmp = tempfile.TemporaryDirectory() + self.fx = Fixture(Path(self._tmp.name)) + + def tearDown(self): + self._tmp.cleanup() + + def test_well_formed_rfc_passes(self): + self.fx.rfc("0001-a-thing.md", front(1, "accepted")) + r = self.fx.run() + self.assertEqual(r.returncode, 0, r.stderr) + self.assertIn("ok", r.stdout) + + def test_missing_front_matter_is_named(self): + self.fx.rfc("0001-a-thing.md", "# no front matter\n") + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("no front matter", r.stderr) + + def test_unclosed_front_matter_is_named(self): + self.fx.rfc("0001-a-thing.md", "---\nrfc: 1\ntitle: T\nstatus: draft\n") + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("not closed", r.stderr) + + def test_missing_required_field_is_named(self): + self.fx.rfc("0001-a-thing.md", "---\nrfc: 1\nstatus: draft\n---\n\nbody\n") + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("missing `title`", r.stderr) + + def test_implemented_is_not_a_status(self): + """Implementation is derived from the REQ registry, never declared.""" + self.fx.rfc("0001-a-thing.md", front(1, "implemented")) + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("derived from the REQ registry", r.stderr) + + def test_number_must_match_filename(self): + self.fx.rfc("0007-a-thing.md", front(9)) + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("disagrees with the filename prefix", r.stderr) + + def test_filename_shape_is_enforced(self): + self.fx.rfc("not-an-rfc.md", front(1)) + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("NNNN-slug.md", r.stderr) + + def test_unknown_introduced_req_is_rejected(self): + self.fx.rfc("0001-a-thing.md", front(1, extra="introduces: [REQ-NOPE]\n")) + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("REQ-NOPE", r.stderr) + + def test_known_introduced_req_is_accepted(self): + self.fx.rfc("0001-a-thing.md", front(1, extra="introduces: [REQ-KNOWN]\n")) + self.assertEqual(self.fx.run().returncode, 0) + + def test_supersedes_must_exist(self): + self.fx.rfc("0002-b.md", front(2, extra="supersedes: [1]\n")) + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("supersedes RFC-1", r.stderr) + + # --- the provisional-number rule ------------------------------------- + + def test_two_drafts_may_share_a_number(self): + """A draft's number is provisional; the collision resolves at merge.""" + self.fx.rfc("0004-one.md", front(4, "draft")) + self.fx.rfc("0004-two.md", front(4, "draft", title="Rival")) + r = self.fx.run() + self.assertEqual(r.returncode, 0, r.stderr) + self.assertIn("provisional until merge", r.stderr) + + def test_draft_may_not_take_a_canonical_number(self): + self.fx.rfc("0004-one.md", front(4, "accepted")) + self.fx.rfc("0004-two.md", front(4, "draft", title="Rival")) + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("already used by", r.stderr) + + def test_two_canonical_rfcs_may_not_share(self): + self.fx.rfc("0004-one.md", front(4, "accepted")) + self.fx.rfc("0004-two.md", front(4, "rejected", title="Rival")) + r = self.fx.run() + self.assertEqual(r.returncode, 1) + self.assertIn("already used by", r.stderr) + + # --- the derived index ------------------------------------------------ + + def test_index_reports_unversioned_outside_git(self): + self.fx.rfc("0001-a-thing.md", front(1, "accepted")) + r = self.fx.run("--index") + self.assertEqual(r.returncode, 0) + self.assertIn("unversioned", r.stdout) + + def test_index_derives_the_revision_from_git(self): + """r is the count of commits touching the file, not a declared field.""" + root = self.fx.root + env = {"GIT_AUTHOR_NAME": "t", "GIT_AUTHOR_EMAIL": "t@e", + "GIT_COMMITTER_NAME": "t", "GIT_COMMITTER_EMAIL": "t@e"} + def git(*a): + subprocess.run(["git", *a], cwd=root, check=True, + capture_output=True, env={**dict(**env), "PATH": "/usr/bin:/bin:/usr/local/bin"}) + git("init", "-q") + self.fx.rfc("0001-a-thing.md", front(1, "accepted")) + git("add", "-A"); git("commit", "-q", "-m", "one") + self.fx.rfc("0001-a-thing.md", front(1, "accepted", title="Retitled")) + git("add", "-A"); git("commit", "-q", "-m", "two") + + r = self.fx.run("--index", "--json") + self.assertEqual(r.returncode, 0, r.stderr) + self.assertIn('"revision": 2', r.stdout) + + +if __name__ == "__main__": + unittest.main()