1
2
3
4
5
6
7
8
9
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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
type T = bv4;
function {:bvbuiltin "bvult"} bvlt(p1: T, p2: T) : bool; // unsigned less than
function {:bvbuiltin "bvxor"} xorT(p1: T, p2: T) : T;
function {:bvbuiltin "bvadd"} bvadd(p1: T, p2: T) : T;
procedure bar({:visible} v: T)
returns ({:hidden} h: T)
ensures true;
{
h := v;
}
procedure foo0({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
returns ({:visible} r1: bool, {:visible} r2: bool,
{:visible} s1: T, {:visible} s2: T, {:visible} s3: T, {:visible} s4: T)
ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1));
{
var {:hidden} t1, t2: T;
r1 := bvlt(x1, y1);
havoc s1;
havoc s2;
s3 := xorT(x1, s1);
s4 := xorT(y1, s2);
t1 := xorT(s1, s3);
t2 := xorT(s2, s4);
r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
}
procedure foo1({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
returns ({:visible} r1: bool, {:visible} r2: bool,
{:visible} s1: T, {:visible} s2: T, {:hidden} s3: T, {:hidden} s4: T)
ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1));
{
var {:hidden} t1, t2: T;
r1 := bvlt(x1, y1);
havoc s1;
havoc s2;
s3 := xorT(x1, s1);
s4 := xorT(y1, s2);
t1 := xorT(s1, s3);
t2 := xorT(s2, s4);
r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
}
procedure foo2({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
returns ({:visible} r1: bool, {:visible} r2: bool,
{:visible} s1: T, {:visible} s2: T)
ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1));
{
var {:hidden} t1, t2: T;
var {:hidden} s3, s4: T;
r1 := bvlt(x1, y1);
havoc s1;
havoc s2;
s3 := xorT(x1, s1);
s4 := xorT(y1, s2);
t1 := xorT(s1, s3);
t2 := xorT(s2, s4);
r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
}
procedure foo3({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
returns ({:visible} r1: bool, {:visible} r2: bool,
{:visible} s1: T, {:visible} s2: T, {:hidden} s3: T, {:hidden} s4: T)
ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1)) && (s4 == xorT(y1,s2)) && (s3 == xorT(x1, s1));
{
var {:hidden} t1, t2: T;
r1 := bvlt(x1, y1);
havoc s1;
havoc s2;
s3 := xorT(x1, s1);
s4 := xorT(y1, s2);
t1 := xorT(s1, s3);
t2 := xorT(s2, s4);
r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
}
procedure bid({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
returns ({:visible} r: bool)
ensures r == bvlt(bvadd(x1,x2), bvadd(y1,y2));
{
var {:hidden} r1, r2: bool;
var {:hidden} s1, s2, s3, s4: T;
call r1, r2, s1, s2, s3, s4 := foo1(x1, x2, y1, y2);
r := r2;
}
|
