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