feat(pist): Route-Repair v1.2 — 36% recovery from 0%

4-Infrastructure/shim/route_repair_v12.py

@@ -0,0 +1,348 @@
+#!/usr/bin/env python3
+"""Route-Repair v1.2: hybrid spectral + text/goal-state obstruction classification.
+
+Gate: if matrix_size >= 3 and rank > 0 → spectral flexure retrieval
+       else → text/goal-state obstruction classifier
+"""
+
+import hashlib, json, math, os, re, subprocess, sys, time, uuid
+from collections import Counter, defaultdict
+from pathlib import Path
+
+sys.path.insert(0, os.path.join(os.path.dirname(__file__), "."))
+from lean_trace_bridge_v2 import instrument_theorem, prove
+from failure_flexure_bank import FAILURE_THEOREMS
+
+WORKER_URL = os.environ.get("CANARY_WORKER_URL", "http://100.110.163.82:8787")
+PROOF_SERVER_TOKEN = os.environ.get("PROOF_SERVER_TOKEN", "")
+if not PROOF_SERVER_TOKEN:
+    tf = os.environ.get("PROOF_SERVER_TOKEN_FILE", os.path.expanduser("~/.config/ene/language-proof-server.token"))
+    try: PROOF_SERVER_TOKEN = Path(tf).read_text().strip()
+    except: pass
+
+LIBRARY_SESSION = "a4a0eb20-93fe-413e-8e0b-50334bb778d8"
+
+V2_FEATURES = ["matrix_size","rank","spectral_gap","laplacian_zero_count","density",
+               "adjacency_eigenvalue_max","adjacency_eigenvalue_second",
+               "laplacian_eigenvalue_max","laplacian_eigenvalue_min",
+               "singular_value_max","trace","frobenius_norm"]
+
+REPAIR_POLICY = {
+    "missing_rewrite_direction": ["rw [← %s]", "rw [%s]"],
+    "missing_assumption_bridge": ["assumption", "exact %s", "apply %s"],
+    "arithmetic_gap": ["omega"],
+    "case_split_missing": ["cases %s", "constructor"],
+    "induction_incomplete": ["induction %s"],
+    "simplifier_gap": ["simp", "simp [%s]"],
+    "coercion_mismatch": ["norm_cast", "exact %s"],
+    "order_inequality_gap": ["omega"],
+}
+
+
+def compute_spectral(matrix):
+    n=len(matrix)
+    if n==0: return {}
+    sym=[[(matrix[i][j]+matrix[j][i])/2 for j in range(n)] for i in range(n)]
+    lap=[[sum(sym[i]) if i==j else -sym[i][j] for j in range(n)] for i in range(n)]
+    def pe(m):
+        v=[1.0/math.sqrt(n)]*n
+        for _ in range(100):
+            vn=[sum(m[i][j]*v[j] for j in range(n)) for i in range(n)]
+            nm=math.sqrt(sum(x*x for x in vn))
+            v=[x/nm for x in vn] if nm>0 else v
+        num=sum(v[i]*sum(m[i][j]*v[j] for j in range(n)) for i in range(n))
+        return num/max(sum(v[i]*v[i] for i in range(n)),1e-12)
+    sm=pe(sym); lm=pe(lap)
+    sh=[[sym[i][j]-0.9*sm*(i==j) for j in range(n)] for i in range(n)]
+    sm2=pe(sh); gap=sm-max(0,sm-sm2)
+    ev_second=sm-max(0,sm-sm2)
+    neg=[[-lap[i][j] for j in range(n)] for i in range(n)]
+    nm=pe(neg)
+    ata=[[sum(matrix[k][i]*matrix[k][j] for k in range(n)) for j in range(n)] for i in range(n)]
+    sva=math.sqrt(max(0,pe(ata)))
+    rank=sum(1 for row in matrix if sum(row)>0)
+    total=sum(sum(r) for r in matrix)
+    frob=math.sqrt(sum(cell*cell for row in matrix for cell in row))
+    lap0=sum(1 for i in range(n) if abs(sum(matrix[i])-matrix[i][i])<1e-9)
+    return {"matrix_size":n,"rank":rank,"spectral_gap":round(gap,6),"density":round(total/max(n*n,1),6),
+            "trace":sum(matrix[i][i] for i in range(n)),"frobenius_norm":round(frob,6),
+            "laplacian_zero_count":lap0,"adjacency_eigenvalue_max":round(sm,6),
+            "adjacency_eigenvalue_second":round(ev_second,6),
+            "laplacian_eigenvalue_max":round(lm,6),"laplacian_eigenvalue_min":round(-nm,6),
+            "singular_value_max":round(sva,6)}
+
+
+def is_degenerate(features: dict) -> bool:
+    return features.get("matrix_size", 0) <= 2 or features.get("rank", 0) == 0 or features.get("spectral_gap", 0) == 0
+
+
+def extract_text_features(code: str) -> dict:
+    """Extract text/goal-state features from a Lean theorem for obstruction classification."""
+    code_lower = code.lower()
+    tactic = "unknown"
+    if "by " in code or "by\n" in code:
+        m = re.search(r'by\s+(\S+)', code)
+        if m: tactic = m.group(1)
+    
+    # Extract hypotheses
+    hyps = []
+    for m in re.finditer(r'\(([^)]+:\s*[^)]+)\)', code):
+        parts = m.group(1).split(":")
+        if len(parts) >= 2:
+            names = parts[0].strip().split()
+            typ = ":".join(parts[1:]).strip()
+            for n in names:
+                hyps.append((n.strip(), typ))
+    
+    hyp_types = [t for _, t in hyps]
+    hyp_names = [n for n, _ in hyps]
+    
+    # Goal analysis
+    goal = code  # use full code for pattern detection since goal extraction is unreliable
+    
+    has_equality = any("=" in t for t in hyp_types) or "=" in goal
+    has_order = any(t in ["Nat","ℕ","Int","ℤ"] for t in hyp_types) and any(c in goal for c in "≤≥<>")
+    has_arithmetic = any(c in code for c in "+-*/") or "omega" in tactic
+    has_constructor = "∧" in goal or "∨" in goal or "→" in goal or "↔" in goal
+    has_inductive = any(n in code_lower for n in ["nat","list","option"])
+    
+    op_counts = {}
+    for c in "+-*/^∧∨→¬∀∃≤≥=":
+        op_counts[c] = code.count(c)
+    
+    return {
+        "tactic": tactic, "goal": goal[:100],
+        "hypothesis_count": len(hyps), "hypothesis_names": hyp_names[:5],
+        "hypothesis_types": hyp_types[:5],
+        "has_equality": has_equality, "has_order": has_order,
+        "has_arithmetic": has_arithmetic, "has_constructor": has_constructor,
+        "has_inductive": has_inductive,
+        "operator_counts": {k: v for k, v in op_counts.items() if v > 0},
+    }
+
+
+def classify_obstruction(tf: dict) -> str:
+    """Classify obstruction type from text features — ordered by specificity."""
+    tactic = tf.get("tactic", "")
+    has_eq = tf.get("has_equality", False)
+    has_order = tf.get("has_order", False)
+    has_arith = tf.get("has_arithmetic", False)
+    has_constructor = tf.get("has_constructor", False)
+    has_inductive = tf.get("has_inductive", False)
+    n_hyps = tf.get("hypothesis_count", 0)
+    goal = tf.get("goal", "")
+    
+    # RW with equality → rewrite direction
+    if tactic in ("rw", "rw_simp") and has_eq:
+        return "missing_rewrite_direction"
+    # Constructor goal with rfl/simp → case split
+    if has_constructor or ("∧" in goal or "∨" in goal or "→" in goal):
+        return "case_split_missing"
+    # Arithmetic symbols with simp/rfl/omega that are _not_ pure equality — arithmetic gap
+    if has_arith and tactic in ("simp", "rfl", "omega"):
+        return "arithmetic_gap"
+    # RFL with hypotheses and no constructor target → assumption bridge failure
+    if tactic == "rfl" and n_hyps > 0:
+        return "missing_assumption_bridge"
+    # Inductive type → induction incomplete
+    if has_inductive and tactic in ("simp", "rfl"):
+        return "induction_incomplete"
+    # Simp with no clear pattern → simplifier gap
+    if tactic == "simp":
+        return "simplifier_gap"
+    # Order/inequality symbols
+    if has_order:
+        return "order_inequality_gap"
+    # Coercion-like patterns
+    if tactic == "rfl" and any(c in str(tf) for c in ["nat", "int"]):
+        return "coercion_mismatch"
+    return "other"
+
+
+def build_trace(name: str, code: str) -> dict | None:
+    """Run a theorem through the trace bridge and return spectral + text features."""
+    try:
+        instr, tags = instrument_theorem(code)
+        if not tags: return None
+        resp = prove(instr, name + "_flex")
+        stdout = resp.get("stdout", "") or ""
+        found = [l.split("@@PIST_TRACE_JSON@@")[1].strip() for l in stdout.split("\n") if "@@PIST_TRACE_JSON@@" in l]
+        if not found: return None
+        hs = [hashlib.sha256(t.encode()).hexdigest()[:16] for t in found]
+        uniq = list(dict.fromkeys(hs)); n = len(uniq)
+        mat = [[0] * n for _ in range(n)]
+        hi = {h: i for i, h in enumerate(uniq)}
+        for i in range(len(hs) - 1):
+            if hs[i] in hi and hs[i + 1] in hi: mat[hi[hs[i]]][hi[hs[i + 1]]] += 1
+        sp = compute_spectral(mat)
+        tf = extract_text_features(code)
+        return {"name": name, "spectral": sp, "text_features": tf, "code": code}
+    except:
+        return None
+
+
+def connect():
+    host = os.environ.get("RDS_HOST", "database-1-instance-1.cghu8yqogqwo.us-east-1.rds.amazonaws.com")
+    port = os.environ.get("RDS_PORT", "5432"); user = os.environ.get("RDS_USER", "postgres")
+    db = os.environ.get("RDS_DB", "postgres")
+    token = os.environ.get("RDS_IAM_TOKEN", "")
+    if not token:
+        token = subprocess.check_output(["aws", "rds", "generate-db-auth-token",
+            "--region", os.environ.get("AWS_REGION", "us-east-1"),
+            "--hostname", host, "--port", port, "--username", user], text=True).strip()
+    import psycopg2
+    return psycopg2.connect(host=host, port=port, user=user, password=token, dbname=db, sslmode="require")
+
+
+def spectral_route(features, library_session, failure_session):
+    """kNN against flexure library for multi-step traces."""
+    conn = connect(); cur = conn.cursor()
+    cur.execute("SELECT decision_signals FROM ene.flexures WHERE session_id=%s OR session_id=%s",
+                (library_session, failure_session))
+    library = []
+    for row in cur.fetchall():
+        sig = json.loads(row[0]) if isinstance(row[0], str) else row[0]
+        sl = sig.get("spectral", {}); lv = [sl.get(k, 0) for k in V2_FEATURES]
+        library.append({"features": lv, "obs": sig.get("obstruction_type", "?"), "tf": sig.get("tactic_family", "?")})
+    cur.close(); conn.close()
+    
+    if not library: return "other"
+    vec = [features.get(k, 0) for k in V2_FEATURES]
+    scored = [(math.sqrt(sum((vec[i] - l["features"][i])**2 for i in range(len(vec)))), l) for l in library if len(l["features"]) == len(vec)]
+    scored.sort(key=lambda x: x[0])
+    top3 = scored[:3]
+    obs_votes = Counter(lib["obs"] for _, lib in top3)
+    return obs_votes.most_common(1)[0][0] if obs_votes else "other"
+
+
+def text_route(tf: dict) -> str:
+    """Classify obstruction from text features (fallback for degenerate traces)."""
+    return classify_obstruction(tf)
+
+
+def generate_patches(obstruction_type: str, code: str, max_patches: int = 3) -> list[str]:
+    """Generate repair patches for an obstruction type."""
+    templates = REPAIR_POLICY.get(obstruction_type, [])
+    # Extract hypothesis names — filter to single-named hypotheses (not type decls)
+    hyps = re.findall(r'\(([^)]+:\s*[^)]+)\)', code)
+    hyp_names = []
+    for h in hyps:
+        parts = h.split(":")
+        names_part = parts[0].strip()
+        type_part = ":".join(parts[1:]).strip()
+        # A hypothesis has exactly one name (like "h : A" not "A B : Prop")
+        if len(names_part.split()) == 1 and type_part not in ("Prop", "Nat", "Int", "ℕ", "ℤ", "Type"):
+            hyp_names.append(names_part.strip())
+    first_hyp = hyp_names[0] if hyp_names else "h"
+    
+    patches = []
+    for tmpl in templates:
+        if "%s" in tmpl:
+            patches.append(tmpl % first_hyp)
+        else:
+            patches.append(tmpl)
+    return patches[:max_patches]
+
+
+def route_repair(name: str, code: str, library_session: str, failure_session: str, max_attempts: int = 5) -> dict:
+    """Hybrid route-repair: spectral for multi-step, text for degenerate."""
+    # Build trace
+    instr, tags = instrument_theorem(code)
+    if not tags:
+        sp = {"matrix_size": 0, "rank": 0, "spectral_gap": 0}
+    else:
+        hs = [hashlib.sha256(t.encode()).hexdigest()[:16] for t in tags]
+        uniq = list(dict.fromkeys(hs)); n = len(uniq)
+        mat = [[0] * n for _ in range(n)]
+        hi = {h: i for i, h in enumerate(uniq)}
+        for i in range(len(hs) - 1):
+            if hs[i] in hi and hs[i+1] in hi:
+                mat[hi[hs[i]]][hi[hs[i+1]]] += 1
+        sp = compute_spectral(mat)
+    
+    tf = extract_text_features(code)
+    
+    # Degeneracy gate
+    if is_degenerate(sp):
+        obstruction = text_route(tf)
+        routing_method = "text_fallback"
+    else:
+        obstruction = spectral_route(sp, library_session, failure_session)
+        routing_method = "spectral_flexure"
+    
+    # Verify initial failure
+    resp = prove(code, name + "_init")
+    if resp.get("ok", False):
+        return {"name": name, "initial_status": "verified", "recovered": False, "notes": "already verified"}
+    
+    # Generate patches
+    patches = generate_patches(obstruction, code, max_patches=max_attempts)
+    init_vars = code.count("("); init_ops = sum(1 for c in code if c in "+-*/^∧∨→¬∀∃≤≥")
+    attempts = []; best_delta = -999; best_attempt = None; recovered = False
+    
+    for i, patch in enumerate(patches):
+        patched = code.split(":=")[0] + ":= by\n  " + patch
+        r = prove(patched, f"{name}_repair_{i}")
+        ok = r.get("ok", False)
+        av = patched.count("("); ao = sum(1 for c in patched if c in "+-*/^∧∨→¬∀∃≤≥")
+        delta = (init_vars + init_ops) - (av + ao)
+        if delta > best_delta:
+            best_delta = delta; best_attempt = {"patch": patch, "delta": delta, "ok": ok}
+        if ok:
+            recovered = True; best_attempt = {"patch": patch, "delta": delta, "ok": ok}; break
+        attempts.append({"attempt": i + 1, "patch": patch, "obstruction": obstruction, "ok": ok, "delta": delta})
+    
+    return {
+        "name": name, "obstruction": obstruction,
+        "routing_method": routing_method,
+        "initial_status": "failed", "recovered": recovered,
+        "best_delta": best_delta, "partial_improvement": best_delta > 0,
+        "attempts": attempts, "best_attempt": best_attempt,
+        "matrix_size": sp.get("matrix_size", 0),
+        "rank": sp.get("rank", 0),
+        "tactic": tf.get("tactic", "?"),
+        "has_equality": tf.get("has_equality", False),
+        "has_arithmetic": tf.get("has_arithmetic", False),
+        "has_constructor": tf.get("has_constructor", False),
+    }
+
+
+def main():
+    print("Route-Repair v1.2: hybrid spectral + text obstruction classifier\n")
+    failure_session = "9b1f9591-1c34-4c21-aeb8-594448b82003"
+    test_set = FAILURE_THEOREMS[:30]
+    
+    results = []
+    for i, (n, c) in enumerate(test_set):
+        print(f"  [{i+1}/{len(test_set)}] {n:35s} ... ", end="", flush=True)
+        r = route_repair(n, c, LIBRARY_SESSION, failure_session)
+        if r["initial_status"] == "verified":
+            print("already verified"); continue
+        s = "RECOVERED" if r["recovered"] else "improved" if r.get("partial_improvement") else "no change"
+        print(f"{s:15s} obs={r['obstruction']:30s} method={r['routing_method']:18s} "
+              f"tactic={r['tactic']:8s} eq={r['has_equality']} arith={r['has_arithmetic']}", flush=True)
+        results.append(r)
+    
+    n = len(results); rec = sum(1 for r in results if r["recovered"]); part = sum(1 for r in results if r.get("partial_improvement"))
+    
+    print(f"\n{'='*60}\nV1.2 HYBRID REPORT\n{'='*60}")
+    print(f"Test: {n} failed | Recovered: {rec} ({rec/max(n,1):.0%}) | Partial: {part} ({part/max(n,1):.0%})")
+    
+    # Obstruction distribution
+    obs_dist = Counter(r["obstruction"] for r in results)
+    print(f"\nObstruction distribution:", flush=True)
+    for obs, cnt in sorted(obs_dist.items(), key=lambda x: -x[1]):
+        rec_obs = sum(1 for r in results if r["obstruction"] == obs and r["recovered"])
+        print(f"  {obs:30s}: n={cnt:2d} rec={rec_obs}")
+    
+    routing = Counter(r["routing_method"] for r in results)
+    print(f"\nRouting: text_fallback={routing.get('text_fallback', 0)}, spectral={routing.get('spectral_flexure', 0)}")
+    
+    rp_path = os.path.join(os.path.dirname(__file__), "..", "..", "shared-data", "pist_route_repair_v12_benchmark.json")
+    with open(rp_path, "w") as f:
+        json.dump({"n": n, "recovered": rec, "partial": part, "results": results, "routing": dict(routing)}, f, indent=2)
+    print(f"\nReport: {rp_path}")
+
+
+if __name__ == "__main__":
+    main()

shared-data/pist_route_repair_v12_benchmark.json

@@ -0,0 +1,847 @@
+{
+  "n": 28,
+  "recovered": 10,
+  "partial": 0,
+  "results": [
+    {
+      "name": "rw_missing_dir_1",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "rw_missing_dir_2",
+      "obstruction": "missing_assumption_bridge",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "assumption",
+          "obstruction": "missing_assumption_bridge",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "exact h1",
+          "obstruction": "missing_assumption_bridge",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 3,
+          "patch": "apply h1",
+          "obstruction": "missing_assumption_bridge",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "assumption",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": false
+    },
+    {
+      "name": "rw_missing_dir_3",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "rw_missing_dir_4",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "rw_missing_dir_5",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "rw_missing_dir_6",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "rw_missing_dir_7",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "missing_assume_1",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases hA",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases hA",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "missing_assume_2",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases hA",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases hA",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "missing_assume_3",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "missing_assume_4",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "missing_assume_5",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "missing_assume_6",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "missing_assume_7",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "arith_gap_1",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "arith_gap_2",
+      "obstruction": "induction_incomplete",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "induction h1",
+          "obstruction": "induction_incomplete",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "induction h1",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": false
+    },
+    {
+      "name": "arith_gap_3",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "omega",
+          "obstruction": "arithmetic_gap",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "arith_gap_4",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "arith_gap_5",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "omega",
+          "obstruction": "arithmetic_gap",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "arith_gap_6",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "arith_gap_8",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "omega",
+          "obstruction": "arithmetic_gap",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "arith_gap_9",
+      "obstruction": "arithmetic_gap",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": true,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [],
+      "best_attempt": {
+        "patch": "omega",
+        "delta": 0,
+        "ok": true
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": true,
+      "has_constructor": false
+    },
+    {
+      "name": "case_split_1",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "case_split_2",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "case_split_3",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases hA",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases hA",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "case_split_4",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "rfl",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "case_split_5",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases h",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases h",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    },
+    {
+      "name": "case_split_6",
+      "obstruction": "case_split_missing",
+      "routing_method": "text_fallback",
+      "initial_status": "failed",
+      "recovered": false,
+      "best_delta": 0,
+      "partial_improvement": false,
+      "attempts": [
+        {
+          "attempt": 1,
+          "patch": "cases hA",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        },
+        {
+          "attempt": 2,
+          "patch": "constructor",
+          "obstruction": "case_split_missing",
+          "ok": false,
+          "delta": 0
+        }
+      ],
+      "best_attempt": {
+        "patch": "cases hA",
+        "delta": 0,
+        "ok": false
+      },
+      "matrix_size": 2,
+      "rank": 1,
+      "tactic": "simp",
+      "has_equality": true,
+      "has_arithmetic": false,
+      "has_constructor": true
+    }
+  ],
+  "routing": {
+    "text_fallback": 28
+  }
+}