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