From 39ba08aca1604f03d9c23517cdb5160da6ad4fdc Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 3 Aug 2026 10:55:42 +0000 Subject: [PATCH] =?UTF-8?q?[ALL]=20DOCS:=20refresh=20NEXT=5FSESSION=20hand?= =?UTF-8?q?off=20=E2=80=94=20verified=20baseline,=20Rocq=209.1.1=20fix,=20?= =?UTF-8?q?corpus-gap=20pickup?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Makes the session bootstrap actually usable after the 2026-08-02 audit, and fixes the drift the audit found in this very file. STEP 2 — corrected Rocq 9.2 -> 9.1.1 (FINDING 3). The old block was wrong in three ways: version, switch package (ocaml-system.4.14.1 -> ocaml-base-compiler .4.14.2), and it omitted --disable-sandboxing, without which opam init fails in an unprivileged container. Replaced with the exact sequence run and verified end-to-end this session (built all 328 files). Records the ~25 min provisioning cost against a ~2m15s build, since that ratio is the main reason to prefer a persistent environment. STEP 3 — replaced the unverifiable baseline with measured values at a5ee2ce: 2912/0 proto, 304/0 tooling, 328/328 Coq files, Qed 12,626 / 0 / 0 / 0 / 30, corpus 64 pass of 165, 4 (not 2) expected audit-docs warnings. Flags that `--all-targets` clippy is NOT clean (FINDING 2) so the next session does not trust a claim this file used to make. Notes the 180 "Closed under the global context" reports as the strongest evidence in the repo. Adds the SBOM drift check, which was missing. STEP 4 — leads with the audit's structural conclusion: Gate C is budget-blocked on the owner-deferred REQ-28, and every other gate's remaining blocker is external too, so "close the gates" is not a viable plan. Points instead at the corpus gap with the measured failure-class breakdown (70% parse-level, 15% REQ-44(b) forward references, together 85%) and records that the forward-ref half is Rust-only, not Coq-blocked. Also notes CI is green as of a5ee2ce and that no in-repo gate checks CI status -- the blind spot that let it stay red for 8+ pushes. audit-docs.sh: exit 0, 0 discrepancies, 4 expected warnings. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_016qQCunxB3dDkhDzdmKoEmU --- NEXT_SESSION.md | 77 +++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 65 insertions(+), 12 deletions(-) diff --git a/NEXT_SESSION.md b/NEXT_SESSION.md index a097079f8..7111b3c59 100644 --- a/NEXT_SESSION.md +++ b/NEXT_SESSION.md @@ -24,14 +24,23 @@ Paranoid-Absolute Verification). metrics.json is the ONLY source of truth for co ## STEP 2 — PROVISION (nothing is pre-installed in a fresh container) - Rust 1.94.1 — pinned by rust-toolchain.toml; `cargo --version`. -- Rocq 9.2 (PRIMARY, required) via opam: +- Rocq **9.1.1** (PRIMARY, required) via opam. This exact sequence was run and + verified end-to-end on a fresh container 2026-08-02 (built all 328 files): sudo apt-get update && sudo apt-get install -y opam libgmp-dev # libgmp-dev = zarith dep - opam init --bare -y && opam switch create rocq --packages=ocaml-system.4.14.1 -y - eval $(opam env --switch=rocq) && opam install rocq-core rocq-stdlib -y --assume-depexts - NOTE: Rocq 9.2 ships the `rocq` binary (NOT `coqc`; `coqc` was removed). The + opam init --bare -y --disable-sandboxing # bubblewrap fails in an unprivileged container + opam switch create rocq ocaml-base-compiler.4.14.2 -y + eval $(opam env --switch=rocq) + opam install -y rocq-core.9.1.1 rocq-stdlib.9.1.0 --assume-depexts + NOTE: **9.1.1, not 9.2.** The Coq Makefile header says "GNUMakefile for Rocq + 9.1.1", CLAUDE.md was corrected to 9.1.1 in the thirteenth session, and the CI + job is named "Coq active build (Rocq 9.1.1)". `metrics.json` `coq.prover` still + says "Rocq 9.2" — that field is stale (recorded as FINDING 3 in Part 11) and + `audit-docs.sh` does not check the prover string. + Rocq 9.x ships the `rocq` binary (NOT `coqc`; `coqc` was removed). The Makefile is rocq-9.x-native (`$(COQBIN)rocq compile`) and `riinac verify` - detects `rocq` (fixed this session). `rocq compile` runs with only COQBIN+PATH - set (no full opam env needed) — that is what the pre-push hook relies on. + detects `rocq`. `rocq compile` runs with only COQBIN+PATH set (no full opam env + needed) — that is what the pre-push hook relies on. + Cost: ~25 min wall-clock to provision. The build itself is only ~2m15s on 4 cores. - Smoke/executable lanes (optional, unlock Gate D1): `bash scripts/provision-smoke-toolchains.sh` provisions F* 2025.12.15, TLA2Tools 1.7.4, Alloy 6.2.0, Isabelle — all verified this session (F* 3 lemmas / TLA 5 / Alloy 6 / Isabelle RIINA_CORE build pass). @@ -43,18 +52,62 @@ Paranoid-Absolute Verification). metrics.json is the ONLY source of truth for co - z3 (optional, NOT installed) — needed for SMT lane (T2f). ## STEP 3 — VERIFY BASELINE (run; capture real output; 0 regressions) +Expected values below were all measured on a fresh container at `a5ee2ce` +(2026-08-02). Re-derive them; do not copy them. - `bash scripts/audit-docs.sh` → exit 0, 0 discrepancies - (2 expected WARNs: Lean syntactic-sorry; Coq warning-status stale — see T4c) -- `bash scripts/update-proof-ledger.sh --check` → up to date + (**4** expected WARNs: Lean syntactic-sorry; pre-commit AND pre-push hooks + absent on a fresh clone; Coq warning-status stale — see T4c) +- `bash scripts/update-proof-ledger.sh --check` → "Proof ledgers are up to date." +- `bash scripts/generate-sbom.sh --check` → both SBOMs up to date - `RUST_MIN_STACK=16777216 cargo test --all --manifest-path 03_PROTO/Cargo.toml` -- `cargo test --all --manifest-path 05_TOOLING/Cargo.toml` -- `cargo clippy --all-targets -- -D warnings` (both workspaces) → clean -- `eval $(opam env --switch=rocq) && make -C 02_FORMAL/coq -j$(nproc)` → green + → **2912 passed / 0 failed / 3 ignored** +- `cargo test --all --manifest-path 05_TOOLING/Cargo.toml` → **304 / 0** +- `cargo clippy -- -D warnings` (both workspaces) → exit 0. Use THIS form — it is + what CLAUDE.md, CONTRIBUTING.md and `verify.rs::run_clippy` enforce. + **`--all-targets` is NOT clean** (4 lints in test code: + `riinac/tests/fuzz_robustness.rs:257` unnecessary_cast; + `riina-core/src/crypto/mod.rs:358/365/370` assert_eq-with-literal-bool). + Recorded as FINDING 2 in Part 11 — fix the lints or drop the claim, but do not + assume the stricter form passes. +- `eval $(opam env --switch=rocq) && make -C 02_FORMAL/coq -j$(nproc)` → exit 0, + **328/328 files**, ~2m15s on 4 cores. Then re-derive from the compiled set: + **Qed 12,626 / Admitted 0 / Abort 0 / Axiom 0 / Parameter 30**. The build emits + **180 `Print Assumptions` reports, every one "Closed under the global context"** + — that is the kernel-level axiom-freedom evidence, stronger than any grep. +- Corpus: `07_EXAMPLES` = 165 `.rii`, **64 pass `riinac check` / 101 fail**. - Confirm metrics.json counts via grep, never by copying docs. Honest claim state: Coq = mechanized; the other 9 lanes = generated/smoke (not independent verification). +- **CI is green as of `a5ee2ce`** (first green `verify` run in 8+ pushes). It had + been red because the workflow pinned `dtolnay/rust-toolchain@1.84.0` against a + 1.94.1 MSRV. No in-repo gate checks "is CI actually green" — check it yourself. ## STEP 4 — ASSESS & EXECUTE (active gate: C — Standard Library Hardening) -Gates A & B are CLOSED. Read Part 11 Gate C rows for what landed. Remaining tractable: + +**START HERE — the 2026-08-02 audit's structural conclusion (Part 11 addendum).** +Gate C's only open exit criterion is REQ-28, the external crypto audit, which the +owner DEFERRED on 2026-06-10. Gate C is therefore budget-blocked, not work-blocked, +and no session can close it. The same is true of every other gate's remaining +blocker: certification (H), an offline signing key (F), maintainer recruitment (J), +a Nix-capable runner (F). **Do not plan around "closing gates" — you will stall on +day one.** + +The highest-leverage work a session CAN finish is the corpus/language-surface gap. +Measured at `a5ee2ce`: 165 examples, 64 pass, **101 fail**, and the failures cluster +hard — 53 unexpected-token + 18 expected-identifier (**70% parse-level**), 15 +variable-not-found (**15%, the REQ-44(b) forward-reference gap**), then 5 effect / +4 expected-type / 3 type-mismatch / 1 each linearity, session, CRDT. **Those two +lanes are 85% of the gap.** REQ-44(b) is independently reproduced: a helper defined +LATER fails `riinac check` with "Variable not found"; the byte-identical program +with it defined FIRST succeeds. Per REQ-44's own de-risking note the forward-ref +half is a **Rust-only** typechecker+evaluator change, NOT Coq-blocked — the core +Coq calculus has no recursion constructor to widen, and `foundations/RecursionSafety.v` +already mechanizes the rule the implementation uses. + +Also unblocked and session-sized: Gate I's three missing documents (Language +Reference, compiler-internals doc, stability/migration policy) and Gate E's +continuous-fuzz tail. + +Read Part 11 Gate C rows for what landed. Remaining tractable: - Gate C: networking (real TCP/TLS + Coq network model); strings NFC/confusables (UAX#15/UTS#39); numeric tower BigInt/decimal/fixed-point; true 64-bit WASM (i32→i64 mixed-rep refactor — the owner previously chose the bounded ">=2^32