Commit 8761602f authored by Clément Fumex's avatar Clément Fumex

- some modifications to bv.why/mlw :

  + size -> size_bv
  + size_int -> size
  + change two_power_size and max_int definitions
  + add axioms to BVConverter
  + new axiom relating nth and nth_bv
  + some reorganisation
- update coq realisation
- modify in consequence the relevant examples and pull the completed ones out of in_progress
parent 556c7936
......@@ -23,6 +23,8 @@ theory bv.BV_Gen
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_ones
remove prop two_power_size_val
remove prop max_int_val
remove prop eq_sub_equiv
remove prop Extensionality
remove prop Nth_bw_or
......@@ -104,6 +106,11 @@ theory bv.BV8
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
end
theory bv.BVConverter_Gen
remove prop toSmall_to_uint
remove prop toBig_to_uint
end
theory bv.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
......
......@@ -23,7 +23,7 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="b0206e6010f9baba3c77f13cd10417bd" expanded="true">
<theory name="BinarySearchInt32" sum="1532a4c6a55e25e07cb0fa8426dc924c" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
......@@ -33,7 +33,7 @@
<proof prover="5"><result status="valid" time="0.01" steps="75"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="5"><result status="valid" time="0.12" steps="94"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="76"/></proof>
......@@ -54,10 +54,10 @@
<proof prover="5"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="5"><result status="valid" time="0.11" steps="116"/></proof>
<proof prover="5"><result status="valid" time="0.11" steps="117"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="5"><result status="valid" time="0.27" steps="136"/></proof>
<proof prover="5"><result status="valid" time="0.27" steps="138"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="91"/></proof>
......@@ -74,7 +74,7 @@
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="1.36" steps="180"/></proof>
<proof prover="5"><result status="valid" time="1.36" steps="182"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
......@@ -94,7 +94,7 @@
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="1.31" steps="181"/></proof>
<proof prover="5"><result status="valid" time="1.31" steps="183"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="101"/></proof>
......
(* module BitCountSpec_2 *)
(* use import bv.BV32 *)
(* use import int.NumOf *)
(* function count_logic (a : t) : int *)
(* val count (bv:t) : t *)
(* ensures { to_uint result = count__logic bv } *)
(* end *)
module BitCount8bit_fact
use import int.Int
use import int.NumOf
use import mach.bv.BVCheck8
use import bv.BV8
use import ref.Ref
function nth_as_bv (a i : t) : t =
......@@ -95,15 +82,15 @@ module BitCount8bit_fact
=
let x = ref n in
x := sub_check !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55));
x := sub !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55));
let ghost x1 = !x in
x := add_check
x := add
(bw_and !x (of_int 0x33))
(bw_and (lsr_bv !x (of_int 2)) (of_int (0x33)));
let ghost x2 = !x in
x := bw_and (add_check !x (lsr_bv !x (of_int 4))) (of_int 0x0F);
x := bw_and (add !x (lsr_bv !x (of_int 4))) (of_int 0x0F);
prove n x1 x2 !x;
......@@ -115,7 +102,7 @@ module BitCount32bit_fact
use import int.Int
use import int.NumOf
use import mach.bv.BVCheck32
use import bv.BV32
use import ref.Ref
function count_logic (bv:t) : int = numof (nth bv) 0 32
......@@ -260,43 +247,43 @@ module BitCount32bit_fact
=
let x = ref n in
assert { ule (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555)) !x };
(* assert { ule (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555)) !x }; *)
(* x = x - ( (x >> 1) & 0x55555555) *)
x := sub_check !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555));
x := sub !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555));
let ghost x1 = !x in
assert { ule (bw_and !x (of_int 0x33333333))
(of_int 0x33333333) };
assert { ule (bw_and (lsr_bv !x (of_int 2)) (of_int (0x33333333)))
(of_int (0x33333333)) };
(* assert { ule (bw_and !x (of_int 0x33333333)) *)
(* (of_int 0x33333333) }; *)
(* assert { ule (bw_and (lsr_bv !x (of_int 2)) (of_int (0x33333333))) *)
(* (of_int (0x33333333)) }; *)
(* x = (x & 0x33333333) + ((x >> 2) & 0x33333333) *)
x := add_check
x := add
(bw_and !x (of_int 0x33333333))
(bw_and (lsr_bv !x (of_int 2)) (of_int (0x33333333)));
let ghost x2 = !x in
assert { ule !x (of_int 0x6666_6666) };
assert { ule (lsr_bv !x (of_int 4)) (of_int 0x0666_6666) };
(* assert { ule !x (of_int 0x6666_6666) }; *)
(* assert { ule (lsr_bv !x (of_int 4)) (of_int 0x0666_6666) }; *)
(* x = (x + (x >> 4)) & 0x0F0F0F0F *)
x := bw_and (add_check !x (lsr_bv !x (of_int 4))) (of_int 0x0F0F0F0F);
x := bw_and (add !x (lsr_bv !x (of_int 4))) (of_int 0x0F0F0F0F);
let ghost x3 = !x in
assert {ult !x (of_int 0x0F0F0F0F)};
assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0F0F)};
assert {uint_in_range 0x0F0F0F0F /\ uint_in_range 0x000F0F0F};
(* assert {ult !x (of_int 0x0F0F0F0F)}; *)
(* assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0F0F)}; *)
(* assert {uint_in_range 0x0F0F0F0F /\ uint_in_range 0x000F0F0F}; *)
(* x = x + (x >> 8) *)
x := add_check !x (lsr_bv !x (of_int 8));
x := add !x (lsr_bv !x (of_int 8));
let ghost x4 = !x in
assert {ult !x (of_int 0x0F000000)};
assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0000)};
(* assert {ult !x (of_int 0x0F000000)}; *)
(* assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0000)}; *)
(* x = x + (x >> 16) *)
x := add_check !x (lsr_bv !x (of_int 16));
x := add !x (lsr_bv !x (of_int 16));
prove n x1 x2 x3 x4 !x;
......@@ -363,9 +350,9 @@ module AsciiCode
use import BitCount32bit_fact
constant one : t = of_int 1
constant lastbit : t = sub size one
constant lastbit : t = sub size_bv one
(* let lastbit () = (sub_check size one) : t *)
(* let lastbit () = (sub_check size_bv one) : t *)
(** {2 ASCII cheksum }
In the beginning the encoding of an ascii character was done on 8
......@@ -410,7 +397,7 @@ module AsciiCode
requires { bw_and b c = zero }
ensures { count_logic (bw_or b c) = count_logic b + count_logic c }
=
assert { forall i. ult i size ->
assert { forall i. ult i size_bv ->
not (nth_bv b i) \/ not (nth_bv c i) };
assert { forall i. not (nth_bv b (of_int i)) \/ not (nth_bv c (of_int i))
-> not (nth b i) \/ not (nth c i) };
......@@ -474,7 +461,7 @@ module GrayCode
use Hamming
constant one : t = of_int 1
constant lastbit : t = sub size one
constant lastbit : t = sub size_bv one
(** {2 Gray code}
Gray codes are bit-wise representations of integers with the
......@@ -535,7 +522,7 @@ module GrayCode
integer *)
lemma nthBinary: forall b i.
ult i size ->
ult i size_bv ->
nth_bv (fromGray b) i <-> even (count_logic (lsr_bv b i))
(** The last property that we check is that if an integer is even
......
This diff is collapsed.
......@@ -16,22 +16,6 @@ module Bitwalker
use import mach.bv.BV
*)
predicate in_small_range (x:BV32.t) = BV32.ule x (BV32.of_int BV8.max_int)
predicate in_small_range2 (x:BV64.t) = BV64.ule x (BV64.of_int BV32.max_int)
lemma toBig_to_uint: forall x:BV8.t.
BV32.to_uint (C8_32.toBig x) = BV8.to_uint x
lemma toSmall_to_uint: forall x:BV32.t. in_small_range x ->
BV32.to_uint x = BV8.to_uint (C8_32.toSmall x)
lemma toBig_to_uint2: forall x:BV32.t.
BV64.to_uint (C32_64.toBig x) = BV32.to_uint x
lemma toSmall_to_uint2: forall x:BV64.t. in_small_range2 x ->
BV64.to_uint x = BV32.to_uint (C32_64.toSmall x)
function nth8_stream (stream : array BV8.t) (pos : int) : bool =
BV8.nth stream[div pos 8] (7 - mod pos 8)
......
This diff is collapsed.
......@@ -12,7 +12,7 @@ theory Utils
constant one : t = of_int 1
constant two : t = of_int 2
constant lastbit : t = sub size one
constant lastbit : t = sub size_bv one
function max (x y : t) : t = (if ult x y then y else x)
function min (x y : t) : t = (if ult x y then x else y)
......@@ -238,7 +238,7 @@ module Hackers_delight
integer *)
lemma nthBinary: forall b i.
ult i size ->
ult i size_bv ->
nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zero
(** The last property that we check is that if an integer is even
......@@ -342,7 +342,7 @@ module Hackers_delight
(** {6 Shifts and rotates} *)
(** shift right and arithmetic shift right (p.20)*)
lemma SR1: forall x n. ult n size ->
lemma SR1: forall x n. ult n size_bv ->
bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (of_int 31) )) (sub (of_int 31) n))
= asr_bv x n
......
......@@ -6,16 +6,17 @@
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.3" timelimit="70" memlimit="1000"/>
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Utils_Spec" sum="610234791a002b9c10f7c59264163ffb" expanded="true">
<theory name="Utils_Spec" sum="3f0ae9505cd1d20116a2836d82f8ab3d" expanded="true">
<goal name="countZero">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="numOfZero">
<proof prover="0"><result status="valid" time="0.47" steps="236"/></proof>
<proof prover="0"><result status="valid" time="0.47" steps="239"/></proof>
<proof prover="3"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="countStep">
......@@ -68,7 +69,7 @@
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter hamming_spec.1" expl="1. assertion" expanded="true">
<proof prover="0"><result status="valid" time="2.43" steps="838"/></proof>
<proof prover="0"><result status="valid" time="2.43" steps="944"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter hamming_spec.2" expl="2. postcondition">
......@@ -82,29 +83,20 @@
</goal>
<goal name="separation">
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="2"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="WP_parameter numof_or" expl="VC for numof_or">
<proof prover="1"><result status="valid" time="0.53"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter triangleInequalityInt.1.1" expl="1. VC for triangleInequalityInt">
<proof prover="0"><result status="valid" time="0.04" steps="74"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.1.2" expl="2. VC for triangleInequalityInt">
<proof prover="2"><result status="valid" time="0.47"/></proof>
</goal>
</transf>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion" expanded="true">
<proof prover="2" timelimit="70"><result status="valid" time="0.77"/></proof>
<proof prover="4"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition">
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
......@@ -115,14 +107,14 @@
<proof prover="1" timelimit="15"><result status="valid" time="2.35"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="e816aa8b35a31288aafa204946296549" expanded="true">
<theory name="Hackers_delight" sum="c1471f5279d8e24b7242c18b19325bf4" expanded="true">
<goal name="WP_parameter ascii" expl="VC for ascii">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="asciiProp">
<proof prover="1" timelimit="20"><result status="valid" time="0.66"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="2.11"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="2.72"/></proof>
</goal>
<goal name="iso">
<proof prover="1"><result status="valid" time="0.43"/></proof>
......
module BitInterval
use import int.Int
use import bv.BV32
predicate interval_eq_bv (a b:t) (i n:t) =
let mask = lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i in
bw_and b mask = bw_and a mask
predicate interval_eq (a b:t) (i n:int) =
forall j. i <= j < i + n -> nth a j = nth b j
let lemma interval_eq_is_equ (a b i n : t)
requires {ult i size /\ ule n size /\ ule (add i n) size}
ensures { interval_eq a b (to_uint i) (to_uint n)
<-> interval_eq_bv a b i n }
=
(* let tmp = lsl_bv (of_int 1) n in *)
(* assert { ult n size -> nth_bv tmp n }; *)
(* assert { n = size -> tmp = zero }; *)
(* assert { forall i. i <> n -> not (nth_bv tmp i) }; *)
(* let tmp2 = sub tmp (of_int 1) in *)
(* assert { forall i. ult i n -> nth_bv tmp2 i }; *)
(* assert { forall i. uge i n /\ ult i size -> not (nth_bv tmp2 i) }; *)
(* let mask = lsl_bv tmp2 i in *)
let mask =
abstract
ensures { forall j. ule i j /\ ult j (add i n) -> nth_bv result j }
ensures { forall j. ult j i -> not (nth_bv result j) }
ensures { forall j. ule (add i n) j -> not (nth_bv result j) }
lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i
end
in
assert { to_uint i + to_uint n = to_uint (add i n) };
assert { forall j. to_uint i <= j /\ j < (to_uint i + to_uint n) -> j = to_uint (of_int j) && nth mask j };
assert { forall j. 0 <= j < to_uint i -> j = to_uint (of_int j) && not (nth mask j) };
assert { forall j. (to_uint i + to_uint n) <= j < size_int -> j = to_uint (of_int j) && not (nth mask j) };
assert { interval_eq a b (to_uint i) (to_uint n)
<-> bw_and b mask = bw_and a mask };
()
use bv.BV64
use bv.BVConverter_32_64 as C32_64
predicate interval_eq_bv_64 (a b:BV64.t) (i n:BV64.t) =
let mask = BV64.lsr_bv (BV64.sub (BV64.lsl_bv (BV64.of_int 1) n) (BV64.of_int 1)) i in
BV64.bw_and b mask = BV64.bw_and a mask
predicate interval_eq_64 (a b:BV64.t) (i n:int) =
forall j. i <= j < i + n -> BV64.nth a j = BV64.nth b j
lemma interval_eq_is_equ_64 : forall a b i n.
BV64.ule i BV64.size -> BV64.ule (BV64.add i n) BV64.size ->
interval_eq_64 a b (BV64.to_uint i) (BV64.to_uint n)
<-> interval_eq_bv_64 a b i n
function maxvalue (len : BV32.t) : BV64.t = BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)
lemma nth_ult:
forall x:BV64.t, len:BV32.t. BV32.to_uint len < 64 ->
(BV64.to_uint x < BV64.to_uint (maxvalue len)
(* <-> (forall j:int. BV32.to_uint len <= j < 64 -> BV64.nth x j = False)) *)
<-> interval_eq_bv_64 BV64.zero x (C32_64.toBig len) (BV64.sub (BV64.of_int 64) (C32_64.toBig len)))
(* predicate bits_interval_is_zero_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) = interval_eq_bv a zero i n *)
(* predicate bits_interval_is_one_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) = interval_eq_bv a ones i n *)
(* predicate bits_interval_is_zero (a:BV32.t) (i : int) (n : int) = interval_eq a zero i n *)
(* predicate bits_interval_is_one (a:BV32.t) (i : int) (n : int) = interval_eq a ones i n *)
(* lemma bits_interval_is_zero_equ : forall a i n. *)
(* ule i (of_int 32) -> ule (add i n) (of_int 32) -> *)
(* bits_interval_is_zero a (to_uint i) (to_uint n) <-> bits_interval_is_zero_bv a i n *)
(* lemma bits_interval_is_one_equ : forall a i n. *)
(* ule i (of_int 32) /\ ule n (sub (of_int 32) i) -> *)
(* bits_interval_is_one a (to_uint i) (to_uint n) <-> bits_interval_is_one_bv a i n *)
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="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitinterval.mlw" expanded="true">
<theory name="BitInterval" sum="18200d09e060eeb168b77260b8d7745e" expanded="true">
<goal name="WP_parameter interval_eq_is_equ" expl="VC for interval_eq_is_equ" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter interval_eq_is_equ.1" expl="1. VC for interval_eq_is_equ">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.2" expl="2. VC for interval_eq_is_equ">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.3" expl="3. VC for interval_eq_is_equ">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.4" expl="4. assertion">
<proof prover="0" obsolete="true"><result status="valid" time="0.74" steps="223"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.56"/></proof>
<proof prover="2"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.5" expl="5. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter interval_eq_is_equ.5.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.38" steps="350"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.5.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="129"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter interval_eq_is_equ.6" expl="6. assertion">
<proof prover="0"><result status="valid" time="1.96" steps="591"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="4.99"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.06"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="2.97" steps="1110"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.04"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.8" expl="8. assertion" expanded="true">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="4.79"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.03"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="4.99"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter interval_eq_is_equ.8.1" expl="1. assertion" expanded="true">
<proof prover="0"><result status="timeout" time="3.57"/></proof>
<proof prover="1"><result status="unknown" time="5.72"/></proof>
<proof prover="2"><result status="unknown" time="0.03"/></proof>
<proof prover="3"><result status="timeout" time="4.95"/></proof>
</goal>
<goal name="WP_parameter interval_eq_is_equ.8.2" expl="2. assertion" expanded="true">
<proof prover="0"><result status="timeout" time="3.42"/></proof>
<proof prover="1"><result status="timeout" time="6.65"/></proof>
<proof prover="2"><result status="unknown" time="0.03"/></proof>
<proof prover="3"><result status="timeout" time="4.98"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter interval_eq_is_equ.9" expl="9. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="4.97"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="unknown" time="0.04"/></proof>
<proof prover="3"><result status="timeout" time="4.98"/></proof>
</goal>
</transf>
</goal>
<goal name="interval_eq_is_equ_64" expanded="true">
</goal>
<goal name="nth_ult" expanded="true">
</goal>
</theory>
</file>
</why3session>
This diff is collapsed.
This diff is collapsed.
module Delight
(*
use import int.Int
use import int.Power
use import bv.BV32
(* use import mach.int.Int32 *)
use import int.EuclideanDivision
type bitVec32 = BV32.t
constant two : bitVec32 = BV32.of_int 2
constant n31 : bitVec32 = BV32.of_int 31
constant n32 : bitVec32 = BV32.of_int 32
constant twoP31 : bitVec32 = BV32.of_int 0x8000_0000
function to_int bitVec32 : int
(* function to_int32 bitVec32 : int32 *)
function from_int int : bitVec32
(* function from_int32 int32 : bitVec32 *)
axiom to_int_1 :
forall i. to_int( of_int i ) = mod i 0x1_0000_0000
(* forall i. 0 <= i < 0x1_0000_0000 -> to_int( of_int i ) = i *)
axiom to_int_2 :
forall i. of_int( to_int i ) = i
(* axiom to_int32_1 : *)
(* forall i. to_int32( of_int32 i ) = i *)
(* axiom to_int32_2 : *)
(* forall i. of_int32( to_int32 i ) = i *)
(* axiom to_int_local : *)
(* forall b. to_int b = BV32.to_int b *)
axiom of_int_local :
forall i. of_int i = BV32.of_int i
(* axiom conversion : *)
(* forall x. to_int x = bitVec32o_int (to_bv x) *)
(* axiom to_int twoP31 = 0x8000_0000 *)
(* axiom to_int two = 2 *)
(* axiom to_int n31 = 31 *)
(* axiom to_int n32 = 32 *)
axiom le_to_int :
forall x y. sle x y <-> (to_int x) <= (to_int y)
axiom lt_to_int :
forall x y. slt x y <-> (to_int x) < (to_int y)
axiom mul_to_int :
forall x y. mul x y = of_int( (to_int x) * (to_int y) )
axiom mul_of_int :
forall i j. mul (of_int i) (of_int j) = of_int( i * j )
(* lemma mod_pow_2 : *)
(* forall x y. slt zero y -> slt y n32 -> *)
(* mod (to_int x) (power 2 (to_int y)) *)
(* = to_int (bw_and x (sub (lsl_bv one y) one)) *)
(* axiom lsl_to_int : *)
(* val lsl_32 (x : int32 ) ( n : int32 ) : int32 *)
(* requires{ 0 <= to_int n < 32 } *)
(* ensures{ to_bv result = BV32.lsl_bv ( to_bv x ) ( to_bv n ) } *)
(* ensures{ 0 <= to_int x -> to_int x * ( power 2 ( to_int n ) ) < twoP31 *)
(* -> to_int result = to_int x * ( power 2 ( to_int n ) ) } *)
(* val lsr_32 (x : int32 ) ( n : int32 ) : int32 *)
(* requires{ 0 <= to_int n < 32 } *)
(* ensures{ to_bv result = BV32.lsr_bv ( to_bv x ) ( to_bv n *)
(* ) } *)
(* ensures{ 0 <= to_int x -> to_int result = div ( to_int x ) ( power 2 ( to_int n ) ) } *)
let test1 ( x : bitVec32 ) : bitVec32
requires{ 0 <= to_int x < 1000 }
ensures{ to_int result = 4 * to_int x }
ensures{ bw_and result ( of_int 0b11 ) = zero }
=
assert{ power 2 2 = 4 };
assert{ lsl_bv x two = mul (of_int( 4 )) x };
assert{ mul (of_int( 4 )) x = of_int( 4 * to_int x ) };
assert{ lsl_bv x two = of_int( 4 * to_int x ) };
lsl_bv x two
(* val bw_and_32 ( x : int32 ) ( y : int32 ) : int32 *)
(* ensures { to_bv result = BV32.bw_and ( to_bv x ) ( to_bv y ) } *)
(* (\* ensures { to_int result = bitVec32o_int ( to_bv result ) } *\) *)
(* val sub_32 ( x : int32 ) ( y : int32 ) : int32 *)
(* ensures { to_bv result = BV32.sub ( to_bv x ) ( to_bv y ) } *)
(* ensures { - 0x8000_0000 <= to_int x - to_int y < twoP31 *)
(* -> to_int result = to_int x - to_int y } *)
(* lemma l : forall y. BV32.slt BV32.zero y -> BV32.slt (BV32.sub y (BV32.of_int 1) ) y *)
(* let f (x y:int32) (ghost k:int32) : int32 *)
(* requires { le zero k } *)
(* requires { lt k n31 } *)
(* requires { to_bv y = BV32.lsl_bv (BV32.of_int 1) (to_bv k) } *)
(* requires { to_int y = power 2 (to_int k) } *)
(* ensures { le zero result } *)
(* ensures { lt result y } *)
(* ensures { to_int result = mod (to_int x) (to_int y) } *)
(* = *)
(* bw_and_32 x ( sub_32 y one ) *)
(* use import ref.Ref *)
(* (\* Returns the digit index of the most significant (non-zero) digit of Number. (from N622-004) *\) *)
(* let get_MSD ( number : int32 ) : int *)
(* requires { not( eq number zero ) } *)
(* ensures { result <> 0 } *)
(* ensures { result < 31 } *)
(* ensures { forall i. result < i < 31 -> BV32.nth ( to_bv number ) i = False } *)
(* = *)
(* let digit_index = ref 0 in *)
(* for i = 0 to 31 do *)
(* invariant { !digit_index <> 0 \/ exists j. i < j /\ j < 31 /\ nth ( to_bv number ) j = True } *)
(* invariant { !digit_index < i -> ( forall j. !digit_index < j /\ j < 31 -> nth ( to_bv number ) j = False ) } *)
(* if( BV32.nth ( to_bv number ) i = True ) *)
(* then *)
(* digit_index := i *)
(* done; *)
(* !digit_index *)
*)
end
<?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="Coq" version="8.4pl5" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5-prerelease" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../hacker.mlw" expanded="true">
<theory name="Delight" sum="9fbbb348fb56261b5035ef172b5233be" expanded="true">
<goal name="WP_parameter test1" expl="VC for test1" expanded="true">
<proof prover="0" obsolete="true"><unedited/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="4.98"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="4.99"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter test1.1" expl="1. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.18"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter test1.2" expl="2. assertion" expanded="true">
<proof prover="1"><result status="valid" time="1.00"/></proof>
</goal>
<goal name="WP_parameter test1.3" expl="3. assertion" expanded="true">
<proof prover="3"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter test1.4" expl="4. assertion" expanded="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter test1.5" expl="5. postcondition" expanded="true">
<proof prover="3"><result status="valid" time="0.43" steps="30"/></proof>
</goal>
<goal name="WP_parameter test1.6" expl="6. postcondition" expanded="true">
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="timeout" time="4.98"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="4.98"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -7,14 +7,14 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="2f88fb831f7ca34916a60c0d40459d0a" expanded="true">
<theory name="TestBV" sum="e016325049a7116c37a2cb173b273bf5" expanded="true">
<goal name="g1">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="f1">
<proof prover="0"><result status="timeout" time="5.01"/></proof>