blob: 28a9ace76518f48f79a22bc898bda5bf4dcdbfe4 (
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
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [constants] *)
module Constants
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [constants::X0] *)
let x0_fwd : result u32 = Return 0
(** [core::num::u32::{8}::MAX] *)
assume val core_num_u32_max_fwd : result u32
(** [constants::X1] *)
let x1_fwd : result u32 = Return 4294967295
(** [constants::X2] *)
let x2_fwd : result u32 = Return 3
(** [constants::incr] *)
let incr_fwd (n : u32) : result u32 =
begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
(** [constants::X3] *)
let x3_fwd : result u32 =
begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
(** [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_fwd : result (u32 & u32) =
begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
(** [constants::P1] *)
let p1_fwd : result (pair_t u32 u32) =
begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
(** [constants::P2] *)
let p2_fwd : result (u32 & u32) = Return (0, 1)
(** [constants::P3] *)
let p3_fwd : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
(** [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_fwd : result (wrap_t i32) =
begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
(** [constants::unwrap_y] *)
let unwrap_y_fwd : result i32 =
begin match y_fwd with | Fail -> Fail | Return w -> Return w.wrap_val end
(** [constants::YVAL] *)
let yval_fwd : result i32 =
begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
(** [constants::get_z1::Z1] *)
let get_z1_z1_fwd : result i32 = Return 3
(** [constants::get_z1] *)
let get_z1_fwd : result i32 =
begin match get_z1_z1_fwd with | Fail -> Fail | Return i -> Return i end
(** [constants::add] *)
let add_fwd (a : i32) (b : i32) : result i32 =
begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
(** [constants::Q1] *)
let q1_fwd : result i32 = Return 5
(** [constants::Q2] *)
let q2_fwd : result i32 =
begin match q1_fwd with | Fail -> Fail | Return i -> Return i end
(** [constants::Q3] *)
let q3_fwd : result i32 =
begin match q2_fwd with
| Fail -> Fail
| Return i ->
begin match add_fwd i 3 with | Fail -> Fail | Return i0 -> Return i0 end
end
(** [constants::get_z2] *)
let get_z2_fwd : result i32 =
begin match get_z1_fwd with
| Fail -> Fail
| Return i ->
begin match q3_fwd with
| Fail -> Fail
| Return i0 ->
begin match add_fwd i i0 with
| Fail -> Fail
| Return i1 ->
begin match q1_fwd with
| Fail -> Fail
| Return i2 ->
begin match add_fwd i2 i1 with
| Fail -> Fail
| Return i3 -> Return i3
end
end
end
end
end
(** [constants::S1] *)
let s1_fwd : result u32 = Return 6
(** [constants::S2] *)
let s2_fwd : result u32 =
begin match s1_fwd with
| Fail -> Fail
| Return i ->
begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end
end
(** [constants::S3] *)
let s3_fwd : result (pair_t u32 u32) =
begin match p3_fwd with | Fail -> Fail | Return p -> Return p end
(** [constants::S4] *)
let s4_fwd : result (pair_t u32 u32) =
begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
|
