Commit 700f4deb authored by Clément Fumex's avatar Clément Fumex

example hacker continued

parent f1c55bac
......@@ -7,119 +7,127 @@ module Delight
(* use import mach.int.Int32 *)
use import int.EuclideanDivision
type int32
function to_int int32 : int
function to_bv int32 : BV32.t
axiom conversion :
forall x. to_int x = BV32.to_int (to_bv x)
constant two_p31 : int = 0x8000_0000
constant zero : int32
axiom value_zero : to_int zero = 0
axiom bv_zero : to_bv zero = BV32.of_int 0
constant one : int32
axiom value_one : to_int one = 1
axiom bv_one : to_bv one = BV32.of_int 1
constant two : int32
axiom value_two : to_int two = 2
axiom bv_two : to_bv two = BV32.of_int 2
constant n31 : int32
axiom value_n31 : to_int n31 = 31
axiom bv_n31 : to_bv n31 = BV32.of_int 31
constant n32 : int32
axiom value_n32 : to_int n32 = 32
axiom bv_n32 : to_bv n32 = BV32.of_int 32
predicate eq int32 int32
axiom int32_eq_fbv:
forall x y. ( to_bv x ) = ( to_bv y ) <-> eq x y
axiom int32_eq_fint:
forall x y. ( to_int x ) = ( to_int y ) <-> eq x y
predicate le int32 int32
axiom int32_le_fbv :
forall x y. BV32.sle (to_bv x) (to_bv y) <-> le x y
axiom int32_le_fint :
forall x y. (to_int x) <= (to_int y) <-> le x y
predicate lt int32 int32
axiom int32_lt_fbv :
forall x y. BV32.slt (to_bv x) (to_bv y) <-> lt x y
axiom int32_lt_fint :
forall x y. (to_int x) < (to_int y) <-> lt x y
lemma mod_pow_2 :
forall x y. le zero y -> lt y n32 ->
mod (to_int x) (power 2 (to_int y))
= BV32.to_int (BV32.bw_and (to_bv x)
(BV32.sub (BV32.lsl_bv BV32.one (to_bv y))
BV32.one))
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 ) ) < two_p31
-> 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 : int32 ) : int32
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 ( to_bv result ) ( BV32.of_int 0b11 ) = BV32.zero }
ensures{ to_int result = 4 * to_int x }
ensures{ bw_and result ( of_int 0b11 ) = zero }
=
assert{ power 2 2 = 4 };
lsl_32 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 = BV32.to_int ( to_bv result ) } *)
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 < two_p31
-> 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
(* 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
(* (\* 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="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../hacker.mlw" expanded="true">
<theory name="Delight" sum="39b2297cf9dbc5ceed65a34352e42749" expanded="true">
<goal name="mod_pow_2" expanded="true">
<proof prover="1" obsolete="true"><result status="timeout" time="4.99"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.03"/></proof>
</goal>
<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="2" 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" obsolete="true"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter test1.2" expl="2. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="WP_parameter test1.3" expl="3. assertion" expanded="true">
<proof prover="1"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter test1.4" expl="4. assertion" expanded="true">
<proof prover="1" obsolete="true"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter test1.5" expl="5. postcondition" expanded="true">
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="21"/></proof>
</goal>
<goal name="WP_parameter test1.6" expl="6. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="4.98"/></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