From c689979b8ce78e7382b165b78eb811007341556b Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 28 Jun 2026 16:58:44 -0500 Subject: [PATCH] fix(avm-isa): implement symmetric negation and explicit signed comparison mitigations - 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) --- formal/SilverSight/AVMIsa/Run.lean | 34 ++++++++++++++++++++++++++ formal/SilverSight/AVMIsa/Step.lean | 37 +++++++++++++++++++++++------ 2 files changed, 64 insertions(+), 7 deletions(-) diff --git a/formal/SilverSight/AVMIsa/Run.lean b/formal/SilverSight/AVMIsa/Run.lean index ca6ee8b7..fb94ddaa 100644 --- a/formal/SilverSight/AVMIsa/Run.lean +++ b/formal/SilverSight/AVMIsa/Run.lean @@ -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 diff --git a/formal/SilverSight/AVMIsa/Step.lean b/formal/SilverSight/AVMIsa/Step.lean index ce7f8d24..8226e7a4 100644 --- a/formal/SilverSight/AVMIsa/Step.lean +++ b/formal/SilverSight/AVMIsa/Step.lean @@ -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 =>