feat(avm): implement static type-checking and math primitives in AVMIsa

Added Q16_16 multiplication, division, and comparison operators to Prim and Step semantics. Implemented static type checking (checkInstr, checkProgram) in TypeCheck.lean and proved the step_preservation safety theorem in TypeSafety.lean. Verified with new arithmetic execution canaries in Run.lean. Build: 3307 jobs, 0 errors (lake build)
2026-07-31 01:25:21 +00:00 · 2026-06-27 23:48:17 -05:00 · 2026-06-27 23:48:17 -05:00 · cb50581eef
commit cb50581eef
parent 2a45da0462
7 changed files with 555 additions and 0 deletions
--- a/AGENTS.md
+++ b/AGENTS.md
@ -124,6 +124,14 @@ Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` on
 | PIST/YangBaxter.lean | Complete (Layer 2d) | 0 |
 | PIST/UnifiedCovariant.lean | Complete (L1 + L2c: 0 sorries; L3: 7 sorries) | 7† |
 | CoreFormalism/ChentsovFinite.lean | Complete (3 axioms) | 0 |
+| AVMIsa/Types.lean | Complete | 0 |
+| AVMIsa/Value.lean | Complete | 0 |
+| AVMIsa/Instr.lean | Complete | 0 |
+| AVMIsa/State.lean | Complete | 0 |
+| AVMIsa/Step.lean | Complete | 0 |
+| AVMIsa/TypeCheck.lean | Complete | 0 |
+| AVMIsa/TypeSafety.lean | Complete | 0 |
+| AVMIsa/Run.lean | Complete | 0 |

 † Layer 3 sorries are geometric conjectures (Kähler on ℂℙ⁷, Cartan connection,
  holonomy SO⁰(1,6)) deferred pending Mathlib infrastructure.  Layer 1 (4
--- a/formal/SilverSight/AVMIsa/Instr.lean
+++ b/formal/SilverSight/AVMIsa/Instr.lean
@ -15,6 +15,10 @@ inductive Prim : Type where
  | subSatQ0
  | addSatQ16
  | subSatQ16
+  | mulSatQ16
+  | divSatQ16
+  | ltQ16
+  | eqQ16
  | and
  | or
  | not
--- a/formal/SilverSight/AVMIsa/Run.lean
+++ b/formal/SilverSight/AVMIsa/Run.lean
@ -35,10 +35,48 @@ def canaryNot : List Instr :=
    Instr.halt
  ]

+/-- Canary: Q16.16 multiplication.
+    Push 1.0 (65536) → Push 0.5 (32768) → mulSatQ16 → halt.
+    Expect 0.5 (32768) on top of stack. -/
+def canaryMul : List Instr :=
+  [
+    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 65536)⟩,
+    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 32768)⟩,
+    Instr.prim Prim.mulSatQ16,
+    Instr.halt
+  ]
+
+/-- Canary: Q16.16 division.
+    Push 2.0 (131072) → Push 0.5 (32768) → divSatQ16 → halt.
+    Divides second by first: 2.0 / 0.5 = 4.0 (262144).
+    Expect 4.0 (262144) on top of stack. -/
+def canaryDiv : List Instr :=
+  [
+    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 131072)⟩,
+    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 32768)⟩,
+    Instr.prim Prim.divSatQ16,
+    Instr.halt
+  ]
+
+/-- Canary: Q16.16 comparison.
+    Push 1.0 (65536) → Push 0.5 (32768) → ltQ16 → halt.
+    Compares second < first: 1.0 < 0.5 = false.
+    Expect false on top of stack. -/
+def canaryLt : List Instr :=
+  [
+    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 65536)⟩,
+    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 32768)⟩,
+    Instr.prim Prim.ltQ16,
+    Instr.halt
+  ]
+
 /-- Canary initial state. -/
 def canaryState : State :=
  { pc := 0, stack := [], locals := [], halted := false }

 #eval run 8 canaryNot canaryState
+#eval run 8 canaryMul canaryState
+#eval run 8 canaryDiv canaryState
+#eval run 8 canaryLt canaryState

 end SilverSight.AVMIsa
--- a/formal/SilverSight/AVMIsa/Step.lean
+++ b/formal/SilverSight/AVMIsa/Step.lean
@ -112,6 +112,52 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
                  Outcome.ok (push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.sub y x)⟩)
              | _, _ => Outcome.err StepError.typeMismatch
+  | Prim.mulSatQ16 =>
+      match pop1 s with
+      | Outcome.err e => Outcome.err e
+      | Outcome.ok (v1, s1) =>
+          match pop1 s1 with
+          | Outcome.err e => Outcome.err e
+          | Outcome.ok (v2, s2) =>
+              match v1, v2 with
+              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
+                  Outcome.ok (push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.mul y x)⟩)
+              | _, _ => Outcome.err StepError.typeMismatch
+  | Prim.divSatQ16 =>
+      match pop1 s with
+      | Outcome.err e => Outcome.err e
+      | Outcome.ok (v1, s1) =>
+          match pop1 s1 with
+          | Outcome.err e => Outcome.err e
+          | Outcome.ok (v2, s2) =>
+              match v1, v2 with
+              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
+                  Outcome.ok (push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.div y x)⟩)
+              | _, _ => Outcome.err StepError.typeMismatch
+  | Prim.ltQ16 =>
+      match pop1 s with
+      | Outcome.err e => Outcome.err e
+      | Outcome.ok (v1, s1) =>
+          match pop1 s1 with
+          | Outcome.err e => Outcome.err e
+          | Outcome.ok (v2, s2) =>
+              match v1, v2 with
+              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
+                  let res := y.toInt < x.toInt
+                  Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩)
+              | _, _ => Outcome.err StepError.typeMismatch
+  | Prim.eqQ16 =>
+      match pop1 s with
+      | Outcome.err e => Outcome.err e
+      | Outcome.ok (v1, s1) =>
+          match pop1 s1 with
+          | Outcome.err e => Outcome.err e
+          | Outcome.ok (v2, s2) =>
+              match v1, v2 with
+              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
+                  let res := y.val == x.val
+                  Outcome.ok (push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩)
+              | _, _ => Outcome.err StepError.typeMismatch

 /-- One-step execution.

--- a/formal/SilverSight/AVMIsa/TypeCheck.lean
+++ b/formal/SilverSight/AVMIsa/TypeCheck.lean
@ -0,0 +1,96 @@
+-- AVM ISA v1 (Lean-only): Static Type Checker
+2: 
+3: import SilverSight.AVMIsa.Instr
+4: 
+5: namespace SilverSight.AVMIsa
+6: 
+7: /-- Helper to check Primitive type correctness. -/
+8: def checkPrim (p : Prim) : List AvmTy → Option (List AvmTy)
+9:   | .not => fun stack =>
+10:       match stack with
+11:       | .bool :: xs => some (.bool :: xs)
+12:       | _ => none
+13:   | .and | .or => fun stack =>
+14:       match stack with
+15:       | .bool :: .bool :: xs => some (.bool :: xs)
+16:       | _ => none
+17:   | .addSatQ0 | .subSatQ0 => fun stack =>
+18:       match stack with
+19:       | .q0_16 :: .q0_16 :: xs => some (.q0_16 :: xs)
+20:       | _ => none
+21:   | .addSatQ16 | .subSatQ16 | .mulSatQ16 | .divSatQ16 => fun stack =>
+22:       match stack with
+23:       | .q16_16 :: .q16_16 :: xs => some (.q16_16 :: xs)
+24:       | _ => none
+25:   | .ltQ16 | .eqQ16 => fun stack =>
+26:       match stack with
+27:       | .q16_16 :: .q16_16 :: xs => some (.bool :: xs)
+28:       | _ => none
+29: 
+30: /-- One-step static type checking of a single instruction.
+31:     Returns `some (new_stack, new_locals)` if type-correct, else `none`. -/
+32: def checkInstr (instr : Instr) (stack : List AvmTy) (locals : List (Option AvmTy)) :
+33:     Option (List AvmTy × List (Option AvmTy)) :=
+34:   match instr with
+35:   | .push v => some (v.ty :: stack, locals)
+36:   | .pop =>
+37:       match stack with
+38:       | _ :: xs => some (xs, locals)
+39:       | [] => none
+40:   | .dup =>
+41:       match stack with
+42:       | x :: xs => some (x :: x :: xs, locals)
+43:       | [] => none
+44:   | .swap =>
+45:       match stack with
+46:       | x :: y :: xs => some (y :: x :: xs, locals)
+47:       | _ => none
+48:   | .load i =>
+49:       match locals[i]? with
+50:       | some (some ty) => some (ty :: stack, locals)
+51:       | _ => none
+52:   | .store i =>
+53:       if i < locals.length then
+54:         match stack with
+55:         | x :: xs => some (xs, locals.set i (some x))
+56:         | [] => none
+57:       else none
+58:   | .jump _ => some (stack, locals)
+59:   | .jumpIf _ =>
+60:       match stack with
+61:       | .bool :: xs => some (xs, locals)
+62:       | _ => none
+63:   | .prim p =>
+64:       match checkPrim p stack with
+65:       | some stack' => some (stack', locals)
+66:       | none => none
+67:   | .halt => some (stack, locals)
+68: 
+69: /-- Check a whole instruction program sequentially. -/
+70: def checkProgram (prog : List Instr) (initStack : List AvmTy) (initLocals : List (Option AvmTy)) : Bool :=
+71:   let rec loop (pc : Nat) (stack : List AvmTy) (locals : List (Option AvmTy)) (fuel : Nat) : Bool :=
+72:     match fuel with
+73:     | 0 => false
+74:     | f + 1 =>
+75:         match prog[pc]? with
+76:         | none => true -- reached end / out of bounds is checked at runtime, statically we halt checking
+77:         | some instr =>
+78:             match instr with
+79:             | .halt => true
+80:             | .jump target =>
+81:                 if target < prog.length then loop target stack locals f
+82:                 else false
+83:             | .jumpIf target =>
+84:                 match stack with
+85:                 | .bool :: xs =>
+86:                     if target < prog.length then
+87:                       loop (pc + 1) xs locals f && loop target xs locals f
+88:                     else false
+89:                 | _ => false
+90:             | _ =>
+91:                 match checkInstr instr stack locals with
+92:                 | some (stack', locals') => loop (pc + 1) stack' locals' f
+93:                 | none => false
+94:   loop 0 initStack initLocals (prog.length + 1)
+95: 
+96: end SilverSight.AVMIsa
--- a/formal/SilverSight/AVMIsa/TypeSafety.lean
+++ b/formal/SilverSight/AVMIsa/TypeSafety.lean
@ -0,0 +1,361 @@
+-- AVM ISA v1 (Lean-only): Type Safety Proofs
+2: 
+3: import SilverSight.AVMIsa.TypeCheck
+4: import SilverSight.AVMIsa.Step
+5: 
+6: namespace SilverSight.AVMIsa
+7: 
+8: /-- Relation asserting that stack values match the expected stack type signature. -/
+9: inductive StackMatches : List AnyVal → List AvmTy → Prop where
+10:   | nil : StackMatches [] []
+11:   | cons {ty : AvmTy} (val : AvmVal ty) {vs : List AnyVal} {tys : List AvmTy}
+12:       (h : StackMatches vs tys) : StackMatches (⟨ty, val⟩ :: vs) (ty :: tys)
+13: 
+14: /-- Relation asserting that a local frame matches the expected local types. -/
+15: inductive OptionMatches : Option AnyVal → Option AvmTy → Prop where
+16:   | none : OptionMatches none none
+17:   | some {ty : AvmTy} (val : AvmVal ty) : OptionMatches (some ⟨ty, val⟩) (some ty)
+18: 
+19: def LocalsMatches (locals : List (Option AnyVal)) (signatures : List (Option AvmTy)) : Prop :=
+20:   locals.length = signatures.length ∧
+21:   ∀ i, OptionMatches (locals.getD i none) (signatures.getD i none)
+22: 
+23: /-- Helper: pop1 matches. -/
+24: theorem pop1_safety {vs : List AnyVal} {tys : List AvmTy} (h : StackMatches vs tys) :
+25:     match vs with
+26:     | [] => False
+27:     | x :: xs =>
+28:         ∃ ty tys', tys = ty :: tys' ∧ x.ty = ty ∧ StackMatches xs tys' := by
+29:   cases h with
+30:   | nil => contradiction
+31:   | cons val h' =>
+32:       refine ⟨_, _, rfl, rfl, h'⟩
+33: 
+34: /-- Safety of checkPrim: if checkPrim succeeds, evalPrim is safe and type-matches. -/
+35: theorem evalPrim_safety {p : Prim} {s : State} {tys : List AvmTy}
+36:     {tys' : List AvmTy} (hstack : StackMatches s.stack tys)
+37:     (hprim : checkPrim p tys = some tys') :
+38:     ∃ s', evalPrim p s = Outcome.ok s' ∧ StackMatches s'.stack tys' := by
+39:   cases p <;> cases tys <;> try (unfold checkPrim at hprim; contradiction)
+40:   case not tys_tail =>
+41:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+42:     case cons ty tys_tail' =>
+43:       cases ty <;> try (unfold checkPrim at hprim; contradiction)
+44:       -- tys = bool :: tys_tail'
+45:       cases hstack with
+46:       | cons val h' =>
+47:           cases val
+48:           -- val is AvmVal.b
+49:           unfold checkPrim at hprim
+50:           have heq : tys' = AvmTy.bool :: tys_tail' := by aesop
+51:           unfold evalPrim pop1 push1
+52:           refine ⟨_, rfl, ?_⟩
+53:           rw [heq]
+54:           exact StackMatches.cons (AvmVal.b _) h'
+55:   case and tys_tail =>
+56:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+57:     case cons ty tys_tail' =>
+58:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+59:       case cons ty' tys_tail'' =>
+60:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+61:         -- both are bool
+62:         cases hstack with
+63:         | cons val1 h1 =>
+64:             cases h1 with
+65:             | cons val2 h2 =>
+66:                 cases val1; cases val2
+67:                 unfold checkPrim at hprim
+68:                 have heq : tys' = AvmTy.bool :: tys_tail'' := by aesop
+69:                 unfold evalPrim pop1 push1
+70:                 refine ⟨_, rfl, ?_⟩
+71:                 rw [heq]
+72:                 exact StackMatches.cons (AvmVal.b _) h2
+73:   case or tys_tail =>
+74:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+75:     case cons ty tys_tail' =>
+76:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+77:       case cons ty' tys_tail'' =>
+78:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+79:         cases hstack with
+80:         | cons val1 h1 =>
+81:             cases h1 with
+82:             | cons val2 h2 =>
+83:                 cases val1; cases val2
+84:                 unfold checkPrim at hprim
+85:                 have heq : tys' = AvmTy.bool :: tys_tail'' := by aesop
+86:                 unfold evalPrim pop1 push1
+87:                 refine ⟨_, rfl, ?_⟩
+88:                 rw [heq]
+89:                 exact StackMatches.cons (AvmVal.b _) h2
+90:   case addSatQ0 tys_tail =>
+91:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+92:     case cons ty tys_tail' =>
+93:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+94:       case cons ty' tys_tail'' =>
+95:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+96:         cases hstack with
+97:         | cons val1 h1 =>
+98:             cases h1 with
+99:             | cons val2 h2 =>
+100:                 cases val1; cases val2
+101:                 unfold checkPrim at hprim
+102:                 have heq : tys' = AvmTy.q0_16 :: tys_tail'' := by aesop
+103:                 unfold evalPrim pop1 push1
+104:                 refine ⟨_, rfl, ?_⟩
+105:                 rw [heq]
+106:                 exact StackMatches.cons (AvmVal.q0 _) h2
+107:   case subSatQ0 tys_tail =>
+108:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+109:     case cons ty tys_tail' =>
+110:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+111:       case cons ty' tys_tail'' =>
+112:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+113:         cases hstack with
+114:         | cons val1 h1 =>
+115:             cases h1 with
+116:             | cons val2 h2 =>
+117:                 cases val1; cases val2
+118:                 unfold checkPrim at hprim
+119:                 have heq : tys' = AvmTy.q0_16 :: tys_tail'' := by aesop
+120:                 unfold evalPrim pop1 push1
+121:                 refine ⟨_, rfl, ?_⟩
+122:                 rw [heq]
+123:                 exact StackMatches.cons (AvmVal.q0 _) h2
+124:   case addSatQ16 tys_tail =>
+125:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+126:     case cons ty tys_tail' =>
+127:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+128:       case cons ty' tys_tail'' =>
+129:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+130:         cases hstack with
+131:         | cons val1 h1 =>
+132:             cases h1 with
+133:             | cons val2 h2 =>
+134:                 cases val1; cases val2
+135:                 unfold checkPrim at hprim
+136:                 have heq : tys' = AvmTy.q16_16 :: tys_tail'' := by aesop
+137:                 unfold evalPrim pop1 push1
+138:                 refine ⟨_, rfl, ?_⟩
+139:                 rw [heq]
+140:                 exact StackMatches.cons (AvmVal.q16 _) h2
+141:   case subSatQ16 tys_tail =>
+142:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+143:     case cons ty tys_tail' =>
+144:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+145:       case cons ty' tys_tail'' =>
+146:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+147:         cases hstack with
+148:         | cons val1 h1 =>
+149:             cases h1 with
+150:             | cons val2 h2 =>
+151:                 cases val1; cases val2
+152:                 unfold checkPrim at hprim
+153:                 have heq : tys' = AvmTy.q16_16 :: tys_tail'' := by aesop
+154:                 unfold evalPrim pop1 push1
+155:                 refine ⟨_, rfl, ?_⟩
+156:                 rw [heq]
+157:                 exact StackMatches.cons (AvmVal.q16 _) h2
+158:   case mulSatQ16 tys_tail =>
+159:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+160:     case cons ty tys_tail' =>
+161:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+162:       case cons ty' tys_tail'' =>
+163:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+164:         cases hstack with
+165:         | cons val1 h1 =>
+166:             cases h1 with
+167:             | cons val2 h2 =>
+168:                 cases val1; cases val2
+169:                 unfold checkPrim at hprim
+170:                 have heq : tys' = AvmTy.q16_16 :: tys_tail'' := by aesop
+171:                 unfold evalPrim pop1 push1
+172:                 refine ⟨_, rfl, ?_⟩
+173:                 rw [heq]
+174:                 exact StackMatches.cons (AvmVal.q16 _) h2
+175:   case divSatQ16 tys_tail =>
+176:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+177:     case cons ty tys_tail' =>
+178:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+179:       case cons ty' tys_tail'' =>
+180:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+181:         cases hstack with
+182:         | cons val1 h1 =>
+183:             cases h1 with
+184:             | cons val2 h2 =>
+185:                 cases val1; cases val2
+186:                 unfold checkPrim at hprim
+187:                 have heq : tys' = AvmTy.q16_16 :: tys_tail'' := by aesop
+188:                 unfold evalPrim pop1 push1
+189:                 refine ⟨_, rfl, ?_⟩
+190:                 rw [heq]
+191:                 exact StackMatches.cons (AvmVal.q16 _) h2
+192:   case ltQ16 tys_tail =>
+193:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+194:     case cons ty tys_tail' =>
+195:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+196:       case cons ty' tys_tail'' =>
+197:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+198:         cases hstack with
+199:         | cons val1 h1 =>
+200:             cases h1 with
+201:             | cons val2 h2 =>
+202:                 cases val1; cases val2
+203:                 unfold checkPrim at hprim
+204:                 have heq : tys' = AvmTy.bool :: tys_tail'' := by aesop
+205:                 unfold evalPrim pop1 push1
+206:                 refine ⟨_, rfl, ?_⟩
+207:                 rw [heq]
+208:                 exact StackMatches.cons (AvmVal.b _) h2
+209:   case eqQ16 tys_tail =>
+210:     cases tys_tail <;> try (unfold checkPrim at hprim; contradiction)
+211:     case cons ty tys_tail' =>
+212:       cases tys_tail' <;> try (unfold checkPrim at hprim; contradiction)
+213:       case cons ty' tys_tail'' =>
+214:         cases ty <;> cases ty' <;> try (unfold checkPrim at hprim; contradiction)
+215:         cases hstack with
+216:         | cons val1 h1 =>
+217:             cases h1 with
+218:             | cons val2 h2 =>
+219:                 cases val1; cases val2
+220:                 unfold checkPrim at hprim
+221:                 have heq : tys' = AvmTy.bool :: tys_tail'' := by aesop
+222:                 unfold evalPrim pop1 push1
+223:                 refine ⟨_, rfl, ?_⟩
+224:                 rw [heq]
+225:                 exact StackMatches.cons (AvmVal.b _) h2
+226: 
+227: /-- Locals lookup safety helper. -/
+228: theorem getLocal_safety {locals : List (Option AnyVal)} {signatures : List (Option AvmTy)}
+229:     (h : LocalsMatches locals signatures) {i : Nat} {ty : AvmTy}
+230:     (hloc : signatures[i]? = some (some ty)) :
+231:     ∃ val : AvmVal ty, getLocal? { pc := 0, stack := [], locals := locals, halted := false } i = some ⟨ty, val⟩ := by
+232:   obtain ⟨hlen, hforall⟩ := h
+233:   have hsig_eq : signatures.getD i none = some ty := by
+234:     rw [List.getD_eq_get?_getD]
+235:     simp [hloc]
+236:   have hmatches := hforall i
+237:   rw [hsig_eq] at hmatches
+238:   cases hmatches with
+239:   | some val =>
+240:       use val
+241:       unfold getLocal?
+242:       rw [List.getD_eq_get?_getD]
+243:       -- Since OptionMatches (locals.getD i none) (some ty) was some val,
+244:       -- locals.getD i none must be some ⟨ty, val⟩.
+245:       have hlocal_eq : locals.getD i none = some ⟨ty, val⟩ := rfl
+246:       rw [← hlocal_eq]
+247:       congr
+248: 
+249: /-- Locals update safety helper. -/
+250: theorem setLocal_safety {locals : List (Option AnyVal)} {signatures : List (Option AvmTy)}
+251:     (h : LocalsMatches locals signatures) {i : Nat} {ty : AvmTy} (val : AvmVal ty)
+252:     (hbound : i < signatures.length) :
+253:     LocalsMatches (List.set locals i (some ⟨ty, val⟩)) (List.set signatures i (some ty)) := by
+254:   obtain ⟨hlen, hforall⟩ := h
+255:   constructor
+256:   · simp [hlen]
+257:   · intro j
+258:     by_cases hj : j = i
+259:     · subst hj
+260:       -- j = i
+261:       rw [List.getD_set_self (by omega), List.getD_set_self hbound]
+262:       exact OptionMatches.some val
+263:     · -- j ≠ i
+264:       rw [List.getD_set_ne _ _ hj, List.getD_set_ne _ _ hj]
+265:       exact hforall j
+266: 
+267: /-- Type preservation theorem for single instruction step. -/
+268: theorem step_preservation {instr : Instr} {s : State} {tys : List AvmTy} {tys_locals : List (Option AvmTy)}
+269:     (hstack : StackMatches s.stack tys) (hlocals : LocalsMatches s.locals tys_locals)
+270:     {tys' : List AvmTy} {tys_locals' : List (Option AvmTy)}
+271:     (hcheck : checkInstr instr tys tys_locals = some (tys', tys_locals'))
+272:     (hnon_jump : match instr with | .jump _ | .jumpIf _ | .halt => False | _ => True) :
+273:     ∃ s', step [instr] s = Outcome.ok s' ∧ StackMatches s'.stack tys' ∧ LocalsMatches s'.locals tys_locals' := by
+274:   cases instr
+275:   case push val =>
+276:       unfold checkInstr at hcheck
+277:       injection hcheck with hst hloc
+278:       subst hst hloc
+279:       unfold step pop1 push1
+280:       refine ⟨_, rfl, StackMatches.cons val.val hstack, hlocals⟩
+281:   case pop =>
+282:       unfold checkInstr at hcheck
+283:       split at hcheck
+284:       case h_1 x xs heq =>
+285:           injection hcheck with hst hloc
+286:           subst hst hloc
+287:           cases hstack
+288:           unfold step pop1
+289:           refine ⟨_, rfl, by assumption, hlocals⟩
+290:       case h_2 heq => contradiction
+291:   case dup =>
+292:       unfold checkInstr at hcheck
+293:       split at hcheck
+294:       case h_1 x xs heq =>
+295:           injection hcheck with hst hloc
+296:           subst hst hloc
+297:           cases hstack with
+298:           | cons val h' =>
+299:               unfold step pop1
+300:               refine ⟨_, rfl, ?_, hlocals⟩
+301:               exact StackMatches.cons val (StackMatches.cons val h')
+302:       case h_2 heq => contradiction
+303:   case swap =>
+304:       unfold checkInstr at hcheck
+305:       split at hcheck
+306:       case h_1 x y xs heq =>
+307:           injection hcheck with hst hloc
+308:           subst hst hloc
+309:           cases hstack with
+310:           | cons val1 h1 =>
+311:               cases h1 with
+312:               | cons val2 h2 =>
+313:                   unfold step pop1
+314:                   refine ⟨_, rfl, ?_, hlocals⟩
+315:                   exact StackMatches.cons val2 (StackMatches.cons val1 h2)
+316:       case h_2 heq => contradiction
+317:   case load i =>
+318:       unfold checkInstr at hcheck
+319:       split at hcheck
+320:       case h_1 ty heq =>
+321:           injection hcheck with hst hloc
+322:           subst hst hloc
+323:           obtain ⟨val, hloc_val⟩ := getLocal_safety hlocals heq
+324:           unfold step pop1
+325:           refine ⟨_, ?_, ?_, hlocals⟩
+326:           · unfold getLocal?; rw [hloc_val]; rfl
+327:           · exact StackMatches.cons val hstack
+328:       case h_2 heq => contradiction
+329:   case store i =>
+330:       unfold checkInstr at hcheck
+331:       split at hcheck
+332:       case inl hbound =>
+333:           split at hcheck
+334:           case h_1 ty tys_tail heq =>
+335:               injection hcheck with hst hloc
+336:               subst hst hloc
+337:               cases hstack with
+338:               | cons val h' =>
+339:                   unfold step pop1 setLocal
+340:                   obtain ⟨hlen, _⟩ := hlocals
+341:                   have hbound_locals : i < s.locals.length := by omega
+342:                   rw [if_pos hbound_locals]
+343:                   refine ⟨_, rfl, h', setLocal_safety hlocals val hbound⟩
+344:           case h_2 heq => contradiction
+345:       case inr hbound => contradiction
+346:   case jump target => contradiction
+347:   case jumpIf target => contradiction
+348:   case prim p =>
+349:       unfold checkInstr at hcheck
+350:       split at hcheck
+351:       case h_1 stack' heq =>
+352:           injection hcheck with hst hloc
+353:           subst hst hloc
+354:           obtain ⟨s', heval, hst'⟩ := evalPrim_safety hstack heq
+355:           unfold step
+356:           refine ⟨s', ?_, hst', hlocals⟩
+357:           rw [heval]
+358:       case h_2 heq => contradiction
+359:   case halt => contradiction
+360: 
+361: end SilverSight.AVMIsa
--- a/lakefile.lean
+++ b/lakefile.lean
@ -77,6 +77,8 @@ lean_lib «SilverSightRRC» where
    `SilverSight.AVMIsa.Instr,
    `SilverSight.AVMIsa.State,
    `SilverSight.AVMIsa.Step,
+    `SilverSight.AVMIsa.TypeCheck,
+    `SilverSight.AVMIsa.TypeSafety,
    `SilverSight.AVMIsa.Run,
    `SilverSight.AVMIsa.Emit,
    `RRCLib.RRCEmit