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