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 573val _ = Globals.priming := NONE; 574 575(*---------------------------------------------------------------------------------*) 576(* An assistant theorem about LEAST *) 577(*---------------------------------------------------------------------------------*) 578 579val LEAST_ADD_LEM = Q.store_thm 580 ("LEAST_ADD_LEM", 581 `!P m. (?n. P n) /\ m <= (LEAST n. P n) ==> 582 ((LEAST n. P n) = (LEAST n. P (m + n)) + m)`, 583 Induct_on `m` THENL [ 584 RW_TAC list_ss [], 585 REPEAT STRIP_TAC THEN LEAST_ELIM_TAC THEN RW_TAC list_ss [] THENL [ 586 `(LEAST n. P n) <= n` by METIS_TAC [FULL_LEAST_INTRO] THEN 587 `n = n - SUC m + SUC m` by RW_TAC arith_ss [] THEN 588 METIS_TAC [], 589 LEAST_ELIM_TAC THEN RW_TAC list_ss [] THENL [ 590 METIS_TAC [], 591 `n'' <= n' + SUC m` by METIS_TAC [LESS_CASES] THEN 592 `(LEAST n. P n) <= n''` by METIS_TAC [FULL_LEAST_INTRO] THEN 593 `(n'' - SUC m) + SUC m = n''` by RW_TAC arith_ss [] THEN 594 `n' <= n'' - SUC m` by METIS_TAC [LESS_CASES] THEN 595 `n' + SUC m <= n''` by RW_TAC arith_ss [] THEN 596 RW_TAC arith_ss []] 597 ]] 598 ); 599 600(*----------------------------------------------------------------------------*) 601(* Assistant theorems for the FUNPOW *) 602(*----------------------------------------------------------------------------*) 603 604val FUNPOW_THM_1 = Q.store_thm 605 ("FUNPOW_THM_1", 606 ` (!f. FUNPOW f 0 = \x.x) /\ 607 (!f n. FUNPOW f (SUC n) = f o (FUNPOW f n))`, 608 RW_TAC list_ss [FUN_EQ_THM, FUNPOW_SUC] THEN 609 RW_TAC list_ss [FUNPOW] 610 ); 611 612val FUNPOW_THM_2 = Q.store_thm 613 ("FUNPOW_THM_2", 614 ` (!f. FUNPOW f 0 = \x.x) /\ 615 (!f n. FUNPOW f (SUC n) = (FUNPOW f n) o f)`, 616 RW_TAC list_ss [FUN_EQ_THM, FUNPOW] 617 ); 618 619val FUNPOW_FUNPOW = Q.store_thm 620 ("FUNPOW_FUNPOW", 621 ` !f m n. (FUNPOW f m) o (FUNPOW f n) = FUNPOW f (m+n)`, 622 Induct_on `m` THENL [ 623 RW_TAC list_ss [FUNPOW_THM_1] THEN 624 METIS_TAC [], 625 RW_TAC list_ss [FUNPOW_THM_1, GSYM SUC_ADD_SYM] 626 ] 627 ); 628 629 630(*----------------------------------------------------------------------------*) 631(* Assistant theorems for the WHILE and LEAST *) 632(* We use the "shortest" as a short-hand of the LEAST-FUNPOW *) 633(*----------------------------------------------------------------------------*) 634 635val stopAt_def = Define ` 636 stopAt P g x = 637 ?n. P (FUNPOW g n x)`; 638 639 640val shortest_def = Define ` 641 shortest P g x = 642 LEAST n. P (FUNPOW g n x)`; 643 644 645val STOPAT_THM = Q.store_thm 646 ("STOPAT_THM", 647 `!m P g x. 648 stopAt P g x /\ 649 m <= shortest P g x ==> 650 stopAt P g (FUNPOW g m x)`, 651 Cases_on `m` THENL [ 652 RW_TAC std_ss [shortest_def, stopAt_def, FUNPOW], 653 RW_TAC std_ss [stopAt_def,shortest_def] THEN 654 `~(n' < LEAST n. P (FUNPOW g n x))` by METIS_TAC [Q.SPEC `\n. P(FUNPOW g n x)` LESS_LEAST] THEN 655 `SUC n <= n'` by RW_TAC arith_ss [] THEN 656 Q.EXISTS_TAC `n' - SUC n` THEN 657 RW_TAC arith_ss [SIMP_RULE std_ss [FUN_EQ_THM] FUNPOW_FUNPOW] 658 ] 659 ); 660 661val SHORTEST_STOP = Q.store_thm 662 ("SHORTEST_STOP", 663 `!x P g. 664 stopAt P g x ==> 665 P (FUNPOW g (shortest P g x) x)`, 666 RW_TAC std_ss [stopAt_def, shortest_def] THEN 667 METIS_TAC [Q.SPECL [`\n. P (FUNPOW g n x)`,`x`] LEAST_INTRO] 668 ); 669 670val SHORTEST_LEM = Q.store_thm 671 ("SHORTEST_LEM", 672 `!x P g. 673 (P x ==> (shortest P g x = 0)) /\ 674 (stopAt P g x ==> 675 ((0 = shortest P g x) ==> P x) /\ 676 (~(P x) = 1 <= shortest P g x))`, 677 REWRITE_TAC [stopAt_def, shortest_def] THEN REPEAT GEN_TAC THEN 678 `(P x ==> ((LEAST n. P (FUNPOW g n x)) = 0))` by ALL_TAC THENL [ 679 STRIP_TAC THEN 680 `P (FUNPOW g 0 x)` by METIS_TAC [FUNPOW] THEN 681 `~(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 682 RW_TAC arith_ss [], 683 STRIP_TAC THENL [ 684 RW_TAC std_ss [], 685 STRIP_TAC THEN 686 `(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 687 RW_TAC std_ss [] THEN EQ_TAC THEN STRIP_TAC THEN 688 FULL_SIMP_TAC arith_ss [] 689 ]] 690 ); 691 692val SHORTEST_THM = Q.store_thm 693 ("SHORTEST_THM", 694 `!x P g m. 695 stopAt P g x /\ 696 m <= shortest P g x ==> 697 (shortest P g x = (shortest P g (FUNPOW g m x) + m))`, 698 RW_TAC std_ss [shortest_def, stopAt_def] THEN 699 REWRITE_TAC [SIMP_RULE std_ss [FUN_EQ_THM] FUNPOW_FUNPOW] THEN 700 CONV_TAC (DEPTH_CONV (ONCE_REWRITE_CONV [Once ADD_SYM])) THEN 701 HO_MATCH_MP_TAC LEAST_ADD_LEM THEN 702 METIS_TAC [] 703 ); 704 705val SHORTEST_CASES = Q.store_thm 706 ("SHORTEST_CASES", 707 `!x P g. 708 stopAt P g x ==> 709 (P x ==> (shortest P g x = 0)) /\ 710 (~P x ==> (shortest P g x = SUC (shortest P g (g x))))`, 711 RW_TAC std_ss [] THENL [ 712 METIS_TAC [SHORTEST_LEM], 713 `1 <= shortest P g x` by METIS_TAC [SHORTEST_LEM] THEN 714 IMP_RES_TAC SHORTEST_THM THEN 715 ASSUME_TAC (DECIDE ``1 = SUC 0``) THEN 716 METIS_TAC [FUNPOW, SUC_ONE_ADD, ADD_SYM] 717 ] 718 ); 719 720val SHORTEST_INDUCTIVE = Q.store_thm 721 ("SHORTEST_INDUCTIVE", 722 `!P g x n. 723 stopAt P g x /\ 724 (shortest P g x = SUC n) ==> 725 stopAt P g (g x) /\ 726 ~(P x) /\ 727 (n = shortest P g (g x))`, 728 RW_TAC std_ss [] THENL [ 729 `SUC 0 <= shortest P g x` by RW_TAC arith_ss [] THEN 730 METIS_TAC [Q.SPEC `SUC 0` STOPAT_THM, FUNPOW], 731 `~(shortest P g x = 0)` by RW_TAC arith_ss [] THEN 732 METIS_TAC [SHORTEST_CASES], 733 `SUC 0 <= shortest P g x` by RW_TAC arith_ss [] THEN 734 IMP_RES_TAC (Q.SPECL [`x`, `P`, `g`, `SUC 0`] SHORTEST_THM) THEN 735 FULL_SIMP_TAC arith_ss [FUNPOW] 736 ] 737 ); 738 739 740(*----------------------------------------------------------------------------*) 741(* Stop when a specific condition holds *) 742(*----------------------------------------------------------------------------*) 743 744val TERD_WHILE_EQ_UNROLL = Q.store_thm 745 ("TERD_WHILE_EQ_UNROLL", 746 `!x P g. 747 stopAt P g x ==> 748 (WHILE ($~ o P) g x = FUNPOW g (shortest P g x) x)`, 749 Induct_on `shortest P g x` THENL [ 750 REWRITE_TAC [Once EQ_SYM_EQ] THEN 751 REPEAT STRIP_TAC THEN 752 IMP_RES_TAC SHORTEST_LEM THEN 753 RW_TAC std_ss [Once WHILE, FUNPOW], 754 755 REPEAT GEN_TAC THEN 756 POP_ASSUM (ASSUME_TAC o (Q.SPECL [`P`, `g:'a ->'a`, `g (x:'a)`])) THEN 757 REWRITE_TAC [Once EQ_SYM_EQ] THEN 758 REPEAT STRIP_TAC THEN 759 `1 <= shortest P g x` by RW_TAC arith_ss [] THEN 760 IMP_RES_TAC SHORTEST_THM THEN 761 `~( P x)` by METIS_TAC [SHORTEST_LEM] THEN 762 `stopAt P g (g x)` by ALL_TAC THENL [ 763 FULL_SIMP_TAC std_ss [stopAt_def] THEN 764 Cases_on `n` THEN 765 FULL_SIMP_TAC std_ss [FUNPOW] THEN 766 METIS_TAC [], 767 PAT_ASSUM ``shortest P g x = k + 1`` (ASSUME_TAC o REWRITE_RULE [REWRITE_RULE [Once ADD_SYM] (GSYM SUC_ONE_ADD)]) THEN 768 ASSUME_TAC (DECIDE ``1 = SUC 0``) THEN 769 REWRITE_TAC [Once WHILE] THEN 770 `v = shortest P g (g x)` by METIS_TAC [FUNPOW, numTheory.INV_SUC] THEN 771 FULL_SIMP_TAC std_ss [FUNPOW] 772 ] 773 ] 774 ); 775 776(*----------------------------------------------------------------------------*) 777(* Unroll the WHILE once, stop unrolling when a condition holds *) 778(*----------------------------------------------------------------------------*) 779 780val UNROLL_ADVANCE = Q.store_thm 781 ("UNROLL_ADVANCE", 782 `!P g x. 783 stopAt P g x ==> 784 (FUNPOW g (shortest P g x) x = 785 if (P x) then x 786 else FUNPOW g (shortest P g (g x)) (g x) 787 )`, 788 RW_TAC list_ss [] THEN 789 METIS_TAC [SHORTEST_CASES, FUNPOW] 790 ); 791 792val WHILE_STILL = Q.store_thm 793 ("WHILE_STILL", 794 `!P g x. 795 stopAt P g x ==> 796 (WHILE ($~ o P) g (WHILE ($~ o P) g x) = WHILE ($~ o P) g x)`, 797 SIMP_TAC std_ss [TERD_WHILE_EQ_UNROLL] THEN 798 RW_TAC std_ss [stopAt_def, shortest_def] THEN 799 IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPEC `\n.P (FUNPOW g n x)` LEAST_EXISTS_IMP)) THEN 800 RW_TAC std_ss [Once WHILE] 801 ); 802 803 804(*---------------------------------------------------------------------------------*) 805(* Run to a particular position *) 806(* Run the instructions in the instruction buffer until the pc reaches a specific *) 807(* position. The running may not terminate and keep going on *) 808(*---------------------------------------------------------------------------------*) 809 810val _ = type_abbrev("STATEPCS", Type`:STATE # (num->bool)`); 811 812val step_def = Define ` 813 step instB = 814 \(s,pcS).(decode_cond s (instB (FST s)),FST s INSERT pcS)`; 815 816val step_FORM1 = Q.store_thm 817 ("step_FORM1", 818 `!instB. step instB = 819 \s.(decode_cond (FST s) (instB (FST (FST s))),FST (FST s) INSERT (SND s))`, 820 RW_TAC std_ss [FUN_EQ_THM] THEN 821 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 822 RW_TAC std_ss [step_def] 823 ); 824 825val STATE_PCS_SEPERATE = Q.store_thm 826 ("STATE_PCS_SEPERATE", 827 `!m pcS0 pcS1 instB s. FST (FUNPOW (step instB) m (s,pcS0)) = 828 FST (FUNPOW (step instB) m (s,pcS1))`, 829 Induct_on `m` THEN RW_TAC std_ss [FUNPOW] THEN 830 FULL_SIMP_TAC std_ss [step_def] 831 ); 832 833val STOPAT_ANY_PCS = Q.store_thm 834 ("STOPAT_ANY_PCS", 835 `!pcS0 pcS1 instB j s. 836 stopAt (\s:STATEPCS. (FST s = j)) (step instB) (s,pcS0) ==> 837 stopAt (\s:STATEPCS. (FST s = j)) (step instB) (s,pcS1)`, 838 RW_TAC std_ss [stopAt_def] THEN 839 Q.EXISTS_TAC `n` THEN 840 RW_TAC std_ss [STATE_PCS_SEPERATE] 841 ); 842 843val STOPAT_ANY_PCS_2 = Q.store_thm 844 ("STOPAT_ANY_PCS_2", 845 `!pcS0 pcS1 instB j s. 846 stopAt (\s:STATEPCS. (FST (FST s) = j)) (step instB) (s,pcS0) ==> 847 stopAt (\s:STATEPCS. (FST (FST s) = j)) (step instB) (s,pcS1)`, 848 RW_TAC std_ss [stopAt_def] THEN 849 Q.EXISTS_TAC `n` THEN 850 METIS_TAC [STATE_PCS_SEPERATE] 851 ); 852 853 854val SHORTEST_INDEPENDENT_OF_PCS = Q.store_thm 855 ("SHORTEST_INDEPENDENT_OF_PCS", 856 `!s0 s1 instB j. 857 stopAt (\s. FST (FST s) = j) (step instB) s0 /\ 858 (FST s0 = FST s1) ==> 859 (shortest (\s. FST (FST s) = j) (step instB) s0 = 860 shortest (\s. FST (FST s) = j) (step instB) s1)`, 861 Induct_on `shortest (\s. FST (FST s) = j) (step instB) s0` THENL [ 862 RW_TAC std_ss [] THEN 863 IMP_RES_TAC SHORTEST_LEM THEN 864 FULL_SIMP_TAC std_ss [] THEN 865 `(\s. FST (FST s) = j) s1` by RW_TAC std_ss [] THEN 866 IMP_RES_TAC SHORTEST_LEM THEN 867 METIS_TAC [], 868 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [] THEN 869 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 870 `?st. (?pcS0. s0 = (st,pcS0)) /\ (?pcS1. s1 = (st,pcS1))` by METIS_TAC [ABS_PAIR_THM, FST] THEN 871 Q.PAT_ASSUM `!j instB s0.p` (MP_TAC o Q.SPECL [`j`,`instB`,`step instB s0`]) THEN 872 FULL_SIMP_TAC std_ss [] THEN 873 STRIP_TAC THEN 874 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [Ntimes step_def 2] o (Q.SPEC `step instB (st,pcS1)`)) THEN 875 ASM_REWRITE_TAC [] THEN 876 IMP_RES_TAC STOPAT_ANY_PCS_2 THEN 877 `~(\s. FST (FST s) = j) (st,pcS1)` by METIS_TAC [FST] THEN 878 `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)`, 879 `step instB`] (INST_TYPE [alpha |-> Type`:STATEPCS`] SHORTEST_LEM), DECIDE (Term `1 = SUC 0`)] THEN 880 `shortest (\s. FST (FST s) = j) (step instB) (st,pcS1) = shortest (\s. FST (FST s) = j) (step instB) (step instB (st,pcS1)) + SUC 0` 881 by METIS_TAC [FUNPOW, SHORTEST_THM] THEN 882 RW_TAC arith_ss [] 883 ] 884 ); 885 886val runTo_def = Define ` 887 runTo instB j (s,pcS) = 888 WHILE (\(s,pcS). ~(FST s = j)) (step instB) (s,pcS)`; 889 890(*----------------------------------------------------------------------------*) 891(* A bunch of theorems about runTo *) 892(*----------------------------------------------------------------------------*) 893 894val runTo_FORM1 = Q.store_thm 895 ("runTo_FORM1", 896 `!instB j s. runTo instB j s = 897 WHILE (\s. ~(FST (FST s) = j)) (step instB) s`, 898 REPEAT GEN_TAC THEN 899 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 900 RW_TAC std_ss [runTo_def] THEN 901 `(\s:STATEPCS. ~(FST (FST s) = j)) = (\(s,pcS). ~(FST s = j))` by ALL_TAC THENL [ 902 RW_TAC std_ss [FUN_EQ_THM] THEN 903 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 904 RW_TAC std_ss [], 905 RW_TAC std_ss [] 906 ] 907 ); 908 909val RUNTO_ADVANCE = Q.store_thm 910 ("RUNTO_ADVANCE", 911 `!instB j s pcS. 912 (runTo instB j (s,pcS) = 913 if (FST s = j) then (s,pcS) 914 else runTo instB j (decode_cond s (instB (FST s)), FST s INSERT pcS) 915 )`, 916 RW_TAC list_ss [runTo_def, step_def] THENL [ 917 RW_TAC list_ss [Once WHILE], 918 RW_TAC list_ss [Once WHILE] 919 ] 920 ); 921 922val RUNTO_EXPAND_ONCE = Q.store_thm 923 ("RUNTO_EXPAND_ONCE", 924 `!instB j s. 925 (runTo instB j s = 926 if (FST (FST s) = j) then s 927 else runTo instB j (step instB s) 928 )`, 929 REPEAT STRIP_TAC THEN 930 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 931 RW_TAC list_ss [step_def, Once RUNTO_ADVANCE] 932 ); 933 934 935val UNROLL_RUNTO = Q.store_thm 936 ("UNROLL_RUNTO", 937 `!instB j s. 938 stopAt (\s:STATEPCS. (FST (FST s) = j)) (step instB) s ==> 939 (runTo instB j s = FUNPOW (step instB) (shortest (\s.(FST (FST s) = j)) (step instB) s) s)`, 940 941 RW_TAC std_ss [runTo_FORM1] THEN 942 ASSUME_TAC (INST_TYPE [alpha |-> Type `:STATEPCS`] TERD_WHILE_EQ_UNROLL) THEN 943 RES_TAC THEN 944 `$~ o (\s:STATEPCS. (FST (FST s) = j)) = (\s:STATEPCS. ~(FST (FST s) = j))` by RW_TAC std_ss [FUN_EQ_THM] THEN 945 METIS_TAC [] 946 ); 947 948 949 950val terd_def = Define ` 951 terd instB j s = 952 stopAt (\s:STATEPCS.FST (FST s) = j) (step instB) s`; 953 954 955val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss; 956 957 958val RUNTO_STATE_PCS_SEPERATE = Q.store_thm 959 ("RUNTO_STATE_PCS_SEPERATE", 960 `!j pcS0 pcS1 instB s. 961 stopAt (\s:STATEPCS.FST (FST s) = j) (step instB) (s,pcS0) ==> 962 (FST (runTo instB j (s,pcS0)) = FST (runTo instB j (s,pcS1)))`, 963 RW_TAC std_ss [UNROLL_RUNTO] THEN 964 IMP_RES_TAC STOPAT_ANY_PCS_2 THEN 965 RW_TAC std_ss [UNROLL_RUNTO] THEN 966 `FST (s,pcS0) = FST (s,pcS1)` by RW_TAC std_ss [] THEN 967 METIS_TAC [SHORTEST_INDEPENDENT_OF_PCS, STATE_PCS_SEPERATE] 968 ); 969 970 971val RUNTO_STILL = Q.store_thm 972 ("RUNTO_STILL", 973 `!j k instB s. 974 terd instB j s ==> 975 (runTo instB j (runTo instB j s) = 976 runTo instB j s)`, 977 RW_TAC std_ss [terd_def, runTo_FORM1] THEN 978 `$~ o (\s:STATEPCS. FST (FST s) = j) = (\s:STATEPCS. ~(FST (FST s) = j))` by RW_TAC std_ss [FUN_EQ_THM] THEN 979 METIS_TAC [WHILE_STILL] 980 ); 981 982 983val RUNTO_PCS_GROW = Q.store_thm 984 ("RUNTO_PCS_GROW", 985 `!n j instB s. 986 (SND s) SUBSET SND (FUNPOW (step instB) n s)`, 987 RW_TAC std_ss [terd_def] THEN 988 Q.ID_SPEC_TAC `s` THEN 989 Induct_on `n` THENL [ 990 RW_TAC std_ss [FUNPOW] THEN 991 RW_TAC set_ss [Once step_FORM1], 992 RW_TAC std_ss [FUNPOW] THEN 993 FULL_SIMP_TAC std_ss [FUNPOW, SIMP_RULE std_ss [FUN_EQ_THM] FUNPOW_FUNPOW] THEN 994 POP_ASSUM (ASSUME_TAC o Q.SPECL [`step instB s`]) THEN 995 POP_ASSUM MP_TAC THEN 996 RW_TAC std_ss [Once step_FORM1] THEN 997 `SND s SUBSET (FST (FST s) INSERT SND s)` by RW_TAC set_ss [SUBSET_INSERT_RIGHT] THEN 998 METIS_TAC [SUBSET_TRANS] 999 ] 1000 ); 1001 1002 1003val RUNTO_PCS_MEMBERS = Q.store_thm 1004 ("RUNTO_PCS_MEMBERS", 1005 `!n m instB s. m < n ==> 1006 FST (FST (FUNPOW (step instB) m s)) IN (SND (FUNPOW(step instB) n s))`, 1007 Induct_on `n` THEN 1008 RW_TAC std_ss [] THEN 1009 Cases_on `m = n` THENL [ 1010 RW_TAC std_ss [FUNPOW_SUC] THEN 1011 Q.ABBREV_TAC `f = FUNPOW (step instB) m` THEN 1012 RW_TAC set_ss [Once step_FORM1], 1013 RW_TAC std_ss [FUNPOW_SUC] THEN 1014 `m < n` by RW_TAC arith_ss [] THEN 1015 `SND (FUNPOW (step instB) n s) SUBSET SND (FUNPOW (step instB) (SUC 0) (FUNPOW (step instB) n s))` by METIS_TAC [RUNTO_PCS_GROW] 1016 THEN FULL_SIMP_TAC set_ss [FUNPOW, SUBSET_DEF] 1017 ] 1018 ); 1019 1020val RUNTO_PCS_MEMBERS_2 = Q.store_thm 1021 ("RUNTO_PCS_MEMBERS_2", 1022 `!n m instB s pcS. m < n ==> 1023 FST (FST (FUNPOW (step instB) m (s,pcS))) IN (SND (FUNPOW(step instB) n (s,{})))`, 1024 Induct_on `n` THEN 1025 RW_TAC std_ss [] THEN 1026 Cases_on `m = n` THENL [ 1027 RW_TAC std_ss [FUNPOW_SUC] THEN 1028 Q.ABBREV_TAC `f = FUNPOW (step instB) m` THEN 1029 RW_TAC set_ss [Once step_FORM1] THEN 1030 Q.UNABBREV_TAC `f` THEN 1031 METIS_TAC [STATE_PCS_SEPERATE, FST], 1032 RW_TAC std_ss [FUNPOW_SUC] THEN 1033 `m < n` by RW_TAC arith_ss [] THEN 1034 `SND (FUNPOW (step instB) n (s,{})) SUBSET SND (FUNPOW (step instB) (SUC 0) (FUNPOW (step instB) n (s,{})))` by METIS_TAC [RUNTO_PCS_GROW] 1035 THEN FULL_SIMP_TAC set_ss [FUNPOW, SUBSET_DEF] 1036 ] 1037 ); 1038 1039val RUNTO_PCS_UNION_LEM = Q.store_thm 1040 ("RUNTO_PCS_UNION_LEM", 1041 `!n instB s pcS pcS'. 1042 pcS' SUBSET SND (FUNPOW (step instB) n (s,pcS)) ==> 1043 (SND (FUNPOW (step instB) n (s,pcS)) UNION pcS' = 1044 (SND (FUNPOW (step instB) n (s, pcS')) UNION pcS))`, 1045 Induct_on `n` THENL [ 1046 RW_TAC set_ss [FUNPOW, UNION_COMM, SUBSET_UNION_ABSORPTION], 1047 1048 RW_TAC std_ss [FUNPOW] THEN 1049 `?s1 pcS1. (step instB) (s,pcS) = (s1,pcS1)` by METIS_TAC [ABS_PAIR_THM] THEN 1050 Q.PAT_ASSUM `!instB.p` (ASSUME_TAC o Q.SPECL [`instB`,`s1`,`pcS1`, `FST (s:STATE) INSERT pcS'`]) THEN 1051 `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, 1052 (SIMP_RULE arith_ss [step_def] o REWRITE_RULE [FUNPOW] o Q.SPECL [`SUC n`, `0`, `instB`,`(s,pcS)`]) RUNTO_PCS_MEMBERS]) THEN 1053 `step instB (s,pcS') = (s1,FST s INSERT pcS')` by FULL_SIMP_TAC std_ss [step_def] THEN 1054 RES_TAC THEN 1055 RW_TAC std_ss [] THEN 1056 `FST (s:STATE) IN SND (FUNPOW (step instB) n (s1,FST s INSERT pcS'))` by (FULL_SIMP_TAC set_ss [step_def] THEN 1057 RW_TAC set_ss [(SIMP_RULE arith_ss [step_def] o REWRITE_RULE [FUNPOW] o 1058 Q.SPECL [`SUC n`, `0`, `instB`,`(s,pcS')`]) RUNTO_PCS_MEMBERS, RUNTO_PCS_GROW]) THEN 1059 `pcS1 = FST (s:STATE) INSERT pcS` by FULL_SIMP_TAC std_ss [step_def] THEN 1060 FULL_SIMP_TAC set_ss [] THEN 1061 METIS_TAC [INSERT_UNION, UNION_COMM] 1062 ] 1063 ); 1064 1065 1066val RUNTO_PCS_UNION = Q.store_thm 1067 ("RUNTO_PCS_UNION", 1068 `!n instB s pcS. 1069 stopAt (\s:STATEPCS.FST (FST s) = j) (step instB) (s,pcS) ==> 1070 (SND (runTo instB j (s,pcS)) = 1071 (SND (runTo instB j (s, ({}))) UNION pcS))`, 1072 RW_TAC std_ss [UNROLL_RUNTO] THEN 1073 IMP_RES_TAC (Q.SPECL [`pcS`,`{}`,`instB`,`j`,`s`] STOPAT_ANY_PCS_2) THEN 1074 RW_TAC std_ss [UNROLL_RUNTO] THEN 1075 METIS_TAC [SHORTEST_INDEPENDENT_OF_PCS, RUNTO_PCS_UNION_LEM, EMPTY_SUBSET, UNION_EMPTY, FST] 1076 ); 1077 1078 1079val RUNTO_COMPOSITION_LEM = Q.store_thm 1080 ("RUNTO_COMPOSITION_LEM", 1081 `!j k instB s0 pcS0. 1082 terd instB j (s0,pcS0) ==> 1083 let (s1,pcS1) = runTo instB j (s0,pcS0) in 1084 ~(k IN ((FST s0) INSERT pcS1)) ==> 1085 (runTo instB k (s0,pcS0) = runTo instB k (s1,pcS1))`, 1086 REPEAT GEN_TAC THEN 1087 Cases_on `k = j` THENL [ 1088 RW_TAC std_ss [] THEN 1089 METIS_TAC [RUNTO_STILL], 1090 1091 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `j` THEN 1092 Q.ID_SPEC_TAC `s0` THEN Q.ID_SPEC_TAC `pcS0` THEN 1093 SIMP_TAC std_ss [terd_def, UNROLL_RUNTO, FORALL_STATE] THEN 1094 Induct_on `shortest (\s. FST (FST s) = j) (step instB) ((pc,pcsr,regs,mem),pcS0)` THENL [ 1095 REWRITE_TAC [Once EQ_SYM_EQ] THEN 1096 RW_TAC std_ss [FUNPOW], 1097 REWRITE_TAC [Once EQ_SYM_EQ] THEN 1098 REPEAT GEN_TAC THEN 1099 `?pc1 cpsr1 regs1 mem1 pcS1. step instB ((pc,pcsr,regs,mem),pcS0) = ((pc1,cpsr1,regs1,mem1),pcS1)` by METIS_TAC [ABS_PAIR_THM] THEN 1100 PAT_ASSUM ``!j instB pcsr regs mem pcS0. P`` (ASSUME_TAC o Q.SPECL [`j`,`instB`,`pc1`,`cpsr1`,`regs1`,`mem1`,`pcS1`]) THEN 1101 REPEAT STRIP_TAC THEN 1102 Q.ABBREV_TAC `s0 = (pc,pcsr,regs,mem)` THEN 1103 Q.ABBREV_TAC `s1 = (pc1,cpsr1,regs1,mem1)` THEN 1104 `1 <= shortest (\s. FST (FST s) = j) (step instB) (s0,pcS0)` by RW_TAC arith_ss [] THEN 1105 `shortest (\s. FST (FST s) = j) (step instB) (s0,pcS0) = 1106 SUC (shortest (\s. FST (FST s) = j) (step instB) (s1,pcS1))` by METIS_TAC [SHORTEST_LEM, SHORTEST_CASES] THEN 1107 ASM_REWRITE_TAC [FUNPOW] THEN 1108 FULL_SIMP_TAC std_ss [] THEN 1109 1110 `stopAt (\s. FST (FST s) = j) (step instB) (FUNPOW (step instB) (SUC 0) (s0,pcS0))` by 1111 METIS_TAC [ONE, Q.SPECL [`1`,`(\s:STATEPCS. FST (FST s) = j)`] 1112 (INST_TYPE [alpha |-> Type `:STATE # (num->bool)`] STOPAT_THM)] THEN 1113 POP_ASSUM MP_TAC THEN 1114 ASM_REWRITE_TAC [FUNPOW] THEN 1115 STRIP_TAC THEN RES_TAC THEN 1116 `?Sn pcSn. FUNPOW (step instB) v (s1,pcS1) = (Sn,pcSn)` by METIS_TAC [ABS_PAIR_THM] THEN 1117 FULL_SIMP_TAC std_ss [LET_THM] THEN 1118 STRIP_TAC THEN 1119 Q.UNABBREV_TAC `s0` THEN 1120 Cases_on `pc = k` THENL [ 1121 FULL_SIMP_TAC set_ss [], 1122 Cases_on `v` THENL [ 1123 FULL_SIMP_TAC set_ss [FUNPOW] THEN 1124 RW_TAC std_ss [runTo_def, Once WHILE], 1125 1126 ASSUME_TAC (DECIDE ``n < SUC n``) THEN 1127 `FST (FST (FUNPOW (step instB) n (s1,pcS1))) IN pcSn /\ pcS1 SUBSET SND (FUNPOW (step instB) n (s1,pcS1))` 1128 by METIS_TAC [RUNTO_PCS_GROW, RUNTO_PCS_MEMBERS, SND] THEN 1129 FULL_SIMP_TAC set_ss [] THEN 1130 ASSUME_TAC (DECIDE ``0 < SUC n``) THEN 1131 IMP_RES_TAC RUNTO_PCS_MEMBERS THEN 1132 `FST (FST (s1,pcS1)) IN SND (Sn,pcSn)` by METIS_TAC [FUNPOW] THEN 1133 Q.UNABBREV_TAC `s1` THEN 1134 FULL_SIMP_TAC set_ss [] THEN 1135 `~(k = pc1)` by (ALL_TAC THEN STRIP_TAC THEN (FULL_SIMP_TAC std_ss [IN_DEF])) THEN 1136 `runTo instB k ((pc,pcsr,regs,mem),pcS0) = runTo instB k ((pc1,cpsr1,regs1,mem1),pcS1)` by 1137 FULL_SIMP_TAC std_ss [runTo_def, Once WHILE] THEN 1138 METIS_TAC [] 1139 ] 1140 ] 1141 ] 1142 ] 1143 ); 1144 1145 1146val RUNTO_COMPOSITION = Q.store_thm 1147 ("RUNTO_COMPOSITION", 1148 `!j k instB s0 pcS0 s1 pcS1. 1149 terd instB j (s0,pcS0) /\ 1150 ((s1,pcS1) = runTo instB j (s0,pcS0)) /\ 1151 ~(k IN ((FST s0) INSERT pcS1)) ==> 1152 (runTo instB k (s0,pcS0) = runTo instB k (s1,pcS1))`, 1153 RW_TAC std_ss [] THEN 1154 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] RUNTO_COMPOSITION_LEM) THEN 1155 `?s' pcS'. runTo instB j (s0,pcS0) = (s',pcS')` by METIS_TAC [ABS_PAIR_THM] THEN 1156 FULL_SIMP_TAC std_ss [] THEN 1157 METIS_TAC [FST,SND] 1158 ); 1159 1160(*---------------------------------------------------------------------------------*) 1161(* Restriction on the modelling of registers and memory *) 1162(*---------------------------------------------------------------------------------*) 1163 1164val in_regs_dom_def = Define ` 1165 in_regs_dom regs = 1166 0 IN (FDOM regs) /\ 1 IN (FDOM regs) /\ 2 IN (FDOM regs) /\ 3 IN (FDOM regs) /\ 1167 4 IN (FDOM regs) /\ 5 IN (FDOM regs) /\ 6 IN (FDOM regs) /\ 7 IN (FDOM regs) /\ 1168 8 IN (FDOM regs) /\ 9 IN (FDOM regs) /\ 10 IN (FDOM regs) /\ 11 IN (FDOM regs) /\ 1169 12 IN (FDOM regs) /\ 13 IN (FDOM regs) /\ 14 IN (FDOM regs)`; 1170 1171 1172val in_mem_dom_def = Define ` 1173 in_mem_dom mem = 1174 !i:num. i IN (FDOM mem)`; 1175 1176 1177val FUPDATE_REFL = Q.store_thm 1178 ("FUPDATE_REFL", 1179 `!i f. i IN FDOM f ==> (f |+ (i,f ' i) = f)`, 1180 RW_TAC list_ss [fmap_EXT] THENL [ 1181 RW_TAC list_ss [FDOM_EQ_FDOM_FUPDATE], 1182 Cases_on `x = i` THEN 1183 RW_TAC list_ss [FAPPLY_FUPDATE_THM] 1184 ] 1185 ); 1186 1187(*------------------------------------------------------------------------------------------------------*) 1188(* Additional theorems for finite maps *) 1189(*------------------------------------------------------------------------------------------------------*) 1190 1191(* Sort in ascending order *) 1192val FUPDATE_LT_COMMUTES = Q.store_thm ( 1193 "FUPDATE_LT_COMMUTES", 1194 ` !f a b c d. c < a ==> (f |+ (a:num, b:word32) |+ (c,d) = f |+ (c,d) |+ (a,b))`, 1195 RW_TAC arith_ss [FUPDATE_COMMUTES] 1196 ); 1197 1198(* Sort in descending order *) 1199val FUPDATE_GT_COMMUTES = Q.store_thm ( 1200 "FUPDATE_GT_COMMUTES", 1201 ` !f a b c d. c > a ==> (f |+ (a:ADDR,b:'b) |+ (c,d) = f |+ (c,d) |+ (a,b))`, 1202 RW_TAC arith_ss [FUPDATE_COMMUTES] 1203 ); 1204 1205val _ = export_theory(); 1206