Changeset 2282 for src/ASM/Test.ma

Timestamp:

Jul 31, 2012, 6:08:00 PM (8 years ago)

Author:

sacerdot

Message:

PUSH case almost finished

File:

• src/ASM/Test.ma (modified) (1 diff)

src/ASM/Test.ma

@@ -2082 +2082 @@
  | #addr_entry @internal_pseudo_address_map_equal_up_to_address_insert_into_internal_ram ]
 qed.
+
+lemma write_at_stack_pointer_status_of_pseudo_status_accA:
+ ∀M,cm,sigma,policy,ps,s,sp.
+ let w ≝ bitvector_of_nat 8 224 in
+ s=status_of_pseudo_status M cm ps sigma policy →
+ sp=get_8051_sfr pseudo_assembly_program cm ps SFR_SP →
+ write_at_stack_pointer …
+  (code_memory_of_pseudo_assembly_program cm sigma policy) s
+  (get_arg_8 … (code_memory_of_pseudo_assembly_program cm sigma policy) s false (DIRECT w))
+  =status_of_pseudo_status
+   (overwrite_or_delete_from_internal_ram sp (\snd M) M)
+   cm
+   (write_at_stack_pointer pseudo_assembly_program cm ps
+    (get_arg_8 pseudo_assembly_program cm ps false (DIRECT w)))
+   sigma policy.
+ try %
+ ** #low #high #accA #cm #sigma #policy #ps #s #sp #EQs #EQsp >EQsp
+ @(write_at_stack_pointer_status_of_pseudo_status … 〈low,high,accA〉) try assumption >EQs
+ @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
+ inversion accA [2:#entry] #EQaccA [2:%] whd in match map_value_using_opt_address_entry; normalize nodelta
+ whd in ⊢ (??%?); whd in match status_of_pseudo_status; normalize nodelta
+ whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta cases entry *
+ #addr normalize nodelta @pair_elim #h #l #_ normalize nodelta
+ change with (get_index_v ??? 17 ? = ?) @get_index_v_set_index
+qed.
+
+(*CSC: move elsewhere*)
+lemma eq_sfr_of_Byte_accA_to_eq:
+ ∀w. sfr_of_Byte w = Some … (inl … SFR_ACC_A) → w = bitvector_of_nat 8 224.
+ #w whd in match sfr_of_Byte; normalize nodelta
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ [#abs destruct(abs)]
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta
+ [ #EQB #_ <(eqb_true_to_eq … EQB) >bitvector_of_nat_inverse_nat_of_bitvector % ] #_
+ inversion (eqb (nat_of_bitvector 8 w) ?) normalize nodelta #_ #abs destruct(abs)
+qed.
+ 
+lemma write_at_stack_pointer_sfr_not_accA:
+ ∀M,cm,sigma,policy,ps,s,sp,w.
+ w ≠ bitvector_of_nat 7 224 →
+ s=status_of_pseudo_status M cm ps sigma policy →
+ sp=get_8051_sfr pseudo_assembly_program cm ps SFR_SP →
+ write_at_stack_pointer …
+  (code_memory_of_pseudo_assembly_program cm sigma policy) s
+  (get_arg_8 … (code_memory_of_pseudo_assembly_program cm sigma policy) s false (DIRECT (true:::w)))
+  =status_of_pseudo_status
+   (delete_from_internal_ram sp M)
+   cm
+   (write_at_stack_pointer pseudo_assembly_program cm ps
+    (get_arg_8 pseudo_assembly_program cm ps false (DIRECT (true:::w))))
+   sigma policy.
+ try %
+ ** #low #high #accA #cm #sigma #policy #ps #s #sp #w #NEQw #EQs #EQsp >EQsp
+ @(write_at_stack_pointer_status_of_pseudo_status … 〈low,high,accA〉) try assumption >EQs
+ @internal_pseudo_address_map_equal_up_to_address_delete_from_internal_ram
+ whd in ⊢ (??%%); inversion (sfr_of_Byte ?) normalize nodelta
+ [ cases not_implemented
+ | ** normalize nodelta #H
+   try (@(get_8051_sfr_status_of_pseudo_status … (refl …)) %)
+   try (@(get_8052_sfr_status_of_pseudo_status … (refl …)) %)
+   @⊥ @(absurd ?? NEQw) lapply(eq_sfr_of_Byte_accA_to_eq … H) #K
+   change with ([[true]]@@w=[[true]]@@bitvector_of_nat 7 224) in K;
+   cases (bv_append_eq_to_eq … K) #_ #X @X
+qed.