Skip to content

Commit 0d27d43

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs(handover): correct B7 audit claim + add HP smoke fixtures + onboarding doc
The 2026-06-03 estate-audit punch list characterised B7 as "HP type-checker ecosystem (13 provers) corpus-only — Rust adapters not scaffolded in src/rust/provers/." That is incorrect. Verified state of the tree (2026-06-03): * src/rust/provers/hp_ecosystem.rs:50-153 — HPEcosystemBackend, a full ProverBackend impl that pattern-matches on ProverKind to select typell / katagoria / tropical-type-check + a discipline tag; implements parse_file / parse_string / apply_tactic / verify_proof. * src/rust/provers/mod.rs:1774-1824 — ProverFactory::create routes TypeLL + KatagoriaVerifier through HPEcosystemBackend, and 39 other *TypeChecker variants (incl. Echo + Tropical) through TypedWasmBackend::for_kind. * tests/common/mod.rs:114/185/245 + tests/gnn_augment_integration.rs:545 already cover HP-ecosystem kinds via is_hp_ecosystem() dispatch. So the backends exist and are wired. What is actually outstanding for estate-scale dispatch on these provers is downstream of the scaffold: 1. Upstream binaries (typell, katagoria, tropical-type-check) are not packaged in any Containerfile / manifests/live-provers.scm — a CI run gets "binary not found" rather than a verify result. 2. No smoke fixtures for the three Tier-8-canonical provers (echo / tropical / katagoria) — this PR adds them. 3. No documented onboarding flow for new HP disciplines, even though the pattern is mechanical and touches ~4 files. This PR delivers what is contained-scope: * docs/handover/B7-AUDIT-CORRECTION.md — correction memo with the file:line evidence above. * tests/fixtures/hp/echo_trivial.tll * tests/fixtures/hp/tropical_trivial.tll * tests/fixtures/hp/katagoria_trivial.k (three minimal smoke fixtures, single identity / refl goal each). * docs/HP-BACKEND-ONBOARDING.md — step-by-step checklist for adding a new HP discipline, with line references into the 4 files an author must touch. Out of scope (deferred to other audit items): * Packaging the upstream binaries — that's part of L3 → L1 hand-off criteria in the D18 PR. * Per-discipline GNN training extraction — that's the deferred TypeDiscipline Phase-2 work (audit item F26). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent bd83308 commit 0d27d43

5 files changed

Lines changed: 296 additions & 0 deletions

File tree

‎docs/HP-BACKEND-ONBOARDING.md‎

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,151 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
6+
# Onboarding a new HP type-discipline backend
7+
8+
This is the working checklist for adding a new HP-ecosystem type
9+
discipline to echidna. The 41 existing variants (TypeLL,
10+
KatagoriaVerifier, TropicalTypeChecker, EchoTypeChecker, ...) all
11+
followed this same pattern.
12+
13+
For background on what already exists, see
14+
`docs/handover/B7-AUDIT-CORRECTION.md`.
15+
16+
## Where the wiring lives
17+
18+
Adding a new discipline `Foo` (i.e. `ProverKind::FooTypeChecker`)
19+
touches exactly four files:
20+
21+
| File | What to add |
22+
|-------------------------------------------------|-------------------------------------------------------------------|
23+
| `src/rust/provers/mod.rs` | Enum variant + parser arm + is_hp_ecosystem + default_executable |
24+
| `src/rust/provers/hp_ecosystem.rs::upstream()` | One match arm: `Foo => ("typell", "foo")` |
25+
| `src/rust/provers/typed_wasm.rs::type_info_for` | `TypeInfo` selector for the discipline (the typed_wasm route) |
26+
| `tests/fixtures/hp/foo_trivial.tll` | One smoke fixture exercising the new wire |
27+
28+
If the discipline ships its own CLI (i.e. not `typell --discipline=foo`
29+
but a standalone binary), it routes through `HPEcosystemBackend` and
30+
the `upstream()` arm returns `("foo-cli", "foo")`. If it lives under
31+
`typell`, it routes through `TypedWasmBackend` via the discipline
32+
parameter.
33+
34+
The deciding question: **does the upstream maintainer ship a separate
35+
binary?** Examples:
36+
37+
- `KatagoriaVerifier` → standalone `katagoria` binary → `HPEcosystemBackend`.
38+
- `TropicalTypeChecker` → standalone `tropical-type-check` binary → either path (currently `TypedWasmBackend`).
39+
- `EchoTypeChecker` → bundled under `typell` → `TypedWasmBackend`.
40+
41+
## Step-by-step
42+
43+
### 1. Add the enum variant
44+
45+
`src/rust/provers/mod.rs`, in the `ProverKind` enum (around line 294):
46+
47+
```rust
48+
pub enum ProverKind {
49+
// ...
50+
FooTypeChecker,
51+
// ...
52+
}
53+
```
54+
55+
### 2. Parser arm
56+
57+
Same file, around line 567 (the string-to-ProverKind parser):
58+
59+
```rust
60+
"footypechecker" | "foo" => Ok(ProverKind::FooTypeChecker),
61+
```
62+
63+
### 3. `is_hp_ecosystem` arm
64+
65+
Same file, around line 434:
66+
67+
```rust
68+
pub fn is_hp_ecosystem(&self) -> bool {
69+
matches!(self,
70+
// ...
71+
| ProverKind::FooTypeChecker
72+
)
73+
}
74+
```
75+
76+
### 4. `default_executable` arm
77+
78+
Same file, around line 1360. Either:
79+
80+
```rust
81+
ProverKind::FooTypeChecker => "typell", // bundled
82+
// or
83+
ProverKind::FooTypeChecker => "foo-cli", // standalone
84+
```
85+
86+
### 5. Factory routing arm
87+
88+
Same file, `ProverFactory::create` (around line 1822). Add to the
89+
appropriate match arm:
90+
91+
- Standalone binary: add to the `HPEcosystemBackend` arm at line
92+
1776-1778.
93+
- Bundled discipline: add to the `TypedWasmBackend` arm at lines
94+
1784-1822.
95+
96+
### 6. (Bundled discipline only) `upstream()` arm
97+
98+
`src/rust/provers/hp_ecosystem.rs`, the `upstream()` match around
99+
line 63:
100+
101+
```rust
102+
ProverKind::FooTypeChecker => ("typell", "foo"),
103+
```
104+
105+
### 7. `TypeInfo` selector
106+
107+
`src/rust/provers/typed_wasm.rs::type_info_for` — return the discipline's
108+
parametric `TypeInfo` so the unified verifier knows what to check.
109+
110+
### 8. Smoke fixture
111+
112+
`tests/fixtures/hp/foo_trivial.tll`:
113+
114+
```
115+
# SPDX-License-Identifier: MPL-2.0
116+
#discipline: foo
117+
118+
theorem foo_identity : ... .
119+
Proof.
120+
foo_refl.
121+
Qed.
122+
```
123+
124+
### 9. Run the smoke
125+
126+
`tests/gnn_augment_integration.rs::test_hp_ecosystem_gnn_wires_top_premise`
127+
already loops over `is_hp_ecosystem()` kinds, so the new variant gets
128+
GNN-wiring coverage for free. A direct backend smoke takes one more
129+
line in `tests/common/mod.rs` if you want it.
130+
131+
## What you DON'T need to touch
132+
133+
- **Confidence levels** — the trust bridge reads
134+
`is_hp_ecosystem()` once; no per-discipline tuning.
135+
- **Corpus extractors** — the HP corpus is built by
136+
`crates/typed_wasm` and indexed by Sigma parameters; new disciplines
137+
inherit the existing pipeline.
138+
- **Result formatter** — `result_formatter.rs` reads `ProverKind`
139+
via Display; the variant name is the user-facing label.
140+
141+
## When the upstream binary doesn't ship
142+
143+
For early-development disciplines where the upstream tool isn't yet
144+
buildable (e.g. an unreleased Wokelang variant), the backend will
145+
return a "binary not found" runtime error. That is the right
146+
behaviour — echidna's trust bridge surfaces it as
147+
`ProverOutcome::Unsupported` and the caller sees a clear signal.
148+
149+
Do **not** stub the backend to return spurious success. Estate
150+
consumers (per the C12 per-repo manifest) configure `[provers]
151+
disabled = ["foo"]` to opt out cleanly.

‎docs/handover/B7-AUDIT-CORRECTION.md‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
6+
# B7 audit correction — HP ecosystem backends are NOT corpus-only
7+
8+
**Status**: Correction.
9+
**Origin**: The 2026-06-03 "what stops echidna from running proof work
10+
across the estate" punch list listed **B7** as:
11+
12+
> _HP type-checker ecosystem (13 provers) corpus-only — KatagoriaVerifier,
13+
> Modal/Session/Choreographic/Epistemic/Refinement/Echo/Dependent/QTT/
14+
> Effect-Row/Tropical/TypeLL backends missing. Rust adapters not
15+
> scaffolded in `src/rust/provers/`. Corpus contributes to vocab/training
16+
> only._
17+
18+
That characterisation is incorrect. This memo replaces B7's "scaffold
19+
missing adapters" framing with what is actually missing.
20+
21+
## What is actually in tree (verified 2026-06-03)
22+
23+
### Unified `HPEcosystemBackend`
24+
25+
`src/rust/provers/hp_ecosystem.rs:50-153` defines
26+
`HPEcosystemBackend`, a full `ProverBackend` implementation that:
27+
28+
- Pattern-matches on `ProverKind` to select the upstream CLI
29+
(`typell`, `katagoria`, `tropical-type-check`) and discipline tag
30+
(`echo`, `session`, `qtt`, `effect-row`, ...) — see
31+
`hp_ecosystem.rs::upstream()` lines 63-126.
32+
- Implements `parse_file`, `parse_string`, `apply_tactic`, and
33+
`verify_proof` against the upstream binary — lines 156-330.
34+
- Injects a `#discipline:` header when the source lacks one (lines
35+
196-205), so estate consumers don't need to know the wire format.
36+
37+
### Routing in `ProverFactory::create`
38+
39+
`src/rust/provers/mod.rs:1774-1824` routes:
40+
41+
| ProverKind | Backend |
42+
|-------------------------------------------------------|--------------------------------------------------|
43+
| `TypeLL`, `KatagoriaVerifier` | `hp_ecosystem::HPEcosystemBackend` |
44+
| 39 other `*TypeChecker` variants incl. `EchoTypeChecker`, `TropicalTypeChecker` | `typed_wasm::TypedWasmBackend::for_kind` |
45+
46+
Both routes exist on `main`. None of the 41 enum variants falls
47+
through to "unsupported".
48+
49+
### Test infrastructure
50+
51+
`tests/common/mod.rs:114`, `:185`, `:245` already special-case
52+
`k.is_hp_ecosystem()` for executable / args / default-binary resolution
53+
in the prover-smoke harness. `tests/gnn_augment_integration.rs:545`
54+
covers `test_hp_ecosystem_gnn_wires_top_premise`.
55+
56+
## What is genuinely outstanding for these backends
57+
58+
The audit's underlying intuition (estate proof work won't run end-to-end
59+
on these provers) is correct — but the gap is downstream of the
60+
scaffold, not the scaffold itself:
61+
62+
1. **Upstream binaries are not packaged.** `typell`, `katagoria`, and
63+
`tropical-type-check` are referenced from `hp_ecosystem.rs::upstream()`
64+
but none of them ship in any of echidna's Containerfiles or the
65+
Guix manifest. `manifests/live-provers.scm` covers Z3, CVC5, Lean4,
66+
Coq, Agda, Isabelle, Idris2, F*, Dafny, TLAPS — the HP triad is
67+
absent. A live CI run can compile and dispatch but the subprocess
68+
exits with "binary not found".
69+
70+
2. **No smoke fixture for the three named provers.** `tests/chapel_fixtures/`
71+
has `coq_trivial.v` and `lean_trivial.lean`; there is no equivalent
72+
`echo_trivial.tll`, `tropical_trivial.tll`, or `katagoria_trivial.k`.
73+
This PR adds the minimum three.
74+
75+
3. **No discoverability for "how do I add a new HP discipline."**
76+
Adding a discipline today means editing the 39-arm match in
77+
`hp_ecosystem.rs::upstream()`, the 41-arm match in
78+
`ProverFactory::create`, and matching arms in `is_hp_ecosystem()`
79+
and `default_executable()`. There is no documented onboarding flow.
80+
81+
## What this PR delivers
82+
83+
- This correction memo (`docs/handover/B7-AUDIT-CORRECTION.md`).
84+
- Three smoke fixtures (`tests/fixtures/hp/`):
85+
- `echo_trivial.tll` — discipline `echo`, single identity goal.
86+
- `tropical_trivial.tll` — discipline `tropical`, resource-aware identity.
87+
- `katagoria_trivial.k` — discipline `verify`, single isomorphism.
88+
- A short onboarding doc (`docs/HP-BACKEND-ONBOARDING.md`) listing the
89+
~4 files an author must touch to add a new HP discipline, with line
90+
references.
91+
92+
What it does **not** deliver:
93+
94+
- The upstream `typell` / `katagoria` / `tropical-type-check` binaries
95+
(those live in `developer-ecosystem/katagoria`,
96+
`verification-ecosystem/tropical-resource-typing`, and
97+
`verification-ecosystem/typell` and are owner-managed).
98+
- A live CI run gate (that needs the binaries packaged first; see
99+
the L3 path checklist in the D18 PR).
100+
- Per-discipline GNN training data extraction (TypeDiscipline Phase-2
101+
deferred — audit item F26).
102+
103+
## Cross-references
104+
105+
- `docs/handover/TODO.md` P4 — Wave-4 + HP ecosystem expansion (now
106+
partially superseded for the HP rows).
107+
- `docs/PROVER_COUNT.md` Tier-8 — canonical 41-variant inventory.
108+
- C12 PR (echidnabot manifest) — per-repo opt-in shape that consumers
109+
using these backends will adopt.
110+
- D18 PR (L3 gate checklist) — packaging the upstream binaries is one
111+
of the L3 → L1 hand-off criteria.

‎tests/fixtures/hp/echo_trivial.tll‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
#discipline: echo
3+
#
4+
# Smoke fixture: echo type-discipline single-goal identity.
5+
# Exercises HPEcosystemBackend with ProverKind::EchoTypeChecker.
6+
# The L3 (echo) obligation reduces to its own type — the simplest
7+
# possible witness that the backend wiring round-trips.
8+
9+
theorem echo_identity : forall (A : EchoType), A |- A.
10+
Proof.
11+
echo_refl.
12+
Qed.

‎tests/fixtures/hp/katagoria_trivial.k‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// discipline: verify
3+
//
4+
// Smoke fixture: katagoria categorical-isomorphism single-goal.
5+
// Exercises HPEcosystemBackend with ProverKind::KatagoriaVerifier.
6+
// The trivial isomorphism A ≅ A reduces by identity functor; smallest
7+
// possible witness that the verifier wiring round-trips.
8+
9+
theorem id_isomorphism (A : Object) : A ≅ A := by
10+
refl

‎tests/fixtures/hp/tropical_trivial.tll‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
#discipline: tropical
3+
#
4+
# Smoke fixture: tropical resource-typing single-goal identity.
5+
# Exercises TypedWasmBackend with ProverKind::TropicalTypeChecker.
6+
# Cost = 0 (additive identity in the tropical semiring); type checks
7+
# trivially under the standard resource-tracking judgement.
8+
9+
theorem tropical_zero_cost : forall (A : TropicalType[cost=0]), A |- A.
10+
Proof.
11+
tropical_refl.
12+
Qed.

0 commit comments

Comments
 (0)