Changeset 2284


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

PUSH finished

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2282 r2284  
    445445    BitVectorTrie C n.
    446446
     447(*
    447448axiom is_in_domain:
    448449  ∀A: Type[0].
     
    462463        f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) →
    463464          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
     465*)
     466
     467axiom lookup_opt_bvt_map2:
     468 ∀A,B,C,n,map1,map2,f,addr.
     469lookup_opt … addr (bvt_map2 A B C n map1 map2 f) =
     470 f (lookup_opt … addr map1) (lookup_opt … addr map2).
    464471
    465472definition lookup_from_internal_ram:
  • src/ASM/AssemblyProofSplit.ma

    r2283 r2284  
    23762376    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
    23772377    cases bitone #bit_one_seven_bits_refl normalize nodelta
    2378     [ @eq_bv_elim #seven_bits_refl normalize nodelta
    2379     | FUFFA inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
    2380       #lookup_from_internal_ram_refl ]
     2378    [ @eq_bv_elim #seven_bits_refl normalize nodelta ]
    23812379    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
    23822380    whd in ⊢ (??%?);
     
    23852383    whd in match execute_1_preinstruction; normalize nodelta
    23862384    >bit_one_seven_bits_refl
    2387     [ alias id "write_at_stack_pointer_accA" = "cic:/matita/cerco/ASM/Test3/write_at_stack_pointer_accA.def(29)".
    2388       >seven_bits_refl
     2385    [ >seven_bits_refl
    23892386      @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉)
    2390       [ @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
    2391         try %
    2392         change with (add ??? = ?); @eq_f2 try %
    2393         @(pose … (set_clock ????)) #status #status_refl
    2394         @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
    2395       | >EQs /demod nohyps/ >add_commutative % ]
    2396     |
    2397     |
    2398     |
    2399     ]
     2387    | @write_at_stack_pointer_status_of_pseudo_status_sfr_not_accA [1:assumption]
     2388    | @write_at_stack_pointer_status_of_pseudo_status_low ]
     2389    [1,3,5: @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
     2390      try %
     2391      change with (add ??? = ?); @eq_f2 try %
     2392      @(pose … (set_clock ????)) #status #status_refl
     2393      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
     2394    |*: >EQs /demod nohyps/ >add_commutative % ]
    24002395  |43: (* POP *)
    24012396    cases daemon
  • 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.