Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .design/build/bootable-multicore-kernel.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
65 changes: 65 additions & 0 deletions .design/reqs/registry.toml
Original file line number Diff line number Diff line change
Expand Up @@ -17692,3 +17692,68 @@ 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.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"
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"
3 changes: 3 additions & 0 deletions .design/reqs/status.md
Original file line number Diff line number Diff line change
Expand Up @@ -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<br>test: `tooling/tests/test_req_registry.py::ReqRegistryOracleTest.test_check_detects_stale_generated_view` - stale generated output is a failing condition<br>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<br>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<br>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<br>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<br>command: `python3 tooling/rfc-check.py` - CI step<br>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<br>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<br>symbol: `CertVerdict`<br>symbol: `from_engine_verdict` - the total, exhaustive, wildcard-free map from engine::Verdict<br>symbol: `is_kernel_budget_signal` - the Q-KBSIGNAL kernel/elaboration-budget discriminator<br>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<br>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<br>symbol: `forge_gate_check` - (2) the `--engine forge` G1 gate pass (check.rs): per-fn dispatch to the per-clause hybrid certificate builder<br>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<br>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<br>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<br>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)<br>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<br>symbol: `STANDARD_AXIOM_ALLOWLIST`<br>doc: `.design/verified/exporter-surface-correspondence.md` - the inspection-tier exporter-surface correspondence table | |
Expand Down
Loading
Loading