Changeset 950


Ignore:
Timestamp:
Jun 14, 2011, 5:46:15 PM (8 years ago)
Author:
sacerdot
Message:

Horrible sub-proof finished :-)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r949 r950  
    15011501(* changed from add to sub *)
    15021502axiom low_internal_ram_of_pseudo_internal_ram_miss:
    1503  ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
     1503 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
    15041504  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    15051505  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
     
    15131513
    15141514definition addressing_mode_ok ≝
    1515  λM:internal_pseudo_address_map.λs:PseudoStatus.
     1515 λT.λM:internal_pseudo_address_map.λs:PreStatus T.
    15161516  λaddr:addressing_mode.
    15171517   match addr with
     
    15421542   
    15431543definition next_internal_pseudo_address_map0 ≝
     1544  λT.
    15441545  λfetched.
    15451546  λM: internal_pseudo_address_map.
    1546   λs: PseudoStatus.
     1547  λs: PreStatus T.
    15471548   match fetched with
    15481549    [ Comment _ ⇒ Some ? M
     
    15551556       match instr with
    15561557        [ ADD addr1 addr2 ⇒
    1557            if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
     1558           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
    15581559            Some ? M
    15591560           else
    15601561            None ?
    15611562        | ADDC addr1 addr2 ⇒
    1562            if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
     1563           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
    15631564            Some ? M
    15641565           else
    15651566            None ?
    15661567        | SUBB addr1 addr2 ⇒
    1567            if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
     1568           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
    15681569            Some ? M
    15691570           else
     
    15751576 λM:internal_pseudo_address_map.
    15761577  λs:PseudoStatus.
    1577     next_internal_pseudo_address_map0 (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
     1578    next_internal_pseudo_address_map0 ?
     1579     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
    15781580   
    15791581definition status_of_pseudo_status:
     
    20742076qed.
    20752077
     2078axiom low_internal_ram_write_at_stack_pointer:
     2079 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     2080  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
     2081  low_internal_ram ? s2 = low_internal_ram T2 s3 →
     2082  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
     2083  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     2084  bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
     2085   low_internal_ram T1
     2086     (write_at_stack_pointer ?
     2087       (set_8051_sfr ?
     2088         (write_at_stack_pointer ?
     2089           (set_8051_sfr ?
     2090             (set_low_internal_ram ? s1
     2091               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
     2092             SFR_SP sp1)
     2093          bl)
     2094        SFR_SP sp2)
     2095      bu)
     2096   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
     2097      (low_internal_ram ?
     2098       (write_at_stack_pointer ?
     2099         (set_8051_sfr ?
     2100           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
     2101          SFR_SP sp2)
     2102        pbu)).
     2103       
    20762104(*
    2077 lemma low_internal_ram_write_at_stack_pointer:
    2078  ∀T,s,x. low_internal_ram T (write_at_stack_pointer T s x) = low_internal_ram T s.
    2079  #T #s #x whd in ⊢ (??(??%)?)
    2080  cases (split ????) #nu #nl normalize nodelta;
    2081  cases (get_index_v bool ????) normalize nodelta; //
    2082 qed.
    2083 
    20842105lemma high_internal_ram_write_at_stack_pointer:
    20852106 ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s.
     
    20892110qed.
    20902111*)
     2112
     2113lemma set_program_counter_set_low_internal_ram:
     2114 ∀T,s,x,y.
     2115  set_program_counter T (set_low_internal_ram … s x) y =
     2116   set_low_internal_ram … (set_program_counter … s y) x.
     2117 //
     2118qed.
     2119
     2120lemma set_clock_set_low_internal_ram:
     2121 ∀T,s,x,y.
     2122  set_clock T (set_low_internal_ram … s x) y =
     2123   set_low_internal_ram … (set_clock … s y) x.
     2124 //
     2125qed.
    20912126
    20922127lemma external_ram_write_at_stack_pointer:
     
    21252160 cases (split ????) #nu #nl normalize nodelta;
    21262161 cases (get_index_v bool ????) %
     2162qed.
     2163
     2164axiom get_index_v_set_index:
     2165 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
     2166
     2167lemma get_8051_sfr_set_8051_sfr:
     2168 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
     2169 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
     2170 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
    21272171qed.
    21282172
     
    21912235  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
    21922236
     2237lemma pair_destruct_1:
     2238 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
     2239 #A #B #a #b *; /2/
     2240qed.
     2241
     2242lemma pair_destruct_2:
     2243 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
     2244 #A #B #a #b *; /2/
     2245qed.
     2246
     2247(*
    21932248lemma blah:
    21942249  ∀m: internal_pseudo_address_map.
     
    22492304  |
    22502305  ].
    2251  
     2306*)
    22522307(*
    22532308map_address0 ... (DIRECT arg) = Some .. →
     
    22762331  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
    22772332    #abs @⊥ normalize in abs; destruct (abs) ]
    2278  * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ?)
     2333 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
    22792334 generalize in match (refl … (code_memory … ps))
    22802335 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
     
    23482403           generalize in match EQ; -EQ;
    23492404           whd in ⊢ (???% → ??%?);
    2350            cases (half_add ???) #carry #new_sp normalize nodelta;
     2405           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;
    23512406           >(eq_bv_to_eq … H2c)
    23522407           change with
     
    23562411           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
    23572412           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
    2358            cases (half_add ???) #carry' #new_sp' normalize nodelta;
     2413           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
     2414           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
    23592415           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
    23602416           @split_eq_status;(* whd in ⊢ (??%%)*)
    23612417            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
    23622418              >code_memory_write_at_stack_pointer %
    2363             | change with
    2364                (low_internal_ram ?
    2365                 (write_at_stack_pointer ?
    2366                  (set_8051_sfr ?
    2367                   (write_at_stack_pointer ?
    2368                    (set_low_internal_ram ? ps
    2369                     (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? ps)))
    2370                   pc_bl) ??) pc_bu) = ?)
     2419            | >set_program_counter_set_low_internal_ram
     2420              >set_clock_set_low_internal_ram
     2421              @low_internal_ram_write_at_stack_pointer
     2422               [ % | %
     2423               | @(pair_destruct_2 … EQ1)
     2424               | @(pair_destruct_2 … EQ2)
     2425               | >(pair_destruct_1 ????? EQpc)
     2426                 >(pair_destruct_2 ????? EQpc)
     2427                 @split_elim #x #y #H <H -x y H;
     2428                 >(pair_destruct_1 ????? EQppc)
     2429                 >(pair_destruct_2 ????? EQppc)
     2430                 @split_elim #x #y #H <H -x y H;
     2431                 >EQ0 % ]
    23712432            |
    23722433            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
Note: See TracChangeset for help on using the changeset viewer.