You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If the input of the ceil function is an integer x(that is, x modulo FRACT_PART is equal to 0), it will return x+1. But I think this does not match the usual semantics of ceil function in mathematics.
The bug is found by Medjai, a symbolic execution tool for the Cairo program. The spec we write for ceil is:
func ceil_spec{range_check_ptr}():
alloc_locals
let (local x) = SymbolicMath64x61()
let (local res) = Math64x61.ceil(x)
verify_le_signed(x, res)
verify_lt_signed(res - Math64x61.ONE, x)
let (_, rem) = signed_div_rem(res, Math64x61.ONE, Math64x61.BOUND)
medjai_assert_eq_felt(rem, 0)
return ()
end
The text was updated successfully, but these errors were encountered:
If the input of the
ceil
function is an integer x(that is, x modulo FRACT_PART is equal to 0), it will return x+1. But I think this does not match the usual semantics of ceil function in mathematics.The bug is found by Medjai, a symbolic execution tool for the Cairo program. The spec we write for
ceil
is:The text was updated successfully, but these errors were encountered: