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