windtf · Nov 3, 2026 · Oct 22, 2026 · Oct 27, 2026 · Oct 27, 2026 · Oct 28, 2026
diff --git a/.github/workflows/stack-test.yml b/.github/workflows/stack-test.yml
@@ -9,7 +9,7 @@ on:
 jobs:
   build:
     runs-on: ubuntu-latest
-    timeout-minutes: 60
+    timeout-minutes: 90
 
     steps:
     - name: Checkout code

diff --git a/benchmark/bench_blake2b b/benchmark/bench_blake2b
diff --git a/benchmark/bench_chacha20 b/benchmark/bench_chacha20
diff --git a/benchmark/bench_sha256 b/benchmark/bench_sha256
diff --git a/benchmark/bench_sodium_memcmp b/benchmark/bench_sodium_memcmp
diff --git a/benchmark/bench_vuln_memcmp b/benchmark/bench_vuln_memcmp
diff --git a/benchmark/bench_x25519 b/benchmark/bench_x25519
diff --git a/benchmark/eval.py b/benchmark/eval.py
@@ -0,0 +1,106 @@
+#!/usr/bin/env python3
+"""Rerun the checker on the benchmark binaries and print its verdicts.
+
+Each program proof under proof/Proof/SMT/Stepper passes only if the
+checker returns the verdict its name states, so a green build is the result.
+This script deletes those modules' compiled files so that GHC rebuilds them,
+runs the build with Bitwuzla, and prints one row per checker run with its
+time. GHC compares source hashes, so touching the sources would not do.
+
+Usage: benchmark/eval.py [--bitwuzla PATH] [--csv FILE]
+"""
+
+import argparse
+import csv
+import os
+import re
+import shutil
+import subprocess
+import sys
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent.parent
+PROOF_SOURCES = ROOT / "proof"
+CHECKER_PROOFS = {"Relational", "RelMem", "Invariant"}
+PROGRAM_PROOFS = sorted(
+    path.relative_to(PROOF_SOURCES).with_suffix("")
+    for path in (PROOF_SOURCES / "Proof/SMT/Stepper").rglob("*.hs")
+    if path.stem not in CHECKER_PROOFS
+)
+COMPILED_SUFFIXES = [".hi", ".o", ".dyn_hi", ".dyn_o"]
+
+VERDICTS = [
+    ("NoLeak", "no leak"),
+    ("Leaks", "leak"),
+    ("OutOfFuel", "out of fuel"),
+    ("OneStepShort", "out of fuel"),
+]
+
+COMPILING = re.compile(r"Compiling (Proof\.SMT\.Stepper\.\S+)")
+EVALUATING = re.compile(r"SymFC evaluating '([^']+)'")
+ELAPSED = re.compile(r"\*\*\* SymFC: Elapsed time: ([0-9.]+)")
+
+
+def verdict_of(proof):
+    for marker, verdict in VERDICTS:
+        if marker in proof:
+            return verdict
+    return None
+
+
+def run_build(bitwuzla):
+    env = dict(os.environ, SBV_Z3=bitwuzla, SBV_Z3_OPTIONS="--produce-models")
+    for build_dir in ROOT.glob(".stack-work/dist/*/*/build"):
+        for module in PROGRAM_PROOFS:
+            for suffix in COMPILED_SUFFIXES:
+                build_dir.joinpath(module).with_suffix(suffix).unlink(missing_ok=True)
+    build = subprocess.Popen(
+        ["stack", "build", "--test", "--no-run-tests", "--force-dirty"],
+        cwd=ROOT,
+        env=env,
+        stdout=subprocess.PIPE,
+        stderr=subprocess.STDOUT,
+        text=True,
+        errors="replace",
+    )
+    rows = []
+    module = proof = None
+    for line in build.stdout:
+        if found := COMPILING.search(line):
+            module = found.group(1).removeprefix("Proof.SMT.Stepper.")
+            if module in CHECKER_PROOFS:
+                module = None
+        elif found := EVALUATING.search(line):
+            proof = found.group(1)
+        elif (found := ELAPSED.search(line)) and proof:
+            verdict = verdict_of(proof)
+            if verdict and module:
+                rows.append((module, proof, verdict, float(found.group(1))))
+            proof = None
+    return build.wait(), rows
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    parser.add_argument("--bitwuzla", default=shutil.which("bitwuzla"))
+    parser.add_argument("--csv", type=Path)
+    args = parser.parse_args()
+    if not args.bitwuzla:
+        sys.exit("bitwuzla not found; pass --bitwuzla PATH")
+
+    status, rows = run_build(args.bitwuzla)
+    rows.sort()
+    width = max((len(proof) for _, proof, _, _ in rows), default=10)
+    for module, proof, verdict, seconds in rows:
+        print(f"{module:14} {proof:{width}} {verdict:12} {seconds:8.1f} s")
+    if args.csv:
+        with args.csv.open("w", newline="") as out:
+            writer = csv.writer(out)
+            writer.writerow(["program", "check", "verdict", "seconds"])
+            writer.writerows(rows)
+    if status != 0:
+        sys.exit("the build failed, so at least one verdict is not the one its proof states")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/benchmark/libsodium b/benchmark/libsodium
diff --git a/benchmark/secure_memory.o b/benchmark/secure_memory.o
diff --git a/package.yaml b/package.yaml
@@ -21,7 +21,8 @@ description:         Please see the README on GitHub at <https://github.com/gith
 
 # The modules listed under the smt-proof flag in the library discharge their
 # properties through an SMT solver while GHC compiles them, so building them
-# needs a solver on PATH and takes as long as the solver does. Pantomime goes through SBV, and SBV's Z3 backend is
+# needs a solver on PATH and takes as long as the solver does. SymFC goes
+# through SBV, and SBV's Z3 backend is
 # pointed at a different binary with SBV_Z3; Z3 itself does not finish these in
 # useful time, while bitwuzla discharges each in under a minute:
 #
@@ -82,10 +83,12 @@ dependencies:
 - exceptions
 - entropy
 - binary
-- pantomime
-- pantomime-clash
-- pantomime-base
+- sym-fc
+- sym-fc-clash
+- sym-fc-base
 - template-haskell
+- constraints
+- comonad
 
 ghc-options:
 - -Wall
@@ -99,7 +102,7 @@ ghc-options:
 - -Wredundant-constraints
 - -fexpose-all-unfoldings
 - -fplugin GHC.TypeLits.Normalise
-- -fplugin Pantomime
+- -fplugin SymFC
 
 library:
   source-dirs:
@@ -120,9 +123,26 @@ library:
         - Proof.Memory.Cache4K.SMT.Array
         - Proof.Memory.Cache4K.SMT.Axioms
         - Proof.Memory.Cache4K.SMT.Coherent
-        - Proof.SMT.Logged
         - Proof.SMT.Sanity
         - Proof.Core.Functional.System
+        - Proof.SMT.Concrete
+        - Proof.SMT.Stepper
+        - Proof.SMT.Stepper.Blake2b
+        - Proof.SMT.Stepper.Chacha
+        - Proof.SMT.Stepper.X25519.Call
+        - Proof.SMT.Stepper.X25519.Cswap
+        - Proof.SMT.Stepper.X25519.Ladder
+        - Proof.SMT.Stepper.X25519.Mul
+        - Proof.SMT.Stepper.Memcmp
+        - Proof.SMT.Stepper.P256Call
+        - Proof.SMT.Stepper.P256Field
+        - Proof.SMT.Stepper.P256Multiply
+        - Proof.SMT.Stepper.P256Recode
+        - Proof.SMT.Stepper.RelMem
+        - Proof.SMT.Stepper.Relational
+        - Proof.SMT.Stepper.Invariant
+        - Proof.SMT.Stepper.Sha256
+        - Proof.SMT.Symbolic
       cpp-options: -DSMT_PROOF
   # Listed explicitly, with no automatic discovery: the solver modules above
   # live in proof/ too, and must only be built with the smt-proof flag.
@@ -156,6 +176,7 @@ library:
     - Proof.Core.Leakage.Driver
     - Proof.Core.Leakage.Invariant
     - Proof.Core.Leakage.Obligation
+    - Access
     - Elf.ElfLoader
     - Elf.Syscall
     - HardwareSim
@@ -173,6 +194,18 @@ library:
     - Pretty
     - Core.RegFile
     - Simulate
+    - Stepper
+    - Stepper.AddrMap
+    - Stepper.Concrete
+    - Stepper.ElfCode
+    - Stepper.Embedding
+    - Stepper.Memory
+    - Stepper.Rel
+    - Stepper.RelMem
+    - Stepper.RelRegs
+    - Stepper.RelState
+    - Stepper.Relational
+    - Stepper.Shift
     - Types
     - Util
 

diff --git a/proof/Proof/Core/Functional/Invariant.hs b/proof/Proof/Core/Functional/Invariant.hs
@@ -12,7 +12,7 @@
 --   * 'invCases' represents each case as a named list of conjuncts, so a
 --     failing QuickCheck run can report which clause broke ('explain');
 --   * 'invAt' is the identical predicate built from '&&' and '||' with no
---     lists, because Pantomime's evaluator diverges on recursion it cannot
+--     lists, because SymFC's evaluator diverges on recursion it cannot
 --     prove terminating -- even over a fully concrete list. Symbolic execution
 --     uses this one.
 --