From d92c8ce119ce3f2e9c87551624c3db3f45e56f66 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:36:11 +0000 Subject: [PATCH 1/4] docs: proof review against PROOF-POLICY; proof ledger; plan correction Re-ran every prover that could be installed and judged each proof against metadatastician/standards 3-practice/PROOF-POLICY.adoc (9bdf864). - Add a proof ledger to docs/EXPLAINME.adoc in the standard's closed vocabulary: 15 obligations, 7 proven (all about models), 7 open, 1 argued. No theory theorem has a proof witness grade, because none has an Agda source. - Correct the stale Solo-core status in SOUNDNESS and PROOF-NEEDS: progress and preservation check under Idris2 0.7.0 and are total (local check; not yet CI-gated). - Correct the completion plan's proof route to the policy: theory in Agda with Rocq and Lean rechecks, engineering in Idris2 or a recorded section 4 exception. Add section 5.0, the verified per-repo results, holes H20 (Face.render_ty is not injective, observed on the built library), H21 (the Coq gate passes planted admits outside its cone) and H22 (the staged Agda is unchecked; check-proofs skips silently), new cross-repo items, and owner questions 16 to 19. doc-truthing and the soundness ledger gate pass; all four files render without warnings. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW --- docs/COMPLETION-PLAN.adoc | 107 ++++++++++++++++++++++---------- docs/EXPLAINME.adoc | 124 ++++++++++++++++++++++++++++++++++++++ docs/PROOF-NEEDS.adoc | 13 ++-- docs/SOUNDNESS.adoc | 9 ++- 4 files changed, 214 insertions(+), 39 deletions(-) diff --git a/docs/COMPLETION-PLAN.adoc b/docs/COMPLETION-PLAN.adoc index 66341247..b5b62dd6 100644 --- a/docs/COMPLETION-PLAN.adoc +++ b/docs/COMPLETION-PLAN.adoc @@ -23,6 +23,8 @@ Each claim carries one of these status labels: No claim is raised above the status the maps support. +*Revision 2026-11-09.* A proof review re-ran every prover that could be installed and judged each proof against `metadatastician/standards` `3-practice/PROOF-POLICY.adoc` (commit `9bdf864`). Section 5.0 records the result. The proof route in section 5 and workflow W7 were corrected to that policy, and holes H20 to H22 were added. + An adversarial review pass checked this plan against the maps, and its corrections are folded in. The session lead also reproduced four headline findings directly on the built compiler: H1 (the interpreter returns 2 for `g(5)` where WebAssembly returns 1), H4 (a non-exhaustive match type-checks and the compiled WebAssembly returns 0), H6 (`check` reports a borrow error on two #554 fixtures that `eval` runs into a runtime type error) and H8 (`total fn loop` type-checks). Proof claims about Idris2 artefacts stay at READ or DOC everywhere, because no survey agent could install idris2. The systemet repo was not checked out, so every theory-level claim attributed to it is unverified. == 1. Ground-truth snapshot @@ -101,17 +103,17 @@ Results were consistent, but they do not prove CI is green. | typed-wasm repo (`/home/user/typed-wasm`) | `cargo test` passes 197 (default features) or 209 (all features). Clippy is clean. All 6 examples build and verify. `tw build` silently stubs bodies it cannot lower (`twice(5)=0`, `parser.rs` ~L895) and the result is VERIFIED. No L5 index guard is emitted: `get_player_hp(0,150)` returns 0. Malformed `session` blocks are accepted. No capabilities carrier is emitted. `tests/e2e.sh` reports 47 passed with 8 skipped (idris2, zig, parser), which is a silent green. Codegen output does not export memory, so multi-module sharing is unexercised. -| L2, L13-imports and L15 sit behind `unstable-*` features, so the default `tw-verify` build skips them. An unknown carrier version returns `Ok(vec![])` (`verify.rs:880,967`). An unknown ownership byte decodes to Unrestricted. 33 Idris2 modules contain no escape hatches by grep (not built). The "ECHIDNA 10^5" and "88/88 parser tests" claims cannot be reproduced: `Parser.mjs` is absent and `src/parser/*.affine` does not parse. +| L2, L13-imports and L15 sit behind `unstable-*` features, so the default `tw-verify` build skips them. An unknown carrier version returns `Ok(vec![])` (`verify.rs:880,967`). An unknown ownership byte decodes to Unrestricted. The 33 Idris2 modules fail under Idris2 0.7.0 at one base-library API change (`Region.idr:179`); with that token adapted in a scratch copy all 33 build, the 13 reject fixtures fail as expected, and 269 table rows check. The pinned 0.8.0 build was not run. `verifierIsSound` is vacuous as a claim about the Rust verifier, because each `VerifierAccepts` constructor already holds the spec witness. `MkAttestation` is public, so attestations can be forged. `Proofs.idr` attests L11 and L12 as proven while `LEVEL-STATUS` calls them draft. The "ECHIDNA 10^5" and "88/88 parser tests" claims cannot be reproduced: `Parser.mjs` is absent and `src/parser/*.affine` does not parse. | No L8, L9, L14 or L16 carriers. No wasmtime gate adapter. No WasmCert tie-back. | Coq `formal/` (20 files) -| All files compile under Coq 8.18. 137 named lemmas are "Closed under the global context". There are 35 in-file closure reports. -| P3, F3 and F4 are true by construction. RealWasm uses unbounded `Z`, not i32. Compile and eval are hand re-implementations, with no extraction or link to `lib/*.ml`. The axiom gate checks only lemmas that have an explicit `Print Assumptions` (`QttSemiring.v` and `Siblings_Stated.v` have none). +| All 20 files compile under Coq 8.18. A generated `Print Assumptions` over all 137 assertions reports every one "Closed under the global context". There are no Admitted, axioms or parameters. The CI gate covers only the 35 printed theorems and their dependencies (96 of 137). A planted `Admitted` false lemma and a planted `Axiom False` outside that set both passed a replica of the gate (H21). The real `Face.render_ty` collides two types that the F-5 model proves distinct (H20). +| Design review per theorem: P3 `borrow_soundness`, F1 `f1_same_cube`, F3, F4 and `QttTyping.usage_soundness` hold by definition. K1, RealCompile, RealLoop, RealMem and RealWasm are sound about their models but the models differ from `lib/codegen.ml` (de Bruijn locals, unbounded `Z`, word addressing, no traps). P2, Rows and QttSemiring are meaningful theory, but not AffineScript's calculus. The full per-theorem table is the proof ledger in `docs/EXPLAINME.adoc`. CI pins Coq 8.20.1, which was not re-run. | No proofs of type soundness for the real type system, effects, inference or coherence. | Idris2 solo-core (`docs/academic/formal-verification/solo-core/*.idr`) -| — -| Hole-free and `%default total` by grep. Never type-checked. `docs/SOUNDNESS.adoc` and `docs/PROOF-NEEDS.adoc` §1 still say `?todo` (doc drift). +| Checks under Idris2 0.7.0 (built from source here): 8 modules, zero errors or warnings; `progress` and `preservation` report total. The stale `?todo` lines in `docs/SOUNDNESS.adoc` and `docs/PROOF-NEEDS.adoc` are corrected in the same change as this revision. +| `affinePreservation` repeats `preservation`. The calculus is the separate Solo model, not `lib/typecheck.ml`. It is a theory result held in Idris2, not Agda. | No CI gate was found in the survey pass. | Lean `docs/academic/tropical-session-types` @@ -120,18 +122,18 @@ Results were consistent, but they do not prove CI is green. | — | anytype (`/home/user/anytype`) -| An exhaustive Rust check of the transcribed Affine tables finds 0 law violations. -| Idris2 was not run. The 19-case golden matrix and 8 CLI cases were counted, not executed. The golden path is probably broken: `abi.ipkg` moved to `src/interface/abi.ipkg` in commit `7329ceb`, but the Justfile and `idris2-proof.yml` still point at the root. That breakage is inferred, not observed. +| An exhaustive Rust check of the transcribed Affine tables finds 0 law violations. Under Idris2 0.7.0 (its pin): the golden path is broken, observed: `idris2 --install abi.ipkg` fails with "File Not Found" because the file moved to `src/interface/abi.ipkg`. With the corrected path, the golden matrix passes 19/19, the CLI cases 8/8, and `check-idris2-proofs.sh` passes (15 gated, 5 quarantined). The Affine tables match `lib/quantity.ml` cell for cell (27 cells). +| The workflow's `paths: '*.ipkg'` filter does not match the moved file. The checker has no soundness theorem; it is TESTED by 27 cases. The Zig seam tests were not run (no zig). | No checker soundness theorem. No join, branching, ADTs, polymorphism, effects or `CostAlgebra`. | typell (`/home/user/typell`) | The workspace builds. 447 tests pass and 3 are ignored. `UsageQuantifier` is not lawful: monotonicity of + and *, distributivity and transitivity all fail. -| Idris `Soundness.idr` covers plain STLC only (not run). `tests/integration_test.rs` is never compiled. +| Idris `Soundness.idr` checks under Idris2 0.7.0 and covers plain STLC only; its header claims effects and let-polymorphism it does not have. Its proof gate reports 5 passes, but `Foreign.idr` is a false pass: Idris2 0.7.0 `--check` exits 0 when an import is missing (reproduced). `LevelMonotonicity` is vacuous. CI installs Idris2 with `nix shell nixpkgs#idris2`, unpinned and on a banned tool. `tests/integration_test.rs` is never compiled. | Not on the AffineScript critical path. | echo-types -| `All.agda` and `Smoke.agda` exit 0. The guardrails pass. There is 1 postulate block, outside `All.agda`. -| `PROOF-STATUS` claims about 200 modules. There are 94 imports, and 96 modules were checked. +| All 6 own lanes and the guardrails pass. Under the canonical `agda --safe --without-K --cubical-compatible`, all 5 non-cubical entrypoints pass cold (Agda 2.6.3, stdlib v2.3, absolute-zero `f486c29`); the `All` cone is 125 local modules. 11 of the 12 files outside every cone also compile; `EchoImageFactorizationPropPostulated` fails as designed. No escape in the cone. +| No recipe passes `--cubical-compatible` on the command line; file pragmas carry it in 131 of 137 files. The canonical flags do not stop the `--cubical` pragma, so the cubical island needs a reviewed profile. `PROOF-STATUS` overclaims ("`--safe --without-K` throughout", "≈200 modules", "every module wired") and still lists graded-comonad laws the repo has ruled out. `gcomonad-*`, `LEcho` and `no-section-weaken` hold only for `collapse : Bool → ⊤`. No grade is recorded; 8 headline theorems are eligible for `PWG-3` once a receipt is recorded. | A parametric `LEcho` over arbitrary drops. | tropical-types @@ -140,8 +142,8 @@ Results were consistent, but they do not prove CI is green. | — | occupancy, secret, residual-evidence, choreographic, epistemic -| All five `check.sh` gates pass, including their rejection fixtures. occupancy's stackcert `cert_sound` fails to compile under Lean 4.15 and depends on `sorryAx`. -| occupancy's Idris spike is not run. +| All five own gates pass, and every wired cone also passes the canonical flags cold, at Agda 2.6.3 (four of them pin 2.6.4.3, which was not installed). Rejection fixtures fail as intended: secret 2/2, epistemic 13/13, residual-evidence 9/9, occupancy 2/2, choreographic 5/5. No escape in any cone. +| secret-types' own `-W error` fails under the canonical flags unless `-W noUnsupportedIndexedMatch` is added. occupancy's Agda check is called by no workflow, Justfile recipe or script, and its R-6 row says PROVEN for two rejection fixtures (it is TESTED). The template Agda gate is broken in secret-types and occupancy (module name versus `include: src`). Lean was not re-run, so occupancy's `stackcert` remains unverified. No Rocq or Lean leg anywhere is `RECONCILED`, so nothing exceeds `PWG-3`, and no repo records a grade. | None of these has an AffineScript consumer. | jtv-halting-islands-ct @@ -150,13 +152,13 @@ Results were consistent, but they do not prove CI is green. | Parser, CLI and tests. | absolute-zero -| The 4 active Agda modules type-check. The Z3 OND checks pass. The archived Coq tree is 17/17 closed. `src/whitespace` has 1 failing test. -| Idris ABI not run; it contains `believe_me` at `Layout.idr:270`. In the Agda CNO, the termination and thermodynamic parts are vacuous. +| The 4 active Agda modules type-check, including under the canonical flags with stdlib 1.7.3 (its CI) and 2.3 (what echo-types uses). The Z3 OND checks pass. The archived Coq tree is 17/17 closed. `src/whitespace` has 1 failing test. +| The Idris ABI builds under Idris2 0.7.0 (the repo pins 0.8.0 through a pack image). It has five `believe_me`: `Layout.idr:270` and `Proofs/DivMod.idr:92,104,114,124`. All five statements are true and provable, so those rows are ASSUMED, not PROVEN. `HasSize` and `HasAlignment` carry no information, so the size and alignment claims are vacuous. `PROOF-STATUS` and `wiki/ABI.md` overclaim on both points. In the Agda CNO, the termination and thermodynamic parts are vacuous. | — | januskey | 135 tests pass. The Agda kernel and 4 reject fixtures pass against resource-algebra `cf9235c`. -| The Zig C ABI is a stub (`TODO(#155)`). T-8 is non-atomic. Idris was not run. +| The Idris ABI type-checks under Idris2 0.7.0 (4 modules) and its 3 reject fixtures fail as expected. `seqCNO` and `tamperBreaksLink` hold for the Idris model only, which the repo states honestly. The Zig C ABI is a stub (9 `TODO(#155)` sites). T-8 is non-atomic. | No AffineScript seam today. | stdlib and aLib @@ -218,6 +220,9 @@ All were observed by RUN unless marked otherwise. The maps confirm that H1–H4 . H17. The lexer accepts the bad escape `\q`, and an empty `match` parses (conformance invalid cases 010 and 011). . H18. The interpreter fails when dereferencing refs returned through calls ("Expected reference type"). The session lead reproduced this on two #554 fixtures. . H19 (typed-wasm). No L5 index guard: `get_player_hp(0,150)` reads an adjacent region. `where` constraints are discarded. Malformed `session` blocks are silently ignored. +. H20. `Face.render_ty` is not injective, contrary to the F-5 model. On the Js face `List[Option[Int]]` and `Option[List[Int]]` both render as `List[Int] | null`; on Cafe both render as `List[Int]?`. The greedy `Option\[\(.*\)\]` regex in `lib/face.ml` causes it (RUN, by calling the built library). +. H21. The Coq proof gate fails open on assertions outside the printed theorems' dependency cone. A planted `Admitted` false lemma and a planted `Axiom False` both passed a replica of `coq-proof-gate.yml` (RUN). The gate also never re-runs when the `lib/*.ml` files the models describe change. +. H22. The staged Agda under `proposals/` (23 files) passes under the canonical flags, but nothing checks it: `tools/check-proofs.sh --agda` reports SKIP, not failure, when `AFFINESCRIPT_ECHO_TYPES_DIR` or `AGDA_STDLIB` is unset, and no workflow or dune rule calls it. No echo-types commit is pinned. == 2. Target architecture @@ -601,6 +606,24 @@ $M compile x.affine -o x.lua; echo rc=$? # expect !=0 == 5. Fastest proof route (ordered by leverage on the shipped compiler) +=== 5.0 Alignment with the estate proof policy + +The governing rules are `metadatastician/standards` `3-practice/PROOF-POLICY.adoc`, read at commit `9bdf864`. + +* *Theory* means a statement true of any implementation, such as soundness of a calculus or semiring laws. Its source of truth is Agda, checked with exactly `agda --safe --without-K --cubical-compatible`, then rechecked in Rocq and in Lean, with no Mathlib. +* *Engineering* means a statement that names a type, function or wire format of one repository. It belongs in Idris2. First-party Rust uses Creusot with Pearlite and Verus. +* An existing Rocq proof of a theory statement counts only as that prover's leg, and only once an Agda source exists and the two statements have been compared and recorded (§3, §2.2). Until then the theorem is `ungraded` (§8.1). +* An existing engineering proof in another prover moves to Idris2 when it is next touched, unless a §4 exception is recorded beside it and in the proof-status file. + +What that means here: + +* *Theory files.* `QttSemiring`, `P2_Progress`, `P2_Stlc`, `Rows`, `AffineUsage`, `QttTyping`, `QttDynamic` and the Idris2 Solo core are theory. None has an Agda source, so every one is `ungraded`. The Coq files are `COQ-CHECKED` target-only evidence. +* *Engineering files.* `K1*`, `Real*`, `P3_*`, `F1` and `F3`–`F5` state properties of this repository's code. No §4 exception is recorded for them. The stated reason in `formal/README.adoc` (interop with typed-wasm and ephapax) is not one of §4's grounds. Question 16 asks the owner to choose. +* *Highest grade reachable in agent sandboxes.* Lean toolchains are downloadable from `releases.lean-lang.org` (4.13.0 and 4.15.0 return HTTP 200), but in this session the automatic permission check refused installing them as external code. Until the owner approves that install (question 19), a Lean leg is `unavailable` in agent sessions, and the best grade they can reach is `PWG-2i`: an Agda source plus a reconciled Rocq leg. +* *Oracles are not proofs.* Z3, Datalog and differential checks earn `TESTED` (with bounds) or `ASSUMED`. They never earn `PROVEN` without an independently checked certificate (§5). +* *Proof ledger.* The ledger now lives in `docs/EXPLAINME.adoc`. It has 15 obligations: 7 `proven` (all about models), 7 `open` and 1 `argued`. No theory theorem is at `PWG-3` or better. +* *Where the Agda sources live* is an owner decision (question 17). + Leverage means how much assurance a rung adds about the actual binary `main.exe` and its outputs, not about an idealised core. [cols="1,3,2,3,3",options="header"] @@ -621,7 +644,7 @@ Leverage means how much assurance a rung adds about the actual binary `main.exe` | P2 | Differential check of `Codegen` against an extracted, proved reference for the int/bool/let/if fragment. This is a test, not a theorem about `codegen.ml`. Method: extract Coq `RealCompile.compile`/`eval` and compare with `Codegen.gen_expr` on generated programs. -| Coq 8.18/8.20 + Extraction to OCaml +| Coq 8.18/8.20 + Extraction to OCaml. Engineering by policy: Idris2, or Coq under a recorded §4 exception (question 16). The comparison itself is `TESTED`. | RUN: the proofs exist and are axiom-free. The link is ABSENT. | Coq uses unbounded `Z`, word-addressed memory and depth-indexed locals. Real codegen uses i32 wrap, byte-addressed memory and name-keyed locals. Needs R-wrap first, and a decision on integer semantics. @@ -641,29 +664,29 @@ Leverage means how much assurance a rung adds about the actual binary `main.exe` | Non-tautological P-3: a separate ownership small-step semantics, the `borrow.ml` lexical rules as an inductive checker, and "accepts implies no stuck deref", including the interprocedural #554 shape. | Coq | ABSENT. The current one is a tautology. -| Hand transcription of a 2306-line pass. Re-validate via P4. +| Hand transcription of a 2306-line pass. Re-validate via P4. Prover: the ownership calculus and its soundness are theory, so Agda (rechecked in Rocq and Lean). The transcription of `borrow.ml` is engineering, so Idris2. | P6 -| Real QTT in Coq: `Q_App` scales by q; typed vars; let/pair/case. Agreement with `main.exe check` on the `affine_*` fixtures. -| Coq +| Real QTT: `Q_App` scales by q; typed vars; let/pair/case. Agreement with `main.exe check` on the `affine_*` fixtures (that agreement is `TESTED`). +| Agda (source), rechecked in Rocq and Lean. The existing Coq `QttTyping` is not a usable leg: it holds by definition. | Model only. `Q_App` lacks scaling. | `QttTyping` is an occurrence counter, not QTT. | P7 | Solo-core progress and preservation actually machine-checked. -| Idris2 -| READ (hole-free by grep). Not checked. -| Covers only the Solo fragment. Blocked on idris2 provisioning. +| Idris2 today; Agda needed for a grade +| RUN: checks under Idris2 0.7.0; `progress` and `preservation` total. Not run in CI. +| Covers only the Solo fragment. Theory held in Idris2, so `ungraded` until an Agda source exists. Add a CI job that also scans the output for errors, because `--check` exits 0 on a missing import. | P8 | Effect-row soundness for real inference (row variables), after H5 is fixed. -| Coq (extend `Rows.v`) +| Agda (source), rechecked in Rocq (extend `Rows.v` as that leg) and Lean | `Rows.v` is monomorphic. | Handlers are blocked on #555 and #623. Do not state P-6 handler soundness against a reference semantics known to be wrong. | P9 | Full verified compiler for the core fragment (CompCert/CakeML-style), or an extracted backend replacing `codegen.ml` for the core. -| Coq +| Engineering: Idris2, or Coq under a recorded §4 exception (question 16) | ABSENT. | Long-term. Only worth it once P1–P3 show the fragment is stable. |=== @@ -693,7 +716,7 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness |=== | Option | (a) | (b) | Notes -| A. Full verified compiler (Coq, then extracted backend for the core fragment). *Elegant default.* +| A. Full verified compiler (in Idris2 per PROOF-POLICY §1, or Coq under a recorded §4 exception), then an extracted backend for the core fragment. *Elegant default.* | 5 | 4 | The most final option. Requires stable core semantics, which do not exist yet (H1, H7, H9). Multi-year. @@ -740,7 +763,7 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness | D. Unconventional: make Polonius-style Datalog primary for borrows (via `borrow_extract.ml` and an external solver), with `borrow.ml` demoted to a fast pre-pass. | 3 | 4 -| A declarative spec is easier to model in Coq. Adds a toolchain dependency. +| A declarative spec is easier to state as theory in Agda. Adds a toolchain dependency. Solver results are `TESTED`, not `PROVEN`. |=== *Recommendation: B, then C, then A.* This departs from the default for the same reason: anytype cannot yet express AffineScript's branching usage. The join law must also be settled in systemet first, under extend-not-redefine. Typell is excluded: its algebra fails the laws (RUN). @@ -832,8 +855,11 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness * Fan-out: a single agent. apt is serialised, because parallel installs clobbered each other in the survey. * Scope: all repos, read-only. * Isolation: one container image snapshot, recorded so later workflows can reuse it. -* Gates: the M0 commands; `cd $TW && cargo test --workspace --all-features`; Coq gate `just -f $AS/formal/justfile check`; echo-types `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda`. -* Stop if: idris2 is still unavailable. Record it as an owner request and do not attempt a source bootstrap without approval; the survey's attempt was denied. +* Gates: the M0 commands; `cd $TW && cargo test --workspace --all-features`; Coq gate `just -f $AS/formal/justfile check` plus a generated `Print Assumptions` over every assertion; every Agda theory entrypoint under exactly `agda --safe --without-K --cubical-compatible`. +* Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, `make bootstrap SCHEME=chezscheme`, `make install PREFIX=/opt/idris2`. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, has not been built in a sandbox. +* Lean is downloadable from `releases.lean-lang.org`, but installing it needs owner approval (question 19); GitHub release downloads are blocked. Until then record every Lean leg as `unavailable`, never as passing. +* Treat an Idris2 `--check` exit code of 0 as a pass only when its output also contains no `Error:` line. +* Stop if: a pinned prover cannot be provisioned. Record the leg as unavailable and continue with the others. * Output: a versioned toolchain manifest, kept out of the repo root. *W1 Ledger the holes (understand + implement tests).* @@ -900,11 +926,12 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150 *W7 Proof bridges (implement + verify).* -* Goal: P2 (R-wrap, extraction test), P3 (`anytype_emit.ml` with the anytype or Z3 oracle), and gate hardening (auto `Print Assumptions`). -* Fan-out: three agents. -** Coq agent in `formal/`. +* Goal: bring the proof track into line with PROOF-POLICY (section 5.0), then P2 (R-wrap, extraction test), P3 (`anytype_emit.ml` with the anytype or Z3 oracle), and gate hardening. +* Fan-out: four agents. +** Agda theory agent: port `QttSemiring` first, then `P2_Stlc`, `Rows` and the Solo core, to Agda under the canonical flags, in the home question 17 settles. For each, record the Rocq leg's statement comparison so it can become `RECONCILED`. Re-prove the Lean leg by hand (no Mathlib) once question 19 is settled; until then record it as `unavailable`. +** Coq agent in `formal/`: close H21 first, and act on the engineering files as question 16 decides. ** OCaml emitter agent. -** anytype agent: fix the `abi.ipkg` path in the Justfile and `idris2-proof.yml`, and draft `gjoin`. The join is a systemet ADR draft only. +** anytype agent: fix the `abi.ipkg` path in the Justfile and `idris2-proof.yml`, and the workflow's `paths` filter. The corrected path already gives 19/19 golden and 8/8 CLI cases under Idris2 0.7.0. Draft `gjoin` as a systemet ADR only. * Gates: ** Generate `AllAssump.v` from a grep of every `Theorem|Lemma|Corollary|Example|Proposition|Fact|Remark` in `formal/*.v` and commit the generator. Then `coqc -Q . ASFormal AllAssump.v | grep -c 'Closed under'` must equal the generated line count. Add a negative test: an `Admitted` lemma in `QttSemiring.v` must fail the gate. ** `dune test` for extraction parity. @@ -968,6 +995,18 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150 * [ ] Owner: jtv-halting-islands-ct LICENSE placeholder. * [ ] Owner: the MAA draft expired on 2026-04-13 and has no SPDX header (no automated edit). Converting maa-framework's vendored absolute-zero to a submodule (typed-wasm ADR-0004) belongs in a maa-scoped session. * [ ] 007: confirm `twasm = TwasmBackendNotYetImplemented` (repo not checked out). +* [ ] anytype: the golden path is broken (observed). Point the Justfile and `idris2-proof.yml` at `src/interface/abi.ipkg`, and widen the workflow `paths` filter to match it. +* [ ] typell: `Foreign.idr` is a false pass in its proof gate; correct `PROOF-STATUS`. Make the gate fail on any `Error:` line. Replace the unpinned `nix shell nixpkgs#idris2` install. Correct the `Soundness.idr` header, which claims effects and let-polymorphism the calculus does not have. +* [ ] Estate-wide Agda: no repo's recipe or CI passes `--cubical-compatible` on the command line, as PROOF-POLICY §2.1 requires, and no repo records a §2.1 receipt or a grade. Re-run at each repo's pinned Agda (2.6.4.3 in four repos; this session had only 2.6.3). +* [ ] echo-types: correct `PROOF-STATUS` (module counts, wiring, the flag claim, the withdrawn graded-comonad framing); put the cubical island under a reviewed proof profile; wire `tutorial/All.agda` or drop the claim. +* [ ] occupancy-types: wire `scripts/check-agda.sh` into CI and `just`; move R-6 to TESTED. secret-types and occupancy-types: fix the template Agda gate. +* [ ] absolute-zero: most CNO lemmas are vacuous (`energy-dissipated` is constantly 0); only `cno-composition` and OND1–OND5 carry content. Record the stdlib pin, and mark the archived Coq and Lean sections as archived in `PROOF-STATUS`. +* [ ] januskey: T-1..T-3 are engineering statements proved in Agda with no §4 exception recorded. +* [ ] Estate-wide: Idris2 0.7.0 `--check` exits 0 when an import is missing. Every Idris2 gate in the estate that trusts only the exit code can pass falsely. This belongs in `standards` (a gate rule) and in each repo's check script. +* [ ] absolute-zero: discharge or name the five `believe_me` lemmas as axioms, give `HasSize` and `HasAlignment` real content, and correct `PROOF-STATUS` and `wiki/ABI.md`. +* [ ] typed-wasm: make `MkAttestation` private, reconcile `Proofs.idr` with `LEVEL-STATUS` on L11 and L12, refresh the stale `PROOF-NEEDS` module counts, and fix the e2e Idris job's 404 tarball URL. Confirm the `Region.idr` build under the pinned Idris2 0.8.0. +* [ ] Every repo above that installs a prover outside Guix or its container needs a PROOF-POLICY §6 deviation record. None has one (anytype's tarball has no digest check; typell's install is unpinned). +* [ ] mathesis: the catalogue rows for this plan's repos were refreshed with a new merge mode for the census, and these repos were added as reconciliation targets (mathesis PR). The theorem-level claims registry is still unbuilt there. * [ ] Issue trackers: update #563, #513, #553, #555, #601 and #623. These are outward-facing; confirm before posting. == 9. Open questions for the owner @@ -987,4 +1026,8 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150 . *Coq pin.* 8.18 (docs) or 8.20.1 (CI)? . *Toolchains.* Approve idris2 in sandboxes; without it, every Idris claim stays unverified. . *Node exemption.* Approve a Node runtime exemption for the dom and cadre e2e harnesses, or port them to Bun? +. *Coq engineering track.* Record a PROOF-POLICY §4 exception for the Coq engineering files (`K1*`, `Real*`, `P3_*`, `F*`), or move them to Idris2 when next touched? Policy's default is Idris2. +. *Home of the Agda theory sources.* AffineScript `formal/agda/`, anytype (beside its grade algebra), or mathesis (which may hold theory with no other natural home)? +. *Idris2 0.8.0.* Approve building Idris2 0.8.0 from source in agent sandboxes (typed-wasm's pin)? An attempt this session was refused by the session's automatic permission check. +. *Lean.* Approve installing pinned Lean toolchains from `releases.lean-lang.org` in agent sandboxes, with a digest recorded as a §6 deviation? The same check refused it this session. Without it, tropical-types and occupancy's `stackcert` cannot be re-checked and no Lean leg can count. . *Status documents.* Re-sign the AFFIRMATION files, and decide whether the stale ROADMAP (January 2026 baseline) is retired or rewritten. \ No newline at end of file diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index a3834751..1b5fa040 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -74,3 +74,127 @@ AffineScript validates the hyperpolymath ecosystem: | Lambda captures don't escape linear bound | `lib/borrow.ml` collect_free + Shared borrows | BUG-004 commit 48422d1 — manual smoke | TEA update param is linear (Wasm custom section) | `lib/tea_bridge.ml` build_ownership_section | `test/test_e2e.ml` test_bridge_update_msg_linear |=== + +[[proof-ledger]] +== Proof Ledger + +One row per proof obligation this repository speaks about, in the closed +vocabulary of `metadatastician/standards` `docs/README-EXPLAINME-STANDARD.adoc` +§5 (`proven`, `proven-with-postulates`, `argued`, `tested-only`, `open`). + +*Receipts.* Recorded on 2026-11-09 at commit `9167b04`: + +* *Coq rows.* Built with `coqc 8.18.0 -Q . ASFormal` in `formal/`, in the + justfile order, on OCaml 4.14.1. A generated `Print Assumptions` over all 137 + assertions reported every one "Closed under the global context". CI pins + Coq 8.20.1, which was not re-run here. +* *Idris2 row.* Checked with Idris2 0.7.0 (`idris2 --check Soundness.idr`). + The run produced zero errors and warnings, and `:total` reported + `progress` and `preservation` total. + +[cols="2,1,2,2,2", options="header"] +|=== +| Obligation | Status | Checker (version, flags) | Where | Trust boundary + +| Code-generation preservation, toy nat/bool compiler (K-1, K-1 with `let`) +| `proven` +| coqc 8.18.0 +| `formal/K1_CodegenPreservation.v:compile_correct`, `formal/K1Let_CodegenPreservation.v:compile_correct` +| A toy compiler and stack machine. Not `lib/codegen.ml`. + +| Code-generation forward simulation on a WASM-shaped model +| `proven` +| coqc 8.18.0 +| `formal/RealCompile.v:compile_correct`, `formal/RealLoop.v:compile_stmt_correct` +| A de Bruijn re-implementation, not `lib/codegen.ml` or `lib/interp.ml`. Integers are unbounded `Z`, not i32. Forward only, with nothing about traps or divergence. `RealLoop` covers let-free statements only. Its header's "observable difference is proved" has no matching theorem. + +| Memory and executor lemmas on the WASM model +| `proven` +| coqc 8.18.0 +| `formal/RealMem.v`, `formal/RealWasm.v` +| Fixed instruction sequences. Addressing is word-based, while codegen uses byte offsets. An out-of-range store is a no-op where WASM traps. + +| QTT `{0,1,ω}` semiring and order laws +| `proven` +| coqc 8.18.0 +| `formal/QttSemiring.v` +| Theory: no Agda source, so PROOF-POLICY gives it no proof witness grade (it is `ungraded`). The tables match `lib/quantity.ml` `q_add`/`q_mul` by inspection only. The CI gate does not cover 16 of the 21 laws. + +| QTT typing soundness for the real quantity checker +| `open` +| - +| `formal/QttTyping.v`, `formal/QttDynamic.v` +| `QttTyping` is an occurrence counter presented as a judgment. `Q_App` does not scale and `Q_Var` accepts any type. `QttDynamic` proves only a lambda-free scaling law and no subject reduction. + +| Progress and preservation, first-order and STLC (P-2) +| `proven` +| coqc 8.18.0 +| `formal/P2_Progress.v`, `formal/P2_Stlc.v` +| Theory, `ungraded`. Textbook STLC with no quantities or affinity, so it is not AffineScript's calculus. + +| Progress and preservation for monomorphic records +| `proven` +| coqc 8.18.0 +| `formal/Rows.v` +| Theory, `ungraded`. Rows are ordered lists with no row variables. This is not the effect-row system. + +| Solo core progress and preservation +| `proven` +| Idris2 0.7.0, `%default total` +| `docs/academic/formal-verification/solo-core/Soundness.idr:progress`, `:preservation` +| A separate Solo model, not `lib/typecheck.ml` or `lib/borrow.ml`. No CI job runs it. It is a theory statement held in Idris2 rather than Agda, so it is `ungraded`. + +| Borrow checker soundness (`lib/borrow.ml`) +| `open` +| - +| `formal/P3_BorrowSound.v`, `formal/P3_BorrowGraph.v` +| `borrow_soundness` holds by definition: `borrow_ok` is defined as the negation of the dynamic oracle it is compared against. `rejects_554` and `move_locality` are proven but small. + +| Face transformer preserves evaluation (F-1) +| `open` +| - +| `formal/F1_TransformerPreservation.v` +| The model is an invented AST elaborator, while the real faces rewrite text line by line (`lib/python_face.ml`). `f1_same_cube` is congruence. + +| Face pragma detection is local and functional (F-3) +| `open` +| - +| `formal/F3_PragmaDecidable.v` +| Both theorems hold for any function and by definition. The real scan limits in `lib/face_pragma.ml` are not modelled. + +| Face error rendering is faithful (F-4) +| `open` +| - +| `formal/F4_ErrorFaithful.v` +| `render` is defined to copy the fields it is claimed to preserve. `lib/face.ml` formatting is not modelled. + +| Face type rendering is injective (F-5) +| `open` +| - +| `formal/F5_RenderFaithful.v:render_inj` +| Proved only for a model that allows `Option` at the top level. The real `Face.render_ty` is not injective: on the Js face `List[Option[Int]]` and `Option[List[Int]]` both render as `List[Int] \| null`, and on Cafe both render as `List[Int]?`. This was observed by calling the built library at `9167b04`. + +| Effect-row soundness for the real inference +| `open` +| - +| - +| `formal/Rows.v` is monomorphic. Effect rows are not checked against performed operations today (hole H5 in `docs/COMPLETION-PLAN.adoc`). + +| Type soundness of the full language +| `argued` +| - +| `docs/academic/proofs/*.md` +| Prose only. +|=== + +*Census.* 15 obligations: 7 `proven`, 7 `open`, 1 `argued`. Every `proven` +row is a statement about a model, not about the shipped OCaml code, as each +row's trust boundary says. + +*Proof Witness Grades.* Of the theory theorems above, 0 are at `PWG-3` or +better. All are `ungraded`, because none has an Agda source (PROOF-POLICY §8.1). + +*Policy position.* PROOF-POLICY §1 puts theory proofs in Agda, rechecked in +Rocq and Lean, and engineering properties of one system in Idris2. This +repository's Coq choice has no §4 exception recorded beside the files. +`docs/COMPLETION-PLAN.adoc` §5.0 sets out what that means. diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index fc43a258..c560af82 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -53,10 +53,13 @@ than the prose corpus suggests: * **`docs/academic/formal-verification/solo-core/`** — the only core-language formalisation. Covers the *Solo* fragment only: STLC + Unit + Product + Sum + `let` + QTT quantities `{0, 1, ω}`. `Syntax/Context/Quantity/Typing` are - populated; **`Soundness.idr` is statements-only** — `data Step` has *no - constructors* ("intentionally omitted until week 3"), and - `progress = ?todo_progress`, `preservation = ?todo_preservation`. Status: - `stated`. It proves nothing yet. Solo *excludes* traits, effects, rows, + populated. *Updated 2026-11-09:* `Soundness.idr` now gives `Step` its + constructors and proves `progress` and `preservation` (into a `Weaker` + sub-context); `affinePreservation` reuses `preservation`. All eight modules + check under Idris2 0.7.0 with `%default total`, no holes and no escape + hatches, and `progress` and `preservation` report total. This was a local + check at commit `9167b04`; no CI job runs it yet. Status: `mechanized` for + the Solo model only (the 2026-06-20 sweep said `stated`). Solo *excludes* traits, effects, rows, refinements, dependent types, ownership/borrowing, records, arrays, modules, and `unsafe`. * **`docs/academic/proofs/*.md`** — seven prose proofs (type-soundness, @@ -147,7 +150,7 @@ obligations. They are the "we might have missed" half of the brief. give `Step` its constructors and prove `progress`/`preservation`/`affinePreservation`. | XL | `partial` -| #513 must-have 1; solo-core (Idris2) `stated`; **progress + preservation +| #513 must-have 1; solo-core (Idris2) progress + preservation checked locally (Idris2 0.7.0, 2026-11-09; not CI-gated); **progress + preservation mechanized** for a first-order fragment (`formal/P2_Progress.v`) AND for the **STLC with functions + the substitution lemma** (`formal/P2_Stlc.v`, funext-free). QTT/affine quantities are the remaining increment diff --git a/docs/SOUNDNESS.adoc b/docs/SOUNDNESS.adoc index c46cc21f..533643ce 100644 --- a/docs/SOUNDNESS.adoc +++ b/docs/SOUNDNESS.adoc @@ -252,8 +252,13 @@ so the hand-off is deliberate. Closing an implementation hole is not the same as having metatheory. The soundness arguments for the holes above (`docs/academic/proofs/*.adoc`, the -comments in `lib/borrow.ml`) remain *prose*, and the Solo core fragment's -`Soundness.idr` progress / preservation are still `?todo`. Mechanisation has +comments in `lib/borrow.ml`) remain *prose*. The Solo core fragment's +`Soundness.idr` progress / preservation are now discharged: all eight +solo-core modules check under Idris2 0.7.0 with `%default total`, no holes and +no escape hatches (local check, 2026-11-09, commit `9167b04`; not yet gated in +CI). They concern the separate Solo model, not `lib/typecheck.ml`, and they are +a theory result in Idris2 rather than Agda (see the proof ledger in +`docs/EXPLAINME.adoc`). Mechanisation has *grown substantially* — the axiom-free Coq/Rocq `formal/` track now covers the Wave-0 codegen-preservation seed (K-1 `K1_CodegenPreservation.v`, K-1-with-`let` `K1Let_CodegenPreservation.v`), the F-1 transformer-preservation composition, and From e5e9ef0e16acaabc172951e881d40dd4ccd09ab7 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:47:12 +0000 Subject: [PATCH 2/4] docs(plan): record owner rulings 2026-11-09 and the Lean results Questions 16-19 and the next-phase choice are ruled: rewrite the definitional theorems first; Agda sources split by topic (semiring laws in resource-algebra, calculus soundness in formal/agda); Idris2 0.8.0 and Lean installs approved with section 6 deviation records; W1 first. With Lean installed from releases.lean-lang.org (digests recorded): tropical-types builds 20/20 at its 4.13.0 pin, and its 334 theorems use no sorry, Mathlib or Classical.choice (102 use propext or Quot.sound); occupancy's stackcert core does not compile at its 4.15.0 pin; the AffineScript copy of the tropical file compiles at 4.13.0. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW --- docs/COMPLETION-PLAN.adoc | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/docs/COMPLETION-PLAN.adoc b/docs/COMPLETION-PLAN.adoc index b5b62dd6..7fe484de 100644 --- a/docs/COMPLETION-PLAN.adoc +++ b/docs/COMPLETION-PLAN.adoc @@ -117,8 +117,8 @@ Results were consistent, but they do not prove CI is green. | No CI gate was found in the survey pass. | Lean `docs/academic/tropical-session-types` -| Not run. -| This is a diverged copy of the tropical-types file (461-line diff). +| Compiles under Lean 4.13.0 with zero errors and no `sorry` (2026-11-09). +| This is a diverged copy of the tropical-types file (412 differing lines after trimming whitespace). | — | anytype (`/home/user/anytype`) @@ -137,13 +137,13 @@ Results were consistent, but they do not prove CI is green. | A parametric `LEcho` over arbitrary drops. | tropical-types -| Lean 4.13 builds 20/20. The transport theorems are axiom-free, but `parametric_resource_transport` is a field repackaging. +| Lean 4.13.0 (its pin, installed from `releases.lean-lang.org`, 2026-11-09): `lake build` completes 20/20. An audit of all 334 theorems finds no `sorry`, no Mathlib and no `Classical.choice`; 102 use only Lean's `propext` and `Quot.sound`, which a grade must list (PROOF-POLICY §8.4). `parametric_resource_transport` is a field repackaging. | Isabelle was not run. The ROOT session covers 5 of 9 theories, and no CI workflow runs Isabelle. | — | occupancy, secret, residual-evidence, choreographic, epistemic | All five own gates pass, and every wired cone also passes the canonical flags cold, at Agda 2.6.3 (four of them pin 2.6.4.3, which was not installed). Rejection fixtures fail as intended: secret 2/2, epistemic 13/13, residual-evidence 9/9, occupancy 2/2, choreographic 5/5. No escape in any cone. -| secret-types' own `-W error` fails under the canonical flags unless `-W noUnsupportedIndexedMatch` is added. occupancy's Agda check is called by no workflow, Justfile recipe or script, and its R-6 row says PROVEN for two rejection fixtures (it is TESTED). The template Agda gate is broken in secret-types and occupancy (module name versus `include: src`). Lean was not re-run, so occupancy's `stackcert` remains unverified. No Rocq or Lean leg anywhere is `RECONCILED`, so nothing exceeds `PWG-3`, and no repo records a grade. +| secret-types' own `-W error` fails under the canonical flags unless `-W noUnsupportedIndexedMatch` is added. occupancy's Agda check is called by no workflow, Justfile recipe or script, and its R-6 row says PROVEN for two rejection fixtures (it is TESTED). The template Agda gate is broken in secret-types and occupancy (module name versus `include: src`). Under its pinned Lean 4.15.0, occupancy's `stackcert` core does not compile: `StackcertCore.lean` has type errors in the proof of `cert_sound` (2026-11-09), so the README's "compiles" is false. No Rocq or Lean leg anywhere is `RECONCILED`, so nothing exceeds `PWG-3`, and no repo records a grade. | None of these has an AffineScript consumer. | jtv-halting-islands-ct @@ -619,7 +619,7 @@ What that means here: * *Theory files.* `QttSemiring`, `P2_Progress`, `P2_Stlc`, `Rows`, `AffineUsage`, `QttTyping`, `QttDynamic` and the Idris2 Solo core are theory. None has an Agda source, so every one is `ungraded`. The Coq files are `COQ-CHECKED` target-only evidence. * *Engineering files.* `K1*`, `Real*`, `P3_*`, `F1` and `F3`–`F5` state properties of this repository's code. No §4 exception is recorded for them. The stated reason in `formal/README.adoc` (interop with typed-wasm and ephapax) is not one of §4's grounds. Question 16 asks the owner to choose. -* *Highest grade reachable in agent sandboxes.* Lean toolchains are downloadable from `releases.lean-lang.org` (4.13.0 and 4.15.0 return HTTP 200), but in this session the automatic permission check refused installing them as external code. Until the owner approves that install (question 19), a Lean leg is `unavailable` in agent sessions, and the best grade they can reach is `PWG-2i`: an Agda source plus a reconciled Rocq leg. +* *Highest grade reachable in agent sandboxes.* With the owner's approval (question 19), Lean 4.13.0 and 4.15.0 were installed from `releases.lean-lang.org` on 2026-11-09, with SHA-256 `44ceeac7…` and `af71a256…` recorded for the §6 deviation. A Lean leg can therefore be re-proved in a sandbox, so `PWG-2ii` is reachable there once the Agda source and both legs are reconciled. * *Oracles are not proofs.* Z3, Datalog and differential checks earn `TESTED` (with bounds) or `ASSUMED`. They never earn `PROVEN` without an independently checked certificate (§5). * *Proof ledger.* The ledger now lives in `docs/EXPLAINME.adoc`. It has 15 obligations: 7 `proven` (all about models), 7 `open` and 1 `argued`. No theory theorem is at `PWG-3` or better. * *Where the Agda sources live* is an owner decision (question 17). @@ -857,13 +857,15 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness * Isolation: one container image snapshot, recorded so later workflows can reuse it. * Gates: the M0 commands; `cd $TW && cargo test --workspace --all-features`; Coq gate `just -f $AS/formal/justfile check` plus a generated `Print Assumptions` over every assertion; every Agda theory entrypoint under exactly `agda --safe --without-K --cubical-compatible`. * Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, `make bootstrap SCHEME=chezscheme`, `make install PREFIX=/opt/idris2`. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, has not been built in a sandbox. -* Lean is downloadable from `releases.lean-lang.org`, but installing it needs owner approval (question 19); GitHub release downloads are blocked. Until then record every Lean leg as `unavailable`, never as passing. +* Lean: install the pinned toolchain from `releases.lean-lang.org` (`curl -sSLO https://releases.lean-lang.org/lean4/v/lean--linux.tar.zst`, extract with `tar --zstd`), and record its SHA-256 as a PROOF-POLICY §6 deviation. The owner approved this on 2026-11-09. GitHub release downloads stay blocked, so elan is not the route. * Treat an Idris2 `--check` exit code of 0 as a pass only when its output also contains no `Error:` line. * Stop if: a pinned prover cannot be provisioned. Record the leg as unavailable and continue with the others. * Output: a versioned toolchain manifest, kept out of the repo root. *W1 Ledger the holes (understand + implement tests).* +*Ruled 2026-11-09:* W1 runs first, once this plan revision and the companion mathesis change land. + * Goal: M1. * Fan-out: one agent per hole, H1–H13 and H16–H18, each in its own git worktree, writing only an xfail fixture and a ledger row. * Scope: affinescript only. @@ -928,7 +930,7 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150 * Goal: bring the proof track into line with PROOF-POLICY (section 5.0), then P2 (R-wrap, extraction test), P3 (`anytype_emit.ml` with the anytype or Z3 oracle), and gate hardening. * Fan-out: four agents. -** Agda theory agent: port `QttSemiring` first, then `P2_Stlc`, `Rows` and the Solo core, to Agda under the canonical flags, in the home question 17 settles. For each, record the Rocq leg's statement comparison so it can become `RECONCILED`. Re-prove the Lean leg by hand (no Mathlib) once question 19 is settled; until then record it as `unavailable`. +** Agda theory agent: port `QttSemiring` first, then `P2_Stlc`, `Rows` and the Solo core, to Agda under the canonical flags, in the home question 17 settles. For each, record the Rocq leg's statement comparison so it can become `RECONCILED`. Re-prove the Lean leg by hand, with no Mathlib. ** Coq agent in `formal/`: close H21 first, and act on the engineering files as question 16 decides. ** OCaml emitter agent. ** anytype agent: fix the `abi.ipkg` path in the Justfile and `idris2-proof.yml`, and the workflow's `paths` filter. The corrected path already gives 19/19 golden and 8/8 CLI cases under Idris2 0.7.0. Draft `gjoin` as a systemet ADR only. @@ -1026,8 +1028,8 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150 . *Coq pin.* 8.18 (docs) or 8.20.1 (CI)? . *Toolchains.* Approve idris2 in sandboxes; without it, every Idris claim stays unverified. . *Node exemption.* Approve a Node runtime exemption for the dom and cadre e2e harnesses, or port them to Bun? -. *Coq engineering track.* Record a PROOF-POLICY §4 exception for the Coq engineering files (`K1*`, `Real*`, `P3_*`, `F*`), or move them to Idris2 when next touched? Policy's default is Idris2. -. *Home of the Agda theory sources.* AffineScript `formal/agda/`, anytype (beside its grade algebra), or mathesis (which may hold theory with no other natural home)? -. *Idris2 0.8.0.* Approve building Idris2 0.8.0 from source in agent sandboxes (typed-wasm's pin)? An attempt this session was refused by the session's automatic permission check. -. *Lean.* Approve installing pinned Lean toolchains from `releases.lean-lang.org` in agent sandboxes, with a digest recorded as a §6 deviation? The same check refused it this session. Without it, tropical-types and occupancy's `stackcert` cannot be re-checked and no Lean leg can count. +. *Coq engineering track.* Record a PROOF-POLICY §4 exception for the Coq engineering files (`K1*`, `Real*`, `P3_*`, `F*`), or move them to Idris2 when next touched? Policy's default is Idris2. *Ruled 2026-11-09:* first rewrite the theorems that hold by definition (P3 `borrow_soundness`, F3, F4, F1 `f1_same_cube`, `QttTyping.usage_soundness`) as real statements about the code; decide the prover for the engineering track after that. +. *Home of the Agda theory sources.* AffineScript `formal/agda/`, anytype (beside its grade algebra), or mathesis (which may hold theory with no other natural home)? *Ruled 2026-11-09:* split by topic. The QTT semiring laws go in resource-algebra as a non-idempotent tier; calculus soundness (STLC, rows, the Solo core) goes in AffineScript `formal/agda/`. +. *Idris2 0.8.0.* Approve building Idris2 0.8.0 from source in agent sandboxes (typed-wasm's pin)? An attempt this session was refused by the session's automatic permission check. *Ruled 2026-11-09:* approved, with a §6 deviation record. +. *Lean.* Approve installing pinned Lean toolchains from `releases.lean-lang.org` in agent sandboxes, with a digest recorded as a §6 deviation? The same check refused it this session. Without it, tropical-types and occupancy's `stackcert` cannot be re-checked and no Lean leg can count. *Ruled 2026-11-09:* approved; Lean 4.13.0 and 4.15.0 are now installed this way, with their digests recorded above. . *Status documents.* Re-sign the AFFIRMATION files, and decide whether the stale ROADMAP (January 2026 baseline) is retired or rewritten. \ No newline at end of file From c0c72d7cd46e81cc4a4e234bec8cc9e08f0affa5 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:50:39 +0000 Subject: [PATCH 3/4] docs: address CodeRabbit review on the proof review - Proof ledger now keyed to every PROOF-NEEDS obligation: 22 rows, 7 proven (models only), 13 open, 2 argued (adds P-5, P-7, P-8, P-10, F-2, F-6, F-7); prose-proof paths corrected to .adoc. - PROOF-NEEDS: P-2 marked mechanized for the Solo model; caveats on P-3, P-4 and the K-1 real-lift text (models, unbounded Z, not i32); F-5 records the real render_ty counterexample and stays open. - Plan: H20-H22 added to M1, W1 and section 3 with test anchors; W0 build steps cd into the Idris2 clone and put it on PATH; cubical pragma modules need a reviewed profile; the Coq gate must also scan for unused axioms; the Solo core needs its own Rocq recheck; the anytype and P3/F2 statuses reflect that Idris2 0.7.0 is provisionable. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW --- docs/COMPLETION-PLAN.adoc | 25 ++++---- docs/EXPLAINME.adoc | 126 ++++++++++++++++++++++++++------------ docs/PROOF-NEEDS.adoc | 41 +++++++++---- 3 files changed, 129 insertions(+), 63 deletions(-) diff --git a/docs/COMPLETION-PLAN.adoc b/docs/COMPLETION-PLAN.adoc index 7fe484de..2046f9bd 100644 --- a/docs/COMPLETION-PLAN.adoc +++ b/docs/COMPLETION-PLAN.adoc @@ -383,7 +383,7 @@ The kernel enters first as an independent oracle for translation validation, and |=== | Component | Owner repo | Why -| xfail pins and ledger entries for H1–H13 and H16–H18 +| xfail pins and ledger entries for H1–H13, H16–H18 and H20–H22 | affinescript (`test/xfail`, `docs/SOUNDNESS.adoc`) | Doctrine 1. Today the ledger claims "one remaining residual", which is an overclaim. @@ -503,13 +503,13 @@ Serialise apt installs; never run two at once. === M1. Ledger the holes before fixing them -*Exit criteria:* each of H1–H13 and H16–H18 has a failing-expectation pin in `test/xfail` (or the e2e suite) and a `docs/SOUNDNESS.adoc` row. The vacuous QTT anchors carry `@linear`/`@erased` annotations and assert `Error`. +*Exit criteria:* each of H1–H13, H16–H18 and H20–H22 has a failing-expectation pin in `test/xfail` (or the e2e suite) and a `docs/SOUNDNESS.adoc` row. The vacuous QTT anchors carry `@linear`/`@erased` annotations and assert `Error`. ---- cd $AS && dune runtest --force > /tmp/m1.log 2>&1; rc=$? n=$(grep -cE 'XFAIL-OK|FENCE-OK' /tmp/m1.log || true) echo "markers=$n dune_rc=$rc" -test "$rc" -eq 0 && test "$n" -ge "$((EXISTING + 16))" # EXISTING = pin count before M1 +test "$rc" -eq 0 && test "$n" -ge "$((EXISTING + 19))" # EXISTING = pin count before M1 bash tools/check-soundness-ledger.sh ---- @@ -621,7 +621,7 @@ What that means here: * *Engineering files.* `K1*`, `Real*`, `P3_*`, `F1` and `F3`–`F5` state properties of this repository's code. No §4 exception is recorded for them. The stated reason in `formal/README.adoc` (interop with typed-wasm and ephapax) is not one of §4's grounds. Question 16 asks the owner to choose. * *Highest grade reachable in agent sandboxes.* With the owner's approval (question 19), Lean 4.13.0 and 4.15.0 were installed from `releases.lean-lang.org` on 2026-11-09, with SHA-256 `44ceeac7…` and `af71a256…` recorded for the §6 deviation. A Lean leg can therefore be re-proved in a sandbox, so `PWG-2ii` is reachable there once the Agda source and both legs are reconciled. * *Oracles are not proofs.* Z3, Datalog and differential checks earn `TESTED` (with bounds) or `ASSUMED`. They never earn `PROVEN` without an independently checked certificate (§5). -* *Proof ledger.* The ledger now lives in `docs/EXPLAINME.adoc`. It has 15 obligations: 7 `proven` (all about models), 7 `open` and 1 `argued`. No theory theorem is at `PWG-3` or better. +* *Proof ledger.* The ledger now lives in `docs/EXPLAINME.adoc`. It has 22 obligation rows, keyed to the `docs/PROOF-NEEDS.adoc` IDs: 7 `proven` (all about models), 13 `open` and 2 `argued`. No theory theorem is at `PWG-3` or better. * *Where the Agda sources live* is an owner decision (question 17). Leverage means how much assurance a rung adds about the actual binary `main.exe` and its outputs, not about an idealised core. @@ -651,7 +651,7 @@ Leverage means how much assurance a rung adds about the actual binary `main.exe` | P3 | QTT verdict validation: emit each function's core fragment to anytype and compare verdicts with `quantity.ml`. | Idris2 (anytype) as oracle. Optionally Z3, encoding usage counts as linear constraints, as a second independent oracle. -| The algebra is lawful (RUN, on transcribed tables). The checker is not proved. idris2 is unavailable. +| The algebra is lawful (RUN, on transcribed tables). The checker is not proved. Idris2 0.7.0, anytype's pin, can now be provisioned (W0), and the checker passes its 19 golden and 8 CLI cases with the corrected `abi.ipkg` path. | anytype has no join, branching or ADTs, so coverage will be partial. Report the coverage percentage as a number and never present it as full. | P4 @@ -748,12 +748,12 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness | A. Rebase `quantity.ml` on anytype: in-process via Idris RefC/Zig, or replace the pass with the extracted checker. *Elegant default.* | 5 | 4 -| The kernel would be the checker. Blocked: anytype lacks join, branching and ADTs, there is no soundness proof yet, and idris2 is unavailable. +| The kernel would be the checker. Blocked: anytype lacks join, branching and ADTs, and there is no soundness proof yet. Idris2 0.7.0 can now be provisioned (W0). | B. Keep `quantity.ml` and `borrow.ml`. Use anytype, plus optionally Z3, as an external oracle in CI for translation validation of verdicts. | 4 | 4 -| Blocked on idris2 for the anytype oracle, because `anytype-check` is an Idris2 executable and the Zig export only spawns that CLI. Only the Z3 oracle can ship now. Coverage is honest and measurable once it runs. +| The anytype oracle can run now: Idris2 0.7.0 builds in a sandbox, and `anytype-check` passes its 19 golden and 8 CLI cases with the corrected `abi.ipkg` path. The Z3 oracle can run beside it. Coverage stays partial, because anytype has no branching or ADTs; report it as a number. | C. Functorise `quantity.ml` over a `GRADE` signature mirroring Lean `ResourceSemiring`. Affine stays the default instance. | 4 @@ -855,8 +855,8 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness * Fan-out: a single agent. apt is serialised, because parallel installs clobbered each other in the survey. * Scope: all repos, read-only. * Isolation: one container image snapshot, recorded so later workflows can reuse it. -* Gates: the M0 commands; `cd $TW && cargo test --workspace --all-features`; Coq gate `just -f $AS/formal/justfile check` plus a generated `Print Assumptions` over every assertion; every Agda theory entrypoint under exactly `agda --safe --without-K --cubical-compatible`. -* Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, `make bootstrap SCHEME=chezscheme`, `make install PREFIX=/opt/idris2`. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, has not been built in a sandbox. +* Gates: the M0 commands; `cd $TW && cargo test --workspace --all-features`; Coq gate `just -f $AS/formal/justfile check` plus a generated `Print Assumptions` over every assertion; every Agda theory entrypoint under exactly `agda --safe --without-K --cubical-compatible`. Record each entrypoint's mode: a file-pragma `--cubical` still passes that command line, so a cubical module counts only under a separately reviewed proof profile, and that obligation stays open until the review is recorded. +* Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, then `cd Idris2 && make bootstrap SCHEME=chezscheme && make install PREFIX=/opt/idris2`. Put `/opt/idris2/bin` on `PATH` for every later step and agent (`export PATH=/opt/idris2/bin:$PATH`), so direct checks and `tools/check-proofs.sh` find it. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, has not been built in a sandbox. * Lean: install the pinned toolchain from `releases.lean-lang.org` (`curl -sSLO https://releases.lean-lang.org/lean4/v/lean--linux.tar.zst`, extract with `tar --zstd`), and record its SHA-256 as a PROOF-POLICY §6 deviation. The owner approved this on 2026-11-09. GitHub release downloads stay blocked, so elan is not the route. * Treat an Idris2 `--check` exit code of 0 as a pass only when its output also contains no `Error:` line. * Stop if: a pinned prover cannot be provisioned. Record the leg as unavailable and continue with the others. @@ -867,7 +867,8 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness *Ruled 2026-11-09:* W1 runs first, once this plan revision and the companion mathesis change land. * Goal: M1. -* Fan-out: one agent per hole, H1–H13 and H16–H18, each in its own git worktree, writing only an xfail fixture and a ledger row. +* Fan-out: one agent per hole, H1–H13, H16–H18 and H20–H22, each in its own git worktree, writing only an xfail fixture and a ledger row. +* Anchors for the new holes. H20: a test that renders `List[Option[Int]]` and `Option[List[Int]]` on the Js and Cafe faces and expects different strings. H21: planted assertions outside the printed theorems' cone, and an unused `Axiom bad : False.`, must each fail the Coq gate, and a change to a modelled `lib/*.ml` file must re-run it. H22: `tools/check-proofs.sh --agda` must fail, not skip, when `AFFINESCRIPT_ECHO_TYPES_DIR` or `AGDA_STDLIB` is unset, and the echo-types revision it checks against must be pinned. * Scope: affinescript only. * Gates: `dune runtest --force` and `bash tools/check-soundness-ledger.sh` on a full clone. * Stop if: any pin passes unexpectedly. That means the hole is not reproduced; re-verify before writing anything. @@ -930,12 +931,12 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150 * Goal: bring the proof track into line with PROOF-POLICY (section 5.0), then P2 (R-wrap, extraction test), P3 (`anytype_emit.ml` with the anytype or Z3 oracle), and gate hardening. * Fan-out: four agents. -** Agda theory agent: port `QttSemiring` first, then `P2_Stlc`, `Rows` and the Solo core, to Agda under the canonical flags, in the home question 17 settles. For each, record the Rocq leg's statement comparison so it can become `RECONCILED`. Re-prove the Lean leg by hand, with no Mathlib. +** Agda theory agent: port `QttSemiring` first, then `P2_Stlc`, `Rows` and the Solo core, to Agda under the canonical flags, in the home question 17 settles. For each, record the Rocq leg's statement comparison so it can become `RECONCILED`. The Solo core has no Rocq proof yet: `P2_Stlc` covers a calculus without quantities and does not count, so write a Rocq recheck of Solo progress and preservation for the quantitative calculus before Solo can reach `PWG-2i`. Re-prove the Lean leg by hand, with no Mathlib. ** Coq agent in `formal/`: close H21 first, and act on the engineering files as question 16 decides. ** OCaml emitter agent. ** anytype agent: fix the `abi.ipkg` path in the Justfile and `idris2-proof.yml`, and the workflow's `paths` filter. The corrected path already gives 19/19 golden and 8/8 CLI cases under Idris2 0.7.0. Draft `gjoin` as a systemet ADR only. * Gates: -** Generate `AllAssump.v` from a grep of every `Theorem|Lemma|Corollary|Example|Proposition|Fact|Remark` in `formal/*.v` and commit the generator. Then `coqc -Q . ASFormal AllAssump.v | grep -c 'Closed under'` must equal the generated line count. Add a negative test: an `Admitted` lemma in `QttSemiring.v` must fail the gate. +** Generate `AllAssump.v` from a grep of every `Theorem|Lemma|Corollary|Example|Proposition|Fact|Remark` in `formal/*.v` and commit the generator. Then `coqc -Q . ASFormal AllAssump.v | grep -c 'Closed under'` must equal the generated line count. Add a negative test: an `Admitted` lemma in `QttSemiring.v` must fail the gate. `Print Assumptions` never reports an axiom that no theorem uses, so also reject any `Axiom`, `Parameter`, `Conjecture`, `Admitted` or `admit` anywhere in `formal/` by a separate scan, with a negative test that an unused `Axiom bad : False.` fails the gate. ** `dune test` for extraction parity. ** In anytype: `./scripts/check-idris2-proofs.sh` (only if idris2 is provisioned). * R-wrap starts only after the owner rules on question 1 (integer semantics); otherwise it may prove agreement with the wrong target. diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index 1b5fa040..49bfa51e 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -78,9 +78,13 @@ AffineScript validates the hyperpolymath ecosystem: [[proof-ledger]] == Proof Ledger -One row per proof obligation this repository speaks about, in the closed -vocabulary of `metadatastician/standards` `docs/README-EXPLAINME-STANDARD.adoc` -§5 (`proven`, `proven-with-postulates`, `argued`, `tested-only`, `open`). +One row per proof obligation this repository speaks about, keyed to the IDs in +`docs/PROOF-NEEDS.adoc`, in the closed vocabulary of `metadatastician/standards` +`docs/README-EXPLAINME-STANDARD.adoc` §5 (`proven`, `proven-with-postulates`, +`argued`, `tested-only`, `open`). P-1 (the inventory itself) and P-9 (withdrawn +with the refinement surface) carry no proof obligation. K-2 is P-6, and K-3 is +part of P-3. K-4 says each `CAPABILITY-MATRIX` row is a latent obligation; those +rows are not listed here. *Receipts.* Recorded on 2026-11-09 at commit `9167b04`: @@ -96,98 +100,140 @@ vocabulary of `metadatastician/standards` `docs/README-EXPLAINME-STANDARD.adoc` |=== | Obligation | Status | Checker (version, flags) | Where | Trust boundary -| Code-generation preservation, toy nat/bool compiler (K-1, K-1 with `let`) +| P-2. Solo core progress and preservation | `proven` -| coqc 8.18.0 -| `formal/K1_CodegenPreservation.v:compile_correct`, `formal/K1Let_CodegenPreservation.v:compile_correct` -| A toy compiler and stack machine. Not `lib/codegen.ml`. +| Idris2 0.7.0, `%default total` +| `docs/academic/formal-verification/solo-core/Soundness.idr:progress`, `:preservation` +| A separate Solo model, not `lib/typecheck.ml` or `lib/borrow.ml`. No CI job runs it. It is a theory statement held in Idris2 rather than Agda, so it is `ungraded`. -| Code-generation forward simulation on a WASM-shaped model +| P-2 (Coq). Progress and preservation, first-order and STLC | `proven` | coqc 8.18.0 -| `formal/RealCompile.v:compile_correct`, `formal/RealLoop.v:compile_stmt_correct` -| A de Bruijn re-implementation, not `lib/codegen.ml` or `lib/interp.ml`. Integers are unbounded `Z`, not i32. Forward only, with nothing about traps or divergence. `RealLoop` covers let-free statements only. Its header's "observable difference is proved" has no matching theorem. +| `formal/P2_Progress.v`, `formal/P2_Stlc.v` +| Theory, `ungraded`. Textbook STLC with no quantities or affinity, so it is not AffineScript's calculus. -| Memory and executor lemmas on the WASM model -| `proven` -| coqc 8.18.0 -| `formal/RealMem.v`, `formal/RealWasm.v` -| Fixed instruction sequences. Addressing is word-based, while codegen uses byte offsets. An out-of-range store is a no-op where WASM traps. +| P-3 and K-3. Borrow checker soundness (`lib/borrow.ml`), rejecting #554 +| `open` +| - +| `formal/P3_BorrowSound.v`, `formal/P3_BorrowGraph.v` +| `borrow_soundness` holds by definition: `borrow_ok` is defined as the negation of the dynamic oracle it is compared against. `rejects_554` and `move_locality` are proven but small. -| QTT `{0,1,ω}` semiring and order laws +| P-4. QTT `{0,1,ω}` semiring and order laws | `proven` | coqc 8.18.0 | `formal/QttSemiring.v` | Theory: no Agda source, so PROOF-POLICY gives it no proof witness grade (it is `ungraded`). The tables match `lib/quantity.ml` `q_add`/`q_mul` by inspection only. The CI gate does not cover 16 of the 21 laws. -| QTT typing soundness for the real quantity checker +| P-4. QTT typing soundness for the real quantity checker | `open` | - | `formal/QttTyping.v`, `formal/QttDynamic.v` | `QttTyping` is an occurrence counter presented as a judgment. `Q_App` does not scale and `Q_Var` accepts any type. `QttDynamic` proves only a lambda-free scaling law and no subject reduction. -| Progress and preservation, first-order and STLC (P-2) +| P-5. HM inference soundness and principality +| `argued` +| - +| `docs/academic/proofs/inference-algorithm.adoc` +| Prose only. + +| P-6 and K-2. Effect-row soundness for the real inference +| `open` +| - +| - +| Blocked on #555. `formal/Rows.v` is monomorphic. Effect rows are not checked against performed operations today (hole H5 in `docs/COMPLETION-PLAN.adoc`). + +| P-7. Name-resolution determinism +| `open` +| - +| - +| Not started. + +| P-8. Parser conformance +| `open` +| - +| `conformance/` +| Not started. The conformance corpus is not wired, and two valid cases fail to parse (`docs/COMPLETION-PLAN.adoc`). + +| P-10. Trait coherence +| `open` +| - +| - +| The implementation rejects concrete overlaps (#559); the uniqueness proof is unwritten. + +| P-11. Progress and preservation for monomorphic records | `proven` | coqc 8.18.0 -| `formal/P2_Progress.v`, `formal/P2_Stlc.v` -| Theory, `ungraded`. Textbook STLC with no quantities or affinity, so it is not AffineScript's calculus. +| `formal/Rows.v` +| Theory, `ungraded`. Rows are ordered lists with no row variables. -| Progress and preservation for monomorphic records +| K-1. Code-generation preservation, toy nat/bool compiler | `proven` | coqc 8.18.0 -| `formal/Rows.v` -| Theory, `ungraded`. Rows are ordered lists with no row variables. This is not the effect-row system. +| `formal/K1_CodegenPreservation.v:compile_correct`, `formal/K1Let_CodegenPreservation.v:compile_correct` +| A toy compiler and stack machine. Not `lib/codegen.ml`. -| Solo core progress and preservation +| K-1. Code-generation forward simulation on a WASM-shaped model | `proven` -| Idris2 0.7.0, `%default total` -| `docs/academic/formal-verification/solo-core/Soundness.idr:progress`, `:preservation` -| A separate Solo model, not `lib/typecheck.ml` or `lib/borrow.ml`. No CI job runs it. It is a theory statement held in Idris2 rather than Agda, so it is `ungraded`. +| coqc 8.18.0 +| `formal/RealCompile.v:compile_correct`, `formal/RealLoop.v:compile_stmt_correct` +| A model, not the shipped compiler: a de Bruijn re-implementation of the source and `eval`, not `lib/codegen.ml` or `lib/interp.ml`. Integers are unbounded `Z`, not i32, so no i32 behaviour is proved. Forward only, with nothing about traps or divergence. `RealLoop` covers let-free statements only. Its header's "observable difference is proved" has no matching theorem. -| Borrow checker soundness (`lib/borrow.ml`) -| `open` -| - -| `formal/P3_BorrowSound.v`, `formal/P3_BorrowGraph.v` -| `borrow_soundness` holds by definition: `borrow_ok` is defined as the negation of the dynamic oracle it is compared against. `rejects_554` and `move_locality` are proven but small. +| K-1. Memory and executor lemmas on the WASM model +| `proven` +| coqc 8.18.0 +| `formal/RealMem.v`, `formal/RealWasm.v` +| Fixed instruction sequences. Addressing is word-based, while codegen uses byte offsets. An out-of-range store is a no-op where WASM traps. -| Face transformer preserves evaluation (F-1) +| F-1. Face transformer preserves evaluation | `open` | - | `formal/F1_TransformerPreservation.v` | The model is an invented AST elaborator, while the real faces rewrite text line by line (`lib/python_face.ml`). `f1_same_cube` is congruence. -| Face pragma detection is local and functional (F-3) +| F-2. Cross-face agreement (same cube) +| `open` +| - +| `invariant-path/proofs/SameCube.agda` (another repository) +| A unit-returning-tail case is proved in invariant-path; it was not re-checked here. Value-returning tails diverge (#601). + +| F-3. Face pragma detection is local and functional | `open` | - | `formal/F3_PragmaDecidable.v` | Both theorems hold for any function and by definition. The real scan limits in `lib/face_pragma.ml` are not modelled. -| Face error rendering is faithful (F-4) +| F-4. Face error rendering is faithful | `open` | - | `formal/F4_ErrorFaithful.v` | `render` is defined to copy the fields it is claimed to preserve. `lib/face.ml` formatting is not modelled. -| Face type rendering is injective (F-5) +| F-5. Face type rendering is injective | `open` | - | `formal/F5_RenderFaithful.v:render_inj` | Proved only for a model that allows `Option` at the top level. The real `Face.render_ty` is not injective: on the Js face `List[Option[Int]]` and `Option[List[Int]]` both render as `List[Int] \| null`, and on Cafe both render as `List[Int]?`. This was observed by calling the built library at `9167b04`. -| Effect-row soundness for the real inference +| F-6. Preview round-trip totality +| `open` +| - +| - +| Not started. + +| F-7. Face confluence with canonicalisation | `open` | - | - -| `formal/Rows.v` is monomorphic. Effect rows are not checked against performed operations today (hole H5 in `docs/COMPLETION-PLAN.adoc`). +| Not started. | Type soundness of the full language | `argued` | - -| `docs/academic/proofs/*.md` +| `docs/academic/proofs/*.adoc` | Prose only. |=== -*Census.* 15 obligations: 7 `proven`, 7 `open`, 1 `argued`. Every `proven` +*Census.* 22 obligations: 7 `proven`, 13 `open`, 2 `argued`. Every `proven` row is a statement about a model, not about the shipped OCaml code, as each row's trust boundary says. diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index c560af82..b7ed15ec 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -146,11 +146,13 @@ obligations. They are the "we might have missed" half of the brief. | — | P-2 -| **Solo progress + preservation.** Discharge the two holes in `Soundness.idr`: - give `Step` its constructors and prove - `progress`/`preservation`/`affinePreservation`. -| XL | `partial` -| #513 must-have 1; solo-core (Idris2) progress + preservation checked locally (Idris2 0.7.0, 2026-11-09; not CI-gated); **progress + preservation +| **Solo progress + preservation.** *Done for the Solo model (checked 2026-11-09):* + `Soundness.idr` gives `Step` its constructors and proves + `progress`/`preservation`/`affinePreservation` under Idris2 0.7.0 with + `%default total`. Remaining, and separate: a CI job for it, and the + policy's Agda source plus Rocq and Lean rechecks. +| XL | `mechanized` +| #513 must-have 1; solo-core (Idris2) progress + preservation checked locally (Idris2 0.7.0, 2026-11-09; not CI-gated). Separately, **progress + preservation mechanized** for a first-order fragment (`formal/P2_Progress.v`) AND for the **STLC with functions + the substitution lemma** (`formal/P2_Stlc.v`, funext-free). QTT/affine quantities are the remaining increment @@ -162,7 +164,10 @@ obligations. They are the "we might have missed" half of the brief. | #513 must-have 2; **mechanized** for a single-bit model (`formal/P3_BorrowSound.v`) and a *multi-resource borrow graph* with loan edges + liveness (`formal/P3_BorrowGraph.v`: soundness, completeness, - move-locality, multi-resource #554 rejected). #554 fixed (SOUNDNESS.adoc); + move-locality, multi-resource #554 rejected). *Caveat (2026-11-09 review):* + `borrow_soundness` holds by definition there (`borrow_ok` is the negation of + the dynamic oracle it is compared with), so it says nothing about + `lib/borrow.ml`; see the proof ledger in `docs/EXPLAINME.adoc`. #554 fixed (SOUNDNESS.adoc); full P-3 needs `lib/borrow.ml`'s CFG + Polonius #553 | P-4 @@ -173,7 +178,10 @@ obligations. They are the "we might have missed" half of the brief. (`{0,1,ω}` laws + occurrence homomorphism), `formal/AffineUsage.v` (`λx.x` affine, `λx. x x` not), `formal/QttTyping.v` — a quantitative type system whose usage context Γ is proven to track usage exactly (`usage x t = Γ x`) — and - `formal/QttDynamic.v`, the *dynamic* half: β-reduction **preserves the usage + `formal/QttDynamic.v`, the *dynamic* half. *Caveat (2026-11-09 review):* + `QttTyping` is an occurrence counter presented as a judgment (`Q_App` does not + scale; `Q_Var` accepts any type), so `usage_soundness` holds by definition; see + the proof ledger. The dynamic half: β-reduction **preserves the usage profile** (`t → t' ⇒ ∀z, usage z t' = usage z t`), with the QTT scaling law (`qof_mult`) and `qtt_context_preserved` composing it with `usage_soundness`. The full operational development on the *real* AST (substitution lemma past the @@ -255,7 +263,10 @@ The work in flight changes which obligations are *load-bearing* and which are **first real `⟦compile p⟧ = ⟦p⟧`** — resolved int/bool/`let`/binary/**if** source, reference `eval`, `compile` to real wasm, `compile_correct` (env↔locals agreement, existential-fuel) + `compile_program_correct`, retiring `K1`/`K1Let` - on real objects. R2's conditionals forced `wexec` to become **fuel-indexed** + on real objects. *Caveat (2026-11-09 review):* these are models, not the + shipped compiler. `RealCompile` re-implements the source and `eval` with de + Bruijn locals, and its integers are unbounded `Z`, not i32, so nothing here is + proved about `lib/codegen.ml` or i32 behaviour. R2's conditionals forced `wexec` to become **fuel-indexed** (nested `list instr` defeats the structural guard checker); R2-loops (`Loop`/`Br`, value-returning tails) is next and settles #601 concretely. * **K-2 — Effect-soundness is *blocked*, not merely unproven.** P-6 cannot be @@ -344,7 +355,13 @@ cover them. collapse onto one string), incl. the Js/Cafe "null"/"?" overlap (`js_no_collapse`, `cafe_no_collapse`, `option_never_atom`). Faithful to the whole-string Unit/Bool match + canonical-inner Option rewrite; models the - name vocabulary, not raw OCaml strings. `lib/face.ml` `render_ty` + name vocabulary, not raw OCaml strings. `lib/face.ml` `render_ty`. + *Counterexample (2026-11-09):* the real `render_ty` is not injective. On the + Js face `List[Option[Int]]` and `Option[List[Int]]` both render as + `List[Int] \| null`, and on Cafe both as `List[Int]?`, because the greedy + `Option\[\(.*\)\]` regex matches across brackets. The model allows `Option` + only at the top level. Injectivity of the real function stays open (hole H20 + in `docs/COMPLETION-PLAN.adoc`). | F-6 | **Preview round-trip totality.** The `preview-{python,js,pseudocode,lucid,cafe}` @@ -409,7 +426,8 @@ F-1 (full transformer preservation) is non-trivial rather than a formality. + the substitution lemma** (`P2_Stlc.v`, funext-free); **P-3 → a multi-resource borrow graph** (`P3_BorrowGraph.v`: loan edges, liveness, move-locality, multi-resource #554 rejected); **F-5 → `render_ty` non-collision** - (`F5_RenderFaithful.v`: every face's renaming injective). *Leftover:* the K-4 + (`F5_RenderFaithful.v`: every face's renaming injective *in the model*; the + real `render_ty` collides on nested types, so F-5 itself stays open, H20). *Leftover:* the K-4 `CAPABILITY-MATRIX` cross-link. | Wave 0 @@ -433,7 +451,8 @@ F-1 (full transformer preservation) is non-trivial rather than a formality. (`formal/RealWasm.v` — real `lib/wasm.ml` IR, i32 core + locals + structured `IfElse`, fuel-indexed `wexec`; `formal/RealCompile.v` — the first real `⟦compile p⟧ = ⟦p⟧` incl. value-returning `if`, retiring K1/K1Let on real - objects). **R2-loops** (`Loop`/`Br`, value-returning tails) is next and settles + objects; these are models with unbounded `Z` integers, not the shipped + compiler or i32). **R2-loops** (`Loop`/`Br`, value-returning tails) is next and settles #601 concretely. Then the still-`prose`/`absent` obligations: P-5 (inference), P-6 (effects — blocked on #555/K-2, = rung R-eff), P-7 (resolution), P-8 (parser), P-10 (coherence); faces F-6/F-7; full-language borrowing (P-3) From 19084c8e3e4c037db71a7dc9b837e2c6933f12e9 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:09:45 +0000 Subject: [PATCH 4/4] docs(plan): Idris2 0.8.0 results and the provisioning prefix fix - typed-wasm passes tools/check-kernel-proofs.sh in full under the pinned Idris2 0.8.0 (15a3e4e): 33 modules, 13 rejections, 197-row explorer, 269 table equalities, 4 negative controls. Region.idr:179 was a 0.7.0-only incompatibility; the ledger item is closed. - januskey and absolute-zero type-check under the 0.8.0 release; januskey's 3 reject fixtures are refused for the expected reason and a planted well-typed fixture fails its script. Their CI pins an idris2-pack image built from Idris2 main (6ca00e72...), not the v0.8.0 tag; that image was not run. New estate item: the Idris2 repos check against three different compilers. - W0 recipe: PREFIX must go to make bootstrap as well as make install, or the install type-checks but cannot run programs, and Idris2 still exits 0. The exit-code rule now covers INTERNAL ERROR and Exception. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW --- docs/COMPLETION-PLAN.adoc | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/docs/COMPLETION-PLAN.adoc b/docs/COMPLETION-PLAN.adoc index 2046f9bd..efa98dde 100644 --- a/docs/COMPLETION-PLAN.adoc +++ b/docs/COMPLETION-PLAN.adoc @@ -103,7 +103,7 @@ Results were consistent, but they do not prove CI is green. | typed-wasm repo (`/home/user/typed-wasm`) | `cargo test` passes 197 (default features) or 209 (all features). Clippy is clean. All 6 examples build and verify. `tw build` silently stubs bodies it cannot lower (`twice(5)=0`, `parser.rs` ~L895) and the result is VERIFIED. No L5 index guard is emitted: `get_player_hp(0,150)` returns 0. Malformed `session` blocks are accepted. No capabilities carrier is emitted. `tests/e2e.sh` reports 47 passed with 8 skipped (idris2, zig, parser), which is a silent green. Codegen output does not export memory, so multi-module sharing is unexercised. -| L2, L13-imports and L15 sit behind `unstable-*` features, so the default `tw-verify` build skips them. An unknown carrier version returns `Ok(vec![])` (`verify.rs:880,967`). An unknown ownership byte decodes to Unrestricted. The 33 Idris2 modules fail under Idris2 0.7.0 at one base-library API change (`Region.idr:179`); with that token adapted in a scratch copy all 33 build, the 13 reject fixtures fail as expected, and 269 table rows check. The pinned 0.8.0 build was not run. `verifierIsSound` is vacuous as a claim about the Rust verifier, because each `VerifierAccepts` constructor already holds the spec witness. `MkAttestation` is public, so attestations can be forged. `Proofs.idr` attests L11 and L12 as proven while `LEVEL-STATUS` calls them draft. The "ECHIDNA 10^5" and "88/88 parser tests" claims cannot be reproduced: `Parser.mjs` is absent and `src/parser/*.affine` does not parse. +| L2, L13-imports and L15 sit behind `unstable-*` features, so the default `tw-verify` build skips them. An unknown carrier version returns `Ok(vec![])` (`verify.rs:880,967`). An unknown ownership byte decodes to Unrestricted. The 33 Idris2 modules fail under Idris2 0.7.0 at one base-library API change (`Region.idr:179`); with that token adapted in a scratch copy all 33 build, the 13 reject fixtures fail as expected, and 269 table rows check. Under the pinned Idris2 0.8.0 (`15a3e4e`, built from source 2026-11-09) the unmodified tree passes `tools/check-kernel-proofs.sh` in full: 33 modules with no `Error:` line, no `believe_me`/`assert_total`/`assert_smaller`/`idris_crash`, 13 rejections for the expected reason, the explorer reproducing all 197 rows of `ops.tsv`, 269 equalities accepted by both Agda and Idris2, and 4 wrong rows refused by both. The `Region.idr:179` failure is a 0.7.0 incompatibility only. `verifierIsSound` is vacuous as a claim about the Rust verifier, because each `VerifierAccepts` constructor already holds the spec witness. `MkAttestation` is public, so attestations can be forged. `Proofs.idr` attests L11 and L12 as proven while `LEVEL-STATUS` calls them draft. The "ECHIDNA 10^5" and "88/88 parser tests" claims cannot be reproduced: `Parser.mjs` is absent and `src/parser/*.affine` does not parse. | No L8, L9, L14 or L16 carriers. No wasmtime gate adapter. No WasmCert tie-back. | Coq `formal/` (20 files) @@ -153,12 +153,12 @@ Results were consistent, but they do not prove CI is green. | absolute-zero | The 4 active Agda modules type-check, including under the canonical flags with stdlib 1.7.3 (its CI) and 2.3 (what echo-types uses). The Z3 OND checks pass. The archived Coq tree is 17/17 closed. `src/whitespace` has 1 failing test. -| The Idris ABI builds under Idris2 0.7.0 (the repo pins 0.8.0 through a pack image). It has five `believe_me`: `Layout.idr:270` and `Proofs/DivMod.idr:92,104,114,124`. All five statements are true and provable, so those rows are ASSUMED, not PROVEN. `HasSize` and `HasAlignment` carry no information, so the size and alignment claims are vacuous. `PROOF-STATUS` and `wiki/ABI.md` overclaim on both points. In the Agda CNO, the termination and thermodynamic parts are vacuous. +| The Idris ABI builds under Idris2 0.7.0 and under the Idris2 0.8.0 release (4 modules, no `Error:` line). CI pins a digest of the `idris2-pack` image instead; its install path names Idris2 commit `6ca00e72…` on `main` (reported version 0.8.0), not the v0.8.0 tag, and that image was not run here. It has five `believe_me`: `Layout.idr:270` and `Proofs/DivMod.idr:92,104,114,124`. All five statements are true and provable, so those rows are ASSUMED, not PROVEN. `HasSize` and `HasAlignment` carry no information, so the size and alignment claims are vacuous. `PROOF-STATUS` and `wiki/ABI.md` overclaim on both points. In the Agda CNO, the termination and thermodynamic parts are vacuous. | — | januskey | 135 tests pass. The Agda kernel and 4 reject fixtures pass against resource-algebra `cf9235c`. -| The Idris ABI type-checks under Idris2 0.7.0 (4 modules) and its 3 reject fixtures fail as expected. `seqCNO` and `tamperBreaksLink` hold for the Idris model only, which the repo states honestly. The Zig C ABI is a stub (9 `TODO(#155)` sites). T-8 is non-atomic. +| The Idris ABI type-checks under Idris2 0.7.0 and the 0.8.0 release (4 modules, no `Error:` line), and `scripts/check-idris-reject.sh` refuses its 3 reject fixtures for the expected reason under both. A planted well-typed fixture makes that script fail, so it fails closed. CI runs the same `idris2-pack` image digest as absolute-zero (Idris2 `main` at `6ca00e72…`, not the v0.8.0 tag), which was not run here. `seqCNO` and `tamperBreaksLink` hold for the Idris model only, which the repo states honestly. The Zig C ABI is a stub (9 `TODO(#155)` sites). T-8 is non-atomic. | No AffineScript seam today. | stdlib and aLib @@ -856,9 +856,9 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness * Scope: all repos, read-only. * Isolation: one container image snapshot, recorded so later workflows can reuse it. * Gates: the M0 commands; `cd $TW && cargo test --workspace --all-features`; Coq gate `just -f $AS/formal/justfile check` plus a generated `Print Assumptions` over every assertion; every Agda theory entrypoint under exactly `agda --safe --without-K --cubical-compatible`. Record each entrypoint's mode: a file-pragma `--cubical` still passes that command line, so a cubical module counts only under a separately reviewed proof profile, and that obligation stays open until the review is recorded. -* Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, then `cd Idris2 && make bootstrap SCHEME=chezscheme && make install PREFIX=/opt/idris2`. Put `/opt/idris2/bin` on `PATH` for every later step and agent (`export PATH=/opt/idris2/bin:$PATH`), so direct checks and `tools/check-proofs.sh` find it. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, has not been built in a sandbox. +* Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, then `cd Idris2 && make bootstrap SCHEME=chezscheme PREFIX=/opt/idris2 && make install PREFIX=/opt/idris2`. Pass `PREFIX` to `make bootstrap` as well as to `make install`: the prefix is compiled into the binary, and without it the libraries land in `$HOME/.idris2` while the Chez support files land under the prefix. Such an install type-checks but cannot run `--exec` or compiled programs, and still exits 0 (reproduced 2026-11-09). Put `/opt/idris2/bin` on `PATH` for every later step and agent (`export PATH=/opt/idris2/bin:$PATH`), so direct checks and `tools/check-proofs.sh` find it. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, builds the same way from commit `15a3e4e70843f7a34100f6470c04b791330788df` (verified 2026-11-09, about 25 minutes), also as a §6 deviation; with `PREFIX` given to both steps, typed-wasm's `tools/check-kernel-proofs.sh` passes with no other environment set. * Lean: install the pinned toolchain from `releases.lean-lang.org` (`curl -sSLO https://releases.lean-lang.org/lean4/v/lean--linux.tar.zst`, extract with `tar --zstd`), and record its SHA-256 as a PROOF-POLICY §6 deviation. The owner approved this on 2026-11-09. GitHub release downloads stay blocked, so elan is not the route. -* Treat an Idris2 `--check` exit code of 0 as a pass only when its output also contains no `Error:` line. +* Treat an Idris2 exit code of 0 as a pass only when its output also contains no `Error:`, `INTERNAL ERROR` or `Exception` line. This holds for `--check` with a missing import and for `--exec` and compiled programs when the Chez support files are missing (both reproduced 2026-11-09). A gate that runs a compiled program must compare its output, not only its exit code. * Stop if: a pinned prover cannot be provisioned. Record the leg as unavailable and continue with the others. * Output: a versioned toolchain manifest, kept out of the repo root. @@ -1007,7 +1007,8 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150 * [ ] januskey: T-1..T-3 are engineering statements proved in Agda with no §4 exception recorded. * [ ] Estate-wide: Idris2 0.7.0 `--check` exits 0 when an import is missing. Every Idris2 gate in the estate that trusts only the exit code can pass falsely. This belongs in `standards` (a gate rule) and in each repo's check script. * [ ] absolute-zero: discharge or name the five `believe_me` lemmas as axioms, give `HasSize` and `HasAlignment` real content, and correct `PROOF-STATUS` and `wiki/ABI.md`. -* [ ] typed-wasm: make `MkAttestation` private, reconcile `Proofs.idr` with `LEVEL-STATUS` on L11 and L12, refresh the stale `PROOF-NEEDS` module counts, and fix the e2e Idris job's 404 tarball URL. Confirm the `Region.idr` build under the pinned Idris2 0.8.0. +* [ ] typed-wasm: make `MkAttestation` private, reconcile `Proofs.idr` with `LEVEL-STATUS` on L11 and L12, refresh the stale `PROOF-NEEDS` module counts, and fix the e2e Idris job's 404 tarball URL. (The `Region.idr` build under the pinned Idris2 0.8.0 is confirmed: the full kernel-proof gate passes, 2026-11-09.) +* [ ] Estate: the Idris2 repos check against two different compilers. typed-wasm pins the v0.8.0 tag (`15a3e4e`); januskey and absolute-zero pin an `idris2-pack` image whose Idris2 is a later `main` commit (`6ca00e72…`, also reporting 0.8.0); anytype pins 0.7.0. A pass under one does not carry to another. Pick one pinned compiler per proof tier and record it in each repo's deed. * [ ] Every repo above that installs a prover outside Guix or its container needs a PROOF-POLICY §6 deviation record. None has one (anytype's tarball has no digest check; typell's install is unpinned). * [ ] mathesis: the catalogue rows for this plan's repos were refreshed with a new merge mode for the census, and these repos were added as reconciliation targets (mathesis PR). The theorem-level claims registry is still unbuilt there. * [ ] Issue trackers: update #563, #513, #553, #555, #601 and #623. These are outward-facing; confirm before posting.