diff --git a/4-Infrastructure/k3s-flake/manifests/actual-budget/deployment.yaml b/4-Infrastructure/k3s-flake/manifests/actual-budget/deployment.yaml new file mode 100644 index 00000000..4d93019c --- /dev/null +++ b/4-Infrastructure/k3s-flake/manifests/actual-budget/deployment.yaml @@ -0,0 +1,34 @@ +apiVersion: apps/v1 +kind: Deployment +metadata: + name: actual-budget + namespace: services + labels: + app: actual-budget +spec: + replicas: 1 + selector: + matchLabels: + app: actual-budget + template: + metadata: + labels: + app: actual-budget + spec: + tolerations: + - key: "node-role.kubernetes.io/control-plane" + operator: "Exists" + effect: "NoSchedule" + containers: + - name: actual-budget + image: ghcr.io/actualbudget/actual-server:26.5.2 + ports: + - containerPort: 5006 + name: http + volumeMounts: + - name: data + mountPath: /data + volumes: + - name: data + persistentVolumeClaim: + claimName: actual-budget-data diff --git a/4-Infrastructure/k3s-flake/manifests/actual-budget/pvc.yaml b/4-Infrastructure/k3s-flake/manifests/actual-budget/pvc.yaml new file mode 100644 index 00000000..71348ccc --- /dev/null +++ b/4-Infrastructure/k3s-flake/manifests/actual-budget/pvc.yaml @@ -0,0 +1,11 @@ +apiVersion: v1 +kind: PersistentVolumeClaim +metadata: + name: actual-budget-data + namespace: services +spec: + accessModes: + - ReadWriteOnce + resources: + requests: + storage: 2Gi diff --git a/4-Infrastructure/k3s-flake/manifests/actual-budget/service.yaml b/4-Infrastructure/k3s-flake/manifests/actual-budget/service.yaml new file mode 100644 index 00000000..bb2766ce --- /dev/null +++ b/4-Infrastructure/k3s-flake/manifests/actual-budget/service.yaml @@ -0,0 +1,15 @@ +apiVersion: v1 +kind: Service +metadata: + name: actual-budget + namespace: services +spec: + type: NodePort + ports: + - port: 5006 + targetPort: 5006 + nodePort: 30815 + protocol: TCP + name: http + selector: + app: actual-budget diff --git a/4-Infrastructure/k3s-flake/manifests/kustomization.yaml b/4-Infrastructure/k3s-flake/manifests/kustomization.yaml index fa2fa9b3..49bf7914 100644 --- a/4-Infrastructure/k3s-flake/manifests/kustomization.yaml +++ b/4-Infrastructure/k3s-flake/manifests/kustomization.yaml @@ -9,3 +9,5 @@ resources: - pulse-receiver - homarr - authentik + - actual-budget + diff --git a/4-Infrastructure/scripts/run_import_workflow.py b/4-Infrastructure/scripts/run_import_workflow.py new file mode 100644 index 00000000..9b11c130 --- /dev/null +++ b/4-Infrastructure/scripts/run_import_workflow.py @@ -0,0 +1,101 @@ +import asyncio +from playwright.async_api import async_playwright +import os + +PASSWORD = "***REMOVED***" +CSV_PATH = "/home/allaun/.gemini/antigravity/scratch/affirm_loans_import.csv" +SCREENSHOT_DIR = "/home/allaun/.gemini/antigravity/scratch/screenshots" +os.makedirs(SCREENSHOT_DIR, exist_ok=True) + +async def main(): + async with async_playwright() as p: + print("[*] Launching browser...") + browser = await p.chromium.launch(headless=True) + context = await browser.new_context(ignore_https_errors=True) + page = await context.new_page() + + # 1. Login + print("[*] Navigating to login page...") + await page.goto("https://budget.researchstack.info/login") + await page.wait_for_selector("input[type='password']") + await page.fill("input[type='password']", PASSWORD) + await page.screenshot(path=f"{SCREENSHOT_DIR}/01_login_filled.png") + await page.click("button:has-text('Sign in')") + await page.wait_for_timeout(5000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/02_after_login.png") + + # 2. Open Budget File + print("[*] Opening 'My Finances' budget...") + await page.click("text=My Finances") + await page.wait_for_timeout(8000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/03_budget_loaded.png") + + # 3. Check if 'Affirm Loans' already exists in the sidebar + sidebar_text = await page.evaluate("document.body.innerText") + if "Affirm Loans" in sidebar_text: + print("[+] 'Affirm Loans' account already exists in sidebar. Clicking it...") + await page.click("text=Affirm Loans") + await page.wait_for_timeout(4000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/04_account_opened.png") + else: + print("[*] Creating 'Affirm Loans' account...") + # Click Add account button (sidebar or main page) + add_account_buttons = page.locator("text=Add account") + await add_account_buttons.first.click() + await page.wait_for_timeout(3000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/04_add_account_modal.png") + + # Click Create local account + await page.click("button:has-text('Create local account')") + await page.wait_for_timeout(3000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/05_local_account_form.png") + + # Fill form + await page.fill("input[name='name']", "Affirm Loans") + await page.check("input[type='checkbox']#offbudget") + await page.screenshot(path=f"{SCREENSHOT_DIR}/06_form_filled.png") + + # Click Create + await page.locator("button:has-text('Create')").last.click() + await page.wait_for_timeout(6000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/07_after_account_created.png") + + # 4. Trigger Import + print("[*] Triggering import...") + # Look for the Import button + import_btn = page.locator("button:has-text('Import'), a:has-text('Import'), span:has-text('Import')") + count = await import_btn.count() + print(f"[*] Found {count} potential import elements") + + # Let's try to click the first visible/available Import button + async with page.expect_file_chooser() as fc_info: + await import_btn.first.click() + file_chooser = await fc_info.value + print(f"[+] Selecting file {CSV_PATH}...") + await file_chooser.set_files(CSV_PATH) + await page.wait_for_timeout(6000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/08_after_file_selected.png") + + # 5. Confirm mapping and import + print("[*] Confirming import mapping...") + # Locate the button that finishes the import + # Usually it says "Import 21 transactions" or "Import" + final_btn = page.locator("button:has-text('transactions'), button:has-text('Import')") + final_count = await final_btn.count() + print(f"[*] Found {final_count} final import buttons") + + await final_btn.last.click() + print("[*] Finalizing import...") + await page.wait_for_timeout(6000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/09_import_finished.png") + + # Get final status + final_text = await page.evaluate("document.body.innerText") + print("\n--- Final Page Body Text ---") + print(final_text[:2000]) + print("----------------------------") + + await browser.close() + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/4-Infrastructure/scripts/run_multi_import.py b/4-Infrastructure/scripts/run_multi_import.py new file mode 100644 index 00000000..14bee4eb --- /dev/null +++ b/4-Infrastructure/scripts/run_multi_import.py @@ -0,0 +1,141 @@ +import asyncio +from playwright.async_api import async_playwright +import os +import glob +import re + +PASSWORD = "***REMOVED***" +IMPORT_DIR = "/home/allaun/.gemini/antigravity/scratch/imports" +SCREENSHOT_DIR = "/home/allaun/.gemini/antigravity/scratch/screenshots/multi_import" +os.makedirs(SCREENSHOT_DIR, exist_ok=True) + +# List of account files to import and their original names +IMPORT_ACCOUNTS = [ + {"file": "Chime-Chime_account.csv", "name": "Chime account"}, + {"file": "Chime-Chime_Secured_Credit.csv", "name": "Chime Secured Credit"}, + {"file": "Capital_One-Quicksilver.csv", "name": "Quicksilver"}, + {"file": "Credit_One_Bank-Visa.csv", "name": "Visa"}, + {"file": "Venmo_-_Personal-Personal_Profile.csv", "name": "Personal Profile"}, + {"file": "Capital_One-credit_Account_8214.csv", "name": "credit Account 8214"}, + {"file": "Capital_One-depository_Account_8109.csv", "name": "depository Account 8109"}, + {"file": "Capital_One-depository_Account_9461.csv", "name": "depository Account 9461"}, + {"file": "Capital_One-depository_Account_9555.csv", "name": "depository Account 9555"}, +] + +async def import_account(page, file_info): + csv_path = os.path.join(IMPORT_DIR, file_info["file"]) + acc_name = file_info["name"] + + if not os.path.exists(csv_path): + print(f"[-] Warning: CSV file {csv_path} does not exist. Skipping.") + return + + print(f"\n[*] Processing account '{acc_name}' from {file_info['file']}...") + + # 1. Check if account already exists in the sidebar + sidebar_text = await page.evaluate("document.body.innerText") + if acc_name in sidebar_text: + print(f"[+] '{acc_name}' already exists in sidebar. Clicking it...") + # To avoid clicking random text, let's find the navigation element or link matching the name + # In Actual, sidebar items are links or text + await page.click(f"text='{acc_name}'") + await page.wait_for_timeout(3000) + else: + print(f"[*] Creating '{acc_name}' account...") + # Click Add account button (sidebar or main page) + add_account_buttons = page.locator("text=Add account") + await add_account_buttons.first.click() + await page.wait_for_timeout(2000) + + # Click Create local account + await page.click("button:has-text('Create local account')") + await page.wait_for_timeout(2000) + + # Fill form (On-budget by default) + await page.fill("input[name='name']", acc_name) + + # Click Create (using the last button to avoid clicking parent hidden button) + await page.locator("button:has-text('Create')").last.click() + await page.wait_for_timeout(5000) + + # 2. Trigger Import + print(f"[*] Triggering import for '{acc_name}'...") + import_btn = page.locator("button:has-text('Import'), a:has-text('Import'), span:has-text('Import')") + count = await import_btn.count() + if count == 0: + print(f"[-] Error: Could not find Import button for '{acc_name}'") + await page.screenshot(path=f"{SCREENSHOT_DIR}/error_{acc_name.replace(' ', '_')}.png") + return + + # Trigger file chooser + async with page.expect_file_chooser() as fc_info: + await import_btn.first.click() + file_chooser = await fc_info.value + print(f"[+] Selecting file {csv_path}...") + await file_chooser.set_files(csv_path) + await page.wait_for_timeout(5000) + + # 3. Confirm mapping and import + print("[*] Confirming import mapping...") + # Locate the button that finishes the import + final_btn = page.locator("button:has-text('transactions'), button:has-text('Import')") + final_count = await final_btn.count() + print(f"[*] Found {final_count} final import buttons") + + if final_count > 0: + await final_btn.last.click() + print("[*] Finalizing import...") + await page.wait_for_timeout(5000) + + # Take a screenshot to document success + safe_name = acc_name.replace(' ', '_') + await page.screenshot(path=f"{SCREENSHOT_DIR}/{safe_name}_imported.png") + print(f"[+] Import of '{acc_name}' completed. Screenshot saved.") + else: + print(f"[-] Error: No final import button found for '{acc_name}'") + await page.screenshot(path=f"{SCREENSHOT_DIR}/error_confirm_{acc_name.replace(' ', '_')}.png") + +async def main(): + async with async_playwright() as p: + print("[*] Launching browser...") + browser = await p.chromium.launch(headless=True) + context = await browser.new_context(ignore_https_errors=True) + page = await context.new_page() + + # Login + print("[*] Navigating to login page...") + await page.goto("https://budget.researchstack.info/login") + await page.wait_for_selector("input[type='password']") + await page.fill("input[type='password']", PASSWORD) + await page.click("button:has-text('Sign in')") + await page.wait_for_timeout(5000) + + # Open Budget File + print("[*] Opening 'My Finances' budget...") + await page.click("text=My Finances") + await page.wait_for_timeout(8000) + + # Loop through accounts and import them + for file_info in IMPORT_ACCOUNTS: + try: + await import_account(page, file_info) + except Exception as e: + print(f"[-] Exception occurred while processing '{file_info['name']}': {e}") + # Save screenshot of failure + safe_name = file_info["name"].replace(' ', '_') + await page.screenshot(path=f"{SCREENSHOT_DIR}/exception_{safe_name}.png") + + # Final screenshot of budget sidebar + # Click budget menu to go to main dashboard or budget overview + try: + await page.click("text=Budget") + await page.wait_for_timeout(5000) + await page.screenshot(path=f"{SCREENSHOT_DIR}/final_sidebar_overview.png") + print("[+] Saved final budget overview screenshot.") + except Exception as e: + print(f"[-] Failed to capture final overview: {e}") + + await browser.close() + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/4-Infrastructure/shim/failure_flexure_bank.py b/4-Infrastructure/shim/failure_flexure_bank.py new file mode 100644 index 00000000..6d5c2843 --- /dev/null +++ b/4-Infrastructure/shim/failure_flexure_bank.py @@ -0,0 +1,85 @@ +"""Failure Flexure Expansion — 50+ deliberately diverse failed/partial Lean proofs. + +Covers 8 failure types: missing_rewrite, missing_assumption, arithmetic_gap, +case_split_missing, induction_incomplete, simplifier_gap, coercion_mismatch, order_gap. + +Each theorem is designed to fail with the specific obstruction type. +""" + +FAILURE_THEOREMS = [ + # ── Missing rewrite direction (rw needs ← or different order) ── + ("rw_missing_dir_1", "theorem t (a b : Nat) (h : a = b) : b + 0 = a + 0 := by\n simp"), + ("rw_missing_dir_2", "theorem t (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by\n rfl"), + ("rw_missing_dir_3", "theorem t (a b : Nat) (h : a + b = b + a) : b + a = a + b := by\n rfl"), + ("rw_missing_dir_4", "theorem t (a b : Nat) (h : a = b) : a*2 = b*2 := by\n simp"), + ("rw_missing_dir_5", "theorem t (a b : Nat) (h : a = b) : a + 1 = b + 1 := by\n rfl"), + ("rw_missing_dir_6", "theorem t (a b : Nat) (h : a = b) : 0 + a = 0 + b := by\n simp"), + ("rw_missing_dir_7", "theorem t (a b : Nat) (h : a = b) (c : Nat) : a + c = b + c := by\n rfl"), + + # ── Missing assumption bridge (needs exact, assumption, apply) ── + ("missing_assume_1", "theorem t (A B : Prop) (hA : A) (hAB : A → B) : B := by\n rfl"), + ("missing_assume_2", "theorem t (A B C : Prop) (hA : A) (hAB : A → B) (hBC : B → C) : C := by\n simp"), + ("missing_assume_3", "theorem t (A B : Prop) (h : A ∧ B) : A := by\n rfl"), + ("missing_assume_4", "theorem t (A B : Prop) (h : A ∨ B) : A ∨ B := by\n simp"), + ("missing_assume_5", "theorem t (A B : Prop) (h : A → B) (hA : A) : B := by\n rfl"), + ("missing_assume_6", "theorem t (A B : Prop) : A → B → A := by\n rfl"), + ("missing_assume_7", "theorem t (P : Prop) : P → ¬¬P := by\n rfl"), + + # ── Arithmetic gap (needs omega, linarith, nlinarith) ── + ("arith_gap_1", "theorem t (a b : Nat) (h : a ≤ b) : a + 1 ≤ b + 1 := by\n rfl"), + ("arith_gap_2", "theorem t (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by\n simp"), + ("arith_gap_3", "theorem t (a b : Nat) (h : a + b = b + a) : a = b := by\n rfl"), + ("arith_gap_4", "theorem t (a b c : Nat) : a + b + c = a + c + b := by\n simp"), + ("arith_gap_5", "theorem t (a b : Nat) : a * (b + 1) = a * b + a := by\n simp"), + ("arith_gap_6", "theorem t (x : Nat) (h : x > 0) : x - 1 < x := by\n simp"), + ("arith_gap_7", "theorem t (a b : Nat) : a + b = b + a := by\n omega"), + ("arith_gap_8", "theorem t (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by\n simp"), + ("arith_gap_9", "theorem t (x : Nat) : x + x = 2 * x := by\n simp"), + ("arith_gap_10", "theorem t (n : Nat) : n + 0 = n := by\n rfl"), + + # ── Case split missing (needs cases, by_cases, constructor) ── + ("case_split_1", "theorem t (A B : Prop) (h : A ∨ B) : B ∨ A := by\n simp"), + ("case_split_2", "theorem t (A B C : Prop) (h : A ∧ B) (h2 : A → C) : C := by\n simp"), + ("case_split_3", "theorem t (A B : Prop) (hA : A) (hB : B) : A ∧ B := by\n rfl"), + ("case_split_4", "theorem t (A B : Prop) (h : A ∨ B) : A ∨ B := by\n rfl"), + ("case_split_5", "theorem t (A B : Prop) (h : A → B) : A ∨ B → B := by\n simp"), + ("case_split_6", "theorem t (A B : Prop) (hA : A) (hB : B) : A ∧ B := by\n simp"), + ("case_split_7", "theorem t (A B : Prop) (h : A ∧ B) : A := by\n simp"), + ("case_split_8", "theorem t (A : Prop) : A → A := by\n rfl"), + + # ── Induction incomplete (missing induction case handling) ── + ("induction_gap_1", "theorem t (n : Nat) : n + 0 = n := by\n simp"), + ("induction_gap_2", "theorem t (n m : Nat) : n + m.succ = (n + m).succ := by\n simp"), + ("induction_gap_3", "theorem t (n : Nat) : n * 0 = 0 := by\n simp"), + ("induction_gap_4", "theorem t (m n : Nat) : m + n = n + m := by\n omega"), + ("induction_gap_5", "theorem t (n : Nat) : 0 + n = n := by\n simp"), + ("induction_gap_6", "theorem t (n : Nat) : n + 0 = n := by\n rfl"), + ("induction_gap_7", "theorem t (n : Nat) : n ≤ n := by\n simp"), + ("induction_gap_8", "theorem t (n : Nat) : n - n = 0 := by\n simp"), + ("induction_gap_9", "theorem t (n : Nat) : n * 1 = n := by\n simp"), + ("induction_gap_10", "theorem t (n m : Nat) : n + m = m + n := by\n simp"), + + # ── Simplifier almost works (needs extra simp lemma) ── + ("simplifier_gap_1", "theorem t (l : List Nat) : l.reverse.reverse = l := by\n simp"), + ("simplifier_gap_2", "theorem t (l : List Nat) : [] ++ l = l := by\n simp"), + ("simplifier_gap_3", "theorem t (s : Set Nat) : s ∪ s = s := by\n simp"), + ("simplifier_gap_4", "theorem t (s : Set Nat) : s ∩ s = s := by\n simp"), + ("simplifier_gap_5", "theorem t (n : Nat) : n + 0 = n := by\n simp"), + ("simplifier_gap_6", "theorem t (a b : Nat) : a + b = b + a := by\n simp"), + + # ── Coercion / type mismatch ── + ("coercion_gap_1", "theorem t (n : Nat) : (n : Nat) = (n : Int) := by\n rfl"), + ("coercion_gap_2", "theorem t (n : Nat) : n = (n : Nat) := by\n rfl"), + ("coercion_gap_3", "theorem t (n : Nat) (m : Nat) : n + m = m + n := by\n omega"), + ("coercion_gap_4", "theorem t (x : Int) : (x : Nat) = (x : Int) := by\n rfl"), + + # ── Order / inequality gap ── + ("order_gap_1", "theorem t (a b : Nat) (h : a ≤ b) : a * 2 ≤ b * 2 := by\n simp"), + ("order_gap_2", "theorem t (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by\n rfl"), + ("order_gap_3", "theorem t (a b : Nat) (h : a ≤ b) : a + 1 ≤ b + 1 := by\n simp"), + ("order_gap_4", "theorem t (a b : Nat) : a ≤ a := by\n rfl"), + ("order_gap_5", "theorem t (a b : Nat) (h : a ≤ b) (h2 : b ≤ a) : a = b := by\n simp"), + ("order_gap_6", "theorem t (a b : Nat) (h : a ≤ b) : 0 ≤ b - a := by\n simp"), + ("order_gap_7", "theorem t (a b : Nat) (h : a < b) : a + 1 ≤ b := by\n simp"), + ("order_gap_8", "theorem t (a b : Nat) (h : a ≤ b) : a ≤ b + 1 := by\n simp"), +] diff --git a/4-Infrastructure/shim/route_repair_v11.py b/4-Infrastructure/shim/route_repair_v11.py new file mode 100644 index 00000000..d491ea53 --- /dev/null +++ b/4-Infrastructure/shim/route_repair_v11.py @@ -0,0 +1,265 @@ +#!/usr/bin/env python3 +"""Route-Repair Loop v1.1: Failure Flexure Expansion + full 13-dim v2 features.""" +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 + +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"] + +OBSTRUCTION_MAP = {"rw_missing_dir": "missing_rewrite_direction","missing_assume": "missing_assumption_bridge", + "arith_gap": "arithmetic_gap","case_split": "case_split_missing","induction_gap": "induction_incomplete", + "simplifier_gap": "simplifier_gap","coercion_gap": "coercion_mismatch","order_gap": "order_inequality_gap"} + +def obstruction_type(name): + for p, l in OBSTRUCTION_MAP.items(): + if name.startswith(p): return l + return "other" + +def classify_tactic(t): + tl=t.lower() + if "rw" in tl: return "rewrite" + if "simp" in tl: return "normalization" + if "omega" in tl or "nlinarith" in tl: return "arithmetic" + if "induction" in tl: return "induction" + if "cases" in tl or "constructor" in tl: return "case_analysis" + if "apply" in tl or "exact" in tl: return "discharge" + if "intro" in tl: return "introduction" + if "have" in tl: return "lemma_introduction" + if "rfl" in tl: return "reflexivity" + return "unknown" + +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 build_trace(name, code): + 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) + sp.update({"name":name,"status":"failed","obstruction":obstruction_type(name), + "tactic":code.split("by")[-1].strip() if "by" in code else "unknown","code":code}) + return sp + 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 ingest_failure_flexures(results): + conn=connect(); cur=conn.cursor() + sid=str(uuid.uuid4()) + cur.execute("INSERT INTO ene.sessions(id,title,event_type,content,metadata) VALUES(%s,%s,'failure_flexure','V1.1 Failure',%s::jsonb)", + (sid,"Failure Flexure v1.1",json.dumps({"source":"failure_flexure_bank","count":len(results)}))) + for r in results: + fid=str(uuid.uuid4()); tf=classify_tactic(r.get("tactic","")) + sp={k:r.get(k,0) for k in V2_FEATURES} + sig=json.dumps({"tactic":r.get("tactic","?"),"tactic_family":tf,"delta_score":abs(r.get("gap",r.get("spectral_gap",0)))*10, + "joint_label":f"{tf}_failed_{r.get('obstruction','?')}","obstruction_type":r.get("obstruction","?"), + "domain":"failure","proof_method":tf,"rrc_shape":"HoldForUnlawfulOrUnderspecifiedShape", + "spectral":sp,"feature_version":"flexure-spectrum-v2"}) + sd=int(hashlib.sha256(r.get("name","?").encode()).hexdigest()[:4],16)%255 + cur.execute("INSERT INTO ene.flexures(id,session_id,step_index,pre_sidon_label,pre_residual,available_crossings,chosen_crossing,decision_signals,post_sidon_label,post_residual,converged) VALUES(%s,%s,%s,%s,%s,%s::jsonb,%s::jsonb,%s::jsonb,%s,%s,%s)", + (fid,sid,0,sd,0.5,"[]",json.dumps({"name":r.get("name","?")}),sig,sd%255,0.5,False)) + conn.commit(); cur.close(); conn.close() + return sid + +def route_repair(name, code, library_session, failure_session, max_attempts=5): + resp=prove(code,name+"_init") + if resp.get("ok",False): + return {"name":name,"initial_status":"verified","recovered":False,"notes":"already verified"} + instr,tags=instrument_theorem(code) + if tags: + 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 + else: mat=[[1]] + sp=compute_spectral(mat) + vec=[sp.get(k,0) for k in V2_FEATURES] + + 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,"tf":sig.get("tactic_family","?"),"obs":sig.get("obstruction_type","?"),"jl":sig.get("joint_label","?")}) + cur.close(); conn.close() + + 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] + votes=Counter(lib["obs"] for _,lib in top3) + predicted_obs=votes.most_common(1)[0][0] if votes else "other" + + # Map obstruction type to patch family + obs_to_family = {"missing_rewrite_direction":"rewrite","missing_assumption_bridge":"discharge", + "arithmetic_gap":"arithmetic","case_split_missing":"case_analysis", + "induction_incomplete":"induction","simplifier_gap":"normalization", + "coercion_mismatch":"normalization","order_inequality_gap":"arithmetic"} + predicted_family = obs_to_family.get(predicted_obs, "normalization") + + # Extract actual hypothesis names from the theorem + hyps = re.findall(r'\(([^)]+:\s*[^)]+)\)', code) + hyp_names = [] + for h in hyps: + parts = h.split(":") + names_part = parts[0].strip() + for n in names_part.split(): + if n.strip(): + hyp_names.append(n.strip()) + first_hyp = hyp_names[0] if hyp_names else "h" + + pc=[] + if predicted_family=="rewrite": + pc+=["rw ["+first_hyp+"]","rw [← "+first_hyp+"]"] + elif predicted_family=="discharge": + pc+=["exact "+first_hyp,"assumption","apply "+first_hyp] + elif predicted_family=="normalization": + pc+=["simp","norm_num"] + elif predicted_family=="arithmetic": + pc+=["omega"] + elif predicted_family=="case_analysis": + pc+=["cases h","constructor"] + elif predicted_family=="induction": + pc+=["induction n"] + else: pc+=["simp","omega"] + + 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(pc[:max_attempts]): + patched=code.split(":=")[0]+":=" if ":=" in code else code + patched+="\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,"family":predicted_family,"ok":ok,"delta":delta}) + + return {"name":name,"obstruction":obstruction_type(name),"initial_status":"failed", + "predicted_family":predicted_family,"recovered":recovered,"best_delta":best_delta, + "partial_improvement":best_delta>0,"attempts":attempts,"best_attempt":best_attempt} + +def main(): + print("V1.1: Failure Flexure Expansion + 13-dim v2 features\n") + traced=[] + for i,(n,c) in enumerate(FAILURE_THEOREMS): + print(f" [{i+1}/{len(FAILURE_THEOREMS)}] {n:35s} ... ",end="",flush=True) + r=build_trace(n,c) + if r is None: print("SKIP") + else: + traced.append(r) + print(f"n={r.get('matrix_size','?'):2d} obs={r.get('obstruction','?')[:20]}") + print(f"\n Traced: {len(traced)}/{len(FAILURE_THEOREMS)}") + + failure_session=ingest_failure_flexures(traced) + print(f" Failure session: {failure_session}") + + combined_session="a4a0eb20-93fe-413e-8e0b-50334bb778d8" + test_set=FAILURE_THEOREMS[:30] + results=[] + rec=part=worse=0; td=0; dc=0 + + 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,combined_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} pred={r['predicted_family']:12s} delta={r['best_delta']:+d}") + results.append(r) + if r["recovered"]: rec+=1 + if r.get("partial_improvement"): part+=1 + if r["best_delta"]<0: worse+=1 + td+=r["best_delta"]; dc+=1 + + n=len(results); ad=td/max(dc,1) + print(f"\n{'='*60}\nROUTE-REPAIR V1.1\n{'='*60}") + print(f"Test set: {n} failed | Recovered: {rec} ({rec/max(n,1):.0%}) | Partial: {part} ({part/max(n,1):.0%}) | Avg ΔC: {ad:.2f}") + + by_obs=defaultdict(lambda:{"t":0,"r":0,"p":0,"d":0}) + for r in results: + o=r.get("obstruction","?"); by_obs[o]["t"]+=1 + if r["recovered"]: by_obs[o]["r"]+=1 + if r.get("partial_improvement"): by_obs[o]["p"]+=1 + by_obs[o]["d"]+=r["best_delta"] + print(f"\nPer-obstruction:") + for o,s in sorted(by_obs.items(),key=lambda x:-x[1]["t"]): + print(f" {o:30s}: n={s['t']:2d} rec={s['r']/max(s['t'],1):.0%} part={s['p']/max(s['t'],1):.0%} ΔC={s['d']/max(s['t'],1):+.1f}") + + rp={"n":n,"recovered":rec,"partial_improvement":part,"avg_delta":round(ad,2), + "failure_session_id":failure_session,"combined_session_id":combined_session,"results":results} + rp_path=os.path.join(os.path.dirname(__file__),"../..","shared-data/pist_route_repair_v11_benchmark.json") + with open(rp_path,"w") as f: json.dump(rp,f,indent=2) + print(f"\nReport: {rp_path}") + +if __name__=="__main__": + main() diff --git a/shared-data/pist_route_repair_v11_benchmark.json b/shared-data/pist_route_repair_v11_benchmark.json new file mode 100644 index 00000000..468a585d --- /dev/null +++ b/shared-data/pist_route_repair_v11_benchmark.json @@ -0,0 +1,850 @@ +{ + "n": 28, + "recovered": 0, + "partial_improvement": 0, + "avg_delta": 0.0, + "failure_session_id": "a89baf86-3536-4453-8e2c-7c66d54cf389", + "combined_session_id": "a4a0eb20-93fe-413e-8e0b-50334bb778d8", + "results": [ + { + "name": "rw_missing_dir_1", + "obstruction": "missing_rewrite_direction", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "rw_missing_dir_2", + "obstruction": "missing_rewrite_direction", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "rw_missing_dir_3", + "obstruction": "missing_rewrite_direction", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "rw_missing_dir_4", + "obstruction": "missing_rewrite_direction", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "rw_missing_dir_5", + "obstruction": "missing_rewrite_direction", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "rw_missing_dir_6", + "obstruction": "missing_rewrite_direction", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "rw_missing_dir_7", + "obstruction": "missing_rewrite_direction", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "missing_assume_1", + "obstruction": "missing_assumption_bridge", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "missing_assume_2", + "obstruction": "missing_assumption_bridge", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "missing_assume_3", + "obstruction": "missing_assumption_bridge", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "missing_assume_4", + "obstruction": "missing_assumption_bridge", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "missing_assume_5", + "obstruction": "missing_assumption_bridge", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "missing_assume_6", + "obstruction": "missing_assumption_bridge", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "missing_assume_7", + "obstruction": "missing_assumption_bridge", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [P]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 P]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [P]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_1", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_2", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_3", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_4", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_5", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_6", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [x]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 x]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [x]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_8", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [a]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 a]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [a]", + "delta": 0, + "ok": false + } + }, + { + "name": "arith_gap_9", + "obstruction": "arithmetic_gap", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [x]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 x]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [x]", + "delta": 0, + "ok": false + } + }, + { + "name": "case_split_1", + "obstruction": "case_split_missing", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "case_split_2", + "obstruction": "case_split_missing", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "case_split_3", + "obstruction": "case_split_missing", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "case_split_4", + "obstruction": "case_split_missing", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "case_split_5", + "obstruction": "case_split_missing", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + }, + { + "name": "case_split_6", + "obstruction": "case_split_missing", + "initial_status": "failed", + "predicted_family": "rewrite", + "recovered": false, + "best_delta": 0, + "partial_improvement": false, + "attempts": [ + { + "attempt": 1, + "patch": "rw [A]", + "family": "rewrite", + "ok": false, + "delta": 0 + }, + { + "attempt": 2, + "patch": "rw [\u2190 A]", + "family": "rewrite", + "ok": false, + "delta": 0 + } + ], + "best_attempt": { + "patch": "rw [A]", + "delta": 0, + "ok": false + } + } + ] +} \ No newline at end of file