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..68f1aea2 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, 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 + 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..f4549abc 100644 --- a/Justfile +++ b/Justfile @@ -250,10 +250,44 @@ 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 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 `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 + work=$(mktemp -d) + 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 -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, coqchk reports no axioms" -# Compile the Coq proof corpus (proofs/coq/**/*.v). -proofs-coq: +# 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..179c6513 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -195,6 +195,50 @@ 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, 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. + +*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 +304,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.