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