mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
feat(pist): Route-Repair v1.1 — 60 failure flexures ingested, obstruction-type voting
This commit is contained in:
Brandon Schneider
parent
e9843fc9ce
commit
34768b3fe8
9 changed files with 1504 additions and 0 deletions
|
|
@ -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
|
||||
11
4-Infrastructure/k3s-flake/manifests/actual-budget/pvc.yaml
Normal file
11
4-Infrastructure/k3s-flake/manifests/actual-budget/pvc.yaml
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
apiVersion: v1
|
||||
kind: PersistentVolumeClaim
|
||||
metadata:
|
||||
name: actual-budget-data
|
||||
namespace: services
|
||||
spec:
|
||||
accessModes:
|
||||
- ReadWriteOnce
|
||||
resources:
|
||||
requests:
|
||||
storage: 2Gi
|
||||
|
|
@ -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
|
||||
|
|
@ -9,3 +9,5 @@ resources:
|
|||
- pulse-receiver
|
||||
- homarr
|
||||
- authentik
|
||||
- actual-budget
|
||||
|
||||
|
|
|
|||
101
4-Infrastructure/scripts/run_import_workflow.py
Normal file
101
4-Infrastructure/scripts/run_import_workflow.py
Normal file
|
|
@ -0,0 +1,101 @@
|
|||
import asyncio
|
||||
from playwright.async_api import async_playwright
|
||||
import os
|
||||
|
||||
PASSWORD = "v1D7TtupOMq8pK"
|
||||
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())
|
||||
141
4-Infrastructure/scripts/run_multi_import.py
Normal file
141
4-Infrastructure/scripts/run_multi_import.py
Normal file
|
|
@ -0,0 +1,141 @@
|
|||
import asyncio
|
||||
from playwright.async_api import async_playwright
|
||||
import os
|
||||
import glob
|
||||
import re
|
||||
|
||||
PASSWORD = "v1D7TtupOMq8pK"
|
||||
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())
|
||||
85
4-Infrastructure/shim/failure_flexure_bank.py
Normal file
85
4-Infrastructure/shim/failure_flexure_bank.py
Normal file
|
|
@ -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"),
|
||||
]
|
||||
265
4-Infrastructure/shim/route_repair_v11.py
Normal file
265
4-Infrastructure/shim/route_repair_v11.py
Normal file
|
|
@ -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()
|
||||
850
shared-data/pist_route_repair_v11_benchmark.json
Normal file
850
shared-data/pist_route_repair_v11_benchmark.json
Normal file
|
|
@ -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
|
||||
}
|
||||
}
|
||||
]
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue