From 20dc69186dcee3a3a8ceec672c01f2bf7eddd8f1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 12:54:18 +0000 Subject: [PATCH 1/9] 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/9] 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/9] 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 2df3d178d7abb6e74ec156b67ce33903207e5db2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:59:41 +0000 Subject: [PATCH 4/9] fix(trust): one trust kernel; Level 4 needs a certificate, Level 5 two small kernels MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 2026-11-09 proof audit found two defects in compute_trust_level. Both were present identically in src/rust/verification/confidence.rs and in its copy in crates/echidna-core-creusot, and no proof caught either. - Level 4 fired on certificate_verified without has_certificate. - Level 5 checked only the producing prover's kernel class, never the confirmers'. One small-kernel prover plus an SMT confirmer scored Level 5. Fixed at the source: the kernel crate (echidna_core::trust). - Level 3 and above count a certificate only when it was produced and verified. - Level 5 needs two or more small-kernel confirmations. They are given by a new TrustFactors input, small_kernel_confirmations: how many of the confirming provers are small-kernel systems with a verified certificate, the producing prover included. Read at most confirming_provers; #[serde(default)] = 0. One kernel, not two: confidence.rs re-exports the kernel's TrustLevel and delegates compute_trust_level to it. It keeps its ProverKind-shaped TrustFactors and maps the prover to a kernel class with is_small_kernel_prover. Contracts stated on the kernel, as Creusot ensures: - TK-4: Level 4 and above imply a small kernel, has_certificate and certificate_verified. - TK-5: Level 5 implies small_kernel_confirmations >= 2 and confirming_provers >= 2. They are not yet discharged by Creusot. Stable-Rust tests check them over every input with counts 0..=4 (tk4, tk5, and tk6 for monotonicity in the evidence), plus regressions for both defects. With the old logic put back in place, three of these tests fail. This departs from the ruling's wording ("every confirming prover is small kernel"). Level 5 instead counts small-kernel confirmations, at least two. Requiring every confirmer to be a small kernel would let one extra SMT agreement lower a result from Level 5 to Level 4, breaking monotonicity. The count also matches the Level 5 definition already in the code: "cross-checked by 2+ independent small-kernel systems". The shipped dispatch paths pass 0 for the new input. They already reported no certificate, so their results do not change. Every other TrustFactors literal gains the field with 0. The confidence.rs Level 5 test now states two small-kernel confirmations, and three tests are new: one small-kernel confirmation is Level 4, a verified flag without a certificate is Level 2, and the kernel's small-kernel class follows is_small_kernel_prover. Retired: verification/proofs/idris2/TrustKernelMonotonicity.idr. It dropped has_certificate and proved the defective Level 5 rule as a property. Under PROOF-POLICY §1, Rust behaviour is verified on the code. PROOF-STATUS R1 records TK-4/TK-5 as tested-only. Creusot is not discharged and Verus is not yet applied, both with their scope. R1 stays open. PROOF-NEEDS marks the Idris row retired. CHANGELOG notes the behaviour change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- CHANGELOG.adoc | 21 ++ benches/proof_benchmarks.rs | 3 + benches/routing_benchmarks.rs | 3 + crates/echidna-core-creusot/src/lib.rs | 210 ++++++++++++- docs/PROOF-NEEDS.adoc | 11 +- docs/PROOF-STATUS.adoc | 17 ++ src/rust/dispatch.rs | 3 + src/rust/verification/confidence.rs | 171 ++++++----- tests/aspect_tests.rs | 2 + tests/concurrency_test.rs | 1 + tests/e2e_prover_test.rs | 6 + tests/neural_property_tests.rs | 3 + tests/p2p_property_tests.rs | 3 + tests/panic_attack_props.rs | 1 + tests/property_tests.rs | 5 + tests/security_aspect_tests.rs | 4 + .../proofs/idris2/TrustKernelMonotonicity.idr | 286 ------------------ .../proofs/idris2/echidna-verif-proofs.ipkg | 1 - 18 files changed, 366 insertions(+), 385 deletions(-) delete mode 100644 verification/proofs/idris2/TrustKernelMonotonicity.idr diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 465dfc81..4c26a3ba 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,27 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Fixed — one trust kernel; Level 4 and Level 5 conditions, 2026-11-09 + +* `+compute_trust_level+` now exists once, in `+echidna-core-creusot+` +(`+echidna_core::trust+`). `+verification::confidence+` re-exports its +`+TrustLevel+` and delegates to it instead of keeping a second copy. +* *Level 4* now needs a produced certificate (`+has_certificate+`) as well +as a verified one. A result with `+certificate_verified+` but no certificate +used to score Level 4. +* *Level 5* now needs two or more small-kernel systems that checked a +certificate. It used to check only the producing prover's kernel class, so +one small-kernel prover plus an SMT confirmer scored Level 5. +* `+TrustFactors+` gains `+small_kernel_confirmations+`, the number of +confirming provers that are small-kernel systems with a verified certificate, +the producing prover included. It defaults to 0 (`+#[serde(default)]+`), so +callers that cannot vouch for their confirmers never reach Level 5. The +shipped dispatch paths set it to 0, as they already reported no certificate. +* Contracts TK-4/TK-5 are stated on the kernel and checked exhaustively over +a finite input space by the crate's tests (`+tested-only+`; the Creusot run +is still open). The Idris 2 `+TrustKernelMonotonicity+` model, which proved +the old Level 5 rule, is retired. + ==== Changed — GraphQL listener default, 2026-11-04 * `+echidna-graphql+` now defaults to `+127.0.0.1:8082+`, avoiding the diff --git a/benches/proof_benchmarks.rs b/benches/proof_benchmarks.rs index 38e35aa1..d58ba8ce 100644 --- a/benches/proof_benchmarks.rs +++ b/benches/proof_benchmarks.rs @@ -149,6 +149,7 @@ fn bench_trust_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Lean, confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -161,6 +162,7 @@ fn bench_trust_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -173,6 +175,7 @@ fn bench_trust_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Lean, confirming_provers: 2, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, diff --git a/benches/routing_benchmarks.rs b/benches/routing_benchmarks.rs index b7ada9d6..66cecba8 100644 --- a/benches/routing_benchmarks.rs +++ b/benches/routing_benchmarks.rs @@ -125,6 +125,7 @@ fn bench_trust_level_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -137,6 +138,7 @@ fn bench_trust_level_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Lean, confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -149,6 +151,7 @@ fn bench_trust_level_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Z3, confirming_provers: 5, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, diff --git a/crates/echidna-core-creusot/src/lib.rs b/crates/echidna-core-creusot/src/lib.rs index d9560c6b..bab6d51b 100644 --- a/crates/echidna-core-creusot/src/lib.rs +++ b/crates/echidna-core-creusot/src/lib.rs @@ -211,6 +211,14 @@ pub struct TrustFactors { pub prover_class: ProverClass, /// Number of independent provers that agree on this result. pub confirming_provers: u32, + /// How many of the `confirming_provers` are small-kernel systems whose + /// certificate for this result was independently verified, the producing + /// prover included. Level 5 needs at least two. `confirming_provers` + /// alone cannot decide that, because it does not say what kind of system + /// each confirmer is. Defaults to 0, so data written before this field + /// existed can never reach Level 5. + #[serde(default)] + pub small_kernel_confirmations: u32, /// Whether a proof certificate was produced. pub has_certificate: bool, /// Whether the certificate was independently verified. @@ -295,23 +303,44 @@ pub fn clamp_trust(level: TrustLevel, min_level: TrustLevel, max_level: TrustLev /// ### Creusot contracts /// ```text /// #[requires(true)] -/// #[ensures( -/// factors.worst_axiom_danger == DangerLevel::Reject -/// ==> result == TrustLevel::Level1 -/// )] -/// #[ensures( -/// !factors.solver_integrity_ok -/// ==> result == TrustLevel::Level1 -/// )] -/// #[ensures(result >= TrustLevel::Level1)] -/// #[ensures(result <= TrustLevel::Level5)] +/// #[ensures(factors.worst_axiom_danger == DangerLevel::Reject ==> result == TrustLevel::Level1)] +/// #[ensures(factors.worst_axiom_danger == DangerLevel::Warning ==> result == TrustLevel::Level1)] +/// #[ensures(!factors.solver_integrity_ok ==> result == TrustLevel::Level1)] +/// // TK-4: Level 4 and above need a small kernel AND a produced, verified certificate. +/// #[ensures(result >= TrustLevel::Level4 ==> +/// factors.prover_class == ProverClass::SmallKernel +/// && factors.has_certificate && factors.certificate_verified)] +/// // TK-5: Level 5 needs two or more small-kernel systems that checked a certificate. +/// #[ensures(result == TrustLevel::Level5 ==> +/// factors.small_kernel_confirmations >= 2 && factors.confirming_provers >= 2)] +/// #[ensures(result >= TrustLevel::Level1 && result <= TrustLevel::Level5)] /// ``` +/// +/// TK-4 and TK-5 close two defects in the earlier rule. Level 4 used to fire +/// on `certificate_verified` without `has_certificate`. Level 5 used to check +/// only the producing prover's kernel class, never the confirmers'. Both +/// are checked exhaustively over a finite input space by +/// `impl_invariants::tk_*`, which run on stable Rust in CI. The Creusot +/// annotations are stated, not yet discharged (see the crate header). #[cfg_attr(feature = "creusot", ensures( factors.worst_axiom_danger == DangerLevel::Reject ==> result == TrustLevel::Level1 ), + ensures( + factors.worst_axiom_danger == DangerLevel::Warning + ==> result == TrustLevel::Level1 + ), ensures(!factors.solver_integrity_ok ==> result == TrustLevel::Level1), + ensures( + result >= TrustLevel::Level4 + ==> (factors.prover_class == ProverClass::SmallKernel + && factors.has_certificate && factors.certificate_verified) + ), + ensures( + result == TrustLevel::Level5 + ==> (factors.small_kernel_confirmations >= 2u32 && factors.confirming_provers >= 2u32) + ), ensures(result >= TrustLevel::Level1 && result <= TrustLevel::Level5) )] pub fn compute_trust_level(factors: &TrustFactors) -> TrustLevel { @@ -339,19 +368,30 @@ pub fn compute_trust_level(factors: &TrustFactors) -> TrustLevel { } let is_small_kernel = factors.prover_class == ProverClass::SmallKernel; + // A certificate counts only when one was produced AND it was verified; + // a verification flag on a result with no certificate carries nothing. + let certified = factors.has_certificate && factors.certificate_verified; + // Small-kernel confirmations can never exceed the confirming provers; + // an inconsistent input is read at the lower count. + let small_kernel_confirmations = + if factors.small_kernel_confirmations < factors.confirming_provers { + factors.small_kernel_confirmations + } else { + factors.confirming_provers + }; - // --- Level 5: two or more small-kernel systems cross-check with certs --- - if factors.confirming_provers >= 2 && factors.certificate_verified && is_small_kernel { + // --- Level 5: two or more small-kernel systems checked a certificate --- + if certified && is_small_kernel && small_kernel_confirmations >= 2 { return TrustLevel::Level5; } - // --- Level 4: single small-kernel system with verified certificate --- - if is_small_kernel && factors.certificate_verified { + // --- Level 4: small-kernel system with a produced, verified certificate --- + if certified && is_small_kernel { return TrustLevel::Level4; } - // --- Level 3: any prover with verified certificate --- - if factors.has_certificate && factors.certificate_verified { + // --- Level 3: any prover with a produced, verified certificate --- + if certified { return TrustLevel::Level3; } @@ -494,6 +534,7 @@ pub mod impl_invariants { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 10, // maximum cross-checking + small_kernel_confirmations: 10, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, @@ -517,6 +558,7 @@ pub mod impl_invariants { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 5, + small_kernel_confirmations: 5, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -579,6 +621,136 @@ pub mod impl_invariants { assert!(TrustLevel::Level4.value() < TrustLevel::Level5.value()); } + // ----------------------------------------------------------------------- + // TK-4 / TK-5: the certificate and kernel conditions of Levels 4 and 5, + // checked over every input in a finite space (bounded model check). + // ----------------------------------------------------------------------- + + /// Every `TrustFactors` with counts in `0..=4`, both certificate flags, + /// every danger level, both integrity states and every prover class. + #[cfg(test)] + fn all_factors() -> Vec { + use crate::axiom_tracker::DangerLevel::{Noted, Reject, Safe, Warning}; + let mut out = Vec::new(); + for pc in [ + ProverClass::SmallKernel, + ProverClass::SmtOrAtp, + ProverClass::Other, + ] { + for confirming_provers in 0u32..=4 { + for small_kernel_confirmations in 0u32..=4 { + for has_certificate in [false, true] { + for certificate_verified in [false, true] { + for worst_axiom_danger in [Safe, Noted, Warning, Reject] { + for solver_integrity_ok in [false, true] { + out.push(TrustFactors { + prover_class: pc, + confirming_provers, + small_kernel_confirmations, + has_certificate, + certificate_verified, + worst_axiom_danger, + solver_integrity_ok, + }); + } + } + } + } + } + } + } + out + } + + /// **TK-4** Level 4 and above need a small-kernel prover with a + /// certificate that was both produced and verified. + #[test] + fn tk4_level4_needs_small_kernel_and_produced_verified_certificate() { + for f in all_factors() { + if compute_trust_level(&f) >= TrustLevel::Level4 { + assert!( + f.prover_class == ProverClass::SmallKernel + && f.has_certificate + && f.certificate_verified, + "TK-4 violated by {f:?}" + ); + } + } + } + + /// **TK-5** Level 5 needs two or more small-kernel systems that checked a + /// certificate, and two or more confirming provers. + #[test] + fn tk5_level5_needs_two_small_kernel_confirmations() { + for f in all_factors() { + if compute_trust_level(&f) == TrustLevel::Level5 { + assert!( + f.small_kernel_confirmations >= 2 && f.confirming_provers >= 2, + "TK-5 violated by {f:?}" + ); + } + } + } + + /// **TK-6** Monotone in the evidence: one more confirming prover, one more + /// small-kernel confirmation, or a produced and verified certificate + /// never lowers the level. + #[test] + fn tk6_more_evidence_never_lowers_trust() { + for f in all_factors() { + let base = compute_trust_level(&f); + let more_provers = TrustFactors { + confirming_provers: f.confirming_provers + 1, + ..f.clone() + }; + let more_kernels = TrustFactors { + confirming_provers: f.confirming_provers + 1, + small_kernel_confirmations: f.small_kernel_confirmations + 1, + ..f.clone() + }; + let certified = TrustFactors { + has_certificate: true, + certificate_verified: true, + ..f.clone() + }; + for g in [more_provers, more_kernels, certified] { + assert!( + compute_trust_level(&g) >= base, + "TK-6: {g:?} scored below {f:?}" + ); + } + } + } + + /// Regression: the two defects found in the 2026-11-09 proof audit. + #[test] + fn tk_regressions_for_the_audited_defects() { + use crate::axiom_tracker::DangerLevel::Safe; + // Level 5 from one small-kernel prover plus an SMT confirmer: the old + // rule saw only the producing prover's class and returned Level5. + let one_kernel = TrustFactors { + prover_class: ProverClass::SmallKernel, + confirming_provers: 2, + small_kernel_confirmations: 1, + has_certificate: true, + certificate_verified: true, + worst_axiom_danger: Safe, + solver_integrity_ok: true, + }; + assert_eq!(compute_trust_level(&one_kernel), TrustLevel::Level4); + // Level 4 without a produced certificate: the old rule returned Level4. + let no_certificate = TrustFactors { + prover_class: ProverClass::SmallKernel, + confirming_provers: 1, + small_kernel_confirmations: 1, + has_certificate: false, + certificate_verified: true, + worst_axiom_danger: Safe, + solver_integrity_ok: true, + }; + assert_eq!(compute_trust_level(&no_certificate), TrustLevel::Level2); + } + // ----------------------------------------------------------------------- // Property: compute_trust_level output is always in [Level1, Level5] // ----------------------------------------------------------------------- @@ -604,6 +776,7 @@ pub mod impl_invariants { let f = TrustFactors { prover_class: pc, confirming_provers: confirming, + small_kernel_confirmations: confirming, has_certificate: certs, certificate_verified: certs, worst_axiom_danger: dl, @@ -632,6 +805,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 2, + small_kernel_confirmations: 2, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -645,6 +819,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -658,6 +833,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmtOrAtp, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -671,6 +847,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmtOrAtp, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -685,6 +862,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Noted, diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index 9aa00127..e39973e9 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -92,10 +92,13 @@ injection-free, L3 type-safe boundary |I2 |Extensive ABI |`+src/abi/EchidnaABI/Types.idr+`, `+Foreign.idr+`, `+Layout.idr+` |All ABI types, no believe_me |I2 -|Stage 8a Trust-Kernel Monotonicity -|`+verification/proofs/idris2/TrustKernelMonotonicity.idr+` -|Reject/Warning danger → Level1; bad integrity → Level1; confirming≥2 + -cert + small_kernel → ≥Level4; zero believe_me |I2 +|Stage 8a Trust-Kernel Monotonicity (*retired 2026-11-09*) +|was `+verification/proofs/idris2/TrustKernelMonotonicity.idr+` +|Retired. The model dropped `+has_certificate+` and proved the defective +Level5 rule (the producing prover's kernel class only) as a property. Under +`+PROOF-POLICY+` §1 Rust behaviour is verified on the code, not restated in +Idris 2: the obligations now live as TK-4/TK-5 contracts on +`+echidna_core::trust::compute_trust_level+` (see PROOF-STATUS R1) |— |Stage 8a Axiom-Policy Ordering |`+verification/proofs/idris2/AxiomPolicyOrdering.idr+` |worstDanger diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index bcf6c700..fc7062f4 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -102,6 +102,23 @@ yet proved)`"; the `+creusot+` dev-dependency is commented out and the crate builds on stable Rust behind a `+creusot+` feature. Annotation is not proof. Row stays `+open+` until a Creusot run yields a receipt with a commit hash. +*Trust kernel (2026-11-09).* `+compute_trust_level+` exists once, in +`+crates/echidna-core-creusot+`; `+src/rust/verification/confidence.rs+` +re-exports its `+TrustLevel+` and delegates to it. Two defects found by the +2026-11-09 proof audit are fixed at that source: Level 4 fired on +`+certificate_verified+` without `+has_certificate+`, and Level 5 checked only +the producing prover's kernel class. The new contracts are TK-4 (Level 4 and +above need a small kernel and a produced, verified certificate) and TK-5 +(Level 5 needs two or more small-kernel confirmations, the new +`+small_kernel_confirmations+` input). They are `+tested-only+`: +`+impl_invariants::tk4_*+`, `+tk5_*+` and `+tk6_*+` (monotone in the +evidence) check every input with counts 0..=4. That covers every case only +because the rule reads counts through `+>= 2+` and a minimum, which is +argued, not mechanised. The Creusot annotations are stated, not discharged. +Verus (§1.2) has not been applied yet; its scope is the same TK obligations +on the same function. The Idris 2 `+TrustKernelMonotonicity+` model, which +proved the defective Level 5 rule, is retired. + |=== === Idris 2 — APIs, ABIs, engineering properties (§1) diff --git a/src/rust/dispatch.rs b/src/rust/dispatch.rs index e04894cd..49229511 100644 --- a/src/rust/dispatch.rs +++ b/src/rust/dispatch.rs @@ -664,6 +664,7 @@ impl ProverDispatcher { let trust_factors = TrustFactors { prover: prover_kind, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: worst_danger, @@ -872,6 +873,7 @@ impl ProverDispatcher { let trust_factors = TrustFactors { prover: primary_prover, confirming_provers: confirming_count, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: worst_danger, @@ -1022,6 +1024,7 @@ impl ProverDispatcher { let trust_factors = TrustFactors { prover: winning_kind, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: worst_danger, diff --git a/src/rust/verification/confidence.rs b/src/rust/verification/confidence.rs index 60c3d80f..895399be 100644 --- a/src/rust/verification/confidence.rs +++ b/src/rust/verification/confidence.rs @@ -15,44 +15,13 @@ use super::axiom_tracker::DangerLevel; use super::portfolio::PortfolioConfidence; use crate::provers::ProverKind; -/// Trust level for a proof result (5-level hierarchy) -#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] -pub enum TrustLevel { - /// Large-TCB system, unchecked result, or uses dangerous axioms - Level1 = 1, - /// Single prover result without certificate, but no dangerous axioms - Level2 = 2, - /// Single prover with proof certificate (Alethe, DRAT/LRAT) - Level3 = 3, - /// Checked by small-kernel system (Lean4, Coq, Isabelle) with proof certificate - Level4 = 4, - /// Cross-checked by 2+ independent small-kernel systems with certificates - Level5 = 5, -} - -impl TrustLevel { - /// Human-readable description - pub fn description(&self) -> &str { - match self { - TrustLevel::Level1 => "Minimal trust: large-TCB, unchecked, or dangerous axioms", - TrustLevel::Level2 => "Basic trust: single prover, no dangerous axioms", - TrustLevel::Level3 => "Moderate trust: single prover with proof certificate", - TrustLevel::Level4 => "High trust: small-kernel prover with certificate", - TrustLevel::Level5 => "Maximum trust: cross-checked by 2+ small-kernel systems", - } - } - - /// Numeric value (1-5) - pub fn value(&self) -> u8 { - *self as u8 - } -} - -impl std::fmt::Display for TrustLevel { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "Level {} ({})", self.value(), self.description()) - } -} +/// Trust level for a proof result (5-level hierarchy). +/// +/// There is one trust kernel: this type and [`compute_trust_level`] come +/// from `echidna-core` (`echidna_core::trust`, the Creusot-annotated crate). +/// This module keeps the `ProverKind`-shaped [`TrustFactors`] that dispatch +/// builds, and maps them onto the kernel's input. +pub use echidna_core::trust::TrustLevel; /// Input factors for computing trust level #[derive(Debug, Clone, Serialize, Deserialize)] @@ -61,6 +30,13 @@ pub struct TrustFactors { pub prover: ProverKind, /// Number of independent provers that agree pub confirming_provers: u32, + /// How many of the `confirming_provers` are small-kernel systems whose + /// certificate for this result was independently verified, the producing + /// prover included. Level 5 needs at least two. Defaults to 0, so a + /// caller that cannot vouch for its confirmers' kernels never reaches + /// Level 5. + #[serde(default)] + pub small_kernel_confirmations: u32, /// Whether a proof certificate was produced pub has_certificate: bool, /// Whether the certificate was independently verified @@ -73,47 +49,36 @@ pub struct TrustFactors { pub portfolio_confidence: Option, } -/// Compute the trust level for a proof result +/// Compute the trust level for a proof result. +/// +/// Delegates to the single kernel, `echidna_core::trust::compute_trust_level`, +/// after mapping the prover to its kernel class and the axiom danger level +/// to the kernel's enum. The kernel's contracts (TK-4: Level 4 and above +/// need a small kernel and a produced, verified certificate; TK-5: Level 5 +/// needs two or more small-kernel confirmations) hold here because there is +/// no second implementation to drift from. pub fn compute_trust_level(factors: &TrustFactors) -> TrustLevel { - // Reject-level axioms always result in Level 1 - if factors.worst_axiom_danger == DangerLevel::Reject { - return TrustLevel::Level1; - } - - // Warning-level axioms cap at Level 1 - if factors.worst_axiom_danger == DangerLevel::Warning { - return TrustLevel::Level1; - } - - // Failed integrity check caps at Level 1 - if !factors.solver_integrity_ok { - return TrustLevel::Level1; - } - - let is_small_kernel = is_small_kernel_prover(factors.prover); - - // Level 5: Cross-checked by 2+ small-kernel systems with certificates - if factors.confirming_provers >= 2 && factors.certificate_verified && is_small_kernel { - return TrustLevel::Level5; - } - - // Level 4: Small-kernel prover with verified certificate - if is_small_kernel && factors.certificate_verified { - return TrustLevel::Level4; - } - - // Level 3: Any prover with verified certificate - if factors.has_certificate && factors.certificate_verified { - return TrustLevel::Level3; - } - - // Level 3: Cross-checked without certificate - if factors.confirming_provers >= 2 { - return TrustLevel::Level3; - } - - // Level 2: Single prover, no dangerous axioms (already checked above) - TrustLevel::Level2 + use echidna_core::trust::{axiom_tracker::DangerLevel as KernelDanger, ProverClass}; + let prover_class = if is_small_kernel_prover(factors.prover) { + ProverClass::SmallKernel + } else { + ProverClass::Other + }; + let worst_axiom_danger = match factors.worst_axiom_danger { + DangerLevel::Safe => KernelDanger::Safe, + DangerLevel::Noted => KernelDanger::Noted, + DangerLevel::Warning => KernelDanger::Warning, + DangerLevel::Reject => KernelDanger::Reject, + }; + echidna_core::trust::compute_trust_level(&echidna_core::trust::TrustFactors { + prover_class, + confirming_provers: factors.confirming_provers, + small_kernel_confirmations: factors.small_kernel_confirmations, + has_certificate: factors.has_certificate, + certificate_verified: factors.certificate_verified, + worst_axiom_danger, + solver_integrity_ok: factors.solver_integrity_ok, + }) } /// Whether a prover has a small trusted computing base (kernel) @@ -150,6 +115,7 @@ mod tests { TrustFactors { prover, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -163,6 +129,7 @@ mod tests { let factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: 2, + small_kernel_confirmations: 2, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -173,11 +140,58 @@ mod tests { assert_eq!(compute_trust_level(&factors), TrustLevel::Level5); } + /// One small-kernel prover plus a confirmer that is not a small-kernel + /// system with a checked certificate is not Level 5 (audit 2026-11-09). + #[test] + fn test_one_small_kernel_confirmation_is_not_level5() { + let factors = TrustFactors { + prover: ProverKind::Lean, + confirming_provers: 2, + small_kernel_confirmations: 1, + has_certificate: true, + certificate_verified: true, + worst_axiom_danger: DangerLevel::Safe, + solver_integrity_ok: true, + portfolio_confidence: Some(PortfolioConfidence::CrossChecked), + }; + + assert_eq!(compute_trust_level(&factors), TrustLevel::Level4); + } + + /// A verified flag with no certificate produced is not Level 4 + /// (audit 2026-11-09). + #[test] + fn test_verified_flag_without_certificate_is_not_level4() { + let mut factors = make_factors(ProverKind::Lean); + factors.certificate_verified = true; + assert_eq!(compute_trust_level(&factors), TrustLevel::Level2); + } + + /// The kernel's notion of a small kernel is `is_small_kernel_prover`. + #[test] + fn test_small_kernel_class_follows_is_small_kernel_prover() { + for prover in [ + ProverKind::Lean, + ProverKind::Coq, + ProverKind::Z3, + ProverKind::CVC5, + ] { + let factors = TrustFactors { + has_certificate: true, + certificate_verified: true, + ..make_factors(prover) + }; + let level4 = compute_trust_level(&factors) == TrustLevel::Level4; + assert_eq!(level4, is_small_kernel_prover(prover), "{prover:?}"); + } + } + #[test] fn test_lean_with_cert_level4() { let factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -193,6 +207,7 @@ mod tests { let factors = TrustFactors { prover: ProverKind::CVC5, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, diff --git a/tests/aspect_tests.rs b/tests/aspect_tests.rs index 5375fd35..5e025552 100644 --- a/tests/aspect_tests.rs +++ b/tests/aspect_tests.rs @@ -65,6 +65,7 @@ fn aspect_security_malicious_input_no_high_trust() { let trust = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, confirming_provers: 10, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, @@ -447,6 +448,7 @@ fn aspect_trust_computation_deterministic() { let factors = TrustFactors { prover: ProverKind::Z3, confirming_provers: 2, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Noted, diff --git a/tests/concurrency_test.rs b/tests/concurrency_test.rs index 747d2c5e..b60dfa7c 100644 --- a/tests/concurrency_test.rs +++ b/tests/concurrency_test.rs @@ -187,6 +187,7 @@ async fn concurrency_trust_level_computation_thread_safe() { let factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, diff --git a/tests/e2e_prover_test.rs b/tests/e2e_prover_test.rs index 1a03c72d..990c6000 100644 --- a/tests/e2e_prover_test.rs +++ b/tests/e2e_prover_test.rs @@ -114,6 +114,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l5 = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, // small-kernel prover confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -127,6 +128,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l4 = compute_trust_level(&TrustFactors { prover: ProverKind::Z3, confirming_provers: 2, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -140,6 +142,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l3 = compute_trust_level(&TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -151,6 +154,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l2 = compute_trust_level(&TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -162,6 +166,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l1 = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Warning, @@ -212,6 +217,7 @@ fn e2e_reject_axiom_prevents_high_trust() { let trust = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, confirming_provers: 5, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, // unsound construct diff --git a/tests/neural_property_tests.rs b/tests/neural_property_tests.rs index 5b380c97..1c46b86a 100644 --- a/tests/neural_property_tests.rs +++ b/tests/neural_property_tests.rs @@ -129,6 +129,7 @@ proptest! { let base_factors = TrustFactors { prover: ProverKind::Z3, confirming_provers: base_count, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -137,6 +138,7 @@ proptest! { }; let more_factors = TrustFactors { confirming_provers: base_count + extra, + small_kernel_confirmations: 0, ..base_factors.clone() }; let base_trust = compute_trust_level(&base_factors); @@ -157,6 +159,7 @@ proptest! { let safe_factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: confirming, + small_kernel_confirmations: 0, has_certificate: has_cert, certificate_verified: has_cert, worst_axiom_danger: DangerLevel::Safe, diff --git a/tests/p2p_property_tests.rs b/tests/p2p_property_tests.rs index 552fadbf..cd19fce6 100644 --- a/tests/p2p_property_tests.rs +++ b/tests/p2p_property_tests.rs @@ -115,6 +115,7 @@ fn arb_trust_factors_with_danger(danger: DangerLevel) -> impl Strategy --- --- TrustKernelMonotonicity.idr --- --- Stage 8a meta-proof: Trust-Kernel Monotonicity. --- --- Proves that the confidence engine's downgrade rules are monotone: --- --- trustMono_reject : worst_danger = Reject → compute_trust = Level1 --- trustMono_warning : worst_danger = Warning → compute_trust = Level1 --- trustMono_integrity: solver_integrity_ok = False → compute_trust = Level1 --- trustMono_level5_conditions : confirming ≥ 2 ∧ certificate_verified = True --- ∧ small_kernel = True → compute_trust ≥ Level4 --- --- Models TrustFactors as a record over the booleans and DangerLevel fields --- that drive the Rust compute_trust_level function. --- Models compute_trust_level exactly from confidence.rs lines 77-116. --- All proofs by exhaustive case analysis. Zero believe-me. - -module TrustKernelMonotonicity - -import Data.Nat -import NatLte - -%default total - --- ========================================================================== --- Section 1: DangerLevel --- ========================================================================== - -||| Mirrors DangerLevel from axiom_tracker.rs. -||| The derive(PartialOrd, Ord) on the Rust side gives Safe < Noted < Warning < Reject -||| (matching declaration order). We do not need the full order here — only -||| equality tests used by compute_trust_level. -public export -data DangerLevel = Safe | Noted | Warning | Reject - --- ========================================================================== --- Section 2: TrustLevel (5-element ordered type) --- ========================================================================== - -||| 5-element trust hierarchy from confidence.rs. -||| Level1 < Level2 < Level3 < Level4 < Level5. -public export -data TrustLevel - = Level1 -- 1: dangerous axiom / bad integrity / rejected - | Level2 -- 2: single prover, no dangerous axioms - | Level3 -- 3: certificate present and verified, or cross-checked - | Level4 -- 4: small-kernel prover with verified certificate - | Level5 -- 5: cross-checked by 2+ small-kernel provers with certs - -||| Numeric encoding of TrustLevel (1–5). -public export -trustValue : TrustLevel -> Nat -trustValue Level1 = 1 -trustValue Level2 = 2 -trustValue Level3 = 3 -trustValue Level4 = 4 -trustValue Level5 = 5 - --- ========================================================================== --- Section 3: TrustLevel ordering --- ========================================================================== - -||| Ordering on TrustLevel encoded via trustValue LTE. -public export -TrustLTE : TrustLevel -> TrustLevel -> Type -TrustLTE a b = trustValue a `LTE` trustValue b - --- Convenience constructor aliases used in proofs below. - -trustLTE_refl : (t : TrustLevel) -> TrustLTE t t -trustLTE_refl Level1 = lteLit 1 1 -trustLTE_refl Level2 = lteLit 2 2 -trustLTE_refl Level3 = lteLit 3 3 -trustLTE_refl Level4 = lteLit 4 4 -trustLTE_refl Level5 = lteLit 5 5 - -||| Level4 ≤ Level4 and Level4 ≤ Level5: both satisfy ≥ Level4. -||| Bodies use lteLit (machine-checked); level4LTELevel5 previously mis-counted -||| as LTE 5 5 instead of LTE 4 5. -level4LTELevel4 : TrustLTE Level4 Level4 -level4LTELevel4 = lteLit 4 4 - -level4LTELevel5 : TrustLTE Level4 Level5 -level4LTELevel5 = lteLit 4 5 - --- ========================================================================== --- Section 4: TrustFactors record --- ========================================================================== - -||| Abstracted TrustFactors record carrying only the fields that -||| determine which branch of compute_trust_level fires. -||| -||| We drop `prover : ProverKind` and fold is_small_kernel into a -||| boolean flag `small_kernel`, which is the only property of the -||| prover that compute_trust_level queries. -||| We drop `portfolio_confidence` and `has_certificate` beyond their -||| influence on certificate_verified, matching the code structure. -public export -record TrustFactors where - constructor MkTrustFactors - confirming_provers : Nat - certificate_verified : Bool - worst_axiom_danger : DangerLevel - solver_integrity_ok : Bool - small_kernel : Bool - --- ========================================================================== --- Section 5: compute_trust_level (Idris2 model of confidence.rs) --- ========================================================================== - -||| Direct transcription of compute_trust_level (confidence.rs lines 77-116). -||| -||| Branch order is preserved exactly: -||| 1. worst_axiom_danger = Reject → Level1 -||| 2. worst_axiom_danger = Warning → Level1 -||| 3. solver_integrity_ok = False → Level1 -||| 4. confirming ≥ 2 ∧ cert_verified ∧ small_kernel → Level5 -||| 5. small_kernel ∧ cert_verified → Level4 -||| 6. cert_verified → Level3 -||| 7. confirming ≥ 2 → Level3 -||| 8. (default) → Level2 -public export -computeTrustLevel : TrustFactors -> TrustLevel -computeTrustLevel f = - case f.worst_axiom_danger of - Reject => Level1 - Warning => Level1 - _ => - case f.solver_integrity_ok of - False => Level1 - True => - case (f.confirming_provers >= 2, f.certificate_verified, f.small_kernel) of - (True, True, True) => Level5 - (_, True, True) => Level4 - (_, True, False) => Level3 - (True, False, _) => Level3 - _ => Level2 - --- ========================================================================== --- Section 6: Downgrade proofs --- ========================================================================== - -||| trustMono_reject: worst_danger = Reject → compute_trust = Level1. -||| -||| Proof: computeTrustLevel pattern-matches on worst_axiom_danger first; -||| the Reject branch immediately returns Level1 regardless of all other fields. -public export -trustMono_reject - : (f : TrustFactors) - -> f.worst_axiom_danger = Reject - -> computeTrustLevel f = Level1 -trustMono_reject (MkTrustFactors _ _ Reject _ _) Refl = Refl -trustMono_reject (MkTrustFactors _ _ Safe _ _) Refl impossible -trustMono_reject (MkTrustFactors _ _ Noted _ _) Refl impossible -trustMono_reject (MkTrustFactors _ _ Warning _ _) Refl impossible - -||| trustMono_warning: worst_danger = Warning → compute_trust = Level1. -||| -||| Proof: the Warning branch fires immediately after Reject, returning Level1. -public export -trustMono_warning - : (f : TrustFactors) - -> f.worst_axiom_danger = Warning - -> computeTrustLevel f = Level1 -trustMono_warning (MkTrustFactors _ _ Warning _ _) Refl = Refl -trustMono_warning (MkTrustFactors _ _ Safe _ _) Refl impossible -trustMono_warning (MkTrustFactors _ _ Noted _ _) Refl impossible -trustMono_warning (MkTrustFactors _ _ Reject _ _) Refl impossible - --- ========================================================================== --- Section 7: Integrity downgrade --- ========================================================================== - -||| A witness that the solver integrity check failed. -||| We use a named record to carry the proof cleanly. -public export -data BadIntegrity : TrustFactors -> Type where - ||| The solver_integrity_ok field is False. - MkBadIntegrity - : (f : TrustFactors) - -> f.solver_integrity_ok = False - -> BadIntegrity f - -||| trustMono_integrity: BadIntegrity f → compute_trust = Level1. -||| -||| Proof: we case-split on worst_axiom_danger. For Reject and Warning the -||| result is Level1 independently (earlier branches fire). For Safe and -||| Noted we reach the solver_integrity_ok = False branch which returns Level1. -public export -trustMono_integrity - : (f : TrustFactors) - -> BadIntegrity f - -> computeTrustLevel f = Level1 -trustMono_integrity (MkTrustFactors _ _ Reject False _) (MkBadIntegrity _ Refl) = Refl -trustMono_integrity (MkTrustFactors _ _ Warning False _) (MkBadIntegrity _ Refl) = Refl -trustMono_integrity (MkTrustFactors _ _ Safe False _) (MkBadIntegrity _ Refl) = Refl -trustMono_integrity (MkTrustFactors _ _ Noted False _) (MkBadIntegrity _ Refl) = Refl --- solver_integrity_ok = True contradicts the BadIntegrity witness: -trustMono_integrity (MkTrustFactors _ _ Reject True _) (MkBadIntegrity _ Refl) impossible -trustMono_integrity (MkTrustFactors _ _ Warning True _) (MkBadIntegrity _ Refl) impossible -trustMono_integrity (MkTrustFactors _ _ Safe True _) (MkBadIntegrity _ Refl) impossible -trustMono_integrity (MkTrustFactors _ _ Noted True _) (MkBadIntegrity _ Refl) impossible - --- ========================================================================== --- Section 8: Level5 sufficient conditions --- ========================================================================== - -||| trustMono_level5_conditions: -||| confirming ≥ 2 ∧ certificate_verified = True ∧ small_kernel = True -||| → compute_trust ≥ Level4. -||| -||| In fact under these conditions compute_trust = Level5, so we prove the -||| equality first and derive ≥ Level4 as a corollary. -||| -||| Proof: we case-split on worst_axiom_danger and solver_integrity_ok. -||| The only dangerous-axiom paths (Reject, Warning) return Level1, which -||| contradicts the Level5 hypothesis — but since we are proving the -||| implication in the SAFE direction (the precondition is the clean case), -||| we can restrict attention to worst_axiom_danger ∈ {Safe, Noted} -||| combined with solver_integrity_ok = True. In that regime, the first -||| inner case fires (True, True, True) → Level5. - -||| Helper: under clean conditions the Level5 branch fires. -public export -trustMono_level5_exact - : (n : Nat) - -> (n >= 2 = True) - -> (danger : DangerLevel) - -> Either (danger = Safe) (danger = Noted) - -> computeTrustLevel (MkTrustFactors n True danger True True) = Level5 -trustMono_level5_exact n hge Safe (Left Refl) with (n >= 2) - trustMono_level5_exact n hge Safe (Left Refl) | True = Refl - trustMono_level5_exact n _ Safe (Left Refl) | False impossible -trustMono_level5_exact n hge Noted (Right Refl) with (n >= 2) - trustMono_level5_exact n hge Noted (Right Refl) | True = Refl - trustMono_level5_exact n _ Noted (Right Refl) | False impossible -trustMono_level5_exact _ _ Reject (Left Refl) impossible -trustMono_level5_exact _ _ Reject (Right Refl) impossible -trustMono_level5_exact _ _ Warning (Left Refl) impossible -trustMono_level5_exact _ _ Warning (Right Refl) impossible - -||| The corollary: under the clean triple-condition the result is ≥ Level4. -||| Since Level5 ≥ Level4 (trustValue Level5 = 5 ≥ 4 = trustValue Level4). -public export -trustMono_level5_conditions - : (n : Nat) - -> (n >= 2 = True) - -> (danger : DangerLevel) - -> Either (danger = Safe) (danger = Noted) - -> TrustLTE Level4 - (computeTrustLevel (MkTrustFactors n True danger True True)) -trustMono_level5_conditions n hge Safe (Left Refl) with (n >= 2) - trustMono_level5_conditions n hge Safe (Left Refl) | True = level4LTELevel5 - trustMono_level5_conditions n _ Safe (Left Refl) | False impossible -trustMono_level5_conditions n hge Noted (Right Refl) with (n >= 2) - trustMono_level5_conditions n hge Noted (Right Refl) | True = level4LTELevel5 - trustMono_level5_conditions n _ Noted (Right Refl) | False impossible -trustMono_level5_conditions _ _ Reject (Left Refl) impossible -trustMono_level5_conditions _ _ Reject (Right Refl) impossible -trustMono_level5_conditions _ _ Warning (Left Refl) impossible -trustMono_level5_conditions _ _ Warning (Right Refl) impossible - --- ========================================================================== --- Section 9: Injectivity witnesses (Level1 is the unique floor) --- ========================================================================== - -||| The three downgrade paths produce identical output (Level1), and that -||| output is incompatible with any level ≥ Level2. -public export -level1NotLevel2 : Level1 = Level2 -> Void -level1NotLevel2 Refl impossible - -public export -level1NotLevel3 : Level1 = Level3 -> Void -level1NotLevel3 Refl impossible - -public export -level1NotLevel4 : Level1 = Level4 -> Void -level1NotLevel4 Refl impossible - -public export -level1NotLevel5 : Level1 = Level5 -> Void -level1NotLevel5 Refl impossible diff --git a/verification/proofs/idris2/echidna-verif-proofs.ipkg b/verification/proofs/idris2/echidna-verif-proofs.ipkg index cf5b4dee..d58a3761 100644 --- a/verification/proofs/idris2/echidna-verif-proofs.ipkg +++ b/verification/proofs/idris2/echidna-verif-proofs.ipkg @@ -28,5 +28,4 @@ modules = AxiomCompleteness , NatLte , ProofStateSerialisation , ProverKindInjectivity - , TrustKernelMonotonicity , TrustLevelSoundness From 5de37bf70e2716cd441f40f9c11d1fea34550446 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:08:18 +0000 Subject: [PATCH 5/9] =?UTF-8?q?docs(proofs):=20PROOF-STATUS=20under=20stri?= =?UTF-8?q?ct=20=C2=A71,=20PWG=20census,=20and=20a=20=C2=A78.2=20cone=20re?= =?UTF-8?q?ceipt?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Owner ruling 2026-11-09: apply PROOF-POLICY §1 strictly. A statement that names one of this repository's types, functions or wire formats is engineering, whichever prover it is written in. The ledger is reworked to match, using the findings of the 2026-11-09 proof audit and its skeptic re-checks. Classification: - Theory: Receipt.agda, ten theorems (R4a). It owes the Rocq and Lean rechecks (R5). - Engineering models with no standing as evidence for the Rust code, which stays open under R1 (Creusot with Pearlite, and Verus, §1.2): - the other eight meta-checker modules (R4b); - the five Lean files, which are not §4 exceptions (R3); - the Idris 2 files under verification/proofs/idris2 (R2b). - The Idris 2 ABI package keeps its §1 home (R2a). Corrections: - R3: the Lean files build green in CI (job 127501093731 at a81467b, the same tree as main). The "all five fail to compile" row was stale. - R2a: cites its CI receipt (run 38496490567, 20/20 modules plus the falsifier fixtures). It also records the coverage gap (10 of 30 .idr files never type-checked) and the narrow dangerous-pattern grep. - R6/E9: ProofComposition.agda proves only list-append associativity and left identity. Moving it would not discharge E9, which no theorem states. PROOF-NEEDS is corrected to match. - The models' disagreements with the Rust code are listed for R1: - Dispatch.compute-trust; - the Integrity "sharpness" claim; - ClampTrust, which models a function Rust does not have; - IntegrityVerification PI-11 against the four fail-open dispatch paths; - Pareto PO-12's no-duplicates assumption; - ProverKindInjectivity, whose encoding differs from the Rust function for 79 of 107 variants. Grades: - PROOF-POLICY §8 Proof Witness Grades replace the Mathesis-brief "Grade 3" wording. - A §8.5 census lists the ten theory theorems, each with its §5 token, PWG, foundation_diverse flag and both recheck legs. Receipt tooling: - scripts/ci/agda-cone-receipt.sh writes the §8.2/§8.4 receipt as one JCS object: toolchain, flags, the import cone with a SHA-256 per file, and a comment-aware scan of that cone for postulates, unsafe pragmas and primTrustMe. Postulates in Agda's own primitives are listed, not counted. - scripts/ci/test-agda-cone-receipt.sh is its fixture test. - The agda-meta-checker job runs both and prints the receipt to the log and the step summary. - Local run with the pinned Agda 2.7.0.1 and stdlib 2.1: the cone of Receipt.agda is 211 modules, the scan is clean, and Agda.Primitive's two universe-level postulate blocks are the only kernel primitives. Adjacent docs: - EXPLAINME no longer calls the Agda models "independent formal verification of the Rust trust-pipeline properties", and no longer lists proofs/agda/ (a §3 fixture tree) as the meta-checker. - DEBT's R9 reference now points at R4b. - meta-checker/README.adoc no longer claims one funext postulate. --safe refuses any postulate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- .github/workflows/agda-meta-checker.yml | 25 +- EXPLAINME.adoc | 11 +- docs/DEBT.adoc | 2 +- docs/PROOF-NEEDS.adoc | 6 +- docs/PROOF-STATUS.adoc | 413 ++++++++++++------------ meta-checker/README.adoc | 2 +- scripts/ci/agda-cone-receipt.sh | 138 ++++++++ scripts/ci/test-agda-cone-receipt.sh | 32 ++ 8 files changed, 423 insertions(+), 206 deletions(-) create mode 100755 scripts/ci/agda-cone-receipt.sh create mode 100755 scripts/ci/test-agda-cone-receipt.sh diff --git a/.github/workflows/agda-meta-checker.yml b/.github/workflows/agda-meta-checker.yml index 301110dc..5a1f6efc 100644 --- a/.github/workflows/agda-meta-checker.yml +++ b/.github/workflows/agda-meta-checker.yml @@ -55,7 +55,7 @@ jobs: GH_TOKEN: ${{ github.token }} run: | set -euo pipefail - PATTERN='^(meta-checker/|scripts/ci/(setup-agda|check-agda|check-receipt-controls)\.sh$|\.github/workflows/agda-meta-checker\.yml$)' + PATTERN='^(meta-checker/|scripts/ci/(setup-agda|check-agda|check-receipt-controls|agda-cone-receipt|test-agda-cone-receipt)\.sh$|\.github/workflows/agda-meta-checker\.yml$)' if [ "${{ github.event_name }}" = "pull_request" ]; then FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \ --paginate --jq '.[].filename') @@ -85,3 +85,26 @@ jobs: - name: Type-check meta-checker (PROOF-POLICY §2.1 canonical invocation) if: steps.detect.outputs.relevant == 'true' run: bash scripts/ci/check-agda.sh + + # PROOF-POLICY §8.2/§8.4: the receipt a PWG-3 grade is derived from. It + # records the toolchain, the flags, the import cone of the theory + # module with a digest per file, and a comment-aware postulate scan of + # that cone. The receipt is printed to the log and the step summary. + - name: Record the §8.2 cone receipt for the theory theorems (Receipt.agda) + if: steps.detect.outputs.relevant == 'true' + env: + AGDA_STDLIB_SHA256: 72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431 + run: | + set -euo pipefail + bash scripts/ci/test-agda-cone-receipt.sh + receipt="$RUNNER_TEMP/agda-cone-receipt.json" + (cd meta-checker && bash ../scripts/ci/agda-cone-receipt.sh src/Echidna/Receipt.agda) > "$receipt" + cat "$receipt" + { + echo '## PROOF-POLICY §8.2 cone receipt (Receipt.agda)' + jq -r '"commit \(.source.commit), \(.toolchain.agda), \(.import_cone.count) modules in the import cone, postulate scan: \(.postulate_scan.result)"' "$receipt" + echo + echo '```json' + cat "$receipt" + echo '```' + } >> "$GITHUB_STEP_SUMMARY" diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 5079b7dd..1ec8cd12 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -164,8 +164,12 @@ ECHIDNA-specific anchors: backends). * `generated/abi/` — auto-generated C headers from the Idris2 ABI. -The Agda meta-checker provides independent formal verification of the -Rust trust-pipeline properties; see `proofs/agda/`. +The Agda meta-checker (`meta-checker/`) type-checks *models* of the trust +pipeline and one theory result (receipt vs warrant). A model is not a proof +about the Rust code: under `3-practice/PROOF-POLICY.adoc` §1 the Rust +behaviour is verified with Creusot/Pearlite and Verus on the code, and that is +still open. `proofs/agda/` is a test corpus, not evidence. Status per +obligation: `docs/PROOF-STATUS.adoc`. == File map: key modules @@ -194,7 +198,8 @@ Rust trust-pipeline properties; see `proofs/agda/`. | `src/ui/tea/`, `src/ui/public/` | TEA sources (compile pipeline unavailable) and working static shell | `src/abi/` | Idris2 formal specifications (ABI contracts + totality proofs) | `ffi/zig/`, `src/zig_ffi/` | Zig FFI implementation -| `proofs/agda/` | Agda meta-checker (independent verification of trust properties) +| `meta-checker/` | Agda meta-checker: trust-pipeline models and the receipt/warrant theory (see `docs/PROOF-STATUS.adoc`) +| `proofs/agda/` | Agda test corpus (fixtures for the Agda backend; not evidence, `PROOF-POLICY` §3) | `tests/` | Integration / property / interface test suites |=== diff --git a/docs/DEBT.adoc b/docs/DEBT.adoc index df7ba09e..7d97b891 100644 --- a/docs/DEBT.adoc +++ b/docs/DEBT.adoc @@ -442,7 +442,7 @@ Fixed so far: the docs and the published site now say "capability present, not currently engaged" instead of claiming a step that does not run. Now machine-checked on the specification side: -`+meta-checker/src/Echidna/Integrity.agda+` (`+docs/PROOF-STATUS.adoc+` R9) +`+meta-checker/src/Echidna/Integrity.agda+` (`+docs/PROOF-STATUS.adoc+` R4b, an engineering model under the 2026-11-09 §1 classification; the Rust obligation is R1) proves that verification in its model requires an initialised manifest and that an uninitialised manifest never verifies. Its explicit hypothesis is digest-comparison soundness: an accepted comparison implies equal digests. diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index e39973e9..643d0bff 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -78,8 +78,10 @@ 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 |*none* (corrected 2026-11-09) +|Not stated by any theorem. `+proofs/agda/ProofComposition.agda+`, cited here +before, proves only list-append associativity and left identity. See +PROOF-STATUS R6 |— |E12 ProofState serialization losslessness |`+verification/proofs/idris2/ProofStateSerialisation.idr+` diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index fc7062f4..1290a387 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -3,7 +3,7 @@ = Proof status — policy-vocabulary view -*Status*: reviewed 2026-11-04. Each row is scoped to its recorded source +*Status*: reviewed 2026-11-09 (strict §1 classification; proof audit of that date). Each row is scoped to its recorded source identity and check; this file does not claim a single revision was checked for every obligation. *Normative policy*: `+3-practice/PROOF-POLICY.adoc+` in @@ -62,242 +62,260 @@ CI gate exists and the authors say it passes" when no receipt is cited. |Not done. |=== -=== Relation to the Mathesis grades - -https://github.com/hyperpolymath/mathesis[mathesis], *Estate-wide Mathematical -Knowledge Architecture* §5, grades a *theorem* by how far its witness has -travelled: **Grade 3** type-checks locally in its home system and is not -translated; **Grade 2i/2ii** one / two independent translations with statement -correspondence recorded; **Grade 1** machine-checked through a verified checker -API in headless CI. - -The two vocabularies are orthogonal — one grades a theorem's reach, the other -records whether a repository's obligation was discharged — but they interact: - -* A home-system leg may be `+proven+` while every independent leg is `+open+`. - That combination *is* Grade 3, and it is the ceiling for anything in this - repository. -* A translation leg is `+argued+`, not `+proven+`, until the statement - correspondence is recorded (`+PROOF-POLICY+` §2: "`the kernel checks the term - only against the translated statement`"). - -Mathesis §6 forbids flattening assurance into a percentage. See R5 and R6. +=== Proof Witness Grades (`+PROOF-POLICY+` §8) + +The only estate proof grade is the *Proof Witness Grade* of `+PROOF-POLICY+` +§8, written with its prefix: `+PWG-3+` < `+PWG-2i+` < `+PWG-2ii+` < +`+PWG-1+`, with `+PWG-1+` the strongest. The Mathesis brief's "Grade 3/2i/2ii/1" +is superseded by §8 and is not used here. + +* PWG grades apply to *theory* theorems only (§8.1). Engineering + obligations, including every statement about this repository's types, + functions or wire formats, carry a §5 token and no grade. +* A grade is *derived from receipts*, never asserted (§8.4). `+PWG-3+` needs a + receipt that records the Agda version, the standard-library pin, the flags + in force, the import cone, and a comment-aware postulate scan of that cone + (§8.2, §8.4). A recheck leg counts only when it is kernel-checked *and* its + statement correspondence is `+RECONCILED+` (§2.2). +* The census below gives counts with their denominator, never a percentage. + +== Classification under §1 (owner ruling 2026-11-09) + +The owner ruled to apply §1's test strictly: a statement that names a type, +function or wire format of this repository is *engineering*, whatever prover +it is written in. Rust behaviour is verified with Creusot/Pearlite and Verus +on the code (§1.2); a separately written model, in Agda, Lean or Idris 2, +does not establish implementation correctness. Consequences for this file: + +* Of the nine meta-checker modules, only `+Receipt.agda+` is theory. The + other eight model echidna's own trust pipeline and are recorded under + R4b as engineering models; the Rust obligations they describe are R1's. +* The five Lean files are engineering models of Rust code, not §4 + exceptions (none carries a §4 header record). Their Rust obligations are + R1's. +* The Idris 2 files under `+verification/proofs/idris2/+` that restate Rust + behaviour (trust levels, clamp, dispatch) are likewise models; the Idris 2 + ABI package in `+src/abi/+` is Idris 2's proper §1 home (R2a). +* The Rocq/Lean recheck obligation (§2, R5) applies to the theory theorems + only: `+Receipt.agda+`. == Obligations Grouped by the `+PROOF-POLICY+` §1 mapping, because that is what decides which verifier is even allowed to carry the row. -=== Rust — Creusot (§1: first-party Rust) +=== Rust — Creusot with Pearlite contracts, and Verus (§1, §1.2) [width="100%",cols="24%,13%,38%,25%",options="header"] |=== |Obligation |Row |Basis |Evidence / next step -|R1. Trust pipeline, dispatch, arbitration, Pareto +|R1. Trust pipeline on the Rust code: trust levels (TK-4, TK-5), clamp, +dispatch stage order and integrity gating, arbitration, Pareto frontier, +portfolio outcome mapping, axiom classification |`+open+` -|`+PROOF-POLICY+` §1 maps first-party Rust to Creusot. -|`+crates/echidna-core-creusot+` describes itself as "`Creusot-annotated (not -yet proved)`"; the `+creusot+` dev-dependency is commented out and the crate -builds on stable Rust behind a `+creusot+` feature. Annotation is not proof. Row -stays `+open+` until a Creusot run yields a receipt with a commit hash. +|`+PROOF-POLICY+` §1 and §1.2 map first-party Rust to Creusot with Pearlite +contracts, and Verus, on the implementation. Under the 2026-11-09 +classification this row also inherits the Rust obligations that the Agda, +Lean and Idris 2 models only describe (R3, R4b, R2b). +|*Creusot:* `+crates/echidna-core-creusot+` carries the contracts. They are +stated, not discharged: `+creusot-contracts+` is not a dependency, the +nightly pin is stale, and no run has produced a receipt. +*Verus:* not yet applied. Planned scope: the same TK-4/TK-5 obligations on +`+echidna_core::trust::compute_trust_level+`, then dispatch integrity gating. +*Tested:* TK-4, TK-5 and monotonicity are `+tested-only+`, checked over every +input with counts 0..=4 by the kernel crate's `+impl_invariants::tk*+` tests. +*Known gaps the models hid:* dispatch accepts an unverified solver in four +ways (an `+Uninitialized+` status, a prover missing from the manifest, no +checker configured, and a `+verify_all()+` error read as an empty report), +and runs the integrity step after proving, not first. Row stays `+open+` +until a Creusot or Verus run yields a receipt with a commit hash. + +|=== *Trust kernel (2026-11-09).* `+compute_trust_level+` exists once, in `+crates/echidna-core-creusot+`; `+src/rust/verification/confidence.rs+` re-exports its `+TrustLevel+` and delegates to it. Two defects found by the 2026-11-09 proof audit are fixed at that source: Level 4 fired on `+certificate_verified+` without `+has_certificate+`, and Level 5 checked only -the producing prover's kernel class. The new contracts are TK-4 (Level 4 and -above need a small kernel and a produced, verified certificate) and TK-5 -(Level 5 needs two or more small-kernel confirmations, the new -`+small_kernel_confirmations+` input). They are `+tested-only+`: -`+impl_invariants::tk4_*+`, `+tk5_*+` and `+tk6_*+` (monotone in the -evidence) check every input with counts 0..=4. That covers every case only -because the rule reads counts through `+>= 2+` and a minimum, which is -argued, not mechanised. The Creusot annotations are stated, not discharged. -Verus (§1.2) has not been applied yet; its scope is the same TK obligations -on the same function. The Idris 2 `+TrustKernelMonotonicity+` model, which -proved the defective Level 5 rule, is retired. - -|=== +the producing prover's kernel class. The contracts are TK-4 (Level 4 and above +need a small kernel and a produced, verified certificate) and TK-5 (Level 5 +needs two or more small-kernel confirmations, the `+small_kernel_confirmations+` +input). The bounded tests cover every case only because the rule reads counts +through `+>= 2+` and a minimum, which is argued, not mechanised. The Idris 2 +`+TrustKernelMonotonicity+` model, which proved the defective Level 5 rule, is +retired. === Idris 2 — APIs, ABIs, engineering properties (§1) -`+PROOF-NEEDS+` lists E2, E3, E5, E6, E7, E12, the VQL-UT row, the extensive -ABI row and the Stage-8a trio as constructively proved, all in -`+verification/proofs/idris2/+` or `+src/abi/+`, all with zero `+believe_me+` -(the `+PROOF-NEEDS+` audit of 2026-05-18 establishes that the 21 -`+believe_me+` grep hits are prose and detector strings). - [width="100%",cols="24%,13%,38%,25%",options="header"] |=== |Obligation |Row |Basis |Evidence / next step -|R2. Idris 2 interface/ABI obligations (E2, E3, E5, E6, E7, E12, Stage 8a, -VQL-UT, extensive ABI) -|`+argued+` -|`+PROOF-POLICY+` §1 maps ABIs and engineering properties to Idris 2. The -artefacts exist and are detailed in `+PROOF-NEEDS+`. -|No `+idris2 --build+` receipt for -`+verification/proofs/idris2/echidna-verif-proofs.ipkg+` is cited with a commit -hash. Promote to `+proven+` by citing a green run and its commit — that is a -one-line change, and it is the cheapest upgrade in this file. +|R2a. ABI package `+src/abi/echidnaabi.ipkg+`: the 20 modules it lists +|`+proven+` +|`+PROOF-POLICY+` §1 maps ABIs to Idris 2. CI receipt: `+idris2-abi-ci+` run +38496490567, head `+6883126+`, built 20/20 modules plus both falsifier +fixtures (`+Mismatch between: True and False+`). The `+src/abi+` tree hash at +that commit is identical to `+2ab7574+`. Trust boundary: the Idris 2 0.8.0 +kernel, built in CI from the v0.8.0 tag. +|*Coverage gap, not covered by this row:* 10 of the 30 `+.idr+` files under +`+src/abi+` are never type-checked: `+EchidnaABI/CapnSchemas.idr+`, +`+CoprocessorForeign.idr+` and `+NeSyAssistTesting.idr+` (outside the ipkg), +`+Foreign.idr+` (module `+Echidna.ABI.Foreign+`, differing from +`+EchidnaABI/Foreign.idr+`), and six byte-identical duplicates at mismatched +paths. Those ten are `+open+`. The CI grep checks `+believe_me+`, +`+assert_total+`, `+unsafePerformIO+` and `+prim__crash+`; it does not check +`+postulate+`, `+partial+`, `+covering+`, `+assert_smaller+` or +`+idris_crash+`. + +|R2b. `+verification/proofs/idris2/+` (10 modules after the +`+TrustKernelMonotonicity+` retirement) +|`+open+` for the Rust obligations they describe (R1) +|CI receipt: dogfood job 127501094018 at `+a81467b+` type-checked the 11-module +package as it then stood ("all files type-check"). Type-checking a model is +not evidence for the Rust code (§1). +|Several modules prove less than their names say: +`+TrustLevelSoundness+` holds by definition of a local function that +disagrees with Rust; `+DispatchCorrectness+` never mentions +`+select_prover+`; `+DispatchOrdering+` proves `+LT 0 1 … LT 0 5+` over an +unused type; `+BasicTotality+` is filler by its own header; +`+ClampTrustBounds+` models a `+Nat → TrustLevel+` function that does not +exist in Rust (the real `+clamp_trust+` is a three-argument range clamp); +`+ProverKindInjectivity+` encodes 79 of 107 variants differently from +`+src/rust/ffi/mod.rs+`, so it is about a different function. Retire or +re-title them; do not count them as evidence. |=== -=== Lean 4 — cross-checks and algebraic properties (§4 exceptions) +=== Lean 4 — engineering models (§1; not §4 exceptions) [width="100%",cols="24%,13%,38%,25%",options="header"] |=== |Obligation |Row |Basis |Evidence / next step -|R3. Lean 4 legs: E4-L4 `+ConfidenceLattice.lean+`, E10 -`+ParetoMaximality.lean+` / `+ParetoStrongMaximality.lean+`, E11 -`+IntegrityVerification.lean+`, E13 `+PortfolioCompleteness.lean+` -|`+open+` -|Directly recorded: `+lake build+` run 2026-05-18 (Lean 4.13.0) — *all five -fail to compile*, 49 / 2 / 1 / 5 / 31 errors, three root causes -(`+unfold_let+` removed in 4.13.0; Mathlib tactics under a zero-mathlib -lakefile; instance synthesis and module resolution). -|Nothing. This row is correct and must not be softened. `+PROOF-NEEDS+` records -that `+ConfidenceLattice.lean+` was left byte-identical and that the -`+unfold_let+` token-swap made it worse (104 errors). The open decision is -Mathlib-vs-core, which is an owner call. +|R3. `+ConfidenceLattice.lean+`, `+ParetoMaximality.lean+`, +`+ParetoStrongMaximality.lean+`, `+IntegrityVerification.lean+`, +`+PortfolioCompleteness.lean+` +|`+open+` for the Rust obligations they describe (R1) +|*Corrected 2026-11-09.* The earlier row said all five fail to compile (a +2026-05-18 run). CI receipt at `+a81467b+`: dogfood run 42100322554, job +127501093731, Lean 4.13.0, `+lake build+` green for all five with no warning +lines. The `+verification/proofs+` tree hash is identical at `+2ab7574+`. No +`+#print axioms+` output is recorded; `+Pareto*+` and `+PortfolioCompleteness+` +use `+Classical.byContradiction+`. No file carries a §4 header record, and +each names `+confidence.rs+`, `+pareto.rs+` or dispatch types, so under §1 +they are engineering models. +|What the models say about the code, for R1: `+ConfidenceLattice+` matched +the pre-2026-11-09 trust rule branch for branch and now describes the old +rule; `+IntegrityVerification+` PI-11 (`+solver_integrity_ok+` iff +`+Verified+`) contradicts the four fail-open paths in dispatch, and its +collision-resistance classes assume injectivity on unbounded byte strings, +which real digests cannot satisfy; PO-12 in `+ParetoMaximality+` assumes no +two candidates share all four objective values, which real input can +violate. Toolchain installed outside Guix or the container with no §6 +deviation record. |=== -=== Agda — theory and metatheory (§1, §2) +=== Agda — theory (§1, §2) and engineering models [width="100%",cols="24%,13%,38%,25%",options="header"] |=== |Obligation |Row |Basis |Evidence / next step -|R4. Agda meta-checker: trust-level order, axiom safety, portfolio, dispatch, -axiom-tracker completeness, integrity, clamp bounds, receipt/warrant (9 modules) +|R4a. Theory: receipt vs warrant, `+meta-checker/src/Echidna/Receipt.agda+` |`+proven+` -|First-party Agda in `+meta-checker/src/+`, type-checked with the §2.1 -canonical invocation. The reproducible local receipt is -link:reports/2026-11-04-agda-meta-checker-receipt.json[`+2026-11-04-agda-meta-checker-receipt.json+`]. -It records base commit `+9dd7847dfb095f0ddf3d41bac3327fcc4486fb6b+` plus -the exact SHA-256 of every checked source and library descriptor, and names -the three source files modified in that working tree. It is not a claim -that the unmodified base commit contains these repairs. - ----- -agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" \ - --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda ----- - -Run from `+meta-checker/+`; the explicit library file lists the pinned -standard library and `+meta-checker/echidna-meta.agda-lib+`. Versions: -Agda `+2.7.0.1+`, `+agda-stdlib+` `+2.1+`; archive digests are in the receipt. -Observed exit 0, all 9 full module paths produced fresh interfaces. -The positive receipt/test witnesses and three rejecting verdict controls -also passed. The log contained 55 warnings, all -`+-W[no]UnsupportedIndexedMatch+`, at six sites in `+TrustLevel+`, -`+AxiomSafety+`, `+ClampTrust+` and `+Receipt+`. `+--safe+` enforces the -absence of proof escape hatches; a text search alone is not the receipt. -|Trust boundary, named: the Agda 2.7.0.1 kernel under `+--safe+`, plus the -stdlib. **Limit, recorded not hidden:** those warnings mean the flagged -functions do not *compute* under Cubical transports. The corpus is -`+--cubical-compatible+`, not `+--cubical+` — exactly the distinction -`+PROOF-POLICY+` §2.1 draws — and dropping the warning, or the flag, to get a -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. - -**Correction to the old receipt:** `+916b769+` predates `+Integrity+`, -`+ClampTrust+` and `+Receipt+`, and its entrypoint omitted -`+AxiomTrackerCompleteness+`. It cannot substantiate a nine-module claim. -The earlier 2026-11-01 timing/count report is historical, not the evidence -for the current `+proven+` row; the source-bound 2026-11-04 receipt replaces it. - -|R9. E11 solver-integrity soundness -|`+proven+` -|`+meta-checker/src/Echidna/Integrity.agda+`, inside the R4 receipt. States the -obligation that had no Agda record: verification requires an initialised -manifest; verification means the recorded digest was matched; a binary with -a different digest is never verified; an uninitialised manifest never -verifies. Digest-comparison soundness is a record *field*, not a postulate, -so the matching theorem is explicitly conditional on that field. -`+sharpness-blocks-soundness+` refutes the exact soundness property for an -accept-everything comparator. -**Scope of the model (from review, 2026-11-01):** a binary is modelled by its -digest alone, so these are statements about *digests*, not bytes. -"Substituted" means "a binary whose digest differs", and two binaries colliding -on a digest are not distinguished by this model. `+≈d-sound+` says that an -accepted comparison implies equal digests; the model contains neither -binary contents nor a hashing function. Content-level collision resistance -is outside this model, not a property established or assumed by that field. - -|**Specification, not implementation.** Rust returns -`+IntegrityStatus::Uninitialized+` for an installed binary with a placeholder -manifest, and dispatch can permit that status. It does not report -`+Verified+` in that case. Agda proves a property of its `+check+` function -and has no dispatch-permission decision. DEBT D9 is therefore a source -comparison, not a machine-checked discrepancy or refinement proof. The Rust -implementation leg remains open under R1's Creusot obligation. - -|R10. ClampTrustBounds -|`+proven+` -|`+meta-checker/src/Echidna/ClampTrust.agda+`, inside the R4 receipt. Restates -the four obligations of `+verification/proofs/idris2/ClampTrustBounds.idr+` -(bounds, monotonicity, fixed points, and — added — idempotence, i.e. that the -clamp lands on a real level rather than between two) over the trust-level type -the gate actually checks. -|This row establishes finite-order algebra in the Agda model. It does not -validate the Idris2 file or its correspondence to runtime code. Existing -Idris2 interface and engineering checks remain active under §1; their -receipt status is R2. Monotonicity here is by step lemma plus transitivity, -rather than the Idris2 file's decision table. - -|R11. Epistemic separation: receipt vs warrant -|`+proven+` -|`+meta-checker/src/Echidna/Receipt.agda+`, inside the R4 receipt. A two-world -Kripke countermodel: a receipt is factive, a warrant is not, and no uniform -function can promote every warrant to a receipt. No receipt for `+sound+` -exists in the coarse frame. The sharpened frame has an inhabited -`+Asserts assumptions sharpened proven sound w-here+` witness, so the -stronger token is not vacuously impossible. Warrant and receipt can coexist -when both are justified. `+proven-with-postulates+` records a named, -explicitly interpreted assumption and a function from it to a receipt; -discharging that assumption is required. `+tested-only+` has a distinct -nonempty sample population with a checked result per sample. The model -refutes unconditional promotions from conditional and bounded evidence. -|Semantic rewrite of the receipt/warrant distinction from +|Checked with the §2.1 canonical invocation as part of the meta-checker +entrypoint (below). A two-world Kripke model: a receipt is factive, a warrant +is not, no uniform function promotes every warrant to a receipt, and neither +conditional nor bounded evidence promotes unconditionally. Semantic rewrite of +the receipt/warrant distinction from https://github.com/hyperpolymath/epistemic-types[epistemic-types] at -`+5422cd5+`, **not** a port or a receipt for that project's theorems. The -source project retains its own proof ownership under §2.2. This model -compares two frames; it implements no discriminating checker, transition, -external test attestation or runtime-evidence adapter. Justifying that a -real check permits the sharper frame is a separate open obligation. The -Rocq/Lean rechecks and statement correspondence also remain open in R5. - -|R5. Independent recheck of R4 in Rocq *and* Lean +`+5422cd5+`, *not* a port of that project's theorems; it implements no checker +or runtime adapter. +|Receipts: the source-bound local receipt +link:reports/2026-11-04-agda-meta-checker-receipt.json[`+2026-11-04-agda-meta-checker-receipt.json+`] +(Agda `+2.7.0.1+`, `+agda-stdlib+` `+2.1+`; source digests match `+2ab7574+`), +and the `+agda-meta-checker+` CI run 42551607796 on `+2ab7574+`, whose log +lists the import cone (242 modules checked, 221 from the stdlib). The models +are elementary: one atom, two worlds. See the census below for grades. + +|R4b. Engineering models: `+TrustLevel+`, `+AxiomSafety+`, `+Portfolio+`, +`+Dispatch+`, `+AxiomTrackerCompleteness+`, `+Integrity+`, `+ClampTrust+`, and +the `+MetaChecker+` aggregator +|`+open+` for the Rust obligations they describe (R1) +|Type-checked under §2.1 inside the same receipt. Under the 2026-11-09 +classification they are engineering models; their Agda proofs are not +evidence for the Rust code. +|What the models say, for R1: +`+Dispatch.compute-trust+` disagrees with Rust (a cross-checked result with no +certificate is Level 3 in Rust and Level 2 in Agda), and `+DispatchOrdering+` +puts integrity first where `+dispatch.rs+` runs it at step 6. +`+Integrity+` restates its soundness hypothesis; no theorem shows any +conclusion fails without it, so its "sharpness" claim does not hold. +`+ClampTrust+` models a function Rust does not have. Vacuous or partial +theorems advertised as properties: `+comment-skip-sound+` and +`+real-pattern-classified+` (`+AxiomSafety+`), `+pipeline-deterministic+` +(`+Dispatch+`), and the module-header claims listed in the 2026-11-09 audit. +The `+UnsupportedIndexedMatch+` warnings (55, at six sites) mean the flagged +functions do not compute under Cubical transports; the corpus is +`+--cubical-compatible+`, as §2.1 requires. + +|R5. Independent recheck of R4a in Rocq *and* Lean |`+open+` -|`+PROOF-POLICY+` §2: every Agda theory proof is rechecked in both, transported -through Dedukti or re-proved, with the route recorded per theorem. -|Never attempted. This is what holds the set at Mathesis *Grade 3*: locally -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. +|`+PROOF-POLICY+` §2: every Agda theory proof is rechecked in both, by Dedukti +transport or re-proof, with the route recorded per theorem. Applies to R4a only. +|Never attempted. No `+.v+`, `+.lean+`, `+.dk+` or `+.lp+` file states a +receipt/warrant theorem, and no §2.2 correspondence record exists. +`+src/rust/exchange/+` speaks Dedukti, so the transport route exists. + +|R6. E9 "proof composition soundness, axiom conflict detection" +|`+open+` +|*Corrected 2026-11-09.* `+PROOF-NEEDS+` cited `+proofs/agda/ProofComposition.agda+`. +That file proves only list-append associativity and left identity; its header +promises consistency of a union that no theorem states. +`+SoundnessPreservation.compose-sound+` ignores its no-conflict hypothesis. +|No theorem states E9, so moving the file would not discharge it (the earlier +"cheap remedy is the move" was wrong). E9 needs stating and proving; under +§1 it names echidna's composition, so it is engineering. |=== +=== Census of theory theorems (`+PROOF-POLICY+` §8.5) + +Denominator: the ten theorems in `+Receipt.agda+`. The file has 18 top-level +proof declarations; three are inhabitation witnesses +(`+warrant-elsewhere+`, `+receipt-in-sharpened-frame+`, +`+one-passing-sample+`) and five are projections, aliases or pairings of +other results (`+postulates-name-an-axiom+`, `+discharge-postulates+`, +`+proven-in-sharpened-frame+`, `+coarse-yet-sharpened+`, +`+warrant-and-receipt+`). Those eight are not graded. + +[width="100%",cols="34%,12%,12%,14%,14%,14%",options="header"] +|=== +|Theorem |§5 token |PWG |`+foundation_diverse+` |Rocq leg |Lean leg + +|`+receipt-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+warrant-not-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+warrant-not-receipt+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+no-receipt-anywhere+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+receipt′-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+frame-receipt-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+false-sample-rejected+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+no-free-promotion+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+no-unconditional-postulate-promotion+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+no-test-promotion+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|=== + +Census: `+PWG-1+` 0/10, `+PWG-2ii+` 0/10, `+PWG-2i+` 0/10, `+PWG-3+` 0/10, +ungraded 10/10. The Agda kernel accepted all ten under the §2.1 flags, so +`+PWG-3+` is within reach, but no committed receipt yet records the import +cone together with a comment-aware postulate scan of it (§8.2, §8.4); the +in-repo receipt records file digests only, and CI relies on `+--safe+` alone. +`+PWG-3+` becomes derivable for all ten once the `+agda-meta-checker+` job +writes that receipt. No result carries `+foundation_diverse+`. + === Calibrated scores (§5 is about proof, not ranking) [width="100%",cols="24%,13%,38%,25%",options="header"] @@ -309,7 +327,7 @@ to update, so it is left as a named action rather than done silently. |Mathesis §6: "`Do not flatten proof confidence into a percentage.`" |The score ranks backends against each other and is unweighted by any receipt. It is a routing heuristic. Do not publish it as assurance and do not compare it -with a Mathesis grade. +with a Proof Witness Grade (§8). |R8. `+echidna.prove.result/1+` `+trust.confidence+` |`+open+`, correctly @@ -368,13 +386,12 @@ mean "ECHIDNA is verified" — it would mean one named obligation was discharged by one named tool with its boundary written down. Nothing here vouches for a prover backend's own soundness. -Four rows are `+proven+` today — R4, R9, R10, R11 — and each names the kernel, -the flags and the limit that qualify it (R4 carries the -`+UnsupportedIndexedMatch+` caveat, R9 the digest-level scope). Every *independent* -leg is still `+open+`: R5 has never been attempted, which is why the corpus sits -at Mathesis Grade 3 and not above it. Those two facts are not in tension — -proven in one kernel is exactly what Grade 3 means — and neither of them is an -omission. +Two rows are `+proven+` today, R2a and R4a, and each names the kernel, the +receipt and the limit that qualify it. Every other first-party obligation is +`+open+`, and most of the Rust behaviour it concerns sits in R1, waiting on a +Creusot or Verus run. The ten theory theorems are ungraded until a receipt +records the import cone and a postulate scan; they cannot rise above `+PWG-3+` +until R5's Rocq and Lean legs exist. None of this is an omission. == Related diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index 8b7ce9ac..02f1544d 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -51,7 +51,7 @@ it provides a **machine-verified guarantee** that the system's safety invariants |=== | Construct | Count -| `postulate` | 1 (funext — standard, provable in HoTT) +| `postulate` | 0 (every module is checked under `--safe`, which refuses one) | `sorry` | 0 | `believe_me` | 0 | `Admitted` | 0 diff --git a/scripts/ci/agda-cone-receipt.sh b/scripts/ci/agda-cone-receipt.sh new file mode 100755 index 00000000..e2ed4ceb --- /dev/null +++ b/scripts/ci/agda-cone-receipt.sh @@ -0,0 +1,138 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# agda-cone-receipt.sh ENTRY.agda — the PROOF-POLICY §8.2 receipt for the +# theory theorems in ENTRY: the Agda version, the standard-library pin, the +# flags in force, the import cone with a SHA-256 per file, and a +# comment-aware scan of that cone for postulates, unsafe pragmas and +# primTrustMe (§8.4). Writes one JCS object to stdout. +# +# Run from meta-checker/ after scripts/ci/check-agda.sh, in the environment +# scripts/ci/setup-agda.sh prepares (AGDA_LIBRARIES_FILE, Agda_datadir). +# AGDA_STDLIB_SHA256 names the pinned stdlib archive digest. +# +# The scan reads Agda source with nested {- -} block comments and -- line +# comments removed and {-# #-} pragmas kept. It does not lex string +# literals; a literal holding "{-" would hide text from it, and --safe is +# still the check that refuses escape hatches. The scan is the record §8.4 +# asks for, not a replacement for --safe. +# +# Postulates in the Agda data directory (Agda.Primitive's universe-level +# primitives) belong to the Agda kernel's trust base. They are listed in the +# receipt, not counted as findings. +# +# Exit codes: 0 receipt written and the scan is clean, 1 a finding outside +# the kernel's own primitives, 2 cannot run. +set -euo pipefail +export LC_ALL=C.UTF-8 + +# strip : source with comments removed and pragmas kept. +strip() { + awk ' + { line = $0; out = ""; i = 1; n = length(line) + while (i <= n) { + two = substr(line, i, 2); three = substr(line, i, 3) + if (depth == 0 && inpragma == 0 && three == "{-#") { inpragma = 1; out = out three; i += 3; continue } + if (inpragma == 1 && three == "#-}") { inpragma = 0; out = out three; i += 3; continue } + if (inpragma == 1) { out = out substr(line, i, 1); i++; continue } + if (depth == 0 && two == "--") break + if (two == "{-") { depth++; i += 2; continue } + if (depth > 0 && two == "-}") { depth--; i += 2; continue } + if (depth == 0) out = out substr(line, i, 1) + i++ + } + print out }' "$1" +} + +# scan: the escape hatches the receipt records, one "line:text" per hit. +scan() { + { strip "$1" | grep -nE '(^|[[:space:](){};])postulate($|[[:space:](){};])|\{-#[[:space:]]*(TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK|NON_COVERING)|primTrustMe' || true; } +} + +# Sourced by scripts/ci/test-agda-cone-receipt.sh for strip and scan only. +# shellcheck disable=SC2317 # exit runs only when executed rather than sourced +if [[ "${AGDA_CONE_RECEIPT_FUNCTIONS_ONLY:-}" == 1 ]]; then return 0 2>/dev/null || exit 0; fi + +entry=${1:?usage: agda-cone-receipt.sh ENTRY.agda} +flags=(--safe --without-K --cubical-compatible) +if ! command -v agda >/dev/null 2>&1 || [[ ! -f "${AGDA_LIBRARIES_FILE:-}" ]]; then + echo "agda-cone-receipt: pinned Agda setup missing" >&2; exit 2 +fi +command -v jq >/dev/null 2>&1 || { echo "agda-cone-receipt: jq missing" >&2; exit 2; } + +tmp=$(mktemp -d) +trap 'rm -rf "$tmp"' EXIT + +agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" "${flags[@]}" \ + --dependency-graph="$tmp/cone.dot" "$entry" > "$tmp/agda.log" 2>&1 \ + || { cat "$tmp/agda.log" >&2; echo "agda-cone-receipt: agda failed" >&2; exit 2; } + +data_dir=$(agda --print-agda-data-dir) +# Include roots: the Agda data directory's lib/prim, then every library's +# include directories from the library file (one .agda-lib path per line). +roots=("$data_dir/lib/prim") +while IFS= read -r lib; do + [[ -n "$lib" ]] || continue + libdir=$(dirname -- "$lib") + while IFS= read -r inc; do + roots+=("$libdir/$inc") + done < <(awk '/^include:/ { sub(/^include:[[:space:]]*/, ""); n = split($0, a, /[[:space:]]+/); for (i = 1; i <= n; i++) if (a[i] != "") print a[i] }' "$lib") +done < "$AGDA_LIBRARIES_FILE" + +# Module names from the dot file's node labels. +grep -oE 'label="[^"]+"' "$tmp/cone.dot" | sed -E 's/^label="//; s/"$//' | sort -u > "$tmp/modules" +[[ -s "$tmp/modules" ]] || { echo "agda-cone-receipt: empty dependency graph" >&2; exit 2; } + +: > "$tmp/cone.jsonl"; : > "$tmp/findings.jsonl"; : > "$tmp/kernel.jsonl" +while IFS= read -r module; do + rel="${module//.//}" + file="" + for root in "${roots[@]}"; do + for ext in agda lagda lagda.md; do + [[ -f "$root/$rel.$ext" ]] && { file="$root/$rel.$ext"; break 2; } + done + done + [[ -n "$file" ]] || { echo "agda-cone-receipt: cannot locate module $module" >&2; exit 2; } + file=$(realpath -- "$file") + case "$file" in + "$(realpath -- "$data_dir")"/*) origin=agda-kernel ;; + "$(realpath -- "$PWD")"/*) origin=first-party ;; + *) origin=library ;; + esac + digest=$(sha256sum "$file" | cut -d' ' -f1) + jq -cn --arg m "$module" --arg o "$origin" --arg d "$digest" '{module: $m, origin: $o, sha256: $d}' >> "$tmp/cone.jsonl" + scan "$file" \ + | while IFS=: read -r ln text; do + if [[ "$origin" == agda-kernel ]]; then target="$tmp/kernel.jsonl"; else target="$tmp/findings.jsonl"; fi + jq -cn --arg m "$module" --argjson l "$ln" --arg t "$text" '{module: $m, line: $l, text: ($t | gsub("^\\s+|\\s+$"; ""))}' >> "$target" + done +done < "$tmp/modules" + +commit=$(git rev-parse HEAD) +dirty=$(git status --porcelain -- . | head -1) +agda_bin=$(command -v agda) +jq -cnS \ + --arg commit "$commit" --arg dirty "${dirty:+yes}" --arg entry "$entry" \ + --arg agda "$(agda --version)" --arg agda_sha "$(sha256sum "$agda_bin" | cut -d' ' -f1)" \ + --arg stdlib_sha "${AGDA_STDLIB_SHA256:-unrecorded}" \ + --argjson flags "$(printf '%s\n' "${flags[@]}" | jq -R . | jq -s .)" \ + --slurpfile cone "$tmp/cone.jsonl" --slurpfile findings "$tmp/findings.jsonl" \ + --slurpfile kernel "$tmp/kernel.jsonl" ' + { + schema_version: 1, + kind: "agda-cone-receipt", + policy: "standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4", + source: {repository: "https://github.com/hyperpolymath/echidna", commit: $commit, + uncommitted_changes: ($dirty == "yes"), entrypoint: $entry}, + toolchain: {agda: $agda, agda_executable_sha256: $agda_sha, + stdlib_archive_sha256: $stdlib_sha, flags: $flags}, + import_cone: {count: ($cone | length), modules: $cone}, + postulate_scan: { + method: "comment-aware: nested block and line comments removed, pragmas kept; string literals not lexed", + kernel_primitives: $kernel, + findings: $findings, + result: (if ($findings | length) == 0 then "clean" else "findings" end) + } + }' +[[ ! -s "$tmp/findings.jsonl" ]] diff --git a/scripts/ci/test-agda-cone-receipt.sh b/scripts/ci/test-agda-cone-receipt.sh new file mode 100755 index 00000000..4998508f --- /dev/null +++ b/scripts/ci/test-agda-cone-receipt.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# Fixture test for the comment-aware scan in agda-cone-receipt.sh: comments +# (line, block, nested) hide nothing they should not, pragmas stay visible, +# and only the keyword `postulate` counts, not identifiers that contain it. +set -euo pipefail +here=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd) +# shellcheck source=scripts/ci/agda-cone-receipt.sh +AGDA_CONE_RECEIPT_FUNCTIONS_ONLY=1 . "$here/agda-cone-receipt.sh" +tmp=$(mktemp -d) +trap 'rm -rf "$tmp"' EXIT +cat > "$tmp/Fx.agda" <<'AGDA' +module Fx where +-- postulate in a line comment +{- postulate in a block {- nested postulate -} still comment postulate -} +x = 1 -- trailing postulate +{-# TERMINATING #-} +postulate + ax : Set +postulates-name : Set +f = primTrustMe +{-# OPTIONS --safe #-} +AGDA +got=$(scan "$tmp/Fx.agda" | cut -d: -f1 | tr '\n' ' ') +want="5 6 9 " +if [[ "$got" == "$want" ]]; then + echo "agda-cone-receipt scan: ok (hits on lines $got)" +else + echo "::error::agda-cone-receipt scan: hits on lines '$got', want '$want'" + exit 1 +fi From 4c3ea688bf19c361f6339f66f853090253df0d7b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:08:41 +0000 Subject: [PATCH 6/9] fix(proofs): name the receipt's dirty-tree flag by its scope Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- scripts/ci/agda-cone-receipt.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/ci/agda-cone-receipt.sh b/scripts/ci/agda-cone-receipt.sh index e2ed4ceb..042a4f2f 100755 --- a/scripts/ci/agda-cone-receipt.sh +++ b/scripts/ci/agda-cone-receipt.sh @@ -124,7 +124,7 @@ jq -cnS \ kind: "agda-cone-receipt", policy: "standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4", source: {repository: "https://github.com/hyperpolymath/echidna", commit: $commit, - uncommitted_changes: ($dirty == "yes"), entrypoint: $entry}, + uncommitted_changes_under_entry_dir: ($dirty == "yes"), entrypoint: $entry}, toolchain: {agda: $agda, agda_executable_sha256: $agda_sha, stdlib_archive_sha256: $stdlib_sha, flags: $flags}, import_cone: {count: ($cone | length), modules: $cone}, From c164ed2bf2f479ebed50c5d4fffc42a015f32157 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:09:42 +0000 Subject: [PATCH 7/9] docs(proofs): record the 2026-11-09 cone receipt; derive PWG-3 for the theory theorems MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/reports/2026-11-09-agda-cone-receipt.json was written by scripts/ci/agda-cone-receipt.sh at 4c3ea688, with no uncommitted change under meta-checker/: - toolchain: pinned Agda 2.7.0.1 (executable SHA-256 6de41437…) and agda-stdlib 2.1 (archive SHA-256 72ca3ea2…); - flags --safe --without-K --cubical-compatible on Receipt.agda, which the kernel accepted; - an import cone of 211 modules, each with its digest; - a clean comment-aware postulate scan. scripts/ci/check-agda.sh passed at the same commit, with 9/9 fresh interfaces. From that receipt, the census derives PWG-3 for 10/10 theory theorems. None reaches PWG-2i or above, because R5's Rocq and Lean legs do not exist. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- docs/PROOF-STATUS.adoc | 56 ++++++++++++------- .../reports/2026-11-09-agda-cone-receipt.json | 1 + 2 files changed, 37 insertions(+), 20 deletions(-) create mode 100644 docs/reports/2026-11-09-agda-cone-receipt.json diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 1290a387..072e0d63 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -296,25 +296,41 @@ other results (`+postulates-name-an-axiom+`, `+discharge-postulates+`, |=== |Theorem |§5 token |PWG |`+foundation_diverse+` |Rocq leg |Lean leg -|`+receipt-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+warrant-not-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+warrant-not-receipt+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+no-receipt-anywhere+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+receipt′-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+frame-receipt-factive+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+false-sample-rejected+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+no-free-promotion+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+no-unconditional-postulate-promotion+` |`+proven+` |ungraded |no |`+open+` |`+open+` -|`+no-test-promotion+` |`+proven+` |ungraded |no |`+open+` |`+open+` +|`+receipt-factive+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+warrant-not-factive+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+warrant-not-receipt+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+no-receipt-anywhere+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+receipt′-factive+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+frame-receipt-factive+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+false-sample-rejected+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+no-free-promotion+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+no-unconditional-postulate-promotion+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` +|`+no-test-promotion+` |`+proven+` |`+PWG-3+` |no |`+open+` |`+open+` |=== -Census: `+PWG-1+` 0/10, `+PWG-2ii+` 0/10, `+PWG-2i+` 0/10, `+PWG-3+` 0/10, -ungraded 10/10. The Agda kernel accepted all ten under the §2.1 flags, so -`+PWG-3+` is within reach, but no committed receipt yet records the import -cone together with a comment-aware postulate scan of it (§8.2, §8.4); the -in-repo receipt records file digests only, and CI relies on `+--safe+` alone. -`+PWG-3+` becomes derivable for all ten once the `+agda-meta-checker+` job -writes that receipt. No result carries `+foundation_diverse+`. +Census: `+PWG-1+` 0/10, `+PWG-2ii+` 0/10, `+PWG-2i+` 0/10, `+PWG-3+` 10/10, +ungraded 0/10. No result carries `+foundation_diverse+`. + +`+PWG-3+` is derived from the receipt +link:reports/2026-11-09-agda-cone-receipt.json[`+2026-11-09-agda-cone-receipt.json+`] +(§8.2, §8.4), written by `+scripts/ci/agda-cone-receipt.sh+`: + +* Commit `+4c3ea688+`, with no uncommitted change under `+meta-checker/+`. + The `+meta-checker/+` sources are identical to `+2ab7574+`. +* Agda 2.7.0.1, executable SHA-256 `+6de41437…+` (the repository pin), and + `+agda-stdlib+` 2.1, archive SHA-256 `+72ca3ea2…+`. +* Flags `+--safe --without-K --cubical-compatible+`, entrypoint + `+src/Echidna/Receipt.agda+`, which the kernel accepted. +* An import cone of 211 modules, each with its SHA-256: 1 first-party, 202 + from the standard library and 8 from Agda's built-in library. +* A comment-aware scan of the cone that is clean. Its only postulates are + `+Agda.Primitive+`'s universe-level primitives, which belong to the + Agda kernel's trust base. + +The `+agda-meta-checker+` job writes the same receipt on every run that +touches these sources. Any change to a cone file invalidates the grade until +a fresh receipt is recorded. The ceiling is `+PWG-3+` while R5's Rocq and +Lean legs are `+open+`. === Calibrated scores (§5 is about proof, not ranking) @@ -389,9 +405,9 @@ prover backend's own soundness. Two rows are `+proven+` today, R2a and R4a, and each names the kernel, the receipt and the limit that qualify it. Every other first-party obligation is `+open+`, and most of the Rust behaviour it concerns sits in R1, waiting on a -Creusot or Verus run. The ten theory theorems are ungraded until a receipt -records the import cone and a postulate scan; they cannot rise above `+PWG-3+` -until R5's Rocq and Lean legs exist. None of this is an omission. +Creusot or Verus run. The ten theory theorems are at `+PWG-3+`, derived from the +2026-11-09 cone receipt; they cannot rise above it until R5's Rocq and Lean +legs exist. None of this is an omission. == Related diff --git a/docs/reports/2026-11-09-agda-cone-receipt.json b/docs/reports/2026-11-09-agda-cone-receipt.json new file mode 100644 index 00000000..c0096cb3 --- /dev/null +++ b/docs/reports/2026-11-09-agda-cone-receipt.json @@ -0,0 +1 @@ +{"import_cone":{"count":211,"modules":[{"module":"Agda.Builtin.Bool","origin":"agda-kernel","sha256":"514fa25a0df7064cdb213507a0f6332c97288a52d538be3a9df06cc7001ba7f5"},{"module":"Agda.Builtin.Equality","origin":"agda-kernel","sha256":"5735edb0be7e530133814e9431d1466bb1e7892c2a4746c1a0d2a3a0dbea91cd"},{"module":"Agda.Builtin.List","origin":"agda-kernel","sha256":"387c75a65f0f14dc6268a8cf84c93b80b7139f0e90ba6d8d6d672f02c2882195"},{"module":"Agda.Builtin.Maybe","origin":"agda-kernel","sha256":"982f7f2afbfbc4ac41b6bdafddfb5e032a5ddfa71e204f39bbecc23967dc4808"},{"module":"Agda.Builtin.Nat","origin":"agda-kernel","sha256":"2e681d9dde9a39460364ee775181f31f7bcb7eba7220bd2ab8e4deb3d02d94c9"},{"module":"Agda.Builtin.Sigma","origin":"agda-kernel","sha256":"5c393f230b359032f64ff78ad693799a162dbf9cada2089048aedb4c6f669e1f"},{"module":"Agda.Builtin.Unit","origin":"agda-kernel","sha256":"03d06283f9d8005beff99fd42de38b7315aa7697099ea22fc19d060600b16249"},{"module":"Agda.Primitive","origin":"agda-kernel","sha256":"e5e4e04900cf1a28202e2ff26bb20d6fa6401fcc9f4049cd8d14fedd5bd697f8"},{"module":"Algebra","origin":"library","sha256":"68574fe8c5138702eaaeeaf8995c18fe39aee139c7c9895530362a481598aa9a"},{"module":"Algebra.Bundles","origin":"library","sha256":"4694a20f513c393d884ced2846ec7e146765d71eecd72148499ec8aa294e4b4d"},{"module":"Algebra.Bundles.Raw","origin":"library","sha256":"63e2b1366e5981632e9f641f4ba209f2bffe4763dbe4cd66a89781d1a7e0df90"},{"module":"Algebra.Consequences.Base","origin":"library","sha256":"1dd3cc76a3d268c3a08fb3a340f9eb18e911aa863afe4b50ebd87ec301a02bd9"},{"module":"Algebra.Consequences.Propositional","origin":"library","sha256":"97a782c17117835e8248ceac1fd378de2eddc4d372fe5325c90e634218fa06bb"},{"module":"Algebra.Consequences.Setoid","origin":"library","sha256":"1446934805faf31a20c401e8567a280ac41236caac784bba0730d54af7f28da1"},{"module":"Algebra.Construct.LiftedChoice","origin":"library","sha256":"cd89bfc08389e152571023dd4878f47df09f7ab4506ff51eac2938bd09d3f977"},{"module":"Algebra.Construct.NaturalChoice.Base","origin":"library","sha256":"8342e6ca3070c23738ff4256d62d4f887d6d4a3a47ebff5536b26f2d3e9f892a"},{"module":"Algebra.Construct.NaturalChoice.Max","origin":"library","sha256":"5645ae0f79adcb3d6dea0e443e295f4a2ce41685dee91591df1838104dc1ac1e"},{"module":"Algebra.Construct.NaturalChoice.MaxOp","origin":"library","sha256":"6e542ae7c407c170b74e80caa3893ba57afe3ccd56228126511186b65585a55f"},{"module":"Algebra.Construct.NaturalChoice.Min","origin":"library","sha256":"a19b2652895621f9d7296553188db05bf104dd42d3ca9e7dadb957e3ab0d6627"},{"module":"Algebra.Construct.NaturalChoice.MinMaxOp","origin":"library","sha256":"71ea1096b7d636353016a072773a1e2865f2a668e86e1c66fa2d9dfbc0d0d9b9"},{"module":"Algebra.Construct.NaturalChoice.MinOp","origin":"library","sha256":"82e7594935a144d306d9fdeb496af03c5819d8263de1a590fdb264b08ca94b42"},{"module":"Algebra.Core","origin":"library","sha256":"7e634f414b5321bdf07203c9cf0b9b767ce3c53fe910726c40f35024e166691a"},{"module":"Algebra.Definitions","origin":"library","sha256":"8060f473f8d19bd297998b4392c2782f4727163489f8cecabe13602a98051635"},{"module":"Algebra.Definitions.RawMagma","origin":"library","sha256":"b65091be0caa130b2ff5c1ffea22792787bb72262b2b6881fb3d83d269a4380d"},{"module":"Algebra.Lattice.Bundles","origin":"library","sha256":"a98d1768afc4d20e2ec6b24ad2ceca364e4459289b711ef0b029aa8e3212a8d0"},{"module":"Algebra.Lattice.Bundles.Raw","origin":"library","sha256":"ae7723213f71c2565459ba848c11925131c52c19f220719311a3b0fdc6503c84"},{"module":"Algebra.Lattice.Construct.NaturalChoice.MaxOp","origin":"library","sha256":"f741b2fffbe5bef177e9aac75c89a9fef5a64935c507f0eed68b7e0a683e820b"},{"module":"Algebra.Lattice.Construct.NaturalChoice.MinMaxOp","origin":"library","sha256":"0e46784f879fd6ed8950589f6d4ea2f2e88923fd6dbc7f08334dd3b2f9cc07cd"},{"module":"Algebra.Lattice.Construct.NaturalChoice.MinOp","origin":"library","sha256":"c1216153d8914a0650a5ce57c713dc00e4cfd71b3ec7a7f444bd9c2a03620e1e"},{"module":"Algebra.Lattice.Properties.BooleanAlgebra","origin":"library","sha256":"585134a60483b6af035c793e666c26e39383d3a65055511cbcc4cbadf28c372c"},{"module":"Algebra.Lattice.Properties.DistributiveLattice","origin":"library","sha256":"e82b816f1ee76c26c7387286631a50345732b3d3779a608af1ed260eb985cb16"},{"module":"Algebra.Lattice.Properties.Lattice","origin":"library","sha256":"315b48528ab4f83d351fd2baf11d3dccb713266ca49036ba83bf54bdfa57afc0"},{"module":"Algebra.Lattice.Properties.Semilattice","origin":"library","sha256":"c4e30b4dfc2760990837f6308e6aeb231dc6e657d2ea2e9d66661a2dacd649d8"},{"module":"Algebra.Lattice.Structures","origin":"library","sha256":"437f53700eef1f46c55bedeffc8654d3168c4279c1b22c96b51123265ed00708"},{"module":"Algebra.Morphism","origin":"library","sha256":"8a95112ecfa55c05692178ab9bfb1ae323b22fba4cb301ed7a953831921fbda8"},{"module":"Algebra.Morphism.Definitions","origin":"library","sha256":"818270682d9684729a68bac0518e2b99298f56c3fe30b067476bf45ca3b7e3f0"},{"module":"Algebra.Morphism.Structures","origin":"library","sha256":"d788089d70bdd4d75135bbca29492edaec3842abcf5fc4f9383f18fc90701266"},{"module":"Algebra.Properties.CommutativeSemigroup","origin":"library","sha256":"6790bf6e2690dbb6a9dbd8b4dc933540d4f6290962bd78995d7756857b0bbedb"},{"module":"Algebra.Properties.Group","origin":"library","sha256":"f00e1139abc3615360c4dbea4d635169116c43d123086ce85e4722ccb65e7954"},{"module":"Algebra.Properties.Loop","origin":"library","sha256":"fe2cb895f208353e8d534b4be4479bce62f9612fb33ddc8fa5087b495688341a"},{"module":"Algebra.Properties.Quasigroup","origin":"library","sha256":"7beabe5a5838eeff9cbad00947102c7950573122feebef25c198f1c46afe2a42"},{"module":"Algebra.Properties.Semigroup","origin":"library","sha256":"4251bf552a3f38fa49d9c03cba16cf9f06d0f39bea51b2a2f5bf538668cae636"},{"module":"Algebra.Structures","origin":"library","sha256":"7cbe41828a109797b463bed65a1235f4702d941b3c55d0f574977506fc660ea9"},{"module":"Algebra.Structures.Biased","origin":"library","sha256":"f0e6579adcefdd68eed3669bed1b6b4d9437a62ea5aa60396717ba8f1e1bd2d8"},{"module":"Axiom.Extensionality.Propositional","origin":"library","sha256":"fdb5f8ea6a8942e17de4be545067b5dc7ee3081a753611f3d6f0c4a3a59e595e"},{"module":"Axiom.UniquenessOfIdentityProofs","origin":"library","sha256":"3e8130b43640052d52ce67207e057bd69eb04df769634f4833bec2057a78d885"},{"module":"Data.Bool.Base","origin":"library","sha256":"124e425ebafee9cbe8fb496b4c8467fdd372b0961ca03e445bfda506738204f6"},{"module":"Data.Bool.Properties","origin":"library","sha256":"1398693823e0edbe7f2506cc0923787fc36c49d37e68d7baa223ce845eb640ad"},{"module":"Data.Empty","origin":"library","sha256":"3a68a9e529c13054202a3892bfcf961bb75db2dc11d63f068189c4cbd48c2cd2"},{"module":"Data.Empty.Polymorphic","origin":"library","sha256":"2b8e9b1b5ad7b7d4c10b95553a96b897b2d3e6957dc1ee75f7cb8ab9fd43008a"},{"module":"Data.Fin.Base","origin":"library","sha256":"684b3764d445b4017bfbe34740198908a7d800e6abca15e38d50c7645ff704e4"},{"module":"Data.Fin.Patterns","origin":"library","sha256":"543640fa272d7d6363d3b3f0524dd5fb8c60133927d4962411629b6ac86ec2de"},{"module":"Data.Fin.Properties","origin":"library","sha256":"144e64dddd37f2bba0f6f207fdb62ba31fef1adb6292eac54770ed1003078771"},{"module":"Data.Irrelevant","origin":"library","sha256":"5f225770f471847144eb3908fecb1d4b0a06e7d7b1cb3a12bdebd840bf17a783"},{"module":"Data.List.Base","origin":"library","sha256":"d8149ac2eb98f05d9d8ddcbffa799bf26b3081edb734c5b7c0cf521ea52ced97"},{"module":"Data.List.Effectful","origin":"library","sha256":"169244f8a8a7e058bb7d5d76f77c2cf0b60539af85730843aeace899cbed37a2"},{"module":"Data.List.Extrema","origin":"library","sha256":"e177981547d339231dcd10d10c5739179d10f2685043f38e771046f740a038e9"},{"module":"Data.List.Extrema.Core","origin":"library","sha256":"d94c99fe03d45344867070f8cbaec3396c9bc623b66c4154127d1d17c9474ab2"},{"module":"Data.List.Membership.Propositional","origin":"library","sha256":"4f40d3237e3f85cb4165a0dc4622a99b964403db2463165a5c277134bcdaee10"},{"module":"Data.List.Membership.Propositional.Properties","origin":"library","sha256":"3a5c7f7aae22171961d1b028f41cd6c3a673c38a215f288f67450d217a762a90"},{"module":"Data.List.Membership.Propositional.Properties.Core","origin":"library","sha256":"f71b07e94dafb2aafd0e3deb2a7092e1e9697f039fff6c200fe6a5ad14c0b352"},{"module":"Data.List.Membership.Setoid","origin":"library","sha256":"9d15100ce32a99263f87ac66490f0826045cb163f04905bfe4076c0f38ebf373"},{"module":"Data.List.Membership.Setoid.Properties","origin":"library","sha256":"937d8518680da216f3aadde070f58fb7789df451ab9040bffdd8a5d84e3daf86"},{"module":"Data.List.Properties","origin":"library","sha256":"bb93f278aaad99dadb311bc8bad7a987594c48da412995221640c1788167d8e9"},{"module":"Data.List.Relation.Binary.Equality.Propositional","origin":"library","sha256":"5fe88f05ba8f6dd6236692949f21935663f3ab5fb7710ff76f30bca383a8a7f1"},{"module":"Data.List.Relation.Binary.Equality.Setoid","origin":"library","sha256":"44788ba07985593a5f491cb859f75c7dbec2d9bdd48435393b91d63a16a3980c"},{"module":"Data.List.Relation.Binary.Pointwise","origin":"library","sha256":"ccb0a9863bb037d1c02ce8e2eab900ce0cc14d5ede28c4fcf2157909499b5088"},{"module":"Data.List.Relation.Binary.Pointwise.Base","origin":"library","sha256":"9397d4e3340a178f8e8eb39f0d3d635047c590e3e56a9965b9346caaa48b9150"},{"module":"Data.List.Relation.Binary.Pointwise.Properties","origin":"library","sha256":"6749b77fb75551b2d8543a795ed130dc7772409dd1cce9e3c8b8d534242f0c01"},{"module":"Data.List.Relation.Binary.Subset.Propositional","origin":"library","sha256":"d4dc33e2ad8f9411f4c898a3f87279b814b7a32462987296183220a31ef2f5d4"},{"module":"Data.List.Relation.Binary.Subset.Setoid","origin":"library","sha256":"1442b2de2d6aefa3a3f3081377191ef48341f5b2aad295a685b8dfe78f0a4f64"},{"module":"Data.List.Relation.Unary.All","origin":"library","sha256":"a20287dd2f08aebfe5275130aef43c80f2dc67fd799797b4cf591ffc1eba911e"},{"module":"Data.List.Relation.Unary.All.Properties","origin":"library","sha256":"500345f52292b5fb4e183a7fa61eeba4921de5406fda8be7fae9d8a48d93c1b3"},{"module":"Data.List.Relation.Unary.AllPairs","origin":"library","sha256":"199353c7f1fea606d1172cab175da06e630bd0857ab39c343631a5b77f42d6e4"},{"module":"Data.List.Relation.Unary.AllPairs.Core","origin":"library","sha256":"7973bfc87cc4d5437cec13968245f84cd2d1ed904041f73c89fe00bfd2363af5"},{"module":"Data.List.Relation.Unary.Any","origin":"library","sha256":"4a5fd2d3e611db9dd899a24c4780d32b054fe7f826ddab0c7d3943264358bcbd"},{"module":"Data.List.Relation.Unary.Any.Properties","origin":"library","sha256":"1d2025158c384501ae9525e831925916f7dc245d2bca70fd511e198e7298d8eb"},{"module":"Data.List.Relation.Unary.Unique.Setoid","origin":"library","sha256":"bee725c98909dca4de6f0011ce76ba5f11be3fbfc81d452c9078e1fe5d3e96fc"},{"module":"Data.Maybe.Base","origin":"library","sha256":"bc28af0cccc19abd81f14e07bbb252a446d097c5a3be47c577dc459926b97c07"},{"module":"Data.Maybe.Relation.Unary.All","origin":"library","sha256":"e11263b6fc8ebf455811cae444b063bd0cd1a224d43533c1f41466752d687bde"},{"module":"Data.Maybe.Relation.Unary.Any","origin":"library","sha256":"d13a5bf5f3e86e587dae439bcc37e25f74842b944ef38525bcec40c0ca440a5e"},{"module":"Data.Nat","origin":"library","sha256":"4f947b8db93635abe0c3b9df82dac8663b38bdb6b19fc7129e2e98a9d49e60ea"},{"module":"Data.Nat.Base","origin":"library","sha256":"0d730c3d8a344c6a38b39ade22bc134f776c1de3e4afef4ec459a65a9814163d"},{"module":"Data.Nat.DivMod","origin":"library","sha256":"fc0e0f1aec03f92f40d1414736db28bb187763ac6c088a3d4249aef866bcf5cd"},{"module":"Data.Nat.DivMod.Core","origin":"library","sha256":"54890eace6f970b6809b4d54f48096ae80430f68cc899fe612eeb3a8950982d4"},{"module":"Data.Nat.Divisibility","origin":"library","sha256":"e0ef5d67aa955922e6cf638ea70b0588e0a658ec6df22dd92d9dd2c8c7ae8224"},{"module":"Data.Nat.Divisibility.Core","origin":"library","sha256":"327dc4a32d56b31b3e7f4300e4e854469055531b36f5cedf96e3376230a1ba67"},{"module":"Data.Nat.GeneralisedArithmetic","origin":"library","sha256":"fa4d41a3b14e0c7128bc3a1ad18eb19891d7610702ea89733f24d127de82f2e9"},{"module":"Data.Nat.Induction","origin":"library","sha256":"b768ba2a504ee3286612227b73e45ff4f1d92f5e6c4845577f1f5710e736741d"},{"module":"Data.Nat.Properties","origin":"library","sha256":"f68418e88255e207050e24d3f5fc5af13af4e0e9a44cf3f9b0586e95853c82f1"},{"module":"Data.Parity.Base","origin":"library","sha256":"93d9ab9884c5e2f419bdd9b2c3d98bdca11381475e8ce473783a0d73af679b17"},{"module":"Data.Product","origin":"library","sha256":"4af8b364f025b3e90991717e6fc03547c11588e88ebd776346ef90c7f83fb6ee"},{"module":"Data.Product.Algebra","origin":"library","sha256":"aa9c82d46e5fafe6bb9a1229ded9fda0c97a21697bd3dd3868a7cacc00d536dc"},{"module":"Data.Product.Base","origin":"library","sha256":"e2585b0cc6d0c2486cf1f30bd98a3855b00666e8aa8bc0aee5be8253c952a99c"},{"module":"Data.Product.Function.Dependent.Propositional","origin":"library","sha256":"006a6ed0c7d8df5898bb4acdd305fa79d7962bfbeef75e85391865c7ab71607f"},{"module":"Data.Product.Function.NonDependent.Propositional","origin":"library","sha256":"8dc88c4e65a53f93e65165b06d568d58c081b29830aa4afcbdb06ba5762b389d"},{"module":"Data.Product.Function.NonDependent.Setoid","origin":"library","sha256":"fb864f70bc1826d4b7913e244876726418267d4287e4af6398e691244b0a5571"},{"module":"Data.Product.Properties","origin":"library","sha256":"ba3d82fb3204913126f44ed57fc2a5819d267c8255f67c0f3f464b80eb909c46"},{"module":"Data.Product.Relation.Binary.Pointwise.NonDependent","origin":"library","sha256":"9ef9124ce289748a9a0367369cc53201f87703fa69cfcbd1d690ddcc57260e0f"},{"module":"Data.Product.Relation.Unary.All","origin":"library","sha256":"e7b8db12b0b07f25a4d4f9c867865c5fc1105700197d92d88cb6db96033da008"},{"module":"Data.Sign.Base","origin":"library","sha256":"6743e6b68e4746d73a3cdf0f0df48d55209ef3e8634af8275de81510e37e2996"},{"module":"Data.Sum","origin":"library","sha256":"7d5827fbbf0c998bbfa905fcaf1ba19e61db25fa578d13e6454c0e15dc67f675"},{"module":"Data.Sum.Algebra","origin":"library","sha256":"195846faf01c4745a4c574b9fbca3107883233b9f8fd46a0ea1272053d58a836"},{"module":"Data.Sum.Base","origin":"library","sha256":"2733ba66eaed94cc0f0b21f2a9ed0533f8a31b5bd487e40384632f1d6204fcfd"},{"module":"Data.Sum.Function.Propositional","origin":"library","sha256":"9f6d3668607fcc5d058e8a23dfc55e817e3e602640ab707082ba6ec40527eeb9"},{"module":"Data.Sum.Function.Setoid","origin":"library","sha256":"6c0163c61256a482d7654210abc32d92e96ce8c0f74bc604838c94a6d8459c10"},{"module":"Data.Sum.Properties","origin":"library","sha256":"003840fe29a2b4061d27c02fe45cfbc2c0491964aa500b01bc083fd550a1a4eb"},{"module":"Data.Sum.Relation.Binary.Pointwise","origin":"library","sha256":"b5e7cba494eb2906049c2d67e652f71fb2e9939be70b25090e5a5444bc0becec"},{"module":"Data.These.Base","origin":"library","sha256":"7f2d088485b960b9ec36cf1923e7b8f07eeb0c57c3fb58e4d05f5e437de84031"},{"module":"Data.Unit","origin":"library","sha256":"320fc4c784fbb6ad847f41ae317f60da346002a119cbca178b2caaa787c2b26c"},{"module":"Data.Unit.Base","origin":"library","sha256":"38cc799f18b6f106336ace8ae66c5a171251c0eb3b6bf32124e33c45d441b2fb"},{"module":"Data.Unit.Polymorphic","origin":"library","sha256":"59060da4fa9b4d71d50ca1330662ff93f691c9b0e606b4a7f6ed9ab58ec6d9b0"},{"module":"Data.Unit.Polymorphic.Base","origin":"library","sha256":"002ae814be1dafd6f6c4193a2254ee19f7793ffef7dcf1d29f9794db0b19f2a8"},{"module":"Data.Unit.Polymorphic.Properties","origin":"library","sha256":"dddc5bdea96be1c01e2952b104c2a04405d2367d6f74f1c104311d05dc12569d"},{"module":"Data.Unit.Properties","origin":"library","sha256":"bb9a390596f27739aa9d9c46ef666e42917df4f5000f675ef1042abe3fe2fc62"},{"module":"Data.Vec","origin":"library","sha256":"79fd35e68ccb8722d3bead8259961ff58fff4b7e9b60a95dc3daa6cb54bad567"},{"module":"Data.Vec.Base","origin":"library","sha256":"73e1151d72d0a4c43496e86bb840ff4f69304c4813a22835937f6017f9accc2e"},{"module":"Data.Vec.Bounded.Base","origin":"library","sha256":"8469f114552ea6ddbb3ef5c0ce3d538a304afd1ae0fbbd54e129891eeff25d2d"},{"module":"Data.Vec.Membership.Propositional","origin":"library","sha256":"14d130719a6b78dcabe1fb18e022a9029f257e2cab8536f284e8fdfdaacf4c61"},{"module":"Data.Vec.Membership.Setoid","origin":"library","sha256":"8ae75229b11fc0f660013833427b9f76f419213417d02b77d832e45b771988a3"},{"module":"Data.Vec.Relation.Unary.All","origin":"library","sha256":"747d8ed58dab65dbbd897cc100156bf6006457cff23a3d46d2ee187fba0f4b84"},{"module":"Data.Vec.Relation.Unary.Any","origin":"library","sha256":"08ffde09605128b3a79a1121e83924d3ee563067d93e231805285c63e50e50be"},{"module":"Echidna.Receipt","origin":"first-party","sha256":"6741bae9360b0b3064ef67b073c06f2831775b70eeb01e1d6e998bc74f02c6e2"},{"module":"Effect.Applicative","origin":"library","sha256":"329c5a59e13bb7449d4fc096a2be47563d53a7082a8ebe81f2b1c61062892d1a"},{"module":"Effect.Choice","origin":"library","sha256":"dc42c9aa4feadfeb76377fdfe1cd1fe5c94830aa941bf88986b11333e4b521ca"},{"module":"Effect.Empty","origin":"library","sha256":"9adc04cbc9b02109047f4f04ed440659d65c766a7b652cd5f6c0af5519d9f8c2"},{"module":"Effect.Functor","origin":"library","sha256":"45fd600321ef1272d2979b3dd85467b91b17630ce69bdbe0e9059381d1c495b4"},{"module":"Effect.Monad","origin":"library","sha256":"dd3b60f2e84fb9ffbfd5053d30caa041ab9749b38c637713b3cad8c477be72bf"},{"module":"Function.Base","origin":"library","sha256":"b021bf843c1974a5d50a1a3362f2d6447018629331a3dc2bb0d9ea85ec029e84"},{"module":"Function.Bundles","origin":"library","sha256":"10a990323e8128199017fe5bfe1ead05a2c18cd3e441b47d6903ef1ec96cfa66"},{"module":"Function.Consequences","origin":"library","sha256":"5cb682d31dc4340e805074791971c6a1dfb49b9d9c931d3e2a9fd2b53b27c11d"},{"module":"Function.Consequences.Propositional","origin":"library","sha256":"8789e6dbfb50651eb93390cb938f8be825c704ffbac99b585810b379308a7702"},{"module":"Function.Consequences.Setoid","origin":"library","sha256":"3ebed8b4ab2d51527e98a3fa50927b5ee75d2a429ecaea4401f7d5e8e38bfb51"},{"module":"Function.Construct.Composition","origin":"library","sha256":"c1caf4f975f57948be134c6fbd1a4b08a933bf2eadfb00ba0645c163302552bd"},{"module":"Function.Construct.Identity","origin":"library","sha256":"afbc000aafc7ef4a2d9a8a431cceaf87d565310d654d60af65f573f04faaba48"},{"module":"Function.Construct.Symmetry","origin":"library","sha256":"e42e0277b255b56a19eefcc7754505de81af865e8aaf7873c10f3e8bec4f0bb9"},{"module":"Function.Core","origin":"library","sha256":"306e35bc28d015d0c3807bde740d1070d79a606c4df81e3d2f67690367958fb0"},{"module":"Function.Definitions","origin":"library","sha256":"6ce79a18384fdae5e01210d1a75a0b4e76004bb07b61024fdc8c5f0cdee17ee5"},{"module":"Function.Dependent.Bundles","origin":"library","sha256":"75bd0bfe77b56a5f1e419c911394dbb18ea395df59560a35d4eab4e8363afdee"},{"module":"Function.Indexed.Relation.Binary.Equality","origin":"library","sha256":"5a9207f7b734362802621b6e58ca763becc510cc8c21f3fee1936d019264d2de"},{"module":"Function.Metric.Bundles","origin":"library","sha256":"e9be9de709f21375d874245cf1812f964abc98cc0f4893e46ec34360296b8160"},{"module":"Function.Metric.Core","origin":"library","sha256":"77fbc11ef41b2d0902505dae9ff9d18b9b09cf1a47e0525acd43c57911463e24"},{"module":"Function.Metric.Definitions","origin":"library","sha256":"4fd018bd96f6ba92a338916b536605987d715a149a509ce2351883d47cc726e1"},{"module":"Function.Metric.Nat","origin":"library","sha256":"2d2938867367ca5fefc0449ebe8b7aafd7149dfac8f98ce81a24238fc8b7a5de"},{"module":"Function.Metric.Nat.Bundles","origin":"library","sha256":"be03a9ea8596b75c7cdffb0e839b314bcc4a258054346ef48414bbf3ac25350d"},{"module":"Function.Metric.Nat.Core","origin":"library","sha256":"d53ba974cdf065994ec1035ef88049b6c411aa8521291076ddd229b61e008d4a"},{"module":"Function.Metric.Nat.Definitions","origin":"library","sha256":"358c5ab7adfb0a87300647be0c706f34ae6a6b4c540b1394cf5620b82eca9171"},{"module":"Function.Metric.Nat.Structures","origin":"library","sha256":"09cbfd1026d06d914d211b9fd77787ac0fd86d0b0bab98743ca72d8d12e6e5e8"},{"module":"Function.Metric.Structures","origin":"library","sha256":"6fc2c084b6d38a88cc800abb935335fb475931636b071db78a0d4a9de30f7ce4"},{"module":"Function.Properties.Bijection","origin":"library","sha256":"a970f070c861154784b4edb6bbeea0f859d93553a50f859dee8a4f7439d17565"},{"module":"Function.Properties.Inverse","origin":"library","sha256":"e0ec3e0ed86cc551a501b20c81312963bf0602fa232054c1b0ff1415edf97d09"},{"module":"Function.Properties.Inverse.HalfAdjointEquivalence","origin":"library","sha256":"94e285d8f62a8fc4810d4ff918f69aac51c5711bc89b75228ce45e33f82b477c"},{"module":"Function.Properties.RightInverse","origin":"library","sha256":"07210f0a8c381f69ef78075d25c6abb281c1ad22f5733e7aaf1f8ebd1ec41062"},{"module":"Function.Properties.Surjection","origin":"library","sha256":"5f98ec8208937948df2c9e31a8d95b7464959c077ff3b35bd2f94ed855c01581"},{"module":"Function.Related.Propositional","origin":"library","sha256":"6ab8ab57b90c9d75f038d25eb27542fff81aaa17e87995f1b3eb5773e2bf96c4"},{"module":"Function.Related.TypeIsomorphisms","origin":"library","sha256":"600690000a6e5ce57fb756587bd512f06ea3bb4a3ef64d9d51349ab13ac8522a"},{"module":"Function.Structures","origin":"library","sha256":"c84e2367ab099bbf55662e537fa6fec597a2fe56393d28e2beade67271e89091"},{"module":"Induction","origin":"library","sha256":"4638093055dc290aa9ad7bd128ac2bed705f00a02f98eb1a390d173b5472aaee"},{"module":"Induction.WellFounded","origin":"library","sha256":"ec6d272aafaf25d841813233833c17f9b62e063fc81d8afbde6851924e461943"},{"module":"Level","origin":"library","sha256":"1168f8373370c10aec0f20bae0cc43db9a34331a49deb4c72efd2574a638a278"},{"module":"Relation.Binary","origin":"library","sha256":"0aafa1229fd4093c924e19f6d64e518a998f352d725af856d4342f3ecd5b0b7d"},{"module":"Relation.Binary.Bundles","origin":"library","sha256":"fd4b0a832bf9f372d2739668c7e0988e0242519686b69616dc67043923ad88c3"},{"module":"Relation.Binary.Consequences","origin":"library","sha256":"d5f1d178492b9e485a3efdcb16dd18fe623896371e2cae3662d8fde1ff94a455"},{"module":"Relation.Binary.Construct.Composition","origin":"library","sha256":"829ca14501f085b08a0504a61c7874cd20cce07ffc883027ef3465e4f44cf347"},{"module":"Relation.Binary.Construct.Flip.EqAndOrd","origin":"library","sha256":"2ac3cd0c1dfec3cb7470f638172c6c4a0c37492ac7625faebe88d8081aed5576"},{"module":"Relation.Binary.Construct.Intersection","origin":"library","sha256":"8dce90a37b1086e18a5844a373ecba240c3740bce099ca2cb1798db734c59d3e"},{"module":"Relation.Binary.Construct.NaturalOrder.Left","origin":"library","sha256":"ecd11c100db5128f1e5a80dcbf365dc5791fdbb6282d189044ca98e1ca945b87"},{"module":"Relation.Binary.Construct.NonStrictToStrict","origin":"library","sha256":"15701c27241a2c7d182cb8c4cbb677196921a995a9fae11a9b4f1f6b494f2d40"},{"module":"Relation.Binary.Construct.On","origin":"library","sha256":"dc3e20ecea3052a02a56229073806bd421e9afdd51d410daee5b8ba43edcd965"},{"module":"Relation.Binary.Core","origin":"library","sha256":"09eda35f4c2f795542f0a2468ade41793e9c9e07889553989e03d343902fcb81"},{"module":"Relation.Binary.Definitions","origin":"library","sha256":"c61495efb42702588229a67461c451dd660bd5d686c244ee1895b9d563547783"},{"module":"Relation.Binary.Indexed.Heterogeneous","origin":"library","sha256":"31fea63ecce5f5f63e13e667a04bd4062f2bfafd9d8215514144e6c28d5b813f"},{"module":"Relation.Binary.Indexed.Heterogeneous.Bundles","origin":"library","sha256":"91210765ebc0293ad041007a0703d93f70d127bdcb045aefeb5e208d1e8b3c06"},{"module":"Relation.Binary.Indexed.Heterogeneous.Construct.Trivial","origin":"library","sha256":"bad2cb0132c973b728690a6467c70bb97aec0aec748eeb7e40a5a640cad45624"},{"module":"Relation.Binary.Indexed.Heterogeneous.Core","origin":"library","sha256":"623b155a1a393ffba78cc893cfba7ce55fec3d49b0ddcd56940b3bd811c28205"},{"module":"Relation.Binary.Indexed.Heterogeneous.Definitions","origin":"library","sha256":"997789408b78b154c81039248354a53dba1c8bcfb873f95636c2dea566089faf"},{"module":"Relation.Binary.Indexed.Heterogeneous.Structures","origin":"library","sha256":"8c48074820f087b9cc507cf7a7db9134f98094a8d82cbc5d391f4ed6e0a7ef84"},{"module":"Relation.Binary.Lattice","origin":"library","sha256":"fd16f6140ae748bb42d2427b8616699d3189d7c2833d2c9d4a968780dae05c26"},{"module":"Relation.Binary.Lattice.Bundles","origin":"library","sha256":"6cdddaed92e07bb7ba4ee39d5e529729c396dcbe3c0f64c469e1ae6d3fa268a9"},{"module":"Relation.Binary.Lattice.Definitions","origin":"library","sha256":"93e0469e47b8ac5bf976432ac83844fcde6e72b71a31cc5700ca1eb595760ce2"},{"module":"Relation.Binary.Lattice.Structures","origin":"library","sha256":"3ab1e5fedbad8cfae67bb5e9dfe012da8c3a4855ae7008ea193e82ec1548bcb5"},{"module":"Relation.Binary.Morphism.Definitions","origin":"library","sha256":"c85beed5112ece49ef091767ce2f8c70581e079bcb2a58d07d18ca06f1389f54"},{"module":"Relation.Binary.Morphism.Structures","origin":"library","sha256":"8aa178e3a7593274250db79c716b4380a458b925f928f234fdb1242b6ad8ef30"},{"module":"Relation.Binary.Properties.DecTotalOrder","origin":"library","sha256":"9410bdcd82e3e7757c1aeac5ae8cad77907ef71d7f5fc7d18695a8cf1b09a657"},{"module":"Relation.Binary.Properties.Poset","origin":"library","sha256":"27eae427096c8eb26d25feb2a5f6053ac210f63d44b09f04c4f71ecc45dbb805"},{"module":"Relation.Binary.Properties.Preorder","origin":"library","sha256":"33eacd3ad2d59770a6dd7fc151a7dd51d4d78c0bb0a7617f90dce7701ae9190e"},{"module":"Relation.Binary.Properties.Setoid","origin":"library","sha256":"ba05a90fbede6b120c7aefe56944f0c5c772f908a1f60d1644ec4c70c9a93293"},{"module":"Relation.Binary.Properties.TotalOrder","origin":"library","sha256":"4043bd7493adbb40e52b432e00c48c07c54d2574c0997bfeb8989e8b764e6f05"},{"module":"Relation.Binary.PropositionalEquality","origin":"library","sha256":"e854dcea3dd081440fecf39ae9124ef1695607f232fd2452a896a1d3cc64e645"},{"module":"Relation.Binary.PropositionalEquality.Algebra","origin":"library","sha256":"7575a469a6bb49a210266444989693340209c015ee28c49a4627ee63895ed46c"},{"module":"Relation.Binary.PropositionalEquality.Core","origin":"library","sha256":"480da0675a0d8ddddcae5c4f74c5526a5da88790fef387aa8b8213dabf842200"},{"module":"Relation.Binary.PropositionalEquality.Properties","origin":"library","sha256":"4ed071c430e9244d3be9b9ca847d74232826c0fed7bf3035da0a6d4a8c7b2137"},{"module":"Relation.Binary.Reasoning.Base.Double","origin":"library","sha256":"11dd426aff0ac8176e6ce929075985c97b2b291c4081d8a7e4620bf6b3489bb3"},{"module":"Relation.Binary.Reasoning.Base.Single","origin":"library","sha256":"489173b58679a1df8b584ca5b86bc392ab9dcbaff40c0c596d9ae952cb935c1b"},{"module":"Relation.Binary.Reasoning.Base.Triple","origin":"library","sha256":"2b4a8f6a4e390a16a48c2c9d14f1fde4b6d861f9dad82d4b144f9a6e74d43e16"},{"module":"Relation.Binary.Reasoning.Preorder","origin":"library","sha256":"82eb3f11d5df9160a068f07a7285c86183875d7df43c373145ea7aaccb3d3f38"},{"module":"Relation.Binary.Reasoning.Setoid","origin":"library","sha256":"9c5553d148470d809a3986b5f1377de6acaca1a45b39df2165d8e0d288fa5049"},{"module":"Relation.Binary.Reasoning.Syntax","origin":"library","sha256":"a7a831d62ed2a3c7d5d0f29521162fbf264d34a48b6c91e9ac9f6168c2067ceb"},{"module":"Relation.Binary.Structures","origin":"library","sha256":"12ccbc4bd7da510ed8edf17018eb10b3d827e08ba1842a623c3370c2cb6ef396"},{"module":"Relation.Binary.Structures.Biased","origin":"library","sha256":"2178213579d5821d3a67fdde7600c32dacd571d1a57c82dc76504e42a814219f"},{"module":"Relation.Nullary","origin":"library","sha256":"56f7f4a54b8d655b0c90dacfd65d29cfc2d7e73d8666bd30a934ae25818a5019"},{"module":"Relation.Nullary.Decidable","origin":"library","sha256":"51c4e7dd26928e770380a6d1b7e01418fd1ab2575f80cf7aaf6db4e49f6947d0"},{"module":"Relation.Nullary.Decidable.Core","origin":"library","sha256":"0082f72e3d2bd247d56d46abf3f70936a08d32c69c3a18cb68f744c8fefb67b8"},{"module":"Relation.Nullary.Indexed","origin":"library","sha256":"fc2ab3ff0e19e4fdc124959c3c1d3a659411100a5b673f5602858cb98b1c8947"},{"module":"Relation.Nullary.Negation","origin":"library","sha256":"2a13db6c365bd54a4d82306dd1fd13b8192539e49dc873ccb1ac5159d6c1b28f"},{"module":"Relation.Nullary.Negation.Core","origin":"library","sha256":"b848e89c226674f8462c9c5aced87e5aa3fe03fdf9cbaffd0c28e9f87ff6c910"},{"module":"Relation.Nullary.Recomputable","origin":"library","sha256":"cacf1a1d98ceed1571bac2ca9a3c1f9967ea6c91fd0dc0ed35b5fc74657b7ce0"},{"module":"Relation.Nullary.Reflects","origin":"library","sha256":"73ec20b5e43a3903b68b994cd0815b9d0c3dcc9e57dae39b4d8b487904a7eea1"},{"module":"Relation.Unary","origin":"library","sha256":"4960f1b9004f19834cbc0271b80a64281a99ba715ffa125f73df80f205745a71"},{"module":"Relation.Unary.PredicateTransformer","origin":"library","sha256":"0d542136370cd7917163dc62278ad7df0e66c0e1c4426e590dbff78ea1b462aa"},{"module":"Relation.Unary.Properties","origin":"library","sha256":"98196ae2887abd71ff2ee3120418e6549dd21792048e431a11e2026169eb0d24"}]},"kind":"agda-cone-receipt","policy":"standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4","postulate_scan":{"findings":[],"kernel_primitives":[{"line":26,"module":"Agda.Primitive","text":"postulate"},{"line":34,"module":"Agda.Primitive","text":"postulate"}],"method":"comment-aware: nested block and line comments removed, pragmas kept; string literals not lexed","result":"clean"},"schema_version":1,"source":{"commit":"4c3ea688bf19c361f6339f66f853090253df0d7b","entrypoint":"src/Echidna/Receipt.agda","repository":"https://github.com/hyperpolymath/echidna","uncommitted_changes_under_entry_dir":false},"toolchain":{"agda":"Agda version 2.7.0.1","agda_executable_sha256":"6de41437c14c05c9fe576d724cc67386444c0fa9fee662a08250fefb91bee8b6","flags":["--safe","--without-K","--cubical-compatible"],"stdlib_archive_sha256":"72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431"}} From 3c70abb52f5e91cf826c508b0ea4d9a4018443c4 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:53:13 +0000 Subject: [PATCH 8/9] fix(fuzz): pass small_kernel_confirmations in the trust fuzz target; assert TK-4/TK-5 The fuzz crate is outside the workspace, so the new TrustFactors field was missed there and the OSS-Fuzz "PR (address)" build failed (E0063). The field is now fuzzed independently, so inconsistent inputs (more small-kernel confirmations than confirmations) are covered too. The target now also asserts the kernel contracts on every input: TK-4 (level >= 4 needs a small kernel and a produced, verified certificate) and TK-5 (level 5 needs two small-kernel confirmations). Checked with `cargo check --manifest-path fuzz/Cargo.toml --bins` (stable 1.99). It was not run under cargo-fuzz: no nightly toolchain here. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- fuzz/fuzz_targets/fuzz_trust_pipeline.rs | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/fuzz/fuzz_targets/fuzz_trust_pipeline.rs b/fuzz/fuzz_targets/fuzz_trust_pipeline.rs index 5263669f..76cb493e 100644 --- a/fuzz/fuzz_targets/fuzz_trust_pipeline.rs +++ b/fuzz/fuzz_targets/fuzz_trust_pipeline.rs @@ -36,6 +36,10 @@ struct FuzzTrustFactors { use_small_kernel: bool, /// Number of independent provers that confirmed the result. confirming_provers: u32, + /// How many of those confirmations came from small-kernel provers. + /// Fuzzed independently, so inconsistent inputs (more small-kernel + /// confirmations than confirmations) are exercised as well. + small_kernel_confirmations: u32, /// Whether a proof certificate was produced. has_certificate: bool, /// Whether the certificate was independently verified. @@ -69,6 +73,7 @@ fuzz_target!(|fuzz: FuzzTrustFactors| { let factors = TrustFactors { prover, confirming_provers: fuzz.confirming_provers, + small_kernel_confirmations: fuzz.small_kernel_confirmations, has_certificate: fuzz.has_certificate, certificate_verified: fuzz.certificate_verified, worst_axiom_danger: index_to_danger(fuzz.worst_axiom_danger_index), @@ -89,6 +94,24 @@ fuzz_target!(|fuzz: FuzzTrustFactors| { "compute_trust_level returned out-of-range value {value} for factors {factors:?}" ); + // TK-4: level 4 or above needs a small-kernel prover and a certificate + // that was both produced and verified. + if value >= 4 { + assert!( + fuzz.use_small_kernel && fuzz.has_certificate && fuzz.certificate_verified, + "TK-4 violated: level {value} without small kernel and verified certificate: {factors:?}" + ); + } + + // TK-5: level 5 needs two small-kernel confirmations, which can never + // exceed the confirming provers. + if value == 5 { + assert!( + fuzz.small_kernel_confirmations >= 2 && fuzz.confirming_provers >= 2, + "TK-5 violated: level 5 with fewer than two small-kernel confirmations: {factors:?}" + ); + } + // Exercise the description and Display impls while we have a live value. let _ = level.description(); let _ = level.to_string(); From 3301b420cbd461bdd9d7a12f5114ad49e4315977 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:05:31 +0000 Subject: [PATCH 9/9] ci(agda): run the meta-checker on pushes that change only the receipt scripts The `push` path filter `scripts/ci/*agda.sh` matches neither agda-cone-receipt.sh nor test-agda-cone-receipt.sh. A push to main that changes only the receipt tooling therefore skipped the workflow, even though the in-job detector counts those files as relevant (Codex P2 on this PR). Both scripts are now listed explicitly. actionlint 1.7.7 is clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- .github/workflows/agda-meta-checker.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/agda-meta-checker.yml b/.github/workflows/agda-meta-checker.yml index 5a1f6efc..271dcea8 100644 --- a/.github/workflows/agda-meta-checker.yml +++ b/.github/workflows/agda-meta-checker.yml @@ -15,6 +15,8 @@ on: - 'meta-checker/**' - 'scripts/ci/*agda.sh' - 'scripts/ci/check-receipt-controls.sh' + - 'scripts/ci/agda-cone-receipt.sh' + - 'scripts/ci/test-agda-cone-receipt.sh' - '.github/workflows/agda-meta-checker.yml' # No paths-filter on pull_request: this is a REQUIRED status check, so it must # report on every PR (a path-filtered required check deadlocks PRs that don't