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
|
module CreusotContracts_Logic_Resolve_Impl2_Resolve_Interface
type t
predicate resolve (self : t)
end
module CreusotContracts_Logic_Resolve_Impl2_Resolve
type t
predicate resolve (self : t) =
true
end
module CreusotContracts_Logic_Resolve_Resolve_Resolve_Interface
type self
predicate resolve (self : self)
end
module CreusotContracts_Logic_Resolve_Resolve_Resolve
type self
predicate resolve (self : self)
end
module CreusotContracts_Logic_Resolve_Impl2
type t
clone CreusotContracts_Logic_Resolve_Impl2_Resolve as Resolve0 with type t = t
clone CreusotContracts_Logic_Resolve_Resolve_Resolve as Resolve1 with type self = t,
predicate resolve = Resolve0.resolve
end
module Sum_SumFirstN_Interface
use mach.int.Int
use mach.int.UInt32
val sum_first_n [@cfg:stackify] (n : uint32) : uint32
ensures { result = div (n * (n + (1 : uint32))) (2 : uint32) }
end
module Sum_SumFirstN
use mach.int.Int
use mach.int.UInt32
clone CreusotContracts_Logic_Resolve_Impl2_Resolve as Resolve1 with type t = ()
clone CreusotContracts_Logic_Resolve_Impl2_Resolve as Resolve0 with type t = uint32
let cfg sum_first_n [@cfg:stackify] (n : uint32) : uint32
ensures { result = div (n * (n + (1 : uint32))) (2 : uint32) }
=
var _0 : uint32;
var n_1 : uint32;
var sum_2 : uint32;
var i_3 : uint32;
var _4 : ();
var _5 : ();
var _6 : bool;
var _7 : uint32;
var _8 : uint32;
var _9 : uint32;
var _10 : ();
var _11 : ();
var _12 : ();
{
n_1 <- n;
goto BB0
}
BB0 {
sum_2 <- (0 : uint32);
i_3 <- (0 : uint32);
goto BB1
}
BB1 {
(* invariant loop_bound { i_3 < n_1 + (1 : uint32) };
invariant sum_value { sum_2 = div (i_3 * (i_3 + (1 : uint32))) (2 : uint32) };
assume { Resolve0.resolve _7 };
_7 <- i_3;
assume { Resolve0.resolve _8 };
_8 <- n_1;
_6 <- _7 <= _8; *)
switch (_6)
| False -> goto BB3
| _ -> goto BB2
end
}
BB2 {
(* assume { Resolve0.resolve _9 };
_9 <- i_3;
sum_2 <- sum_2 + _9;
i_3 <- i_3 + (1 : uint32);
_5 <- ();
assume { Resolve1.resolve _5 }; *)
goto BB1
}
BB3 {
(* assume { Resolve0.resolve n_1 }; *)
(* assume { Resolve0.resolve i_3 };
_4 <- (); *)
assume { Resolve1.resolve _4 };
(* assume { Resolve0.resolve _0 };
_0 <- sum_2;
assume { Resolve0.resolve sum_2 }; *)
return _0
}
end
|
