diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 465dfc81..4c26a3ba 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,27 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Fixed — one trust kernel; Level 4 and Level 5 conditions, 2026-11-09 + +* `+compute_trust_level+` now exists once, in `+echidna-core-creusot+` +(`+echidna_core::trust+`). `+verification::confidence+` re-exports its +`+TrustLevel+` and delegates to it instead of keeping a second copy. +* *Level 4* now needs a produced certificate (`+has_certificate+`) as well +as a verified one. A result with `+certificate_verified+` but no certificate +used to score Level 4. +* *Level 5* now needs two or more small-kernel systems that checked a +certificate. It used to check only the producing prover's kernel class, so +one small-kernel prover plus an SMT confirmer scored Level 5. +* `+TrustFactors+` gains `+small_kernel_confirmations+`, the number of +confirming provers that are small-kernel systems with a verified certificate, +the producing prover included. It defaults to 0 (`+#[serde(default)]+`), so +callers that cannot vouch for their confirmers never reach Level 5. The +shipped dispatch paths set it to 0, as they already reported no certificate. +* Contracts TK-4/TK-5 are stated on the kernel and checked exhaustively over +a finite input space by the crate's tests (`+tested-only+`; the Creusot run +is still open). The Idris 2 `+TrustKernelMonotonicity+` model, which proved +the old Level 5 rule, is retired. + ==== Changed — GraphQL listener default, 2026-11-04 * `+echidna-graphql+` now defaults to `+127.0.0.1:8082+`, avoiding the diff --git a/benches/proof_benchmarks.rs b/benches/proof_benchmarks.rs index 38e35aa1..d58ba8ce 100644 --- a/benches/proof_benchmarks.rs +++ b/benches/proof_benchmarks.rs @@ -149,6 +149,7 @@ fn bench_trust_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Lean, confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -161,6 +162,7 @@ fn bench_trust_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -173,6 +175,7 @@ fn bench_trust_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Lean, confirming_provers: 2, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, diff --git a/benches/routing_benchmarks.rs b/benches/routing_benchmarks.rs index b7ada9d6..66cecba8 100644 --- a/benches/routing_benchmarks.rs +++ b/benches/routing_benchmarks.rs @@ -125,6 +125,7 @@ fn bench_trust_level_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -137,6 +138,7 @@ fn bench_trust_level_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Lean, confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -149,6 +151,7 @@ fn bench_trust_level_computation(c: &mut Criterion) { TrustFactors { prover: ProverKind::Z3, confirming_provers: 5, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, diff --git a/crates/echidna-core-creusot/src/lib.rs b/crates/echidna-core-creusot/src/lib.rs index d9560c6b..bab6d51b 100644 --- a/crates/echidna-core-creusot/src/lib.rs +++ b/crates/echidna-core-creusot/src/lib.rs @@ -211,6 +211,14 @@ pub struct TrustFactors { pub prover_class: ProverClass, /// Number of independent provers that agree on this result. pub confirming_provers: u32, + /// How many of the `confirming_provers` are small-kernel systems whose + /// certificate for this result was independently verified, the producing + /// prover included. Level 5 needs at least two. `confirming_provers` + /// alone cannot decide that, because it does not say what kind of system + /// each confirmer is. Defaults to 0, so data written before this field + /// existed can never reach Level 5. + #[serde(default)] + pub small_kernel_confirmations: u32, /// Whether a proof certificate was produced. pub has_certificate: bool, /// Whether the certificate was independently verified. @@ -295,23 +303,44 @@ pub fn clamp_trust(level: TrustLevel, min_level: TrustLevel, max_level: TrustLev /// ### Creusot contracts /// ```text /// #[requires(true)] -/// #[ensures( -/// factors.worst_axiom_danger == DangerLevel::Reject -/// ==> result == TrustLevel::Level1 -/// )] -/// #[ensures( -/// !factors.solver_integrity_ok -/// ==> result == TrustLevel::Level1 -/// )] -/// #[ensures(result >= TrustLevel::Level1)] -/// #[ensures(result <= TrustLevel::Level5)] +/// #[ensures(factors.worst_axiom_danger == DangerLevel::Reject ==> result == TrustLevel::Level1)] +/// #[ensures(factors.worst_axiom_danger == DangerLevel::Warning ==> result == TrustLevel::Level1)] +/// #[ensures(!factors.solver_integrity_ok ==> result == TrustLevel::Level1)] +/// // TK-4: Level 4 and above need a small kernel AND a produced, verified certificate. +/// #[ensures(result >= TrustLevel::Level4 ==> +/// factors.prover_class == ProverClass::SmallKernel +/// && factors.has_certificate && factors.certificate_verified)] +/// // TK-5: Level 5 needs two or more small-kernel systems that checked a certificate. +/// #[ensures(result == TrustLevel::Level5 ==> +/// factors.small_kernel_confirmations >= 2 && factors.confirming_provers >= 2)] +/// #[ensures(result >= TrustLevel::Level1 && result <= TrustLevel::Level5)] /// ``` +/// +/// TK-4 and TK-5 close two defects in the earlier rule. Level 4 used to fire +/// on `certificate_verified` without `has_certificate`. Level 5 used to check +/// only the producing prover's kernel class, never the confirmers'. Both +/// are checked exhaustively over a finite input space by +/// `impl_invariants::tk_*`, which run on stable Rust in CI. The Creusot +/// annotations are stated, not yet discharged (see the crate header). #[cfg_attr(feature = "creusot", ensures( factors.worst_axiom_danger == DangerLevel::Reject ==> result == TrustLevel::Level1 ), + ensures( + factors.worst_axiom_danger == DangerLevel::Warning + ==> result == TrustLevel::Level1 + ), ensures(!factors.solver_integrity_ok ==> result == TrustLevel::Level1), + ensures( + result >= TrustLevel::Level4 + ==> (factors.prover_class == ProverClass::SmallKernel + && factors.has_certificate && factors.certificate_verified) + ), + ensures( + result == TrustLevel::Level5 + ==> (factors.small_kernel_confirmations >= 2u32 && factors.confirming_provers >= 2u32) + ), ensures(result >= TrustLevel::Level1 && result <= TrustLevel::Level5) )] pub fn compute_trust_level(factors: &TrustFactors) -> TrustLevel { @@ -339,19 +368,30 @@ pub fn compute_trust_level(factors: &TrustFactors) -> TrustLevel { } let is_small_kernel = factors.prover_class == ProverClass::SmallKernel; + // A certificate counts only when one was produced AND it was verified; + // a verification flag on a result with no certificate carries nothing. + let certified = factors.has_certificate && factors.certificate_verified; + // Small-kernel confirmations can never exceed the confirming provers; + // an inconsistent input is read at the lower count. + let small_kernel_confirmations = + if factors.small_kernel_confirmations < factors.confirming_provers { + factors.small_kernel_confirmations + } else { + factors.confirming_provers + }; - // --- Level 5: two or more small-kernel systems cross-check with certs --- - if factors.confirming_provers >= 2 && factors.certificate_verified && is_small_kernel { + // --- Level 5: two or more small-kernel systems checked a certificate --- + if certified && is_small_kernel && small_kernel_confirmations >= 2 { return TrustLevel::Level5; } - // --- Level 4: single small-kernel system with verified certificate --- - if is_small_kernel && factors.certificate_verified { + // --- Level 4: small-kernel system with a produced, verified certificate --- + if certified && is_small_kernel { return TrustLevel::Level4; } - // --- Level 3: any prover with verified certificate --- - if factors.has_certificate && factors.certificate_verified { + // --- Level 3: any prover with a produced, verified certificate --- + if certified { return TrustLevel::Level3; } @@ -494,6 +534,7 @@ pub mod impl_invariants { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 10, // maximum cross-checking + small_kernel_confirmations: 10, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, @@ -517,6 +558,7 @@ pub mod impl_invariants { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 5, + small_kernel_confirmations: 5, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -579,6 +621,136 @@ pub mod impl_invariants { assert!(TrustLevel::Level4.value() < TrustLevel::Level5.value()); } + // ----------------------------------------------------------------------- + // TK-4 / TK-5: the certificate and kernel conditions of Levels 4 and 5, + // checked over every input in a finite space (bounded model check). + // ----------------------------------------------------------------------- + + /// Every `TrustFactors` with counts in `0..=4`, both certificate flags, + /// every danger level, both integrity states and every prover class. + #[cfg(test)] + fn all_factors() -> Vec { + use crate::axiom_tracker::DangerLevel::{Noted, Reject, Safe, Warning}; + let mut out = Vec::new(); + for pc in [ + ProverClass::SmallKernel, + ProverClass::SmtOrAtp, + ProverClass::Other, + ] { + for confirming_provers in 0u32..=4 { + for small_kernel_confirmations in 0u32..=4 { + for has_certificate in [false, true] { + for certificate_verified in [false, true] { + for worst_axiom_danger in [Safe, Noted, Warning, Reject] { + for solver_integrity_ok in [false, true] { + out.push(TrustFactors { + prover_class: pc, + confirming_provers, + small_kernel_confirmations, + has_certificate, + certificate_verified, + worst_axiom_danger, + solver_integrity_ok, + }); + } + } + } + } + } + } + } + out + } + + /// **TK-4** Level 4 and above need a small-kernel prover with a + /// certificate that was both produced and verified. + #[test] + fn tk4_level4_needs_small_kernel_and_produced_verified_certificate() { + for f in all_factors() { + if compute_trust_level(&f) >= TrustLevel::Level4 { + assert!( + f.prover_class == ProverClass::SmallKernel + && f.has_certificate + && f.certificate_verified, + "TK-4 violated by {f:?}" + ); + } + } + } + + /// **TK-5** Level 5 needs two or more small-kernel systems that checked a + /// certificate, and two or more confirming provers. + #[test] + fn tk5_level5_needs_two_small_kernel_confirmations() { + for f in all_factors() { + if compute_trust_level(&f) == TrustLevel::Level5 { + assert!( + f.small_kernel_confirmations >= 2 && f.confirming_provers >= 2, + "TK-5 violated by {f:?}" + ); + } + } + } + + /// **TK-6** Monotone in the evidence: one more confirming prover, one more + /// small-kernel confirmation, or a produced and verified certificate + /// never lowers the level. + #[test] + fn tk6_more_evidence_never_lowers_trust() { + for f in all_factors() { + let base = compute_trust_level(&f); + let more_provers = TrustFactors { + confirming_provers: f.confirming_provers + 1, + ..f.clone() + }; + let more_kernels = TrustFactors { + confirming_provers: f.confirming_provers + 1, + small_kernel_confirmations: f.small_kernel_confirmations + 1, + ..f.clone() + }; + let certified = TrustFactors { + has_certificate: true, + certificate_verified: true, + ..f.clone() + }; + for g in [more_provers, more_kernels, certified] { + assert!( + compute_trust_level(&g) >= base, + "TK-6: {g:?} scored below {f:?}" + ); + } + } + } + + /// Regression: the two defects found in the 2026-11-09 proof audit. + #[test] + fn tk_regressions_for_the_audited_defects() { + use crate::axiom_tracker::DangerLevel::Safe; + // Level 5 from one small-kernel prover plus an SMT confirmer: the old + // rule saw only the producing prover's class and returned Level5. + let one_kernel = TrustFactors { + prover_class: ProverClass::SmallKernel, + confirming_provers: 2, + small_kernel_confirmations: 1, + has_certificate: true, + certificate_verified: true, + worst_axiom_danger: Safe, + solver_integrity_ok: true, + }; + assert_eq!(compute_trust_level(&one_kernel), TrustLevel::Level4); + // Level 4 without a produced certificate: the old rule returned Level4. + let no_certificate = TrustFactors { + prover_class: ProverClass::SmallKernel, + confirming_provers: 1, + small_kernel_confirmations: 1, + has_certificate: false, + certificate_verified: true, + worst_axiom_danger: Safe, + solver_integrity_ok: true, + }; + assert_eq!(compute_trust_level(&no_certificate), TrustLevel::Level2); + } + // ----------------------------------------------------------------------- // Property: compute_trust_level output is always in [Level1, Level5] // ----------------------------------------------------------------------- @@ -604,6 +776,7 @@ pub mod impl_invariants { let f = TrustFactors { prover_class: pc, confirming_provers: confirming, + small_kernel_confirmations: confirming, has_certificate: certs, certificate_verified: certs, worst_axiom_danger: dl, @@ -632,6 +805,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 2, + small_kernel_confirmations: 2, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -645,6 +819,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -658,6 +833,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmtOrAtp, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -671,6 +847,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmtOrAtp, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -685,6 +862,7 @@ mod tests { let factors = TrustFactors { prover_class: ProverClass::SmallKernel, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Noted, diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index d36f2149..34bed899 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -96,10 +96,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 a95f3601..c318766a 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -106,6 +106,23 @@ shipped code. *Verus:* not started; no Verus specification or proof exists. Row stays `+open+` until a Creusot or Verus run on shipped code yields a receipt with a commit hash. +*Trust kernel (2026-11-09).* `+compute_trust_level+` exists once, in +`+crates/echidna-core-creusot+`; `+src/rust/verification/confidence.rs+` +re-exports its `+TrustLevel+` and delegates to it. Two defects found by the +2026-11-09 proof audit are fixed at that source: Level 4 fired on +`+certificate_verified+` without `+has_certificate+`, and Level 5 checked only +the producing prover's kernel class. The new contracts are TK-4 (Level 4 and +above need a small kernel and a produced, verified certificate) and TK-5 +(Level 5 needs two or more small-kernel confirmations, the new +`+small_kernel_confirmations+` input). They are `+tested-only+`: +`+impl_invariants::tk4_*+`, `+tk5_*+` and `+tk6_*+` (monotone in the +evidence) check every input with counts 0..=4. That covers every case only +because the rule reads counts through `+>= 2+` and a minimum, which is +argued, not mechanised. The Creusot annotations are stated, not discharged. +Verus (§1.2) has not been applied yet; its scope is the same TK obligations +on the same function. The Idris 2 `+TrustKernelMonotonicity+` model, which +proved the defective Level 5 rule, is retired. + |=== === Idris 2 — APIs, ABIs, engineering properties (§1) diff --git a/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/src/rust/dispatch.rs b/src/rust/dispatch.rs index e04894cd..49229511 100644 --- a/src/rust/dispatch.rs +++ b/src/rust/dispatch.rs @@ -664,6 +664,7 @@ impl ProverDispatcher { let trust_factors = TrustFactors { prover: prover_kind, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: worst_danger, @@ -872,6 +873,7 @@ impl ProverDispatcher { let trust_factors = TrustFactors { prover: primary_prover, confirming_provers: confirming_count, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: worst_danger, @@ -1022,6 +1024,7 @@ impl ProverDispatcher { let trust_factors = TrustFactors { prover: winning_kind, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: worst_danger, diff --git a/src/rust/verification/confidence.rs b/src/rust/verification/confidence.rs index 60c3d80f..895399be 100644 --- a/src/rust/verification/confidence.rs +++ b/src/rust/verification/confidence.rs @@ -15,44 +15,13 @@ use super::axiom_tracker::DangerLevel; use super::portfolio::PortfolioConfidence; use crate::provers::ProverKind; -/// Trust level for a proof result (5-level hierarchy) -#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] -pub enum TrustLevel { - /// Large-TCB system, unchecked result, or uses dangerous axioms - Level1 = 1, - /// Single prover result without certificate, but no dangerous axioms - Level2 = 2, - /// Single prover with proof certificate (Alethe, DRAT/LRAT) - Level3 = 3, - /// Checked by small-kernel system (Lean4, Coq, Isabelle) with proof certificate - Level4 = 4, - /// Cross-checked by 2+ independent small-kernel systems with certificates - Level5 = 5, -} - -impl TrustLevel { - /// Human-readable description - pub fn description(&self) -> &str { - match self { - TrustLevel::Level1 => "Minimal trust: large-TCB, unchecked, or dangerous axioms", - TrustLevel::Level2 => "Basic trust: single prover, no dangerous axioms", - TrustLevel::Level3 => "Moderate trust: single prover with proof certificate", - TrustLevel::Level4 => "High trust: small-kernel prover with certificate", - TrustLevel::Level5 => "Maximum trust: cross-checked by 2+ small-kernel systems", - } - } - - /// Numeric value (1-5) - pub fn value(&self) -> u8 { - *self as u8 - } -} - -impl std::fmt::Display for TrustLevel { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "Level {} ({})", self.value(), self.description()) - } -} +/// Trust level for a proof result (5-level hierarchy). +/// +/// There is one trust kernel: this type and [`compute_trust_level`] come +/// from `echidna-core` (`echidna_core::trust`, the Creusot-annotated crate). +/// This module keeps the `ProverKind`-shaped [`TrustFactors`] that dispatch +/// builds, and maps them onto the kernel's input. +pub use echidna_core::trust::TrustLevel; /// Input factors for computing trust level #[derive(Debug, Clone, Serialize, Deserialize)] @@ -61,6 +30,13 @@ pub struct TrustFactors { pub prover: ProverKind, /// Number of independent provers that agree pub confirming_provers: u32, + /// How many of the `confirming_provers` are small-kernel systems whose + /// certificate for this result was independently verified, the producing + /// prover included. Level 5 needs at least two. Defaults to 0, so a + /// caller that cannot vouch for its confirmers' kernels never reaches + /// Level 5. + #[serde(default)] + pub small_kernel_confirmations: u32, /// Whether a proof certificate was produced pub has_certificate: bool, /// Whether the certificate was independently verified @@ -73,47 +49,36 @@ pub struct TrustFactors { pub portfolio_confidence: Option, } -/// Compute the trust level for a proof result +/// Compute the trust level for a proof result. +/// +/// Delegates to the single kernel, `echidna_core::trust::compute_trust_level`, +/// after mapping the prover to its kernel class and the axiom danger level +/// to the kernel's enum. The kernel's contracts (TK-4: Level 4 and above +/// need a small kernel and a produced, verified certificate; TK-5: Level 5 +/// needs two or more small-kernel confirmations) hold here because there is +/// no second implementation to drift from. pub fn compute_trust_level(factors: &TrustFactors) -> TrustLevel { - // Reject-level axioms always result in Level 1 - if factors.worst_axiom_danger == DangerLevel::Reject { - return TrustLevel::Level1; - } - - // Warning-level axioms cap at Level 1 - if factors.worst_axiom_danger == DangerLevel::Warning { - return TrustLevel::Level1; - } - - // Failed integrity check caps at Level 1 - if !factors.solver_integrity_ok { - return TrustLevel::Level1; - } - - let is_small_kernel = is_small_kernel_prover(factors.prover); - - // Level 5: Cross-checked by 2+ small-kernel systems with certificates - if factors.confirming_provers >= 2 && factors.certificate_verified && is_small_kernel { - return TrustLevel::Level5; - } - - // Level 4: Small-kernel prover with verified certificate - if is_small_kernel && factors.certificate_verified { - return TrustLevel::Level4; - } - - // Level 3: Any prover with verified certificate - if factors.has_certificate && factors.certificate_verified { - return TrustLevel::Level3; - } - - // Level 3: Cross-checked without certificate - if factors.confirming_provers >= 2 { - return TrustLevel::Level3; - } - - // Level 2: Single prover, no dangerous axioms (already checked above) - TrustLevel::Level2 + use echidna_core::trust::{axiom_tracker::DangerLevel as KernelDanger, ProverClass}; + let prover_class = if is_small_kernel_prover(factors.prover) { + ProverClass::SmallKernel + } else { + ProverClass::Other + }; + let worst_axiom_danger = match factors.worst_axiom_danger { + DangerLevel::Safe => KernelDanger::Safe, + DangerLevel::Noted => KernelDanger::Noted, + DangerLevel::Warning => KernelDanger::Warning, + DangerLevel::Reject => KernelDanger::Reject, + }; + echidna_core::trust::compute_trust_level(&echidna_core::trust::TrustFactors { + prover_class, + confirming_provers: factors.confirming_provers, + small_kernel_confirmations: factors.small_kernel_confirmations, + has_certificate: factors.has_certificate, + certificate_verified: factors.certificate_verified, + worst_axiom_danger, + solver_integrity_ok: factors.solver_integrity_ok, + }) } /// Whether a prover has a small trusted computing base (kernel) @@ -150,6 +115,7 @@ mod tests { TrustFactors { prover, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -163,6 +129,7 @@ mod tests { let factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: 2, + small_kernel_confirmations: 2, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -173,11 +140,58 @@ mod tests { assert_eq!(compute_trust_level(&factors), TrustLevel::Level5); } + /// One small-kernel prover plus a confirmer that is not a small-kernel + /// system with a checked certificate is not Level 5 (audit 2026-11-09). + #[test] + fn test_one_small_kernel_confirmation_is_not_level5() { + let factors = TrustFactors { + prover: ProverKind::Lean, + confirming_provers: 2, + small_kernel_confirmations: 1, + has_certificate: true, + certificate_verified: true, + worst_axiom_danger: DangerLevel::Safe, + solver_integrity_ok: true, + portfolio_confidence: Some(PortfolioConfidence::CrossChecked), + }; + + assert_eq!(compute_trust_level(&factors), TrustLevel::Level4); + } + + /// A verified flag with no certificate produced is not Level 4 + /// (audit 2026-11-09). + #[test] + fn test_verified_flag_without_certificate_is_not_level4() { + let mut factors = make_factors(ProverKind::Lean); + factors.certificate_verified = true; + assert_eq!(compute_trust_level(&factors), TrustLevel::Level2); + } + + /// The kernel's notion of a small kernel is `is_small_kernel_prover`. + #[test] + fn test_small_kernel_class_follows_is_small_kernel_prover() { + for prover in [ + ProverKind::Lean, + ProverKind::Coq, + ProverKind::Z3, + ProverKind::CVC5, + ] { + let factors = TrustFactors { + has_certificate: true, + certificate_verified: true, + ..make_factors(prover) + }; + let level4 = compute_trust_level(&factors) == TrustLevel::Level4; + assert_eq!(level4, is_small_kernel_prover(prover), "{prover:?}"); + } + } + #[test] fn test_lean_with_cert_level4() { let factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -193,6 +207,7 @@ mod tests { let factors = TrustFactors { prover: ProverKind::CVC5, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, diff --git a/tests/aspect_tests.rs b/tests/aspect_tests.rs index 5375fd35..5e025552 100644 --- a/tests/aspect_tests.rs +++ b/tests/aspect_tests.rs @@ -65,6 +65,7 @@ fn aspect_security_malicious_input_no_high_trust() { let trust = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, confirming_provers: 10, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, @@ -447,6 +448,7 @@ fn aspect_trust_computation_deterministic() { let factors = TrustFactors { prover: ProverKind::Z3, confirming_provers: 2, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Noted, diff --git a/tests/concurrency_test.rs b/tests/concurrency_test.rs index 747d2c5e..b60dfa7c 100644 --- a/tests/concurrency_test.rs +++ b/tests/concurrency_test.rs @@ -187,6 +187,7 @@ async fn concurrency_trust_level_computation_thread_safe() { let factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, diff --git a/tests/e2e_prover_test.rs b/tests/e2e_prover_test.rs index 1a03c72d..990c6000 100644 --- a/tests/e2e_prover_test.rs +++ b/tests/e2e_prover_test.rs @@ -114,6 +114,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l5 = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, // small-kernel prover confirming_provers: 3, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -127,6 +128,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l4 = compute_trust_level(&TrustFactors { prover: ProverKind::Z3, confirming_provers: 2, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -140,6 +142,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l3 = compute_trust_level(&TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Safe, @@ -151,6 +154,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l2 = compute_trust_level(&TrustFactors { prover: ProverKind::Z3, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -162,6 +166,7 @@ fn e2e_trust_pipeline_all_levels_ordered() { let l1 = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, confirming_provers: 1, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Warning, @@ -212,6 +217,7 @@ fn e2e_reject_axiom_prevents_high_trust() { let trust = compute_trust_level(&TrustFactors { prover: ProverKind::Lean, confirming_provers: 5, + small_kernel_confirmations: 0, has_certificate: true, certificate_verified: true, worst_axiom_danger: DangerLevel::Reject, // unsound construct diff --git a/tests/neural_property_tests.rs b/tests/neural_property_tests.rs index 5b380c97..1c46b86a 100644 --- a/tests/neural_property_tests.rs +++ b/tests/neural_property_tests.rs @@ -129,6 +129,7 @@ proptest! { let base_factors = TrustFactors { prover: ProverKind::Z3, confirming_provers: base_count, + small_kernel_confirmations: 0, has_certificate: false, certificate_verified: false, worst_axiom_danger: DangerLevel::Safe, @@ -137,6 +138,7 @@ proptest! { }; let more_factors = TrustFactors { confirming_provers: base_count + extra, + small_kernel_confirmations: 0, ..base_factors.clone() }; let base_trust = compute_trust_level(&base_factors); @@ -157,6 +159,7 @@ proptest! { let safe_factors = TrustFactors { prover: ProverKind::Lean, confirming_provers: confirming, + small_kernel_confirmations: 0, has_certificate: has_cert, certificate_verified: has_cert, worst_axiom_danger: DangerLevel::Safe, diff --git a/tests/p2p_property_tests.rs b/tests/p2p_property_tests.rs index 552fadbf..cd19fce6 100644 --- a/tests/p2p_property_tests.rs +++ b/tests/p2p_property_tests.rs @@ -115,6 +115,7 @@ fn arb_trust_factors_with_danger(danger: DangerLevel) -> impl Strategy --- --- TrustKernelMonotonicity.idr --- --- Stage 8a meta-proof: Trust-Kernel Monotonicity. --- --- Proves that the confidence engine's downgrade rules are monotone: --- --- trustMono_reject : worst_danger = Reject → compute_trust = Level1 --- trustMono_warning : worst_danger = Warning → compute_trust = Level1 --- trustMono_integrity: solver_integrity_ok = False → compute_trust = Level1 --- trustMono_level5_conditions : confirming ≥ 2 ∧ certificate_verified = True --- ∧ small_kernel = True → compute_trust ≥ Level4 --- --- Models TrustFactors as a record over the booleans and DangerLevel fields --- that drive the Rust compute_trust_level function. --- Models compute_trust_level exactly from confidence.rs lines 77-116. --- All proofs by exhaustive case analysis. Zero believe-me. - -module TrustKernelMonotonicity - -import Data.Nat -import NatLte - -%default total - --- ========================================================================== --- Section 1: DangerLevel --- ========================================================================== - -||| Mirrors DangerLevel from axiom_tracker.rs. -||| The derive(PartialOrd, Ord) on the Rust side gives Safe < Noted < Warning < Reject -||| (matching declaration order). We do not need the full order here — only -||| equality tests used by compute_trust_level. -public export -data DangerLevel = Safe | Noted | Warning | Reject - --- ========================================================================== --- Section 2: TrustLevel (5-element ordered type) --- ========================================================================== - -||| 5-element trust hierarchy from confidence.rs. -||| Level1 < Level2 < Level3 < Level4 < Level5. -public export -data TrustLevel - = Level1 -- 1: dangerous axiom / bad integrity / rejected - | Level2 -- 2: single prover, no dangerous axioms - | Level3 -- 3: certificate present and verified, or cross-checked - | Level4 -- 4: small-kernel prover with verified certificate - | Level5 -- 5: cross-checked by 2+ small-kernel provers with certs - -||| Numeric encoding of TrustLevel (1–5). -public export -trustValue : TrustLevel -> Nat -trustValue Level1 = 1 -trustValue Level2 = 2 -trustValue Level3 = 3 -trustValue Level4 = 4 -trustValue Level5 = 5 - --- ========================================================================== --- Section 3: TrustLevel ordering --- ========================================================================== - -||| Ordering on TrustLevel encoded via trustValue LTE. -public export -TrustLTE : TrustLevel -> TrustLevel -> Type -TrustLTE a b = trustValue a `LTE` trustValue b - --- Convenience constructor aliases used in proofs below. - -trustLTE_refl : (t : TrustLevel) -> TrustLTE t t -trustLTE_refl Level1 = lteLit 1 1 -trustLTE_refl Level2 = lteLit 2 2 -trustLTE_refl Level3 = lteLit 3 3 -trustLTE_refl Level4 = lteLit 4 4 -trustLTE_refl Level5 = lteLit 5 5 - -||| Level4 ≤ Level4 and Level4 ≤ Level5: both satisfy ≥ Level4. -||| Bodies use lteLit (machine-checked); level4LTELevel5 previously mis-counted -||| as LTE 5 5 instead of LTE 4 5. -level4LTELevel4 : TrustLTE Level4 Level4 -level4LTELevel4 = lteLit 4 4 - -level4LTELevel5 : TrustLTE Level4 Level5 -level4LTELevel5 = lteLit 4 5 - --- ========================================================================== --- Section 4: TrustFactors record --- ========================================================================== - -||| Abstracted TrustFactors record carrying only the fields that -||| determine which branch of compute_trust_level fires. -||| -||| We drop `prover : ProverKind` and fold is_small_kernel into a -||| boolean flag `small_kernel`, which is the only property of the -||| prover that compute_trust_level queries. -||| We drop `portfolio_confidence` and `has_certificate` beyond their -||| influence on certificate_verified, matching the code structure. -public export -record TrustFactors where - constructor MkTrustFactors - confirming_provers : Nat - certificate_verified : Bool - worst_axiom_danger : DangerLevel - solver_integrity_ok : Bool - small_kernel : Bool - --- ========================================================================== --- Section 5: compute_trust_level (Idris2 model of confidence.rs) --- ========================================================================== - -||| Direct transcription of compute_trust_level (confidence.rs lines 77-116). -||| -||| Branch order is preserved exactly: -||| 1. worst_axiom_danger = Reject → Level1 -||| 2. worst_axiom_danger = Warning → Level1 -||| 3. solver_integrity_ok = False → Level1 -||| 4. confirming ≥ 2 ∧ cert_verified ∧ small_kernel → Level5 -||| 5. small_kernel ∧ cert_verified → Level4 -||| 6. cert_verified → Level3 -||| 7. confirming ≥ 2 → Level3 -||| 8. (default) → Level2 -public export -computeTrustLevel : TrustFactors -> TrustLevel -computeTrustLevel f = - case f.worst_axiom_danger of - Reject => Level1 - Warning => Level1 - _ => - case f.solver_integrity_ok of - False => Level1 - True => - case (f.confirming_provers >= 2, f.certificate_verified, f.small_kernel) of - (True, True, True) => Level5 - (_, True, True) => Level4 - (_, True, False) => Level3 - (True, False, _) => Level3 - _ => Level2 - --- ========================================================================== --- Section 6: Downgrade proofs --- ========================================================================== - -||| trustMono_reject: worst_danger = Reject → compute_trust = Level1. -||| -||| Proof: computeTrustLevel pattern-matches on worst_axiom_danger first; -||| the Reject branch immediately returns Level1 regardless of all other fields. -public export -trustMono_reject - : (f : TrustFactors) - -> f.worst_axiom_danger = Reject - -> computeTrustLevel f = Level1 -trustMono_reject (MkTrustFactors _ _ Reject _ _) Refl = Refl -trustMono_reject (MkTrustFactors _ _ Safe _ _) Refl impossible -trustMono_reject (MkTrustFactors _ _ Noted _ _) Refl impossible -trustMono_reject (MkTrustFactors _ _ Warning _ _) Refl impossible - -||| trustMono_warning: worst_danger = Warning → compute_trust = Level1. -||| -||| Proof: the Warning branch fires immediately after Reject, returning Level1. -public export -trustMono_warning - : (f : TrustFactors) - -> f.worst_axiom_danger = Warning - -> computeTrustLevel f = Level1 -trustMono_warning (MkTrustFactors _ _ Warning _ _) Refl = Refl -trustMono_warning (MkTrustFactors _ _ Safe _ _) Refl impossible -trustMono_warning (MkTrustFactors _ _ Noted _ _) Refl impossible -trustMono_warning (MkTrustFactors _ _ Reject _ _) Refl impossible - --- ========================================================================== --- Section 7: Integrity downgrade --- ========================================================================== - -||| A witness that the solver integrity check failed. -||| We use a named record to carry the proof cleanly. -public export -data BadIntegrity : TrustFactors -> Type where - ||| The solver_integrity_ok field is False. - MkBadIntegrity - : (f : TrustFactors) - -> f.solver_integrity_ok = False - -> BadIntegrity f - -||| trustMono_integrity: BadIntegrity f → compute_trust = Level1. -||| -||| Proof: we case-split on worst_axiom_danger. For Reject and Warning the -||| result is Level1 independently (earlier branches fire). For Safe and -||| Noted we reach the solver_integrity_ok = False branch which returns Level1. -public export -trustMono_integrity - : (f : TrustFactors) - -> BadIntegrity f - -> computeTrustLevel f = Level1 -trustMono_integrity (MkTrustFactors _ _ Reject False _) (MkBadIntegrity _ Refl) = Refl -trustMono_integrity (MkTrustFactors _ _ Warning False _) (MkBadIntegrity _ Refl) = Refl -trustMono_integrity (MkTrustFactors _ _ Safe False _) (MkBadIntegrity _ Refl) = Refl -trustMono_integrity (MkTrustFactors _ _ Noted False _) (MkBadIntegrity _ Refl) = Refl --- solver_integrity_ok = True contradicts the BadIntegrity witness: -trustMono_integrity (MkTrustFactors _ _ Reject True _) (MkBadIntegrity _ Refl) impossible -trustMono_integrity (MkTrustFactors _ _ Warning True _) (MkBadIntegrity _ Refl) impossible -trustMono_integrity (MkTrustFactors _ _ Safe True _) (MkBadIntegrity _ Refl) impossible -trustMono_integrity (MkTrustFactors _ _ Noted True _) (MkBadIntegrity _ Refl) impossible - --- ========================================================================== --- Section 8: Level5 sufficient conditions --- ========================================================================== - -||| trustMono_level5_conditions: -||| confirming ≥ 2 ∧ certificate_verified = True ∧ small_kernel = True -||| → compute_trust ≥ Level4. -||| -||| In fact under these conditions compute_trust = Level5, so we prove the -||| equality first and derive ≥ Level4 as a corollary. -||| -||| Proof: we case-split on worst_axiom_danger and solver_integrity_ok. -||| The only dangerous-axiom paths (Reject, Warning) return Level1, which -||| contradicts the Level5 hypothesis — but since we are proving the -||| implication in the SAFE direction (the precondition is the clean case), -||| we can restrict attention to worst_axiom_danger ∈ {Safe, Noted} -||| combined with solver_integrity_ok = True. In that regime, the first -||| inner case fires (True, True, True) → Level5. - -||| Helper: under clean conditions the Level5 branch fires. -public export -trustMono_level5_exact - : (n : Nat) - -> (n >= 2 = True) - -> (danger : DangerLevel) - -> Either (danger = Safe) (danger = Noted) - -> computeTrustLevel (MkTrustFactors n True danger True True) = Level5 -trustMono_level5_exact n hge Safe (Left Refl) with (n >= 2) - trustMono_level5_exact n hge Safe (Left Refl) | True = Refl - trustMono_level5_exact n _ Safe (Left Refl) | False impossible -trustMono_level5_exact n hge Noted (Right Refl) with (n >= 2) - trustMono_level5_exact n hge Noted (Right Refl) | True = Refl - trustMono_level5_exact n _ Noted (Right Refl) | False impossible -trustMono_level5_exact _ _ Reject (Left Refl) impossible -trustMono_level5_exact _ _ Reject (Right Refl) impossible -trustMono_level5_exact _ _ Warning (Left Refl) impossible -trustMono_level5_exact _ _ Warning (Right Refl) impossible - -||| The corollary: under the clean triple-condition the result is ≥ Level4. -||| Since Level5 ≥ Level4 (trustValue Level5 = 5 ≥ 4 = trustValue Level4). -public export -trustMono_level5_conditions - : (n : Nat) - -> (n >= 2 = True) - -> (danger : DangerLevel) - -> Either (danger = Safe) (danger = Noted) - -> TrustLTE Level4 - (computeTrustLevel (MkTrustFactors n True danger True True)) -trustMono_level5_conditions n hge Safe (Left Refl) with (n >= 2) - trustMono_level5_conditions n hge Safe (Left Refl) | True = level4LTELevel5 - trustMono_level5_conditions n _ Safe (Left Refl) | False impossible -trustMono_level5_conditions n hge Noted (Right Refl) with (n >= 2) - trustMono_level5_conditions n hge Noted (Right Refl) | True = level4LTELevel5 - trustMono_level5_conditions n _ Noted (Right Refl) | False impossible -trustMono_level5_conditions _ _ Reject (Left Refl) impossible -trustMono_level5_conditions _ _ Reject (Right Refl) impossible -trustMono_level5_conditions _ _ Warning (Left Refl) impossible -trustMono_level5_conditions _ _ Warning (Right Refl) impossible - --- ========================================================================== --- Section 9: Injectivity witnesses (Level1 is the unique floor) --- ========================================================================== - -||| The three downgrade paths produce identical output (Level1), and that -||| output is incompatible with any level ≥ Level2. -public export -level1NotLevel2 : Level1 = Level2 -> Void -level1NotLevel2 Refl impossible - -public export -level1NotLevel3 : Level1 = Level3 -> Void -level1NotLevel3 Refl impossible - -public export -level1NotLevel4 : Level1 = Level4 -> Void -level1NotLevel4 Refl impossible - -public export -level1NotLevel5 : Level1 = Level5 -> Void -level1NotLevel5 Refl impossible diff --git a/verification/proofs/idris2/echidna-verif-proofs.ipkg b/verification/proofs/idris2/echidna-verif-proofs.ipkg index cf5b4dee..d58a3761 100644 --- a/verification/proofs/idris2/echidna-verif-proofs.ipkg +++ b/verification/proofs/idris2/echidna-verif-proofs.ipkg @@ -28,5 +28,4 @@ modules = AxiomCompleteness , NatLte , ProofStateSerialisation , ProverKindInjectivity - , TrustKernelMonotonicity , TrustLevelSoundness