Commit 8a3775ad authored by Clément Fumex's avatar Clément Fumex

add rightmostbittrick example

parent eda3dfb6
module Rmbt
use import int.Int
use import ref.Ref
use import bv.BV32
let ghost min_elt (a : t) : t
requires { a <> zero }
ensures { ult result (of_int 32) }
ensures { eq_sub_bv a zero zero result }
ensures { nth_bv a result }
=
let i = ref zero in
while ult !i (of_int 32) && not (nth_bv a !i) do
variant {32 - to_uint !i}
invariant {eq_sub_bv a zero zero !i}
i := add !i (of_int 1)
done;
!i
let rightmost_bit_trick (x: t) (ghost p : ref int) : t
requires { x <> zero }
writes { p }
ensures { 0 <= !p < 32 }
ensures { eq_sub x zero 0 !p }
ensures { nth x !p }
ensures { eq_sub result zero 0 !p }
ensures { eq_sub result zero (!p+1) 32 }
ensures { nth result !p }
=
let ghost p_bv = min_elt x in
ghost p := to_uint p_bv;
assert { nth_bv (neg x) p_bv };
let res = bw_and x (neg x) in
assert {eq_sub_bv res zero (add p_bv (of_int 1)) (sub (of_int 31) p_bv )};
res
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="25" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="25" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="25" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="25" memlimit="1000"/>
<prover id="4" name="CVC4_nobv" version="1.4" timelimit="5" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" expanded="true">
<theory name="Rmbt" sum="22df8c7ca2050e5b953f124af6c44263" expanded="true">
<goal name="WP_parameter min_elt" expl="VC for min_elt">
<transf name="split_goal_wp">
<goal name="WP_parameter min_elt.1" expl="1. loop invariant init">
<proof prover="0"><result status="timeout" time="25.03"/></proof>
<proof prover="1"><result status="valid" time="0.21"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter min_elt.2" expl="2. loop invariant preservation">
<proof prover="0"><result status="timeout" time="25.02"/></proof>
<proof prover="1"><result status="valid" time="1.64"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter min_elt.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="1.44" steps="355"/></proof>
<proof prover="1"><result status="valid" time="0.55"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="timeout" time="24.98"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter min_elt.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter min_elt.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter min_elt.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter min_elt.7" expl="7. postcondition">
<proof prover="0"><result status="timeout" time="25.00"/></proof>
<proof prover="1"><result status="unknown" time="1.31"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="timeout" time="5.99"/></proof>
</goal>
<goal name="WP_parameter min_elt.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="72"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter min_elt.9" expl="9. postcondition">
<proof prover="0"><result status="timeout" time="25.02"/></proof>
<proof prover="1"><result status="unknown" time="1.43"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="timeout" time="5.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter rightmost_bit_trick.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.2" expl="2. assertion">
<proof prover="0"><result status="timeout" time="25.02"/></proof>
<proof prover="1"><result status="unknown" time="11.22"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="timeout" time="5.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.3" expl="3. assertion">
<proof prover="0"><result status="timeout" time="25.02"/></proof>
<proof prover="1"><result status="timeout" time="24.98"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="4"><result status="timeout" time="5.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.20" steps="140"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="timeout" time="25.00"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.5" expl="5. postcondition">
<proof prover="0" timelimit="45"><result status="timeout" time="45.04"/></proof>
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="timeout" time="24.92"/></proof>
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="80"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="timeout" time="24.86"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.7" expl="7. postcondition">
<proof prover="0" timelimit="45"><result status="timeout" time="45.05"/></proof>
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="2"><result status="unknown" time="0.07"/></proof>
<proof prover="3"><result status="timeout" time="24.96"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.8" expl="8. postcondition" expanded="true">
<proof prover="0" timelimit="45"><result status="timeout" time="45.05"/></proof>
<proof prover="1"><result status="valid" time="0.89"/></proof>
<proof prover="2"><result status="unknown" time="0.07"/></proof>
<proof prover="3"><result status="timeout" time="24.97"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.9" expl="9. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.15" steps="177"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
<proof prover="2"><result status="unknown" time="0.07"/></proof>
<proof prover="3"><result status="timeout" time="25.01"/></proof>
<proof prover="4"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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