Skip to content

Commit f18d85f

Browse files
committed
feat(s3): extract typed_wasm engine + route 39 disciplines through TypeInfo
The TypedWasm prover oracle is now a standalone crate at crates/typed_wasm with zero echidna-core dependencies. The pure parse/analyse engine is parametrised by a TypeInfo value, so the 39 *TypeChecker variants all route through one backend with discipline-specific active-level sets, replacing the catch-all HPEcosystemBackend route. - crates/typed_wasm/src/lib.rs: pure engine (parse + obligation generation + TypeInfo + analyse). 9 crate-level tests covering the level-filter semantics and the discipline-aware analysis flow. - Cargo.toml: crates/typed_wasm added to [workspace].members; typed-wasm added as a path dependency. - src/rust/provers/typed_wasm.rs: rewritten as a thin adapter that maps typed_wasm::Analysis onto echidna's core ProofState/Goal types. Adds TypedWasmBackend::with_type_info and ::for_kind constructors, plus a type_info_for(kind) helper that maps each *TypeChecker variant to its discipline's active safety-level set (linear, affine, modal, temporal, refinement, session, …). TypedWasmBackend::new preserved for the legacy full-oracle callers. - src/rust/provers/mod.rs: ProverFactory::create now routes the 39 *TypeChecker variants through TypedWasmBackend::for_kind. TypeLL and KatagoriaVerifier continue to dispatch through HPEcosystemBackend as genuine HP upstream binaries. Tests: 9/9 crate + 10/10 adapter + 625/625 echidna lib pass. https://claude.ai/code/session_01NaC5RXjTyr5xg9XXUa2FCC
1 parent 1b3a0e9 commit f18d85f

5 files changed

Lines changed: 1296 additions & 1089 deletions

File tree

Cargo.lock

Lines changed: 8 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,12 @@ chrono = { version = "0.4", features = ["serde"] }
7676
# Temporary files (used by prover backends to invoke external solvers)
7777
tempfile = "3"
7878

79+
# TypedWasm engine — standalone crate at crates/typed_wasm.
80+
# Provides the pure parse/analyse engine; provers/typed_wasm.rs is a thin
81+
# adapter that maps its `Analysis` onto echidna core types, and routes the
82+
# 39 *TypeChecker discipline variants through discipline-specific TypeInfo.
83+
typed-wasm = { path = "crates/typed_wasm" }
84+
7985
[features]
8086
default = []
8187
chapel = [] # Enable Chapel parallel proof search (requires Zig FFI library)
@@ -106,6 +112,7 @@ harness = false
106112

107113
[workspace]
108114
members = [
115+
"crates/typed_wasm",
109116
"src/interfaces/graphql",
110117
"src/interfaces/grpc",
111118
"src/interfaces/rest",

0 commit comments

Comments
 (0)