1 2open HolKernel Parse boolLib bossLib BasicProvers; 3 4val _ = new_theory "GraphLang"; 5val _ = ParseExtras.temp_loose_equality() 6 7open wordsTheory wordsLib pairTheory listTheory relationTheory; 8open pred_setTheory arithmeticTheory combinTheory; 9open arm_decompTheory set_sepTheory progTheory addressTheory; 10open m0_decompTheory riscv_progTheory; 11open arm_decompLib m0_decompLib; 12 13val op by = BasicProvers.byA 14 15val RW1 = ONCE_REWRITE_RULE; 16val RW = REWRITE_RULE; 17 18val _ = Datatype `variable = 19 VarNone 20 | VarNat num 21 | VarWord8 word8 22 | VarWord ('a word) 23 | VarMem ('a word -> word8) 24 | VarDom ('a word set) 25 | VarBool bool`; 26 27(* States are a mapping from names to the variable type, which is 28 a union of the available names. *) 29 30val _ = type_abbrev("state",``:string -> 'a variable``); 31 32(* Accessors for grabbing variables by name and expected type. *) 33 34val var_acc_def = zDefine ` 35 var_acc nm (f:'a state) = f nm`; 36 37val var_nat_def = zDefine ` 38 var_nat nm st = case var_acc nm st of VarNat n => n | _ => 0`; 39 40val var_word8_def = zDefine ` 41 var_word8 nm st = case var_acc nm st of VarWord8 w => w | _ => 0w`; 42 43val var_word_def = zDefine ` 44 var_word nm st = case var_acc nm st of VarWord w => w | _ => 0w`; 45 46val var_mem_def = zDefine ` 47 var_mem nm st = case var_acc nm st of VarMem m => m | _ => (\x. 0w)`; 48 49val var_dom_def = zDefine ` 50 var_dom nm st = case var_acc nm st of VarDom d => d | _ => {}`; 51 52val var_bool_def = zDefine ` 53 var_bool nm st = case var_acc nm st of VarBool b => b | _ => F`; 54 55(* The variable updator. *) 56 57val var_upd_def = zDefine ` 58 var_upd nm v f = ((nm =+ v) f)`; 59 60val _ = zDefine ` 61 default_state = (\x. VarNone)`; 62 63(* The type of nodes. *) 64 65val _ = Datatype `next_node = NextNode num | Ret | Err`; 66 67val _ = Datatype `node = 68 Basic next_node ((string # ('a state -> 'a variable)) list) 69 | Cond next_node next_node ('a state -> bool) 70 | Call next_node string (('a state -> 'a variable) list) (string list)`; 71 72val _ = zDefine ` 73 Skip nn = Cond nn nn (\x. T)`; 74 75(* The type for a total graph function, including list of inputs, list 76 of outputs, graph, and entry point. *) 77 78val _ = Datatype `graph_function = 79 GraphFunction (string list) (string list) (num -> 'a node option) num`; 80 81(* The definition of execution of a single node. *) 82 83val fold_def = zDefine ` 84 (fold f [] s = s) /\ 85 (fold f (x::xs) s = fold f xs (f x s))`; 86 87val save_vals_def = zDefine ` 88 save_vals vars vals st = 89 fold (\(var, val). var_upd var val) (ZIP (vars,vals)) st`; 90 91val init_vars_def = zDefine ` 92 init_vars vars accs st = 93 save_vals vars (MAP (\i. i st) accs) default_state`; 94 95val return_vars_def = zDefine ` 96 return_vars inner outer inner_st = 97 save_vals outer (MAP (\v. var_acc v inner_st) inner)`; 98 99val upd_vars_def = zDefine ` 100 upd_vars upds st = 101 save_vals (MAP FST upds) (MAP (\(nm, vf). vf st) upds) st`; 102 103val _ = type_abbrev("stack",``:(next_node # 'a state # string) list``); 104 105val upd_stack_def = zDefine ` 106 (upd_stack nn stf (x :: xs) = (nn, stf (FST (SND x)), SND (SND x)) :: xs) /\ 107 (upd_stack nn stf [] = []:'a stack)`; 108 109val exec_node_def = zDefine ` 110 (exec_node Gamma st (Basic cont upds) stack = 111 {upd_stack cont (K (upd_vars upds st)) stack}) /\ 112 (exec_node Gamma st (Cond left right cond) stack = 113 {upd_stack (if cond st then left else right) I stack}) /\ 114 (exec_node Gamma st (Call cont fname inputs outputs) stack = 115 case Gamma fname of NONE => {upd_stack Err I stack} 116 | SOME (GraphFunction inps outps graph1 ep) => 117 {(NextNode ep, init_vars inps inputs st, fname) :: stack})`; 118 119val exec_node_return_def = zDefine ` 120 (exec_node_return _ _ (Basic _ _) stack = {}) /\ 121 (exec_node_return _ _ (Cond _ _ _) stack = {}) /\ 122 (exec_node_return Gamma st (Call cont fname inputs outputs) stack = 123 case Gamma fname of NONE => {} 124 | SOME (GraphFunction inps outps graph ep) => 125 {upd_stack cont (return_vars outps outputs st) stack})`; 126 127(* The single-step relation on graph states. *) 128 129val exec_graph_step_def = zDefine ` 130 exec_graph_step Gamma stack stack' = 131 case stack of 132 (NextNode nn, st, fname) :: _ => 133 (case Gamma fname of | NONE => F 134 | SOME (GraphFunction _ _ graph _) => 135 (case graph nn of NONE => (stack' = upd_stack Err I stack) 136 | SOME node => stack' IN exec_node Gamma st node stack)) 137 | (Ret, st, _) :: (NextNode nn, _, fname) :: _ => 138 (case Gamma fname of | NONE => F 139 | SOME (GraphFunction _ _ graph _) => 140 (case graph nn of NONE => (stack' = upd_stack Err I stack) 141 | SOME node => stack' IN exec_node_return Gamma st node (TL stack))) 142 | [] => F 143 | [_] => F 144 | _ => stack' = upd_stack Err I (TL stack)` 145 146(* Multi-step relations. *) 147 148val _ = zDefine ` 149 exec_graph Gamma = RTC (exec_graph_step Gamma)`; 150 151val exec_graph_n_def = zDefine ` 152 exec_graph_n Gamma n = NRC (exec_graph_step Gamma) n`; 153 154 155(* more abstract representation of graph *) 156 157val _ = type_abbrev("update",``:(string # ('a state -> 'a variable)) list``) 158val _ = type_abbrev("assert",``:'a state->bool``) 159 160val _ = Datatype ` 161 jump = Jump ('a word) | Return` 162 163val _ = Datatype ` 164 next = IF ('a assert) next next (* if ... then ... else ... *) 165 | ASM ('a assert option) ('a update) ('a jump) 166 | CALL ('a assert option) ('a update) string ('a jump)`; 167 168val _ = Datatype ` 169 inst = Inst ('a word) ('a assert) ('a next) (* name, inv, what happens *)` 170 171val _ = Datatype ` 172 func = Func string ('a word) ('a inst list) (* name, entry point, insts *)`; 173 174(* execution *) 175 176val get_assert_def = Define ` 177 (get_assert NONE = \x.T) /\ 178 (get_assert (SOME a) = a)`; 179 180val apply_update_def = Define ` 181 (apply_update [] s = s) /\ 182 (apply_update ((x,y)::xs) s = (x =+ y s) (apply_update xs s))`; 183 184val check_jump_def = Define ` 185 (check_jump (Jump p) s w = (w = p)) /\ 186 (check_jump Return s w = (var_word "ret" s = w))`; 187 188val check_ret_def = Define ` 189 (check_ret (Jump p) s t = (var_word "ret" t = p)) /\ 190 (check_ret Return s t = (var_word "ret" t = var_word "ret" s))`; 191 192val exec_next_def = Define ` 193 (exec_next locs (IF guard n1 n2) s t w call = 194 if guard s then exec_next locs n1 s t w call 195 else exec_next locs n2 s t w call) /\ 196 (exec_next locs (ASM assert update jmp) s t w call = 197 get_assert assert s /\ 198 (apply_update update s = t) /\ 199 check_jump jmp t w /\ (call = NONE)) /\ 200 (exec_next locs (CALL assert update name jmp) s t w call = 201 get_assert assert s /\ 202 (apply_update update s = t) /\ 203 locs name <> NONE /\ 204 check_jump (Jump (THE (locs name))) t w /\ 205 check_ret jmp s t /\ (call = SOME name))` 206 207(* representation in ARM SPEC *) 208 209val arm_STATE_CPSR_def = Define ` 210 arm_STATE_CPSR s = 211 arm_CPSR_N (var_bool "n" s) * 212 arm_CPSR_Z (var_bool "z" s) * 213 arm_CPSR_C (var_bool "c" s) * 214 arm_CPSR_V (var_bool "v" s)`; 215 216val arm_STATE_REGS_def = Define ` 217 arm_STATE_REGS s = 218 arm_REG (R_mode (w2w (var_word8 "mode" s)) 0w) (var_word "r0" s) * 219 arm_REG (R_mode (w2w (var_word8 "mode" s)) 1w) (var_word "r1" s) * 220 arm_REG (R_mode (w2w (var_word8 "mode" s)) 2w) (var_word "r2" s) * 221 arm_REG (R_mode (w2w (var_word8 "mode" s)) 3w) (var_word "r3" s) * 222 arm_REG (R_mode (w2w (var_word8 "mode" s)) 4w) (var_word "r4" s) * 223 arm_REG (R_mode (w2w (var_word8 "mode" s)) 5w) (var_word "r5" s) * 224 arm_REG (R_mode (w2w (var_word8 "mode" s)) 6w) (var_word "r6" s) * 225 arm_REG (R_mode (w2w (var_word8 "mode" s)) 7w) (var_word "r7" s) * 226 arm_REG (R_mode (w2w (var_word8 "mode" s)) 8w) (var_word "r8" s) * 227 arm_REG (R_mode (w2w (var_word8 "mode" s)) 9w) (var_word "r9" s) * 228 arm_REG (R_mode (w2w (var_word8 "mode" s)) 10w) (var_word "r10" s) * 229 arm_REG (R_mode (w2w (var_word8 "mode" s)) 11w) (var_word "r11" s) * 230 arm_REG (R_mode (w2w (var_word8 "mode" s)) 12w) (var_word "r12" s) * 231 arm_REG (R_mode (w2w (var_word8 "mode" s)) 13w) (var_word "r13" s) * 232 arm_REG (R_mode (w2w (var_word8 "mode" s)) 14w) (var_word "r14" s)`; 233 234val arm_STACK_MEMORY_def = Define ` 235 arm_STACK_MEMORY = arm_MEMORY`; 236 237val arm_STATE_def = Define ` 238 arm_STATE s = 239 arm_STATE_REGS s * arm_STATE_CPSR s * 240 arm_OK (w2w (var_word8 "mode" s)) * 241 arm_MEMORY (var_dom "dom" s) (var_mem "mem" s) * 242 arm_STACK_MEMORY (var_dom "dom_stack" s) (var_mem "stack" s)`; 243 244val arm_STATE_thm = save_thm("arm_STATE_thm", 245 arm_STATE_def 246 |> REWRITE_RULE [arm_STATE_CPSR_def,arm_STATE_REGS_def,STAR_ASSOC] 247 |> SPEC_ALL); 248 249(* representation in M0 SPEC *) 250 251val m0_STATE_PSR_def = Define ` 252 m0_STATE_PSR s = 253 m0_PSR_N (var_bool "n" s) * 254 m0_PSR_Z (var_bool "z" s) * 255 m0_PSR_C (var_bool "c" s) * 256 m0_PSR_V (var_bool "v" s)`; 257 258val m0_STATE_REGS_def = Define ` 259 m0_STATE_REGS s = 260 m0_REG RName_0 (var_word "r0" s) * 261 m0_REG RName_1 (var_word "r1" s) * 262 m0_REG RName_2 (var_word "r2" s) * 263 m0_REG RName_3 (var_word "r3" s) * 264 m0_REG RName_4 (var_word "r4" s) * 265 m0_REG RName_5 (var_word "r5" s) * 266 m0_REG RName_6 (var_word "r6" s) * 267 m0_REG RName_7 (var_word "r7" s) * 268 m0_REG RName_8 (var_word "r8" s) * 269 m0_REG RName_9 (var_word "r9" s) * 270 m0_REG RName_10 (var_word "r10" s) * 271 m0_REG RName_11 (var_word "r11" s) * 272 m0_REG RName_12 (var_word "r12" s) * 273 m0_REG RName_SP_main (var_word "r13" s) * 274 m0_REG RName_LR (var_word "r14" s)`; 275 276val m0_STACK_MEMORY_def = Define ` 277 m0_STACK_MEMORY = m0_MEMORY`; 278 279val m0_STATE_def = Define ` 280 m0_STATE s = 281 m0_STATE_REGS s * m0_STATE_PSR s * 282 m0_CurrentMode Mode_Thread * 283 m0_MEMORY (var_dom "dom" s) (var_mem "mem" s) * 284 m0_STACK_MEMORY (var_dom "dom_stack" s) (var_mem "stack" s) * 285 m0_COUNT (var_nat "clock" s)`; 286 287val m0_STATE_thm = save_thm("m0_STATE_thm", 288 m0_STATE_def 289 |> REWRITE_RULE [m0_STATE_PSR_def,m0_STATE_REGS_def,STAR_ASSOC] 290 |> SPEC_ALL); 291 292(* representation in RISCV-V SPEC *) 293 294val riscv_STATE_REGS_def = Define ` 295 riscv_STATE_REGS s = 296 riscv_REG 0w (var_word "r0" s) * 297 riscv_REG 1w (var_word "r1" s) * 298 riscv_REG 2w (var_word "r2" s) * 299 riscv_REG 3w (var_word "r3" s) * 300 riscv_REG 4w (var_word "r4" s) * 301 riscv_REG 5w (var_word "r5" s) * 302 riscv_REG 6w (var_word "r6" s) * 303 riscv_REG 7w (var_word "r7" s) * 304 riscv_REG 8w (var_word "r8" s) * 305 riscv_REG 9w (var_word "r9" s) * 306 riscv_REG 10w (var_word "r10" s) * 307 riscv_REG 11w (var_word "r11" s) * 308 riscv_REG 12w (var_word "r12" s) * 309 riscv_REG 13w (var_word "r13" s) * 310 riscv_REG 14w (var_word "r14" s) * 311 riscv_REG 15w (var_word "r15" s) * 312 riscv_REG 16w (var_word "r16" s) * 313 riscv_REG 17w (var_word "r17" s) * 314 riscv_REG 18w (var_word "r18" s) * 315 riscv_REG 19w (var_word "r19" s) * 316 riscv_REG 20w (var_word "r20" s) * 317 riscv_REG 21w (var_word "r21" s) * 318 riscv_REG 22w (var_word "r22" s) * 319 riscv_REG 23w (var_word "r23" s) * 320 riscv_REG 24w (var_word "r24" s) * 321 riscv_REG 25w (var_word "r25" s) * 322 riscv_REG 26w (var_word "r26" s) * 323 riscv_REG 27w (var_word "r27" s) * 324 riscv_REG 28w (var_word "r28" s) * 325 riscv_REG 29w (var_word "r29" s) * 326 riscv_REG 30w (var_word "r30" s) * 327 riscv_REG 31w (var_word "r31" s)`; 328 329val riscv_STACK_MEMORY_def = Define ` 330 riscv_STACK_MEMORY = riscv_MEMORY`; 331 332val riscv_STATE_def = Define ` 333 riscv_STATE s = 334 riscv_STATE_REGS s * ~riscv_RV64I * 335 riscv_MEMORY (var_dom "dom" s) (var_mem "mem" s) * 336 riscv_STACK_MEMORY (var_dom "dom_stack" s) (var_mem "stack" s)`; 337 338val riscv_STATE_thm = save_thm("riscv_STATE_thm", 339 riscv_STATE_def 340 |> REWRITE_RULE [riscv_STATE_REGS_def,STAR_ASSOC] 341 |> SPEC_ALL); 342 343(* misc *) 344 345val var_update_thm = store_thm("var_update_thm", 346 ``(var_dom n ((n1 =+ x) s) = 347 if n = n1 then (case x of VarDom y => y | _ => EMPTY) else 348 var_dom n s) /\ 349 (var_nat n ((n1 =+ x) s) = 350 if n = n1 then (case x of VarNat y => y | _ => 0) else 351 var_nat n s) /\ 352 (var_word8 n ((n1 =+ x) s) = 353 if n = n1 then (case x of VarWord8 y => y | _ => 0w) else 354 var_word8 n s) /\ 355 (var_word n ((n1 =+ x) s) = 356 if n = n1 then (case x of VarWord y => y | _ => 0w) else 357 var_word n s) /\ 358 (var_mem n ((n1 =+ x) s) = 359 if n = n1 then (case x of VarMem y => y | _ => \x. 0w) else 360 var_mem n s) /\ 361 (var_bool n ((n1 =+ x) s) = 362 if n = n1 then (case x of VarBool y => y | _ => F) else 363 var_bool n s)``, 364 SRW_TAC [] [var_dom_def,var_mem_def,var_bool_def,var_nat_def, 365 var_word8_def,var_word_def,var_acc_def,APPLY_UPDATE_THM]); 366 367val all_names_def = Define ` 368 all_names = 369 ["r0"; "r1"; "r2"; "r3"; "r4"; "r5"; "r6"; "r7"; "r8"; "r9"; 370 "r10"; "r11"; "r12"; "r13"; "r14"; "r15"; "r16"; "r17"; "r18"; "r19"; 371 "r20"; "r21"; "r22"; "r23"; "r24"; "r25"; "r26"; "r27"; "r28"; "r29"; 372 "r30"; "r31"; "mode"; "n"; "z"; "c"; "v"; 373 "mem"; "dom"; "stack"; "dom_stack"; "clock"]`; 374 375val ret_and_all_names_def = Define ` 376 ret_and_all_names = "ret"::all_names ++ ["ret_addr_input"]`; 377 378val all_names_ignore_def = Define ` 379 all_names_ignore = all_names ++ ["ret_addr_input_ignore"]`; 380 381val all_names_with_input_def = Define ` 382 all_names_with_input = all_names ++ ["ret_addr_input"]`; 383 384val LIST_SUBSET_def = Define ` 385 LIST_SUBSET xs ys = EVERY (\x. MEM x ys) xs`; 386 387val upd_ok_def = Define ` 388 upd_ok u = ALL_DISTINCT (MAP FST u) /\ 389 LIST_SUBSET (MAP FST u) all_names`; 390 391val jump_ok_def = Define ` 392 (jump_ok (Jump p) = EVEN (w2n p)) /\ 393 (jump_ok Return = T)`; 394 395val next_ok_def = Define ` 396 (next_ok (ASM s u l) = upd_ok u /\ jump_ok l) /\ 397 (next_ok (IF b n1 n2) = next_ok n1 /\ next_ok n2) /\ 398 (next_ok (CALL a u n j) = 399 (MAP FST u = ret_and_all_names) /\ jump_ok j /\ 400 !st. check_ret j st (apply_update u st))` 401 402val IMPL_INST_def = Define ` 403 IMPL_INST code locs (Inst (n:'a word) assert next) = 404 next_ok next /\ EVEN (w2n n) /\ 405 !s t call w. 406 assert s /\ exec_next locs next s t w call ==> 407 let (c,m,x,p) = code in SPEC m (x s * p n) c (x t * p w)`; 408 409val a_tools = ``(ARM_MODEL,arm_STATE,arm_PC)`` 410val m_tools = ``(M0_MODEL,m0_STATE,m0_PC)`` 411val r_tools = ``(RISCV_MODEL,riscv_STATE,riscv_PC)`` 412 413val ARM_def = Define `ARM (c:((word32 # word32) set)) = (c,^a_tools)`; 414val M0_def = Define `M0 (c:(word32 # (word16 + word32)) set) = (c,^m_tools)`; 415val RISCV_def = Define `RISCV (c:(word64 # (word8 list)) set) = (c,^r_tools)`; 416 417val _ = ``IMPL_INST (ARM _)``; 418val _ = ``IMPL_INST (M0 _)``; 419val _ = ``IMPL_INST (RISCV _)``; 420 421val IMPL_INST_IF = store_thm("IMPL_INST_IF", 422 ``IMPL_INST code locs (Inst pc1 assert1 next1) /\ 423 IMPL_INST code locs (Inst pc1 assert2 next2) ==> 424 (!s. assert1 s ==> assert2 s) ==> 425 !guard. IMPL_INST code locs (Inst pc1 assert1 (IF guard next1 next2))``, 426 SIMP_TAC std_ss [IMPL_INST_def,exec_next_def,next_ok_def] \\ METIS_TAC []); 427 428val IMPL_INST_IF_ALT = store_thm("IMPL_INST_IF_ALT", 429 ``IMPL_INST code locs (Inst pc1 assert1 next1) /\ 430 IMPL_INST code locs (Inst pc1 assert2 next2) ==> 431 !guard. IMPL_INST code locs 432 (Inst pc1 (\s. if guard s then assert1 s else assert2 s) 433 (IF guard next1 next2))``, 434 SIMP_TAC std_ss [IMPL_INST_def,exec_next_def,next_ok_def] \\ METIS_TAC []); 435 436val IMPL_INST_SIMP_IF = store_thm("IMPL_INST_SIMP_IF", 437 ``IMPL_INST code locs 438 (Inst pc assert (IF guard (ASM (SOME s1) up1 j1) 439 (ASM (SOME s2) up2 j2))) <=> 440 IMPL_INST code locs 441 (Inst pc assert (IF guard (ASM (SOME (\s. guard s ==> s1 s)) up1 j1) 442 (ASM (SOME (\s. ~guard s ==> s2 s)) up2 j2)))``, 443 SIMP_TAC std_ss [IMPL_INST_def,exec_next_def,get_assert_def,next_ok_def]); 444 445val IMPL_INST_IF_RW = store_thm("IMPL_INST_IF_RW", 446 ``(IMPL_INST code locs 447 (Inst pc assert (IF guard (ASM (SOME (\s. T)) up1 j1) next)) <=> 448 IMPL_INST code locs 449 (Inst pc assert (IF guard (ASM NONE up1 j1) next))) /\ 450 (IMPL_INST code locs 451 (Inst pc assert (IF guard next (ASM (SOME (\s. T)) up1 j1))) <=> 452 IMPL_INST code locs 453 (Inst pc assert (IF guard next (ASM NONE up1 j1))))``, 454 SIMP_TAC std_ss [IMPL_INST_def,exec_next_def,get_assert_def,next_ok_def]); 455 456val IMPL_INST_IF_SPLIT = store_thm("IMPL_INST_IF_SPLIT", 457 ``IMPL_INST c locs (Inst n b (IF g (ASM x u (Jump j)) next)) <=> 458 IMPL_INST c locs (Inst n (\s. b s /\ g s) (ASM x u (Jump j))) /\ 459 IMPL_INST c locs (Inst n (\s. b s /\ ~(g s)) next)``, 460 SIMP_TAC std_ss [IMPL_INST_def,check_jump_def,exec_next_def,next_ok_def] 461 \\ METIS_TAC []); 462 463val IMPL_INST_IF_SIMP1 = store_thm("IMPL_INST_IF_SIMP1", 464 ``IMPL_INST c locs (Inst n (K T) (IF g next1 next2)) ==> 465 !a. (!s. a s ==> g s) ==> IMPL_INST c locs (Inst n a next1)``, 466 SIMP_TAC std_ss [IMPL_INST_def,check_jump_def,exec_next_def,next_ok_def] 467 \\ METIS_TAC []); 468 469val IMPL_INST_IF_SIMP2 = store_thm("IMPL_INST_IF_SIMP2", 470 ``IMPL_INST c locs (Inst n (K T) (IF g next1 next2)) ==> 471 !a. (!s. a s ==> ($~ o g) s) ==> IMPL_INST c locs (Inst n a next2)``, 472 SIMP_TAC std_ss [IMPL_INST_def,check_jump_def,exec_next_def,next_ok_def] 473 \\ METIS_TAC []); 474 475val IMPL_INST_SET_ASSUM = store_thm("IMPL_INST_SET_ASSUM", 476 ``IMPL_INST c locs (Inst n (K T) next) ==> 477 !a. IMPL_INST c locs (Inst n a next)``, 478 SIMP_TAC std_ss [IMPL_INST_def,check_jump_def,exec_next_def] 479 \\ METIS_TAC []); 480 481val IMPL_INST_IF_COMPOSE1 = store_thm("IMPL_INST_IF_COMPOSE1", 482 ``IMPL_INST c locs (Inst n b (IF g (ASM pre u1 (Jump w)) next)) /\ 483 IMPL_INST c locs (Inst w g (ASM NONE [] (Jump j))) ==> 484 (!s. g s ==> g (apply_update u1 s)) ==> 485 IMPL_INST c locs (Inst n b (IF g (ASM pre u1 (Jump j)) next))``, 486 PairCases_on `c` 487 \\ rename [`(c,m,c6,c7)`] 488 \\ SIMP_TAC (srw_ss()) [IMPL_INST_def,check_jump_def,exec_next_def,next_ok_def] 489 \\ REPEAT STRIP_TAC \\ REVERSE (Cases_on `g s`) 490 \\ FULL_SIMP_TAC std_ss [] 491 \\ TRY (Q.PAT_ASSUM `!s t cc. bbb` (MP_TAC o Q.SPECL [`s`,`t`,`call`,`w'`]) 492 \\ FULL_SIMP_TAC std_ss [] \\ NO_TAC) 493 \\ rpt BasicProvers.TOP_CASE_TAC \\ rpt var_eq_tac \\ fs [] 494 \\ MATCH_MP_TAC (progTheory.SPEC_COMPOSE 495 |> Q.SPECL [`x`,`p`,`c`,`m`,`c`,`q`] 496 |> SIMP_RULE std_ss [UNION_IDEMPOT] |> GEN_ALL) 497 \\ fs [] 498 \\ first_x_assum (qspecl_then [`s`,`apply_update u1 s`] mp_tac) 499 \\ fs [] \\ strip_tac 500 \\ FULL_SIMP_TAC std_ss [get_assert_def,apply_update_def] \\ METIS_TAC []); 501 502val IMPL_INST_IF_COMPOSE2 = store_thm("IMPL_INST_IF_COMPOSE2", 503 ``IMPL_INST c locs (Inst n b (IF g next (ASM pre u1 (Jump w)))) /\ 504 IMPL_INST c locs (Inst w ($~ o g) (ASM NONE [] (Jump j))) ==> 505 (!s. g (apply_update u1 s) <=> g s) ==> 506 IMPL_INST c locs (Inst n b (IF g next (ASM pre u1 (Jump j))))``, 507 PairCases_on `c` 508 \\ rename [`(c,m,c6,c7)`] 509 \\ SIMP_TAC (srw_ss()) [IMPL_INST_def,check_jump_def,exec_next_def,next_ok_def] 510 \\ REPEAT STRIP_TAC \\ Cases_on `g s` 511 \\ FULL_SIMP_TAC std_ss [] 512 \\ TRY (Q.PAT_ASSUM `!s t cc. bbb` (MP_TAC o Q.SPECL [`s`,`t`,`call`,`w'`]) 513 \\ FULL_SIMP_TAC std_ss [] \\ NO_TAC) 514 \\ rpt BasicProvers.TOP_CASE_TAC \\ rpt var_eq_tac \\ fs [] 515 \\ MATCH_MP_TAC (progTheory.SPEC_COMPOSE 516 |> Q.SPECL [`x`,`p`,`c`,`m`,`c`,`q`] 517 |> SIMP_RULE std_ss [UNION_IDEMPOT] |> GEN_ALL) 518 \\ fs [] 519 \\ first_x_assum (qspecl_then [`s`,`apply_update u1 s`] mp_tac) 520 \\ fs [] \\ strip_tac 521 \\ FULL_SIMP_TAC std_ss [get_assert_def,apply_update_def] \\ METIS_TAC []); 522 523val LESS_EQ_APPEND = store_thm("LESS_EQ_APPEND", 524 ``!xs n. n <= LENGTH xs ==> ?ys zs. (xs = ys ++ zs) /\ (LENGTH ys = n)``, 525 Induct \\ Cases_on `n` \\ FULL_SIMP_TAC (srw_ss()) [LENGTH_NIL] 526 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [LENGTH,APPEND]); 527 528val EL_LENGTH_APPEND = store_thm("EL_LENGTH_APPEND", 529 ``!n xs ys. (EL (LENGTH xs) (xs ++ ys) = EL 0 ys) /\ 530 (EL (LENGTH xs + n) (xs ++ ys) = EL n ys)``, 531 REPEAT STRIP_TAC \\ `LENGTH xs <= LENGTH xs + n` by DECIDE_TAC 532 \\ FULL_SIMP_TAC std_ss [rich_listTheory.EL_APPEND2]); 533 534val DROP_LENGTH_ADD_APPEND = store_thm("DROP_LENGTH_ADD_APPEND", 535 ``!xs n ys. DROP (LENGTH xs + n) (xs ++ ys) = DROP n ys``, 536 Induct \\ ASM_SIMP_TAC (srw_ss()) [LENGTH,ADD_CLAUSES]); 537 538val LUPDATE_LENGTH_ADD_APPEND = store_thm("LUPDATE_LENGTH_ADD_APPEND", 539 ``!xs x n ys. (LUPDATE x (LENGTH xs) (xs ++ ys) = xs ++ LUPDATE x 0 ys) /\ 540 (LUPDATE x (LENGTH xs + n) (xs ++ ys) = xs ++ LUPDATE x n ys)``, 541 Induct \\ ASM_SIMP_TAC (srw_ss()) [LENGTH,ADD_CLAUSES,LUPDATE_def]); 542 543val EL_LENGTH_REVERSE_APPEND = store_thm("EL_LENGTH_REVERSE_APPEND", 544 ``(EL (LENGTH xs + n) (REVERSE xs ++ ys) = EL n ys) /\ 545 (EL (LENGTH xs) (REVERSE xs ++ ys) = EL 0 ys)``, 546 ONCE_REWRITE_TAC [GSYM LENGTH_REVERSE] 547 \\ SIMP_TAC std_ss [EL_LENGTH_APPEND]); 548 549val arm_STATE_all_names = store_thm("arm_STATE_all_names", 550 ``EVERY (\n. s1 n = s2 n) all_names ==> 551 (arm_STATE s1 = arm_STATE s2)``, 552 SIMP_TAC std_ss [arm_STATE_thm,EVERY_DEF,all_names_def, 553 var_word8_def,var_dom_def,var_mem_def,var_nat_def, 554 var_word_def,STAR_ASSOC,var_acc_def,var_bool_def]); 555 556val m0_STATE_all_names = store_thm("m0_STATE_all_names", 557 ``EVERY (\n. s1 n = s2 n) all_names ==> 558 (m0_STATE s1 = m0_STATE s2)``, 559 SIMP_TAC std_ss [m0_STATE_thm,EVERY_DEF,all_names_def, 560 var_word8_def,var_dom_def,var_mem_def,var_nat_def, 561 var_word_def,STAR_ASSOC,var_acc_def,var_bool_def]); 562 563val riscv_STATE_all_names = store_thm("riscv_STATE_all_names", 564 ``EVERY (\n. s1 n = s2 n) all_names ==> 565 (riscv_STATE s1 = riscv_STATE s2)``, 566 SIMP_TAC std_ss [riscv_STATE_thm,EVERY_DEF,all_names_def, 567 var_word8_def,var_dom_def,var_mem_def,var_nat_def, 568 var_word_def,STAR_ASSOC,var_acc_def,var_bool_def]); 569 570(* translation from my graph lang to Tom's *) 571 572val get_jump_def = Define ` 573 (get_jump (Jump j) = NextNode (w2n j)) /\ 574 (get_jump Return = Ret)`; 575 576val next_trans_def = Define ` 577 (next_trans n t (ASM NONE upd jump) = 578 (t, 579 [(n,Basic (get_jump jump) upd)])) /\ 580 (next_trans n t (ASM (SOME a) upd jump) = 581 (t+2, 582 [(n,Cond (NextNode t) Err a); 583 (t,Basic (get_jump jump) upd)])) /\ 584 (next_trans n t (IF guard n1 n2) = 585 let (t1,xs) = next_trans t (t+4) n1 in 586 let (t2,ys) = next_trans (t+2) t1 n2 in 587 (t2,[(n,Cond (NextNode t) (NextNode (t+2)) guard)] ++ xs ++ ys)) /\ 588 (next_trans n t (CALL a upd name r) = 589 (t+2, 590 [(n,Cond (NextNode t) Err (get_assert a)); 591 (t,Call (get_jump r) name (MAP SND upd) all_names_ignore)]))` 592 593val inst_trans_def = Define ` 594 inst_trans t (Inst l _ next) = next_trans (w2n l) t next`; 595 596val list_inst_trans_def = Define ` 597 (list_inst_trans t [] = []) /\ 598 (list_inst_trans t (x::xs) = 599 let (t1,ys) = inst_trans t x in 600 ys ++ list_inst_trans t1 xs)`; 601 602val graph_def = zDefine ` 603 (graph [] = K NONE) /\ 604 (graph ((x,y)::xs) = (x =+ SOME y) (graph xs))`; 605 606val func_trans_def = zDefine ` 607 func_trans (Func name entry l) = 608 (name,GraphFunction ret_and_all_names all_names_with_input 609 (graph (list_inst_trans 1 l)) (w2n entry))`; 610 611val list_func_trans_def = zDefine ` 612 list_func_trans fs = graph (MAP func_trans fs)`; 613 614(* condition decompiler has to prove *) 615 616val inst_loc_def = Define ` 617 inst_loc (Inst loc _ _) = w2n loc`; 618 619val fs_locs_def = Define ` 620 (fs_locs [] = K NONE) /\ 621 (fs_locs ((Func name entry l)::xs) = (name =+ SOME entry) (fs_locs xs))`; 622 623val func_ok_def = Define ` 624 func_ok code names (Func name entry l) = 625 ALL_DISTINCT (MAP inst_loc l) /\ EVEN (w2n entry) /\ 626 !i assert next. 627 MEM (Inst i assert next) l ==> 628 IMPL_INST code names (Inst i assert next) /\ (assert = K T)`; 629 630val funcs_ok_def = Define ` 631 funcs_ok code fs = EVERY (func_ok code (fs_locs fs)) fs`; 632 633(* proving a simulation result *) 634 635val find_inst_def = Define ` 636 (find_inst n [] = NONE) /\ 637 (find_inst n ((Inst l asrt next)::xs) = 638 if l = n then SOME (Inst l asrt next) else find_inst n xs)`; 639 640val find_func_def = Define ` 641 (find_func n [] = NONE) /\ 642 (find_func n ((Func name entry insts)::xs) = 643 if n = name then SOME (Func name entry insts) else find_func n xs)`; 644 645val good_stack_tail_def = Define ` 646 (good_stack_tail fs ([]:'a stack) = T) /\ 647 (good_stack_tail fs [x] = T) /\ 648 (good_stack_tail fs ((l1,s1,n1)::(l2,s2,n2)::xs) = 649 good_stack_tail fs ((l2,s2,n2)::xs) /\ 650 ?n x1 x2 g x3 ret y1 y2 y3. 651 (l2 = NextNode n) /\ 652 (list_func_trans fs n2 = SOME (GraphFunction x1 x2 g x3)) /\ 653 (g n = SOME (Call ret y1 y2 y3)) /\ 654 (case ret of 655 | NextNode i => (var_word "ret" s1 = n2w i) /\ EVEN i 656 | Ret => (var_word "ret" s1 = var_word "ret" s2) 657 | Err => F))` 658 659val good_stack_def = Define ` 660 good_stack fs stack = 661 good_stack_tail fs stack /\ 662 (case FST (HD stack) of 663 | Err => F 664 | NextNode n => EVEN n 665 | Ret => T)`; 666 667val NRC_Err = prove( 668 ``!n s st name s2. 669 NRC (exec_graph_step Gamma) n ((Err,st,name)::s) s2 ==> 670 ~(good_stack fs s2)``, 671 Induct \\ FULL_SIMP_TAC (srw_ss()) [good_stack_def,NRC,PULL_EXISTS] 672 \\ REPEAT STRIP_TAC \\ FIRST_X_ASSUM MATCH_MP_TAC 673 \\ Q.PAT_ASSUM `exec_graph_step Gamma ((Err,st,name)::s) z` MP_TAC 674 \\ SIMP_TAC (srw_ss()) [exec_graph_step_def,upd_stack_def] 675 \\ Cases_on `s` \\ FULL_SIMP_TAC (srw_ss()) [] 676 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 677 \\ PairCases_on `h` \\ FULL_SIMP_TAC (srw_ss()) [upd_stack_def] 678 \\ METIS_TAC []); 679 680val list_func_trans_EQ_SOME_IMP = prove( 681 ``!fs. 682 (list_func_trans fs name = SOME (GraphFunction x1 x2 graph1 x3)) ==> 683 ?entry l. (find_func name fs = SOME (Func name entry l)) /\ 684 (x1 = ret_and_all_names) /\ (x2 = all_names_with_input) /\ 685 (x3 = w2n entry) /\ 686 (graph1 = graph (list_inst_trans 1 l)) /\ 687 (fs_locs fs name = SOME (n2w x3))``, 688 Induct \\ FULL_SIMP_TAC std_ss [list_func_trans_def,MAP,graph_def] 689 \\ Cases_on `h` \\ FULL_SIMP_TAC (srw_ss()) [func_trans_def,graph_def,fs_locs_def] 690 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,find_func_def] 691 \\ STRIP_TAC \\ Cases_on `s = name` \\ FULL_SIMP_TAC (srw_ss()) [] 692 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [RW1[MULT_COMM]MULT_DIV,n2w_w2n]); 693 694val odd_nums_def = Define ` 695 (odd_nums k 0 = []) /\ 696 (odd_nums k (SUC n) = (k:num) :: odd_nums (k+2) n)`; 697 698val odd_nums_ADD = prove( 699 ``!m n k. odd_nums k (m + n) = odd_nums k m ++ odd_nums (k + 2 * m) n``, 700 Induct \\ FULL_SIMP_TAC std_ss [odd_nums_def,APPEND,ADD_CLAUSES, 701 MULT_CLAUSES,ADD_ASSOC]); 702 703val next_trans_IMP = prove( 704 ``!nn n k k1 xs. 705 ODD k /\ (next_trans n k nn = (k1,xs)) ==> 706 ?y ys. (xs = (n,y)::ys) /\ EVERY (ODD o FST) ys /\ ODD k1 /\ 707 PERM (MAP FST xs) (n :: odd_nums k (LENGTH (TL xs))) /\ 708 (k1 = k + 2 * (LENGTH (TL xs)))``, 709 REVERSE Induct 710 \\ SIMP_TAC (srw_ss()) [next_trans_def,LET_DEF,CONS_11,EVERY_DEF,ODD_ADD] 711 THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) 712 THEN1 (Cases 713 \\ EVAL_TAC \\ SIMP_TAC (srw_ss()) [] \\ EVAL_TAC \\ SRW_TAC [] [] 714 \\ FULL_SIMP_TAC std_ss [ODD_ADD]) 715 \\ REPEAT STRIP_TAC 716 \\ Cases_on `next_trans k (k + 4) nn` \\ FULL_SIMP_TAC std_ss [] 717 \\ Cases_on `next_trans (k + 2) q nn'` \\ FULL_SIMP_TAC std_ss [] 718 \\ `ODD (k + 4) /\ ODD (k + 2)` by FULL_SIMP_TAC (srw_ss()) [ODD_ADD] 719 \\ RES_TAC \\ RES_TAC 720 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bb` (K ALL_TAC)) \\ REVERSE (SRW_TAC [] []) 721 \\ FULL_SIMP_TAC std_ss [odd_nums_def,CONS_11] 722 \\ FULL_SIMP_TAC std_ss [sortingTheory.PERM_CONS_IFF,MAP,TL] 723 THEN1 DECIDE_TAC 724 \\ FULL_SIMP_TAC std_ss [ADD_CLAUSES,odd_nums_def] 725 \\ MATCH_MP_TAC sortingTheory.APPEND_PERM_SYM 726 \\ FULL_SIMP_TAC std_ss [sortingTheory.PERM_CONS_IFF,MAP,TL,APPEND] 727 \\ FULL_SIMP_TAC std_ss [GSYM ADD_ASSOC] 728 \\ MATCH_MP_TAC sortingTheory.APPEND_PERM_SYM 729 \\ FULL_SIMP_TAC std_ss [odd_nums_ADD] 730 \\ MATCH_MP_TAC sortingTheory.PERM_CONG 731 \\ FULL_SIMP_TAC std_ss [ADD_ASSOC]); 732 733val next_trans_lemma = prove( 734 ``!nn n k k1 xs. 735 ODD k /\ (next_trans n k nn = (k1,xs)) ==> 736 ?y ys. (xs = (n,y)::ys) /\ EVERY (ODD o FST) ys /\ ODD k1``, 737 METIS_TAC [next_trans_IMP]); 738 739val graph_APPEND_ODD = prove( 740 ``!ys. 741 EVERY (ODD o FST) ys ==> 742 (graph (ys ++ xs) (2 * m) = graph xs (2 * m))``, 743 Induct \\ FULL_SIMP_TAC std_ss [APPEND,FORALL_PROD,EVERY_DEF,graph_def, 744 APPLY_UPDATE_THM] 745 \\ SRW_TAC [] [] \\ IMP_RES_TAC EVEN_ODD_EXISTS 746 \\ Q.MATCH_ASSUM_RENAME_TAC `2 * m = SUC (2 * n)` 747 \\ `(2 * m) MOD 2 = (SUC (2 * n)) MOD 2` by METIS_TAC [] 748 \\ POP_ASSUM MP_TAC 749 \\ ONCE_REWRITE_TAC [MULT_COMM] 750 \\ FULL_SIMP_TAC (srw_ss()) [MOD_MULT,ADD1] 751 \\ ONCE_REWRITE_TAC [DECIDE ``m * 2 = m * 2 + 0:num``] 752 \\ FULL_SIMP_TAC (srw_ss()) [MOD_MULT,ADD1]); 753 754val graph_list_inst_trans_EQ_SOME_IMP = prove( 755 ``!l k n x. 756 ODD k /\ EVEN n /\ n < dimword (:'a) /\ 757 (graph (list_inst_trans k l) n = SOME x) ==> 758 ?a t. find_inst ((n2w n) :'a word) l = SOME (Inst (n2w n) a t)``, 759 Induct \\ FULL_SIMP_TAC std_ss [list_inst_trans_def,graph_def] 760 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [inst_trans_def,find_inst_def] 761 \\ REPEAT STRIP_TAC 762 \\ Cases_on `next_trans (w2n c) k n` 763 \\ FULL_SIMP_TAC std_ss [LET_DEF] 764 \\ IMP_RES_TAC next_trans_lemma 765 \\ NTAC 2 (POP_ASSUM (K ALL_TAC)) 766 \\ SRW_TAC [] [] 767 \\ FULL_SIMP_TAC std_ss [APPEND,graph_def,APPLY_UPDATE_THM] 768 \\ Cases_on `c` \\ FULL_SIMP_TAC (srw_ss()) [] 769 \\ Q.MATCH_ASSUM_RENAME_TAC `n1 ��� n2 MOD dimword (:'a)` 770 \\ IMP_RES_TAC (EVEN_ODD_EXISTS |> SPEC_ALL |> CONJUNCT1) 771 \\ FIRST_X_ASSUM MATCH_MP_TAC 772 \\ Q.EXISTS_TAC `q` \\ FULL_SIMP_TAC std_ss [] 773 \\ NTAC 3 (POP_ASSUM MP_TAC) 774 \\ FULL_SIMP_TAC std_ss [graph_APPEND_ODD] 775 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []); 776 777val MEM_IMP_graph_SOME = prove( 778 ``!nodes i x. 779 MEM (i,x) nodes /\ ALL_DISTINCT (MAP FST nodes) ==> 780 (graph nodes i = SOME x)``, 781 Induct \\ FULL_SIMP_TAC (srw_ss()) [FORALL_PROD,MEM_MAP,graph_def] 782 \\ NTAC 3 STRIP_TAC \\ Cases_on `p_1 = i` \\ FULL_SIMP_TAC std_ss [] 783 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM]); 784 785val exec_graph_step_NOT_ZERO = prove( 786 ``!s2. NRC (exec_graph_step (list_func_trans fs)) n 787 ((NextNode k,st,name)::t) s2 /\ ODD k /\ good_stack fs s2 ==> n <> 0``, 788 Cases_on `n` 789 \\ FULL_SIMP_TAC (srw_ss()) [ADD1,NRC,good_stack_def,EVERY_DEF] 790 \\ FULL_SIMP_TAC std_ss [EVEN_ODD] 791 \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss []); 792 793val ZIP_MAP_MAP = prove( 794 ``!xs f g. ZIP (MAP f xs, MAP g xs) = MAP (\x. (f x, g x)) xs``, 795 Induct \\ SRW_TAC [] []); 796 797val NOT_MEM_IMP_fold_var_upd_ALT = prove( 798 ``!l st x y. 799 ~(MEM x (MAP FST l)) ==> 800 (fold (\(var,val). var_upd var val) l ((x =+ y) st) = 801 (x =+ y) (fold (\(var,val). var_upd var val) l st))``, 802 Induct \\ SRW_TAC [] [fold_def,var_upd_def] 803 \\ Cases_on `h` \\ FULL_SIMP_TAC (srw_ss()) [fold_def,var_upd_def] 804 \\ `((q =+ r) ((x =+ y) st)) = ((x =+ y) ((q =+ r) st))` 805 by METIS_TAC [UPDATE_COMMUTES] \\ METIS_TAC []); 806 807val NOT_MEM_IMP_fold_var_upd = prove( 808 ``!l st x y. 809 ~(MEM x (MAP FST l)) ==> 810 (fold (\(var,val). var_upd var val) (MAP (\(p1,p2). (p1,p2 st1)) l) 811 ((x =+ y st1) st) = 812 (x =+ y st1) 813 (fold (\(var,val). var_upd var val) (MAP (\(p1,p2). (p1,p2 st1)) l) st))``, 814 REPEAT STRIP_TAC \\ MATCH_MP_TAC NOT_MEM_IMP_fold_var_upd_ALT 815 \\ FULL_SIMP_TAC std_ss [MEM_MAP,FORALL_PROD]); 816 817val NOT_MEM_IMP_fold_var_upd_HO = prove( 818 ``!l st x y. 819 ~(MEM x (MAP FST l)) ==> 820 (fold (\(var,val). var_upd var (val t)) l ((x =+ y t) st) = 821 (x =+ y t) (fold (\(var,val). var_upd var (val t)) l st))``, 822 Induct \\ SRW_TAC [] [fold_def,var_upd_def] 823 \\ Cases_on `h` \\ FULL_SIMP_TAC (srw_ss()) [fold_def,var_upd_def] 824 \\ `((q =+ r t) ((x =+ y t) st)) = ((x =+ y t) ((q =+ r t) st))` 825 by METIS_TAC [UPDATE_COMMUTES] \\ METIS_TAC []); 826 827val upd_vars_thm = prove( 828 ``!l st. upd_ok l ==> (upd_vars l st = apply_update l st)``, 829 SIMP_TAC std_ss [upd_vars_def,save_vals_def,ZIP_MAP_MAP,LAMBDA_PROD] 830 \\ Induct 831 \\ FULL_SIMP_TAC std_ss [apply_update_def,FORALL_PROD,MAP,fold_def,var_upd_def] 832 \\ FULL_SIMP_TAC std_ss [upd_ok_def,ALL_DISTINCT,MAP] 833 \\ FULL_SIMP_TAC std_ss [NOT_MEM_IMP_fold_var_upd] 834 \\ REPEAT STRIP_TAC \\ AP_TERM_TAC 835 \\ FIRST_X_ASSUM MATCH_MP_TAC 836 \\ FULL_SIMP_TAC std_ss [LIST_SUBSET_def,EVERY_DEF]); 837 838val fold_MAP = prove( 839 ``!xs f g s. fold f (MAP g xs) s = fold (f o g) xs s``, 840 Induct \\ SRW_TAC [] [fold_def,MAP]); 841 842val fold_EQ_apply_update = prove( 843 ``!l s1 s2 n. 844 ALL_DISTINCT (MAP FST l) /\ MEM n (MAP FST l) ==> 845 (fold (\x. var_upd (FST x) (SND x st)) l s1 n = 846 apply_update l st n)``, 847 Induct \\ FULL_SIMP_TAC std_ss [MEM,MAP,ALL_DISTINCT] 848 \\ Cases \\ FULL_SIMP_TAC std_ss [fold_def,var_upd_def,LAMBDA_PROD] 849 \\ REPEAT STRIP_TAC 850 \\ FULL_SIMP_TAC std_ss [NOT_MEM_IMP_fold_var_upd_HO,apply_update_def] 851 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 852 \\ METIS_TAC []); 853 854val upd_ok_IMP_var_word_ret = prove( 855 ``!l. upd_ok l ==> 856 (var_word "ret" (apply_update l st) = var_word "ret" st)``, 857 Induct \\ FULL_SIMP_TAC std_ss [FORALL_PROD] 858 \\ FULL_SIMP_TAC std_ss [apply_update_def,upd_ok_def,MAP,LIST_SUBSET_def, 859 EVERY_DEF,ALL_DISTINCT,var_word_def,var_acc_def, 860 APPLY_UPDATE_THM] 861 \\ `~MEM "ret" all_names` by ALL_TAC 862 THEN1 (SIMP_TAC std_ss [all_names_def] \\ EVAL_TAC) 863 \\ SRW_TAC [] []); 864 865val good_stack_tail_UPDATE = prove( 866 ``good_stack_tail fs ((i,st,name)::t) /\ upd_ok l ==> 867 good_stack_tail fs ((i,apply_update l st,name)::t)``, 868 Cases_on `t` \\ FULL_SIMP_TAC std_ss [good_stack_tail_def] 869 \\ PairCases_on `h` \\ FULL_SIMP_TAC std_ss [good_stack_tail_def] 870 \\ Cases_on `upd_ok l` \\ FULL_SIMP_TAC std_ss [] 871 \\ IMP_RES_TAC upd_ok_IMP_var_word_ret \\ FULL_SIMP_TAC std_ss []); 872 873val good_stack_tail_STEP = prove( 874 ``good_stack_tail fs ((i,st,name)::t) ==> 875 !k. good_stack_tail fs ((k,st,name)::t)``, 876 Cases_on `t` \\ FULL_SIMP_TAC std_ss [good_stack_tail_def] 877 \\ PairCases_on `h` \\ FULL_SIMP_TAC std_ss [good_stack_tail_def]); 878 879val var_word_fold_IGNORE = prove( 880 ``!t s st. 881 ~(MEM x (MAP FST t)) ==> 882 (var_word x 883 (fold (\(var,val). var_upd var val) (MAP (\x. (FST x,SND x st)) t) s) = 884 var_word x s)``, 885 Induct \\ FULL_SIMP_TAC std_ss [MAP,fold_def,MEM,MAP] 886 \\ FULL_SIMP_TAC std_ss [var_word_def,var_upd_def,var_acc_def, 887 APPLY_UPDATE_THM]); 888 889val save_vals_lemma = prove( 890 ``(MAP FST l = ("ret"::all_names ++ ["ret_addr_input"])) ==> 891 (var_word "ret" (save_vals ("ret"::all_names ++ ["ret_addr_input"]) 892 (MAP (\i. i st) (MAP SND l)) s) = 893 var_word "ret" (apply_update l st))``, 894 Cases_on `l` \\ FULL_SIMP_TAC (srw_ss()) [MAP,save_vals_def,fold_def] 895 \\ FULL_SIMP_TAC std_ss [var_upd_def] \\ REPEAT STRIP_TAC 896 \\ POP_ASSUM (ASSUME_TAC o GSYM) 897 \\ FULL_SIMP_TAC std_ss [MAP_MAP_o,o_DEF,ZIP_MAP_MAP] 898 \\ `~(MEM "ret" (MAP FST t))` by ALL_TAC 899 THEN1 (POP_ASSUM (ASSUME_TAC o GSYM) 900 \\ FULL_SIMP_TAC std_ss [all_names_def] \\ EVAL_TAC) 901 \\ FULL_SIMP_TAC std_ss [var_word_fold_IGNORE] \\ Cases_on `h` 902 \\ FULL_SIMP_TAC std_ss [apply_update_def,var_word_def,var_acc_def, 903 APPLY_UPDATE_THM]); 904 905val find_func_IMP_EVEN = prove( 906 ``!fs s s entry l. 907 EVERY (func_ok code jjj) fs /\ 908 (find_func s fs = SOME (Func s entry l)) ==> 909 EVEN (w2n entry)``, 910 Induct \\ TRY (Cases_on `h`) \\ FULL_SIMP_TAC std_ss [find_func_def] 911 \\ REPEAT STRIP_TAC \\ Cases_on `s' = s` 912 \\ FULL_SIMP_TAC (srw_ss()) [funcs_ok_def,func_ok_def,fs_locs_def] 913 \\ RES_TAC) |> SPEC_ALL |> Q.INST [`jjj`|->`fs_locs fs`] 914 |> SIMP_RULE std_ss [GSYM funcs_ok_def]; 915 916val find_inst_IMP_LIST_SUBSET = prove( 917 ``!l k1. 918 i < dimword (:'a) /\ ALL_DISTINCT (MAP inst_loc l) /\ ODD k1 /\ 919 (find_inst (n2w i) l = SOME (Inst ((n2w i) :'a word) a next)) ==> 920 ?k2. ODD k2 /\ 921 (LIST_SUBSET (SND (next_trans i k2 next)) (list_inst_trans k1 l))``, 922 Induct \\ FULL_SIMP_TAC std_ss [find_inst_def] \\ Cases_on `h` 923 \\ FULL_SIMP_TAC std_ss [find_inst_def,inst_loc_def,MAP,ALL_DISTINCT] 924 \\ Cases_on `c = n2w i` \\ FULL_SIMP_TAC (srw_ss()) [] 925 \\ REPEAT STRIP_TAC THEN1 926 (Q.EXISTS_TAC `k1` 927 \\ FULL_SIMP_TAC (srw_ss()) [LIST_SUBSET_def,EVERY_MEM,list_inst_trans_def, 928 inst_trans_def,w2n_n2w] \\ Cases_on `next_trans i k1 next` 929 \\ FULL_SIMP_TAC std_ss [LET_DEF,MEM_APPEND]) 930 \\ FULL_SIMP_TAC std_ss [] 931 \\ FULL_SIMP_TAC (srw_ss()) [LIST_SUBSET_def,EVERY_MEM,list_inst_trans_def, 932 inst_trans_def,w2n_n2w] 933 \\ Cases_on `next_trans (w2n (c:'a word)) k1 n` 934 \\ FULL_SIMP_TAC std_ss [MEM_APPEND,LET_DEF] 935 \\ `ODD q` by IMP_RES_TAC next_trans_IMP 936 \\ METIS_TAC []) |> Q.SPECL [`l`,`1`] |> SIMP_RULE std_ss []; 937 938val NOT_MEM_odd_nums = prove( 939 ``!l k n. ODD k /\ EVEN n ==> ~(MEM n (odd_nums k l))``, 940 Induct \\ FULL_SIMP_TAC std_ss [odd_nums_def,MEM] 941 \\ REPEAT STRIP_TAC 942 \\ FULL_SIMP_TAC std_ss [ODD_EVEN] 943 \\ FULL_SIMP_TAC std_ss [ODD_EVEN] 944 \\ `~(EVEN (k+2))` by FULL_SIMP_TAC std_ss [EVEN_ADD] 945 \\ RES_TAC); 946 947val MEM_odd_nums = prove( 948 ``!l k i. MEM k (odd_nums i l) ==> i <= k``, 949 Induct \\ FULL_SIMP_TAC std_ss [odd_nums_def,MEM] 950 \\ REPEAT STRIP_TAC \\ RES_TAC \\ DECIDE_TAC); 951 952val ALL_DISTINCT_odd_nums = prove( 953 ``!l k. ALL_DISTINCT (odd_nums k l)``, 954 Induct \\ FULL_SIMP_TAC std_ss [odd_nums_def,ALL_DISTINCT] 955 \\ POP_ASSUM (K ALL_TAC) \\ REPEAT STRIP_TAC 956 \\ IMP_RES_TAC MEM_odd_nums \\ DECIDE_TAC); 957 958val EVEN_ODD_MEM_list_inst_trans = prove( 959 ``!l k. 960 EVERY (\i. EVEN (inst_loc i)) l /\ 961 MEM e (MAP FST (list_inst_trans k l)) /\ ODD k ==> 962 if EVEN e then MEM e (MAP inst_loc l) else k <= e``, 963 Induct \\ FULL_SIMP_TAC std_ss [list_inst_trans_def,MAP,MEM] 964 \\ REPEAT STRIP_TAC \\ Cases_on `inst_trans k h` \\ Cases_on `h` 965 \\ FULL_SIMP_TAC std_ss [LET_DEF,MEM,MAP_APPEND,inst_trans_def] 966 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,inst_loc_def] 967 \\ Q.MATCH_ASSUM_RENAME_TAC `next_trans (w2n c) k nn = (k1,xs)` 968 \\ MP_TAC (next_trans_IMP |> Q.SPECL [`nn`,`w2n (c:'a word)`] |> SPEC_ALL) 969 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 970 \\ FULL_SIMP_TAC std_ss [MEM_APPEND,MEM,MAP,inst_loc_def,TL] 971 THEN1 (Q.PAT_ASSUM `xs = yyy` ASSUME_TAC 972 \\ FULL_SIMP_TAC std_ss [TL,HD,MAP,sortingTheory.PERM_CONS_IFF] 973 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP] 974 \\ Cases_on `y'` \\ FULL_SIMP_TAC std_ss [] 975 \\ `ODD q` by (RES_TAC \\ FULL_SIMP_TAC std_ss []) 976 \\ ASM_SIMP_TAC std_ss [EVEN_ODD] 977 \\ IMP_RES_TAC sortingTheory.PERM_MEM_EQ 978 \\ FULL_SIMP_TAC std_ss [MEM_MAP,PULL_EXISTS,FORALL_PROD] 979 \\ RES_TAC \\ IMP_RES_TAC MEM_odd_nums) 980 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [ODD_ADD,ODD_EVEN,EVEN_DOUBLE] 981 \\ RES_TAC \\ Cases_on `EVEN e` \\ FULL_SIMP_TAC std_ss [] 982 \\ DECIDE_TAC) 983 984val EVEN_MEM_list_inst_trans = prove( 985 ``EVERY (\i. EVEN (inst_loc i)) l /\ 986 MEM e (MAP FST (list_inst_trans k l)) /\ EVEN e /\ ODD k ==> 987 MEM e (MAP inst_loc l)``, 988 METIS_TAC [EVEN_ODD_MEM_list_inst_trans]) 989 990val ODD_MEM_list_inst_trans = prove( 991 ``EVERY (\i. EVEN (inst_loc i)) l /\ 992 MEM e (MAP FST (list_inst_trans k l)) /\ ODD e /\ ODD k ==> 993 k <= e``, 994 METIS_TAC [EVEN_ODD_MEM_list_inst_trans,EVEN_ODD]) 995 996val ODD_MEM_odd_nums = prove( 997 ``!l k i. MEM k (odd_nums i l) /\ ODD i ==> ODD k /\ k < i + 2 * l``, 998 Induct \\ FULL_SIMP_TAC std_ss [odd_nums_def,MEM] 999 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1000 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [ODD_ADD] 1001 \\ RES_TAC \\ DECIDE_TAC); 1002 1003val ALL_DISTINCT_list_inst_trans = prove( 1004 ``!l k. EVERY (\i. EVEN (inst_loc i)) l /\ 1005 ODD k /\ ALL_DISTINCT (MAP inst_loc l) ==> 1006 ALL_DISTINCT (MAP FST (list_inst_trans k l))``, 1007 Induct THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) 1008 \\ FULL_SIMP_TAC std_ss [list_inst_trans_def,LET_DEF] 1009 \\ REPEAT STRIP_TAC \\ Cases_on `inst_trans k h` 1010 \\ FULL_SIMP_TAC std_ss [MAP_APPEND,ALL_DISTINCT_APPEND,MAP,ALL_DISTINCT] 1011 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [EVERY_DEF,inst_loc_def] 1012 \\ FULL_SIMP_TAC std_ss [inst_trans_def] 1013 \\ `ODD q` by IMP_RES_TAC next_trans_IMP 1014 \\ FULL_SIMP_TAC std_ss [] 1015 \\ MP_TAC (next_trans_IMP |> Q.SPECL [`n`,`w2n (c:'a word)`,`k`,`q`,`r`]) 1016 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1017 THEN1 (IMP_RES_TAC sortingTheory.ALL_DISTINCT_PERM 1018 \\ FULL_SIMP_TAC std_ss [TL,ALL_DISTINCT,ALL_DISTINCT_odd_nums] 1019 \\ MATCH_MP_TAC NOT_MEM_odd_nums 1020 \\ FULL_SIMP_TAC std_ss [EVEN_DOUBLE]) 1021 \\ IMP_RES_TAC sortingTheory.PERM_MEM_EQ 1022 \\ FULL_SIMP_TAC std_ss [inst_loc_def,TL,MEM] 1023 \\ FULL_SIMP_TAC std_ss [] 1024 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [HD,TL] 1025 \\ Q.PAT_ASSUM `~bbb` MP_TAC 1026 \\ SIMP_TAC std_ss [] THEN1 1027 (MATCH_MP_TAC (EVEN_MEM_list_inst_trans |> GEN_ALL) 1028 \\ Q.LIST_EXISTS_TAC [`(k + 2 * LENGTH ys)`] 1029 \\ FULL_SIMP_TAC std_ss [EVEN_DOUBLE]) 1030 \\ IMP_RES_TAC ODD_MEM_odd_nums 1031 \\ IMP_RES_TAC ODD_MEM_list_inst_trans 1032 \\ `F` by DECIDE_TAC); 1033 1034val find_func_IMP_MEM = prove( 1035 ``!xs x y. (find_func x xs = SOME y) ==> MEM y xs``, 1036 Induct \\ FULL_SIMP_TAC std_ss [find_func_def] \\ Cases 1037 \\ SRW_TAC [] [find_func_def] \\ RES_TAC \\ FULL_SIMP_TAC std_ss []); 1038 1039val find_inst_IMP_MEM = prove( 1040 ``!xs x y. (find_inst x xs = SOME y) ==> MEM y xs``, 1041 Induct \\ FULL_SIMP_TAC std_ss [find_inst_def] \\ Cases 1042 \\ SRW_TAC [] [find_inst_def] \\ RES_TAC \\ FULL_SIMP_TAC std_ss []); 1043 1044val graph_SOME_IMP = prove( 1045 ``!xs n y. (graph xs n = SOME y) ==> MEM (n,y) xs``, 1046 Induct \\ FULL_SIMP_TAC std_ss [graph_def,FORALL_PROD, 1047 APPLY_UPDATE_THM,MEM] \\ SRW_TAC [] []); 1048 1049val graph_APPEND = prove( 1050 ``!xs ys x. 1051 graph (xs ++ ys) x = 1052 case graph xs x of 1053 | NONE => graph ys x 1054 | y => y``, 1055 Induct \\ FULL_SIMP_TAC std_ss [graph_def,APPEND, 1056 FORALL_PROD,APPLY_UPDATE_THM] \\ SRW_TAC [] []); 1057 1058val list_inst_trans_IMP_LESS = prove( 1059 ``!l k n x. 1060 (graph (list_inst_trans k (l:'a inst list)) n = SOME x) /\ 1061 EVEN n /\ ODD k ==> 1062 n < dimword (:'a)``, 1063 Induct \\ FULL_SIMP_TAC std_ss [graph_def,FORALL_PROD, 1064 APPLY_UPDATE_THM,MEM,list_inst_trans_def,LET_DEF] 1065 \\ REPEAT STRIP_TAC \\ Cases_on `inst_trans k h` 1066 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [inst_trans_def] 1067 \\ `ODD q` by IMP_RES_TAC next_trans_IMP 1068 \\ FULL_SIMP_TAC std_ss [graph_APPEND] 1069 \\ Cases_on `graph r n` \\ FULL_SIMP_TAC std_ss [] 1070 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 1071 \\ IMP_RES_TAC graph_SOME_IMP 1072 \\ IMP_RES_TAC next_trans_IMP 1073 \\ FULL_SIMP_TAC std_ss [MEM] 1074 \\ `w2n c < dimword(:'a)` by METIS_TAC [w2n_lt] 1075 \\ FULL_SIMP_TAC (srw_ss()) [] 1076 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [EVERY_MEM,FORALL_PROD] 1077 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [EVEN_ODD]); 1078 1079val good_stack_tail_return_vars = prove( 1080 ``good_stack_tail fs ((ret,st1,name1)::t) ==> 1081 good_stack_tail fs ((ret,return_vars all_names_with_input 1082 all_names_ignore st st1,name1)::t)``, 1083 Cases_on `t` \\ FULL_SIMP_TAC std_ss [good_stack_tail_def] 1084 \\ PairCases_on `h` \\ FULL_SIMP_TAC std_ss [good_stack_tail_def] 1085 \\ `var_word "ret" (return_vars all_names_with_input all_names_ignore st st1) = 1086 var_word "ret" st1` by ALL_TAC 1087 \\ FULL_SIMP_TAC std_ss [] 1088 \\ FULL_SIMP_TAC std_ss [var_word_def,var_acc_def,return_vars_def, 1089 save_vals_def,fold_def,var_upd_def,all_names_def] \\ EVAL_TAC 1090 \\ FULL_SIMP_TAC std_ss [var_word_def,var_acc_def,return_vars_def, 1091 save_vals_def,fold_def,var_upd_def] \\ EVAL_TAC) 1092 1093val func_ok_EXPEND_CODE = store_thm("func_ok_EXPEND_CODE", 1094 ``func_ok code locs f ==> 1095 !c. (case (code,c) of 1096 | ((c1,x1), (c2,x2)) => (c1 SUBSET c2 /\ (x1 = x2))) ==> 1097 func_ok c locs f``, 1098 Cases_on `f` \\ SIMP_TAC std_ss [func_ok_def,IMPL_INST_def] 1099 \\ PairCases_on `code` \\ FULL_SIMP_TAC (srw_ss()) [] 1100 \\ REPEAT STRIP_TAC \\ PairCases_on `c'` \\ FULL_SIMP_TAC (srw_ss()) [] 1101 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 1102 \\ IMP_RES_TAC SPEC_SUBSET_CODE 1103 \\ every_case_tac \\ fs [] 1104 \\ metis_tac [SPEC_SUBSET_CODE]); 1105 1106val return_vars_SAME = prove( 1107 ``!n. MEM n all_names ==> 1108 (st n = return_vars all_names_with_input all_names_ignore st st1 n)``, 1109 FULL_SIMP_TAC std_ss [GSYM EVERY_MEM] 1110 \\ FULL_SIMP_TAC std_ss [all_names_def,EVERY_DEF,return_vars_def] 1111 \\ FULL_SIMP_TAC std_ss [var_word_def,var_acc_def,return_vars_def, 1112 save_vals_def,fold_def,var_upd_def] \\ EVAL_TAC 1113 \\ FULL_SIMP_TAC std_ss [var_word_def,var_acc_def,return_vars_def, 1114 save_vals_def,fold_def,var_upd_def] \\ EVAL_TAC) 1115 1116val MEM_CAll_next_trans = prove( 1117 ``!n1 d k q r. MEM (n,Call x1 x2 x3 x4) r /\ (next_trans d k n1 = (q,r)) ==> 1118 (x4 = all_names_ignore)``, 1119 Induct \\ FULL_SIMP_TAC (srw_ss()) [next_trans_def,MEM] 1120 \\ REPEAT STRIP_TAC 1121 \\ TRY (Cases_on `o'` \\ FULL_SIMP_TAC (srw_ss()) [next_trans_def]) 1122 \\ Cases_on `next_trans k (k + 4) n1` \\ FULL_SIMP_TAC std_ss [LET_DEF] 1123 \\ Cases_on `next_trans (k + 2) q' n1'` \\ FULL_SIMP_TAC std_ss [LET_DEF] 1124 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) [MEM,MEM_APPEND] \\ RES_TAC); 1125 1126val MEM_Call_list_inst_trans = prove( 1127 ``!l k. MEM (n,Call x1 x2 x3 x4) (list_inst_trans k l) ==> 1128 (x4 = all_names_ignore)``, 1129 Induct \\ FULL_SIMP_TAC std_ss [list_inst_trans_def,MEM] 1130 \\ REPEAT STRIP_TAC \\ Cases_on `inst_trans k h` 1131 \\ FULL_SIMP_TAC std_ss [LET_DEF,MEM_APPEND] \\ RES_TAC 1132 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [inst_trans_def] 1133 \\ IMP_RES_TAC MEM_CAll_next_trans); 1134 1135val arm_assert_for_def = Define ` 1136 (arm_assert_for ([]:32 stack) = SEP_F) /\ 1137 (arm_assert_for ((loc,state,name)::rest) = 1138 arm_STATE state * arm_PC (case loc of NextNode n => n2w n 1139 | _ => var_word "ret" state))`; 1140 1141val m0_assert_for_def = Define ` 1142 (m0_assert_for ([]:32 stack) = SEP_F) /\ 1143 (m0_assert_for ((loc,state,name)::rest) = 1144 m0_STATE state * m0_PC (case loc of NextNode n => n2w n 1145 | _ => var_word "ret" state))`; 1146 1147fun exec_graph_step_IMP_exec_next arch = let 1148 val (assert_for_def,code,tm) = 1149 if arch = "arm" then 1150 (arm_assert_for_def,``ARM code``, 1151 ``arm_assert_for s4 = arm_STATE s7 * arm_PC w``) else 1152 if arch = "m0" then 1153 (m0_assert_for_def,``M0 code``, 1154 ``m0_assert_for s4 = m0_STATE s7 * m0_PC w``) else fail() 1155 in prove( 1156 ``!next i k n. 1157 NRC (exec_graph_step (list_func_trans fs)) n 1158 ((NextNode i,st,name)::t) s2 /\ n <> 0/\ funcs_ok ^code fs /\ 1159 (list_func_trans fs name = SOME (GraphFunction x1 x2 (graph nodes) x3)) /\ 1160 ODD k /\ LIST_SUBSET (SND (next_trans i k next)) nodes /\ 1161 ALL_DISTINCT (MAP FST nodes) /\ next_ok next /\ 1162 good_stack_tail fs ((NextNode i,st,name)::t) /\ good_stack fs s2 ==> 1163 ?s4 s7 j j1 call w. 1164 exec_next (fs_locs fs) next st s7 w call /\ 1165 ^tm /\ 1166 good_stack fs s4 /\ 1167 NRC (exec_graph_step (list_func_trans fs)) j 1168 ((NextNode i,st,name)::t) s4 /\ j1 < n /\ 1169 NRC (exec_graph_step (list_func_trans fs)) j1 s4 s2``, 1170 Induct \\ NTAC 4 STRIP_TAC 1171 THEN1 (* IF *) 1172 (Cases_on `n` \\ FULL_SIMP_TAC std_ss [NRC] \\ REPEAT STRIP_TAC 1173 \\ Q.PAT_X_ASSUM `exec_graph_step (list_func_trans fs) 1174 ((NextNode i,st,name)::t) z` MP_TAC 1175 \\ ASM_SIMP_TAC (srw_ss()) [Once exec_graph_step_def] 1176 \\ FULL_SIMP_TAC std_ss [next_trans_def] 1177 \\ Cases_on `next_trans k (k + 4) next` \\ FULL_SIMP_TAC (srw_ss()) [] 1178 \\ Q.MATCH_ASSUM_RENAME_TAC `next_trans k (k + 4) next1 = (t1,xs)` 1179 \\ Cases_on `next_trans (k+2) t1 next'` \\ FULL_SIMP_TAC (srw_ss()) [] 1180 \\ Q.MATCH_ASSUM_RENAME_TAC `next_trans (k+2) t1 next2 = (t2,ys)` 1181 \\ FULL_SIMP_TAC std_ss [LIST_SUBSET_def,EVERY_DEF,LET_DEF] 1182 \\ IMP_RES_TAC MEM_IMP_graph_SOME 1183 \\ FULL_SIMP_TAC std_ss [] 1184 \\ SIMP_TAC (srw_ss()) [exec_node_def,exec_next_def,upd_stack_def] 1185 \\ Cases_on `f st` \\ FULL_SIMP_TAC std_ss [next_ok_def] 1186 THEN1 (SRW_TAC [] [] \\ Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC) 1187 \\ Q.PAT_X_ASSUM `!xx.bbb` (MP_TAC o Q.SPECL [`k`,`k+4`,`n'`]) 1188 \\ `n' <> 0` by ALL_TAC THEN1 (IMP_RES_TAC exec_graph_step_NOT_ZERO) 1189 \\ FULL_SIMP_TAC std_ss [ODD_ADD,EVERY_APPEND] 1190 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1191 \\ IMP_RES_TAC good_stack_tail_STEP \\ FULL_SIMP_TAC std_ss [] 1192 \\ Q.LIST_EXISTS_TAC [`s4`,`s7`,`SUC j`,`j1`,`call`,`w`] 1193 \\ FULL_SIMP_TAC std_ss [] 1194 \\ REVERSE STRIP_TAC THEN1 DECIDE_TAC 1195 \\ REWRITE_TAC [NRC] 1196 \\ FULL_SIMP_TAC (srw_ss()) [exec_graph_step_def,exec_node_def,upd_stack_def]) 1197 THEN1 (SRW_TAC [] [] 1198 \\ Q.PAT_X_ASSUM `!xx.bbb` (MP_TAC o Q.SPECL [`k+2`,`t1`,`n'`]) 1199 \\ `ODD (k+2) /\ ODD (k+4)` by FULL_SIMP_TAC std_ss [ODD_ADD] 1200 \\ `n' <> 0` by ALL_TAC THEN1 (IMP_RES_TAC exec_graph_step_NOT_ZERO) 1201 \\ `ODD t1` by METIS_TAC [next_trans_lemma] 1202 \\ FULL_SIMP_TAC std_ss [ODD_ADD,EVERY_APPEND] 1203 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1204 \\ IMP_RES_TAC good_stack_tail_STEP \\ FULL_SIMP_TAC std_ss [] 1205 \\ Q.LIST_EXISTS_TAC [`s4`,`s7`,`SUC j`,`j1`,`call`,`w`] 1206 \\ FULL_SIMP_TAC std_ss [] 1207 \\ REVERSE STRIP_TAC THEN1 DECIDE_TAC 1208 \\ REWRITE_TAC [NRC] 1209 \\ FULL_SIMP_TAC (srw_ss()) [exec_graph_step_def,exec_node_def,upd_stack_def])) 1210 THEN1 (* ASM *) 1211 (Cases_on `^(mk_var("o'",``:32 assert option``))` THEN1 1212 (Cases_on `n` \\ FULL_SIMP_TAC std_ss [NRC] \\ REPEAT STRIP_TAC 1213 \\ Q.PAT_X_ASSUM `exec_graph_step (list_func_trans fs) 1214 ((NextNode i,st,name)::t) z` MP_TAC 1215 \\ ASM_SIMP_TAC (srw_ss()) [Once exec_graph_step_def] 1216 \\ FULL_SIMP_TAC std_ss [next_trans_def] 1217 \\ FULL_SIMP_TAC std_ss [LIST_SUBSET_def,EVERY_DEF] 1218 \\ IMP_RES_TAC MEM_IMP_graph_SOME 1219 \\ FULL_SIMP_TAC std_ss [] 1220 \\ SIMP_TAC (srw_ss()) [exec_node_def] 1221 \\ FULL_SIMP_TAC std_ss [upd_stack_def] 1222 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1223 \\ FULL_SIMP_TAC std_ss [exec_next_def] 1224 \\ Q.LIST_EXISTS_TAC [`z`,`SUC 0`,`n'`] 1225 \\ FULL_SIMP_TAC std_ss [assert_for_def,upd_vars_thm,next_ok_def] 1226 \\ FULL_SIMP_TAC std_ss [get_assert_def] 1227 \\ Q.EXISTS_TAC `(case get_jump j of 1228 NextNode n => n2w n 1229 | Ret => var_word "ret" (apply_update l st) 1230 | Err => var_word "ret" (apply_update l st))` 1231 \\ FULL_SIMP_TAC std_ss [] 1232 \\ REVERSE (REPEAT STRIP_TAC) 1233 THEN1 (REWRITE_TAC [NRC,DECIDE ``1 = SUC 0``] 1234 \\ FULL_SIMP_TAC (srw_ss()) [exec_graph_step_def,exec_node_def,upd_stack_def] 1235 \\ FULL_SIMP_TAC std_ss [upd_vars_thm]) 1236 THEN1 (Cases_on `j` 1237 \\ FULL_SIMP_TAC (srw_ss()) [get_jump_def,good_stack_def,EVERY_DEF] 1238 \\ FULL_SIMP_TAC std_ss [EVEN_DOUBLE,jump_ok_def] 1239 \\ MATCH_MP_TAC good_stack_tail_UPDATE 1240 \\ IMP_RES_TAC good_stack_tail_STEP 1241 \\ FULL_SIMP_TAC std_ss []) 1242 \\ Cases_on `j` 1243 \\ FULL_SIMP_TAC (srw_ss()) [check_jump_def,get_jump_def]) 1244 \\ Cases_on `n` \\ FULL_SIMP_TAC std_ss [NRC] \\ REPEAT STRIP_TAC 1245 \\ Q.PAT_X_ASSUM `exec_graph_step (list_func_trans fs) 1246 ((NextNode i,st,name)::t) z` MP_TAC 1247 \\ ASM_SIMP_TAC (srw_ss()) [Once exec_graph_step_def] 1248 \\ FULL_SIMP_TAC std_ss [next_trans_def] 1249 \\ FULL_SIMP_TAC std_ss [LIST_SUBSET_def,EVERY_DEF] 1250 \\ IMP_RES_TAC MEM_IMP_graph_SOME 1251 \\ FULL_SIMP_TAC std_ss [] 1252 \\ SIMP_TAC (srw_ss()) [exec_node_def,get_assert_def] 1253 \\ FULL_SIMP_TAC std_ss [upd_stack_def] 1254 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [next_ok_def] 1255 \\ Cases_on `x st` \\ FULL_SIMP_TAC std_ss [] 1256 \\ IMP_RES_TAC NRC_Err 1257 \\ Q.MATCH_ASSUM_RENAME_TAC `SUC n1 <> 0` 1258 \\ `n1 <> 0` by ALL_TAC THEN1 (IMP_RES_TAC exec_graph_step_NOT_ZERO) 1259 \\ Cases_on `n1` \\ FULL_SIMP_TAC std_ss [NRC] 1260 \\ Q.PAT_X_ASSUM `exec_graph_step (list_func_trans fs) 1261 ((NextNode _,st,name)::t) _` MP_TAC 1262 \\ ASM_SIMP_TAC (srw_ss()) [Once exec_graph_step_def] 1263 \\ SIMP_TAC (srw_ss()) [exec_node_def,upd_stack_def] 1264 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [exec_next_def] 1265 \\ Q.LIST_EXISTS_TAC [`z'`,`SUC (SUC 0)`,`n`] 1266 \\ FULL_SIMP_TAC std_ss [assert_for_def,upd_vars_thm,next_ok_def,get_assert_def] 1267 \\ FULL_SIMP_TAC std_ss [] 1268 \\ Q.EXISTS_TAC `(case get_jump j of 1269 NextNode n => n2w n 1270 | Ret => var_word "ret" (apply_update l st) 1271 | Err => var_word "ret" (apply_update l st))` 1272 \\ FULL_SIMP_TAC std_ss [] 1273 \\ REVERSE (REPEAT STRIP_TAC) THEN1 DECIDE_TAC 1274 THEN1 (REWRITE_TAC [NRC,DECIDE ``2 = SUC (SUC 0)``] 1275 \\ FULL_SIMP_TAC (srw_ss()) [exec_graph_step_def,exec_node_def,upd_stack_def] 1276 \\ FULL_SIMP_TAC std_ss [upd_vars_thm]) 1277 THEN1 (Cases_on `j` 1278 \\ FULL_SIMP_TAC (srw_ss()) [get_jump_def,good_stack_def,EVERY_DEF] 1279 \\ FULL_SIMP_TAC std_ss [EVEN_DOUBLE,jump_ok_def] 1280 \\ MATCH_MP_TAC good_stack_tail_UPDATE 1281 \\ IMP_RES_TAC good_stack_tail_STEP 1282 \\ FULL_SIMP_TAC std_ss []) 1283 \\ Cases_on `j` 1284 \\ FULL_SIMP_TAC (srw_ss()) [check_jump_def,get_jump_def]) 1285 THEN (* CALL *) Cases_on `n` \\ FULL_SIMP_TAC std_ss [NRC] \\ REPEAT STRIP_TAC 1286 \\ Q.PAT_X_ASSUM `exec_graph_step (list_func_trans fs) 1287 ((NextNode i,st,name)::t) z` MP_TAC 1288 \\ ASM_SIMP_TAC (srw_ss()) [Once exec_graph_step_def] 1289 \\ FULL_SIMP_TAC std_ss [next_trans_def] 1290 \\ FULL_SIMP_TAC std_ss [LIST_SUBSET_def,EVERY_DEF] 1291 \\ IMP_RES_TAC MEM_IMP_graph_SOME 1292 \\ FULL_SIMP_TAC std_ss [] 1293 \\ SIMP_TAC (srw_ss()) [exec_node_def] 1294 \\ REVERSE (Cases_on `get_assert o' st`) 1295 \\ FULL_SIMP_TAC std_ss [upd_stack_def] 1296 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1297 \\ IMP_RES_TAC NRC_Err 1298 \\ Q.MATCH_ASSUM_RENAME_TAC `SUC n1 <> 0` 1299 \\ `n1 <> 0` by ALL_TAC THEN1 (IMP_RES_TAC exec_graph_step_NOT_ZERO) 1300 \\ Cases_on `n1` \\ FULL_SIMP_TAC std_ss [NRC] 1301 \\ Q.PAT_X_ASSUM `exec_graph_step (list_func_trans fs) 1302 ((NextNode _,st,name)::t) _` MP_TAC 1303 \\ ASM_SIMP_TAC (srw_ss()) [Once exec_graph_step_def] 1304 \\ SIMP_TAC (srw_ss()) [exec_node_def,upd_stack_def] 1305 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [exec_next_def] 1306 \\ Cases_on `list_func_trans fs s` \\ FULL_SIMP_TAC std_ss [] 1307 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [] 1308 \\ IMP_RES_TAC NRC_Err 1309 \\ Q.ABBREV_TAC `n' = n` \\ POP_ASSUM (K ALL_TAC) 1310 \\ Cases_on `x` \\ FULL_SIMP_TAC (srw_ss()) [init_vars_def] 1311 \\ Q.MATCH_ASSUM_RENAME_TAC 1312 `list_func_trans fs s = SOME (GraphFunction inp out f n)` 1313 \\ `inp = ret_and_all_names` by ALL_TAC 1314 THEN1 (IMP_RES_TAC list_func_trans_EQ_SOME_IMP) 1315 \\ `fs_locs fs s = SOME (n2w n)` by ALL_TAC 1316 THEN1 (IMP_RES_TAC list_func_trans_EQ_SOME_IMP) 1317 \\ FULL_SIMP_TAC std_ss [check_jump_def] 1318 \\ Q.LIST_EXISTS_TAC [`z'`,`SUC (SUC 0)`,`n'`] 1319 \\ REVERSE (REPEAT STRIP_TAC) \\ FULL_SIMP_TAC std_ss [] 1320 THEN1 DECIDE_TAC 1321 THEN1 (REWRITE_TAC [NRC,DECIDE ``2 = SUC (SUC 0)``] 1322 \\ FULL_SIMP_TAC (srw_ss()) [exec_graph_step_def,exec_node_def, 1323 upd_stack_def] \\ FULL_SIMP_TAC std_ss [init_vars_def,MAP]) 1324 THEN1 1325 (ASM_SIMP_TAC (srw_ss()) [next_ok_def,good_stack_def,HD,FST] 1326 \\ IMP_RES_TAC good_stack_tail_STEP 1327 \\ ASM_SIMP_TAC (srw_ss()) [good_stack_tail_def] 1328 \\ `EVEN n` by ALL_TAC THEN1 1329 (IMP_RES_TAC list_func_trans_EQ_SOME_IMP 1330 \\ FULL_SIMP_TAC std_ss [EVEN_DOUBLE,jump_ok_def] 1331 \\ IMP_RES_TAC find_func_IMP_EVEN) 1332 \\ FULL_SIMP_TAC std_ss [next_ok_def] 1333 \\ Cases_on `j` 1334 \\ FULL_SIMP_TAC (srw_ss()) [get_jump_def,check_ret_def,EVEN_DOUBLE] 1335 \\ FULL_SIMP_TAC std_ss [RW1[MULT_COMM]MULT_DIV,n2w_w2n] 1336 \\ FULL_SIMP_TAC std_ss [ret_and_all_names_def] 1337 \\ FULL_SIMP_TAC std_ss [save_vals_lemma,jump_ok_def]) 1338 THEN1 (FULL_SIMP_TAC (srw_ss()) [assert_for_def] 1339 \\ AP_THM_TAC \\ AP_TERM_TAC 1340 \\ TRY (MATCH_MP_TAC arm_STATE_all_names) 1341 \\ TRY (MATCH_MP_TAC m0_STATE_all_names) 1342 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MAP_MAP_o,o_DEF] 1343 \\ FULL_SIMP_TAC std_ss [next_ok_def] 1344 \\ Q.PAT_X_ASSUM `MAP FST l = ret_and_all_names` (ASSUME_TAC o GSYM) 1345 \\ FULL_SIMP_TAC std_ss [save_vals_def,ZIP_MAP_MAP,fold_MAP] 1346 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MAP_MAP_o,o_DEF] 1347 \\ POP_ASSUM (ASSUME_TAC o GSYM) 1348 \\ REPEAT STRIP_TAC 1349 \\ MATCH_MP_TAC fold_EQ_apply_update 1350 \\ FULL_SIMP_TAC std_ss [] 1351 \\ FULL_SIMP_TAC std_ss [ret_and_all_names_def] 1352 \\ FULL_SIMP_TAC std_ss [MEM,all_names_def] \\ EVAL_TAC) 1353 \\ FULL_SIMP_TAC std_ss [next_ok_def]) end; 1354 1355fun exec_inst_progress arch = let 1356 val lemma = exec_graph_step_IMP_exec_next arch 1357 val (assert_for_def,code,tm) = 1358 if arch = "arm" then 1359 (arm_assert_for_def,``ARM code``, 1360 ``SPEC ARM_MODEL (arm_assert_for ((NextNode i,st,name)::t)) code 1361 (arm_assert_for s4)``) else 1362 if arch = "m0" then 1363 (m0_assert_for_def,``M0 code``, 1364 ``SPEC M0_MODEL (m0_assert_for ((NextNode i,st,name)::t)) code 1365 (m0_assert_for s4)``) else fail() 1366 in prove( 1367 ``NRC (exec_graph_step (list_func_trans fs)) n 1368 ((NextNode i,st,name)::t) s2 /\ funcs_ok ^code fs /\ 1369 (find_func name fs = SOME (Func name entry l)) /\ 1370 (find_inst (n2w i) l = SOME (Inst (n2w i) a next)) /\ 1371 (list_func_trans fs name = 1372 SOME (GraphFunction x1 x2 (graph nodes) x3)) /\ ODD k /\ 1373 LIST_SUBSET (SND (next_trans i k next)) nodes /\ 1374 ALL_DISTINCT (MAP FST nodes) /\ 1375 IMPL_INST ^code (fs_locs fs) (Inst (n2w i) (K T) next) /\ 1376 n <> 0 /\ good_stack fs ((NextNode i,st,name)::t) /\ good_stack fs s2 ==> 1377 ?s4 j j1. 1378 NRC (exec_graph_step (list_func_trans fs)) j 1379 ((NextNode i,st,name)::t) s4 /\ 1380 NRC (exec_graph_step (list_func_trans fs)) j1 s4 s2 /\ j1 < n /\ 1381 good_stack fs s4 /\ ^tm``, 1382 SIMP_TAC (srw_ss()) [IMPL_INST_def] \\ REPEAT STRIP_TAC 1383 \\ FULL_SIMP_TAC (srw_ss()) [assert_for_def] 1384 \\ FULL_SIMP_TAC std_ss [RW1[MULT_COMM]MULT_DIV] 1385 \\ MP_TAC (lemma |> SPEC_ALL) 1386 \\ FULL_SIMP_TAC std_ss [] 1387 \\ FULL_SIMP_TAC std_ss [good_stack_def] 1388 \\ REPEAT STRIP_TAC \\ RES_TAC 1389 \\ fs [ARM_def,M0_def,RISCV_def] 1390 \\ Q.LIST_EXISTS_TAC [`s4`,`j`,`j1`] \\ FULL_SIMP_TAC std_ss []) end; 1391 1392fun exec_func_step_IMP arch = let 1393 val lemma = exec_inst_progress arch 1394 val (assert_for_def,code,assert_for_tm,model_tm) = 1395 if arch = "arm" then 1396 (arm_assert_for_def,``ARM code``,``arm_assert_for``,``ARM_MODEL``) else 1397 if arch = "m0" then 1398 (m0_assert_for_def,``M0 code``,``m0_assert_for``,``M0_MODEL``) else 1399 fail() 1400 in prove( 1401 ``funcs_ok ^code fs ==> 1402 !n s1 s2. 1403 good_stack fs s1 /\ good_stack fs s2 /\ 1404 exec_graph_n (list_func_trans fs) n s1 s2 ==> 1405 SPEC ^model_tm (^assert_for_tm s1) code (^assert_for_tm s2)``, 1406 STRIP_TAC 1407 \\ completeInduct_on `n` \\ Cases_on `n = 0` 1408 \\ FULL_SIMP_TAC std_ss [exec_graph_n_def,NRC,SPEC_REFL] 1409 \\ REPEAT STRIP_TAC 1410 \\ `?s3. NRC (exec_graph_step (list_func_trans fs)) (n-1) s3 s2 /\ 1411 exec_graph_step (list_func_trans fs) s1 s3` by 1412 (Cases_on `n` \\ FULL_SIMP_TAC std_ss [exec_graph_n_def,NRC] \\ METIS_TAC []) 1413 \\ POP_ASSUM MP_TAC 1414 \\ SIMP_TAC (srw_ss()) [exec_graph_step_def] 1415 \\ Cases_on `s1` \\ FULL_SIMP_TAC (srw_ss()) [] 1416 \\ `?l st name. h = (l,st,name)` by METIS_TAC [PAIR] 1417 \\ REVERSE (Cases_on `l`) \\ FULL_SIMP_TAC (srw_ss()) [] 1418 THEN1 (FULL_SIMP_TAC (srw_ss()) [good_stack_def,EVERY_DEF]) 1419 THEN1 1420 (Cases_on `t` \\ FULL_SIMP_TAC (srw_ss()) [] 1421 \\ `?l1 st1 name1. h' = (l1,st1,name1)` by METIS_TAC [PAIR] 1422 \\ FULL_SIMP_TAC (srw_ss()) [upd_stack_def] 1423 \\ REVERSE (Cases_on `l1`) \\ FULL_SIMP_TAC (srw_ss()) [] 1424 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1425 THEN1 IMP_RES_TAC NRC_Err THEN1 IMP_RES_TAC NRC_Err 1426 \\ Cases_on `list_func_trans fs name1` \\ FULL_SIMP_TAC (srw_ss()) [] 1427 \\ Cases_on `x` \\ FULL_SIMP_TAC (srw_ss()) [] 1428 \\ Q.MATCH_ASSUM_RENAME_TAC `list_func_trans fs name1 = 1429 SOME (GraphFunction x1 x2 graph1 x3)` 1430 \\ Cases_on `graph1 n'` \\ FULL_SIMP_TAC (srw_ss()) [] 1431 THEN1 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [upd_stack_def] 1432 \\ IMP_RES_TAC NRC_Err) 1433 \\ Cases_on `x` \\ FULL_SIMP_TAC (srw_ss()) [exec_node_return_def] 1434 \\ Cases_on `list_func_trans fs s` \\ FULL_SIMP_TAC (srw_ss()) [] 1435 \\ Cases_on `x` \\ FULL_SIMP_TAC (srw_ss()) [exec_node_return_def] 1436 \\ FULL_SIMP_TAC std_ss [upd_stack_def] 1437 \\ CONV_TAC ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM UNION_IDEMPOT])) 1438 \\ MATCH_MP_TAC SPEC_COMPOSE 1439 \\ Q.EXISTS_TAC `^assert_for_tm s3` 1440 \\ `(^assert_for_tm ((Ret,st,name)::(NextNode n',st1,name1)::t') = 1441 ^assert_for_tm s3) /\ good_stack fs s3` by ALL_TAC THEN1 1442 (Q.MATCH_ASSUM_RENAME_TAC `list_func_trans fs name2 = 1443 SOME (GraphFunction y1 y2 graph2 y3)` 1444 \\ FULL_SIMP_TAC std_ss [] 1445 \\ Q.PAT_ASSUM `good_stack fs (xx::yy::tt)` MP_TAC 1446 \\ SIMP_TAC (srw_ss()) [good_stack_def,good_stack_tail_def,HD,FST] 1447 \\ STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [] 1448 \\ Q.PAT_ASSUM `g = graph1` ASSUME_TAC \\ FULL_SIMP_TAC (srw_ss()) [] 1449 \\ NTAC 6 (POP_ASSUM MP_TAC) \\ FULL_SIMP_TAC std_ss [] 1450 \\ REPEAT (POP_ASSUM (fn th => if is_eq (concl th) then ALL_TAC else NO_TAC)) 1451 \\ NTAC 6 STRIP_TAC 1452 \\ Q.MATCH_ASSUM_RENAME_TAC `graph1 n1 = SOME (Call ret name2 l l0)` 1453 \\ `(y2 = all_names_with_input) /\ (l0 = all_names_ignore)` by ALL_TAC THEN1 1454 (IMP_RES_TAC list_func_trans_EQ_SOME_IMP 1455 \\ FULL_SIMP_TAC std_ss [] 1456 \\ IMP_RES_TAC graph_SOME_IMP 1457 \\ IMP_RES_TAC MEM_Call_list_inst_trans) 1458 \\ FULL_SIMP_TAC std_ss [] 1459 \\ REVERSE (REPEAT STRIP_TAC) 1460 THEN1 (Cases_on `ret` \\ FULL_SIMP_TAC (srw_ss()) []) 1461 THEN1 (MATCH_MP_TAC good_stack_tail_return_vars 1462 \\ IMP_RES_TAC good_stack_tail_STEP \\ FULL_SIMP_TAC std_ss []) 1463 \\ FULL_SIMP_TAC std_ss [assert_for_def] 1464 \\ MATCH_MP_TAC (METIS_PROVE [] ``(f1 = f2) /\ (x1 = x2) ==> (f1 x1 = f2 x2)``) 1465 \\ STRIP_TAC THEN1 1466 (AP_TERM_TAC 1467 \\ TRY (MATCH_MP_TAC arm_STATE_all_names) 1468 \\ TRY (MATCH_MP_TAC m0_STATE_all_names) 1469 \\ FULL_SIMP_TAC std_ss [EVERY_MEM] 1470 \\ METIS_TAC [return_vars_SAME]) 1471 \\ Cases_on `ret` \\ FULL_SIMP_TAC (srw_ss()) [] 1472 \\ AP_TERM_TAC 1473 \\ FULL_SIMP_TAC std_ss [var_word_def,var_acc_def,return_vars_def, 1474 save_vals_def,fold_def,var_upd_def,all_names_def] \\ EVAL_TAC 1475 \\ FULL_SIMP_TAC std_ss [var_word_def,var_acc_def,return_vars_def, 1476 save_vals_def,fold_def,var_upd_def] \\ EVAL_TAC) 1477 \\ FULL_SIMP_TAC std_ss [SPEC_REFL,PULL_FORALL,AND_IMP_INTRO] 1478 \\ FIRST_X_ASSUM MATCH_MP_TAC 1479 \\ Q.EXISTS_TAC `n-1` \\ FULL_SIMP_TAC std_ss [] 1480 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [] 1481 \\ REPEAT STRIP_TAC \\ DECIDE_TAC) 1482 \\ Cases_on `list_func_trans fs name` \\ FULL_SIMP_TAC (srw_ss()) [] 1483 \\ Cases_on `x` \\ FULL_SIMP_TAC (srw_ss()) [] 1484 \\ Q.MATCH_ASSUM_RENAME_TAC `list_func_trans fs name = 1485 SOME (GraphFunction x1 x2 graph1 x3)` 1486 \\ Cases_on `graph1 n'` \\ FULL_SIMP_TAC (srw_ss()) [] 1487 THEN1 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [upd_stack_def] 1488 \\ IMP_RES_TAC NRC_Err) 1489 \\ FULL_SIMP_TAC (srw_ss()) [] 1490 \\ IMP_RES_TAC list_func_trans_EQ_SOME_IMP 1491 \\ FULL_SIMP_TAC std_ss [] \\ SRW_TAC [] [] 1492 \\ `EVEN n'` by ALL_TAC THEN1 (FULL_SIMP_TAC (srw_ss()) [good_stack_def]) 1493 \\ `n' < 2 ** 32` by 1494 (IMP_RES_TAC list_inst_trans_IMP_LESS 1495 \\ FULL_SIMP_TAC std_ss [] \\ fs []) 1496 \\ fs [] 1497 \\ IMP_RES_TAC (graph_list_inst_trans_EQ_SOME_IMP 1498 |> INST_TYPE [``:'a``|->``:32``] 1499 |> SIMP_RULE (srw_ss()) []) 1500 \\ FULL_SIMP_TAC std_ss [] 1501 \\ Q.MATCH_ASSUM_RENAME_TAC `graph (list_inst_trans 1 l) i = SOME x` 1502 \\ Q.MATCH_ASSUM_RENAME_TAC `find_inst (n2w i) l = SOME (Inst (n2w i) a next)` 1503 \\ FULL_SIMP_TAC std_ss [funcs_ok_def,EVERY_MEM] 1504 \\ IMP_RES_TAC find_func_IMP_MEM 1505 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [func_ok_def] 1506 \\ IMP_RES_TAC find_inst_IMP_MEM 1507 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 1508 \\ `i < 4294967296` by DECIDE_TAC 1509 \\ IMP_RES_TAC (find_inst_IMP_LIST_SUBSET 1510 |> INST_TYPE [``:'a``|->``:32``] 1511 |> SIMP_RULE (srw_ss()) []) 1512 \\ MP_TAC (lemma 1513 |> Q.INST [`x1`|->`ret_and_all_names`, 1514 `x2`|->`all_names_with_input`, 1515 `k`|->`k2`, 1516 `x3`|->`w2n entry`, 1517 `nodes`|->`list_inst_trans 1 l`]) 1518 \\ FULL_SIMP_TAC (srw_ss()) [funcs_ok_def,EVERY_MEM] 1519 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 1520 (MATCH_MP_TAC ALL_DISTINCT_list_inst_trans 1521 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,IMPL_INST_def,func_ok_def] 1522 \\ Cases \\ REPEAT STRIP_TAC \\ RES_TAC 1523 \\ FULL_SIMP_TAC std_ss [inst_loc_def]) 1524 \\ REPEAT STRIP_TAC 1525 \\ CONV_TAC ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM UNION_IDEMPOT])) 1526 \\ MATCH_MP_TAC SPEC_COMPOSE 1527 \\ Q.EXISTS_TAC `(^assert_for_tm s4)` \\ FULL_SIMP_TAC std_ss [] 1528 \\ FULL_SIMP_TAC std_ss [SPEC_REFL,PULL_FORALL,AND_IMP_INTRO] 1529 \\ FIRST_X_ASSUM MATCH_MP_TAC 1530 \\ Q.EXISTS_TAC `j1` \\ FULL_SIMP_TAC std_ss []) end 1531 1532val _ = save_thm("arm_exec_func_step_IMP", exec_func_step_IMP "arm"); 1533val _ = save_thm("m0_exec_func_step_IMP", exec_func_step_IMP "m0"); 1534 1535(* misc lemmas *) 1536 1537val LIST_IMPL_INST_def = Define ` 1538 (LIST_IMPL_INST code names [] = T) /\ 1539 (LIST_IMPL_INST code names ((Inst i assert next)::xs) = 1540 IMPL_INST code names (Inst i assert next) /\ (assert = K T) /\ 1541 LIST_IMPL_INST code names xs)`; 1542 1543val IMP_LIST_IMPL_INST = store_thm("IMP_LIST_IMPL_INST", 1544 ``IMPL_INST code names (Inst i (K T) next) /\ 1545 LIST_IMPL_INST code names xs ==> 1546 LIST_IMPL_INST code names ((Inst i (K T) next)::xs)``, 1547 SIMP_TAC std_ss [LIST_IMPL_INST_def]); 1548 1549val IMP_func_ok = store_thm("IMP_func_ok", 1550 ``!insts. LIST_IMPL_INST code names insts ==> 1551 ALL_DISTINCT (MAP inst_loc insts) /\ EVEN (w2n entry) ==> 1552 func_ok code names (Func name entry insts)``, 1553 SIMP_TAC std_ss [func_ok_def] \\ Induct 1554 \\ FULL_SIMP_TAC std_ss [LIST_IMPL_INST_def,MAP,ALL_DISTINCT,MEM] \\ Cases 1555 \\ FULL_SIMP_TAC std_ss [LIST_IMPL_INST_def,MAP,ALL_DISTINCT,MEM,inst_loc_def] 1556 \\ REPEAT STRIP_TAC 1557 \\ RES_TAC \\ FULL_SIMP_TAC (srw_ss()) []); 1558 1559val IMP_EVERY_func_ok = store_thm("IMP_EVERY_func_ok", 1560 ``func_ok code locs f /\ 1561 EVERY (func_ok code locs) fs ==> 1562 EVERY (func_ok code locs) (f::fs)``, 1563 FULL_SIMP_TAC std_ss [EVERY_DEF]); 1564 1565val _ = wordsLib.guess_lengths () 1566 1567val word32_def = Define ` 1568 (word32 (b1:word8) (b2:word8) (b3:word8) (b4:word8)) :word32 = 1569 b1 @@ b2 @@ b3 @@ b4`; 1570 1571val word64_def = Define ` 1572 (word64 (b1:word8) (b2:word8) (b3:word8) (b4:word8) 1573 (b5:word8) (b6:word8) (b7:word8) (b8:word8)) :word64 = 1574 b1 @@ b2 @@ b3 @@ b4 @@ b5 @@ b6 @@ b7 @@ b8`; 1575 1576val READ32_def = zDefine ` 1577 READ32 a mem = word32 (mem (a + 3w)) (mem (a + 2w)) (mem (a + 1w)) (mem a)`; 1578 1579val READ64_def = zDefine ` 1580 READ64 a mem = 1581 word64 (mem (a + 7w)) (mem (a + 6w)) (mem (a + 5w)) (mem (a + 4w)) 1582 (mem (a + 3w)) (mem (a + 2w)) (mem (a + 1w)) (mem a)`; 1583 1584val READ8_def = zDefine ` 1585 READ8 a mem = (mem:'a word -> word8) a`; 1586 1587val WRITE32_def = zDefine ` 1588 WRITE32 (a:word32) (w:word32) (mem:word32->word8) = 1589 (a =+ w2w w) 1590 ((a + 1w =+ w2w (w >>> 8)) 1591 ((a + 2w =+ w2w (w >>> 16)) 1592 ((a + 3w =+ w2w (w >>> 24)) mem)))`; 1593 1594val WRITE64_def = zDefine ` 1595 WRITE64 (a:word64) (w:word64) (mem:word64->word8) = 1596 (a =+ w2w w) 1597 ((a + 1w =+ w2w (w >>> 8)) 1598 ((a + 2w =+ w2w (w >>> 16)) 1599 ((a + 3w =+ w2w (w >>> 24)) 1600 ((a + 4w =+ w2w (w >>> 32)) 1601 ((a + 5w =+ w2w (w >>> 40)) 1602 ((a + 6w =+ w2w (w >>> 48)) 1603 ((a + 7w =+ w2w (w >>> 56)) mem)))))))`; 1604 1605val WRITE8_def = zDefine ` 1606 WRITE8 (a:'a word) (w:word8) (mem:'a word->word8) = (a =+ w) mem`; 1607 1608val READ32_expand64 = store_thm("READ32_expand64", 1609 ``READ32 (a:word64) m = 1610 w2w (READ8 a m) || 1611 (w2w (READ8 (a+1w) m) << 8) || 1612 (w2w (READ8 (a+2w) m) << 16) || 1613 (w2w (READ8 (a+3w) m) << 24)``, 1614 fs [READ32_def,READ8_def,word32_def] \\ blastLib.BBLAST_TAC); 1615 1616val func_name_def = Define ` 1617 func_name (Func name entry l) = name`; 1618 1619val func_body_trans_def = zDefine ` 1620 func_body_trans f = SND (func_trans f)`; 1621 1622val list_func_trans_thm = store_thm("list_func_trans_thm", 1623 ``list_func_trans fs = 1624 graph (MAP (\f. (func_name f, func_body_trans f)) fs)``, 1625 SIMP_TAC std_ss [list_func_trans_def] \\ AP_TERM_TAC 1626 \\ Induct_on `fs` \\ FULL_SIMP_TAC std_ss [MAP] \\ Cases 1627 \\ FULL_SIMP_TAC std_ss [func_name_def,func_trans_def,func_body_trans_def]); 1628 1629val word_extract_thm = store_thm("word_extract_thm", 1630 ``((7 >< 0) (w:word32) = (w2w w):word8) /\ 1631 ((15 >< 8) (w:word32) = (w2w (w >>> 8)):word8) /\ 1632 ((23 >< 16) (w:word32) = (w2w (w >>> 16)):word8) /\ 1633 ((31 >< 24) (w:word32) = (w2w (w >>> 24)):word8) /\ 1634 ((31 >< 0) (v:word64) = ((w2w v):word32)) /\ 1635 ((63 >< 32) (v:word64) = ((w2w (v >>> 32)):word32))``, 1636 blastLib.BBLAST_TAC); 1637 1638val n2w_lsr = 1639 ``n2w (w2n ((w:'a word) >>> m)):'a word`` 1640 |> SIMP_CONV std_ss [w2n_lsr] |> RW [n2w_w2n] 1641 1642val Align_lemma = prove( 1643 ``!w. (arm$Align (w,2) = w >>> 1 << 1) /\ 1644 (m0$Align (w,2) = w >>> 1 << 1) /\ 1645 (arm$Align (w,4) = w >>> 2 << 2) /\ 1646 (m0$Align (w,4) = w >>> 2 << 2)``, 1647 Cases \\ SIMP_TAC std_ss [n2w_lsr,armTheory.Align_def, 1648 m0Theory.Align_def,w2n_n2w,WORD_MUL_LSL,word_mul_n2w]); 1649 1650val REMOVE_Align = store_thm("REMOVE_Align", 1651 ``!w. ALIGNED w ==> 1652 (arm$Align (w,2) = w) /\ (arm$Align (w,4) = w) /\ 1653 (m0$Align (w,2) = w) /\ (m0$Align (w,4) = w)``, 1654 SIMP_TAC std_ss [Align_lemma,ALIGNED_def] \\ blastLib.BBLAST_TAC); 1655 1656val byte_lemma = prove( 1657 ``(((b1:word8) @@ (b2:word8)):word16 = w2w b1 << 8 || w2w b2) /\ 1658 (((h1:word16) @@ (b2:word8)):24 word = w2w h1 << 8 || w2w b2) /\ 1659 (((b1:word8) @@ (h2:word16)):24 word = w2w b1 << 16 || w2w h2) /\ 1660 (((h1:word16) @@ (h2:word16)):word32 = w2w h1 << 16 || w2w h2)``, 1661 blastLib.BBLAST_TAC); 1662 1663val lemma = blastLib.BBLAST_PROVE 1664 ``(w && 1w = 0w) <=> ~(w:word32) ' 0`` 1665 1666val Aligned2_thm = prove( 1667 ``(arm$Aligned (w:word32,2) = (w && 1w = 0w)) /\ 1668 (m0$Aligned (w:word32,2) = (w && 1w = 0w))``, 1669 FULL_SIMP_TAC std_ss [lemma] 1670 \\ SIMP_TAC std_ss [armTheory.Aligned_def,m0Theory.Aligned_def, 1671 armTheory.Align_def,m0Theory.Align_def,ALIGNED_INTRO] 1672 \\ Cases_on `w` \\ FULL_SIMP_TAC (srw_ss()) [ALIGNED_n2w] 1673 \\ FULL_SIMP_TAC (srw_ss()) [wordsTheory.word_index, 1674 bitTheory.BIT_def, bitTheory.BITS_THM] 1675 \\ `(2 * (n DIV 2)) < 4294967296` by ALL_TAC THEN1 1676 (SIMP_TAC bool_ss [GSYM (EVAL ``2 * 2147483648:num``),LT_MULT_LCANCEL] 1677 \\ FULL_SIMP_TAC std_ss [DIV_LT_X]) 1678 \\ FULL_SIMP_TAC std_ss [] 1679 \\ ASSUME_TAC (DIVISION |> Q.SPEC `2` |> SIMP_RULE std_ss [] 1680 |> GSYM |> Q.SPEC `n`) 1681 \\ Cases_on `n MOD 2 = 0` \\ FULL_SIMP_TAC std_ss [] 1682 \\ FULL_SIMP_TAC std_ss [AC MULT_COMM MULT_ASSOC] 1683 \\ `n MOD 2 < 2` by FULL_SIMP_TAC std_ss [] 1684 \\ DECIDE_TAC); 1685 1686val Aligned_thm = prove( 1687 ``(arm$Aligned (w:word32,4) = (w && 3w = 0w)) /\ 1688 (m0$Aligned (w:word32,4) = (w && 3w = 0w))``, 1689 SIMP_TAC std_ss [armTheory.Aligned_def,m0Theory.Aligned_def, 1690 armTheory.Align_def,m0Theory.Align_def,ALIGNED_INTRO] 1691 \\ Cases_on `w` \\ FULL_SIMP_TAC (srw_ss()) [ALIGNED_n2w] 1692 \\ `(4 * (n DIV 4)) < 4294967296` by ALL_TAC THEN1 1693 (SIMP_TAC bool_ss [GSYM (EVAL ``4 * 1073741824:num``),LT_MULT_LCANCEL] 1694 \\ FULL_SIMP_TAC std_ss [DIV_LT_X]) 1695 \\ FULL_SIMP_TAC std_ss [] 1696 \\ ASSUME_TAC (DIVISION |> Q.SPEC `4` |> SIMP_RULE std_ss [] |> GSYM |> Q.SPEC `n`) 1697 \\ Cases_on `n MOD 4 = 0` \\ FULL_SIMP_TAC std_ss [] 1698 \\ FULL_SIMP_TAC std_ss [AC MULT_COMM MULT_ASSOC] \\ DECIDE_TAC); 1699 1700val w2n_eq = prove( 1701 ``!w. (w2n w = 0) <=> (w = 0w)``, 1702 Cases \\ FULL_SIMP_TAC (srw_ss()) []); 1703 1704val decomp_simp1 = prove( 1705 ``(K x y = x) /\ (SUC n = n + 1)``, 1706 SIMP_TAC std_ss [FUN_EQ_THM,ADD1]); 1707 1708val decomp_simp1 = save_thm("decomp_simp1", 1709 LIST_CONJ [GSYM word32_def,Aligned_thm,Aligned2_thm,ALIGNED, 1710 decomp_simp1,word_extract_thm,word_bits_mask,word_extract_w2w_mask, 1711 ALIGNED_INTRO,w2n_eq,byte_lemma]) 1712 1713val decomp_simp2 = store_thm("decomp_simp2", 1714 ``(K x = \y. x) /\ (SUC = \n. n + 1)``, 1715 SIMP_TAC std_ss [FUN_EQ_THM,ADD1]); 1716 1717val decomp_simp3 = store_thm("decomp_simp3", 1718 ``(K = \x y. x) /\ (ALIGNED x = (x && 3w = 0w)) /\ 1719 (REV xs [] = REVERSE xs)``, 1720 SIMP_TAC std_ss [FUN_EQ_THM,ALIGNED_def] \\ EVAL_TAC); 1721 1722val CALL_TAG_def = Define ` 1723 CALL_TAG (s:string) (is_tail_call:bool) = T`; 1724 1725val unspecified_pre_def = zDefine `unspecified_pre = F`; 1726 1727val SKIP_TAG_def = zDefine ` 1728 SKIP_TAG (s:string) = unspecified_pre`; 1729 1730val SKIP_SPEC_ARM = store_thm("SKIP_SPEC_ARM", 1731 ``!asm n. 1732 SPEC ARM_MODEL (arm_PC p * cond (SKIP_TAG asm)) {} (arm_PC (p + n2w n))``, 1733 SIMP_TAC std_ss [SKIP_TAG_def,SPEC_MOVE_COND,unspecified_pre_def]); 1734 1735val SKIP_SPEC_M0 = store_thm("SKIP_SPEC_M0", 1736 ``!asm n. 1737 SPEC ARM_MODEL (arm_PC p * cond (SKIP_TAG asm)) {} (arm_PC (p + n2w n))``, 1738 SIMP_TAC std_ss [SKIP_TAG_def,SPEC_MOVE_COND,unspecified_pre_def]); 1739 1740val SKIP_SPEC_RISCV = store_thm("SKIP_SPEC_RISCV", 1741 ``!asm n. 1742 SPEC RISCV_MODEL (riscv_PC p * cond (SKIP_TAG asm)) {} (riscv_PC (p + n2w n))``, 1743 SIMP_TAC std_ss [SKIP_TAG_def,SPEC_MOVE_COND,unspecified_pre_def]); 1744 1745val fake_spec = store_thm("fake_spec", 1746 ``SPEC ARM_MODEL (aPC p * aR 0w r0 * cond (unspecified_pre)) {} 1747 (aR 0w ARB * aPC (p + 4w))``, 1748 SIMP_TAC std_ss [unspecified_pre_def,SPEC_MOVE_COND]); 1749 1750val WORD_LEMMA = prove( 1751 ``(a - l = w) = (l = a - w:word32)``, 1752 blastLib.BBLAST_TAC); 1753 1754val SP_LEMMA = store_thm("SP_LEMMA", 1755 ``((a - n2w (l + n) * 4w = r13 - 4w * n2w l) ==> b) ==> 1756 ALIGNED a /\ ALIGNED r13 /\ (n = w2n (a - r13:word32) DIV 4) ==> b``, 1757 Cases_on `b` \\ FULL_SIMP_TAC std_ss [] 1758 \\ REPEAT STRIP_TAC \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] 1759 \\ FULL_SIMP_TAC std_ss [Once ADD_COMM] 1760 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_RIGHT_ADD_DISTRIB] 1761 \\ FULL_SIMP_TAC std_ss [WORD_SUB_PLUS] 1762 \\ FULL_SIMP_TAC std_ss [AC WORD_MULT_ASSOC WORD_MULT_COMM] 1763 \\ FULL_SIMP_TAC std_ss [WORD_LCANCEL_SUB] 1764 \\ FULL_SIMP_TAC std_ss [WORD_LEMMA] 1765 \\ `ALIGNED (a - r13)` by METIS_TAC [ALIGNED_SUB] 1766 \\ Cases_on `a - r13` 1767 \\ FULL_SIMP_TAC std_ss [w2n_n2w,ALIGNED_n2w,word_mul_n2w] 1768 \\ MP_TAC (MATCH_MP DIVISION (DECIDE ``0<4:num``) |> Q.SPEC `n'`) 1769 \\ FULL_SIMP_TAC std_ss [AC MULT_COMM MULT_ASSOC] 1770 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ REPEAT STRIP_TAC 1771 \\ FULL_SIMP_TAC std_ss []); 1772 1773val ALIGNED_IMP_BITS_01 = store_thm("ALIGNED_IMP_BITS_01", 1774 ``ALIGNED w ==> ~(w ' 0) /\ ~(w ' 1)``, 1775 SIMP_TAC std_ss [ALIGNED_def] \\ blastLib.BBLAST_TAC); 1776 1777val BITS_01_IMP_ALIGNED = store_thm("BITS_01_IMP_ALIGNED", 1778 ``~(w ' 0) /\ ~(w ' 1) ==> ((b ==> ALIGNED w) <=> ALIGNED w)``, 1779 SIMP_TAC std_ss [ALIGNED_def] \\ blastLib.BBLAST_TAC); 1780 1781val ALIGNED_Align = store_thm("ALIGNED_Align", 1782 ``(ALIGNED (arm$Align (w,2)) = ~(w ' 1)) /\ 1783 (ALIGNED (arm$Align (w,4)) = T) /\ 1784 (ALIGNED (m0$Align (w,2)) = ~(w ' 1)) /\ 1785 (ALIGNED (m0$Align (w,4)) = T)``, 1786 SIMP_TAC std_ss [Align_lemma,ALIGNED_def] \\ blastLib.BBLAST_TAC); 1787 1788val carry_out_def = zDefine ` 1789 carry_out w1 w2 c = CARRY_OUT w1 w2 c`; 1790 1791val OVERFLOW_EQ = store_thm("OVERFLOW_EQ", 1792 ``OVERFLOW x y c = 1793 (word_msb x = word_msb y) /\ 1794 (word_msb x <> word_msb (if c then x - ~y else x + y))``, 1795 SIMP_TAC std_ss [add_with_carry_def,LET_DEF] 1796 \\ Cases_on `x` \\ Cases_on `y` \\ FULL_SIMP_TAC std_ss [] 1797 \\ Cases_on `c` \\ FULL_SIMP_TAC std_ss [w2n_n2w,word_add_n2w] 1798 \\ FULL_SIMP_TAC std_ss [word_sub_def,WORD_NEG,WORD_NOT_NOT] 1799 \\ FULL_SIMP_TAC std_ss [ADD_ASSOC,word_add_n2w]); 1800 1801val BIT_31 = prove( 1802 ``BIT 31 m = ((m DIV 2**31) MOD 2 = 1)``, 1803 SIMP_TAC std_ss [bitTheory.BIT_def,bitTheory.BITS_THM]); 1804 1805val word32_msb_n2w = store_thm("word32_msb_n2w", 1806 ``word_msb ((n2w n):word32) = ((n DIV 2**31) MOD 2 = 1)``, 1807 SIMP_TAC (srw_ss()) [word_msb_n2w,BIT_31]); 1808 1809val count_leading_zero_bits_def = zDefine ` 1810 count_leading_zero_bits (w:'a word) = 1811 (n2w (arm$CountLeadingZeroBits w)):'a word`; 1812 1813val count_leading_zero_bits_thm = 1814 store_thm("count_leading_zero_bits_thm", 1815 ``(n2w (arm$CountLeadingZeroBits w) = count_leading_zero_bits w) /\ 1816 (n2w (m0$CountLeadingZeroBits w) = count_leading_zero_bits w)``, 1817 FULL_SIMP_TAC std_ss [m0Theory.CountLeadingZeroBits_def, 1818 armTheory.CountLeadingZeroBits_def,count_leading_zero_bits_def, 1819 armTheory.HighestSetBit_def,m0Theory.HighestSetBit_def]); 1820 1821val word_add_with_carry_def = zDefine ` 1822 word_add_with_carry (w1:'a word) w2 c = 1823 FST (add_with_carry (w1,w2,c))`; 1824 1825(* graph format helpers *) 1826 1827val MemAcc8_def = Define ` 1828 MemAcc8 m a = READ8 a m`; 1829 1830val MemAcc32_def = Define ` 1831 MemAcc32 m a = READ32 a (m:word32->word8)`; 1832 1833val MemAcc64_def = Define ` 1834 MemAcc64 m a = READ64 a (m:word64->word8)`; 1835 1836val MemUpdate8_def = Define ` 1837 MemUpdate8 m a w = WRITE8 a w m`; 1838 1839val MemUpdate32_def = Define ` 1840 MemUpdate32 m a w = WRITE32 a w (m:word32->word8)`; 1841 1842val MemUpdate64_def = Define ` 1843 MemUpdate64 m a w = WRITE64 a w (m:word64->word8)`; 1844 1845val ShiftLeft_def = Define ` 1846 ShiftLeft (w:'a word) (y:'a word) = word_lsl w (w2n y)`; 1847 1848val ShiftRight_def = Define ` 1849 ShiftRight (w:'a word) (y:'a word) = word_lsr w (w2n y)`; 1850 1851val SignedShiftRight_def = Define ` 1852 SignedShiftRight (w:'a word) (y:'a word) = word_asr w (w2n y)`; 1853 1854val w2w_carry_alt = prove( 1855 ``((w2w:word32 -> 33 word) (w1:word32) << w2n ((w2w (w2:word32)):word8)) ' 32 <=> 1856 (ShiftLeft ((w2w:word32 -> word64) (w1:word32)) 1857 (w2w ((w2w:word32->word8) w2))) ' 32``, 1858 FULL_SIMP_TAC (srw_ss()) [ShiftLeft_def] 1859 \\ `w2n ((w2w:word8->word64) (w2w w2)) = w2n ((w2w w2):word8)` by 1860 (FULL_SIMP_TAC (srw_ss()) [w2w_def] 1861 \\ MATCH_MP_TAC LESS_TRANS \\ Q.EXISTS_TAC `256` 1862 \\ FULL_SIMP_TAC (srw_ss()) []) 1863 \\ FULL_SIMP_TAC (srw_ss()) [word_lsl_def,fcpTheory.FCP_BETA] 1864 \\ Q.ABBREV_TAC `n = w2n ((w2w:word32->word8) w2)` 1865 \\ Cases_on `n <= 32` \\ FULL_SIMP_TAC (srw_ss()) [] 1866 \\ `32 - n < dimindex (:33) /\ 32 - n < dimindex (:64)` by 1867 (FULL_SIMP_TAC (srw_ss()) [] \\ DECIDE_TAC) 1868 \\ FULL_SIMP_TAC std_ss [wordsTheory.w2w]); 1869 1870val w2w_carry = prove( 1871 ``EVERY (\i. (((w2w (w:word32) << i):33 word) ' 32) <=> 1872 ((w && n2w (2 ** (32 - i))) <> 0w)) (GENLIST I 32)``, 1873 FULL_SIMP_TAC (srw_ss()) [EVAL ``GENLIST I 32``,EVERY_DEF, 1874 ShiftLeft_def,ShiftRight_def,w2n_n2w] \\ blastLib.BBLAST_TAC) |> SIMP_RULE std_ss [EVAL ``GENLIST I 32``,EVERY_DEF]; 1875 1876val rw16 = prove( 1877 ``EVERY (\i. ((w:word16) ' i = ((w && n2w (2 ** i)) <> 0w)) /\ 1878 (word_bit i w = ((w && n2w (2 ** i)) <> 0w)) /\ 1879 (word_lsr w i = ShiftRight w ((n2w i):word16)) /\ 1880 (word_asr w i = SignedShiftRight w ((n2w i):word16)) /\ 1881 (word_lsl w i = ShiftLeft w ((n2w i):word16))) (GENLIST I 16) /\ 1882 (word_msb w = (w:word16) ' 15)``, 1883 FULL_SIMP_TAC (srw_ss()) [EVAL ``GENLIST I 16``,EVERY_DEF, 1884 ShiftLeft_def,ShiftRight_def,SignedShiftRight_def,w2n_n2w] \\ blastLib.BBLAST_TAC) 1885 |> SIMP_RULE std_ss [EVAL ``GENLIST I 16``,EVERY_DEF] 1886 1887val rw64 = prove( 1888 ``EVERY (\i. ((w:word64) ' i = ((w && n2w (2 ** i)) <> 0w)) /\ 1889 (word_bit i w = ((w && n2w (2 ** i)) <> 0w)) /\ 1890 (word_lsr w i = ShiftRight w ((n2w i):word64)) /\ 1891 (word_asr w i = SignedShiftRight w ((n2w i):word64)) /\ 1892 (word_lsl w i = ShiftLeft w ((n2w i):word64))) (GENLIST I 64) /\ 1893 (word_msb w = (w:word64) ' 63)``, 1894 FULL_SIMP_TAC (srw_ss()) [EVAL ``GENLIST I 64``,EVERY_DEF, 1895 ShiftLeft_def,ShiftRight_def,SignedShiftRight_def,w2n_n2w] \\ blastLib.BBLAST_TAC) 1896 |> SIMP_RULE std_ss [EVAL ``GENLIST I 64``,EVERY_DEF] 1897 1898val rw8 = prove( 1899 ``EVERY (\i. ((w:word8) ' i = ((w && n2w (2 ** i)) <> 0w)) /\ 1900 (word_bit i w = ((w && n2w (2 ** i)) <> 0w)) /\ 1901 (word_lsr w i = ShiftRight w ((n2w i):word8)) /\ 1902 (word_asr w i = SignedShiftRight w ((n2w i):word8)) /\ 1903 (word_lsl w i = ShiftLeft w ((n2w i):word8))) (GENLIST I 8) /\ 1904 (word_msb w = (w:word8) ' 7)``, 1905 FULL_SIMP_TAC (srw_ss()) [EVAL ``GENLIST I 8``,EVERY_DEF, 1906 ShiftLeft_def,ShiftRight_def,SignedShiftRight_def,w2n_n2w] \\ blastLib.BBLAST_TAC) 1907 |> SIMP_RULE std_ss [EVAL ``GENLIST I 8``,EVERY_DEF] 1908 1909val rw4 = let 1910 val lemma = blastLib.BBLAST_PROVE 1911 ``!v. ((w2w (v:word32)):word8 = w2w (v && 255w)) /\ 1912 (v && 255w) <+ 256w:word32`` 1913 val w2w_w2w_lemma = prove( 1914 ``w2n (w2w (v:word32) :word8) = w2n (v && 255w:word32)``, 1915 fs [w2n_11,Once lemma,w2w_def] \\ assume_tac lemma \\ fs [WORD_LO]); 1916 val lemma1 = prove( 1917 ``(w:word32) ' (w2n (w2w (v:word32) :word8) - (1 :num)) /\ 1918 w2n (w2w (v:word32) :word8) <= (32 :num) 1919 <=> 1920 (v && 255w) <+ 33w /\ 1921 if v && 255w = 0w then w ' 0 else ShiftRight w ((v && 255w) - 1w) ' 0``, 1922 fs [w2w_w2w_lemma,ShiftRight_def] 1923 \\ qspec_then `255w && v` mp_tac lemma 1924 \\ rw [] 1925 \\ Cases_on `255w && v` 1926 \\ fs [WORD_LO] 1927 \\ rewrite_tac [GSYM word_sub_def] 1928 \\ full_simp_tac std_ss [word_arith_lemma2] 1929 \\ `~(n < 1) /\ (n - 1) < 4294967296 /\ (n <= 32 = n < 33)` by decide_tac 1930 \\ fs [word_lsr_def,fcpTheory.FCP_BETA] 1931 \\ Cases_on `n < 33` \\ fs []) 1932 val lemma2 = prove( 1933 ``(w:word32) ' (w2n (w2w (v:word32) :word8)) /\ 1934 w2n (w2w (v:word32) :word8) <= (31 :num) 1935 <=> 1936 (v && 255w) <+ 32w /\ ShiftRight w (v && 255w) ' 0``, 1937 fs [w2w_w2w_lemma,ShiftRight_def] 1938 \\ qspec_then `255w && v` mp_tac lemma 1939 \\ rw [] 1940 \\ Cases_on `255w && v` 1941 \\ fs [WORD_LO] 1942 \\ `n < 4294967296 /\ (n <= 31 = n < 32)` by decide_tac 1943 \\ fs [word_lsr_def,fcpTheory.FCP_BETA] 1944 \\ Cases_on `n < 32` \\ fs []) 1945 val lemma1 = CONJ lemma1 (lemma1 |> RW1 [CONJ_COMM]) 1946 val lemma2 = CONJ lemma2 (lemma2 |> RW1 [CONJ_COMM]) 1947 val lemma3 = CONJ lemma1 lemma2 |> RW [GSYM CONJ_ASSOC] 1948 in lemma3 end; 1949 1950val rw1 = prove( 1951 ``EVERY (\i. ((w:word32) ' i = ((w && n2w (2 ** i)) <> 0w)) /\ 1952 (word_bit i w = ((w && n2w (2 ** i)) <> 0w)) /\ 1953 (word_lsr w i = ShiftRight w ((n2w i):word32)) /\ 1954 (word_asr w i = SignedShiftRight w ((n2w i):word32)) /\ 1955 (word_lsl w i = ShiftLeft w ((n2w i):word32))) (GENLIST I 32) /\ 1956 (word_msb w = (w:word32) ' 31)``, 1957 FULL_SIMP_TAC (srw_ss()) [EVAL ``GENLIST I 32``,EVERY_DEF, 1958 ShiftLeft_def,ShiftRight_def,SignedShiftRight_def,w2n_n2w] \\ blastLib.BBLAST_TAC) 1959 |> SIMP_RULE std_ss [EVAL ``GENLIST I 32``,EVERY_DEF] 1960 1961val word_add_with_carry_eq = prove( 1962 ``word_add_with_carry (x:'a word) y z = 1963 x + y + if z then 1w else 0w``, 1964 Cases_on `z` \\ Cases_on `x` \\ Cases_on `y` 1965 \\ FULL_SIMP_TAC std_ss [word_add_with_carry_def] 1966 \\ FULL_SIMP_TAC std_ss [carry_out_def,add_with_carry_def,LET_DEF] 1967 \\ FULL_SIMP_TAC std_ss [w2n_n2w,w2w_def,word_add_n2w]); 1968 1969val w2w_blast = prove( 1970 ``!w. w <+ n2w (2 ** 33):word64 ==> 1971 ((w2w ((w2w w):word32) = w) <=> (w && (n2w (2 ** 32)) = 0w))``, 1972 blastLib.BBLAST_TAC); 1973 1974val carry_out_eq = prove( 1975 ``carry_out (x:word32) (y:word32) z = 1976 ((w2w x + w2w y + if z then 1w else 0w:word64) && n2w (2 ** 32)) <> 0w``, 1977 Cases_on `z` \\ Cases_on `x` \\ Cases_on `y` 1978 \\ FULL_SIMP_TAC std_ss [carry_out_def,add_with_carry_def,LET_DEF] 1979 \\ FULL_SIMP_TAC std_ss [w2n_n2w,w2w_def,word_add_n2w] 1980 \\ `(n + n') < 18446744073709551616` by (fs [] \\ DECIDE_TAC) 1981 \\ `(n + n' + 1) < 18446744073709551616` by (fs [] \\ DECIDE_TAC) 1982 \\ `n2w (n + n' + 1) <+ n2w (2 ** 33):word64 /\ 1983 n2w (n + n') <+ n2w (2 ** 33):word64` by (fs [WORD_LO] \\ DECIDE_TAC) 1984 \\ IMP_RES_TAC w2w_blast 1985 \\ `(n + n' + 1) < dimword (:64)` by (fs [WORD_LO] \\ DECIDE_TAC) 1986 \\ `(n + n' + 1) MOD dimword (:32) < dimword (:64) /\ 1987 (n + n') MOD dimword (:32) < dimword (:64)` by 1988 (REPEAT STRIP_TAC \\ MATCH_MP_TAC LESS_TRANS 1989 \\ Q.EXISTS_TAC `dimword (:32)` 1990 \\ FULL_SIMP_TAC std_ss [MATCH_MP MOD_LESS ZERO_LT_dimword] 1991 \\ EVAL_TAC) 1992 \\ `(n + n') < dimword (:64)` by DECIDE_TAC 1993 \\ FULL_SIMP_TAC std_ss [w2w_def,w2n_n2w,n2w_11]); 1994 1995val rw3 = prove( 1996 ``(w << w2n y = ShiftLeft (w:word64) (w2w (y:word32))) /\ 1997 (w >>> w2n y = ShiftRight (w:word64) (w2w (y:word32))) /\ 1998 (w << w2n x = ShiftLeft (w:word64) (w2w (x:word8))) /\ 1999 (w >>> w2n x = ShiftRight (w:word64) (w2w (x:word8))) /\ 2000 (v << w2n x = ShiftLeft (v:word32) (w2w (x:word8))) /\ 2001 (v >>> w2n x = ShiftRight (v:word32) (w2w (x:word8)))``, 2002 Cases_on `y` \\ Cases_on `x` \\ fs [ShiftLeft_def,ShiftRight_def,w2w_def] 2003 \\ `n < 18446744073709551616` by DECIDE_TAC \\ fs [] 2004 \\ `n' < 18446744073709551616` by DECIDE_TAC \\ fs [] 2005 \\ `n' < 4294967296` by DECIDE_TAC \\ fs []); 2006 2007val fix_align = blastLib.BBLAST_PROVE 2008 ``(((63 '' 3) v = v:word64) <=> (v && 7w = 0w)) /\ 2009 ((v = ((63 '' 3) v):word64) <=> (v && 7w = 0w)) /\ 2010 (((63 '' 2) v = v:word64) <=> (v && 3w = 0w)) /\ 2011 ((v = ((63 '' 2) v):word64) <=> (v && 3w = 0w)) /\ 2012 (((63 '' 1) v = v:word64) <=> (v && 1w = 0w)) /\ 2013 ((v = ((63 '' 1) v):word64) <=> (v && 1w = 0w)) /\ 2014 (((31 '' 2) w = w:word32) <=> (w && 1w = 0w) /\ (w && 2w = 0w)) /\ 2015 ((w = (31 '' 2) w:word32) <=> (w && 1w = 0w) /\ (w && 2w = 0w)) /\ 2016 (((31 '' 1) w = w:word32) <=> (w && 1w = 0w)) /\ 2017 ((w = (31 '' 1) w:word32) <=> (w && 1w = 0w)) /\ 2018 ((31 '' 2) w = w >>> 2 << 2) /\ 2019 ((31 '' 1) w = w >>> 1 << 1) /\ 2020 ((31 '' 0) w = w)``; 2021 2022val w2w_w2w_and_255 = prove( 2023 ``w2w ((w2w:word32->word8) v) = (v && 0xFFw)``, 2024 blastLib.BBLAST_TAC) 2025 2026val Shift_intro = prove( 2027 ``(w >> w2n ((w2w:word32->word8) v) = SignedShiftRight w (v && 0xFFw)) /\ 2028 (w >>> w2n ((w2w:word32->word8) v) = ShiftRight w (v && 0xFFw)) /\ 2029 (w << w2n ((w2w:word32->word8) v) = ShiftLeft w (v && 0xFFw))``, 2030 fs [SignedShiftRight_def,ShiftRight_def,ShiftLeft_def,GSYM w2w_w2w_and_255] 2031 \\ fs [w2w_def,w2n_n2w] 2032 \\ `w2n v MOD 256 < 4294967296` by all_tac \\ fs [] 2033 \\ match_mp_tac LESS_TRANS \\ qexists_tac `256` \\ fs []); 2034 2035val blast_append_0_lemma = prove( 2036 ``(((w2w:word32 -> 31 word) w @@ (0w:word1)) : word32 = w << 1) /\ 2037 (((w2w:word32 -> 30 word) w @@ (0w:word2)) : word32 = w << 2)``, 2038 blastLib.BBLAST_TAC); 2039 2040val graph_format_preprocessing = save_thm("graph_format_preprocessing", 2041 LIST_CONJ [MemAcc8_def, MemAcc32_def, MemAcc64_def, 2042 ShiftLeft_def, ShiftRight_def, 2043 MemUpdate8_def, MemUpdate32_def, MemUpdate64_def] |> GSYM 2044 |> CONJ rw1 |> CONJ rw3 |> CONJ rw64 |> CONJ rw16 |> CONJ rw8 |> CONJ rw4 2045 |> CONJ w2w_carry |> CONJ w2w_carry_alt 2046 |> CONJ carry_out_eq 2047 |> CONJ READ32_expand64 2048 |> CONJ word_add_with_carry_eq 2049 |> CONJ fix_align 2050 |> CONJ Shift_intro 2051 |> CONJ blast_append_0_lemma 2052 |> RW [GSYM CONJ_ASSOC] 2053 |> SIMP_RULE std_ss []) 2054 2055(* misc *) 2056 2057val STAR_IF = store_thm("STAR_IF", 2058 ``(if b then x else y) * (q:'a set set) = (if b then x * q else STAR y q)``, 2059 Cases_on `b` \\ FULL_SIMP_TAC std_ss []) 2060 2061val emp_STAR = store_thm("emp_STAR", 2062 ``(emp * p = p) /\ (p * emp = p:'a set set)``, 2063 SIMP_TAC std_ss [SEP_CLAUSES]) 2064 2065val T_IMP = store_thm("T_IMP",``(T ==> b) ==> b``,SIMP_TAC std_ss []) 2066 2067val EQ_T = store_thm("EQ_T",``(x = T) ==> x``,SIMP_TAC std_ss []) 2068 2069val ret_lemma = store_thm("ret_lemma", 2070 ``(s "ret" = VarWord w) ==> (w = var_word "ret" s)``, 2071 SRW_TAC [] [var_word_def,var_acc_def]); 2072 2073val apply_update_NIL = store_thm("apply_update_NIL", 2074 ``apply_update [] s = (s:'a->'b)``, 2075 SIMP_TAC std_ss [apply_update_def]); 2076 2077val var_word_apply_update = store_thm("var_word_apply_update", 2078 ``var_word n (apply_update ((x,y)::xs) s) = 2079 if n = x then (case y s of VarWord w => w | _ => 0w) else 2080 var_word n (apply_update xs s)``, 2081 SRW_TAC [] [var_word_def,var_acc_def,apply_update_def,APPLY_UPDATE_THM]); 2082 2083val I_LEMMA = store_thm("I_LEMMA", 2084 ``(\x.x:'a) = I``, 2085 SIMP_TAC std_ss [FUN_EQ_THM]); 2086 2087val Aligned_Align = store_thm("Aligned_Align", 2088 ``arm$Aligned (w,n) ==> (arm$Align (w:'a word,n) = w)``, 2089 SIMP_TAC std_ss [armTheory.Aligned_def,armTheory.Align_def]); 2090 2091val SWITCH_LEMMA = store_thm("SWITCH_LEMMA", 2092 ``SPEC m (p * f x) c (q * f x) <=> 2093 !v. (v = x) ==> SPEC m (p * f v) c (q * f v)``, 2094 SIMP_TAC std_ss []); 2095 2096val SWITCH_COMBINE = store_thm("SWITCH_COMBINE", 2097 ``(b1 ==> SPEC m p c1 q1) /\ (b2 ==> SPEC m p c2 q2) ==> 2098 (~b1 ==> b2) ==> SPEC m p (c1 UNION c2) (if b1 then q1 else q2)``, 2099 Cases_on `b1` \\ FULL_SIMP_TAC std_ss [] 2100 \\ REPEAT STRIP_TAC 2101 \\ MATCH_MP_TAC (SPEC_SUBSET_CODE |> SIMP_RULE std_ss [PULL_FORALL,AND_IMP_INTRO]) 2102 \\ TRY (Q.EXISTS_TAC `c1` \\ FULL_SIMP_TAC (srw_ss()) [] \\ NO_TAC) 2103 \\ TRY (Q.EXISTS_TAC `c2` \\ FULL_SIMP_TAC (srw_ss()) [] \\ NO_TAC)); 2104 2105val SPEC_PC_LEMMA = store_thm("SPEC_PC_LEMMA", 2106 ``SPEC m (p * r x) c q ==> 2107 !pc. (pc = x) ==> SPEC m (p * r pc) c q``, 2108 SIMP_TAC std_ss []); 2109 2110val ABBBREV_CODE_LEMMA = store_thm("ABBBREV_CODE_LEMMA", 2111 ``!a (x :('a, 'b, 'c) processor) p c q. 2112 (a ==> SPEC x p c q) ==> !d. c SUBSET d ==> a ==> SPEC x p d q``, 2113 REPEAT STRIP_TAC THEN RES_TAC THEN IMP_RES_TAC SPEC_SUBSET_CODE); 2114 2115val NEQ_SYM = store_thm("NEQ_SYM", 2116 ``~(x = y) <=> ~(y = x)``, 2117 METIS_TAC []); 2118 2119val SKIP_TAG_IMP_CALL_ARM = store_thm("SKIP_TAG_IMP_CALL_ARM", 2120 ``IMPL_INST (ARM code) locs 2121 (Inst entry (K T) 2122 (ASM (SOME (\s. SKIP_TAG str)) [] 2123 (Jump exit))) ==> 2124 !old. (old = str) ==> 2125 !name. 2126 (locs name = SOME entry) ==> 2127 IMPL_INST (ARM code) locs 2128 (Inst entry (K T) 2129 (CALL NONE 2130 [("ret",(\s. VarWord exit)); 2131 ("r0",var_acc "r0"); 2132 ("r1",var_acc "r1"); 2133 ("r2",var_acc "r2"); 2134 ("r3",var_acc "r3"); 2135 ("r4",var_acc "r4"); 2136 ("r5",var_acc "r5"); 2137 ("r6",var_acc "r6"); 2138 ("r7",var_acc "r7"); 2139 ("r8",var_acc "r8"); 2140 ("r9",var_acc "r9"); 2141 ("r10",var_acc "r10"); 2142 ("r11",var_acc "r11"); 2143 ("r12",var_acc "r12"); 2144 ("r13",var_acc "r13"); 2145 ("r14",var_acc "r14"); 2146 ("r15",var_acc "r15"); 2147 ("r16",var_acc "r16"); 2148 ("r17",var_acc "r17"); 2149 ("r18",var_acc "r18"); 2150 ("r19",var_acc "r19"); 2151 ("r20",var_acc "r20"); 2152 ("r21",var_acc "r21"); 2153 ("r22",var_acc "r22"); 2154 ("r23",var_acc "r23"); 2155 ("r24",var_acc "r24"); 2156 ("r25",var_acc "r25"); 2157 ("r26",var_acc "r26"); 2158 ("r27",var_acc "r27"); 2159 ("r28",var_acc "r28"); 2160 ("r29",var_acc "r29"); 2161 ("r30",var_acc "r30"); 2162 ("r31",var_acc "r31"); 2163 ("mode",var_acc "mode"); ("n",var_acc "n"); 2164 ("z",var_acc "z"); ("c",var_acc "c"); ("v",var_acc "v"); 2165 ("mem",var_acc "mem"); ("dom",var_acc "dom"); 2166 ("stack",var_acc "stack"); 2167 ("dom_stack",var_acc "dom_stack"); 2168 ("clock",var_acc "clock"); ("ret_addr_input",var_acc "r0")] 2169 name (Jump exit)))``, 2170 fs [IMPL_INST_def,next_ok_def,check_ret_def,exec_next_def, 2171 check_jump_def,get_assert_def,LET_THM] 2172 \\ fs [ARM_def] \\ rpt BasicProvers.TOP_CASE_TAC \\ fs [] 2173 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2174 arm_STATE_CPSR_def,var_bool_def,var_nat_def,m0_STATE_PSR_def, 2175 var_word_def,var_acc_def,ret_and_all_names_def,all_names_def, 2176 var_dom_def,var_word_def,var_mem_def,var_word8_def] 2177 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2178 arm_STATE_CPSR_def,var_bool_def,arm_STATE_REGS_def, 2179 m0_STATE_REGS_def,var_nat_def,m0_STATE_PSR_def, 2180 var_word_def,var_acc_def,ret_and_all_names_def,all_names_def, 2181 var_dom_def,var_word_def,var_mem_def,var_word8_def] 2182 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2183 arm_STATE_REGS_def,STAR_ASSOC,SPEC_REFL]); 2184 2185val SKIP_TAG_IMP_CALL_M0 = store_thm("SKIP_TAG_IMP_CALL_M0", 2186 ``IMPL_INST (M0 code) locs 2187 (Inst entry (K T) 2188 (ASM (SOME (\s. SKIP_TAG str)) [] 2189 (Jump exit))) ==> 2190 !old. (old = str) ==> 2191 !name. 2192 (locs name = SOME entry) ==> 2193 IMPL_INST (M0 code) locs 2194 (Inst entry (K T) 2195 (CALL NONE 2196 [("ret",(\s. VarWord exit)); 2197 ("r0",var_acc "r0"); 2198 ("r1",var_acc "r1"); 2199 ("r2",var_acc "r2"); 2200 ("r3",var_acc "r3"); 2201 ("r4",var_acc "r4"); 2202 ("r5",var_acc "r5"); 2203 ("r6",var_acc "r6"); 2204 ("r7",var_acc "r7"); 2205 ("r8",var_acc "r8"); 2206 ("r9",var_acc "r9"); 2207 ("r10",var_acc "r10"); 2208 ("r11",var_acc "r11"); 2209 ("r12",var_acc "r12"); 2210 ("r13",var_acc "r13"); 2211 ("r14",var_acc "r14"); 2212 ("r15",var_acc "r15"); 2213 ("r16",var_acc "r16"); 2214 ("r17",var_acc "r17"); 2215 ("r18",var_acc "r18"); 2216 ("r19",var_acc "r19"); 2217 ("r20",var_acc "r20"); 2218 ("r21",var_acc "r21"); 2219 ("r22",var_acc "r22"); 2220 ("r23",var_acc "r23"); 2221 ("r24",var_acc "r24"); 2222 ("r25",var_acc "r25"); 2223 ("r26",var_acc "r26"); 2224 ("r27",var_acc "r27"); 2225 ("r28",var_acc "r28"); 2226 ("r29",var_acc "r29"); 2227 ("r30",var_acc "r30"); 2228 ("r31",var_acc "r31"); 2229 ("mode",var_acc "mode"); ("n",var_acc "n"); 2230 ("z",var_acc "z"); ("c",var_acc "c"); ("v",var_acc "v"); 2231 ("mem",var_acc "mem"); ("dom",var_acc "dom"); 2232 ("stack",var_acc "stack"); 2233 ("dom_stack",var_acc "dom_stack"); 2234 ("clock",var_acc "clock"); ("ret_addr_input",var_acc "r0")] 2235 name (Jump exit)))``, 2236 fs [IMPL_INST_def,next_ok_def,check_ret_def,exec_next_def, 2237 check_jump_def,get_assert_def,LET_THM] 2238 \\ fs [M0_def] \\ rpt BasicProvers.TOP_CASE_TAC \\ fs [] 2239 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2240 arm_STATE_CPSR_def,var_bool_def,var_nat_def,m0_STATE_PSR_def, 2241 var_word_def,var_acc_def,ret_and_all_names_def,all_names_def, 2242 var_dom_def,var_word_def,var_mem_def,var_word8_def] 2243 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2244 arm_STATE_CPSR_def,var_bool_def,arm_STATE_REGS_def, 2245 m0_STATE_REGS_def,var_nat_def,m0_STATE_PSR_def, 2246 var_word_def,var_acc_def,ret_and_all_names_def,all_names_def, 2247 var_dom_def,var_word_def,var_mem_def,var_word8_def] 2248 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2249 arm_STATE_REGS_def,STAR_ASSOC,SPEC_REFL]); 2250 2251val SKIP_TAG_IMP_CALL_RISCV = store_thm("SKIP_TAG_IMP_CALL_RISCV", 2252 ``IMPL_INST (RISCV c) locs 2253 (Inst entry (K T) 2254 (ASM (SOME (\s. SKIP_TAG str)) [] 2255 (Jump exit))) ==> 2256 !old. (old = str) ==> 2257 !name. 2258 (locs name = SOME entry) ==> 2259 IMPL_INST (RISCV code) locs 2260 (Inst entry (K T) 2261 (CALL NONE 2262 [("ret",(\s. VarWord exit)); 2263 ("r0",var_acc "r0"); 2264 ("r1",var_acc "r1"); 2265 ("r2",var_acc "r2"); 2266 ("r3",var_acc "r3"); 2267 ("r4",var_acc "r4"); 2268 ("r5",var_acc "r5"); 2269 ("r6",var_acc "r6"); 2270 ("r7",var_acc "r7"); 2271 ("r8",var_acc "r8"); 2272 ("r9",var_acc "r9"); 2273 ("r10",var_acc "r10"); 2274 ("r11",var_acc "r11"); 2275 ("r12",var_acc "r12"); 2276 ("r13",var_acc "r13"); 2277 ("r14",var_acc "r14"); 2278 ("r15",var_acc "r15"); 2279 ("r16",var_acc "r16"); 2280 ("r17",var_acc "r17"); 2281 ("r18",var_acc "r18"); 2282 ("r19",var_acc "r19"); 2283 ("r20",var_acc "r20"); 2284 ("r21",var_acc "r21"); 2285 ("r22",var_acc "r22"); 2286 ("r23",var_acc "r23"); 2287 ("r24",var_acc "r24"); 2288 ("r25",var_acc "r25"); 2289 ("r26",var_acc "r26"); 2290 ("r27",var_acc "r27"); 2291 ("r28",var_acc "r28"); 2292 ("r29",var_acc "r29"); 2293 ("r30",var_acc "r30"); 2294 ("r31",var_acc "r31"); 2295 ("mode",var_acc "mode"); ("n",var_acc "n"); 2296 ("z",var_acc "z"); ("c",var_acc "c"); ("v",var_acc "v"); 2297 ("mem",var_acc "mem"); ("dom",var_acc "dom"); 2298 ("stack",var_acc "stack"); 2299 ("dom_stack",var_acc "dom_stack"); 2300 ("clock",var_acc "clock"); ("ret_addr_input",var_acc "r10")] 2301 name (Jump exit)))``, 2302 fs [IMPL_INST_def,next_ok_def,check_ret_def,exec_next_def, 2303 check_jump_def,get_assert_def,LET_THM] 2304 \\ fs [RISCV_def] \\ rpt BasicProvers.TOP_CASE_TAC \\ fs [] 2305 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2306 arm_STATE_CPSR_def,var_bool_def,var_nat_def,m0_STATE_PSR_def, 2307 var_word_def,var_acc_def,ret_and_all_names_def,all_names_def, 2308 var_dom_def,var_word_def,var_mem_def,var_word8_def] 2309 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2310 arm_STATE_CPSR_def,var_bool_def,arm_STATE_REGS_def, 2311 m0_STATE_REGS_def,var_nat_def,m0_STATE_PSR_def,riscv_STATE_REGS_def, 2312 riscv_STATE_def, 2313 var_word_def,var_acc_def,ret_and_all_names_def,all_names_def, 2314 var_dom_def,var_word_def,var_mem_def,var_word8_def] 2315 \\ fs [apply_update_def,APPLY_UPDATE_THM,arm_STATE_def,m0_STATE_def, 2316 arm_STATE_REGS_def,STAR_ASSOC,SPEC_REFL]); 2317 2318val fixwidth_w2v = prove( 2319 ``fixwidth (dimindex (:'a)) (w2v (w:'a word)) = w2v w``, 2320 EVAL_TAC \\ fs []); 2321 2322val bit_field_insert_31_16 = store_thm("bit_field_insert_31_16", 2323 ``(bit_field_insert 31 16 v (w:word32) = 2324 (v << 16 || (w << 16) >>> 16):word32) /\ 2325 (bit_field_insert 31 16 (x:word16) (w:word32) = 2326 (w2w x << 16 || (w << 16) >>> 16):word32)``, 2327 blastLib.BBLAST_TAC); 2328 2329val v2w_field_insert_31_16 = prove( 2330 ``(v2w (field_insert 31 16 2331 (field 15 0 (w2v (w:word32))) 2332 (w2v (v:word32)))) = 2333 bit_field_insert 31 16 w v``, 2334 fs [bit_field_insert_def,bitstringTheory.field_insert_def] 2335 \\ once_rewrite_tac [GSYM fixwidth_w2v] 2336 \\ rewrite_tac [GSYM bitstringTheory.word_modify_v2w,bitstringTheory.v2w_w2v] 2337 \\ AP_THM_TAC \\ AP_TERM_TAC \\ fs [FUN_EQ_THM] 2338 \\ rpt strip_tac \\ IF_CASES_TAC \\ fs [] 2339 \\ EVAL_TAC \\ Cases_on `i` \\ fs [] 2340 \\ rpt (Cases_on `n` \\ fs [] \\ Cases_on `n'` \\ fs [])); 2341 2342val word_cancel_extra = store_thm("word_cancel_extra", 2343 ``(w + x ��� w = x:'a word) /\ 2344 (w + x ��� (w + y) = x - y:'a word) /\ 2345 (w + x ��� (w - y) = x + y:'a word)``, 2346 fs [WORD_LEFT_ADD_DISTRIB]); 2347 2348val export_init_rw = save_thm("export_init_rw", 2349 CONJ bit_field_insert_31_16 v2w_field_insert_31_16); 2350 2351val m0_preprocessing = save_thm("m0_preprocessing", 2352 CONJ (EVAL ``RName_LR = RName_PC``) (EVAL ``RName_PC = RName_LR``)); 2353 2354val WRITE64_intro = store_thm("WRITE64_intro", 2355 ``m���a ��� (7 >< 0) w; a + 1w ��� (15 >< 8) w; 2356 a + 3w ��� (31 >< 24) w; a + 7w ��� (63 >< 56) w; 2357 a + 5w ��� (47 >< 40) w; a + 2w ��� (23 >< 16) w; 2358 a + 4w ��� (39 >< 32) w; a + 6w ��� (55 >< 48) w��� = 2359 WRITE64 (a:word64) (w:word64) (m:word64->word8)``, 2360 fs [WRITE64_def,FUN_EQ_THM,combinTheory.APPLY_UPDATE_THM] 2361 \\ rw [] \\ fs [] \\ fs [WORD_EQ_ADD_CANCEL] 2362 \\ blastLib.BBLAST_TAC); 2363 2364val v2w_sing = store_thm("v2w_sing", 2365 ``v2w [x] = if x then 1w else 0w``, 2366 Cases_on `x` \\ EVAL_TAC); 2367 2368val _ = export_theory(); 2369