Skip to content

Fix the semantics of the signed remainder: MIN % -1 overflows #21

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
karthikbhargavan wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Fix the semantics of the signed remainder: MIN % -1 overflows #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion backends/coq/Primitives.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -251,7 +251,12 @@ Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) :=
if to_Z y =? 0 then Fail_ Failure else
mk_scalar ty (to_Z x / to_Z y).

Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)).
Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) :=
if to_Z y =? 0 then Fail_ Failure else
(* There can be an overflow if [x] is equal to the lower bound and [y] to [-1]:
the remainder is then in bounds (it is [0]) but the operation panics in Rust *)
if (to_Z x =? scalar_min ty) && (to_Z y =? (-1)) then Fail_ Failure else
mk_scalar ty (Z.rem (to_Z x) (to_Z y)).

Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)).

Expand Down
11 changes: 10 additions & 1 deletion backends/fstar/Primitives.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,16 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
let _ = assert_norm(int_rem (-1) (-2) = -1)

let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
if y <> 0 then
(* There can be an overflow if [x] is equal to the lower bound and [y] to [-1]:
the remainder is then in bounds (it is [0]) but the operation panics in Rust *)
if x = scalar_min ty && y = -1 then Fail Failure
else mk_scalar ty (int_rem x y)
else Fail Failure

(* Checking consistency with Rust: [MIN % -1] panics, [MIN % 1] doesn't *)
let _ = assert_norm(scalar_rem #I32 (-0x80000000) (-1) = Fail Failure)
let _ = assert_norm(scalar_rem #I32 (-0x80000000) 1 = Ok 0)

let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
mk_scalar ty (x + y)
Expand Down
18 changes: 11 additions & 7 deletions backends/lean/Aeneas/Std/Scalar/CheckedOps/Rem.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,27 +58,31 @@ Signed checked rem
-/
theorem core.num.checked_rem_IScalar_bv_spec {ty} (x y : IScalar ty) :
match core.num.checked_rem_IScalar x y with
| some z => y.val ≠ 0 ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
| none => y.val = 0 := by
| some z => y.val ≠ 0 ∧ ¬ (x.val = IScalar.min ty ∧ y.val = -1) ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
| none => y.val = 0 ∨ (x.val = IScalar.min ty ∧ y.val = -1) := by
simp [checked_rem_IScalar, Option.ofResult, IScalar.rem]
split_ifs
. zify at *
simp_all
. rename_i hnz
. rename_i hnz hNoOverflow
simp
have hnz' : y.val ≠ 0 := by zify at *; simp_all
have : x % y = x.rem y := by rfl
have ⟨ _, hz ⟩ := spec_imp_exists (@IScalar.rem_bv_spec _ x y hnz')
have ⟨ _, hz ⟩ := spec_imp_exists (@IScalar.rem_bv_spec _ x y hnz' (by simp; tauto))
simp [this, IScalar.rem, hnz] at hz
split_ifs at hz
simp at hz
simp [*]
tauto
. simp_all

iscalar @[step_pure «%S».checked_rem x y]
theorem «%S».checked_rem_bv_spec (x y : «%S») :
match core.num.checked_rem_IScalar x y with
| some z => y.val ≠ 0 ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
| none => y.val = 0 := by
| some z => y.val ≠ 0 ∧ ¬ (x.val = «%S».min ∧ y.val = -1) ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
| none => y.val = 0 ∨ (x.val = «%S».min ∧ y.val = -1) := by
have := core.num.checked_rem_IScalar_bv_spec x y
simp_all only [«%S».bv]
simp_all only [«%S».bv, IScalar.min, «%S».min, «%S».numBits]
cases h: core.num.checked_rem_IScalar x y <;> simp_all

end Aeneas.Std
43 changes: 34 additions & 9 deletions backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,10 @@ def UScalar.rem {ty : UScalarTy} (x y : UScalar ty) : Result (UScalar ty) :=
if y.val != 0 then ok ⟨ BitVec.umod x.bv y.bv ⟩ else fail divisionByZero

def IScalar.rem {ty : IScalarTy} (x y : IScalar ty) : Result (IScalar ty) :=
if y.val != 0 then ok ⟨ BitVec.srem x.bv y.bv ⟩
if y.val != 0 then
-- There can be an overflow if `x` is equal to the lower bound and `y` to `-1`
if ¬ (x.val = IScalar.min ty && y.val = -1) then ok ⟨ BitVec.srem x.bv y.bv ⟩
else fail integerOverflow
else fail divisionByZero

def UScalar.try_rem {ty : UScalarTy} (x y : UScalar ty) : Option (UScalar ty) :=
Expand Down Expand Up @@ -62,6 +65,23 @@ namespace Tests
#assert bv_srem (-7) 3 = -1
#assert bv_srem 7 (-3) = 1
#assert bv_srem (-7) (-3) = -1

-- Checking that `MIN % -1` overflows (like `MIN / -1`) while `MIN % 1` succeeds
#assert (IScalar.rem (I8.ofInt (-2^7)) (I8.ofInt (-1)) == fail integerOverflow)
#assert (IScalar.rem (I16.ofInt (-2^15)) (I16.ofInt (-1)) == fail integerOverflow)
#assert (IScalar.rem (I32.ofInt (-2^31)) (I32.ofInt (-1)) == fail integerOverflow)
#assert (IScalar.rem (I64.ofInt (-2^63)) (I64.ofInt (-1)) == fail integerOverflow)
#assert (IScalar.rem (I128.ofInt (-2^127)) (I128.ofInt (-1)) == fail integerOverflow)
#assert (IScalar.rem (I8.ofInt (-2^7)) (I8.ofInt 1) == ok (I8.ofInt 0))
#assert (IScalar.rem (I16.ofInt (-2^15)) (I16.ofInt 1) == ok (I16.ofInt 0))
#assert (IScalar.rem (I32.ofInt (-2^31)) (I32.ofInt 1) == ok (I32.ofInt 0))
#assert (IScalar.rem (I64.ofInt (-2^63)) (I64.ofInt 1) == ok (I64.ofInt 0))
#assert (IScalar.rem (I128.ofInt (-2^127)) (I128.ofInt 1) == ok (I128.ofInt 0))
#assert (IScalar.rem (I32.ofInt (-7)) (I32.ofInt (-1)) == ok (I32.ofInt 0))
#assert (IScalar.rem (I32.ofInt 7) (I32.ofInt 3) == ok (I32.ofInt 1))
#assert (IScalar.rem (I32.ofInt 7) (I32.ofInt 0) == fail divisionByZero)
#assert (UScalar.rem (U32.ofNat 7) (U32.ofNat 3) == ok (U32.ofNat 1))
#assert (UScalar.rem (U32.ofNat 7) (U32.ofNat 0) == fail divisionByZero)
Comment on lines +69 to +84

@abentkamp abentkamp Jul 29, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These tests should probably converted to Rust and go into tests/src

end Tests

/-!
Expand All @@ -81,10 +101,12 @@ theorem UScalar.rem_bv_spec {ty} (x : UScalar ty) {y : UScalar ty} (hzero : y.va
simp

/-- Generic theorem - shouldn't be used much -/
theorem IScalar.rem_bv_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0) :
theorem IScalar.rem_bv_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0)
(hNoOverflow : ¬ (x.val = IScalar.min ty ∧ y.val = -1)) :
x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ∧ z.bv = BitVec.srem x.bv y.bv ⦄ := by
conv => arg 1; simp [HMod.hMod]
simp only [spec_ok, rem, bne_iff_ne, ne_eq, hzero, not_false_eq_true, ↓reduceIte]
simp only [spec_ok, rem, bne_iff_ne, ne_eq, hzero, not_false_eq_true, ↓reduceIte,
Int.reduceNeg, Bool.and_eq_true, decide_eq_true_eq, hNoOverflow]
simp only [val]
simp only [BitVec.toInt_srem, bv_toInt_eq, and_true]

Expand All @@ -93,9 +115,10 @@ uscalar theorem «%S».rem_bv_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0)
x % y ⦃ z => (↑z : Nat) = ↑x % ↑y ∧ z.bv = x.bv % y.bv ⦄ :=
UScalar.rem_bv_spec x hnz

iscalar theorem «%S».rem_bv_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0) :
iscalar theorem «%S».rem_bv_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0)
(hNoOverflow : ¬ (x.val = «%S».min ∧ y.val = -1)) :
x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ∧ z.bv = BitVec.srem x.bv y.bv ⦄ :=
IScalar.rem_bv_spec x hnz
IScalar.rem_bv_spec x hnz (by scalar_tac)

/-!
Theorems with a specification which only uses integers
Expand All @@ -110,19 +133,21 @@ theorem UScalar.rem_spec {ty} (x : UScalar ty) {y : UScalar ty} (hzero : y.val
exact h.1

/-- Generic theorem - shouldn't be used much -/
theorem IScalar.rem_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0) :
theorem IScalar.rem_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0)
(hNoOverflow : ¬ (x.val = IScalar.min ty ∧ y.val = -1)) :
x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ⦄ := by
apply spec_mono
· apply rem_bv_spec x hzero
· apply rem_bv_spec x hzero hNoOverflow
· intros x' h
exact h.1

uscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0) :
x % y ⦃ z => (↑z : Nat) = ↑x % ↑y ⦄ :=
UScalar.rem_spec x hnz

iscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0) :
iscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0)
(hNoOverflow : ¬ (x.val = «%S».min ∧ y.val = -1)) :
x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ⦄ :=
IScalar.rem_spec x hnz
IScalar.rem_spec x hnz (by scalar_tac)

end Aeneas.Std
10 changes: 8 additions & 2 deletions src/interp/InterpExpressions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1037,8 +1037,14 @@ let eval_binary_op_concrete_compute (span : Meta.span) (binop : binop)
if sv2_value = Z.zero then Error ()
else mk_scalar ptr_size sv1_int_ty (Z.div sv1_value sv2_value)
| Rem OPanic ->
(* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
if sv2_value = Z.zero then Error ()
(* See [https://github.com/ocaml/Zarith/blob/master/z.mli].
[MIN % -1] panics in Rust (like [MIN / -1]): the result
is in bounds (it is [0]) so [mk_scalar] doesn't catch it. *)
if
sv2_value = Z.zero
|| (sv1_value = scalar_min ptr_size sv1_int_ty
&& sv2_value = Z.minus_one)
then Error ()
else mk_scalar ptr_size sv1_int_ty (Z.rem sv1_value sv2_value)
| Add OPanic ->
mk_scalar ptr_size sv1_int_ty (Z.add sv1_value sv2_value)
Expand Down