diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 5a4abd9..ad666ca 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -1,12 +1,15 @@ # SPDX-License-Identifier: MPL-2.0 # STATE.a2ml — Project state checkpoint -# Last updated: 2026-06-12 (governance checkpoint; previous: 2026-04-04 CRG C complete) +# Last updated: 2026-07-29 (CI-reality checkpoint; previous: 2026-06-12 governance) +# +# Human-readable counterpart: docs/STATE-OF-PLAY-2026-07-29.adoc [metadata] project = "maa-framework" version = "0.1.0" -last-updated = "2026-06-12" -status = "CRG C compliance achieved; estate-standardized governance layer landed" +last-updated = "2026-07-29" +status = "CI is genuinely green and each gate is proven falsifiable; aletheia CLI incomplete and blocked on one design ruling" +measured-against = "measured 2026-07-29 vs origin/main 7d964ee; re-verified 2026-08-03 vs origin/main 2bf7a13 — all figures still hold" [project-context] name = "maa-framework" @@ -14,13 +17,44 @@ completion-percentage = 50 phase = "Governance & estate standardization (post-CRG-C; spec/implementation phases per ROADMAP.adoc still open)" [testing-status] -unit-tests = "26 in aletheia + 13 in brainfuck + 5 in whitespace = 44 total" -e2e-tests = "10 brainfuck interpreter E2E tests" -property-tests = "11 property-based tests (determinism, equivalence, reversibility)" -security-tests = "11 aspect tests (bounds, memory safety, input validation)" +aletheia-unit-tests = "29 pass, 0 fail (was 26; +3 for SHA-pin detection in PR #144)" +aletheia-integration-tests = "2 pass, 27 FAIL — expected; the suite specifies an unbuilt CLI (issue #124)" +aletheia-clippy = "23 findings, NOT a blocking gate (issue #125, blocked on #124)" +absolute-zero-tests = "13 brainfuck + 5 whitespace unit, 10 E2E, 11 property, 11 aspect — run in the upstream repo, not here" benchmarks = "criterion-based (absolute-zero/benches/cno_benchmarks.rs)" -test-result = "ALL PASS as of 2026-04-04 CRG C checkpoint: 39 tests absolute-zero + 26 unit tests aletheia" -note = "absolute-zero/ is a git submodule since PR #89; its tests run in the upstream repo" +test-result = "aletheia unit + fmt + zero-dep GREEN on main via root rust-ci.yml" +integration-test-caveat = "The 27 failures are NOT flaky and NOT a regression. tests/integration_tests.rs asserts on stdout SUBSTRINGS, so it is a UI contract, not a specification — every assertion can be satisfied by checks that verify nothing. Do not 'fix' it by writing checks to match the strings; see [open-questions].rsr-source-of-truth" +note = "absolute-zero/ is a git submodule since PR #89; aletheia/ is VENDORED plain files, not a submodule" + +[ci-status] +# Measured 2026-07-29 on origin/main 7d964ee +rust-ci = "PASS — build debug+release, 29 unit tests, cargo fmt, zero-dependency assertion" +governance = "PASS — 10 jobs; workflow linter and staleness both green" +codeql = "PASS" +secret-scanner = "PASS" +hypatia-scan = "PASS" +dogfood-gate = "PASS — repaired in #140/#141 by vendoring the validation scripts" +ossf-scorecard = "PASS — was dying at checkout on a stray gitlink; fixed in #145 (merged) and green on main since. NOTE: scorecard.yml triggers only on push-to-main/schedule/workflow_dispatch, NOT pull_request, so it cannot be proven on a PR." +mirror = "PASS" +boj-trigger = "PASS" +disabled-manually = "GitHub Pages (Ddraig SSG), Instant Sync, Push email notification — these report NOTHING; a green board is not full coverage" + +[gating-reality] +only-real-rust-gate = ".github/workflows/rust-ci.yml AT THE REPOSITORY ROOT (added 2026-07-21 in PR #123)" +inert-workflows = "The 16 files under aletheia/.github/workflows/ have NEVER executed. GitHub Actions reads .github/workflows/ at the repository ROOT ONLY, and aletheia/ is vendored (mode 100644), not a submodule. Editing them has no effect on CI." +cost-of-that-gap = "b5322c2 (2026-06-17) dropped a brace in aletheia/src/config.rs; main did not compile FOR OVER A MONTH because nothing was compiling it. Repaired in PR #123." +local-gates = "just build/test/fmt/lint/deps-check/check now run the same commands as CI (PR #144, closes #99). Before that every recipe echoed 'not configured yet' and exited 0." +falsifiability-proven = "just fmt exits 1 on deliberately malformed Rust while just build stays 0; reverting restores 0. A gate nobody has watched fail is not a gate." + +[proof-state] +# Measured 2026-07-29 against absolute-zero @87902bb7 +admitted-count = 0 +axiom-count = 23 +axiom-files = "physics/LandauerDerivation.v (6), quantum/QuantumCNO.v (6), common/StatMechBasis.v (5), physics/StatMech.v (3), common/PhysicsConstants.v (2), lambda/LambdaCNO.v (1)" +falsified-claim = "PROOF-NEEDS.md previously claimed '1 Admitted in LambdaCNO.v'. There are ZERO. y_not_cno is a KEPT AXIOM with a written rationale. The claim was wrong in BOTH directions — it overstated the incompleteness and understated the trusted base 23x. Corrected in PR #144." +gate-implication = "An Axiom PASSES a 'no sorry / no Admitted' gate silently. Counting only Admitted measures the wrong thing; any proof gate here must scan for Axiom too." +authoritative-record = "The in-source AXIOM AUDIT at the end of proofs/coq/physics/LandauerDerivation.v, NOT PROOF-NEEDS.md. It is self-critical: it records that cno_zero_energy_dissipation_derived is an axiom DESPITE its _derived name, and that the triage docs' DISCHARGE marks are inaccurate." +urgent-proof-item = "NOT y_not_cno. The audit's own SOUNDNESS WARNINGS: prob_nonneg and prob_normalized are false over unconstrained function-type distributions, and shannon_entropy_maximum's inequality is BACKWARDS. All three currently UNUSED — cheap now, expensive later." [crg-compliance] tier = "C" @@ -39,12 +73,51 @@ docs = "CHANGELOG.md seeded, Keep-a-Changelog format (#81); docs-template/ skele dependabot = "actions bumps #59-#69, #92-#96 (checkout, artifacts, codeql-action, rust-toolchain, trufflehog, cache, pages)" estate-standardization = "2026-06-12: merged estate-standardization-20260607 — 6a2 manifest + README, anchors/ -> 6a2/anchor/, agent_instructions/ -> bot_directives/, flat contractiles, svc/k9 -> self-validating/, GOVERNANCE.adoc, Guix manifest.scm replaces flake.nix; codeql cron weekly -> monthly cherry-picked (standards#288)" +[recent-work-2026-07] +# The CI repair campaign, 2026-07-21..29. All merged unless noted. +pr-123 = "aletheia had not compiled since 2026-06-17 (dropped brace) — repaired, and root rust-ci.yml added: the first real Rust gate this repo has ever had" +pr-128 = "SHA-pinned the four unpinned actions in pages.yml (missed the #123 squash by 10 minutes; relanded)" +pr-139 = "removed the unrunnable SonarCloud step that was breaking Governance AND CodeQL" +pr-140-141 = "validate-action repos had been deleted upstream; validation scripts vendored, Dogfood Gate green again" +pr-142 = "repointed codeql-action at a SHA that exists — BUT was a `git commit -a` on a dirty tree and carried TWO unrelated defects onto main (see [incidents])" +pr-143 = "restored guix.scm identity + licence after the squisher-corpus clobber" +pr-144 = "aletheia SHA-pin check made real; root Justfile wired (closes #99); PROOF-NEEDS.md and aletheia/CLAUDE.md corrected" +pr-145 = "removed the stray worktree gitlink breaking every recursive checkout — MERGED; OSSF Scorecard green on main since" + +[incidents] +squisher-corpus-clobber = "An automated sweep on 2026-07-26 ~16:00 BST copied hyper-repos/squisher-corpus/guix.scm BYTE-FOR-BYTE into a large number of estate repos instead of generating one per repo. Its own commit message names the bug: 'chore: update guix.scm from squisher-corpus'. Here it rewrote the package identity AND replaced MPL-2.0 with PMPL-1.0-or-later. Fixed in #143." +clobber-is-a-policy-violation = "absolute-zero/.claude/CLAUDE.md lists PMPL-1.0 / PMPL-1.0-or-later under BANNED ('License: MPL-2.0 only'), and [recent-work].license-migration below records an estate-wide migration AWAY from PMPL to MPL-2.0. The licence half was a policy violation, not merely an error." +stray-worktree-gitlink = ".claude/worktrees/maa-ci-repair was committed as a gitlink (mode 160000) with NO .gitmodules entry. Git refuses: 'fatal: No url found for submodule path ... in .gitmodules'. This broke OSSF Scorecard AT CHECKOUT, before a single probe ran, and breaks any recursive clone. Fixed in #145; .claude/worktrees/ now gitignored." +gitlink-shape-is-a-repeat = "639f389 (2026-02-21) left aletheia as a gitlink with no .gitmodules entry. A gitlink WITHOUT its mapping resolves to a silently-empty directory — git's quietest failure — and went unnoticed for over a month." +dead-sha-pin-check = "aletheia's own Silver-level 'GitHub Actions SHA pinning' check used `line.contains(\"@v\") && !line.contains(\"@\")`, which is UNSATISFIABLE — every repo passed unconditionally, including this one while it carried the unpinned @master action that had broken Governance and CodeQL. Fixed with 3 tests in #144." + +[open-questions] +# These need a human ruling; they are not research tasks. +rsr-source-of-truth = "BLOCKS #124 AND #125. What defines RSR compliance — hypatia's rsr-conformance oracle, a spec in standards, or aletheia's integration tests? If the oracle is canonical, the honest answer may be for aletheia to CONSUME it and DELETE the aspirational tests rather than build to their strings." +absolute-zero-pin = "Is 87902bb7 the intended CNO state? The re-pin was a SEMANTIC BUMP, not a restore — the original pin ad085baa was orphaned by an upstream force-push and its content is unrecoverable, so this cannot be verified from inside the repo." +submodule-or-vendored = "Settle permanently. The repo has oscillated three times (#89 -> bef4c92 -> #117). While absolute-zero accepts force-pushes to main, ANY pin will be orphaned again by the next rollout." +aletheia-licence = "Is PR #135's move of aletheia to PMPL-1.0-or-later + CC-BY-SA-4.0 intended? It runs against the written ban noted in [incidents].clobber-is-a-policy-violation." + [blockers] spec-uploads = "ROADMAP Phase 1 (specification documents for framework, Oblibeny, Aletheia) not yet uploaded" -proof-debt = "upstream proof debt recorded in docs/proof-debt.md and docs/tech-debt-2026-05-26.md (80 Coq Axiom/Admitted + 54 Lean sorry/axiom markers across 25 files, all vendored/submodule scope)" -root-justfile = "root Justfile build/test/fmt/lint recipes are placeholders; real builds live in aletheia/ (cargo)" +proof-debt = "See [proof-state]. Note the older figure in docs/proof-debt.md (80 Coq Axiom/Admitted + 54 Lean markers) is ESTATE/vendored scope; absolute-zero itself measures 0 Admitted + 23 Axiom as of 2026-07-29." +aletheia-cli = "issue #124 — 27/29 integration tests fail; blocked on [open-questions].rsr-source-of-truth" +aletheia-clippy = "issue #125 — 23 findings; blocked on #124 because the dead code IS the missing feature" [next-actions] +resolve-rsr-source-of-truth = "Answer [open-questions].rsr-source-of-truth — it unblocks both #124 and #125" +empty-merged-prs = "#146 (ci(codeql) cron weekly->monthly) and #147 (Worktree maa ci repair) are BOTH EMPTY — git diff between parent and merge is blank. #146 stated change was already present. A merged PR title is not evidence the change happened; check git diff --stat." +soundness-axioms = "Fix or delete prob_nonneg, prob_normalized, shannon_entropy_maximum while they are still unused" changelog-automation = "adopt changelog-reusable.yml (standards#206) so CHANGELOG.md stays in sync" hypatia-ignore-prune = "drop stale aletheia/examples/SafeDOMExample.res entry (file deleted in #74); migrate demo exemptions per .hypatia-ignore TODO 2026-Q3" submodule-docs = "document `git submodule update --init` for absolute-zero/ in QUICKSTART-DEV" + +[landmines] +root-only-workflows = "GitHub Actions reads .github/workflows/ at the repository ROOT ONLY. The 16 files under aletheia/.github/workflows/ are inert." +merged-pr-is-not-landed-work = "A push to a branch whose PR has ALREADY merged fires no pull_request event and produces ZERO runs, with no error. Verify by comparing each run's headSha against `git rev-parse HEAD`." +early-exit-linter = "The Governance workflow linter exits after its SPDX/permissions block, BEFORE the SHA-pin check. Fixing the first defect REVEALS the second; expect the bar to stay red." +gh-pr-checks-hides-startup-failure = "A parse-rejected or policy-rejected workflow produces NO check run at all. Use `gh run list --json conclusion`." +generic-summary-is-not-detection = "The staleness job prints 'Remove legacy scorecard-enforcer.yml' on ANY failure regardless of whether that file exists. Only ##[error] lines naming a path are real." +never-commit-dash-a = "Two separate defects reached main in one `git commit -a` (#142). Never use it in this repo." +never-allow-dead-code = "Do not silence #125 with #![allow(dead_code)]. The dead code is the specification of the missing feature, and rust-ci.yml's header forbids it." +never-restore-aletheia-from-mirror = "The in-tree copy is AHEAD — 134 tracked files vs 108, 45 in-tree only. The mirrors' only unique asset is 62 commits of history to 2026-01-03." diff --git a/README.md b/README.md index 91febbe..c976077 100644 --- a/README.md +++ b/README.md @@ -29,6 +29,30 @@ secure, and sustainable systems. > Detailed specification documents will be uploaded as development > progresses. +**Current state (2026-07-29):** CI is green across every enabled workflow, and +each gate has been shown capable of failing. `aletheia` builds, passes 29 unit +tests, is formatted, and has zero dependencies — enforced by +`.github/workflows/rust-ci.yml`, the repository's first real Rust gate (added +2026-07-21). + +Two known gaps, both in `aletheia` and both blocked on one design ruling: + +| Issue | Gap | +|----|----| +| [#124](https://github.com/hyperpolymath/maa-framework/issues/124) | The CLI surface is unbuilt — `main.rs` wires 3 checks; the integration suite specifies far more. 27 of 29 integration tests fail **by design**, not by regression. | +| [#125](https://github.com/hyperpolymath/maa-framework/issues/125) | 23 clippy findings, mostly dead code that exists *because* of #124. Not yet a blocking gate. | + +> [!WARNING] +> **`aletheia/.github/workflows/` is inert.** GitHub Actions reads +> `.github/workflows/` at the *repository root only*, and `aletheia/` is +> vendored as plain tracked files rather than a submodule. Those 16 workflow +> files have never executed. Add gates at the root, not there. + +📄 **Full measured snapshot: [`docs/STATE-OF-PLAY-2026-07-29.adoc`](docs/STATE-OF-PLAY-2026-07-29.adoc)** +— CI status, what is actually gated, proof state, open questions, and the +landmines to read before changing CI or history here. Machine-readable +counterpart: [`.machine_readable/6a2/STATE.a2ml`](.machine_readable/6a2/STATE.a2ml). + # Overview The MAA Framework is an integrated ecosystem comprising: diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md index 9b24acd..7950185 100644 --- a/TEST-NEEDS.md +++ b/TEST-NEEDS.md @@ -9,15 +9,42 @@ Copyright (c) Jonathan D.A. Jewell ## CRG Grade: C — ACHIEVED 2026-04-04 All CRG C requirements met across the absolute-zero crate: -- Unit tests: 44 total (26 in aletheia src, 13 brainfuck, 5 whitespace) +- Unit tests: 47 total (**29** in aletheia src, 13 brainfuck, 5 whitespace) - Smoke tests: build and self-verification pass - P2P/property-based: 11 deterministic property tests in `absolute-zero/tests/property_based.rs` (100% pass) - E2E/reflexive: 10 brainfuck interpreter E2E tests in `absolute-zero/tests/brainfuck_e2e.rs` (100% pass) - Security aspect tests: 11 tests in `absolute-zero/tests/security_aspects.rs` (100% pass) - Criterion benchmarks: `absolute-zero/benches/cno_benchmarks.rs` (compiles and runs) -Note: aletheia integration tests require a functioning binary with specific CLI output format; -those 27 tests are pre-existing failures (binary CLI output does not match expected strings). +> **Updated 2026-07-29.** aletheia unit tests went 26 → **29**: three new tests for +> SHA-pin detection (PR #144), added alongside a fix for a check that could never +> fail. One tautological `assert!(true)` was replaced with a real assertion at the +> same time. `absolute-zero/` is a submodule — its tests run in the upstream repo, +> not in this repository's CI. + +### The 27 failing aletheia integration tests + +They fail **by design, not by regression** — and the distinction matters: + +`tests/integration_tests.rs` (806 lines, 32 tests) describes a CLI that has never +been written: 16 Bronze checks plus Silver, `--help`, `--version`, `--verbose`, +`--badge`, `--init-hook`, `--format=`, HTML output. `main.rs` currently parses +`` plus `--json`/`--sarif` and wires **three** checks. + +> [!CAUTION] +> Every assertion in that suite is on a **stdout substring**, e.g. +> `assert!(stdout.contains("Bronze-level RSR compliance: ACHIEVED"))`. That pins +> the *wording* of the verdict and says nothing about what the checks must +> verify — so the whole suite can be satisfied by checks that verify nothing. +> +> **Do not "fix" these by writing checks that emit the expected strings.** That +> would invent a definition of RSR compliance and encode it as canonical, while +> a definition already exists in the estate (hypatia's `rsr-conformance` oracle). +> Tracked as issue #124, blocked on that source-of-truth ruling. + +They are deliberately **not** in the CI gate and **not** in `just test` +(`--bins` only). Adding them without resolving #124 would make the bar green by +breaking it. ## Current State diff --git a/docs/STATE-OF-PLAY-2026-07-29.adoc b/docs/STATE-OF-PLAY-2026-07-29.adoc new file mode 100644 index 0000000..113ad20 --- /dev/null +++ b/docs/STATE-OF-PLAY-2026-07-29.adoc @@ -0,0 +1,320 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += State of Play — maa-framework +:toc: macro +:toclevels: 3 +:icons: font +:revdate: 2026-07-29 + +A measured snapshot of what is real, what is gated, and what is known to be +broken. Figures were measured on 2026-07-29 against `origin/main` `7d964ee`, +and *re-verified 2026-08-03* against `origin/main` `2bf7a13` — all still hold. +Where an earlier claim turned out to be wrong it is marked *FALSIFIED* rather +than quietly dropped. + +toc::[] + +== One-paragraph summary + +`maa-framework` is the hub and governance repository for the MAA paradigm. The +microkernel implementation lives in-tree at `aletheia/` (Rust, 5 modules, zero +dependencies); the Certified Null Operation reference is a git submodule at +`absolute-zero/`. As of 2026-07-29 the CI is genuinely green for the first +time: every gate on `main` passes and, importantly, each one has been shown +capable of failing. The two significant open items are both in `aletheia` and +both blocked on a single unanswered design question, recorded in +<>. + +== CI status + +[cols="2,1,4"] +|=== +|Workflow |State |Note + +|Rust CI |PASS |build (debug+release), 29 unit tests, `cargo fmt`, zero-dependency assertion +|Governance |PASS |10 jobs; workflow linter and staleness both green +|CodeQL |PASS |`actions` language analysis +|Secret Scanner |PASS | +|Hypatia Security Scan |PASS | +|Dogfood Gate |PASS |repaired in #140/#141 by vendoring the validation scripts +|OSSF Scorecard |PASS |was dying at checkout on a stray gitlink; fixed in #145 and green on `main` since +|Mirror to Git Forges |PASS | +|BoJ Server Build Trigger |PASS | +|GitHub Pages (Ddraig SSG) |disabled |`disabled_manually`; cancelled runs are expected +|Instant Sync |disabled |`disabled_manually` +|Push email notification |disabled |`disabled_manually` +|=== + +CAUTION: A green board is not the same as full coverage. Three workflows above +are `disabled_manually`, so they report nothing at all. When reading this table, +ask what is *not* running as well as what passed. + +== What is actually gated + +The root `.github/workflows/rust-ci.yml` is the only real gate on the Rust code, +and it is recent — it was added 2026-07-21 in #123. + +[IMPORTANT] +==== +*GitHub Actions reads `.github/workflows/` at the repository root only.* + +`aletheia/` is vendored as plain tracked files (mode 100644), not a submodule. +The 16 workflow files under `aletheia/.github/workflows/` have therefore *never +executed, not once*, and there is no standalone `hyperpolymath/aletheia` repo +running them either — it was deleted around January 2026 and its content +vendored here. + +Editing anything under `aletheia/.github/workflows/` has *no effect on CI*. +==== + +That gap had a measurable cost. Commit `b5322c2` (2026-06-17) dropped a brace in +`aletheia/src/config.rs`; `main` did not compile *for over a month* and nothing +noticed, because nothing was compiling it. Repaired in #123. + +=== Local gates + +`just check` now runs the same commands as CI, in the same order: + +[source,console] +---- +just build # cargo build --locked --all-targets, then --release +just test # cargo test --locked --bins +just fmt # cargo fmt --check (fmt-fix applies) +just lint # cargo clippy --locked --all-targets +just deps-check # zero-dependency assertion, copied from rust-ci.yml +just check # all of the above +just self-verify # run aletheia against this repository +---- + +Before #144 every one of those recipes printed `"… not configured yet"` and +exited 0. + +== aletheia + +Zero dependencies, `#![forbid(unsafe_code)]`, offline-first — all three still +hold and `deps-check` enforces the first mechanically. + +[cols="3,1,4"] +|=== +|File |Lines |Contents + +|`src/main.rs` |121 |CLI entry, arg parsing, `verify_repository`, exit policy +|`src/checks.rs` |~360 |compliance checks, glob matching, SHA-pin detection +|`src/config.rs` |243 |`.aletheia.toml` loading, hand-rolled TOML parse +|`src/output.rs` |226 |human / JSON / SARIF report printing +|`src/types.rs` |89 |`ComplianceLevel`, `CheckResult`, `ComplianceReport` +|=== + +* Unit tests: *29 pass, 0 fail* +* Integration tests: *2 pass, 27 fail* — see <> +* Clippy: *23 findings*, not yet a blocking gate — see <> + +=== The CLI is unfinished — issue #124 [[issue-124]] + +`main.rs` parses only `` plus `--json` / `--sarif`, and wires *three* +checks. `tests/integration_tests.rs` is 806 lines / 32 tests describing a much +larger tool: 16 Bronze checks plus Silver, `--help`, `--version`, `--verbose`, +`--badge`, `--init-hook`, `--format=`, HTML output. + +This is *writing, not wiring*. The functionality has never been written. + +[WARNING] +==== +Those tests assert on *stdout substrings*: + +[source,rust] +---- +assert!(stdout.contains("Bronze-level RSR compliance: ACHIEVED")) +---- + +That pins the *wording* of the verdict and says nothing about what the checks +must verify — so every assertion can be satisfied by checks that verify nothing. +Treat the suite as a UI contract, not a specification. + +There is also a duplication risk: a definition of RSR conformance already exists +in the estate (hypatia's `rsr-conformance` oracle). Building to these strings +would create a second, divergent definition. +==== + +=== Clippy — issue #125 [[issue-125]] + +Most of the 23 findings are dead code that exists *because* the modules in +<> are unwired. Deleting it removes what #124 needs; suppressing it +with `#![allow(dead_code)]` is forbidden by the `rust-ci.yml` header. *#125 is +therefore blocked on #124* — same decision, not two. + +When #125 closes, `-D warnings` must be added to `Justfile` *and* `rust-ci.yml` +in the same change, so local and CI never disagree about what "lint passes" +means. + +== Proof state + +Measured against `absolute-zero @87902bb7`: + +[source,console] +---- +$ grep -rn "Admitted" absolute-zero --include=*.v | wc -l +0 +$ grep -rn "^Axiom" absolute-zero --include=*.v | wc -l +23 +---- + +*FALSIFIED:* `PROOF-NEEDS.md` previously claimed *"1 `Admitted` in +`LambdaCNO.v`"*. There are *zero*. `y_not_cno` is a *KEPT AXIOM* with a written +rationale. The old wording was wrong in both directions — it overstated the +incompleteness and understated the trusted base 23×. + +[IMPORTANT] +==== +An `Axiom` *passes* a "no `sorry` / no `Admitted`" gate silently. Counting only +`Admitted` measures the wrong thing. Any proof gate for this repo must scan for +`Axiom` too. +==== + +The Coq is considerably better than its own summary document was. The *AXIOM +AUDIT* at the end of `proofs/coq/physics/LandauerDerivation.v` classifies every +axiom, and is self-critical: it records that +`cno_zero_energy_dissipation_derived` is an axiom *despite its `_derived` name*, +and that the triage docs' "DISCHARGE" marks on two axioms are inaccurate. + +The genuinely urgent proof item is not `y_not_cno`. It is the audit's own +*SOUNDNESS WARNINGS*: `prob_nonneg` and `prob_normalized` are false over +unconstrained function-type distributions, and `shannon_entropy_maximum`'s +inequality is *backwards*. All three are currently *unused* — cheap to fix now, +expensive to discover later. + +== Recent incidents worth knowing about + +=== The `squisher-corpus` clobber + +An automated sweep on 2026-07-26 ~16:00 BST copied +`hyper-repos/squisher-corpus/guix.scm` *byte-for-byte* into a large number of +estate repos instead of generating one per repo. The sweep's own commit message +names the bug: `chore: update guix.scm from squisher-corpus`. + +In this repository it rewrote the package identity to `squisher-corpus` *and* +replaced the licence `MPL-2.0` with `PMPL-1.0-or-later`. Restored in #143. + +Two things make this more than cosmetic: + +. `absolute-zero/.claude/CLAUDE.md` lists `PMPL-1.0` / `PMPL-1.0-or-later` under + *BANNED* — "License: MPL-2.0 only". `STATE.a2ml` separately records an + estate-wide migration *away* from PMPL to MPL-2.0. So the licence half was a + policy violation, not merely an error. +. It reached `origin/main` *after* the local copy had already been cleaned, via + #142 — an unrelated CI fix that swept up a dirty working-tree file. + +=== One careless `commit -a`, two defects + +#142 carried *two* unrelated broken things onto `main`: the `guix.scm` clobber +above, and `.claude/worktrees/maa-ci-repair` committed as a *gitlink* (mode +160000) with no `.gitmodules` entry. The latter breaks every recursive checkout: + +---- +fatal: No url found for submodule path '.claude/worktrees/maa-ci-repair' in .gitmodules +---- + +That is what was failing OSSF Scorecard — it died at checkout, before running a +single probe. Fixed in #145, with `.claude/worktrees/` added to `.gitignore`; +Scorecard has been green on `main` since. + +TIP: Scorecard could not be proven on the pull request, because `scorecard.yml` +triggers only on `push` to `main`, `schedule` and `workflow_dispatch` — not on +`pull_request`. The fix was verified locally instead (`git submodule status` +exits 0 listing only `absolute-zero`) and confirmed on `main` after merge. + +NOTE: This repository has been bitten by this exact shape before. `639f389` +(2026-02-21) left `aletheia` as a gitlink with no `.gitmodules` entry. A gitlink +*without* its mapping resolves to a silently-empty directory — git's quietest +failure mode — and that one went unnoticed for over a month. + +=== aletheia's SHA-pinning check could never fail + +[source,rust] +---- +if line.contains("@v") && !line.contains("@") { // unsatisfiable +---- + +`contains("@v")` implies `contains("@")`, so the second clause is always false +and the "unpinned" flag could never be set. Every repository passed the +Silver-level *GitHub Actions SHA pinning* check unconditionally — including this +one, while it carried `SonarSource/sonarqube-scan-action@master`, the very +unpinned action that had broken Governance and CodeQL. Fixed with a real +implementation and three tests in #144. + +== Open questions [[open-questions]] + +These need a human ruling. They are not research tasks. + +. *What is the source of truth for RSR compliance checks?* hypatia's + `rsr-conformance` oracle, a spec in `standards`, or aletheia's integration + tests? This blocks both #124 and #125. If the oracle is canonical, the honest + answer may be for aletheia to consume it and delete the aspirational tests. +. *Is `87902bb7` the intended `absolute-zero` CNO state?* The re-pin was a + semantic bump, not a restore — the original pin `ad085baa` was orphaned by an + upstream force-push and its content is unrecoverable, so this cannot be + verified from inside the repo. +. *Submodule or vendored, permanently?* The repo has oscillated three times + (#89 → `bef4c92` → #117). While `absolute-zero` accepts force-pushes to `main`, + any pin will be orphaned again by the next rollout. +. *Is aletheia's move to PMPL-1.0-or-later + CC-BY-SA (#135) intended?* It runs + against the written ban noted above. + +== Open issues + +[cols="1,4,2"] +|=== +|Issue |Summary |Status + +|#124 |aletheia CLI surface missing; 27/29 integration tests fail |awaiting ruling (question 1) +|#125 |clippy `-D warnings`, 23 findings |blocked on #124 +|#102 |duplicate Justfiles — decide canonical |open; confirmed real by the mirror diff +|#101 |`instant-sync.yml` lacks `FARM_DISPATCH_TOKEN` presence gate |open +|#100 |adopt `changelog-reusable.yml` (standards#206) |open +|#98 |prune stale `.hypatia-ignore`; migrate 2026-Q3 exemptions |open +|=== + +Closed 2026-07-29: *#99* — root `Justfile` wired to real cargo targets (#144). + +== Landmines + +Read before changing CI or history here. + +. *Root-only workflow discovery.* The 16 files under + `aletheia/.github/workflows/` are inert. Fixes applied there do nothing. +. *A merged PR is not landed work.* #123 squash-merged while a follow-up commit + was in flight; the commit was authored ten minutes after the merge head and + belonged to nothing. A push to a branch whose PR has already merged fires no + `pull_request` event and produces *zero runs, with no error*. Verify by + comparing each run's `headSha` against `git rev-parse HEAD`. +. *A merged PR can also change nothing at all.* Both #146 (`ci(codeql): cron + weekly→monthly`) and #147 (`Worktree maa ci repair`) are *empty* — `git diff` + between their parents and merge commits is completely blank. #146's stated + change was already present (`cron: '0 6 1 * *'` was monthly before it merged). + A merged PR title is not evidence that the change it describes happened; + check `git diff --stat `. +. *Early-exit linters mask downstream failures.* The Governance workflow linter + accumulates failures through its SPDX/permissions block and exits *before* + reaching the SHA-pin check. Fixing the first defect *reveals* the second. +. *`gh pr checks` hides startup failures.* A parse-rejected or policy-rejected + workflow produces *no check run at all*. Use `gh run list --json conclusion`. +. *A generic remediation summary is not a detection.* The staleness job prints + "Remove legacy scorecard-enforcer.yml" on any failure, whether or not that file + exists. Only `##[error]` lines naming a path are real. +. *Never `git commit -a` here.* Two separate defects reached `main` that way in + a single commit (#142). +. *Do not silence #125 with `#![allow(dead_code)]`.* The dead code is the + specification of the missing feature. +. *Never restore `aletheia/` from a mirror.* The in-tree copy is *ahead* — 134 + tracked files versus 108, with 45 in-tree only. The mirrors' only unique asset + is 62 commits of history to 2026-01-03. + +== Provenance + +Measured 2026-07-29 against `origin/main` `7d964ee` and `absolute-zero` +`87902bb7`. Commands used: `gh run view --log-failed`, `gh run list --json +conclusion`, `git submodule status`, `git ls-tree`, `cargo test --locked`, +`cargo clippy --locked --all-targets`, `cargo fmt --check`, and `grep` counts +over `absolute-zero/**/*.v`. + +Machine-readable counterpart: `.machine_readable/6a2/STATE.a2ml`.