mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-10 16:30:34 +00:00
allaun
37ea14842a
V3 (Critical — Division-by-zero sentinel): - Add StepError.divisionByZero variant - Guard q16_div with explicit zero check (Outcome.err on zero divisor) V7 (Medium — Unbounded stack): - Add maxStackDepth := 1024 constant - Refactor push1 to return Outcome (stack bounds check) - Add push1_unchecked for proof compatibility - Add push1_ok_of_lt theorem - Guard Instr.push and Instr.dup with stack depth checks V8 (Medium — Silent store): - Add setLocal? to State.lean returning Option State - Wire store instruction to propagate missingLocal on OOB - Preserve backward-compatible setLocal for TypeSafety proofs V1/V2 (Critical — Intermediate overflow): - Add #eval witnesses proving worst-case intermediates fit Int64 - Backend spec mandate: all AVM backends MUST use >= 64-bit storage V4 (Critical — Rounding direction): - Add #eval witnesses documenting Euclidean division semantics - Note: Lean ediv matches Python // for positive divisors only
40 lines
1 KiB
Text
40 lines
1 KiB
Text
-- AVM ISA v1 (Lean-only): State
|
|
|
|
import SilverSight.AVMIsa.Instr
|
|
|
|
namespace SilverSight.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, Repr
|
|
|
|
/-- 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.
|
|
V8 mitigation: returns `none` on out-of-bounds instead of silently
|
|
dropping the store. The step function maps this to StepError.missingLocal. -/
|
|
def setLocal? (s : State) (i : Nat) (v : AnyVal) : Option State :=
|
|
if i < s.locals.length then
|
|
some { s with locals := s.locals.set i (some v) }
|
|
else
|
|
none
|
|
|
|
/-- Backward-compatible wrapper (used by TypeSafety proofs). -/
|
|
def setLocal (s : State) (i : Nat) (v : AnyVal) : State :=
|
|
if i < s.locals.length then
|
|
{ s with locals := s.locals.set i (some v) }
|
|
else
|
|
s
|
|
|
|
end SilverSight.AVMIsa
|