Merge branch 'main' into feat/cross-repo-proof-dag

Author: hyperpolymath

.trusted-base-ignore

@@ -28,9 +28,19 @@ crates/echidna-core-spark/src/axiom_tracker.rs
 # ─────────────────────────────────────────────────────────────────────────────
 # Hazard-classification helpers in the corpus extractor (NOT uses)
 # ─────────────────────────────────────────────────────────────────────────────
-# `corpus/agda.rs::collect_hazards` and `corpus/idris2.rs::collect_hazards`
-# each run a single-line `if text.contains("unsafePerformIO" / "unsafeCoerce"
-# / "Obj.magic")` to flag corpus entries that *contain* those patterns.
+# `corpus/agda.rs`, `corpus/idris2.rs` and `corpus/fstar.rs` each run a
+# single-line `if text.contains("unsafePerformIO" / "unsafeCoerce" / "Obj.magic"
+# / "admit" / ...)` to flag corpus entries that *contain* those patterns.
 # Same FP class — the substring is a hazard sentinel, not an escape hatch.
 src/rust/corpus/agda.rs
 src/rust/corpus/idris2.rs
+src/rust/corpus/fstar.rs
+
+# ─────────────────────────────────────────────────────────────────────────────
+# Test corpus fixtures (sample prover inputs, NOT trust-kernel proofs)
+# ─────────────────────────────────────────────────────────────────────────────
+# `tests/corpus_fixtures/` holds sample source files fed to the corpus
+# extractors as test inputs — e.g. a minif2f Lean problem stubbed with `sorry`,
+# an F* smoke file with `assume val oracle`. They exercise the scanner; they are
+# not proof obligations in the trusted base.
+tests/corpus_fixtures/

docs/HP-BACKEND-ONBOARDING.md

@@ -0,0 +1,151 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# Onboarding a new HP type-discipline backend
+
+This is the working checklist for adding a new HP-ecosystem type
+discipline to echidna. The 41 existing variants (TypeLL,
+KatagoriaVerifier, TropicalTypeChecker, EchoTypeChecker, ...) all
+followed this same pattern.
+
+For background on what already exists, see
+`docs/handover/B7-AUDIT-CORRECTION.md`.
+
+## Where the wiring lives
+
+Adding a new discipline `Foo` (i.e. `ProverKind::FooTypeChecker`)
+touches exactly four files:
+
+| File                                            | What to add                                                       |
+|-------------------------------------------------|-------------------------------------------------------------------|
+| `src/rust/provers/mod.rs`                       | Enum variant + parser arm + is_hp_ecosystem + default_executable  |
+| `src/rust/provers/hp_ecosystem.rs::upstream()`  | One match arm: `Foo => ("typell", "foo")`                         |
+| `src/rust/provers/typed_wasm.rs::type_info_for` | `TypeInfo` selector for the discipline (the typed_wasm route)     |
+| `tests/fixtures/hp/foo_trivial.tll`             | One smoke fixture exercising the new wire                         |
+
+If the discipline ships its own CLI (i.e. not `typell --discipline=foo`
+but a standalone binary), it routes through `HPEcosystemBackend` and
+the `upstream()` arm returns `("foo-cli", "foo")`. If it lives under
+`typell`, it routes through `TypedWasmBackend` via the discipline
+parameter.
+
+The deciding question: **does the upstream maintainer ship a separate
+binary?** Examples:
+
+- `KatagoriaVerifier`  → standalone `katagoria` binary → `HPEcosystemBackend`.
+- `TropicalTypeChecker` → standalone `tropical-type-check` binary → either path (currently `TypedWasmBackend`).
+- `EchoTypeChecker`     → bundled under `typell`                  → `TypedWasmBackend`.
+
+## Step-by-step
+
+### 1. Add the enum variant
+
+`src/rust/provers/mod.rs`, in the `ProverKind` enum (around line 294):
+
+```rust
+pub enum ProverKind {
+    // ...
+    FooTypeChecker,
+    // ...
+}
+```
+
+### 2. Parser arm
+
+Same file, around line 567 (the string-to-ProverKind parser):
+
+```rust
+"footypechecker" | "foo" => Ok(ProverKind::FooTypeChecker),
+```
+
+### 3. `is_hp_ecosystem` arm
+
+Same file, around line 434:
+
+```rust
+pub fn is_hp_ecosystem(&self) -> bool {
+    matches!(self,
+        // ...
+        | ProverKind::FooTypeChecker
+    )
+}
+```
+
+### 4. `default_executable` arm
+
+Same file, around line 1360. Either:
+
+```rust
+ProverKind::FooTypeChecker => "typell",       // bundled
+// or
+ProverKind::FooTypeChecker => "foo-cli",      // standalone
+```
+
+### 5. Factory routing arm
+
+Same file, `ProverFactory::create` (around line 1822). Add to the
+appropriate match arm:
+
+- Standalone binary: add to the `HPEcosystemBackend` arm at line
+  1776-1778.
+- Bundled discipline: add to the `TypedWasmBackend` arm at lines
+  1784-1822.
+
+### 6. (Bundled discipline only) `upstream()` arm
+
+`src/rust/provers/hp_ecosystem.rs`, the `upstream()` match around
+line 63:
+
+```rust
+ProverKind::FooTypeChecker => ("typell", "foo"),
+```
+
+### 7. `TypeInfo` selector
+
+`src/rust/provers/typed_wasm.rs::type_info_for` — return the discipline's
+parametric `TypeInfo` so the unified verifier knows what to check.
+
+### 8. Smoke fixture
+
+`tests/fixtures/hp/foo_trivial.tll`:
+
+```
+# SPDX-License-Identifier: MPL-2.0
+#discipline: foo
+
+theorem foo_identity : ... .
+Proof.
+  foo_refl.
+Qed.
+```
+
+### 9. Run the smoke
+
+`tests/gnn_augment_integration.rs::test_hp_ecosystem_gnn_wires_top_premise`
+already loops over `is_hp_ecosystem()` kinds, so the new variant gets
+GNN-wiring coverage for free. A direct backend smoke takes one more
+line in `tests/common/mod.rs` if you want it.
+
+## What you DON'T need to touch
+
+- **Confidence levels** — the trust bridge reads
+  `is_hp_ecosystem()` once; no per-discipline tuning.
+- **Corpus extractors** — the HP corpus is built by
+  `crates/typed_wasm` and indexed by Sigma parameters; new disciplines
+  inherit the existing pipeline.
+- **Result formatter** — `result_formatter.rs` reads `ProverKind`
+  via Display; the variant name is the user-facing label.
+
+## When the upstream binary doesn't ship
+
+For early-development disciplines where the upstream tool isn't yet
+buildable (e.g. an unreleased Wokelang variant), the backend will
+return a "binary not found" runtime error. That is the right
+behaviour — echidna's trust bridge surfaces it as
+`ProverOutcome::Unsupported` and the caller sees a clear signal.
+
+Do **not** stub the backend to return spurious success. Estate
+consumers (per the C12 per-repo manifest) configure `[provers]
+disabled = ["foo"]` to opt out cleanly.

docs/handover/B7-AUDIT-CORRECTION.md

@@ -0,0 +1,111 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# B7 audit correction — HP ecosystem backends are NOT corpus-only
+
+**Status**: Correction.
+**Origin**: The 2026-06-03 "what stops echidna from running proof work
+across the estate" punch list listed **B7** as:
+
+> _HP type-checker ecosystem (13 provers) corpus-only — KatagoriaVerifier,
+> Modal/Session/Choreographic/Epistemic/Refinement/Echo/Dependent/QTT/
+> Effect-Row/Tropical/TypeLL backends missing. Rust adapters not
+> scaffolded in `src/rust/provers/`. Corpus contributes to vocab/training
+> only._
+
+That characterisation is incorrect. This memo replaces B7's "scaffold
+missing adapters" framing with what is actually missing.
+
+## What is actually in tree (verified 2026-06-03)
+
+### Unified `HPEcosystemBackend`
+
+`src/rust/provers/hp_ecosystem.rs:50-153` defines
+`HPEcosystemBackend`, a full `ProverBackend` implementation that:
+
+- Pattern-matches on `ProverKind` to select the upstream CLI
+  (`typell`, `katagoria`, `tropical-type-check`) and discipline tag
+  (`echo`, `session`, `qtt`, `effect-row`, ...) — see
+  `hp_ecosystem.rs::upstream()` lines 63-126.
+- Implements `parse_file`, `parse_string`, `apply_tactic`, and
+  `verify_proof` against the upstream binary — lines 156-330.
+- Injects a `#discipline:` header when the source lacks one (lines
+  196-205), so estate consumers don't need to know the wire format.
+
+### Routing in `ProverFactory::create`
+
+`src/rust/provers/mod.rs:1774-1824` routes:
+
+| ProverKind                                            | Backend                                          |
+|-------------------------------------------------------|--------------------------------------------------|
+| `TypeLL`, `KatagoriaVerifier`                         | `hp_ecosystem::HPEcosystemBackend`               |
+| 39 other `*TypeChecker` variants incl. `EchoTypeChecker`, `TropicalTypeChecker` | `typed_wasm::TypedWasmBackend::for_kind` |
+
+Both routes exist on `main`. None of the 41 enum variants falls
+through to "unsupported".
+
+### Test infrastructure
+
+`tests/common/mod.rs:114`, `:185`, `:245` already special-case
+`k.is_hp_ecosystem()` for executable / args / default-binary resolution
+in the prover-smoke harness. `tests/gnn_augment_integration.rs:545`
+covers `test_hp_ecosystem_gnn_wires_top_premise`.
+
+## What is genuinely outstanding for these backends
+
+The audit's underlying intuition (estate proof work won't run end-to-end
+on these provers) is correct — but the gap is downstream of the
+scaffold, not the scaffold itself:
+
+1. **Upstream binaries are not packaged.** `typell`, `katagoria`, and
+   `tropical-type-check` are referenced from `hp_ecosystem.rs::upstream()`
+   but none of them ship in any of echidna's Containerfiles or the
+   Guix manifest. `manifests/live-provers.scm` covers Z3, CVC5, Lean4,
+   Coq, Agda, Isabelle, Idris2, F*, Dafny, TLAPS — the HP triad is
+   absent. A live CI run can compile and dispatch but the subprocess
+   exits with "binary not found".
+
+2. **No smoke fixture for the three named provers.** `tests/chapel_fixtures/`
+   has `coq_trivial.v` and `lean_trivial.lean`; there is no equivalent
+   `echo_trivial.tll`, `tropical_trivial.tll`, or `katagoria_trivial.k`.
+   This PR adds the minimum three.
+
+3. **No discoverability for "how do I add a new HP discipline."**
+   Adding a discipline today means editing the 39-arm match in
+   `hp_ecosystem.rs::upstream()`, the 41-arm match in
+   `ProverFactory::create`, and matching arms in `is_hp_ecosystem()`
+   and `default_executable()`. There is no documented onboarding flow.
+
+## What this PR delivers
+
+- This correction memo (`docs/handover/B7-AUDIT-CORRECTION.md`).
+- Three smoke fixtures (`tests/fixtures/hp/`):
+  - `echo_trivial.tll`         — discipline `echo`, single identity goal.
+  - `tropical_trivial.tll`     — discipline `tropical`, resource-aware identity.
+  - `katagoria_trivial.k`      — discipline `verify`, single isomorphism.
+- A short onboarding doc (`docs/HP-BACKEND-ONBOARDING.md`) listing the
+  ~4 files an author must touch to add a new HP discipline, with line
+  references.
+
+What it does **not** deliver:
+
+- The upstream `typell` / `katagoria` / `tropical-type-check` binaries
+  (those live in `developer-ecosystem/katagoria`,
+  `verification-ecosystem/tropical-resource-typing`, and
+  `verification-ecosystem/typell` and are owner-managed).
+- A live CI run gate (that needs the binaries packaged first; see
+  the L3 path checklist in the D18 PR).
+- Per-discipline GNN training data extraction (TypeDiscipline Phase-2
+  deferred — audit item F26).
+
+## Cross-references
+
+- `docs/handover/TODO.md` P4 — Wave-4 + HP ecosystem expansion (now
+  partially superseded for the HP rows).
+- `docs/PROVER_COUNT.md` Tier-8 — canonical 41-variant inventory.
+- C12 PR (echidnabot manifest) — per-repo opt-in shape that consumers
+  using these backends will adopt.
+- D18 PR (L3 gate checklist) — packaging the upstream binaries is one
+  of the L3 → L1 hand-off criteria.

meta-checker/src/Echidna/AxiomSafety.agda

@@ -174,11 +174,20 @@ worst-comm Rejected IncompleteProof = refl
 worst-comm Rejected Rejected = refl
 
 -- THEOREM: worst-policy is associative
+-- NB: `worst-policy` splits on its FIRST argument, so `worst-policy x c` is
+-- stuck for a neutral `c` unless `x` reduces to the absorbing element
+-- `Rejected`. Clauses whose left fold collapses to `Rejected` may keep the
+-- `c` wildcard; the `IncompleteProof·IncompleteProof`, `ClassicalAxioms·
+-- IncompleteProof` and the whole `Clean` row do NOT collapse, so they must
+-- enumerate the remaining argument(s) concretely for `refl` to reduce.
 worst-assoc : ∀ (a b c : AxiomPolicy) →
   worst-policy (worst-policy a b) c ≡ worst-policy a (worst-policy b c)
 worst-assoc Rejected _ _ = refl
 worst-assoc IncompleteProof Rejected _ = refl
-worst-assoc IncompleteProof IncompleteProof _ = refl
+worst-assoc IncompleteProof IncompleteProof Rejected = refl
+worst-assoc IncompleteProof IncompleteProof IncompleteProof = refl
+worst-assoc IncompleteProof IncompleteProof ClassicalAxioms = refl
+worst-assoc IncompleteProof IncompleteProof Clean = refl
 worst-assoc IncompleteProof ClassicalAxioms Rejected = refl
 worst-assoc IncompleteProof ClassicalAxioms IncompleteProof = refl
 worst-assoc IncompleteProof ClassicalAxioms ClassicalAxioms = refl
@@ -188,7 +197,10 @@ worst-assoc IncompleteProof Clean IncompleteProof = refl
 worst-assoc IncompleteProof Clean ClassicalAxioms = refl
 worst-assoc IncompleteProof Clean Clean = refl
 worst-assoc ClassicalAxioms Rejected _ = refl
-worst-assoc ClassicalAxioms IncompleteProof _ = refl
+worst-assoc ClassicalAxioms IncompleteProof Rejected = refl
+worst-assoc ClassicalAxioms IncompleteProof IncompleteProof = refl
+worst-assoc ClassicalAxioms IncompleteProof ClassicalAxioms = refl
+worst-assoc ClassicalAxioms IncompleteProof Clean = refl
 worst-assoc ClassicalAxioms ClassicalAxioms Rejected = refl
 worst-assoc ClassicalAxioms ClassicalAxioms IncompleteProof = refl
 worst-assoc ClassicalAxioms ClassicalAxioms ClassicalAxioms = refl
@@ -197,7 +209,22 @@ worst-assoc ClassicalAxioms Clean Rejected = refl
 worst-assoc ClassicalAxioms Clean IncompleteProof = refl
 worst-assoc ClassicalAxioms Clean ClassicalAxioms = refl
 worst-assoc ClassicalAxioms Clean Clean = refl
-worst-assoc Clean b c = refl
+worst-assoc Clean Rejected Rejected = refl
+worst-assoc Clean Rejected IncompleteProof = refl
+worst-assoc Clean Rejected ClassicalAxioms = refl
+worst-assoc Clean Rejected Clean = refl
+worst-assoc Clean IncompleteProof Rejected = refl
+worst-assoc Clean IncompleteProof IncompleteProof = refl
+worst-assoc Clean IncompleteProof ClassicalAxioms = refl
+worst-assoc Clean IncompleteProof Clean = refl
+worst-assoc Clean ClassicalAxioms Rejected = refl
+worst-assoc Clean ClassicalAxioms IncompleteProof = refl
+worst-assoc Clean ClassicalAxioms ClassicalAxioms = refl
+worst-assoc Clean ClassicalAxioms Clean = refl
+worst-assoc Clean Clean Rejected = refl
+worst-assoc Clean Clean IncompleteProof = refl
+worst-assoc Clean Clean ClassicalAxioms = refl
+worst-assoc Clean Clean Clean = refl
 
 ------------------------------------------------------------------------
 -- CRITICAL: Comment-skipping soundness