diff --git a/.machine_readable/coaptation/receipts/latest.toml b/.machine_readable/coaptation/receipts/latest.toml index c97cd1ce..6e4e715b 100644 --- a/.machine_readable/coaptation/receipts/latest.toml +++ b/.machine_readable/coaptation/receipts/latest.toml @@ -104,4 +104,4 @@ bust.contractile-parse-error = "latent" [provenance] contractiles = "intend@89c97164fbff must@b2888ac670fb trust@484d6509ce86 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91" -descriptiles = "deed@7182c2cc6635 anchor@11df55a6aaeb" +descriptiles = "deed@7182c2cc6635 anchor@bba9793279e0" diff --git a/CLAUDE.md b/CLAUDE.md index f6673838..7ac949c8 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -6,7 +6,7 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell - + # You are in the hyperpolymath estate — orient before acting @@ -79,7 +79,7 @@ Put every question that needs the owner's decision through the selector (the Ask - **Golden path** (ANCHOR) — `just check` → Every generated view matches its data: catalogue, census tests, atlas, claims registry, bridges; Every gated proof checks in the pinned Guix shell, with no axiom, Admitted, sorry or postulate in its cone. - **State** — phase incubating; maturity experimental. Milestones and next actions: `docs/status/ROADMAP.adoc`. - + ## Estate-Wide Format Migration Directives diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index cbc1d2a9..f9911f02 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -105,7 +105,8 @@ not exist yet, so no bridge is checked against both homes. ____ THY-1, reachability is monotone under additive features, is proved in Agda and re-proved in Rocq and Lean. CI checks all three in a -pinned Guix shell. +pinned Guix shell. A theorem enters the theory shelf only under a stated +admission rule, and a generated index lists each one with its dependant. ____ How this is implemented:: @@ -117,7 +118,10 @@ The sources are `link:verification/proofs/agda/FeatureReachability.agda[]`, `.github/workflows/agda-proof-policy.yml` runs it in the Guix shell pinned by `build/channels.scm` and `build/manifest.scm`, with planted controls (`tests/proofs/gate_controls_test.sh`). CI run 43057783538 on `main` at -`b2cf524` passed. See the <>. +`b2cf524` passed. See the <>. The admission rule is in +`link:docs/theory/README.adoc[]`; `link:scripts/registry/theory.mjs[]` checks +each record in `docs/theory/admissions.jsonl` against the claim pins and +renders `docs/theory/generated/index.adoc` with the grade the registry derives. Caveat:: The proof is about a graph model. That the model matches Cargo's feature @@ -193,15 +197,6 @@ badges on a public repository. The README carries none, because no Best Practices project identifier is recorded for Mathesis. ==== -[CAUTION] -==== -Template example proofs: `verification/proofs/idris2/`, -`verification/proofs/tlaplus/`, `verification/proofs/agda/Properties.agda`, -`verification/proofs/coq/TypeSafety.v` and -`verification/proofs/lean4/ApiTypes.lean` come from the RSR template. They -are not Mathesis obligations. WO 4.1 of the re-anchoring plan removes them. -==== - [CAUTION] ==== Contract probes: the `must` contract states six Mathesis invariants with @@ -223,7 +218,7 @@ guard and the public frame (8 test files, all passed on 2026-11-11) |View determinism, row validation, the public frame (13 tests) |`tests/registry/` -|Registry derivation through fixture receipts (14 tests) +|Registry derivation through fixture receipts, and the admissions of the theory shelf (17 tests) |`tests/proofs/gate_controls_test.sh` |A planted `postulate`, `Admitted` and `sorry` each fail the proof gate (CI) @@ -271,7 +266,7 @@ and `_⊔_` as builtins. |open |- |`docs/proposals/mathesis-research-programme.adoc` -|Not yet stated in a prover (WO 4.1) +|Not yet stated in a prover (next on the theory shelf) |=== Proofs: 3 proven of 5; 1 argued, 1 open. The registry derives `PWG-1` for diff --git a/README.adoc b/README.adoc index dd5df8cb..a3949a39 100644 --- a/README.adoc +++ b/README.adoc @@ -30,7 +30,8 @@ describes what is proved, where, and how strongly. repositories, generated into one view. * *Home theory.* THY-1, reachability is monotone under additive features, is proved in Agda and re-proved in Rocq and Lean. CI checks all three in a - pinned Guix shell. + pinned Guix shell. A theorem enters the theory shelf only under a stated + admission rule, and a generated index lists each one with its dependant. * *Applied systems.* Methods that apply mathematics to decisions, starting with accounting and finance. Design documents only so far. * *Privacy by count.* The frame names public repositories only. The number of @@ -39,7 +40,7 @@ describes what is proved, where, and how strongly. [NOTE] .Planned ==== -The theory shelf's admission rule and the token-lattice theorems, the applied +The token-lattice theorems of the theory shelf, the applied shelf tied to the evidence rules, a published atlas, receipts in more home repositories, and a scheduled census. See link:docs/status/ROADMAP.adoc[the roadmap]. @@ -90,6 +91,10 @@ records (`claims/`), and generated views (`generated/`) |`verification/receipts/` |The proof receipt of Mathesis +|`docs/theory/` +|The theory shelf: the admission rule, the admission records and the +generated theorem index + |`applied-systems/` |The applied shelf diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index 11ac0219..51879408 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -223,13 +223,6 @@ your own repo - but do not read their emptiness as neglect here. | `docs/reports/performance/` | `docs/reports/quality/` | `docs/reports/security/` -| `docs/theory/` -| `docs/theory/computing/` -| `docs/theory/formalisms/` -| `docs/theory/mathematics/` -| `docs/theory/ontologies/` -| `docs/theory/other/` -| `docs/theory/socio-technical/` | `docs/whitepapers/academic/` | `docs/whitepapers/industry/` | `examples/` diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 8daa8b2a..9a2213fc 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -33,7 +33,7 @@ watch) ladder, starting with the chain of PROOF-POLICY §5. Ruling D-10 puts their home in Mathesis. |Agda, re-checked in Rocq and Lean -|Open (WO 4.1) +|Open (next on the theory shelf) |Statements: `docs/proposals/mathesis-research-programme.adoc` |To be allocated @@ -46,16 +46,9 @@ home in Mathesis. No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed declares neither capability. -[NOTE] -.Template example proofs -==== -`verification/proofs/idris2/`, `verification/proofs/tlaplus/`, -`verification/proofs/agda/Properties.agda`, -`verification/proofs/coq/TypeSafety.v` and -`verification/proofs/lean4/ApiTypes.lean` come from the RSR template. They -are examples, not Mathesis obligations. WO 4.1 of the re-anchoring plan -removes them. -==== +The template example proofs of the RSR template (Idris2, TLA+, and one +example each for Agda, Rocq and Lean) were removed in WO 4.1 of the +re-anchoring plan. They were never Mathesis obligations. == Banned patterns diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 6d1e69ae..5ef49f5c 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -18,7 +18,7 @@ reader of PROOF-POLICY §8.5.1. |`PWG-1` |The receipt `verification/receipts/theory_praxis.deed`; the record below -|The token-lattice theorems (WO 4.1) +|The token-lattice theorems (next on the theory shelf) |Open |- |Not yet stated in a prover @@ -31,8 +31,7 @@ reader of PROOF-POLICY §8.5.1. *Overall*: 1 of 3 obligations discharged; 2 open. These are counts, not a percentage: PROOF-POLICY §8 grades are derived from receipts and are never -flattened. The template example proofs are not obligations (see -link:PROOF-NEEDS.adoc[PROOF-NEEDS]). +flattened. The template example proofs were removed in WO 4.1. == Theory theorems diff --git a/docs/status/READINESS.adoc b/docs/status/READINESS.adoc index 7754a954..9628bc06 100644 --- a/docs/status/READINESS.adoc +++ b/docs/status/READINESS.adoc @@ -85,7 +85,7 @@ public repository is not reached |D |alpha-unstable |CI passes with controls; THY-1 at `PWG-1` in three provers -|A dogfood log; the template example proofs still sit in the gate (WO 4.1) +|A dogfood log |=== The applied shelf (`applied-systems/`) is not graded: it holds design diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index ea956beb..4f56276d 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -145,6 +145,20 @@ One pull request that changes census rows is open at a time (atlas README, ** The merge that joined WO 3.2 and WO 3.5 dropped two entries of `(variant (paths :diverged))`. WO 3.4 restores them. +=== Re-anchoring: stage 4 (2026-11-11) + +* WO 4.1, the theory shelf: `docs/theory/README.adoc` states the admission + rule. `docs/theory/admissions.jsonl` holds one authored record for each + home theorem; `claims-registry.mjs` checks it against the claim pins and + generates `docs/theory/generated/index.adoc`. All template example proofs + and the six template stubs under `docs/theory/` are removed (owner rulings + 2026-11-11). +* Next, by owner ruling: an append-only ledger of the theory work, written + only by a `just theory-ledger` recipe and checked in CI, in its own pull + request. +* Finding: the `intend` contract still marks stage 3 `in_progress` and + stage 4 `declared`; a contract edit needs owner review. + [[stages]] == Stages @@ -173,14 +187,14 @@ gate gap, Agda, Rocq and Lean in CI, the receipt of Mathesis |3 |Tell the truth: deed, capabilities, contracts, entry documents, no private names, affirmation -|In progress: WO 3.1, 3.2, 3.3 and 3.5 merged; WO 3.4 in review; WO 3.6 -next +|Done: WO 3.1 to 3.6 merged (pull requests 73 to 78); the affirmation +anchors `c81cb84` |4 |The three shelves: the theory admission rule and the token-lattice theorems, the applied shelf tied to the evidence spine, the published atlas (needs a ruling) -|Declared +|In progress: WO 4.1 in review |5 |Scale: receipts in the home repositories, the bridge lock pilot, a diff --git a/docs/theory/README.adoc b/docs/theory/README.adoc index 20ef5b6d..287788bc 100644 --- a/docs/theory/README.adoc +++ b/docs/theory/README.adoc @@ -1,3 +1,63 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= theory Unit += The theory shelf + +The theory shelf holds the theorems whose home is Mathesis: theory that an +estate rule, vocabulary or interface depends on, and that no single system +owns. The other two shelves are the atlas (`docs/atlas/`) and the applied +systems (`applied-systems/`). + +== The admission rule + +A theorem enters the shelf only when all three conditions hold: + +. *It is theory* by the test of + https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY] + §1. A statement that names a type, function or wire format of one + repository is engineering, and belongs to that repository. A statement + that would be true of any implementation is theory. +. *No single system owns it.* A theorem about one system's own behaviour + lives in that system's repository. +. *An estate rule, vocabulary or interface depends on it,* and the record + names that dependant. + +A theorem that meets the rule is proved in Agda and re-checked in Rocq and +Lean (PROOF-POLICY §1 and §2), with a receipt in `verification/receipts/`. + +== Where the records are + +[cols="1,3",options="header"] +|=== +|Path |Contents + +|`admissions.jsonl` +|One authored admission record for each theorem: why it is theory, why no +single system owns it, and the dependant (repository, path and rule). It +holds no grade. + +|`generated/index.adoc` +|The theorem index, generated by `scripts/registry/claims-registry.mjs` from +the admission records, the claim pins and the receipt. Never edit it by hand. + +|`../../verification/proofs/` +|The Agda, Rocq and Lean sources. + +|`../../verification/receipts/theory_praxis.deed` +|The proof receipt of Mathesis (PROOF-POLICY §8.5.1). +|=== + +`just registry-check` (part of `just check`) fails when the index is stale, +when a home theorem has no admission record, or when an admission names no +dependant, a non-public dependant repository, or a theorem with no claim +pin. + +== Admitting a theorem + +. State the theorem, prove it in Agda, and re-prove it in Rocq and Lean. +. Add each leg to the receipt, from observed checker runs. +. Pin the claim in `docs/atlas/claims/claims.jsonl`. +. Add its admission record to `admissions.jsonl`. +. Run `bun scripts/registry/claims-registry.mjs build`, then `just check`. + +The token-lattice theorems are the next candidates (ruling D-10). Their +statements are in `docs/proposals/mathesis-research-programme.adoc`. diff --git a/docs/theory/admissions.jsonl b/docs/theory/admissions.jsonl new file mode 100644 index 00000000..a50ba048 --- /dev/null +++ b/docs/theory/admissions.jsonl @@ -0,0 +1 @@ +{"admitted":"2026-11-11","dependant":{"path":"docs/UPSTREAM-DEPENDENCY-WATCH.adoc","repository":"metadatastician/standards","rule":"Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build."},"id":"hyperpolymath/mathesis#THY-1","owner":"No single system owns it: it describes the feature resolution that any Cargo workspace exhibits, and Cargo is third-party.","theory":"It names no type, function or wire format of one repository: it holds for any dependency graph whose edges are guarded by features closed under Horn rules (PROOF-POLICY §1)."} diff --git a/docs/theory/computing/README.adoc b/docs/theory/computing/README.adoc deleted file mode 100644 index be73e735..00000000 --- a/docs/theory/computing/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Computing Theory diff --git a/docs/theory/formalisms/README.adoc b/docs/theory/formalisms/README.adoc deleted file mode 100644 index fcbc818e..00000000 --- a/docs/theory/formalisms/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Formalisms Theory diff --git a/docs/theory/generated/index.adoc b/docs/theory/generated/index.adoc new file mode 100644 index 00000000..552f85ab --- /dev/null +++ b/docs/theory/generated/index.adoc @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// GENERATED by scripts/registry/claims-registry.mjs from docs/theory/admissions.jsonl, +// docs/atlas/claims/claims.jsonl and the receipt they pin; do not hand-edit. += Theorem index of the theory shelf + +One row for each theorem whose home is Mathesis. The grade is derived from +the receipt by the canon reader, never typed. The admission rule is in +link:../README.adoc[the theory README]. + +Theorems: 1. + +[cols="1,3,1,2,3",options="header"] +|=== +|Theorem |Statement |PWG |Source and receipt |Dependant + +|THY-1 |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. |`PWG-1` |`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`; `verification/receipts/theory_praxis.deed` at `9aa1662da5b2` |https://github.com/metadatastician/standards/blob/main/docs/UPSTREAM-DEPENDENCY-WATCH.adoc[metadatastician/standards]: Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build. + +|=== diff --git a/docs/theory/mathematics/README.adoc b/docs/theory/mathematics/README.adoc deleted file mode 100644 index f4653d15..00000000 --- a/docs/theory/mathematics/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Mathematics Theory diff --git a/docs/theory/ontologies/README.adoc b/docs/theory/ontologies/README.adoc deleted file mode 100644 index 2008f2ab..00000000 --- a/docs/theory/ontologies/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Ontologies Theory diff --git a/docs/theory/other/README.adoc b/docs/theory/other/README.adoc deleted file mode 100644 index 16ed2b16..00000000 --- a/docs/theory/other/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Other Theory diff --git a/docs/theory/socio-technical/README.adoc b/docs/theory/socio-technical/README.adoc deleted file mode 100644 index 91fa6701..00000000 --- a/docs/theory/socio-technical/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Socio technical Theory diff --git a/mathesis_chora.deed b/mathesis_chora.deed index 5c70f37f..b91c1a28 100644 --- a/mathesis_chora.deed +++ b/mathesis_chora.deed @@ -283,15 +283,8 @@ (directory :id "report-unit-quality" :ply 3 :path "docs/reports/quality" :description "Specialised repository for quality findings and evidence.") (directory :id "report-unit-security" :ply 3 :path "docs/reports/security" :description "Specialised repository for security findings and evidence.")) (directory :id "standards-unit" :ply 2 :path "docs/standards" :description "Standards unit for high-rigor verification.") - (directory :id "theory-track" :ply 2 :path "docs/theory" :description "Documentation track for domain-specific theory and research foundations.\nCategorised by discipline." - (canonical-locations :computing "computing/" :formalisms "formalisms/" :mathematics "mathematics/" :ontologies "ontologies/" :other "other/" :socio_technical "socio-technical/") - :invariants ("Theoretical claims MUST reference established academic or technical formalisms") - (directory :id "theory-unit-computing" :ply 3 :path "docs/theory/computing" :description "Theoretical foundation for computing.") - (directory :id "theory-unit-formalisms" :ply 3 :path "docs/theory/formalisms" :description "Theoretical foundation for formalisms.") - (directory :id "theory-unit-mathematics" :ply 3 :path "docs/theory/mathematics" :description "Theoretical foundation for mathematics.") - (directory :id "theory-unit-ontologies" :ply 3 :path "docs/theory/ontologies" :description "Theoretical foundation for ontologies.") - (directory :id "theory-unit-other" :ply 3 :path "docs/theory/other" :description "Theoretical foundation for other.") - (directory :id "theory-unit-socio-technical" :ply 3 :path "docs/theory/socio-technical" :description "Theoretical foundation for socio technical.")) + (directory :id "theory-track" :ply 2 :path "docs/theory" :description "The theory shelf: the admission rule (README.adoc), the authored\nadmission records (admissions.jsonl) and the generated theorem index\n(generated/index.adoc). Re-anchoring plan WO 4.1." + :invariants ("A theorem enters only when the admission rule of README.adoc holds" "Each theorem whose home is Mathesis has an admission record and a receipt")) (directory :id "whitepapers-track" :ply 2 :path "docs/whitepapers" :description "Unit for strategic publications and whitepapers. Categorised by target\naudience: Academic, Industry, and Outreach." (canonical-locations :academic "academic/" :industry "industry/" :outreach "outreach/") :invariants ("Each sub-track MUST have a clear audience definition in its README") @@ -362,12 +355,12 @@ "The theory theorems whose home is Mathesis (THY-1)" "The applied methods in applied-systems/" )) - ; Measured 2026-11-11 over the tracked files. Rust, Idris2 and TLA+ are - ; template material (verification/proofs/idris2/, verification/proofs/tlaplus/, - ; scripts/*.rs). WO 3.2 removed the Zig and Idris2 seam (src/interface/); - ; WO 4.1 of the re-anchoring plan decides which of the rest stay. + ; Measured 2026-11-11 over the tracked files. Idris2 remains for the + ; coaptation core (.machine_readable/coaptation/core/), Rust for the + ; template tools (scripts/*.rs). WO 3.2 removed the Zig seam; WO 4.1 + ; removed the template example proofs, the last TLA+ file among them. (implementation-policy - :allowed ("JavaScript on Bun" "Shell" "AWK" "jq" "Just" "Nickel" "Guile Scheme (Guix)" "Agda" "Rocq" "Lean 4" "AsciiDoc" "Rust" "Idris2" "Zig" "TLA+") + :allowed ("JavaScript on Bun" "Shell" "AWK" "jq" "Just" "Nickel" "Guile Scheme (Guix)" "Agda" "Rocq" "Lean 4" "AsciiDoc" "Rust" "Idris2") :forbidden ("Node.js" "npm" "Nix" "Python" "Go" "TypeScript" "ReScript")) ; `just check` is the recipe that CI runs in the pinned Guix shell ; (agda-proof-policy.yml, re-anchoring plan WO 2.5). @@ -1032,7 +1025,12 @@ :removed ("archetypes/" "build/docs-seed/" "build/templates/" "rsr-template-repo_chora.deed" "src/interface/" "benches/" "build/container/Containerfile" "tests/ffi_strings_test.sh" - ".github/workflows/rust-ci.yml" ".github/workflows/release.yml") + ".github/workflows/rust-ci.yml" ".github/workflows/release.yml" + "verification/proofs/idris2/" "verification/proofs/tlaplus/" + "verification/proofs/agda/Properties.agda" "verification/proofs/coq/TypeSafety.v" + "verification/proofs/lean4/ApiTypes.lean" + "docs/theory/computing/" "docs/theory/formalisms/" "docs/theory/mathematics/" + "docs/theory/ontologies/" "docs/theory/other/" "docs/theory/socio-technical/") ; .github/labels.json and .github/label-classifier.json: their ; _generated_from no longer names a private repository (WO 3.5). ; docs/EXPLAINME.adoc is a pointer to the root EXPLAINME (WO 3.4). @@ -1041,7 +1039,10 @@ "docs/EXPLAINME.adoc" ".machine_readable/root-allow.txt" "Justfile" "scripts/run-proven-suite.sh" "tests/run_proven_suite_test.sh" "tests/proven_suite_test.sh" - ".github/workflows/actions.lock"))) + ".github/workflows/actions.lock" + "docs/theory/README.adoc" "verification/proofs/README.adoc" + "verification/proofs/agda/MANIFEST" "verification/proofs/coq/MANIFEST" + "verification/proofs/lean4/MANIFEST"))) ; provenance — what this repo was minted FROM. Written once, at mint, ; by build/just/repo-init.just. Tools that want "what is this repo" read ; the rest of the deed; tools that want "where did it come from" read this. diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index 5f6d77f9..c5d76f70 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -28,6 +28,7 @@ import {fileURLToPath, pathToFileURL} from 'node:url'; import path from 'node:path'; import {readJsonl} from '../atlas/census-atlas.mjs'; import {validateBridges, renderBridges} from './bridges.mjs'; +import {validateAdmissions, renderTheoryIndex} from './theory.mjs'; const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..'); const claimsFile = path.join(root, 'docs/atlas/claims/claims.jsonl'); @@ -35,6 +36,8 @@ const reposFile = path.join(root, 'docs/atlas/census/repos.jsonl'); const viewFile = path.join(root, 'docs/atlas/generated/registry.adoc'); const bridgesFile = path.join(root, 'docs/atlas/claims/bridges.jsonl'); const bridgesView = path.join(root, 'docs/atlas/generated/bridges.adoc'); +const admissionsFile = path.join(root, 'docs/theory/admissions.jsonl'); +const theoryView = path.join(root, 'docs/theory/generated/index.adoc'); const KINDS = new Set(['theorem', 'demonstration', 'assumption']); const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']); @@ -222,17 +225,18 @@ async function main() { const inventory = await readJsonl(reposFile); const rows = validate(await readJsonl(claimsFile), inventory); const bridges = validateBridges(await readJsonl(bridgesFile), inventory); + const admissions = validateAdmissions(await readJsonl(admissionsFile), rows, inventory); const derived = await deriveAll(rows, receiptsDir, await loadReader()); - const views = [[viewFile, render(derived)], [bridgesView, renderBridges(bridges)]]; + const views = [[viewFile, render(derived)], [bridgesView, renderBridges(bridges)], [theoryView, renderTheoryIndex(derived, admissions)]]; if (cmd === 'build') { - await mkdir(path.dirname(viewFile), {recursive: true}); + await Promise.all(views.map(([file]) => mkdir(path.dirname(file), {recursive: true}))); await Promise.all(views.map(([file, body]) => writeFile(file, body))); - console.log(`WROTE ${path.relative(root, viewFile)} (${rows.length} claims) and ${path.relative(root, bridgesView)} (${bridges.length} bridges)`); + console.log(`WROTE ${path.relative(root, viewFile)} (${rows.length} claims) and ${path.relative(root, bridgesView)} (${bridges.length} bridges) and ${path.relative(root, theoryView)} (${admissions.length} admissions)`); } else { const committed = await Promise.all(views.map(([file]) => readFile(file, 'utf8').catch(() => ''))); const stale = views.filter(([, body], i) => committed[i] !== body).map(([file]) => path.relative(root, file)); if (stale.length) throw new Error(`${stale.join(', ')} stale; run: bun scripts/registry/claims-registry.mjs build`); - console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); views match (${rows.length} claims, ${bridges.length} bridges)`); + console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); views match (${rows.length} claims, ${bridges.length} bridges, ${admissions.length} admissions)`); } } diff --git a/scripts/registry/theory.mjs b/scripts/registry/theory.mjs new file mode 100644 index 00000000..587ddd49 --- /dev/null +++ b/scripts/registry/theory.mjs @@ -0,0 +1,87 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// The theory shelf of Mathesis (re-anchoring plan WO 4.1). +// +// docs/theory/admissions.jsonl holds one authored admission record for each +// theorem whose home is Mathesis. A theorem enters the shelf only when the +// admission rule of docs/theory/README.adoc holds: it is theory by the test of +// PROOF-POLICY §1, no single system owns it, and an estate rule, vocabulary or +// interface depends on it. The record states each condition and names the +// dependant. It holds no grade: claims-registry.mjs derives the grade from the +// receipt and renders docs/theory/generated/index.adoc from both. + +export const HOME = 'hyperpolymath/mathesis'; +const FIELDS = new Set(['id', 'admitted', 'theory', 'owner', 'dependant']); +const DEPENDANT_FIELDS = new Set(['repository', 'path', 'rule']); + +const text = v => typeof v === 'string' && v.trim() !== ''; + +// Throw `message` unless `ok`. +const need = (ok, message) => { + if (!ok) throw new Error(message); +}; + +// Throw unless every admission is well formed, names a public dependant, and +// matches one home theorem pin; and unless every home theorem pin has one +// admission. `rows` are the validated claim pins. +export function validateAdmissions(admissions, rows, inventory) { + need(Array.isArray(admissions), 'docs/theory/admissions.jsonl must hold one admission record on each line'); + const visibility = new Map(inventory.map(r => [r.full_name, r.visibility])); + const home = new Map(rows.filter(r => r.repo === HOME && r.kind === 'theorem').map(r => [r.id, r])); + const seen = new Set(); + admissions.forEach((a, i) => { + const where = `admission ${i + 1}`; + for (const k of Object.keys(a)) need(FIELDS.has(k), `Unknown field (an admission holds no grade) ${k}: ${where}`); + need(home.has(a.id), `No home theorem pin for ${a.id}: ${where}`); + need(!seen.has(a.id), `Duplicate admission ${a.id}`); + seen.add(a.id); + need(typeof a.admitted === 'string' && /^\d{4}-\d{2}-\d{2}$/.test(a.admitted), `admitted is a date: ${a.id}`); + need(text(a.theory), `Missing theory test: ${a.id}`); + need(text(a.owner), `Missing owner test: ${a.id}`); + const d = a.dependant; + need(d !== null && typeof d === 'object', `Missing dependant: ${a.id}`); + for (const k of Object.keys(d)) need(DEPENDANT_FIELDS.has(k), `Unknown dependant field ${k}: ${a.id}`); + need(visibility.get(d.repository) === 'public', `Nonpublic or unlisted dependant repository: ${a.id}`); + need(text(d.path) && text(d.rule), `The dependant names a path and a rule: ${a.id}`); + }); + for (const id of home.keys()) need(seen.has(id), `Home theorem ${id} has no admission record`); + return admissions; +} + +const cell = s => String(s).replaceAll('|', String.raw`\|`).replaceAll('\n', ' '); + +// Render the theorem index from the derived registry rows of the home +// theorems and their admissions. +export function renderTheoryIndex(derived, admissions) { + const byId = new Map(admissions.map(a => [a.id, a])); + const home = derived.filter(d => d.row.repo === HOME && d.row.kind === 'theorem') + .sort((a, b) => a.row.claim.localeCompare(b.row.claim, 'en', {numeric: true})); + const out = [ + '// SPDX-License-Identifier: CC-BY-SA-4.0', + '// GENERATED by scripts/registry/claims-registry.mjs from docs/theory/admissions.jsonl,', + '// docs/atlas/claims/claims.jsonl and the receipt they pin; do not hand-edit.', + '= Theorem index of the theory shelf', + '', + 'One row for each theorem whose home is Mathesis. The grade is derived from', + 'the receipt by the canon reader, never typed. The admission rule is in', + 'link:../README.adoc[the theory README].', + '', + `Theorems: ${home.length}.`, + '', + '[cols="1,3,1,2,3",options="header"]', + '|===', + '|Theorem |Statement |PWG |Source and receipt |Dependant', + '', + ]; + for (const d of home) { + const r = d.row; + const a = byId.get(r.id); + const names = r.agda ? `\`${cell(r.agda.module)}\`: ${r.agda.names.map(n => '`' + cell(n) + '`').join(', ')}` : '-'; + const receipt = r.receipt ? `\`${cell(r.receipt.path)}\` at \`${r.source_commit.slice(0, 12)}\`` : 'no receipt'; + const dep = `https://github.com/${a.dependant.repository}/blob/main/${a.dependant.path}[${cell(a.dependant.repository)}]: ${cell(a.dependant.rule)}`; + out.push(`|${r.claim} |${cell(r.statement)} |\`${d.pwg}\` |${names}; ${receipt} |${dep}`, ''); + } + out.push('|===', ''); + return out.join('\n'); +} diff --git a/tests/golden/check_controls_test.sh b/tests/golden/check_controls_test.sh index b6c8ca8f..b1443fa7 100644 --- a/tests/golden/check_controls_test.sh +++ b/tests/golden/check_controls_test.sh @@ -36,7 +36,7 @@ expect_fail "stale catalogue" "$d" test "a row that no census wrote" # A proof that does not check: a gated Agda module gains a type error. d=$(copy proof) -printf '\nbroken : Set\nbroken = Set\n' >> "$d/verification/proofs/agda/Properties.agda" -expect_fail "failing proof" "$d" check-proofs "Properties.agda" +printf '\nbroken : Set\nbroken = Set\n' >> "$d/verification/proofs/agda/FeatureReachability.agda" +expect_fail "failing proof" "$d" check-proofs "FeatureReachability.agda" exit "$fail" diff --git a/tests/registry/theory.test.mjs b/tests/registry/theory.test.mjs new file mode 100644 index 00000000..e520e615 --- /dev/null +++ b/tests/registry/theory.test.mjs @@ -0,0 +1,42 @@ +// SPDX-License-Identifier: MPL-2.0 +// The theory shelf (re-anchoring plan WO 4.1): admissions match the home +// theorem pins, name a public dependant, hold no grade; the index is +// deterministic. +import {test, expect} from 'bun:test'; +import {readFileSync} from 'node:fs'; +import {validateAdmissions, renderTheoryIndex, HOME} from '../../scripts/registry/theory.mjs'; +import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; + +const read = p => parseJsonl(readFileSync(new URL(p, import.meta.url), 'utf8')); +const rows = read('../../docs/atlas/claims/claims.jsonl'); +const inventory = read('../../docs/atlas/census/repos.jsonl'); +const admissions = read('../../docs/theory/admissions.jsonl'); +const [a] = admissions; + +test('the committed admissions match the home theorem pins', () => { + expect(validateAdmissions(admissions, rows, inventory)).toHaveLength(rows.filter(r => r.repo === HOME && r.kind === 'theorem').length); +}); + +test('validation fails closed', () => { + const bad = (list, msg) => expect(() => validateAdmissions(list, rows, inventory)).toThrow(msg); + bad([], /has no admission record/); + bad([a, a], /Duplicate admission/); + bad([{...a, pwg: 'PWG-1'}], /holds no grade/); + bad([{...a, id: 'hyperpolymath/mathesis#THY-99'}], /No home theorem pin/); + bad([{...a, admitted: 'today'}], /admitted is a date/); + bad([{...a, theory: ''}], /Missing theory test/); + bad([{...a, owner: ' '}], /Missing owner test/); + bad([{...a, dependant: {...a.dependant, repository: 'o/hidden'}}], /Nonpublic or unlisted dependant/); + bad([{...a, dependant: {...a.dependant, rule: ''}}], /names a path and a rule/); + bad([{...a, dependant: {...a.dependant, grade: 'x'}}], /Unknown dependant field/); +}); + +test('the index is deterministic and takes the grade from the derivation', () => { + const home = rows.filter(r => r.repo === HOME && r.kind === 'theorem'); + const derived = home.map(row => ({row, pwg: 'PWG-1', reasons: [], evidence: row.source_commit})); + const view = renderTheoryIndex(derived, admissions); + expect(renderTheoryIndex([...derived].reverse(), admissions)).toEqual(view); + expect(view).toContain('`PWG-1`'); + expect(renderTheoryIndex(derived.map(d => ({...d, pwg: 'ungraded'})), admissions)).toContain('`ungraded`'); + expect(view).toContain(`Theorems: ${home.length}.`); +}); diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index eb22d4c4..7b055c89 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -1,60 +1,37 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= Formal Verification Proofs += Formal verification proofs -This directory contains formal proofs organised by proof assistant. +The sources of the theorems whose home is Mathesis, one directory for each +prover. The admission rule and the theorem index are in +link:../../docs/theory/README.adoc[the theory shelf]. -== Directory Structure +[cols="1,3",options="header"] +|=== +|Path |Contents -[source] ----- -proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs (mandatory) -│ │ ├── Pointers.idr # Non-null pointer safety -│ │ ├── Layout.idr # Memory layout correctness -│ │ ├── Platform.idr # Platform type size proofs -│ │ ├── Foreign.idr # FFI return type proofs -│ │ └── Compliance.idr # C ABI compliance -│ └── Types.idr # Core data type well-formedness -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── ApiTypes.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── Properties.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── TypeSafety.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── StateMachine.tla ----- +|`agda/` +|The Agda source of truth (PROOF-POLICY §1) -== Verification Commands +|`coq/` +|The Rocq re-proofs -[source,bash] ----- -just proof-check-all # Run all proof checkers -just proof-check-idris2 # Idris2 only -just proof-check-lean4 # Lean4 only -just proof-check-agda # Agda only -just proof-check-coq # Coq only ----- +|`lean4/` +|The Lean re-proofs -== Banned Patterns +|`/MANIFEST` +|The modules that the proof gate checks (`gated`) +|=== -The following MUST NOT appear in any proof file: +== Checking -- `believe_me` (Idris2) -- `assert_total` (Idris2) -- `postulate` (Idris2/Agda) -- `sorry` (Lean4) -- `Admitted` (Coq) -- `unsafeCoerce` (Haskell) +`scripts/check-proofs.sh ` compiles each gated module and then audits +its axioms. CI runs it in the pinned Guix shell through `just check-proofs`: -CI enforces this via `panic-attack assail --proofs-only`. - -== Adding New Proofs +[source,bash] +---- +guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check-proofs +---- -1. Choose the appropriate prover (see PROOF-NEEDS.md) -2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory -3. Ensure `%default total` (Idris2) or equivalent -4. Run the verification command -5. Update PROOF-STATUS.md +The template example proofs (Idris2, TLA+ and one example each for Agda, +Rocq and Lean) were removed in WO 4.1 of the re-anchoring plan. diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST index 3bb613a5..16863dbd 100644 --- a/verification/proofs/agda/MANIFEST +++ b/verification/proofs/agda/MANIFEST @@ -1,5 +1,4 @@ # Agda proof manifest — read by scripts/check-proofs.sh agda # Format: ||gated|quarantine| # Prior check (2026-07-17): agda --safe only; full 2026-11 policy pending CI. -verification/proofs/agda|Properties.agda|gated| template examples on Agda.Builtin only, no library (2026-11-10); passes the canonical invocation verification/proofs/agda|FeatureReachability.agda|gated| additive features: reachability monotone in the requested set (no library imports) diff --git a/verification/proofs/agda/Properties.agda b/verification/proofs/agda/Properties.agda deleted file mode 100644 index f3677b51..00000000 --- a/verification/proofs/agda/Properties.agda +++ /dev/null @@ -1,55 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Agda Proof Template: Inductive and coinductive properties --- Replace with your project's domain-specific proofs. --- All proofs must be total (no postulate, no {-# TERMINATING #-}). --- --- No library imports: only the Agda.Builtin modules that ship with Agda. --- The agda-stdlib 2.3 package of the pinned Guix does not build (re-anchoring --- plan WO 1.4, owner ruling 2026-11-10), and these examples need little of it. - -module Properties where - -open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) -open import Agda.Builtin.List using (List; []; _∷_) -open import Agda.Builtin.Equality using (_≡_; refl) - -cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y -cong f refl = refl - -length : ∀ {A : Set} → List A → Nat -length [] = zero -length (_ ∷ xs) = suc (length xs) - -_++_ : ∀ {A : Set} → List A → List A → List A -[] ++ ys = ys -(x ∷ xs) ++ ys = x ∷ (xs ++ ys) - -data _≤_ : Nat → Nat → Set where - z≤n : ∀ {n} → zero ≤ n - s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n - --- Example: Proof that list append preserves total length --- Replace with your project's domain proofs. - -append-length : ∀ {A : Set} (xs ys : List A) → - length (xs ++ ys) ≡ length xs + length ys -append-length [] ys = refl -append-length (_ ∷ xs) ys = cong suc (append-length xs ys) - --- Example: Monotonicity proof template --- Use for state machines, confidence scores, trust levels -record Monotone {A : Set} (_≤A_ : A → A → Set) (f : A → A) : Set where - field - preserves : ∀ {x y} → x ≤A y → f x ≤A f y - --- Example: Idempotence proof template --- Use for normalisation, deduplication, formatting -record Idempotent {A : Set} (_≡A_ : A → A → Set) (f : A → A) : Set where - field - idem : ∀ (x : A) → f (f x) ≡A f x - --- Example: Natural number successor is monotone -suc-monotone : Monotone _≤_ suc -suc-monotone = record { preserves = s≤s } diff --git a/verification/proofs/coq/MANIFEST b/verification/proofs/coq/MANIFEST index d9567b65..f9e003f3 100644 --- a/verification/proofs/coq/MANIFEST +++ b/verification/proofs/coq/MANIFEST @@ -1,5 +1,4 @@ # Coq proof manifest — read by scripts/check-proofs.sh coq # Format: ||gated|quarantine| # Ground-truthed 2026-07-17 with coqc. -verification/proofs/coq|TypeSafety.v|gated| compiles under `coqc` verification/proofs/coq|FeatureReachability.v|gated| THY-1 Rocq leg, re-proved; prelude only; Print Assumptions: closed diff --git a/verification/proofs/coq/TypeSafety.v b/verification/proofs/coq/TypeSafety.v deleted file mode 100644 index 8f5b4189..00000000 --- a/verification/proofs/coq/TypeSafety.v +++ /dev/null @@ -1,73 +0,0 @@ -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* - Coq Proof Template: Type system soundness - Replace with your project's type system proofs. - All proofs must be complete — NO Admitted allowed. -*) - -Require Import Coq.Lists.List. -Require Import Coq.Arith.Arith. -Require Import Coq.Bool.Bool. -Import ListNotations. - -(** * Example: Simple expression language with type safety *) -(** Replace this entire section with your project's type system. *) - -(** Types *) -Inductive ty : Type := - | TyNat : ty - | TyBool : ty. - -(** Expressions *) -Inductive expr : Type := - | EConst : nat -> expr - | ETrue : expr - | EFalse : expr - | EPlus : expr -> expr -> expr - | EEq : expr -> expr -> expr. - -(** Values *) -Inductive value : Type := - | VNat : nat -> value - | VBool : bool -> value. - -(** Typing relation *) -Inductive has_type : expr -> ty -> Prop := - | T_Const : forall n, has_type (EConst n) TyNat - | T_True : has_type ETrue TyBool - | T_False : has_type EFalse TyBool - | T_Plus : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EPlus e1 e2) TyNat - | T_Eq : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EEq e1 e2) TyBool. - -(** Evaluation *) -Inductive eval : expr -> value -> Prop := - | E_Const : forall n, eval (EConst n) (VNat n) - | E_True : eval ETrue (VBool true) - | E_False : eval EFalse (VBool false) - | E_Plus : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EPlus e1 e2) (VNat (n1 + n2)) - | E_Eq : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)). - -(** Value typing *) -Definition value_has_type (v : value) (t : ty) : Prop := - match v, t with - | VNat _, TyNat => True - | VBool _, TyBool => True - | _, _ => False - end. - -(** Type soundness: well-typed expressions evaluate to well-typed values *) -Theorem type_soundness : forall e t v, - has_type e t -> eval e v -> value_has_type v t. -Proof. - intros e t v Htype Heval. - induction Htype; inversion Heval; subst; simpl; auto. -Qed. diff --git a/verification/proofs/idris2/ABI/Compliance.idr b/verification/proofs/idris2/ABI/Compliance.idr deleted file mode 100644 index ee5efdd1..00000000 --- a/verification/proofs/idris2/ABI/Compliance.idr +++ /dev/null @@ -1,41 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: C ABI compliance --- Proves that struct layouts are C ABI compliant. --- All proofs MUST be constructive and total; proof escape hatches are forbidden. - -module ABI.Compliance - -import ABI.Layout -import ABI.Platform - -%default total - -||| Evidence that every field in a layout is correctly aligned. -public export -data AllFieldsAligned : List StructField -> Type where - AFANil : AllFieldsAligned [] - AFACons : FieldAligned f -> AllFieldsAligned fs -> AllFieldsAligned (f :: fs) - -||| Evidence that every field is within the struct bounds. -public export -data AllFieldsInBounds : (size : Nat) -> List StructField -> Type where - AFBNil : AllFieldsInBounds size [] - AFBCons : FieldInBounds size f -> AllFieldsInBounds size fs -> AllFieldsInBounds size (f :: fs) - -||| A struct layout is C ABI compliant when: -||| 1. All fields are aligned to their natural alignment -||| 2. All fields are within bounds of the struct size -||| 3. The struct size is a multiple of the struct alignment -public export -record CABICompliant (layout : StructLayout) where - constructor MkCompliant - fieldsAligned : AllFieldsAligned (layoutFields layout) - fieldsInBounds : AllFieldsInBounds (layoutSize layout) (layoutFields layout) - sizeAligned : modNatNZ (layoutSize layout) (layoutAlignment layout) SIsNonZero = 0 - -||| An empty struct is trivially compliant (size=1, alignment=1). -export -emptyStructCompliant : CABICompliant (MkLayout "empty" [] 1 1) -emptyStructCompliant = MkCompliant AFANil AFBNil Refl diff --git a/verification/proofs/idris2/ABI/Foreign.idr b/verification/proofs/idris2/ABI/Foreign.idr deleted file mode 100644 index 6c83435f..00000000 --- a/verification/proofs/idris2/ABI/Foreign.idr +++ /dev/null @@ -1,53 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: FFI function return type proofs --- Proves that all FFI functions return expected types. --- All proofs MUST be constructive and total; proof escape hatches are forbidden. - -module ABI.Foreign - -%default total - -||| Result type for FFI operations. -||| All FFI functions must return through this type. -public export -data FFIResult : Type -> Type where - FFISuccess : (value : a) -> FFIResult a - FFIError : (code : Int) -> (msg : String) -> FFIResult a - -||| Proof that FFIResult is a functor (map preserves structure). -export -mapFFIResult : (a -> b) -> FFIResult a -> FFIResult b -mapFFIResult f (FFISuccess value) = FFISuccess (f value) -mapFFIResult f (FFIError code msg) = FFIError code msg - -||| Proof that mapping identity preserves the result. -export -mapIdPreserves : (r : FFIResult a) -> mapFFIResult Prelude.id r = r -mapIdPreserves (FFISuccess value) = Refl -mapIdPreserves (FFIError code msg) = Refl - -||| An FFI function specification: name, argument types, return type. -public export -record FFISpec where - constructor MkFFISpec - ffiName : String - ffiReturnType : Type - -||| Proof that an FFI spec has a specific return type. -||| Use this to verify at compile time that FFI functions return the -||| types we expect across the C ABI boundary. -public export -FFIReturns : FFISpec -> Type -> Type -FFIReturns spec ty = ffiReturnType spec = ty - -||| C calling convention marker. -||| Proofs about calling convention compatibility. -public export -data CallingConv = CDecl | StdCall | FastCall - -||| All hyperpolymath FFI uses CDecl. -public export -defaultCallingConv : CallingConv -defaultCallingConv = CDecl diff --git a/verification/proofs/idris2/ABI/Layout.idr b/verification/proofs/idris2/ABI/Layout.idr deleted file mode 100644 index f0935aeb..00000000 --- a/verification/proofs/idris2/ABI/Layout.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Memory layout correctness --- Proves struct size, alignment, and padding properties. --- All proofs MUST be constructive and total; proof escape hatches are forbidden. - -module ABI.Layout - -%default total - -||| Witness that a type has a known size in bytes at compile time. -public export -interface HasSize (ty : Type) where - sizeOf : Nat - -||| Witness that a type has a known alignment in bytes. -public export -interface HasAlignment (ty : Type) where - alignOf : Nat - -||| Calculate padding needed to reach the next aligned offset. -||| paddingFor offset alignment = bytes to add so (offset + padding) `mod` alignment == 0 -public export -paddingFor : (offset : Nat) -> (alignment : Nat) -> {auto 0 ok : NonZero alignment} -> Nat -paddingFor offset alignment = let r = modNatNZ offset alignment ok - in case r of - Z => Z - (S _) => minus alignment r - -||| Proof that an offset with zero remainder needs zero padding. -export -alignedNeedsPadding : (n : Nat) -> (a : Nat) -> {auto 0 ok : NonZero a} -> - modNatNZ n a ok = 0 -> paddingFor n a = 0 -alignedNeedsPadding n a prf = rewrite prf in Refl - -||| A field within a struct, carrying its offset and size. -public export -record StructField where - constructor MkField - fieldName : String - fieldOffset : Nat - fieldSize : Nat - fieldAlignment : Nat - -||| Proof that a field is correctly aligned within a struct. -public export -FieldAligned : StructField -> Type -FieldAligned f = modNatNZ (fieldOffset f) (fieldAlignment f) SIsNonZero = 0 - -||| Proof that a field does not overflow past a given struct size. -public export -FieldInBounds : (structSize : Nat) -> StructField -> Type -FieldInBounds sz f = LTE (fieldOffset f + fieldSize f) sz - -||| A struct layout is a list of fields with a total size. -public export -record StructLayout where - constructor MkLayout - layoutName : String - layoutFields : List StructField - layoutSize : Nat - layoutAlignment : Nat diff --git a/verification/proofs/idris2/ABI/Platform.idr b/verification/proofs/idris2/ABI/Platform.idr deleted file mode 100644 index 0b5ab107..00000000 --- a/verification/proofs/idris2/ABI/Platform.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Platform-specific type size proofs --- Proves that C type sizes are correct per platform. --- All proofs MUST be constructive and total; proof escape hatches are forbidden. - -module ABI.Platform - -%default total - -||| Supported target platforms for ABI verification. -public export -data Platform = Linux64 | LinuxARM64 | MacOS64 | MacOSARM64 - | Windows64 | FreeBSD64 | WASM32 - -||| Pointer size in bytes for each platform. -public export -ptrSize : Platform -> Nat -ptrSize WASM32 = 4 -ptrSize _ = 8 - -||| C `int` size in bytes. -public export -cIntSize : Platform -> Nat -cIntSize _ = 4 - -||| C `size_t` size in bytes (matches pointer size). -public export -cSizeT : Platform -> Nat -cSizeT = ptrSize - -||| Proof that size_t always equals pointer size on all platforms. -export -sizeTEqPtrSize : (p : Platform) -> cSizeT p = ptrSize p -sizeTEqPtrSize _ = Refl - -||| Proof that pointer size is always 4 or 8 bytes. -export -ptrSizeValid : (p : Platform) -> Either (ptrSize p = 4) (ptrSize p = 8) -ptrSizeValid WASM32 = Left Refl -ptrSizeValid Linux64 = Right Refl -ptrSizeValid LinuxARM64 = Right Refl -ptrSizeValid MacOS64 = Right Refl -ptrSizeValid MacOSARM64 = Right Refl -ptrSizeValid Windows64 = Right Refl -ptrSizeValid FreeBSD64 = Right Refl - -||| Proof that C int is always 4 bytes on all platforms. -export -cIntAlways4 : (p : Platform) -> cIntSize p = 4 -cIntAlways4 _ = Refl - -||| Proof that pointer size is always at least 4 bytes. -export -ptrSizeAtLeast4 : (p : Platform) -> LTE 4 (ptrSize p) -ptrSizeAtLeast4 WASM32 = lteRefl -ptrSizeAtLeast4 Linux64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 LinuxARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOS64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOSARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 Windows64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 FreeBSD64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) diff --git a/verification/proofs/idris2/ABI/Pointers.idr b/verification/proofs/idris2/ABI/Pointers.idr deleted file mode 100644 index 310c4849..00000000 --- a/verification/proofs/idris2/ABI/Pointers.idr +++ /dev/null @@ -1,52 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Non-null pointer safety --- Template proof — customise for your project's pointer types. --- All proofs MUST be constructive and total; proof escape hatches are forbidden. - -module ABI.Pointers - -import Data.So - -%default total - -||| A pointer value that has been proven non-null. -||| The `So` constraint carries a compile-time witness that `ptr /= 0`. -public export -record SafePtr where - constructor MkSafePtr - ptr : Bits64 - {auto 0 nonNull : So (ptr /= 0)} - -||| Proof that SafePtr can never hold a null (zero) value. -||| This is enforced by the `So` constraint in the record. -export -safePtrNeverNull : (sp : SafePtr) -> So (sp.ptr /= 0) -safePtrNeverNull sp = sp.nonNull - -||| Wrap a raw pointer with a runtime null check. -||| Returns Nothing if the pointer is null. -export -checkPtr : (raw : Bits64) -> Maybe SafePtr -checkPtr 0 = Nothing -checkPtr raw = case choose (raw /= 0) of - Left prf => Just (MkSafePtr raw) - Right _ => Nothing - -||| Proof that checkPtr 0 always returns Nothing. -export -checkPtrZeroIsNothing : checkPtr 0 = Nothing -checkPtrZeroIsNothing = Refl - -||| An opaque handle backed by a non-null pointer. -||| Use this for FFI resource handles (file descriptors, sockets, etc.). -public export -record Handle (tag : String) where - constructor MkHandle - safePtr : SafePtr - -||| Proof that two handles with equal pointers are equal. -export -handlePtrEq : (h1, h2 : Handle tag) -> h1.safePtr.ptr = h2.safePtr.ptr -> h1 = h2 -handlePtrEq (MkHandle (MkSafePtr p)) (MkHandle (MkSafePtr p)) Refl = Refl diff --git a/verification/proofs/idris2/MANIFEST b/verification/proofs/idris2/MANIFEST deleted file mode 100644 index 867d0d03..00000000 --- a/verification/proofs/idris2/MANIFEST +++ /dev/null @@ -1,11 +0,0 @@ -# Idris2 proof manifest — read by scripts/check-proofs.sh idris2 -# Format: ||gated|quarantine| -# gated = must compile. quarantine = known-broken, must keep failing. -# Ground-truthed 2026-07-17 with idris2 0.7.0 (developer/tools/opt/pack). -# Types.idr re-checked with idris2 0.8.0: it compiles, so it is gated. -verification/proofs/idris2|ABI/Foreign.idr|gated| compiles — real content, not a stub -verification/proofs/idris2|Types.idr|gated| compiles under idris2 0.8.0 (imports Data.Nat); a template type, not a proof obligation -verification/proofs/idris2|ABI/Layout.idr|quarantine| Undefined name NonZero (needs Data.Nat); then a genuine unification failure (S ?x vs f .fieldAlignment) -verification/proofs/idris2|ABI/Platform.idr|quarantine| Undefined name LTE (needs Data.Nat); then Undefined name lteRefl -verification/proofs/idris2|ABI/Pointers.idr|quarantine| .nonNull declared at quantity 0 (erased) yet projected into a value position, plus a unification failure — design decision, not a typo -verification/proofs/idris2|ABI/Compliance.idr|quarantine| depends on quarantined ABI.Layout / ABI.Platform diff --git a/verification/proofs/idris2/Types.idr b/verification/proofs/idris2/Types.idr deleted file mode 100644 index e89a852f..00000000 --- a/verification/proofs/idris2/Types.idr +++ /dev/null @@ -1,40 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- Typing Proof: Core data type well-formedness --- Template — replace with your project's core types. --- All proofs MUST be constructive and total; proof escape hatches are forbidden. - -module Types - -import Data.Nat - -%default total - -||| Example: A bounded natural number (0 to max). -||| Replace with your project's core types. -public export -record Bounded (max : Nat) where - constructor MkBounded - value : Nat - {auto inBounds : LTE value max} - -||| Proof that a Bounded value is always <= max. -export -boundedLeMax : (b : Bounded max) -> LTE b.value max -boundedLeMax b = b.inBounds - -||| Proof that zero is always a valid Bounded value. -export -zeroIsBounded : {max : Nat} -> Bounded (S max) -zeroIsBounded = MkBounded 0 - -||| Example: A non-empty list with a compile-time guarantee. -public export -data NonEmpty : List a -> Type where - IsNonEmpty : NonEmpty (x :: xs) - -||| Proof that cons always produces a non-empty list. -export -consIsNonEmpty : (x : a) -> (xs : List a) -> NonEmpty (x :: xs) -consIsNonEmpty _ _ = IsNonEmpty diff --git a/verification/proofs/lean4/ApiTypes.lean b/verification/proofs/lean4/ApiTypes.lean deleted file mode 100644 index 8997f2b6..00000000 --- a/verification/proofs/lean4/ApiTypes.lean +++ /dev/null @@ -1,42 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Typing Proof: Public API type safety --- Template — replace with your project's API types. --- Proves properties about exported function signatures. - --- Example: Result type used across API boundaries -inductive ApiResult (α : Type) where - | ok : α → ApiResult α - | error : Nat → String → ApiResult α - -namespace ApiResult - -- Proof: map preserves structure (functor law: map id = id) - def map (f : α → β) : ApiResult α → ApiResult β - | .ok v => .ok (f v) - | .error c m => .error c m - - -- By `rfl` after `cases`: under Lean 4.29.0 `simp [map]` brings in `propext`. - theorem map_id : ∀ (r : ApiResult α), map id r = r := by - intro r - cases r <;> rfl - - -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f) - theorem map_comp (f : α → β) (g : β → γ) : - ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by - intro r - cases r <;> rfl -end ApiResult - --- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000) --- Replace with your project's numeric invariants -structure BoundedNat (max : Nat) where - val : Nat - le_max : val ≤ max - -theorem bounded_nat_le {max : Nat} (b : BoundedNat max) : b.val ≤ max := - b.le_max - --- Proof: zero is always bounded -def zeroBounded {max : Nat} (h : 0 < max) : BoundedNat max := - ⟨0, Nat.zero_le max⟩ diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST index 5708f1b4..aa66f7ae 100644 --- a/verification/proofs/lean4/MANIFEST +++ b/verification/proofs/lean4/MANIFEST @@ -1,5 +1,4 @@ # Lean4 proof manifest — read by scripts/check-proofs.sh lean4 # Format: ||gated|quarantine| # Ground-truthed 2026-07-17 with Lean leanprover/lean4:v4.15.0 (via elan). -verification/proofs/lean4|ApiTypes.lean|gated| compiles under Lean 4.29.0 (2026-11-10, axiom audit: none); both laws by rfl, because simp brings in propext under 4.29.0; not rechecked under 4.15.0 since that change verification/proofs/lean4|FeatureReachability.lean|gated| THY-1 Lean leg, re-proved; core only; #print axioms: none diff --git a/verification/proofs/tlaplus/StateMachine.tla b/verification/proofs/tlaplus/StateMachine.tla deleted file mode 100644 index f3484947..00000000 --- a/verification/proofs/tlaplus/StateMachine.tla +++ /dev/null @@ -1,91 +0,0 @@ ---------------------------- MODULE StateMachine ---------------------------- -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* *) -(* TLA+ Specification Template: State Machine *) -(* Replace with your project's distributed protocol or state machine. *) -(* Use TLC model checker to verify properties. *) -(* *) -(* Example: A simple request pipeline with safety properties. *) -(* Replace States, Init, Next with your project's actual states. *) -(***************************************************************************) - -EXTENDS Naturals, Sequences, FiniteSets - -CONSTANTS - MaxRequests \* Upper bound on concurrent requests (for model checking) - -VARIABLES - state, \* Current pipeline state - processed, \* Number of processed requests - queue \* Request queue - -vars == <> - -\* Pipeline states — replace with your project's states -States == {"idle", "scanning", "routing", "dispatching", "done", "failed"} - -\* Valid transitions — replace with your project's transition rules -ValidTransition(from, to) == - \/ from = "idle" /\ to = "scanning" - \/ from = "scanning" /\ to = "routing" - \/ from = "scanning" /\ to = "failed" - \/ from = "routing" /\ to = "dispatching" - \/ from = "routing" /\ to = "failed" - \/ from = "dispatching" /\ to = "done" - \/ from = "dispatching" /\ to = "failed" - \/ from = "done" /\ to = "idle" - \/ from = "failed" /\ to = "idle" - -\* Initial state -Init == - /\ state = "idle" - /\ processed = 0 - /\ queue = <<>> - -\* Transition action -Transition(newState) == - /\ ValidTransition(state, newState) - /\ state' = newState - /\ IF newState = "done" - THEN processed' = processed + 1 - ELSE processed' = processed - /\ UNCHANGED queue - -\* Enqueue a request (only when idle or scanning) -Enqueue == - /\ state \in {"idle", "scanning"} - /\ Len(queue) < MaxRequests - /\ queue' = Append(queue, "request") - /\ UNCHANGED <> - -\* Next-state relation -Next == - \/ \E s \in States : Transition(s) - \/ Enqueue - -\* Fairness: the system must eventually process -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) - -\* ---- SAFETY PROPERTIES ---- - -\* State is always valid -TypeInvariant == state \in States - -\* Processed count never decreases (monotonicity) -ProcessedMonotonic == processed >= 0 - -\* Queue never exceeds max -QueueBounded == Len(queue) <= MaxRequests - -\* No impossible transitions (e.g., idle -> done) -NoSkipStates == - [][state' # state => - ValidTransition(state, state')]_state - -\* ---- LIVENESS PROPERTIES ---- - -\* Every request eventually completes or fails -EventualCompletion == <>(state = "done" \/ state = "failed") - -============================================================================