Commit 9a8867c7 authored by Clément Fumex's avatar Clément Fumex

update rightmostbittrick example

parent f44d8621
......@@ -3,7 +3,7 @@ module Rmbt
use import ref.Ref
use import bv.BV32
let ghost min_elt (a : t) : t
let ghost rightmost_position_set (a : t) : t
requires { a <> zero }
ensures { ult result (of_int 32) }
ensures { eq_sub_bv a zero zero result }
......@@ -27,7 +27,7 @@ module Rmbt
ensures { eq_sub result zero (!p+1) 32 }
ensures { nth result !p }
=
let ghost p_bv = min_elt x in
let ghost p_bv = rightmost_position_set x in
ghost p := to_uint p_bv;
assert { nth_bv (neg x) p_bv };
let res = bw_and x (neg x) in
......
......@@ -9,57 +9,57 @@
<prover id="6" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" expanded="true">
<theory name="Rmbt" sum="6445b4e19089da0d1885e4a56720b0af" expanded="true">
<goal name="WP_parameter min_elt" expl="VC for min_elt" expanded="true">
<goal name="WP_parameter rightmost_position_set" expl="VC for rightmost_position_set" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter min_elt.1" expl="1. loop invariant init">
<goal name="WP_parameter rightmost_position_set.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.91" steps="183"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter min_elt.2" expl="2. loop invariant preservation">
<goal name="WP_parameter rightmost_position_set.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter min_elt.3" expl="3. loop variant decrease">
<goal name="WP_parameter rightmost_position_set.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="1.25" steps="296"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter min_elt.4" expl="4. postcondition">
<goal name="WP_parameter rightmost_position_set.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.5" expl="5. postcondition">
<goal name="WP_parameter rightmost_position_set.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.6" expl="6. postcondition">
<goal name="WP_parameter rightmost_position_set.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.7" expl="7. postcondition">
<goal name="WP_parameter rightmost_position_set.7" expl="7. postcondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter min_elt.8" expl="8. postcondition">
<goal name="WP_parameter rightmost_position_set.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.9" expl="9. postcondition">
<goal name="WP_parameter rightmost_position_set.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment