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