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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [demo] *)
module Demo
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [demo::choose]: forward function
Source: 'src/demo.rs', lines 5:0-5:70 *)
let choose (t : Type0) (b : bool) (x : t) (y : t) : result t =
if b then Return x else Return y
(** [demo::choose]: backward function 0
Source: 'src/demo.rs', lines 5:0-5:70 *)
let choose_back
(t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
if b then Return (ret, y) else Return (x, ret)
(** [demo::mul2_add1]: forward function
Source: 'src/demo.rs', lines 13:0-13:31 *)
let mul2_add1 (x : u32) : result u32 =
let* i = u32_add x x in u32_add i 1
(** [demo::use_mul2_add1]: forward function
Source: 'src/demo.rs', lines 17:0-17:43 *)
let use_mul2_add1 (x : u32) (y : u32) : result u32 =
let* i = mul2_add1 x in u32_add i y
(** [demo::incr]: merged forward/backward function
(there is a single backward function, and the forward function returns ())
Source: 'src/demo.rs', lines 21:0-21:31 *)
let incr (x : u32) : result u32 =
u32_add x 1
(** [demo::CList]
Source: 'src/demo.rs', lines 27:0-27:17 *)
type cList_t (t : Type0) =
| CList_CCons : t -> cList_t t -> cList_t t
| CList_CNil : cList_t t
(** [demo::list_nth]: forward function
Source: 'src/demo.rs', lines 32:0-32:56 *)
let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0 then Return x else let* i1 = u32_sub i 1 in list_nth t n1 tl i1
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut]: forward function
Source: 'src/demo.rs', lines 47:0-47:68 *)
let rec list_nth_mut
(t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0
then Return x
else let* i1 = u32_sub i 1 in list_nth_mut t n1 tl i1
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut]: backward function 0
Source: 'src/demo.rs', lines 47:0-47:68 *)
let rec list_nth_mut_back
(t : Type0) (n : nat) (l : cList_t t) (i : u32) (ret : t) :
result (cList_t t)
=
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0
then Return (CList_CCons ret tl)
else
let* i1 = u32_sub i 1 in
let* tl1 = list_nth_mut_back t n1 tl i1 ret in
Return (CList_CCons x tl1)
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut1]: loop 0: forward function
Source: 'src/demo.rs', lines 62:0-71:1 *)
let rec list_nth_mut1_loop
(t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0
then Return x
else let* i1 = u32_sub i 1 in list_nth_mut1_loop t n1 tl i1
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut1]: forward function
Source: 'src/demo.rs', lines 62:0-62:77 *)
let list_nth_mut1 (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
list_nth_mut1_loop t n l i
(** [demo::list_nth_mut1]: loop 0: backward function 0
Source: 'src/demo.rs', lines 62:0-71:1 *)
let rec list_nth_mut1_loop_back
(t : Type0) (n : nat) (l : cList_t t) (i : u32) (ret : t) :
result (cList_t t)
=
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
begin match l with
| CList_CCons x tl ->
if i = 0
then Return (CList_CCons ret tl)
else
let* i1 = u32_sub i 1 in
let* tl1 = list_nth_mut1_loop_back t n1 tl i1 ret in
Return (CList_CCons x tl1)
| CList_CNil -> Fail Failure
end
(** [demo::list_nth_mut1]: backward function 0
Source: 'src/demo.rs', lines 62:0-62:77 *)
let list_nth_mut1_back
(t : Type0) (n : nat) (l : cList_t t) (i : u32) (ret : t) :
result (cList_t t)
=
list_nth_mut1_loop_back t n l i ret
(** [demo::i32_id]: forward function
Source: 'src/demo.rs', lines 73:0-73:28 *)
let rec i32_id (n : nat) (i : i32) : result i32 =
if is_zero n
then Fail OutOfFuel
else
let n1 = decrease n in
if i = 0
then Return 0
else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1
(** Trait declaration: [demo::Counter]
Source: 'src/demo.rs', lines 83:0-83:17 *)
noeq type counter_t (self : Type0) = {
incr : self -> result usize;
incr_back : self -> result self;
}
(** [demo::{usize}::incr]: forward function
Source: 'src/demo.rs', lines 88:4-88:31 *)
let usize_incr (self : usize) : result usize =
let* _ = usize_add self 1 in Return self
(** [demo::{usize}::incr]: backward function 0
Source: 'src/demo.rs', lines 88:4-88:31 *)
let usize_incr_back (self : usize) : result usize =
usize_add self 1
(** Trait implementation: [demo::{usize}]
Source: 'src/demo.rs', lines 87:0-87:22 *)
let demo_CounterUsizeInst : counter_t usize = {
incr = usize_incr;
incr_back = usize_incr_back;
}
(** [demo::use_counter]: forward function
Source: 'src/demo.rs', lines 95:0-95:59 *)
let use_counter
(t : Type0) (counterTInst : counter_t t) (cnt : t) : result usize =
counterTInst.incr cnt
(** [demo::use_counter]: backward function 0
Source: 'src/demo.rs', lines 95:0-95:59 *)
let use_counter_back
(t : Type0) (counterTInst : counter_t t) (cnt : t) : result t =
counterTInst.incr_back cnt
|
