From c78335ca7053dad4f65ca920009d96ffdc7611c2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:15:38 +0000 Subject: [PATCH] ci(abi): gate the Idris2 proofs on every PR, with module-shaped paths The Idris2 modules are named PanicAttack.ABI. but lived in src/abi/, so `idris2 --check src/abi/.idr` failed on a module-name mismatch from any directory. No CI job checked them, which is how Stripping.idr sat on main not compiling while PROOF-NEEDS called it closed. - Move src/abi/*.idr to src/abi/PanicAttack/ABI/ (pure renames) and add src/abi/panic-attack-abi.ipkg listing the five modules. - Add the `abi-proofs` job to proven-tests.yml: every PR and push to main runs `idris2 --typecheck src/abi/panic-attack-abi.ipkg` and fails on a non-zero exit or any `Error:` line. It reuses the framework job's pinned installer and Idris2 cache key, and only the actions that workflow already locks, so actions.lock is unchanged. - PROOF-NEEDS.adoc: the gate is now the receipt; the first local receipt is kept; the gate row leaves the open list. EXPLAINME and PROOF-PROGRAMME point at the new paths. CHANGELOG history and the retired .a2ml files are left as they are. Checked locally: the package type-checks (Idris2 0.7.0); a planted false lemma and a planted missing import both fail it; the job's run step passes as written; actionlint 1.7.7 is clean; validate-sha-pins and check-allowed-actions pass with the checksum-pinned yq v4.54.1. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u --- .github/workflows/proven-tests.yml | 56 ++++++++++++++++- EXPLAINME.adoc | 6 +- PROOF-NEEDS.adoc | 60 +++++++++---------- PROOF-PROGRAMME.adoc | 12 ++-- .../ABI}/AttestationUnforgeability.idr | 0 .../ABI}/ClassificationSoundness.idr | 0 .../ABI}/PatternCompleteness.idr | 0 src/abi/{ => PanicAttack/ABI}/Stripping.idr | 0 src/abi/{ => PanicAttack/ABI}/Types.idr | 0 src/abi/panic-attack-abi.ipkg | 15 +++++ 10 files changed, 107 insertions(+), 42 deletions(-) rename src/abi/{ => PanicAttack/ABI}/AttestationUnforgeability.idr (100%) rename src/abi/{ => PanicAttack/ABI}/ClassificationSoundness.idr (100%) rename src/abi/{ => PanicAttack/ABI}/PatternCompleteness.idr (100%) rename src/abi/{ => PanicAttack/ABI}/Stripping.idr (100%) rename src/abi/{ => PanicAttack/ABI}/Types.idr (100%) create mode 100644 src/abi/panic-attack-abi.ipkg diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index 82ab20c..a31591e 100644 --- a/.github/workflows/proven-tests.yml +++ b/.github/workflows/proven-tests.yml @@ -3,7 +3,7 @@ # # proven-tests.yml — the estate's evidence-graded test framework, wired. # -# THE TWO JOBS DO DIFFERENT THINGS AND NEITHER PRETENDS TO BE THE OTHER +# THE JOBS DO DIFFERENT THINGS AND NONE PRETENDS TO BE ANOTHER # --------------------------------------------------------------------- # `ledger` (every PR, blocking, minutes): derives a proven-tests run report from # THIS repo's suite — from a test inventory the runner emitted in the same @@ -22,6 +22,10 @@ # and it would make every contributor wait on a compiler that cannot change # for them. # +# `abi-proofs` (every PR, blocking): type-checks this repository's own Idris2 +# proofs in src/abi with the same pinned Idris2. It reuses the framework job's +# toolchain cache, so it costs a compiler build only on a cold cache. +# # WHY THE REPORT IS A FILE, NOT A PARAGRAPH: docs/INTEROP-PANIC-ATTACK.adoc in # proven-tests-and-benches fixes the mapping in prose; a report plus a verifier # is the same mapping with something at stake. @@ -142,6 +146,56 @@ jobs: retention-days: 30 if-no-files-found: warn + abi-proofs: + # Every PR: type-check this repo's own Idris2 ABI proofs (src/abi). Without + # this, src/abi/PanicAttack/ABI/Stripping.idr sat on main not compiling + # while PROOF-NEEDS.adoc called it closed. The toolchain comes from the same + # pinned installer and cache key as the framework job, so a warm cache makes + # this a type-check, not a compiler build. + name: Idris2 — src/abi proofs type-check + runs-on: ubuntu-latest + timeout-minutes: 60 + steps: + - name: Checkout this repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Checkout proven-tests-and-benches at the pinned commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/proven-tests-and-benches + ref: ${{ env.PROVEN_TESTS_PIN }} + path: .proven-tests + persist-credentials: false + + - name: Cache the Idris2 toolchain + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: ~/.idris2 + key: idris2-v${{ env.IDRIS2_VERSION }}-${{ runner.os }} + + - name: Install Idris2 (chez backend) + working-directory: .proven-tests + env: + IDRIS2_VERSION: v${{ env.IDRIS2_VERSION }} + run: bash scripts/install-idris2.sh + + - name: Type-check src/abi + run: | + set -euo pipefail + export PATH="$HOME/.idris2/bin:$PATH" + idris2 --version + # `idris2 --check` can exit 0 while printing an error, so require + # both a zero exit and no `Error:` line. + status=0 + out="$(idris2 --typecheck src/abi/panic-attack-abi.ipkg 2>&1)" || status=$? + printf '%s\n' "$out" + if [ "$status" -ne 0 ] || grep -q '^Error' <<<"$out"; then + echo "::error::src/abi Idris2 proofs do not type-check (exit $status)" + exit 1 + fi + framework: name: Framework — the grader is exercised (scheduled) if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 8724d1f..f2ea553 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -52,9 +52,9 @@ The README makes claims. This file backs them up. | `src/comment_marker.rs` | Inline `// panic-attack: accepted [- reason]` suppression marker — `//` / `#` / `--` / `;` / `%` leaders, string-literal aware | `src/ffi_kind.rs` | UnsafeFFI (PA013) subtyping: BuildSystem (`build.zig` / `build.rs` — audit-accepted), RuntimeAbi (`bindings/` / `ffi/` / `sys/` / `cdef.zig`), TestMock (`tests/mocks/` / `_stub`), Unknown | `src/jit_context.rs` | JIT-framework classifier: Cranelift / Llvm / Wasm / Javascript / None; `transmute_targets_fn_ptr` recogniser for fn-ptr type-punning -| `src/abi/PatternCompleteness.idr` | PA1 Idris2 proof — every Lang/Category has a detector -| `src/abi/ClassificationSoundness.idr` | PA2 Idris2 proof — severity total order + maxSeverity commutativity -| `src/abi/Stripping.idr` | Layer 1.0 partial — line-comment-strip foundation (shape lemma + base cases of `stripLineCommentsIdempotent` Qed-closed) +| `src/abi/PanicAttack/ABI/PatternCompleteness.idr` | PA1 Idris2 model of analyzer dispatch; vacuous as stated (see `PROOF-NEEDS.adoc`) +| `src/abi/PanicAttack/ABI/ClassificationSoundness.idr` | PA2 Idris2 proof — severity total order, `sevMax` upper bounds, monotone encoding +| `src/abi/PanicAttack/ABI/Stripping.idr` | Layer 1.0 — Idris2 model of line-comment stripping, proved idempotent (`stripLineCommentsIdempotent`) | `src/kanren/` | Logic engine (unification, fact database, taint, cross-lang) | `src/kanren/core.rs` | Term, substitution, unification, FactDB, forward chaining | `src/kanren/taint.rs` | Source→sink tracking (user input, network, deserialization) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index c1e8c65..25b024e 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -27,27 +27,29 @@ compiles at `f2a6a70eaec0cb02331e3264e05f185b5faab0f7`. The only `unsafe` is in `examples/vulnerable_program.rs`, a deliberately buggy program that exists to be scanned. -== Receipt for the Idris2 modules - -* *Checker:* Idris2 0.7.0, the version `proven-tests.yml` pins, built from - tag `v0.7.0` (`27780073c8631826d846499840b3857d9b9a4fd5`) on Chez Scheme - 9.5.8. -* *Source:* `src/abi/*.idr` at - `3dc4728762f37c1e5bebdb988783c7683c50fb55`. -* *Invocation:* the modules are named `PanicAttack.ABI.` but live in - `src/abi/`, so `idris2 --check src/abi/.idr` fails on a module-name - mismatch from any directory. Each was checked from a tree that places - `src/abi/.idr` at `PanicAttack/ABI/.idr`, with - `idris2 --check PanicAttack/ABI/.idr`. A pass is exit 0 *and* no - `Error:` line, because `idris2 --check` can exit 0 while printing an - error. -* *Result:* all five modules pass. Every module sets `%default total` and - uses no `believe_me`, `assert_total`, `postulate` or holes. -* *Negative controls:* a planted false lemma and a planted non-terminating - definition in `Stripping.idr` were both rejected, so the check can fail. -* *Gate:* no CI job runs this check. That obligation is `OPEN` below. Until - it closes, the statuses here rest on this one local run, and any change - to `src/abi/` invalidates them. +== How the Idris2 modules are checked + +The modules live at `src/abi/PanicAttack/ABI/.idr`, so each path matches +its module name, and `src/abi/panic-attack-abi.ipkg` lists them all. + +* *Gate:* the `abi-proofs` job in `.github/workflows/proven-tests.yml` runs + on every pull request and on pushes to `main`: + `idris2 --typecheck src/abi/panic-attack-abi.ipkg`. A pass is exit 0 + *and* no `Error:` line, because `idris2 --check` can exit 0 while printing + an error. Its toolchain is Idris2 0.7.0 from the same pinned installer and + cache as the framework job. Each green run of that job is the current + receipt; a failing run revokes the statuses below. +* *Negative controls* for the package route: a planted false lemma and a + planted missing import each make it exit non-zero with an `Error:` line. +* *Hygiene:* every module sets `%default total` and uses no `believe_me`, + `assert_total`, `postulate` or holes. + +First receipt, before the gate existed: Idris2 0.7.0, built from tag +`v0.7.0` (`27780073c8631826d846499840b3857d9b9a4fd5`) on Chez Scheme 9.5.8, +over `src/abi/*.idr` at `3dc4728762f37c1e5bebdb988783c7683c50fb55`. Each +module was checked from a module-shaped copy of the tree. All five passed, +and a planted false lemma and a planted non-terminating definition in +`Stripping.idr` were both rejected. == Ledger @@ -57,14 +59,14 @@ exists to be scanned. |Severity order: `Low < Medium < High < Critical` is a total order; `sevMax` is an upper bound; the numeric encoding is monotone (PA2) -|`src/abi/ClassificationSoundness.idr` +|`src/abi/PanicAttack/ABI/ClassificationSoundness.idr` |`PROVEN` (model) |The model's `Severity` matches the variant names and order of `src/types.rs`; that correspondence is `ASSUMED` (a hand transcription). The Rust order itself comes from `#[derive(PartialOrd, Ord)]`. |Line-comment stripping is idempotent: `strip (strip s) = strip s` -|`src/abi/Stripping.idr` +|`src/abi/PanicAttack/ABI/Stripping.idr` |`PROVEN` (model) |Did not compile on `main` before `3dc4728`; repaired there without changing the theorem. The repaired model equals the previous one: @@ -74,7 +76,7 @@ comments and string literals are not modelled. Model to Rust `strip_proof_comments`: `ASSUMED`. |Attestation chain: integrity, authenticity, non-repudiation -|`src/abi/AttestationUnforgeability.idr` +|`src/abi/PanicAttack/ABI/AttestationUnforgeability.idr` |`PROVEN` (model), relative to the `ASSUMED` hypotheses listed here |The module's `parameters` block assumes: @@ -92,7 +94,7 @@ model, not a computational security reduction. Model to |Every language reaches an analyzer; every weak-point category has a detector; cross-language checks run on every file (PA1) -|`src/abi/PatternCompleteness.idr` +|`src/abi/PanicAttack/ABI/PatternCompleteness.idr` |`PROVEN` (model); supports no claim about the Rust code |The theorem is vacuous: `GenericAnalyzer : HasAnalyzer lang` inhabits the witness type for every language, so it holds whatever the dispatch @@ -107,7 +109,7 @@ when `configuration.is_some()`. That model claim is false of the implementation. |Declarations for the ABI-facing types and their C integer encodings -|`src/abi/Types.idr` +|`src/abi/PanicAttack/ABI/Types.idr` |No theorem |Repaired in `3dc4728` so it compiles. It contains no proof and nothing imports it. Drift: its `Severity` is `Info / Warning / Error / Critical` @@ -130,12 +132,6 @@ not establish a faithful hexad-to-octad map. |=== |Obligation |Verifier (§1, §1.2) |Notes -|Gate the Idris2 modules in CI -|CI -|Run the receipt's invocation on every change to `src/abi/`, failing on -any `Error:` line. Moving the files to `src/abi/PanicAttack/ABI/` would -let a plain `idris2 --check` work. - |`strip_proof_comments` is idempotent and preserves positions outside comments and strings |Creusot/Pearlite and Verus diff --git a/PROOF-PROGRAMME.adoc b/PROOF-PROGRAMME.adoc index 7726fb8..9bcb2ce 100644 --- a/PROOF-PROGRAMME.adoc +++ b/PROOF-PROGRAMME.adoc @@ -14,12 +14,12 @@ ____ [width="100%",cols="34%,33%,33%",options="header",] |=== |ID |File |Mechanises -|*PA1* |`+src/abi/PatternCompleteness.idr+` |Every `+Lang+` constructor +|*PA1* |`+src/abi/PanicAttack/ABI/PatternCompleteness.idr+` |Every `+Lang+` constructor has at least one analyzer; every `+WPCategory+` has at least one detector; cross-language checks apply uniformly. Top theorem: `+completeScanForAll+`. -|*PA2* |`+src/abi/ClassificationSoundness.idr+` |`+Severity+` is totally +|*PA2* |`+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` |`+Severity+` is totally ordered (`+LTE+`); `+maxSeverity+` is commutative + idempotent; numeric ABI encoding preserves the ordering. |=== @@ -81,7 +81,7 @@ Worked example — *PA004 (UnsafeCode)*: [source,idris] ---- --- src/abi/PA004_UnsafeCode.idr +-- src/abi/PanicAttack/ABI/PA004_UnsafeCode.idr SoundnessPA004 : (file : String) -> (loc : Loc) -> contains (stripStrings file) "unsafe " loc -> isUnsafeBlock (locate file loc) @@ -266,7 +266,7 @@ Recommended order (each row is parallel-iseable; rows are sequenced): |=== |# |Phase |Output |Estimated effort |Risk |1 |*Foundation*: Layer 1.0 (comment/string-strip idempotence + token -preservation) |`+src/abi/Stripping.idr+` + 1 Idris2 module |3–5 days +preservation) |`+src/abi/PanicAttack/ABI/Stripping.idr+` + 1 Idris2 module |3–5 days |low |2 |*Quick wins*: Hexad↔Octad roundtrip proptest + Layer 1 @@ -316,8 +316,8 @@ docs/proof artefacts that don’t touch the hot path. * `+PROOF-NEEDS.md+` — current proof-debt ledger (this document is the long-term plan; that one tracks the immediate next step). -* `+src/abi/PatternCompleteness.idr+` (PA1) -* `+src/abi/ClassificationSoundness.idr+` (PA2) +* `+src/abi/PanicAttack/ABI/PatternCompleteness.idr+` (PA1) +* `+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` (PA2) * `+hyperpolymath/proven+` — leaf validator library; cross-fit candidates listed above. * ROADMAP.adoc "`Long-Term`" section: "`Formal verification of core diff --git a/src/abi/AttestationUnforgeability.idr b/src/abi/PanicAttack/ABI/AttestationUnforgeability.idr similarity index 100% rename from src/abi/AttestationUnforgeability.idr rename to src/abi/PanicAttack/ABI/AttestationUnforgeability.idr diff --git a/src/abi/ClassificationSoundness.idr b/src/abi/PanicAttack/ABI/ClassificationSoundness.idr similarity index 100% rename from src/abi/ClassificationSoundness.idr rename to src/abi/PanicAttack/ABI/ClassificationSoundness.idr diff --git a/src/abi/PatternCompleteness.idr b/src/abi/PanicAttack/ABI/PatternCompleteness.idr similarity index 100% rename from src/abi/PatternCompleteness.idr rename to src/abi/PanicAttack/ABI/PatternCompleteness.idr diff --git a/src/abi/Stripping.idr b/src/abi/PanicAttack/ABI/Stripping.idr similarity index 100% rename from src/abi/Stripping.idr rename to src/abi/PanicAttack/ABI/Stripping.idr diff --git a/src/abi/Types.idr b/src/abi/PanicAttack/ABI/Types.idr similarity index 100% rename from src/abi/Types.idr rename to src/abi/PanicAttack/ABI/Types.idr diff --git a/src/abi/panic-attack-abi.ipkg b/src/abi/panic-attack-abi.ipkg new file mode 100644 index 0000000..4d874b8 --- /dev/null +++ b/src/abi/panic-attack-abi.ipkg @@ -0,0 +1,15 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- The Idris2 ABI models and proofs. Type-check with: +-- idris2 --typecheck src/abi/panic-attack-abi.ipkg +-- A pass is exit 0 and no `Error:` line in the output. +package panic-attack-abi + +sourcedir = "." + +modules = PanicAttack.ABI.Types + , PanicAttack.ABI.PatternCompleteness + , PanicAttack.ABI.ClassificationSoundness + , PanicAttack.ABI.Stripping + , PanicAttack.ABI.AttestationUnforgeability