Skip to content

Commit 687779b

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: add Agda meta-checker formally verifying trust pipeline
Comprehensive Agda formalisation proving 30+ properties about ECHIDNA's core safety invariants: - TrustLevel: total order, monotonic composition, dangerous axiom capping - AxiomSafety: policy ordering, worst-case composition, comment soundness - Portfolio: cross-checking improvement, disagreement detection - Dispatch: integrity failure handling, max trust requirements, determinism Zero postulates (except standard funext), zero sorry, zero believe_me. CI workflow type-checks all proofs on every push to meta-checker/. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 77b901c commit 687779b

8 files changed

Lines changed: 1011 additions & 0 deletions

File tree

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

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# CI workflow for ECHIDNA Agda meta-checker
3+
# Type-checks all formal proofs verifying trust pipeline correctness
4+
5+
name: Agda Meta-Checker
6+
7+
on:
8+
push:
9+
branches: [main]
10+
paths:
11+
- 'meta-checker/**'
12+
pull_request:
13+
branches: [main]
14+
paths:
15+
- 'meta-checker/**'
16+
workflow_dispatch:
17+
18+
permissions:
19+
contents: read
20+
21+
jobs:
22+
verify-proofs:
23+
name: Type-check Agda proofs
24+
runs-on: ubuntu-latest
25+
steps:
26+
- name: Checkout
27+
uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
28+
29+
- name: Setup Haskell
30+
uses: haskell-actions/setup@v2
31+
with:
32+
ghc-version: '9.6'
33+
cabal-version: '3.10'
34+
35+
- name: Cache Agda
36+
uses: actions/cache@v4
37+
with:
38+
path: |
39+
~/.cabal
40+
~/.agda
41+
key: agda-${{ runner.os }}-${{ hashFiles('meta-checker/**/*.agda') }}
42+
43+
- name: Install Agda
44+
run: |
45+
cabal update
46+
cabal install Agda-2.7.0.1
47+
48+
- name: Install Agda standard library
49+
run: |
50+
mkdir -p ~/.agda
51+
cd /tmp
52+
wget -q https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz
53+
tar xzf v2.1.tar.gz
54+
echo "/tmp/agda-stdlib-2.1/standard-library.agda-lib" > ~/.agda/libraries
55+
echo "standard-library" > ~/.agda/defaults
56+
57+
- name: Type-check meta-checker
58+
run: |
59+
cd meta-checker
60+
echo "$PWD/echidna-meta.agda-lib" >> ~/.agda/libraries
61+
agda src/Echidna/MetaChecker.agda
62+
echo "✓ All 30+ properties machine-verified"

‎meta-checker/README.adoc‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
3+
4+
= ECHIDNA Meta-Checker
5+
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
6+
:toc:
7+
8+
== Overview
9+
10+
The ECHIDNA meta-checker is an **Agda formalisation** that proves correctness properties
11+
about ECHIDNA's trust-hardening pipeline. When Agda successfully type-checks these modules,
12+
it provides a **machine-verified guarantee** that the system's safety invariants hold.
13+
14+
== Verified Properties (30+)
15+
16+
=== Trust Level System (`TrustLevel.agda`)
17+
18+
* Trust levels form a **total order** (reflexive, antisymmetric, transitive, total)
19+
* `min-trust` correctly computes lower bounds
20+
* **Dangerous axioms always cap trust at Level1**
21+
* Safe axioms preserve trust level
22+
* Capping is monotonic
23+
24+
=== Axiom Safety (`AxiomSafety.agda`)
25+
26+
* Axiom policies form a total preorder
27+
* `worst-policy` is commutative, associative, with identity (Clean)
28+
* **Rejected is absorbing** — once rejected, always rejected
29+
* Comment-aware scanning is sound
30+
* Every danger class maps to exactly one policy
31+
32+
=== Portfolio Verification (`Portfolio.agda`)
33+
34+
* **Cross-checking improves trust** over single-solver
35+
* Inconclusive and timeout always produce Level1
36+
* Small-kernel provers always have higher trust
37+
* Agreement relation is reflexive and symmetric
38+
* Unknown verdicts never count as agreement
39+
40+
=== Dispatch Pipeline (`Dispatch.agda`)
41+
42+
* **Failed integrity always produces Level1**
43+
* **Dangerous axioms always produce Level1**
44+
* Maximum trust (Level5) requires all positive factors
45+
* Pipeline is monotonically degrading
46+
* Pipeline is deterministic
47+
48+
== Zero Unsafe Constructs
49+
50+
[cols="1,1"]
51+
|===
52+
| Construct | Count
53+
54+
| `postulate` | 1 (funext — standard, provable in HoTT)
55+
| `sorry` | 0
56+
| `believe_me` | 0
57+
| `Admitted` | 0
58+
| `TRUSTME` | 0
59+
|===
60+
61+
== Running
62+
63+
[source,bash]
64+
----
65+
# Install Agda (requires GHC)
66+
cabal install Agda
67+
68+
# Install standard library
69+
agda-stdlib-utils install
70+
71+
# Type-check all proofs
72+
cd meta-checker
73+
agda src/Echidna/MetaChecker.agda
74+
----
75+
76+
If the command exits with code 0, all 30+ properties are machine-verified.
77+
78+
== CI Integration
79+
80+
The `.github/workflows/agda-meta-checker.yml` workflow automatically type-checks
81+
the meta-checker on every push. A green badge means all proofs are valid.
82+
83+
== Architecture
84+
85+
The meta-checker mirrors the Rust source structure:
86+
87+
[cols="1,1"]
88+
|===
89+
| Agda Module | Rust Source
90+
91+
| `Echidna.TrustLevel` | `verification/confidence.rs`
92+
| `Echidna.AxiomSafety` | `verification/axiom_tracker.rs`
93+
| `Echidna.Portfolio` | `verification/portfolio.rs`
94+
| `Echidna.Dispatch` | `dispatch.rs`
95+
|===
96+
97+
Each Agda definition is annotated with which Rust function or type it models.
98+
The proofs verify that the *design* is correct — they do not replace unit tests
99+
which verify that the *implementation* matches the design.

‎meta-checker/echidna-meta.agda-lib‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Agda library file for ECHIDNA meta-checker
3+
name: echidna-meta
4+
depend: standard-library
5+
include: src

0 commit comments

Comments
 (0)