Changeset 951


Ignore:
Timestamp:
Jun 15, 2011, 1:35:27 AM (8 years ago)
Author:
sacerdot
Message:

long call case completed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r950 r951  
    15891589       let pc ≝ sigma pap (program_counter ? ps) in
    15901590       let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    1591        let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (low_internal_ram … ps) in
     1591       let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
    15921592        Some …
    15931593         (mk_PreStatus (BitVectorTrie Byte 16)
     
    21022102        pbu)).
    21032103       
    2104 (*
    2105 lemma high_internal_ram_write_at_stack_pointer:
    2106  ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s.
    2107  #T #s #x whd in ⊢ (??(??%)?)
    2108  cases (split ????) #nu #nl normalize nodelta;
    2109  cases (get_index_v bool ????) %
    2110 qed.
    2111 *)
     2104axiom high_internal_ram_write_at_stack_pointer:
     2105 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     2106  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
     2107  high_internal_ram ? s2 = high_internal_ram T2 s3 →
     2108  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
     2109  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     2110  bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
     2111   high_internal_ram T1
     2112     (write_at_stack_pointer ?
     2113       (set_8051_sfr ?
     2114         (write_at_stack_pointer ?
     2115           (set_8051_sfr ?
     2116             (set_high_internal_ram ? s1
     2117               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
     2118             SFR_SP sp1)
     2119          bl)
     2120        SFR_SP sp2)
     2121      bu)
     2122   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
     2123      (high_internal_ram ?
     2124       (write_at_stack_pointer ?
     2125         (set_8051_sfr ?
     2126           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
     2127          SFR_SP sp2)
     2128        pbu)).
    21122129
    21132130lemma set_program_counter_set_low_internal_ram:
     
    21222139  set_clock T (set_low_internal_ram … s x) y =
    21232140   set_low_internal_ram … (set_clock … s y) x.
     2141 //
     2142qed.
     2143
     2144lemma set_program_counter_set_high_internal_ram:
     2145 ∀T,s,x,y.
     2146  set_program_counter T (set_high_internal_ram … s x) y =
     2147   set_high_internal_ram … (set_program_counter … s y) x.
     2148 //
     2149qed.
     2150
     2151lemma set_clock_set_high_internal_ram:
     2152 ∀T,s,x,y.
     2153  set_clock T (set_high_internal_ram … s x) y =
     2154   set_high_internal_ram … (set_clock … s y) x.
     2155 //
     2156qed.
     2157
     2158lemma set_low_internal_ram_set_high_internal_ram:
     2159 ∀T,s,x,y.
     2160  set_low_internal_ram T (set_high_internal_ram … s x) y =
     2161   set_high_internal_ram … (set_low_internal_ram … s y) x.
    21242162 //
    21252163qed.
     
    24142452           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
    24152453           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
    2416            @split_eq_status;(* whd in ⊢ (??%%)*)
     2454           @split_eq_status;
    24172455            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
    24182456              >code_memory_write_at_stack_pointer %
     
    24302468                 @split_elim #x #y #H <H -x y H;
    24312469                 >EQ0 % ]
    2432             |
     2470            | >set_low_internal_ram_set_high_internal_ram
     2471              >set_program_counter_set_high_internal_ram
     2472              >set_clock_set_high_internal_ram
     2473              @high_internal_ram_write_at_stack_pointer
     2474               [ % | %
     2475               | @(pair_destruct_2 … EQ1)
     2476               | @(pair_destruct_2 … EQ2)
     2477               | >(pair_destruct_1 ????? EQpc)
     2478                 >(pair_destruct_2 ????? EQpc)
     2479                 @split_elim #x #y #H <H -x y H;
     2480                 >(pair_destruct_1 ????? EQppc)
     2481                 >(pair_destruct_2 ????? EQppc)
     2482                 @split_elim #x #y #H <H -x y H;
     2483                 >EQ0 % ]           
    24332484            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
    24342485              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
Note: See TracChangeset for help on using the changeset viewer.