1(* ------------------------------------------------------------------------ *) 2(* ARM Machine Code Semantics *) 3(* ========================== *) 4(* Provide interface to Hoare logic *) 5(* ------------------------------------------------------------------------ *) 6 7(* interactive use: 8 app load ["armTheory", "wordsLib"]; 9*) 10 11open HolKernel boolLib bossLib; 12 13open arithmeticTheory bitTheory wordsTheory combinTheory; 14open arm_coretypesTheory arm_seq_monadTheory arm_opsemTheory armTheory; 15 16val _ = new_theory "arm_step"; 17 18(* ------------------------------------------------------------------------- *) 19 20val _ = numLib.prefer_num(); 21val _ = wordsLib.prefer_word(); 22 23infix \\ << >> 24 25val op \\ = op THEN; 26val op << = op THENL; 27val op >> = op THEN1; 28 29(* ------------------------------------------------------------------------- *) 30(* Access functions for ARM model *) 31(* ------------------------------------------------------------------------- *) 32 33val _ = Hol_datatype` 34 arm_bit = psrN | psrZ | psrC | psrV | psrQ | psrJ 35 | psrE | psrA | psrI | psrF | psrT`; 36 37val _ = Hol_datatype 38 `arm_sctlr_bit = sctlrV | sctlrU | sctlrA | sctlrEE | sctlrTE | sctlrNMFI`; 39 40val _ = Hol_datatype 41 `arm_scr_bit = scrnET | scrAW | scrFW | scrEA | scrFIQ | scrIRQ | scrNS`; 42 43val ARM_ARCH_def = Define` 44 ARM_ARCH s = s.information.arch`; 45 46val ARM_EXTENSIONS_def = Define` 47 ARM_EXTENSIONS s = s.information.extensions`; 48 49val ARM_UNALIGNED_SUPPORT_def = Define` 50 ARM_UNALIGNED_SUPPORT s = s.information.unaligned_support`; 51 52val ARM_READ_CPSR_def = Define` 53 ARM_READ_CPSR s = s.psrs (0,CPSR)`; 54 55val ARM_WRITE_CPSR_def = Define` 56 ARM_WRITE_CPSR d s = s with psrs updated_by ((0,CPSR) =+ d)`; 57 58val ARM_MODE_def = Define` 59 ARM_MODE s = (ARM_READ_CPSR s).M`; 60 61val ARM_WRITE_MODE_def = Define` 62 ARM_WRITE_MODE m s = ARM_WRITE_CPSR (ARM_READ_CPSR s with M := m) s`; 63 64val word4_def = Define` 65 word4 (b3,b2,b1,b0) : word4 = 66 FCP i. (i = 3) /\ b3 \/ (i = 2) /\ b2 \/ (i = 1) /\ b1 \/ (i = 0) /\ b0`; 67 68val ARM_READ_GE_def = Define` 69 ARM_READ_GE s = (ARM_READ_CPSR s).GE`; 70 71val ARM_WRITE_GE_def = Define` 72 ARM_WRITE_GE ge s = ARM_WRITE_CPSR (ARM_READ_CPSR s with GE := ge) s`; 73 74val ARM_READ_IT_def = Define` 75 ARM_READ_IT s = (ARM_READ_CPSR s).IT`; 76 77val ARM_WRITE_IT_def = Define` 78 ARM_WRITE_IT it s = ARM_WRITE_CPSR (ARM_READ_CPSR s with IT := it) s`; 79 80val ARM_READ_STATUS_def = Define` 81 (ARM_READ_STATUS psrN s = (ARM_READ_CPSR s).N) /\ 82 (ARM_READ_STATUS psrZ s = (ARM_READ_CPSR s).Z) /\ 83 (ARM_READ_STATUS psrC s = (ARM_READ_CPSR s).C) /\ 84 (ARM_READ_STATUS psrV s = (ARM_READ_CPSR s).V) /\ 85 (ARM_READ_STATUS psrQ s = (ARM_READ_CPSR s).Q) /\ 86 (ARM_READ_STATUS psrJ s = (ARM_READ_CPSR s).J) /\ 87 (ARM_READ_STATUS psrE s = (ARM_READ_CPSR s).E) /\ 88 (ARM_READ_STATUS psrA s = (ARM_READ_CPSR s).A) /\ 89 (ARM_READ_STATUS psrI s = (ARM_READ_CPSR s).I) /\ 90 (ARM_READ_STATUS psrF s = (ARM_READ_CPSR s).F) /\ 91 (ARM_READ_STATUS psrT s = (ARM_READ_CPSR s).T)`; 92 93val ARM_WRITE_STATUS_def = Define` 94 (ARM_WRITE_STATUS psrN b s = 95 ARM_WRITE_CPSR (ARM_READ_CPSR s with N := b) s) /\ 96 (ARM_WRITE_STATUS psrZ b s = 97 ARM_WRITE_CPSR (ARM_READ_CPSR s with Z := b) s) /\ 98 (ARM_WRITE_STATUS psrC b s = 99 ARM_WRITE_CPSR (ARM_READ_CPSR s with C := b) s) /\ 100 (ARM_WRITE_STATUS psrV b s = 101 ARM_WRITE_CPSR (ARM_READ_CPSR s with V := b) s) /\ 102 (ARM_WRITE_STATUS psrQ b s = 103 ARM_WRITE_CPSR (ARM_READ_CPSR s with Q := b) s) /\ 104 (ARM_WRITE_STATUS psrJ b s = 105 ARM_WRITE_CPSR (ARM_READ_CPSR s with J := b) s) /\ 106 (ARM_WRITE_STATUS psrE b s = 107 ARM_WRITE_CPSR (ARM_READ_CPSR s with E := b) s) /\ 108 (ARM_WRITE_STATUS psrA b s = 109 ARM_WRITE_CPSR (ARM_READ_CPSR s with A := b) s) /\ 110 (ARM_WRITE_STATUS psrI b s = 111 ARM_WRITE_CPSR (ARM_READ_CPSR s with I := b) s) /\ 112 (ARM_WRITE_STATUS psrF b s = 113 ARM_WRITE_CPSR (ARM_READ_CPSR s with F := b) s) /\ 114 (ARM_WRITE_STATUS psrT b s = 115 ARM_WRITE_CPSR (ARM_READ_CPSR s with T := b) s)`; 116 117val ARM_READ_SCTLR_def = Define` 118 (ARM_READ_SCTLR sctlrV s = s.coprocessors.state.cp15.SCTLR.V) /\ 119 (ARM_READ_SCTLR sctlrA s = s.coprocessors.state.cp15.SCTLR.A) /\ 120 (ARM_READ_SCTLR sctlrU s = s.coprocessors.state.cp15.SCTLR.U) /\ 121 (ARM_READ_SCTLR sctlrEE s = s.coprocessors.state.cp15.SCTLR.EE) /\ 122 (ARM_READ_SCTLR sctlrTE s = s.coprocessors.state.cp15.SCTLR.TE) /\ 123 (ARM_READ_SCTLR sctlrNMFI s = s.coprocessors.state.cp15.SCTLR.NMFI)`; 124 125val ARM_READ_SCR_def = Define` 126 (ARM_READ_SCR scrnET s = s.coprocessors.state.cp15.SCR.nET) /\ 127 (ARM_READ_SCR scrAW s = s.coprocessors.state.cp15.SCR.AW) /\ 128 (ARM_READ_SCR scrFW s = s.coprocessors.state.cp15.SCR.FW) /\ 129 (ARM_READ_SCR scrEA s = s.coprocessors.state.cp15.SCR.EA) /\ 130 (ARM_READ_SCR scrFIQ s = s.coprocessors.state.cp15.SCR.FIQ) /\ 131 (ARM_READ_SCR scrIRQ s = s.coprocessors.state.cp15.SCR.IRQ) /\ 132 (ARM_READ_SCR scrNS s = s.coprocessors.state.cp15.SCR.NS)`; 133 134val ARM_READ_TEEHBR_def = Define` 135 ARM_READ_TEEHBR s = s.coprocessors.state.cp14.TEEHBR`; 136 137val SPSR_MODE_def = Define` 138 SPSR_MODE (m:word5) = 139 case m 140 of 0b10001w => SPSR_fiq 141 | 0b10010w => SPSR_irq 142 | 0b10011w => SPSR_svc 143 | 0b10110w => SPSR_mon 144 | 0b10111w => SPSR_abt 145 | _ => SPSR_und`; 146 147val ARM_READ_SPSR_MODE_def = Define` 148 ARM_READ_SPSR_MODE m s = s.psrs (0,SPSR_MODE m)`; 149 150val ARM_READ_SPSR_def = Define` 151 ARM_READ_SPSR s = ARM_READ_SPSR_MODE (ARM_MODE s) s`; 152 153val ARM_WRITE_SPSR_MODE_def = Define` 154 ARM_WRITE_SPSR_MODE (m:word5) d s = 155 s with psrs updated_by ((0,SPSR_MODE m) =+ d)`; 156 157val ARM_WRITE_SPSR_def = Define` 158 ARM_WRITE_SPSR d s = ARM_WRITE_SPSR_MODE (ARM_MODE s) d s`; 159 160local 161 val l = fst (listSyntax.dest_list 162 ``[0b10001w;0b10010w;0b10011w;0b10110w;0b10111w;0b11011w]:word5 list``) 163 fun rule thm m = GEN_ALL (RIGHT_CONV_RULE EVAL 164 (Drule.SPEC_ALL (Thm.SPEC m thm))) 165in 166 val ARM_READ_SPSR_MODE = save_thm("ARM_READ_SPSR_MODE", 167 Drule.LIST_CONJ (List.map (rule ARM_READ_SPSR_MODE_def) l)); 168 val ARM_WRITE_SPSR_MODE = save_thm("ARM_WRITE_SPSR_MODE", 169 Drule.LIST_CONJ (List.map (rule ARM_WRITE_SPSR_MODE_def) l)); 170end; 171 172val ARM_READ_MODE_SPSR_def = Define` 173 ARM_READ_MODE_SPSR s = (ARM_READ_SPSR s).M`; 174 175val ARM_WRITE_MODE_SPSR_def = Define` 176 ARM_WRITE_MODE_SPSR m s = ARM_WRITE_SPSR (ARM_READ_SPSR s with M := m) s`; 177 178val ARM_READ_GE_SPSR_def = Define` 179 ARM_READ_GE_SPSR s = (ARM_READ_SPSR s).GE`; 180 181val ARM_WRITE_GE_SPSR_def = Define` 182 ARM_WRITE_GE_SPSR ge s = ARM_WRITE_SPSR (ARM_READ_SPSR s with GE := ge) s`; 183 184val ARM_READ_IT_SPSR_def = Define` 185 ARM_READ_IT_SPSR s = (ARM_READ_SPSR s).IT`; 186 187val ARM_WRITE_IT_SPSR_def = Define` 188 ARM_WRITE_IT_SPSR it s = ARM_WRITE_SPSR (ARM_READ_SPSR s with IT := it) s`; 189 190val ARM_READ_STATUS_SPSR_def = Define` 191 (ARM_READ_STATUS_SPSR psrN s = (ARM_READ_SPSR s).N) /\ 192 (ARM_READ_STATUS_SPSR psrZ s = (ARM_READ_SPSR s).Z) /\ 193 (ARM_READ_STATUS_SPSR psrC s = (ARM_READ_SPSR s).C) /\ 194 (ARM_READ_STATUS_SPSR psrV s = (ARM_READ_SPSR s).V) /\ 195 (ARM_READ_STATUS_SPSR psrQ s = (ARM_READ_SPSR s).Q) /\ 196 (ARM_READ_STATUS_SPSR psrJ s = (ARM_READ_SPSR s).J) /\ 197 (ARM_READ_STATUS_SPSR psrE s = (ARM_READ_SPSR s).E) /\ 198 (ARM_READ_STATUS_SPSR psrA s = (ARM_READ_SPSR s).A) /\ 199 (ARM_READ_STATUS_SPSR psrI s = (ARM_READ_SPSR s).I) /\ 200 (ARM_READ_STATUS_SPSR psrF s = (ARM_READ_SPSR s).F) /\ 201 (ARM_READ_STATUS_SPSR psrT s = (ARM_READ_SPSR s).T)`; 202 203val ARM_WRITE_STATUS_SPSR_def = Define` 204 (ARM_WRITE_STATUS_SPSR psrN b s = 205 ARM_WRITE_SPSR (ARM_READ_SPSR s with N := b) s) /\ 206 (ARM_WRITE_STATUS_SPSR psrZ b s = 207 ARM_WRITE_SPSR (ARM_READ_SPSR s with Z := b) s) /\ 208 (ARM_WRITE_STATUS_SPSR psrC b s = 209 ARM_WRITE_SPSR (ARM_READ_SPSR s with C := b) s) /\ 210 (ARM_WRITE_STATUS_SPSR psrV b s = 211 ARM_WRITE_SPSR (ARM_READ_SPSR s with V := b) s) /\ 212 (ARM_WRITE_STATUS_SPSR psrQ b s = 213 ARM_WRITE_SPSR (ARM_READ_SPSR s with Q := b) s) /\ 214 (ARM_WRITE_STATUS_SPSR psrJ b s = 215 ARM_WRITE_SPSR (ARM_READ_SPSR s with J := b) s) /\ 216 (ARM_WRITE_STATUS_SPSR psrE b s = 217 ARM_WRITE_SPSR (ARM_READ_SPSR s with E := b) s) /\ 218 (ARM_WRITE_STATUS_SPSR psrA b s = 219 ARM_WRITE_SPSR (ARM_READ_SPSR s with A := b) s) /\ 220 (ARM_WRITE_STATUS_SPSR psrI b s = 221 ARM_WRITE_SPSR (ARM_READ_SPSR s with I := b) s) /\ 222 (ARM_WRITE_STATUS_SPSR psrF b s = 223 ARM_WRITE_SPSR (ARM_READ_SPSR s with F := b) s) /\ 224 (ARM_WRITE_STATUS_SPSR psrT b s = 225 ARM_WRITE_SPSR (ARM_READ_SPSR s with T := b) s)`; 226 227val ARM_READ_EVENT_REGISTER_def = Define` 228 ARM_READ_EVENT_REGISTER s = s.event_register 0`; 229 230val ARM_READ_INTERRUPT_WAIT_def = Define` 231 ARM_READ_INTERRUPT_WAIT s = s.interrupt_wait 0`; 232 233val ARM_WAIT_FOR_EVENT_def = Define` 234 ARM_WAIT_FOR_EVENT s = s with event_register updated_by (0 =+ F)`; 235 236val ARM_SEND_EVENT_def = Define` 237 ARM_SEND_EVENT s = s with event_register updated_by (K (K T))`; 238 239val ARM_WAIT_FOR_INTERRUPT_def = Define` 240 ARM_WAIT_FOR_INTERRUPT s = s with interrupt_wait updated_by (0 =+ T)`; 241 242val ARM_READ_MEM_def = Define` 243 ARM_READ_MEM a s = s.memory a`; 244 245val ARM_WRITE_MEM_def = Define` 246 ARM_WRITE_MEM a w s = s with memory updated_by (a =+ w)`; 247 248val ARM_WRITE_MEM_WRITE_def = Define` 249 ARM_WRITE_MEM_WRITE a w s = s with accesses updated_by CONS (MEM_WRITE a w)`; 250 251val ARM_WRITE_MEM_READ_def = Define` 252 ARM_WRITE_MEM_READ a s = s with accesses updated_by CONS (MEM_READ a)`; 253 254val RevLookUpRName_def = Define` 255 RevLookUpRName (n:word4,m:word5) = 256 case (n,m) 257 of (0w, _ ) => RName_0usr 258 | (1w, _ ) => RName_1usr 259 | (2w, _ ) => RName_2usr 260 | (3w, _ ) => RName_3usr 261 | (4w, _ ) => RName_4usr 262 | (5w, _ ) => RName_5usr 263 | (6w, _ ) => RName_6usr 264 | (7w, _ ) => RName_7usr 265 | (8w, 0b10001w) => RName_8fiq 266 | (8w, _ ) => RName_8usr 267 | (9w, 0b10001w) => RName_9fiq 268 | (9w, _ ) => RName_9usr 269 | (10w,0b10001w) => RName_10fiq 270 | (10w,_ ) => RName_10usr 271 | (11w,0b10001w) => RName_11fiq 272 | (11w,_ ) => RName_11usr 273 | (12w,0b10001w) => RName_12fiq 274 | (12w,_ ) => RName_12usr 275 | (13w,0b10001w) => RName_SPfiq 276 | (13w,0b10010w) => RName_SPirq 277 | (13w,0b10011w) => RName_SPsvc 278 | (13w,0b10111w) => RName_SPabt 279 | (13w,0b11011w) => RName_SPund 280 | (13w,0b10110w) => RName_SPmon 281 | (13w,_ ) => RName_SPusr 282 | (14w,0b10001w) => RName_LRfiq 283 | (14w,0b10010w) => RName_LRirq 284 | (14w,0b10011w) => RName_LRsvc 285 | (14w,0b10111w) => RName_LRabt 286 | (14w,0b11011w) => RName_LRund 287 | (14w,0b10110w) => RName_LRmon 288 | (14w,_ ) => RName_LRusr 289 | (15w,_ ) => RName_PC`; 290 291val ARM_READ_REG_MODE_def = Define` 292 ARM_READ_REG_MODE x s = s.registers (0,RevLookUpRName x)`; 293 294val ARM_WRITE_REG_MODE_def = Define` 295 ARM_WRITE_REG_MODE x w s = 296 s with registers updated_by ((0,RevLookUpRName x) =+ w)`; 297 298val ARM_READ_REG_def = Define` 299 ARM_READ_REG n s = ARM_READ_REG_MODE (n,ARM_MODE s) s`; 300 301val ARM_WRITE_REG_def = Define` 302 ARM_WRITE_REG n w s = ARM_WRITE_REG_MODE (n,ARM_MODE s) w s`; 303 304val CLEAR_EXCLUSIVE_BY_ADDRESS_def = Define` 305 CLEAR_EXCLUSIVE_BY_ADDRESS (a,n) s = 306 s with monitors updated_by (ExclusiveMonitors_state_fupd (\state. 307 SND (s.monitors.ClearExclusiveByAddress (a,<| proc := 0 |>,n) state)))`; 308 309val MARK_EXCLUSIVE_GLOBAL_def = Define` 310 MARK_EXCLUSIVE_GLOBAL (a,n) s = 311 s with monitors updated_by (ExclusiveMonitors_state_fupd (\state. 312 SND (s.monitors.MarkExclusiveGlobal (a,<| proc := 0 |>,n) state)))`; 313 314val MARK_EXCLUSIVE_LOCAL_def = Define` 315 MARK_EXCLUSIVE_LOCAL (a,n) s = 316 s with monitors updated_by (ExclusiveMonitors_state_fupd (\state. 317 SND (s.monitors.MarkExclusiveLocal (a,<| proc := 0 |>,n) state)))`; 318 319val CLEAR_EXCLUSIVE_LOCAL_def = Define` 320 CLEAR_EXCLUSIVE_LOCAL s = 321 s with monitors updated_by (ExclusiveMonitors_state_fupd (\state. 322 SND (s.monitors.ClearExclusiveLocal 0 state)))`; 323 324val STATE_OPTION_def = Define` 325 STATE_OPTION f s = 326 case f s 327 of Error _ => NONE 328 | ValueState _ q => SOME q`; 329 330val ARM_NEXT_def = Define` 331 ARM_NEXT inp = STATE_OPTION (arm_next <| proc := 0 |> inp)`; 332 333(* ------------------------------------------------------------------------- *) 334(* Facilitate evaluation of set_q to when the saturation condition unknown *) 335(* ------------------------------------------------------------------------- *) 336 337(* 338val condT_set_q = Q.store_thm("condT_set_q", 339 `!b ii. (if b then set_q ii else constT ()) = 340 seqT (read_cpsr ii) 341 (\cpsr. write_cpsr ii (if b then cpsr with Q := T else cpsr))`, 342 SRW_TAC [] [FUN_EQ_THM, APPLY_UPDATE_ID, arm_state_component_equality, 343 set_q_def, constT_def, condT_def, seqT_def, 344 write_cpsr_def, write__psr_def, writeT_def, 345 read_cpsr_def, read_cpsr_def, read__psr_def, readT_def]); 346 347val ARM_WRITE_STATUS_Q = Q.store_thm("ARM_WRITE_STATUS_Q", 348 `!b s. 349 (if b then ARM_WRITE_STATUS psrQ T s else s) = 350 ARM_WRITE_STATUS psrQ (b \/ ARM_READ_STATUS psrQ s) s`, 351 SRW_TAC [] [ARM_WRITE_STATUS_def, ARM_READ_STATUS_def, 352 ARM_WRITE_CPSR_def, ARM_READ_CPSR_def, arm_state_component_equality] 353 \\ MATCH_MP_TAC (GSYM UPDATE_APPLY_IMP_ID) 354 \\ SRW_TAC [] [ARMpsr_component_equality]); 355 356(* ------------------------------------------------------------------------- *) 357(* Evaluation for alignment and other miscellany *) 358(* ------------------------------------------------------------------------- *) 359 360val UPDATE_ID = Q.store_thm("UPDATE_ID", 361 `!a b c. (a =+ b) o (a =+ c) = a =+ b`, 362 SRW_TAC [] [UPDATE_def,FUN_EQ_THM]); 363 364val UPDATE_ID_o = Q.store_thm("UPDATE_ID_o", 365 `(!a b. (a =+ b) o (a =+ b) = (a =+ b)) /\ 366 (!a b g. (a =+ b) o ((a =+ b) o g) = (a =+ b) o g)`, 367 SRW_TAC [] [FUN_EQ_THM, UPDATE_def]); 368 369val UPDATE_ID_o2 = Q.store_thm("UPDATE_ID_o2", 370 `(!a b c. (a =+ b) o (a =+ c) = (a =+ b)) /\ 371 (!a b c g. (a =+ b) o ((a =+ c) o g) = (a =+ b) o g)`, 372 SRW_TAC [] [FUN_EQ_THM, UPDATE_def]); 373 374val FST_SHIFT_C = Q.store_thm("FST_SHIFT_C", 375 `(!w s. s <> 0 ==> (FST (LSL_C (w, s)) = w << s)) /\ 376 (!w s. s <> 0 ==> (FST (LSR_C (w, s)) = w >>> s)) /\ 377 (!w s. s <> 0 ==> (FST (ASR_C (w, s)) = w >> s)) /\ 378 (!w s. s <> 0 ==> (FST (ROR_C (w, s)) = w #>> s)) /\ 379 (!w s. (if s = 0 then w else w << s) = w << s) /\ 380 (!w s. (if s = 0 then w else w >>> s) = w >>> s) /\ 381 (!w s. (if s = 0 then w else w >> s) = w >> s) /\ 382 (!w s. (if s = 0 then w else w #>> s) = w #>> s)`, 383 SRW_TAC [] [LSL_C_def, LSR_C_def, ASR_C_def, ROR_C_def] \\ SRW_TAC [] []); 384 385val EXTRACT_ROR = Q.store_thm("EXTRACT_ROR", 386 `(!a:word32. (( 7 >< 0 ) (a #>> 8 ) = (15 >< 8 ) a : word8)) /\ 387 (!a:word32. (( 7 >< 0 ) (a #>> 16) = (23 >< 16) a : word8)) /\ 388 (!a:word32. (( 7 >< 0 ) (a #>> 24) = (31 >< 24) a : word8)) /\ 389 (!a:word32. ((23 >< 16) (a #>> 8) = (31 >< 24) a : word8)) /\ 390 (!a:word32. ((23 >< 16) (a #>> 16) = ( 7 >< 0 ) a : word8)) /\ 391 (!a:word32. ((23 >< 16) (a #>> 24) = (15 >< 8 ) a : word8)) /\ 392 (!a:word32. ((15 >< 0 ) (a #>> 8 ) = (23 >< 8 ) a : word16)) /\ 393 (!a:word32. ((15 >< 0 ) (a #>> 16) = (31 >< 16) a : word16)) /\ 394 (!a:word32. ((31 >< 16) (a #>> 16) = (15 >< 0 ) a : word16))`, 395 SRW_TAC [wordsLib.WORD_EXTRACT_ss] []); 396 397val SInt_0 = Q.store_thm("SInt_0", 398 `SInt 0w = 0`, SRW_TAC [] [integer_wordTheory.w2i_def]); 399 400val align_1 = save_thm("align_1", 401 simpLib.SIMP_PROVE (srw_ss()++wordsLib.WORD_BIT_EQ_ss) [align_def] 402 ``align(a,1) = a``); 403 404val align_248 = save_thm("align_248", 405 numLib.REDUCE_RULE 406 (Drule.LIST_CONJ (List.map (fn t => Q.SPEC t align_slice) [`1`,`2`,`3`]))); 407 408val aligned_248 = Q.store_thm("aligned_248", 409 `(!a:word32. aligned(a,2) = ~word_lsb a) /\ 410 (!a:word32. aligned(a,4) = ((1 >< 0) a = 0w:word2)) /\ 411 (!a:word32. aligned(a,8) = ((2 >< 0) a = 0w:word3))`, 412 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [aligned_def, align_248]); 413 414val align_lem = Q.prove( 415 `(!b:word32. align(b,2) + (0 -- 0) b = b) /\ 416 (!b:word32. align(b,4) + (1 -- 0) b = b) /\ 417 (!b:word32. align(b,8) + (2 -- 0) b = b)`, 418 SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_248]); 419 420val align_lem2 = 421 METIS_PROVE [align_lem, WORD_ADD_ASSOC] 422 ``(!a:word32 b. align(a,2) + b = align(a,2) + align(b,2) + (0 -- 0) b) /\ 423 (!a:word32 b. align(a,4) + b = align(a,4) + align(b,4) + (1 -- 0) b) /\ 424 (!a:word32 b. align(a,8) + b = align(a,8) + align(b,8) + (2 -- 0) b)``; 425 426val align_lem2b = 427 METIS_PROVE [align_lem, WORD_ADD_ASSOC] 428 ``(!a:word32 b. align(a,4) + b = align(a,4) + align(b,2) + (0 -- 0) b)``; 429 430val align_2_align_4 = Q.store_thm("align_2_align_4", 431 `!a:word32. align(align(a,4),2) = align(a,4)`, 432 SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_248]); 433 434val align_aligned = Q.prove( 435 `(!a:word32 b. align(align(a,2) + b,2) = align(a,2) + align(b,2)) /\ 436 (!a:word32 b. align(align(a,4) + b,4) = align(a,4) + align(b,4)) /\ 437 (!a:word32 b. align(align(a,8) + b,8) = align(a,8) + align(b,8))`, 438 REPEAT STRIP_TAC 439 \\ CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [align_lem2])) 440 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_248] 441 \\ REWRITE_TAC [GSYM WORD_ADD_LSL] 442 \\ Q.PAT_ABBREV_TAC `x:word32 = (f a + g b)` 443 << [`x << 1 + (0 >< 0) b = x << 1 || (0 >< 0) b` 444 by (MATCH_MP_TAC WORD_ADD_OR \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []), 445 `x << 2 + (1 >< 0) b = x << 2 || (1 >< 0) b` 446 by (MATCH_MP_TAC WORD_ADD_OR \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []), 447 `x << 3 + (2 >< 0) b = x << 3 || (2 >< 0) b` 448 by (MATCH_MP_TAC WORD_ADD_OR \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [])] 449 \\ POP_ASSUM SUBST1_TAC 450 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] [] 451 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []); 452 453val align_aligned2 = Q.store_thm("align_aligned2", 454 `(!a:word32 b. align(align(a,4) + b,2) = align(a,4) + align(b,2))`, 455 REPEAT STRIP_TAC 456 \\ CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [align_lem2b])) 457 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_248] 458 \\ REWRITE_TAC [GSYM WORD_ADD_LSL, 459 wordsLib.WORD_DECIDE ``(a:word32) << 2 = a << 1 << 1``] 460 \\ Q.ABBREV_TAC `x:word32 = ((31 >< 1) b + (31 >< 2) a << 1)` 461 \\ `x << 1 + (0 >< 0) b = x << 1 || (0 >< 0) b` 462 by (MATCH_MP_TAC WORD_ADD_OR \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []) 463 \\ POP_ASSUM SUBST1_TAC 464 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] [] 465 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []); 466 467val align_aligned = save_thm("align_aligned", 468 CONJ align_aligned2 align_aligned); 469 470val align_sum = save_thm("align_sum", 471 REWRITE_RULE [GSYM align_aligned, WORD_ADD_ASSOC] align_lem2); 472 473val aligned_thm1 = Q.prove( 474 `(!a:word32 b. aligned(a,2) /\ aligned(b,2) ==> (align (a + b,2) = a + b)) /\ 475 (!a:word32 b. aligned(a,4) /\ aligned(b,4) ==> (align (a + b,4) = a + b)) /\ 476 (!a:word32 b. aligned(a,8) /\ aligned(b,8) ==> (align (a + b,8) = a + b))`, 477 METIS_TAC [aligned_def, align_aligned]); 478 479val aligned_thm2 = Q.prove( 480 `!a:word32. aligned(a,4) ==> aligned(a,2)`, 481 METIS_TAC [aligned_def, align_2_align_4]); 482 483val aligned_thm = save_thm("aligned_thm", 484 Drule.LIST_CONJ [aligned_thm2, aligned_thm1, 485 aligned_def |> Drule.SPEC_ALL |> EQ_IMP_RULE |> fst |> GSYM |> GEN_ALL]); 486 487val align_aligned3 = Q.store_thm("align_aligned3", 488 `!pc x: word32. 489 aligned (pc + 8w + x, 4) /\ aligned (pc, 4) ==> 490 aligned (x + align (pc, 4) + 8w, 4)`, 491 METIS_TAC [aligned_thm, WORD_ADD_COMM, WORD_ADD_ASSOC]); 492 493val aligned_align = Q.store_thm("aligned_align", 494 `(!a:word32. aligned(a,1)) /\ 495 (!a:word32. aligned(align(a,2),2)) /\ 496 (!a:word32. aligned(align(a,4),2)) /\ 497 (!a:word32. aligned(align(a,4),4)) /\ 498 (!a:word32. aligned(align(a,8),8))`, 499 METIS_TAC [aligned_def,aligned_thm,align_1,align_id_248]); 500 501val aligned_sum = Q.store_thm("aligned_sum", 502 `(!a:word32 b. aligned(align(a,2) + b,2) = aligned(b,2)) /\ 503 (!a:word32 b. aligned(align(a,4) + b,2) = aligned(b,2)) /\ 504 (!a:word32 b. aligned(align(a,4) + b,4) = aligned(b,4))`, 505 SIMP_TAC (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) 506 [align_aligned, align_aligned2, aligned_def]); 507 508val align_bits = Q.store_thm("align_bits", 509 `(!a:word32. (0 -- 0) (align(a,2)) = 0w) /\ 510 (!a:word32. (1 -- 0) (align(a,4)) = 0w) /\ 511 (!a:word32. (2 -- 0) (align(a,8)) = 0w)`, 512 SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_248]); 513 514val align_bits_sum = Q.store_thm("align_bits_sum", 515 `!a:word32 n. (1 >< 0) (align (a,4) + n) = (1 >< 0) n : word2`, 516 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [] 517 \\ SIMP_TAC (srw_ss()) [Once WORD_ADD_BIT] 518 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_248] 519 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) []); 520 521val align_or = Q.prove( 522 `(!a:word32. align (a,2) + 1w = align (a,2) || 1w) /\ 523 (!a:word32. align (a,4) + 1w = align (a,4) || 1w) /\ 524 (!a:word32. align (a,4) + 2w = align (a,4) || 2w) /\ 525 (!a:word32. align (a,4) + 3w = align (a,4) || 3w)`, (* /\ 526 (!a:word32. align (a,8) + 1w = align (a,8) || 1w) /\ 527 (!a:word32. align (a,8) + 2w = align (a,8) || 2w) /\ 528 (!a:word32. align (a,8) + 3w = align (a,8) || 3w) /\ 529 (!a:word32. align (a,8) + 4w = align (a,8) || 4w) /\ 530 (!a:word32. align (a,8) + 5w = align (a,8) || 5w) /\ 531 (!a:word32. align (a,8) + 6w = align (a,8) || 6w) /\ 532 (!a:word32. align (a,8) + 7w = align (a,8) || 7w)`, *) 533 REPEAT STRIP_TAC \\ MATCH_MP_TAC WORD_ADD_OR 534 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [align_248]); 535 536val align_neq = Q.prove( 537 `(!a:word32 b. align (a,2) + 0w <> align (b,2) + 1w) /\ 538 (!a:word32 b. align (a,2) + 1w <> align (b,2) + 0w) /\ 539 (!a:word32 b. align (a,4) + 0w <> align (b,4) + 1w) /\ 540 (!a:word32 b. align (a,4) + 0w <> align (b,4) + 2w) /\ 541 (!a:word32 b. align (a,4) + 0w <> align (b,4) + 3w) /\ 542 (!a:word32 b. align (a,4) + 1w <> align (b,4) + 0w) /\ 543 (!a:word32 b. align (a,4) + 1w <> align (b,4) + 2w) /\ 544 (!a:word32 b. align (a,4) + 1w <> align (b,4) + 3w) /\ 545 (!a:word32 b. align (a,4) + 2w <> align (b,4) + 0w) /\ 546 (!a:word32 b. align (a,4) + 2w <> align (b,4) + 1w) /\ 547 (!a:word32 b. align (a,4) + 2w <> align (b,4) + 3w) /\ 548 (!a:word32 b. align (a,4) + 3w <> align (b,4) + 0w) /\ 549 (!a:word32 b. align (a,4) + 3w <> align (b,4) + 1w) /\ 550 (!a:word32 b. align (a,4) + 3w <> align (b,4) + 2w)`, 551 SRW_TAC [] [align_or] \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [align_248]); 552 553val align_neq = save_thm("align_neq", SIMP_RULE (srw_ss()) [] align_neq); 554 555val align2_add_times2 = Q.store_thm("align2_add_times2", 556 `!a:word32 b. 557 align (align (a,2) + 4w + 2w * b,2) = align (a,2) + 4w + 2w * b`, 558 REPEAT STRIP_TAC 559 \\ REWRITE_TAC 560 [wordsLib.WORD_DECIDE ``a + 4w + 2w * b = a + 2w * (b + 2w)``] 561 \\ Q.ABBREV_TAC `c = b + 2w:word32` 562 \\ SRW_TAC [wordsLib.WORD_MUL_LSL_ss] [align_aligned] 563 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss,wordsLib.WORD_BIT_EQ_ss] [align_248]); 564 565val align_1comp = Q.store_thm("align_1comp", 566 `!a:word32. ~align(a,4) = align(~a,4) + 3w`, 567 REWRITE_TAC [align_or] \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [align_248]); 568 569val align_relative_thm1 = Q.prove( 570 `(!a:word32 b c. 571 (b = -c) ==> ((a = align (a + b, 2) + c) = aligned (a + b, 2))) /\ 572 (!a:word32 b c. 573 (b = -c) ==> ((a = align (a + b, 4) + c) = aligned (a + b, 4))) /\ 574 (!a:word32 b c. 575 (b = -c) ==> ((a = align (a + b, 8) + c) = aligned (a + b, 8)))`, 576 REPEAT STRIP_TAC 577 \\ SRW_TAC [wordsLib.WORD_ARITH_EQ_ss] [aligned_def]); 578 579val align_relative_thm2 = Q.prove( 580 `(!a:word32 b c. 581 (b = c + 1w) ==> ((a = c - align (~a + b, 4)) = aligned (c - a, 4))) /\ 582 (!a:word32 b. ((a = b - align (b - a, 4)) = aligned (b - a, 4)))`, 583 SRW_TAC [] [WORD_EQ_SUB_LADD, WORD_NOT] 584 \\ SRW_TAC [wordsLib.WORD_ARITH_EQ_ss] [aligned_def] 585 \\ CONV_TAC wordsLib.WORD_ARITH_CONV); 586 587val word_add_plus1 = Q.prove( 588 `!a b. n2w (w2n a + w2n b + 1) = a + b + 1w : word32`, 589 SRW_TAC [] [word_add_def] 590 \\ METIS_TAC [arithmeticTheory.MOD_PLUS, DECIDE ``0 < 4294967296``, 591 simpLib.SIMP_PROVE (srw_ss()) [] ``1 = 1 MOD 4294967296``]); 592 593val align_relative_thm3 = Q.prove( 594 `(!a:word32 b d c. 595 (b = -d) ==> ((a = align (FST (add_with_carry(a,b,c)),4) + d + 596 -(if c then 1w else 0w)) = 597 aligned (FST (add_with_carry(a,b,c)),4))) /\ 598 (!a:word32 b c. 599 ((a = b + (if c then 0w else -1w) + 600 -align (FST (add_with_carry(~a,b,c)),4)) = 601 aligned (FST (add_with_carry(~a,b,c)),4))) /\ 602 (!a:word32 b d c. 603 (b = ~d) ==> ((a = align (FST (add_with_carry(a,b,c)),4) + d + 604 (if c then 0w else 1w)) = 605 aligned (FST (add_with_carry(a,b,c)),4)))`, 606 REPEAT STRIP_TAC \\ Cases_on `c` 607 \\ SRW_TAC [] [FST_ADD_WITH_CARRY, align_relative_thm1] 608 \\ SRW_TAC [boolSimps.LET_ss, wordsLib.WORD_ARITH_EQ_ss] 609 [word_add_plus1, add_with_carry_def, aligned_def] 610 \\ CONV_TAC wordsLib.WORD_ARITH_CONV); 611 612val align_relative_thm = save_thm("align_relative_thm", 613 Drule.LIST_CONJ (Drule.CONJUNCTS align_relative_thm1 @ 614 [align_relative_thm2 |> REWRITE_RULE [word_sub_def], 615 align_relative_thm3 |> REWRITE_RULE [EVAL ``-1w:word32``], 616 align_relative_thm3 617 |> Thm.CONJUNCT1 |> Drule.SPEC_ALL 618 |> Q.INST [`b:word32` |-> `0w:word32`, `d:word32` |-> `0w:word32`] 619 |> SIMP_RULE std_ss [WORD_NEG_0, WORD_ADD_0], 620 align_relative_thm3 621 |> Thm.CONJUNCT2 |> Thm.CONJUNCT1 |> Drule.SPEC_ALL 622 |> Q.INST [`b:word32` |-> `0w:word32`] 623 |> SIMP_RULE std_ss [EVAL ``-1w:word32``, WORD_ADD_0], 624 align_relative_thm3 625 |> Drule.CONJUNCTS |> last |> Drule.SPEC_ALL 626 |> Q.INST [`b:word32` |-> `0xFFFFFFFFw:word32`, 627 `d:word32` |-> `0w:word32`] 628 |> SIMP_RULE std_ss [EVAL ``0xFFFFFFFFw = ~0w:word32``, WORD_ADD_0], 629 align_relative_thm2 630 |> Thm.CONJUNCT1 |> Drule.SPEC_ALL 631 |> Q.INST [`b:word32` |-> `1w:word32`, `c:word32` |-> `0w:word32`] 632 |> SIMP_RULE std_ss [WORD_SUB_LZERO, WORD_ADD_0]])); 633 634val align_relative_add_with_carry = Q.prove( 635 `(!a:word32 b c d. 636 (b = -d) ==> 637 (FST (add_with_carry (a,b,c)) + -1w * (if c then 1w else 0w) + d = a)) /\ 638 (!a:word32 b c d. 639 (b = ~d) ==> 640 (FST (add_with_carry (a,b,c)) + (if c then 0w else 1w) + d = a)) /\ 641 (!a:word32 b c. 642 (-1w * FST (add_with_carry (-1w * a + -1w,b,c)) + 643 (if c then 0w else 0xFFFFFFFFw) + b = a)) /\ 644 (!a:word32 b c d. 645 (b = -d) ==> 646 (d + FST (add_with_carry (a,b,c)) + -1w * (if c then 1w else 0w) = a)) /\ 647 (!a:word32 b c d. 648 (b = ~d) ==> 649 (d + FST (add_with_carry (a,b,c)) + (if c then 0w else 1w) = a)) /\ 650 (!a:word32 b c. 651 (b + -1w * FST (add_with_carry (-1w * a + -1w,b,c)) + 652 (if c then 0w else 0xFFFFFFFFw) = a)) /\ 653 (!a:word32 b c d e. 654 (b = -(d + e)) ==> 655 (d + FST (add_with_carry (a,b,c)) + 656 -1w * (if c then 1w else 0w) + e = a)) /\ 657 (!a:word32 b c d e. 658 (b = ~(d + e)) ==> 659 (d + FST (add_with_carry (a,b,c)) + (if c then 0w else 1w) + e = a)) /\ 660 (!a:word32 b c. 661 (b + -1w * FST (add_with_carry (-1w * a + -1w,b + 8w,c)) + 662 (if c then 0w else 0xFFFFFFFFw) + 8w = a)) /\ 663 (!a:word32 b c d. 664 (b = -d) ==> 665 (FST (add_with_carry (a,b,c)) + d + -1w * (if c then 1w else 0w) = a)) /\ 666 (!a:word32 b c d. 667 (b = ~d) ==> 668 (FST (add_with_carry (a,b,c)) + d + (if c then 0w else 1w) = a)) /\ 669 (!a:word32 b c. 670 (-1w * FST (add_with_carry (-1w * a + -1w,b,c)) + 671 b + (if c then 0w else 0xFFFFFFFFw) = a))`, 672 REPEAT STRIP_TAC \\ Cases_on `c` \\ SRW_TAC [] [FST_ADD_WITH_CARRY] 673 \\ SRW_TAC [boolSimps.LET_ss, wordsLib.WORD_ARITH_EQ_ss] 674 [word_add_plus1, add_with_carry_def]); 675 676val align_relative_add_with_carry = save_thm("align_relative_add_with_carry", 677 Drule.LIST_CONJ 678 [align_relative_add_with_carry, 679 align_relative_add_with_carry 680 |> Thm.CONJUNCT2 |> Thm.CONJUNCT2 |> Thm.CONJUNCT1 |> Drule.SPEC_ALL 681 |> Q.INST [`b:word32` |-> `0w:word32`] 682 |> SIMP_RULE std_ss [WORD_ADD_0] 683 |> GEN_ALL, 684 align_relative_add_with_carry 685 |> Thm.CONJUNCT2 |> Thm.CONJUNCT1 |> Drule.SPEC_ALL 686 |> Q.INST [`b:word32` |-> `0xFFFFFFFFw:word32`, 687 `d:word32` |-> `0w:word32`] 688 |> SIMP_RULE std_ss [EVAL ``0xFFFFFFFFw = ~0w:word32``, WORD_ADD_0] 689 |> GEN_ALL, 690 align_relative_add_with_carry 691 |> Thm.CONJUNCT1 |> Drule.SPEC_ALL 692 |> Q.INST [`b:word32` |-> `0w:word32`, `d:word32` |-> `0w:word32`] 693 |> SIMP_RULE std_ss [WORD_NEG_0, WORD_ADD_0] 694 |> GEN_ALL]); 695 696val aligned_con_thm = Q.prove( 697 `!n a:word32. 0 < n ==> 698 (aligned((if aligned(a + a,n) then a else 0w) + 699 (if aligned(a + a,n) then a else 0w),n))`, 700 SRW_TAC [] [] \\ EVAL_TAC \\ SRW_TAC [] [arithmeticTheory.ZERO_DIV]); 701 702val aligned_con_thms = save_thm("aligned_con_thms", 703 Drule.LIST_CONJ 704 (List.map (fn t => aligned_con_thm 705 |> Q.SPEC t 706 |> SIMP_RULE std_ss []) [`2`,`4`])); 707 708val aligned_con_plus4_thm = Q.store_thm("aligned_con_plus4_thm", 709 `!a:word32. 710 (aligned((if aligned(a + a,4) then a else 0w) + 711 (if aligned(a + a,4) then a else 0w) + 4w,4))`, 712 SRW_TAC [] [] \\ EVAL_TAC \\ SRW_TAC [] [arithmeticTheory.ZERO_DIV] 713 \\ METIS_TAC [aligned_def, align_aligned, EVAL ``align(4w:word32,4)``]); 714 715val aligned_con_shift_thm = Q.prove( 716 `!n f:bool[32] # num -> bool[32] # bool x a:word32. 717 0 < n /\ x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 718 (aligned((if aligned(a + FST (f (a,x)),n) then a else 0w) + 719 FST (f (if aligned(a + FST (f (a,x)),n) then a else 0w,x)),n))`, 720 SRW_TAC [] [] \\ EVAL_TAC \\ SRW_TAC [] [arithmeticTheory.ZERO_DIV]); 721 722val aligned_con_shift_neg_thm = Q.prove( 723 `!n f:bool[32] # num -> bool[32] # bool x a:word32. 724 0 < n /\ x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 725 (aligned((if aligned(a + -FST (f (a,x)),n) then a else 0w) + 726 -FST (f (if aligned(a + -FST (f (a,x)),n) then a else 0w,x)),n))`, 727 SRW_TAC [] [] \\ EVAL_TAC \\ SRW_TAC [] [arithmeticTheory.ZERO_DIV]); 728 729val aligned_con_shift_thm2 = Q.SPEC `2` aligned_con_shift_thm; 730val aligned_con_shift_thm4 = Q.SPEC `4` aligned_con_shift_thm; 731val aligned_con_shift_neg_thm2 = Q.SPEC `2` aligned_con_shift_neg_thm; 732val aligned_con_shift_neg_thm4 = Q.SPEC `4` aligned_con_shift_neg_thm; 733 734val NUMERAL_NOT_ZERO = Q.prove( 735 `(!n. NUMERAL (BIT1 n) <> 0n) /\ (!n. NUMERAL (BIT2 n) <> 0n)`, 736 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF, 737 arithmeticTheory.BIT1, arithmeticTheory.BIT2] 738 \\ DECIDE_TAC); 739 740val NUMERAL_FST_SHIFT_C = Drule.LIST_CONJ 741 (List.map (fn t => CONJ (Q.SPECL [`0w`,`NUMERAL (BIT1 n)`] t) 742 (Q.SPECL [`0w`,`NUMERAL (BIT2 n)`] t) 743 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,ZERO_SHIFT] 744 |> GEN_ALL) 745 (List.take(Drule.CONJUNCTS FST_SHIFT_C,4))); 746 747val aligned_con_shift_thms = save_thm("aligned_con_shift_thms", 748 Drule.LIST_CONJ (List.concat 749 (List.map (fn thm => 750 List.map (fn t => (CONJ (thm |> Q.SPECL [t,`NUMERAL (BIT1 n)`,`a`]) 751 (thm |> Q.SPECL [t,`NUMERAL (BIT2 n)`,`a`])) 752 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,NUMERAL_FST_SHIFT_C]) 753 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 754 [aligned_con_shift_thm2,aligned_con_shift_thm4, 755 aligned_con_shift_neg_thm2, aligned_con_shift_neg_thm4]))); 756 757val aligned_con_rrx_thm = Q.prove( 758 `!n b a:word32. n IN {2; 4} ==> 759 (aligned((if aligned(a + SND (word_rrx (b,a)),n) then a else 0w) + 760 SND (word_rrx 761 (b,if aligned(a + SND (word_rrx (b,a)),n) then a else 0w)),n))`, 762 SRW_TAC [] [] \\ EVAL_TAC \\ SRW_TAC [] [arithmeticTheory.ZERO_DIV]); 763 764val aligned_con_rrx_neg_thm = Q.prove( 765 `!n b a:word32. n IN {2; 4} ==> 766 (aligned((if aligned(a + -SND (word_rrx (b,a)),n) then a else 0w) + 767 -SND (word_rrx 768 (b,if aligned(a + -SND (word_rrx (b,a)),n) then a else 0w)),n))`, 769 SRW_TAC [] [] \\ EVAL_TAC \\ SRW_TAC [] [arithmeticTheory.ZERO_DIV]); 770 771val aligned_con_rrx_thms = save_thm("aligned_con_rrx_thms", 772 Drule.LIST_CONJ 773 [aligned_con_rrx_thm |> Q.SPEC `2`, 774 aligned_con_rrx_thm |> Q.SPEC `4`, 775 aligned_con_rrx_neg_thm |> Q.SPEC `2`, 776 aligned_con_rrx_neg_thm |> Q.SPEC `4`] 777 |> SIMP_RULE (std_ss++pred_setSimps.PRED_SET_ss) []); 778 779(* ------------------------------------------------------------------------- *) 780 781val aligned_bx_def = zDefine `aligned_bx a = (1 >< 0) a <> (0b10w:word2)`; 782 783val aligned_bx_n2w = save_thm("aligned_bx_n2w", 784let val thm = aligned_bx_def |> Q.SPEC `n2w a` |> GEN_ALL in 785 CONJ (INST_TYPE [alpha |-> ``:32``] thm) 786 (INST_TYPE [alpha |-> ``:8``] thm) 787 |> SIMP_RULE (srw_ss()) [bitTheory.BITS_ZERO3, word_extract_n2w] 788end); 789 790val _ = computeLib.add_persistent_funs ["aligned_bx_n2w"]; 791 792val aligned_bx_0w = EVAL ``aligned_bx (0w:word32)``; 793val aligned_bx_1w = EVAL ``aligned_bx (1w:word32)``; 794val aligned_bx_m1w = EVAL ``aligned_bx (-1w:word32)``; 795 796val align_bx_bit = Q.store_thm("align_bx_bit", 797 `(!a:word32. (~a) ' 0 = ~a ' 0) /\ 798 (!a:word32 n. (a && n2w n) ' 0 = a ' 0 /\ ODD n) /\ 799 (!a:word32 n. (a || n2w n) ' 0 = a ' 0 \/ ODD n) /\ 800 (!a:word32 n. (a ?? n2w n) ' 0 = a ' 0 <> ODD n) /\ 801 (!a:word32 n. (a + n2w n) ' 0 = a ' 0 <> ODD n)`, 802 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [WORD_ADD_BIT0, n2w_def, BIT0_ODD]); 803 804val aligned_bx_thm = Q.store_thm("aligned_bx_thm", 805 `!a:word32. aligned_bx a = (~a ' 0 ==> ~a ' 1)`, 806 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [aligned_bx_def] \\ METIS_TAC []); 807 808val aligned_bx_branch = Q.store_thm("aligned_bx_branch", 809 `!a:word32. aligned_bx ((if aligned_bx a then a else 0w))`, 810 SRW_TAC [] [aligned_bx_def, aligned_bx_0w]); 811 812val aligned_bx_1comp = Q.store_thm("aligned_bx_1comp", 813 `!a:word32. aligned_bx (~(if aligned_bx (~a) then a else 0w))`, 814 SRW_TAC [] [aligned_bx_def]); 815 816val aligned_bx_2comp = Q.store_thm("aligned_bx_2comp", 817 `!a:word32. aligned_bx (-(if aligned_bx (-a) then a else 0w))`, 818 SRW_TAC [] [aligned_bx_def]); 819 820val aligned_bx_and = Q.store_thm("aligned_bx_and", 821 `!a:word32 b. aligned_bx ((if aligned_bx (a && b) then a else 0w) && b)`, 822 SRW_TAC [] [aligned_bx_def]); 823 824val aligned_bx_eor = Q.store_thm("aligned_bx_eor", 825 `!a:word32 b. aligned_bx ((if aligned_bx (a ?? b) then a else b) ?? b)`, 826 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [aligned_bx_def] \\ METIS_TAC []); 827 828val aligned_bx_orr = Q.prove( 829 `!a:word32 b. aligned_bx ((if aligned_bx (a || b) then a else 1w) || b)`, 830 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [aligned_bx_def] \\ METIS_TAC []); 831 832val aligned_bx_orr = save_thm("aligned_bx_orr", 833 CONJ (aligned_bx_orr |> Q.SPECL [`a`,`0w`] |> SIMP_RULE (srw_ss()) []) 834 aligned_bx_orr); 835 836val word_plus8 = Q.prove( 837 `!pc:word32. align (pc,4) + 8w = (align (pc,4) >>> 2 + 2w) << 2`, 838 SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_248]); 839 840val aligned_bx_and_pc = Q.store_thm("aligned_bx_and_pc", 841 `(!pc:word32 b. aligned_bx ((align (pc,4) + 8w) && b)) /\ 842 !pc:word32 b. ~(((align (pc,4) + 8w) && b) ' 0)`, 843 NTAC 2 STRIP_TAC \\ REWRITE_TAC [word_plus8] 844 \\ Q.ABBREV_TAC `x = align (pc,4) >>> 2 + 2w : word32` 845 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss, ARITH_ss] [aligned_bx_def]); 846 847val aligned_bx_bic_pc = Q.store_thm("aligned_bx_bic_pc", 848 `!pc:word32 b. (b && ~(align (pc,4) + 8w)) ' 0 = b ' 0`, 849 STRIP_TAC \\ REWRITE_TAC [word_plus8] 850 \\ Q.ABBREV_TAC `x = align (pc,4) >>> 2 + 2w : word32` 851 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss, ARITH_ss] [aligned_bx_def]); 852 853val aligned_bx_eor_pc = Q.store_thm("aligned_bx_eor_pc", 854 `(!pc:word32 b. aligned_bx ((align (pc,4) + 8w) ?? b) = aligned_bx b) /\ 855 !pc:word32 b. ((align (pc,4) + 8w) ?? b) ' 0 = b ' 0`, 856 NTAC 2 STRIP_TAC \\ REWRITE_TAC [word_plus8] 857 \\ Q.ABBREV_TAC `x = align (pc,4) >>> 2 + 2w : word32` 858 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss, ARITH_ss] [aligned_bx_def]); 859 860val aligned_bx_orr_pc = Q.store_thm("aligned_bx_orr_pc", 861 `(!pc:word32 b. aligned_bx ((align (pc,4) + 8w) || b) = aligned_bx b) /\ 862 !pc:word32 b. ((align (pc,4) + 8w) || b) ' 0 = b ' 0`, 863 NTAC 2 STRIP_TAC \\ REWRITE_TAC [word_plus8] 864 \\ Q.ABBREV_TAC `x = align (pc,4) >>> 2 + 2w : word32` 865 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss, ARITH_ss] [aligned_bx_def]); 866 867val eor_bit0 = Q.prove( 868 `(!a b:word32. (b + (a ?? 1w)) ' 0 = ~(a + b) ' 0) /\ 869 !a b:word32. (b + ~(a ?? 1w)) ' 0 = ~(~a + b) ' 0`, 870 SRW_TAC [] [WORD_ADD_BIT0, 871 wordsLib.WORD_DECIDE ``!a:word32. (~(a ?? 1w)) ' 0 = ~(~a) ' 0``, 872 wordsLib.WORD_DECIDE ``!a:word32. (a ?? 1w) ' 0 = ~a ' 0``] 873 \\ METIS_TAC []); 874 875val eor_bit0_cor = 876 eor_bit0 |> Drule.CONJUNCTS 877 |> List.map (SIMP_RULE (srw_ss()) [] o Q.SPECL [`a`,`b + 1w`]) 878 |> Drule.LIST_CONJ; 879 880val aligned_bx_add_with_carry = Q.store_thm("aligned_bx_add_with_carry", 881 `(!a:word32 b c. 882 aligned_bx (FST (add_with_carry 883 (if aligned_bx (FST (add_with_carry(a,b,c))) then 884 a 885 else 886 a ?? 1w,b,c)))) /\ 887 (!a:word32 b c. 888 aligned_bx (FST (add_with_carry 889 (~if aligned_bx (FST (add_with_carry(~a,b,c))) then 890 a 891 else 892 a ?? 1w,b,c))))`, 893 SRW_TAC [] [aligned_bx_def] \\ Cases_on `c` 894 \\ FULL_SIMP_TAC (srw_ss()++boolSimps.LET_ss) 895 [add_with_carry_def, GSYM word_add_def, word_add_plus1, 896 GSYM aligned_bx_def, aligned_bx_thm] 897 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) 898 [eor_bit0, eor_bit0_cor]); 899 900val aligned_bx_add_sub = Q.prove( 901 `!a:word32 b. aligned_bx ((if aligned_bx (a + b) then a else a ?? 1w) + b)`, 902 SRW_TAC [] [aligned_bx_def] 903 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) 904 [GSYM aligned_bx_def, aligned_bx_thm, eor_bit0]); 905 906val aligned_bx_rev_add_sub = Q.prove( 907 `!a:word32 b. aligned_bx (b + -(if aligned_bx (b + -a) then a else a ?? 1w))`, 908 SRW_TAC [] [aligned_bx_def, WORD_NEG] 909 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) 910 [GSYM aligned_bx_def, aligned_bx_thm, eor_bit0, eor_bit0_cor]); 911 912val aligned_bx_rsb = Q.prove( 913 `!a:word32 b. 914 aligned_bx (~(if aligned_bx (~a + b) then a else a ?? 1w) + b)`, 915 SRW_TAC [] [aligned_bx_def] 916 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) 917 [GSYM aligned_bx_def, aligned_bx_thm, eor_bit0]); 918 919val aligned_bx_add_sub = save_thm("aligned_bx_add_sub", 920 Drule.LIST_CONJ 921 [aligned_bx_add_sub |> Q.SPECL [`a`,`0w`] |> SIMP_RULE (srw_ss()) [word_0], 922 aligned_bx_rev_add_sub |> Q.SPECL [`a`,`0w`] 923 |> SIMP_RULE std_ss [WORD_ADD_0], 924 aligned_bx_rsb |> Q.SPECL [`a`,`0w`] |> SIMP_RULE (srw_ss()) [], 925 aligned_bx_add_sub, aligned_bx_rev_add_sub, aligned_bx_rsb]); 926 927val aligned_bx_add_sub_pc = Q.prove( 928 `(!a:word32 b. (align(a,4) + b) ' 0 = b ' 0) /\ 929 !a:word32 b. aligned_bx (align(a,4) + b) = aligned_bx b`, 930 SRW_TAC [wordsLib.WORD_EXTRACT_ss] 931 [aligned_bx_thm, align_248, WORD_ADD_BIT0, Once WORD_ADD_BIT] 932 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) []); 933 934val extract_bit0_plus1 = Q.prove( 935 `!b:word32. ((0 >< 0) b + 1w:word32) ' 1 <=> b ' 0`, 936 STRIP_TAC 937 \\ `((0 >< 0) b = 0w:word32) \/ ((0 >< 0) b = 1w:word32)` 938 by SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [] 939 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) []); 940 941val aligned_bx_add_sub_pc2 = Q.prove( 942 `(!a:word32 b. (align(a,4) + 8w + b) ' 0 = b ' 0) /\ 943 (!a:word32 b. (~(align(a,4) + 8w) + b) ' 0 = ~b ' 0) /\ 944 (!a:word32 b. aligned_bx (align(a,4) + 8w + b) = aligned_bx b) /\ 945 !a:word32 b. aligned_bx (~(align(a,4) + 8w) + b) = 946 ((1 >< 0) b <> 3w:word2)`, 947 NTAC 3 STRIP_TAC \\ REPEAT GEN_TAC \\ REWRITE_TAC [word_plus8] 948 \\ Q.ABBREV_TAC `x = align (a,4) >>> 2 + 2w : word32` 949 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] 950 [aligned_bx_thm, align_248, WORD_ADD_BIT0, Once WORD_ADD_BIT, 951 extract_bit0_plus1, 952 wordsLib.WORD_DECIDE ``!a:word32. (0 >< 0) (~(a << 2)) = 1w:word32``, 953 wordsLib.WORD_DECIDE ``!a:word32. ~(a << 2) ' 1``, 954 wordsLib.WORD_DECIDE ``!a:word32. ~(a << 2) ' 0``, 955 wordsLib.WORD_DECIDE ``!a:word32. (~(a << 2)) ' 1``, 956 wordsLib.WORD_DECIDE ``!a:word32. (~(a << 2)) ' 0``] 957 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) [] 958 \\ METIS_TAC []); 959 960val aligned_bx_add_sub_pc3 = Q.prove( 961 `!a:word32 pc. 962 aligned_bx 963 ((if aligned_bx (a + -(align(pc,4) + 8w)) then a else 0w) + 964 -(align(pc,4) + 8w))`, 965 NTAC 2 STRIP_TAC \\ REWRITE_TAC [word_plus8] 966 \\ Q.ABBREV_TAC `x = align (pc,4) >>> 2 + 2w : word32` 967 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] [aligned_bx_def]); 968 969val aligned_bx_add_sub_pc = save_thm("aligned_bx_add_sub_pc", 970 Drule.LIST_CONJ 971 [CONJ (aligned_bx_add_sub_pc |> Thm.CONJUNCT1 |> Q.SPECL [`a`,`0w`]) 972 (aligned_bx_add_sub_pc |> Thm.CONJUNCT2 |> Q.SPECL [`a`,`0w`]) 973 |> SIMP_RULE (srw_ss()) [word_0, aligned_bx_0w], 974 aligned_bx_add_sub_pc, aligned_bx_add_sub_pc2, aligned_bx_add_sub_pc3]); 975 976val aligned_bx_add_with_carry_pair = Q.store_thm( 977 "aligned_bx_add_with_carry_pair", 978 `(!a:word32 c. 979 aligned_bx 980 (FST (add_with_carry 981 (if aligned_bx (FST (add_with_carry (a,a,c))) then a else 0w, 982 if aligned_bx (FST (add_with_carry (a,a,c))) then a else 0w, 983 c)))) /\ 984 (!a:word32 c. 985 aligned_bx 986 (FST (add_with_carry 987 (~if aligned_bx (FST (add_with_carry (~a,a,c))) then a else 0w, 988 if aligned_bx (FST (add_with_carry (~a,a,c))) then a else 0w, 989 c)))) /\ 990 (!a:word32 c. 991 aligned_bx 992 (FST (add_with_carry 993 (if aligned_bx (FST (add_with_carry (a,~a,c))) then a else 0w, 994 ~if aligned_bx (FST (add_with_carry (a,~a,c))) then a else 0w, 995 c))))`, 996 SRW_TAC [] [aligned_bx_def] 997 \\ SRW_TAC [boolSimps.LET_ss] [add_with_carry_def]); 998 999val aligned_bx_add_pair = Q.store_thm("aligned_bx_add_pair", 1000 `!a:word32. 1001 aligned_bx 1002 ((if aligned_bx (a + a) then a else 0w) + 1003 (if aligned_bx (a + a) then a else 0w))`, 1004 SRW_TAC [] [aligned_bx_def]); 1005 1006val aligned_bx_shift_pair = Q.prove( 1007 `(!f:bool[32] # num -> bool[32] # bool x a:word32. 1008 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1009 aligned_bx 1010 ((if aligned_bx (a && FST (f (a,x))) then a else 0w) && 1011 FST (f (if aligned_bx (a && FST (f (a,x))) then a else 0w,x)))) /\ 1012 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1013 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1014 aligned_bx 1015 ((if aligned_bx (a && ~FST (f (a,x))) then a else 0w) && 1016 ~FST (f (if aligned_bx (a && ~FST (f (a,x))) then a else 0w,x)))) /\ 1017 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1018 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1019 aligned_bx 1020 ((if aligned_bx (a ?? FST (f (a,x))) then a else 0w) ?? 1021 FST (f (if aligned_bx (a ?? FST (f (a,x))) then a else 0w,x)))) /\ 1022 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1023 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1024 aligned_bx 1025 ((if aligned_bx (a || FST (f (a,x))) then a else 0w) || 1026 FST (f (if aligned_bx (a || FST (f (a,x))) then a else 0w,x)))) /\ 1027 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1028 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1029 aligned_bx 1030 (FST (f (if aligned_bx (FST (f (a,x))) then a else 0w,x)))) /\ 1031 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1032 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1033 aligned_bx 1034 (~FST (f (if aligned_bx (~FST (f (a,x))) then a else 0w,x)))) /\ 1035 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1036 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1037 aligned_bx 1038 (-FST (f (if aligned_bx (-FST (f (a,x))) then a else 0w,x)))) /\ 1039 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1040 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1041 aligned_bx 1042 ((if aligned_bx (a + FST (f (a,x))) then a else 0w) + 1043 FST (f (if aligned_bx (a + FST (f (a,x))) then a else 0w,x)))) /\ 1044 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1045 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1046 aligned_bx 1047 ((if aligned_bx (a + -FST (f (a,x))) then a else 0w) + 1048 -FST (f (if aligned_bx (a + -FST (f (a,x))) then a else 0w,x)))) /\ 1049 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1050 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1051 aligned_bx 1052 (FST (f (if aligned_bx (FST (f (a,x)) + -a) then a else 0w,x)) + 1053 -if aligned_bx (FST (f (a,x)) + -a) then a else 0w))`, 1054 SRW_TAC [] [aligned_bx_def]); 1055 1056val aligned_bx_rrx_pair = Q.store_thm("aligned_bx_rrx_pair", 1057 `(!x a:word32. 1058 aligned_bx 1059 ((if aligned_bx (a && SND (word_rrx (x,a))) then a else 0w) && 1060 SND (word_rrx (x,if aligned_bx (a && SND (word_rrx (x,a))) 1061 then a else 0w)))) /\ 1062 (!x a:word32. 1063 aligned_bx 1064 ((if aligned_bx (a && ~SND (word_rrx (x,a))) then a else 0w) && 1065 ~SND (word_rrx (x,if aligned_bx (a && ~SND (word_rrx (x,a))) 1066 then a else 0w)))) /\ 1067 (!x a:word32. 1068 aligned_bx 1069 ((if aligned_bx (a ?? SND (word_rrx (x,a))) then a else 0w) ?? 1070 SND (word_rrx (x,if aligned_bx (a ?? SND (word_rrx (x,a))) 1071 then a else 0w)))) /\ 1072 (!x a:word32. 1073 aligned_bx 1074 ((if aligned_bx (a || SND (word_rrx (x,a))) then a else 0w) || 1075 SND (word_rrx (x,if aligned_bx (a || SND (word_rrx (x,a))) 1076 then a else 0w)))) /\ 1077 (!x a:word32. 1078 aligned_bx 1079 (SND (word_rrx 1080 (x,if aligned_bx (SND (word_rrx (x,a))) then a else 0w)))) /\ 1081 (!x a:word32. 1082 aligned_bx 1083 (~SND (word_rrx 1084 (x,if aligned_bx (~SND (word_rrx (x,a))) then a else 0w)))) /\ 1085 (!x a:word32. 1086 aligned_bx 1087 (-SND (word_rrx 1088 (x,if aligned_bx (-SND (word_rrx (x,a))) then a else 0w)))) /\ 1089 (!x a:word32. 1090 aligned_bx 1091 ((if aligned_bx (a + SND (word_rrx (x,a))) then a else 0w) + 1092 SND (word_rrx (x,if aligned_bx (a + SND (word_rrx (x,a))) 1093 then a else 0w)))) /\ 1094 (!x a:word32. 1095 aligned_bx 1096 ((if aligned_bx (a + -SND (word_rrx (x,a))) then a else 0w) + 1097 -SND (word_rrx (x,if aligned_bx (a + -SND (word_rrx (x,a))) 1098 then a else 0w)))) /\ 1099 (!x a:word32. 1100 aligned_bx 1101 (SND (word_rrx (x,if aligned_bx (SND (word_rrx (x,a)) + -a) 1102 then a else 0w)) + 1103 -if aligned_bx (SND (word_rrx (x,a)) + -a) then a else 0w))`, 1104 SRW_TAC [] [aligned_bx_def] \\ Cases_on `x` \\ SRW_TAC [] [word_rrx_0]); 1105 1106val aligned_bx_add_with_carry_shift_pair = Q.prove( 1107 `(!f:bool[32] # num -> bool[32] # bool x a:word32. 1108 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1109 aligned_bx 1110 (FST (add_with_carry 1111 (if aligned_bx (FST (add_with_carry (a,FST (f (a,x)),c))) 1112 then a else 0w, 1113 FST (f (if aligned_bx (FST (add_with_carry (a,FST (f (a,x)),c))) 1114 then a else 0w,x)), 1115 c)))) /\ 1116 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1117 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1118 aligned_bx 1119 (FST (add_with_carry 1120 (~if aligned_bx (FST (add_with_carry (~a,FST (f (a,x)),c))) 1121 then a else 0w, 1122 FST (f (if aligned_bx (FST (add_with_carry (~a,FST (f (a,x)),c))) 1123 then a else 0w,x)), 1124 c)))) /\ 1125 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1126 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1127 aligned_bx 1128 (FST (add_with_carry 1129 (if aligned_bx (FST (add_with_carry (a,~FST (f (a,x)),c))) 1130 then a else 0w, 1131 ~FST (f (if aligned_bx (FST (add_with_carry (a,~FST (f (a,x)),c))) 1132 then a else 0w,x)), 1133 c))))`, 1134 SRW_TAC [] [aligned_bx_def] 1135 \\ SRW_TAC [boolSimps.LET_ss] [add_with_carry_def]); 1136 1137val aligned_bx_add_with_carry_rrx_pair = Q.store_thm( 1138 "aligned_bx_add_with_carry_rrx_pair", 1139 `(!x a:word32. 1140 aligned_bx 1141 (FST (add_with_carry 1142 (if aligned_bx (FST (add_with_carry (a,SND (word_rrx (x,a)),c))) 1143 then a else 0w, 1144 SND (word_rrx (x, 1145 if aligned_bx (FST (add_with_carry (a,SND (word_rrx (x,a)),c))) 1146 then a else 0w)), 1147 c)))) /\ 1148 (!x a:word32. 1149 aligned_bx 1150 (FST (add_with_carry 1151 (~if aligned_bx (FST (add_with_carry (~a,SND (word_rrx (x,a)),c))) 1152 then a else 0w, 1153 SND (word_rrx (x, 1154 if aligned_bx (FST (add_with_carry (~a,SND (word_rrx (x,a)),c))) 1155 then a else 0w)), 1156 c)))) /\ 1157 (!x a:word32. 1158 aligned_bx 1159 (FST (add_with_carry 1160 (if aligned_bx (FST (add_with_carry (a,~SND (word_rrx (x,a)),c))) 1161 then a else 0w, 1162 ~SND (word_rrx (x, 1163 if aligned_bx (FST (add_with_carry (a,~SND (word_rrx (x,a)),c))) 1164 then a else 0w)), 1165 c))))`, 1166 SRW_TAC [] [aligned_bx_def] \\ Cases_on `x` 1167 \\ SRW_TAC [boolSimps.LET_ss] [add_with_carry_def, word_rrx_0]); 1168 1169val lem = Q.prove( 1170 `(!x:word32. n2w (w2n x + 4294967296) = x) /\ 1171 (!x:word32. n2w (w2n x + 4294967295) = x + -1w) /\ 1172 (!x:word32. n2w (w2n x + 0x80000000) = x + 0x80000000w) /\ 1173 (!x:word32. n2w (w2n x + 0x7FFFFFFF) = x + 0x7FFFFFFFw) /\ 1174 (!x:word32. n2w (w2n (~x) + 1) = ~x + 1w) /\ 1175 !x:word32. n2w (w2n (x << 2) + 1) = x << 2 || 1w`, 1176 REPEAT STRIP_TAC 1177 << [ 1178 ONCE_REWRITE_TAC [GSYM n2w_mod] 1179 \\ SRW_TAC [ARITH_ss] [ADD_MODULUS_LEFT, 1180 n2w_mod |> INST_TYPE [alpha |-> ``:32``] |> EVAL_RULE], 1181 SRW_TAC [] [word_add_def], 1182 SRW_TAC [] [word_add_def], 1183 SRW_TAC [] [word_add_def], 1184 SRW_TAC [] [word_add_def], 1185 `n2w (w2n (x << 2) + 1) = x << 2 + 1w` by SRW_TAC [] [word_add_def] 1186 \\ POP_ASSUM SUBST1_TAC 1187 \\ MATCH_MP_TAC WORD_ADD_OR 1188 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []]); 1189 1190val lem2 = Q.prove( 1191 `(!x:word32. (1 >< 0) (x << 2 + -1w) <> 2w:word2) /\ 1192 (!x:word32. (1 >< 0) (x << 2 + 1w) <> 2w:word2) /\ 1193 (!x:word32. (1 >< 0) (x << 2 + 0x7FFFFFFFw) <> 2w:word2) /\ 1194 (!x:word32. (1 >< 0) (x << 2 + 0x80000001w) <> 2w:word2) /\ 1195 (!x:word32. (1 >< 0) (~(x << 2) + 0x80000000w) <> 2w:word2) /\ 1196 (!x:word32. (1 >< 0) (~(x << 2)) <> 2w:word2)`, 1197 SRW_TAC [fcpLib.FCP_ss,wordsLib.SIZES_ss] 1198 [word_extract_def, w2w, word_bits_def] 1199 \\ Q.EXISTS_TAC `0` 1200 \\ SRW_TAC [fcpLib.FCP_ss,ARITH_ss] [] 1201 \\ SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) [Once WORD_ADD_BIT0]); 1202 1203val lem3 = Q.prove( 1204 `(!x:word32. (1 >< 0) (~(x << 2) + 1w) <> 2w:word2) /\ 1205 (!x:word32. (1 >< 0) (~(x << 2) + 0x80000001w) <> 2w:word2) /\ 1206 (!x:word32. (1 >< 0) (x << 2 + 0x80000000w) <> 2w:word2)`, 1207 SRW_TAC [fcpLib.FCP_ss,wordsLib.SIZES_ss] 1208 [word_extract_def, w2w, word_bits_def, word_1comp_def] 1209 \\ Q.EXISTS_TAC `1` 1210 \\ SRW_TAC [fcpLib.FCP_ss,wordsLib.WORD_EXTRACT_ss,ARITH_ss] 1211 [Once WORD_ADD_BIT, extract_bit0_plus1] 1212 \\ FULL_SIMP_TAC (std_ss++wordsLib.WORD_BIT_EQ_ss) []); 1213 1214val aligned_bx_add_sub_shift_pc = Q.prove( 1215 `(!f:bool[32] # num -> bool[32] # bool x a:word32 pc. 1216 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1217 aligned_bx 1218 (FST (f (if aligned_bx (FST (f (a,x)) + -(align (pc,4) + 8w)) 1219 then a else 0w,x)) + -(align (pc,4) + 8w))) /\ 1220 (!f:bool[32] # num -> bool[32] # bool x a:word32 pc. 1221 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1222 aligned_bx 1223 (FST (add_with_carry (~(align (pc,4) + 8w), 1224 FST (f 1225 (if aligned_bx (FST (add_with_carry 1226 (~(align (pc, 4) + 8w), FST (f (a,x)), c))) 1227 then 1228 a 1229 else 1230 0w,x)),c)))) /\ 1231 (!f:bool[32] # num -> bool[32] # bool x a:word32 pc. 1232 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1233 aligned_bx 1234 (FST (add_with_carry (align (pc,4) + 8w, 1235 ~FST (f 1236 (if aligned_bx (FST (add_with_carry 1237 (align (pc, 4) + 8w, ~FST (f (a,x)), c))) 1238 then 1239 a 1240 else 1241 0w,x)),c)))) /\ 1242 (!f:bool[32] # num -> bool[32] # bool x a:word32 pc. 1243 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1244 aligned_bx 1245 (FST (add_with_carry (align (pc,4) + 8w, 1246 FST (f 1247 (if aligned_bx (FST (add_with_carry 1248 (align (pc, 4) + 8w, FST (f (a,x)), c))) 1249 then 1250 a 1251 else 1252 0w,x)),c))))`, 1253 REPEAT STRIP_TAC \\ REWRITE_TAC [word_plus8] 1254 \\ Q.ABBREV_TAC `z = align (pc,4) >>> 2 + 2w : word32` 1255 \\ SRW_TAC [boolSimps.LET_ss] [aligned_bx_def, add_with_carry_def, 1256 GSYM word_add_def, word_add_plus1] 1257 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_EXTRACT_ss) 1258 [lem, lem2, lem3, GSYM word_add_def, word_add_plus1]); 1259 1260val aligned_bx_add_sub_rrx_pc = Q.store_thm("aligned_bx_add_sub_rrx_pc", 1261 `(!x a:word32 pc. 1262 aligned_bx 1263 (SND (word_rrx 1264 (x,if aligned_bx (SND (word_rrx (x,a)) + -(align (pc,4) + 8w)) 1265 then a else 0w)) + -(align (pc,4) + 8w))) /\ 1266 (!x a:word32 pc. 1267 aligned_bx 1268 (FST (add_with_carry (~(align (pc,4) + 8w), 1269 SND (word_rrx 1270 (x,if aligned_bx (FST (add_with_carry 1271 (~(align (pc, 4) + 8w), SND (word_rrx (x,a)), c))) 1272 then a else 0w)),c)))) /\ 1273 (!x a:word32 pc. 1274 aligned_bx 1275 (FST (add_with_carry (align (pc,4) + 8w, 1276 ~SND (word_rrx 1277 (x,if aligned_bx (FST (add_with_carry 1278 (align (pc, 4) + 8w, ~SND (word_rrx (x,a)), c))) 1279 then a else 0w)),c)))) /\ 1280 (!x a:word32 pc. 1281 aligned_bx 1282 (FST (add_with_carry (align (pc,4) + 8w, 1283 SND (word_rrx 1284 (x,if aligned_bx (FST (add_with_carry 1285 (align (pc, 4) + 8w, SND (word_rrx (x,a)), c))) 1286 then a else 0w)),c))))`, 1287 REPEAT STRIP_TAC \\ REWRITE_TAC [word_plus8] \\ Cases_on `x` 1288 \\ Q.ABBREV_TAC `z = align (pc,4) >>> 2 + 2w : word32` 1289 \\ SRW_TAC [boolSimps.LET_ss] [aligned_bx_def, add_with_carry_def, 1290 GSYM word_add_def, word_add_plus1, word_rrx_0] 1291 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_EXTRACT_ss) 1292 [lem, lem2, lem3, GSYM word_add_def, word_add_plus1]); 1293 1294val aligned_bx_pair_shift_thms = save_thm("aligned_bx_pair_shift_thms", 1295 Drule.LIST_CONJ (List.concat 1296 (List.map (fn thm => 1297 List.map (fn t => (CONJ (thm |> Q.SPECL [t,`NUMERAL (BIT1 n)`,`a`]) 1298 (thm |> Q.SPECL [t,`NUMERAL (BIT2 n)`,`a`])) 1299 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,NUMERAL_FST_SHIFT_C]) 1300 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 1301 (Drule.CONJUNCTS aligned_bx_shift_pair @ 1302 Drule.CONJUNCTS aligned_bx_add_sub_shift_pc @ 1303 Drule.CONJUNCTS aligned_bx_add_with_carry_shift_pair)))); 1304 1305val aligned_bx_add_with_carry_literal_pc = 1306 Q.store_thm("aligned_bx_add_with_carry_literal_pc", 1307 `(!pc:word32 n c. 1308 aligned_bx 1309 (FST (add_with_carry (align (pc,4) + 8w, n2w n, c))) = 1310 if c then aligned_bx (n2w n + 9w:word32) 1311 else aligned_bx (n2w n + 8w:word32)) /\ 1312 (!pc:word32 n c. 1313 aligned_bx 1314 (FST (add_with_carry (~(align (pc,4) + 8w), n2w n, c))) = 1315 if c then (1 >< 0) (n2w n + 1w:word32) <> 3w:word2 1316 else (1 >< 0) (n2w n : word32) <> 3w:word2)`, 1317 REPEAT STRIP_TAC \\ Cases_on `c` 1318 \\ SRW_TAC [] [FST_ADD_WITH_CARRY] 1319 \\ Q.ABBREV_TAC `x:word32 = n2w n` 1320 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC, aligned_bx_add_sub_pc, 1321 ONCE_REWRITE_RULE [WORD_ADD_COMM] aligned_bx_add_sub_pc, 1322 ``x + -1w * (a + 0x8w) = ~(a + 8w) + (x + 0x1w)`` 1323 |> wordsLib.WORD_ARITH_CONV |> EQT_ELIM] 1324 \\ SRW_TAC [] [WORD_NOT, WORD_LEFT_ADD_DISTRIB] 1325 ); 1326 1327val aligned_bx_1comp_pc = Q.store_thm("aligned_bx_1comp_pc", 1328 `!a:word32. aligned_bx (~(align (a,4) + 8w))`, 1329 STRIP_TAC \\ REWRITE_TAC [word_plus8] 1330 \\ Q.ABBREV_TAC `x = align (a,4) >>> 2 + 2w : word32` 1331 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss, ARITH_ss] [aligned_bx_def]); 1332 1333val aligned_bx_add_with_carry_pc = Q.store_thm("aligned_bx_add_with_carry_pc", 1334 `(!pc a:word32. 1335 aligned_bx 1336 (FST (add_with_carry 1337 (align (pc,4) + 8w, 1338 if aligned_bx (FST (add_with_carry (align (pc,4) + 8w,a,c))) 1339 then a else 0w,c)))) /\ 1340 (!pc a:word32. 1341 aligned_bx 1342 (FST (add_with_carry 1343 (~(align (pc,4) + 8w), 1344 if aligned_bx (FST (add_with_carry (~(align (pc,4) + 8w),a,c))) 1345 then a else 0w,c)))) /\ 1346 (!pc a:word32. 1347 aligned_bx 1348 (FST (add_with_carry 1349 (align (pc,4) + 8w, 1350 ~if aligned_bx (FST (add_with_carry (align (pc,4) + 8w,~a,c))) 1351 then a else 0w,c))))`, 1352 REPEAT STRIP_TAC \\ REWRITE_TAC [word_plus8] 1353 \\ Q.ABBREV_TAC `x = align (pc,4) >>> 2 + 2w : word32` 1354 \\ SRW_TAC [] [aligned_bx_def] 1355 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss,boolSimps.LET_ss,ARITH_ss] 1356 [GSYM word_add_def, word_add_plus1, add_with_carry_def, 1357 lem, lem2, lem3] 1358 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []); 1359 1360val aligned_bx_add_with_carry_pair_pc = Q.store_thm( 1361 "aligned_bx_add_with_carry_pair_pc", 1362 `(!a:word32 c. 1363 aligned_bx 1364 (FST (add_with_carry (align (a,4) + 8w, align (a,4) + 8w, c)))) /\ 1365 (!a:word32 c. 1366 aligned_bx 1367 (FST (add_with_carry (~(align (a,4) + 8w), align (a,4) + 8w, c)))) /\ 1368 (!a:word32 c. 1369 aligned_bx 1370 (FST (add_with_carry (align (a,4) + 8w, ~(align (a,4) + 8w), c))))`, 1371 SRW_TAC [boolSimps.LET_ss] 1372 [WORD_NOT, WORD_LEFT_ADD_DISTRIB, GSYM word_add_def, word_add_plus1, 1373 add_with_carry_def] 1374 \\ SIMP_TAC std_ss [aligned_bx_add_sub_pc, GSYM WORD_ADD_ASSOC, 1375 wordsLib.WORD_DECIDE ``2w * a = a + a:word32``] 1376 \\ EVAL_TAC); 1377 1378val aligned_and_aligned_bx = Q.prove( 1379 `(!f:bool[32] # num -> bool[32] # bool a:word32 x. 1380 aligned 1381 (if aligned (a,4) /\ aligned_bx (a + 8w ?? FST (f (a + 8w,x))) 1382 then a else -8w,4)) /\ 1383 (!f:bool[32] # num -> bool[32] # bool a:word32 x c. 1384 aligned 1385 (if aligned (a,4) /\ 1386 aligned_bx (FST (add_with_carry 1387 (~(a + 8w), FST (f (a + 8w,x)), c))) 1388 then a else -8w,4)) /\ 1389 (!f:bool[32] # num -> bool[32] # bool a:word32 x c. 1390 aligned 1391 (if aligned (a,4) /\ 1392 aligned_bx (FST (add_with_carry 1393 (a + 8w, FST (f (a + 8w,x)), c))) 1394 then a else -8w,4)) /\ 1395 (!f:bool[32] # num -> bool[32] # bool a:word32 x c. 1396 aligned 1397 (if aligned (a,4) /\ 1398 aligned_bx (FST (add_with_carry 1399 (a + 8w, ~FST (f (a + 8w,x)), c))) 1400 then a else -8w,4)) /\ 1401 (!f:bool[32] # num -> bool[32] # bool a:word32 x. 1402 aligned 1403 (if aligned (a,4) /\ aligned_bx (FST (f (a + 8w,x)) + -(a + 8w)) 1404 then a else -8w,4)) /\ 1405 (!f:bool[32] # num -> bool[32] # bool a:word32 x. 1406 aligned 1407 (if aligned (a,4) /\ aligned_bx (a + 8w + FST (f (a + 8w,x))) 1408 then a else -8w,4)) /\ 1409 (!f:bool[32] # num -> bool[32] # bool a:word32 x. 1410 aligned 1411 (if aligned (a,4) /\ aligned_bx (a + 8w + -FST (f (a + 8w,x))) 1412 then a else -8w,4)) /\ 1413 (!f:bool[32] # num -> bool[32] # bool a:word32 x. 1414 aligned 1415 (if aligned (a,4) /\ aligned_bx (FST (f (a + 8w,x))) 1416 then a else -8w,4)) /\ 1417 (!f:bool[32] # num -> bool[32] # bool a:word32 x. 1418 aligned 1419 (if aligned (a,4) /\ aligned_bx (~FST (f (a + 8w,x))) 1420 then a else -8w,4)) /\ 1421 (!f:bool[32] # num -> bool[32] # bool a:word32 x. 1422 aligned 1423 (if aligned (a,4) /\ aligned_bx (a + 8w || FST (f (a + 8w,x))) 1424 then a else -8w,4))`, 1425 SRW_TAC [] [] \\ EVAL_TAC); 1426 1427val minus8 = EVAL ``-8w:word32``; 1428 1429val aligned_and_aligned_bx_thms = save_thm("aligned_and_aligned_bx_thms", 1430 Drule.LIST_CONJ (List.concat 1431 (List.map (fn thm => map (fn t => thm |> Q.SPEC t |> REWRITE_RULE [minus8]) 1432 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 1433 (Drule.CONJUNCTS aligned_and_aligned_bx)))); 1434 1435val aligned_and_aligned_bx_rrx = Q.prove( 1436 `(!a:word32 x. 1437 aligned 1438 (if aligned (a,4) /\ aligned_bx (a + 8w ?? SND (word_rrx (x,a + 8w))) 1439 then a else -8w,4)) /\ 1440 (!a:word32 x c. 1441 aligned 1442 (if aligned (a,4) /\ 1443 aligned_bx (FST (add_with_carry 1444 (~(a + 8w), SND (word_rrx (x,a + 8w)), c))) 1445 then a else -8w,4)) /\ 1446 (!a:word32 x c. 1447 aligned 1448 (if aligned (a,4) /\ 1449 aligned_bx (FST (add_with_carry 1450 (a + 8w, SND (word_rrx (x,a + 8w)), c))) 1451 then a else -8w,4)) /\ 1452 (!a:word32 x c. 1453 aligned 1454 (if aligned (a,4) /\ 1455 aligned_bx (FST (add_with_carry 1456 (a + 8w, ~SND (word_rrx (x,a + 8w)), c))) 1457 then a else -8w,4)) /\ 1458 (!a:word32 x. 1459 aligned 1460 (if aligned (a,4) /\ aligned_bx (SND (word_rrx (x,a + 8w)) + -(a + 8w)) 1461 then a else -8w,4)) /\ 1462 (!a:word32 x. 1463 aligned 1464 (if aligned (a,4) /\ aligned_bx (a + 8w + SND (word_rrx (x,a + 8w))) 1465 then a else -8w,4)) /\ 1466 (!a:word32 x. 1467 aligned 1468 (if aligned (a,4) /\ aligned_bx (a + 8w + -SND (word_rrx (x,a + 8w))) 1469 then a else -8w,4)) /\ 1470 (!a:word32 x. 1471 aligned 1472 (if aligned (a,4) /\ aligned_bx (SND (word_rrx (x,a + 8w))) 1473 then a else -8w,4)) /\ 1474 (!a:word32 x. 1475 aligned 1476 (if aligned (a,4) /\ aligned_bx (~SND (word_rrx (x,a + 8w))) 1477 then a else -8w,4)) /\ 1478 (!a:word32 x. 1479 aligned 1480 (if aligned (a,4) /\ aligned_bx (a + 8w || SND (word_rrx (x,a + 8w))) 1481 then a else -8w,4))`, 1482 SRW_TAC [] [] \\ EVAL_TAC); 1483 1484val aligned_and_aligned_bx_rrx = save_thm("aligned_and_aligned_bx_rrx", 1485 REWRITE_RULE [minus8] aligned_and_aligned_bx_rrx); 1486 1487val lem = Q.prove( 1488 `(!a:word32. FST (add_with_carry (a,0w,c)) = if c then a + 1w else a) /\ 1489 (!a:word32. FST (add_with_carry (0w,a,c)) = if c then a + 1w else a)`, 1490 SRW_TAC [boolSimps.LET_ss] [add_with_carry_def, word_add_def]); 1491 1492val aligned_bx_and_aligned_add_with_carry = Q.prove( 1493 `(!f:bool[32] # num -> bool[32] # bool x a:word32 c. 1494 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1495 aligned_bx 1496 (FST (add_with_carry 1497 ((if aligned (a,4) /\ 1498 aligned_bx (FST (add_with_carry 1499 (a + 8w, FST (f (a + 8w,x)),c))) 1500 then a else -8w) + 8w, 1501 FST (f ((if aligned (a,4) /\ 1502 aligned_bx (FST (add_with_carry 1503 (a + 8w, FST (f (a + 8w,x)),c))) 1504 then a else -8w) + 8w,x)),c)))) /\ 1505 (!f:bool[32] # num -> bool[32] # bool x a:word32 c. 1506 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1507 aligned_bx 1508 (FST (add_with_carry 1509 (~((if aligned (a,4) /\ 1510 aligned_bx (FST (add_with_carry 1511 (~(a + 8w), FST (f (a + 8w,x)),c))) 1512 then a else -8w) + 8w), 1513 FST (f ((if aligned (a,4) /\ 1514 aligned_bx (FST (add_with_carry 1515 (~(a + 8w), FST (f (a + 8w,x)),c))) 1516 then a else -8w) + 8w,x)),c)))) /\ 1517 (!f:bool[32] # num -> bool[32] # bool x a:word32 c. 1518 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1519 aligned_bx 1520 (FST (add_with_carry 1521 ((if aligned (a,4) /\ 1522 aligned_bx (FST (add_with_carry 1523 (a + 8w, ~FST (f (a + 8w,x)),c))) 1524 then a else -8w) + 8w, 1525 ~FST (f ((if aligned (a,4) /\ 1526 aligned_bx (FST (add_with_carry 1527 (a + 8w, ~FST (f (a + 8w,x)),c))) 1528 then a else -8w) + 8w,x)),c))))`, 1529 SRW_TAC [] [aligned_bx_0w, lem] 1530 \\ SRW_TAC [] [aligned_bx_0w, aligned_bx_1w, aligned_bx_m1w]); 1531 1532val aligned_bx_and_aligned_add_with_carry_rrx = Q.prove( 1533 `(!x a:word32 c. 1534 aligned_bx 1535 (FST (add_with_carry 1536 ((if aligned (a,4) /\ 1537 aligned_bx (FST (add_with_carry 1538 (a + 8w, SND (word_rrx (x,a + 8w)),c))) 1539 then a else -8w) + 8w, 1540 SND (word_rrx (x,(if aligned (a,4) /\ 1541 aligned_bx (FST (add_with_carry 1542 (a + 8w, SND (word_rrx (x,a + 8w)),c))) 1543 then a else -8w) + 8w)),c)))) /\ 1544 (!x a:word32 c. 1545 aligned_bx 1546 (FST (add_with_carry 1547 (~((if aligned (a,4) /\ 1548 aligned_bx (FST (add_with_carry 1549 (~(a + 8w), SND (word_rrx (x,a + 8w)),c))) 1550 then a else -8w) + 8w), 1551 SND (word_rrx (x,(if aligned (a,4) /\ 1552 aligned_bx (FST (add_with_carry 1553 (~(a + 8w), SND (word_rrx (x,a + 8w)),c))) 1554 then a else -8w) + 8w)),c)))) /\ 1555 (!x a:word32 c. 1556 aligned_bx 1557 (FST (add_with_carry 1558 ((if aligned (a,4) /\ 1559 aligned_bx (FST (add_with_carry 1560 (a + 8w, ~SND (word_rrx (x,a + 8w)),c))) 1561 then a else -8w) + 8w, 1562 ~SND (word_rrx (x,(if aligned (a,4) /\ 1563 aligned_bx (FST (add_with_carry 1564 (a + 8w, ~SND (word_rrx (x,a + 8w)),c))) 1565 then a else -8w) + 8w)),c))))`, 1566 SRW_TAC [] [aligned_bx_0w, lem] \\ Cases_on `x` 1567 \\ SRW_TAC [] [word_rrx_0, lem, aligned_bx_0w, aligned_bx_1w, 1568 aligned_bx_m1w, 1569 EVAL ``aligned_bx (0x80000000w:word32)``, 1570 EVAL ``aligned_bx (0x80000001w:word32)``, 1571 EVAL ``aligned_bx (0x7FFFFFFFw:word32)``] 1572 \\ Cases_on `c` 1573 \\ SRW_TAC [boolSimps.LET_ss] [add_with_carry_def] 1574 \\ EVAL_TAC); 1575 1576val aligned_bx_and_aligned_add_with_carry_rrx = save_thm( 1577 "aligned_bx_and_aligned_add_with_carry_rrx", 1578 REWRITE_RULE [minus8] aligned_bx_and_aligned_add_with_carry_rrx); 1579 1580val aligned_bx_and_aligned = Q.prove( 1581 `(!f:bool[32] # num -> bool[32] # bool x a:word32. 1582 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1583 aligned_bx 1584 ((if aligned (a,4) /\ aligned_bx (a + 8w ?? FST (f (a + 8w,x))) 1585 then a else -8w) + 8w ?? 1586 FST (f ((if aligned (a,4) /\ aligned_bx (a + 8w ?? FST (f (a + 8w,x))) 1587 then a else -8w) + 8w,x)))) /\ 1588 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1589 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1590 aligned_bx 1591 (FST (f ((if aligned (a,4) /\ aligned_bx (FST (f (a + 8w,x)) + -(a + 8w)) 1592 then a else -8w) + 8w,x)) + 1593 -((if aligned (a,4) /\ aligned_bx (FST (f (a + 8w,x)) + -(a + 8w)) 1594 then a else -8w) + 8w))) /\ 1595 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1596 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1597 aligned_bx 1598 ((if aligned (a,4) /\ aligned_bx (a + 8w + FST (f (a + 8w,x))) 1599 then a else -8w) + 8w + 1600 FST (f ((if aligned (a,4) /\ aligned_bx (a + 8w + FST (f (a + 8w,x))) 1601 then a else -8w) + 8w,x)))) /\ 1602 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1603 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1604 aligned_bx 1605 ((if aligned (a,4) /\ aligned_bx (a + 8w + -FST (f (a + 8w,x))) 1606 then a else -8w) + 8w + 1607 -FST (f ((if aligned (a,4) /\ aligned_bx (a + 8w + -FST (f (a + 8w,x))) 1608 then a else -8w) + 8w,x)))) /\ 1609 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1610 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1611 aligned_bx 1612 (FST (f ((if aligned (a,4) /\ aligned_bx (FST (f (a + 8w,x))) 1613 then a else -8w) + 8w,x)))) /\ 1614 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1615 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1616 aligned_bx 1617 (~FST (f ((if aligned (a,4) /\ aligned_bx (~FST (f (a + 8w,x))) 1618 then a else -8w) + 8w,x)))) /\ 1619 (!f:bool[32] # num -> bool[32] # bool x a:word32. 1620 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1621 aligned_bx 1622 ((if aligned (a,4) /\ aligned_bx (a + 8w || FST (f (a + 8w,x))) 1623 then a else -8w) + 8w || 1624 FST (f ((if aligned (a,4) /\ aligned_bx (a + 8w || FST (f (a + 8w,x))) 1625 then a else -8w) + 8w,x))))`, 1626 SRW_TAC [] [aligned_bx_0w] \\ EVAL_TAC); 1627 1628val aligned_bx_and_aligned_thms = save_thm("aligned_bx_and_aligned_thms", 1629 Drule.LIST_CONJ (List.concat 1630 (List.map (fn thm => 1631 List.map (fn t => (CONJ (thm |> Q.SPECL [t,`NUMERAL (BIT1 n)`,`a`]) 1632 (thm |> Q.SPECL [t,`NUMERAL (BIT2 n)`,`a`])) 1633 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,NUMERAL_FST_SHIFT_C,minus8]) 1634 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 1635 (Drule.CONJUNCTS aligned_bx_and_aligned_add_with_carry @ 1636 Drule.CONJUNCTS aligned_bx_and_aligned)))); 1637 1638val aligned_bx_and_aligned_rrx = Q.prove( 1639 `(!x a:word32. 1640 aligned_bx 1641 ((if aligned (a,4) /\ aligned_bx (a + 8w ?? SND (word_rrx (x,a + 8w))) 1642 then a else -8w) + 8w ?? 1643 SND (word_rrx (x, 1644 (if aligned (a,4) /\ aligned_bx (a + 8w ?? SND (word_rrx (x,a + 8w))) 1645 then a else -8w) + 8w)))) /\ 1646 (!x a:word32. 1647 aligned_bx 1648 (SND (word_rrx (x, 1649 (if aligned (a,4) /\ aligned_bx (SND (word_rrx (x,a + 8w)) + -(a + 8w)) 1650 then a else -8w) + 8w)) + 1651 -((if aligned (a,4) /\ aligned_bx (SND (word_rrx (x,a + 8w)) + -(a + 8w)) 1652 then a else -8w) + 8w))) /\ 1653 (!x a:word32. 1654 aligned_bx 1655 ((if aligned (a,4) /\ aligned_bx (a + 8w + SND (word_rrx (x,a + 8w))) 1656 then a else -8w) + 8w + 1657 SND (word_rrx (x, 1658 (if aligned (a,4) /\ aligned_bx (a + 8w + SND (word_rrx (x,a + 8w))) 1659 then a else -8w) + 8w)))) /\ 1660 (!x a:word32. 1661 aligned_bx 1662 ((if aligned (a,4) /\ aligned_bx (a + 8w + -SND (word_rrx (x,a + 8w))) 1663 then a else -8w) + 8w + 1664 -SND (word_rrx (x, 1665 (if aligned (a,4) /\ aligned_bx (a + 8w + -SND (word_rrx (x,a + 8w))) 1666 then a else -8w) + 8w)))) /\ 1667 (!x a:word32. 1668 aligned_bx 1669 (SND (word_rrx (x, 1670 (if aligned (a,4) /\ aligned_bx (SND (word_rrx (x,a + 8w))) 1671 then a else -8w) + 8w)))) /\ 1672 (!x a:word32. 1673 aligned_bx 1674 (~SND (word_rrx (x, 1675 (if aligned (a,4) /\ aligned_bx (~SND (word_rrx (x,a + 8w))) 1676 then a else -8w) + 8w)))) /\ 1677 (!x a:word32. 1678 aligned_bx 1679 ((if aligned (a,4) /\ aligned_bx (a + 8w || SND (word_rrx (x,a + 8w))) 1680 then a else -8w) + 8w || 1681 SND (word_rrx (x, 1682 (if aligned (a,4) /\ aligned_bx (a + 8w || SND (word_rrx (x,a + 8w))) 1683 then a else -8w) + 8w))))`, 1684 SRW_TAC [] [aligned_bx_0w] \\ Cases_on `x` \\ EVAL_TAC); 1685 1686val aligned_bx_and_aligned_rrx = save_thm("aligned_bx_and_aligned_rrx", 1687 REWRITE_RULE [minus8] aligned_bx_and_aligned_rrx); 1688 1689val align_ldr_lsl = Q.store_thm("align_ldr_lsl", 1690 `!pc rm: word32. 1691 align (pc,4) <> 1692 align (pc,4) + 8w + 1693 FST 1694 (LSL_C 1695 (if 1696 aligned (align (pc,4) + 8w + 1697 FST (LSL_C (if rm << 2 <> 0xFFFFFFF8w then rm else 0w,2)), 4) 1698 then 1699 (if rm << 2 <> 0xFFFFFFF8w then rm else 0w) 1700 else 1701 0w,2))`, 1702 SRW_TAC [boolSimps.LET_ss, wordsLib.WORD_CANCEL_ss] [LSL_C_def]); 1703 1704(* ------------------------------------------------------------------------- *) 1705 1706val aligned_aligned = Q.store_thm("aligned_aligned", 1707 `(!a:word32 b. aligned(if b then align(a,4) else 0xFFFFFFF8w,4)) /\ 1708 (!a:word32 b. aligned (if aligned (a,4) /\ b then a else 0xFFFFFFF8w, 4)) /\ 1709 (!a:word8. aligned (if aligned (a,4) then a else 0w, 4)) /\ 1710 (!a:word32 b c. 1711 aligned 1712 ((if b /\ aligned (a + 8w,4) /\ c then a else 0xFFFFFFF8w) + 8w, 4)) /\ 1713 (!a:word32. aligned(if aligned(a,4) then a else 0w,4)) /\ 1714 (!a:word32. aligned(~(if aligned(~a,4) then a else 0xFFFFFFFFw),4)) /\ 1715 (!a:word32 b. aligned((if aligned(a && b,4) then a else 0w) && b,4)) /\ 1716 (!a:word32 b. aligned((if aligned(a ?? b,4) then a else b) ?? b,4)) /\ 1717 (!a:word32 b:word32. 1718 aligned((if aligned(a,4) /\ aligned(b,4) then a else 0w),4) /\ 1719 aligned((if aligned(a,4) /\ aligned(b,4) then b else 0w),4)) /\ 1720 (!a:word32 b. 1721 aligned(align(a,4) + 8w + 1722 (if aligned(align(a,4) + 8w + b,4) then b else 0w),4)) /\ 1723 (!a:word32 b. 1724 aligned(align(a,4) + 8w + 1725 -(if aligned(align(a,4) + 8w + -b,4) then b else 0w),4))`, 1726 SRW_TAC [] [aligned_align, aligned_sum] \\ EVAL_TAC); 1727 1728val aligned_over_bitwise = Q.store_thm("aligned_over_bitwise", 1729 `(!a b:word32. aligned(align(a,4) + 8w && b, 4)) /\ 1730 (!a:word32. ~aligned(~(align(a,4) + 8w), 4)) /\ 1731 (!a b:word32. aligned(align(a,4) + 8w ?? b, 4) = aligned(b,4)) /\ 1732 (!a b:word32. aligned(a || b, 4) = aligned(a,4) /\ aligned(b,4))`, 1733 SRW_TAC [wordsLib.WORD_EXTRACT_ss] [align_bits_sum, aligned_248, align_248, 1734 wordsLib.WORD_DECIDE ``((1 >< 0) (~a) = 0w:word2) = 1735 ((1 >< 0) (a:word32) = 3w:word2)``] 1736 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [] 1737 \\ METIS_TAC []); 1738 1739val word2_cases = wordsLib.WORD_DECIDE 1740 ``!a:word2. (a = 0w) \/ (a = 1w) \/ (a = 2w) \/ (a = 3w)``; 1741 1742val align_over_and = 1743 wordsTheory.WORD_w2w_OVER_ADD 1744 |> INST_TYPE [alpha |-> ``:32``, beta |-> ``:2``] 1745 |> SIMP_RULE (srw_ss()) 1746 [wordsLib.WORD_DECIDE ``w2w (w:word32) = ((1 >< 0) w):word2``] 1747 |> Once; 1748 1749val aligned_neg = Q.store_thm("aligned_neg", 1750 `!a:word32. aligned(-a,4) = aligned(a,4)`, 1751 SRW_TAC [] [WORD_NEG, aligned_248, align_over_and, 1752 wordsLib.WORD_DECIDE ``(1 >< 0) (~(a:word32)) = ~((1 >< 0) a) : word2``] 1753 \\ Q.SPEC_THEN `(1 >< 0) a` STRIP_ASSUME_TAC word2_cases 1754 \\ ASM_SIMP_TAC (srw_ss()) []); 1755 1756val aligned_neg_pc = Q.store_thm("aligned_neg_pc", 1757 `!a:word32. aligned(-(align(a,4) + 8w),4)`, 1758 SRW_TAC [] [aligned_sum, aligned_neg] \\ EVAL_TAC); 1759 1760val aligned_neg_pc = 1761 CONJ (SIMP_RULE (srw_ss()) [] aligned_neg_pc) 1762 (SIMP_RULE (srw_ss()) [WORD_LEFT_ADD_DISTRIB] aligned_neg_pc); 1763 1764val lem = Q.prove( 1765 `(!x:word32. n2w (w2n x + 1) = x + 1w)`, SRW_TAC [] [word_add_def]); 1766 1767val aligned_aligned_add_with_carry = Q.store_thm( 1768 "aligned_aligned_add_with_carry", 1769 `(!a:word32 b c. 1770 aligned (FST (add_with_carry 1771 (align(a,4) + 8w, 1772 if aligned (FST (add_with_carry (align(a,4) + 8w,b,c)),4) then b else 1773 if c then 0xFFFFFFFFw else 0w,c)),4)) /\ 1774 (!a:word32 b c. 1775 aligned (FST (add_with_carry 1776 (align(a,4) + 8w, 1777 ~(if aligned (FST (add_with_carry (align(a,4) + 8w,~b,c)),4) then b 1778 else if c then 0w else 0xFFFFFFFFw),c)),4)) /\ 1779 (!a:word32 b c. 1780 aligned (FST (add_with_carry 1781 (~(align(a,4) + 8w), 1782 if aligned (FST (add_with_carry (~(align(a,4) + 8w),b,c)),4) then b 1783 else if c then 0w else 1w,c)),4))`, 1784 REPEAT STRIP_TAC \\ Cases_on `c` 1785 \\ SIMP_TAC (std_ss++boolSimps.LET_ss) 1786 [add_with_carry_def, GSYM word_add_def, word_add_plus1, lem] 1787 \\ SRW_TAC [] [aligned_sum] 1788 \\ FULL_SIMP_TAC (srw_ss()) [WORD_NOT, aligned_neg_pc] 1789 \\ EVAL_TAC); 1790 1791val aligned_aligned_shift = Q.prove( 1792 `(!f:bool[32] # num -> bool[32] # bool x a:word32 b. 1793 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1794 aligned (FST (f (if aligned (a,4) /\ aligned (FST (f (b,x)), 4) 1795 then b else 0w,x)),4)) /\ 1796 (!f:bool[32] # num -> bool[32] # bool x a:word32 b. 1797 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1798 aligned (FST (f ((if aligned (a,4) /\ aligned (FST (f (b + 8w,x)), 4) 1799 then b else 0xFFFFFFF8w) + 8w,x)),4)) /\ 1800 (!f:bool[32] # num -> bool[32] # bool x a b. 1801 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1802 aligned ((if aligned (a && FST (f (b,x)), 4) then a else 0w) && 1803 FST (f (if aligned (a && FST (f (b,x)), 4) then b else 0w,x)), 4)) /\ 1804 (!f:bool[32] # num -> bool[32] # bool x a b. 1805 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1806 aligned ((if aligned (a && ~FST (f (b,x)), 4) then a else 0w) && 1807 ~FST (f (if aligned (a && ~FST (f (b,x)), 4) then b else 0w,x)), 4)) /\ 1808 (!f:bool[32] # num -> bool[32] # bool x a b. 1809 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1810 aligned ((if aligned (a ?? FST (f (b,x)), 4) then a else 0w) ?? 1811 FST (f (if aligned (a ?? FST (f (b,x)), 4) then b else 0w,x)), 4)) /\ 1812 (!f:bool[32] # num -> bool[32] # bool x a b. 1813 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1814 aligned ((if aligned (a || FST (f (b,x)), 4) then a else 0w) || 1815 FST (f (if aligned (a || FST (f (b,x)), 4) then b else 0w,x)), 4)) /\ 1816 (!f:bool[32] # num -> bool[32] # bool x a. 1817 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1818 aligned (FST (f (if aligned (FST (f (a,x)) + -a,4) then a else 0w, x)) + 1819 -if aligned (FST (f (a,x)) + -a,4) then a else 0w,4)) /\ 1820 (!f:bool[32] # num -> bool[32] # bool x a b. 1821 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1822 aligned (align(a,4) + 8w + 1823 FST (f (if aligned (align(a,4) + 8w + FST (f (b,x)),4) 1824 then b else 0w, x)),4)) /\ 1825 (!f:bool[32] # num -> bool[32] # bool x a b. 1826 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1827 aligned (FST (f (if aligned (FST (f (b,x)) + -(align(a,4) + 8w),4) 1828 then b else 0w, x)) + -(align(a,4) + 8w),4)) /\ 1829 (!f:bool[32] # num -> bool[32] # bool x a b. 1830 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1831 aligned (align(a,4) + 8w + 1832 -FST (f (if aligned (align(a,4) + 8w + -FST (f (b,x)),4) 1833 then b else 0w, x)),4))`, 1834 SRW_TAC [] [aligned_sum, aligned_neg_pc] \\ EVAL_TAC); 1835 1836val aligned_aligned_shift = 1837 CONJ 1838 (aligned_aligned_shift 1839 |> Thm.CONJUNCT1 1840 |> Drule.SPEC_ALL 1841 |> Q.INST [`a` |-> `0w`] 1842 |> REWRITE_RULE [EVAL ``aligned (0w:word32,4)``] 1843 |> Q.GEN `b` |> Q.GEN `x` |> Q.GEN `f`) 1844 aligned_aligned_shift; 1845 1846val aligned_aligned_shift_thms = save_thm("aligned_aligned_shift_thms", 1847 Drule.LIST_CONJ (List.concat 1848 (List.map (fn thm => 1849 List.map (fn t => (CONJ (thm |> Q.SPECL [t,`NUMERAL (BIT1 n)`,`a`]) 1850 (thm |> Q.SPECL [t,`NUMERAL (BIT2 n)`,`a`])) 1851 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,NUMERAL_FST_SHIFT_C]) 1852 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 1853 (Drule.CONJUNCTS aligned_aligned_shift)))); 1854 1855val aligned_aligned_shift_pc = Q.prove( 1856 `(!f:bool[32] # num -> bool[32] # bool x a:word32 b c. 1857 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1858 aligned 1859 (FST (f ((if b /\ c /\ aligned (FST (f (a + 8w,x)),4) 1860 then a else 0xFFFFFFF8w) + 8w,x)), 4)) /\ 1861 (!f:bool[32] # num -> bool[32] # bool x a b. 1862 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1863 aligned 1864 ((if b /\ aligned (a + 8w ?? FST (f (a + 8w,x)), 4) 1865 then a else 0xFFFFFFF8w) + 8w ?? 1866 FST (f ((if b /\ aligned (a + 8w ?? FST (f (a + 8w,x)), 4) 1867 then a else 0xFFFFFFF8w) + 8w,x)), 4)) /\ 1868 (!f:bool[32] # num -> bool[32] # bool x a b. 1869 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1870 aligned 1871 ((if b /\ aligned (a + 8w + FST (f (a + 8w,x)), 4) 1872 then a else 0xFFFFFFF8w) + 8w + 1873 FST (f ((if b /\ aligned (a + 8w + FST (f (a + 8w,x)), 4) 1874 then a else 0xFFFFFFF8w) + 8w,x)), 4)) /\ 1875 (!f:bool[32] # num -> bool[32] # bool x a b. 1876 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1877 aligned 1878 ((if b /\ aligned (a + 8w + -FST (f (a + 8w,x)), 4) 1879 then a else 0xFFFFFFF8w) + 8w + 1880 -FST (f ((if b /\ aligned (a + 8w + -FST (f (a + 8w,x)), 4) 1881 then a else 0xFFFFFFF8w) + 8w,x)), 4)) /\ 1882 (!f:bool[32] # num -> bool[32] # bool x a b. 1883 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 1884 aligned 1885 (FST (f ((if b /\ aligned (FST (f (a + 8w,x)) + -(a + 8w), 4) 1886 then a else 0xFFFFFFF8w) + 8w,x)) + 1887 -((if b /\ aligned (FST (f (a + 8w,x)) + -(a + 8w), 4) 1888 then a else 0xFFFFFFF8w) + 8w), 4))`, 1889 SRW_TAC [] [aligned_sum, aligned_neg_pc] \\ EVAL_TAC); 1890 1891val aligned_aligned_shift_pc_thms = save_thm("aligned_aligned_shift_pc_thms", 1892 Drule.LIST_CONJ (List.concat 1893 (List.map (fn thm => 1894 List.map (fn t => (CONJ (thm |> Q.SPECL [t,`NUMERAL (BIT1 n)`,`a`]) 1895 (thm |> Q.SPECL [t,`NUMERAL (BIT2 n)`,`a`])) 1896 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,NUMERAL_FST_SHIFT_C]) 1897 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 1898 (Drule.CONJUNCTS aligned_aligned_shift_pc)))); 1899 1900val aligned_neg_pc2 = Q.prove( 1901 `!a:word32. aligned(-(align(a,4) + 0x80000008w),4)`, 1902 SRW_TAC [] [aligned_sum, aligned_neg] \\ EVAL_TAC); 1903 1904val aligned_neg_pc2 = 1905 SIMP_RULE (srw_ss()) [EVAL ``-1w:word32``, WORD_LEFT_ADD_DISTRIB] 1906 aligned_neg_pc2; 1907 1908val aligned_aligned_rrx = Q.prove( 1909 `(!x a:word32 b. 1910 aligned (SND (word_rrx (x, 1911 if b /\ aligned (SND (word_rrx (x,a)), 4) then a else 0w)),4)) /\ 1912 (!x a:word32 b. 1913 aligned (SND (word_rrx (x, 1914 (if b /\ aligned (SND (word_rrx (x,a + 8w)), 4) 1915 then a else 0xFFFFFFF8w) + 8w)),4)) /\ 1916 (!x a:word32 b. 1917 aligned ((if aligned (a && SND (word_rrx (x,b)), 4) then a else 0w) && 1918 SND (word_rrx (x, 1919 if aligned (a && SND (word_rrx (x,b)), 4) then b else 0w)), 4)) /\ 1920 (!x a:word32 b. 1921 aligned ((if aligned (a && ~SND (word_rrx (x,b)), 4) then a else 0w) && 1922 ~SND (word_rrx (x, 1923 if aligned (a && ~SND (word_rrx (x,b)), 4) then b else 0w)), 4)) /\ 1924 (!x a:word32 b. 1925 aligned ((if aligned (a ?? SND (word_rrx (x,b)), 4) then a else 0w) ?? 1926 SND (word_rrx (x, 1927 if aligned (a ?? SND (word_rrx (x,b)), 4) then b else 0w)), 4)) /\ 1928 (!x a:word32 b. 1929 aligned ((if aligned (a || SND (word_rrx (x,b)), 4) then a else 0w) || 1930 SND (word_rrx (x, 1931 if aligned (a || SND (word_rrx (x,b)), 4) then b else 0w)), 4)) /\ 1932 (!x a:word32. 1933 aligned (SND (word_rrx (x, 1934 if aligned (SND (word_rrx (x,a)) + -a,4) then a else 0w)) + 1935 -if aligned (SND (word_rrx (x,a)) + -a,4) then a else 0w,4)) /\ 1936 (!x a:word32 b. 1937 aligned (align(a,4) + 8w + 1938 SND (word_rrx (x, 1939 if aligned (align(a,4) + 8w + SND (word_rrx (x,b)),4) 1940 then b else 0w)),4)) /\ 1941 (!x a:word32 b. 1942 aligned (SND (word_rrx (x, 1943 if aligned (SND (word_rrx (x,b)) + -(align(a,4) + 8w),4) 1944 then b else 0w)) + -(align(a,4) + 8w),4)) /\ 1945 (!x a:word32 b. 1946 aligned (align(a,4) + 8w + 1947 -SND (word_rrx (x, 1948 if aligned (align(a,4) + 8w + -SND (word_rrx (x,b)),4) 1949 then b else 0w)),4))`, 1950 REPEAT STRIP_TAC \\ Cases_on `x` 1951 \\ SRW_TAC [] 1952 [WORD_LEFT_ADD_DISTRIB, aligned_sum, aligned_neg_pc, word_rrx_0] 1953 \\ EVAL_TAC \\ REWRITE_TAC [aligned_neg_pc2]); 1954 1955val aligned_aligned_rrx = save_thm("aligned_aligned_rrx", 1956 CONJ 1957 (aligned_aligned_rrx 1958 |> Thm.CONJUNCT1 1959 |> Drule.SPEC_ALL 1960 |> Q.INST [`b` |-> `T`] 1961 |> REWRITE_RULE [] 1962 |> GEN_ALL) 1963 aligned_aligned_rrx); 1964 1965val aligned_aligned_rrx_pc = Q.store_thm("aligned_aligned_rrx_pc", 1966 `(!x a:word32 b c. 1967 aligned 1968 (SND (word_rrx (x,(if b /\ c /\ aligned (SND (word_rrx (x,a + 8w)),4) 1969 then a else 0xFFFFFFF8w) + 8w)), 4)) /\ 1970 (!x a:word32 b. 1971 aligned 1972 ((if b /\ aligned (a + 8w ?? SND (word_rrx (x,a + 8w)), 4) 1973 then a else 0xFFFFFFF8w) + 8w ?? 1974 SND (word_rrx (x, 1975 (if b /\ aligned (a + 8w ?? SND (word_rrx (x,a + 8w)), 4) 1976 then a else 0xFFFFFFF8w) + 8w)), 4)) /\ 1977 (!x a:word32 b. 1978 aligned 1979 ((if b /\ aligned (a + 8w + SND (word_rrx (x,a + 8w)), 4) 1980 then a else 0xFFFFFFF8w) + 8w + 1981 SND (word_rrx (x, 1982 (if b /\ aligned (a + 8w + SND (word_rrx (x,a + 8w)), 4) 1983 then a else 0xFFFFFFF8w) + 8w)), 4)) /\ 1984 (!x a:word32 b. 1985 aligned 1986 ((if b /\ aligned (a + 8w + -SND (word_rrx (x,a + 8w)), 4) 1987 then a else 0xFFFFFFF8w) + 8w + 1988 -SND (word_rrx (x, 1989 (if b /\ aligned (a + 8w + -SND (word_rrx (x,a + 8w)), 4) 1990 then a else 0xFFFFFFF8w) + 8w)), 4)) /\ 1991 (!x a:word32 b. 1992 aligned 1993 (SND (word_rrx (x, 1994 (if b /\ aligned (SND (word_rrx (x,a + 8w)) + -(a + 8w), 4) 1995 then a else 0xFFFFFFF8w) + 8w)) + 1996 -((if b /\ aligned (SND (word_rrx (x,a + 8w)) + -(a + 8w), 4) 1997 then a else 0xFFFFFFF8w) + 8w), 4))`, 1998 REPEAT STRIP_TAC \\ Cases_on `x` 1999 \\ SRW_TAC [] [aligned_sum, aligned_neg_pc, word_rrx_0] 2000 \\ EVAL_TAC); 2001 2002val aligned_pc_pc = Q.store_thm("aligned_pc_pc", 2003 `!a:word32. aligned(align(a,4) + 8w + (align(a,4) + 8w),4)`, 2004 SIMP_TAC std_ss [aligned_sum, 2005 wordsLib.WORD_DECIDE ``a + b + (a + b) = a + (a + (b + b)) : 'a word``] 2006 \\ EVAL_TAC); 2007 2008val aligned_aligned_rsb = Q.store_thm("aligned_aligned_rsb", 2009 `(!a:word32 b. 2010 aligned((if aligned(b + -(align(a,4) + 8w),4) then b else 0w) + 2011 -(align(a,4) + 8w),4))`, 2012 SRW_TAC [] [aligned_neg_pc]); 2013 2014val add_with_carry = Q.store_thm("add_with_carry", 2015 `(!a:word32 b c d. 2016 FST (add_with_carry (a + d + -(if c then 1w else 0w),b,c)) = 2017 a + (d + b)) /\ 2018 (!a:word32 b c d. 2019 FST (add_with_carry (a + d + (if c then 0w else 1w),b,c)) = 2020 a + (d + b + 1w)) /\ 2021 (!a:word32 b c d. 2022 FST (add_with_carry (~(d + (if c then 0w else 0xFFFFFFFFw) + a),b,c)) = 2023 -a + (b - d))`, 2024 SRW_TAC [boolSimps.LET_ss] 2025 [WORD_NOT, WORD_LEFT_ADD_DISTRIB, GSYM word_add_def, 2026 add_with_carry_def, word_add_plus1]); 2027 2028val add_with_carry0 = save_thm("add_with_carry0", 2029 Drule.LIST_CONJ 2030 [add_with_carry 2031 |> Thm.CONJUNCT1 2032 |> Q.SPECL [`a`,`0w`,`c`,`0w`] 2033 |> REWRITE_RULE [WORD_ADD_0] 2034 |> GEN_ALL, 2035 add_with_carry 2036 |> Thm.CONJUNCT2 |> Thm.CONJUNCT1 2037 |> Q.SPECL [`a`,`0xFFFFFFFFw`,`c`,`0x0w`] 2038 |> REWRITE_RULE [WORD_ADD_0, EVAL ``0xFFFFFFFFw + 1w : word32``] 2039 |> GEN_ALL, 2040 add_with_carry 2041 |> Thm.CONJUNCT2 |> Thm.CONJUNCT2 2042 |> Q.SPECL [`a`,`0w`,`c`,`0x0w`] 2043 |> REWRITE_RULE [WORD_ADD_0, WORD_SUB_RZERO] 2044 |> GEN_ALL]); 2045 2046val aligned_pc_thm = Q.store_thm("aligned_pc_thm", 2047 `!a:word32. aligned (a,4) ==> aligned (a + 8w, 4)`, 2048 METIS_TAC [aligned_thm, aligned_def, EVAL ``aligned (8w:word32,4)``]); 2049 2050val aligned_bitwise_thm = Q.store_thm("aligned_bitwise_thm", 2051 `(!a:word32 b. 2052 aligned (a,4) /\ aligned (b,4) ==> (align (a || b, 4) = a || b)) /\ 2053 (!a:word32 b. 2054 aligned (a,4) /\ aligned (b,4) ==> (align (a ?? b, 4) = a ?? b)) /\ 2055 (!a:word32 b. aligned (a,4) ==> (align (a && b,4) = a && b))`, 2056 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [aligned_248, align_248]); 2057 2058(* ------------------------------------------------------------------------- *) 2059 2060val align4 = EVAL ``align (4w:word32,4)``; 2061val align8 = EVAL ``align (8w:word32,4)``; 2062val align4m = EVAL ``align (0xFFFFFFFCw:word32,4)``; 2063 2064val align_plus4 = Q.prove( 2065 `!a:word32. align (a + 4w, 4) = align (a,4) + 4w`, 2066 SUBST1_TAC (SYM align4) 2067 \\ SRW_TAC [] [ONCE_REWRITE_RULE [WORD_ADD_COMM] align_aligned, align4]); 2068 2069val align_plus_extra = Q.prove( 2070 `(!a:word32. align (a + 8w, 4) = align (a,4) + 8w) /\ 2071 (!a:word32. align (a + 0xFFFFFFFCw, 4) = align (a,4) + 0xFFFFFFFCw)`, 2072 SUBST1_TAC (SYM align8) 2073 \\ SUBST1_TAC (SYM align4m) 2074 \\ SRW_TAC [] [ONCE_REWRITE_RULE [WORD_ADD_COMM] align_aligned, 2075 align8,align4m]); 2076 2077val aligned_mul4 = Q.prove( 2078 `!a:word32. aligned (4w * a, 4)`, 2079 SRW_TAC [wordsLib.WORD_MUL_LSL_ss,wordsLib.WORD_EXTRACT_ss] [aligned_248]); 2080 2081val align_mul4 = aligned_mul4 |> REWRITE_RULE [aligned_def] |> GSYM; 2082 2083val neq_align_plus4 = Q.prove( 2084 `!a:word32. align (a + 4w, 4) <> align (a, 4)`, 2085 SRW_TAC [wordsLib.WORD_ARITH_EQ_ss] [align_plus4]); 2086 2087val BIT_ALIGN4 = Q.prove( 2088 `(!n. NUMERAL (BIT2 (BIT1 n)) = 4 * (n + 1)) /\ 2089 (!n. NUMERAL (BIT1 (BIT2 n)) = 4 * (n + 1) + 1) /\ 2090 (!n. NUMERAL (BIT2 (BIT2 n)) = 4 * (n + 1) + 2) /\ 2091 (!n. NUMERAL (BIT1 (BIT1 (BIT1 n))) = 4 * (2 * n + 1) + 3) /\ 2092 (!n. NUMERAL (BIT1 (BIT1 (BIT2 n))) = 4 * (2 * n + 2) + 3)`, 2093 REPEAT STRIP_TAC 2094 \\ CONV_TAC (LHS_CONV (REWRITE_CONV [NUMERAL_DEF, BIT2, BIT1])) 2095 \\ DECIDE_TAC); 2096 2097val aligned_numeric = Q.prove( 2098 `aligned (0w:word32,4) /\ 2099 !n. aligned (n2w (NUMERAL (BIT2 (BIT1 n))) : word32, 4)`, 2100 REPEAT STRIP_TAC >> EVAL_TAC 2101 \\ Q.SPEC_THEN `n` SUBST1_TAC (Thm.CONJUNCT1 BIT_ALIGN4) 2102 \\ REWRITE_TAC [GSYM word_mul_n2w, aligned_mul4]); 2103 2104val align_sum_numeric = Q.prove( 2105 `(!n. n2w (NUMERAL (BIT2 (BIT1 n))) = 2106 align (n2w (NUMERAL (BIT2 (BIT1 n))),4) :word32) /\ 2107 (!n. n2w (NUMERAL (BIT1 (BIT2 n))) = 2108 align (n2w (NUMERAL (BIT2 (BIT1 n))),4) + 1w :word32) /\ 2109 (!n. n2w (NUMERAL (BIT2 (BIT2 n))) = 2110 align (n2w (NUMERAL (BIT2 (BIT1 n))),4) + 2w :word32) /\ 2111 (!n. n2w (NUMERAL (BIT1 (BIT1 (BIT1 n)))) = 2112 align (4w * (2w * n2w n + 1w),4) + 3w :word32) /\ 2113 (!n. n2w (NUMERAL (BIT1 (BIT1 (BIT2 n)))) = 2114 align (4w * (2w * n2w n + 2w),4) + 3w :word32)`, 2115 REWRITE_TAC [align_mul4] 2116 \\ ONCE_REWRITE_TAC [BIT_ALIGN4] 2117 \\ SRW_TAC [] [WORD_LEFT_ADD_DISTRIB, GSYM word_mul_n2w, GSYM word_add_n2w, 2118 align_plus4, align_mul4, 2119 METIS_PROVE [ALT_ZERO, ADD_CLAUSES] 2120 ``(ZERO + 1 = 1) /\ (n2w ZERO = 0w)``]); 2121 2122val align_neq2 = Q.store_thm("align_neq2", 2123 `!a:word32 b n. 2124 aligned (a, 4) ==> 2125 align (b, 4) <> a + 1w /\ 2126 align (b, 4) <> a + 2w /\ 2127 align (b, 4) <> a + 3w /\ 2128 align (b, 4) <> a + n2w (NUMERAL (BIT1 (BIT2 n))) /\ (* 1 *) 2129 align (b, 4) <> a + n2w (NUMERAL (BIT2 (BIT2 n))) /\ (* 2 *) 2130 align (b, 4) <> a + n2w (NUMERAL (BIT1 (BIT1 (BIT1 n)))) /\ (* 3 *) 2131 align (b, 4) <> a + n2w (NUMERAL (BIT1 (BIT1 (BIT2 n)))) /\ (* 3 *) 2132 align (b, 4) + 1w <> a /\ 2133 align (b, 4) + 1w <> a + 2w /\ 2134 align (b, 4) + 1w <> a + 3w /\ 2135 align (b, 4) + 1w <> a + n2w (NUMERAL (BIT2 (BIT1 n))) /\ (* 0 *) 2136 align (b, 4) + 1w <> a + n2w (NUMERAL (BIT2 (BIT2 n))) /\ (* 2 *) 2137 align (b, 4) + 1w <> a + n2w (NUMERAL (BIT1 (BIT1 (BIT1 n)))) /\ (* 3 *) 2138 align (b, 4) + 1w <> a + n2w (NUMERAL (BIT1 (BIT1 (BIT2 n)))) /\ (* 3 *) 2139 align (b, 4) + 2w <> a /\ 2140 align (b, 4) + 2w <> a + 1w /\ 2141 align (b, 4) + 2w <> a + 3w /\ 2142 align (b, 4) + 2w <> a + n2w (NUMERAL (BIT2 (BIT1 n))) /\ (* 0 *) 2143 align (b, 4) + 2w <> a + n2w (NUMERAL (BIT1 (BIT2 n))) /\ (* 1 *) 2144 align (b, 4) + 2w <> a + n2w (NUMERAL (BIT1 (BIT1 (BIT1 n)))) /\ (* 3 *) 2145 align (b, 4) + 2w <> a + n2w (NUMERAL (BIT1 (BIT1 (BIT2 n)))) /\ (* 3 *) 2146 align (b, 4) + 3w <> a /\ 2147 align (b, 4) + 3w <> a + 1w /\ 2148 align (b, 4) + 3w <> a + 2w /\ 2149 align (b, 4) + 3w <> a + n2w (NUMERAL (BIT2 (BIT1 n))) /\ (* 0 *) 2150 align (b, 4) + 3w <> a + n2w (NUMERAL (BIT1 (BIT2 n))) /\ (* 1 *) 2151 align (b, 4) + 3w <> a + n2w (NUMERAL (BIT2 (BIT2 n)))`, (* 2 *) 2152 NTAC 4 STRIP_TAC 2153 \\ POP_ASSUM (fn th => 2154 REPEAT CONJ_TAC \\ 2155 ONCE_REWRITE_TAC [th |> REWRITE_RULE [aligned_def]]) 2156 \\ REWRITE_TAC [align_neq] 2157 \\ ONCE_REWRITE_TAC [align_sum_numeric] 2158 \\ REWRITE_TAC [align_neq, GSYM align_aligned, WORD_ADD_ASSOC]); 2159 2160val align2 = EVAL ``align (2w:word32,2)``; 2161 2162val align_plus2 = Q.prove( 2163 `!a:word32. align (a + 2w, 2) = align (a,2) + 2w`, 2164 SUBST1_TAC (SYM align2) 2165 \\ SRW_TAC [] [ONCE_REWRITE_RULE [WORD_ADD_COMM] align_aligned, align2]); 2166 2167val aligned_mul2 = Q.prove( 2168 `!a:word32. aligned (2w * a, 2)`, 2169 SRW_TAC [wordsLib.WORD_MUL_LSL_ss,wordsLib.WORD_EXTRACT_ss] [aligned_248]); 2170 2171val align_mul2 = aligned_mul2 |> REWRITE_RULE [aligned_def] |> GSYM; 2172 2173val BIT_ALIGN2 = Q.prove( 2174 `(!n. NUMERAL (BIT1 n) = 2 * n + 1) /\ 2175 (!n. NUMERAL (BIT2 n) = 2 * (n + 1))`, 2176 REPEAT STRIP_TAC 2177 \\ CONV_TAC (LHS_CONV (REWRITE_CONV [NUMERAL_DEF, BIT2, BIT1])) 2178 \\ DECIDE_TAC); 2179 2180val align_sum_numeric2 = Q.prove( 2181 `(!n. n2w (NUMERAL (BIT2 n)) = 2182 align (n2w (NUMERAL (BIT2 n)),2) :word32) /\ 2183 (!n. n2w (NUMERAL (BIT1 n)) = 2184 align (2w * n2w n,2) + 1w :word32)`, 2185 REWRITE_TAC [align_mul2] 2186 \\ ONCE_REWRITE_TAC [BIT_ALIGN2] 2187 \\ SRW_TAC [] [WORD_LEFT_ADD_DISTRIB, GSYM word_mul_n2w, GSYM word_add_n2w, 2188 align_mul2, align_plus2, 2189 METIS_PROVE [ALT_ZERO, ADD_CLAUSES] 2190 ``(ZERO + 1 = 1) /\ (n2w ZERO = 0w)``]); 2191 2192val align_neq3 = Q.store_thm("align_neq3", 2193 `!a:word32 b m n. 2194 aligned (a, 2) ==> 2195 align (b, 2) <> a + n2w (NUMERAL (BIT1 n)) /\ (* 0,1 *) 2196 align (b, 2) + n2w (NUMERAL (BIT2 m)) <> 2197 a + n2w (NUMERAL (BIT1 n)) /\ (* 0,1 *) 2198 align (b, 2) + n2w (NUMERAL (BIT1 n)) <> a /\ (* 1,0 *) 2199 align (b, 2) + n2w (NUMERAL (BIT1 m)) <> 2200 a + n2w (NUMERAL (BIT2 n))`, (* 1,0 *) 2201 NTAC 5 STRIP_TAC 2202 \\ POP_ASSUM (fn th => 2203 REPEAT CONJ_TAC \\ 2204 ONCE_REWRITE_TAC [th |> REWRITE_RULE [aligned_def]]) 2205 \\ REWRITE_TAC [align_neq] 2206 \\ ONCE_REWRITE_TAC [align_sum_numeric2] 2207 \\ REWRITE_TAC [align_neq, GSYM align_aligned, WORD_ADD_ASSOC]); 2208 2209val neq_pc_plus4a = Q.prove( 2210 `(!b:word32 pc a. 2211 pc <> align ((if pc <> align (a + b,4) then a else a + 4w) + b,4)) /\ 2212 (!pc:word32 a. 2213 pc + 1w <> 2214 align ((if pc <> align (a + 4w,4) then a else a + 4w),4) + 5w) /\ 2215 (!pc:word32 a. 2216 pc + 2w <> 2217 align ((if pc <> align (a + 4w,4) then a else a + 4w),4) + 6w) /\ 2218 (!pc:word32 a. 2219 pc + 3w <> 2220 align ((if pc <> align (a + 4w,4) then a else a + 4w),4) + 7w) /\ 2221 (!pc:word32 a. 2222 pc + 1w <> 2223 align ((if pc <> align (a + 8w,4) then a else a + 4w),4) + 9w) /\ 2224 (!pc:word32 a. 2225 pc + 2w <> 2226 align ((if pc <> align (a + 8w,4) then a else a + 4w),4) + 10w) /\ 2227 (!pc:word32 a. 2228 pc + 3w <> 2229 align ((if pc <> align (a + 8w,4) then a else a + 4w),4) + 11w) /\ 2230 (!pc:word32 a. 2231 pc + 1w <> 2232 align ((if pc <> align (a + 0xFFFFFFFCw,4) then a else a + 4w),4) + 2233 0xFFFFFFFDw) /\ 2234 (!pc:word32 a. 2235 pc + 2w <> 2236 align ((if pc <> align (a + 0xFFFFFFFCw,4) then a else a + 4w),4) + 2237 0xFFFFFFFEw) /\ 2238 (!pc:word32 a. 2239 pc + 3w <> 2240 align ((if pc <> align (a + 0xFFFFFFFCw,4) then a else a + 4w),4) + 2241 0xFFFFFFFFw)`, 2242 SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) [align_plus4, align_plus_extra] 2243 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) 2244 [align_aligned |> ONCE_REWRITE_RULE [WORD_ADD_COMM]] 2245); 2246 2247val neq_pc_plus4 = Q.prove( 2248 `!b:word32 pc a. 2249 aligned (b,4) ==> 2250 pc <> align ((if pc <> align (a + b,4) 2251 then a else a + 4w),4) + b`, 2252 SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) [aligned_def, align_plus4] 2253 \\ Q.PAT_ASSUM `c = align (c,4)` SUBST_ALL_TAC 2254 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) 2255 [align_aligned |> ONCE_REWRITE_RULE [WORD_ADD_COMM]]); 2256 2257val neq_pc_plus4_plus = Q.prove( 2258 `(!a:word32 c d. 2259 aligned (c,4) ==> 2260 (align ((if pc <> align(x,4) then a else a + 4w) + c,4) = 2261 align (if pc <> align(x,4) then a else a + 4w,4) + c)) /\ 2262 (!a:word32 c d. 2263 aligned (c,4) ==> 2264 (align ((if pc <> align(x,4) /\ y then a else a + 4w) + c,4) = 2265 align (if pc <> align(x,4) /\ y then a else a + 4w,4) + c))`, 2266 SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) [aligned_def, align_plus4] 2267 \\ Q.PAT_ASSUM `c = align (c,4)` SUBST_ALL_TAC 2268 \\ FULL_SIMP_TAC (srw_ss()) 2269 [align_aligned |> ONCE_REWRITE_RULE [WORD_ADD_COMM]]); 2270 2271val neq_pc_plus4_plus = save_thm("neq_pc_plus4_plus", 2272 Drule.LIST_CONJ 2273 (List.map (fn thm => GEN_ALL (MATCH_MP (Drule.SPEC_ALL thm) 2274 (aligned_numeric |> Thm.CONJUNCT2 |> Drule.SPEC_ALL))) 2275 (Drule.CONJUNCTS neq_pc_plus4_plus))); 2276 2277val neq_pc_plus4 = save_thm("neq_pc_plus4", 2278 Drule.LIST_CONJ 2279 [neq_pc_plus4a, 2280 MATCH_MP (Drule.SPEC_ALL neq_pc_plus4) 2281 (aligned_numeric |> Thm.CONJUNCT2 |> Drule.SPEC_ALL), 2282 neq_pc_plus4 |> Q.SPEC `0w` 2283 |> REWRITE_RULE [Thm.CONJUNCT1 aligned_numeric, WORD_ADD_0]]); 2284 2285val neq_pc_plus4_t2 = Q.prove( 2286 `(!b:word32 pc a. 2287 aligned (b,4) ==> 2288 pc <> align ((if pc <> align (a + b,4) /\ pc + 2w <> align (a + b,4) 2289 then a else a + 4w),4) + b) /\ 2290 (!b:word32 pc a. 2291 aligned (b,4) ==> 2292 pc + 2w <> align ((if pc <> align (a + b,4) /\ pc + 2w <> align (a + b,4) 2293 then a else a + 4w),4) + b)`, 2294 SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) [aligned_def, align_plus4] 2295 \\ Q.PAT_ASSUM `c = align (c,4)` SUBST_ALL_TAC 2296 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) 2297 [align_aligned |> ONCE_REWRITE_RULE [WORD_ADD_COMM]] 2298 \\ ASM_REWRITE_TAC [wordsLib.WORD_DECIDE 2299 ``a + 0xFFFFFFFCw = a + 2w + 0xFFFFFFFAw:word32``] 2300 \\ EVAL_TAC); 2301 2302val neq_pc_plus4_t2 = save_thm("neq_pc_plus4_t2", 2303 Drule.LIST_CONJ 2304 (List.map (fn thm => MATCH_MP (Drule.SPEC_ALL thm) 2305 (aligned_numeric |> Thm.CONJUNCT2 |> Drule.SPEC_ALL)) 2306 (Drule.CONJUNCTS neq_pc_plus4_t2))); 2307 2308val aligned_over_memread = Q.store_thm("aligned_over_memread", 2309 `(!b x:word8 y. 2310 aligned (if b then x else y,4) = 2311 if b then aligned (x,4) else aligned (y,4)) /\ 2312 (!b x:word8 y. 2313 aligned_bx (if b then x else y) = 2314 if b then aligned_bx x else aligned_bx y) /\ 2315 (!b c x:word8 y z. 2316 aligned_bx (if b then x else if c then y else z) = 2317 if b then aligned_bx x else if c then aligned_bx y else aligned_bx z)`, 2318 SRW_TAC [] []); 2319 2320val aligned_concat = with_flag (wordsLib.guessing_word_lengths,true) 2321 Q.store_thm("aligned_concat", 2322 `!a:word8 b:word8 c:word8 d:word8. 2323 aligned ((a @@ b @@ c @@ d) : word32, 4) = aligned (d,4)`, 2324 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [aligned_248, aligned_def, align_248]); 2325 2326val aligned_bx_concat = with_flag (wordsLib.guessing_word_lengths,true) 2327 Q.store_thm("aligned_bx_concat", 2328 `!a:word8 b:word8 c:word8 d:word8. 2329 aligned_bx ((a @@ b @@ c @@ d) : word32) = aligned_bx d`, 2330 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [aligned_bx_def]); 2331 2332val aligned_bx_aligned_bx = Q.store_thm("aligned_bx_aligned_bx", 2333 `!a:word8. aligned_bx (if aligned_bx a then a else 0w)`, 2334 SRW_TAC [] [] \\ EVAL_TAC); 2335 2336val it_mode_concat = with_flag (wordsLib.guessing_word_lengths,true) 2337 Q.store_thm("it_mode_concat", 2338 `!a:word8 b:word8 c:word8 d:word8. 2339 ((4 >< 0) ((a @@ b @@ c @@ d) : word32) = (4 >< 0) d) /\ 2340 ((15 >< 10) ((a @@ b @@ c @@ d) : word32) = (7 >< 2) c) /\ 2341 ((26 >< 25) ((a @@ b @@ c @@ d) : word32) = (2 >< 1) a)`, 2342 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []); 2343 2344(* ------------------------------------------------------------------------- *) 2345 2346val extract_of_double_word = with_flag (wordsLib.guessing_word_lengths,true) 2347 Q.store_thm("extract_of_double_word", 2348 `!a:word32 b:word32. 2349 ((63 >< 32) (a @@ b) = a) /\ ((31 >< 0 ) (a @@ b) = b)`, 2350 SRW_TAC [wordsLib.WORD_EXTRACT_ss] []); 2351 2352val aligned_pair = Q.prove( 2353 `!a:word32. 2354 aligned ((if aligned (a + a,4) then a else 0w) + 2355 (if aligned (a + a,4) then a else 0w), 4)`, 2356 SRW_TAC [] [] \\ EVAL_TAC); 2357 2358fun aligned_neq_thms thm = 2359 MATCH_MP (Drule.SPEC_ALL align_neq2) (Drule.SPEC_ALL thm); 2360 2361fun aligned_neq_thms2 thm = 2362 MATCH_MP (Drule.SPEC_ALL align_neq3) (Drule.SPEC_ALL thm); 2363 2364val aligned_pair_thms = save_thm("aligned_pair_thms", 2365 aligned_neq_thms aligned_pair); 2366 2367val aligned_shift_pair = Q.prove( 2368 `(!f:bool[32] # num -> bool[32] # bool x a:word32. 2369 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 2370 aligned ((if aligned (a + FST (f (a,x)),4) then a else 0w) + 2371 FST (f (if aligned (a + FST (f (a,x)),4) then a else 0w,x)), 4)) /\ 2372 (!f:bool[32] # num -> bool[32] # bool x a:word32. 2373 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 2374 aligned ((if aligned (a + -FST (f (a,x)),4) then a else 0w) + 2375 -FST (f (if aligned (a + -FST (f (a,x)),4) then a else 0w,x)), 4))`, 2376 SRW_TAC [] [] \\ EVAL_TAC); 2377 2378val aligned_rrx_pair = Q.prove( 2379 `(!x a:word32. 2380 aligned ((if aligned (a + SND (word_rrx (x,a)),4) then a else 0w) + 2381 SND (word_rrx (x, 2382 if aligned (a + SND (word_rrx (x,a)),4) then a else 0w)), 4)) /\ 2383 (!x a:word32. 2384 aligned ((if aligned (a + -SND (word_rrx (x,a)),4) then a else 0w) + 2385 -SND (word_rrx (x, 2386 if aligned (a + -SND (word_rrx (x,a)),4) then a else 0w)), 4))`, 2387 CONJ_TAC \\ Cases \\ SRW_TAC [] [] \\ EVAL_TAC); 2388 2389val aligned_shift_pair_thms = 2390 Drule.LIST_CONJ (List.concat 2391 (List.map (fn thm => 2392 List.map (fn t => (CONJ (thm |> Q.SPECL [t,`NUMERAL (BIT1 n)`,`a`]) 2393 (thm |> Q.SPECL [t,`NUMERAL (BIT2 n)`,`a`])) 2394 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,NUMERAL_FST_SHIFT_C]) 2395 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 2396 (Drule.CONJUNCTS aligned_shift_pair))); 2397 2398val aligned_rm_thms = Q.store_thm("aligned_rm_thms", 2399 `(!pc:word32 b. 2400 aligned (align (pc,4) + 8w + 2401 if aligned (align (pc,4) + 8w + b,4) then b else 0w,4)) /\ 2402 (!pc:word32 b. 2403 aligned (align (pc,4) + 8w + 2404 -(if aligned (align (pc,4) + 8w + -b,4) then b else 0w),4)) /\ 2405 (!pc:word32 b. 2406 aligned (align (pc,4) + 8w + 2407 (if aligned (align (pc,4) + 8w + b,4) then b else 0w) + 4w,4)) /\ 2408 (!pc:word32 b. 2409 aligned (align (pc,4) + 8w + 2410 -(if aligned (align (pc,4) + 8w + -b,4) then b else 0w) + 4w,4)) /\ 2411 (!pc:word32 b. 2412 aligned (align (pc,4) + 8w + 2413 if aligned (align (pc,4) + 8w + b,2) then b else 0w,2)) /\ 2414 (!pc:word32 b. 2415 aligned (align (pc,4) + 8w + 2416 -(if aligned (align (pc,4) + 8w + -b,2) then b else 0w),2))`, 2417 SRW_TAC [] [aligned_sum] \\ EVAL_TAC 2418 \\ FULL_SIMP_TAC std_ss [aligned_def, align_aligned, aligned_align, 2419 align_plus4, WORD_EQ_ADD_LCANCEL, EVAL ``-1w:word32``, 2420 wordsLib.WORD_DECIDE ``b + a + 8w = a + (b + 8w) : word32``, 2421 wordsLib.WORD_DECIDE ``b + a + 12w = a + (b + 8w + 4w) : word32``] 2422 \\ POP_ASSUM (SUBST1_TAC o SYM) \\ DECIDE_TAC); 2423 2424val aligned_shift_rm = Q.prove( 2425 `(!f:bool[32] # num -> bool[32] # bool x. 2426 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 2427 aligned (align (pc,4) + 8w + 2428 FST (f (if aligned (align (pc,4) + 8w + FST (f (b,x)),4) 2429 then b else 0w,x)),4)) /\ 2430 (!f:bool[32] # num -> bool[32] # bool x. 2431 x <> 0 /\ (FST (f (0w, x)) = 0w) ==> 2432 aligned (align (pc,4) + 8w + 2433 -FST (f (if aligned (align (pc,4) + 8w + -FST (f (b,x)),4) 2434 then b else 0w,x)),4))`, 2435 SRW_TAC [] [aligned_sum] \\ EVAL_TAC); 2436 2437val aligned_rrx_rm_thms = Q.store_thm("aligned_rrx_rm_thms", 2438 `(!pc:word32 b x. 2439 aligned 2440 (align (pc,4) + 8w + 2441 SND (word_rrx (x,if aligned (align (pc,4) + 8w + SND (word_rrx (x,b)),4) 2442 then b else 0w)),4)) /\ 2443 (!pc:word32 b x. 2444 aligned 2445 (align (pc,4) + 8w + 2446 -SND (word_rrx (x, 2447 if aligned (align (pc,4) + 8w + -SND (word_rrx (x,b)),4) 2448 then b else 0w)),4))`, 2449 REPEAT STRIP_TAC \\ Cases_on `x` 2450 \\ SRW_TAC [] [aligned_sum, word_rrx_0] \\ EVAL_TAC); 2451 2452val aligned_shift_rm_thms = save_thm("aligned_shift_rm_thms", 2453 Drule.LIST_CONJ (List.concat 2454 (List.map (fn thm => 2455 List.map (fn t => (CONJ (thm |> Q.SPECL [t,`NUMERAL (BIT1 n)`]) 2456 (thm |> Q.SPECL [t,`NUMERAL (BIT2 n)`])) 2457 |> SIMP_RULE std_ss [NUMERAL_NOT_ZERO,NUMERAL_FST_SHIFT_C]) 2458 [`LSL_C`,`LSR_C`,`ASR_C`,`ROR_C`]) 2459 (Drule.CONJUNCTS aligned_shift_rm)))); 2460 2461val aligned_rrx_pair_thms = save_thm("aligned_rrx_pair_thms", 2462 Drule.LIST_CONJ 2463 (List.map aligned_neq_thms (Drule.CONJUNCTS aligned_rrx_pair))); 2464 2465val aligned_shift_pair_thms = save_thm("aligned_shift_pair_thms", 2466 Drule.LIST_CONJ 2467 (List.map aligned_neq_thms (Drule.CONJUNCTS aligned_shift_pair_thms))); 2468 2469val aligned_align_shift_rm_thms = save_thm("aligned_align_shift_rm_thms", 2470 Drule.LIST_CONJ 2471 (List.map aligned_neq_thms (Drule.CONJUNCTS aligned_shift_rm_thms))); 2472 2473val aligned_align_rrx_rm_thms = save_thm("aligned_align_rrx_rm_thms", 2474 Drule.LIST_CONJ 2475 (List.map aligned_neq_thms (Drule.CONJUNCTS aligned_rrx_rm_thms))); 2476 2477val aligned_align_rm_thms = save_thm("aligned_align_rm_thms", 2478 Drule.LIST_CONJ 2479 ((List.map aligned_neq_thms 2480 (List.take(Drule.CONJUNCTS aligned_rm_thms,4))) @ 2481 (List.map aligned_neq_thms2 2482 (List.drop(Drule.CONJUNCTS aligned_rm_thms,4))))); 2483 2484val aligned_0_thms = save_thm("aligned_0_thms", 2485 aligned_neq_thms (``aligned (0w:word32, 4)`` |> EVAL |> EQT_ELIM) 2486 |> SIMP_RULE (srw_ss()) []); 2487 2488val aligned_align_thms = save_thm("aligned_align_thms", 2489 aligned_neq_thms (aligned_align |> Drule.CONJUNCTS |> el 4)); 2490 2491val aligned_align_thms2 = save_thm("aligned_align_thms2", 2492 aligned_neq_thms2 (aligned_align |> Drule.CONJUNCTS |> el 3)); 2493 2494(* ------------------------------------------------------------------------- *) 2495 2496val _ = Parse.overload_on 2497 ("GOOD_MODE", ``\m:word5. m IN {16w; 17w; 18w; 19w; 23w; 27w; 31w}``); 2498 2499val good_mode = Q.store_thm("good_mode", 2500 `(!n:word32. 2501 (4 >< 0) (if GOOD_MODE ((4 >< 0) n) then n else n || 31w) <> 22w:word5) /\ 2502 (!n:word32. 2503 GOOD_MODE ((4 >< 0) (if GOOD_MODE ((4 >< 0) n) then n else n || 31w))) /\ 2504 (!n:word8. 2505 (4 >< 0) (if GOOD_MODE ((4 >< 0) n) then n else n || 31w) <> 22w:word5) /\ 2506 (!n:word8. 2507 GOOD_MODE ((4 >< 0) (if GOOD_MODE ((4 >< 0) n) then n else n || 31w))) /\ 2508 (!psr. 2509 (if GOOD_MODE (psr.M) /\ (psr.IT = 0w) then psr 2510 else psr with <| IT := 0w; M := 16w |>).M <> 22w) /\ 2511 (!psr. 2512 GOOD_MODE ((if GOOD_MODE (psr.M) /\ (psr.IT = 0w) then psr 2513 else psr with <| IT := 0w; M := 16w |>).M))`, 2514 SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_EXTRACT_ss) []); 2515 2516val good_it = Q.store_thm("good_it", 2517 `!b it:word8. (if b /\ (it = 0w) then it else 0w) = 0w`, 2518 SRW_TAC [] []); 2519 2520val IT_concat = with_flag (wordsLib.guessing_word_lengths,true) 2521 Q.store_thm("IT_concat", 2522 `!w:word8. (7 >< 2) w @@ (1 >< 0) w = w`, 2523 SRW_TAC [wordsLib.WORD_EXTRACT_ss] []); 2524 2525val IT_concat0 = with_flag (wordsLib.guessing_word_lengths,true) 2526 Q.store_thm("IT_concat0", 2527 `!a:word8 b:word8. ((7 >< 2) a @@ (2 >< 1) b = 0w) = 2528 ((7 >< 2) a = 0w) /\ ((2 >< 1) b = 0w)`, 2529 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [] \\ DECIDE_TAC); 2530 2531val divisor_neq_zero = Q.store_thm("divisor_neq_zero", 2532 `!m:word32. (if m <> 0w then m else 1w) <> 0w`, 2533 SRW_TAC [] []); 2534 2535val it_con_thm = with_flag (wordsLib.guessing_word_lengths,true) 2536 Q.store_thm("it_con_thm", 2537 `(!a:word8. (7 >< 2) (if (7 >< 2) a = 0w then a else 0w) = 0w) /\ 2538 (!a:word8. (2 >< 1) (if (2 >< 1) a = 0w then a else 0w) = 0w)`, 2539 SRW_TAC [] []); 2540 2541val it_mode_imp_thm = with_flag (wordsLib.guessing_word_lengths,true) 2542 Q.store_thm("it_mode_imp_thm", 2543 `(!a:word8 b:word8 c:word8 d:word8. 2544 GOOD_MODE ((4 >< 0) (a @@ b @@ c @@ d)) ==> GOOD_MODE ((4 >< 0) d)) /\ 2545 (!a:word8 b:word8 c:word8 d:word8. 2546 ((15 >< 10) (a @@ b @@ c @@ d) @@ (26 >< 25) (a @@ b @@ c @@ d) = 0w) ==> 2547 ((2 >< 1) a = 0w) /\ ((7 >< 2) c = 0w))`, 2548 SRW_TAC [] [it_mode_concat, IT_concat0]); 2549 2550(* ------------------------------------------------------------------------- *) 2551 2552val FCP_ISET = Q.prove( 2553 `((FCP i. F) = 0w:word2) /\ ((FCP i. (i = 0)) = 1w:word2) /\ 2554 ((FCP i. (i = 1)) = 2w:word2) /\ ((FCP i. (i = 1) \/ (i = 0)) = 3w:word2)`, 2555 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []); 2556 2557val bx_write_pc_thm = Q.prove( 2558 `!address:word32. 2559 (if address ' 0 then 2560 select_instr_set ii InstrSet_Thumb >>= 2561 (\u. branch_to ii ((31 '' 1) address)) 2562 else if ~(address ' 1) then 2563 select_instr_set ii InstrSet_ARM >>= 2564 (\u. branch_to ii address) 2565 else 2566 errorT s) = 2567 if aligned_bx address then 2568 (\s. 2569 if (s.psrs (ii.proc,CPSR)).J /\ (s.psrs (ii.proc,CPSR)).T /\ 2570 ~(address ' 0) 2571 then 2572 errorT "select_instr_set: unpredictable" s 2573 else 2574 write_cpsr ii 2575 ((s.psrs (ii.proc,CPSR)) with 2576 <| J := F; T := address ' 0 |>) s) >>= 2577 (\u. branch_to ii 2578 (if address ' 0 then (31 '' 1) address else address)) 2579 else 2580 errorT s`, 2581 SRW_TAC [] [aligned_bx_thm, select_instr_set_def, 2582 current_instr_set_def, 2583 read_isetstate_def, write_isetstate_def, 2584 read_cpsr_def, read__psr_def, 2585 write_cpsr_def, write__psr_def, 2586 seqT_def, readT_def, writeT_def, constT_def, 2587 EVAL ``1w:word2 ' 1``, EVAL ``1w:word2 ' 0``, word_0, FUN_EQ_THM] 2588 \\ FULL_SIMP_TAC (srw_ss()) [] 2589 \\ Cases_on `(x.psrs (ii.proc,CPSR)).J` 2590 \\ Cases_on `(x.psrs (ii.proc,CPSR)).T` 2591 \\ ASM_SIMP_TAC (srw_ss()) [FCP_ISET]); 2592 2593val align32 = 2594 align_248 |> INST_TYPE [alpha |-> ``:32``] 2595 |> SIMP_RULE (srw_ss()) [] 2596 |> GSYM; 2597 2598val bx_write_pc = save_thm("bx_write_pc", 2599 SIMP_RULE std_ss [align32, bx_write_pc_thm, branch_to_def] bx_write_pc_def); 2600 2601val branch_write_pc = Q.store_thm("branch_write_pc", 2602 `!address ii. 2603 branch_write_pc ii address = 2604 seqT (parT (arch_version ii) (read_cpsr ii)) 2605 (\(version,cpsr). 2606 if version < 6 /\ ~aligned(address,4) /\ ~cpsr.J /\ ~cpsr.T 2607 then 2608 errorT "branch_write_pc: unpredictable" 2609 else 2610 branch_to ii 2611 (if ~cpsr.J /\ ~cpsr.T then 2612 align (address,4) 2613 else 2614 align (address,2)))`, 2615 SRW_TAC [] [branch_write_pc_def, arch_version_def, read_cpsr_def, 2616 read__psr_def, current_instr_set_def, 2617 read_isetstate_def, branch_to_def, errorT_def, 2618 read_arch_def, version_number_def, 2619 parT_def, seqT_def, readT_def, writeT_def, 2620 constT_def, 2621 FUN_EQ_THM] 2622 \\ Cases_on `(x.psrs (ii.proc,CPSR)).J` 2623 \\ Cases_on `(x.psrs (ii.proc,CPSR)).T` 2624 \\ ASM_SIMP_TAC (srw_ss()) [GSYM aligned_248, align32, FCP_ISET]); 2625 2626val compare_branch_instr_thm = Q.prove( 2627 `!ii imm6:word6. 2628 (\rn:word32. 2629 if nonzero <=/=> (rn = 0w) then 2630 read_reg ii 15w >>= 2631 (\pc. 2632 let imm32 = w2w imm6 << 1 in 2633 branch_write_pc ii (pc + imm32)) 2634 else 2635 increment_pc ii Encoding_Thumb) = 2636 (\rn. 2637 (read_reg ii 15w ||| current_instr_set ii) >>= 2638 (\(pc,iset). 2639 if (iset = InstrSet_ARM) then 2640 if nonzero <=/=> (rn = 0w) then 2641 branch_write_pc ii (pc + w2w imm6 << 1) 2642 else 2643 increment_pc ii Encoding_Thumb 2644 else 2645 branch_to ii (if nonzero <=/=> (rn = 0w) then 2646 (31 '' 1) (pc + w2w imm6 << 1) 2647 else 2648 pc - 2w)))`, 2649 SRW_TAC [boolSimps.LET_ss] [current_instr_set_def, 2650 read_isetstate_def, read_cpsr_def, read__psr_def, 2651 read_reg_def, read_pc_def, read__reg_def, 2652 parT_def, seqT_def, readT_def, writeT_def, 2653 constT_def, branch_write_pc_def, arch_version_def, 2654 read_arch_def, branch_to_def, 2655 increment_pc_def, 2656 FUN_EQ_THM] 2657 \\ NTAC 2 (SRW_TAC [] [])); 2658 2659val compare_branch_instr = save_thm("compare_branch_instr", 2660 REWRITE_RULE [compare_branch_instr_thm, align32] 2661 arm_opsemTheory.compare_branch_instr); 2662 2663val error_option_case_COND_RAND = Q.store_thm("error_option_case_COND_RAND", 2664 `!c f f1 a0 a1 a2 a3. 2665 error_option_CASE (if c then ValueState a0 a1 else ValueState a2 a3) f f1 = 2666 if c then 2667 f a0 a1 2668 else 2669 f a2 a3`, 2670 SRW_TAC [] []); 2671 2672(* ------------------------------------------------------------------------- *) 2673 2674val ARM_READ_REG_FROM_MODE = Q.store_thm("ARM_READ_REG_FROM_MODE", 2675 `(!s m. ARM_READ_REG_MODE (0w, m) s = ARM_READ_REG 0w s) /\ 2676 (!s m. ARM_READ_REG_MODE (1w, m) s = ARM_READ_REG 1w s) /\ 2677 (!s m. ARM_READ_REG_MODE (2w, m) s = ARM_READ_REG 2w s) /\ 2678 (!s m. ARM_READ_REG_MODE (3w, m) s = ARM_READ_REG 3w s) /\ 2679 (!s m. ARM_READ_REG_MODE (4w, m) s = ARM_READ_REG 4w s) /\ 2680 (!s m. ARM_READ_REG_MODE (5w, m) s = ARM_READ_REG 5w s) /\ 2681 (!s m. ARM_READ_REG_MODE (6w, m) s = ARM_READ_REG 6w s) /\ 2682 (!s m. ARM_READ_REG_MODE (7w, m) s = ARM_READ_REG 7w s) /\ 2683 (!s. (ARM_MODE s = 0b10001w) ==> 2684 (ARM_READ_REG_MODE (8w, 0b10001w) s = ARM_READ_REG 8w s)) /\ 2685 (!s m. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2686 (ARM_READ_REG_MODE (8w, m) s = ARM_READ_REG 8w s)) /\ 2687 (!s. (ARM_MODE s = 0b10001w) ==> 2688 (ARM_READ_REG_MODE (9w, 0b10001w) s = ARM_READ_REG 9w s)) /\ 2689 (!s m. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2690 (ARM_READ_REG_MODE (9w, m) s = ARM_READ_REG 9w s)) /\ 2691 (!s. (ARM_MODE s = 0b10001w) ==> 2692 (ARM_READ_REG_MODE (10w, 0b10001w) s = ARM_READ_REG 10w s)) /\ 2693 (!s m. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2694 (ARM_READ_REG_MODE (10w, m) s = ARM_READ_REG 10w s)) /\ 2695 (!s. (ARM_MODE s = 0b10001w) ==> 2696 (ARM_READ_REG_MODE (11w, 0b10001w) s = ARM_READ_REG 11w s)) /\ 2697 (!s m. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2698 (ARM_READ_REG_MODE (11w, m) s = ARM_READ_REG 11w s)) /\ 2699 (!s. (ARM_MODE s = 0b10001w) ==> 2700 (ARM_READ_REG_MODE (12w, 0b10001w) s = ARM_READ_REG 12w s)) /\ 2701 (!s m. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2702 (ARM_READ_REG_MODE (12w, m) s = ARM_READ_REG 12w s)) /\ 2703 (!s m. (ARM_MODE s = m) ==> 2704 (ARM_READ_REG_MODE (13w, m) s = ARM_READ_REG 13w s)) /\ 2705 (!s m. (ARM_MODE s = m) ==> 2706 (ARM_READ_REG_MODE (14w, m) s = ARM_READ_REG 14w s)) /\ 2707 (!s m. ARM_READ_REG_MODE (15w,m) s = ARM_READ_REG 15w s)`, 2708 SRW_TAC [] [ARM_READ_REG_MODE_def,ARM_READ_REG_def,RevLookUpRName_def]); 2709 2710val ARM_WRITE_REG_FROM_MODE = Q.store_thm("ARM_WRITE_REG_FROM_MODE", 2711 `(!s m d. ARM_WRITE_REG_MODE (0w, m) d s = ARM_WRITE_REG 0w d s) /\ 2712 (!s m d. ARM_WRITE_REG_MODE (1w, m) d s = ARM_WRITE_REG 1w d s) /\ 2713 (!s m d. ARM_WRITE_REG_MODE (2w, m) d s = ARM_WRITE_REG 2w d s) /\ 2714 (!s m d. ARM_WRITE_REG_MODE (3w, m) d s = ARM_WRITE_REG 3w d s) /\ 2715 (!s m d. ARM_WRITE_REG_MODE (4w, m) d s = ARM_WRITE_REG 4w d s) /\ 2716 (!s m d. ARM_WRITE_REG_MODE (5w, m) d s = ARM_WRITE_REG 5w d s) /\ 2717 (!s m d. ARM_WRITE_REG_MODE (6w, m) d s = ARM_WRITE_REG 6w d s) /\ 2718 (!s m d. ARM_WRITE_REG_MODE (7w, m) d s = ARM_WRITE_REG 7w d s) /\ 2719 (!s d. (ARM_MODE s = 0b10001w) ==> 2720 (ARM_WRITE_REG_MODE (8w, 0b10001w) d s = ARM_WRITE_REG 8w d s)) /\ 2721 (!s m d. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2722 (ARM_WRITE_REG_MODE (8w, m) d s = ARM_WRITE_REG 8w d s)) /\ 2723 (!s d. (ARM_MODE s = 0b10001w) ==> 2724 (ARM_WRITE_REG_MODE (9w, 0b10001w) d s = ARM_WRITE_REG 9w d s)) /\ 2725 (!s m d. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2726 (ARM_WRITE_REG_MODE (9w, m) d s = ARM_WRITE_REG 9w d s)) /\ 2727 (!s d. (ARM_MODE s = 0b10001w) ==> 2728 (ARM_WRITE_REG_MODE (10w, 0b10001w) d s = ARM_WRITE_REG 10w d s)) /\ 2729 (!s m d. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2730 (ARM_WRITE_REG_MODE (10w, m) d s = ARM_WRITE_REG 10w d s)) /\ 2731 (!s d. (ARM_MODE s = 0b10001w) ==> 2732 (ARM_WRITE_REG_MODE (11w, 0b10001w) d s = ARM_WRITE_REG 11w d s)) /\ 2733 (!s m d. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2734 (ARM_WRITE_REG_MODE (11w, m) d s = ARM_WRITE_REG 11w d s)) /\ 2735 (!s d. (ARM_MODE s = 0b10001w) ==> 2736 (ARM_WRITE_REG_MODE (12w, 0b10001w) d s = ARM_WRITE_REG 12w d s)) /\ 2737 (!s m d. (ARM_MODE s <> 0b10001w) /\ (m <> 0b10001w) ==> 2738 (ARM_WRITE_REG_MODE (12w, m) d s = ARM_WRITE_REG 12w d s)) /\ 2739 (!s m d. (ARM_MODE s = m) ==> 2740 (ARM_WRITE_REG_MODE (13w, m) d s = ARM_WRITE_REG 13w d s)) /\ 2741 (!s m d. (ARM_MODE s = m) ==> 2742 (ARM_WRITE_REG_MODE (14w, m) d s = ARM_WRITE_REG 14w d s)) /\ 2743 (!s m d. ARM_WRITE_REG_MODE (15w,m) d s = ARM_WRITE_REG 15w d s)`, 2744 SRW_TAC [] [ARM_WRITE_REG_MODE_def,ARM_WRITE_REG_def,RevLookUpRName_def]); 2745 2746val ARM_READ_SPSR_FROM_MODE = Q.store_thm("ARM_READ_SPSR_FROM_MODE", 2747 `(!s. (ARM_MODE s = 0b10001w) ==> 2748 (ARM_READ_SPSR_MODE 0b10001w s = ARM_READ_SPSR s)) /\ 2749 (!s. (ARM_MODE s = 0b10010w) ==> 2750 (ARM_READ_SPSR_MODE 0b10010w s = ARM_READ_SPSR s)) /\ 2751 (!s. (ARM_MODE s = 0b10011w) ==> 2752 (ARM_READ_SPSR_MODE 0b10011w s = ARM_READ_SPSR s)) /\ 2753 (!s. (ARM_MODE s = 0b10110w) ==> 2754 (ARM_READ_SPSR_MODE 0b10110w s = ARM_READ_SPSR s)) /\ 2755 (!s. (ARM_MODE s = 0b10111w) ==> 2756 (ARM_READ_SPSR_MODE 0b10111w s = ARM_READ_SPSR s)) /\ 2757 (!s. (ARM_MODE s = 0b11011w) ==> 2758 (ARM_READ_SPSR_MODE 0b11011w s = ARM_READ_SPSR s))`, 2759 SRW_TAC [] [ARM_READ_SPSR_def]); 2760 2761val ARM_WRITE_SPSR_FROM_MODE = Q.store_thm("ARM_WRITE_SPSR_FROM_MODE", 2762 `(!d s. (ARM_MODE s = 0b10001w) ==> 2763 (ARM_WRITE_SPSR_MODE 0b10001w d s = ARM_WRITE_SPSR d s)) /\ 2764 (!d s. (ARM_MODE s = 0b10010w) ==> 2765 (ARM_WRITE_SPSR_MODE 0b10010w d s = ARM_WRITE_SPSR d s)) /\ 2766 (!d s. (ARM_MODE s = 0b10011w) ==> 2767 (ARM_WRITE_SPSR_MODE 0b10011w d s = ARM_WRITE_SPSR d s)) /\ 2768 (!d s. (ARM_MODE s = 0b10110w) ==> 2769 (ARM_WRITE_SPSR_MODE 0b10110w d s = ARM_WRITE_SPSR d s)) /\ 2770 (!d s. (ARM_MODE s = 0b10111w) ==> 2771 (ARM_WRITE_SPSR_MODE 0b10111w d s = ARM_WRITE_SPSR d s)) /\ 2772 (!d s. (ARM_MODE s = 0b11011w) ==> 2773 (ARM_WRITE_SPSR_MODE 0b11011w d s = ARM_WRITE_SPSR d s))`, 2774 SRW_TAC [] [ARM_WRITE_SPSR_def]); 2775 2776val ARM_WRITE_CPSR = Q.store_thm("ARM_WRITE_CPSR", 2777 `(!b state cpsr. 2778 (ARM_READ_CPSR state = cpsr) ==> 2779 (ARM_WRITE_CPSR (cpsr with N := b) state = 2780 ARM_WRITE_STATUS psrN b state)) /\ 2781 (!b state cpsr. 2782 (ARM_READ_CPSR state = cpsr) ==> 2783 (ARM_WRITE_CPSR (cpsr with Z := b) state = 2784 ARM_WRITE_STATUS psrZ b state)) /\ 2785 (!b state cpsr. 2786 (ARM_READ_CPSR state = cpsr) ==> 2787 (ARM_WRITE_CPSR (cpsr with C := b) state = 2788 ARM_WRITE_STATUS psrC b state)) /\ 2789 (!b state cpsr. 2790 (ARM_READ_CPSR state = cpsr) ==> 2791 (ARM_WRITE_CPSR (cpsr with V := b) state = 2792 ARM_WRITE_STATUS psrV b state)) /\ 2793 (!b state cpsr. 2794 (ARM_READ_CPSR state = cpsr) ==> 2795 (ARM_WRITE_CPSR (cpsr with Q := b) state = 2796 ARM_WRITE_STATUS psrQ b state)) /\ 2797 (!b state cpsr. 2798 (ARM_READ_CPSR state = cpsr) ==> 2799 (ARM_WRITE_CPSR (cpsr with J := b) state = 2800 ARM_WRITE_STATUS psrJ b state)) /\ 2801 (!b state cpsr. 2802 (ARM_READ_CPSR state = cpsr) ==> 2803 (ARM_WRITE_CPSR (cpsr with E := b) state = 2804 ARM_WRITE_STATUS psrE b state)) /\ 2805 (!b state cpsr. 2806 (ARM_READ_CPSR state = cpsr) ==> 2807 (ARM_WRITE_CPSR (cpsr with A := b) state = 2808 ARM_WRITE_STATUS psrA b state)) /\ 2809 (!b state cpsr. 2810 (ARM_READ_CPSR state = cpsr) ==> 2811 (ARM_WRITE_CPSR (cpsr with I := b) state = 2812 ARM_WRITE_STATUS psrI b state)) /\ 2813 (!b state cpsr. 2814 (ARM_READ_CPSR state = cpsr) ==> 2815 (ARM_WRITE_CPSR (cpsr with F := b) state = 2816 ARM_WRITE_STATUS psrF b state)) /\ 2817 (!b state cpsr. 2818 (ARM_READ_CPSR state = cpsr) ==> 2819 (ARM_WRITE_CPSR (cpsr with T := b) state = 2820 ARM_WRITE_STATUS psrT b state)) /\ 2821 (!ge state cpsr. 2822 (ARM_READ_CPSR state = cpsr) ==> 2823 (ARM_WRITE_CPSR (cpsr with GE := ge) state = 2824 ARM_WRITE_GE ge state)) /\ 2825 (!it state cpsr. 2826 (ARM_READ_CPSR state = cpsr) ==> 2827 (ARM_WRITE_CPSR (cpsr with IT := it) state = 2828 ARM_WRITE_IT it state)) /\ 2829 (!m state cpsr. 2830 (ARM_READ_CPSR state = cpsr) ==> 2831 (ARM_WRITE_CPSR (cpsr with M := m) state = 2832 ARM_WRITE_MODE m state))`, 2833 SRW_TAC [] [ARM_WRITE_STATUS_def, ARM_WRITE_GE_def, ARM_WRITE_IT_def, 2834 ARM_WRITE_MODE_def, ARM_READ_CPSR_def, ARM_WRITE_CPSR_def, 2835 APPLY_UPDATE_THM, FUN_EQ_THM, arm_state_component_equality]); 2836 2837val ARM_WRITE_SPSR = Q.store_thm("ARM_WRITE_SPSR", 2838 `(!b state cpsr. 2839 (ARM_READ_SPSR state = cpsr) ==> 2840 (ARM_WRITE_SPSR (cpsr with N := b) state = 2841 ARM_WRITE_STATUS_SPSR psrN b state)) /\ 2842 (!b state cpsr. 2843 (ARM_READ_SPSR state = cpsr) ==> 2844 (ARM_WRITE_SPSR (cpsr with Z := b) state = 2845 ARM_WRITE_STATUS_SPSR psrZ b state)) /\ 2846 (!b state cpsr. 2847 (ARM_READ_SPSR state = cpsr) ==> 2848 (ARM_WRITE_SPSR (cpsr with C := b) state = 2849 ARM_WRITE_STATUS_SPSR psrC b state)) /\ 2850 (!b state cpsr. 2851 (ARM_READ_SPSR state = cpsr) ==> 2852 (ARM_WRITE_SPSR (cpsr with V := b) state = 2853 ARM_WRITE_STATUS_SPSR psrV b state)) /\ 2854 (!b state cpsr. 2855 (ARM_READ_SPSR state = cpsr) ==> 2856 (ARM_WRITE_SPSR (cpsr with Q := b) state = 2857 ARM_WRITE_STATUS_SPSR psrQ b state)) /\ 2858 (!b state cpsr. 2859 (ARM_READ_SPSR state = cpsr) ==> 2860 (ARM_WRITE_SPSR (cpsr with J := b) state = 2861 ARM_WRITE_STATUS_SPSR psrJ b state)) /\ 2862 (!b state cpsr. 2863 (ARM_READ_SPSR state = cpsr) ==> 2864 (ARM_WRITE_SPSR (cpsr with E := b) state = 2865 ARM_WRITE_STATUS_SPSR psrE b state)) /\ 2866 (!b state cpsr. 2867 (ARM_READ_SPSR state = cpsr) ==> 2868 (ARM_WRITE_SPSR (cpsr with A := b) state = 2869 ARM_WRITE_STATUS_SPSR psrA b state)) /\ 2870 (!b state cpsr. 2871 (ARM_READ_SPSR state = cpsr) ==> 2872 (ARM_WRITE_SPSR (cpsr with I := b) state = 2873 ARM_WRITE_STATUS_SPSR psrI b state)) /\ 2874 (!b state cpsr. 2875 (ARM_READ_SPSR state = cpsr) ==> 2876 (ARM_WRITE_SPSR (cpsr with F := b) state = 2877 ARM_WRITE_STATUS_SPSR psrF b state)) /\ 2878 (!b state cpsr. 2879 (ARM_READ_SPSR state = cpsr) ==> 2880 (ARM_WRITE_SPSR (cpsr with T := b) state = 2881 ARM_WRITE_STATUS_SPSR psrT b state)) /\ 2882 (!ge state cpsr. 2883 (ARM_READ_SPSR state = cpsr) ==> 2884 (ARM_WRITE_SPSR (cpsr with GE := ge) state = 2885 ARM_WRITE_GE_SPSR ge state)) /\ 2886 (!it state cpsr. 2887 (ARM_READ_SPSR state = cpsr) ==> 2888 (ARM_WRITE_SPSR (cpsr with IT := it) state = 2889 ARM_WRITE_IT_SPSR it state)) /\ 2890 (!m state cpsr. 2891 (ARM_READ_SPSR state = cpsr) ==> 2892 (ARM_WRITE_SPSR (cpsr with M := m) state = 2893 ARM_WRITE_MODE_SPSR m state))`, 2894 SRW_TAC [] [ARM_WRITE_STATUS_SPSR_def, ARM_WRITE_GE_SPSR_def, 2895 ARM_WRITE_IT_SPSR_def, ARM_WRITE_MODE_SPSR_def, ARM_READ_SPSR_def, 2896 ARM_WRITE_SPSR_def, ARM_READ_SPSR_MODE_def, ARM_WRITE_SPSR_MODE_def, 2897 APPLY_UPDATE_THM, FUN_EQ_THM, arm_state_component_equality]); 2898 2899(* ------------------------------------------------------------------------- *) 2900 2901val MARK_AND_CLEAR_EXCLUSIVE = Q.store_thm("MARK_AND_CLEAR_EXCLUSIVE", 2902 `(!mon mstate a n s. 2903 (mon = s.monitors) ==> 2904 (s with monitors := mon with state := 2905 SND (mon.ClearExclusiveByAddress (a,<| proc := 0 |>,n) 2906 mstate) = 2907 CLEAR_EXCLUSIVE_BY_ADDRESS (a,n) 2908 (s with monitors := mon with state := mstate)) /\ 2909 (s with monitors := mon with state := mon.state = s)) /\ 2910 (!mon mstate a n s. 2911 (mon = s.monitors) ==> 2912 (s with monitors := mon with state := 2913 SND (mon.MarkExclusiveLocal (a,<| proc := 0 |>,n) 2914 mstate) = 2915 MARK_EXCLUSIVE_LOCAL (a,n) 2916 (s with monitors := mon with state := mstate)) /\ 2917 (s with monitors := mon with state := mon.state = s)) /\ 2918 (!mon mstate a n s. 2919 (mon = s.monitors) ==> 2920 (s with monitors := mon with state := 2921 SND (mon.MarkExclusiveGlobal (a,<| proc := 0 |>,n) 2922 mstate) = 2923 MARK_EXCLUSIVE_GLOBAL (a,n) 2924 (s with monitors := mon with state := mstate)) /\ 2925 (s with monitors := mon with state := mon.state = s)) /\ 2926 (!mon mstate s. 2927 (mon = s.monitors) ==> 2928 (s with monitors := mon with state := 2929 SND (mon.ClearExclusiveLocal 0 mstate) = 2930 CLEAR_EXCLUSIVE_LOCAL 2931 (s with monitors := mon with state := mstate)) /\ 2932 (s with monitors := mon with state := mon.state = s))`, 2933 SRW_TAC [] [CLEAR_EXCLUSIVE_BY_ADDRESS_def, MARK_EXCLUSIVE_GLOBAL_def, 2934 MARK_EXCLUSIVE_LOCAL_def, CLEAR_EXCLUSIVE_LOCAL_def, 2935 arm_state_component_equality, ExclusiveMonitors_component_equality]); 2936 2937val ARM_WRITE_MEM_o = Q.store_thm("ARM_WRITE_MEM_o", 2938 `(!a w g s. 2939 (ARM_WRITE_MEM a w (s with memory updated_by g) = 2940 (s with memory updated_by (a =+ w) o g))) /\ 2941 (!a w g s. 2942 (ARM_WRITE_MEM_WRITE a w (s with accesses updated_by g) = 2943 (s with accesses updated_by (CONS (MEM_WRITE a w)) o g))) /\ 2944 (!a g s. 2945 (ARM_WRITE_MEM_READ a (s with accesses updated_by g) = 2946 (s with accesses updated_by (CONS (MEM_READ a)) o g)))`, 2947 SRW_TAC [] 2948 [ARM_WRITE_MEM_def, ARM_WRITE_MEM_WRITE_def, ARM_WRITE_MEM_READ_def]); 2949 2950val ARM_WRITE_REG_o = Q.store_thm("ARM_WRITE_REG_o", 2951 `!x w g s. 2952 (ARM_WRITE_REG_MODE x w (s with registers updated_by g) = 2953 (s with registers updated_by ((0,RevLookUpRName x) =+ w) o g))`, 2954 SRW_TAC [] [ARM_WRITE_REG_MODE_def]); 2955 2956val ARM_WRITE_PSR_o = Q.store_thm("ARM_WRITE_PSR_o", 2957 `(!w g s. 2958 (ARM_WRITE_CPSR w (s with psrs updated_by g) = 2959 (s with psrs updated_by ((0,CPSR) =+ w) o g))) /\ 2960 (!w g s. 2961 (ARM_WRITE_SPSR_MODE 0b10001w w (s with psrs updated_by g) = 2962 (s with psrs updated_by ((0,SPSR_fiq) =+ w) o g))) /\ 2963 (!w g s. 2964 (ARM_WRITE_SPSR_MODE 0b10010w w (s with psrs updated_by g) = 2965 (s with psrs updated_by ((0,SPSR_irq) =+ w) o g))) /\ 2966 (!w g s. 2967 (ARM_WRITE_SPSR_MODE 0b10011w w (s with psrs updated_by g) = 2968 (s with psrs updated_by ((0,SPSR_svc) =+ w) o g))) /\ 2969 (!w g s. 2970 (ARM_WRITE_SPSR_MODE 0b10110w w (s with psrs updated_by g) = 2971 (s with psrs updated_by ((0,SPSR_mon) =+ w) o g))) /\ 2972 (!w g s. 2973 (ARM_WRITE_SPSR_MODE 0b10111w w (s with psrs updated_by g) = 2974 (s with psrs updated_by ((0,SPSR_abt) =+ w) o g))) /\ 2975 (!w g s. 2976 (ARM_WRITE_SPSR_MODE 0b11011w w (s with psrs updated_by g) = 2977 (s with psrs updated_by ((0,SPSR_und) =+ w) o g)))`, 2978 SRW_TAC [] [ARM_WRITE_CPSR_def, ARM_WRITE_SPSR_MODE_def, SPSR_MODE_def]); 2979 2980val ARM_WRITE_CPSR_o = Q.store_thm("ARM_WRITE_CPSR_o", 2981 `(!b state cpsr. 2982 ARM_WRITE_CPSR (ARMpsr_N_fupd (K b) cpsr) state = 2983 ARM_WRITE_STATUS psrN b (ARM_WRITE_CPSR cpsr state)) /\ 2984 (!b state cpsr. 2985 ARM_WRITE_CPSR (ARMpsr_Z_fupd (K b) cpsr) state = 2986 ARM_WRITE_STATUS psrZ b (ARM_WRITE_CPSR cpsr state)) /\ 2987 (!b state cpsr. 2988 ARM_WRITE_CPSR (ARMpsr_C_fupd (K b) cpsr) state = 2989 ARM_WRITE_STATUS psrC b (ARM_WRITE_CPSR cpsr state)) /\ 2990 (!b state cpsr. 2991 ARM_WRITE_CPSR (ARMpsr_V_fupd (K b) cpsr) state = 2992 ARM_WRITE_STATUS psrV b (ARM_WRITE_CPSR cpsr state)) /\ 2993 (!b state cpsr. 2994 ARM_WRITE_CPSR (ARMpsr_Q_fupd (K b) cpsr) state = 2995 ARM_WRITE_STATUS psrQ b (ARM_WRITE_CPSR cpsr state)) /\ 2996 (!b state cpsr. 2997 ARM_WRITE_CPSR (ARMpsr_J_fupd (K b) cpsr) state = 2998 ARM_WRITE_STATUS psrJ b (ARM_WRITE_CPSR cpsr state)) /\ 2999 (!b state cpsr. 3000 ARM_WRITE_CPSR (ARMpsr_E_fupd (K b) cpsr) state = 3001 ARM_WRITE_STATUS psrE b (ARM_WRITE_CPSR cpsr state)) /\ 3002 (!b state cpsr. 3003 ARM_WRITE_CPSR (ARMpsr_A_fupd (K b) cpsr) state = 3004 ARM_WRITE_STATUS psrA b (ARM_WRITE_CPSR cpsr state)) /\ 3005 (!b state cpsr. 3006 ARM_WRITE_CPSR (ARMpsr_I_fupd (K b) cpsr) state = 3007 ARM_WRITE_STATUS psrI b (ARM_WRITE_CPSR cpsr state)) /\ 3008 (!b state cpsr. 3009 ARM_WRITE_CPSR (ARMpsr_F_fupd (K b) cpsr) state = 3010 ARM_WRITE_STATUS psrF b (ARM_WRITE_CPSR cpsr state)) /\ 3011 (!b state cpsr. 3012 ARM_WRITE_CPSR (ARMpsr_T_fupd (K b) cpsr) state = 3013 ARM_WRITE_STATUS psrT b (ARM_WRITE_CPSR cpsr state)) /\ 3014 (!ge state cpsr. 3015 ARM_WRITE_CPSR (ARMpsr_GE_fupd (K ge) cpsr) state = 3016 ARM_WRITE_GE ge (ARM_WRITE_CPSR cpsr state)) /\ 3017 (!it state cpsr. 3018 ARM_WRITE_CPSR (ARMpsr_IT_fupd (K it) cpsr) state = 3019 ARM_WRITE_IT it (ARM_WRITE_CPSR cpsr state))`, 3020 SRW_TAC [] [ARM_WRITE_STATUS_def, ARM_WRITE_GE_def, ARM_WRITE_IT_def, 3021 ARM_WRITE_MODE_def, ARM_READ_CPSR_def, ARM_WRITE_CPSR_def, 3022 APPLY_UPDATE_THM, FUN_EQ_THM, arm_state_component_equality]); 3023 3024val SPSR_MODE_NOT_CPSR = Q.prove( 3025 `!m. SPSR_MODE m <> CPSR`, 3026 STRIP_TAC \\ Cases_on `m IN {17w; 18w; 19w; 22w; 23w}` 3027 \\ FULL_SIMP_TAC (srw_ss()) [SPSR_MODE_def]); 3028 3029val ARM_WRITE_SPSR_o = Q.store_thm("ARM_WRITE_SPSR_o", 3030 `(!b state cpsr. 3031 (ARM_WRITE_SPSR (ARMpsr_N_fupd (K b) cpsr) state = 3032 ARM_WRITE_STATUS_SPSR psrN b (ARM_WRITE_SPSR cpsr state))) /\ 3033 (!b state cpsr. 3034 (ARM_WRITE_SPSR (ARMpsr_Z_fupd (K b) cpsr) state = 3035 ARM_WRITE_STATUS_SPSR psrZ b (ARM_WRITE_SPSR cpsr state))) /\ 3036 (!b state cpsr. 3037 (ARM_WRITE_SPSR (ARMpsr_C_fupd (K b) cpsr) state = 3038 ARM_WRITE_STATUS_SPSR psrC b (ARM_WRITE_SPSR cpsr state))) /\ 3039 (!b state cpsr. 3040 (ARM_WRITE_SPSR (ARMpsr_V_fupd (K b) cpsr) state = 3041 ARM_WRITE_STATUS_SPSR psrV b (ARM_WRITE_SPSR cpsr state))) /\ 3042 (!b state cpsr. 3043 (ARM_WRITE_SPSR (ARMpsr_Q_fupd (K b) cpsr) state = 3044 ARM_WRITE_STATUS_SPSR psrQ b (ARM_WRITE_SPSR cpsr state))) /\ 3045 (!b state cpsr. 3046 (ARM_WRITE_SPSR (ARMpsr_J_fupd (K b) cpsr) state = 3047 ARM_WRITE_STATUS_SPSR psrJ b (ARM_WRITE_SPSR cpsr state))) /\ 3048 (!b state cpsr. 3049 (ARM_WRITE_SPSR (ARMpsr_E_fupd (K b) cpsr) state = 3050 ARM_WRITE_STATUS_SPSR psrE b (ARM_WRITE_SPSR cpsr state))) /\ 3051 (!b state cpsr. 3052 (ARM_WRITE_SPSR (ARMpsr_A_fupd (K b) cpsr) state = 3053 ARM_WRITE_STATUS_SPSR psrA b (ARM_WRITE_SPSR cpsr state))) /\ 3054 (!b state cpsr. 3055 (ARM_WRITE_SPSR (ARMpsr_I_fupd (K b) cpsr) state = 3056 ARM_WRITE_STATUS_SPSR psrI b (ARM_WRITE_SPSR cpsr state))) /\ 3057 (!b state cpsr. 3058 (ARM_WRITE_SPSR (ARMpsr_F_fupd (K b) cpsr) state = 3059 ARM_WRITE_STATUS_SPSR psrF b (ARM_WRITE_SPSR cpsr state))) /\ 3060 (!b state cpsr. 3061 (ARM_WRITE_SPSR (ARMpsr_T_fupd (K b) cpsr) state = 3062 ARM_WRITE_STATUS_SPSR psrT b (ARM_WRITE_SPSR cpsr state))) /\ 3063 (!ge state cpsr. 3064 (ARM_WRITE_SPSR (ARMpsr_GE_fupd (K ge) cpsr) state = 3065 ARM_WRITE_GE_SPSR ge (ARM_WRITE_SPSR cpsr state))) /\ 3066 (!it state cpsr. 3067 (ARM_WRITE_SPSR (ARMpsr_IT_fupd (K it) cpsr) state = 3068 ARM_WRITE_IT_SPSR it (ARM_WRITE_SPSR cpsr state)))`, 3069 SRW_TAC [] [ARM_WRITE_STATUS_SPSR_def, ARM_WRITE_GE_SPSR_def, 3070 ARM_WRITE_IT_SPSR_def, ARM_WRITE_MODE_SPSR_def, ARM_READ_SPSR_def, 3071 ARM_WRITE_SPSR_def, ARM_READ_SPSR_MODE_def, ARM_WRITE_SPSR_MODE_def, 3072 ARM_MODE_def, ARM_READ_CPSR_def, APPLY_UPDATE_THM, FUN_EQ_THM, 3073 SPSR_MODE_NOT_CPSR, arm_state_component_equality]); 3074 3075(* ------------------------------------------------------------------------- *) 3076 3077fun arm_reg_rule thm = 3078 Drule.LIST_CONJ 3079 (List.tabulate(16, fn i => 3080 let val r = wordsSyntax.mk_wordii(i,4) in 3081 (GEN_ALL o RIGHT_CONV_RULE EVAL o Drule.SPEC_ALL o Thm.SPEC r) thm 3082 end)); 3083 3084local 3085 val regs = 3086 [(0, "10000"), (1, "10000"), (2, "10000"), (3, "10000"), (4, "10000"), 3087 (5, "10000"), (6, "10000"), (7, "10000"), (8, "10000"), (8, "10001"), 3088 (9, "10000"), (9, "10001"), (10,"10000"), (10,"10001"), (11,"10000"), 3089 (11,"10001"), (12,"10000"), (12,"10001"), (13,"10000"), (13,"10001"), 3090 (13,"10010"), (13,"10011"), (13,"10111"), (13,"11011"), (13,"10110"), 3091 (14,"10000"), (14,"10001"), (14,"10010"), (14,"10011"), (14,"10111"), 3092 (14,"11011"), (14,"10110"), (15,"10000")] 3093in 3094 fun arm_reg_rule thm = 3095 Drule.LIST_CONJ (List.map (fn (i,s) => 3096 let val n = wordsSyntax.mk_wordii(i,4) 3097 val m = wordsSyntax.mk_wordi(Arbnum.fromBinString s,5) 3098 val x = pairSyntax.mk_pair(n,m) 3099 in 3100 (GEN_ALL o RIGHT_CONV_RULE EVAL o Drule.SPEC_ALL o Thm.SPEC x) thm 3101 end) regs) 3102end; 3103 3104val ARM_READ_REG_MODE = save_thm("ARM_READ_REG_MODE", 3105 SIMP_RULE (srw_ss()) [ARM_READ_REG_FROM_MODE] 3106 (arm_reg_rule ARM_READ_REG_MODE_def)); 3107 3108val ARM_WRITE_REG_MODE = save_thm("ARM_WRITE_REG_MODE", 3109 SIMP_RULE (srw_ss()) [ARM_WRITE_REG_FROM_MODE] 3110 (arm_reg_rule ARM_WRITE_REG_MODE_def)); 3111 3112val ARM_WRITE_REG_o = save_thm("ARM_WRITE_REG_o", 3113 SIMP_RULE (srw_ss()) [ARM_WRITE_REG_FROM_MODE] 3114 (arm_reg_rule ARM_WRITE_REG_o)); 3115 3116(* ------------------------------------------------------------------------- *) 3117 3118val PSR_OF_UPDATES = Q.store_thm("PSR_OF_UPDATES", 3119 `(!n m d s. ARM_READ_CPSR (ARM_WRITE_REG_MODE (n,m) d s) = ARM_READ_CPSR s) /\ 3120 (!n d s. ARM_READ_CPSR (ARM_WRITE_REG n d s) = ARM_READ_CPSR s) /\ 3121 (!a d s. ARM_READ_CPSR (ARM_WRITE_MEM a d s) = ARM_READ_CPSR s) /\ 3122 (!a d s. ARM_READ_CPSR (ARM_WRITE_MEM_WRITE a d s) = ARM_READ_CPSR s) /\ 3123 (!a s. ARM_READ_CPSR (ARM_WRITE_MEM_READ a s) = ARM_READ_CPSR s) /\ 3124 (!d s. ARM_READ_CPSR (ARM_WRITE_CPSR d s) = d) /\ 3125 (!d s. ARM_READ_CPSR (ARM_WRITE_SPSR d s) = ARM_READ_CPSR s) /\ 3126 (!m d s. ARM_READ_CPSR (ARM_WRITE_SPSR_MODE m d s) = ARM_READ_CPSR s) /\ 3127 (!f d s. ARM_READ_CPSR (ARM_WRITE_STATUS_SPSR f d s) = ARM_READ_CPSR s) /\ 3128 (!d s. ARM_READ_CPSR (ARM_WRITE_GE_SPSR d s) = ARM_READ_CPSR s) /\ 3129 (!x y s. ARM_READ_CPSR (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = 3130 ARM_READ_CPSR s) /\ 3131 (!d s. ARM_READ_CPSR (ARM_WRITE_IT_SPSR d s) = ARM_READ_CPSR s) /\ 3132 (!d s. ARM_READ_CPSR (ARM_WRITE_MODE_SPSR d s) = ARM_READ_CPSR s) /\ 3133 (!n m d s. ARM_READ_SPSR (ARM_WRITE_REG_MODE (n,m) d s) = ARM_READ_SPSR s) /\ 3134 (!n d s. ARM_READ_SPSR (ARM_WRITE_REG n d s) = ARM_READ_SPSR s) /\ 3135 (!a d s. ARM_READ_SPSR (ARM_WRITE_MEM a d s) = ARM_READ_SPSR s) /\ 3136 (!a d s. ARM_READ_SPSR (ARM_WRITE_MEM_WRITE a d s) = ARM_READ_SPSR s) /\ 3137 (!a s. ARM_READ_SPSR (ARM_WRITE_MEM_READ a s) = ARM_READ_SPSR s) /\ 3138 (!d s. ARM_READ_SPSR (ARM_WRITE_CPSR d s) = ARM_READ_SPSR_MODE d.M s) /\ 3139 (!d s. ARM_READ_SPSR (ARM_WRITE_SPSR d s) = d)`, 3140 REPEAT STRIP_TAC \\ TRY (Cases_on `f`) 3141 \\ SRW_TAC [] [ARM_WRITE_REG_MODE_def, ARM_WRITE_REG_def, ARM_WRITE_MEM_def, 3142 ARM_WRITE_MEM_READ_def, ARM_WRITE_MEM_WRITE_def, 3143 ARM_WRITE_SPSR_def, ARM_WRITE_CPSR_def, ARM_READ_CPSR_def, 3144 ARM_WRITE_SPSR_MODE_def, ARM_WRITE_STATUS_SPSR_def, 3145 ARM_WRITE_GE_SPSR_def, ARM_WRITE_IT_SPSR_def, 3146 ARM_WRITE_MODE_SPSR_def, ARM_READ_SPSR_def, 3147 CLEAR_EXCLUSIVE_BY_ADDRESS_def] 3148 \\ SRW_TAC [] [ARM_WRITE_SPSR_MODE_def, SPSR_MODE_NOT_CPSR, UPDATE_def] 3149 \\ FULL_SIMP_TAC (srw_ss()) [ARM_MODE_def, SPSR_MODE_NOT_CPSR, 3150 ARM_READ_SPSR_MODE_def, ARM_READ_CPSR_def]); 3151 3152val CPSR_COMPONENTS_OF_UPDATES = Q.store_thm("CPSR_COMPONENTS_OF_UPDATES", 3153 `(!f n m d s. 3154 ARM_READ_STATUS f (ARM_WRITE_REG_MODE (n,m) d s) = ARM_READ_STATUS f s) /\ 3155 (!f n d s. ARM_READ_STATUS f (ARM_WRITE_REG n d s) = ARM_READ_STATUS f s) /\ 3156 (!f a d s. ARM_READ_STATUS f (ARM_WRITE_MEM a d s) = ARM_READ_STATUS f s) /\ 3157 (!f a d s. ARM_READ_STATUS f (ARM_WRITE_MEM_WRITE a d s) = 3158 ARM_READ_STATUS f s) /\ 3159 (!f a s. ARM_READ_STATUS f (ARM_WRITE_MEM_READ a s) = ARM_READ_STATUS f s) /\ 3160 (!f ge s. ARM_READ_STATUS f (ARM_WRITE_GE ge s) = ARM_READ_STATUS f s) /\ 3161 (!f it s. ARM_READ_STATUS f (ARM_WRITE_IT it s) = ARM_READ_STATUS f s) /\ 3162 (!f m s. ARM_READ_STATUS f (ARM_WRITE_MODE m s) = ARM_READ_STATUS f s) /\ 3163 (!f b s. ARM_READ_STATUS f (ARM_WRITE_STATUS f b s) = b) /\ 3164 (!f f2 b s. f2 <> f ==> 3165 (ARM_READ_STATUS f (ARM_WRITE_STATUS f2 b s) = ARM_READ_STATUS f s)) /\ 3166 (!f x y s. ARM_READ_STATUS f (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = 3167 ARM_READ_STATUS f s) /\ 3168 (!f d s. ARM_READ_STATUS f (ARM_WRITE_SPSR d s) = ARM_READ_STATUS f s) /\ 3169 (!f it s. ARM_READ_STATUS f (ARM_WRITE_IT_SPSR it s) = 3170 ARM_READ_STATUS f s) /\ 3171 (!f ge s. ARM_READ_STATUS f (ARM_WRITE_GE_SPSR ge s) = 3172 ARM_READ_STATUS f s) /\ 3173 (!f m s. ARM_READ_STATUS f (ARM_WRITE_MODE_SPSR m s) = 3174 ARM_READ_STATUS f s) /\ 3175 (!f f2 b s. ARM_READ_STATUS f (ARM_WRITE_STATUS_SPSR f2 b s) = 3176 ARM_READ_STATUS f s) /\ 3177 (!n m d s. ARM_READ_IT (ARM_WRITE_REG_MODE (n,m) d s) = ARM_READ_IT s) /\ 3178 (!n d s. ARM_READ_IT (ARM_WRITE_REG n d s) = ARM_READ_IT s) /\ 3179 (!a d s. ARM_READ_IT (ARM_WRITE_MEM a d s) = ARM_READ_IT s) /\ 3180 (!a d s. ARM_READ_IT (ARM_WRITE_MEM_WRITE a d s) = ARM_READ_IT s) /\ 3181 (!a s. ARM_READ_IT (ARM_WRITE_MEM_READ a s) = ARM_READ_IT s) /\ 3182 (!ge s. ARM_READ_IT (ARM_WRITE_GE ge s) = ARM_READ_IT s) /\ 3183 (!it s. ARM_READ_IT (ARM_WRITE_IT it s) = it) /\ 3184 (!m s. ARM_READ_IT (ARM_WRITE_MODE m s) = ARM_READ_IT s) /\ 3185 (!f b s. ARM_READ_IT (ARM_WRITE_STATUS f b s) = ARM_READ_IT s) /\ 3186 (!d s. ARM_READ_IT (ARM_WRITE_SPSR d s) = ARM_READ_IT s) /\ 3187 (!it s. ARM_READ_IT (ARM_WRITE_IT_SPSR it s) = ARM_READ_IT s) /\ 3188 (!ge s. ARM_READ_IT (ARM_WRITE_GE_SPSR ge s) = ARM_READ_IT s) /\ 3189 (!m s. ARM_READ_IT (ARM_WRITE_MODE_SPSR m s) = ARM_READ_IT s) /\ 3190 (!f b s. ARM_READ_IT (ARM_WRITE_STATUS_SPSR f b s) = ARM_READ_IT s) /\ 3191 (!n m d s. ARM_READ_GE (ARM_WRITE_REG_MODE (n,m) d s) = ARM_READ_GE s) /\ 3192 (!n d s. ARM_READ_GE (ARM_WRITE_REG n d s) = ARM_READ_GE s) /\ 3193 (!a d s. ARM_READ_GE (ARM_WRITE_MEM a d s) = ARM_READ_GE s) /\ 3194 (!a d s. ARM_READ_GE (ARM_WRITE_MEM_WRITE a d s) = ARM_READ_GE s) /\ 3195 (!a s. ARM_READ_GE (ARM_WRITE_MEM_READ a s) = ARM_READ_GE s) /\ 3196 (!ge s. ARM_READ_GE (ARM_WRITE_GE ge s) = ge) /\ 3197 (!it s. ARM_READ_GE (ARM_WRITE_IT it s) = ARM_READ_GE s) /\ 3198 (!m s. ARM_READ_GE (ARM_WRITE_MODE m s) = ARM_READ_GE s) /\ 3199 (!f b s. ARM_READ_GE (ARM_WRITE_STATUS f b s) = ARM_READ_GE s) /\ 3200 (!d s. ARM_READ_GE (ARM_WRITE_SPSR d s) = ARM_READ_GE s) /\ 3201 (!it s. ARM_READ_GE (ARM_WRITE_IT_SPSR it s) = ARM_READ_GE s) /\ 3202 (!ge s. ARM_READ_GE (ARM_WRITE_GE_SPSR ge s) = ARM_READ_GE s) /\ 3203 (!m s. ARM_READ_GE (ARM_WRITE_MODE_SPSR m s) = ARM_READ_GE s) /\ 3204 (!f b s. ARM_READ_GE (ARM_WRITE_STATUS_SPSR f b s) = ARM_READ_GE s) /\ 3205 (!n m d s. ARM_MODE (ARM_WRITE_REG_MODE (n,m) d s) = ARM_MODE s) /\ 3206 (!n d s. ARM_MODE (ARM_WRITE_REG n d s) = ARM_MODE s) /\ 3207 (!a d s. ARM_MODE (ARM_WRITE_MEM a d s) = ARM_MODE s) /\ 3208 (!a d s. ARM_MODE (ARM_WRITE_MEM_WRITE a d s) = ARM_MODE s) /\ 3209 (!a s. ARM_MODE (ARM_WRITE_MEM_READ a s) = ARM_MODE s) /\ 3210 (!it s. ARM_MODE (ARM_WRITE_IT it s) = ARM_MODE s) /\ 3211 (!ge s. ARM_MODE (ARM_WRITE_GE ge s) = ARM_MODE s) /\ 3212 (!m s. ARM_MODE (ARM_WRITE_MODE m s) = m) /\ 3213 (!f b s. ARM_MODE (ARM_WRITE_STATUS f b s) = ARM_MODE s) /\ 3214 (!d s. ARM_MODE (ARM_WRITE_SPSR d s) = ARM_MODE s) /\ 3215 (!it s. ARM_MODE (ARM_WRITE_IT_SPSR it s) = ARM_MODE s) /\ 3216 (!ge s. ARM_MODE (ARM_WRITE_GE_SPSR ge s) = ARM_MODE s) /\ 3217 (!m s. ARM_MODE (ARM_WRITE_MODE_SPSR m s) = ARM_MODE s) /\ 3218 (!f b s. ARM_MODE (ARM_WRITE_STATUS_SPSR f b s) = ARM_MODE s)`, 3219 REPEAT STRIP_TAC \\ TRY (Cases_on `f`) 3220 \\ SRW_TAC [] [ARM_MODE_def, ARM_READ_STATUS_def, ARM_READ_IT_def, 3221 ARM_READ_GE_def, PSR_OF_UPDATES] 3222 \\ TRY (Cases_on `f2`) 3223 \\ SIMP_TAC (srw_ss()) [ARM_READ_CPSR_def, ARM_WRITE_CPSR_def, 3224 ARM_READ_SPSR_def, ARM_WRITE_SPSR_def, ARM_WRITE_SPSR_MODE_def, 3225 ARM_WRITE_STATUS_SPSR_def, ARM_WRITE_IT_SPSR_def, 3226 ARM_WRITE_GE_SPSR_def, ARM_WRITE_MODE_SPSR_def, 3227 ARM_WRITE_STATUS_def, ARM_WRITE_IT_def, ARM_WRITE_GE_def, 3228 ARM_WRITE_MODE_def, SPSR_MODE_NOT_CPSR, UPDATE_def] 3229 \\ FULL_SIMP_TAC (srw_ss()) [SPSR_MODE_NOT_CPSR, UPDATE_def, 3230 ARM_READ_SPSR_MODE_def, ARM_WRITE_SPSR_MODE_def]); 3231 3232val SPSR_COMPONENTS_OF_UPDATES = Q.store_thm("SPSR_COMPONENTS_OF_UPDATES", 3233 `(!f n m d s. ARM_READ_STATUS_SPSR f (ARM_WRITE_REG_MODE (n,m) d s) = 3234 ARM_READ_STATUS_SPSR f s) /\ 3235 (!f n d s. ARM_READ_STATUS_SPSR f (ARM_WRITE_REG n d s) = 3236 ARM_READ_STATUS_SPSR f s) /\ 3237 (!f a d s. ARM_READ_STATUS_SPSR f (ARM_WRITE_MEM a d s) = 3238 ARM_READ_STATUS_SPSR f s) /\ 3239 (!f a d s. ARM_READ_STATUS_SPSR f (ARM_WRITE_MEM_WRITE a d s) = 3240 ARM_READ_STATUS_SPSR f s) /\ 3241 (!f a s. ARM_READ_STATUS_SPSR f (ARM_WRITE_MEM_READ a s) = 3242 ARM_READ_STATUS_SPSR f s) /\ 3243 (!f f2 b s. ARM_READ_STATUS_SPSR f (ARM_WRITE_STATUS f2 b s) = 3244 ARM_READ_STATUS_SPSR f s) /\ 3245 (!f ge s. ARM_READ_STATUS_SPSR f (ARM_WRITE_GE ge s) = 3246 ARM_READ_STATUS_SPSR f s) /\ 3247 (!f it s. ARM_READ_STATUS_SPSR f (ARM_WRITE_IT it s) = 3248 ARM_READ_STATUS_SPSR f s) /\ 3249 (!f b s. ARM_READ_STATUS_SPSR f (ARM_WRITE_STATUS_SPSR f b s) = b) /\ 3250 (!f f2 b s. f <> f2 ==> 3251 (ARM_READ_STATUS_SPSR f (ARM_WRITE_STATUS_SPSR f2 b s) = 3252 ARM_READ_STATUS_SPSR f s)) /\ 3253 (!f ge s. ARM_READ_STATUS_SPSR f (ARM_WRITE_GE_SPSR ge s) = 3254 ARM_READ_STATUS_SPSR f s) /\ 3255 (!f it s. ARM_READ_STATUS_SPSR f (ARM_WRITE_IT_SPSR it s) = 3256 ARM_READ_STATUS_SPSR f s) /\ 3257 (!f m s. ARM_READ_STATUS_SPSR f (ARM_WRITE_MODE_SPSR m s) = 3258 ARM_READ_STATUS_SPSR f s) /\ 3259 (!n m d s. ARM_READ_IT_SPSR (ARM_WRITE_REG_MODE (n,m) d s) = 3260 ARM_READ_IT_SPSR s) /\ 3261 (!n d s. ARM_READ_IT_SPSR (ARM_WRITE_REG n d s) = ARM_READ_IT_SPSR s) /\ 3262 (!a d s. ARM_READ_IT_SPSR (ARM_WRITE_MEM a d s) = ARM_READ_IT_SPSR s) /\ 3263 (!a d s. ARM_READ_IT_SPSR (ARM_WRITE_MEM_WRITE a d s) = 3264 ARM_READ_IT_SPSR s) /\ 3265 (!a s. ARM_READ_IT_SPSR (ARM_WRITE_MEM_READ a s) = ARM_READ_IT_SPSR s) /\ 3266 (!f b s. ARM_READ_IT_SPSR (ARM_WRITE_STATUS f b s) = ARM_READ_IT_SPSR s) /\ 3267 (!ge s. ARM_READ_IT_SPSR (ARM_WRITE_GE ge s) = ARM_READ_IT_SPSR s) /\ 3268 (!it s. ARM_READ_IT_SPSR (ARM_WRITE_IT it s) = ARM_READ_IT_SPSR s) /\ 3269 (!f b s. ARM_READ_IT_SPSR (ARM_WRITE_STATUS_SPSR f b s) = 3270 ARM_READ_IT_SPSR s) /\ 3271 (!ge s. ARM_READ_IT_SPSR (ARM_WRITE_GE_SPSR ge s) = ARM_READ_IT_SPSR s) /\ 3272 (!it s. ARM_READ_IT_SPSR (ARM_WRITE_IT_SPSR it s) = it) /\ 3273 (!m s. ARM_READ_IT_SPSR (ARM_WRITE_MODE_SPSR m s) = ARM_READ_IT_SPSR s) /\ 3274 (!n m d s. ARM_READ_GE_SPSR (ARM_WRITE_REG_MODE (n,m) d s) = 3275 ARM_READ_GE_SPSR s) /\ 3276 (!n d s. ARM_READ_GE_SPSR (ARM_WRITE_REG n d s) = ARM_READ_GE_SPSR s) /\ 3277 (!a d s. ARM_READ_GE_SPSR (ARM_WRITE_MEM a d s) = ARM_READ_GE_SPSR s) /\ 3278 (!a d s. ARM_READ_GE_SPSR (ARM_WRITE_MEM_WRITE a d s) = 3279 ARM_READ_GE_SPSR s) /\ 3280 (!a s. ARM_READ_GE_SPSR (ARM_WRITE_MEM_READ a s) = ARM_READ_GE_SPSR s) /\ 3281 (!f b s. ARM_READ_GE_SPSR (ARM_WRITE_STATUS f b s) = ARM_READ_GE_SPSR s) /\ 3282 (!ge s. ARM_READ_GE_SPSR (ARM_WRITE_GE ge s) = ARM_READ_GE_SPSR s) /\ 3283 (!it s. ARM_READ_GE_SPSR (ARM_WRITE_IT it s) = ARM_READ_GE_SPSR s) /\ 3284 (!f b s. ARM_READ_GE_SPSR (ARM_WRITE_STATUS_SPSR f b s) = 3285 ARM_READ_GE_SPSR s) /\ 3286 (!ge s. ARM_READ_GE_SPSR (ARM_WRITE_GE_SPSR ge s) = ge) /\ 3287 (!it s. ARM_READ_GE_SPSR (ARM_WRITE_IT_SPSR it s) = ARM_READ_GE_SPSR s) /\ 3288 (!m s. ARM_READ_GE_SPSR (ARM_WRITE_MODE_SPSR m s) = ARM_READ_GE_SPSR s) /\ 3289 (!n m d s. ARM_READ_MODE_SPSR (ARM_WRITE_REG_MODE (n,m) d s) = 3290 ARM_READ_MODE_SPSR s) /\ 3291 (!n d s. ARM_READ_MODE_SPSR (ARM_WRITE_REG n d s) = ARM_READ_MODE_SPSR s) /\ 3292 (!a d s. ARM_READ_MODE_SPSR (ARM_WRITE_MEM a d s) = ARM_READ_MODE_SPSR s) /\ 3293 (!a d s. ARM_READ_MODE_SPSR (ARM_WRITE_MEM_WRITE a d s) = 3294 ARM_READ_MODE_SPSR s) /\ 3295 (!a s. ARM_READ_MODE_SPSR (ARM_WRITE_MEM_READ a s) = ARM_READ_MODE_SPSR s) /\ 3296 (!f b s. ARM_READ_MODE_SPSR (ARM_WRITE_STATUS f b s) = 3297 ARM_READ_MODE_SPSR s) /\ 3298 (!ge s. ARM_READ_MODE_SPSR (ARM_WRITE_GE ge s) = ARM_READ_MODE_SPSR s) /\ 3299 (!it s. ARM_READ_MODE_SPSR (ARM_WRITE_IT it s) = ARM_READ_MODE_SPSR s) /\ 3300 (!f b s. ARM_READ_MODE_SPSR (ARM_WRITE_STATUS_SPSR f b s) = 3301 ARM_READ_MODE_SPSR s) /\ 3302 (!ge s. ARM_READ_MODE_SPSR (ARM_WRITE_GE_SPSR ge s) = 3303 ARM_READ_MODE_SPSR s) /\ 3304 (!it s. ARM_READ_MODE_SPSR (ARM_WRITE_IT_SPSR it s) = 3305 ARM_READ_MODE_SPSR s) /\ 3306 (!m s. ARM_READ_MODE_SPSR (ARM_WRITE_MODE_SPSR m s) = m)`, 3307 REPEAT STRIP_TAC \\ TRY (Cases_on `f`) 3308 \\ SRW_TAC [] [ARM_READ_SPSR_def, ARM_READ_STATUS_SPSR_def, 3309 ARM_READ_IT_SPSR_def, ARM_READ_GE_SPSR_def, ARM_READ_MODE_SPSR_def, 3310 PSR_OF_UPDATES, ARM_MODE_def] 3311 \\ TRY (Cases_on `f2`) 3312 \\ SIMP_TAC (srw_ss()) [ARM_READ_CPSR_def, ARM_MODE_def, ARM_WRITE_CPSR_def, 3313 ARM_READ_SPSR_def, ARM_WRITE_SPSR_def, ARM_WRITE_SPSR_MODE_def, 3314 ARM_WRITE_STATUS_SPSR_def, ARM_WRITE_IT_SPSR_def, 3315 ARM_WRITE_GE_SPSR_def, ARM_WRITE_MODE_SPSR_def, 3316 ARM_WRITE_STATUS_def, ARM_WRITE_IT_def, ARM_WRITE_GE_def, 3317 ARM_WRITE_MODE_def, SPSR_MODE_NOT_CPSR, UPDATE_def] 3318 \\ FULL_SIMP_TAC (srw_ss()) [SPSR_MODE_NOT_CPSR, UPDATE_def, 3319 ARM_READ_SPSR_MODE_def, ARM_WRITE_SPSR_MODE_def]); 3320 3321val LESS_THM = 3322 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM; 3323 3324val RevLookUpRName = Q.store_thm("RevLookUpRName", 3325 `((RevLookUpRName (n,m) = RName_0usr) = (n = 0w)) /\ 3326 ((RevLookUpRName (n,m) = RName_1usr) = (n = 1w)) /\ 3327 ((RevLookUpRName (n,m) = RName_2usr) = (n = 2w)) /\ 3328 ((RevLookUpRName (n,m) = RName_3usr) = (n = 3w)) /\ 3329 ((RevLookUpRName (n,m) = RName_4usr) = (n = 4w)) /\ 3330 ((RevLookUpRName (n,m) = RName_5usr) = (n = 5w)) /\ 3331 ((RevLookUpRName (n,m) = RName_6usr) = (n = 6w)) /\ 3332 ((RevLookUpRName (n,m) = RName_7usr) = (n = 7w)) /\ 3333 ((RevLookUpRName (n,m) = RName_8usr) = (n = 8w) /\ m <> 17w) /\ 3334 ((RevLookUpRName (n,m) = RName_8fiq) = (n = 8w) /\ (m = 17w)) /\ 3335 ((RevLookUpRName (n,m) = RName_9usr) = (n = 9w) /\ m <> 17w) /\ 3336 ((RevLookUpRName (n,m) = RName_9fiq) = (n = 9w) /\ (m = 17w)) /\ 3337 ((RevLookUpRName (n,m) = RName_10usr) = (n = 10w) /\ m <> 17w) /\ 3338 ((RevLookUpRName (n,m) = RName_10fiq) = (n = 10w) /\ (m = 17w)) /\ 3339 ((RevLookUpRName (n,m) = RName_11usr) = (n = 11w) /\ m <> 17w) /\ 3340 ((RevLookUpRName (n,m) = RName_11fiq) = (n = 11w) /\ (m = 17w)) /\ 3341 ((RevLookUpRName (n,m) = RName_12usr) = (n = 12w) /\ m <> 17w) /\ 3342 ((RevLookUpRName (n,m) = RName_12fiq) = (n = 12w) /\ (m = 17w)) /\ 3343 ((RevLookUpRName (n,m) = RName_SPusr) = (n = 13w) /\ 3344 m NOTIN {17w;18w;19w;22w;23w;27w}) /\ 3345 ((RevLookUpRName (n,m) = RName_SPfiq) = (n = 13w) /\ (m = 17w)) /\ 3346 ((RevLookUpRName (n,m) = RName_SPirq) = (n = 13w) /\ (m = 18w)) /\ 3347 ((RevLookUpRName (n,m) = RName_SPsvc) = (n = 13w) /\ (m = 19w)) /\ 3348 ((RevLookUpRName (n,m) = RName_SPmon) = (n = 13w) /\ (m = 22w)) /\ 3349 ((RevLookUpRName (n,m) = RName_SPabt) = (n = 13w) /\ (m = 23w)) /\ 3350 ((RevLookUpRName (n,m) = RName_SPund) = (n = 13w) /\ (m = 27w)) /\ 3351 ((RevLookUpRName (n,m) = RName_LRusr) = (n = 14w) /\ 3352 m NOTIN {17w;18w;19w;22w;23w;27w}) /\ 3353 ((RevLookUpRName (n,m) = RName_LRfiq) = (n = 14w) /\ (m = 17w)) /\ 3354 ((RevLookUpRName (n,m) = RName_LRirq) = (n = 14w) /\ (m = 18w)) /\ 3355 ((RevLookUpRName (n,m) = RName_LRsvc) = (n = 14w) /\ (m = 19w)) /\ 3356 ((RevLookUpRName (n,m) = RName_LRmon) = (n = 14w) /\ (m = 22w)) /\ 3357 ((RevLookUpRName (n,m) = RName_LRabt) = (n = 14w) /\ (m = 23w)) /\ 3358 ((RevLookUpRName (n,m) = RName_LRund) = (n = 14w) /\ (m = 27w)) /\ 3359 ((RevLookUpRName (n,m) = RName_PC) = (n = 15w))`, 3360 wordsLib.Cases_on_word `n` 3361 \\ RULE_ASSUM_TAC (SIMP_RULE (srw_ss()) [LESS_THM]) 3362 \\ FULL_SIMP_TAC bool_ss [] \\ EVAL_TAC 3363 \\ Cases_on `m = 17w` 3364 \\ ASM_SIMP_TAC bool_ss [] \\ EVAL_TAC 3365 \\ Cases_on `(m = 18w) \/ (m = 19w) \/ (m = 22w) \/ (m = 23w) \/ (m = 27w)` 3366 \\ FULL_SIMP_TAC (srw_ss()) [] \\ EVAL_TAC); 3367 3368val RevLookUpRName_neq = Q.store_thm("RevLookUpRName_neq", 3369 `!n1 n2 m1 m2. 3370 n1 <> n2 ==> RevLookUpRName (n1, m1) <> RevLookUpRName (n2, m2)`, 3371 REPEAT STRIP_TAC 3372 \\ Cases_on `RevLookUpRName (n1, m1)` 3373 \\ Cases_on `RevLookUpRName (n2, m2)` 3374 \\ FULL_SIMP_TAC (srw_ss()) [RevLookUpRName]); 3375 3376val REG_MODE_OF_UPDATES = Q.store_thm("REG_MODE_OF_UPDATES", 3377 `(!n1 n2 m1 m2 d s. n1 <> n2 ==> 3378 (ARM_READ_REG_MODE (n1,m1) (ARM_WRITE_REG_MODE (n2,m2) d s) = 3379 ARM_READ_REG_MODE (n1,m1) s)) /\ 3380 (!n1 n2 m d s. n1 <> n2 ==> 3381 (ARM_READ_REG_MODE (n1,m) (ARM_WRITE_REG n2 d s) = 3382 ARM_READ_REG_MODE (n1,m) s)) /\ 3383 (!n m d s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_REG_MODE (n,m) d s) = d) /\ 3384 (!n m a d s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_MEM a d s) = 3385 ARM_READ_REG_MODE (n,m) s) /\ 3386 (!n m a d s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_MEM_WRITE a d s) = 3387 ARM_READ_REG_MODE (n,m) s) /\ 3388 (!n m a s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_MEM_READ a s) = 3389 ARM_READ_REG_MODE (n,m) s) /\ 3390 (!n m x y s. ARM_READ_REG_MODE (n,m) (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = 3391 ARM_READ_REG_MODE (n,m) s) /\ 3392 (!n m it s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_IT it s) = 3393 ARM_READ_REG_MODE (n,m) s) /\ 3394 (!n m ge s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_GE ge s) = 3395 ARM_READ_REG_MODE (n,m) s) /\ 3396 (!n m1 m2 s. ARM_READ_REG_MODE (n,m1) (ARM_WRITE_MODE m2 s) = 3397 ARM_READ_REG_MODE (n,m1) s) /\ 3398 (!n m f b s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_STATUS f b s) = 3399 ARM_READ_REG_MODE (n,m) s) /\ 3400 (!n m d s. ARM_READ_REG_MODE (n,m) (ARM_WRITE_SPSR d s) = 3401 ARM_READ_REG_MODE (n,m) s)`, 3402 SRW_TAC [] [ARM_WRITE_REG_MODE_def, ARM_WRITE_REG_def, ARM_WRITE_MEM_def, 3403 ARM_WRITE_MEM_WRITE_def, ARM_WRITE_MEM_READ_def, 3404 ARM_WRITE_SPSR_def, ARM_WRITE_IT_def, ARM_WRITE_GE_def, 3405 ARM_WRITE_MODE_def, ARM_WRITE_CPSR_def, ARM_READ_REG_MODE_def, 3406 CLEAR_EXCLUSIVE_BY_ADDRESS_def] 3407 \\ TRY (Cases_on `f`) 3408 \\ SRW_TAC [] [ARM_WRITE_SPSR_MODE_def, ARM_WRITE_STATUS_def, 3409 ARM_WRITE_CPSR_def, UPDATE_def] 3410 \\ METIS_TAC [RevLookUpRName_neq]); 3411 3412val REG_OF_UPDATES = Q.prove( 3413 `(!n1 n2 m d s. n1 <> n2 ==> 3414 (ARM_READ_REG n1 (ARM_WRITE_REG_MODE (n2,m) d s) = ARM_READ_REG n1 s)) /\ 3415 (!n1 n2 d s. n1 <> n2 ==> 3416 (ARM_READ_REG n1 (ARM_WRITE_REG n2 d s) = ARM_READ_REG n1 s)) /\ 3417 (!n d s. ARM_READ_REG n (ARM_WRITE_REG n d s) = d) /\ 3418 (!n a d s. ARM_READ_REG n (ARM_WRITE_MEM a d s) = ARM_READ_REG n s) /\ 3419 (!n a d s. ARM_READ_REG n (ARM_WRITE_MEM_WRITE a d s) = ARM_READ_REG n s) /\ 3420 (!n a s. ARM_READ_REG n (ARM_WRITE_MEM_READ a s) = ARM_READ_REG n s) /\ 3421 (!n x y s. ARM_READ_REG n (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = 3422 ARM_READ_REG n s) /\ 3423 (!n it s. ARM_READ_REG n (ARM_WRITE_IT it s) = ARM_READ_REG n s) /\ 3424 (!n ge s. ARM_READ_REG n (ARM_WRITE_GE ge s) = ARM_READ_REG n s) /\ 3425 (!n m s. ARM_READ_REG n (ARM_WRITE_MODE m s) = ARM_READ_REG_MODE (n,m) s) /\ 3426 (!n f b s. ARM_READ_REG n (ARM_WRITE_STATUS f b s) = ARM_READ_REG n s) /\ 3427 (!n d s. ARM_READ_REG n (ARM_WRITE_SPSR d s) = ARM_READ_REG n s)`, 3428 SRW_TAC [] 3429 [ARM_READ_REG_def, ARM_WRITE_REG_def, REG_MODE_OF_UPDATES, 3430 CPSR_COMPONENTS_OF_UPDATES, ARM_MODE_def, PSR_OF_UPDATES]); 3431 3432val REG_OF_UPDATES = save_thm("REG_OF_UPDATES", 3433 CONJ REG_MODE_OF_UPDATES REG_OF_UPDATES); 3434 3435val MEM_OF_UPDATES = Q.store_thm("MEM_OF_UPDATES", 3436 `(!a n m d s. 3437 ARM_READ_MEM a (ARM_WRITE_REG_MODE (n,m) d s) = ARM_READ_MEM a s) /\ 3438 (!a n d s. ARM_READ_MEM a (ARM_WRITE_REG n d s) = ARM_READ_MEM a s) /\ 3439 (!a d s. ARM_READ_MEM a (ARM_WRITE_MEM a d s) = d) /\ 3440 (!a b x s. ~(a = b) ==> 3441 (ARM_READ_MEM a (ARM_WRITE_MEM b x s) = ARM_READ_MEM a s)) /\ 3442 (!a b d s. ARM_READ_MEM a (ARM_WRITE_MEM_WRITE b d s) = ARM_READ_MEM a s) /\ 3443 (!a b s. ARM_READ_MEM a (ARM_WRITE_MEM_READ b s) = ARM_READ_MEM a s) /\ 3444 (!a x y s. 3445 ARM_READ_MEM a (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = ARM_READ_MEM a s) /\ 3446 (!a it s. ARM_READ_MEM a (ARM_WRITE_IT it s) = ARM_READ_MEM a s) /\ 3447 (!a ge s. ARM_READ_MEM a (ARM_WRITE_GE ge s) = ARM_READ_MEM a s) /\ 3448 (!a m s. ARM_READ_MEM a (ARM_WRITE_MODE m s) = ARM_READ_MEM a s) /\ 3449 (!a f b s. ARM_READ_MEM a (ARM_WRITE_STATUS f b s) = ARM_READ_MEM a s) /\ 3450 (!a d s. ARM_READ_MEM a (ARM_WRITE_SPSR d s) = ARM_READ_MEM a s)`, 3451 SRW_TAC [] [ARM_WRITE_REG_MODE_def, ARM_WRITE_REG_def, ARM_WRITE_MEM_def, 3452 ARM_WRITE_MEM_READ_def, ARM_WRITE_MEM_WRITE_def, 3453 ARM_WRITE_SPSR_def, ARM_WRITE_IT_def, ARM_WRITE_GE_def, 3454 ARM_WRITE_MODE_def, ARM_WRITE_CPSR_def, ARM_READ_MEM_def, 3455 CLEAR_EXCLUSIVE_BY_ADDRESS_def] 3456 \\ TRY (Cases_on `f`) 3457 \\ SRW_TAC [] [ARM_WRITE_SPSR_MODE_def, ARM_WRITE_STATUS_def, 3458 ARM_WRITE_CPSR_def, UPDATE_def]); 3459 3460val MONITORS_OF_UPDATES = Q.store_thm("MONITORS_OF_UPDATES", 3461 `(!n m d s. (ARM_WRITE_REG_MODE (n,m) d s).monitors = s.monitors) /\ 3462 (!n d s. (ARM_WRITE_REG n d s).monitors = s.monitors) /\ 3463 (!a d s. (ARM_WRITE_MEM a d s).monitors = s.monitors) /\ 3464 (!a d s. (ARM_WRITE_MEM_WRITE a d s).monitors = s.monitors) /\ 3465 (!a s. (ARM_WRITE_MEM_READ a s).monitors = s.monitors) /\ 3466 (!it s. (ARM_WRITE_IT it s).monitors = s.monitors) /\ 3467 (!ge s. (ARM_WRITE_GE ge s).monitors = s.monitors) /\ 3468 (!m s. (ARM_WRITE_MODE m s).monitors = s.monitors) /\ 3469 (!f b s. (ARM_WRITE_STATUS f b s).monitors = s.monitors) /\ 3470 (!d s. (ARM_WRITE_SPSR d s).monitors = s.monitors)`, 3471 SRW_TAC [] [ARM_WRITE_REG_MODE_def, ARM_WRITE_REG_def, ARM_WRITE_MEM_def, 3472 ARM_WRITE_MEM_READ_def, ARM_WRITE_MEM_WRITE_def, 3473 ARM_WRITE_SPSR_def, ARM_WRITE_IT_def, ARM_WRITE_GE_def, 3474 ARM_WRITE_MODE_def, ARM_WRITE_CPSR_def] 3475 \\ TRY (Cases_on `f`) 3476 \\ SRW_TAC [] [ARM_WRITE_SPSR_MODE_def, ARM_WRITE_STATUS_def, 3477 ARM_WRITE_CPSR_def, UPDATE_def]); 3478 3479val ARM_READ_CPSR_COMPONENT_UNCHANGED = 3480 Q.store_thm("ARM_READ_CPSR_COMPONENT_UNCHANGED", 3481 `(!b s. (ARM_READ_STATUS psrN s = b) ==> 3482 ((ARM_READ_CPSR s with N := b) = ARM_READ_CPSR s)) /\ 3483 (!b s. (ARM_READ_STATUS psrZ s = b) ==> 3484 ((ARM_READ_CPSR s with Z := b) = ARM_READ_CPSR s)) /\ 3485 (!b s. (ARM_READ_STATUS psrC s = b) ==> 3486 ((ARM_READ_CPSR s with C := b) = ARM_READ_CPSR s)) /\ 3487 (!b s. (ARM_READ_STATUS psrV s = b) ==> 3488 ((ARM_READ_CPSR s with V := b) = ARM_READ_CPSR s)) /\ 3489 (!b s. (ARM_READ_STATUS psrQ s = b) ==> 3490 ((ARM_READ_CPSR s with Q := b) = ARM_READ_CPSR s)) /\ 3491 (!b s. (ARM_READ_STATUS psrJ s = b) ==> 3492 ((ARM_READ_CPSR s with J := b) = ARM_READ_CPSR s)) /\ 3493 (!b s. (ARM_READ_STATUS psrE s = b) ==> 3494 ((ARM_READ_CPSR s with E := b) = ARM_READ_CPSR s)) /\ 3495 (!b s. (ARM_READ_STATUS psrA s = b) ==> 3496 ((ARM_READ_CPSR s with A := b) = ARM_READ_CPSR s)) /\ 3497 (!b s. (ARM_READ_STATUS psrI s = b) ==> 3498 ((ARM_READ_CPSR s with I := b) = ARM_READ_CPSR s)) /\ 3499 (!b s. (ARM_READ_STATUS psrF s = b) ==> 3500 ((ARM_READ_CPSR s with F := b) = ARM_READ_CPSR s)) /\ 3501 (!b s. (ARM_READ_STATUS psrT s = b) ==> 3502 ((ARM_READ_CPSR s with T := b) = ARM_READ_CPSR s)) /\ 3503 (!it s. (ARM_READ_IT s = it) ==> 3504 ((ARM_READ_CPSR s with IT := it) = ARM_READ_CPSR s)) /\ 3505 (!ge s. (ARM_READ_GE s = ge) ==> 3506 ((ARM_READ_CPSR s with GE := ge) = ARM_READ_CPSR s)) /\ 3507 (!m s. (ARM_MODE s = m) ==> 3508 ((ARM_READ_CPSR s with M := m) = ARM_READ_CPSR s))`, 3509 SRW_TAC [] [arm_state_component_equality, ARMpsr_component_equality, 3510 UPDATE_APPLY_IMP_ID, 3511 ARM_MODE_def, ARM_WRITE_MODE_def, 3512 ARM_READ_GE_def, ARM_WRITE_GE_def, 3513 ARM_READ_IT_def, ARM_WRITE_IT_def, 3514 ARM_READ_STATUS_def, ARM_WRITE_STATUS_def, 3515 ARM_READ_CPSR_def, ARM_WRITE_CPSR_def, 3516 ARM_READ_REG_MODE_def, ARM_WRITE_REG_MODE_def, 3517 ARM_READ_REG_def, ARM_WRITE_REG_def, 3518 ARM_READ_MEM_def, ARM_WRITE_MEM_def]); 3519 3520val ARM_READ_UNCHANGED = Q.store_thm("ARM_READ_UNCHANGED", 3521 `(!f b s. (ARM_READ_STATUS f s = b) ==> (ARM_WRITE_STATUS f b s = s)) /\ 3522 (!it s. (ARM_READ_IT s = it) ==> (ARM_WRITE_IT it s = s)) /\ 3523 (!ge s. (ARM_READ_GE s = ge) ==> (ARM_WRITE_GE ge s = s)) /\ 3524 (!m s. (ARM_MODE s = m) ==> (ARM_WRITE_MODE m s = s)) /\ 3525 (!cpsr s. (ARM_READ_CPSR s = cpsr) ==> (ARM_WRITE_CPSR cpsr s = s)) /\ 3526 (!f b s. (ARM_READ_STATUS_SPSR f s = b) ==> 3527 (ARM_WRITE_STATUS_SPSR f b s = s)) /\ 3528 (!it s. (ARM_READ_IT_SPSR s = it) ==> (ARM_WRITE_IT_SPSR it s = s)) /\ 3529 (!ge s. (ARM_READ_GE_SPSR s = ge) ==> (ARM_WRITE_GE_SPSR ge s = s)) /\ 3530 (!m s. (ARM_READ_MODE_SPSR s = m) ==> (ARM_WRITE_MODE_SPSR m s = s)) /\ 3531 (!w s. (ARM_READ_SPSR s = w) ==> (ARM_WRITE_SPSR w s = s)) /\ 3532 (!n w s. (ARM_READ_REG n s = w) ==> (ARM_WRITE_REG n w s = s)) /\ 3533 (!n m w s. (ARM_READ_REG_MODE (n,m) s = w) ==> 3534 (ARM_WRITE_REG_MODE (n,m) w s = s))`, (* /\ 3535 (!a w s. (ARM_READ_MEM a s = w) ==> (ARM_WRITE_MEM a w s = s))`, *) 3536 REPEAT STRIP_TAC \\ TRY (Cases_on `f`) 3537 \\ SRW_TAC [] [arm_state_component_equality, ARMpsr_component_equality, 3538 UPDATE_APPLY_IMP_ID, 3539 ARM_MODE_def, ARM_WRITE_MODE_def, 3540 ARM_READ_MODE_SPSR_def, ARM_WRITE_MODE_SPSR_def, 3541 ARM_READ_GE_def, ARM_WRITE_GE_def, 3542 ARM_READ_GE_SPSR_def, ARM_WRITE_GE_SPSR_def, 3543 ARM_READ_IT_def, ARM_WRITE_IT_def, 3544 ARM_READ_IT_SPSR_def, ARM_WRITE_IT_SPSR_def, 3545 ARM_READ_STATUS_def, ARM_WRITE_STATUS_def, 3546 ARM_READ_STATUS_SPSR_def, ARM_WRITE_STATUS_SPSR_def, 3547 ARM_READ_CPSR_def, ARM_WRITE_CPSR_def, 3548 ARM_READ_SPSR_def, ARM_WRITE_SPSR_def, 3549 ARM_READ_SPSR_MODE_def, ARM_WRITE_SPSR_MODE_def, 3550 ARM_READ_REG_MODE_def, ARM_WRITE_REG_MODE_def, 3551 ARM_READ_REG_def, ARM_WRITE_REG_def, 3552 ARM_READ_MEM_def, ARM_WRITE_MEM_def]); 3553 3554val ARM_READ_STATUS_UPDATES = Q.store_thm("ARM_READ_STATUS_UPDATES", 3555 `(!state state'. 3556 (ARM_READ_STATUS psrN state <=/=> ARM_READ_STATUS psrV state) /\ 3557 (ARM_READ_STATUS psrV state' = ARM_READ_STATUS psrV state) ==> 3558 (ARM_WRITE_STATUS psrV (~ARM_READ_STATUS psrN state) state' = state')) /\ 3559 (!state state'. 3560 ~(ARM_READ_STATUS psrC state /\ ~ARM_READ_STATUS psrZ state) /\ 3561 (ARM_READ_STATUS psrC state' = ARM_READ_STATUS psrC state) ==> 3562 (ARM_WRITE_STATUS psrC 3563 (ARM_READ_STATUS psrZ state /\ 3564 ARM_READ_STATUS psrC state) state' = state'))`, 3565 REPEAT STRIP_TAC 3566 \\ MATCH_MP_TAC (Thm.CONJUNCT1 ARM_READ_UNCHANGED) 3567 \\ METIS_TAC []); 3568 3569(* ------------------------------------------------------------------------- *) 3570 3571val _ = wordsLib.guess_lengths(); 3572 3573val ARM_ALIGN_BX_def = Define` 3574 (ARM_ALIGN_BX ii npass (opc:word32) enc instr) : bool option M = 3575 let align_pc = 3576 seqT (read__reg ii RName_PC) 3577 (\pc. write__reg ii RName_PC 3578 (align(pc,if enc = Encoding_ARM then 4 else 2))) 3579 and write___reg n v = 3580 seqT (read_cpsr ii) 3581 (\cpsr. 3582 seqT (LookUpRName ii (n, cpsr.M)) 3583 (\rname. write__reg ii rname v)) 3584 in 3585 let align_dp opc n mode1 version rn C = 3586 if version >= 7 then (* aligned_bx result *) 3587 if (n = 15w) \/ (opc = 0b1101w) \/ (opc = 0b1111w) then 3588 if opc IN {0b0000w; 0b1110w} then (* AND, BIC *) 3589 align_pc 3590 else 3591 (case mode1 3592 of Mode1_register imm5 type m => 3593 (if (m = 15w) /\ (type = 0b00w) /\ (imm5 = 0w) then 3594 align_pc 3595 else 3596 if m = 15w then 3597 address_mode1 ii F mode1 >>= 3598 (\(shifted,C_shift). 3599 let result = FST (data_processing_alu opc rn shifted C) in 3600 read__reg ii RName_PC >>= 3601 (\pc. 3602 write__reg ii RName_PC 3603 (if aligned(pc,4) /\ aligned_bx result 3604 then pc else -8w))) 3605 else 3606 align_pc >>= 3607 (\u:unit. 3608 ((if opc IN {0b1101w; 0b1111w} then 3609 constT 0w 3610 else 3611 read_reg ii n) ||| read_reg ii m ||| 3612 address_mode1 ii F mode1) >>= 3613 (\(rn,rm,(shifted,C_shift)). 3614 let result = FST (data_processing_alu opc rn shifted C) 3615 in 3616 write___reg m (if aligned_bx result then rm else 0w)))) 3617 | _ => align_pc) 3618 else 3619 align_pc >>= 3620 (\u:unit. 3621 address_mode1 ii F mode1 >>= 3622 (\(shifted,C_shift). 3623 let result = FST (data_processing_alu opc rn shifted C) in 3624 let align_rn = 3625 write___reg n 3626 (if aligned_bx result then 3627 rn 3628 else if opc IN {0b0000w; 0b1110w} then (* AND, BIC *) 3629 0w 3630 else if opc = 0b1100w then (* ORR *) 3631 1w 3632 else if opc = 0b0001w then (* EOR *) 3633 shifted 3634 else 3635 rn ?? 1w) 3636 in 3637 let align_shift_reg m = 3638 if n = m then 3639 write___reg n (if aligned_bx result then rn else 0w) 3640 else 3641 align_rn 3642 in 3643 (case mode1 3644 of Mode1_immediate _ => align_rn 3645 | Mode1_register _ _ m => align_shift_reg m 3646 | Mode1_register_shifted_register _ _ m => constT ()))) 3647 else (* version < 6, aligned (result,4) *) 3648 if (n = 15w) \/ (opc = 0b1101w) \/ (opc = 0b1111w) then 3649 (case mode1 3650 of Mode1_register imm5 type m => 3651 (if opc IN {0b0000w; 0b1110w} then (* AND, BIC *) 3652 align_pc 3653 else if m = 15w then 3654 if (type = 0b00w) /\ (imm5 = 0w) then 3655 align_pc 3656 else 3657 address_mode1 ii F mode1 >>= 3658 (\(shifted,C_shift). 3659 let result = FST (data_processing_alu opc rn shifted C) in 3660 read__reg ii RName_PC >>= 3661 (\pc. 3662 write__reg ii RName_PC 3663 (if aligned(pc,4) /\ aligned(result,4) then 3664 pc 3665 else 3666 -8w))) 3667 else 3668 align_pc >>= 3669 (\u:unit. 3670 ((if opc IN {0b1101w; 0b1111w} then 3671 constT 0w 3672 else 3673 read_reg ii n) ||| 3674 read_reg ii m ||| address_mode1 ii F mode1) >>= 3675 (\(rn,rm,(shifted,C_shift)). 3676 let result = FST (data_processing_alu opc rn shifted C) in 3677 write___reg m 3678 (if aligned(result,4) then rm else 3679 case opc 3680 of 0b0101w => if C then -1w else 0w 3681 | 0b0110w => if C then 0w else -1w 3682 | 0b0111w => if C then 0w else 1w 3683 | 0b1111w => -1w 3684 | _ => 0w)))) 3685 | _ => align_pc) 3686 else 3687 align_pc >>= 3688 (\u:unit. 3689 address_mode1 ii F mode1 >>= 3690 (\(shifted,C_shift). 3691 let result = FST (data_processing_alu opc rn shifted C) in 3692 (case mode1 3693 of Mode1_immediate _ => 3694 write___reg n 3695 (case opc 3696 of 0b0000w => (* AND *) 3697 (if aligned(result,4) then rn else 0w) 3698 | 0b1110w => (* BIC *) 3699 (if aligned(result,4) then rn else 0w) 3700 | 0b0001w => (* EOR *) 3701 (if aligned(result,4) then rn else shifted) 3702 | 0b1100w => (* ORR *) 3703 (align(rn,4)) (* possibly no solution *) 3704 | 0b0010w => (* SUB *) 3705 (align(result,4) + shifted) 3706 | 0b0011w => (* RSB *) 3707 (shifted - align(result,4)) 3708 | 0b0100w => (* ADD *) 3709 (align(result,4) - shifted) 3710 | 0b0101w => (* ADC *) 3711 (align(result,4) - shifted - if C then 1w else 0w) 3712 | 0b0110w => (* SBC *) 3713 (align(result,4) + shifted + if C then 0w else 1w) 3714 | _ => (* RSC *) 3715 (shifted + (if C then 0w else -1w) - 3716 align(result,4))) 3717 | Mode1_register imm5 type m => 3718 if n = m then 3719 if opc IN {0b0101w; 0b0110w; 0b0111w} then 3720 constT () (* no solution *) 3721 else 3722 write___reg n (if aligned(result,4) then rn else 0w) 3723 else if opc = 0b1100w then (* ORR *) 3724 write___reg n (if aligned(result,4) then rn else 0w) >>= 3725 (\u:unit. 3726 if m = 15w then 3727 read__reg ii RName_PC >>= 3728 (\pc. 3729 write__reg ii RName_PC 3730 (if (type = 0b00w) /\ (imm5 = 0w) \/ 3731 aligned(result,4) 3732 then pc else -8w)) 3733 else 3734 (read_reg ii m >>= 3735 (\rm. 3736 write___reg m 3737 (if aligned(result,4) then rm else 0w)))) 3738 else 3739 write___reg n 3740 (case opc 3741 of 0b0000w => (* AND *) 3742 (if aligned(result,4) then rn else 0w) 3743 | 0b1110w => (* BIC *) 3744 (if aligned(result,4) then rn else 0w) 3745 | 0b0001w => (* EOR *) 3746 (if aligned(result,4) then rn else shifted) 3747 | 0b0010w => (* SUB *) 3748 (align(result,4) + shifted) 3749 | 0b0011w => (* RSB *) 3750 (shifted - align(result,4)) 3751 | 0b0100w => (* ADD *) 3752 (align(result,4) - shifted) 3753 | 0b0101w => (* ADC *) 3754 (align(result,4) - shifted - if C then 1w else 0w) 3755 | 0b0110w => (* SBC *) 3756 (align(result,4) + shifted + if C then 0w else 1w) 3757 | _ => (* RSC *) 3758 (shifted + (if C then 0w else -1w) - 3759 align(result,4))) 3760 | Mode1_register_shifted_register _ _ m => constT ()))) 3761 and align_br m = 3762 align_pc >>= 3763 (\u:unit. 3764 condT (m <> 15w) 3765 (read_reg ii m >>= 3766 (\rm. write___reg m (if aligned_bx rm then rm else 0w))) >>= 3767 (\u:unit. constT NONE)) 3768 and good_spsr_mode = 3769 (read_cpsr ii ||| read_spsr ii) >>= 3770 (\(cpsr,spsr). 3771 write_spsr ii 3772 (if GOOD_MODE spsr.M /\ (spsr.IT = 0w) then spsr 3773 else spsr with <| M := 16w; IT := 0w |>)) 3774 in 3775 if npass then align_pc >>= (\u:unit. constT NONE) else 3776 case instr 3777 of Branch (Branch_Exchange m) => (* bx_write *) 3778 align_br m 3779 | Branch (Branch_Link_Exchange_Register m) => (* bx_write *) 3780 align_br m 3781 | DataProcessing (Add_Sub add n d imm12) => 3782 (* alu_write *) 3783 align_pc >>= 3784 (\u:unit. 3785 if (enc = Encoding_ARM) /\ (d = 15w) /\ n <> 15w then 3786 arch_version ii >>= 3787 (\version. 3788 condT (version <> 6) 3789 ((read_reg ii n ||| arm_expand_imm ii imm12) >>= 3790 (\(rn,imm32). 3791 let result = if add then rn + imm32 else rn - imm32 3792 in 3793 write___reg n 3794 (if version >= 7 then 3795 if aligned_bx result then rn else rn ?? 1w 3796 else (* version < 6 *) 3797 align(result, 4) - (result - rn)))) >>= 3798 (\u:unit. constT NONE)) 3799 else if (enc = Encoding_Thumb2) /\ (d = 13w) /\ n <> 15w then 3800 (read_reg ii n ||| arm_expand_imm ii imm12) >>= 3801 (\(rn,imm32). 3802 let result = if add then rn + imm32 else rn - imm32 3803 in 3804 write___reg n (align(result, 4) - (result - rn)) >>= 3805 (\u:unit. constT NONE)) 3806 else 3807 constT NONE) 3808 | DataProcessing (Data_Processing opc setflags n d mode1) => 3809 (* alu_write or branch_write *) 3810 condT (setflags /\ (d = 15w) /\ 3811 ((enc = Encoding_ARM) \/ 3812 (enc = Encoding_Thumb2) /\ (n = 14w) /\ (opc = 0b0010w))) 3813 good_spsr_mode >>= 3814 (\u:unit. 3815 (if (enc = Encoding_ARM) /\ (d = 15w) /\ ((3 -- 2 ) opc) <> 2w 3816 then 3817 arch_version ii >>= 3818 (\version. 3819 (if (version = 6) \/ (version >= 7) /\ setflags then 3820 align_pc 3821 else 3822 ((if opc IN {0b1101w; 0b1111w} then 3823 constT 0w 3824 else 3825 read_reg ii n) ||| read_flags ii) >>= 3826 (\(rn,(N,Z,C,V)). 3827 align_dp opc n mode1 version rn C)) >>= 3828 (\u:unit. constT NONE)) 3829 else if enc <> Encoding_ARM /\ (d = 13w) /\ 3830 opc IN {0b0010w; 0b0100w; 0b1101w} 3831 then 3832 (read_reg ii n ||| read_flags ii) >>= 3833 (\(rn,(N,Z,C,V)). 3834 align_dp opc n mode1 4 rn C >>= (\u:unit. constT NONE)) 3835 else 3836 align_pc >>= (\u:unit. constT NONE))) 3837 | DataProcessing (Divide _ _ _ m) => 3838 align_pc >>= 3839 (\u:unit. 3840 condT (m <> 15w) 3841 (read_reg ii m >>= 3842 (\rm. write___reg m (if rm <> 0w then rm else 1w))) >>= 3843 (\u:unit. constT NONE)) 3844 | LoadStore (Load indx add load_byte _ _ n t mode2) => (* load_write *) 3845 align_pc >>= 3846 (\u:unit. 3847 if ~load_byte /\ (t = 15w) then 3848 if n = 15w then 3849 (case mode2 of 3850 Mode2_register 2w 0w m => 3851 ((read_reg ii m >>= 3852 (\rm. 3853 write___reg m 3854 (if rm << 2 <> 0xFFFFFFF8w then rm else 0w))) >>= 3855 (\u:unit. constT (SOME T))) 3856 | _ => constT (SOME T)) 3857 else 3858 arch_version ii >>= 3859 (\version. 3860 condT (if version >= 5 then 3861 ~aligned_bx opc \/ 3862 (enc = Encoding_Thumb2) /\ 3863 ~aligned_bx ((23 >< 16) opc) 3864 else 3865 ~aligned (opc,4)) 3866 ((read__reg ii RName_PC ||| read_reg ii n) >>= 3867 (\(pc,rn). 3868 address_mode2 ii indx add rn mode2 >>= 3869 (\(offset_addr,address). 3870 write___reg n 3871 (if pc <> align (address,4) /\ 3872 (enc <> Encoding_Thumb2 \/ 3873 pc + 2w <> align (address,4)) 3874 then rn else rn + 4w)))) >>= 3875 (\u:unit. constT (SOME T))) 3876 else 3877 constT NONE) 3878 | LoadStore (Load_Multiple indx add system _ n registers) => 3879 (* load_write *) 3880 align_pc >>= 3881 (\u:unit. 3882 if n <> 15w /\ registers ' 15 then 3883 (condT system good_spsr_mode ||| arch_version ii) >>= 3884 (\(u:unit,version). 3885 condT ((if version >= 5 then 3886 ~aligned_bx opc \/ 3887 (enc = Encoding_Thumb2) /\ 3888 ~aligned_bx ((23 >< 16) opc) 3889 else 3890 ~aligned (opc,4))) 3891 ((read__reg ii RName_PC ||| read_reg ii n) >>= 3892 (\(pc,rn). 3893 let count = n2w (4 * bit_count registers) in 3894 let address = if add then rn else rn - count in 3895 let address = if indx = add then address + 4w 3896 else address in 3897 let address = address + (count - 4w) 3898 in 3899 write___reg n 3900 (if pc <> align (address,4) /\ 3901 (enc <> Encoding_Thumb2 \/ 3902 pc + 2w <> align (address,4)) 3903 then rn else rn + 4w))) >>= 3904 (\u:unit. constT (SOME T))) 3905 else 3906 constT NONE) 3907 | LoadStore (Return_From_Exception P inc _ n) => 3908 align_pc >>= 3909 (\u:unit. 3910 (read__reg ii RName_PC ||| read_reg ii n) >>= 3911 (\(pc,rn). 3912 let address = if inc then rn else rn - 8w in 3913 let address = if P = inc then address + 4w else address in 3914 let address = address + 4w 3915 in 3916 write___reg n 3917 (if pc <> align (address,4) /\ 3918 (enc <> Encoding_Thumb2 \/ 3919 pc + 2w <> align (address,4)) 3920 then rn else rn + 4w) >>= 3921 (\u:unit. constT (SOME F)))) 3922 | StatusAccess (Register_to_Status _ mask n) => 3923 (align_pc ||| current_mode_is_priviledged ii) >>= 3924 (\(u:unit,priviledged). 3925 condT (mask ' 0 /\ priviledged /\ n <> 15w) 3926 (read_reg ii n >>= 3927 (\rn. 3928 write___reg n 3929 (if GOOD_MODE ((4 >< 0) rn) then rn else rn || 31w))) >>= 3930 (\u:unit. constT NONE)) 3931 | _ => align_pc >>= (\u:unit. constT NONE)`; 3932 3933(* ------------------------------------------------------------------------- *) 3934 3935val ARM_MEMORY_FOOTPRINT_def = Define` 3936 ARM_MEMORY_FOOTPRINT ii npass inst = 3937 let lookup_rname n = 3938 if n = 15w then 3939 constT RName_PC 3940 else 3941 read_cpsr ii >>= (\cpsr. LookUpRName ii (n,cpsr.M)) 3942 in 3943 let write_address (r,a) = 3944 lookup_rname r >>= 3945 (\name. condT (name <> RName_PC) (write__reg ii name a)) 3946 in 3947 let reg_align (r,a,n,rn) = write_address (r,align(rn + a,n) - a) 3948 and con_align (r,a,n,rn) = write_address (r,if aligned(a,n) then rn else 0w) 3949 in 3950 let align_mode2 (load,indx,add,byte,n,mode2) = 3951 (if load /\ is_mode2_immediate mode2 then 3952 read_reg_literal ii n 3953 else 3954 read_reg ii n) >>= 3955 (\rn. 3956 address_mode2 ii indx add rn mode2 >>= 3957 (\(offset_addr,address). 3958 if byte then 3959 constT NONE 3960 else 3961 case mode2 3962 of Mode2_register _ _ m => 3963 if n = 15w then 3964 read_reg ii m >>= 3965 (\rm. 3966 con_align (m, address, 4, rm) >>= 3967 (\u. 3968 address_mode2 ii indx add rn mode2 >>= 3969 (\(offset_addr,address). 3970 constT (SOME (align (address,4)))))) 3971 else if n = m then 3972 con_align (n, address, 4, rn) >>= 3973 (\u. 3974 read_reg ii n >>= 3975 (\rn. 3976 address_mode2 ii indx add rn mode2 >>= 3977 (\(offset_addr,address). 3978 constT (SOME (align (address,4)))))) 3979 else 3980 reg_align (n, address - rn, 4, rn) >>= 3981 (\u:unit. constT (SOME (align (address,4)))) 3982 | _ => 3983 reg_align (n, address - rn, 4, rn) >>= 3984 (\u:unit. constT (SOME (align (address,4)))))) 3985 and align_mode3 (load,indx,add,N,B,n,mode3) = 3986 (if load /\ is_mode3_immediate mode3 then 3987 read_reg_literal ii n 3988 else 3989 read_reg ii n) >>= 3990 (\rn. 3991 address_mode3 ii indx add rn mode3 >>= 3992 (\(offset_addr,address). 3993 if N = 1 then 3994 constT NONE 3995 else 3996 case mode3 3997 of Mode3_register _ m => 3998 if n = 15w then 3999 read_reg ii m >>= 4000 (\rm. 4001 con_align (m, address, N, rm) >>= 4002 (\u. 4003 address_mode3 ii indx add rn mode3 >>= 4004 (\(offset_addr,address). constT NONE))) 4005 else if n = m then 4006 con_align (n, address, N, rn) >>= 4007 (\u. 4008 read_reg ii n >>= 4009 (\rn. 4010 address_mode3 ii indx add rn mode3 >>= 4011 (\(offset_addr,address). constT NONE))) 4012 else 4013 reg_align (n, address - rn, N, rn) >>= 4014 (\u:unit. constT NONE) 4015 | _ => 4016 reg_align (n, address - rn, N, rn) >>= 4017 (\u:unit. constT NONE))) 4018 in 4019 if npass then constT NONE else 4020 case inst 4021 of Branch (Table_Branch_Byte n is_tbh m) => 4022 (read_reg ii n ||| read_reg ii m) >>= 4023 (\(rn,rm). 4024 condT is_tbh (reg_align (n,LSL(rm,1),2,rn)) >>= 4025 (\u:unit. constT NONE)) 4026 | Miscellaneous (Swap swap_byte n _ _) => 4027 read_reg ii n >>= 4028 (\rn. 4029 condT (~swap_byte) (reg_align (n,0w,4,rn)) >>= 4030 (\u:unit. constT NONE)) 4031 | LoadStore (Return_From_Exception P inc _ n) => 4032 read_reg ii n >>= 4033 (\rn. 4034 let address = if inc then rn else rn - 8w in 4035 let address = if P = inc then address + 4w else address 4036 in 4037 reg_align (n, address - rn, 4, rn) >>= 4038 (\u:unit. constT (SOME (align (address,4) + 4w)))) 4039 | LoadStore (Store_Return_State P inc _ mode) => 4040 read_reg_mode ii (13w,mode) >>= 4041 (\rn. 4042 let address = if inc then rn else rn - 8w in 4043 let address = if P = inc then address + 4w else address 4044 in 4045 write_reg_mode ii (13w,mode) 4046 (align (address, 4) - (address - rn)) >>= 4047 (\u:unit. constT NONE)) 4048 | LoadStore (Load indx add load_byte _ _ n _ mode2) => 4049 align_mode2 (T,indx,add,load_byte,n,mode2) 4050 | LoadStore (Load_Halfword indx add _ _ load_half _ n _ mode3) => 4051 align_mode3 (T,indx,add,if load_half then 2 else 1,2,n,mode3) 4052 | LoadStore (Load_Dual indx add _ n _ _ mode3) => 4053 align_mode3 (T,indx,add,4,8,n,mode3) 4054 | LoadStore (Load_Multiple indx add _ _ n registers) => 4055 read_reg ii n >>= 4056 (\rn. 4057 let count = 4 * bit_count registers in 4058 let base_address = if add then rn else rn - n2w count in 4059 let start_address = if indx = add then base_address + 4w 4060 else base_address 4061 in 4062 reg_align (n, start_address - rn, 4, rn) >>= 4063 (\u:unit. 4064 constT (SOME (align (start_address,4) + n2w (count - 4))))) 4065 | LoadStore (Load_Exclusive n _ imm8) => 4066 read_reg ii n >>= 4067 (\rn. reg_align (n, (w2w imm8) << 2, 4, rn) >>= (\u:unit. constT NONE)) 4068 | LoadStore (Load_Exclusive_Doubleword n _ _) => 4069 read_reg ii n >>= 4070 (\rn. reg_align (n,0w,8,rn) >>= (\u:unit. constT NONE)) 4071 | LoadStore (Load_Exclusive_Halfword n _) => 4072 read_reg ii n >>= 4073 (\rn. reg_align (n,0w,2,rn) >>= (\u:unit. constT NONE)) 4074 | LoadStore (Load_Exclusive_Byte n _) => 4075 read_reg ii n >>= (\rn. constT NONE) 4076 | LoadStore (Store indx add store_byte _ _ n _ mode2) => 4077 align_mode2 (F,indx,add,store_byte,n,mode2) 4078 | LoadStore (Store_Halfword indx add _ _ n _ mode3) => 4079 align_mode3 (F,indx,add,2,2,n,mode3) 4080 | LoadStore (Store_Dual indx add _ n _ _ mode3) => 4081 align_mode3 (F,indx,add,4,8,n,mode3) 4082 | LoadStore (Store_Multiple indx add _ _ n registers) => 4083 read_reg ii n >>= 4084 (\rn. 4085 let count = 4 * bit_count registers in 4086 let base_address = if add then rn else rn - n2w count in 4087 let start_address = if indx = add then base_address + 4w 4088 else base_address 4089 in 4090 reg_align (n, start_address - rn, 4, rn) >>= 4091 (\u:unit. constT NONE)) 4092 | LoadStore (Store_Exclusive n _ _ imm8) => 4093 read_reg ii n >>= 4094 (\rn. 4095 reg_align (n, (w2w imm8) << 2, 4, rn) >>= 4096 (\u:unit. constT NONE)) 4097 | LoadStore (Store_Exclusive_Doubleword n _ _ _) => 4098 read_reg ii n >>= 4099 (\rn. reg_align (n,0w,8,rn) >>= (\u:unit. constT NONE)) 4100 | LoadStore (Store_Exclusive_Halfword n _ _) => 4101 read_reg ii n >>= 4102 (\rn. reg_align (n,0w,2,rn) >>= (\u:unit. constT NONE)) 4103 | LoadStore (Store_Exclusive_Byte n _ _) => 4104 read_reg ii n >>= (\rn. constT NONE) 4105 | _ => constT NONE`; 4106 4107(* ------------------------------------------------------------------------- *) 4108 4109val arm_next_thm = Q.store_thm("arm_next_thm", 4110 `!s x P h g inp. 4111 (!s. P s ==> (g s = s)) /\ 4112 (P s ==> (h (g s) = x)) /\ 4113 (arm_next <| proc := 0 |> inp (g s) = ValueState () x) ==> 4114 (P s ==> (ARM_NEXT inp s = SOME (h s)))`, 4115 SRW_TAC [] [STATE_OPTION_def,ARM_NEXT_def] 4116 \\ `g s = s` by RES_TAC \\ POP_ASSUM SUBST_ALL_TAC 4117 \\ Cases_on `arm_next <|proc := 0|> inp s` 4118 \\ FULL_SIMP_TAC (srw_ss()) []); 4119 4120val arm_next_thm2 = Q.store_thm("arm_next_thm2", 4121 `!s c x1 x2 P h1 h2 g inp. 4122 (!s. P s ==> (g s = s)) /\ 4123 (P s ==> (h1 (g s) = x1)) /\ 4124 (P s ==> (h2 (g s) = x2)) /\ 4125 (arm_next <| proc := 0 |> inp (g s) = 4126 if c then ValueState () x1 else ValueState () x2) ==> 4127 (P s ==> (ARM_NEXT inp s = SOME (if c then h1 s else h2 s)))`, 4128 SRW_TAC [] [STATE_OPTION_def,ARM_NEXT_def] 4129 \\ `g s = s` by RES_TAC \\ POP_ASSUM SUBST_ALL_TAC 4130 \\ Cases_on `arm_next <|proc := 0|> inp s` 4131 \\ FULL_SIMP_TAC (srw_ss()) []);*) 4132 4133(* ------------------------------------------------------------------------- *) 4134 4135val _ = export_theory (); 4136