allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-08-06 15:05:46 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(avm-isa): implement symmetric negation and explicit signed comparison mitigations

Browse source 
- V5: Enforce symmetric raw boundaries [-2147483647, 2147483647] internally using ofAvmRaw/ofAvmRawQ0 and all VM-level Q16/Q0 arithmetic results.
- V6: Decompose Q16 comparison into explicit sign bit and magnitude checks to ensure backend comparison signedness.
- Added V5 and V6 canaries in Run.lean verifying symmetric negation involution and correct signed comparison.

Build: 3307 jobs, 0 errors (lake build)
This commit is contained in:
allaun 2026-06-28 16:58:44 -05:00
parent 02888af08e
commit c689979b8c
2 changed files with 64 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
formal/SilverSight/AVMIsa/Run.lean
View file

@ -144,4 +144,38 @@ def canaryDivByZero : List Instr :=
-- V7 witness: maxStackDepth is 1024.
#eval maxStackDepth -- expect 1024
-- ─────────────────────────────────────────────────────────────────────────────
-- §V5 Symmetric negation involution canary
-- ─────────────────────────────────────────────────────────────────────────────
/-- V5 canary: subtraction 0 - x is symmetric and clamps -2147483648 to 2147483647.
Push 0.0 → Push -2147483648 → subSatQ16 → should result in 2147483647 (maxVal). -/
def canaryV5Negation : List Instr :=
[
Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 0)⟩,
Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt (-2147483648))⟩,
Instr.prim Prim.subSatQ16,
Instr.halt
]
#eval run 8 canaryV5Negation canaryState
-- Expected: Outcome.ok with stack containing 2147483647
-- ─────────────────────────────────────────────────────────────────────────────
-- §V6 Signed comparison signedness canary
-- ─────────────────────────────────────────────────────────────────────────────
/-- V6 canary: checks that -2000000000 < 65536 is true (signed comparison).
Push -2000000000 → Push 65536 → ltQ16 → should result in true. -/
def canaryV6SignedLt : List Instr :=
[
Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt (-2000000000))⟩,
Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 65536)⟩,
Instr.prim Prim.ltQ16,
Instr.halt
]
#eval run 8 canaryV6SignedLt canaryState
-- Expected: Outcome.ok with stack containing bool true
end SilverSight.AVMIsa

37
formal/SilverSight/AVMIsa/Step.lean
View file

@ -23,6 +23,26 @@ inductive Outcome (α : Type) : Type where
| err : StepError → Outcome α
deriving Inhabited, Repr
/-- Bounded/symmetric Q16 construction.
V5 mitigation: clamps raw values to [-2147483647, 2147483647] internally.
This guarantees that the negative boundary is symmetric, making negation
a perfect involution for all VM values. -/
def ofAvmRaw (raw : Int) : SilverSight.Q16_16 :=
let clamped :=
if raw > 2147483647 then 2147483647
else if raw < -2147483647 then -2147483647
else raw
SilverSight.FixedPoint.Q16_16.ofRawInt clamped
/-- Bounded/symmetric Q0 construction.
V5 mitigation: clamps raw values to [-32767, 32767] internally. -/
def ofAvmRawQ0 (raw : Int) : SilverSight.Q0_16 :=
let clamped :=
if raw > 32767 then 32767
else if raw < -32767 then -32767
else raw
SilverSight.FixedPoint.Q0_16.ofRawInt clamped
/-- Pop one element from stack. -/
def pop1 (s : State) : Outcome (AnyVal × State) :=
match s.stack with
@ -100,7 +120,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (SilverSight.Q0_16.add y x)⟩
push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (ofAvmRawQ0 (y.toInt + x.toInt))⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.subSatQ0 =>
match pop1 s with
@ -111,7 +131,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (SilverSight.Q0_16.sub y x)⟩
push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (ofAvmRawQ0 (y.toInt - x.toInt))⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.addSatQ16 =>
match pop1 s with
@ -122,7 +142,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.add y x)⟩
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw (y.toInt + x.toInt))⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.subSatQ16 =>
match pop1 s with
@ -133,7 +153,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.sub y x)⟩
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw (y.toInt - x.toInt))⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.mulSatQ16 =>
match pop1 s with
@ -144,7 +164,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| Outcome.ok (v2, s2) =>
match v1, v2 with
| ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.mul y x)⟩
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw ((y.toInt * x.toInt) / 65536))⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.divSatQ16 =>
-- V3 mitigation: explicit division-by-zero error
@ -159,7 +179,7 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
if x.toInt = 0 then
Outcome.err StepError.divisionByZero
else
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.div y x)⟩
push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw ((y.toInt * 65536) / x.toInt))⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.ltQ16 =>
match pop1 s with
@ -170,7 +190,10 @@ def evalPrim (p : Prim) (s : State) : Outcome State :=
| 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
-- V6: Explicit signed comparison via sign decomposition
let sa := y.toInt < 0
let sb := x.toInt < 0
let res := if sa != sb then sa else y.toInt < x.toInt
push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩
| _, _ => Outcome.err StepError.typeMismatch
| Prim.eqQ16 =>