From 79cda2776dee7feea9a106c66515c0ae9cd67453 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 10:14:09 +0100 Subject: [PATCH 1/2] audit: classify 2 PA021 legitimate mathematical axioms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two Agda postulates flagged by PA021, both with inline justification: proofs/agda/Basic.agda: funext (function extensionality) — HoTT-standard axiom; Coq's FunctionalExtensionality, Lean's funext, HoTT Axiom 2.9.3. Provable in Cubical Agda; postulated in plain Agda. proofs/agda/SoundnessPreservation.agda: Conflicts is an INTENTIONAL parameter (abstract binary predicate); the caller supplies a concrete proof of ¬ Conflicts at use-site. Theorem interface, not debt. Adds: - audits/assail-classifications.a2ml (entries=2) - audits/audit-pa021-axioms-2026-05-26.md Anti-gameability: only these two postulates suppressed; new postulates in these or other proof files remain visible. Refs hyperpolymath/panic-attack#32 (estate sweep tracker). Co-Authored-By: Claude Opus 4.7 (1M context) --- audits/assail-classifications.a2ml | 141 +++++------------------- audits/audit-pa021-axioms-2026-05-26.md | 59 ++++++++++ 2 files changed, 89 insertions(+), 111 deletions(-) create mode 100644 audits/audit-pa021-axioms-2026-05-26.md diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml index 22ae0baa..0033afc4 100644 --- a/audits/assail-classifications.a2ml +++ b/audits/assail-classifications.a2ml @@ -1,113 +1,32 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# Classification registry for panic-attack assail findings that are confirmed -# legitimate patterns and should not be treated as actionable weak-points. -# -# Format mirrors the panic-attack user-classification registry protocol. -# Cross-reference: audits/audit-ffi-boundary.md - -[metadata] -name = "echidna-assail-classifications" -project = "echidna" -version = "1.0.0" -schema_version = "1.0.0" +;; SPDX-License-Identifier: MPL-2.0 +;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +;; +;; Assail Classifications — echidna +;; See panic-attack/.claude/CLAUDE.md § "User-Classification Registry". (assail-classifications - - ; ─── src/rust/ffi/mod.rs — C-ABI exports + raw-pointer handling ────────── - (classification - (file "src/rust/ffi/mod.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §1") - (rationale "C-ABI exports for the Zig FFI layer; 24 documented unsafe blocks reviewed in linked audit")) - - (classification - (file "src/rust/ffi/mod.rs") - (category "ResourceLeak") - (audit "audits/audit-ffi-boundary.md §1") - (rationale "Box::into_raw ownership-transfer to Zig caller; Zig calls rust_free_* to drop — not an actual leak")) - - ; ─── src/rust/ffi/spark_axiom.rs — Rust→SPARK via C ABI ───────────────── - (classification - (file "src/rust/ffi/spark_axiom.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §2") - (rationale "extern C callouts to SPARK-compiled policy enforcement; pointer preconditions enforced by Ada contracts")) - - ; ─── src/rust/proof_search.rs — Chapel FFI, feature-gated ─────────────── - (classification - (file "src/rust/proof_search.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §3") - (rationale "Chapel parallel-search FFI behind #[cfg(feature = chapel)]; all 7 unsafe blocks reviewed in linked audit")) - - ; ─── src/interfaces/graphql/ffi_wrapper.rs ──────────────────────────────── - (classification - (file "src/interfaces/graphql/ffi_wrapper.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §4") - (rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1")) - - ; ─── src/interfaces/grpc/ffi_wrapper.rs ─────────────────────────────────── - (classification - (file "src/interfaces/grpc/ffi_wrapper.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §4") - (rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1")) - - ; ─── src/interfaces/rest/ffi_wrapper.rs ─────────────────────────────────── - (classification - (file "src/interfaces/rest/ffi_wrapper.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §4") - (rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1")) - - ; ─── src/rust/provers/z3.rs — SMT-LIB parser backend ───────────────────── - (classification - (file "src/rust/provers/z3.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §5") - (rationale "No unsafe blocks present; panic-attack unwrap_calls/allocations score reflects legitimate SMT-LIB parsing patterns (18 unwrap_or_else for parser recovery, 54KB allocations normal for proof state)")) - - (classification - (file "src/rust/provers/z3.rs") - (category "PanicPath") - (audit "audits/audit-ffi-boundary.md §5") - (rationale "Parser .expect(token) method calls (line 727+ self.expect) are structured S-expression parsing, not panic sites; error propagated via ? operator")) - - ; ─── src/rust/fault_tolerance/resilience.rs — Circuit breaker ───────────── - (classification - (file "src/rust/fault_tolerance/resilience.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §5") - (rationale "No unsafe blocks; allocations reflect AtomicU32 counter management and Vec growth in backoff/retry state machines — expected for fault tolerance")) - - ; ─── src/rust/provers/pvs.rs — PVS backend (3168 LoC) ────────────────────── - (classification - (file "src/rust/provers/pvs.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §6") - (rationale "No unsafe blocks; allocations (204 units) reflect PVS AST structures (expr, types, case selections, quantifiers); pattern matches enum-to-Box conversions in parser (ln 46-100)")) - - ; ─── src/rust/provers/hol4.rs — HOL4 backend (2621 LoC) ─────────────────── - (classification - (file "src/rust/provers/hol4.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §7") - (rationale "No unsafe blocks; allocations (174 units) + 1 panic site reflect HOL4 tactic evaluation & type parser recursion (spawn at line 1430, vec! at lines 928+)")) - - (classification - (file "src/rust/provers/hol4.rs") - (category "PanicPath") - (audit "audits/audit-ffi-boundary.md §7") - (rationale "One panic site from process spawn error handling (line 1430); struct-to-vec conversions for tactics (Metis, Simp) return Err not panic")) - - ; ─── src/rust/provers/mod.rs — 105 prover backend exports ──────────────── - (classification - (file "src/rust/provers/mod.rs") - (category "UnsafeCode") - (audit "audits/audit-ffi-boundary.md §8") - (rationale "No unsafe blocks; allocations (148 units) reflect 105 prover modules and ProverKind enum variants (ln 96-200); structural not FFI")) - -) + (metadata + (version "1.0.0") + (project "echidna") + (last-updated "2026-05-26") + (entries 2) + (status "active")) + + ;; ─── PA021 ProofDrift — legitimate mathematical axioms ───────────────── + ;; Both findings are postulates with inline justification in the source + ;; (funext is HoTT-standard; Conflicts is an INTENTIONAL parameter not a + ;; proof debt). See audits/audit-pa021-axioms-2026-05-26.md. + + (classification + (file "proofs/agda/Basic.agda") + (category "ProofDrift") + (classification "legitimate-mathematical-axiom") + (audit "audits/audit-pa021-axioms-2026-05-26.md §1") + (rationale "funext: function extensionality, postulated in plain Agda (provable in Cubical Agda); standard mathematical axiom accepted by Coq, Lean, HoTT. Inline justification at line 172-177.")) + + (classification + (file "proofs/agda/SoundnessPreservation.agda") + (category "ProofDrift") + (classification "intentional-parameter") + (audit "audits/audit-pa021-axioms-2026-05-26.md §2") + (rationale "Conflicts is an abstract binary predicate parameter; the caller supplies a concrete proof of ¬ Conflicts when sets are disjoint. INTENTIONAL design parameter, not proof debt. Inline justification at line 44-53."))) diff --git a/audits/audit-pa021-axioms-2026-05-26.md b/audits/audit-pa021-axioms-2026-05-26.md new file mode 100644 index 00000000..745a64b4 --- /dev/null +++ b/audits/audit-pa021-axioms-2026-05-26.md @@ -0,0 +1,59 @@ + + +# Audit: legitimate mathematical axioms (PA021) + +**Auditor**: Jonathan D.A. Jewell +**Date**: 2026-05-26 +**Scope**: 2 panic-attack PA021 ProofDrift findings, both postulates with inline justification in the source. +**Cross-reference**: campaign tracker [hyperpolymath/panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32). +**Registry**: `audits/assail-classifications.a2ml`. + +## §1 — `proofs/agda/Basic.agda` — `funext` (function extensionality) + +Line 172-179 of `Basic.agda`: + +```agda +-- provable in Cubical Agda (--cubical). In plain Agda it must be +-- postulated. It is a standard mathematical axiom accepted by all +-- major proof assistants (Coq's Functional Extensionality, Lean's +-- funext, HoTT axiom). It does NOT compromise soundness. +-- See: HoTT Book, Section 2.9; nLab "function extensionality" +postulate + funext : {A B : Set} {f g : A → B} + → ((x : A) → f x ≡ g x) → f ≡ g +``` + +`funext` is one of the foundational axioms of dependent type theory. Coq has `FunctionalExtensionality.functional_extensionality`; Lean's mathlib has `funext`; HoTT has Axiom 2.9.3. It is provable in Cubical Agda but must be postulated in plain Agda — a well-known constraint of the underlying type theory. + +**Classification**: `legitimate-mathematical-axiom`. + +## §2 — `proofs/agda/SoundnessPreservation.agda` — `Conflicts` (intentional parameter) + +Line 44-53 of `SoundnessPreservation.agda`: + +```agda +-- Conflicts is an abstract binary predicate over two axiom lists. +-- We leave it as a postulate-free parameter: the caller supplies a +-- concrete proof of ¬ Conflicts when they know the sets are disjoint. +... +-- an axiom that the other marks Reject. +postulate + Conflicts : List Axiom → List Axiom → Set +``` + +The comment explicitly tags this as "INTENTIONAL PARAMETER — 'Conflicts' is domain knowledge about which axioms conflict". This is a parameterised theorem: the theorem statement quantifies over an arbitrary `Conflicts` predicate, and the caller proves `¬ Conflicts` (or supplies a concrete relation) at use-site. This is NOT a proof debt — it is the *interface* of the theorem. + +**Classification**: `intentional-parameter`. + +## Anti-gameability + +The registry is `audits/assail-classifications.a2ml`. Adding new postulates to either file does NOT become silently suppressed — only these two specific postulates are classified. Any new `postulate` or `sorry` in these or other proof files remains visible. + +## Verification + +No proof source touched; `agda --check` rebuild is moot (input unchanged from main). + +Refs hyperpolymath/panic-attack#32. From 35fb127207551fd90a7651c4d7ae5f6bd109fbce Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 10:14:47 +0100 Subject: [PATCH 2/2] fix: restore pre-existing FFI-boundary classifications (was overwritten) Previous commit on this branch overwrote the existing 14 FFI-boundary classification entries in audits/assail-classifications.a2ml. This commit restores them in full and re-appends the 2 new PA021 entries. No-op semantically vs the intended PR state, but corrects the diff. Co-Authored-By: Claude Opus 4.7 (1M context) --- audits/assail-classifications.a2ml | 136 +++++++++++++++++++++++++---- 1 file changed, 117 insertions(+), 19 deletions(-) diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml index 0033afc4..a2946d7a 100644 --- a/audits/assail-classifications.a2ml +++ b/audits/assail-classifications.a2ml @@ -1,32 +1,130 @@ -;; SPDX-License-Identifier: MPL-2.0 -;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -;; -;; Assail Classifications — echidna -;; See panic-attack/.claude/CLAUDE.md § "User-Classification Registry". +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Classification registry for panic-attack assail findings that are confirmed +# legitimate patterns and should not be treated as actionable weak-points. +# +# Format mirrors the panic-attack user-classification registry protocol. +# Cross-reference: audits/audit-ffi-boundary.md + +[metadata] +name = "echidna-assail-classifications" +project = "echidna" +version = "1.0.0" +schema_version = "1.0.0" (assail-classifications - (metadata - (version "1.0.0") - (project "echidna") - (last-updated "2026-05-26") - (entries 2) - (status "active")) - ;; ─── PA021 ProofDrift — legitimate mathematical axioms ───────────────── - ;; Both findings are postulates with inline justification in the source - ;; (funext is HoTT-standard; Conflicts is an INTENTIONAL parameter not a - ;; proof debt). See audits/audit-pa021-axioms-2026-05-26.md. + ; ─── src/rust/ffi/mod.rs — C-ABI exports + raw-pointer handling ────────── + (classification + (file "src/rust/ffi/mod.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §1") + (rationale "C-ABI exports for the Zig FFI layer; 24 documented unsafe blocks reviewed in linked audit")) + + (classification + (file "src/rust/ffi/mod.rs") + (category "ResourceLeak") + (audit "audits/audit-ffi-boundary.md §1") + (rationale "Box::into_raw ownership-transfer to Zig caller; Zig calls rust_free_* to drop — not an actual leak")) + + ; ─── src/rust/ffi/spark_axiom.rs — Rust→SPARK via C ABI ───────────────── + (classification + (file "src/rust/ffi/spark_axiom.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §2") + (rationale "extern C callouts to SPARK-compiled policy enforcement; pointer preconditions enforced by Ada contracts")) + + ; ─── src/rust/proof_search.rs — Chapel FFI, feature-gated ─────────────── + (classification + (file "src/rust/proof_search.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §3") + (rationale "Chapel parallel-search FFI behind #[cfg(feature = chapel)]; all 7 unsafe blocks reviewed in linked audit")) + + ; ─── src/interfaces/graphql/ffi_wrapper.rs ──────────────────────────────── + (classification + (file "src/interfaces/graphql/ffi_wrapper.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §4") + (rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1")) + + ; ─── src/interfaces/grpc/ffi_wrapper.rs ─────────────────────────────────── + (classification + (file "src/interfaces/grpc/ffi_wrapper.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §4") + (rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1")) + + ; ─── src/interfaces/rest/ffi_wrapper.rs ─────────────────────────────────── + (classification + (file "src/interfaces/rest/ffi_wrapper.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §4") + (rationale "Interface-layer wrapper over src/rust/ffi/mod.rs C-ABI; CStr/raw-pointer patterns identical to §1")) + + ; ─── src/rust/provers/z3.rs — SMT-LIB parser backend ───────────────────── + (classification + (file "src/rust/provers/z3.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §5") + (rationale "No unsafe blocks present; panic-attack unwrap_calls/allocations score reflects legitimate SMT-LIB parsing patterns (18 unwrap_or_else for parser recovery, 54KB allocations normal for proof state)")) + + (classification + (file "src/rust/provers/z3.rs") + (category "PanicPath") + (audit "audits/audit-ffi-boundary.md §5") + (rationale "Parser .expect(token) method calls (line 727+ self.expect) are structured S-expression parsing, not panic sites; error propagated via ? operator")) + + ; ─── src/rust/fault_tolerance/resilience.rs — Circuit breaker ───────────── + (classification + (file "src/rust/fault_tolerance/resilience.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §5") + (rationale "No unsafe blocks; allocations reflect AtomicU32 counter management and Vec growth in backoff/retry state machines — expected for fault tolerance")) + + ; ─── src/rust/provers/pvs.rs — PVS backend (3168 LoC) ────────────────────── + (classification + (file "src/rust/provers/pvs.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §6") + (rationale "No unsafe blocks; allocations (204 units) reflect PVS AST structures (expr, types, case selections, quantifiers); pattern matches enum-to-Box conversions in parser (ln 46-100)")) + + ; ─── src/rust/provers/hol4.rs — HOL4 backend (2621 LoC) ─────────────────── + (classification + (file "src/rust/provers/hol4.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §7") + (rationale "No unsafe blocks; allocations (174 units) + 1 panic site reflect HOL4 tactic evaluation & type parser recursion (spawn at line 1430, vec! at lines 928+)")) + + (classification + (file "src/rust/provers/hol4.rs") + (category "PanicPath") + (audit "audits/audit-ffi-boundary.md §7") + (rationale "One panic site from process spawn error handling (line 1430); struct-to-vec conversions for tactics (Metis, Simp) return Err not panic")) + + ; ─── src/rust/provers/mod.rs — 105 prover backend exports ──────────────── + (classification + (file "src/rust/provers/mod.rs") + (category "UnsafeCode") + (audit "audits/audit-ffi-boundary.md §8") + (rationale "No unsafe blocks; allocations (148 units) reflect 105 prover modules and ProverKind enum variants (ln 96-200); structural not FFI")) + + ; ─── PA021 ProofDrift — legitimate mathematical axioms ─────────────────── + ; Both findings are postulates with inline justification in the source + ; (funext is HoTT-standard; Conflicts is INTENTIONAL parameter, not debt). + ; See audits/audit-pa021-axioms-2026-05-26.md. (classification (file "proofs/agda/Basic.agda") (category "ProofDrift") - (classification "legitimate-mathematical-axiom") (audit "audits/audit-pa021-axioms-2026-05-26.md §1") - (rationale "funext: function extensionality, postulated in plain Agda (provable in Cubical Agda); standard mathematical axiom accepted by Coq, Lean, HoTT. Inline justification at line 172-177.")) + (rationale "funext: function extensionality, postulated in plain Agda (provable in Cubical); standard mathematical axiom accepted by Coq, Lean, HoTT. Inline justification at line 172-177.")) (classification (file "proofs/agda/SoundnessPreservation.agda") (category "ProofDrift") - (classification "intentional-parameter") (audit "audits/audit-pa021-axioms-2026-05-26.md §2") - (rationale "Conflicts is an abstract binary predicate parameter; the caller supplies a concrete proof of ¬ Conflicts when sets are disjoint. INTENTIONAL design parameter, not proof debt. Inline justification at line 44-53."))) + (rationale "Conflicts is an abstract binary predicate parameter; caller supplies concrete proof of ¬ Conflicts when sets are disjoint. INTENTIONAL parameter, not proof debt. Inline justification at line 44-53.")) + +)