diff --git a/.github/workflows/agda-meta-checker.yml b/.github/workflows/agda-meta-checker.yml index 301110dc..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 @@ -55,7 +57,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 +87,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/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/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]] 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/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/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 9aa00127..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+` @@ -92,10 +94,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..072e0d63 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,224 +62,275 @@ 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. |=== -=== Idris 2 — APIs, ABIs, engineering properties (§1) +*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 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. -`+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). +=== Idris 2 — APIs, ABIs, engineering properties (§1) [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) -|`+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 +|R4a. Theory: receipt vs warrant, `+meta-checker/src/Echidna/Receipt.agda+` |`+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+` |`+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+` 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) @@ -292,7 +343,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 @@ -351,13 +402,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 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"}} 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(); 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..042a4f2f --- /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_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}, + 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 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/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"); } } } 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/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(); 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