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