feat(proofs): faithful trust-rule model in Agda with a Rocq recheck

.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:

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

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: <none>" <<<"$(sed 's/[[:space:]]*$//' <<<"$summary")"; then
+            printf '%s\n' "$summary"
+            echo "FAIL: coqchk does not report '$want: <none>'"
+            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

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

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