Ignore:
Timestamp:
May 16, 2012, 1:29:17 AM (8 years ago)
Author:
sacerdot
Message:

AssemblyProof? splitted.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1948 r1952  
    22052205  //
    22062206qed.
    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 #policy
    2220   change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    2221   @(pose … (program_counter ?? ps)) #ppc #EQppc
    2222   generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;
    2223   @pair_elim #labels #costs #H0 normalize nodelta
    2224   @pair_elim #assembled #costs' #EQ1 normalize nodelta
    2225   @pair_elim #pi #newppc #EQ2 normalize nodelta
    2226   @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
    2227   @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    2228   whd in match execute_1_pseudo_instruction; normalize nodelta
    2229   whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
    2230   lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
    2231   lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    2232   [>EQ2 %]
    2233   inversion pi
    2234   [2,3: (* Comment, Cost *)
    2235     #ARG #EQ
    2236     #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
    2237     whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    2238     whd in match (execute_1_pseudo_instruction0 ?????);
    2239     %{0} @split_eq_status
    2240    CSC: STOP HERE, was // but requires -H0 -H3 because of \fst and \pi1
    2241    ⇒ 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 nodelta
    2247        [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 #EQ4       
    2250          * * #H2a #H2b whd in ⊢ (% → ?) #H2
    2251          >H2b >(eq_instruction_to_eq … H2a)
    2252          #EQ %[@1]
    2253          <MAP >(eq_bv_eq … H2) >EQ
    2254          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 #arg2
    2260        #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 ⊢ (% → ?) #H2c
    2265        >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; #ARG2
    2269        normalize nodelta;
    2270        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    2271        #result #flags
    2272        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    2273   |5: (* Call *) #label #MAP
    2274       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 ⊢ (% → ?) #H2c
    2282            >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 with
    2288             ((?=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 #EQppc
    2291            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_pointer
    2293            >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
    2294            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_ram
    2300               >set_clock_set_low_internal_ram
    2301               @low_internal_ram_write_at_stack_pointer
    2302                [ >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_ram
    2313               >set_program_counter_set_high_internal_ram
    2314               >set_clock_set_high_internal_ram
    2315               @high_internal_ram_write_at_stack_pointer
    2316                [ >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 #EQ1
    2354          @pair_elim' #fst_5_pc #rest_pc #EQ2
    2355          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 #EQn
    2360           * * #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 ?) ? = ? → ?) #EQ4
    2363           @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
    2364           @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_sfr
    2368          
    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; #EQ4
    2373            generalize in match (refl … (split bool 4 4 pc_bu))
    2374            cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
    2375            generalize in match (refl … (split bool 3 8 rest_addr))
    2376            cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
    2377            change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
    2378            generalize in match
    2379             (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; #EQ7
    2383            @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 #MAP
    2389       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 ⊢ (% → ?) #H2c
    2396            >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 match
    2402             (refl ?
    2403              (sub_16_with_carry
    2404               (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 ⊢ (% → ?) #H2c
    2415            >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 #EQ4
    2422            @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 match
    2426           (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; #EQ1
    2429          generalize in match
    2430           (refl …
    2431             (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
    2432          cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
    2433          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 ⊢ (% → ?) #H2c
    2439            >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; #EQ4
    2446            generalize in match (refl … (split bool 4 4 pc_bu))
    2447            cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
    2448            generalize in match (refl … (split bool 3 8 rest_addr))
    2449            cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
    2450            change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
    2451            generalize in match
    2452             (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; #EQ7   
    2456            @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 ⊢ (% → ?) #H2c
    2467        >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; #ARG2
    2471        normalize nodelta; #MAP;
    2472        [1: change in ⊢ (? → %) with
    2473         ((let 〈result,flags〉 ≝
    2474           add_8_with_carry
    2475            (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 ⊢ (???% → ?) with
    2482          (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
    2483         >get_arg_8_set_clock
    2484        [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 ⊢ (? → %) with
    2488         ((let 〈result,flags〉 ≝
    2489           add_8_with_carry
    2490            (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_ram
    2496        
    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 #flags
    2501        #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 ⊢ (% → ?) #H2c
    2507        >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 #result
    2511        | 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_program
    2516       (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_program
    2521         (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 nodelta
    2528             cases (split bool 1 3 nu')
    2529             #bit_1' #ignore'
    2530             normalize nodelta
    2531             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.