Skip to content

Commit c411739

Browse files
committed
docs(claude-md): sharpen v2.2+ status for Chapel FFI and GNN training
Explore-agent investigation found these are genuinely pending (unlike the Tamarin/ProVerif entry, which was stale doc). Replacing the vague one-liners with precise state so future agents don't rediscover the gap: - Chapel: Zig shim + Chapel POC ready behind --features chapel, 6/6 proof_search tests pass, but dispatch.rs still bypasses the ChapelParallelSearch strategy. 7 L2 sub-waves tracked in docs/handover/TODO.md, gated on L1 Cap'n Proto. - GNN training: Flux.jl declared, 9 files import it, ~1.4k LoC of training scaffolds exist, but never invoked on real data — models/neural/ is absent, metadata files read '0 words, 0 classes', inference falls back to cosine. Corpus ready (66,674 proofs, 553 MB).
1 parent 6f0c04b commit c411739

1 file changed

Lines changed: 26 additions & 8 deletions

File tree

CLAUDE.md

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -134,16 +134,34 @@ The v1.5 trust hardening added:
134134
- Idris2 formal proofs: 7 GNN properties (0 believe_me)
135135
- 28 new tests, 0 clippy warnings
136136

137-
**Next (v2.2+)**:
138-
- Train GNN/Transformer on larger corpus (Flux.jl)
139-
- Chapel → Rust C FFI bridge
137+
**Next (v2.2+)** (precise status):
138+
139+
- **Chapel → Rust C FFI bridge (L2, half-done)**. Zig shim
140+
(`src/zig_ffi/`, 738 LoC, 4 files) and Chapel POC (`src/chapel/`,
141+
970 LoC) in place behind `--features chapel`; `cargo build --features
142+
chapel` works standalone, 6/6 `proof_search` tests pass. The gap:
143+
`dispatch.rs` still bypasses the feature-gated `ChapelParallelSearch`
144+
strategy in `proof_search.rs`. Integration is split into 7 L2 sub-waves
145+
tracked in `docs/handover/TODO.md`, gated on L1 Cap'n Proto completion.
146+
Direct Rust↔Chapel today goes through Zig (no shortcut path).
147+
148+
- **Train GNN/Transformer on larger corpus (Flux.jl, scaffold-only)**.
149+
Flux.jl is declared in `src/julia/Project.toml` and imported across
150+
9 files; ~1.4k LoC of training scaffolds exist
151+
(`train_advanced_models.jl`, `training/train.jl`,
152+
`models/neural_solver.jl`). **Never invoked on real data**:
153+
`models/neural/` does not exist, `models/model_metadata.txt` reads
154+
`0 words, 0 classes`, and `src/julia/api/gnn_endpoint.jl:40-114`
155+
falls back to cosine similarity when no trained model is found.
156+
Corpus ready: `training_data/` 553 MB, 66,674 proofs / 179,933 tactics
157+
across 16 prover systems — untouched.
140158

141159
Note: Tamarin (`provers/tamarin.rs`, 596 LoC, 5 tests) and ProVerif
142-
(`provers/proverif.rs`, 800 LoC, 8 tests) are already shipped as real
143-
backends inside the 105 prover count — an earlier "v2.2+ Tamarin/ProVerif
144-
bridge" entry was stale doc. Corpus fixtures (`.spthy` / `.pv` samples)
145-
and CI provisioning of `tamarin-prover` / `proverif` binaries are tracked
146-
as Wave-3 work in `docs/handover/TODO.md`.
160+
(`provers/proverif.rs`, 800 LoC, 8 tests) were previously listed under
161+
v2.2+ as "bridge" work — in fact both are already shipped real backends
162+
inside the 105 prover count. Remaining Wave-3 work for these is corpus
163+
fixtures (`.spthy` / `.pv` samples) and CI provisioning of upstream
164+
binaries, tracked in `docs/handover/TODO.md`.
147165

148166
## Useful Commands
149167

0 commit comments

Comments
 (0)