Ignore:
Timestamp:
Jun 15, 2011, 2:22:59 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r951 r959  
    22092209qed.
    22102210
     2211lemma program_counter_set_8051_sfr:
     2212 ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
     2213 //
     2214qed.
     2215
    22112216lemma eq_rect_Type1_r:
    22122217  ∀A: Type[1].
     
    22292234 //
    22302235qed.
     2236
     2237axiom pair_elim':
     2238  ∀A,B,C: Type[0].
     2239  ∀T: A → B → C.
     2240  ∀p.
     2241  ∀P: A×B → C → Prop.
     2242    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
     2243      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
     2244
     2245axiom pair_elim'':
     2246  ∀A,B,C,C': Type[0].
     2247  ∀T: A → B → C.
     2248  ∀T': A → B → C'.
     2249  ∀p.
     2250  ∀P: A×B → C → C' → Prop.
     2251    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
     2252      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
    22312253
    22322254axiom split_elim':
     
    23702392    #abs @⊥ normalize in abs; destruct (abs) ]
    23712393 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
    2372  generalize in match (refl … (code_memory … ps))
    2373  cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
     2394 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
    23742395 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    23752396  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
     
    25092530              >clock_write_at_stack_pointer %]
    25102531       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    2511          generalize in match
    2512           (refl …
    2513             (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
    2514          cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
    2515          generalize in match
    2516           (refl …
    2517             (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
    2518          cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
     2532         @pair_elim' #fst_5_addr #rest_addr #EQ1
     2533         @pair_elim' #fst_5_pc #rest_pc #EQ2
    25192534         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
    25202535         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
    25212536         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
    25222537         change in ⊢ (? →??%?) with (execute_1_0 ??)
    2523            cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    2524            * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    2525            >H2b >(eq_instruction_to_eq … H2a)
    2526            generalize in match EQ; -EQ;
    2527            whd in ⊢ (???% → ?);
    2528            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
     2538         @pair_elim' * #instr #newppc' #ticks #EQn
     2539          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
     2540          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     2541          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
     2542          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
     2543          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
     2544          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
     2545          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
     2546          >get_8051_sfr_set_8051_sfr
     2547         
     2548          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
    25292549           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    25302550           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
Note: See TracChangeset for help on using the changeset viewer.