Skip to content

Commit 74e0504

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Claude/fix prover wiring epy ir (#29)
Co-authored-by: Claude <noreply@anthropic.com>
1 parent 207716c commit 74e0504

56 files changed

Lines changed: 1081 additions & 1370 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.claude/CLAUDE.md‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,70 @@ The following files in `.machine_readable/` contain structured project metadata:
1010
- `.machine_readable/6a2/PLAYBOOK.a2ml` - Operational runbook
1111
- `.machine_readable/bot_directives/*.a2ml` - Per-bot permission and scope rules
1212

13+
## Canonical Roadmap
14+
15+
See [`docs/ROADMAP.md`](../docs/ROADMAP.md) for the single source of truth on
16+
where ECHIDNA is going: the 8‑stage map, row‑by‑row endpoint targets,
17+
current sprint (S1–S5), and agent‑tier guidance. Record decisions
18+
there, not in chat.
19+
20+
## Supervised Multi-Agent Execution
21+
22+
When a supervising agent (Opus) plans work that will be implemented by
23+
a focused executor (Sonnet) or a mechanical bulk agent (Haiku), the
24+
supervisor MUST run a **Haiku scout pass** immediately before spawning
25+
the implementation agent, unless the scope is strictly single‑file
26+
and under ten lines of change.
27+
28+
### Scout pattern
29+
30+
**Purpose**: clear obvious cruft (unused imports, stale comments,
31+
dead stubs, broken references) so the implementation agent arrives
32+
to clean ground and does not burn tokens on trivial lint.
33+
34+
**When to run**: once per upcoming step, after the step's scope is
35+
locked and before the implementation agent is launched.
36+
37+
**Prompt template** (copy this verbatim, fill in the file list):
38+
39+
```
40+
Haiku scout, scope = <exact file list for the step>
41+
42+
1. Confirm each file compiles in isolation (cargo check --lib / julia -e).
43+
2. Scan for: unused imports, dead code, `todo!()/FIXME/XXX`,
44+
orphan type references, stale doc comments referring to
45+
renamed symbols, broken `mod.rs` exports.
46+
3. Trivially fix:
47+
- unused imports (remove)
48+
- obvious typos in comments
49+
- unused `_var` renames
50+
4. DO NOT fix — FLAG to me:
51+
- any TODO with semantic content (may be load-bearing)
52+
- anything requiring judgement about intent
53+
- any cross-module change
54+
5. Report: <20 lines. Green-light or list of blockers.
55+
```
56+
57+
**Caveats**:
58+
59+
- Scout is **not** a full audit. Full audits remain the periodic
60+
cross‑module sweep (cf. the Agent A + Agent B pattern in session
61+
history); scout is narrow prep for an imminent step.
62+
- Scout must **not over‑fix**. TODO/FIXME comments sometimes
63+
contain the spec for the upcoming work — flag, don't delete.
64+
- Scout is **idempotent**. Re‑running on unchanged code should
65+
produce the same report.
66+
- If scout flags a blocker, the supervisor decides whether to
67+
resolve it inline, expand the step's scope, or defer. The
68+
implementation agent does not launch until the supervisor
69+
green‑lights.
70+
71+
**Commit convention** (when the scout applied trivial fixes):
72+
73+
```
74+
chore(<scope>): scout-pass trivial cleanup ahead of <step id>
75+
```
76+
1377
### CRITICAL: .scm metadata files are DEPRECATED
1478

1579
**All `.scm` state/metadata files have been replaced by `.a2ml`.**

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,3 +193,6 @@ deps/
193193
.cache/
194194
build/
195195
dist/
196+
197+
# Subagent worktrees (isolation mode)
198+
.claude/worktrees/

‎crates/typed_wasm/Cargo.toml‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
3+
[package]
4+
name = "typed-wasm"
5+
version = "0.1.0"
6+
edition = "2021"
7+
authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
8+
license = "PMPL-1.0-or-later"
9+
description = "TypedWasm prover oracle engine for ECHIDNA — standalone domain types and engine"
10+
repository = "https://github.com/hyperpolymath/echidna"
11+
12+
[dependencies]
13+
anyhow = "1"
14+
async-trait = "0.1"
15+
tokio = { version = "1", features = ["full"] }
16+
serde = { version = "1", features = ["derive"] }
17+
serde_json = "1"

‎docs/ROADMAP.md‎

Lines changed: 192 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,192 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
4+
# ECHIDNA Roadmap
5+
6+
**Status**: canonical • supersedes the aspirational parts of
7+
[`FUTURE_DEVELOPMENT_ROADMAP.md`](./FUTURE_DEVELOPMENT_ROADMAP.md).
8+
**Last revised**: 2026‑04‑20
9+
**Scope**: the shortest honest path from today's repo to the endpoint vision.
10+
11+
This document is the single source of truth for where ECHIDNA is going.
12+
The domain‑specific plans under [`handover/`](./handover/) and
13+
[`design/SPARK_ADOPTION_PLAN.md`](./design/SPARK_ADOPTION_PLAN.md) are
14+
still authoritative for their sub‑areas; they fit *inside* this
15+
roadmap as implementations of individual stages.
16+
17+
## 1. Endpoint
18+
19+
ECHIDNA, when complete, is the **reasoning substrate of the
20+
hyperpolymath ecosystem** — not just a proof tool. It is:
21+
22+
* a unified interface to every mature theorem prover, SMT solver,
23+
model checker, and type checker in public use;
24+
* an ML layer (GNN + Transformer over Flux.jl) that actually learns
25+
premise selection, tactic synthesis, and strategy routing well
26+
enough to beat hand‑curated choices on held‑out theorems;
27+
* a persistent E‑R layer (Verisim) that stores every proof, tactic
28+
application, and version as a content‑addressed row and closes a
29+
real learning loop over historical outcomes;
30+
* a parallel dispatch layer (Chapel) that runs portfolio solves
31+
across CPU cores and dispatches specialised work to coprocessors
32+
(GPU / tensor / vector / FPGA / QPU);
33+
* a high‑speed IPC fabric (Cap'n Proto) between the Rust core and
34+
the Julia ML sidecar and between the backend and the frontend;
35+
* a frontend in AffineScript + Deno (TEA architecture) with i18n via
36+
the LOL locale repo;
37+
* a 16‑endpoint Zig ABI that external consumers (Coursera labs,
38+
other projects) link against, with an SPDX‑pinned, Guix‑built,
39+
Chainguard‑based container managed by Stapeln and hardened by the
40+
Vordr / Selur / Svalinn / Cerro‑Torre surround;
41+
* itself formally verified — the trust kernel's critical invariants
42+
are proved in SPARK and in Idris2 / Agda.
43+
44+
From a user's seat: **indistinguishable from magic for easy
45+
obligations, honest about ambiguity for hard ones, never silently
46+
wrong.**
47+
48+
## 2. Stage map
49+
50+
```
51+
Stage 1 Train the model at all ML layer can receive signal
52+
1a extractors emit premises [done 2026‑04‑20, 22 of 50 ✓]
53+
1b align_premises joins correctly [done 2026‑04‑19 ✓]
54+
1c residual extractor gaps fixed [in progress, 28 to go]
55+
1d vocab covers the surface [255 K; target ~1 M]
56+
57+
Stage 2 Signal becomes useful MRR moves off 0.66 baseline
58+
2a run training at scale hardware task
59+
2b online vocab growth new feature
60+
2c re‑baseline and publish metrics run gate
61+
62+
Stage 3 Learning loop closes model improves from outcomes
63+
3a Verisim read paths cross‑prover queries by goal_hash
64+
3b hypatia strategy loop wired `mv_prover_success_by_class` reads
65+
3c Proof / TacticApplication / ProofVersion emission wired
66+
[defined 2026‑04‑19 ✓, emission pending]
67+
68+
Stage 4 Interaction layer honest every declared ProverKind works
69+
4a typed_wasm → crates/typed_wasm extract to standalone crate
70+
4b 40 TypeChecker variant dispatch Sigma‑route via the crate
71+
4c tactic synthesis template 37 suggest_tactics stubs replaced
72+
4d search_theorems template 49 stubs replaced, query Verisim
73+
74+
Stage 5 Distributed & fast scale + specialised hardware
75+
5a Cap'n Proto IPC Rust ↔ Julia, :8090
76+
5b Chapel full integration dispatch.rs picks by config
77+
5c coprocessor abstraction trait + tensor/vector/QPU/FPGA
78+
5d Tier‑4 live‑CI provisioning 19 backends, Containerfile path
79+
80+
Stage 6 Cross‑prover semantics translation actually works
81+
6a OpenTheory bridge real bidirectional term translation
82+
6b Dedukti bridge real λΠ modulo as lingua franca
83+
6c mathematical identity arbitration canonicalise across representations
84+
6d Coursera delivery Zig ABI exposes capability
85+
86+
Stage 7 Sovereign tooling surround the rest of the ecosystem
87+
7a Stapeln container lifecycle
88+
7b Vordr entry gate
89+
7c Selur scheduler
90+
7d Svalinn trust boundary
91+
7e Cerro‑Torre observability
92+
7f AffineScript‑TEA frontend src/rescript/, ≥33 modules
93+
7g LOL i18n locale/ + t!() macro
94+
7h Zig ABI 16‑endpoint surface src/zig/echidna_abi.zig
95+
96+
Stage 8 Self‑verified ECHIDNA proves ECHIDNA
97+
8a Idris2 meta‑proofs extend from 32 modules to full kernel
98+
8b Agda meta‑proofs extend from 12 modules
99+
8c SPARK‑verified trust kernel crates/echidna-core-spark/
100+
8d panic‑attack hardened proptest + AFL++ nightly
101+
```
102+
103+
## 3. Endpoint target — row by row
104+
105+
| Claim | Today | End‑state target |
106+
|---|---|---|
107+
| "Every important solver" | 59 backends; 37 `suggest_tactics` stubs; 49 `search_theorems` stubs | **65 backends, every one with real `suggest_tactics` (GNN‑ranked top‑k) and `search_theorems` (queries Verisim by `goal_hash`) — no `Ok(vec![])` returns anywhere** |
108+
| "Vocab at 2.5 M" | 255 K | **~1 M canonical tokens** after Mathport + Iris + VST + Flyspeck + HoTT absorption, with **online growth** adding tokens during training |
109+
| "Chapel fully supported" | 2 files, POC only | **`dispatch.rs` picks Chapel‑parallel dispatch by config**; runtime init + cancellation + error propagation wired; ≥1 OoM speedup on portfolio solves |
110+
| "Cap'n Proto serialisation" | 0 `.capnp` files | **`crates/echidna-wire/`** contains schemas for ProofState / Goal / Tactic / EmbeddingRequest / RankingResponse; IPC on :8090 is Cap'n Proto; JSON retained only as debug fallback |
111+
| "Vordr / Selur / Svalinn / Cerro‑Torre / Stapeln" | Not present | Each named as a versioned dependency in Cargo.toml or the container definition, wired into its role |
112+
| "AffineScript‑TEA frontend" | Not present (10 `.res` files stub) | **`src/rescript/`** holds ≥33 AffineScript‑TEA modules, persistent Model → Msg → Update loop, talks to core over Cap'n Proto WebSocket |
113+
| "LOL i18n" | Not present | **`locale/`** with LOL‑sourced translations; `t!()` macro for every user‑facing string |
114+
| "Rust/SPARK base stable" | Rust only | **`crates/echidna-core-spark/`** holds the Ada/SPARK‑verified kernel (axiom scanning, trust‑level computation); proved free of runtime errors; called from Rust via C ABI |
115+
| "16‑endpoint Zig ABI" | 4 shared libs, endpoint count unverified | **`src/zig/echidna_abi.zig`** exports exactly 16 functions (`echidna_prove`, `echidna_apply_tactic`, `echidna_rank_premises`, `echidna_verify_certificate`, `echidna_post_octad`, `echidna_query_identity`, …) with a versioned header |
116+
| "100 K+ per prover" | Uneven; long tail <20 K | **Top 15 provers ≥ 100 K records each**; next 20 ≥ 25 K each; bottom 10 synthetically augmented to ≥ 10 K; `stats_UNIFIED.json` reports the distribution publicly |
117+
| "Panic‑attacked" | No fuzz infra | **`benches/panic_attack/`** with proptest + AFL++ harnesses covering every parser, FFI boundary, IPC schema; nightly CI ≥ 1 h; zero known panic paths |
118+
| "Prover count" | 59 real, 105 declared | **`ProverKind` = 65 variants, every one factory‑dispatched**; CLAUDE.md states the canonical count; no orphans |
119+
120+
## 4. Current sprint — "the smallest set that flips half the table"
121+
122+
Five concrete commitments. Landed together inside ~6 weeks they move
123+
"Every important solver", "Vocab", "Prover count", half of "100 K+",
124+
and start the self‑learning loop closure.
125+
126+
| # | Stage | Commitment | Agent tier |
127+
|---|---|---|---|
128+
| S1 | 1c | Finish the extractor premise‑emission wave (22 done; 28 remaining) | **Sonnet** (in flight) |
129+
| S2 | 2a / 2c | Run training on the fixed corpus; record new MRR; commit `metrics_baseline.jsonl` | **Hardware / you** |
130+
| S3 | 4a / 4b | Extract `typed_wasm` to `crates/typed_wasm/`; route 40 TypeChecker variants through Sigma parameters | **Opus‑design + Sonnet‑impl** |
131+
| S4 | 3a / 3b | Wire Verisim cross‑prover read paths (`goal_hash` queries + `mv_prover_success_by_class` + hypatia loop) | **Opus‑design + Sonnet‑impl** |
132+
| S5 | 4c / 4d (pilot) | Tactic synthesis template for 5 high‑value provers (coq, lean, agda, isabelle, z3) using the GNN | **Opus‑design + Sonnet‑impl** |
133+
134+
After S1–S5 land, the roadmap's next sprint takes up Stage 5 (IPC +
135+
Chapel + Tier‑4 CI) and Stage 8 begins in parallel.
136+
137+
## 5. Agent‑tier guidance
138+
139+
**Opus** (supervisor): architecture, schema design, cross‑module
140+
contracts, merge review. Touches: IPC protocol design, Verisim
141+
schema additions, Chapel FFI shape, coprocessor trait, SPARK kernel
142+
surface.
143+
144+
**Sonnet** (executor): focused implementation against a clear spec,
145+
3–20 files, moderate complexity. Touches: per‑prover tactic
146+
synthesis, Verisim read client, typed_wasm crate extraction,
147+
adapter code, worker logic.
148+
149+
**Haiku** (bulk): template‑driven mechanical edits, CI YAML,
150+
deletes, repetitive stubs. Touches: Tier‑4 provisioning shell
151+
commands, extractor boilerplate, per‑prover factory branches that
152+
follow a mould, localisation key additions.
153+
154+
## 6. Inheritance from existing planning docs
155+
156+
* **[`docs/FUTURE_DEVELOPMENT_ROADMAP.md`](FUTURE_DEVELOPMENT_ROADMAP.md)**
157+
— 2026‑01‑29 vision document. Its chapters on RL for tactic
158+
search (§1.1), active learning (§1.2), and distributed dispatch
159+
map onto Stages 3c / 4c and 5b/5c of this roadmap. Retain as
160+
background reading; this document is the source of truth for
161+
sequencing.
162+
* **[`docs/handover/PRODUCTION-WIRING-PLAN.md`](handover/PRODUCTION-WIRING-PLAN.md)**
163+
— L1/L2/L3 sprint doc. L1 = Stage 5a. L2 = Stage 5b. L3 Wave‑1/2
164+
are complete (in Stage 4 surface); Wave‑3 is partially complete in
165+
this branch (tamarin/proverif/metamath/twelf/ortools); Wave‑4 is
166+
Stage 5d.
167+
* **[`docs/design/SPARK_ADOPTION_PLAN.md`](design/SPARK_ADOPTION_PLAN.md)**
168+
— design for the SPARK‑verified kernel. Executes Stage 8c.
169+
* **[`docs/handover/L1-CAPNPROTO-PROMPT.md`](handover/L1-CAPNPROTO-PROMPT.md)**
170+
— implementation brief for Stage 5a. Use as the Sonnet prompt
171+
when S6 begins.
172+
* **[`docs/handover/L2-CHAPEL-PROMPT.md`](handover/L2-CHAPEL-PROMPT.md)**
173+
— implementation brief for Stage 5b.
174+
* **[`docs/handover/L3-LIVE-PROVER-CI-PROMPT.md`](handover/L3-LIVE-PROVER-CI-PROMPT.md)**
175+
— implementation brief for Stage 5d.
176+
* **[`docs/handover/STATE.md`](handover/STATE.md)** and
177+
**[`.machine_readable/6a2/STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml)**
178+
— running log of session‑by‑session progress. Continue to use as
179+
running state; sync highlights to §2 of this document at each
180+
sprint boundary.
181+
182+
## 7. How to update this roadmap
183+
184+
* When a stage sub‑item lands, mark its line `[done YYYY‑MM‑DD ✓]`
185+
in §2 and update the corresponding row of §3.
186+
* When a new endpoint target emerges, add a row to §3, extend §2's
187+
stage map if it doesn't already fit, and add it to the sprint
188+
plan in §4 only once it's next‑up.
189+
* Don't remove rows from §3 when they land — keep the history
190+
visible, the "Today" column becomes "Done" and the "End‑state"
191+
column stays as the invariant.
192+
* Record non‑trivial decisions in this doc, not in chat.

‎scripts/extract_abc.jl‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,14 @@ function run_extract()
4343
"goal"=>"$(splitext(f)[2][2:end])_circuit size=$(sz)",
4444
"kind"=>splitext(f)[2][2:end],
4545
"context"=>Any[]))
46+
# Emit premises: identifiers from circuit filename stem
47+
stem = splitext(basename(f))[1]
48+
for hm in eachmatch(r"\b([a-zA-Z_][a-zA-Z0-9_]{1,40})\b", stem)
49+
h = strip(hm.captures[1])
50+
!isempty(h) && length(h) < 50 && push!(pm, Dict{String,Any}(
51+
"proof_id"=>id, "premise"=>h,
52+
"prover"=>"ABC", "theorem"=>basename(f), "source"=>"abc"))
53+
end
4654
id += 1
4755
catch e; println("Warning: $f: $e"); end
4856
end

‎scripts/extract_acl2.jl‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ const REPO_ROOT = dirname(dirname(abspath(@__FILE__)))
2626
const EXTERNAL_DIR = joinpath(REPO_ROOT, "external_corpora", "acl2")
2727
const OUTPUT_DIR = joinpath(REPO_ROOT, "training_data")
2828
const OUTPUT_FILE = joinpath(OUTPUT_DIR, "proof_states_acl2.jsonl")
29+
const PREMISES_FILE = joinpath(OUTPUT_DIR, "premises_acl2.jsonl")
2930
const STATS_FILE = joinpath(OUTPUT_DIR, "stats_acl2.json")
3031
const START_ID = 92000
3132

@@ -297,8 +298,17 @@ function run()::Tuple{Int,Int}
297298
end
298299
println(" Generated $added unique synthetic proofs")
299300

301+
# ACL2 premise patterns: :use hints, :in-theory enables, defthm names
302+
acl2_hyp_patterns = [
303+
r":use\s+\(?:?instance\s+([a-zA-Z0-9_-]+)",
304+
r":use\s+\(([a-zA-Z0-9_-]+)",
305+
r":in-theory\s+\(enable\s+([a-zA-Z0-9_\s-]+)\)",
306+
r"\(defthm\s+([a-zA-Z0-9_-]+)",
307+
]
308+
300309
current_id = START_ID
301310
output_records = Dict{String,Any}[]
311+
premises = Dict{String,Any}[]
302312
for entry in all_entries
303313
record = Dict{String,Any}(
304314
"id" => current_id,
@@ -310,6 +320,25 @@ function run()::Tuple{Int,Int}
310320
"source" => get(entry, "source", "acl2"),
311321
)
312322
push!(output_records, record)
323+
# Emit premise records from hints/tactic_proof
324+
proof_text = get(entry, "tactic_proof", "") * " " * string(get(entry, "hints", ""))
325+
thm_name = entry["theorem"]
326+
for hyp_pattern in acl2_hyp_patterns
327+
for hyp_match in eachmatch(hyp_pattern, proof_text)
328+
hyps = [strip(h) for h in split(hyp_match.captures[1], ' ')]
329+
for hyp in hyps
330+
if !isempty(hyp) && length(hyp) < 50
331+
push!(premises, Dict{String,Any}(
332+
"proof_id" => current_id,
333+
"premise" => String(hyp),
334+
"prover" => "ACL2",
335+
"theorem" => thm_name,
336+
"source" => get(entry, "source", "acl2"),
337+
))
338+
end
339+
end
340+
end
341+
end
313342
current_id += 1
314343
end
315344

@@ -318,6 +347,11 @@ function run()::Tuple{Int,Int}
318347
println(fh, JSON3.write(rec))
319348
end
320349
end
350+
open(PREMISES_FILE, "w") do fh
351+
for p in premises
352+
println(fh, JSON3.write(p))
353+
end
354+
end
321355

322356
stats = Dict{String,Any}(
323357
"prover" => "ACL2",

‎scripts/extract_acl2s.jl‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,13 @@ function extract_acl2s_proofs()
4848
"theorem" => name, "goal" => statement,
4949
"context" => Any[],
5050
))
51+
# Emit premises: ACL2s identifiers from theorem statement
52+
for hm in eachmatch(r"\b([a-zA-Z][a-zA-Z0-9_\-]{1,40})\b", statement)
53+
h = strip(hm.captures[1])
54+
!isempty(h) && length(h) < 50 && push!(premises, Dict{String,Any}(
55+
"proof_id"=>current_id, "premise"=>h,
56+
"prover"=>"ACL2s", "theorem"=>name, "source"=>"acl2s"))
57+
end
5158
current_id += 1
5259
end
5360
end

0 commit comments

Comments
 (0)