docs(proofs): PROOF-STATUS under strict §1, a §8.2 cone receipt, and a PWG census

.github/workflows/agda-meta-checker.yml

@@ -15,6 +15,8 @@ on:
       - 'meta-checker/**'
       - 'scripts/ci/*agda.sh'
       - 'scripts/ci/check-receipt-controls.sh'
+      - 'scripts/ci/agda-cone-receipt.sh'
+      - 'scripts/ci/test-agda-cone-receipt.sh'
       - '.github/workflows/agda-meta-checker.yml'
   # No paths-filter on pull_request: this is a REQUIRED status check, so it must
   # report on every PR (a path-filtered required check deadlocks PRs that don't
@@ -55,7 +57,7 @@ jobs:
           GH_TOKEN: ${{ github.token }}
         run: |
           set -euo pipefail
-          PATTERN='^(meta-checker/|scripts/ci/(setup-agda|check-agda|check-receipt-controls)\.sh$|\.github/workflows/agda-meta-checker\.yml$)'
+          PATTERN='^(meta-checker/|scripts/ci/(setup-agda|check-agda|check-receipt-controls|agda-cone-receipt|test-agda-cone-receipt)\.sh$|\.github/workflows/agda-meta-checker\.yml$)'
           if [ "${{ github.event_name }}" = "pull_request" ]; then
             FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \
                       --paginate --jq '.[].filename')
@@ -85,3 +87,26 @@ jobs:
       - name: Type-check meta-checker (PROOF-POLICY §2.1 canonical invocation)
         if: steps.detect.outputs.relevant == 'true'
         run: bash scripts/ci/check-agda.sh
+
+      # PROOF-POLICY §8.2/§8.4: the receipt a PWG-3 grade is derived from. It
+      # records the toolchain, the flags, the import cone of the theory
+      # module with a digest per file, and a comment-aware postulate scan of
+      # that cone. The receipt is printed to the log and the step summary.
+      - name: Record the §8.2 cone receipt for the theory theorems (Receipt.agda)
+        if: steps.detect.outputs.relevant == 'true'
+        env:
+          AGDA_STDLIB_SHA256: 72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431
+        run: |
+          set -euo pipefail
+          bash scripts/ci/test-agda-cone-receipt.sh
+          receipt="$RUNNER_TEMP/agda-cone-receipt.json"
+          (cd meta-checker && bash ../scripts/ci/agda-cone-receipt.sh src/Echidna/Receipt.agda) > "$receipt"
+          cat "$receipt"
+          {
+            echo '## PROOF-POLICY §8.2 cone receipt (Receipt.agda)'
+            jq -r '"commit \(.source.commit), \(.toolchain.agda), \(.import_cone.count) modules in the import cone, postulate scan: \(.postulate_scan.result)"' "$receipt"
+            echo
+            echo '```json'
+            cat "$receipt"
+            echo '```'
+          } >> "$GITHUB_STEP_SUMMARY"

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

EXPLAINME.adoc

@@ -164,8 +164,12 @@ ECHIDNA-specific anchors:
   backends).
 * `generated/abi/` — auto-generated C headers from the Idris2 ABI.
 
-The Agda meta-checker provides independent formal verification of the
-Rust trust-pipeline properties; see `proofs/agda/`.
+The Agda meta-checker (`meta-checker/`) type-checks *models* of the trust
+pipeline and one theory result (receipt vs warrant). A model is not a proof
+about the Rust code: under `3-practice/PROOF-POLICY.adoc` §1 the Rust
+behaviour is verified with Creusot/Pearlite and Verus on the code, and that is
+still open. `proofs/agda/` is a test corpus, not evidence. Status per
+obligation: `docs/PROOF-STATUS.adoc`.
 
 == File map: key modules
 
@@ -194,7 +198,8 @@ Rust trust-pipeline properties; see `proofs/agda/`.
 | `src/ui/tea/`, `src/ui/public/` | TEA sources (compile pipeline unavailable) and working static shell
 | `src/abi/`                 | Idris2 formal specifications (ABI contracts + totality proofs)
 | `ffi/zig/`, `src/zig_ffi/` | Zig FFI implementation
-| `proofs/agda/`             | Agda meta-checker (independent verification of trust properties)
+| `meta-checker/`            | Agda meta-checker: trust-pipeline models and the receipt/warrant theory (see `docs/PROOF-STATUS.adoc`)
+| `proofs/agda/`             | Agda test corpus (fixtures for the Agda backend; not evidence, `PROOF-POLICY` §3)
 | `tests/`                   | Integration / property / interface test suites
 |===
 

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,

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,