From dbeb616e3333812f15852a31a7e827da77005993 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:27:36 +0000 Subject: [PATCH 1/2] feat(proofs): faithful trust-rule model in Agda with a Rocq recheck Echidna.TrustRule transcribes compute_trust_level from src/rust/verification/confidence.rs: separate certificate flags, the confirming-prover count, and the four rules in Rust order. It proves the two Level1 guards, what Level5 requires, and monotonicity in every factor. It is in the MetaChecker closure, so agda-meta-checker.yml checks it with the section 2.1 flags. The existing Dispatch.compute-trust model is not faithful: with two confirming provers and no certificate, Rust returns Level3 and the model returns Level2. dispatch-model-diverges states this as a theorem; the older model is left in place. verification/proofs/rocq/TrustRule.v re-proves the same statements. just proofs-verif-rocq compiles it and fails unless Print Assumptions reports every theorem closed; just proofs-coq, which the CI Coq job runs, now depends on it. The Lean leg is open. Two findings in the Rust rule are recorded in PROOF-STATUS R12 for an owner decision, not changed here: Level5 does not enforce "2+ small-kernel provers", and Level4/5 do not check has_certificate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- .github/workflows/dogfood-proofs-ci.yml | 2 + CHANGELOG.adoc | 16 ++ Justfile | 33 ++- docs/PROOF-STATUS.adoc | 45 +++- meta-checker/src/Echidna/MetaChecker.agda | 3 + meta-checker/src/Echidna/TrustRule.agda | 300 ++++++++++++++++++++++ verification/proofs/rocq/TrustRule.v | 185 +++++++++++++ 7 files changed, 580 insertions(+), 4 deletions(-) create mode 100644 meta-checker/src/Echidna/TrustRule.agda create mode 100644 verification/proofs/rocq/TrustRule.v diff --git a/.github/workflows/dogfood-proofs-ci.yml b/.github/workflows/dogfood-proofs-ci.yml index 141953ff..aa8b0382 100644 --- a/.github/workflows/dogfood-proofs-ci.yml +++ b/.github/workflows/dogfood-proofs-ci.yml @@ -24,6 +24,7 @@ on: - 'proofs/**' - 'verification/proofs/lean4/**' - 'verification/proofs/idris2/**' + - 'verification/proofs/rocq/**' - 'Justfile' - '.github/workflows/dogfood-proofs-ci.yml' pull_request: @@ -32,6 +33,7 @@ on: - 'proofs/**' - 'verification/proofs/lean4/**' - 'verification/proofs/idris2/**' + - 'verification/proofs/rocq/**' - 'Justfile' - '.github/workflows/dogfood-proofs-ci.yml' workflow_dispatch: diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 465dfc81..818f3430 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,22 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Added — trust-rule model with a Rocq recheck, 2026-11-09 + +* *`+meta-checker/src/Echidna/TrustRule.agda+`* transcribes + `+compute_trust_level+` (`+src/rust/verification/confidence.rs+`) and + proves its guards, what Level5 requires, and monotonicity in every factor. + It replaces nothing: `+Dispatch.compute-trust+` stays, and a theorem + (`+dispatch-model-diverges+`) records the input on which that older model + and the Rust rule disagree. Ledger row R12 in `+docs/PROOF-STATUS.adoc+`. +* *`+verification/proofs/rocq/TrustRule.v+`* re-proves the same statements + in Rocq. `+just proofs-verif-rocq+` compiles it and fails unless every + theorem is closed under the global context; `+just proofs-coq+` (the CI Coq + job) now runs it. The Lean leg is open. +* Two findings in the Rust rule are recorded for an owner decision, not + changed: Level5 does not check "2+ small-kernel provers", and Level4/5 do + not check that a certificate was produced. + ==== Changed — GraphQL listener default, 2026-11-04 * `+echidna-graphql+` now defaults to `+127.0.0.1:8082+`, avoiding the diff --git a/Justfile b/Justfile index 3f11a86f..d257916a 100644 --- a/Justfile +++ b/Justfile @@ -250,10 +250,37 @@ test-s4-loop: # exact same commands. # Type-check the whole dogfood proof corpus across every assistant. -proofs: proofs-coq proofs-lean proofs-agda proofs-idris proofs-verif-lean proofs-verif-idris +proofs: proofs-coq proofs-lean proofs-agda proofs-idris proofs-verif-lean proofs-verif-idris proofs-verif-rocq -# Compile the Coq proof corpus (proofs/coq/**/*.v). -proofs-coq: +# Compile the Rocq rechecks of the meta-checker (verification/proofs/rocq/*.v). +# These are PROOF-POLICY §2 recheck legs, not dogfood corpus. Each file is compiled +# in a temporary copy so no .vo/.glob lands in the tree, then `Print Assumptions` +# must report every theorem closed under the global context. +proofs-verif-rocq: + #!/usr/bin/env bash + set -euo pipefail + work=$(mktemp -d) + trap 'rm -rf "$work"' EXIT + cp verification/proofs/rocq/*.v "$work/" + cd "$work" + for f in $(ls *.v | sort); do + echo "coqc $f" + coqc -q "$f" + mod="${f%.v}" + thms=$(grep -oE '^(Theorem|Lemma) [A-Za-z0-9_]+' "$f" | awk '{print $2}') + { echo "Require Import $mod."; for t in $thms; do echo "Print Assumptions $t."; done; } > "assumptions_$mod.v" + open=$(coqc -Q . '' "assumptions_$mod.v" 2>&1 | grep -vc 'Closed under the global context' || true) + if [ "$open" -ne 0 ]; then + coqc -Q . '' "assumptions_$mod.v" + echo "FAIL: $f has a theorem that rests on an assumption" + exit 1 + fi + done + echo "Rocq recheck legs: all files compile, every theorem closed" + +# Compile the Coq proof corpus (proofs/coq/**/*.v), then the Rocq recheck legs +# (CI's Coq job runs this recipe, so the legs ride on its toolchain). +proofs-coq: proofs-verif-rocq #!/usr/bin/env bash set -euo pipefail cd proofs/coq diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index bcf6c700..414f27f0 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -195,6 +195,47 @@ invalidate its use for that changed source until a fresh check is recorded. The earlier 2026-11-01 timing/count report is historical, not the evidence for the current `+proven+` row; the source-bound 2026-11-04 receipt replaces it. +**Model fidelity, found 2026-11-09:** `+Dispatch.compute-trust+` is not a +faithful model of `+compute_trust_level+`. With two confirming provers and +no certificate, the Rust code returns Level3 (its `+confirming_provers >= 2+` +rule) and the model returns Level2. The model also uses one flag for both +"certificate produced" and "certificate verified". The theorems hold of the +model; they do not transfer to that input. R12 adds a faithful model and +states the divergence as a theorem (`+dispatch-model-diverges+`). + +|R12. `+compute_trust_level+` rule (`+confidence.rs+`): guards, what Level5 +requires, monotonicity in every factor +|`+proven+` (Agda, model); model-to-Rust correspondence `+argued+` +|`+meta-checker/src/Echidna/TrustRule.agda+` transcribes the Rust rule line +for line: separate certificate flags, the confirming count, the four rules in +Rust order. Theorems: `+dangerous-gives-level1+`, +`+integrity-failure-gives-level1+`, `+level5-sound+`, `+compute-mono+`, and +two witnesses, `+level5-without-certificate+` and `+dispatch-model-diverges+`. +In the `+MetaChecker+` closure, so `+agda-meta-checker.yml+` checks it with +Agda `+2.7.0.1+` and stdlib `+2.1+`. Session check 2026-11-09 (not a +receipt): Agda `+2.6.3+` with stdlib `+1.7.3+`, all three §2.1 flags, exit 0, +all 10 modules from fresh interfaces. Unlike the R4 modules, `+TrustRule+` +raises no `+UnsupportedIndexedMatch+` warning: equality and order proofs are +matched only in absurd clauses, or through stdlib `+≤-pred+`. A mutant with a +non-monotone rule fails to check. The transcription from Rust is unchecked by any kernel, so the row +rests on it as an `+argued+` assumption. +|*Rocq leg:* `+verification/proofs/rocq/TrustRule.v+`, route `+re-proved+` +(no Dedukti transport here). Each statement restates the Agda one of the same +name. Coq `+8.18.0+` compiles it, every theorem is closed under the global +context, and the same mutant fails. CI runs it as `+just proofs-verif-rocq+` +inside the Coq job. Correspondence state: `+COQ-CHECKED+`, `+BRIDGE-PENDING+` +until the statement-by-statement table in the file header is reviewed. +*Lean leg:* `+open+`; no Lean toolchain could be run where this was written. + +*Findings in the Rust, not fixed here:* +(a) Level5 is documented as "cross-checked by 2+ independent small-kernel +systems", but `+TrustFactors+` carries only the primary prover's kernel and a +count of agreeing provers, so the documented condition is not enforced. +(b) Level4 and Level5 test `+certificate_verified+` but not +`+has_certificate+`, so a verified flag with no certificate reaches Level5 +(`+level5-without-certificate+`). Which behaviour is intended is an owner +decision. + |R9. E11 solver-integrity soundness |`+proven+` |`+meta-checker/src/Echidna/Integrity.agda+`, inside the R4 receipt. States the @@ -260,9 +301,11 @@ Rocq/Lean rechecks and statement correspondence also remain open in R5. |`+open+` |`+PROOF-POLICY+` §2: every Agda theory proof is rechecked in both, transported through Dedukti or re-proved, with the route recorded per theorem. -|Never attempted. This is what holds the set at Mathesis *Grade 3*: locally +|Never attempted for the R4 modules. This is what holds the set at Mathesis *Grade 3*: locally checked, untranslated. ECHIDNA's `+src/rust/exchange/+` speaks Dedukti, so the transport route exists; using it is unstarted work, not a missing capability. +The first Rocq leg exists for R12 (`+verification/proofs/rocq/TrustRule.v+`, +re-proved); its Lean leg and every R4 module's legs remain open. |R6. E9 "proof composition soundness" |`+argued+`, with a location defect diff --git a/meta-checker/src/Echidna/MetaChecker.agda b/meta-checker/src/Echidna/MetaChecker.agda index 2fff5bb5..84cfd3f2 100644 --- a/meta-checker/src/Echidna/MetaChecker.agda +++ b/meta-checker/src/Echidna/MetaChecker.agda @@ -96,6 +96,9 @@ open import Echidna.Receipt public open import Echidna.Integrity public open import Echidna.ClampTrust public open import Echidna.AxiomTrackerCompleteness public +-- Qualified: its names (compute, rule, Factors) would shadow the coarser +-- Dispatch model, which it is compared against. +import Echidna.TrustRule as TrustRule ------------------------------------------------------------------------ -- Summary: Key safety invariants proven diff --git a/meta-checker/src/Echidna/TrustRule.agda b/meta-checker/src/Echidna/TrustRule.agda new file mode 100644 index 00000000..ae624387 --- /dev/null +++ b/meta-checker/src/Echidna/TrustRule.agda @@ -0,0 +1,300 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- TrustRule.agda — a line-for-line model of `compute_trust_level` +-- (src/rust/verification/confidence.rs) and what it guarantees. +-- +-- `Echidna.Dispatch.compute-trust` models the same function more coarsely: +-- one flag stands for both "a certificate was produced" and "it was +-- verified", and a cross-check without a certificate yields Level2 there, +-- where the Rust code yields Level3 (`confirming_provers >= 2`). +-- `dispatch-model-diverges` below exhibits that input. This module keeps +-- the two certificate flags and the confirming count apart, as Rust does. +-- +-- Proved here, about the model: +-- +-- 1. guards — dangerous axioms or a failed integrity check give +-- Level1, whatever else holds; +-- 2. level5-sound — Level5 implies a small-kernel prover, a verified +-- certificate, at least two confirming provers, a +-- passed integrity check and no dangerous axiom; +-- 3. compute-mono — improving any factor never lowers the level; +-- 4. two witnesses — Level5 with no certificate produced +-- (`level5-without-certificate`), and the input on +-- which `Dispatch.compute-trust` disagrees with the +-- Rust rule (`dispatch-model-diverges`). +-- +-- Not provable here, and recorded as a finding: Level5 is documented as +-- "cross-checked by 2+ independent small-kernel systems", but the Rust +-- factors carry only the PRIMARY prover's kernel and a count of agreeing +-- provers. Nothing in `TrustFactors` says the other provers have small +-- kernels, so the code cannot enforce the documented condition. +-- +-- The correspondence between this model and the Rust source is a +-- transcription that no kernel checked: PROOF-POLICY records it as ASSUMED. + +module Echidna.TrustRule where + +open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s) +open import Data.Nat.Properties using (≤-pred) +open import Data.Bool using (Bool; true; false; if_then_else_; _∧_; _∨_; not) +open import Data.Product using (_×_; _,_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Echidna.TrustLevel +open import Echidna.AxiomSafety using (DangerClass; DC-Safe) +import Echidna.Dispatch as Dispatch + +------------------------------------------------------------------------ +-- The factors, as in `TrustFactors` (confidence.rs). `small-kernel` is +-- `is_small_kernel_prover(prover)`; the portfolio field is unused by +-- `compute_trust_level` and is left out. +------------------------------------------------------------------------ + +record Factors : Set where + field + small-kernel : Bool + confirming : ℕ + has-certificate : Bool + certificate-verified : Bool + danger : DangerLevel + integrity-ok : Bool + +open Factors + +-- `confirming_provers >= 2` +cross : ℕ → Bool +cross zero = false +cross (suc zero) = false +cross (suc (suc _)) = true + +-- Warning and Reject both force Level1 in the Rust code. +dangerous : DangerLevel → Bool +dangerous Safe = false +dangerous Noted = false +dangerous Warning = true +dangerous Reject = true + +-- The four rules after the guards, in the Rust order (first match wins): +-- L5: cross ∧ verified ∧ small-kernel; L4: small-kernel ∧ verified; +-- L3: has ∧ verified; L3: cross; otherwise L2. +rule : (sk cc hc cv : Bool) → TrustLevel +rule sk cc hc cv = + if cc ∧ cv ∧ sk then Level5 else + if sk ∧ cv then Level4 else + if hc ∧ cv then Level3 else + if cc then Level3 else Level2 + +bad : Factors → Bool +bad f = dangerous (danger f) ∨ not (integrity-ok f) + +compute : Factors → TrustLevel +compute f = if bad f then Level1 + else rule (small-kernel f) (cross (confirming f)) + (has-certificate f) (certificate-verified f) + +------------------------------------------------------------------------ +-- 1. Guards +------------------------------------------------------------------------ + +dangerous-gives-level1 : ∀ f → dangerous (danger f) ≡ true → compute f ≡ Level1 +dangerous-gives-level1 f p with dangerous (danger f) +... | true = refl + +integrity-failure-gives-level1 : ∀ f → integrity-ok f ≡ false → compute f ≡ Level1 +integrity-failure-gives-level1 f p with dangerous (danger f) | integrity-ok f +... | true | _ = refl +... | false | false = refl + +------------------------------------------------------------------------ +-- 2. What Level5 requires +------------------------------------------------------------------------ + +cross-sound : ∀ n → cross n ≡ true → 2 ≤ n +-- Only absurd patterns touch the equality proof: no constructor-injectivity +-- match, so no UnsupportedIndexedMatch warning under --cubical-compatible. +cross-sound zero () +cross-sound (suc zero) () +cross-sound (suc (suc n)) _ = s≤s (s≤s z≤n) + +-- Of the four rules, only the first yields Level5. +rule-level5 : ∀ sk cc hc cv → rule sk cc hc cv ≡ Level5 → + sk ≡ true × cc ≡ true × cv ≡ true +rule-level5 true true _ true _ = refl , refl , refl +rule-level5 true true true false () +rule-level5 true true false false () +rule-level5 true false _ true () +rule-level5 true false true false () +rule-level5 true false false false () +rule-level5 false true true true () +rule-level5 false true false true () +rule-level5 false true true false () +rule-level5 false true false false () +rule-level5 false false true true () +rule-level5 false false false true () +rule-level5 false false true false () +rule-level5 false false false false () + +level5-sound : ∀ f → compute f ≡ Level5 → + small-kernel f ≡ true × certificate-verified f ≡ true × + 2 ≤ confirming f × integrity-ok f ≡ true × dangerous (danger f) ≡ false +level5-sound f p with dangerous (danger f) in ed | integrity-ok f in ei +level5-sound f () | true | _ +level5-sound f () | false | false +level5-sound f p | false | true + with rule-level5 (small-kernel f) (cross (confirming f)) + (has-certificate f) (certificate-verified f) p +... | sk , cc , cv = sk , cv , cross-sound (confirming f) cc , refl , refl + +------------------------------------------------------------------------ +-- 3. Monotonicity +------------------------------------------------------------------------ + +-- false ≤ true on Bool +data _≤B_ : Bool → Bool → Set where + f≤f : false ≤B false + f≤t : false ≤B true + t≤t : true ≤B true + +cross-mono : ∀ {m n} → m ≤ n → cross m ≤B cross n +-- As in cross-sound, the order proof is matched only in absurd clauses. +cross-mono {zero} {zero} _ = f≤f +cross-mono {zero} {suc zero} _ = f≤f +cross-mono {zero} {suc (suc _)} _ = f≤t +cross-mono {suc zero} {zero} () +cross-mono {suc zero} {suc zero} _ = f≤f +cross-mono {suc zero} {suc (suc _)} _ = f≤t +cross-mono {suc (suc _)} {zero} () +cross-mono {suc (suc _)} {suc zero} p with ≤-pred p +... | () +cross-mono {suc (suc _)} {suc (suc _)} _ = t≤t + +-- rule with the varying argument first, so each lemma below is one table +rule-at-sk rule-at-cc rule-at-hc rule-at-cv : Bool → Bool → Bool → Bool → TrustLevel +rule-at-sk x a b c = rule x a b c +rule-at-cc x a b c = rule a x b c +rule-at-hc x a b c = rule a b x c +rule-at-cv x a b c = rule a b c x + +-- rule is monotone in sk (false ≤ true), the other three fixed. +rule-mono-sk : ∀ a b c → rule-at-sk false a b c ≤ₜ rule-at-sk true a b c +rule-mono-sk false false false = ≤ₜ-refl Level2 +rule-mono-sk false false true = l2≤4 +rule-mono-sk false true false = ≤ₜ-refl Level2 +rule-mono-sk false true true = l3≤4 +rule-mono-sk true false false = ≤ₜ-refl Level3 +rule-mono-sk true false true = l3≤5 +rule-mono-sk true true false = ≤ₜ-refl Level3 +rule-mono-sk true true true = l3≤5 + +-- rule is monotone in cc (false ≤ true), the other three fixed. +rule-mono-cc : ∀ a b c → rule-at-cc false a b c ≤ₜ rule-at-cc true a b c +rule-mono-cc false false false = l2≤3 +rule-mono-cc false false true = l2≤3 +rule-mono-cc false true false = l2≤3 +rule-mono-cc false true true = ≤ₜ-refl Level3 +rule-mono-cc true false false = l2≤3 +rule-mono-cc true false true = l4≤5 +rule-mono-cc true true false = l2≤3 +rule-mono-cc true true true = l4≤5 + +-- rule is monotone in hc (false ≤ true), the other three fixed. +rule-mono-hc : ∀ a b c → rule-at-hc false a b c ≤ₜ rule-at-hc true a b c +rule-mono-hc false false false = ≤ₜ-refl Level2 +rule-mono-hc false false true = l2≤3 +rule-mono-hc false true false = ≤ₜ-refl Level3 +rule-mono-hc false true true = ≤ₜ-refl Level3 +rule-mono-hc true false false = ≤ₜ-refl Level2 +rule-mono-hc true false true = ≤ₜ-refl Level4 +rule-mono-hc true true false = ≤ₜ-refl Level3 +rule-mono-hc true true true = ≤ₜ-refl Level5 + +-- rule is monotone in cv (false ≤ true), the other three fixed. +rule-mono-cv : ∀ a b c → rule-at-cv false a b c ≤ₜ rule-at-cv true a b c +rule-mono-cv false false false = ≤ₜ-refl Level2 +rule-mono-cv false false true = l2≤3 +rule-mono-cv false true false = ≤ₜ-refl Level3 +rule-mono-cv false true true = ≤ₜ-refl Level3 +rule-mono-cv true false false = l2≤4 +rule-mono-cv true false true = l2≤4 +rule-mono-cv true true false = l3≤5 +rule-mono-cv true true true = l3≤5 + +rule-mono : ∀ {sk sk′ cc cc′ hc hc′ cv cv′} → + sk ≤B sk′ → cc ≤B cc′ → hc ≤B hc′ → cv ≤B cv′ → + rule sk cc hc cv ≤ₜ rule sk′ cc′ hc′ cv′ +rule-mono {sk} {sk′} {cc} {cc′} {hc} {hc′} {cv} {cv′} psk pcc phc pcv = + ≤ₜ-trans (step-sk psk) (≤ₜ-trans (step-cc pcc) (≤ₜ-trans (step-hc phc) (step-cv pcv))) + where + step-sk : sk ≤B sk′ → rule sk cc hc cv ≤ₜ rule sk′ cc hc cv + step-sk f≤f = ≤ₜ-refl _ + step-sk f≤t = rule-mono-sk cc hc cv + step-sk t≤t = ≤ₜ-refl _ + step-cc : cc ≤B cc′ → rule sk′ cc hc cv ≤ₜ rule sk′ cc′ hc cv + step-cc f≤f = ≤ₜ-refl _ + step-cc f≤t = rule-mono-cc sk′ hc cv + step-cc t≤t = ≤ₜ-refl _ + step-hc : hc ≤B hc′ → rule sk′ cc′ hc cv ≤ₜ rule sk′ cc′ hc′ cv + step-hc f≤f = ≤ₜ-refl _ + step-hc f≤t = rule-mono-hc sk′ cc′ cv + step-hc t≤t = ≤ₜ-refl _ + step-cv : cv ≤B cv′ → rule sk′ cc′ hc′ cv ≤ₜ rule sk′ cc′ hc′ cv′ + step-cv f≤f = ≤ₜ-refl _ + step-cv f≤t = rule-mono-cv sk′ cc′ hc′ + step-cv t≤t = ≤ₜ-refl _ + +-- g is at least as good as f in every factor: no worse axioms, and every +-- flag and the confirming count at least as high. +record _⊑_ (f g : Factors) : Set where + field + sk-≤ : small-kernel f ≤B small-kernel g + conf-≤ : confirming f ≤ confirming g + hc-≤ : has-certificate f ≤B has-certificate g + cv-≤ : certificate-verified f ≤B certificate-verified g + io-≤ : integrity-ok f ≤B integrity-ok g + dg-≤ : dangerous (danger g) ≤B dangerous (danger f) + +-- If g fails a guard, so does f (it is no better on either guard factor). +bad-anti : ∀ {f g} → f ⊑ g → bad g ≡ true → bad f ≡ true +bad-anti {f} {g} le p with dangerous (danger f) | dangerous (danger g) + | integrity-ok f | integrity-ok g + | _⊑_.dg-≤ le | _⊑_.io-≤ le +... | true | _ | _ | _ | _ | _ = refl +... | false | true | _ | _ | () | _ +... | false | false | false | _ | _ | _ = refl +... | false | false | true | false | _ | () +... | false | false | true | true | _ | _ with p +... | () + +compute-mono : ∀ {f g} → f ⊑ g → compute f ≤ₜ compute g +compute-mono {f} {g} le with bad f in ef | bad g in eg +... | true | _ = l1≤ +... | false | true with bad-anti le eg +... | bf rewrite ef with bf +... | () +compute-mono {f} {g} le | false | false = + rule-mono (_⊑_.sk-≤ le) (cross-mono (_⊑_.conf-≤ le)) (_⊑_.hc-≤ le) (_⊑_.cv-≤ le) + +------------------------------------------------------------------------ +-- 4. Witnesses +------------------------------------------------------------------------ + +-- Level5 is reached with no certificate produced: the Level5 and Level4 +-- rules test `certificate_verified` but not `has_certificate`. +level5-without-certificate : + compute record { small-kernel = true ; confirming = 2 ; has-certificate = false + ; certificate-verified = true ; danger = Safe ; integrity-ok = true } + ≡ Level5 +level5-without-certificate = refl + +-- A cross-check by two provers with no certificate: the Rust rule gives +-- Level3; Dispatch.compute-trust gives Level2 for the same situation. +dispatch-model-diverges : + compute record { small-kernel = false ; confirming = 2 ; has-certificate = false + ; certificate-verified = false ; danger = Safe ; integrity-ok = true } + ≡ Level3 + × Dispatch.compute-trust + record { integrity-ok = true ; has-certificate = false ; small-kernel = false + ; axiom-danger = DC-Safe ; cross-checked = true } + ≡ Level2 +dispatch-model-diverges = refl , refl diff --git a/verification/proofs/rocq/TrustRule.v b/verification/proofs/rocq/TrustRule.v new file mode 100644 index 00000000..907e28f8 --- /dev/null +++ b/verification/proofs/rocq/TrustRule.v @@ -0,0 +1,185 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) +(* + TrustRule.v — Rocq recheck of meta-checker/src/Echidna/TrustRule.agda. + + Route: re-proved (PROOF-POLICY §2). The Agda module was not transported + through Dedukti; each statement below is restated by hand to match the + Agda statement of the same name (`-` becomes `_`), and proved again here. + The definitions are transcribed from the Agda module, which is itself a + transcription of `compute_trust_level` in + src/rust/verification/confidence.rs. + + Correspondence, statement by statement: + dangerous_gives_level1, integrity_failure_gives_level1 (guards) + rule_level5, level5_sound (Level5) + rule_mono, compute_mono (monotonicity) + level5_without_certificate, dispatch_model_diverges (witnesses) + The Agda order _≤ₜ_ is an inductive relation with the same fifteen + cases as `le_t` below. +*) + +From Coq Require Import Arith Bool Lia. + +Inductive TrustLevel := Level1 | Level2 | Level3 | Level4 | Level5. + +(* Same cases as Echidna.TrustLevel._≤ₜ_ *) +Inductive le_t : TrustLevel -> TrustLevel -> Prop := +| l1_le : forall t, le_t Level1 t +| l2_le_2 : le_t Level2 Level2 | l2_le_3 : le_t Level2 Level3 +| l2_le_4 : le_t Level2 Level4 | l2_le_5 : le_t Level2 Level5 +| l3_le_3 : le_t Level3 Level3 | l3_le_4 : le_t Level3 Level4 +| l3_le_5 : le_t Level3 Level5 +| l4_le_4 : le_t Level4 Level4 | l4_le_5 : le_t Level4 Level5 +| l5_le_5 : le_t Level5 Level5. + +Lemma le_t_refl : forall t, le_t t t. +Proof. destruct t; constructor. Qed. + +Lemma le_t_trans : forall a b c, le_t a b -> le_t b c -> le_t a c. +Proof. intros a b c H1 H2; inversion H1; subst; inversion H2; subst; constructor. Qed. + +Inductive DangerLevel := Safe | Noted | Warning | Reject. + +Record Factors := mkFactors { + small_kernel : bool; + confirming : nat; + has_certificate : bool; + certificate_verified : bool; + danger : DangerLevel; + integrity_ok : bool +}. + +(* confirming_provers >= 2 *) +Definition cross (n : nat) : bool := + match n with 0 | 1 => false | S (S _) => true end. + +Definition dangerous (d : DangerLevel) : bool := + match d with Safe | Noted => false | Warning | Reject => true end. + +Definition rule (sk cc hc cv : bool) : TrustLevel := + if cc && cv && sk then Level5 else + if sk && cv then Level4 else + if hc && cv then Level3 else + if cc then Level3 else Level2. + +Definition bad (f : Factors) : bool := + dangerous (danger f) || negb (integrity_ok f). + +Definition compute (f : Factors) : TrustLevel := + if bad f then Level1 + else rule (small_kernel f) (cross (confirming f)) + (has_certificate f) (certificate_verified f). + +(* 1. Guards *) + +Theorem dangerous_gives_level1 : forall f, + dangerous (danger f) = true -> compute f = Level1. +Proof. intros f H; unfold compute, bad; rewrite H; reflexivity. Qed. + +Theorem integrity_failure_gives_level1 : forall f, + integrity_ok f = false -> compute f = Level1. +Proof. + intros f H; unfold compute, bad; rewrite H. + destruct (dangerous (danger f)); reflexivity. +Qed. + +(* 2. What Level5 requires *) + +Lemma cross_sound : forall n, cross n = true -> 2 <= n. +Proof. intros [|[|n]] H; simpl in H; try discriminate; lia. Qed. + +Lemma rule_level5 : forall sk cc hc cv, + rule sk cc hc cv = Level5 -> sk = true /\ cc = true /\ cv = true. +Proof. + intros [] [] [] []; unfold rule; simpl; intro H; + try discriminate; repeat split; reflexivity. +Qed. + +Theorem level5_sound : forall f, compute f = Level5 -> + small_kernel f = true /\ certificate_verified f = true /\ + 2 <= confirming f /\ integrity_ok f = true /\ dangerous (danger f) = false. +Proof. + intros f H; unfold compute, bad in H. + destruct (dangerous (danger f)) eqn:Ed; simpl in H; try discriminate. + destruct (integrity_ok f) eqn:Ei; simpl in H; try discriminate. + destruct (rule_level5 _ _ _ _ H) as [Hsk [Hcc Hcv]]. + repeat split; auto. apply cross_sound; exact Hcc. +Qed. + +(* 3. Monotonicity: false <= true on bool *) + +Definition le_b (a b : bool) : Prop := a = true -> b = true. + +Lemma cross_mono : forall m n, m <= n -> le_b (cross m) (cross n). +Proof. + unfold le_b; intros [|[|m]] [|[|n]] Hle H; simpl in *; try discriminate; + try reflexivity; lia. +Qed. + +Theorem rule_mono : forall sk sk' cc cc' hc hc' cv cv', + le_b sk sk' -> le_b cc cc' -> le_b hc hc' -> le_b cv cv' -> + le_t (rule sk cc hc cv) (rule sk' cc' hc' cv'). +Proof. + unfold le_b; intros [] [] [] [] [] [] [] [] H1 H2 H3 H4; + unfold rule; simpl; + try (specialize (H1 eq_refl); discriminate); + try (specialize (H2 eq_refl); discriminate); + try (specialize (H3 eq_refl); discriminate); + try (specialize (H4 eq_refl); discriminate); + constructor. +Qed. + +(* g is at least as good as f in every factor *) +Record better (f g : Factors) : Prop := { + sk_le : le_b (small_kernel f) (small_kernel g); + conf_le : confirming f <= confirming g; + hc_le : le_b (has_certificate f) (has_certificate g); + cv_le : le_b (certificate_verified f) (certificate_verified g); + io_le : le_b (integrity_ok f) (integrity_ok g); + dg_le : le_b (dangerous (danger g)) (dangerous (danger f)) +}. + +Lemma bad_anti : forall f g, better f g -> bad g = true -> bad f = true. +Proof. + intros f g [_ _ _ _ Hio Hdg]; unfold bad, le_b in *. + destruct (dangerous (danger f)), (dangerous (danger g)), + (integrity_ok f), (integrity_ok g); simpl; intro H; + auto; try discriminate; + try (specialize (Hdg eq_refl); discriminate); + try (specialize (Hio eq_refl); discriminate). +Qed. + +Theorem compute_mono : forall f g, better f g -> le_t (compute f) (compute g). +Proof. + intros f g Hb; unfold compute. + destruct (bad f) eqn:Ef; [constructor|]. + destruct (bad g) eqn:Eg. + - rewrite (bad_anti f g Hb Eg) in Ef; discriminate. + - destruct Hb as [Hsk Hconf Hhc Hcv _ _]. + apply rule_mono; auto. apply cross_mono; exact Hconf. +Qed. + +(* 4. Witnesses *) + +Theorem level5_without_certificate : + compute (mkFactors true 2 false true Safe true) = Level5. +Proof. reflexivity. Qed. + +(* Echidna.Dispatch.compute-trust, transcribed: one certificate flag and a + cross-checked flag; no certificate gives Level2 whatever else holds. *) +Inductive DangerClass := DC_Safe | DC_Noted | DC_Warning | DC_Reject. + +Definition dispatch_compute (io : bool) (d : DangerClass) (h s c : bool) + : TrustLevel := + match io, d with + | false, _ | _, DC_Warning | _, DC_Reject => Level1 + | true, _ => + if h then (if s then (if c then Level5 else Level4) else Level3) + else Level2 + end. + +Theorem dispatch_model_diverges : + compute (mkFactors false 2 false false Safe true) = Level3 /\ + dispatch_compute true DC_Safe false false true = Level2. +Proof. split; reflexivity. Qed. From b4a74ead29def780307444d951494d3cae11d519 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:52:29 +0000 Subject: [PATCH 2/2] fix(proofs): gate the Rocq legs on coqchk, not a theorem-name regex proofs-verif-rocq took theorem names from unindented Theorem/Lemma lines and ran Print Assumptions on each. An admitted Fact, Corollary, Remark or indented lemma was never checked, and a file with no matching line passed vacuously. The recipe now runs coqchk -o, Rocq's separate checker kernel, over every compiled library. Its context summary lists each Axiom, Parameter and Admitted declaration whatever its keyword or position, and whether or not a theorem uses it. The recipe requires all four "relying on" lines to read ; any other output, including none, fails. Checked: the real file passes; an indented admitted Fact, an admitted Corollary, an Axiom, and an admitted Remark in a section each fail; a coqchk that prints nothing or exits non-zero fails. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --- CHANGELOG.adoc | 4 ++-- Justfile | 29 ++++++++++++++++++----------- docs/PROOF-STATUS.adoc | 7 +++++-- 3 files changed, 25 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 818f3430..68f1aea2 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -17,8 +17,8 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. (`+dispatch-model-diverges+`) records the input on which that older model and the Rust rule disagree. Ledger row R12 in `+docs/PROOF-STATUS.adoc+`. * *`+verification/proofs/rocq/TrustRule.v+`* re-proves the same statements - in Rocq. `+just proofs-verif-rocq+` compiles it and fails unless every - theorem is closed under the global context; `+just proofs-coq+` (the CI Coq + in Rocq. `+just proofs-verif-rocq+` compiles it, then + requires `+coqchk -o+` to report no axioms and no unsafe flags; `+just proofs-coq+` (the CI Coq job) now runs it. The Lean leg is open. * Two findings in the Rust rule are recorded for an owner decision, not changed: Level5 does not check "2+ small-kernel provers", and Level4/5 do diff --git a/Justfile b/Justfile index d257916a..f4549abc 100644 --- a/Justfile +++ b/Justfile @@ -254,8 +254,11 @@ proofs: proofs-coq proofs-lean proofs-agda proofs-idris proofs-verif-lean proofs # Compile the Rocq rechecks of the meta-checker (verification/proofs/rocq/*.v). # These are PROOF-POLICY §2 recheck legs, not dogfood corpus. Each file is compiled -# in a temporary copy so no .vo/.glob lands in the tree, then `Print Assumptions` -# must report every theorem closed under the global context. +# in a temporary copy so no .vo/.glob lands in the tree. Then `coqchk`, Rocq's +# separate checker kernel, re-checks every compiled library and must report no +# axioms and no unsafe flags. Every Axiom, Parameter and Admitted declaration +# counts as an axiom, whatever its keyword, indentation or section, and whether +# or not a theorem uses it. Any other summary output fails the recipe. proofs-verif-rocq: #!/usr/bin/env bash set -euo pipefail @@ -263,20 +266,24 @@ proofs-verif-rocq: trap 'rm -rf "$work"' EXIT cp verification/proofs/rocq/*.v "$work/" cd "$work" + mods=() for f in $(ls *.v | sort); do echo "coqc $f" - coqc -q "$f" - mod="${f%.v}" - thms=$(grep -oE '^(Theorem|Lemma) [A-Za-z0-9_]+' "$f" | awk '{print $2}') - { echo "Require Import $mod."; for t in $thms; do echo "Print Assumptions $t."; done; } > "assumptions_$mod.v" - open=$(coqc -Q . '' "assumptions_$mod.v" 2>&1 | grep -vc 'Closed under the global context' || true) - if [ "$open" -ne 0 ]; then - coqc -Q . '' "assumptions_$mod.v" - echo "FAIL: $f has a theorem that rests on an assumption" + coqc -q -Q . '' "$f" + mods+=("${f%.v}") + done + echo "coqchk -o ${mods[*]}" + summary=$(coqchk -o -silent -Q . '' "${mods[@]}" 2>&1 | sed -n '/^CONTEXT SUMMARY/,$p') + for want in 'Axioms' 'Constants/Inductives relying on type-in-type' \ + 'Constants/Inductives relying on unsafe (co)fixpoints' \ + 'Inductives whose positivity is assumed'; do + if ! grep -qxF "* $want: " <<<"$(sed 's/[[:space:]]*$//' <<<"$summary")"; then + printf '%s\n' "$summary" + echo "FAIL: coqchk does not report '$want: '" exit 1 fi done - echo "Rocq recheck legs: all files compile, every theorem closed" + echo "Rocq recheck legs: all files compile, coqchk reports no axioms" # Compile the Coq proof corpus (proofs/coq/**/*.v), then the Rocq recheck legs # (CI's Coq job runs this recipe, so the legs ride on its toolchain). diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 414f27f0..179c6513 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -221,8 +221,11 @@ non-monotone rule fails to check. The transcription from Rust is unchecked by an rests on it as an `+argued+` assumption. |*Rocq leg:* `+verification/proofs/rocq/TrustRule.v+`, route `+re-proved+` (no Dedukti transport here). Each statement restates the Agda one of the same -name. Coq `+8.18.0+` compiles it, every theorem is closed under the global -context, and the same mutant fails. CI runs it as `+just proofs-verif-rocq+` +name. Coq `+8.18.0+` compiles it, and `+coqchk -o+` (the separate checker +kernel) re-checks the compiled library and reports no axioms. Any `+Axiom+`, +`+Parameter+` or `+Admitted+` declaration, used or not, would be listed. The +same mutant fails, as do four planted escape hatches (an indented `+Fact+`, a +`+Corollary+`, an `+Axiom+`, a `+Remark+` in a section). CI runs it as `+just proofs-verif-rocq+` inside the Coq job. Correspondence state: `+COQ-CHECKED+`, `+BRIDGE-PENDING+` until the statement-by-statement table in the file header is reviewed. *Lean leg:* `+open+`; no Lean toolchain could be run where this was written.