blob: a06582062554c85bf873e79932fa4546027c01da (
plain)
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
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [constants] *)
module Constants
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [constants::X0] *)
let x0_body : result u32 = Return 0
let x0_c : u32 = eval_global x0_body
(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
(** [constants::X1] *)
let x1_body : result u32 = Return core_num_u32_max_c
let x1_c : u32 = eval_global x1_body
(** [constants::X2] *)
let x2_body : result u32 = Return 3
let x2_c : u32 = eval_global x2_body
(** [constants::incr] *)
let incr_fwd (n : u32) : result u32 =
begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end
(** [constants::X3] *)
let x3_body : result u32 =
begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end
let x3_c : u32 = eval_global x3_body
(** [constants::mk_pair0] *)
let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
(** [constants::Pair] *)
type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
(** [constants::mk_pair1] *)
let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
Return (Mkpair_t x y)
(** [constants::P0] *)
let p0_body : result (u32 & u32) =
begin match mk_pair0_fwd 0 1 with
| Fail e -> Fail e
| Return p -> Return p
end
let p0_c : (u32 & u32) = eval_global p0_body
(** [constants::P1] *)
let p1_body : result (pair_t u32 u32) =
begin match mk_pair1_fwd 0 1 with
| Fail e -> Fail e
| Return p -> Return p
end
let p1_c : pair_t u32 u32 = eval_global p1_body
(** [constants::P2] *)
let p2_body : result (u32 & u32) = Return (0, 1)
let p2_c : (u32 & u32) = eval_global p2_body
(** [constants::P3] *)
let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
let p3_c : pair_t u32 u32 = eval_global p3_body
(** [constants::Wrap] *)
type wrap_t (t : Type0) = { wrap_val : t; }
(** [constants::Wrap::{0}::new] *)
let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
Return (Mkwrap_t val0)
(** [constants::Y] *)
let y_body : result (wrap_t i32) =
begin match wrap_new_fwd i32 2 with
| Fail e -> Fail e
| Return w -> Return w
end
let y_c : wrap_t i32 = eval_global y_body
(** [constants::unwrap_y] *)
let unwrap_y_fwd : result i32 = Return y_c.wrap_val
(** [constants::YVAL] *)
let yval_body : result i32 =
begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end
let yval_c : i32 = eval_global yval_body
(** [constants::get_z1::Z1] *)
let get_z1_z1_body : result i32 = Return 3
let get_z1_z1_c : i32 = eval_global get_z1_z1_body
(** [constants::get_z1] *)
let get_z1_fwd : result i32 = Return get_z1_z1_c
(** [constants::add] *)
let add_fwd (a : i32) (b : i32) : result i32 =
begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end
(** [constants::Q1] *)
let q1_body : result i32 = Return 5
let q1_c : i32 = eval_global q1_body
(** [constants::Q2] *)
let q2_body : result i32 = Return q1_c
let q2_c : i32 = eval_global q2_body
(** [constants::Q3] *)
let q3_body : result i32 =
begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end
let q3_c : i32 = eval_global q3_body
(** [constants::get_z2] *)
let get_z2_fwd : result i32 =
begin match get_z1_fwd with
| Fail e -> Fail e
| Return i ->
begin match add_fwd i q3_c with
| Fail e -> Fail e
| Return i0 ->
begin match add_fwd q1_c i0 with
| Fail e -> Fail e
| Return i1 -> Return i1
end
end
end
(** [constants::S1] *)
let s1_body : result u32 = Return 6
let s1_c : u32 = eval_global s1_body
(** [constants::S2] *)
let s2_body : result u32 =
begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end
let s2_c : u32 = eval_global s2_body
(** [constants::S3] *)
let s3_body : result (pair_t u32 u32) = Return p3_c
let s3_c : pair_t u32 u32 = eval_global s3_body
(** [constants::S4] *)
let s4_body : result (pair_t u32 u32) =
begin match mk_pair1_fwd 7 8 with
| Fail e -> Fail e
| Return p -> Return p
end
let s4_c : pair_t u32 u32 = eval_global s4_body
|
