From de90ab5579723ab737cb287f935161e12fec5100 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 12:38:17 -0500 Subject: [PATCH] =?UTF-8?q?feat(pist):=20Route-Repair=20v1.2=20=E2=80=94?= =?UTF-8?q?=2036%=20recovery=20from=200%?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- 4-Infrastructure/shim/route_repair_v12.py | 348 +++++++ .../pist_route_repair_v12_benchmark.json | 847 ++++++++++++++++++ 2 files changed, 1195 insertions(+) create mode 100644 4-Infrastructure/shim/route_repair_v12.py create mode 100644 shared-data/pist_route_repair_v12_benchmark.json diff --git a/4-Infrastructure/shim/route_repair_v12.py b/4-Infrastructure/shim/route_repair_v12.py new file mode 100644 index 00000000..d5fad4b0 --- /dev/null +++ b/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() diff --git a/shared-data/pist_route_repair_v12_benchmark.json b/shared-data/pist_route_repair_v12_benchmark.json new file mode 100644 index 00000000..ff8f2f19 --- /dev/null +++ b/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 + } +} \ No newline at end of file