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