1(* interactive use: 2 3quietdec := true; 4loadPath := (concat Globals.HOLDIR "/examples/dev/sw") :: !loadPath; 5 6app load ["numLib", "pred_setSimps", "pred_setTheory", 7 "arithmeticTheory", "wordsTheory", "pairTheory", "listTheory", "whileTheory", "finite_mapTheory", "fcpLib", "wordsLib"]; 8 9open numLib pred_setSimps pred_setTheory arithmeticTheory wordsTheory 10 pairTheory listTheory whileTheory finite_mapTheory wordsLib; 11 12quietdec := false; 13*) 14 15open HolKernel Parse boolLib bossLib numLib pred_setSimps pred_setTheory 16 arithmeticTheory wordsTheory pairTheory listTheory whileTheory finite_mapTheory 17 wordsLib; 18 19val _ = new_theory "preARM"; 20 21(*----------------------------------------------------------------------------*) 22(* Registers *) 23(*----------------------------------------------------------------------------*) 24 25val _ = type_abbrev("REGISTER", Type`:word4`); 26 27(*----------------------------------------------------------------------------*) 28(* CPSR, In user programs only the top 4 bits of the CPSR are relevant *) 29(* N - the result was negative *) 30(* Z - the result was zero *) 31(* C - the result produced a carry out *) 32(* V - the result generated an arithmetic overflow *) 33(*----------------------------------------------------------------------------*) 34 35val _ = type_abbrev("CPSR", Type`:word32`); 36val _ = Hol_datatype `SRS = SN | SZ | SC | SV`; 37 38val getS_def = Define 39 `getS (cpsr : CPSR) (flag:SRS) = 40 case flag of 41 SN => cpsr ' 31 | 42 SZ => cpsr ' 30 | 43 SC => cpsr ' 29 | 44 SV => cpsr ' 28 45 `; 46 47val getS_thm = Q.store_thm ( 48 "getS_thm", 49 `(getS (cpsr : CPSR) SN = cpsr ' 31) /\ 50 (getS (cpsr : CPSR) SZ = cpsr ' 30) /\ 51 (getS (cpsr : CPSR) SC = cpsr ' 29) /\ 52 (getS (cpsr : CPSR) SV = cpsr ' 28) 53 `, 54 RW_TAC std_ss [getS_def]); 55 56 57val setS_def = Define 58 `setS (cpsr : CPSR) (flag:SRS) = 59 case flag of 60 SN => (cpsr !! 0x80000000w) | 61 SZ => (cpsr !! 0x40000000w) | 62 SC => (cpsr !! 0x20000000w) | 63 SV => (cpsr !! 0x10000000w) 64 `; 65 66val setS_thm = Q.store_thm ( 67 "setS_thm", 68 `(setS (cpsr : CPSR) SN = (cpsr !! 0x80000000w)) /\ 69 (setS (cpsr : CPSR) SZ = (cpsr !! 0x40000000w)) /\ 70 (setS (cpsr : CPSR) SC = (cpsr !! 0x20000000w)) /\ 71 (setS (cpsr : CPSR) SV = (cpsr !! 0x10000000w)) 72 `, 73 RW_TAC std_ss [setS_def]); 74 75val setNZCV_def = Define 76 `setNZCV (cpsr : CPSR) (N, Z, C, V) = 77 word_modify 78 (\i b. 79 (i = 31) /\ N \/ (i = 30) /\ Z \/ (i = 29) /\ C \/ 80 (i = 28) /\ V \/ i < 28 /\ b) cpsr`; 81 82val setNZCV_thm = Q.store_thm ( 83 "setNZCV_thm", 84 `(getS (setNZCV (cpsr : CPSR) (N,Z,C,V)) SN = N) /\ 85 (getS (setNZCV (cpsr : CPSR) (N,Z,C,V)) SZ = Z) /\ 86 (getS (setNZCV (cpsr : CPSR) (N,Z,C,V)) SC = C) /\ 87 (getS (setNZCV (cpsr : CPSR) (N,Z,C,V)) SV = V)`, 88 89 RW_TAC (std_ss++fcpLib.FCP_ss++wordsLib.SIZES_ss) [getS_def, setNZCV_def, word_modify_def]); 90 91 92(*-------------------------------------------------------------------------------*) 93(* Operator *) 94(*-------------------------------------------------------------------------------*) 95 96val _ = Hol_datatype ` OPERATOR = MOV | 97 ADD | SUB | RSB | MUL | MLA | 98 AND | ORR | EOR | CMP | TST | 99 LSL | LSR | ASR | ROR | 100 LDR | STR | LDMFD | STMFD | 101 MRS | MSR | 102 B | BL 103 `; 104 105(*-------------------------------------------------------------------------------*) 106(* Condition Codes *) 107(*-------------------------------------------------------------------------------*) 108 109val _ = Hol_datatype ` COND = EQ | CS | MI | VS | HI | GE | GT | AL | 110 NE | CC | PL | VC | LS | LT | LE | NV`; 111 112(*-------------------------------------------------------------------------------*) 113(* Expressions *) 114(*-------------------------------------------------------------------------------*) 115 116val _ = type_abbrev("ADDR", Type`:word30`); 117val _ = type_abbrev("DATA", Type`:word32`); 118val _ = type_abbrev("DISTANCE", Type`:num`); 119 120val _ = Hol_datatype 121 `OFFSET = POS of DISTANCE 122 | NEG of DISTANCE 123 | INR 124 `; 125 126val _ = Hol_datatype 127 `EXP = MEM of num # OFFSET (* (register, offset) *) 128 | NCONST of num 129 | WCONST of word32 130 | REG of num 131 | WREG of num 132 `; 133 134val FP_def = 135 Define `FP = REG 11`; 136 137val IP_def = 138 Define `IP = REG 12`; 139 140val SP_def = 141 Define `SP = REG 13`; 142 143val LR_def = 144 Define `LR = REG 14`; 145 146val PC_def = 147 Define `PC = REG 15`; 148 149(*-------------------------------------------------------------------------------*) 150(* Operations *) 151(*-------------------------------------------------------------------------------*) 152 153(* An instruction: ((operator, condition code, set flags), destination, source, jump) *) 154val _ = type_abbrev("OPERATION", Type`:OPERATOR # (COND option) # bool`); 155val _ = type_abbrev("INST", Type`:OPERATION # (EXP option) # (EXP list) # (OFFSET option)`); 156 157(*---------------------------------------------------------------------------------*) 158(* State *) 159(*---------------------------------------------------------------------------------*) 160 161val _ = type_abbrev("STATE", Type`: num # CPSR # (REGISTER |-> DATA) # (ADDR |-> DATA)`); 162 163val FORALL_DSTATE = Q.store_thm 164 ("FORALL_DSTATE", 165 `(!s:(REGISTER |-> DATA) # (ADDR |-> DATA). P s) = 166 !regs mem. P (regs,mem)`, 167 SIMP_TAC std_ss [FORALL_PROD]); 168 169val FORALL_STATE = Q.store_thm 170 ("FORALL_STATE", 171 `(!s:STATE. P s) = !pc pcsr regs mem. P (pc,pcsr,(regs,mem))`, 172 SIMP_TAC std_ss [FORALL_PROD]); 173 174(*---------------------------------------------------------------------------------*) 175(* Read and write registers and memory *) 176(*---------------------------------------------------------------------------------*) 177 178val MEM_ADDR_def = Define `MEM_ADDR (addr:word32) = (31 >< 2) addr:word30`; 179 180val read_def = 181 Define ` 182 read (regs,mem) (exp:EXP) = 183 case exp of 184 MEM (r,offset) => 185 (case offset of 186 POS k => mem ' ((MEM_ADDR (regs ' (n2w r))) + (n2w k)) | 187 NEG k => mem ' ((MEM_ADDR (regs ' (n2w r))) - (n2w k)) 188 ) | 189 NCONST i => n2w i | 190 WCONST w => w | 191 REG r => regs ' (n2w:num->word4 r) 192`; 193 194val read_thm = Q.store_thm ( 195 "read_thm", 196 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (MEM_ADDR (regs ' (n2w r)) + (n2w k))) /\ 197 (read (regs,mem) (MEM (r,NEG k)) = mem ' (MEM_ADDR (regs ' (n2w r)) - (n2w k))) /\ 198 (read (regs,mem) (NCONST i) = n2w i) /\ 199 (read (regs,mem) (WCONST w) = w) /\ 200 (read (regs,mem) (REG r) = regs ' (n2w r)) /\ 201 (read (regs,mem) (MEM (r,INR)) = ARB)`, 202 RW_TAC std_ss [read_def]); 203 204val write_def = 205 Define ` 206 write (regs,mem) (exp:EXP) (v:DATA)= 207 case exp of 208 MEM (r,offset) => 209 (regs, 210 (case offset of 211 POS k => mem |+ (MEM_ADDR (regs ' (n2w r)) + (n2w k), v) | 212 NEG k => mem |+ (MEM_ADDR (regs ' (n2w r)) - (n2w k), v) 213 )) | 214 REG r => ( regs |+ ((n2w:num->REGISTER r), v), 215 mem ) | 216 _ => (regs, mem) 217 `; 218 219val write_thm = Q.store_thm ( 220 "write_thm", 221 ` (write (regs,mem) (MEM (r,POS k)) v = (regs, mem |+ (MEM_ADDR (regs ' (n2w r)) + (n2w k), v))) /\ 222 (write (regs,mem) (MEM (r,NEG k)) v = (regs, mem |+ (MEM_ADDR (regs ' (n2w r)) - (n2w k), v))) /\ 223 (write (regs,mem) (MEM (r,INR)) v = (regs,ARB)) /\ 224 (write (regs,mem) (REG r) v = (regs |+ ((n2w r), v), mem))`, 225 RW_TAC std_ss [write_def]); 226 227(*---------------------------------------------------------------------------------*) 228(* Decoding and execution of an instruction *) 229(* All instructions are executed conditionally *) 230(*---------------------------------------------------------------------------------*) 231 232val goto_def = 233 Define ` 234 goto (pc, SOME jump) = 235 case jump of 236 POS n => pc + n | 237 NEG n => pc - n | 238 INR => pc 239 `; 240 241val goto_thm = Q.store_thm ( 242 "goto_thm", 243 ` (goto (pc, SOME (POS n)) = pc + n) /\ 244 (goto (pc, SOME (NEG n)) = pc - n) /\ 245 (goto (pc, SOME INR) = pc) 246 `, 247 RW_TAC std_ss [goto_def]); 248 249 250val decode_op_def = 251 Define ` 252 decode_op (pc,cpsr,s) (op,dst,src,jump) = 253 case op of 254 MOV => (cpsr, write s (THE dst) (read s (HD src))) 255 | 256 257 (* we assume that the stack goes from low addresses to high addresses even it is "FD", 258 change LDMFD to be LDMFA if necessary *) 259 260 LDMFD => (case THE dst of 261 REG r => 262 (* We must read values from the original state instead of the updated state *) 263 (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read s (MEM(r,POS(i+1)))), i+1)) (s,0) src)) 264 | 265 WREG r => 266 (cpsr, write (FST (FOLDL (\(s1,i) reg. (write s1 reg (read s (MEM(r,POS(i+1)))), i+1)) (s,0) src)) 267 (REG r) (read s (REG r) + n2w (4*LENGTH src))) 268 ) 269 | 270 271 (* we assume that the stack goes from low addresses to high addresses even it is "FD", 272 change STMFA to be STMFD if necessary *) 273 274 STMFD => (case THE dst of 275 REG r => 276 (cpsr, 277 (* We must read values from the original state instead of the updated state *) 278 FST (FOLDL (\(s1,i) reg. (write s1 (MEM(r,NEG i)) (read s reg), i+1)) (s,0) (REVERSE src))) | 279 WREG r => 280 (cpsr, 281 write (FST (FOLDL (\(s1,i) reg. (write s1 (MEM(r,NEG i)) (read s reg), i+1)) (s,0) (REVERSE src))) 282 (REG r) (read s (REG r) - n2w (4*LENGTH src))) 283 ) 284 | 285 ADD => (cpsr, (write s (THE dst) (read s (HD src) + read s (HD (TL (src)))))) 286 | 287 SUB => (cpsr, (write s (THE dst) (read s (HD src) - read s (HD (TL (src)))))) 288 | 289 RSB => (cpsr, (write s (THE dst) (read s (HD (TL (src))) - read s (HD src)))) 290 | 291 MUL => (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src)))))) 292 | 293 MLA => (cpsr, (write s (THE dst) (read s (HD src) * read s (HD (TL (src))) + 294 read s (HD (TL (TL (src)))) ))) 295 | 296 AND => (cpsr, (write s (THE dst) (read s (HD src) && read s (HD (TL (src)))))) 297 | 298 ORR => (cpsr, (write s (THE dst) (read s (HD src) !! read s (HD (TL (src)))))) 299 | 300 EOR => (cpsr, (write s (THE dst) (read s (HD src) ?? read s (HD (TL (src)))))) 301 | 302 303 LSL => (cpsr, (write s (THE dst) 304 (read s (HD src) << w2n (read s (HD (TL (src))))))) 305 | 306 LSR => (cpsr, (write s (THE dst) 307 (read s (HD src) >>> w2n (read s (HD (TL (src))))))) 308 | 309 ASR => (cpsr, (write s (THE dst) 310 (read s (HD src) >> w2n (read s (HD (TL (src))))))) 311 | 312 ROR => (cpsr, (write s (THE dst) 313 (read s (HD src) #>> w2n (read s (HD (TL (src))))))) 314 | 315 316 CMP => (let a = read s (HD src) in 317 let b = read s (HD (TL (src))) in 318 (setNZCV cpsr (word_msb (a - b), 319 a = b, 320 b <=+ a, 321 ~(word_msb a = word_msb b) /\ ~(word_msb a = word_msb (a - b))), s)) 322 | 323 324 (* The carry flag is always set to false. This does not correspond to 325 real ARM assembler. There you could set the carry flag by passing 326 an shift as second argument. *) 327 TST => (let a = read s (HD src) in 328 let b = read s (HD (TL (src))) in 329 (setNZCV cpsr (word_msb (a && b), 330 (a && b) = 0w, 331 F, 332 cpsr ' 28), s)) 333 334 | 335 336 LDR => (cpsr, (write s (THE dst) (read s (HD src)))) 337 (* write the value in src (i.e. the memory) to the dst (i.e. the register)*) 338 | 339 340 STR => (cpsr, (write s (HD src) (read s (THE dst)))) 341 (* write the value in src (i.e. the register) to the dst (i.e. the memory)*) 342 | 343 344 MSR => (read s (HD src), s) 345 | 346 MRS => (cpsr, (write s (THE dst) cpsr)) 347 | 348 349 B => (cpsr, s) 350 | 351 BL => (cpsr, write s (REG 14) (n2w (SUC pc))) 352 `; 353 354val decode_op_thm = Q.store_thm 355("decode_op_thm", 356 `!pc cpsr s dst src jump. 357 (decode_op (pc,cpsr,s) (MOV,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\ 358 (decode_op (pc,cpsr,s) (ADD,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) + read s (HD (TL src))))) /\ 359 (decode_op (pc,cpsr,s) (SUB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) - read s (HD (TL src))))) /\ 360 (decode_op (pc,cpsr,s) (RSB,SOME dst,src,jump) = (cpsr, write s dst (read s (HD (TL src)) - read s (HD src)))) /\ 361 (decode_op (pc,cpsr,s) (MUL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) * read s (HD (TL src))))) /\ 362 (decode_op (pc,cpsr,s) (MLA,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) * read s (HD (TL src)) + read s (HD (TL (TL src)))))) /\ 363 (decode_op (pc,cpsr,s) (AND,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) && read s (HD (TL src))))) /\ 364 (decode_op (pc,cpsr,s) (ORR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) !! read s (HD (TL src))))) /\ 365 (decode_op (pc,cpsr,s) (EOR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) ?? read s (HD (TL src))))) /\ 366 (decode_op (pc,cpsr,s) (CMP,NONE,src,jump) = ( 367 let a = read s (HD src) in 368 let b = read s (HD (TL (src))) in 369 (setNZCV cpsr (word_msb (a - b), 370 a = b, 371 b <=+ a, 372 ~(word_msb a = word_msb b) /\ ~(word_msb a = word_msb (a - b))), s))) /\ 373 (decode_op (pc,cpsr,s) (TST,NONE,src,jump) = 374 (let a = read s (HD src) in 375 let b = read s (HD (TL (src))) in 376 (setNZCV cpsr (word_msb (a && b), 377 (a && b) = 0w, 378 F, 379 cpsr ' 28), s))) /\ 380 (decode_op (pc,cpsr,s) (LSL,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) << w2n (read s (HD (TL src)))))) /\ 381 (decode_op (pc,cpsr,s) (LSR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >>> w2n (read s (HD (TL src)))))) /\ 382 (decode_op (pc,cpsr,s) (ASR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) >> w2n (read s (HD (TL src)))))) /\ 383 (decode_op (pc,cpsr,s) (ROR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src) #>> w2n (read s (HD (TL src)))))) /\ 384 (decode_op (pc,cpsr,s) (LDR,SOME dst,src,jump) = (cpsr, write s dst (read s (HD src)))) /\ 385 (decode_op (pc,cpsr,s) (STR,SOME dst,src,jump) = (cpsr, write s (HD src) (read s dst))) /\ 386 (decode_op (pc,cpsr,s) (LDMFD, SOME (REG r),src,jump) = 387 (cpsr, FST (FOLDL 388 (\(s1,i) reg. 389 (write s1 reg (read s (MEM (r,POS (i + 1)))), 390 i + 1)) (s,0) src))) /\ 391 (decode_op (pc,cpsr,s) (LDMFD,SOME (WREG r),src,jump) = 392 (cpsr, write (FST 393 (FOLDL 394 (\(s1,i) reg. 395 (write s1 reg 396 (read s (MEM (r,POS (i + 1)))),i + 1)) 397 (s,0) src)) (REG r) 398 (read s (REG r) + n2w (4*LENGTH src)))) /\ 399 (decode_op (pc,cpsr,s) (STMFD,SOME (REG r),src,jump) = 400 (cpsr, FST (FOLDL 401 (\(s1,i) reg. 402 (write s1 (MEM (r,NEG i)) (read s reg),i + 1)) 403 (s,0) (REVERSE src)))) /\ 404 (decode_op (pc,cpsr,s) (STMFD,SOME (WREG r),src,jump) = 405 (cpsr, write (FST 406 (FOLDL 407 (\(s1,i) reg. 408 (write s1 (MEM (r,NEG i)) (read s reg), 409 i + 1)) (s,0) (REVERSE src))) (REG r) 410 (read s (REG r) - n2w (4*LENGTH src)))) /\ 411 (decode_op (pc,cpsr,s) (MRS,SOME dst,src,jump) = (cpsr,write s dst cpsr)) /\ 412 (decode_op (pc,cpsr,s) (MSR,NONE,src,jump) = (read s (HD src),s)) /\ 413 (decode_op (pc,cpsr,s) (B,NONE,src,jump) = (cpsr,s)) /\ 414 (decode_op (pc,cpsr,s) (BL,NONE,src,jump) = (cpsr,write s (REG 14) (n2w (SUC pc))))`, 415 416 RW_TAC std_ss [decode_op_def]); 417 418val decode_cond_cpsr_def = 419 Define `(decode_cond_cpsr cpsr EQ = getS cpsr SZ) /\ 420 (decode_cond_cpsr cpsr CS = getS cpsr SC) /\ 421 (decode_cond_cpsr cpsr MI = getS cpsr SN) /\ 422 (decode_cond_cpsr cpsr VS = getS cpsr SV) /\ 423 (decode_cond_cpsr cpsr HI = ((getS cpsr SC) /\ ~(getS cpsr SZ))) /\ 424 (decode_cond_cpsr cpsr GE = ((getS cpsr SN) = (getS cpsr SV))) /\ 425 (decode_cond_cpsr cpsr GT = (~(getS cpsr SZ) /\ ((getS cpsr SN) = (getS cpsr SV)))) /\ 426 (decode_cond_cpsr cpsr AL = T) /\ 427 (decode_cond_cpsr cpsr NE = ~(getS cpsr SZ)) /\ 428 (decode_cond_cpsr cpsr CC = ~(getS cpsr SC)) /\ 429 (decode_cond_cpsr cpsr PL = ~(getS cpsr SN)) /\ 430 (decode_cond_cpsr cpsr VC = ~(getS cpsr SV)) /\ 431 (decode_cond_cpsr cpsr LS = (~(getS cpsr SC) \/ (getS cpsr SZ))) /\ 432 (decode_cond_cpsr cpsr LT = ~((getS cpsr SN) = (getS cpsr SV))) /\ 433 (decode_cond_cpsr cpsr LE = ((getS cpsr SZ) \/ ~((getS cpsr SN) = (getS cpsr SV)))) /\ 434 (decode_cond_cpsr cpsr NV = F)` 435 436 437val decode_cond_def = 438 Define ` 439 (decode_cond ((pc,cpsr,s):STATE) (((op,cond,sflag), dst, src, jump):INST)) = 440 (case cond of 441 NONE => (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump)) 442 | 443 SOME c => 444 if (decode_cond_cpsr cpsr c) then (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump)) 445 else (pc+1, cpsr, s)) 446 `; 447 448val decode_cond_thm = Q.store_thm 449( "decode_cond_thm", 450 `!pc cpsr s op sflag dst src jump. 451 (decode_cond (pc,cpsr,s) ((op,NONE,sflag),dst,src,jump) = (pc+1, decode_op (pc,cpsr,s) (op,dst,src,jump))) /\ 452 (decode_cond (pc,cpsr,s) ((op,SOME AL,sflag),dst,src,jump) = (goto(pc,jump), decode_op (pc,cpsr,s) (op,dst,src,jump))) /\ 453 (decode_cond (pc,cpsr,s) ((op,SOME NV,sflag),dst,src,jump) = (pc+1, cpsr, s))`, 454 455 RW_TAC std_ss [decode_cond_def, decode_cond_cpsr_def]); 456 457 458 459(*---------------------------------------------------------------------------------*) 460(* Upload instructions into the instruction buffer *) 461(*---------------------------------------------------------------------------------*) 462 463(* upload and uploadCode: upload the instructions into the instruction buffer beginning from start *) 464(* By default, the code is uploaded to the buffer starting from address 0 (this is what the uploadCode describes *) 465 466val upload_def = Define ` 467 (upload (stm::stmL) iB start = upload stmL (\addr. if addr = start then stm else iB addr) (SUC start)) /\ 468 (upload ([]) iB start = iB) 469 `; 470 471 472val UPLOAD_NOT_AFFECT_LOWER = Q.store_thm ( 473 "UPLOAD_NOT_AFFECT_LOWER", 474 `!instL iB start n. n < start ==> 475 ((upload instL iB start) n = iB n)`, 476 Induct_on `instL` THEN 477 RW_TAC std_ss [upload_def] THEN 478 Induct_on `n` THEN 479 RW_TAC std_ss [upload_def] THEN 480 `SUC n < SUC start` by RW_TAC arith_ss [] THEN 481 RES_TAC THEN 482 POP_ASSUM (K ALL_TAC) THEN 483 POP_ASSUM (ASSUME_TAC o Q.SPEC `(\addr:num. if addr = start then h else iB addr)`) THEN 484 FULL_SIMP_TAC arith_ss [] 485 ); 486 487val UPLOAD_LEM = Q.store_thm ( 488 "UPLOAD_LEM", 489 `!instL iB start n. n < LENGTH instL ==> 490 ((upload instL iB start) (start+n) = EL n instL)`, 491 Induct_on `n` THEN Induct_on `instL` THEN RW_TAC list_ss [upload_def] THENL [ 492 RW_TAC arith_ss [UPLOAD_NOT_AFFECT_LOWER], 493 RES_TAC THEN 494 POP_ASSUM (ASSUME_TAC o Q.SPECL [`SUC start`,`(\addr. if addr = start then h else iB addr)`]) THEN 495 METIS_TAC [ADD_SUC, SUC_ADD_SYM, ADD_SYM] 496 ] 497 ); 498 499val UPLOAD_START_POINT_INDEPENDENT = Q.store_thm ( 500 "UPLOAD_START_POINT_INDEPENDENT", 501 `!instL start1 start2 iB addr. addr < LENGTH instL ==> 502 ((upload instL iB start1) (start1+addr) = (upload instL iB start2) (start2+addr))`, 503 RW_TAC std_ss [UPLOAD_LEM] 504 ); 505 506val uploadCode_def = 507 Define `uploadCode instL iB = upload instL iB 0`; 508 509 510val UPLOADCODE_LEM = Q.store_thm ( 511 "UPLOADCODE_LEM", 512 `!instL iB n. n < LENGTH instL ==> 513 ((uploadCode instL iB) n = EL n instL)`, 514 RW_TAC std_ss [uploadCode_def] THEN 515 IMP_RES_TAC UPLOAD_LEM THEN 516 POP_ASSUM (ASSUME_TAC o Q.SPECL [`0`,`iB`]) THEN 517 FULL_SIMP_TAC arith_ss [] 518 ); 519 520val uploadSeg_def = Define ` 521 (uploadSeg 0 segs iB = iB) /\ 522 (uploadSeg (SUC n) segs iB = 523 upload (EL n segs) (uploadSeg n segs iB) (10 * n))`; 524 525val UPLOADSEG_LEM = Q.store_thm 526 ("UPLOADSEG_LEM", 527 `!n segs instB. uploadSeg n segs instB = 528 (if n > 0 then upload (EL (PRE n) segs) (uploadSeg (PRE n) segs instB) (10 * (PRE n)) else instB)`, 529 Cases_on `n` THEN RW_TAC list_ss [uploadSeg_def] 530 ); 531 532(*---------------------------------------------------------------------------------*) 533(* Running of a ARM program *) 534(* Run the instruction in the instruction buffer for n steps *) 535(*---------------------------------------------------------------------------------*) 536 537val run_def = 538 Define 539 `run n instB P (pc,cpsr,st) = 540 if n = 0 then (pc,cpsr,st) 541 else 542 if P (pc,cpsr,st) then (pc,cpsr,st) 543 else run (n-1) instB P (decode_cond (pc,cpsr,st) (instB pc))`; 544 545val run_ind = fetch "-" "run_ind"; 546 547val RUN_LEM_1 = Q.store_thm 548 ("RUN_LEM_1", 549 `!n instB s. 550 (run (SUC n) instB P s = 551 if P s then s 552 else run n instB P (decode_cond s (instB (FST s))) 553 ) /\ 554 (run 0 instB P s = s)`, 555 SIMP_TAC list_ss [FORALL_STATE] THEN REPEAT GEN_TAC THEN 556 RW_TAC list_ss [Once run_def, LET_THM] THENL [ 557 RW_TAC list_ss [Once run_def, LET_THM], 558 RW_TAC list_ss [Once run_def, LET_THM] 559 ] 560 ); 561 562val RUN_LEM_2 = Q.store_thm 563 ("RUN_LEM_2", 564 `!n instB P s. P s ==> (run n instB P s = s)`, 565 SIMP_TAC list_ss [FORALL_STATE] THEN 566 Induct_on `n` THEN RW_TAC list_ss [RUN_LEM_1] 567 ); 568 569 570val RUN_THM_1 = Q.store_thm 571 ("RUN_THM_1", 572 `!m n s instB. 573 (run (m+n) instB P s = run n instB P (run m instB P s))`, 574 Induct_on `m` THEN REPEAT GEN_TAC THENL [ 575 RW_TAC list_ss [RUN_LEM_1], 576 `SUC m + n = SUC (m + n)` by RW_TAC list_ss [ADD_SUC] THEN 577 ASM_REWRITE_TAC [] THEN RW_TAC list_ss [RUN_LEM_1] THEN 578 RW_TAC list_ss [RUN_LEM_2] 579 ] 580 ); 581 582val _ = Globals.priming := NONE; 583 584(*---------------------------------------------------------------------------------*) 585(* An assistant theorem about LEAST *) 586(*---------------------------------------------------------------------------------*) 587 588val LEAST_ADD_LEM = Q.store_thm 589 ("LEAST_ADD_LEM", 590 `!P m. (?n. P n) /\ m <= (LEAST n. P n) ==> 591 ((LEAST n. P n) = (LEAST n. P (m + n)) + m)`, 592 Induct_on `m` THENL [ 593 RW_TAC list_ss [], 594 REPEAT STRIP_TAC THEN LEAST_ELIM_TAC THEN RW_TAC list_ss [] THENL [ 595 `(LEAST n. P n) <= n` by METIS_TAC [FULL_LEAST_INTRO] THEN 596 `n = n - SUC m + SUC m` by RW_TAC arith_ss [] THEN 597 METIS_TAC [], 598 LEAST_ELIM_TAC THEN RW_TAC list_ss [] THENL [ 599 METIS_TAC [], 600 `n'' <= n' + SUC m` by METIS_TAC [LESS_CASES] THEN 601 `(LEAST n. P n) <= n''` by METIS_TAC [FULL_LEAST_INTRO] THEN 602 `(n'' - SUC m) + SUC m = n''` by RW_TAC arith_ss [] THEN 603 `n' <= n'' - SUC m` by METIS_TAC [LESS_CASES] THEN 604 `n' + SUC m <= n''` by RW_TAC arith_ss [] THEN 605 RW_TAC arith_ss []] 606 ]] 607 ); 608 609(*----------------------------------------------------------------------------*) 610(* Assistant theorems for the FUNPOW *) 611(*----------------------------------------------------------------------------*) 612 613val FUNPOW_THM_1 = Q.store_thm 614 ("FUNPOW_THM_1", 615 ` (!f. FUNPOW f 0 = \x.x) /\ 616 (!f n. FUNPOW f (SUC n) = f o (FUNPOW f n))`, 617 RW_TAC list_ss [FUN_EQ_THM, FUNPOW_SUC] THEN 618 RW_TAC list_ss [FUNPOW] 619 ); 620 621val FUNPOW_THM_2 = Q.store_thm 622 ("FUNPOW_THM_2", 623 ` (!f. FUNPOW f 0 = \x.x) /\ 624 (!f n. FUNPOW f (SUC n) = (FUNPOW f n) o f)`, 625 RW_TAC list_ss [FUN_EQ_THM, FUNPOW] 626 ); 627 628val FUNPOW_FUNPOW = Q.store_thm 629 ("FUNPOW_FUNPOW", 630 ` !f m n. (FUNPOW f m) o (FUNPOW f n) = FUNPOW f (m+n)`, 631 Induct_on `m` THENL [ 632 RW_TAC list_ss [FUNPOW_THM_1] THEN 633 METIS_TAC [], 634 RW_TAC list_ss [FUNPOW_THM_1, GSYM SUC_ADD_SYM] 635 ] 636 ); 637 638 639(*----------------------------------------------------------------------------*) 640(* Assistant theorems for the WHILE and LEAST *) 641(* We use the "shortest" as a short-hand of the LEAST-FUNPOW *) 642(*----------------------------------------------------------------------------*) 643 644val stopAt_def = Define ` 645 stopAt P g x = 646 ?n. P (FUNPOW g n x)`; 647 648 649val shortest_def = Define ` 650 shortest P g x = 651 LEAST n. P (FUNPOW g n x)`; 652 653 654val STOPAT_THM = Q.store_thm 655 ("STOPAT_THM", 656 `!m P g x. 657 stopAt P g x /\ 658 m <= shortest P g x ==> 659 stopAt P g (FUNPOW g m x)`, 660 Cases_on `m` THENL [ 661 RW_TAC std_ss [shortest_def, stopAt_def, FUNPOW], 662 RW_TAC std_ss [stopAt_def,shortest_def] THEN 663 `~(n' < LEAST n. P (FUNPOW g n x))` by METIS_TAC [Q.SPEC `\n. P(FUNPOW g n x)` LESS_LEAST] THEN 664 `SUC n <= n'` by RW_TAC arith_ss [] THEN 665 Q.EXISTS_TAC `n' - SUC n` THEN 666 RW_TAC arith_ss [SIMP_RULE std_ss [FUN_EQ_THM] FUNPOW_FUNPOW] 667 ] 668 ); 669 670val SHORTEST_STOP = Q.store_thm 671 ("SHORTEST_STOP", 672 `!x P g. 673 stopAt P g x ==> 674 P (FUNPOW g (shortest P g x) x)`, 675 RW_TAC std_ss [stopAt_def, shortest_def] THEN 676 METIS_TAC [Q.SPECL [`\n. P (FUNPOW g n x)`,`x`] LEAST_INTRO] 677 ); 678 679val SHORTEST_LEM = Q.store_thm 680 ("SHORTEST_LEM", 681 `!x P g. 682 (P x ==> (shortest P g x = 0)) /\ 683 (stopAt P g x ==> 684 ((0 = shortest P g x) ==> P x) /\ 685 (~(P x) = 1 <= shortest P g x))`, 686 REWRITE_TAC [stopAt_def, shortest_def] THEN REPEAT GEN_TAC THEN 687 `(P x ==> ((LEAST n. P (FUNPOW g n x)) = 0))` by ALL_TAC THENL [ 688 STRIP_TAC THEN 689 `P (FUNPOW g 0 x)` by METIS_TAC [FUNPOW] THEN 690 `~(0 < (LEAST n. P (FUNPOW g n x)))` by METIS_TAC [SIMP_RULE std_ss [] (Q.SPECL [`\n.P (FUNPOW g n x)`, `0`] LESS_LEAST)] THEN 691 RW_TAC arith_ss [], 692 STRIP_TAC THENL [ 693 RW_TAC std_ss [], 694 STRIP_TAC THEN 695 `(0 = LEAST n. P (FUNPOW g n x)) ==> P x` by METIS_TAC [Q.SPEC `\n. P (FUNPOW g n x)` LEAST_EXISTS_IMP, FUNPOW] THEN 696 RW_TAC std_ss [] THEN EQ_TAC THEN STRIP_TAC THEN 697 FULL_SIMP_TAC arith_ss [] 698 ]] 699 ); 700 701val SHORTEST_THM = Q.store_thm 702 ("SHORTEST_THM", 703 `!x P g m. 704 stopAt P g x /\ 705 m <= shortest P g x ==> 706 (shortest P g x = (shortest P g (FUNPOW g m x) + m))`, 707 RW_TAC std_ss [shortest_def, stopAt_def] THEN 708 REWRITE_TAC [SIMP_RULE std_ss [FUN_EQ_THM] FUNPOW_FUNPOW] THEN 709 CONV_TAC (DEPTH_CONV (ONCE_REWRITE_CONV [Once ADD_SYM])) THEN 710 HO_MATCH_MP_TAC LEAST_ADD_LEM THEN 711 METIS_TAC [] 712 ); 713 714val SHORTEST_CASES = Q.store_thm 715 ("SHORTEST_CASES", 716 `!x P g. 717 stopAt P g x ==> 718 (P x ==> (shortest P g x = 0)) /\ 719 (~P x ==> (shortest P g x = SUC (shortest P g (g x))))`, 720 RW_TAC std_ss [] THENL [ 721 METIS_TAC [SHORTEST_LEM], 722 `1 <= shortest P g x` by METIS_TAC [SHORTEST_LEM] THEN 723 IMP_RES_TAC SHORTEST_THM THEN 724 ASSUME_TAC (DECIDE ``1 = SUC 0``) THEN 725 METIS_TAC [FUNPOW, SUC_ONE_ADD, ADD_SYM] 726 ] 727 ); 728 729val SHORTEST_INDUCTIVE = Q.store_thm 730 ("SHORTEST_INDUCTIVE", 731 `!P g x n. 732 stopAt P g x /\ 733 (shortest P g x = SUC n) ==> 734 stopAt P g (g x) /\ 735 ~(P x) /\ 736 (n = shortest P g (g x))`, 737 RW_TAC std_ss [] THENL [ 738 `SUC 0 <= shortest P g x` by RW_TAC arith_ss [] THEN 739 METIS_TAC [Q.SPEC `SUC 0` STOPAT_THM, FUNPOW], 740 `~(shortest P g x = 0)` by RW_TAC arith_ss [] THEN 741 METIS_TAC [SHORTEST_CASES], 742 `SUC 0 <= shortest P g x` by RW_TAC arith_ss [] THEN 743 IMP_RES_TAC (Q.SPECL [`x`, `P`, `g`, `SUC 0`] SHORTEST_THM) THEN 744 FULL_SIMP_TAC arith_ss [FUNPOW] 745 ] 746 ); 747 748 749(*----------------------------------------------------------------------------*) 750(* Stop when a specific condition holds *) 751(*----------------------------------------------------------------------------*) 752 753val TERD_WHILE_EQ_UNROLL = Q.store_thm 754 ("TERD_WHILE_EQ_UNROLL", 755 `!x P g. 756 stopAt P g x ==> 757 (WHILE ($~ o P) g x = FUNPOW g (shortest P g x) x)`, 758 Induct_on `shortest P g x` THENL [ 759 REWRITE_TAC [Once EQ_SYM_EQ] THEN 760 REPEAT STRIP_TAC THEN 761 IMP_RES_TAC SHORTEST_LEM THEN 762 RW_TAC std_ss [Once WHILE, FUNPOW], 763 764 REPEAT GEN_TAC THEN 765 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`P`, `g:'a ->'a`, `g (x:'a)`])) THEN 766 REWRITE_TAC [Once EQ_SYM_EQ] THEN 767 REPEAT STRIP_TAC THEN 768 `1 <= shortest P g x` by RW_TAC arith_ss [] THEN 769 IMP_RES_TAC SHORTEST_THM THEN 770 `~( P x)` by METIS_TAC [SHORTEST_LEM] THEN 771 `stopAt P g (g x)` by ALL_TAC THENL [ 772 FULL_SIMP_TAC std_ss [stopAt_def] THEN 773 Cases_on `n` THEN 774 FULL_SIMP_TAC std_ss [FUNPOW] THEN 775 METIS_TAC [], 776 PAT_ASSUM ``shortest P g x = k + 1`` (ASSUME_TAC o REWRITE_RULE [REWRITE_RULE [Once ADD_SYM] (GSYM SUC_ONE_ADD)]) THEN 777 ASSUME_TAC (DECIDE ``1 = SUC 0``) THEN 778 REWRITE_TAC [Once WHILE] THEN 779 `v = shortest P g (g x)` by METIS_TAC [FUNPOW, numTheory.INV_SUC] THEN 780 FULL_SIMP_TAC std_ss [FUNPOW] 781 ] 782 ] 783 ); 784 785(*----------------------------------------------------------------------------*) 786(* Unroll the WHILE once, stop unrolling when a condition holds *) 787(*----------------------------------------------------------------------------*) 788 789val UNROLL_ADVANCE = Q.store_thm 790 ("UNROLL_ADVANCE", 791 `!P g x. 792 stopAt P g x ==> 793 (FUNPOW g (shortest P g x) x = 794 if (P x) then x 795 else FUNPOW g (shortest P g (g x)) (g x) 796 )`, 797 RW_TAC list_ss [] THEN 798 METIS_TAC [SHORTEST_CASES, FUNPOW] 799 ); 800 801val WHILE_STILL = Q.store_thm 802 ("WHILE_STILL", 803 `!P g x. 804 stopAt P g x ==> 805 (WHILE ($~ o P) g (WHILE ($~ o P) g x) = WHILE ($~ o P) g x)`, 806 SIMP_TAC std_ss [TERD_WHILE_EQ_UNROLL] THEN 807 RW_TAC std_ss [stopAt_def, shortest_def] THEN 808 IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPEC `\n.P (FUNPOW g n x)` LEAST_EXISTS_IMP)) THEN 809 RW_TAC std_ss [Once WHILE] 810 ); 811 812 813(*---------------------------------------------------------------------------------*) 814(* Run to a particular position *) 815(* Run the instructions in the instruction buffer until the pc reaches a specific *) 816(* position. The running may not terminate and keep going on *) 817(*---------------------------------------------------------------------------------*) 818 819val _ = type_abbrev("STATEPCS", Type`:STATE # (num->bool)`); 820 821val step_def = Define ` 822 step instB = 823 \(s,pcS).(decode_cond s (instB (FST s)),FST s INSERT pcS)`; 824 825val step_FORM1 = Q.store_thm 826 ("step_FORM1", 827 `!instB. step instB = 828 \s.(decode_cond (FST s) (instB (FST (FST s))),FST (FST s) INSERT (SND s))`, 829 RW_TAC std_ss [FUN_EQ_THM] THEN 830 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 831 RW_TAC std_ss [step_def] 832 ); 833 834val STATE_PCS_SEPERATE = Q.store_thm 835 ("STATE_PCS_SEPERATE", 836 `!m pcS0 pcS1 instB s. FST (FUNPOW (step instB) m (s,pcS0)) = 837 FST (FUNPOW (step instB) m (s,pcS1))`, 838 Induct_on `m` THEN RW_TAC std_ss [FUNPOW] THEN 839 FULL_SIMP_TAC std_ss [step_def] 840 ); 841 842val STOPAT_ANY_PCS = Q.store_thm 843 ("STOPAT_ANY_PCS", 844 `!pcS0 pcS1 instB j s. 845 stopAt (\s:STATEPCS. (FST s = j)) (step instB) (s,pcS0) ==> 846 stopAt (\s:STATEPCS. (FST s = j)) (step instB) (s,pcS1)`, 847 RW_TAC std_ss [stopAt_def] THEN 848 Q.EXISTS_TAC `n` THEN 849 RW_TAC std_ss [STATE_PCS_SEPERATE] 850 ); 851 852val STOPAT_ANY_PCS_2 = Q.store_thm 853 ("STOPAT_ANY_PCS_2", 854 `!pcS0 pcS1 instB j s. 855 stopAt (\s:STATEPCS. (FST (FST s) = j)) (step instB) (s,pcS0) ==> 856 stopAt (\s:STATEPCS. (FST (FST s) = j)) (step instB) (s,pcS1)`, 857 RW_TAC std_ss [stopAt_def] THEN 858 Q.EXISTS_TAC `n` THEN 859 METIS_TAC [STATE_PCS_SEPERATE] 860 ); 861 862 863val SHORTEST_INDEPENDENT_OF_PCS = Q.store_thm 864 ("SHORTEST_INDEPENDENT_OF_PCS", 865 `!s0 s1 instB j. 866 stopAt (\s. FST (FST s) = j) (step instB) s0 /\ 867 (FST s0 = FST s1) ==> 868 (shortest (\s. FST (FST s) = j) (step instB) s0 = 869 shortest (\s. FST (FST s) = j) (step instB) s1)`, 870 Induct_on `shortest (\s. FST (FST s) = j) (step instB) s0` THENL [ 871 RW_TAC std_ss [] THEN 872 IMP_RES_TAC SHORTEST_LEM THEN 873 FULL_SIMP_TAC std_ss [] THEN 874 `(\s. FST (FST s) = j) s1` by RW_TAC std_ss [] THEN 875 IMP_RES_TAC SHORTEST_LEM THEN 876 METIS_TAC [], 877 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [] THEN 878 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 879 `?st. (?pcS0. s0 = (st,pcS0)) /\ (?pcS1. s1 = (st,pcS1))` by METIS_TAC [ABS_PAIR_THM, FST] THEN 880 Q.PAT_ASSUM `!j instB s0.p` (MP_TAC o Q.SPECL [`j`,`instB`,`step instB s0`]) THEN 881 FULL_SIMP_TAC std_ss [] THEN 882 STRIP_TAC THEN 883 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [Ntimes step_def 2] o (Q.SPEC `step instB (st,pcS1)`)) THEN 884 ASM_REWRITE_TAC [] THEN 885 IMP_RES_TAC STOPAT_ANY_PCS_2 THEN 886 `~(\s. FST (FST s) = j) (st,pcS1)` by METIS_TAC [FST] THEN 887 `SUC 0 <= shortest (\s:STATEPCS. FST (FST s) = j) (step instB) (st,pcS1)` by METIS_TAC [Q.SPECL [`(st,pcS1)`,`(\s:STATEPCS. FST (FST s) = j)`, 888 `step instB`] (INST_TYPE [alpha |-> Type`:STATEPCS`] SHORTEST_LEM), DECIDE (Term `1 = SUC 0`)] THEN 889 `shortest (\s. FST (FST s) = j) (step instB) (st,pcS1) = shortest (\s. FST (FST s) = j) (step instB) (step instB (st,pcS1)) + SUC 0` 890 by METIS_TAC [FUNPOW, SHORTEST_THM] THEN 891 RW_TAC arith_ss [] 892 ] 893 ); 894 895val runTo_def = Define ` 896 runTo instB j (s,pcS) = 897 WHILE (\(s,pcS). ~(FST s = j)) (step instB) (s,pcS)`; 898 899(*----------------------------------------------------------------------------*) 900(* A bunch of theorems about runTo *) 901(*----------------------------------------------------------------------------*) 902 903val runTo_FORM1 = Q.store_thm 904 ("runTo_FORM1", 905 `!instB j s. runTo instB j s = 906 WHILE (\s. ~(FST (FST s) = j)) (step instB) s`, 907 REPEAT GEN_TAC THEN 908 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 909 RW_TAC std_ss [runTo_def] THEN 910 `(\s:STATEPCS. ~(FST (FST s) = j)) = (\(s,pcS). ~(FST s = j))` by ALL_TAC THENL [ 911 RW_TAC std_ss [FUN_EQ_THM] THEN 912 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 913 RW_TAC std_ss [], 914 RW_TAC std_ss [] 915 ] 916 ); 917 918val RUNTO_ADVANCE = Q.store_thm 919 ("RUNTO_ADVANCE", 920 `!instB j s pcS. 921 (runTo instB j (s,pcS) = 922 if (FST s = j) then (s,pcS) 923 else runTo instB j (decode_cond s (instB (FST s)), FST s INSERT pcS) 924 )`, 925 RW_TAC list_ss [runTo_def, step_def] THENL [ 926 RW_TAC list_ss [Once WHILE], 927 RW_TAC list_ss [Once WHILE] 928 ] 929 ); 930 931val RUNTO_EXPAND_ONCE = Q.store_thm 932 ("RUNTO_EXPAND_ONCE", 933 `!instB j s. 934 (runTo instB j s = 935 if (FST (FST s) = j) then s 936 else runTo instB j (step instB s) 937 )`, 938 REPEAT STRIP_TAC THEN 939 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 940 RW_TAC list_ss [step_def, Once RUNTO_ADVANCE] 941 ); 942 943 944val UNROLL_RUNTO = Q.store_thm 945 ("UNROLL_RUNTO", 946 `!instB j s. 947 stopAt (\s:STATEPCS. (FST (FST s) = j)) (step instB) s ==> 948 (runTo instB j s = FUNPOW (step instB) (shortest (\s.(FST (FST s) = j)) (step instB) s) s)`, 949 950 RW_TAC std_ss [runTo_FORM1] THEN 951 ASSUME_TAC (INST_TYPE [alpha |-> Type `:STATEPCS`] TERD_WHILE_EQ_UNROLL) THEN 952 RES_TAC THEN 953 `$~ o (\s:STATEPCS. (FST (FST s) = j)) = (\s:STATEPCS. ~(FST (FST s) = j))` by RW_TAC std_ss [FUN_EQ_THM] THEN 954 METIS_TAC [] 955 ); 956 957 958 959val terd_def = Define ` 960 terd instB j s = 961 stopAt (\s:STATEPCS.FST (FST s) = j) (step instB) s`; 962 963 964val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss; 965 966 967val RUNTO_STATE_PCS_SEPERATE = Q.store_thm 968 ("RUNTO_STATE_PCS_SEPERATE", 969 `!j pcS0 pcS1 instB s. 970 stopAt (\s:STATEPCS.FST (FST s) = j) (step instB) (s,pcS0) ==> 971 (FST (runTo instB j (s,pcS0)) = FST (runTo instB j (s,pcS1)))`, 972 RW_TAC std_ss [UNROLL_RUNTO] THEN 973 IMP_RES_TAC STOPAT_ANY_PCS_2 THEN 974 RW_TAC std_ss [UNROLL_RUNTO] THEN 975 `FST (s,pcS0) = FST (s,pcS1)` by RW_TAC std_ss [] THEN 976 METIS_TAC [SHORTEST_INDEPENDENT_OF_PCS, STATE_PCS_SEPERATE] 977 ); 978 979 980val RUNTO_STILL = Q.store_thm 981 ("RUNTO_STILL", 982 `!j k instB s. 983 terd instB j s ==> 984 (runTo instB j (runTo instB j s) = 985 runTo instB j s)`, 986 RW_TAC std_ss [terd_def, runTo_FORM1] THEN 987 `$~ o (\s:STATEPCS. FST (FST s) = j) = (\s:STATEPCS. ~(FST (FST s) = j))` by RW_TAC std_ss [FUN_EQ_THM] THEN 988 METIS_TAC [WHILE_STILL] 989 ); 990 991 992val RUNTO_PCS_GROW = Q.store_thm 993 ("RUNTO_PCS_GROW", 994 `!n j instB s. 995 (SND s) SUBSET SND (FUNPOW (step instB) n s)`, 996 RW_TAC std_ss [terd_def] THEN 997 Q.ID_SPEC_TAC `s` THEN 998 Induct_on `n` THENL [ 999 RW_TAC std_ss [FUNPOW] THEN 1000 RW_TAC set_ss [Once step_FORM1], 1001 RW_TAC std_ss [FUNPOW] THEN 1002 FULL_SIMP_TAC std_ss [FUNPOW, SIMP_RULE std_ss [FUN_EQ_THM] FUNPOW_FUNPOW] THEN 1003 POP_ASSUM (ASSUME_TAC o Q.SPECL [`step instB s`]) THEN 1004 POP_ASSUM MP_TAC THEN 1005 RW_TAC std_ss [Once step_FORM1] THEN 1006 `SND s SUBSET (FST (FST s) INSERT SND s)` by RW_TAC set_ss [SUBSET_INSERT_RIGHT] THEN 1007 METIS_TAC [SUBSET_TRANS] 1008 ] 1009 ); 1010 1011 1012val RUNTO_PCS_MEMBERS = Q.store_thm 1013 ("RUNTO_PCS_MEMBERS", 1014 `!n m instB s. m < n ==> 1015 FST (FST (FUNPOW (step instB) m s)) IN (SND (FUNPOW(step instB) n s))`, 1016 Induct_on `n` THEN 1017 RW_TAC std_ss [] THEN 1018 Cases_on `m = n` THENL [ 1019 RW_TAC std_ss [FUNPOW_SUC] THEN 1020 Q.ABBREV_TAC `f = FUNPOW (step instB) m` THEN 1021 RW_TAC set_ss [Once step_FORM1], 1022 RW_TAC std_ss [FUNPOW_SUC] THEN 1023 `m < n` by RW_TAC arith_ss [] THEN 1024 `SND (FUNPOW (step instB) n s) SUBSET SND (FUNPOW (step instB) (SUC 0) (FUNPOW (step instB) n s))` by METIS_TAC [RUNTO_PCS_GROW] 1025 THEN FULL_SIMP_TAC set_ss [FUNPOW, SUBSET_DEF] 1026 ] 1027 ); 1028 1029val RUNTO_PCS_MEMBERS_2 = Q.store_thm 1030 ("RUNTO_PCS_MEMBERS_2", 1031 `!n m instB s pcS. m < n ==> 1032 FST (FST (FUNPOW (step instB) m (s,pcS))) IN (SND (FUNPOW(step instB) n (s,{})))`, 1033 Induct_on `n` THEN 1034 RW_TAC std_ss [] THEN 1035 Cases_on `m = n` THENL [ 1036 RW_TAC std_ss [FUNPOW_SUC] THEN 1037 Q.ABBREV_TAC `f = FUNPOW (step instB) m` THEN 1038 RW_TAC set_ss [Once step_FORM1] THEN 1039 Q.UNABBREV_TAC `f` THEN 1040 METIS_TAC [STATE_PCS_SEPERATE, FST], 1041 RW_TAC std_ss [FUNPOW_SUC] THEN 1042 `m < n` by RW_TAC arith_ss [] THEN 1043 `SND (FUNPOW (step instB) n (s,{})) SUBSET SND (FUNPOW (step instB) (SUC 0) (FUNPOW (step instB) n (s,{})))` by METIS_TAC [RUNTO_PCS_GROW] 1044 THEN FULL_SIMP_TAC set_ss [FUNPOW, SUBSET_DEF] 1045 ] 1046 ); 1047 1048val RUNTO_PCS_UNION_LEM = Q.store_thm 1049 ("RUNTO_PCS_UNION_LEM", 1050 `!n instB s pcS pcS'. 1051 pcS' SUBSET SND (FUNPOW (step instB) n (s,pcS)) ==> 1052 (SND (FUNPOW (step instB) n (s,pcS)) UNION pcS' = 1053 (SND (FUNPOW (step instB) n (s, pcS')) UNION pcS))`, 1054 Induct_on `n` THENL [ 1055 RW_TAC set_ss [FUNPOW, UNION_COMM, SUBSET_UNION_ABSORPTION], 1056 1057 RW_TAC std_ss [FUNPOW] THEN 1058 `?s1 pcS1. (step instB) (s,pcS) = (s1,pcS1)` by METIS_TAC [ABS_PAIR_THM] THEN 1059 Q.PAT_ASSUM `!instB.p` (ASSUME_TAC o Q.SPECL [`instB`,`s1`,`pcS1`, `FST (s:STATE) INSERT pcS'`]) THEN 1060 `FST (s:STATE) INSERT pcS' SUBSET SND (FUNPOW (step instB) n (s1,pcS1))` by (FULL_SIMP_TAC set_ss [step_def] THEN RW_TAC set_ss [INSERT_SUBSET, 1061 (SIMP_RULE arith_ss [step_def] o REWRITE_RULE [FUNPOW] o Q.SPECL [`SUC n`, `0`, `instB`,`(s,pcS)`]) RUNTO_PCS_MEMBERS]) THEN 1062 `step instB (s,pcS') = (s1,FST s INSERT pcS')` by FULL_SIMP_TAC std_ss [step_def] THEN 1063 RES_TAC THEN 1064 RW_TAC std_ss [] THEN 1065 `FST (s:STATE) IN SND (FUNPOW (step instB) n (s1,FST s INSERT pcS'))` by (FULL_SIMP_TAC set_ss [step_def] THEN 1066 RW_TAC set_ss [(SIMP_RULE arith_ss [step_def] o REWRITE_RULE [FUNPOW] o 1067 Q.SPECL [`SUC n`, `0`, `instB`,`(s,pcS')`]) RUNTO_PCS_MEMBERS, RUNTO_PCS_GROW]) THEN 1068 `pcS1 = FST (s:STATE) INSERT pcS` by FULL_SIMP_TAC std_ss [step_def] THEN 1069 FULL_SIMP_TAC set_ss [] THEN 1070 METIS_TAC [INSERT_UNION, UNION_COMM] 1071 ] 1072 ); 1073 1074 1075val RUNTO_PCS_UNION = Q.store_thm 1076 ("RUNTO_PCS_UNION", 1077 `!n instB s pcS. 1078 stopAt (\s:STATEPCS.FST (FST s) = j) (step instB) (s,pcS) ==> 1079 (SND (runTo instB j (s,pcS)) = 1080 (SND (runTo instB j (s, ({}))) UNION pcS))`, 1081 RW_TAC std_ss [UNROLL_RUNTO] THEN 1082 IMP_RES_TAC (Q.SPECL [`pcS`,`{}`,`instB`,`j`,`s`] STOPAT_ANY_PCS_2) THEN 1083 RW_TAC std_ss [UNROLL_RUNTO] THEN 1084 METIS_TAC [SHORTEST_INDEPENDENT_OF_PCS, RUNTO_PCS_UNION_LEM, EMPTY_SUBSET, UNION_EMPTY, FST] 1085 ); 1086 1087 1088val RUNTO_COMPOSITION_LEM = Q.store_thm 1089 ("RUNTO_COMPOSITION_LEM", 1090 `!j k instB s0 pcS0. 1091 terd instB j (s0,pcS0) ==> 1092 let (s1,pcS1) = runTo instB j (s0,pcS0) in 1093 ~(k IN ((FST s0) INSERT pcS1)) ==> 1094 (runTo instB k (s0,pcS0) = runTo instB k (s1,pcS1))`, 1095 REPEAT GEN_TAC THEN 1096 Cases_on `k = j` THENL [ 1097 RW_TAC std_ss [] THEN 1098 METIS_TAC [RUNTO_STILL], 1099 1100 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `j` THEN 1101 Q.ID_SPEC_TAC `s0` THEN Q.ID_SPEC_TAC `pcS0` THEN 1102 SIMP_TAC std_ss [terd_def, UNROLL_RUNTO, FORALL_STATE] THEN 1103 Induct_on `shortest (\s. FST (FST s) = j) (step instB) ((pc,pcsr,regs,mem),pcS0)` THENL [ 1104 REWRITE_TAC [Once EQ_SYM_EQ] THEN 1105 RW_TAC std_ss [FUNPOW], 1106 REWRITE_TAC [Once EQ_SYM_EQ] THEN 1107 REPEAT GEN_TAC THEN 1108 `?pc1 cpsr1 regs1 mem1 pcS1. step instB ((pc,pcsr,regs,mem),pcS0) = ((pc1,cpsr1,regs1,mem1),pcS1)` by METIS_TAC [ABS_PAIR_THM] THEN 1109 PAT_ASSUM ``!j instB pcsr regs mem pcS0. P`` (ASSUME_TAC o Q.SPECL [`j`,`instB`,`pc1`,`cpsr1`,`regs1`,`mem1`,`pcS1`]) THEN 1110 REPEAT STRIP_TAC THEN 1111 Q.ABBREV_TAC `s0 = (pc,pcsr,regs,mem)` THEN 1112 Q.ABBREV_TAC `s1 = (pc1,cpsr1,regs1,mem1)` THEN 1113 `1 <= shortest (\s. FST (FST s) = j) (step instB) (s0,pcS0)` by RW_TAC arith_ss [] THEN 1114 `shortest (\s. FST (FST s) = j) (step instB) (s0,pcS0) = 1115 SUC (shortest (\s. FST (FST s) = j) (step instB) (s1,pcS1))` by METIS_TAC [SHORTEST_LEM, SHORTEST_CASES] THEN 1116 ASM_REWRITE_TAC [FUNPOW] THEN 1117 FULL_SIMP_TAC std_ss [] THEN 1118 1119 `stopAt (\s. FST (FST s) = j) (step instB) (FUNPOW (step instB) (SUC 0) (s0,pcS0))` by 1120 METIS_TAC [ONE, Q.SPECL [`1`,`(\s:STATEPCS. FST (FST s) = j)`] 1121 (INST_TYPE [alpha |-> Type `:STATE # (num->bool)`] STOPAT_THM)] THEN 1122 POP_ASSUM MP_TAC THEN 1123 ASM_REWRITE_TAC [FUNPOW] THEN 1124 STRIP_TAC THEN RES_TAC THEN 1125 `?Sn pcSn. FUNPOW (step instB) v (s1,pcS1) = (Sn,pcSn)` by METIS_TAC [ABS_PAIR_THM] THEN 1126 FULL_SIMP_TAC std_ss [LET_THM] THEN 1127 STRIP_TAC THEN 1128 Q.UNABBREV_TAC `s0` THEN 1129 Cases_on `pc = k` THENL [ 1130 FULL_SIMP_TAC set_ss [], 1131 Cases_on `v` THENL [ 1132 FULL_SIMP_TAC set_ss [FUNPOW] THEN 1133 RW_TAC std_ss [runTo_def, Once WHILE], 1134 1135 ASSUME_TAC (DECIDE ``n < SUC n``) THEN 1136 `FST (FST (FUNPOW (step instB) n (s1,pcS1))) IN pcSn /\ pcS1 SUBSET SND (FUNPOW (step instB) n (s1,pcS1))` 1137 by METIS_TAC [RUNTO_PCS_GROW, RUNTO_PCS_MEMBERS, SND] THEN 1138 FULL_SIMP_TAC set_ss [] THEN 1139 ASSUME_TAC (DECIDE ``0 < SUC n``) THEN 1140 IMP_RES_TAC RUNTO_PCS_MEMBERS THEN 1141 `FST (FST (s1,pcS1)) IN SND (Sn,pcSn)` by METIS_TAC [FUNPOW] THEN 1142 Q.UNABBREV_TAC `s1` THEN 1143 FULL_SIMP_TAC set_ss [] THEN 1144 `~(k = pc1)` by (ALL_TAC THEN STRIP_TAC THEN (FULL_SIMP_TAC std_ss [IN_DEF])) THEN 1145 `runTo instB k ((pc,pcsr,regs,mem),pcS0) = runTo instB k ((pc1,cpsr1,regs1,mem1),pcS1)` by 1146 FULL_SIMP_TAC std_ss [runTo_def, Once WHILE] THEN 1147 METIS_TAC [] 1148 ] 1149 ] 1150 ] 1151 ] 1152 ); 1153 1154 1155val RUNTO_COMPOSITION = Q.store_thm 1156 ("RUNTO_COMPOSITION", 1157 `!j k instB s0 pcS0 s1 pcS1. 1158 terd instB j (s0,pcS0) /\ 1159 ((s1,pcS1) = runTo instB j (s0,pcS0)) /\ 1160 ~(k IN ((FST s0) INSERT pcS1)) ==> 1161 (runTo instB k (s0,pcS0) = runTo instB k (s1,pcS1))`, 1162 RW_TAC std_ss [] THEN 1163 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] RUNTO_COMPOSITION_LEM) THEN 1164 `?s' pcS'. runTo instB j (s0,pcS0) = (s',pcS')` by METIS_TAC [ABS_PAIR_THM] THEN 1165 FULL_SIMP_TAC std_ss [] THEN 1166 METIS_TAC [FST,SND] 1167 ); 1168 1169(*---------------------------------------------------------------------------------*) 1170(* Restriction on the modelling of registers and memory *) 1171(*---------------------------------------------------------------------------------*) 1172 1173val in_regs_dom_def = Define ` 1174 in_regs_dom regs = 1175 0 IN (FDOM regs) /\ 1 IN (FDOM regs) /\ 2 IN (FDOM regs) /\ 3 IN (FDOM regs) /\ 1176 4 IN (FDOM regs) /\ 5 IN (FDOM regs) /\ 6 IN (FDOM regs) /\ 7 IN (FDOM regs) /\ 1177 8 IN (FDOM regs) /\ 9 IN (FDOM regs) /\ 10 IN (FDOM regs) /\ 11 IN (FDOM regs) /\ 1178 12 IN (FDOM regs) /\ 13 IN (FDOM regs) /\ 14 IN (FDOM regs)`; 1179 1180 1181val in_mem_dom_def = Define ` 1182 in_mem_dom mem = 1183 !i:num. i IN (FDOM mem)`; 1184 1185 1186val FUPDATE_REFL = Q.store_thm 1187 ("FUPDATE_REFL", 1188 `!i f. i IN FDOM f ==> (f |+ (i,f ' i) = f)`, 1189 RW_TAC list_ss [fmap_EXT] THENL [ 1190 RW_TAC list_ss [FDOM_EQ_FDOM_FUPDATE], 1191 Cases_on `x = i` THEN 1192 RW_TAC list_ss [FAPPLY_FUPDATE_THM] 1193 ] 1194 ); 1195 1196(*------------------------------------------------------------------------------------------------------*) 1197(* Additional theorems for finite maps *) 1198(*------------------------------------------------------------------------------------------------------*) 1199 1200(* Sort in ascending order *) 1201val FUPDATE_LT_COMMUTES = Q.store_thm ( 1202 "FUPDATE_LT_COMMUTES", 1203 `!f a b c d. c <+ a ==> (f |+ (a, b) |+ (c,d) = f |+ (c,d) |+ (a,b))`, 1204 RW_TAC arith_ss [FUPDATE_COMMUTES, WORD_LOWER_NOT_EQ] 1205 ); 1206 1207(* Sort in descending order *) 1208val FUPDATE_GT_COMMUTES = Q.store_thm ( 1209 "FUPDATE_GT_COMMUTES", 1210 `!f a b c d. c >+ a ==> (f |+ (a,b) |+ (c,d) = f |+ (c,d) |+ (a,b))`, 1211 SIMP_TAC std_ss [WORD_HI] THEN 1212 REPEAT STRIP_TAC THEN 1213 `~(w2n c = w2n a)` by DECIDE_TAC THEN 1214 FULL_SIMP_TAC std_ss [w2n_11, FUPDATE_COMMUTES] 1215 ); 1216 1217val word4_distinct = let 1218 fun mk_word_disj_term n m = 1219 let 1220 val n_term = mk_comb (Term `n2w:num->word4`, term_of_int n); 1221 val m_term = mk_comb (Term `n2w:num->word4`, term_of_int m); 1222 in 1223 mk_neg (mk_eq (n_term, m_term)) 1224 end; 1225 1226 fun my_mk_conj (t1, t2) = if t1 = T then t2 else 1227 if t2 = T then t1 else 1228 mk_conj (t1, t2); 1229 1230 fun mk_all_disj_term t n m = 1231 let 1232 val current_term = if ((n = m) orelse (n = 0) orelse (m = 0)) then T else mk_word_disj_term (n-1) (m-1); 1233 val t' = my_mk_conj (current_term, t); 1234 in 1235 if (n = 0) then t' else 1236 if (m = 0) then mk_all_disj_term t' (n-1) (n-1) else 1237 mk_all_disj_term t' n (m-1) 1238 end; 1239 1240 val term = mk_all_disj_term T 16 16; 1241 val thm = prove (term, WORDS_TAC); 1242 in 1243 CONJ thm (GSYM thm) 1244 end; 1245val _ = save_thm ("word4_distinct", word4_distinct); 1246 1247val fupdate_lt_commutes_word4 = let 1248 val fupdate_thm = let 1249 val thm = (INST_TYPE [alpha |-> Type `:word4`] FUPDATE_COMMUTES); 1250 val (varl, _) = strip_forall (concl thm); 1251 val thm = SPEC_ALL thm; 1252 val thm = GEN (el 5 varl) thm; 1253 val thm = GEN (el 3 varl) thm; 1254 val thm = GEN (el 1 varl) thm; 1255 val thm = GEN (el 4 varl) thm; 1256 val thm = GEN (el 2 varl) thm; 1257 in thm end; 1258 1259 fun mk_fupdate_thm n m = 1260 let 1261 val n_term = mk_comb (Term `n2w:num->word4`, term_of_int n); 1262 val m_term = mk_comb (Term `n2w:num->word4`, term_of_int m); 1263 in 1264 SPECL [n_term, m_term] fupdate_thm 1265 end; 1266 1267 val (n, m) = (2, 1) 1268 val t = TRUTH 1269 fun mk_all t n m = 1270 let 1271 val current_thm = if ((n = m) orelse (n = 1) orelse (m = 0)) then TRUTH else mk_fupdate_thm (n-1) (m-1); 1272 val t' = CONJ current_thm t; 1273 in 1274 if ((n = 0) orelse (n = 1)) then t' else 1275 if (m = 0) then mk_all t' (n-1) (n-1) else 1276 mk_all t' n (m-1) 1277 end; 1278 1279 val thm = mk_all TRUTH 16 16; 1280 val thm' = REWRITE_RULE [word4_distinct] thm 1281 in 1282 thm' 1283 end; 1284 1285val _ = save_thm ("fupdate_lt_commutes_word4", fupdate_lt_commutes_word4); 1286 1287 1288val ADD_DIV = prove ( 1289``!x:num y:num n:num. 1290(0 < n) ==> 1291((x + y) DIV n = 1292 (x + (y MOD n)) DIV n + y DIV n)``, 1293 1294REPEAT STRIP_TAC THEN 1295`(x + y) DIV n = (((y DIV n) * n + (x + (y MOD n))) DIV n)` by METIS_TAC [DIVISION, ADD_COMM, ADD_ASSOC] THEN 1296POP_ASSUM (fn thm => ONCE_REWRITE_TAC[thm]) THEN 1297ASM_SIMP_TAC arith_ss [ADD_DIV_ADD_DIV]) 1298 1299val SUM_FUN_RANGE = prove ( 1300``!n f. SUM n f = SUM n (\m. if (m < n) then f m else 0)``, 1301 1302REWRITE_TAC [sum_numTheory.SUM] THEN 1303REPEAT GEN_TAC THEN 1304MATCH_MP_TAC sum_numTheory.GSUM_FUN_EQUAL THEN 1305SIMP_TAC std_ss []) 1306 1307 1308val w2n_lsr = store_thm ("w2n_lsr", 1309``(w2n (w >>> m)) = (w2n w DIV 2**m)``, 1310 1311Induct_on `m` THENL [ 1312 SIMP_TAC std_ss [SHIFT_ZERO, EXP], 1313 1314 SIMP_TAC std_ss [EXP] THEN 1315 ONCE_REWRITE_TAC[MULT_SYM] THEN 1316 SIMP_TAC std_ss [GSYM DIV_DIV_DIV_MULT] THEN 1317 POP_ASSUM (fn thm => REWRITE_TAC [GSYM thm]) THEN 1318 `(w >>> SUC m) = ((w >>> m) >>> (SUC 0))` by ALL_TAC THEN1 ( 1319 REWRITE_TAC [LSR_ADD, ADD_CLAUSES] 1320 ) THEN 1321 POP_ASSUM (fn thm => REWRITE_TAC [thm]) THEN 1322 Q.ABBREV_TAC `v = w >>> m` THEN 1323 POP_ASSUM (fn thm => ALL_TAC) THEN 1324 1325 FULL_SIMP_TAC std_ss [word_lsr_def, w2n_def] THEN 1326 `0 < dimindex (:'a)` by REWRITE_TAC [DIMINDEX_GT_0] THEN 1327 Q.ABBREV_TAC `a = dimindex (:'a)` THEN 1328 `a <= dimindex (:'a)` by ASM_SIMP_TAC arith_ss [] THEN 1329 Q.PAT_ASSUM `Abbrev x` (fn thm => ALL_TAC) THEN 1330 Induct_on `a` THENL [ 1331 SIMP_TAC std_ss [], 1332 1333 Cases_on `a` THENL [ 1334 FULL_SIMP_TAC arith_ss [sum_numTheory.SUM_def, fcpTheory.FCP_BETA, DIMINDEX_GT_0, bitTheory.SBIT_def, COND_RAND, COND_RATOR], 1335 1336 REPEAT STRIP_TAC THEN 1337 FULL_SIMP_TAC arith_ss [] THEN 1338 ONCE_REWRITE_TAC [sum_numTheory.SUM_def] THEN 1339 SIMP_TAC std_ss [] THEN 1340 `!x. ((x + SBIT (v ' SUC n) (SUC n)) DIV 2) = 1341 (x DIV 2 + SBIT (v ' SUC n) n)` by ALL_TAC THEN1 ( 1342 ONCE_REWRITE_TAC [ADD_COMM] THEN 1343 Tactical.REVERSE (`SBIT (v ' SUC n) (SUC n) = SBIT (v ' SUC n) n * 2` by ALL_TAC) THEN1 ( 1344 ASM_SIMP_TAC std_ss [ADD_DIV_ADD_DIV] 1345 ) THEN 1346 SIMP_TAC arith_ss [bitTheory.SBIT_def, COND_RATOR, COND_RAND, EXP] 1347 ) THEN 1348 POP_ASSUM (fn thm => REWRITE_TAC[thm]) THEN 1349 Q.PAT_ASSUM `a = b` (fn thm => REWRITE_TAC[GSYM thm]) THEN 1350 ONCE_REWRITE_TAC[SUM_FUN_RANGE] THEN 1351 FULL_SIMP_TAC arith_ss [fcpTheory.FCP_BETA, ADD_CLAUSES] THEN 1352 SIMP_TAC std_ss [sum_numTheory.SUM_def] THEN 1353 ONCE_REWRITE_TAC[SUM_FUN_RANGE] THEN 1354 SIMP_TAC arith_ss [bitTheory.SBIT_def, SUC_ONE_ADD] 1355 ] 1356 ] 1357]); 1358 1359val MEM_ADDR_ADD_CONST = store_thm ("MEM_ADDR_ADD_CONST", 1360``MEM_ADDR(x + n2w y) = MEM_ADDR (x + (n2w (y MOD 4))) + (MEM_ADDR (n2w y))``, 1361 ONCE_REWRITE_TAC[GSYM w2n_11] THEN 1362 REWRITE_TAC [MEM_ADDR_def] THEN 1363 WORDS_TAC THEN 1364 SIMP_TAC std_ss [SIMP_RULE std_ss [dimindex_32] (INST_TYPE [alpha |-> Type `:32`] (GSYM word_lsr_n2w))] THEN 1365 SIMP_TAC arith_ss [w2n_lsr, bitTheory.BITS_def, MOD_2EXP_def, DIV_2EXP_def, 1366 word_add_def, w2n_n2w, dimword_32] THEN 1367 `!x n m. ((0 < n) /\ (n <= m)) ==> ((x MOD n MOD m) = x MOD n)` by ALL_TAC THEN1 ( 1368 REPEAT STRIP_TAC THEN 1369 MATCH_MP_TAC LESS_MOD THEN 1370 `x MOD n < n` by ASM_SIMP_TAC arith_ss [DIVISION] THEN 1371 ASM_SIMP_TAC arith_ss [] 1372 ) THEN 1373 `(w2n x + y MOD 4294967296) MOD 4294967296 = 1374 (w2n x + y) MOD 4294967296` by ALL_TAC THEN1 ( 1375 `w2n x = w2n x MOD 4294967296` by ALL_TAC THEN1 ( 1376 MATCH_MP_TAC (GSYM LESS_MOD) THEN 1377 SIMP_TAC std_ss [w2n_lt, GSYM dimword_32] 1378 ) THEN 1379 `0 < 4294967296` by DECIDE_TAC THEN 1380 PROVE_TAC[MOD_PLUS] 1381 ) THEN 1382 ASM_SIMP_TAC std_ss [] THEN 1383 `4294967296 = 4 * 1073741824` by SIMP_TAC arith_ss [] THEN 1384 ASM_REWRITE_TAC[] THEN 1385 SIMP_TAC std_ss [GSYM DIV_MOD_MOD_DIV] THEN 1386 SIMP_TAC std_ss [MOD_PLUS] THEN 1387 `0 < 4` by DECIDE_TAC THEN 1388 METIS_TAC[ADD_DIV]); 1389 1390val MEM_ADDR_CONST_EVAL = store_thm ("MEM_ADDR_CONST_EVAL", 1391``MEM_ADDR(n2w y) = n2w (y DIV 4)``, 1392 REWRITE_TAC [MEM_ADDR_def] THEN 1393 WORDS_TAC THEN 1394 SIMP_TAC std_ss [bitTheory.BITS_def, DIV_2EXP_def, MOD_2EXP_def] THEN 1395 `!x n m. ((0 < n) /\ (n <= m)) ==> ((x MOD n MOD m) = x MOD n)` by ALL_TAC THEN1 ( 1396 REPEAT STRIP_TAC THEN 1397 MATCH_MP_TAC LESS_MOD THEN 1398 `x MOD n < n` by ASM_SIMP_TAC arith_ss [DIVISION] THEN 1399 ASM_SIMP_TAC arith_ss [] 1400 ) THEN 1401 ASM_SIMP_TAC std_ss []) 1402 1403 1404val MEM_ADDR_ADD_CONST_MOD = store_thm ("MEM_ADDR_ADD_CONST_MOD", 1405``!x y. (y MOD 4 = 0) ==> (MEM_ADDR(x + n2w y) = MEM_ADDR x + (n2w (y DIV 4)))``, 1406 REPEAT STRIP_TAC THEN 1407 ONCE_ASM_REWRITE_TAC[MEM_ADDR_ADD_CONST] THEN 1408 ASM_REWRITE_TAC[WORD_ADD_0, MEM_ADDR_CONST_EVAL]); 1409 1410 1411val MEM_ADDR_ADD_CONST_MULT = store_thm ("MEM_ADDR_ADD_CONST_MULT", 1412``!x y. (MEM_ADDR(x + n2w (y*4)) = MEM_ADDR x + (n2w y))``, 1413 REPEAT STRIP_TAC THEN 1414 ONCE_ASM_REWRITE_TAC[MEM_ADDR_ADD_CONST] THEN 1415 ASM_REWRITE_TAC[MEM_ADDR_CONST_EVAL] THEN 1416 SIMP_TAC arith_ss [MOD_EQ_0, MULT_DIV, WORD_ADD_0]); 1417 1418val _ = export_theory(); 1419