feat(avm): add Lean-only strict-typed ISA skeleton (v1)

0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean

@@ -0,0 +1,42 @@
+-- AVM ISA v1 (Lean-only): Instructions
+-- Closed-world opcodes. No CALL/IMPORT. No string dispatch.
+
+import Semantics.AVMIsa.Value
+
+namespace Semantics.AVMIsa
+
+/-- Finite primitive set (closed-world).
+
+If extensibility is needed, add a constructor here and define its semantics in Lean.
+Backends must implement the same semantics.
+-/
+inductive Prim : Type where
+  | addSatQ0
+  | subSatQ0
+  | addSatQ16
+  | subSatQ16
+  | and
+  | or
+  | not
+  deriving DecidableEq, BEq, Inhabited
+
+/-- Core instruction set.
+
+`load`/`store` use `Nat` indices in this v1 skeleton.
+Strict implementations SHOULD replace them with `Fin n` once the local-frame
+size is part of `Program`.
+-/
+inductive Instr : Type where
+  | push : AnyVal → Instr
+  | pop : Instr
+  | dup : Instr
+  | swap : Instr
+  | load : Nat → Instr
+  | store : Nat → Instr
+  | jump : Nat → Instr
+  | jumpIf : Nat → Instr
+  | prim : Prim → Instr
+  | halt : Instr
+  deriving Inhabited
+
+end Semantics.AVMIsa

0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Run.lean

@@ -0,0 +1,44 @@
+-- AVM ISA v1 (Lean-only): Run semantics (fuel-bounded)
+
+import Semantics.AVMIsa.Step
+
+namespace Semantics.AVMIsa
+
+/-- Fuel for total execution. -/
+abbrev Fuel := Nat
+
+/-- Fuel-bounded run.
+
+Stops when:
+- fuel exhausted
+- machine halted
+- an error occurs
+-/
+def run (fuel : Fuel) (program : List Instr) (s : State) : Outcome State :=
+  match fuel with
+  | 0 => Outcome.ok s
+  | Nat.succ f =>
+      if s.halted then Outcome.ok s
+      else
+        match step program s with
+        | Outcome.err e => Outcome.err e
+        | Outcome.ok s1 => run f program s1
+
+/-- Canary: boolean not.
+
+#eval should produce `true` on top of stack.
+-/
+def canaryNot : List Instr :=
+  [
+    Instr.push ⟨AvmTy.bool, AvmVal.b false⟩,
+    Instr.prim Prim.not,
+    Instr.halt
+  ]
+
+/-- Canary initial state. -/
+def canaryState : State :=
+  { pc := 0, stack := [], locals := [], halted := false }
+
+#eval run 8 canaryNot canaryState
+
+end Semantics.AVMIsa

0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean

@@ -0,0 +1,31 @@
+-- AVM ISA v1 (Lean-only): State
+
+import Semantics.AVMIsa.Instr
+
+namespace Semantics.AVMIsa
+
+/-- Machine state.
+
+This is intentionally minimal in v1. It is sufficient to define a total `run`
+with fuel.
+-/
+structure State where
+  pc : Nat
+  stack : List AnyVal
+  locals : List (Option AnyVal)
+  halted : Bool
+
+deriving Inhabited
+
+/-- Safe locals lookup (returns `none` when out of bounds). -/
+def getLocal? (s : State) (i : Nat) : Option AnyVal :=
+  s.locals.getD i none
+
+/-- 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) }
+  else
+    s
+
+end Semantics.AVMIsa

0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean

@@ -0,0 +1,162 @@
+-- AVM ISA v1 (Lean-only): Step semantics
+
+import Semantics.AVMIsa.State
+
+namespace Semantics.AVMIsa
+
+/-- Error tags for rejected states (ill-typed, underflow, etc.). -/
+inductive StepError : Type where
+  | stackUnderflow
+  | typeMismatch
+  | invalidJump
+  | missingLocal
+  deriving Inhabited, DecidableEq, BEq
+
+/-- Outcome type for AVM execution.
+
+We avoid Float and avoid exceptions. Backends should mirror this boundary.
+-/
+inductive Outcome (α : Type) : Type where
+  | ok : α → Outcome α
+  | err : StepError → Outcome α
+  deriving Inhabited
+
+/-- Pop one element from stack. -/
+def pop1 (s : State) : Outcome (AnyVal × State) :=
+  match s.stack with
+  | [] => Outcome.err StepError.stackUnderflow
+  | x :: xs => Outcome.ok (x, { s with stack := xs })
+
+/-- Push one element onto stack. -/
+def push1 (s : State) (v : AnyVal) : State :=
+  { s with stack := v :: s.stack }
+
+/-- Evaluate a primitive.
+
+NOTE: This v1 skeleton implements only a small subset. Extend strictly by
+adding Lean semantics; do not delegate meaning to backends.
+-/
+def evalPrim (p : Prim) (s : State) : Outcome State :=
+  match p with
+  | Prim.not =>
+      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)⟩)
+          | _ => Outcome.err StepError.typeMismatch
+  | Prim.and =>
+      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) =>
+              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
+  | Prim.or =>
+      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) =>
+              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
+  | Prim.addSatQ0 =>
+      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) =>
+              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
+  | Prim.subSatQ0 =>
+      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) =>
+              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
+  | _ =>
+      -- Remaining primitives are not yet implemented in v1.
+      Outcome.err StepError.typeMismatch
+
+/-- One-step execution.
+
+`Program` is modeled as a list for v1.
+-/
+def step (program : List Instr) (s : State) : Outcome State :=
+  if s.halted then
+    Outcome.ok s
+  else
+    match program.get? s.pc with
+    | none => Outcome.err StepError.invalidJump
+    | some instr =>
+        match instr with
+        | Instr.halt => Outcome.ok { s with halted := true }
+        | Instr.push v => Outcome.ok { s with pc := s.pc + 1, stack := v :: s.stack }
+        | Instr.pop =>
+            match pop1 s with
+            | Outcome.err e => Outcome.err e
+            | Outcome.ok (_, s1) => Outcome.ok { s1 with pc := s.pc + 1 }
+        | Instr.dup =>
+            match s.stack with
+            | [] => Outcome.err StepError.stackUnderflow
+            | x :: xs => Outcome.ok { s with pc := s.pc + 1, stack := x :: x :: xs }
+        | Instr.swap =>
+            match s.stack with
+            | a :: b :: xs => Outcome.ok { s with pc := s.pc + 1, stack := b :: a :: xs }
+            | _ => Outcome.err StepError.stackUnderflow
+        | Instr.load i =>
+            match getLocal? s i with
+            | none => Outcome.err StepError.missingLocal
+            | some v => Outcome.ok { s with pc := s.pc + 1, stack := v :: s.stack }
+        | Instr.store i =>
+            match pop1 s with
+            | Outcome.err e => Outcome.err e
+            | Outcome.ok (v, s1) => Outcome.ok { (setLocal s1 i v) with pc := s.pc + 1 }
+        | Instr.jump target =>
+            if target < program.length then
+              Outcome.ok { s with pc := target }
+            else
+              Outcome.err StepError.invalidJump
+        | Instr.jumpIf target =>
+            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
+        | Instr.prim p =>
+            match evalPrim p s with
+            | Outcome.err e => Outcome.err e
+            | Outcome.ok s1 => Outcome.ok { s1 with pc := s.pc + 1 }
+
+end Semantics.AVMIsa

0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean

@@ -0,0 +1,15 @@
+-- AVM ISA v1 (Lean-only): Types
+-- Core rule: closed-world finite type universe; no Float.
+
+import Semantics.FixedPoint
+
+namespace Semantics.AVMIsa
+
+/-- Finite AVM type universe. Closed-world; extend only by adding constructors. -/
+inductive AvmTy : Type where
+  | q0_16 : AvmTy
+  | q16_16 : AvmTy
+  | bool : AvmTy
+  deriving DecidableEq, BEq, Inhabited
+
+end Semantics.AVMIsa

0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean

@@ -0,0 +1,29 @@
+-- AVM ISA v1 (Lean-only): Values
+-- Values are strictly typed; no dynamic Any.
+
+import Semantics.AVMIsa.Types
+import Semantics.FixedPoint
+
+namespace Semantics.AVMIsa
+
+/-- Typed value payload. -/
+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
+
+/-- Existential wrapper for storing values in an untyped container.
+
+We use this in the ISA skeleton to keep the state representation simple.
+Typing is enforced by an explicit type-check pass and by instruction semantics
+that can reject ill-typed stacks.
+
+Later upgrade path: replace with a fully typed stack representation.
+-/
+structure AnyVal where
+  ty : AvmTy
+  val : AvmVal ty
+
+deriving Inhabited
+
+end Semantics.AVMIsa