-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathp4_exec_sem_frames_soundnessScript.sml
157 lines (148 loc) · 4.85 KB
/
p4_exec_sem_frames_soundnessScript.sml
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
open HolKernel boolLib Parse bossLib;
val _ = new_theory "p4_exec_sem_frames_soundness";
open p4Lib;
open listTheory ottTheory p4Theory p4_auxTheory p4_exec_semTheory p4_exec_sem_stmt_soundnessTheory;
Definition frame_list_exec_sound:
(frame_list_exec_sound (type:'a itself) frame_list =
!(ctx:'a ctx) ascope g_scope_list status state'.
frames_exec ctx (ascope, g_scope_list, frame_list, status) = SOME state' ==>
frames_red ctx (ascope, g_scope_list, frame_list, status) state')
End
Theorem frame_list_exec_sound_red:
!type frame_list. frame_list_exec_sound type frame_list
Proof
Induct_on `frame_list` >> (
fs [frame_list_exec_sound] >>
Cases_on `status` >> (
fs [frames_exec_def]
)
) >>
rpt strip_tac >>
pairLib.PairCases_on `ctx` >>
rename1 `(apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map)` >>
Cases_on `frame_list` >| [
(* Single frame (comp1) *)
pairLib.PairCases_on `h` >>
fs [frames_exec_def] >>
Cases_on `scopes_to_pass h0 func_map b_func_map g_scope_list` >> (
fs []
) >>
Cases_on `map_to_pass h0 b_func_map` >> (
fs []
) >>
Cases_on `tbl_to_pass h0 b_func_map tbl_map` >> (
fs []
) >>
Cases_on `stmt_exec (apply_table_f,ext_map,func_map,x',pars_map,x'')
(ascope,x,[(h0,h1,h2)],status_running)` >- (
fs []
) >>
pairLib.PairCases_on `x'''` >>
fs [] >>
Cases_on `scopes_to_retrieve h0 func_map b_func_map g_scope_list x'''1` >> (
fs []
) >>
rw [] >>
rename1 `(ascope', x'''1, frame_list', status')` >>
assume_tac stmt_stack_exec_sound_red >>
fs [stmt_stack_exec_sound] >>
RES_TAC >>
irule (SIMP_RULE list_ss [] (Q.SPECL [`apply_table_f`, `ext_map`, `func_map`, `b_func_map`, `pars_map`, `tbl_map`, `ascope`, `g_scope_list`, `h0`, `h1`, `h2`, `[]`] ((valOf o find_clause_frames_red) "frames_comp1"))) >>
fs [clause_name_def] >>
qexists_tac `x'''1` >>
fs [],
(* Multiple frames *)
pairLib.PairCases_on `h` >>
pairLib.PairCases_on `h'` >>
fs [frames_exec_def] >>
Cases_on `scopes_to_pass h0 func_map b_func_map g_scope_list` >> (
fs []
) >>
Cases_on `map_to_pass h0 b_func_map` >> (
fs []
) >>
Cases_on `tbl_to_pass h0 b_func_map tbl_map` >> (
fs []
) >>
rename1 `(ascope,g_scope_list',[(h0,h1,h2)],status_running)` >>
Cases_on `stmt_exec (apply_table_f,ext_map,func_map,x',pars_map,x'')
(ascope,g_scope_list',[(h0,h1,h2)],status_running)` >> (
fs []
) >>
pairLib.PairCases_on `x` >>
rename1 `(ascope', x1, frame_list', status')` >>
rename1 `(ascope', g_scope_list'', frame_list', status')` >>
fs [] >>
Cases_on `status'` >> (
fs []
) >| [
(* comp1 *)
Cases_on `scopes_to_retrieve h0 func_map b_func_map g_scope_list g_scope_list''` >> (
fs []
) >>
rw [] >>
assume_tac stmt_stack_exec_sound_red >>
fs [stmt_stack_exec_sound] >>
RES_TAC >>
irule (SIMP_RULE list_ss [] (Q.SPECL [`apply_table_f`, `ext_map`, `func_map`, `b_func_map`, `pars_map`, `tbl_map`, `ascope`, `g_scope_list`, `h0`, `h1`, `h2`, `(h'0,h'1,h'2)::t`] ((valOf o find_clause_frames_red) "frames_comp1"))) >>
fs [clause_name_def, notret_def] >>
qexists_tac `g_scope_list''` >>
fs [],
(* comp2 *)
Cases_on `frame_list'` >> (
fs []
) >>
Cases_on `t'` >> (
fs []
) >>
PairCases_on `h` >>
fs [] >>
Cases_on `assign g_scope_list'' v (lval_varname (varn_star h0'))` >> (
fs []
) >>
Cases_on `scopes_to_retrieve h0' func_map b_func_map g_scope_list x` >> (
fs []
) >>
Cases_on `lookup_funn_sig_body h0' func_map b_func_map ext_map` >> (
fs []
) >>
PairCases_on `x''''` >>
fs [] >>
Cases_on `scopes_to_pass h'0 func_map b_func_map x'''` >> (
fs []
) >>
Cases_on `copyout (MAP FST x''''1) (MAP SND x''''1) x'''' h'2 h2'` >> (
fs []
) >>
PairCases_on `x'''''` >>
fs [] >>
Cases_on `scopes_to_retrieve h'0 func_map b_func_map x''' x'''''0` >> (
fs []
) >>
rw [] >>
IMP_RES_TAC stmt_exec_status_returnv_inv >>
rw [] >>
assume_tac stmt_stack_exec_sound_red >>
fs [stmt_stack_exec_sound] >>
RES_TAC >>
fs [] >>
irule (SIMP_RULE list_ss [] (Q.SPECL [`x''''1`, `apply_table_f`, `ext_map`, `func_map`, `b_func_map`, `pars_map`, `tbl_map`, `ascope`, `g_scope_list`, `h0`, `h1`, `h2`, `h'0`, `h'1`, `h'2`, `t`] ((valOf o find_clause_frames_red) "frames_comp2"))) >>
fs [clause_name_def] >>
qexistsl_tac [`g_scope_list''`, `x`, `x'''`, `x''''`, `x'''''0`, `h2'`, `h1'`, `v`] >>
fs [lambda_FST, lambda_SND],
(* comp1 *)
Cases_on `scopes_to_retrieve h0 func_map b_func_map g_scope_list g_scope_list''` >> (
fs []
) >>
rw [] >>
assume_tac stmt_stack_exec_sound_red >>
fs [stmt_stack_exec_sound] >>
RES_TAC >>
irule (SIMP_RULE list_ss [] (Q.SPECL [`apply_table_f`, `ext_map`, `func_map`, `b_func_map`, `pars_map`, `tbl_map`, `ascope`, `g_scope_list`, `h0`, `h1`, `h2`, `(h'0,h'1,h'2)::t`] ((valOf o find_clause_frames_red) "frames_comp1"))) >>
fs [clause_name_def, notret_def] >>
qexists_tac `g_scope_list''` >>
fs []
]
]
QED
val _ = export_theory ();