From a84a704dbf2c9996b1b38ec653e2a82a5e5dc7fd Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Tue, 26 May 2026 16:05:08 -0500 Subject: [PATCH] feat(avm): add Lean-only strict-typed ISA skeleton (v1) --- .../Semantics/Semantics/AVMIsa/Instr.lean | 42 +++++ .../lean/Semantics/Semantics/AVMIsa/Run.lean | 44 +++++ .../Semantics/Semantics/AVMIsa/State.lean | 31 ++++ .../lean/Semantics/Semantics/AVMIsa/Step.lean | 162 ++++++++++++++++++ .../Semantics/Semantics/AVMIsa/Types.lean | 15 ++ .../Semantics/Semantics/AVMIsa/Value.lean | 29 ++++ 6 files changed, 323 insertions(+) create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Run.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Instr.lean new file mode 100644 index 00000000..21271eab --- /dev/null +++ b/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 diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Run.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Run.lean new file mode 100644 index 00000000..b00eb5fa --- /dev/null +++ b/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 diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/State.lean new file mode 100644 index 00000000..42e73316 --- /dev/null +++ b/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 diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Step.lean new file mode 100644 index 00000000..5e390abc --- /dev/null +++ b/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 diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Types.lean new file mode 100644 index 00000000..24a869cd --- /dev/null +++ b/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 diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Value.lean new file mode 100644 index 00000000..a6e88887 --- /dev/null +++ b/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