From 20dc69186dcee3a3a8ceec672c01f2bf7eddd8f1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 12:54:18 +0000 Subject: [PATCH 1/5] fix(deps): move rmcp to 3.9.0 off three RustSec advisories cargo audit fails on rmcp 3.5.0 (crates/echidna-mcp) with RUSTSEC-2026-0457 (fixed >=3.7.0), RUSTSEC-2026-0461 (>=3.6.0) and RUSTSEC-2026-0462 (>=3.9.0), published after main last passed the Dependency audit check. `cargo update -p rmcp` moves rmcp and rmcp-macros to 3.9.0, inside the existing "3" requirement; no other entry changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- Cargo.lock | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0bf91e23..0592b0e7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -133,7 +133,7 @@ version = "1.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" dependencies = [ - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -144,7 +144,7 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" dependencies = [ "anstyle", "once_cell_polyfill", - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -640,7 +640,7 @@ version = "3.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -1246,7 +1246,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -2093,7 +2093,7 @@ version = "0.50.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7957b9740744892f114936ab4a57b3f487491bbeafaf8083688b16841a4240e5" dependencies = [ - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -2837,20 +2837,22 @@ dependencies = [ [[package]] name = "rmcp" -version = "3.5.0" +version = "3.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fae7019994ae0fe4ada40b732f798f3ff26f0f04facb1477f1bf37eb4f18a2d3" +checksum = "d24a7e92f4bcaa36b97fa93c4fa7ca8f3e669eced949345b3462dba333c7f909" dependencies = [ "base64 0.23.1", "chrono", "futures", "indexmap", + "libc", "pastey", "pin-project-lite", "rmcp-macros", "schemars", "serde", "serde_json", + "sha2 0.11.0", "thiserror", "tokio", "tokio-util", @@ -2860,9 +2862,9 @@ dependencies = [ [[package]] name = "rmcp-macros" -version = "3.5.0" +version = "3.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7e66877136e969d5a2d561ee5841b17717a0619aebd64abb47a2a2f46e34683" +checksum = "b3140f24a766f80f9ec1607bde85680959a69b83d46fa9ce87dadab7e67ab029" dependencies = [ "darling 0.24.0", "proc-macro2", @@ -2910,7 +2912,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -3251,7 +3253,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "52d1cfed4120b4d927bf7c0f86d2087a4a7d6027c906d9f9d525a80573b9be51" dependencies = [ "libc", - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -3391,10 +3393,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" dependencies = [ "fastrand", - "getrandom 0.4.2", + "getrandom 0.3.4", "once_cell", "rustix", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -4198,7 +4200,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] From 17ebbb1f64bb5985130c9a86749dd61f6f398ffe Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 12:56:24 +0000 Subject: [PATCH 2/5] style: rustfmt src/rust/proof_search.rs `cargo fmt --check` fails on main (2ab7574) in five places in src/rust/proof_search.rs, so rust-ci 'Cargo check + clippy + fmt' is red on every PR. Formatting only; no code change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- src/rust/proof_search.rs | 25 +++++++++++-------------- 1 file changed, 11 insertions(+), 14 deletions(-) diff --git a/src/rust/proof_search.rs b/src/rust/proof_search.rs index 3c90d3bf..949b63c9 100644 --- a/src/rust/proof_search.rs +++ b/src/rust/proof_search.rs @@ -384,7 +384,8 @@ mod chapel_ffi { let start = start.clone(); std::thread::spawn(move || { start.wait(); - let strategy = ChapelParallelSearch::new().expect("real Chapel runtime"); + let strategy = + ChapelParallelSearch::new().expect("real Chapel runtime"); assert_eq!(ChapelParallelSearch::available_prover_count(), 0); for _ in 0..2 { assert!(strategy.available()); @@ -414,10 +415,8 @@ mod chapel_ffi { // No global environment mutation races with other Rust tests, and // no external prover can be dispatched by this allocation/free probe. let empty_path = tempfile::tempdir().expect("empty prover search directory"); - let mut command = real_probe_command( - "real_search_without_provers_fails_and_frees_result", - CHILD, - ); + let mut command = + real_probe_command("real_search_without_provers_fails_and_frees_result", CHILD); command.env("PATH", empty_path.path()); run_real_probe( &mut command, @@ -478,7 +477,10 @@ mod chapel_ffi { matches!(stopped_before_cleanup, Ok(true)), "deadline returned with a live or unobservable prover: {stopped_before_cleanup:?}" ); - assert!(elapsed < Duration::from_secs(3), "deadline took {elapsed:?}"); + assert!( + elapsed < Duration::from_secs(3), + "deadline took {elapsed:?}" + ); let result = result.expect("native timeout returns a failed search result"); assert!(!result.success); assert_eq!( @@ -500,17 +502,12 @@ mod chapel_ffi { .expect("write finite prover"); std::fs::set_permissions(&prover, std::fs::Permissions::from_mode(0o700)) .expect("make finite prover executable"); - let mut command = real_probe_command( - "real_search_deadline_stops_the_owned_prover", - CHILD, - ); + let mut command = + real_probe_command("real_search_deadline_stops_the_owned_prover", CHILD); command .env("PATH", fixture.path()) .env(PID_FILE, fixture.path().join("prover.pid")); - run_real_probe( - &mut command, - "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED", - ); + run_real_probe(&mut command, "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED"); } } } From f48fe0aaf82f9fc560f3d0aebec5aeb018da33e3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 12:58:57 +0000 Subject: [PATCH 3/5] fix(ffi): annotate the audited Zig context-pointer casts for Hypatia Hypatia's code_safety/zig_ptr_cast and zig_align_cast now flag the nine `@ptrCast(@alignCast(raw))` lines in src/zig_ffi/chapel_bridge.zig and src/zig_ffi/runtime_owner.zig as high, and the governance Hypatia baseline gate is red on main (2ab7574) as a result. Each of those lines recovers a callback's own `*@This()` from the type-erased `*anyopaque` it was registered with (runtime_owner.Work .context, or a std.mem.Allocator vtable's ptr), so the cast restores the original type and alignment. Fixed at source with a reasoned inline `hypatia: allow` per rule on each line, as the scanner documents, rather than a baseline entry. No code change: comments only. Checked by simulating ScannerSuppression.inline_allowed?/4 and directive_re at hypatia 82396d81 (the CI pin): 18 unsuppressed findings on main, 0 with this change. The scanner itself could not be built here (hex.pm is unreachable). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- src/zig_ffi/chapel_bridge.zig | 15 ++++++++++----- src/zig_ffi/runtime_owner.zig | 12 ++++++++---- 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/zig_ffi/chapel_bridge.zig b/src/zig_ffi/chapel_bridge.zig index 807c23fe..f8d12591 100644 --- a/src/zig_ffi/chapel_bridge.zig +++ b/src/zig_ffi/chapel_bridge.zig @@ -70,7 +70,8 @@ fn callOnOwner(owner: anytype, comptime function: anytype, args: anytype, result result: @TypeOf(result), fn run(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.result.* = @call(.auto, function, self.arguments); } }; @@ -650,7 +651,8 @@ const CallerAllocator = struct { } fn alloc(raw: *anyopaque, len: usize, alignment: std.mem.Alignment, ret_addr: usize) ?[*]u8 { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds if (!self.record() or self.allocations >= self.fail_after) return null; const pointer = std.heap.c_allocator.rawAlloc(len, alignment, ret_addr) orelse return null; self.allocations += 1; @@ -659,7 +661,8 @@ const CallerAllocator = struct { } fn resize(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) bool { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); _ = memory; _ = alignment; @@ -669,7 +672,8 @@ const CallerAllocator = struct { } fn remap(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) ?[*]u8 { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); _ = memory; _ = alignment; @@ -679,7 +683,8 @@ const CallerAllocator = struct { } fn free(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, ret_addr: usize) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); // The backing allocator is cross-thread safe so a failed assertion // never requires corrupting memory or leaking the test allocation. diff --git a/src/zig_ffi/runtime_owner.zig b/src/zig_ffi/runtime_owner.zig index 79d9d543..da2f1b8a 100644 --- a/src/zig_ffi/runtime_owner.zig +++ b/src/zig_ffi/runtime_owner.zig @@ -169,7 +169,8 @@ const Probe = struct { } fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.wrong_thread = self.wrong_thread or self.init_id != std.Thread.getCurrentId(); self.calls += 1; } @@ -239,7 +240,8 @@ test "shutdown drains accepted work and refuses new work before joining" { shutdown_failed: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.mutex.lock(); self.entered = true; self.changed.broadcast(); @@ -311,7 +313,8 @@ test "owner callbacks cannot re-enter or finalize themselves" { stop_refused: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds var nested = Work{ .context = self.probe, .run = Probe.work }; self.call_refused = if (self.owner.call(&nested)) |_| false else |err| err == error.ReentrantCall; self.stop_refused = if (self.owner.shutdown()) |_| false else |err| err == error.ReentrantCall; @@ -358,7 +361,8 @@ test "a nonowner process-exit request refuses active work without a join cycle" exit_refused: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.mutex.lock(); self.entered = true; self.changed.broadcast(); From fa92ee01f9e2c1586a7836fd7662dc800187f037 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:22:54 +0000 Subject: [PATCH 4/5] proof(agda): real E9 composition soundness in the gated meta-checker; relabel the two corpus files MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The proof audit found E9 ("proof composition soundness") evidenced by two corpus files that do not prove it: ProofComposition.agda proves list-append associativity, and SoundnessPreservation.agda's compose-sound discharges a Bool flag with `∧` while ignoring its Conflicts hypothesis. PROOF-STATUS R6 called that evidence "good, merely misfiled". New meta-checker/src/Echidna/Composition.agda, theory over an arbitrary logic (formulae, models and satisfaction are module parameters, not postulates): cut (composition preserves semantic soundness, using both premises), weakening, explosion (inconsistent axioms entail everything, so soundness preservation is vacuous without a conflict check), compose-realised (a sound conflict detector makes every composite realised), detector-must-flag, and a concrete literal logic where pos 0 and neg 0 clash and entail an unrelated goal. It is imported by MetaChecker.agda, so agda-meta-checker (pinned Agda 2.7.0.1, canonical flags) gates it. No Rust code composes proofs; none is claimed. PROOF-NEEDS E9 now cites the new module; PROOF-STATUS R6 is corrected. The two corpus files keep their place as §3 fixtures with headers that say what they actually prove. Checked locally with agda --safe --without-K --cubical-compatible on Agda 2.6.3 + stdlib 1.7.3: Composition and the full MetaChecker closure exit 0. The pinned 2.7.0.1 run is CI's. Mutation check: replacing SoundDetector with a trivial property makes compose-realised fail. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- docs/PROOF-NEEDS.adoc | 7 +- docs/PROOF-STATUS.adoc | 27 ++-- meta-checker/src/Echidna/Composition.agda | 173 ++++++++++++++++++++++ meta-checker/src/Echidna/MetaChecker.agda | 10 ++ proofs/agda/ProofComposition.agda | 11 +- proofs/agda/SoundnessPreservation.agda | 17 +-- 6 files changed, 216 insertions(+), 29 deletions(-) create mode 100644 meta-checker/src/Echidna/Composition.agda diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index 9aa00127..8f101f99 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -78,8 +78,11 @@ 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 must flag +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..7bd14462 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -265,19 +265,20 @@ 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. +|`+proven+` (Agda leg, pending the first CI receipt of this module) +|`+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+`. 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. |=== diff --git a/meta-checker/src/Echidna/Composition.agda b/meta-checker/src/Echidna/Composition.agda new file mode 100644 index 00000000..c0322c91 --- /dev/null +++ b/meta-checker/src/Echidna/Composition.agda @@ -0,0 +1,173 @@ +-- 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-must-flag any sound detector must report a conflict 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 (¬_) +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 + + -- A sound detector cannot miss an inconsistent composition. + detector-must-flag : {Conflicts : Ctx → Ctx → Set} → SoundDetector Conflicts + → (Γ Δ : Ctx) → ¬ Consistent (Γ ++ Δ) → ¬ ¬ Conflicts Γ Δ + detector-must-flag det Γ Δ inc noc = inc (det Γ Δ noc) + +------------------------------------------------------------------------ +-- 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..4aa5079b 100644 --- a/meta-checker/src/Echidna/MetaChecker.agda +++ b/meta-checker/src/Echidna/MetaChecker.agda @@ -66,6 +66,15 @@ -- ✓ 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 must flag every inconsistent composition +-- 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 +105,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 From 3bb0b8c1b52919a8279a3054efd5b9c108295e12 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:16:59 +0000 Subject: [PATCH 5/5] fix(proofs): decidable detector-must-flag; receipt-honest R4/R6 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review on #471 (Codex): - Composition.agda: for an arbitrary Set-valued Conflicts relation the old detector-must-flag gave only ¬¬ Conflicts, not a reportable witness. It is renamed detector-cannot-miss and kept, and a new detector-must-flag takes a decision procedure (Dec) and returns the Conflicts witness itself. MetaChecker, PROOF-NEEDS E9 and R6 say so. - scripts/ci/check-agda.sh: the agda-meta-checker job now prints a source-bound receipt (toolchain, flags, library descriptors, SHA-256 of every source), so a CI run can stand as the receipt PROOF-POLICY §8 needs. - PROOF-STATUS R6: argued, not proven, until that job's receipt on main exists. The local check used Agda 2.6.3, not the pin. - PROOF-STATUS R4: records that MetaChecker.agda now imports Composition (ten modules). The nine receipted modules are unchanged, so the row stands for them; the new entrypoint digest awaits the same CI receipt. - The "Not obligations" note no longer describes R6 as a corpus placement defect; R6 cites the meta-checker module and the corpus files disclaim E9. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- docs/PROOF-NEEDS.adoc | 3 ++- docs/PROOF-STATUS.adoc | 23 +++++++++++++++----- meta-checker/src/Echidna/Composition.agda | 26 +++++++++++++++++------ meta-checker/src/Echidna/MetaChecker.agda | 4 +++- scripts/ci/check-agda.sh | 11 ++++++++++ 5 files changed, 54 insertions(+), 13 deletions(-) diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index 8f101f99..d36f2149 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -80,7 +80,8 @@ no collisions in kind_to_u8 |I2 |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 must flag +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 diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 7bd14462..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,7 +272,8 @@ 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" -|`+proven+` (Agda leg, pending the first CI receipt of this module) +|`+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). @@ -275,7 +283,12 @@ 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+`. No +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. @@ -316,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 index c0322c91..1cf6c2e6 100644 --- a/meta-checker/src/Echidna/Composition.agda +++ b/meta-checker/src/Echidna/Composition.agda @@ -21,8 +21,12 @@ -- 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-must-flag any sound detector must report a conflict whenever --- the joined axioms are inconsistent; +-- 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. -- @@ -43,7 +47,7 @@ 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 (¬_) +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). @@ -130,10 +134,20 @@ module Semantics (Form Model : Set) (_⊨_ : Model → Form → Set) where compose-realised det {Γ₁} {Γ₂} h₁ h₂ nc with det Γ₁ Γ₂ nc ... | M , m = M , m , cut h₁ h₂ M m - -- A sound detector cannot miss an inconsistent composition. + -- 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) → ¬ Consistent (Γ ++ Δ) → ¬ ¬ Conflicts Γ Δ - detector-must-flag det Γ Δ inc noc = inc (det Γ Δ noc) + → ((Γ Δ : 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 diff --git a/meta-checker/src/Echidna/MetaChecker.agda b/meta-checker/src/Echidna/MetaChecker.agda index 4aa5079b..b00b01f3 100644 --- a/meta-checker/src/Echidna/MetaChecker.agda +++ b/meta-checker/src/Echidna/MetaChecker.agda @@ -72,7 +72,9 @@ -- ✓ 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 must flag every inconsistent composition +-- ✓ 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, 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"