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
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [constants] *)
module Constants
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [constants::X0]
Source: 'tests/src/constants.rs', lines 7:0-7:17 *)
let x0_body : result u32 = Ok 0
let x0 : u32 = eval_global x0_body
(** [constants::X1]
Source: 'tests/src/constants.rs', lines 9:0-9:17 *)
let x1_body : result u32 = Ok core_u32_max
let x1 : u32 = eval_global x1_body
(** [constants::X2]
Source: 'tests/src/constants.rs', lines 12:0-12:17 *)
let x2_body : result u32 = Ok 3
let x2 : u32 = eval_global x2_body
(** [constants::incr]:
Source: 'tests/src/constants.rs', lines 19:0-19:32 *)
let incr (n : u32) : result u32 =
u32_add n 1
(** [constants::X3]
Source: 'tests/src/constants.rs', lines 17:0-17:17 *)
let x3_body : result u32 = incr 32
let x3 : u32 = eval_global x3_body
(** [constants::mk_pair0]:
Source: 'tests/src/constants.rs', lines 25:0-25:51 *)
let mk_pair0 (x : u32) (y1 : u32) : result (u32 & u32) =
Ok (x, y1)
(** [constants::Pair]
Source: 'tests/src/constants.rs', lines 38:0-38:23 *)
type pair_t (t1 t2 : Type0) = { x : t1; y : t2; }
(** [constants::mk_pair1]:
Source: 'tests/src/constants.rs', lines 29:0-29:55 *)
let mk_pair1 (x : u32) (y1 : u32) : result (pair_t u32 u32) =
Ok { x = x; y = y1 }
(** [constants::P0]
Source: 'tests/src/constants.rs', lines 33:0-33:24 *)
let p0_body : result (u32 & u32) = mk_pair0 0 1
let p0 : (u32 & u32) = eval_global p0_body
(** [constants::P1]
Source: 'tests/src/constants.rs', lines 34:0-34:28 *)
let p1_body : result (pair_t u32 u32) = mk_pair1 0 1
let p1 : pair_t u32 u32 = eval_global p1_body
(** [constants::P2]
Source: 'tests/src/constants.rs', lines 35:0-35:24 *)
let p2_body : result (u32 & u32) = Ok (0, 1)
let p2 : (u32 & u32) = eval_global p2_body
(** [constants::P3]
Source: 'tests/src/constants.rs', lines 36:0-36:28 *)
let p3_body : result (pair_t u32 u32) = Ok { x = 0; y = 1 }
let p3 : pair_t u32 u32 = eval_global p3_body
(** [constants::Wrap]
Source: 'tests/src/constants.rs', lines 51:0-51:18 *)
type wrap_t (t : Type0) = { value : t; }
(** [constants::{constants::Wrap<T>}::new]:
Source: 'tests/src/constants.rs', lines 56:4-56:41 *)
let wrap_new (t : Type0) (value : t) : result (wrap_t t) =
Ok { value = value }
(** [constants::Y]
Source: 'tests/src/constants.rs', lines 43:0-43:22 *)
let y_body : result (wrap_t i32) = wrap_new i32 2
let y : wrap_t i32 = eval_global y_body
(** [constants::unwrap_y]:
Source: 'tests/src/constants.rs', lines 45:0-45:30 *)
let unwrap_y : result i32 =
Ok y.value
(** [constants::YVAL]
Source: 'tests/src/constants.rs', lines 49:0-49:19 *)
let yval_body : result i32 = unwrap_y
let yval : i32 = eval_global yval_body
(** [constants::get_z1::Z1]
Source: 'tests/src/constants.rs', lines 64:4-64:17 *)
let get_z1_z1_body : result i32 = Ok 3
let get_z1_z1 : i32 = eval_global get_z1_z1_body
(** [constants::get_z1]:
Source: 'tests/src/constants.rs', lines 63:0-63:28 *)
let get_z1 : result i32 =
Ok get_z1_z1
(** [constants::add]:
Source: 'tests/src/constants.rs', lines 68:0-68:39 *)
let add (a : i32) (b : i32) : result i32 =
i32_add a b
(** [constants::Q1]
Source: 'tests/src/constants.rs', lines 76:0-76:17 *)
let q1_body : result i32 = Ok 5
let q1 : i32 = eval_global q1_body
(** [constants::Q2]
Source: 'tests/src/constants.rs', lines 77:0-77:17 *)
let q2_body : result i32 = Ok q1
let q2 : i32 = eval_global q2_body
(** [constants::Q3]
Source: 'tests/src/constants.rs', lines 78:0-78:17 *)
let q3_body : result i32 = add q2 3
let q3 : i32 = eval_global q3_body
(** [constants::get_z2]:
Source: 'tests/src/constants.rs', lines 72:0-72:28 *)
let get_z2 : result i32 =
let* i = get_z1 in let* i1 = add i q3 in add q1 i1
(** [constants::S1]
Source: 'tests/src/constants.rs', lines 82:0-82:18 *)
let s1_body : result u32 = Ok 6
let s1 : u32 = eval_global s1_body
(** [constants::S2]
Source: 'tests/src/constants.rs', lines 83:0-83:18 *)
let s2_body : result u32 = incr s1
let s2 : u32 = eval_global s2_body
(** [constants::S3]
Source: 'tests/src/constants.rs', lines 84:0-84:29 *)
let s3_body : result (pair_t u32 u32) = Ok p3
let s3 : pair_t u32 u32 = eval_global s3_body
(** [constants::S4]
Source: 'tests/src/constants.rs', lines 85:0-85:29 *)
let s4_body : result (pair_t u32 u32) = mk_pair1 7 8
let s4 : pair_t u32 u32 = eval_global s4_body
(** [constants::V]
Source: 'tests/src/constants.rs', lines 88:0-88:31 *)
type v_t (t : Type0) (n : usize) = { x : array t n; }
(** [constants::{constants::V<T, N>#1}::LEN]
Source: 'tests/src/constants.rs', lines 93:4-93:24 *)
let v_len_body (t : Type0) (n : usize) : result usize = Ok n
let v_len (t : Type0) (n : usize) : usize = eval_global (v_len_body t n)
(** [constants::use_v]:
Source: 'tests/src/constants.rs', lines 96:0-96:42 *)
let use_v (t : Type0) (n : usize) : result usize =
Ok (v_len t n)
|
