Changeset 2282


Ignore:
Timestamp:
Jul 31, 2012, 6:08:00 PM (7 years ago)
Author:
sacerdot
Message:

PUSH case almost finished

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2279 r2282  
    863863                 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
    864864             else
    865                match lookup_from_internal_ram … d M with
    866                [ None ⇒
    867                    Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
    868                | Some ul_addr ⇒
    869                    Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M)
    870                ]
     865               Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (lookup_from_internal_ram … d M) M)
    871866         | _ ⇒ λother: False. ⊥
    872867         ] (subaddressing_modein … addr1)
  • src/ASM/AssemblyProofSplit.ma

    r2279 r2282  
    11571157      ]
    11581158    ]
    1159   |*)12: (* JC *)
     1159  |12: (* JC *)
    11601160    >EQP -P normalize nodelta
    11611161    whd in match assembly_1_pseudoinstruction; normalize nodelta
     
    19231923    cases bitone #bit_one_seven_bits_refl normalize nodelta
    19241924    [ @eq_bv_elim #seven_bits_refl normalize nodelta
    1925     | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
     1925    | FUFFA inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
    19261926      #lookup_from_internal_ram_refl ]
    1927     @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
     1927    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
    19281928    whd in ⊢ (??%?);
    19291929    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1930     whd in ⊢ (??%?);
    1931     @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
    1932     @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
    1933     [1,3,5,7:
    1934       @eq_f2 try %
    1935       @(pose … (set_clock ????)) #status #status_refl
    1936       @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try %
    1937       @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
    1938     |*:
    1939       >EQs >EQticks <instr_refl
    1940       @(write_at_stack_pointer_status_of_pseudo_status 〈low,high,accA〉)
    1941       [2,4,6,8: @set_8051_sfr_status_of_pseudo_status try %
    1942       | >get_8051_sfr_set_8051_sfr
    1943         cut (new_sp = (add … (get_8051_sfr … ps SFR_SP) (bitvector_of_nat … 1)))
    1944         [ >(pair_destruct_2 ????? (sym_eq … carry_new_sp_refl))
    1945           change with (add ??? = ?); @eq_f2 try %
    1946           cases daemon (*CSC: use @get_8051_sfr_status_of_pseudo_status*) ] #EQnew_sp
    1947         >EQnew_sp
    1948         @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
    1949        
    1950      
    1951          XXX
    1952         (*CSC: lemma here*)
    1953         cases accA
    1954         whd in match overwrite_or_delete_from_internal_ram; normalize nodelta
    1955         [ whd whd in match delete_from_internal_ram; normalize nodelta
    1956           @pair_elim #bit_one
    1957         |
    1958         ]
    1959       |
    1960       |
    1961       ]
     1930    whd in match execute_1_0; normalize nodelta
     1931    whd in match execute_1_preinstruction; normalize nodelta
     1932    >bit_one_seven_bits_refl
     1933    [ alias id "write_at_stack_pointer_accA" = "cic:/matita/cerco/ASM/Test3/write_at_stack_pointer_accA.def(29)".
     1934      >seven_bits_refl
     1935      @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉)
     1936      [ @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
     1937        try %
     1938        change with (add ??? = ?); @eq_f2 try %
     1939        @(pose … (set_clock ????)) #status #status_refl
     1940        @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
     1941      | >EQs /demod nohyps/ >add_commutative % ]
     1942    |
     1943    |
     1944    |
    19621945    ]
    19631946  |43: (* POP *)
  • src/ASM/Test.ma

    r2281 r2282  
    20822082 | #addr_entry @internal_pseudo_address_map_equal_up_to_address_insert_into_internal_ram ]
    20832083qed.
     2084
     2085lemma write_at_stack_pointer_status_of_pseudo_status_accA:
     2086 ∀M,cm,sigma,policy,ps,s,sp.
     2087 let w ≝ bitvector_of_nat 8 224 in
     2088 s=status_of_pseudo_status M cm ps sigma policy →
     2089 sp=get_8051_sfr pseudo_assembly_program cm ps SFR_SP →
     2090 write_at_stack_pointer …
     2091  (code_memory_of_pseudo_assembly_program cm sigma policy) s
     2092  (get_arg_8 … (code_memory_of_pseudo_assembly_program cm sigma policy) s false (DIRECT w))
     2093  =status_of_pseudo_status
     2094   (overwrite_or_delete_from_internal_ram sp (\snd M) M)
     2095   cm
     2096   (write_at_stack_pointer pseudo_assembly_program cm ps
     2097    (get_arg_8 pseudo_assembly_program cm ps false (DIRECT w)))
     2098   sigma policy.
     2099 try %
     2100 ** #low #high #accA #cm #sigma #policy #ps #s #sp #EQs #EQsp >EQsp
     2101 @(write_at_stack_pointer_status_of_pseudo_status … 〈low,high,accA〉) try assumption >EQs
     2102 @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
     2103 inversion accA [2:#entry] #EQaccA [2:%] whd in match map_value_using_opt_address_entry; normalize nodelta
     2104 whd in ⊢ (??%?); whd in match status_of_pseudo_status; normalize nodelta
     2105 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta cases entry *
     2106 #addr normalize nodelta @pair_elim #h #l #_ normalize nodelta
     2107 change with (get_index_v ??? 17 ? = ?) @get_index_v_set_index
     2108qed.
     2109
     2110(*CSC: move elsewhere*)
     2111lemma eq_sfr_of_Byte_accA_to_eq:
     2112 ∀w. sfr_of_Byte w = Some … (inl … SFR_ACC_A) → w = bitvector_of_nat 8 224.
     2113 #w whd in match sfr_of_Byte; normalize nodelta
     2114 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2115 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2116 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2117 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2118 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2119 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2120 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2121 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2122 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2123 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2124 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2125 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2126 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2127 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2128 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2129 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2130 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2131 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2132 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2133 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2134 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2135 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2136 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2137 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
     2138 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta
     2139 [ #EQB #_ <(eqb_true_to_eq … EQB) >bitvector_of_nat_inverse_nat_of_bitvector % ] #_
     2140 inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ #abs destruct(abs)
     2141qed.
     2142 
     2143lemma write_at_stack_pointer_sfr_not_accA:
     2144 ∀M,cm,sigma,policy,ps,s,sp,w.
     2145 w ≠ bitvector_of_nat 7 224 →
     2146 s=status_of_pseudo_status M cm ps sigma policy →
     2147 sp=get_8051_sfr pseudo_assembly_program cm ps SFR_SP →
     2148 write_at_stack_pointer …
     2149  (code_memory_of_pseudo_assembly_program cm sigma policy) s
     2150  (get_arg_8 … (code_memory_of_pseudo_assembly_program cm sigma policy) s false (DIRECT (true:::w)))
     2151  =status_of_pseudo_status
     2152   (delete_from_internal_ram sp M)
     2153   cm
     2154   (write_at_stack_pointer pseudo_assembly_program cm ps
     2155    (get_arg_8 pseudo_assembly_program cm ps false (DIRECT (true:::w))))
     2156   sigma policy.
     2157 try %
     2158 ** #low #high #accA #cm #sigma #policy #ps #s #sp #w #NEQw #EQs #EQsp >EQsp
     2159 @(write_at_stack_pointer_status_of_pseudo_status … 〈low,high,accA〉) try assumption >EQs
     2160 @internal_pseudo_address_map_equal_up_to_address_delete_from_internal_ram
     2161 whd in ⊢ (??%%); inversion (sfr_of_Byte ?) normalize nodelta
     2162 [ cases not_implemented
     2163 | ** normalize nodelta #H
     2164   try (@(get_8051_sfr_status_of_pseudo_status … (refl …)) %)
     2165   try (@(get_8052_sfr_status_of_pseudo_status … (refl …)) %)
     2166   @⊥ @(absurd ?? NEQw) lapply(eq_sfr_of_Byte_accA_to_eq … H) #K
     2167   change with ([[true]]@@w=[[true]]@@bitvector_of_nat 7 224) in K;
     2168   cases (bv_append_eq_to_eq … K) #_ #X @X
     2169qed.
Note: See TracChangeset for help on using the changeset viewer.