diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b9115f0c..f5110a58 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -361,6 +361,24 @@ jobs: test/kyaml_test.exs \ test/kyaml_conformance_test.exs + # The proof ledger's exunit rows are tested-only on these files, and + # their status is derived from this run, not typed in. The file list + # comes from the ledger, so a new exunit row is run without editing CI. + - name: Proof-ledger runtime tests (exunit lane) + env: + PROOF_RECEIPTS: /tmp/proof-receipts.jsonl + run: | + # Every test file a row names, whatever that row's lane: a row demoted + # to lane none still has its file run, so derive can see the underclaim. + mapfile -t files < <(jq -r 'select(.file | test("^test/.*\\.exs$")) | .file' verification/proof-ledger.jsonl | sort -u) + bash scripts/proof-ledger-ci.sh exunit "${files[@]}" + + - name: Ledger statuses agree with this run (exunit) + if: always() + env: + PROOF_RECEIPTS: /tmp/proof-receipts.jsonl + run: bash scripts/proof-ledger.sh derive exunit "$PROOF_RECEIPTS" + - name: Checkout the governance-pinned baseline helper uses: actions/checkout@v7.0.1 with: diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml index 9628701a..357630dd 100644 --- a/.github/workflows/verify-proofs.yml +++ b/.github/workflows/verify-proofs.yml @@ -12,11 +12,17 @@ on: - Justfile - pack.toml - verification/proofs/idris2/** - - verification/proofs/lean4/** - verification/proofs/tlaplus/** - verification/proofs/agda/** - verification/PROOF-STATUS.adoc - scripts/check-proof-status.sh + - verification/proof-ledger.jsonl + - scripts/proof-ledger.sh + - scripts/proof-ledger-ci.sh + - tests/proof-ledger-test.sh + - README.adoc + - AFFIRMATION.adoc + - EXPLAINME.adoc - scripts/check-trusted-base.sh - docs/proof-debt.adoc - test/soundness/** @@ -37,11 +43,17 @@ on: - Justfile - pack.toml - verification/proofs/idris2/** - - verification/proofs/lean4/** - verification/proofs/tlaplus/** - verification/proofs/agda/** - verification/PROOF-STATUS.adoc - scripts/check-proof-status.sh + - verification/proof-ledger.jsonl + - scripts/proof-ledger.sh + - scripts/proof-ledger-ci.sh + - tests/proof-ledger-test.sh + - README.adoc + - AFFIRMATION.adoc + - EXPLAINME.adoc - scripts/check-trusted-base.sh - docs/proof-debt.adoc - test/soundness/** @@ -80,6 +92,9 @@ jobs: env: IDRIS2_VERSION: v0.7.0 + # Receipts this job writes; the last step derives the ledger's idris2 + # and verdicts rows from them (scripts/proof-ledger.sh derive). + PROOF_RECEIPTS: /tmp/proof-receipts.jsonl steps: - name: Checkout @@ -178,8 +193,10 @@ jobs: echo "── $f ─────────────────────────────────────────────" if idris2 --check "$f"; then echo "✓ $f" + bash "$GITHUB_WORKSPACE/scripts/proof-ledger.sh" receipt idris2 pass "verification/proofs/idris2/$f" else echo "✗ $f" + bash "$GITHUB_WORKSPACE/scripts/proof-ledger.sh" receipt idris2 fail "verification/proofs/idris2/$f" failed=$((failed + 1)) fi done @@ -194,17 +211,24 @@ jobs: # live in the ABI and verify *packages*, which the per-file --check loop # never builds. Gate them here so they can't silently rot again. - name: Build the ABI proof package (Types, GraphQL, gRPC, REST, FFI, RuleEngine) - run: idris2 --build src/abi/hypatia-abi.ipkg + run: bash scripts/proof-ledger-ci.sh ipkg src/abi/hypatia-abi.ipkg - name: Build the verify package (PipelineState, Verify.Fuel) - run: idris2 --build verify/hypatia-verify.ipkg + run: bash scripts/proof-ledger-ci.sh ipkg verify/hypatia-verify.ipkg # HYP-01: Verdict.idr claims a `Sound` verdict is constructible only # from a confirming prover re-check. The typechecker is the falsifier: # tests/accept/ must be accepted, and every tests/reject/ module must be # refused at `invalid` with the diagnostic its `-- EXPECT:` line names. - name: Verdict accept/reject fixtures (HYP-01) - run: bash scripts/check-verdicts.sh + run: bash scripts/proof-ledger-ci.sh verdicts + + # The ledger is canonical, but its statuses are not typed in: every row + # in these lanes must say exactly what this run's receipts make it. An + # overclaim and a stale underclaim both fail (owner ruling 2026-11-09). + - name: Ledger statuses agree with this run (idris2, verdicts) + if: always() + run: bash scripts/proof-ledger.sh derive idris2,verdicts "$PROOF_RECEIPTS" - name: Summary if: always() @@ -219,8 +243,11 @@ jobs: done } >> "$GITHUB_STEP_SUMMARY" - lake-build: - name: lake build + # Lean is no longer a proof lane here: the engineering proofs it held moved + # to Idris2 (PROOF-POLICY section 3; verification/proofs/idris2/). It stays + # for the HYP-01 positive control, which re-runs Lean on a fixture. + lean-hole-recheck: + name: Lean hole re-check (HYP-01 control) runs-on: ubuntu-latest timeout-minutes: 20 permissions: @@ -228,25 +255,21 @@ jobs: env: ELAN_VERSION: v4.0.0 - # Pinned (not :stable) so the proofs are checked against the exact Lean - # they were verified with. Matches verification/proofs/lean4/lean-toolchain; - # bump both together. A moving :stable can break version-sensitive lemmas. + # Pinned (not :stable): tests/accept/LeanHoleRecheckSound.idr records + # the Lean version whose output it digests. LEAN_TOOLCHAIN: leanprover/lean4:v4.30.0 + PROOF_RECEIPTS: /tmp/proof-receipts.jsonl steps: - name: Checkout uses: actions/checkout@v7.0.1 - - name: Cache Lean toolchain and build + - name: Cache Lean toolchain id: cache-lean uses: actions/cache@v6.1.0 with: - path: | - ~/.elan - verification/proofs/lean4/.lake - key: lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-${{ hashFiles('verification/proofs/lean4/lakefile.lean', 'verification/proofs/lean4/*.lean') }} - restore-keys: | - lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}- + path: ~/.elan + key: lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-toolchain - name: Install elan + Lean 4 if: steps.cache-lean.outputs.cache-hit != 'true' @@ -258,33 +281,27 @@ jobs: - name: Put elan on PATH run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - - name: lake build - working-directory: verification/proofs/lean4 - run: | - set -euo pipefail - lean --version - lake --version - lake build - # HYP-01 positive control: the SoundVerdict in # tests/accept/LeanHoleRecheckSound.idr records digests of a Lean run. # Re-run Lean on the fixture from the repository root (where the # control's paths are relative to) and require both digests to match. - name: Re-check the Lean proof-hole fixture against the HYP-01 control - run: bash scripts/recheck-lean-hole.sh + run: | + set -euo pipefail + lean --version + bash scripts/proof-ledger-ci.sh leanhole + + - name: Ledger status agrees with this run (leanhole) + if: always() + run: bash scripts/proof-ledger.sh derive leanhole "$PROOF_RECEIPTS" - name: Summary if: always() run: | { - echo "## Lean proof verification" + echo "## Lean (HYP-01 positive control)" echo "" echo "- Toolchain: \`${LEAN_TOOLCHAIN}\` via elan \`${ELAN_VERSION}\`" - echo "- Proof files:" - for f in verification/proofs/lean4/*.lean; do - [ "$(basename "$f")" = "lakefile.lean" ] && continue - echo " - \`$(basename "$f")\`" - done } >> "$GITHUB_STEP_SUMMARY" # Estate PROOF-POLICY / Mathesis Grade 3 gate for the one Agda artefact: @@ -305,6 +322,7 @@ jobs: # Grade 3 receipt names an exact checker (estate PROOF-POLICY). # Deliberately not the runner's APT package, whose version floats. AGDA_VERSION: 2.8.0.2 + PROOF_RECEIPTS: /tmp/proof-receipts.jsonl steps: - name: Checkout @@ -334,7 +352,16 @@ jobs: set -euo pipefail agda --version sha256sum LogtalkMigration.agda - agda --safe --without-K --cubical-compatible LogtalkMigration.agda + if agda --safe --without-K --cubical-compatible LogtalkMigration.agda; then + bash "$GITHUB_WORKSPACE/scripts/proof-ledger.sh" receipt agda pass verification/proofs/agda/LogtalkMigration.agda -- checker="Agda $AGDA_VERSION" + else + bash "$GITHUB_WORKSPACE/scripts/proof-ledger.sh" receipt agda fail verification/proofs/agda/LogtalkMigration.agda + exit 1 + fi + + - name: Ledger statuses agree with this run (agda) + if: always() + run: bash scripts/proof-ledger.sh derive agda "$PROOF_RECEIPTS" - name: Summary if: always() @@ -355,6 +382,13 @@ jobs: permissions: contents: read timeout-minutes: 15 + env: + # Pinned: `releases/latest` moves, and the v1.8.0 tag is a rolling + # nightly. v1.7.4 is TLC 2.19 (rev 5a47802), the checker the ledger's + # KinGate bounds were measured with. + TLA2TOOLS_TAG: v1.7.4 + TLA2TOOLS_SHA256: 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 + PROOF_RECEIPTS: /tmp/proof-receipts.jsonl steps: - name: Checkout @@ -371,32 +405,29 @@ jobs: uses: actions/cache@v6.1.0 with: path: ~/.local/share/tla2tools.jar - key: tla2tools-v1.8.0 + key: tla2tools-${{ env.TLA2TOOLS_TAG }}-${{ env.TLA2TOOLS_SHA256 }} - name: Fetch tla2tools.jar if: steps.cache-tla.outputs.cache-hit != 'true' run: | + set -euo pipefail mkdir -p ~/.local/share - curl -sSL -o ~/.local/share/tla2tools.jar \ - https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar - ls -la ~/.local/share/tla2tools.jar + curl --proto '=https' -fsSL -o ~/.local/share/tla2tools.jar \ + "https://github.com/tlaplus/tlaplus/releases/download/${TLA2TOOLS_TAG}/tla2tools.jar" + - name: Verify the tla2tools.jar digest + run: echo "${TLA2TOOLS_SHA256} $HOME/.local/share/tla2tools.jar" | sha256sum -c - + + # Fails if TLC prints an error or does not declare completion; the + # receipt carries the distinct-state count and depth. - name: Model-check KinGate (H8) - working-directory: verification/proofs/tlaplus run: | - java -XX:+UseParallelGC \ - -cp "$HOME/.local/share/tla2tools.jar" tlc2.TLC \ - -workers auto -config KinGate.cfg KinGate.tla \ - | tee tlc.log - # Fail if TLC printed an error or didn't declare completion. - if grep -q "Error:" tlc.log; then - echo "::error::TLC found an invariant / property violation" - exit 1 - fi - if ! grep -q "Model checking completed. No error has been found." tlc.log; then - echo "::error::TLC did not report clean completion" - exit 1 - fi + TLA2TOOLS_JAR="$HOME/.local/share/tla2tools.jar" \ + bash scripts/proof-ledger-ci.sh tlc verification/proofs/tlaplus/KinGate.tla verification/proofs/tlaplus/KinGate.cfg + + - name: Ledger statuses agree with this run (tlc) + if: always() + run: bash scripts/proof-ledger.sh derive tlc "$PROOF_RECEIPTS" - name: Upload TLC log on failure if: failure() @@ -426,6 +457,21 @@ jobs: - name: PROOF-STATUS.adoc agrees with the tree run: bash scripts/check-proof-status.sh + # The machine ledger is canonical (README-EXPLAINME section 5): it must + # obey its rules and the tree, and the Proof Ledger table must be its + # rendering. The contracts plant each defect the check exists to catch. + - name: Proof ledger is valid and agrees with the tree + run: bash scripts/proof-ledger.sh check + + - name: Proof Ledger table is the ledger's rendering + run: bash scripts/proof-ledger.sh render --check + + - name: Every quoted census is the ledger's + run: bash scripts/proof-ledger.sh claims + + - name: Proof ledger contracts (planted defects) + run: bash tests/proof-ledger-test.sh + check-trusted-base: name: check-trusted-base runs-on: ubuntu-latest diff --git a/.machine_readable/testing/blitz.a2ml b/.machine_readable/testing/blitz.a2ml index cba82d31..25f3e6ba 100644 --- a/.machine_readable/testing/blitz.a2ml +++ b/.machine_readable/testing/blitz.a2ml @@ -267,7 +267,7 @@ evidence = [ [aspects.safety] status = "strong" -evidence = ["verification/proofs/tlaplus/", "verification/proofs/idris2/", "verification/proofs/lean4/"] +evidence = ["verification/proofs/tlaplus/", "verification/proofs/idris2/"] banned-patterns-clean = true default-total-idris = true diff --git a/.reuse/dep5 b/.reuse/dep5 index 97db7052..a06444c7 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -28,3 +28,10 @@ Comment: Verbatim `gh actions-lock` output, copied byte-for-byte from the hyperpolymath/standards .github/workflows/actions.lock at b3ce78e). These are tool-owned files: never hand-edit or reformat them; replace them with a fresh copy instead. + +Files: verification/proof-ledger.jsonl +Copyright: 2026 Jonathan D.A. Jewell +License: MPL-2.0 +Comment: The machine proof ledger: one JCS object per line, so it cannot + carry an SPDX comment. Machine-readable specification data, licensed as + code. diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 1b0b9826..7b8eee48 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -19,8 +19,16 @@ state and commitments. Companion detail: * *Guix-only builds.* Nix is retired estate-wide (owner ruling 2026-06-05); `guix.scm` / guix channels are the sole reproducible-build manifests. No `flake.nix` remains; all references reconciled. -* *The formal-proof corpus verifies and is CI-gated* across Idris 2 (v0.7.0), - Lean 4 (v4.30.0) and TLA+ — *zero escape hatches outside +* *The formal-proof corpus checks in CI* across Idris 2 (v0.7.0), + Agda (2.8.0.2, one artefact) and TLA+ (bounded TLC + model checking, which is `tested-only`, not a proof). What each artefact + proves, and how strongly, is the proof ledger + (`verification/proof-ledger.jsonl`, rendered in + `verification/PROOF-STATUS.adoc#proof-ledger`): 22 proven of 42; + 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Four of the + Lean proofs rested on the Lean kernel axioms `propext` and `Quot.sound`, + which a source scan does not see and `Lean.collectAxioms` does; they moved + to Idris2 on 2026-11-09, which has no such axioms. *Zero escape hatches outside `test/soundness/fixtures/`* (`believe_me` / `sorry` / `postulate` / `assert_total` / `admit` / `native_decide`). Re-measured 2026-09-26 over the git-tracked tree by `scripts/check-trusted-base.sh`: outside that @@ -33,9 +41,11 @@ state and commitments. Companion detail: the `check-trusted-base` CI job fails if one loses its fixture status or an un-annotated marker appears elsewhere. (An earlier revision of this sentence claimed "zero escape hatches" unscoped, which the fixture corpus - made literally false; see #831.) One obligation remains open — - neural-convergence (PageRank + ESN) — blocked only on Mathlib network - access; the handover is at `docs/proofs/HANDOVER-neural-convergence.md`. + made literally false; see #831.) The neural-convergence theorems (PageRank + and ESN) are open theory rows. They are planned in Agda over constructive + reals, without Mathlib, which PROOF-POLICY forbids; the plan is + `docs/proofs/HANDOVER-neural-convergence.adoc`. (An earlier revision called + them "blocked only on Mathlib network access".) * *The unified-api-adapter wire contract cannot silently drift.* The Zig enum, the Idris2 ABI and the Rust client are pinned to one golden source (`ffi/connectors.json`) by `test/unified-api-adapter-contract_test.exs` under diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 2a32f694..3fd75d73 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -12,6 +12,50 @@ https://semver.org/[Semantic Versioning]. === Changed +==== Proof-ledger statuses are derived from CI receipts (2026-11-09) + +* Every ledger row names its `lane`: the CI job whose receipt decides it + (`idris2`, `agda`, `verdicts`, `tlc`, `exunit`, or `none` for argued and + open rows). Each checker job writes receipts as it checks + (`scripts/proof-ledger-ci.sh`), then runs `scripts/proof-ledger.sh derive` + for its lanes. That step fails on an overclaim (the ledger stronger than + the run) and on a stale underclaim (weaker), as the owner ruled. TLC's + receipt carries its state count and depth, which the row's bounds must + match. +* `tla2tools.jar` is pinned to v1.7.4 (TLC 2.19) and its SHA-256 is + verified. CI used to fetch `releases/latest` under a cache key named + `v1.8.0`, and that tag is a rolling nightly. +* The exunit rows' test files now run in `ci.yml` on pull requests targeting + `main` or `develop`. + `retraction_test.exs` and `dispatch_manifest_test.exs` used to run only + inside the full integration suite. + +==== Lean engineering proofs move to Idris2 (2026-11-09) + +* `RateLimiting`, `BayesianUpdate`, `ParserTotality`, `PageRankInvariants` + and `ESNSpectralScaling` are now Idris2 (`verification/proofs/idris2/`, + `%default total`), theorem for theorem (PROOF-POLICY §3; owner decision). + Four of them had rested on the Lean kernel axioms `propext` and + `Quot.sound`; the ledger rows are now `proven`, which makes the census + 22 proven of 42. +* `verification/proofs/lean4/` is removed. The `lake build` job becomes + `Lean hole re-check (HYP-01 control)`, which keeps the pinned Lean only for + the verdict fixture. + +==== Proof claims follow the machine proof ledger (2026-11-09) + +* `EXPLAINME.adoc` is back at the repository root, as README-EXPLAINME + requires, and every claim in it was re-checked against the tree. It gains + a `#proof-ledger` section that cites `verification/proof-ledger.jsonl`. The + README's own overclaims are listed under its known gaps. +* README, AFFIRMATION and EXPLAINME quote the ledger's census, and + `scripts/proof-ledger.sh claims` fails CI when a quoted census and the + ledger disagree. +* The neural-convergence handover is rewritten: Agda first, over + constructive reals, with no Mathlib, which PROOF-POLICY forbids. + `docs/proofs/needs.adoc` now points at the ledger instead of keeping a + list of its own. + ==== WH013 reads steps with RE001's workflow reader (2026-11-04) RE001's reader is now its own module, `Hypatia.WorkflowYaml`, and WH013 reads diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc new file mode 100644 index 00000000..ef28226a --- /dev/null +++ b/EXPLAINME.adoc @@ -0,0 +1,293 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Hypatia — EXPLAINME +:toc: preamble +:icons: font + +This file backs each README claim with a code path and an honest caveat; read +it after the README if you want to know what is real. + +Counts were taken from the tree on 2026-11-09 with the command shown. +Volatile figures (repositories, outcomes, dispatches) are not quoted; generate +them with `mix hypatia.recipe_health`, `mix hypatia.strategy_effectiveness` +or `mix hypatia.watch`. + +== Claim-to-implementation map + +=== Symbolic rules, distilled from learning + +[quote, README.adoc] +____ +*Symbolic reasoning* — 35 Elixir rule modules producing fast, deterministic findings +____ + +[quote, README.adoc] +____ +The system learns complex patterns through neural analysis, then *distils* them into simple, +fast declarative rules that can be pre-emptively injected into new repositories, applied as +cures to existing ones, and executed without ML inference overhead. +____ + +How this is implemented:: +Pure-Elixir modules in link:lib/rules/[] behind `Hypatia.Rules` +(link:lib/rules/rules.ex[]). The escript runs them with no OTP tree and no +neural process (`app: nil` in link:mix.exs[]). + +Caveat:: +`find lib/rules -maxdepth 1 -name '*.ex' | wc -l` gives 42, not 35; the +generated link:docs/rules/catalogue.adoc[] says 41 and lacks +`structured_format`. No code path distils learned patterns into rules: +`learn_from_fix/3` and `promote_patterns/0` in link:lib/rules/learning.ex[] +have no outside callers, and `git grep RecipeGenerator` finds no caller. +The rules are hand-written. + +=== Neural learning + +[quote, README.adoc] +____ +*Neural learning* — 8 networks on a shared blackboard, learning which fixes actually stick +____ + +How this is implemented:: +Eight networks in link:lib/neural/[] (trust graph, mixture of experts, +liquid state machine, echo state, radial basis, GNN, VAE, sequence model) +run in six phases over the ETS blackboard under +link:lib/neural/coordinator.ex[], which calls the GNN, VAE and sequence +GenServers at lines 792, 865 and 869. All are plain Elixir (no Nx in +link:mix.exs[]). In link:lib/pattern_analyzer.ex[] the result can only +lower a recipe's confidence (`min/2`) or demote the finding. + +Caveat:: +PageRank convergence and the echo-state property are `open` ledger rows. +A comment in `pattern_analyzer.ex` still says "all 5 networks". + +=== Bayesian confidence and outcome feedback + +[quote, README.adoc] +____ +*Bayesian confidence* — every recipe carries a Beta-distributed confidence updated from real + outcomes, which gates whether a fix is applied automatically, proposed as a PR, or merely reported +____ + +[quote, README.adoc] +____ +Outcomes flow back through +`mix hypatia.record_outcome`, which drives the Bayesian update and, when a recipe degrades, +auto-quarantine. +____ + +How this is implemented:: +link:lib/outcome_tracker.ex[] lines 20–22 (prior strength 10, cap 0.99, +floor 0.10). Tiers 0.95 and 0.85 are in link:lib/triangle_router.ex[] +lines 24–25. `OutcomeTracker.quarantined?/2` (re-scan verification rate +below 0.30) downgrades `auto_execute` to review in +link:lib/fleet_dispatcher.ex[] line 267. + +Caveat:: +That recipe quarantine is not `Hypatia.Safety.Quarantine`, which nothing +calls (<>). The Idris2 model of the update uses natural-number +pseudo-counts, not Elixir floats. + +=== Machine-checked proofs + +[quote, README.adoc] +____ +*Machine-checked proofs* — Idris2 proofs of the ABI and the decision logic (confidence bounds, + safety-triangle routing, dispatch thresholds, quarantine, rollback, the Bayesian update and rate + limiting), one Agda model of the Logtalk-to-Elixir migration, and a TLA+ + model of the Kin gate that is model-checked on a bounded instance. The proofs are about models of + the code, not the Elixir runtime itself. Proof ledger: 22 proven of 42; 0 proven-with-postulates, + 11 tested-only, 2 argued, 7 open +____ + +How this is implemented:: +See <>. link:.github/workflows/verify-proofs.yml[] runs +`idris2 --check` per proof file, `idris2 --build` of both ipkgs, Agda in +its strict profile and TLC; Lean runs only for the HYP-01 control. + +Caveat:: +The Bayesian-update, rate-limiting, parser and neural-precondition proofs moved +from Lean to Idris2 on 2026-11-09, which removed the Lean kernel axioms +(`propext`, `Quot.sound`) four of them rested on. +The TLA+ row is `tested-only`: one bounded instance. The modelled rate +limiter is not called by any dispatch path. The census matches the ledger. + +=== The safety triangle and novelty gating + +[quote, README.adoc] +____ +Every finding is routed *Eliminate > Substitute > Control*, in that order — remove the hazard +if you can, replace it if you cannot, and only then add a control around it. +____ + +[quote, README.adoc] +____ +Unknown findings are forced to `report_only` regardless of score (novelty gating). +____ + +How this is implemented:: +link:lib/pattern_analyzer.ex[] chains `VerisimConnector`, `PatternRegistry` +and `TriangleRouter`; link:lib/dispatch_manifest.ex[] writes +`pending.jsonl`. Eliminate dispatch passes the Kin gate +(link:lib/fleet_dispatcher.ex[] lines 235, 972–983). A novel finding goes to +Control in link:lib/neural/dispatch_guard.ex[] line 69. + +Caveat:: +The ordering is proved over models (`safety-triangle`, `abi-rule-engine`, +`dispatch-strategy`), not over the Elixir router. With the coordinator down, +an action is capped at review, not report-only (line 67). + +=== Architecture table + +[quote, README.adoc] +____ +133 Elixir modules — pipeline, rules, VCL, neural, safety, web, merge orchestration +____ + +How this is implemented:: +Each README row, measured: ++ +[cols="1,2", options="header"] +|=== +| README row | Tree +| `lib/`: 133 | 154 `.ex` files (`+ls lib/**/*.ex \| wc -l+`), 180 `defmodule` +| `lib/rules/`: 35 | 42, as above +| `lib/neural/`, `lib/vcl/` | Correct +| `lib/merge_orchestration/`: 12 | Correct (one file in `kin_gate/`) +| `lib/hypatia/web/` | SARIF is link:lib/hypatia/sarif.ex[], outside `web/` +| `src/Hypatia/ABI/` | Also `Verdict`, `Retraction`; `Gen.idr` is a generator +| `ffi/zig/`: 18, 16 | Correct; pinned by link:.github/workflows/zig.yml[] +| Rust workspace | 7 members in link:Cargo.toml[] +|=== + +Caveat:: +The README links `docs/architecture/topology.md`; the file is +link:docs/architecture/topology.adoc[]. + +=== Installation, usage and the operational surface + +[quote, README.adoc] +____ +`just --list` shows all 39 recipes; `CONTRIBUTING.md` treats `just` as the canonical entry point. +____ + +[quote, README.adoc] +____ +Running the supervision tree also serves an HTML dashboard, an SSE event stream, a Prometheus +`/metrics` endpoint and a bearer-authenticated `/api/*` on port 9090. +____ + +How this is implemented:: +link:Justfile[] (with `contractile.just`), link:lib/hypatia/cli.ex[], +link:lib/mix/tasks/[]; link:mise.toml[] pins Erlang 27.3.4.4 and Elixir +1.17.3. link:lib/application.ex[] supervises 24 children (two more when +configured); link:lib/hypatia/web/router.ex[] serves `/`, `/metrics`, `/api`. + +Caveat:: +The Justfiles hold 43 recipes. `just build-all` builds Rust and Elixir only. +The CLI has six commands, not five (`secret-alerts`); there are 16 Mix +tasks, not 15. No `guix.scm` is tracked. `CONTRIBUTING.md` is in `.github/`. +`/api/*` needs a bearer token when `HYPATIA_API_BEARER_TOKEN` is set and not +empty. Otherwise only loopback clients are answered, unless +`HYPATIA_API_ALLOW_NONLOCAL=true` lets non-local clients in without a token. + +=== Project status and licence + +[quote, README.adoc] +____ +242 tests that are excluded from every run, the safety systems that are built but not yet invoked +by any dispatch path, and the CI blockage currently stopping the Rust lane. +____ + +[quote, README.adoc] +____ +Source files declare `MPL-2.0` and +documentation declares `CC-BY-SA-4.0`, both via per-file SPDX headers +____ + +How this is implemented:: +link:test/test_helper.exs[] excludes `:verisim_data`; nine test files carry +that tag. The safety modules are in link:lib/safety/[]. Every tracked +`+lib/**/*.ex+` file carries `MPL-2.0`; link:LICENSES/[] holds both texts. + +Caveat:: +The nine files hold 224 literal `test` blocks; 242 needs a `mix test` run +this audit did not make. The Rust blockage is stale: entry CI-1 of +link:docs/DEBT-REGISTER.adoc[] records the fix, visible in +link:integration/Cargo.toml[] lines 48–55. `docs/DEBT-REGISTER.md` is dead. +45 of 152 tracked `.adoc` files have no SPDX header (recorded for the owner, +not a licence change). + +== Dogfooded across the account + +[cols="1,2,2", options="header"] +|=== +| Technology / pattern | Used here | Also used in +| Idris2 ABI plus Zig C ABI | link:src/Hypatia/ABI/[], link:ffi/zig/[] +| link:https://github.com/hyperpolymath/echidna[echidna] +| Hypatia as estate scanner | link:.github/workflows/hypatia-scan.yml[] +| `hypatia-scan-reusable.yml` in + link:https://github.com/metadatastician/standards[standards], called by + echidna and gitbot-fleet +| JSONL dispatch manifests | link:lib/dispatch_manifest.ex[] +| link:https://github.com/hyperpolymath/gitbot-fleet[gitbot-fleet] + `scripts/dispatch-runner.sh` +| Machine proof ledger | link:verification/proof-ledger.jsonl[] +| README-EXPLAINME standard §5 in + link:https://github.com/metadatastician/standards[standards] +|=== + +[[known-gaps]] +== Known gaps + +[CAUTION] +==== +Safety systems are built but not wired. `Safety.RateLimiter` and +`Safety.Quarantine` have no caller in `lib/`. `BatchRollback.rollback/2` is +reached only through `Kin.Contingency.rollback_wave/2`, which nothing calls. +`SelfDiagnostics.record_dispatch_failure/0` and `record_dispatch_success/0` +have no callers, so its circuit breaker never opens. The moduledoc of +`lib/fleet_dispatcher.ex` (line 47) still names the rate limiter. +==== + +[CAUTION] +==== +README overclaims, each detailed above: learned patterns are not distilled +into rules (the promotion and recipe-generation code is never invoked); the +counts of rule modules, `lib/` modules, Just recipes, CLI commands and Mix +tasks are wrong; `just build-all` is narrower than stated; `guix.scm` is +absent; two links are dead. Excluded `:verisim_data` tests run in no +workflow (debt register T-1). +==== + +== Evidence index + +[cols="2,3", options="header"] +|=== +| Path | Proves +| `lib/pattern_analyzer.ex` | Scan, pattern, triangle, neural guard, dispatch +| `lib/neural/dispatch_guard.ex` | Novel goes to Control; no coordinator caps at review +| `lib/fleet_dispatcher.ex` | Kin gate review; recipe-quarantine downgrade +| `lib/outcome_tracker.ex` | Beta update; re-scan with `panic-attack assail` +| `lib/application.ex` | What is supervised +| `.github/workflows/zig.yml` | FFI tests run; exactly 18 `hypatia_*` exports +| `.github/workflows/verify-proofs.yml` | Idris2, Agda and TLC in CI; Lean for the HYP-01 control +| `docs/DEBT-REGISTER.adoc` | What is broken, ungated or stale +|=== + +[[proof-ledger]] +== Proof ledger + +The machine ledger link:verification/proof-ledger.jsonl[] is canonical. It is +validated by `bash scripts/proof-ledger.sh check`, and its rendered table is +in link:verification/PROOF-STATUS.adoc#proof-ledger[PROOF-STATUS.adoc]. Where +this file or the README disagrees with the ledger, the ledger wins. + +Census, from `scripts/proof-ledger.sh check`: + +[source,text] +---- +22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open. +---- + +Of the three theory rows, `logtalk-migration` is `PWG-3`; +`pagerank-convergence` and `esn-echo-state` are ungraded and `open`. diff --git a/README.adoc b/README.adoc index fbd00f90..8647158e 100644 --- a/README.adoc +++ b/README.adoc @@ -24,8 +24,12 @@ It combines: * *Neural learning* — 8 networks on a shared blackboard, learning which fixes actually stick * *Bayesian confidence* — every recipe carries a Beta-distributed confidence updated from real outcomes, which gates whether a fix is applied automatically, proposed as a PR, or merely reported -* *Machine-checked proofs* — Idris2 ABI definitions with dependent types, Lean 4 proofs of the - Bayesian update and rate-limiting properties, and a TLA+ model of the Kin gate +* *Machine-checked proofs* — Idris2 proofs of the ABI and the decision logic (confidence bounds, + safety-triangle routing, dispatch thresholds, quarantine, rollback, the Bayesian update and rate + limiting), one Agda model of the Logtalk-to-Elixir migration, and a TLA+ + model of the Kin gate that is model-checked on a bounded instance. The proofs are about models of + the code, not the Elixir runtime itself. Proof ledger: 22 proven of 42; 0 proven-with-postulates, + 11 tested-only, 2 argued, 7 open (link:EXPLAINME.adoc#proof-ledger[details]) === Core philosophy @@ -76,7 +80,7 @@ PatternRegistry ──> TriangleRouter ──> FleetDispatcher ──> DispatchM | `src/Hypatia/ABI/` | Idris2 ABI — Types, GraphQL, gRPC, REST, FFI, RuleEngine | `ffi/zig/` | Zig C ABI bridge — 18 exports + 16 protocol connectors | `adapters/ cli/ data/ fixer/ integration/` | Rust workspace -| `verification/` | Lean 4 proofs, TLA+ specs +| `verification/` | Proof ledger and proofs: Idris2, Agda, TLA+ |=== See link:docs/architecture/topology.md[docs/architecture/topology.md] for the full map. diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc deleted file mode 100644 index b384906c..00000000 --- a/docs/EXPLAINME.adoc +++ /dev/null @@ -1,139 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -= Hypatia: Neurosymbolic CI/CD Intelligence — Show Me The Receipts -:toc: -:icons: font - -The README makes claims. This file backs them up with evidence. - -== Key Claims From README - -[quote, README section "Core Philosophy"] -____ -"Dumb rules from smart learning" - -The system learns complex patterns through neural analysis, then *distills* them into simple, fast-acting declarative rules that can be pre-emptively injected into new repositories, applied as cures to existing repositories, executed without ML inference overhead, and formally verified for correctness. -____ - -*Evidence:* The learning pipeline (CLAUDE.md line 77-101) demonstrates this cycle: -1. **Learning** — 5 neural networks (Graph of Trust, Mixture of Experts, Liquid State Machine, Echo State Network, Radial Neural Network) analyze verisim-data -2. **Distillation** — PatternRegistry deduplicates findings into 46 canonical recipes (PA001-PA046 + 20 OpenSSF Scorecard recipes) -3. **Symbolic** — Recipes and checks execute as pure-Elixir rules in `lib/rules/*.ex` (no ML needed for the deterministic checks) -4. **Verification** — Idris2 ABI proofs formally verify recipe correctness - -This is proven by the metrics: 1635 dispatched actions (600 auto-execute with 95%+ confidence, 667 review, 368 report), 16,671 outcomes recorded (99% success rate), 46 recipes zero-uncovered (every category has a recipe). - -*Caveat:* The "dumb rules" are fast but not universally applicable — categories below 0.85 confidence force review (not auto-execute), and below 0.50 confidence auto-generate explanatory recipes before dispatch. - -[quote, README section "Overview" and "Safety Triangle Pipeline"] -____ -Hypatia combines: Neural Learning, Symbolic Reasoning, Formal Verification, Graph Intelligence, Distributed Cache, P2P Federation. - -The safety triangle pipeline: Eliminate > Substitute > Control -____ - -*Evidence:* The architecture (lines 49-100) shows all 6 layers implemented: -- Verification (Haskell Liquid types, property testing, formal proofs) -- Learning (neural subsystem with 5 networks) -- Symbolic (Elixir rule modules in `lib/rules/*.ex`) -- Data (ArangoDB graph, Dragonfly cache, Radicle P2P) -- Action (robot-repo-automaton, hooks, diagnostics) -- Forge adapters (6: GitHub, GitLab, Bitbucket, Codeberg, sr.ht, Gitea) - -The safety triangle (CLAUDE.md lines 53-73) routes findings through: -1. **Eliminate** — Remove root cause permanently (0 risk, lowest cost) -2. **Substitute** — Replace bad component with good alternative (medium cost/risk) -3. **Control** — Add monitoring/limits (highest cost, medium risk, reversible) - -This is operationalized in TriangleRouter, FleetDispatcher (confidence-gated), and circuit breaker safety systems. - -*Caveat:* The P2P federation (Radicle) is integrated in architecture but not deployed in production; currently uses git-backed verisim-data flat files. - -== Technology Choices - -[cols="1,2"] -|=== -| Technology | Learn More - -| **Elixir 1.16+** | https://elixir-lang.org (8 core modules, OTP GenServers, concurrency) -| **Rust** | https://www.rust-lang.org (adapters, CLI, data layer, fixer) -| **Julia 1.10+** | https://julialang.org (5 neural networks, training pipeline) -| **Elixir / OTP** | Rule modules (error catalog, pattern detection) -| **Haskell** | Formal verification (Liquid types, property testing) -| **Idris2 ABI** | https://www.idris-lang.org (type-safe GraphQL, gRPC, REST with proofs) -| **Zig FFI** | https://ziglang.org (C ABI bridge for 7 exported functions) -| **ArangoDB** | Graph database (relationship modeling) -| **Dragonfly** | Distributed cache (sub-millisecond rule lookups) -| **VeriSimDB** | Cross-modal consistency for scan data -|=== - -== Dogfooded Across The Account - -[cols="1,2,2", options="header"] -|=== -| Technology | Role in Hypatia | Also Used In - -| *Idris2 ABI* (hyperpolymath standard) -| `src/Hypatia/ABI/` — formal specs for GraphQL, gRPC, REST with dependent type proofs; `ffiReturnsApiResponse` proof in `FFI.idr` -| gossamer (`gossamer/src/interface/abi/`), burble (`burble/src/Burble/ABI/`), verisimdb, proven, typed-wasm — every repo with an FFI layer - -| *Zig FFI* (hyperpolymath standard) -| `ffi/zig/src/` — 7 C-compatible exported functions (`hypatia_health_check`, `hypatia_scan_repo`, `hypatia_dispatch`, etc.) -| gossamer (`gossamer/src/interface/ffi/`), burble (`ffi/zig/src/ffi.zig`), tangle, ephapax — same Idris2→Zig→C pattern - -| *VeriSimDB + VCL query layer* -| Built-in Elixir VCL parser + FileExecutor; queries verisim-data flat-file store; 954 patterns tracked across 298 repos -| burble (state and session storage), idaptik (game state), boj-server (scan results), nextgen-databases monorepo - -| *panic-attack* -| Re-scan verification after dispatch — confirms fixes removed weak points; `diagnostics.ex` watches for binary on `$PATH` -| Used estate-wide as pre-commit gate (`panic-attack assail`); panicbot wraps it in CI - -| *Elixir/OTP* -| 8 GenServers (VCL, RateLimiter, Quarantine, LearningScheduler, Diagnostics, Neural, Kin, Application supervisor); fault isolation -| burble (P2P voice control plane), gitbot-fleet (bot orchestration) - -| *Julia neural networks* -| 5 networks (Graph of Trust, MoE, LSM, ESN, RBF) + training pipeline from real verisim-data outcomes -| KnotTheory.jl (topology data processing), batch scripts estate-wide -|=== - -== File Map: Key Modules - -[cols="1,2"] -|=== -| Path | What's There - -| `lib/pattern_analyzer.ex` | Full pipeline orchestrator (scan → patterns → triangle → dispatch) -| `lib/verisimdb_connector.ex` | VCL queries with file I/O fallback -| `lib/pattern_registry.ex` | Deduplicates findings into 46 canonical recipes -| `lib/triangle_router.ex` | Routes through Eliminate > Substitute > Control -| `lib/fleet_dispatcher.ex` | Confidence-gated dispatch (file-based + HTTP, circuit breaker) -| `lib/dispatch_manifest.ex` | Writes JSONL manifests for bash execution layer -| `lib/outcome_tracker.ex` | Records outcomes, Bayesian confidence updating, re-scan verification -| `lib/recipe_generator.ex` | Auto-generates recipes for uncovered categories (0.50 confidence) -| `lib/scorecard_ingestor.ex` | Ingests OpenSSF Scorecard checks as patterns -| `lib/learning_scheduler.ex` | GenServer: polls outcomes, drives feedback loop -| `lib/self_diagnostics.ex` | Health monitoring, circuit breaker, auto-recovery -| `lib/neural/` | 5 networks (graph-of-trust, moe, lsm, esn, rbf) + coordinator -| `lib/vcl/` | VCL client, file executor, query functions -| `src/Hypatia/ABI/` | Idris2 specs (Types, GraphQL, gRPC, REST, FFI, RuleEngine, Gen) -| `ffi/zig/src/` | 7 C-compatible exported functions -| `adapters/ cli/ data/ fixer/ integration/` | Rust workspace (root crates) -| `proofs/agda/` | Formal verification of safety triangle correctness -|=== - -== Metrics (as of 2026-03-07) - -- 302 repos scanned (3385 weak points) -- 1635 dispatched actions (600 auto-execute, 667 review, 368 report) -- 16,671 outcomes recorded (99% success rate) -- 46 recipes (0 uncovered categories), 20 OpenSSF Scorecard recipes, 5 RSR compliance rules -- 5 neural networks + coordinator in OTP supervision -- Bayesian Beta-distribution confidence (prior_strength=10, floor=0.10, cap=0.99) -- Re-scan verification via panic-attacker -- 3 safety systems: rate limiter (50/bot/min, 200/global/min), quarantine (soft/hard/permanent), batch rollback -- VCL integrated with file executor, query cache, cross-repo analytics - -== Questions? - -Open an issue in the hyperpolymath/hypatia repository for questions about the safety triangle routing, neural network architecture, recipe distillation, or verisim-data integration for cross-repo CI/CD intelligence. diff --git a/docs/README.adoc b/docs/README.adoc index a60072ce..68badb03 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -110,7 +110,7 @@ Detailed per-surface references. For the high-level overview see link:guides/api == Reference -* link:EXPLAINME.adoc[`EXPLAINME.adoc`] — annotated tour of the codebase. +* link:../EXPLAINME.adoc[`EXPLAINME.adoc`] (repository root) — claims, evidence and the proof ledger. == History diff --git a/docs/proofs/HANDOVER-neural-convergence.adoc b/docs/proofs/HANDOVER-neural-convergence.adoc index 0efdc12c..2dca7558 100644 --- a/docs/proofs/HANDOVER-neural-convergence.adoc +++ b/docs/proofs/HANDOVER-neural-convergence.adoc @@ -1,219 +1,147 @@ -== HANDOVER — Complete the proof corpus: neural-convergence proofs (Lean 4 + Mathlib) +// SPDX-License-Identifier: CC-BY-SA-4.0 +== HANDOVER — Neural-convergence theorems: Agda first, constructive reals === Mission -Hypatia’s formal-proof corpus spans *Idris 2, Lean 4, and TLA+*. Every -existing proof verifies and is CI-gated. *One obligation is open: -neural-network convergence.* Two Lean files prove only ℕ -_preconditions_; the real analytical theorems (PageRank power-iteration -convergence; ESN echo-state stability) need *Mathlib*. This must be done -in an environment where Mathlib’s `+.olean+` cache CDN is reachable (the -Claude-on-the-web sandbox blocks it — -`+lakecache.blob.core.windows.net+` and `+mathlib4.lean-cache.cloud+` -403). Locally, with normal internet, it just works. - -=== Repo state (do not redo) - -* Branch: `+claude/hopeful-ptolemy-ZdYqp+` (proof work is merged to -`+main+`). -* #433 — made the corpus actually compile (it had never been -machine-checked). -* #434 — CI hardening: gate the Idris ABI + verify packages, pin Lean, -fix the Idris cache. -* #440 — reconciled the proof-status docs. -* Pinned toolchain: *Idris 2 `+v0.7.0+`*, *Lean `+v4.30.0+`*, TLA+ -tla2tools 2.19. Agda retired. Zero escape hatches -(`+believe_me+`/`+assert_total+`/`+postulate+`/`+sorry+`/`+Admitted+`/`+unsafeCoerce+` -= 0). - -=== The corpus (current truth) - -[width="100%",cols="34%,33%,33%",options="header",] -|=== -|Obligation |File |Status -|H1 confidence bounds -|`+verification/proofs/idris2/ConfidenceBounds.idr+` |✅ - -|H2 dispatch monotonicity -|`+verification/proofs/idris2/DispatchStrategy.idr+` |✅ - -|H3 safety-triangle order -|`+verification/proofs/idris2/SafetyTriangle.idr+` |✅ - -|H4 rate limiting |`+verification/proofs/lean4/RateLimiting.lean+` |✅ - -|H5 quarantine |`+verification/proofs/idris2/Quarantine.idr+` |✅ - -|H6 outcome-log monotonicity |`+lib/outcome_tracker.ex+` (runtime -assertion; Agda retired) |✅ - -|H7 Bayesian update |`+verification/proofs/lean4/BayesianUpdate.lean+` -|✅ - -|H8 kin-gate atomicity |`+verification/proofs/tlaplus/KinGate.tla+` |✅ - -|H9 neural consensus aggregation -|`+verification/proofs/idris2/NeuralConsensus.idr+` |✅ - -|parser totality |`+verification/proofs/lean4/ParserTotality.lean+` |✅ - -|ABI package + verify package |`+src/Hypatia/ABI/*.idr+` -(incl. `+RuleEngine.idr+`), `+verify/src/*.idr+` |✅ - -|*Neural convergence — PageRank* -|`+verification/proofs/lean4/PageRankInvariants.lean+` |⛔ preconditions -only - -|*Neural convergence — ESN* -|`+verification/proofs/lean4/ESNSpectralScaling.lean+` |⛔ preconditions -only -|=== - -=== Toolchain install (local) - -[source,bash] ----- -curl -fL https://raw.githubusercontent.com/leanprover/elan/v4.0.0/elan-init.sh | sh -s -- -y -elan toolchain install leanprover/lean4:v4.30.0 # matches the repo pin -# Idris2 v0.7.0 (only to re-verify the Idris side): chezscheme + bootstrap, or idris2-pack -# TLA+ (only to re-verify H8): Java 21 + tla2tools.jar ----- - -=== CI-hygiene design decision (read before coding) - -Do *not* add Mathlib to the existing `+verification/proofs/lean4/+` -project — it is the _fast_ gate (no deps, builds in seconds, runs every -push). Create a *separate* project -`+verification/proofs/lean4-mathlib/+` with its own `+lakefile.lean+` -(`+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.30.0"+`), -its own `+lean-toolchain+` (`+leanprover/lean4:v4.30.0+`), and the new -proof files. Gate it in a *separate cached CI job* (below). Keep the -existing ℕ-precondition files where they are. - -=== Theorem 1 — PageRank power-iteration convergence - -* New file `+PageRankConvergence.lean+` in the mathlib project. Models -`+lib/neural/graph_of_trust.ex+`. -* *Statement:* for `+xₖ₊₁ = α·P·xₖ + (1-α)·v+` with `+P+` -column-stochastic and `+0 ≤ α < 1+`, there is a unique fixed point and -the iterates converge to it. -* *Strategy:* the damped Google operator `+G(x) = α·P·x + (1-α)·v+` is a -contraction with modulus `+α+` in the ℓ¹ norm (column-stochastic ⇒ -`+‖P x‖₁ ≤ ‖x‖₁+`). Then Banach. -* *Mathlib:* `+ContractingWith+` -(`+Mathlib.Topology.MetricSpace.Contracting+`), -`+ContractingWith.fixedPoint+`, `+…fixedPoint_unique+`, -`+…tendsto_iterate_fixedPoint+`. Space `+EuclideanSpace ℝ (Fin n)+` or -`+PiLp 1+`; matrices via `+Matrix.toLin'+`. (Confirm exact lemma names -in v4.30.0.) - -=== Theorem 2 — ESN echo-state stability - -* New file `+ESNStability.lean+`. Models -`+lib/neural/echo_state_network.ex+`. -* *Frame it in the sup norm, as an ℓ∞ operator-norm contraction -(`+‖W‖∞ < 1+`), NOT as spectral radius `+ρ(W) < 1+`.* Since 2026-10 the -runtime scales the reservoir so its induced ∞-norm (largest absolute row -sum) is `+@reservoir_norm+` = 0.95; it does not compute the spectral -radius. (Before that it scaled the largest single _entry_, which bounds -neither norm: the 80-node reservoir had ρ ≈ 2 and two runs from different -initial states never converged. A proof of the old code would have been a -proof of a false claim.) `+test/neural_test.exs+` now checks both the -row-sum bound and the convergence of two initial states. -* *Statement:* for leak rate `+0 < a ≤ 1+` and `+‖W‖∞ < 1+`, the update -`+F_u(x) = (1 - a)·x + a·tanh(W·x + w·u)+` (tanh applied componentwise, -1-Lipschitz) satisfies -`+‖F_u(x) - F_u(y)‖∞ ≤ (1 - a + a·‖W‖∞)·‖x - y‖∞+` for every input `+u+`. -Corollaries: the modulus is < 1, so two trajectories under the same input -sequence approach each other geometrically (exponential forgetting of the -initial state), and a state that starts in `+[-1, 1]ⁿ+` stays there for any input. -* *Mathlib:* on `+Fin n → ℝ+` the default norm is already the sup norm, -and Mathlib has the ℓ∞ operator norm of a matrix as the max row sum -(`+Matrix.linfty_opNorm+` and friends; confirm names in v4.30.0). -`+LipschitzWith+` for the componentwise tanh (`+Real.tanh+` derivative ≤ 1), -then compose. `+ContractingWith+` is only needed for a fixed-input fixed -point; the forgetting statement is a direct induction on the step bound. - -=== Hard constraints - -* No -`+sorry+`/`+believe_me+`/`+postulate+`/`+assert_total+`/`+admit+`/`+native_decide+`. -Fully constructive. -* SPDX header on every file (`+MPL-2.0+` + the copyright line above). -* Lean stays pinned at v4.30.0; Mathlib is the `+v4.30.0+` tag (exists, -matches). -* When done: flip both rows PARTIAL→COMPLETE in -`+verification/PROOF-STATUS.md+` and `+docs/proofs/needs.md+`. - -=== CI job to add (separate, cached — parallel to `+lake-build+`, not folded in) - -[source,yaml] ----- - lake-build-mathlib: - name: lake build (mathlib) - runs-on: ubuntu-latest - timeout-minutes: 60 # `lake exe cache get` is ~5 GB - env: { LEAN_TOOLCHAIN: leanprover/lean4:v4.30.0 } - steps: - - uses: actions/checkout@ - - # install elan + Lean v4.30.0 (mirror the existing lake-build job) - - uses: actions/cache@ - with: - path: | - ~/.elan - ~/.cache/mathlib - verification/proofs/lean4-mathlib/.lake - key: mathlib-v4.30.0-${{ runner.os }}-${{ hashFiles('verification/proofs/lean4-mathlib/**/*.lean') }} - - run: cd verification/proofs/lean4-mathlib && lake exe cache get && lake build ----- - -Add `+verification/proofs/lean4-mathlib/**+` to the workflow `+paths:+` -(push + pull_request). - -=== Verify the whole corpus before finishing - -[source,bash] ----- -idris2 --build src/abi/hypatia-abi.ipkg -idris2 --build verify/hypatia-verify.ipkg -cd verification/proofs/idris2 && for f in *.idr; do idris2 --check "$f" || exit 1; done; cd - -cd verification/proofs/lean4 && lake build && cd - -cd verification/proofs/lean4-mathlib && lake exe cache get && lake build && cd - -cd verification/proofs/tlaplus && java -cp /path/tla2tools.jar tlc2.TLC -config KinGate.cfg KinGate.tla ----- - -=== Gotchas already solved (recognise these in the codebase) - -* base-0.7 renames: `+lteRefl+`→`+reflexive+`, -`+lteTransitive+`→`+transitive+`; Nat lemmas `+multRightSuccPlus+`, -`+plusLteMonotone*+`, `+lteAddRight+`. -* Lean 4.30: `+List.mem_cons_self+` has implicit args; -`+List.filter_cons+`, `+decide_eq_true_eq+`; use -`+induction … generalizing+` when the IH must hold for a changing state. -* Idris refutation of impossible equalities / empty GADTs: -`+Refl impossible+` / `+case x of _ impossible+` (no `+Uninhabited+` -instance to lean on). -* Idris reserved words used as identifiers were the bug class: `+data+`, -`+record+`, `+partial+`. -* `+src/Hypatia/ABI/*.idr+` are the real files (build namespace -`+Hypatia.ABI.*+`, reached via `+sourcedir = ".."+` in the ipkg). They were -never symlinks: `+src/abi/*.idr+` held byte-identical duplicate files that -nothing compiled, deleted 2026-09-22 (issue #815). - -=== Definition of done - -[arabic] -. Both theorems proven in Lean+Mathlib, no escape hatches, -`+lake build+` clean. -. Separate cached CI job gating them; workflow `+paths:+` updated. -. `+PROOF-STATUS.md+` + `+needs.md+` rows flipped to COMPLETE. -. Whole-corpus verification passes. -. Draft PR against `+main+`. - -=== Out of scope (other contributors) - -Repo-hygiene PR (173 medium scan findings: `+timeout-minutes+` on -`+ci.yml+`/`+clusterfuzzlite.yml+`, the `+setup-java+` SHA-pin -false-positive); `+PipelineState+`→real `+proven+` integration; -documenting the `+src/Hypatia/ABI+` layout; the `+gitbot-fleet+` / -`+.git-private-farm+` repos. +Two theory obligations are open in the proof ledger +(`+verification/proof-ledger.jsonl+`, rows `+pagerank-convergence+` and +`+esn-echo-state+`; rendered in `+verification/PROOF-STATUS.adoc#proof-ledger+`): + +* *PageRank:* the damped power iteration in `+lib/neural/graph_of_trust.ex+` + converges to a unique stationary vector. +* *ESN:* with the reservoir scaled as `+lib/neural/echo_state_network.ex+` + scales it, two state trajectories under the same input converge + geometrically (the echo-state property), and `+[-1, 1]ⁿ+` is invariant. + +Both are *theory* (PROOF-POLICY §1): the source of truth is an Agda proof, +rechecked in Rocq and Lean. The owner chose (2026-11-09) to state them over +*constructive reals*, so the theorems are the textbook ones and not +rational approximations of them. + +This supersedes the earlier version of this handover, which planned the +proofs in Lean 4 with Mathlib. PROOF-POLICY forbids Mathlib as a +dependency (§2) and puts theory in Agda first; that plan is withdrawn. The +Lean files `+PageRankInvariants.lean+` and `+ESNSpectralScaling.lean+` prove +natural-number *preconditions* only. Under PROOF-POLICY §3 they are +engineering evidence, not legs of these theorems. + +=== Constraints + +* Every file checks under the canonical invocation (PROOF-POLICY §2.1): + `+agda --safe --without-K --cubical-compatible+`, Agda `+2.8.0.2+` + (the version CI pins). No `+postulate+`, no `+--cubical+`, no + `+TERMINATING+` or other unsafe pragma. +* One dependency: agda-stdlib, pinned to a release tag and commit that + the receipt records. Feasibility checked 2026-11-09: agda-stdlib `+v2.3+` + (commit `+8326c7475af1fa456ca04a0203c168d5d7ff842b+`) loads + `+Data.Rational+` under the profile on Agda 2.8.0.2, and a Bishop-real + record over it type-checks. The first check builds the library (about two + minutes); later checks take seconds. +* No real-analysis library is assumed. The reals are built here, small and + only as far as the two theorems need. +* Hypotheses the runtime cannot discharge are *module parameters*, never + postulates. A theorem proved for every activation that is 1-Lipschitz and + bounded by 1 is a theorem; the claim that `+tanh+` is such an activation + is its own ledger row. + +=== Construction plan + +Files live in `+verification/proofs/agda/NeuralConvergence/+`. Each milestone +checks on its own and lands as its own stacked PR, with its ledger rows. + +M0 — reals (`+Reals.agda+`):: +Bishop regular sequences: `+x : ℕ → ℚ+` with +`+∣ x m - x n ∣ ≤ 1/(m+1) + 1/(n+1)+`. Equality `+x ≈ y+` iff +`+∣ x n - y n ∣ ≤ 2/(n+1)+` for all `+n+` (a setoid, not `+_≡_+`). Order, +`+_+_+`, multiplication by a rational, `+∣_∣+`, `+max+`, the triangle +inequality. Everything the theorems use carries an explicit modulus. + +M1 — completeness (`+Complete.agda+`):: +A sequence of reals that is Cauchy with an explicit modulus has a limit +(the diagonal construction), and the limit is unique up to `+_≈_+`. + +M2 — Banach, constructively (`+Contraction.agda+`):: +On `+Vec ℝ n+` under a norm with the triangle inequality, a map with a +rational modulus `+0 ≤ c < 1+` has a fixed point, it is unique, and the +iterates satisfy `+‖xₖ - x*‖ ≤ cᵏ / (1 - c) · ‖x₁ - x₀‖+`. The rate is the +modulus of convergence, so the statement is constructive by construction. + +M3 — PageRank (`+PageRank.agda+`):: +`+G(x) = α·P·x + (1 - α)·v+` with `+P+` column-sub-stochastic (non-negative +rational entries, each column summing to at most 1) and a rational +`+0 ≤ α < 1+`. `+G+` is an ℓ¹ contraction with modulus `+α+`, because such a +`+P+` gives `+‖P x‖₁ ≤ ‖x‖₁+`. Then M2. State it for sub-stochastic `+P+`, not +only stochastic: the runtime builds sub-stochastic matrices. A node with no +outgoing edge gives a zero column. `+iterate_trust/4+` in +`+lib/neural/graph_of_trust.ex+` sums every parallel edge into a source's +out-weight but takes one of them into each target, so repeated outcomes +leak mass. The theorem then covers convergence for every runtime input. The +leak changes what the fixed point means, and is a runtime defect to fix in +the runtime, not to model. *Ledger:* `+pagerank-convergence+` +becomes `+proven+` at PWG-3 once this checks in CI. + +M4 — ESN (`+EchoState.agda+`):: +`+F_u(x) = (1 - a)·x + a·σ(W·x + w·u)+` for a rational leak rate +`+0 < a ≤ 1+`, `+W+` with rational entries and induced ∞-norm (largest +absolute row sum) `+‖W‖∞ ≤ ρ < 1+`, and σ a module parameter that is +1-Lipschitz with `+∣σ t∣ ≤ 1+`. Show +`+‖F_u(x) - F_u(y)‖∞ ≤ (1 - a + a·ρ)·‖x - y‖∞+` for every input `+u+`. +Corollaries, by induction on the input sequence: two trajectories approach +each other geometrically, and `+[-1, 1]ⁿ+` is invariant. Frame it in the +∞-norm, *not* the spectral radius: the runtime has scaled by the induced +∞-norm (`+@reservoir_norm+` = 0.95) since 2026-10, and `+test/neural_test.exs+` +checks both that bound and the convergence of two initial states. +*Ledger:* `+esn-echo-state+` becomes `+proven+` at PWG-3. + +M5 — tanh (`+Tanh.agda+`), its own row:: +Construct `+tanh+` on the reals (a convergent series or continued fraction +with an explicit modulus) and prove it 1-Lipschitz and bounded by 1. Until +this lands, M4 holds for every such σ, and the row recording that `+tanh+` +is one stays `+open+`. + +=== What the theorems do not cover + +* The runtime uses IEEE floats. The theorems are about reals; the link from + them to `+lib/neural/*.ex+` is the `+models-runtime-refinement+` row, which is + `+open+` and names no evidence yet. `+test/neural_test.exs+` checks the ESN + ∞-norm bound and the convergence of two initial states; it is a candidate + for that row's evidence, not yet recorded as it. +* Matrix entries are rational in the model. The runtime's weights are + floats, every one of which is a rational, so no generality is lost there; + rounding during iteration is what the model does not see. + +=== The recheck legs (after PWG-3) + +PROOF-POLICY §2: transport each witness through Dedukti first, and re-prove +in Rocq and in Lean only where transport is unavailable. No Mathlib in the +Lean leg. A leg counts toward PWG-2i or PWG-2ii only once its statement has +been compared with the Agda statement and that comparison recorded +(`+RECONCILED+`, §2.2). Record each leg in the theory row's `+legs+` field. + +=== CI + +Add an `+agda-neural+` job beside the existing `+agda strict-profile check+` +job in `+.github/workflows/verify-proofs.yml+`. It should pin Agda +`+2.8.0.2+` and the agda-stdlib tag and commit, cache the stdlib interface +files keyed on that commit, and check every file in +`+NeuralConvergence/+` with the §2.1 invocation. A missing or failing checker +is a failure, never a skip. Its summary records what PWG-3 needs: the checker +version, the stdlib pin, the flags in force, the import cone and each +source digest (PROOF-POLICY §8.2). + +=== Definition of done (per milestone) + +. Every file in the milestone checks under the §2.1 invocation, locally and + in CI. +. `+bash scripts/proof-ledger.sh check+` passes with the rows the milestone + changes, and `+render --write+` has refreshed `+PROOF-STATUS.adoc+`. +. The PR body carries the receipt: checker version, stdlib pin, invocation, + source digests and the run that checked them. + +=== Gotchas already met + +* Agda's `+1/_+` in `+Data.Rational+` is the inverse of a rational. For + 1/(n+1) write `(+ 1) / suc n`, with the integer constructor from + `+Data.Integer+` and `+_/_+` from `+Data.Rational+`. +* Equality of reals is `+_≈_+`; every lemma about reals is up to it. + Reaching for `+_≡_+` on reals is the usual first wrong turn. diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc index dddf4b28..4332b9fd 100644 --- a/docs/proofs/gap-analysis.adoc +++ b/docs/proofs/gap-analysis.adoc @@ -1,5 +1,11 @@ == Proofs Gap Analysis +NOTE: Historical (2026-04-22), kept as the record of that analysis. Since then +the Lean engineering proofs moved to Idris2 (2026-11-09), an Agda artefact +returned, and every prover runs in CI. The current state is the proof ledger +(`+verification/proof-ledger.jsonl+`); the convergence plan is +`+docs/proofs/HANDOVER-neural-convergence.adoc+`. + *Date:* 2026-04-22 *Scope:* VCL query correctness + neural ensemble convergence *Status:* Inventory + prioritised plan. No code changes yet. diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc index 7246aaee..079917ce 100644 --- a/docs/proofs/needs.adoc +++ b/docs/proofs/needs.adoc @@ -1,96 +1,28 @@ -== PROOF-NEEDS.md — hypatia - -=== Current State (Updated 2026-06-05) - -* **src/Hypatia/ABI/*.idr**: `+Types.idr+`, `+FFI.idr+`, `+GraphQL.idr+`, -`+GRPC.idr+`, `+REST.idr+`, `+RuleEngine.idr+` — built as the -`+hypatia-abi+` package under `+--total+`. -* **verify/src/*.idr**: `+PipelineState.idr+`, `+Verify/Fuel.idr+` — -`+hypatia-verify+` package. -* *verification/proofs/idris2/*: 7 standalone proof files -(`+idris2 --check+`). -* *verification/proofs/lean4/*: 5 Lean files (`+lake build+`). -* *verification/proofs/tlaplus/*: `+KinGate.tla+` (TLC model-check). -* *Toolchain*: Idris2 `+v0.7.0+`, Lean `+v4.30.0+` (both pinned), TLA+ -tla2tools 2.19. Agda was retired 2026-04-22 (see PROOF-STATUS.md -"`Retired proofs`"). -* *Escape hatches*: 0 — no `+believe_me+` / `+assert_total+` / -`+postulate+` / `+sorry+` / `+Admitted+` / `+unsafeCoerce+` in any proof -file. -* All of the above is gated by `+.github/workflows/verify-proofs.yml+`. - -=== Completed Proofs - -[width="100%",cols="24%,30%,46%",options="header",] -|=== -|File |Covers |Obligation -|`+verification/proofs/idris2/ConfidenceBounds.idr+` |Confidence bounded -[0,1]; Bayesian update preserves invariant |H1 ✅ - -|`+verification/proofs/idris2/DispatchStrategy.idr+` |Dispatch strategy -monotone (confidence → strategy) |H2 ✅ - -|`+verification/proofs/idris2/SafetyTriangle.idr+` |Eliminate > -Substitute > Control strict ordering |H3 ✅ - -|`+verification/proofs/lean4/RateLimiting.lean+` |Window counters never -exceed configured bounds |H4 ✅ - -|`+verification/proofs/idris2/Quarantine.idr+` |Quarantine trigger -exclusivity + release correctness |H5 ✅ - -|`+lib/outcome_tracker.ex+` (`+assert_h6_monotone/2+`) |Outcome-log -timestamp monotonicity — runtime assertion + echidnabot audit |H6 -(retired from Agda) - -|`+verification/proofs/lean4/BayesianUpdate.lean+` |Posterior in (0,1), -monotone in successes/failures, zero-obs identity |H7 ✅ - -|`+verification/proofs/tlaplus/KinGate.tla+` |Kin-gate atomicity / -mutual exclusion (TLC: 1.78M states, no errors) |H8 ✅ - -|`+verification/proofs/idris2/NeuralConsensus.idr+` |Uniform-mean -aggregation in [0,1], bounded below by n·min |H9 ✅ - -|`+verification/proofs/idris2/VerisimdbConnector.idr+` |Connector -completeness / soundness / preservation |— - -|`+verification/proofs/idris2/BatchRollback.idr+` |Batch rollback -transactionality / reversibility |— - -|`+verification/proofs/lean4/ParserTotality.lean+` |VCL `+FROM+`-clause -parser totality + round-trip |— -|=== - -=== What Still Needs Proving - -These are the *only* open proof obligations. Both currently prove ℕ -_structural preconditions_ over the natural-number model; the full -analytical theorems require Mathlib and are in progress. - -[width="100%",cols="24%,28%,32%,16%",options="header",] -|=== -|Component |Proven today |Target theorem |Prover -|PageRank power-iteration convergence (`+PageRankInvariants.lean+`) -|non-negativity, column-stochastic normalisation preconditions -|Banach-contraction convergence of the damped Google matrix (α < 1) -|Lean 4 + Mathlib - -|ESN echo-state stability (`+ESNSpectralScaling.lean+`) |floor-clamped -denominator is positive (scaling well-defined) |operator-norm -contraction ⇒ bounded trajectory + exponential forgetting |Lean 4 + -Mathlib -|=== - -=== Recommended Prover - -*Idris2* for ABI / type-level invariants. *Lean 4* for algorithmic and -numerical properties (*+ Mathlib* for the analytic convergence results). -*TLA+* for model-checked concurrency. (Agda is no longer in the -toolchain.) - -=== Priority - -*MEDIUM* — H1–H9 are complete (H6 as a runtime assertion). The remaining -work is the two neural-convergence theorems, which require pulling in -Mathlib. +// SPDX-License-Identifier: CC-BY-SA-4.0 +== Proof needs — hypatia + +What still needs proving is the set of rows in the proof ledger whose status +is not `+proven+`. The ledger is `+verification/proof-ledger.jsonl+` and is +canonical; `+verification/PROOF-STATUS.adoc#proof-ledger+` renders it with a +census line. This file keeps no list of its own. The earlier hand-kept +inventory here drifted: it called Agda retired after an Agda artefact was +reinstated, and planned Lean with Mathlib, which PROOF-POLICY forbids. + +To list the open work: + +[source,bash] +---- +jq -r 'select(.status != "proven") | "\(.status)\t\(.id)\t\(.obligation)"' verification/proof-ledger.jsonl +---- + +Plans: + +* Neural convergence (rows `+pagerank-convergence+` and `+esn-echo-state+`): + `+docs/proofs/HANDOVER-neural-convergence.adoc+`. Agda first, over + constructive reals, then the Rocq and Lean legs. +* The Lean engineering proofs moved to Idris2 on 2026-11-09 (PROOF-POLICY §3; + owner decision), which removed the Lean kernel axioms (`+propext+`, + `+Quot.sound+`) four of them rested on. + +Prover mapping and statuses: the estate PROOF-POLICY +(`+metadatastician/standards/3-practice/PROOF-POLICY.adoc+`). diff --git a/scripts/proof-ledger-ci.sh b/scripts/proof-ledger-ci.sh new file mode 100644 index 00000000..eddb8c35 --- /dev/null +++ b/scripts/proof-ledger-ci.sh @@ -0,0 +1,85 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# proof-ledger-ci.sh — run one checker and record its receipts, so the proof +# ledger's statuses are derived from what this run checked +# (scripts/proof-ledger.sh derive). The checker's own exit status is the +# step's: a receipt is written for a failure too, then the step fails. +# +# proof-ledger-ci.sh ipkg PKG.ipkg idris2 --build; one receipt per module +# proof-ledger-ci.sh verdicts scripts/check-verdicts.sh; tests/accept, tests/reject +# proof-ledger-ci.sh leanhole scripts/recheck-lean-hole.sh; the Lean-hole control's fixture +# proof-ledger-ci.sh tlc SPEC.tla CFG TLC; the receipt carries distinct states and depth +# proof-ledger-ci.sh exunit FILE... mix test FILE...; one receipt per file +# +# Receipts go to $PROOF_RECEIPTS. Run from the repository root. + +set -uo pipefail + +ledger="scripts/proof-ledger.sh" +rc=0 + +case "${1:-}" in + ipkg) + lane=idris2 + pkg=${2:?ipkg} + mapfile -t files < <(bash "$ledger" ipkg-files "$pkg") + [ "${#files[@]}" -gt 0 ] || { echo "::error::proof-ledger-ci: $pkg lists no modules"; exit 2; } + idris2 --build "$pkg" || rc=$? + ;; + verdicts) + lane=verdicts + files=(tests/accept/*.idr tests/reject/*.idr) + bash scripts/check-verdicts.sh || rc=$? + ;; + leanhole) + # The control's obligation includes digests re-derived from a fresh Lean + # run, so its receipt comes from that re-check (the Idris acceptance of + # the fixture is the verdicts lane's, and fails that job by itself). + lane=leanhole + files=(tests/accept/LeanHoleRecheckSound.idr) + bash scripts/recheck-lean-hole.sh || rc=$? + ;; + tlc) + spec=${2:?spec} cfg=${3:?cfg} jar=${TLA2TOOLS_JAR:?TLA2TOOLS_JAR} + files=("$spec") + log=$(mktemp) + ( cd "$(dirname "$spec")" && java -XX:+UseParallelGC -cp "$jar" tlc2.TLC \ + -workers auto -config "$(basename "$cfg")" "$(basename "$spec")" ) | tee "$log" || rc=$? + if grep -q "Error:" "$log"; then + echo "::error::TLC found an invariant / property violation"; rc=1 + fi + if ! grep -q "Model checking completed. No error has been found." "$log"; then + echo "::error::TLC did not report clean completion"; rc=1 + fi + states=$(grep -oE '[0-9]+ distinct states found, 0 states left on queue' "$log" | tail -1 | cut -d' ' -f1) + depth=$(grep -oE 'depth of the complete state graph search is [0-9]+' "$log" | grep -oE '[0-9]+$') + cp "$log" "$(dirname "$spec")/tlc.log" + if [ "$rc" -eq 0 ] && [ -n "$states" ] && [ -n "$depth" ]; then + bash "$ledger" receipt tlc pass "${files[@]}" -- distinct_states="$states" depth="$depth" + else + bash "$ledger" receipt tlc fail "${files[@]}" + [ "$rc" -ne 0 ] || { echo "::error::TLC reported no state count or depth"; rc=1; } + fi + exit "$rc" + ;; + exunit) + lane=exunit + shift + files=("$@") + [ "${#files[@]}" -gt 0 ] || { echo "::error::proof-ledger-ci: exunit needs test files"; exit 2; } + mix test "${files[@]}" || rc=$? + ;; + *) + echo "usage: $0 ipkg PKG | verdicts | leanhole | tlc SPEC CFG | exunit FILE..." >&2 + exit 2 + ;; +esac + +if [ "$rc" -eq 0 ]; then + bash "$ledger" receipt "$lane" pass "${files[@]}" +else + bash "$ledger" receipt "$lane" fail "${files[@]}" +fi +exit "$rc" diff --git a/scripts/proof-ledger.sh b/scripts/proof-ledger.sh new file mode 100755 index 00000000..c4b63ddc --- /dev/null +++ b/scripts/proof-ledger.sh @@ -0,0 +1,454 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# proof-ledger.sh — the machine proof ledger (verification/proof-ledger.jsonl) +# is canonical; the Proof Ledger table in verification/PROOF-STATUS.adoc is +# rendered from it (README-EXPLAINME-STANDARD section 5, rule 1). +# +# proof-ledger.sh check validate the ledger against its rules and the tree +# proof-ledger.sh claims every census README, AFFIRMATION or EXPLAINME quotes is the ledger's +# proof-ledger.sh receipt LANE pass|fail FILE... [-- k=v...] append receipts ($PROOF_RECEIPTS) +# proof-ledger.sh derive LANES [RECEIPTS] each row in LANES must say what the receipts make it +# proof-ledger.sh render print the AsciiDoc block for PROOF-STATUS.adoc +# proof-ledger.sh render --check fail if PROOF-STATUS.adoc holds a different block +# proof-ledger.sh render --write replace the block in PROOF-STATUS.adoc +# +# One JSON object per line, I-JSON serialised as JCS (RFC 8785): keys sorted, +# no insignificant whitespace, one final LF. The ledger is held to a profile +# in which `jq -cS` output IS the JCS form: ASCII strings and no numbers. +# +# Status vocabulary (closed; PROOF-POLICY section 5 gives the upper-case +# labels): proven, proven-with-postulates, argued, tested-only, open. +# Proof Witness Grades (PROOF-POLICY section 8) are recorded for theory rows +# only: 3, 2i, 2ii, 1 or ungraded. A grade is computed from the row's legs, +# never asserted (section 8.4). A leg (rocq, lean, or other for a +# foundation-diverse witness) counts when its kernel accepted it (proven or +# proven-with-postulates) and its statement correspondence is reconciled +# (section 8.2). PWG-1 needs a current per-commit receipt for every witness; +# this ledger records none yet, so PWG-1 is refused. +# +# The policy this gate enforces is pinned by repository, path and full +# commit in POLICY_PIN (PROOF-POLICY section 7). Moving the pin is a +# reviewed change; the check fails when the pin is missing or malformed. +# +# Exit: 0 = ledger valid (and the block current, for render --check); +# 1 = invalid or stale; 2 = usage or IO error. + +set -euo pipefail + +LEDGER="${PROOF_LEDGER:-verification/proof-ledger.jsonl}" +DOC="${PROOF_STATUS_DOC:-verification/PROOF-STATUS.adoc}" +BEGIN_MARK='// BEGIN GENERATED: scripts/proof-ledger.sh render (do not edit by hand)' +END_MARK='// END GENERATED: proof ledger' +AGDA_PROFILE='--safe --without-K --cubical-compatible' +# PROOF-POLICY section 7: repository, path and full 40-character commit. +POLICY_PIN="${PROOF_POLICY_PIN-metadatastician/standards 3-practice/PROOF-POLICY.adoc b8f60511e76c9015d86990317162dce653c92fe1}" + +# `receipt` and `ipkg-files` run from proof subdirectories and need no ledger. +need_ledger() { [ -f "$LEDGER" ] || { echo "::error::proof-ledger: $LEDGER not found"; exit 2; }; } + +# Validate ledger serialisation, schema, policy grades and referenced files +# and names. Return 1 for detected violations; an empty ledger exits 1. +check() { + local fails=0 n=0 line id unparsed=0 + if ! [[ "$POLICY_PIN" =~ ^[A-Za-z0-9_.-]+/[A-Za-z0-9_.-]+\ [^\ ]+\.adoc\ [0-9a-f]{40}$ ]]; then + echo "::error::proof-ledger: the PROOF-POLICY pin is missing or malformed ('$POLICY_PIN'); it names repository, path and full commit (section 7)" + fails=$((fails + 1)) + fi + # Byte profile: every line is its own `jq -cS` rendering, ASCII only, and + # the file ends in exactly one LF. + if LC_ALL=C grep -nP '[^\x00-\x7F]' "$LEDGER" >/dev/null; then + echo "::error::proof-ledger: non-ASCII byte in $LEDGER (the profile is ASCII so that jq -cS is JCS)"; fails=$((fails + 1)) + fi + if [ -n "$(tail -c1 "$LEDGER")" ] || [ -z "$(tail -c2 "$LEDGER" | head -c1)" ]; then + echo "::error::proof-ledger: $LEDGER must end in exactly one LF"; fails=$((fails + 1)) + fi + while IFS= read -r line; do + n=$((n + 1)) + if ! canon=$(jq -cS . <<<"$line" 2>/dev/null); then + echo "::error::proof-ledger: line $n is not JSON"; fails=$((fails + 1)); unparsed=1 + elif [ "$(jq -r type <<<"$canon")" != object ]; then + echo "::error::proof-ledger: line $n is not a JSON object"; fails=$((fails + 1)); unparsed=1 + elif [ "$canon" != "$line" ]; then + echo "::error::proof-ledger: line $n is not in canonical (jq -cS / JCS) form"; fails=$((fails + 1)) + fi + done < "$LEDGER" + [ "$n" -gt 0 ] || { echo "::error::proof-ledger: $LEDGER has no rows"; exit 1; } + # The schema pass reads every line as a JSON object; a line that is not one + # would abort it, so stop here with the lines named. + if [ "$unparsed" -eq 1 ]; then + echo "proof-ledger: INVALID ($fails problem(s)) in $LEDGER" + return 1 + fi + + # Schema and status rules, one message per broken rule. + local errs + errs=$(jq -r --arg agda "$AGDA_PROFILE" ' + def need(k; t): if (has(k) and (.[k] | type) == t) then empty else "\(.id // "?"): field \(k) must be a \(t)" end; + # Field types first: a row with a missing or mistyped field gets only + # those messages, since the rules below assume the types. + . as $r + | [ need("id"; "string"), need("kind"; "string"), need("obligation"; "string"), + need("status"; "string"), need("checker"; "string"), need("file"; "string"), + need("names"; "array"), need("axioms"; "array"), need("bounds"; "string"), + need("trust_boundary"; "string"), need("lane"; "string"), + (if any(.names[]?, .axioms[]?; type != "string") then "\(.id // "?"): names and axioms hold strings" else empty end) ] as $te + | if ($te | length) > 0 then $te[] else + ( [keys[] | select(IN("id","kind","obligation","status","checker","file","names","axioms","bounds","trust_boundary","lane","pwg","foundation_diverse","legs") | not)] + | if length > 0 then "\($r.id): unknown field(s) \(join(", "))" else empty end ), + # The lane is the CI job whose receipt decides the status (`derive`): + # a proof lane can only make a row proven, a test lane tested-only, and + # a row with no lane is argued or open. + ( if IN(.lane; "idris2", "agda", "verdicts", "leanhole", "tlc", "exunit", "none") then empty + else "\(.id): lane \(.lane) is not idris2, agda, verdicts, leanhole, tlc, exunit or none" end ), + ( if (.lane == "none") != (.checker == "-") then "\(.id): a row has a checker exactly when it has a lane" else empty end ), + ( if IN(.lane; "idris2", "agda") and (IN(.status; "proven", "proven-with-postulates") | not) + then "\(.id): lane \(.lane) is a proof lane; its row is proven or proven-with-postulates" else empty end ), + ( if IN(.lane; "verdicts", "leanhole", "tlc", "exunit") and .status != "tested-only" + then "\(.id): lane \(.lane) is a test lane; its row is tested-only" else empty end ), + ( if .lane == "none" and (IN(.status; "argued", "open") | not) + then "\(.id): a row with no lane is argued or open" else empty end ), + # The profile in which jq -cS is JCS has no numbers anywhere, and a + # control character would break the rendered table. + ( if [.. | numbers] | length > 0 then "\(.id): the ledger profile holds no numbers (write them as strings)" else empty end ), + ( if [.. | strings | select(any(explode[]; . < 32 or . == 127))] | length > 0 then "\(.id): a string holds a control character" else empty end ), + ( if .checker == "" or .obligation == "" or .trust_boundary == "" then "\(.id): checker, obligation and trust_boundary are not empty (use - for no checker)" else empty end ), + ( if (.id | test("^[a-z0-9]+(-[a-z0-9]+)*$")) then empty else "\(.id): id must be lower-case words joined by -" end ), + ( if IN(.kind; "engineering", "theory") then empty else "\(.id): kind must be engineering or theory" end ), + ( if IN(.status; "proven", "proven-with-postulates", "argued", "tested-only", "open") then empty + else "\(.id): status \(.status) is outside the closed vocabulary" end ), + ( if (.status == "proven" or .status == "proven-with-postulates") and .checker == "-" then "\(.id): a proven row names its checker" else empty end ), + ( if .status == "proven" and (.axioms | length) > 0 then "\(.id): proven rests on no axioms; with \(.axioms | join(", ")) it is proven-with-postulates" else empty end ), + ( if .status == "proven-with-postulates" and (.axioms | length) == 0 then "\(.id): proven-with-postulates lists its axioms" else empty end ), + ( if .status != "proven" and .status != "proven-with-postulates" and (.axioms | length) > 0 then "\(.id): only a proven row carries axioms" else empty end ), + ( if .status == "tested-only" and .bounds == "" then "\(.id): tested-only gives its bounds" else empty end ), + ( if .status != "tested-only" and .bounds != "" then "\(.id): only a tested-only row has bounds" else empty end ), + ( if .status != "open" and .file == "-" then "\(.id): only an open row may have no file" else empty end ), + ( if .file != "-" and (.names | length) == 0 then "\(.id): a row with a file names what it rests on in that file" else empty end ), + ( if .kind == "theory" then + ( if IN(.pwg; "3", "2i", "2ii", "1", "ungraded") then empty else "\(.id): a theory row records pwg as 3, 2i, 2ii, 1 or ungraded" end ), + ( if (.foundation_diverse | type) == "boolean" then empty else "\(.id): a theory row records foundation_diverse" end ), + ( if (.legs | type) == "array" then + # A leg: {prover, route, status, correspondence, axioms}; every + # field is checked, since the grade is computed from them. + ( .legs[] | . as $l + | if type != "object" then "\($r.id): a leg is an object" + else + ( [keys[] | select(IN("prover","route","status","correspondence","axioms") | not)] + | if length > 0 then "\($r.id): unknown leg field(s) \(join(", "))" else empty end ), + ( if IN($l.prover; "rocq", "lean", "other") then empty else "\($r.id): a leg prover is rocq, lean or other" end ), + ( if IN($l.route; "transported", "re-proved") then empty else "\($r.id): a leg route is transported or re-proved" end ), + ( if IN($l.status; "proven", "proven-with-postulates", "assumed", "waived", "unavailable", "bridge-pending") then empty + else "\($r.id): a leg status is proven, proven-with-postulates, assumed, waived, unavailable or bridge-pending" end ), + ( if IN($l.correspondence; "reconciled", "pending") then empty else "\($r.id): a leg correspondence is reconciled or pending" end ), + ( if ($l.axioms | type) == "array" and all($l.axioms[]; type == "string") then empty else "\($r.id): a leg lists its axioms as strings" end ), + ( if $l.status == "proven" and ($l.axioms | length) > 0 then "\($r.id): a proven leg rests on no axioms" else empty end ) + end ) + else "\(.id): a theory row records its legs" end ), + # The grade the legs support (section 8.2), compared with the one + # recorded: a grade is computed, never asserted. + ( def counts: type == "object" and IN(.status; "proven", "proven-with-postulates") and .correspondence == "reconciled"; + def counted(p): [.legs[]? | select(counts and .prover == p)] | length > 0; + (if ((.status == "proven" or .status == "proven-with-postulates") + and (.checker | contains("Agda")) and (.checker | contains($agda))) | not then "ungraded" + elif counted("rocq") and counted("lean") then "2ii" + elif counted("rocq") or counted("lean") then "2i" + else "3" end) as $grade + | if .pwg == "1" then "\(.id): PWG-1 needs a current per-commit receipt for every witness, which this ledger does not record (section 8.2)" + elif .pwg != $grade then + (if $grade == "ungraded" and .pwg != "ungraded" + then "\(.id): PWG-\(.pwg) needs an Agda proof that is proven or proven-with-postulates under the PROOF-POLICY 2.1 invocation (\($agda)); the legs support ungraded" + else "\(.id): pwg is \(.pwg), and the legs support \(if $grade == "ungraded" then "ungraded" else "PWG-" + $grade end)" end) + else empty end ), + ( if (.foundation_diverse == true) != ([.legs[]? | select(type == "object" and .prover == "other" and IN(.status; "proven", "proven-with-postulates") and .correspondence == "reconciled")] | length > 0) + then "\(.id): foundation_diverse is true exactly when an other-foundation leg counts (section 8.3)" else empty end ) + else + ( if has("pwg") or has("legs") or has("foundation_diverse") then "\(.id): pwg, legs and foundation_diverse belong to theory rows" else empty end ) + end ) + end + ' "$LEDGER") + if [ -n "$errs" ]; then + while IFS= read -r e; do echo "::error::proof-ledger: $e"; done <<<"$errs" + fails=$((fails + $(wc -l <<<"$errs"))) + fi + local dups + dups=$(jq -r '.id' "$LEDGER" | sort | uniq -d) + if [ -n "$dups" ]; then echo "::error::proof-ledger: duplicate id(s): $dups"; fails=$((fails + 1)); fi + + # Currency against the tree: the file exists, and every name it rests on + # is in it (a renamed proof turns this red). + local file name + while IFS=$'\t' read -r id file name; do + if [ ! -f "$file" ]; then + echo "::error::proof-ledger: $id names $file, which does not exist"; fails=$((fails + 1)); continue + fi + if [ -n "$name" ] && ! grep -qwF -- "$name" "$file"; then + echo "::error::proof-ledger: $id says $file holds '$name', and it does not (renamed or removed?)"; fails=$((fails + 1)) + fi + done < <(jq -r 'select(.file != "-" and (.names | type) == "array" and (.file | type) == "string") | .id as $i | .file as $f | if (.names | length) == 0 then [$i, $f, ""] else (.names[] | [$i, $f, .]) end | @tsv' "$LEDGER") + + if [ "$fails" -gt 0 ]; then + echo "proof-ledger: INVALID ($fails problem(s)) in $LEDGER" + return 1 + fi + echo "proof-ledger: $n rows valid; $(census)" +} + +# A census, never a percentage (PROOF-POLICY 8.4, README-EXPLAINME 5 rule 2). +census() { + jq -rs ' + def c(s): [.[] | select(.status == s)] | length; + def g(p): [.[] | select(.kind == "theory" and .pwg == p)] | length; + "\(c("proven")) proven of \(length); \(c("proven-with-postulates")) proven-with-postulates, \(c("tested-only")) tested-only, \(c("argued")) argued, \(c("open")) open. Theory rows: \([.[] | select(.kind == "theory")] | length) (PWG-1 \(g("1")), PWG-2ii \(g("2ii")), PWG-2i \(g("2i")), PWG-3 \(g("3")), ungraded \(g("ungraded")))." + ' "$LEDGER" +} + +# Write the generated AsciiDoc block, including markers, to standard output; +# this function does not validate the ledger or update the document. +render() { + printf '%s\n' "$BEGIN_MARK" + printf '%s\n' '[[proof-ledger]]' + printf '%s\n' '=== Proof Ledger' + printf '\n' + # shellcheck disable=SC2016 # the backticks are AsciiDoc, printed literally + printf 'Rendered from `+%s+`, which is canonical: where this table and the\n' "$LEDGER" + printf 'ledger disagree, the ledger wins and this table is regenerated. No status\n' + printf 'is typed in unchecked: each checker job derives its rows from that run'"'"'s\n' + # shellcheck disable=SC2016 # AsciiDoc backticks, printed literally + printf 'receipts (`+scripts/proof-ledger.sh derive+`) and fails on an overclaim or\n' + printf 'a stale underclaim.\n' + # shellcheck disable=SC2016 # the backticks are AsciiDoc, printed literally + printf 'Checked against PROOF-POLICY as pinned by `+%s+`.\n' "$POLICY_PIN" + printf '\n' + printf '*Census:* %s\n' "$(census)" + printf '\n' + printf '%s\n' '[cols="3,1,2,2,2",options="header"]' + printf '%s\n' '|===' + printf '%s\n' '|Obligation |Status |Checker (version, flags) |Where |Trust boundary' + jq -r ' + def esc: gsub("\\|"; "{vbar}"); + def code: "`+" + . + "+`"; + "\n|" + (.obligation | esc) + + "\n|" + .status + + (if (.axioms | length) > 0 then " (" + (.axioms | join(", ")) + ")" else "" end) + + (if .kind == "theory" then (if .pwg == "ungraded" then ", ungraded" else ", PWG-" + .pwg end) + + (if .foundation_diverse then " +foundation-diverse" else "" end) else "" end) + + "\n|" + (if .checker == "-" then "-" else (.checker | esc) end) + + "\n|" + (if .file == "-" then "-" else (.file | code) + (if (.names | length) > 0 then ": " + (.names | map(code) | join(", ")) else "" end) end) + + "\n|" + (.trust_boundary | esc) + + (if .bounds != "" then ". Bounds: " + (.bounds | esc) else "" end) + ' "$LEDGER" + printf '%s\n' '|===' + printf '%s\n' "$END_MARK" +} + +# Receipts: one JCS line per checked file, written by the CI job that checked +# it, to $PROOF_RECEIPTS. `receipt LANE RESULT FILE... [-- key=value...]`. +# Extra fields carry what the status depends on (TLC's state count and depth). +RECEIPTS="${PROOF_RECEIPTS:-proof-receipts.jsonl}" +# Append one canonical JSON receipt per FILE to RECEIPTS, without checking +# file existence. Arguments after -- add string fields as key=value pairs; +# lane, result and file take precedence over extra fields with those names. +# Exit 2 for a result other than pass or fail; jq and append errors propagate. +receipt() { + local lane=${1:?lane} result=${2:?result} f extra='{}' kv + shift 2 + case "$result" in pass|fail) ;; *) echo "::error::proof-ledger: receipt result must be pass or fail" >&2; exit 2 ;; esac + local files=() + while [ $# -gt 0 ] && [ "$1" != "--" ]; do files+=("$1"); shift; done + [ "${1:-}" = "--" ] && shift + for kv in "$@"; do + extra=$(jq -cS --arg k "${kv%%=*}" --arg v "${kv#*=}" '. + {($k): $v}' <<<"$extra") + done + for f in ${files[@]+"${files[@]}"}; do + jq -cnS --arg lane "$lane" --arg result "$result" --arg file "$f" --argjson extra "$extra" \ + '$extra + {lane: $lane, result: $result, file: $file}' >> "$RECEIPTS" + done +} + +# The source files an ipkg builds: its `modules`, resolved against its +# `sourcedir`, as paths from the repository root. A receipt for a package +# build names every module the build checked. +ipkg_files() { + local ipkg=${1:?ipkg} dir src + dir=$(dirname "$ipkg") + src=$(sed -nE 's/^sourcedir[[:space:]]*=[[:space:]]*"([^"]*)".*/\1/p' "$ipkg") + awk '/^modules[[:space:]]*=/{on=1; sub(/^modules[[:space:]]*=/, "")} + on && /^[[:space:]]*$/{exit} + on && /^[A-Za-z]+[[:space:]]*=/{exit} + on { gsub(/[,[:space:]]+/, "\n"); printf "%s", $0; print "" }' "$ipkg" \ + | grep -E '^[A-Z][A-Za-z0-9_.]*$' \ + | while IFS= read -r m; do + realpath --relative-to=. -m "$dir/${src:-.}/${m//.//}.idr" + done +} + +# Derive each row's status in LANES from this run's receipts and require the +# ledger to say exactly that: stronger is an overclaim, weaker a stale +# underclaim, and both fail. A proof lane's passing receipt makes a row +# proven (proven-with-postulates when axioms are listed); a test lane's +# makes it tested-only. Use the last receipt for each lane/file pair. TLC +# state count and depth must match the ledger exactly; theory grades must +# agree with the derived status and counted legs. A missing or failing +# receipt makes the status open. Passing receipts for rows with lane none +# are underclaims; files with no row produce warnings in any selected lane. +# LANES is comma-separated; the optional second argument overrides RECEIPTS. +# Return 1 for missing receipts or disagreements, 0 when only warnings remain. +# Malformed JSON and other jq failures propagate; the ledger is not modified. +derive() { + local lanes=${1:?comma-separated lanes} file=${2:-$RECEIPTS} + [ -f "$file" ] || { echo "::error::proof-ledger: no receipts at $file"; return 1; } + local out + out=$(jq -rn --arg lanes "$lanes" --slurpfile led "$LEDGER" --slurpfile rec "$file" ' + def rank(s): {"open":0,"argued":1,"tested-only":2,"proven-with-postulates":3,"proven":4}[s]; + def counts: type == "object" and IN(.status; "proven", "proven-with-postulates") and .correspondence == "reconciled"; + def legs_grade: [.legs[]? | select(counts) | .prover] as $p + | if ($p | index("rocq")) and ($p | index("lean")) then "2ii" + elif ($p | index("rocq")) or ($p | index("lean")) then "2i" else "3" end; + ($lanes | split(",")) as $L + | ($rec | map(select(.lane as $l | $L | index($l)))) as $R + | ( $led[] | select(.lane as $l | $L | index($l)) | . as $row + | ([$R[] | select(.lane == $row.lane and .file == $row.file)] | last) as $r + | (if $r == null or $r.result != "pass" then "open" + elif IN($row.lane; "idris2", "agda") then (if ($row.axioms | length) > 0 then "proven-with-postulates" else "proven" end) + else "tested-only" end) as $d + | ( if $d != $row.status then + (if rank($row.status) > rank($d) then "OVERCLAIM" else "UNDERCLAIM" end) + + "\t\($row.id): the ledger says \($row.status); this run'"'"'s receipt makes it \($d)" + + (if $r == null then " (no receipt for \($row.file) in lane \($row.lane))" + elif $r.result != "pass" then " (\($row.file) failed)" else "" end) + else empty end ), + # TLC bounds: the state count and depth the row states, compared + # exactly with what this run found (a substring match would let + # 44715 stand for 444715). + ( if $row.lane == "tlc" and $r != null and $r.result == "pass" then + ([$row.bounds | capture("(?[0-9]+) distinct states")] | first | .n?) as $n + | ([$row.bounds | capture("depth (?[0-9]+)")] | first | .d?) as $dep + | if $n == ($r.distinct_states | tostring) and $dep == ($r.depth | tostring) then empty + else "OVERCLAIM\t\($row.id): bounds say \"\($row.bounds)\"; this run found \($r.distinct_states) distinct states, depth \($r.depth)" end + else empty end ), + # The grade this run supports: the Agda receipt and the legs. + ( if $row.kind == "theory" then + (if $d == "proven" or $d == "proven-with-postulates" then ($row | legs_grade) else "ungraded" end) as $g + | if $row.pwg == $g then empty + else (if $row.pwg == "ungraded" then "UNDERCLAIM" elif $g == "ungraded" then "OVERCLAIM" + elif ({"3":0,"2i":1,"2ii":2,"1":3}[$row.pwg]) > ({"3":0,"2i":1,"2ii":2}[$g]) then "OVERCLAIM" else "UNDERCLAIM" end) + + "\t\($row.id): pwg is \($row.pwg); this run'"'"'s receipts and the legs support \(if $g == "ungraded" then "ungraded" else "PWG-" + $g end)" end + else empty end ) + ), + # Row identity does not hang on the mutable lane: a file that passes in + # a lane where no row names it, while a row with no lane does, is an + # underclaim (a demoted row cannot dodge the gate by leaving its lane). + ( $R[] | select(.result == "pass") | . as $r + | [$led[] | select(.file == $r.file)] as $named + | if ($named | map(select(.lane == $r.lane)) | length) > 0 then empty + elif ($named | map(select(.lane == "none")) | length) > 0 then + "UNDERCLAIM\t\($named | map(select(.lane == "none") | "\(.id) (\(.status))") | join(", ")): \($r.file) passes in lane \($r.lane), and the row records no lane" + elif ($named | length) > 0 then empty + else "UNRECORDED\t\($r.file) checks in lane \($r.lane) and no ledger row names it" end ) + ') + local bad=0 kind msg + while IFS=$'\t' read -r kind msg; do + [ -n "$kind" ] || continue + case "$kind" in + UNRECORDED) echo "::warning::proof-ledger: $msg" ;; + *) echo "::error::proof-ledger: $kind $msg"; bad=$((bad + 1)) ;; + esac + done <<<"$out" + local rows + rows=$(jq -r --arg lanes "$lanes" 'select(.lane as $l | $lanes | split(",") | index($l)) | .id' "$LEDGER" | wc -l) + if [ "$bad" -gt 0 ]; then + echo "proof-ledger: derive ($lanes): $bad row(s) disagree with this run's receipts" + return 1 + fi + echo "proof-ledger: derive ($lanes): all $rows row(s) agree with this run's receipts" +} + +# Every census a claim document quotes ("N proven of M; ...") must be the +# ledger's census: README's proof count is derived from the ledger, never +# typed in (README-EXPLAINME section 5, rule 2). Lines are joined first, so a +# census wrapped across lines is still read whole. Each document named must +# exist and quote at least one census: a renamed file or a census reworded +# out of the pattern would otherwise pass unread. +CLAIM_DOCS="${PROOF_CLAIM_DOCS:-README.adoc AFFIRMATION.adoc EXPLAINME.adoc}" +claims() { + local want doc found fails=0 seen=0 c here + want=$(census | sed 's/ Theory rows:.*//') + for doc in $CLAIM_DOCS; do + if [ ! -f "$doc" ]; then + echo "::error::proof-ledger: claim document $doc does not exist"; fails=$((fails + 1)); continue + fi + found=$(tr '\n' ' ' < "$doc" | tr -s ' ' | grep -oE '[0-9]+ proven of [0-9]+(; [0-9]+ proven-with-postulates, [0-9]+ tested-only, [0-9]+ argued, [0-9]+ open\.?)?' || true) + here=0 + while IFS= read -r c; do + [ -n "$c" ] || continue + seen=$((seen + 1)); here=$((here + 1)) + [ "${c%.}." = "$want" ] && continue + echo "::error::proof-ledger: $doc quotes the census '$c'; the ledger's is '$want'" + fails=$((fails + 1)) + done <<<"$found" + if [ "$here" -eq 0 ]; then + echo "::error::proof-ledger: $doc quotes no census ('N proven of M; ...'); a claim document states the ledger's"; fails=$((fails + 1)) + fi + done + if [ "$fails" -gt 0 ]; then return 1; fi + echo "proof-ledger: $seen quoted census(es) agree with the ledger" +} + +# Exactly one BEGIN and one END marker, BEGIN first: a second block (a bad +# merge, a hand copy) would publish two tables while the first one passed. +markers_ok() { + local b e + b=$(grep -cxF -- "$BEGIN_MARK" "$DOC" || true) + e=$(grep -cxF -- "$END_MARK" "$DOC" || true) + [ "$b" = 1 ] && [ "$e" = 1 ] || return 1 + [ "$(grep -nxF -- "$BEGIN_MARK" "$DOC" | cut -d: -f1)" -lt "$(grep -nxF -- "$END_MARK" "$DOC" | cut -d: -f1)" ] +} + +# Print the document from its first BEGIN marker through its first END +# marker, inclusive. Call markers_ok first to verify the marker pair. +doc_block() { + awk -v b="$BEGIN_MARK" -v e="$END_MARK" '$0 == b { on = 1 } on { print } $0 == e { exit }' "$DOC" +} + +case "${1:-}" in + check) need_ledger; check ;; + claims) need_ledger; claims ;; + receipt) shift; receipt "$@" ;; + derive) need_ledger; derive "${2:-}" "${3:-}" ;; + ipkg-files) ipkg_files "${2:-}" ;; + render) + need_ledger + case "${2:-}" in + "") render ;; + --check) + [ -f "$DOC" ] || { echo "::error::proof-ledger: $DOC not found"; exit 2; } + if ! markers_ok; then + echo "::error::proof-ledger: $DOC lacks the generated-block markers, holds more than one pair, or has them out of order; it needs exactly one pair (render --write needs them too)"; exit 2 + fi + if ! diff -u <(doc_block) <(render); then + echo "::error::proof-ledger: the Proof Ledger block in $DOC is not the rendering of $LEDGER; run scripts/proof-ledger.sh render --write" + exit 1 + fi + echo "proof-ledger: $DOC block is current" ;; + --write) + [ -f "$DOC" ] || { echo "::error::proof-ledger: $DOC not found"; exit 2; } + if ! markers_ok; then + echo "::error::proof-ledger: $DOC lacks the generated-block markers, holds more than one pair, or has them out of order; it needs exactly one pair"; exit 2 + fi + tmp=$(mktemp); blk=$(mktemp) + render > "$blk" + # The block is read from a file, not passed with -v: awk would + # process backslash escapes in a -v value. + awk -v b="$BEGIN_MARK" -v e="$END_MARK" ' + NR == FNR { block = block $0 "\n"; next } + $0 == b { printf "%s", block; skip = 1; next } + $0 == e { skip = 0; next } + !skip { print }' "$blk" "$DOC" > "$tmp" + cat "$tmp" > "$DOC"; rm -f "$tmp" "$blk" + echo "proof-ledger: wrote the block into $DOC" ;; + *) echo "usage: $0 render [--check|--write]" >&2; exit 2 ;; + esac ;; + *) echo "usage: $0 check | claims | receipt LANE pass|fail FILE... [-- k=v...] | derive LANES [RECEIPTS] | render [--check|--write]" >&2; exit 2 ;; +esac diff --git a/tests/proof-ledger-test.sh b/tests/proof-ledger-test.sh new file mode 100755 index 00000000..09d9ddc2 --- /dev/null +++ b/tests/proof-ledger-test.sh @@ -0,0 +1,205 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Contracts of scripts/proof-ledger.sh: the real ledger passes, and every +# planted defect (an overclaim, a vocabulary escape, a renamed proof, a +# non-canonical line, a hand-edited table) turns it red. +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$repo_root" +work="$(mktemp -d)" +trap 'rm -rf -- "$work"' EXIT +script="scripts/proof-ledger.sh" +pass=0; fail=0 + +expect() { #