mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
67e77d8f24
Moves all classification authority from Python into Lean: - Adds `0-Core-Formalism/lean/Semantics/PistClassifyTrace.lean` executable. Reads a raw trace JSON and emits spectral radius, RRC shape, and tactic family using `Semantics.PIST.Spectral` and `Semantics.PIST.Classify`. - Registers `pist-classify-trace` in `lakefile.toml`. - Fixes `Semantics.PIST.Spectral` power iteration to handle directed transition matrices: - `symmetrize` now preserves half-integer weights as Q16_16 raw values. - `matVecMul` uses saturated Q16_16 arithmetic to prevent overflow. - Rewrites `4-Infrastructure/shim/pist_trace_classify_offline.py` as a pure I/O wrapper: reads JSON, calls the Lean classifier, optionally calls `rrc-watchdog`, and emits the combined JSON. Removes Python-side spectral computation, shape thresholds, tactic heuristic, and KNN. - Updates `AGENTS.md` and `4-Infrastructure/AGENTS.md` with the new build baseline and shim contract. Verification: - `lake build` → 8604 jobs, 0 errors - Canary trace outputs match previous Python outputs to within Q16_16 rounding (e.g., apply_chain λ_q16 = 59044 vs 59045). - `python3 -m py_compile` on the rewritten shim passes.
89 lines
3.5 KiB
Text
89 lines
3.5 KiB
Text
-- PistClassifyTrace.lean
|
|
-- SilverSight-ruleset-first proof-trace classifier executable.
|
|
--
|
|
-- Authority: this executable is the sole classifier. It reads a raw trace
|
|
-- JSON, computes spectral features with Q16_16 arithmetic, and emits the
|
|
-- predicted RRC shape and tactic family. Python shims may only format I/O
|
|
-- and call this executable.
|
|
|
|
import Semantics.PIST.Spectral
|
|
import Semantics.PIST.Classify
|
|
import Lean.Data.Json
|
|
|
|
open Lean
|
|
open Semantics.PIST
|
|
|
|
namespace PistClassifyTrace
|
|
|
|
/-- Raw input expected from the Python shim. -/
|
|
structure Input where
|
|
name : String
|
|
transition_matrix : Array (Array Int)
|
|
deriving FromJson
|
|
|
|
/-- Shape string used when no higher-energy regime is detected.
|
|
Matches RRC.Emit.shapeStr for HoldForUnlawfulOrUnderspecifiedShape. -/
|
|
def holdShape : String := "HoldForUnlawfulOrUnderspecifiedShape"
|
|
|
|
/-- Map the library tactic family to the Python-facing string. -/
|
|
def tacticFamilyString : Spectral.TacticFamily → String
|
|
| .rewrite => "rewrite"
|
|
| .normalization => "normalization"
|
|
| .arithmetic => "arithmetic"
|
|
| .induction => "induction"
|
|
| .algebraic => "algebraic"
|
|
| .case_analysis => "case_analysis"
|
|
| .discharge => "discharge"
|
|
| .reflexivity => "reflexivity"
|
|
| .unknown => "unknown"
|
|
|
|
/-- Build a JSON object from a Q16_16 spectral profile. -/
|
|
def spectralProfileJson (p : Spectral.SpectralProfile) : Json :=
|
|
Json.mkObj [
|
|
("matrix_size", toJson p.matrix_size.toInt),
|
|
("rank", toJson p.rank.toInt),
|
|
("spectral_gap", toJson p.spectral_gap.toInt),
|
|
("density", toJson p.density.toInt),
|
|
("trace_val", toJson p.trace_val.toInt),
|
|
("frobenius_norm", toJson p.frobenius_norm.toInt),
|
|
("laplacian_zero_count", toJson p.laplacian_zero_count.toInt),
|
|
("adjacency_eigenvalue_max", toJson p.adjacency_eigenvalue_max.toInt),
|
|
("laplacian_eigenvalue_max", toJson p.laplacian_eigenvalue_max.toInt),
|
|
("singular_value_max", toJson p.singular_value_max.toInt)
|
|
]
|
|
|
|
/-- Build the classifier output JSON. -/
|
|
def outputJson (name : String) (profile : Spectral.SpectralProfile)
|
|
(shape : String) (tactic : String) : Json :=
|
|
Json.mkObj [
|
|
("theorem_name", toJson name),
|
|
("spectral_radius", toJson profile.adjacency_eigenvalue_max.toInt),
|
|
("spectral_radius_q16", toJson profile.adjacency_eigenvalue_max.toInt),
|
|
("predicted_rrc_shape", toJson shape),
|
|
("tactic_family", toJson tactic),
|
|
("spectral_profile", spectralProfileJson profile)
|
|
]
|
|
|
|
end PistClassifyTrace
|
|
|
|
def main (args : List String) : IO Unit := do
|
|
let inputStr ←
|
|
match args with
|
|
| [] =>
|
|
let stdin ← IO.getStdin
|
|
stdin.readToEnd
|
|
| [path] => IO.FS.readFile path
|
|
| _ => throw (IO.userError "Usage: pist-classify-trace [trace.json]")
|
|
|
|
match Json.parse inputStr with
|
|
| .error e =>
|
|
IO.println (Json.compress (Json.mkObj [("error", toJson s!"JSON parse error: {e}")]))
|
|
| .ok j =>
|
|
match (fromJson? j : Except String PistClassifyTrace.Input) with
|
|
| .error e =>
|
|
IO.println (Json.compress (Json.mkObj [("error", toJson e)]))
|
|
| .ok input =>
|
|
let profile := Spectral.computeSpectral input.transition_matrix
|
|
let shape := (Classify.classifyExact input.transition_matrix).getD PistClassifyTrace.holdShape
|
|
let tactic := PistClassifyTrace.tacticFamilyString (Spectral.classifyTacticFromName input.name)
|
|
IO.println (Json.compress (PistClassifyTrace.outputJson input.name profile shape tactic))
|