Commit 4920bbf3 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

example bitwalker: a version of 'peek' closer to SPARK-generated version

parent 735f4968
......@@ -63,8 +63,37 @@ module Bitwalker
end
end
(** return [value] with the bit of index [left] from the left set to [flag] *)
(* version where [left] is an int and not a bitvector, which
is closer to the result of the SPARK translation from signed
integers *)
let poke_64bit (value : BV64.t) (left : int) (flag : bool) : BV64.t
requires { 0 <= left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - left ->
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - left) }
=
let ghost left_bv = BV64.of_int left in
assert { BV64.ult left_bv (BV64.of_int 64) };
assert { (BV64.sub (BV64.of_int 63) left_bv) = BV64.of_int (63 - left) };
abstract
ensures { forall i:BV64.t. BV64.ule i (BV64.of_int 63) ->
i <> BV64.sub (BV64.of_int 63) left_bv ->
BV64.nth_bv result i = BV64.nth_bv value i }
ensures { flag = BV64.nth_bv result (BV64.sub (BV64.of_int 63) left_bv) }
let mask =
BV64.lsl_bv (BV64.int_check 1) (BV64.of_int (63 - left))
in
match flag with
| True -> BV64.bw_or value mask
| False -> BV64.bw_and value (BV64.bw_not mask)
end
end
(* return the bit of [byte] at position [left] starting from the
left *)
(* return the bit of [byte] at position [left] starting from the left *)
let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
requires { 0 <= BV32.to_uint left < 8 }
ensures { result = BV8.nth byte (7 - BV32.to_uint left) }
......
......@@ -8,7 +8,7 @@
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<file name="../bitwalker.mlw" expanded="true">
<theory name="Bitwalker" sum="d4430f5ae75e998e1d531d208d35f01e" expanded="true">
<theory name="Bitwalker" sum="d063c58dd0638984e7de5c762acbe711" expanded="true">
<goal name="nth64">
<proof prover="0"><result status="valid" time="0.10" steps="135"/></proof>
<proof prover="3"><result status="valid" time="0.46"/></proof>
......@@ -29,5768 +29,10 @@
<goal name="WP_parameter nth_ultpre0.3" expl="3. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter nth_ultpre0.3.1" expl="1. postcondition">
<proof prover="3" timelimit="20"><result status="valid" time="2.37"/></proof>
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_library name="BuiltIn"/>
<ip_qualid name="real"/>
</ts_pos>
<ts_pos name="tuple0" arity="0" id="20"
ip_theory="Tuple0">
<ip_library name="why3"/>
<ip_library name="Tuple0"/>
<ip_qualid name="tuple0"/>
</ts_pos>
<ts_pos name="unit" arity="0" id="21"
ip_theory="Unit">
<ip_library name="why3"/>
<ip_library name="Unit"/>
<ip_qualid name="unit"/>
</ts_pos>
<ts_pos name="&apos;mark" arity="0" id="64"
ip_theory="Mark">
<ip_library name="why3"/>
<ip_library name="Mark"/>
<ip_qualid name="&apos;mark"/>
</ts_pos>
<ts_pos name="array" arity="1" id="3425"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="array"/>
</ts_pos>
<ts_pos name="ref" arity="1" id="5775"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ls_pos name="infix =" id="10"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_library name="BuiltIn"/>
<ip_qualid name="infix ="/>
</ls_pos>
<ls_pos name="zero" id="968"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="969"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="970"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix &gt;" id="973"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;"/>
</ls_pos>
<ls_pos name="infix +" id="2139"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="2140"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="2141"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="abs" id="2254"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="abs"/>
</ls_pos>
<ls_pos name="div" id="2379"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="div"/>
</ls_pos>
<ls_pos name="mod" id="2382"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="mod"/>
</ls_pos>
<ls_pos name="get" id="2998"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="3001"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix []" id="3008"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix []"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3021"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="get" id="3433"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="3448"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix []" id="3473"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix []"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3490"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="andb" id="4784"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="andb"/>
</ls_pos>
<ls_pos name="orb" id="4793"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="orb"/>
</ls_pos>
<ls_pos name="notb" id="4802"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="notb"/>
</ls_pos>
<ls_pos name="xorb" id="4807"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="xorb"/>
</ls_pos>
<ls_pos name="implb" id="4816"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="implb"/>
</ls_pos>
<ls_pos name="prefix !" id="5781"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="pow2" id="6071"
ip_theory="Pow2int">
<ip_library name="bv"/>
<ip_qualid name="pow2"/>
</ls_pos>
<ls_pos name="nth" id="6546"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="nth"/>
</ls_pos>
<ls_pos name="zero" id="6551"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="ones" id="6554"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="ones"/>
</ls_pos>
<ls_pos name="bw_and" id="6557"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="bw_and"/>
</ls_pos>
<ls_pos name="bw_or" id="6564"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="bw_or"/>
</ls_pos>
<ls_pos name="bw_xor" id="6571"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="bw_xor"/>
</ls_pos>
<ls_pos name="bw_not" id="6578"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="bw_not"/>
</ls_pos>
<ls_pos name="lsr" id="6583"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="lsr"/>
</ls_pos>
<ls_pos name="asr" id="6594"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="asr"/>
</ls_pos>
<ls_pos name="lsl" id="6605"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="lsl"/>
</ls_pos>
<ls_pos name="ugt" id="6668"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="ugt"/>
</ls_pos>
<ls_pos name="uge" id="6679"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="uge"/>
</ls_pos>
<ls_pos name="slt" id="6690"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="slt"/>
</ls_pos>
<ls_pos name="sle" id="6701"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="sle"/>
</ls_pos>
<ls_pos name="sgt" id="6712"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="sgt"/>
</ls_pos>
<ls_pos name="sge" id="6723"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="sge"/>
</ls_pos>
<ls_pos name="add" id="6732"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="add"/>
</ls_pos>
<ls_pos name="sub" id="6738"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="sub"/>
</ls_pos>
<ls_pos name="neg" id="6744"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="neg"/>
</ls_pos>
<ls_pos name="mul" id="6748"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="mul"/>
</ls_pos>
<ls_pos name="udiv" id="6754"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="udiv"/>
</ls_pos>
<ls_pos name="urem" id="6760"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="urem"/>
</ls_pos>
<ls_pos name="nth_bv" id="6766"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="nth_bv"/>
</ls_pos>
<ls_pos name="lsr_bv" id="6776"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="lsr_bv"/>
</ls_pos>
<ls_pos name="asr_bv" id="6787"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="asr_bv"/>
</ls_pos>
<ls_pos name="lsl_bv" id="6793"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="lsl_bv"/>
</ls_pos>
<ls_pos name="rotate_right" id="6804"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="rotate_right"/>
</ls_pos>
<ls_pos name="rotate_left" id="6805"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="rotate_left"/>
</ls_pos>
<ls_pos name="eq" id="6876"
ip_theory="BV64">
<ip_library name="bv"/>
<ip_qualid name="eq"/>
</ls_pos>
<ls_pos name="size" id="6891"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="size"/>
</ls_pos>
<ls_pos name="two_power_size" id="6892"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="two_power_size"/>
</ls_pos>
<ls_pos name="nth" id="6896"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="nth"/>
</ls_pos>
<ls_pos name="zero" id="6901"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="ones" id="6904"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="ones"/>
</ls_pos>
<ls_pos name="bw_and" id="6907"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_and"/>
</ls_pos>
<ls_pos name="bw_or" id="6914"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_or"/>
</ls_pos>
<ls_pos name="bw_xor" id="6921"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_xor"/>
</ls_pos>
<ls_pos name="bw_not" id="6928"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_not"/>
</ls_pos>
<ls_pos name="lsr" id="6933"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsr"/>
</ls_pos>
<ls_pos name="asr" id="6944"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="asr"/>
</ls_pos>
<ls_pos name="lsl" id="6955"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsl"/>
</ls_pos>
<ls_pos name="to_int" id="6968"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="to_int"/>
</ls_pos>
<ls_pos name="to_uint" id="6969"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="to_uint"/>
</ls_pos>
<ls_pos name="of_int" id="6970"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="of_int"/>
</ls_pos>
<ls_pos name="uint_in_range" id="6981"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="uint_in_range"/>
</ls_pos>
<ls_pos name="ule" id="7007"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="ule"/>
</ls_pos>
<ls_pos name="ugt" id="7018"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="ugt"/>
</ls_pos>
<ls_pos name="uge" id="7029"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="uge"/>
</ls_pos>
<ls_pos name="slt" id="7040"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="slt"/>
</ls_pos>
<ls_pos name="sle" id="7051"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sle"/>
</ls_pos>
<ls_pos name="sgt" id="7062"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sgt"/>
</ls_pos>
<ls_pos name="sge" id="7073"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sge"/>
</ls_pos>
<ls_pos name="add" id="7082"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="add"/>
</ls_pos>
<ls_pos name="sub" id="7088"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sub"/>
</ls_pos>
<ls_pos name="neg" id="7094"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="neg"/>
</ls_pos>
<ls_pos name="mul" id="7098"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="mul"/>
</ls_pos>
<ls_pos name="udiv" id="7104"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="udiv"/>
</ls_pos>
<ls_pos name="urem" id="7110"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="urem"/>
</ls_pos>
<ls_pos name="nth_bv" id="7116"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="nth_bv"/>
</ls_pos>
<ls_pos name="lsr_bv" id="7126"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsr_bv"/>
</ls_pos>
<ls_pos name="asr_bv" id="7137"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="asr_bv"/>
</ls_pos>
<ls_pos name="lsl_bv" id="7143"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsl_bv"/>
</ls_pos>
<ls_pos name="rotate_right" id="7154"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="rotate_right"/>
</ls_pos>
<ls_pos name="rotate_left" id="7155"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="rotate_left"/>
</ls_pos>
<ls_pos name="eq_sub_bv" id="7175"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq_sub_bv"/>
</ls_pos>
<ls_pos name="eq_sub" id="7196"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq_sub"/>
</ls_pos>
<ls_pos name="eq" id="7226"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq"/>
</ls_pos>
<ls_pos name="size" id="7591"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="size"/>
</ls_pos>
<ls_pos name="two_power_size" id="7592"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="two_power_size"/>
</ls_pos>
<ls_pos name="max_int" id="7593"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="max_int"/>
</ls_pos>
<ls_pos name="nth" id="7596"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="nth"/>
</ls_pos>
<ls_pos name="zero" id="7601"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="ones" id="7604"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="ones"/>
</ls_pos>
<ls_pos name="bw_and" id="7607"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="bw_and"/>
</ls_pos>
<ls_pos name="bw_or" id="7614"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="bw_or"/>
</ls_pos>
<ls_pos name="bw_xor" id="7621"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="bw_xor"/>
</ls_pos>
<ls_pos name="bw_not" id="7628"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="bw_not"/>
</ls_pos>
<ls_pos name="lsr" id="7633"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="lsr"/>
</ls_pos>
<ls_pos name="asr" id="7644"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="asr"/>
</ls_pos>
<ls_pos name="lsl" id="7655"
ip_theory="BV8">
<ip_library name="bv"/>
<ip_qualid name="lsl"/>