1
2open HolKernel Parse boolLib bossLib BasicProvers;
3open wordsTheory wordsLib arithmeticTheory listTheory pairTheory mp_then
4     combinTheory x64asm_syntaxTheory x64asm_semanticsTheory relationTheory;
5
6val _ = new_theory "x64asm_properties";
7
8Inductive steps:
9  (���s (n:num).
10    steps (s,n) (s,n))
11  ���
12  (���s1 s2 n.
13    step s1 s2 ��� steps (s1,n) (s2,n))
14  ���
15  (���s1 s2 n.
16    step s1 s2 ��� steps (s1,n+1) (s2,n))
17  ���
18  (���s1 n1 s2 n2 s3 n3.
19    steps (s1,n1) (s2,n2) ���
20    steps (s2,n2) (s3,n3) ��� steps (s1,n1) (s3,n3))
21End
22
23Theorem step_consts:
24  step (State t0) (State t1) ���
25  t1.instructions = t0.instructions ���
26  ���w x. read_mem w t0 = SOME x ��� read_mem w t1 = SOME x
27Proof
28  fs [step_cases] \\ rw [] \\ fs []
29  \\ EVAL_TAC
30  \\ gvs[APPLY_UPDATE_THM,write_mem_def,AllCaseEqs(),read_mem_def]
31  \\ metis_tac[optionTheory.NOT_NONE_SOME, optionTheory.SOME_11]
32QED
33
34Theorem steps_consts:
35  ���x y.
36    steps x y ���
37    (���t1 m. y = (State t1,m) ��� ���t0 n. x = (State t0,n)) ���
38    ���t0 n t1 m.
39      x = (State t0,n) ��� y = (State t1,m) ���
40      t1.instructions = t0.instructions ���
41      ���w x. read_mem w t0 = SOME x ��� read_mem w t1 = SOME x
42Proof
43  Induct_on ���steps��� \\ rw [] \\ gvs[]
44  \\ imp_res_tac step_consts \\ gvs[]
45  \\ gs[Once step_cases]
46QED
47
48Theorem steps_inst:
49  steps (State t0,n) (State t1,m) ��� t1.instructions = t0.instructions
50Proof
51  rw [] \\ imp_res_tac steps_consts \\ fs []
52QED
53
54Theorem steps_trans:
55  ���x y z. steps x y ��� steps y z ��� steps x z
56Proof
57  fs [FORALL_PROD] \\ metis_tac [steps_rules]
58QED
59
60Theorem steps_refl[simp]:
61  ���x. steps x x
62Proof
63  once_rewrite_tac [steps_cases] \\ fs [FORALL_PROD]
64QED
65
66Theorem IMP_steps_state:
67  (���mid. steps (start,n) mid ��� ���s. steps mid (State s,n) ��� P s) ���
68  ���s. steps (start,n) (State s,n) ��� P s
69Proof
70  rw [] \\ metis_tac [steps_trans]
71QED
72
73Theorem IMP_steps_alt:
74  (���y. steps x y ��� ���t1. steps y (State t1,n) ��� P t1) ���
75  ���t1. steps x (State t1,n) ��� P t1
76Proof
77  metis_tac [steps_trans]
78QED
79
80Theorem IMP_steps:
81  (���mid outcome. steps start mid ��� steps mid outcome ��� P outcome) ���
82  ���outcome. steps start outcome ��� P outcome
83Proof
84  rw [] \\ qexists_tac ���outcome��� \\ fs []
85  \\ PairCases_on ���start��� \\ PairCases_on ���mid��� \\ PairCases_on ���outcome���
86  \\ match_mp_tac (steps_rules |> CONJUNCTS |> last)
87  \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs []
88QED
89
90Theorem IMP_step:
91  (���mid outcome. step (FST start) (mid) ��� steps (mid,SND start) outcome ��� P outcome) ���
92  ���outcome. steps start outcome ��� P outcome
93Proof
94  rw [] \\ qexists_tac ���outcome��� \\ fs []
95  \\ PairCases_on ���start��� \\ PairCases_on ���outcome���
96  \\ match_mp_tac (steps_rules |> CONJUNCTS |> last)
97  \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs []
98  \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 2) \\ fs []
99QED
100
101Theorem IMP_step':
102  (���mid outcome. step s mid ��� steps (mid,n) outcome ��� P outcome) ���
103  ���outcome. steps (s,SUC n) outcome ��� P outcome
104Proof
105  rw [] \\ qexists_tac ���outcome��� \\ fs []
106  \\ PairCases_on ���outcome���
107  \\ match_mp_tac (steps_rules |> CONJUNCTS |> last)
108  \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [ADD1]
109  \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 3) \\ fs []
110QED
111
112Theorem IMP_start:
113  P start ���
114  ���outcome. steps start outcome ��� P outcome
115Proof
116  rw [] \\ qexists_tac ���start��� \\ fs [] \\ PairCases_on ���start���
117  \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 1 |> DISCH T) \\ fs []
118QED
119
120Theorem steps_imp_RTC_step:
121  ���s t. steps s t ��� step��� (FST s) (FST t)
122Proof
123  Induct_on ���steps��� \\ fs []
124  \\ metis_tac [RTC_TRANSITIVE,transitive_def]
125QED
126
127Theorem step_determ:
128  step x y ��� step x z ==> y = z
129Proof
130  once_rewrite_tac [step_cases] \\ rw [] \\ gvs[]
131  \\ ntac 2 (fs [take_branch_cases] \\ gvs [])
132  \\ gvs [APPEND_11_LENGTH]
133QED
134
135Theorem not_step_Halt[simp]:
136  ~step (Halt e1 o1) u
137Proof
138  once_rewrite_tac [step_cases] \\ fs []
139QED
140
141Theorem RTC_step_determ:
142  ���x e1 o1 e2 o2.
143    step��� x (Halt e1 o1) ��� step��� x (Halt e2 o2) ��� e2 = e1 ��� o2 = o1
144Proof
145  Induct_on ���RTC��� \\ simp[]
146  \\ metis_tac[step_determ, RTC_CASES1, not_step_Halt,
147               TypeBase.one_one_of ���:s_or_h���]
148QED
149
150Theorem steps_IMP_NRC_step:
151  ���s k res r. steps (s,k) (res,r) ��� ���k. NRC step k s res
152Proof
153  Induct_on ���steps��� \\ rw[]
154  THEN1 (qexists_tac ���0��� \\ fs [])
155  THEN1 (qexists_tac ���SUC 0��� \\ fs [])
156  THEN1 (qexists_tac ���SUC 0��� \\ fs [])
157  \\ metis_tac [NRC_ADD_I]
158QED
159
160Theorem NRC_step_determ:
161  ���k s res1 res2. NRC step k s res1 ��� NRC step k s res2 ��� res1 = res2
162Proof
163  Induct \\ fs [NRC] \\ rw []
164  \\ imp_res_tac step_determ \\ rw [] \\ res_tac
165QED
166
167Triviality steps_NRC:
168  ���s1 n1 s2 n2.
169    steps (s1,n1) (s2,n2) ��� ���k. NRC step (n1 - n2 + k) s1 s2 ��� n2 ��� n1
170Proof
171  Induct_on ���steps��� \\ rw [] \\ gvs []
172  THEN1 (qexists_tac ���0��� \\ fs [])
173  THEN1 (qexists_tac ���SUC 0��� \\ fs [])
174  THEN1 (qexists_tac ���0��� \\ fs [])
175  \\ qexists_tac ���k+k'���
176  \\ ���k + k' + n1 ��� n3 = (k + n1 ��� n2) + (k' + n2 ��� n3)��� by fs []
177  \\ metis_tac [NRC_ADD_I]
178QED
179
180Theorem step_mono:
181  step (State t1) (State t2) ��� t1.output ��� t2.output
182Proof
183  rw [step_cases] \\
184  gvs [write_reg_def,inc_def,set_pc_def,set_stack_def,write_mem_def,
185       AllCaseEqs(),unset_reg_def,put_char_def]
186QED
187
188Theorem NRC_step_mono:
189  ���n t1 t2. NRC step n (State t1) (State t2) ��� t1.output ��� t2.output
190Proof
191  Induct \\ fs [NRC_SUC_RECURSE_LEFT] \\ rw []
192  \\ Cases_on ���z��� \\ fs [] \\ res_tac
193  \\ imp_res_tac step_mono
194  \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS
195QED
196
197Theorem asm_output_PREFIX:
198  NRC step k (State t) (State t1) ���
199  steps (State t,k) (State t2,0) ���
200  t1.output ��� t2.output
201Proof
202  rw [] \\ drule steps_NRC \\ fs [] \\ rw []
203  \\ imp_res_tac NRC_ADD_E
204  \\ imp_res_tac NRC_step_determ \\ rw []
205  \\ imp_res_tac NRC_step_mono
206QED
207
208Theorem lprefix_chain_step:
209  lprefix_chain {fromList t'.output | step��� (State t) (State t')}
210Proof
211  fs [lprefix_lubTheory.lprefix_chain_def] \\ rw []
212  \\ fs [llistTheory.LPREFIX_fromList,llistTheory.from_toList]
213  \\ imp_res_tac RTC_NRC
214  \\ ���n ��� n' ��� n' ��� n��� by fs []
215  \\ fs [LESS_EQ_EXISTS] \\ rw []
216  \\ metis_tac [NRC_ADD_E,NRC_step_determ,NRC_step_mono,
217                rich_listTheory.IS_PREFIX_TRANS]
218QED
219
220val _ = export_theory();
221