1open HolKernel boolLib bossLib 2open blastLib stateLib 3open set_sepTheory progTheory temporal_stateTheory arm8_stepTheory 4 5val () = new_theory "arm8_prog" 6 7(* ------------------------------------------------------------------------ *) 8 9val _ = 10 stateLib.sep_definitions "arm8" 11 [["PSTATE"], ["SCTLR_EL1"], ["TCR_EL1"]] 12 [["undefined"], ["branch_hint"]] 13 arm8_stepTheory.NextStateARM8_def 14 15val arm8_instr_def = Define` 16 arm8_instr (a, i: word32) = 17 { (arm8_c_MEM a, arm8_d_word8 ((7 >< 0) i)); 18 (arm8_c_MEM (a + 1w), arm8_d_word8 ((15 >< 8) i)); 19 (arm8_c_MEM (a + 2w), arm8_d_word8 ((23 >< 16) i)); 20 (arm8_c_MEM (a + 3w), arm8_d_word8 ((31 >< 24) i)) }` 21 22val ARM8_MODEL_def = Define` 23 ARM8_MODEL = 24 (STATE arm8_proj, NEXT_REL (=) NextStateARM8, arm8_instr, 25 ($= :arm8_state -> arm8_state -> bool), (K F: arm8_state -> bool))` 26 27val ARM8_IMP_SPEC = Theory.save_thm ("ARM8_IMP_SPEC", 28 stateTheory.IMP_SPEC 29 |> Q.ISPECL [`arm8_proj`, `NextStateARM8`, `arm8_instr`] 30 |> REWRITE_RULE [GSYM ARM8_MODEL_def] 31 ) 32 33val ARM8_IMP_TEMPORAL = Theory.save_thm ("ARM8_IMP_TEMPORAL", 34 temporal_stateTheory.IMP_TEMPORAL 35 |> Q.ISPECL [`arm8_proj`, `NextStateARM8`, `arm8_instr`, 36 `(=): arm8_state -> arm8_state -> bool`, 37 `K F: arm8_state -> bool`] 38 |> REWRITE_RULE [GSYM ARM8_MODEL_def] 39 ) 40 41(* ------------------------------------------------------------------------ *) 42 43(* Aliases *) 44 45val arm8_REG_def = DB.definition "arm8_REG_def" 46val arm8_MEM_def = DB.definition "arm8_MEM_def" 47 48val (arm8_REGISTERS_def, arm8_REGISTERS_INSERT) = 49 stateLib.define_map_component ("arm8_REGISTERS", "reg", arm8_REG_def) 50 51val (arm8_MEMORY_def, arm8_MEMORY_INSERT) = 52 stateLib.define_map_component ("arm8_MEMORY", "mem", arm8_MEM_def) 53 54val arm8_WORD_def = Define` 55 arm8_WORD a (i: word32) = 56 arm8_MEM a ((7 >< 0) i) * 57 arm8_MEM (a + 1w) ((15 >< 8) i) * 58 arm8_MEM (a + 2w) ((23 >< 16) i) * 59 arm8_MEM (a + 3w) ((31 >< 24) i)`; 60 61val arm8_WORD_MEMORY_def = Define` 62 arm8_WORD_MEMORY dmem mem = 63 {BIGUNION { BIGUNION (arm8_WORD a (mem a)) | a IN dmem /\ aligned 2 a}}` 64 65val arm8_DWORD_def = Define` 66 arm8_DWORD a (i: word64) = 67 arm8_MEM a ((7 >< 0) i) * 68 arm8_MEM (a + 1w) ((15 >< 8) i) * 69 arm8_MEM (a + 2w) ((23 >< 16) i) * 70 arm8_MEM (a + 3w) ((31 >< 24) i) * 71 arm8_MEM (a + 4w) ((39 >< 32) i) * 72 arm8_MEM (a + 5w) ((47 >< 40) i) * 73 arm8_MEM (a + 6w) ((55 >< 48) i) * 74 arm8_MEM (a + 7w) ((63 >< 56) i)`; 75 76val arm8_DWORD_MEMORY_def = Define` 77 arm8_DWORD_MEMORY dmem mem = 78 {BIGUNION { BIGUNION (arm8_DWORD a (mem a)) | a IN dmem /\ aligned 3 a}}` 79 80val arm8_pc_def = Define` 81 arm8_pc pc = 82 arm8_PC pc * arm8_exception NoException * arm8_PSTATE_EL 0w * 83 arm8_SCTLR_EL1_E0E F * arm8_TCR_EL1_TBI0 F * arm8_TCR_EL1_TBI1 F * 84 arm8_SCTLR_EL1_SA0 F * set_sep$cond (aligned 2 pc)`; 85 86val aS_def = Define ` 87 aS (n,z,c,v) = 88 arm8_PSTATE_N n * arm8_PSTATE_Z z * arm8_PSTATE_C c * arm8_PSTATE_V v`; 89 90(* ------------------------------------------------------------------------ *) 91 92val aS_HIDE = Q.store_thm("aS_HIDE", 93 `~aS = ~arm8_PSTATE_N * ~arm8_PSTATE_Z * ~arm8_PSTATE_C * ~arm8_PSTATE_V`, 94 SIMP_TAC std_ss [SEP_HIDE_def, aS_def, SEP_CLAUSES, FUN_EQ_THM] 95 \\ SIMP_TAC std_ss [SEP_EXISTS] 96 \\ METIS_TAC [aS_def, pairTheory.PAIR] 97 ) 98 99val arm_CPSR_T_F = Q.store_thm("arm_CPSR_T_F", 100 `( n ==> (arm8_PSTATE_N T = arm8_PSTATE_N n)) /\ 101 (~n ==> (arm8_PSTATE_N F = arm8_PSTATE_N n)) /\ 102 ( z ==> (arm8_PSTATE_Z T = arm8_PSTATE_Z z)) /\ 103 (~z ==> (arm8_PSTATE_Z F = arm8_PSTATE_Z z)) /\ 104 ( c ==> (arm8_PSTATE_C T = arm8_PSTATE_C c)) /\ 105 (~c ==> (arm8_PSTATE_C F = arm8_PSTATE_C c)) /\ 106 ( v ==> (arm8_PSTATE_V T = arm8_PSTATE_V v)) /\ 107 (~v ==> (arm8_PSTATE_V F = arm8_PSTATE_V v))`, 108 simp [] 109 ) 110 111(* ------------------------------------------------------------------------ *) 112 113val arm8_PC_INTRO = Q.store_thm("arm8_PC_INTRO", 114 `SPEC m (p1 * arm8_pc pc) code 115 (p2 * arm8_PC pc' * arm8_exception NoException * arm8_PSTATE_EL 0w * 116 arm8_SCTLR_EL1_E0E F * arm8_TCR_EL1_TBI0 F * arm8_TCR_EL1_TBI1 F * 117 arm8_SCTLR_EL1_SA0 F) ==> 118 (aligned 2 pc ==> aligned 2 pc') ==> 119 SPEC m (p1 * arm8_pc pc) code (p2 * arm8_pc pc')`, 120 REPEAT STRIP_TAC 121 \\ FULL_SIMP_TAC std_ss 122 [arm8_pc_def, SPEC_MOVE_COND, STAR_ASSOC, SEP_CLAUSES] 123 ) 124 125val arm8_TEMPORAL_PC_INTRO = Q.store_thm("arm8_TEMPORAL_PC_INTRO", 126 `TEMPORAL_NEXT m (p1 * arm8_pc pc) code 127 (p2 * arm8_PC pc' * arm8_exception NoException * arm8_PSTATE_EL 0w * 128 arm8_SCTLR_EL1_E0E F * arm8_TCR_EL1_TBI0 F * arm8_TCR_EL1_TBI1 F * 129 arm8_SCTLR_EL1_SA0 F) ==> 130 (aligned 2 pc ==> aligned 2 pc') ==> 131 TEMPORAL_NEXT m (p1 * arm8_pc pc) code (p2 * arm8_pc pc')`, 132 REPEAT STRIP_TAC 133 \\ FULL_SIMP_TAC std_ss 134 [arm8_pc_def, TEMPORAL_NEXT_MOVE_COND, STAR_ASSOC, SEP_CLAUSES] 135 ) 136 137(* ------------------------------------------------------------------------ *) 138 139val lem = Q.prove( 140 `!x. ((\s. x = s) = {x})`, 141 rewrite_tac [GSYM stateTheory.SEP_EQ_SINGLETON, set_sepTheory.SEP_EQ_def] 142 \\ simp [FUN_EQ_THM] 143 \\ REPEAT strip_tac 144 \\ eq_tac 145 \\ simp [] 146 ) 147 148fun thm v n x y = 149 stateTheory.MAPPED_COMPONENT_INSERT 150 |> Q.ISPECL 151 [`\a:word64. aligned ^n a`, `2n ** ^n`, `\a i. arm8_c_MEM (a + n2w i)`, 152 `\v i. arm8_d_word8 (EL i ^v)`, x, y] 153 |> Conv.CONV_RULE 154 (Conv.LAND_CONV 155 (SIMP_CONV (srw_ss()) 156 [arm8_MEM_def, arm8_WORD_def, arm8_DWORD_def, 157 pred_setTheory.INSERT_UNION_EQ, lem, 158 set_sepTheory.STAR_def, set_sepTheory.SPLIT_def, 159 blastLib.BBLAST_PROVE 160 ``a <> a + 1w:word64 /\ a <> a + 2w /\ a <> a + 3w /\ 161 a <> a + 4w /\ a <> a + 5w /\ a <> a + 6w /\ a <> a + 7w``]) 162 THENC REWRITE_CONV []) 163 164val lem1 = Q.prove( 165 `!i. i < 4 ==> n2w i <+ (4w: word64)`, 166 simp [wordsTheory.word_lo_n2w]) 167 168val lem2 = Q.prove( 169 `aligned 2 (a: word64) /\ aligned 2 b /\ x <+ 4w /\ y <+ 4w ==> 170 ((a + x = b + y) = (a = b) /\ (x = y))`, 171 simp [alignmentTheory.aligned_extract] 172 \\ blastLib.BBLAST_TAC 173 ) 174 175val v4 = ``[( 7 >< 0) v; (15 >< 8) v; 176 (23 >< 16) v; (31 >< 24) (v:word32)]:word8 list`` 177 178 179(* Need ``(\a. ..) c`` below for automation to work *) 180val arm8_WORD_MEMORY_INSERT = Q.store_thm("arm8_WORD_MEMORY_INSERT", 181 `!f df c d. 182 c IN df /\ (\a. aligned 2 a) c ==> 183 (arm8_WORD c d * arm8_WORD_MEMORY (df DELETE c) f = 184 arm8_WORD_MEMORY df ((c =+ d) f))`, 185 match_mp_tac (thm v4 ``2n`` `arm8_WORD` `arm8_WORD_MEMORY`) 186 \\ rw [arm8_WORD_MEMORY_def] 187 \\ `(i = j) = (n2w i = n2w j: word64)` by simp [] 188 \\ asm_rewrite_tac [] 189 \\ match_mp_tac lem2 190 \\ simp [lem1] 191 ) 192 193val lem1 = Q.prove( 194 `!i. i < 8 ==> n2w i <+ (8w: word64)`, 195 simp [wordsTheory.word_lo_n2w]) 196 197val lem2 = Q.prove( 198 `aligned 3 (a: word64) /\ aligned 3 b /\ x <+ 8w /\ y <+ 8w ==> 199 ((a + x = b + y) = (a = b) /\ (x = y))`, 200 simp [alignmentTheory.aligned_extract] 201 \\ blastLib.BBLAST_TAC 202 ) 203 204val v8 = ``[( 7 >< 0) v; (15 >< 8) v; 205 (23 >< 16) v; (31 >< 24) v; 206 (39 >< 32) v; (47 >< 40) v; 207 (55 >< 48) v; (63 >< 56) (v:word64)]:word8 list`` 208 209val arm8_DWORD_MEMORY_INSERT = Q.store_thm("arm8_DWORD_MEMORY_INSERT", 210 `!f df c d. 211 c IN df /\ (\a. aligned 3 a) c ==> 212 (arm8_DWORD c d * arm8_DWORD_MEMORY (df DELETE c) f = 213 arm8_DWORD_MEMORY df ((c =+ d) f))`, 214 match_mp_tac (thm v8 ``3n`` `arm8_DWORD` `arm8_DWORD_MEMORY`) 215 \\ rw [arm8_DWORD_MEMORY_def] 216 \\ `(i = j) = (n2w i = n2w j: word64)` by simp [] 217 \\ asm_rewrite_tac [] 218 \\ match_mp_tac lem2 219 \\ simp [lem1] 220 ) 221 222(* ------------------------------------------------------------------------ *) 223 224(* Theorems for moving literal loads into the code pool *) 225 226val arm_instr_star = Q.prove( 227 `!a w. 228 {arm8_instr (a, w)} = 229 arm8_MEM a ((7 >< 0) w) * 230 arm8_MEM (a + 1w) ((15 >< 8) w) * 231 arm8_MEM (a + 2w) ((23 >< 16) w) * 232 arm8_MEM (a + 3w) ((31 >< 24) w)`, 233 srw_tac [wordsLib.WORD_ARITH_EQ_ss] 234 [pred_setTheory.INSERT_UNION_EQ, arm8_instr_def, arm8_MEM_def, 235 set_sepTheory.STAR_def, set_sepTheory.SPLIT_def] 236 \\ simp [boolTheory.FUN_EQ_THM] 237 \\ metis_tac [] 238 ) 239 240val arm_instr_star_not_disjoint = Q.prove( 241 `!a w p. 242 ~DISJOINT (arm8_instr (a, w)) p ==> 243 ({p} * 244 arm8_MEM a ((7 >< 0) w) * 245 arm8_MEM (a + 1w) ((15 >< 8) w) * 246 arm8_MEM (a + 2w) ((23 >< 16) w) * 247 arm8_MEM (a + 3w) ((31 >< 24) w) = SEP_F)`, 248 rw [set_sepTheory.STAR_def, set_sepTheory.SPLIT_def, 249 arm8_instr_def, arm8_MEM_def, pred_setTheory.DISJOINT_DEF] 250 \\ simp [boolTheory.FUN_EQ_THM, set_sepTheory.SEP_F_def] 251 \\ Cases_on `(arm8_c_MEM a,arm8_d_word8 ((7 >< 0) w)) IN p` 252 \\ simp [] 253 \\ Cases_on `(arm8_c_MEM (a + 1w),arm8_d_word8 ((15 >< 8) w)) IN p` 254 \\ simp [] 255 \\ Cases_on `(arm8_c_MEM (a + 2w),arm8_d_word8 ((23 >< 16) w)) IN p` 256 \\ simp [] 257 \\ Cases_on `(arm8_c_MEM (a + 3w),arm8_d_word8 ((31 >< 24) w)) IN p` 258 \\ simp [] 259 \\ fs [pred_setTheory.INSERT_INTER] 260 ) 261 262val MOVE_TO_TEMPORAL_ARM_CODE_POOL = Q.store_thm 263 ("MOVE_TO_TEMPORAL_ARM_CODE_POOL", 264 `!a w c p q. 265 TEMPORAL_NEXT ARM8_MODEL 266 (p * 267 arm8_MEM a ((7 >< 0) w) * 268 arm8_MEM (a + 1w) ((15 >< 8) w) * 269 arm8_MEM (a + 2w) ((23 >< 16) w) * 270 arm8_MEM (a + 3w) ((31 >< 24) w)) 271 c 272 (q * 273 arm8_MEM a ((7 >< 0) w) * 274 arm8_MEM (a + 1w) ((15 >< 8) w) * 275 arm8_MEM (a + 2w) ((23 >< 16) w) * 276 arm8_MEM (a + 3w) ((31 >< 24) w)) = 277 TEMPORAL_NEXT ARM8_MODEL 278 (cond (DISJOINT (arm8_instr (a, w)) (BIGUNION (IMAGE arm8_instr c))) * 279 p) 280 ((a, w) INSERT c) 281 q`, 282 REPEAT strip_tac 283 \\ once_rewrite_tac [GSYM temporal_stateTheory.TEMPORAL_NEXT_CODE] 284 \\ rewrite_tac [ARM8_MODEL_def, stateTheory.CODE_POOL, 285 pred_setTheory.IMAGE_INSERT, 286 pred_setTheory.IMAGE_EMPTY, 287 pred_setTheory.BIGUNION_INSERT, 288 pred_setTheory.BIGUNION_EMPTY] 289 \\ Cases_on `DISJOINT (arm8_instr (a, w)) (BIGUNION (IMAGE arm8_instr c))` 290 \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES, 291 temporal_stateTheory.TEMPORAL_NEXT_FALSE_PRE, 292 AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] 293 \\ imp_res_tac arm_instr_star_not_disjoint 294 \\ fs [set_sepTheory.SEP_CLAUSES, 295 temporal_stateTheory.TEMPORAL_NEXT_FALSE_PRE, 296 AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] 297 ) 298 299val MOVE_TO_ARM_CODE_POOL = Q.store_thm("MOVE_TO_ARM_CODE_POOL", 300 `!a w c p q. 301 SPEC ARM8_MODEL 302 (p * 303 arm8_MEM a ((7 >< 0) w) * 304 arm8_MEM (a + 1w) ((15 >< 8) w) * 305 arm8_MEM (a + 2w) ((23 >< 16) w) * 306 arm8_MEM (a + 3w) ((31 >< 24) w)) 307 c 308 (q * 309 arm8_MEM a ((7 >< 0) w) * 310 arm8_MEM (a + 1w) ((15 >< 8) w) * 311 arm8_MEM (a + 2w) ((23 >< 16) w) * 312 arm8_MEM (a + 3w) ((31 >< 24) w)) = 313 SPEC ARM8_MODEL 314 (cond (DISJOINT (arm8_instr (a, w)) (BIGUNION (IMAGE arm8_instr c))) * 315 p) 316 ((a, w) INSERT c) 317 q`, 318 REPEAT strip_tac 319 \\ once_rewrite_tac [GSYM progTheory.SPEC_CODE] 320 \\ rewrite_tac [ARM8_MODEL_def, stateTheory.CODE_POOL, 321 pred_setTheory.IMAGE_INSERT, 322 pred_setTheory.IMAGE_EMPTY, 323 pred_setTheory.BIGUNION_INSERT, 324 pred_setTheory.BIGUNION_EMPTY] 325 \\ Cases_on `DISJOINT (arm8_instr (a, w)) (BIGUNION (IMAGE arm8_instr c))` 326 \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES, 327 progTheory.SPEC_FALSE_PRE, 328 AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] 329 \\ imp_res_tac arm_instr_star_not_disjoint 330 \\ fs [set_sepTheory.SEP_CLAUSES, progTheory.SPEC_FALSE_PRE, 331 AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] 332 ) 333 334val sub_intro = Theory.save_thm("sub_intro", 335 simpLib.SIMP_PROVE (srw_ss()) [] 336 ``(a + (-b + c) = a - b + c : word64) /\ (a + -b = a - b)`` 337 ) 338 339val tac = asm_simp_tac (srw_ss()++wordsLib.WORD_CANCEL_ss) 340 [pred_setTheory.INSERT_INTER] 341 342(* 343val top = utilsLib.rhsc (wordsLib.WORD_EVAL_CONV ``word_T - 2w : word32``) 344*) 345 346val DISJOINT_arm_instr = Q.store_thm("DISJOINT_arm_instr", 347 `!a pc x y. 348 3w <+ a /\ a <+ 0xFFFFFFFFFFFFFFFDw ==> 349 DISJOINT (arm8_instr (pc + a, x)) (arm8_instr (pc, y))`, 350 rw [arm8_instr_def, pred_setTheory.DISJOINT_DEF] 351 \\ `a + 1w <> 0w` by blastLib.FULL_BBLAST_TAC 352 \\ `a + 2w <> 0w` by blastLib.FULL_BBLAST_TAC 353 \\ `a + 3w <> 0w` by blastLib.FULL_BBLAST_TAC 354 \\ `a <> 0w` by blastLib.FULL_BBLAST_TAC 355 \\ `3w <> a` by blastLib.FULL_BBLAST_TAC 356 \\ `2w <> a` by blastLib.FULL_BBLAST_TAC 357 \\ `1w <> a` by blastLib.FULL_BBLAST_TAC 358 \\ tac 359 ) 360 361val lem = Q.prove( 362 `!a x y. arm8_instr (a + 4w, x) INTER arm8_instr (a, y) = {}`, 363 rw [arm8_instr_def, pred_setTheory.DISJOINT_DEF] 364 \\ tac 365 ) 366 367val DISJOINT_arm_instr_2 = Q.prove( 368 `!a pc x1 x2 y. 369 DISJOINT (arm8_instr (pc + a, x1)) 370 (arm8_instr (pc + a + 4w, x2) UNION arm8_instr (pc, y)) = 371 DISJOINT (arm8_instr (pc + a, x1)) (arm8_instr (pc, y))`, 372 rw [pred_setTheory.DISJOINT_DEF, lem] 373 \\ metis_tac [pred_setTheory.INTER_COMM] 374 ) 375 376val rearrange = 377 blastLib.BBLAST_PROVE ``a + (b + c + d) = a + (b + c) + d : word64`` 378 379fun disjoint_arm_instr q = 380 DISJOINT_arm_instr 381 |> Q.SPEC q 382 |> Drule.SPEC_ALL 383 |> Conv.CONV_RULE (LAND_CONV blastLib.BBLAST_CONV) 384 |> REWRITE_RULE [rearrange] 385 |> Drule.GEN_ALL 386 387fun disjoint_arm_instr_2 q = 388 DISJOINT_arm_instr_2 389 |> Q.SPEC q 390 |> REWRITE_RULE [sub_intro, wordsTheory.WORD_ADD_ASSOC, 391 GSYM wordsTheory.WORD_ADD_SUB_ASSOC] 392 |> Drule.GEN_ALL 393 394val disjoint_arm_instr_thms = Theory.save_thm("disjoint_arm_instr_thms", 395 Drule.LIST_CONJ 396 ([disjoint_arm_instr `(w2w (w: word8) + 8w) + 4w`, 397 disjoint_arm_instr `w2w (w: word8) + 8w`, 398 disjoint_arm_instr `w2w (w: word12) + 8w`] @ 399 List.map disjoint_arm_instr_2 [`a`, `-a`, `a + b`, `a - b`]) 400 ) 401 402(* ------------------------------------------------------------------------ *) 403 404val () = export_theory() 405