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
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [external]: function definitions *)
module External.Funs
open Primitives
include External.Types
include External.Opaque
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [external::swap] *)
let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
begin match core_mem_swap_fwd t x y st with
| Fail -> Fail
| Return (st0, _) ->
begin match core_mem_swap_back0 t x y st st0 with
| Fail -> Fail
| Return (st1, _) ->
begin match core_mem_swap_back1 t x y st st1 with
| Fail -> Fail
| Return (st2, _) -> Return (st2, ())
end
end
end
(** [external::swap] *)
let swap_back
(t : Type0) (x : t) (y : t) (st : state) (st0 : state) :
result (state & (t & t))
=
begin match core_mem_swap_fwd t x y st with
| Fail -> Fail
| Return (st1, _) ->
begin match core_mem_swap_back0 t x y st st1 with
| Fail -> Fail
| Return (st2, x0) ->
begin match core_mem_swap_back1 t x y st st2 with
| Fail -> Fail
| Return (_, y0) -> Return (st0, (x0, y0))
end
end
end
(** [external::test_new_non_zero_u32] *)
let test_new_non_zero_u32_fwd
(x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) =
begin match core_num_nonzero_non_zero_u32_new_fwd x st with
| Fail -> Fail
| Return (st0, opt) ->
begin match
core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
with
| Fail -> Fail
| Return (st1, nzu) -> Return (st1, nzu)
end
end
(** [external::test_vec] *)
let test_vec_fwd : result unit =
let v = vec_new u32 in
begin match vec_push_back u32 v 0 with
| Fail -> Fail
| Return _ -> Return ()
end
(** Unit test for [external::test_vec] *)
let _ = assert_norm (test_vec_fwd = Return ())
(** [external::custom_swap] *)
let custom_swap_fwd
(t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
begin match core_mem_swap_fwd t x y st with
| Fail -> Fail
| Return (st0, _) ->
begin match core_mem_swap_back0 t x y st st0 with
| Fail -> Fail
| Return (st1, x0) ->
begin match core_mem_swap_back1 t x y st st1 with
| Fail -> Fail
| Return (st2, _) -> Return (st2, x0)
end
end
end
(** [external::custom_swap] *)
let custom_swap_back
(t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) :
result (state & (t & t))
=
begin match core_mem_swap_fwd t x y st with
| Fail -> Fail
| Return (st1, _) ->
begin match core_mem_swap_back0 t x y st st1 with
| Fail -> Fail
| Return (st2, _) ->
begin match core_mem_swap_back1 t x y st st2 with
| Fail -> Fail
| Return (_, y0) -> Return (st0, (ret, y0))
end
end
end
(** [external::test_custom_swap] *)
let test_custom_swap_fwd
(x : u32) (y : u32) (st : state) : result (state & unit) =
begin match custom_swap_fwd u32 x y st with
| Fail -> Fail
| Return (st0, _) -> Return (st0, ())
end
(** [external::test_custom_swap] *)
let test_custom_swap_back
(x : u32) (y : u32) (st : state) (st0 : state) :
result (state & (u32 & u32))
=
begin match custom_swap_back u32 x y st 1 st0 with
| Fail -> Fail
| Return (st1, (x0, y0)) -> Return (st1, (x0, y0))
end
(** [external::test_swap_non_zero] *)
let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
begin match swap_fwd u32 x 0 st with
| Fail -> Fail
| Return (st0, _) ->
begin match swap_back u32 x 0 st st0 with
| Fail -> Fail
| Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0)
end
end
|
