Verified binary search in sorted array

BinarySearch.sol

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);
  }
}

Output_BinarySearch.mlw

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

Would this be significantly cheaper without recursion?