1"""Per-theorem SAT instance sizes for the bv_decide proofs.23Re-elaborates each module with `trace.Meta.Tactic.bv` enabled and `--json` output: every trace4block is one JSON message carrying its source position, so each "AIG has N nodes" value (size of5the bit-blasted And-Inverter Graph handed to CaDiCaL) is attributed to the enclosing theorem6exactly. `bv_decide` calls closed by preprocessing alone emit no AIG. Requires a prior7`lake build` (imports must be compiled).89Run (from formal/): ../.venv/bin/python scripts/aig_sizes.py10"""11from __future__ import annotations12import json, os, re, subprocess, sys, time13from pathlib import Path1415HERE = Path(__file__).resolve().parent.parent16MODULES = ["Sha256Words", "Sha256Step", "Schedule", "LocalCollision"]1718def theorem_at(src_lines, lineno):19 name = None20 for i in range(lineno - 1, -1, -1):21 m = re.match(r"\s*(?:theorem|lemma|def)\s+([\w.']+)", src_lines[i])22 if m:23 return m.group(1)24 return name2526def main():27 env = dict(os.environ)28 env["PATH"] = str(Path.home() / ".elan" / "bin") + os.pathsep + env.get("PATH", "")29 rows = []30 for mod in MODULES:31 path = HERE / "Wp34" / f"{mod}.lean"32 src = path.read_text().splitlines()33 t0 = time.time()34 r = subprocess.run(["lake", "env", "lean", "--json", "-D", "trace.Meta.Tactic.bv=true", str(path)],35 cwd=HERE, env=env, capture_output=True, text=True)36 dt = time.time() - t037 for line in r.stdout.splitlines():38 try:39 msg = json.loads(line)40 except json.JSONDecodeError:41 continue42 for m in re.finditer(r"AIG has (\d+) nodes", msg.get("data", "")):43 rows.append((mod, theorem_at(src, msg["pos"]["line"]), int(m.group(1))))44 print(f"# {mod}: re-elaborated with trace in {dt:.1f} s, exit {r.returncode}", file=sys.stderr)45 print("module\ttheorem\taig_nodes")46 for mod, name, n in rows:47 print(f"{mod}\t{name}\t{n}")4849if __name__ == "__main__":50 main()51