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
|
signature external_FunsTheory =
sig
type thm = Thm.thm
(* Definitions *)
val custom_swap_back_def : thm
val custom_swap_fwd_def : thm
val swap_back_def : thm
val swap_fwd_def : thm
val test_custom_swap_back_def : thm
val test_custom_swap_fwd_def : thm
val test_new_non_zero_u32_fwd_def : thm
val test_swap_non_zero_fwd_def : thm
val test_vec_fwd_def : thm
val external_Funs_grammars : type_grammar.grammar * term_grammar.grammar
(*
[external_Opaque] Parent theory of "external_Funs"
[custom_swap_back_def] Definition
⊢ ∀x y st ret st0.
custom_swap_back x y st ret st0 =
do
(st1,_) <- core_mem_swap_fwd x y st;
(st2,_) <- core_mem_swap_back0 x y st st1;
(_,y0) <- core_mem_swap_back1 x y st st2;
Return (st0,ret,y0)
od
[custom_swap_fwd_def] Definition
⊢ ∀x y st.
custom_swap_fwd x y st =
do
(st0,_) <- core_mem_swap_fwd x y st;
(st1,x0) <- core_mem_swap_back0 x y st st0;
(st2,_) <- core_mem_swap_back1 x y st st1;
Return (st2,x0)
od
[swap_back_def] Definition
⊢ ∀x y st st0.
swap_back x y st st0 =
do
(st1,_) <- core_mem_swap_fwd x y st;
(st2,x0) <- core_mem_swap_back0 x y st st1;
(_,y0) <- core_mem_swap_back1 x y st st2;
Return (st0,x0,y0)
od
[swap_fwd_def] Definition
⊢ ∀x y st.
swap_fwd x y st =
do
(st0,_) <- core_mem_swap_fwd x y st;
(st1,_) <- core_mem_swap_back0 x y st st0;
(st2,_) <- core_mem_swap_back1 x y st st1;
Return (st2,())
od
[test_custom_swap_back_def] Definition
⊢ ∀x y st st0.
test_custom_swap_back x y st st0 =
custom_swap_back x y st (int_to_u32 1) st0
[test_custom_swap_fwd_def] Definition
⊢ ∀x y st.
test_custom_swap_fwd x y st =
do (st0,_) <- custom_swap_fwd x y st; Return (st0,()) od
[test_new_non_zero_u32_fwd_def] Definition
⊢ ∀x st.
test_new_non_zero_u32_fwd x st =
do
(st0,opt) <- core_num_nonzero_non_zero_u32_new_fwd x st;
core_option_option_unwrap_fwd opt st0
od
[test_swap_non_zero_fwd_def] Definition
⊢ ∀x st.
test_swap_non_zero_fwd x st =
do
(st0,_) <- swap_fwd x (int_to_u32 0) st;
(st1,x0,_) <- swap_back x (int_to_u32 0) st st0;
if x0 = int_to_u32 0 then Fail Failure else Return (st1,x0)
od
[test_vec_fwd_def] Definition
⊢ test_vec_fwd =
(let
v = vec_new
in
monad_ignore_bind (vec_push_back v (int_to_u32 0)) (Return ()))
*)
end
|
