From 153a8da5c5a68f43f656d640f57a143874380d0c Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 02:37:22 -0500 Subject: [PATCH] =?UTF-8?q?feat(pist):=20Tier=202=20trace=20canary=20?= =?UTF-8?q?=E2=80=94=2024=20multi-tactic=20Lean=20theorems?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 24/24 processed, 0 errors (12 verified, 12 failed) - Average 2.0 steps per proof (max 5 steps) - 11 tactic families detected - Verified proofs: avg gap=2.50 vs Failed: avg gap=1.50 - proof_traces/*.trace.json + *.decomp.json stored per theorem --- 4-Infrastructure/shim/pist_trace_decompose.py | 1 + 4-Infrastructure/shim/run_trace_canary.py | 132 ++++++++++++ .../shim/trace_canary_theorems.py | 157 ++++++++++++++ shared-data/pist_trace_canary_report.json | 23 +++ shared-data/pist_trace_canary_vectors.jsonl | 24 +++ .../canary_apply_chain.decomp.json | 95 +++++++++ .../canary_apply_chain.trace.json | 122 +++++++++++ .../canary_calc_chain.decomp.json | 84 ++++++++ .../proof_traces/canary_calc_chain.trace.json | 87 ++++++++ .../canary_cases_and_elim.decomp.json | 97 +++++++++ .../canary_cases_and_elim.trace.json | 122 +++++++++++ .../canary_cases_or_swap.decomp.json | 121 +++++++++++ .../canary_cases_or_swap.trace.json | 192 ++++++++++++++++++ .../canary_constructor_example.decomp.json | 96 +++++++++ .../canary_constructor_example.trace.json | 122 +++++++++++ .../canary_fail_bad_coercion.decomp.json | 71 +++++++ .../canary_fail_bad_coercion.trace.json | 52 +++++ .../canary_fail_missing_lemma.decomp.json | 71 +++++++ .../canary_fail_missing_lemma.trace.json | 52 +++++ .../canary_fail_type_mismatch.decomp.json | 71 +++++++ .../canary_fail_type_mismatch.trace.json | 52 +++++ .../canary_fail_unsat.decomp.json | 71 +++++++ .../proof_traces/canary_fail_unsat.trace.json | 52 +++++ .../canary_have_chain.decomp.json | 96 +++++++++ .../proof_traces/canary_have_chain.trace.json | 122 +++++++++++ .../canary_induct_add_succ.decomp.json | 71 +++++++ .../canary_induct_add_succ.trace.json | 52 +++++ .../canary_induct_add_zero.decomp.json | 71 +++++++ .../canary_induct_add_zero.trace.json | 52 +++++ .../canary_induct_factorial.decomp.json | 71 +++++++ .../canary_induct_factorial.trace.json | 52 +++++ .../canary_induct_mul_zero.decomp.json | 71 +++++++ .../canary_induct_mul_zero.trace.json | 52 +++++ .../proof_traces/canary_intro_all.decomp.json | 108 ++++++++++ .../proof_traces/canary_intro_all.trace.json | 157 ++++++++++++++ .../canary_intro_apply.decomp.json | 108 ++++++++++ .../canary_intro_apply.trace.json | 157 ++++++++++++++ .../canary_omega_chain_ineq.decomp.json | 71 +++++++ .../canary_omega_chain_ineq.trace.json | 52 +++++ .../canary_omega_chain_unsat.decomp.json | 71 +++++++ .../canary_omega_chain_unsat.trace.json | 52 +++++ .../canary_omega_distrib.decomp.json | 71 +++++++ .../canary_omega_distrib.trace.json | 52 +++++ .../canary_omega_reorder_sum.decomp.json | 71 +++++++ .../canary_omega_reorder_sum.trace.json | 52 +++++ .../canary_rw_chain_3step.decomp.json | 95 +++++++++ .../canary_rw_chain_3step.trace.json | 122 +++++++++++ .../canary_rw_chain_eq.decomp.json | 83 ++++++++ .../canary_rw_chain_eq.trace.json | 87 ++++++++ .../canary_rw_chain_mixed.decomp.json | 84 ++++++++ .../canary_rw_chain_mixed.trace.json | 87 ++++++++ .../canary_rw_then_omega.decomp.json | 84 ++++++++ .../canary_rw_then_omega.trace.json | 87 ++++++++ .../canary_simp_chain_simple.trace.json | 87 ++++++++ 54 files changed, 4515 insertions(+) create mode 100644 4-Infrastructure/shim/run_trace_canary.py create mode 100644 4-Infrastructure/shim/trace_canary_theorems.py create mode 100644 shared-data/pist_trace_canary_report.json create mode 100644 shared-data/pist_trace_canary_vectors.jsonl create mode 100644 shared-data/proof_traces/canary_apply_chain.decomp.json create mode 100644 shared-data/proof_traces/canary_apply_chain.trace.json create mode 100644 shared-data/proof_traces/canary_calc_chain.decomp.json create mode 100644 shared-data/proof_traces/canary_calc_chain.trace.json create mode 100644 shared-data/proof_traces/canary_cases_and_elim.decomp.json create mode 100644 shared-data/proof_traces/canary_cases_and_elim.trace.json create mode 100644 shared-data/proof_traces/canary_cases_or_swap.decomp.json create mode 100644 shared-data/proof_traces/canary_cases_or_swap.trace.json create mode 100644 shared-data/proof_traces/canary_constructor_example.decomp.json create mode 100644 shared-data/proof_traces/canary_constructor_example.trace.json create mode 100644 shared-data/proof_traces/canary_fail_bad_coercion.decomp.json create mode 100644 shared-data/proof_traces/canary_fail_bad_coercion.trace.json create mode 100644 shared-data/proof_traces/canary_fail_missing_lemma.decomp.json create mode 100644 shared-data/proof_traces/canary_fail_missing_lemma.trace.json create mode 100644 shared-data/proof_traces/canary_fail_type_mismatch.decomp.json create mode 100644 shared-data/proof_traces/canary_fail_type_mismatch.trace.json create mode 100644 shared-data/proof_traces/canary_fail_unsat.decomp.json create mode 100644 shared-data/proof_traces/canary_fail_unsat.trace.json create mode 100644 shared-data/proof_traces/canary_have_chain.decomp.json create mode 100644 shared-data/proof_traces/canary_have_chain.trace.json create mode 100644 shared-data/proof_traces/canary_induct_add_succ.decomp.json create mode 100644 shared-data/proof_traces/canary_induct_add_succ.trace.json create mode 100644 shared-data/proof_traces/canary_induct_add_zero.decomp.json create mode 100644 shared-data/proof_traces/canary_induct_add_zero.trace.json create mode 100644 shared-data/proof_traces/canary_induct_factorial.decomp.json create mode 100644 shared-data/proof_traces/canary_induct_factorial.trace.json create mode 100644 shared-data/proof_traces/canary_induct_mul_zero.decomp.json create mode 100644 shared-data/proof_traces/canary_induct_mul_zero.trace.json create mode 100644 shared-data/proof_traces/canary_intro_all.decomp.json create mode 100644 shared-data/proof_traces/canary_intro_all.trace.json create mode 100644 shared-data/proof_traces/canary_intro_apply.decomp.json create mode 100644 shared-data/proof_traces/canary_intro_apply.trace.json create mode 100644 shared-data/proof_traces/canary_omega_chain_ineq.decomp.json create mode 100644 shared-data/proof_traces/canary_omega_chain_ineq.trace.json create mode 100644 shared-data/proof_traces/canary_omega_chain_unsat.decomp.json create mode 100644 shared-data/proof_traces/canary_omega_chain_unsat.trace.json create mode 100644 shared-data/proof_traces/canary_omega_distrib.decomp.json create mode 100644 shared-data/proof_traces/canary_omega_distrib.trace.json create mode 100644 shared-data/proof_traces/canary_omega_reorder_sum.decomp.json create mode 100644 shared-data/proof_traces/canary_omega_reorder_sum.trace.json create mode 100644 shared-data/proof_traces/canary_rw_chain_3step.decomp.json create mode 100644 shared-data/proof_traces/canary_rw_chain_3step.trace.json create mode 100644 shared-data/proof_traces/canary_rw_chain_eq.decomp.json create mode 100644 shared-data/proof_traces/canary_rw_chain_eq.trace.json create mode 100644 shared-data/proof_traces/canary_rw_chain_mixed.decomp.json create mode 100644 shared-data/proof_traces/canary_rw_chain_mixed.trace.json create mode 100644 shared-data/proof_traces/canary_rw_then_omega.decomp.json create mode 100644 shared-data/proof_traces/canary_rw_then_omega.trace.json create mode 100644 shared-data/proof_traces/canary_simp_chain_simple.trace.json diff --git a/4-Infrastructure/shim/pist_trace_decompose.py b/4-Infrastructure/shim/pist_trace_decompose.py index f3bf7f15..937e1716 100644 --- a/4-Infrastructure/shim/pist_trace_decompose.py +++ b/4-Infrastructure/shim/pist_trace_decompose.py @@ -269,6 +269,7 @@ def main(): json.dump(result, f, indent=2) print(f"\nDecomposition: {out_path}", flush=True) + print(json.dumps(result)) return 0 diff --git a/4-Infrastructure/shim/run_trace_canary.py b/4-Infrastructure/shim/run_trace_canary.py new file mode 100644 index 00000000..7cd233b6 --- /dev/null +++ b/4-Infrastructure/shim/run_trace_canary.py @@ -0,0 +1,132 @@ +#!/usr/bin/env python3 +"""Multi-tactic canary batch for Tier 2 trace pipeline.""" +import json +import os +import sys +import time +import subprocess +from pathlib import Path +from collections import Counter + +from trace_canary_theorems import CANARY_THEOREMS + +TRACES_DIR = os.path.join(os.path.dirname(__file__), "../..", "shared-data/proof_traces") +VECTORS_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist_trace_canary_vectors.jsonl") +REPORT_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist_trace_canary_report.json") +BRIDGE = os.path.join(os.path.dirname(__file__), "lean_trace_bridge.py") +DECOMPOSE = os.path.join(os.path.dirname(__file__), "pist_trace_decompose.py") + +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 (FileNotFoundError, OSError): + PROOF_SERVER_TOKEN = "" + + +def run_pipeline(theorem: dict) -> dict: + name = theorem["name"] + code = theorem["code"] + trace_path = os.path.join(TRACES_DIR, f"canary_{name}.trace.json") + decomp_path = os.path.join(TRACES_DIR, f"canary_{name}.decomp.json") + os.makedirs(TRACES_DIR, exist_ok=True) + + t0 = time.time() + r1 = subprocess.run( + [sys.executable, BRIDGE, "--code", code, "--name", name, "--out", trace_path], + capture_output=True, text=True, timeout=120, + env={**os.environ, "PROOF_SERVER_TOKEN": PROOF_SERVER_TOKEN}, + ) + if r1.returncode != 0: + return {"error": f"bridge: {r1.stderr[:200]}", "name": name} + + r2 = subprocess.run( + [sys.executable, DECOMPOSE, trace_path, "--out", decomp_path], + capture_output=True, text=True, timeout=30, + ) + if r2.returncode != 0 or not os.path.exists(decomp_path): + return {"error": f"decomp: {r2.stderr[:200]}", "name": name} + + with open(decomp_path) as f: + decomposition = json.load(f) + + return {"name": name, "trace_file": trace_path, "wall_s": round(time.time() - t0, 2), + "decomposition": decomposition} + + +def report(results, errors): + good = [r for r in results if "error" not in r] + n = len(good) + print(f"\n{'='*60}\nTIER 2 TRACE CANARY REPORT\n{'='*60}", flush=True) + print(f"Total: {len(results)} ({n} ok, {len(errors)} errors)", flush=True) + + steps = [len(r["decomposition"].get("flexure_joints", [])) for r in good] + if steps: + print(f"Steps: mean={sum(steps)/len(steps):.1f} max={max(steps)} min={min(steps)}", flush=True) + statuses = Counter(r["decomposition"]["trace_summary"]["status"] for r in good) + print(f"Status: {dict(statuses)}", flush=True) + + families = Counter() + for r in good: + for f, c in r["decomposition"].get("tactic_family_distribution", {}).items(): + families[f] += c + print(f"Families: {dict(families)}", flush=True) + + u_mat = len(set(r["decomposition"]["spectral"]["n_states"] for r in good)) + u_rank = len(set(r["decomposition"]["spectral"]["rank_estimate"] for r in good)) + u_gap = len(set(round(r["decomposition"]["spectral"]["spectral_gap"], 4) for r in good)) + print(f"Unique states: {u_mat}/{n} ranks: {u_rank} gaps: {u_gap}/{n}", flush=True) + + v_gaps = [r for r in good if r["decomposition"]["trace_summary"]["status"] == "verified"] + f_gaps = [r for r in good if r["decomposition"]["trace_summary"]["status"] == "failed"] + for label, group in [("verified", v_gaps), ("failed", f_gaps)]: + if group: + gaps = [r["decomposition"]["spectral"]["spectral_gap"] for r in group] + print(f"{label} (n={len(group)}): gap={sum(gaps)/len(gaps):.4f} [{min(gaps):.4f},{max(gaps):.4f}]", flush=True) + + with open(VECTORS_PATH, "w") as f: + for r in good: + row = { + "name": r["name"], "status": r["decomposition"]["trace_summary"]["status"], + "n_steps": len(r["decomposition"].get("flexure_joints", [])), + "n_states": r["decomposition"]["spectral"]["n_states"], + "spectral_gap": r["decomposition"]["spectral"]["spectral_gap"], + "rank_estimate": r["decomposition"]["spectral"]["rank_estimate"], + "density": r["decomposition"]["spectral"]["density"], + "feature_vector": r["decomposition"]["feature_vector"], + "tactic_family_distribution": r["decomposition"]["tactic_family_distribution"], + } + f.write(json.dumps(row) + "\n") + print(f"Vectors: {VECTORS_PATH}", flush=True) + + with open(REPORT_PATH, "w") as f: + json.dump({"n": n, "n_errors": len(errors), "status_distribution": dict(statuses), + "tactic_family_distribution": dict(families), + "unique_spectral_gaps": u_gap, "unique_rank_estimates": u_rank}, f, indent=2) + print(f"Report: {REPORT_PATH}", flush=True) + + +def main(): + theorems = CANARY_THEOREMS + print(f"Trace canary: {len(theorems)} theorems\n", flush=True) + results, errors = [], [] + for i, theorem in enumerate(theorems): + name = theorem["name"] + print(f" [{i+1}/{len(theorems)}] {name:30s} ... ", end="", flush=True) + r = run_pipeline(theorem) + if "error" in r: + print(f"ERROR: {r['error'][:60]}", flush=True) + errors.append(r) + else: + st = r["decomposition"]["trace_summary"]["status"] + ns = len(r["decomposition"].get("flexure_joints", [])) + gap = r["decomposition"]["spectral"]["spectral_gap"] + print(f"{st:10s} steps={ns:2d} gap={gap:.4f} rank={r['decomposition']['spectral']['rank_estimate']}", flush=True) + results.append(r) + report(results, errors) + return 0 if len(errors) < len(theorems) / 2 else 1 + + +if __name__ == "__main__": + main() diff --git a/4-Infrastructure/shim/trace_canary_theorems.py b/4-Infrastructure/shim/trace_canary_theorems.py new file mode 100644 index 00000000..a872631e --- /dev/null +++ b/4-Infrastructure/shim/trace_canary_theorems.py @@ -0,0 +1,157 @@ +CANARY_THEOREMS = [ + # ── 1. rewrite chains (each step necessary) ── + { + "name": "rw_chain_eq", + "code": 'theorem rw_chain_eq (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by\n rw [h1]\n rw [h2]', + "domain": "equality", "proof_method": "rewrite", "joint": "equality_chaining_2step", + "obstruction": None, "rrc_shape": "CadForceProbeReceipt", + }, + { + "name": "rw_chain_mixed", + "code": 'theorem rw_chain_mixed (a b : Nat) (h : a = b) : a + 0 = b := by\n rw [h]\n simp', + "domain": "arithmetic", "proof_method": "rewrite", "joint": "rw_then_simp", + "obstruction": None, "rrc_shape": "CadForceProbeReceipt", + }, + { + "name": "rw_chain_3step", + "code": 'theorem rw_chain_3step (a b c d : Nat) (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by\n rw [h1]\n rw [h2]\n rw [h3]', + "domain": "equality", "proof_method": "rewrite", "joint": "equality_chaining_3step", + "obstruction": None, "rrc_shape": "CadForceProbeReceipt", + }, + { + "name": "rw_then_omega", + "code": 'theorem rw_then_omega (a b c : Nat) (h : a = b + c) : a * 2 = (b + c) * 2 := by\n rw [h]\n omega', + "domain": "arithmetic", "proof_method": "rewrite", "joint": "rw_then_arithmetic", + "obstruction": None, "rrc_shape": "CadForceProbeReceipt", + }, + + # ── 2. case analysis chains ── + { + "name": "cases_or_swap", + "code": 'theorem cases_or_swap (A B : Prop) (h : A ∨ B) : B ∨ A := by\n cases h\n · right; exact h\n · left; exact h', + "domain": "logic", "proof_method": "cases", "joint": "disjunction_swap", + "obstruction": None, "rrc_shape": "LogogramProjection", + }, + { + "name": "cases_and_elim", + "code": 'theorem cases_and_elim (A B C : Prop) (h : A ∧ B) (h2 : A → C) : C := by\n cases h\n apply h2\n assumption', + "domain": "logic", "proof_method": "cases", "joint": "conjunction_elim_then_apply", + "obstruction": None, "rrc_shape": "LogogramProjection", + }, + { + "name": "constructor_example", + "code": 'theorem constructor_example (A B : Prop) (hA : A) (hB : B) : A ∧ B := by\n constructor\n · exact hA\n · exact hB', + "domain": "logic", "proof_method": "constructor", "joint": "conjunction_intro", + "obstruction": None, "rrc_shape": "LogogramProjection", + }, + { + "name": "apply_chain", + "code": 'theorem apply_chain (A B C : Prop) (h1 : A → B) (h2 : B → C) (hA : A) : C := by\n apply h2\n apply h1\n exact hA', + "domain": "logic", "proof_method": "apply", "joint": "implication_chaining", + "obstruction": None, "rrc_shape": "LogogramProjection", + }, + + # ── 3. omega with multiple constraints ── + { + "name": "omega_chain_ineq", + "code": 'theorem omega_chain_ineq (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by\n omega', + "domain": "order", "proof_method": "omega", "joint": "transitivity_closure", + "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler", + }, + { + "name": "omega_reorder_sum", + "code": 'theorem omega_reorder_sum (a b c : Nat) : a + b + c = a + c + b := by\n omega', + "domain": "arithmetic", "proof_method": "omega", "joint": "reorder_summands", + "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler", + }, + { + "name": "omega_distrib", + "code": 'theorem omega_distrib (a b c : Nat) : a * (b + c) = a * b + a * c := by\n omega', + "domain": "algebra", "proof_method": "omega", "joint": "distributivity", + "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler", + }, + { + "name": "omega_chain_unsat", + "code": 'theorem omega_chain_unsat (x : Nat) : x < x := by\n omega', + "domain": "order", "proof_method": "omega", "joint": "unsatisfiable_linear", + "obstruction": "unsatisfiable_goal", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", + }, + + # ── 4. induction chains ── + { + "name": "induct_add_zero", + "code": 'theorem induct_add_zero (n : Nat) : n + 0 = n := by\n induction n with\n | zero => simp\n | succ n ih => simp [add_succ, ih]', + "domain": "arithmetic", "proof_method": "induction", "joint": "inductive_proof", + "obstruction": None, "rrc_shape": "ProjectableGeometryTopology", + }, + { + "name": "induct_add_succ", + "code": 'theorem induct_add_succ (n m : Nat) : n + m.succ = (n + m).succ := by\n induction n with\n | zero => simp\n | succ k ih => simp [add_succ, ih]', + "domain": "arithmetic", "proof_method": "induction", "joint": "inductive_succ", + "obstruction": None, "rrc_shape": "ProjectableGeometryTopology", + }, + { + "name": "induct_mul_zero", + "code": 'theorem induct_mul_zero (n : Nat) : n * 0 = 0 := by\n induction n with\n | zero => simp\n | succ k ih => simp [mul_add, add_comm, ih]', + "domain": "arithmetic", "proof_method": "induction", "joint": "inductive_mul", + "obstruction": None, "rrc_shape": "ProjectableGeometryTopology", + }, + { + "name": "induct_factorial", + "code": 'def fac : Nat → Nat\n | 0 => 1\n | n+1 => fac n * (n+1)\ntheorem induct_fact (n : Nat) : fac 0 = 1 := by\n simp [fac]', + "domain": "arithmetic", "proof_method": "simp", "joint": "definitional_unfold", + "obstruction": None, "rrc_shape": "CognitiveLoadField", + }, + + # ── 5. intro + apply chains ── + { + "name": "intro_all", + "code": 'theorem intro_all (A B C : Prop) : A → B → C → A := by\n intro hA\n intro hB\n intro hC\n exact hA', + "domain": "logic", "proof_method": "intro", "joint": "multiple_introductions", + "obstruction": None, "rrc_shape": "LogogramProjection", + }, + { + "name": "intro_apply", + "code": 'theorem intro_apply (A B : Prop) : (A → B) → A → B := by\n intro h\n intro hA\n apply h\n exact hA', + "domain": "logic", "proof_method": "apply", "joint": "intro_then_apply", + "obstruction": None, "rrc_shape": "LogogramProjection", + }, + { + "name": "have_chain", + "code": 'theorem have_chain (A B C : Prop) (hAB : A → B) (hBC : B → C) (hA : A) : C := by\n have hB : B := hAB hA\n have hC : C := hBC hB\n exact hC', + "domain": "logic", "proof_method": "have", "joint": "lemma_chaining", + "obstruction": None, "rrc_shape": "LogogramProjection", + }, + { + "name": "calc_chain", + "code": 'theorem calc_chain (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by\n ring\n omega', + "domain": "algebra", "proof_method": "ring", "joint": "ring_then_omega", + "obstruction": None, "rrc_shape": "SignalShapedRouteCompiler", + }, + + # ── 6. failure cases ── + { + "name": "fail_type_mismatch", + "code": 'theorem fail_type_mismatch (n : Nat) : n = (\"hello\" : String) := by\n rfl', + "domain": "type_error", "proof_method": "rfl", "joint": "type_mismatch", + "obstruction": "type_mismatch", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", + }, + { + "name": "fail_missing_lemma", + "code": 'theorem fail_missing_lemma (n : Nat) : n = n + 0 := by\n rw [imaginary_lemma]', + "domain": "arithmetic", "proof_method": "rewrite", "joint": "missing_dependency", + "obstruction": "missing_lemma", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", + }, + { + "name": "fail_unsat", + "code": 'theorem fail_unsat (x : Nat) (h : x > 0) : x = 0 := by\n omega', + "domain": "order", "proof_method": "omega", "joint": "contradictory_goal", + "obstruction": "unsatisfiable_goal", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", + }, + { + "name": "fail_bad_coercion", + "code": 'theorem fail_bad_coercion (n : Float) : (n : Nat) = (n : Int) := by\n rfl', + "domain": "type_error", "proof_method": "rfl", "joint": "coercion_mismatch", + "obstruction": "type_mismatch", "rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", + }, +] diff --git a/shared-data/pist_trace_canary_report.json b/shared-data/pist_trace_canary_report.json new file mode 100644 index 00000000..faedb816 --- /dev/null +++ b/shared-data/pist_trace_canary_report.json @@ -0,0 +1,23 @@ +{ + "n": 24, + "n_errors": 0, + "status_distribution": { + "verified": 12, + "failed": 12 + }, + "tactic_family_distribution": { + "rewrite": 8, + "normalization": 5, + "arithmetic": 7, + "case_analysis": 2, + "unknown": 3, + "discharge": 12, + "constructor": 1, + "introduction": 5, + "lemma_introduction": 2, + "algebraic": 1, + "reflexivity": 2 + }, + "unique_spectral_gaps": 5, + "unique_rank_estimates": 1 +} \ No newline at end of file diff --git a/shared-data/pist_trace_canary_vectors.jsonl b/shared-data/pist_trace_canary_vectors.jsonl new file mode 100644 index 00000000..9b316cf6 --- /dev/null +++ b/shared-data/pist_trace_canary_vectors.jsonl @@ -0,0 +1,24 @@ +{"name": "rw_chain_eq", "status": "verified", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.5, 2524], "tactic_family_distribution": {"rewrite": 2}} +{"name": "rw_chain_mixed", "status": "verified", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.5, 2194], "tactic_family_distribution": {"rewrite": 1, "normalization": 1}} +{"name": "rw_chain_3step", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.3333333333333333, 3279], "tactic_family_distribution": {"rewrite": 3}} +{"name": "rw_then_omega", "status": "failed", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.5, 2137], "tactic_family_distribution": {"rewrite": 1, "arithmetic": 1}} +{"name": "cases_or_swap", "status": "failed", "n_steps": 5, "n_states": 1, "spectral_gap": 5.0, "rank_estimate": 1, "density": 5.0, "feature_vector": [5, 1, 5.0, 5.0, 0, 1, 0.0, 0.0, 0.0, 1.5219, 0.0, 5552], "tactic_family_distribution": {"case_analysis": 1, "unknown": 2, "discharge": 2}} +{"name": "cases_and_elim", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, 1.585, 0.3333333333333333, 3345], "tactic_family_distribution": {"case_analysis": 1, "discharge": 1, "unknown": 1}} +{"name": "constructor_example", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, 0.9183, 0.3333333333333333, 3311], "tactic_family_distribution": {"constructor": 1, "discharge": 2}} +{"name": "apply_chain", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.3333333333333333, 3548], "tactic_family_distribution": {"discharge": 3}} +{"name": "omega_chain_ineq", "status": "verified", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 1.0, 1082], "tactic_family_distribution": {"arithmetic": 1}} +{"name": "omega_reorder_sum", "status": "verified", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 1.0, 1056], "tactic_family_distribution": {"arithmetic": 1}} +{"name": "omega_distrib", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1071], "tactic_family_distribution": {"arithmetic": 1}} +{"name": "omega_chain_unsat", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1141], "tactic_family_distribution": {"arithmetic": 1}} +{"name": "induct_add_zero", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1042], "tactic_family_distribution": {"normalization": 1}} +{"name": "induct_add_succ", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1076], "tactic_family_distribution": {"normalization": 1}} +{"name": "induct_mul_zero", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1076], "tactic_family_distribution": {"normalization": 1}} +{"name": "induct_factorial", "status": "verified", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 1.0, 1061], "tactic_family_distribution": {"normalization": 1}} +{"name": "intro_all", "status": "verified", "n_steps": 4, "n_states": 1, "spectral_gap": 4.0, "rank_estimate": 1, "density": 4.0, "feature_vector": [4, 1, 4.0, 4.0, 0, 1, 0.0, 0.0, 0.0, 0.8113, 0.25, 4316], "tactic_family_distribution": {"introduction": 3, "discharge": 1}} +{"name": "intro_apply", "status": "verified", "n_steps": 4, "n_states": 1, "spectral_gap": 4.0, "rank_estimate": 1, "density": 4.0, "feature_vector": [4, 1, 4.0, 4.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.25, 4532], "tactic_family_distribution": {"introduction": 2, "discharge": 2}} +{"name": "have_chain", "status": "verified", "n_steps": 3, "n_states": 1, "spectral_gap": 3.0, "rank_estimate": 1, "density": 3.0, "feature_vector": [3, 1, 3.0, 3.0, 0, 1, 0.0, 0.0, 0.0, 0.9183, 0.3333333333333333, 3427], "tactic_family_distribution": {"lemma_introduction": 2, "discharge": 1}} +{"name": "calc_chain", "status": "failed", "n_steps": 2, "n_states": 1, "spectral_gap": 2.0, "rank_estimate": 1, "density": 2.0, "feature_vector": [2, 1, 2.0, 2.0, 0, 1, 0.0, 0.0, 0.0, 1.0, 0.0, 2270], "tactic_family_distribution": {"algebraic": 1, "arithmetic": 1}} +{"name": "fail_type_mismatch", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1170], "tactic_family_distribution": {"reflexivity": 1}} +{"name": "fail_missing_lemma", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1198], "tactic_family_distribution": {"rewrite": 1}} +{"name": "fail_unsat", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1112], "tactic_family_distribution": {"arithmetic": 1}} +{"name": "fail_bad_coercion", "status": "failed", "n_steps": 1, "n_states": 1, "spectral_gap": 1.0, "rank_estimate": 1, "density": 1.0, "feature_vector": [1, 1, 1.0, 1.0, 0, 1, 0.0, 0.0, 0.0, -0.0, 0.0, 1108], "tactic_family_distribution": {"reflexivity": 1}} diff --git a/shared-data/proof_traces/canary_apply_chain.decomp.json b/shared-data/proof_traces/canary_apply_chain.decomp.json new file mode 100644 index 00000000..7e1e34f7 --- /dev/null +++ b/shared-data/proof_traces/canary_apply_chain.decomp.json @@ -0,0 +1,95 @@ +{ + "trace_summary": { + "theorem_name": "apply_chain", + "status": "verified", + "n_steps": 3, + "n_unique_goal_states": 1, + "n_flexure_joints": 3 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 3.0, + "spectral_gap": 3.0, + "laplacian_eigenvalue_max": 3.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 3.0, + "trace": 3, + "density": 3.0 + }, + "feature_vector": [ + 3, + 1, + 3.0, + 3.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.3333333333333333, + 3548 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "discharge": 3 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "apply h2", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "apply h1", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_apply_chain.trace.json b/shared-data/proof_traces/canary_apply_chain.trace.json new file mode 100644 index 00000000..a6a2eee3 --- /dev/null +++ b/shared-data/proof_traces/canary_apply_chain.trace.json @@ -0,0 +1,122 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "ea1cebff0a2f62a9dc7d1cc85661f9c790c7ae51895a98436d7811135006f54f", + "theorem_name": "apply_chain", + "status": "verified", + "tactic_count": 3, + "total_elapsed_ms": 3548, + "steps": [ + { + "step": 0, + "tactic": "apply h2", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1263, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "apply h1", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1199, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "exact hA", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1086, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 3 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "apply h2", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "apply h1", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_calc_chain.decomp.json b/shared-data/proof_traces/canary_calc_chain.decomp.json new file mode 100644 index 00000000..dd5c74ed --- /dev/null +++ b/shared-data/proof_traces/canary_calc_chain.decomp.json @@ -0,0 +1,84 @@ +{ + "trace_summary": { + "theorem_name": "calc_chain", + "status": "failed", + "n_steps": 2, + "n_unique_goal_states": 1, + "n_flexure_joints": 2 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 2.0, + "spectral_gap": 2.0, + "laplacian_eigenvalue_max": 2.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 2.0, + "trace": 2, + "density": 2.0 + }, + "feature_vector": [ + 2, + 1, + 2.0, + 2.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 1.0, + 0.0, + 2270 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "algebraic": 1, + "arithmetic": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "ring", + "tactic_family": "algebraic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_calc_chain.trace.json b/shared-data/proof_traces/canary_calc_chain.trace.json new file mode 100644 index 00000000..5b91d836 --- /dev/null +++ b/shared-data/proof_traces/canary_calc_chain.trace.json @@ -0,0 +1,87 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "ffc91916d335aac079945c103d27ef03412d0a551b8c8b7e11d5195fe925c39b", + "theorem_name": "calc_chain", + "status": "failed", + "tactic_count": 2, + "total_elapsed_ms": 2270, + "steps": [ + { + "step": 0, + "tactic": "ring", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1104, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "omega", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1166, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 2 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "ring", + "tactic_family": "algebraic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_cases_and_elim.decomp.json b/shared-data/proof_traces/canary_cases_and_elim.decomp.json new file mode 100644 index 00000000..3153b5c6 --- /dev/null +++ b/shared-data/proof_traces/canary_cases_and_elim.decomp.json @@ -0,0 +1,97 @@ +{ + "trace_summary": { + "theorem_name": "cases_and_elim", + "status": "verified", + "n_steps": 3, + "n_unique_goal_states": 1, + "n_flexure_joints": 3 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 3.0, + "spectral_gap": 3.0, + "laplacian_eigenvalue_max": 3.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 3.0, + "trace": 3, + "density": 3.0 + }, + "feature_vector": [ + 3, + 1, + 3.0, + 3.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 1.585, + 0.3333333333333333, + 3345 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "case_analysis": 1, + "discharge": 1, + "unknown": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "cases h", + "tactic_family": "case_analysis", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "apply h2", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "assumption", + "tactic_family": "unknown", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_cases_and_elim.trace.json b/shared-data/proof_traces/canary_cases_and_elim.trace.json new file mode 100644 index 00000000..353a92c3 --- /dev/null +++ b/shared-data/proof_traces/canary_cases_and_elim.trace.json @@ -0,0 +1,122 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "b9e3ed9d2456aff7773a8aa63c814a443e4fd9ace06630c76776b25ba0885d37", + "theorem_name": "cases_and_elim", + "status": "verified", + "tactic_count": 3, + "total_elapsed_ms": 3345, + "steps": [ + { + "step": 0, + "tactic": "cases h", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1072, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "apply h2", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1148, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "assumption", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1125, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 3 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "cases h", + "tactic_family": "case_analysis", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "apply h2", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "assumption", + "tactic_family": "unknown", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_cases_or_swap.decomp.json b/shared-data/proof_traces/canary_cases_or_swap.decomp.json new file mode 100644 index 00000000..eae9af43 --- /dev/null +++ b/shared-data/proof_traces/canary_cases_or_swap.decomp.json @@ -0,0 +1,121 @@ +{ + "trace_summary": { + "theorem_name": "cases_or_swap", + "status": "failed", + "n_steps": 5, + "n_unique_goal_states": 1, + "n_flexure_joints": 5 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 5.0, + "spectral_gap": 5.0, + "laplacian_eigenvalue_max": 5.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 5.0, + "trace": 5, + "density": 5.0 + }, + "feature_vector": [ + 5, + 1, + 5.0, + 5.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 1.5219, + 0.0, + 5552 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "case_analysis": 1, + "unknown": 2, + "discharge": 2 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "cases h", + "tactic_family": "case_analysis", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "\u00b7 right", + "tactic_family": "unknown", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "exact h", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 3, + "tactic": "\u00b7 left", + "tactic_family": "unknown", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 4, + "tactic": "exact h", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_cases_or_swap.trace.json b/shared-data/proof_traces/canary_cases_or_swap.trace.json new file mode 100644 index 00000000..bf02f929 --- /dev/null +++ b/shared-data/proof_traces/canary_cases_or_swap.trace.json @@ -0,0 +1,192 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "a5d1516151f774e41626c35fdc80c48b283ebce812be3114261e2a0022ee7f34", + "theorem_name": "cases_or_swap", + "status": "failed", + "tactic_count": 5, + "total_elapsed_ms": 5552, + "steps": [ + { + "step": 0, + "tactic": "cases h", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1138, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "\u00b7 right", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1140, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "exact h", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1115, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 3, + "tactic": "\u00b7 left", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1106, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 4, + "tactic": "exact h", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1053, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 5 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "cases h", + "tactic_family": "case_analysis", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "\u00b7 right", + "tactic_family": "unknown", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "exact h", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 3, + "tactic": "\u00b7 left", + "tactic_family": "unknown", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 4, + "tactic": "exact h", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_constructor_example.decomp.json b/shared-data/proof_traces/canary_constructor_example.decomp.json new file mode 100644 index 00000000..effaf60e --- /dev/null +++ b/shared-data/proof_traces/canary_constructor_example.decomp.json @@ -0,0 +1,96 @@ +{ + "trace_summary": { + "theorem_name": "constructor_example", + "status": "verified", + "n_steps": 3, + "n_unique_goal_states": 1, + "n_flexure_joints": 3 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 3.0, + "spectral_gap": 3.0, + "laplacian_eigenvalue_max": 3.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 3.0, + "trace": 3, + "density": 3.0 + }, + "feature_vector": [ + 3, + 1, + 3.0, + 3.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 0.9183, + 0.3333333333333333, + 3311 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "constructor": 1, + "discharge": 2 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "constructor", + "tactic_family": "constructor", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "\u00b7 exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "\u00b7 exact hB", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_constructor_example.trace.json b/shared-data/proof_traces/canary_constructor_example.trace.json new file mode 100644 index 00000000..b24f9522 --- /dev/null +++ b/shared-data/proof_traces/canary_constructor_example.trace.json @@ -0,0 +1,122 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "2eb590d2a9b457143e96ac5f046833f24ab5f93ff05ae6944cce0b81ddf6740e", + "theorem_name": "constructor_example", + "status": "verified", + "tactic_count": 3, + "total_elapsed_ms": 3311, + "steps": [ + { + "step": 0, + "tactic": "constructor", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1096, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "\u00b7 exact hA", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1107, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "\u00b7 exact hB", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1108, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 3 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "constructor", + "tactic_family": "constructor", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "\u00b7 exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "\u00b7 exact hB", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_bad_coercion.decomp.json b/shared-data/proof_traces/canary_fail_bad_coercion.decomp.json new file mode 100644 index 00000000..880a067e --- /dev/null +++ b/shared-data/proof_traces/canary_fail_bad_coercion.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "fail_bad_coercion", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1108 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "reflexivity": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "rfl", + "tactic_family": "reflexivity", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_bad_coercion.trace.json b/shared-data/proof_traces/canary_fail_bad_coercion.trace.json new file mode 100644 index 00000000..d28e02cb --- /dev/null +++ b/shared-data/proof_traces/canary_fail_bad_coercion.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "0361d21827da4cd215292e606e203e24b1d862d7fc08075d6cae898b04824cc7", + "theorem_name": "fail_bad_coercion", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1108, + "steps": [ + { + "step": 0, + "tactic": "rfl", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1108, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "rfl", + "tactic_family": "reflexivity", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_missing_lemma.decomp.json b/shared-data/proof_traces/canary_fail_missing_lemma.decomp.json new file mode 100644 index 00000000..04216c16 --- /dev/null +++ b/shared-data/proof_traces/canary_fail_missing_lemma.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "fail_missing_lemma", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1198 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "rewrite": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [imaginary_lemma]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_missing_lemma.trace.json b/shared-data/proof_traces/canary_fail_missing_lemma.trace.json new file mode 100644 index 00000000..a0ea491e --- /dev/null +++ b/shared-data/proof_traces/canary_fail_missing_lemma.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "695a8dc0a0b929b09b6f795eaebb82982558d7e6da2addd6d88472a26ed7bf0f", + "theorem_name": "fail_missing_lemma", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1198, + "steps": [ + { + "step": 0, + "tactic": "rw [imaginary_lemma]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1198, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [imaginary_lemma]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_type_mismatch.decomp.json b/shared-data/proof_traces/canary_fail_type_mismatch.decomp.json new file mode 100644 index 00000000..91258015 --- /dev/null +++ b/shared-data/proof_traces/canary_fail_type_mismatch.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "fail_type_mismatch", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1170 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "reflexivity": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "rfl", + "tactic_family": "reflexivity", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_type_mismatch.trace.json b/shared-data/proof_traces/canary_fail_type_mismatch.trace.json new file mode 100644 index 00000000..7a193471 --- /dev/null +++ b/shared-data/proof_traces/canary_fail_type_mismatch.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "0f481ab618a4e39cd28480436a43bf0dcf541fa62801d3e58588d66f355f54c6", + "theorem_name": "fail_type_mismatch", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1170, + "steps": [ + { + "step": 0, + "tactic": "rfl", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1170, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "rfl", + "tactic_family": "reflexivity", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_unsat.decomp.json b/shared-data/proof_traces/canary_fail_unsat.decomp.json new file mode 100644 index 00000000..5e77061c --- /dev/null +++ b/shared-data/proof_traces/canary_fail_unsat.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "fail_unsat", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1112 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "arithmetic": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_fail_unsat.trace.json b/shared-data/proof_traces/canary_fail_unsat.trace.json new file mode 100644 index 00000000..2cb66203 --- /dev/null +++ b/shared-data/proof_traces/canary_fail_unsat.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "ea07e0d3bd2e3d976b55b4cf94201957550a8733b53e3f84725d2d67b46d4cfc", + "theorem_name": "fail_unsat", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1112, + "steps": [ + { + "step": 0, + "tactic": "omega", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1112, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_have_chain.decomp.json b/shared-data/proof_traces/canary_have_chain.decomp.json new file mode 100644 index 00000000..5e4c2320 --- /dev/null +++ b/shared-data/proof_traces/canary_have_chain.decomp.json @@ -0,0 +1,96 @@ +{ + "trace_summary": { + "theorem_name": "have_chain", + "status": "verified", + "n_steps": 3, + "n_unique_goal_states": 1, + "n_flexure_joints": 3 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 3.0, + "spectral_gap": 3.0, + "laplacian_eigenvalue_max": 3.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 3.0, + "trace": 3, + "density": 3.0 + }, + "feature_vector": [ + 3, + 1, + 3.0, + 3.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 0.9183, + 0.3333333333333333, + 3427 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "lemma_introduction": 2, + "discharge": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "have hB : B := hAB hA", + "tactic_family": "lemma_introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "have hC : C := hBC hB", + "tactic_family": "lemma_introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "exact hC", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_have_chain.trace.json b/shared-data/proof_traces/canary_have_chain.trace.json new file mode 100644 index 00000000..22b6c5d8 --- /dev/null +++ b/shared-data/proof_traces/canary_have_chain.trace.json @@ -0,0 +1,122 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "555b7633b2fe1f0fd58e666ef2d03da6f4f7ac5b6be0eefbe32dcf7af342eae3", + "theorem_name": "have_chain", + "status": "verified", + "tactic_count": 3, + "total_elapsed_ms": 3427, + "steps": [ + { + "step": 0, + "tactic": "have hB : B := hAB hA", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1113, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "have hC : C := hBC hB", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1214, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "exact hC", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1100, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 3 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "have hB : B := hAB hA", + "tactic_family": "lemma_introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "have hC : C := hBC hB", + "tactic_family": "lemma_introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "exact hC", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_add_succ.decomp.json b/shared-data/proof_traces/canary_induct_add_succ.decomp.json new file mode 100644 index 00000000..46fa8ae0 --- /dev/null +++ b/shared-data/proof_traces/canary_induct_add_succ.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "induct_add_succ", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1076 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "normalization": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ k ih => simp [add_succ, ih]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_add_succ.trace.json b/shared-data/proof_traces/canary_induct_add_succ.trace.json new file mode 100644 index 00000000..73a13eec --- /dev/null +++ b/shared-data/proof_traces/canary_induct_add_succ.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "198197fa574402142bbac958dc8944df994bd2c010f5b163adc6567ba7e849df", + "theorem_name": "induct_add_succ", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1076, + "steps": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ k ih => simp [add_succ, ih]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1076, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ k ih => simp [add_succ, ih]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_add_zero.decomp.json b/shared-data/proof_traces/canary_induct_add_zero.decomp.json new file mode 100644 index 00000000..5d017120 --- /dev/null +++ b/shared-data/proof_traces/canary_induct_add_zero.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "induct_add_zero", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1042 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "normalization": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ n ih => simp [add_succ, ih]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_add_zero.trace.json b/shared-data/proof_traces/canary_induct_add_zero.trace.json new file mode 100644 index 00000000..0b80cf57 --- /dev/null +++ b/shared-data/proof_traces/canary_induct_add_zero.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "58308f000c8cf3b7a19c12f46a40a8b8822f5f84a5860e100bf5d93bac55ad16", + "theorem_name": "induct_add_zero", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1042, + "steps": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ n ih => simp [add_succ, ih]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1042, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ n ih => simp [add_succ, ih]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_factorial.decomp.json b/shared-data/proof_traces/canary_induct_factorial.decomp.json new file mode 100644 index 00000000..4d5a43d2 --- /dev/null +++ b/shared-data/proof_traces/canary_induct_factorial.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "induct_factorial", + "status": "verified", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 1.0, + 1061 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "normalization": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "simp [fac]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_factorial.trace.json b/shared-data/proof_traces/canary_induct_factorial.trace.json new file mode 100644 index 00000000..1e2b6f44 --- /dev/null +++ b/shared-data/proof_traces/canary_induct_factorial.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "16f00e21118bd73911fcb21b83283770989bdafebd84f2ab69243ffefb66fe66", + "theorem_name": "induct_factorial", + "status": "verified", + "tactic_count": 1, + "total_elapsed_ms": 1061, + "steps": [ + { + "step": 0, + "tactic": "simp [fac]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1061, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "simp [fac]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_mul_zero.decomp.json b/shared-data/proof_traces/canary_induct_mul_zero.decomp.json new file mode 100644 index 00000000..2935679a --- /dev/null +++ b/shared-data/proof_traces/canary_induct_mul_zero.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "induct_mul_zero", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1076 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "normalization": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ k ih => simp [mul_add, add_comm, ih]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_induct_mul_zero.trace.json b/shared-data/proof_traces/canary_induct_mul_zero.trace.json new file mode 100644 index 00000000..5e8dbd51 --- /dev/null +++ b/shared-data/proof_traces/canary_induct_mul_zero.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "aaf9644978fbd40566dc96f63d1cf70c7086d5eaedaeb70fdb348ee3228a430e", + "theorem_name": "induct_mul_zero", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1076, + "steps": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ k ih => simp [mul_add, add_comm, ih]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1076, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "induction n with | zero => simp | succ k ih => simp [mul_add, add_comm, ih]", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_intro_all.decomp.json b/shared-data/proof_traces/canary_intro_all.decomp.json new file mode 100644 index 00000000..15ab6612 --- /dev/null +++ b/shared-data/proof_traces/canary_intro_all.decomp.json @@ -0,0 +1,108 @@ +{ + "trace_summary": { + "theorem_name": "intro_all", + "status": "verified", + "n_steps": 4, + "n_unique_goal_states": 1, + "n_flexure_joints": 4 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 4.0, + "spectral_gap": 4.0, + "laplacian_eigenvalue_max": 4.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 4.0, + "trace": 4, + "density": 4.0 + }, + "feature_vector": [ + 4, + 1, + 4.0, + 4.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 0.8113, + 0.25, + 4316 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "introduction": 3, + "discharge": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "intro hA", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "intro hB", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "intro hC", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 3, + "tactic": "exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_intro_all.trace.json b/shared-data/proof_traces/canary_intro_all.trace.json new file mode 100644 index 00000000..eefd9c33 --- /dev/null +++ b/shared-data/proof_traces/canary_intro_all.trace.json @@ -0,0 +1,157 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "6cd826b82467f96a11c9c1730a2b5b7c71d8caa4b34805110a2b51c99c00651c", + "theorem_name": "intro_all", + "status": "verified", + "tactic_count": 4, + "total_elapsed_ms": 4316, + "steps": [ + { + "step": 0, + "tactic": "intro hA", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1004, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "intro hB", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1122, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "intro hC", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1029, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 3, + "tactic": "exact hA", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1161, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 4 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "intro hA", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "intro hB", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "intro hC", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 3, + "tactic": "exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_intro_apply.decomp.json b/shared-data/proof_traces/canary_intro_apply.decomp.json new file mode 100644 index 00000000..65a1730a --- /dev/null +++ b/shared-data/proof_traces/canary_intro_apply.decomp.json @@ -0,0 +1,108 @@ +{ + "trace_summary": { + "theorem_name": "intro_apply", + "status": "verified", + "n_steps": 4, + "n_unique_goal_states": 1, + "n_flexure_joints": 4 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 4.0, + "spectral_gap": 4.0, + "laplacian_eigenvalue_max": 4.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 4.0, + "trace": 4, + "density": 4.0 + }, + "feature_vector": [ + 4, + 1, + 4.0, + 4.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 1.0, + 0.25, + 4532 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "introduction": 2, + "discharge": 2 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "intro h", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "intro hA", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "apply h", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 3, + "tactic": "exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_intro_apply.trace.json b/shared-data/proof_traces/canary_intro_apply.trace.json new file mode 100644 index 00000000..1fc6a714 --- /dev/null +++ b/shared-data/proof_traces/canary_intro_apply.trace.json @@ -0,0 +1,157 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "da21735150a22821368a9558b2a064c574b7f822a59c9112146f9728140733f1", + "theorem_name": "intro_apply", + "status": "verified", + "tactic_count": 4, + "total_elapsed_ms": 4532, + "steps": [ + { + "step": 0, + "tactic": "intro h", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1149, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "intro hA", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1065, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "apply h", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1229, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 3, + "tactic": "exact hA", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1089, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 4 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "intro h", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "intro hA", + "tactic_family": "introduction", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "apply h", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 3, + "tactic": "exact hA", + "tactic_family": "discharge", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_chain_ineq.decomp.json b/shared-data/proof_traces/canary_omega_chain_ineq.decomp.json new file mode 100644 index 00000000..8a565186 --- /dev/null +++ b/shared-data/proof_traces/canary_omega_chain_ineq.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "omega_chain_ineq", + "status": "verified", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 1.0, + 1082 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "arithmetic": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_chain_ineq.trace.json b/shared-data/proof_traces/canary_omega_chain_ineq.trace.json new file mode 100644 index 00000000..b534a81e --- /dev/null +++ b/shared-data/proof_traces/canary_omega_chain_ineq.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "28b82a6c260edf2bb49330f7b550dad25dc4f52e9b05458ea3e359db543f1636", + "theorem_name": "omega_chain_ineq", + "status": "verified", + "tactic_count": 1, + "total_elapsed_ms": 1082, + "steps": [ + { + "step": 0, + "tactic": "omega", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1082, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_chain_unsat.decomp.json b/shared-data/proof_traces/canary_omega_chain_unsat.decomp.json new file mode 100644 index 00000000..ca4ea51e --- /dev/null +++ b/shared-data/proof_traces/canary_omega_chain_unsat.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "omega_chain_unsat", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1141 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "arithmetic": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_chain_unsat.trace.json b/shared-data/proof_traces/canary_omega_chain_unsat.trace.json new file mode 100644 index 00000000..b590a438 --- /dev/null +++ b/shared-data/proof_traces/canary_omega_chain_unsat.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "5230b5bd4815dd0b78eb21b270ff11d3ea24bfeeb0c6c1437837a5ce968259cf", + "theorem_name": "omega_chain_unsat", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1141, + "steps": [ + { + "step": 0, + "tactic": "omega", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1141, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_distrib.decomp.json b/shared-data/proof_traces/canary_omega_distrib.decomp.json new file mode 100644 index 00000000..c740ea9c --- /dev/null +++ b/shared-data/proof_traces/canary_omega_distrib.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "omega_distrib", + "status": "failed", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.0, + 1071 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "arithmetic": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_distrib.trace.json b/shared-data/proof_traces/canary_omega_distrib.trace.json new file mode 100644 index 00000000..318d8987 --- /dev/null +++ b/shared-data/proof_traces/canary_omega_distrib.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "caa088677ed4572fe89029b07d4184a54d71729acd710ec218f8ff1083cd390d", + "theorem_name": "omega_distrib", + "status": "failed", + "tactic_count": 1, + "total_elapsed_ms": 1071, + "steps": [ + { + "step": 0, + "tactic": "omega", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1071, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_reorder_sum.decomp.json b/shared-data/proof_traces/canary_omega_reorder_sum.decomp.json new file mode 100644 index 00000000..c7e66133 --- /dev/null +++ b/shared-data/proof_traces/canary_omega_reorder_sum.decomp.json @@ -0,0 +1,71 @@ +{ + "trace_summary": { + "theorem_name": "omega_reorder_sum", + "status": "verified", + "n_steps": 1, + "n_unique_goal_states": 1, + "n_flexure_joints": 1 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 1.0, + "spectral_gap": 1.0, + "laplacian_eigenvalue_max": 1.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 1.0, + "trace": 1, + "density": 1.0 + }, + "feature_vector": [ + 1, + 1, + 1.0, + 1.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 1.0, + 1056 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "arithmetic": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_omega_reorder_sum.trace.json b/shared-data/proof_traces/canary_omega_reorder_sum.trace.json new file mode 100644 index 00000000..3a329fac --- /dev/null +++ b/shared-data/proof_traces/canary_omega_reorder_sum.trace.json @@ -0,0 +1,52 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "34eb1411ee65a817e73e1a0fd58cabc6a85f959f966b031b0508cafe7779e660", + "theorem_name": "omega_reorder_sum", + "status": "verified", + "tactic_count": 1, + "total_elapsed_ms": 1056, + "steps": [ + { + "step": 0, + "tactic": "omega", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1056, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 1 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_chain_3step.decomp.json b/shared-data/proof_traces/canary_rw_chain_3step.decomp.json new file mode 100644 index 00000000..ea81f29f --- /dev/null +++ b/shared-data/proof_traces/canary_rw_chain_3step.decomp.json @@ -0,0 +1,95 @@ +{ + "trace_summary": { + "theorem_name": "rw_chain_3step", + "status": "verified", + "n_steps": 3, + "n_unique_goal_states": 1, + "n_flexure_joints": 3 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 3.0, + "spectral_gap": 3.0, + "laplacian_eigenvalue_max": 3.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 3.0, + "trace": 3, + "density": 3.0 + }, + "feature_vector": [ + 3, + 1, + 3.0, + 3.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.3333333333333333, + 3279 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "rewrite": 3 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h1]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "rw [h2]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "rw [h3]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_chain_3step.trace.json b/shared-data/proof_traces/canary_rw_chain_3step.trace.json new file mode 100644 index 00000000..d4159632 --- /dev/null +++ b/shared-data/proof_traces/canary_rw_chain_3step.trace.json @@ -0,0 +1,122 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "1ff8b91260cbf4e62acd45fa1114b20dc0dd3e94bed90241654673aed39d1246", + "theorem_name": "rw_chain_3step", + "status": "verified", + "tactic_count": 3, + "total_elapsed_ms": 3279, + "steps": [ + { + "step": 0, + "tactic": "rw [h1]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1066, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "rw [h2]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1094, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 2, + "tactic": "rw [h3]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1119, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 3 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h1]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "rw [h2]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 2, + "tactic": "rw [h3]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_chain_eq.decomp.json b/shared-data/proof_traces/canary_rw_chain_eq.decomp.json new file mode 100644 index 00000000..d016d1c0 --- /dev/null +++ b/shared-data/proof_traces/canary_rw_chain_eq.decomp.json @@ -0,0 +1,83 @@ +{ + "trace_summary": { + "theorem_name": "rw_chain_eq", + "status": "verified", + "n_steps": 2, + "n_unique_goal_states": 1, + "n_flexure_joints": 2 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 2.0, + "spectral_gap": 2.0, + "laplacian_eigenvalue_max": 2.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 2.0, + "trace": 2, + "density": 2.0 + }, + "feature_vector": [ + 2, + 1, + 2.0, + 2.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + -0.0, + 0.5, + 2524 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "rewrite": 2 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h1]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "rw [h2]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_chain_eq.trace.json b/shared-data/proof_traces/canary_rw_chain_eq.trace.json new file mode 100644 index 00000000..d03f74fd --- /dev/null +++ b/shared-data/proof_traces/canary_rw_chain_eq.trace.json @@ -0,0 +1,87 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "fb9ee92a7900d8987e1e38d4dfadb08e55ab3c4cc759243fe3f83aa945e87789", + "theorem_name": "rw_chain_eq", + "status": "verified", + "tactic_count": 2, + "total_elapsed_ms": 2524, + "steps": [ + { + "step": 0, + "tactic": "rw [h1]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1243, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "rw [h2]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1281, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 2 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h1]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "rw [h2]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_chain_mixed.decomp.json b/shared-data/proof_traces/canary_rw_chain_mixed.decomp.json new file mode 100644 index 00000000..a59a8902 --- /dev/null +++ b/shared-data/proof_traces/canary_rw_chain_mixed.decomp.json @@ -0,0 +1,84 @@ +{ + "trace_summary": { + "theorem_name": "rw_chain_mixed", + "status": "verified", + "n_steps": 2, + "n_unique_goal_states": 1, + "n_flexure_joints": 2 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 2.0, + "spectral_gap": 2.0, + "laplacian_eigenvalue_max": 2.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 2.0, + "trace": 2, + "density": 2.0 + }, + "feature_vector": [ + 2, + 1, + 2.0, + 2.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 1.0, + 0.5, + 2194 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "rewrite": 1, + "normalization": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "simp", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_chain_mixed.trace.json b/shared-data/proof_traces/canary_rw_chain_mixed.trace.json new file mode 100644 index 00000000..23920784 --- /dev/null +++ b/shared-data/proof_traces/canary_rw_chain_mixed.trace.json @@ -0,0 +1,87 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "862ef6b1cf0e2eda6faf9968f33fc8e4147b48e614911bc996d1fb1258d23b39", + "theorem_name": "rw_chain_mixed", + "status": "verified", + "tactic_count": 2, + "total_elapsed_ms": 2194, + "steps": [ + { + "step": 0, + "tactic": "rw [h]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1105, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "simp", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1089, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 2 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + }, + { + "step": 1, + "tactic": "simp", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_then_omega.decomp.json b/shared-data/proof_traces/canary_rw_then_omega.decomp.json new file mode 100644 index 00000000..0e99649a --- /dev/null +++ b/shared-data/proof_traces/canary_rw_then_omega.decomp.json @@ -0,0 +1,84 @@ +{ + "trace_summary": { + "theorem_name": "rw_then_omega", + "status": "failed", + "n_steps": 2, + "n_unique_goal_states": 1, + "n_flexure_joints": 2 + }, + "spectral": { + "n_states": 1, + "eigenvalue_max": 2.0, + "spectral_gap": 2.0, + "laplacian_eigenvalue_max": 2.0, + "rank_estimate": 1, + "zero_rows": 0, + "frobenius_norm": 2.0, + "trace": 2, + "density": 2.0 + }, + "feature_vector": [ + 2, + 1, + 2.0, + 2.0, + 0, + 1, + 0.0, + 0.0, + 0.0, + 1.0, + 0.5, + 2137 + ], + "feature_names": [ + "n_steps", + "n_unique_goal_states", + "transition_density", + "spectral_gap", + "laplacian_zero_count", + "rank_estimate", + "avg_delta_goal_count", + "avg_delta_hypothesis", + "avg_delta_symbol", + "tactic_family_entropy", + "verified_ratio", + "total_elapsed" + ], + "tactic_family_distribution": { + "rewrite": 1, + "arithmetic": 1 + }, + "delta_stats": { + "avg_goal_delta": 0.0, + "avg_hypothesis_delta": 0.0, + "avg_symbol_delta": 0.0, + "max_delta_score": 0 + }, + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + }, + { + "step": 1, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_rw_then_omega.trace.json b/shared-data/proof_traces/canary_rw_then_omega.trace.json new file mode 100644 index 00000000..bf81906d --- /dev/null +++ b/shared-data/proof_traces/canary_rw_then_omega.trace.json @@ -0,0 +1,87 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "d1beb5b4ad2dc2941198c6d14e781358d6d6161d7f4f9e8c4a94fc934ca5d656", + "theorem_name": "rw_then_omega", + "status": "failed", + "tactic_count": 2, + "total_elapsed_ms": 2137, + "steps": [ + { + "step": 0, + "tactic": "rw [h]", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1003, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "omega", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1134, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 2 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "rw [h]", + "tactic_family": "rewrite", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + }, + { + "step": 1, + "tactic": "omega", + "tactic_family": "arithmetic", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file diff --git a/shared-data/proof_traces/canary_simp_chain_simple.trace.json b/shared-data/proof_traces/canary_simp_chain_simple.trace.json new file mode 100644 index 00000000..a5c5e039 --- /dev/null +++ b/shared-data/proof_traces/canary_simp_chain_simple.trace.json @@ -0,0 +1,87 @@ +{ + "trace_version": "proof-trace-v1", + "receipt_hash": "974cd133f3c42af1013f13bfb435cc55fb31c57fb7674ac6948542aa2ae8aeaf", + "theorem_name": "simp_chain_simple", + "status": "failed", + "tactic_count": 2, + "total_elapsed_ms": 2227, + "steps": [ + { + "step": 0, + "tactic": "simp", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1163, + "result": "success", + "stdout_preview": "", + "stderr_preview": "" + }, + { + "step": 1, + "tactic": "rfl", + "before_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "after_goal_hash": "01ba4719c80b6fe911b091a7c05124b64eeece964e09c058ef8f9805daca546b", + "before_goal_text": "\n", + "after_goal_text": "\n", + "goal_count_before": 1, + "goal_count_after": 1, + "hypothesis_count_before": 0, + "hypothesis_count_after": 0, + "operator_count_before": 0, + "operator_count_after": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "elapsed_ms": 1064, + "result": "failure", + "stdout_preview": "", + "stderr_preview": "" + } + ], + "goal_transition_matrix": [ + [ + 2 + ] + ], + "flexure_joints": [ + { + "step": 0, + "tactic": "simp", + "tactic_family": "normalization", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "success" + }, + { + "step": 1, + "tactic": "rfl", + "tactic_family": "reflexivity", + "delta_score": 0, + "delta": { + "symbol_delta": 0, + "hypothesis_delta": 0, + "goal_count_delta": 0 + }, + "result": "failure" + } + ] +} \ No newline at end of file