hacker.mlw 3.89 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3

module Delight

Clément Fumex's avatar
Clément Fumex committed
4
5
6
7
  use import int.Int
  use import int.Power
  use import bv.BV32
  (* use import mach.int.Int32 *)
MARCHE Claude's avatar
MARCHE Claude committed
8
9
  use import int.EuclideanDivision

Clément Fumex's avatar
Clément Fumex committed
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
  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
  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 }
  =
  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 ) } *)
    
  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 }
MARCHE Claude's avatar
MARCHE Claude committed
102
    ensures { to_int result = mod (to_int x) (to_int y) } 
Clément Fumex's avatar
Clément Fumex committed
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
  = 
    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
MARCHE Claude's avatar
MARCHE Claude committed
124
125

end