Skip to content

Instantly share code, notes, and snippets.

@chriseth

chriseth/BinarySearch.sol

Last active Nov 27, 2018
Embed
What would you like to do?
Verified binary search in sorted array
contract BinarySearch {
///@why3
/// requires { arg_data.length < UInt256.max_uint256 }
/// requires { 0 <= to_int arg_begin <= to_int arg_end <= arg_data.length }
/// requires { forall i j: int. 0 <= i <= j < arg_data.length -> to_int arg_data[i] <= to_int arg_data[j] }
/// variant { to_int arg_end - to_int arg_begin }
/// ensures {
/// to_int result < UInt256.max_uint256 -> (to_int arg_begin <= to_int result < to_int arg_end && to_int arg_data[to_int result] = to_int arg_value)
/// }
/// ensures {
/// to_int result = UInt256.max_uint256 -> (forall i: int. to_int arg_begin <= i < to_int arg_end -> to_int arg_data[i] <> to_int arg_value)
/// }
function find_internal(uint[] data, uint begin, uint end, uint value) internal returns (uint ret) {
uint len = end - begin;
if (len == 0 || (len == 1 && data[begin] != value)) {
return 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff;
}
uint mid = begin + len / 2;
uint v = data[mid];
if (value < v)
return find_internal(data, begin, mid, value);
else if (value > v)
return find_internal(data, mid + 1, end, value);
else
return mid;
}
///@why3
/// requires { arg_data.length < UInt256.max_uint256 }
/// requires { forall i j: int. 0 <= i <= j < arg_data.length -> to_int arg_data[i] <= to_int arg_data[j] }
/// ensures {
/// to_int result < UInt256.max_uint256 -> to_int arg_data[to_int result] = to_int arg_value
/// }
/// ensures {
/// to_int result = UInt256.max_uint256 -> forall i: int. 0 <= i < arg_data.length -> to_int arg_data[i] <> to_int arg_value
/// }
function find(uint[] data, uint value) returns (uint ret) {
return find_internal(data, 0, data.length, value);
}
}
module UInt256
use import mach.int.Unsigned
type uint256
constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
clone export mach.int.Unsigned with
type t = uint256,
constant max = max_uint256
end
module Solidity
use import int.Int
use import ref.Ref
use import map.Map
use import array.Array
use import int.ComputerDivision
use import mach.int.Unsigned
use import UInt256
exception Ret
type state = StateUnused
let rec _find_internal (state: state) (arg_data: array uint256) (arg_begin: uint256) (arg_end: uint256) (arg_value: uint256):
(uint256)
requires { arg_data.length < UInt256.max_uint256 } requires { 0 <= to_int arg_begin <= to_int arg_end <= arg_data.length } requires { forall i j: int. 0 <= i <= j < arg_data.length -> to_int arg_data[i] <= to_int arg_data[j] } variant { to_int arg_end - to_int arg_begin } ensures { to_int result < UInt256.max_uint256 -> (to_int arg_begin <= to_int result < to_int arg_end && to_int arg_data[to_int result] = to_int arg_value) } ensures { to_int result = UInt256.max_uint256 -> (forall i: int. to_int arg_begin <= i < to_int arg_end -> to_int arg_data[i] <> to_int arg_value) }
=
let _data = ref arg_data in
let _begin = ref arg_begin in
let _end = ref arg_end in
let _value = ref arg_value in
let _ret: ref uint256 = ref (of_int 0) in
let _len: ref uint256 = ref (of_int 0) in
let _mid: ref uint256 = ref (of_int 0) in
let _v: ref uint256 = ref (of_int 0) in
try
begin
_len := (!_end - !_begin);
if ((!_len = (of_int 0)) || (((!_len = (of_int 1)) && ((!_data[to_int !_begin]) <> !_value)))) then
begin
begin _ret := (of_int 115792089237316195423570985008687907853269984665640564039457584007913129639935); raise Ret end
end;
_mid := (!_begin + (!_len / (of_int 2)));
_v := (!_data[to_int !_mid]);
if (!_value < !_v) then
begin _ret := (_find_internal StateUnused !_data !_begin !_mid !_value); raise Ret end
else
if (!_value > !_v) then
begin _ret := (_find_internal StateUnused !_data (!_mid + (of_int 1)) !_end !_value); raise Ret end
else
begin _ret := !_mid; raise Ret end
end;
raise Ret
with Ret -> (!_ret)
end
let rec _find (state: state) (arg_data: array uint256) (arg_value: uint256):
(uint256)
requires { arg_data.length < UInt256.max_uint256 } requires { forall i j: int. 0 <= i <= j < arg_data.length -> to_int arg_data[i] <= to_int arg_data[j] } ensures { to_int result < UInt256.max_uint256 -> to_int arg_data[to_int result] = to_int arg_value } ensures { to_int result = UInt256.max_uint256 -> forall i: int. 0 <= i < arg_data.length -> to_int arg_data[i] <> to_int arg_value }
=
let _data = ref arg_data in
let _value = ref arg_value in
let _ret: ref uint256 = ref (of_int 0) in
try
begin
begin _ret := (_find_internal StateUnused !_data (of_int 0) (of_int !_data.length) !_value); raise Ret end
end;
raise Ret
with Ret -> (!_ret)
end
end
@moodysalem

This comment has been minimized.

Copy link

@moodysalem moodysalem commented Nov 27, 2018

Would this be significantly cheaper without recursion?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.