diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index 9aa00127..d36f2149 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -78,8 +78,12 @@ no collisions in kind_to_u8 |I2 |E7 GNN embedding faithfulness |`+src/abi/EchidnaABI/Gnn.idr+` |Structural properties, feature bounds, score normalisation |I2 -|E9 Proof composition soundness |`+proofs/agda/ProofComposition.agda+` -|Soundness preservation, axiom conflict detection |Agda +|E9 Proof composition soundness |`+meta-checker/src/Echidna/Composition.agda+` +|Cut preserves semantic soundness; explosion shows a conflict check is +load-bearing; a sound detector realises every composite, and a sound +detector that decides its conflict relation returns a conflict witness for +every inconsistent one. Theory over an arbitrary logic; no Rust composer +exists to verify |Agda |E12 ProofState serialization losslessness |`+verification/proofs/idris2/ProofStateSerialisation.idr+` diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index bcf6c700..14dabd27 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -188,6 +188,13 @@ functions do not *compute* under Cubical transports. The corpus is clean log would weaken the profile. Full Cubical and the independent Rocq and Lean legs were not run for this receipt. Changes to any recorded source invalidate its use for that changed source until a fresh check is recorded. +**Since that receipt,** `+MetaChecker.agda+` changed: it now also imports +`+Composition+` (R6), so the checked closure is ten modules. The nine modules +this row covers are unchanged and keep their recorded digests, so the row +stands for them; the entrypoint's new digest, and R6, are covered only once +the `+agda-meta-checker+` job, which now prints a source-bound receipt +(toolchain, flags, library descriptors and every source's SHA-256), has run +on `+main+`. **Correction to the old receipt:** `+916b769+` predates `+Integrity+`, `+ClampTrust+` and `+Receipt+`, and its entrypoint omitted @@ -265,19 +272,26 @@ checked, untranslated. ECHIDNA's `+src/rust/exchange/+` speaks Dedukti, so the transport route exists; using it is unstarted work, not a missing capability. |R6. E9 "proof composition soundness" -|`+argued+`, with a location defect -|`+PROOF-NEEDS+` evidences it with `+proofs/agda/ProofComposition.agda+`. But -`+PROOF-POLICY+` §3 says `+proofs//+` trees are fixtures, "`outside -this policy`". -|The obligation survives; its evidence sits where the policy says evidence -cannot live. **New (2026-11-01):** the whole `+proofs/agda/+` tree — 13 files -including `+ProofComposition.agda+` — type-checks under -`+agda --safe --without-K --cubical-compatible+`, 13/13, no postulates. So the -cheap remedy is the *move* to a policy-conformant location -(`+verification/proofs/agda/+`), not re-stating the obligation as unsupported: -the evidence is good, it is merely filed where §3 says evidence cannot live. -Recorded, not resolved — moving it is a repository change with cross-references -to update, so it is left as a named action rather than done silently. +|`+argued+` until the `+agda-meta-checker+` job prints a source-bound receipt +for this module on `+main+` +|`+meta-checker/src/Echidna/Composition.agda+`, imported by +`+MetaChecker.agda+` and so inside the `+agda-meta-checker+` closure (pinned +Agda 2.7.0.1, canonical flags). +|*Corrected 2026-11-09.* The earlier entry called the old evidence "good, +merely misfiled". It was not good: `+ProofComposition.agda+` proved +list-append associativity, and `+SoundnessPreservation.agda+`'s +`+compose-sound+` discharged a Bool flag with `+∧+` while ignoring its conflict +hypothesis. The replacement is theory over an arbitrary logic: `+cut+` +(composition preserves semantic soundness), `+explosion+` (why a conflict +check is load-bearing), `+compose-realised+`, and `+detector-must-flag+` +(a detector that decides its conflict relation returns a conflict witness +for every inconsistent composition; without decidability only +`+detector-cannot-miss+`, a double negation, holds). Type-checked locally +under the canonical flags (Agda 2.6.3, not the pinned toolchain, so not a +receipt). No +Rust code composes proofs, so no implementation is claimed. The two corpus +files stay in `+proofs/agda/+` as fixtures, with headers saying what they +show. Rocq/Lean rechecks (§2): not started. |=== @@ -315,9 +329,9 @@ row. They exercise parsers and backends. Listing them is deliberate: an absent row should read as *out of policy*, not *forgotten*. The same holds for `+archive/logtalk/+` (dead, quarantined) and for `+echidna-playground/+`. -Note the tension with R6 — one artefact in a corpus directory is cited by -`+PROOF-NEEDS+` as covering a real obligation. §3 is why that is a defect in -placement rather than a status question. +R6 used to cite a corpus artefact as covering a real obligation. It now cites +`+meta-checker/src/Echidna/Composition.agda+`, and both corpus files say in +their headers that they are not E9 evidence. == Standing assumptions diff --git a/meta-checker/src/Echidna/Composition.agda b/meta-checker/src/Echidna/Composition.agda new file mode 100644 index 00000000..1cf6c2e6 --- /dev/null +++ b/meta-checker/src/Echidna/Composition.agda @@ -0,0 +1,187 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +------------------------------------------------------------------------ +-- Proof composition soundness and why conflict detection matters (E9) +-- +-- Theory, stated for an arbitrary logic: a type of formulae, a type of +-- models and a satisfaction relation are module parameters (not +-- postulates). A proof is the semantic certificate a trusted kernel is +-- assumed to give: every model of its axioms satisfies its goal. The +-- kernel's own soundness is the ASSUMED boundary; this module proves what +-- composing such certificates preserves, and what it does not. +-- +-- cut composition is sound: if Γ₁ entails φ and φ,Γ₂ +-- entails ψ, then Γ₁,Γ₂ entails ψ. Both premises +-- are used; neither is ignored. +-- weaken-left/right adding axioms never breaks an entailment. +-- explosion an inconsistent axiom set entails everything, so +-- soundness preservation alone says nothing once the +-- composed axioms conflict; +-- compose-realised with a conflict detector that is sound (no reported +-- conflict ⇒ the joined axioms have a model), the +-- composite's axioms and goal hold together in some +-- model: the composition is not vacuously "sound"; +-- detector-cannot-miss for any sound detector, "no conflict" is refutable +-- whenever the joined axioms are inconsistent +-- (only a double negation, for an arbitrary relation); +-- detector-must-flag a sound detector that DECIDES its conflict relation +-- returns a conflict witness, the reportable flag, +-- whenever the joined axioms are inconsistent; +-- Literals.* a concrete logic in which pos 0 and neg 0 clash, +-- and that clash entails an unrelated goal. +-- +-- This replaces proofs/agda/SoundnessPreservation.agda as E9's evidence: +-- that file's `compose-sound` discharged a Bool flag with `∧` and never +-- used its conflict hypothesis. No ECHIDNA Rust code composes proofs +-- today, so nothing here verifies an implementation; it states the +-- obligation a future composer and its conflict detector must meet. +-- +-- Checked with: agda --safe --without-K --cubical-compatible +-- No postulates. +------------------------------------------------------------------------ + +module Echidna.Composition where + +open import Data.Bool using (Bool; true; false) +open import Data.Nat using (ℕ) +open import Data.List using (List; []; _∷_; _++_) +open import Data.Product using (Σ; _,_; _×_) +open import Data.Empty using (⊥; ⊥-elim) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) + +-- Every element satisfies P (defined here to avoid library-version drift). +data All {A : Set} (P : A → Set) : List A → Set where + [] : All P [] + _∷_ : {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs) + +module Semantics (Form Model : Set) (_⊨_ : Model → Form → Set) where + + Ctx : Set + Ctx = List Form + + _⊨*_ : Model → Ctx → Set + M ⊨* Γ = All (M ⊨_) Γ + + -- Semantic entailment: every model of Γ satisfies φ. + _⊩_ : Ctx → Form → Set + Γ ⊩ φ = (M : Model) → M ⊨* Γ → M ⊨ φ + + Consistent : Ctx → Set + Consistent Γ = Σ Model (λ M → M ⊨* Γ) + + ---------------------------------------------------------------------- + -- Splitting and joining satisfaction across _++_ + ---------------------------------------------------------------------- + + join : {M : Model} (Γ Δ : Ctx) → M ⊨* Γ → M ⊨* Δ → M ⊨* (Γ ++ Δ) + join [] Δ [] d = d + join (_ ∷ Γ) Δ (p ∷ g) d = p ∷ join Γ Δ g d + + left : {M : Model} (Γ Δ : Ctx) → M ⊨* (Γ ++ Δ) → M ⊨* Γ + left [] Δ _ = [] + left (_ ∷ Γ) Δ (p ∷ h) = p ∷ left Γ Δ h + + right : {M : Model} (Γ Δ : Ctx) → M ⊨* (Γ ++ Δ) → M ⊨* Δ + right [] Δ h = h + right (_ ∷ Γ) Δ (_ ∷ h) = right Γ Δ h + + ---------------------------------------------------------------------- + -- Composition preserves soundness + ---------------------------------------------------------------------- + + -- A certified proof: axioms, goal, and the kernel's semantic certificate. + record Proof : Set where + constructor certified + field + axioms : Ctx + goal : Form + sound : axioms ⊩ goal + open Proof public + + -- Cut: the second proof uses the first one's goal as a lemma. + cut : {Γ₁ Γ₂ : Ctx} {φ ψ : Form} → Γ₁ ⊩ φ → (φ ∷ Γ₂) ⊩ ψ → (Γ₁ ++ Γ₂) ⊩ ψ + cut {Γ₁} {Γ₂} h₁ h₂ M m = h₂ M (h₁ M (left Γ₁ Γ₂ m) ∷ right Γ₁ Γ₂ m) + + compose : (p : Proof) (Γ₂ : Ctx) (ψ : Form) → (goal p ∷ Γ₂) ⊩ ψ → Proof + compose p Γ₂ ψ h = certified (axioms p ++ Γ₂) ψ (cut (sound p) h) + + weaken-right : {Γ : Ctx} (Δ : Ctx) {φ : Form} → Γ ⊩ φ → (Γ ++ Δ) ⊩ φ + weaken-right {Γ} Δ h M m = h M (left Γ Δ m) + + weaken-left : (Δ : Ctx) {Γ : Ctx} {φ : Form} → Γ ⊩ φ → (Δ ++ Γ) ⊩ φ + weaken-left Δ {Γ} h M m = h M (right Δ Γ m) + + ---------------------------------------------------------------------- + -- Why the conflict check is load-bearing + ---------------------------------------------------------------------- + + -- Inconsistent axioms entail every formula: "sound" becomes vacuous. + explosion : {Γ : Ctx} → ¬ Consistent Γ → (φ : Form) → Γ ⊩ φ + explosion nc φ M m = ⊥-elim (nc (M , m)) + + -- A conflict detector is sound when "no conflict" guarantees a model of + -- the joined axiom sets. + SoundDetector : (Ctx → Ctx → Set) → Set + SoundDetector Conflicts = (Γ Δ : Ctx) → ¬ Conflicts Γ Δ → Consistent (Γ ++ Δ) + + -- With a sound detector and no reported conflict, the composite is + -- realised: one model satisfies all its axioms and its goal. + compose-realised : {Conflicts : Ctx → Ctx → Set} → SoundDetector Conflicts + → {Γ₁ Γ₂ : Ctx} {φ ψ : Form} + → Γ₁ ⊩ φ → (φ ∷ Γ₂) ⊩ ψ → ¬ Conflicts Γ₁ Γ₂ + → Σ Model (λ M → M ⊨* (Γ₁ ++ Γ₂) × M ⊨ ψ) + compose-realised det {Γ₁} {Γ₂} h₁ h₂ nc with det Γ₁ Γ₂ nc + ... | M , m = M , m , cut h₁ h₂ M m + + -- For an arbitrary relation, soundness only refutes "no conflict": a + -- double negation, not a witness a checker could report. + detector-cannot-miss : {Conflicts : Ctx → Ctx → Set} → SoundDetector Conflicts + → (Γ Δ : Ctx) → ¬ Consistent (Γ ++ Δ) → ¬ ¬ Conflicts Γ Δ + detector-cannot-miss det Γ Δ inc noc = inc (det Γ Δ noc) + + -- A detector is a decision procedure. A sound one returns the conflict + -- witness itself for every inconsistent composition: the reportable flag. + detector-must-flag : {Conflicts : Ctx → Ctx → Set} → SoundDetector Conflicts + → ((Γ Δ : Ctx) → Dec (Conflicts Γ Δ)) + → (Γ Δ : Ctx) → ¬ Consistent (Γ ++ Δ) → Conflicts Γ Δ + detector-must-flag det decide Γ Δ inc with decide Γ Δ + ... | yes c = c + ... | no nc = ⊥-elim (inc (det Γ Δ nc)) + +------------------------------------------------------------------------ +-- A concrete logic: literals over a Boolean valuation +------------------------------------------------------------------------ + +module Literals where + + data Lit : Set where + pos neg : ℕ → Lit + + _⊨ₗ_ : (ℕ → Bool) → Lit → Set + v ⊨ₗ pos n = v n ≡ true + v ⊨ₗ neg n = v n ≡ false + + open Semantics Lit (ℕ → Bool) _⊨ₗ_ public + + true≢false : true ≡ false → ⊥ + true≢false () + + -- pos 0 and neg 0 have no common model … + clash : ¬ Consistent (pos 0 ∷ neg 0 ∷ []) + clash (v , (p ∷ (q ∷ []))) = true≢false (trans (sym p) q) + + -- … so their composition "proves" an unrelated goal. + clash-entails-anything : (pos 0 ∷ neg 0 ∷ []) ⊩ pos 1 + clash-entails-anything = explosion clash (pos 1) + + -- A genuine composition: from pos 0, and from pos 0 with pos 1, derive + -- pos 1; the composite's axioms are pos 0, pos 1 and it is realised. + lemma₁ : (pos 0 ∷ []) ⊩ pos 0 + lemma₁ M (p ∷ []) = p + + lemma₂ : (pos 0 ∷ pos 1 ∷ []) ⊩ pos 1 + lemma₂ M (_ ∷ (q ∷ [])) = q + + composed : (pos 0 ∷ pos 1 ∷ []) ⊩ pos 1 + composed = cut {Γ₁ = pos 0 ∷ []} {Γ₂ = pos 1 ∷ []} {φ = pos 0} {ψ = pos 1} lemma₁ lemma₂ diff --git a/meta-checker/src/Echidna/MetaChecker.agda b/meta-checker/src/Echidna/MetaChecker.agda index 2fff5bb5..b00b01f3 100644 --- a/meta-checker/src/Echidna/MetaChecker.agda +++ b/meta-checker/src/Echidna/MetaChecker.agda @@ -66,6 +66,17 @@ -- ✓ Fixed points 0/1 -> Level1, >=5 -> Level5 -- ✓ The clamp is idempotent -- +-- FROM Composition (E9, theory over an arbitrary logic): +-- ✓ Cut: composing certified proofs preserves semantic soundness +-- ✓ Weakening on either side preserves entailment +-- ✓ Inconsistent axioms entail everything (explosion), so soundness +-- preservation alone is vacuous without a conflict check +-- ✓ A sound conflict detector makes a composite realised +-- ✓ A sound detector that decides its conflict relation returns a +-- conflict witness for every inconsistent composition (for an +-- undecided relation, only a double negation) +-- No ECHIDNA Rust code composes proofs today; nothing here verifies one. +-- -- TOTAL: 45+ proven properties, 0 postulates, 0 sorry, 0 believe_me, -- 0 Admitted. -- @@ -96,6 +107,7 @@ open import Echidna.Receipt public open import Echidna.Integrity public open import Echidna.ClampTrust public open import Echidna.AxiomTrackerCompleteness public +open import Echidna.Composition public ------------------------------------------------------------------------ -- Summary: Key safety invariants proven diff --git a/proofs/agda/ProofComposition.agda b/proofs/agda/ProofComposition.agda index 2cf2feaf..6cac208f 100644 --- a/proofs/agda/ProofComposition.agda +++ b/proofs/agda/ProofComposition.agda @@ -1,10 +1,11 @@ -- SPDX-License-Identifier: MPL-2.0 --- ProofComposition.agda — axiom-set consistency for composed proofs. +-- ProofComposition.agda — corpus fixture (PROOF-POLICY §3): list algebra +-- over axiom lists. -- --- Simplified version: proves that combining two consistent axiom --- lists yields a consistent union if neither introduces the other's --- negation. Enough to exercise the agda backend without fighting --- stdlib namespace clashes. +-- What it proves: axiom-list concatenation is associative and has a left +-- identity. It does NOT prove consistency or soundness of composed proofs, +-- and it is not E9's evidence: that is meta-checker/src/Echidna/ +-- Composition.agda (cut soundness, explosion, sound conflict detectors). module ProofComposition where diff --git a/proofs/agda/SoundnessPreservation.agda b/proofs/agda/SoundnessPreservation.agda index 0cbc8ddb..d1749c26 100644 --- a/proofs/agda/SoundnessPreservation.agda +++ b/proofs/agda/SoundnessPreservation.agda @@ -1,14 +1,13 @@ -- SPDX-License-Identifier: MPL-2.0 --- SoundnessPreservation.agda — composed proofs are sound when axiom sets --- are conflict-free. +-- SoundnessPreservation.agda — corpus fixture (PROOF-POLICY §3): Bool-flag +-- composition. -- --- Models a Proof as a record carrying a list of axiom indices and a --- soundness flag. Proves that composing two individually-sound proofs --- whose axiom sets do not conflict yields a sound composite proof. --- --- "Conflict" is an abstract predicate so the proof is parametric: --- concrete conflict detectors (e.g. the axiom danger tracker in --- src/rust/verification/axioms.rs) can instantiate it at will. +-- What it proves: if two Bool "sound" flags are true, their conjunction is +-- true. `compose-sound` takes a Conflicts hypothesis but never uses it, so +-- it says nothing about conflicting axioms and is not evidence that +-- composition preserves soundness. E9's evidence is meta-checker/src/ +-- Echidna/Composition.agda, where soundness is semantic entailment and the +-- conflict check is shown to be load-bearing (`explosion`). module SoundnessPreservation where diff --git a/scripts/ci/check-agda.sh b/scripts/ci/check-agda.sh index beac224d..b12b9dfa 100644 --- a/scripts/ci/check-agda.sh +++ b/scripts/ci/check-agda.sh @@ -35,4 +35,15 @@ while IFS= read -r -d '' source; do done < <(find src -type f -name '*.agda' -print0) echo "$total source modules, $((total - missing)) with fresh interfaces" [[ "$total" -gt 0 && "$missing" -eq 0 ]] + +# Source-bound receipt (PROOF-POLICY §8): toolchain, flags and the SHA-256 of +# every first-party source and library descriptor this run checked. +echo "receipt: $version; commit ${GITHUB_SHA:-$(git -C "$repo_root" rev-parse HEAD)}" +echo "receipt: flags --safe --without-K --cubical-compatible; library file $AGDA_LIBRARIES_FILE" +while IFS= read -r lib; do + if [[ -n "$lib" ]]; then + echo "receipt: library $lib sha256 $(sha256sum "$lib" | cut -d" " -f1)" + fi +done < "$AGDA_LIBRARIES_FILE" +find src -type f -name "*.agda" -print0 | sort -z | xargs -0 sha256sum | sed "s/^/receipt: /" bash "$repo_root/scripts/ci/check-receipt-controls.sh"