Changeset 1952 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 16, 2012, 1:29:17 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1948 r1952 2205 2205 // 2206 2206 qed. 2207 2208 theorem main_thm:2209 ∀M.2210 ∀M'.2211 ∀cm.2212 ∀ps.2213 ∀sigma.2214 ∀policy.2215 next_internal_pseudo_address_map M cm ps = Some … M' →2216 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =2217 status_of_pseudo_status M' …2218 (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.2219 #M #M' * #preamble #instr_list #ps #sigma #policy2220 change with (next_internal_pseudo_address_map0 ????? = ? → ?)2221 @(pose … (program_counter ?? ps)) #ppc #EQppc2222 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;2223 @pair_elim #labels #costs #H0 normalize nodelta2224 @pair_elim #assembled #costs' #EQ1 normalize nodelta2225 @pair_elim #pi #newppc #EQ2 normalize nodelta2226 @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels2227 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels2228 whd in match execute_1_pseudo_instruction; normalize nodelta2229 whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta2230 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc2231 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)2232 [>EQ2 %]2233 inversion pi2234 [2,3: (* Comment, Cost *)2235 #ARG #EQ2236 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;2237 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP2238 whd in match (execute_1_pseudo_instruction0 ?????);2239 %{0} @split_eq_status2240 CSC: STOP HERE, was // but requires H0 H3 because of \fst and \pi12241 ⇒ CHANGE TO AVOID \fst and \pi1! (*2242 try (<H3 H0 H3 //)2243 [ <add_zero in H3; #H3 >H3 H0 H3 //2244  H0 H3 /demod/*)2245 4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)2246 @Some_Some_elim #MAP cases (pol ?) normalize nodelta2247 [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'2248 whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)2249 @pair_elim' * #instr #newppc' #ticks #EQ42250 * * #H2a #H2b whd in ⊢ (% → ?) #H22251 >H2b >(eq_instruction_to_eq … H2a)2252 #EQ %[@1]2253 <MAP >(eq_bv_eq … H2) >EQ2254 whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)2255 cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %2256 whd in ⊢ (??%?)2257 whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)2258 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %2259 6: (* Mov *) #arg1 #arg22260 #H1 #H2 #EQ %[@1]2261 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)2262 change in ⊢ (? → ??%?) with (execute_1_0 ??)2263 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2264 * * #H2a #H2b whd in ⊢ (% → ?) #H2c2265 >H2b >(eq_instruction_to_eq … H2a)2266 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?);2267 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; whd in ⊢ (???% → ??%?)2268 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG22269 normalize nodelta;2270 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)]2271 #result #flags2272 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) %2273 5: (* Call *) #label #MAP2274 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP;2275 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;2276 [ (* short *) #abs @⊥ destruct (abs)2277 3: (* long *) #H1 #H2 #EQ %[@1]2278 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)2279 change in ⊢ (? → ??%?) with (execute_1_0 ??)2280 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2281 * * #H2a #H2b whd in ⊢ (% → ?) #H2c2282 >H2b >(eq_instruction_to_eq … H2a)2283 generalize in match EQ; EQ;2284 whd in ⊢ (???% → ??%?);2285 generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;2286 >(eq_bv_eq … H2c)2287 change with2288 ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →2289 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)2290 generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc2291 generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;2292 >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer2293 >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr2294 generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;2295 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c)2296 @split_eq_status;2297 [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)2298 >code_memory_write_at_stack_pointer %2299  >set_program_counter_set_low_internal_ram2300 >set_clock_set_low_internal_ram2301 @low_internal_ram_write_at_stack_pointer2302 [ >EQ0 @pol  %  %2303  @(pair_destruct_2 … EQ1)2304  @(pair_destruct_2 … EQ2)2305  >(pair_destruct_1 ????? EQpc)2306 >(pair_destruct_2 ????? EQpc)2307 @split_elim #x #y #H <H x y H;2308 >(pair_destruct_1 ????? EQppc)2309 >(pair_destruct_2 ????? EQppc)2310 @split_elim #x #y #H <H x y H;2311 >EQ0 % ]2312  >set_low_internal_ram_set_high_internal_ram2313 >set_program_counter_set_high_internal_ram2314 >set_clock_set_high_internal_ram2315 @high_internal_ram_write_at_stack_pointer2316 [ >EQ0 @pol  %  %2317  @(pair_destruct_2 … EQ1)2318  @(pair_destruct_2 … EQ2)2319  >(pair_destruct_1 ????? EQpc)2320 >(pair_destruct_2 ????? EQpc)2321 @split_elim #x #y #H <H x y H;2322 >(pair_destruct_1 ????? EQppc)2323 >(pair_destruct_2 ????? EQppc)2324 @split_elim #x #y #H <H x y H;2325 >EQ0 % ]2326  >external_ram_write_at_stack_pointer whd in ⊢ (??%?)2327 >external_ram_write_at_stack_pointer whd in ⊢ (???%)2328 >external_ram_write_at_stack_pointer whd in ⊢ (???%)2329 >external_ram_write_at_stack_pointer %2330  change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))2331 >EQ0 %2332  >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)2333 >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)2334 >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)2335 >special_function_registers_8051_write_at_stack_pointer %2336  >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)2337 >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)2338 >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)2339 >special_function_registers_8052_write_at_stack_pointer %2340  >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)2341 >p1_latch_write_at_stack_pointer whd in ⊢ (???%)2342 >p1_latch_write_at_stack_pointer whd in ⊢ (???%)2343 >p1_latch_write_at_stack_pointer %2344  >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)2345 >p3_latch_write_at_stack_pointer whd in ⊢ (???%)2346 >p3_latch_write_at_stack_pointer whd in ⊢ (???%)2347 >p3_latch_write_at_stack_pointer %2348  >clock_write_at_stack_pointer whd in ⊢ (??%?)2349 >clock_write_at_stack_pointer whd in ⊢ (???%)2350 >clock_write_at_stack_pointer whd in ⊢ (???%)2351 >clock_write_at_stack_pointer %]2352 (* (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; H1;2353 @pair_elim' #fst_5_addr #rest_addr #EQ12354 @pair_elim' #fst_5_pc #rest_pc #EQ22355 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))2356 cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]2357 generalize in match (option_destruct_Some ??? TEQ) TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)2358 change in ⊢ (? →??%?) with (execute_1_0 ??)2359 @pair_elim' * #instr #newppc' #ticks #EQn2360 * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)2361 generalize in match EQ; EQ; normalize nodelta; >(eq_bv_eq … H2c)2362 @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ42363 @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ52364 @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx EQx;2365 change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)2366 @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)2367 >get_8051_sfr_set_8051_sfr2368 2369 whd in EQ:(???%) ⊢ ? >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)2370 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)2371 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))2372 cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ42373 generalize in match (refl … (split bool 4 4 pc_bu))2374 cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ52375 generalize in match (refl … (split bool 3 8 rest_addr))2376 cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ62377 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)2378 generalize in match2379 (refl …2380 (half_add 16 (sigma 〈preamble,instr_list〉 newppc)2381 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))2382 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ72383 @split_eq_status try %2384 [ change with (? = sigma ? (address_of_word_labels ps label))2385 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)2386  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)2387 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]2388 4: (* Jmp *) #label #MAP2389 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP >MAP MAP;2390 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;2391 [3: (* long *) #H1 #H2 #EQ %[@1]2392 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)2393 change in ⊢ (? → ??%?) with (execute_1_0 ??)2394 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2395 * * #H2a #H2b whd in ⊢ (% → ?) #H2c2396 >H2b >(eq_instruction_to_eq … H2a)2397 generalize in match EQ; EQ;2398 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c)2399 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %2400 1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; H1;2401 generalize in match2402 (refl ?2403 (sub_16_with_carry2404 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))2405 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))2406 false))2407 cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;2408 generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;2409 generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;2410 #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]2411 generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)2412 change in ⊢ (? → ??%?) with (execute_1_0 ??)2413 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2414 * * #H2a #H2b whd in ⊢ (% → ?) #H2c2415 >H2b >(eq_instruction_to_eq … H2a)2416 generalize in match EQ; EQ;2417 whd in ⊢ (???% → ?);2418 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c)2419 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)2420 generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))2421 cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ42422 @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))2423 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)2424  (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; H1;2425 generalize in match2426 (refl …2427 (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))2428 cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ12429 generalize in match2430 (refl …2431 (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))2432 cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ22433 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))2434 cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]2435 generalize in match (option_destruct_Some ??? TEQ) TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)2436 change in ⊢ (? →??%?) with (execute_1_0 ??)2437 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2438 * * #H2a #H2b whd in ⊢ (% → ?) #H2c2439 >H2b >(eq_instruction_to_eq … H2a)2440 generalize in match EQ; EQ;2441 whd in ⊢ (???% → ?);2442 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)2443 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)2444 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))2445 cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ42446 generalize in match (refl … (split bool 4 4 pc_bu))2447 cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ52448 generalize in match (refl … (split bool 3 8 rest_addr))2449 cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ62450 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)2451 generalize in match2452 (refl …2453 (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)2454 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))2455 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ72456 @split_eq_status try %2457 [ change with (? = sigma ?? (address_of_word_labels ps label))2458 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)2459  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)2460 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]2461  (* Instruction *) pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta;2462 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]2463 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)2464 change in ⊢ (? → ??%?) with (execute_1_0 ??)2465 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2466 * * #H2a #H2b whd in ⊢ (% → ?) #H2c2467 >H2b >(eq_instruction_to_eq … H2a)2468 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; MAP;2469 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1;2470 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG22471 normalize nodelta; #MAP;2472 [1: change in ⊢ (? → %) with2473 ((let 〈result,flags〉 ≝2474 add_8_with_carry2475 (get_arg_8 ? ps false ACC_A)2476 (get_arg_8 ?2477 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))2478 false (DIRECT ARG2))2479 ? in ?) = ?)2480 [2,3: %]2481 change in ⊢ (???% → ?) with2482 (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)2483 >get_arg_8_set_clock2484 [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?2485 [2,4: #abs @⊥ normalize in abs; destruct (abs)2486 *:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]2487 [ change in ⊢ (? → %) with2488 ((let 〈result,flags〉 ≝2489 add_8_with_carry2490 (get_arg_8 ? ps false ACC_A)2491 (get_arg_8 ?2492 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))2493 false (DIRECT ARG2))2494 ? in ?) = ?)2495 >get_arg_8_set_low_internal_ram2496 2497 cases (add_8_with_carry ???)2498 2499 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)]2500 #result #flags2501 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) %2502  (* INC *) #arg1 #H1 #H2 #EQ %[@1]2503 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)2504 change in ⊢ (? → ??%?) with (execute_1_0 ??)2505 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;2506 * * #H2a #H2b whd in ⊢ (% → ?) #H2c2507 >H2b >(eq_instruction_to_eq … H2a)2508 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?);2509 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; normalize nodelta; [1,2,3: #ARG]2510 [1,2,3,4: cases (half_add ???) #carry #result2511  cases (half_add ???) #carry #bl normalize nodelta;2512 cases (full_add ????) #carry' #bu normalize nodelta ]2513 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) newppc';2514 [5: %2515 1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program2516 (set_program_counter pseudo_assembly_program ps newppc)2517 (\fst (ticks_of0 〈preamble,instr_list〉2518 (program_counter pseudo_assembly_program ps)2519 (Instruction (INC Identifier (DIRECT ARG))))2520 +clock pseudo_assembly_program2521 (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))2522 [2,3: // ]2523 <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]2524 whd in ⊢ (??%%)2525 cases (split bool 4 4 ARG)2526 #nu' #nl'2527 normalize nodelta2528 cases (split bool 1 3 nu')2529 #bit_1' #ignore'2530 normalize nodelta2531 cases (get_index_v bool 4 nu' ? ?)2532 [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %2533 2534 ]2535 cases daemon (* EASY CASES TO BE COMPLETED *)2536 qed.
Note: See TracChangeset
for help on using the changeset viewer.