fix(avm-isa): stabilize AVMIsa + PIST.Trace build; canary #eval fires clean

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>

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

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
+  if i < s.locals.length then
-    { s with locals := s.locals.set ⟨i, h⟩ (some v) }
+    { s with locals := s.locals.set i (some v) }
   else
     s
 

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
+          match v with
-          | AvmTy.bool =>
+          | ⟨AvmTy.bool, AvmVal.b x⟩ =>
-              let b := match v.val with | AvmVal.b x => x
+              Outcome.ok (push1 s1 ⟨AvmTy.bool, AvmVal.b (!x)⟩)
-              Outcome.ok (push1 s1 ⟨AvmTy.bool, AvmVal.b (!b)⟩)
           | _ => 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
+              match v1, v2 with
-                let b1 := match v1.val with | AvmVal.b x => x
+              | ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ =>
-                let b2 := match v2.val with | AvmVal.b x => x
+                  Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 && b1)⟩)
-                Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 && b1)⟩)
+              | _, _ => Outcome.err StepError.typeMismatch
-              else
-                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
+              match v1, v2 with
-                let b1 := match v1.val with | AvmVal.b x => x
+              | ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ =>
-                let b2 := match v2.val with | AvmVal.b x => x
+                  Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 || b1)⟩)
-                Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 || b1)⟩)
+              | _, _ => Outcome.err StepError.typeMismatch
-              else
-                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
+              match v1, v2 with
-                let x := match v1.val with | AvmVal.q0 q => q
+              | ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
-                let y := match v2.val with | AvmVal.q0 q => q
+                  Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.add y x)⟩)
-                Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.addSat y x)⟩)
+              | _, _ => Outcome.err StepError.typeMismatch
-              else
-                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
+              match v1, v2 with
-                let x := match v1.val with | AvmVal.q0 q => q
+              | ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
-                let y := match v2.val with | AvmVal.q0 q => q
+                  Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.sub y x)⟩)
-                Outcome.ok (push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (Semantics.Q0_16.subSat y x)⟩)
+              | _, _ => Outcome.err StepError.typeMismatch
-              else
-                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
+                match v with
-                  let b := match v.val with | AvmVal.b x => x
+                | ⟨AvmTy.bool, AvmVal.b b⟩ =>
-                  if b then
+                    if b then
-                    if target < program.length then Outcome.ok { s1 with pc := target } else Outcome.err StepError.invalidJump
+                      if target < program.length then
-                  else
+                        Outcome.ok { s1 with pc := target }
-                    Outcome.ok { s1 with pc := s.pc + 1 }
+                      else
-                else
+                        Outcome.err StepError.invalidJump
-                  Outcome.err StepError.typeMismatch
+                    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

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

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

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),
+    ("target",           Json.str targetFmt.pretty),
-    ("goal_index", Json.num (toNat g.index)),
+    ("goal_id",          Json.str g.name.toString),
-    ("hypotheses", Json.arr hyps),
+    ("hypotheses",       Json.arr hyps),
-    ("hypothesis_count", Json.num hyps.size)
+    ("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"),
+    ("event",      Json.str "pist_trace_state"),
-    ("tag", Json.str tag.getString),
+    ("tag",        Json.str tag.getString),
-    ("goal_count", Json.num goals.size),
+    ("goal_count", natToJson goals.length),
-    ("goals", Json.arr goalJsons)
+    ("goals",      Json.arr goalJsons.toArray)
   ]
 
-  -- Emit to logInfo so it appears in stdout
   logInfo m!"@@PIST_TRACE_JSON@@{payload.compress}"
 
 end PIST.Trace