From 5290413080574b3480cefd822666cb8fba84af0b Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 21:39:46 -0500 Subject: [PATCH] fix(avm-isa): stabilize AVMIsa + PIST.Trace build; canary #eval fires clean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit AVMIsa fixes (all pre-existing errors from the upstream merge): - Types.lean: add Repr to AvmTy - Value.lean: replace `deriving Inhabited` with explicit instance (AnyVal is a dependent structure; auto-derive can't pick a default ty+val pair); add Repr instance that delegates to AvmVal.repr - Instr.lean: add Repr to Prim and Instr - State.lean: fix `List.set ⟨i, h⟩` → `List.set i` (List.set takes Nat, not Fin); drop now-dead `h` binding; add Repr to State - Step.lean: rewrite evalPrim branches to pattern-match directly on AnyVal `⟨ty, val⟩` pairs instead of `if v.ty = T` + separate val match (Lean can't unify `AvmVal v.ty` with `AvmVal T` from a propositional if-guard); replace `List.get? pc` (removed in Lean 4.30) with `list[pc]?` subscript; rename Q0_16.addSat/subSat → Q0_16.add/sub (no sat variants exist); add Repr to StepError and Outcome PIST.Trace fixes: - Drop invalid `set_option pp.pretty true` - MVarId.toNat → MVarId.name.toString - List.size → List.length (then .toArray for Json.arr) - Json.num takes JsonNumber {mantissa : Int, exponent : Int}; cast Nat → Int - goals.mapM goalToJson: lift MetaM → TacticM via liftMetaM Canary result: `#eval run 8 canaryNot canaryState` → Outcome.ok { pc := 2, stack := [AvmVal.b true], halted := true } Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> --- .../Semantics/Semantics/AVMIsa/Instr.lean | 4 +- .../Semantics/Semantics/AVMIsa/State.lean | 6 +- .../lean/Semantics/Semantics/AVMIsa/Step.lean | 71 +++++++++---------- .../Semantics/Semantics/AVMIsa/Types.lean | 2 +- .../Semantics/Semantics/AVMIsa/Value.lean | 7 +- 2-Search-Space/PIST/Trace.lean | 24 +++---- 6 files changed, 56 insertions(+), 58 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean index 21271eab..a73b3616 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean @@ -18,7 +18,7 @@ inductive Prim : Type where | and | or | not - deriving DecidableEq, BEq, Inhabited + deriving DecidableEq, BEq, Inhabited, Repr /-- Core instruction set. @@ -37,6 +37,6 @@ inductive Instr : Type where | jumpIf : Nat → Instr | prim : Prim → Instr | halt : Instr - deriving Inhabited + deriving Inhabited, Repr end Semantics.AVMIsa diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean index 42e73316..1c2dd72f 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean @@ -15,7 +15,7 @@ structure State where locals : List (Option AnyVal) halted : Bool -deriving Inhabited +deriving Inhabited, Repr /-- Safe locals lookup (returns `none` when out of bounds). -/ def getLocal? (s : State) (i : Nat) : Option AnyVal := @@ -23,8 +23,8 @@ def getLocal? (s : State) (i : Nat) : Option AnyVal := /-- Safe locals set (no-op when out of bounds). -/ def setLocal (s : State) (i : Nat) (v : AnyVal) : State := - if h : i < s.locals.length then - { s with locals := s.locals.set ⟨i, h⟩ (some v) } + if i < s.locals.length then + { s with locals := s.locals.set i (some v) } else s diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean index 5e390abc..8dc5ebc4 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean @@ -10,7 +10,7 @@ inductive StepError : Type where | typeMismatch | invalidJump | missingLocal - deriving Inhabited, DecidableEq, BEq + deriving Inhabited, DecidableEq, BEq, Repr /-- Outcome type for AVM execution. @@ -19,7 +19,7 @@ We avoid Float and avoid exceptions. Backends should mirror this boundary. inductive Outcome (α : Type) : Type where | ok : α → Outcome α | err : StepError → Outcome α - deriving Inhabited + deriving Inhabited, Repr /-- Pop one element from stack. -/ def pop1 (s : State) : Outcome (AnyVal × State) := @@ -42,10 +42,9 @@ def evalPrim (p : Prim) (s : State) : Outcome State := match pop1 s with | Outcome.err e => Outcome.err e | Outcome.ok (v, s1) => - match v.ty with - | AvmTy.bool => - let b := match v.val with | AvmVal.b x => x - Outcome.ok (push1 s1 ⟨AvmTy.bool, AvmVal.b (!b)⟩) + match v with + | ⟨AvmTy.bool, AvmVal.b x⟩ => + Outcome.ok (push1 s1 ⟨AvmTy.bool, AvmVal.b (!x)⟩) | _ => Outcome.err StepError.typeMismatch | Prim.and => match pop1 s with @@ -54,12 +53,10 @@ def evalPrim (p : Prim) (s : State) : Outcome State := match pop1 s1 with | Outcome.err e => Outcome.err e | Outcome.ok (v2, s2) => - if v1.ty = AvmTy.bool ∧ v2.ty = AvmTy.bool then - let b1 := match v1.val with | AvmVal.b x => x - let b2 := match v2.val with | AvmVal.b x => x - Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 && b1)⟩) - else - Outcome.err StepError.typeMismatch + match v1, v2 with + | ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ => + Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 && b1)⟩) + | _, _ => Outcome.err StepError.typeMismatch | Prim.or => match pop1 s with | Outcome.err e => Outcome.err e @@ -67,12 +64,10 @@ def evalPrim (p : Prim) (s : State) : Outcome State := match pop1 s1 with | Outcome.err e => Outcome.err e | Outcome.ok (v2, s2) => - if v1.ty = AvmTy.bool ∧ v2.ty = AvmTy.bool then - let b1 := match v1.val with | AvmVal.b x => x - let b2 := match v2.val with | AvmVal.b x => x - Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 || b1)⟩) - else - Outcome.err StepError.typeMismatch + match v1, v2 with + | ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ => + Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 || b1)⟩) + | _, _ => Outcome.err StepError.typeMismatch | Prim.addSatQ0 => match pop1 s with | Outcome.err e => Outcome.err e @@ -80,12 +75,10 @@ def evalPrim (p : Prim) (s : State) : Outcome State := match pop1 s1 with | Outcome.err e => Outcome.err e | Outcome.ok (v2, s2) => - if v1.ty = AvmTy.q0_16 ∧ v2.ty = AvmTy.q0_16 then - let x := match v1.val with | AvmVal.q0 q => q - let y := match v2.val with | AvmVal.q0 q => q - Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.addSat y x)⟩) - else - Outcome.err StepError.typeMismatch + match v1, v2 with + | ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ => + Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.add y x)⟩) + | _, _ => Outcome.err StepError.typeMismatch | Prim.subSatQ0 => match pop1 s with | Outcome.err e => Outcome.err e @@ -93,12 +86,10 @@ def evalPrim (p : Prim) (s : State) : Outcome State := match pop1 s1 with | Outcome.err e => Outcome.err e | Outcome.ok (v2, s2) => - if v1.ty = AvmTy.q0_16 ∧ v2.ty = AvmTy.q0_16 then - let x := match v1.val with | AvmVal.q0 q => q - let y := match v2.val with | AvmVal.q0 q => q - Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.subSat y x)⟩) - else - Outcome.err StepError.typeMismatch + match v1, v2 with + | ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ => + Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.sub y x)⟩) + | _, _ => Outcome.err StepError.typeMismatch | _ => -- Remaining primitives are not yet implemented in v1. Outcome.err StepError.typeMismatch @@ -111,7 +102,7 @@ def step (program : List Instr) (s : State) : Outcome State := if s.halted then Outcome.ok s else - match program.get? s.pc with + match program[s.pc]? with | none => Outcome.err StepError.invalidJump | some instr => match instr with @@ -146,14 +137,16 @@ def step (program : List Instr) (s : State) : Outcome State := match pop1 s with | Outcome.err e => Outcome.err e | Outcome.ok (v, s1) => - if v.ty = AvmTy.bool then - let b := match v.val with | AvmVal.b x => x - if b then - if target < program.length then Outcome.ok { s1 with pc := target } else Outcome.err StepError.invalidJump - else - Outcome.ok { s1 with pc := s.pc + 1 } - else - Outcome.err StepError.typeMismatch + match v with + | ⟨AvmTy.bool, AvmVal.b b⟩ => + if b then + if target < program.length then + Outcome.ok { s1 with pc := target } + else + Outcome.err StepError.invalidJump + else + Outcome.ok { s1 with pc := s.pc + 1 } + | _ => Outcome.err StepError.typeMismatch | Instr.prim p => match evalPrim p s with | Outcome.err e => Outcome.err e diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean index 24a869cd..1acf9b19 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean @@ -10,6 +10,6 @@ inductive AvmTy : Type where | q0_16 : AvmTy | q16_16 : AvmTy | bool : AvmTy - deriving DecidableEq, BEq, Inhabited + deriving DecidableEq, BEq, Inhabited, Repr end Semantics.AVMIsa diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean index a6e88887..526ea6ba 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean @@ -11,6 +11,7 @@ inductive AvmVal : AvmTy → Type where | q0 : Semantics.Q0_16 → AvmVal AvmTy.q0_16 | q16 : Semantics.Q16_16 → AvmVal AvmTy.q16_16 | b : Bool → AvmVal AvmTy.bool + deriving Repr /-- Existential wrapper for storing values in an untyped container. @@ -24,6 +25,10 @@ structure AnyVal where ty : AvmTy val : AvmVal ty -deriving Inhabited +instance : Inhabited AnyVal where + default := { ty := AvmTy.bool, val := AvmVal.b false } + +instance : Repr AnyVal where + reprPrec v _ := repr v.val end Semantics.AVMIsa diff --git a/2-Search-Space/PIST/Trace.lean b/2-Search-Space/PIST/Trace.lean index b184a4f2..465de671 100644 --- a/2-Search-Space/PIST/Trace.lean +++ b/2-Search-Space/PIST/Trace.lean @@ -2,8 +2,6 @@ import Lean open Lean Elab Tactic Meta -set_option pp.pretty true - /-! # PIST Trace — goal-state snapshotter for Tier 2 flexure recording. @@ -24,6 +22,9 @@ theorem t (n : Nat) : n + 0 = n := by namespace PIST.Trace +private def natToJson (n : Nat) : Json := + Json.num { mantissa := (n : Int), exponent := 0 } + private def goalToJson (g : MVarId) : MetaM Json := do let decl ← g.getDecl let target ← instantiateMVars decl.type @@ -40,10 +41,10 @@ private def goalToJson (g : MVarId) : MetaM Json := do ] return Json.mkObj [ - ("target", Json.str targetFmt.pretty), - ("goal_index", Json.num (toNat g.index)), - ("hypotheses", Json.arr hyps), - ("hypothesis_count", Json.num hyps.size) + ("target", Json.str targetFmt.pretty), + ("goal_id", Json.str g.name.toString), + ("hypotheses", Json.arr hyps), + ("hypothesis_count", natToJson hyps.size) ] /-- Emit a structured goal-state snapshot tagged with `tag`. @@ -53,16 +54,15 @@ can scrape it from Lean's stdout. -/ elab "trace_state_json" tag:str : tactic => do let goals ← getGoals - let goalJsons ← goals.mapM goalToJson + let goalJsons ← goals.mapM (fun g => liftMetaM (goalToJson g)) let payload : Json := Json.mkObj [ - ("event", Json.str "pist_trace_state"), - ("tag", Json.str tag.getString), - ("goal_count", Json.num goals.size), - ("goals", Json.arr goalJsons) + ("event", Json.str "pist_trace_state"), + ("tag", Json.str tag.getString), + ("goal_count", natToJson goals.length), + ("goals", Json.arr goalJsons.toArray) ] - -- Emit to logInfo so it appears in stdout logInfo m!"@@PIST_TRACE_JSON@@{payload.compress}" end PIST.Trace