Changeset 2284 for src/ASM/Test.ma


Ignore:
Timestamp:
Aug 1, 2012, 4:56:20 PM (8 years ago)
Author:
sacerdot
Message:

PUSH finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2282 r2284  
    21412141qed.
    21422142 
    2143 lemma write_at_stack_pointer_sfr_not_accA:
     2143lemma write_at_stack_pointer_status_of_pseudo_status_sfr_not_accA:
    21442144 ∀M,cm,sigma,policy,ps,s,sp,w.
    21452145 w ≠ bitvector_of_nat 7 224 →
     
    21682168   cases (bv_append_eq_to_eq … K) #_ #X @X
    21692169qed.
     2170 
     2171lemma write_at_stack_pointer_status_of_pseudo_status_low:
     2172 ∀M,cm,sigma,policy,ps,s,sp,w.
     2173 s=status_of_pseudo_status M cm ps sigma policy →
     2174 sp=get_8051_sfr pseudo_assembly_program cm ps SFR_SP →
     2175 write_at_stack_pointer …
     2176  (code_memory_of_pseudo_assembly_program cm sigma policy) s
     2177  (get_arg_8 … (code_memory_of_pseudo_assembly_program cm sigma policy) s false (DIRECT (false:::w)))
     2178  =status_of_pseudo_status
     2179   (overwrite_or_delete_from_internal_ram sp (lookup_from_internal_ram … (false:::w) M) M)
     2180   cm
     2181   (write_at_stack_pointer pseudo_assembly_program cm ps
     2182    (get_arg_8 pseudo_assembly_program cm ps false (DIRECT (false:::w))))
     2183   sigma policy.
     2184 try %
     2185 ** #low #high #accA #cm #sigma #policy #ps #s #sp #w #EQs #EQsp >EQsp
     2186 @(write_at_stack_pointer_status_of_pseudo_status … 〈low,high,accA〉) try assumption >EQs
     2187 @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
     2188 whd in ⊢ (??%?); whd in match status_of_pseudo_status; normalize nodelta
     2189 whd in match low_internal_ram_of_pseudo_low_internal_ram; normalize nodelta
     2190 whd in match internal_ram_of_pseudo_internal_ram; normalize nodelta
     2191 lapply (lookup_opt_bvt_map2 … (low_internal_ram pseudo_assembly_program cm ps) low
     2192   (map_opt_value_using_opt_address_entry sigma) w)
     2193 inversion (lookup_opt ????) [2:#x] #EQ1
     2194 (*CSC: Take lemmas out*)
     2195 [2: >(lookup_opt_lookup_miss … EQ1)
     2196   whd in match map_opt_value_using_opt_address_entry; normalize nodelta
     2197   inversion (eq_bv ???) normalize nodelta [2: #_ #abs destruct(abs)]
     2198   #EQ2 #_ <(eq_bv_eq … EQ2) @eq_f2 try %
     2199   whd in match get_arg_8; normalize nodelta
     2200   inversion (lookup_opt ????) [2:#res] #EQ3
     2201   [2: >(lookup_opt_lookup_miss … EQ3) % | >(lookup_opt_lookup_hit … EQ3 (zero 8)) %]
     2202 | >(lookup_opt_lookup_hit … EQ1 (zero 8))
     2203   whd in match map_opt_value_using_opt_address_entry; normalize nodelta
     2204   inversion (eq_bv ???) normalize nodelta [#_ #abs destruct(abs)]
     2205   #EQ2 @Some_Some_elim #EQ3 >EQ3 @eq_f2 try %
     2206   whd in match get_arg_8; normalize nodelta
     2207   inversion (lookup_opt ????) [2:#res] #EQ3
     2208   [2: >(lookup_opt_lookup_miss … EQ3) % | >(lookup_opt_lookup_hit … EQ3 (zero 8)) %]   
     2209qed.
Note: See TracChangeset for help on using the changeset viewer.