purescript-mycroft-z3-wasm

The WASM backend for mycroft: the official z3-solver npm package (Z3 compiled to WebAssembly) behind the same Solver interface. No native binary, no subprocess — mycroft runs in Node today and in the browser tomorrow.

Mycroft.Solver.Z3Wasm exports two things:

newZ3WasmSolver :: { log :: Maybe (String -> Effect Unit) } -> Aff Solver
shutdownZ3Wasm  :: Aff Unit

The returned Solver is the ordinary mycroft session — everything in Mycroft.SmtLib (declareConst, assert/assertNamed, checkSat, getModel, getUnsatCore, push/pop/inNewScope, …) works unchanged. The only difference from the subprocess backend is where you get the solver and how you tear it down.

import Mycroft.Solver.Z3Wasm (newZ3WasmSolver, shutdownZ3Wasm)

main = launchAff_ do
  s <- newZ3WasmSolver { log: Nothing }
  x <- declareConst s "x" tInt
  Smt.assert s (app ">" [ x, intLit 5 ])
  r <- checkSat s          -- Sat
  m <- getModel s          -- x ↦ 6
  stop s
  shutdownZ3Wasm           -- see below — call it last

mycroft's Mycroft.Solver factors the solver into a Transport — a send/close pair over a stream of response chunks — and builds the whole session (:print-success framing, the streaming s-expr parser, scope tracking) on top via newSolverWith. The subprocess backend's transport is a child z3 -in -smt2; this package's transport is one persistent Z3_eval_smtlib2_string context.

Z3's eval_smtlib2_string carries state across calls, so mycroft's lockstep write-one-read-one discipline maps onto exactly one eval per command, and the response string feeds the very same parser the subprocess backend uses. Same veneer, same tests, different wire.

The WASM module and its worker pool are initialised once per process and shared by every solver; each newZ3WasmSolver gets its own Z3 context on that shared pool. stop s releases one solver's context. shutdownZ3Wasm tears down the shared worker pool — so:

• Call it once, last, after every solver is stopped.
• In Node it is mandatory to exit: the pthread workers are live handles and the process will not exit while they run. Forget it and your program hangs at the end.
• No further WASM solvers can be created after it (the next newZ3WasmSolver would re-init a fresh pool).

The z3-solver build uses pthreads, hence SharedArrayBuffer, hence the page must be cross-origin isolated. Serve it with:

Cross-Origin-Opener-Policy: same-origin
Cross-Origin-Embedder-Policy: require-corp

Without those headers SharedArrayBuffer is undefined and init() fails. In Node no headers are needed — it just works.

npm install          # pulls z3-solver (the WASM Z3)
spago build
spago test           # runs the full integration suite — NO z3 binary required

The test suite (Test.Z3Wasm.Main) replays mycroft's subprocess integration beats against the WASM backend — sat-with-model, push/pop scoping, enum-sort model decode, deterministic unsat cores — proving the two backends are interchangeable behind the Solver interface.

• mycroft — the solver session, SMTLib veneer, and the Transport/newSolverWith seam this backend fills.
• z3-solver (npm) — Z3 built to WebAssembly. Pulled by npm install, not by spago.