Changeset 2282 for src/ASM/Test.ma


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

PUSH case almost finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.