Changeset 884 for src

Timestamp:

Jun 4, 2011, 6:16:08 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/AssemblyProof.ma (modified) (6 diffs)

src/ASM/AssemblyProof.ma

@@ -455 +455 @@
   (n: nat)
   (l: Vector addressing_mode_tag (S n))
-  (P: addressing_mode → Prop) on l:
+  on l:
+  ∀P: l → Prop.
   ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
   ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
@@ -465 +466 @@
       match y with
       [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
-      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.
+      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
                ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
                ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
@@ -489 +490 @@
   [ VEmpty          ⇒ λAbsurd. ⊥
   | VCons len hd tl ⇒ λProof. ?
-  ] (refl ? (S n)).
+  ] (refl ? (S n)). cases daemon. qed. (*
   [ destruct(Absurd)
   | # A1 # A2 # A3 # A4 # A5 # A6 # A7
@@ -495 +496 @@
     # A15 # A16 # A17 # A18 # A19 # X
     cases X
-    # SUB cases daemon ] qed.(*
+    # SUB cases daemon ] qed.
     cases SUB
     [ # BYTE
@@ -681 +682 @@
  (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
 
+axiom bitvector_elim_complete:
+ ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
+
+lemma bitvector_elim_complete':
+ ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
+ #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
+ generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
+qed.
+
+lemma andb_elim':
+ ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
+ #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
+qed.
+
 lemma test:
   ∀pc,i.
@@ -689 +704 @@
         eq_instruction (\fst instr_pc)) i = true.
  #pc #i cases i #arg try #arg2 whd in ⊢ (??%?)
-   [2,4: @(list_addressing_mode_tags_elim_prop ? [[addr16]] ???????????????????? arg) whd try % #XX
+   [2,4: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
          whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
-       cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP;
-       whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) try cases PP normalize in XX;
-       [1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17: cases XX
-       |*:@split_elim #b1 #b2 #EQ >EQ -EQ;
+         @split_elim #b1 #b2 #EQ >EQ -EQ;
         change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
-        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
-        >lookup_insert_miss //
+        whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)
+        >lookup_insert_miss try @not_eqvb_SS
         >lookup_insert_miss //
         >lookup_insert_hit
-        whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?)
         whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
         >half_add_SO >half_add_SO
-        >lookup_insert_miss [2,4: @not_eqvb_S]
-        >lookup_insert_hit >lookup_insert_hit]
-   |
-        
+        >lookup_insert_miss try @not_eqvb_S
+        >lookup_insert_hit
+        >lookup_insert_hit
+        (* REFL MISSING *)
+        cases daemon
+   |1,3: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
+     whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
+     @split_elim #b1 #b2 #EQ >EQ -EQ;
+     change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
+     whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)
+     >lookup_insert_miss //
+     >lookup_insert_hit
+     generalize in match b1 @(bitvector_elim_complete')
+     @andb_elim' @andb_elim' @andb_elim' whd in ⊢ (??%?)
+     >half_add_SO >lookup_insert_hit normalize
+     (* FALSO!!! AJMP vs ACALL *)
+   
+     
+     whd in ⊢ (??%?) whd in ⊢ (??(match % with [ _ ⇒ % | _ ⇒ ?])?)
+     check andb_elim.
+      (λV.(let 〈instr_pc,ticks〉 ≝
+           fetch0
+           (insert Byte 16 (bitvector_of_nat 16 (S pc)) b2
+            (insert Byte 16 (bitvector_of_nat 16 pc)
+             (V@@[[true; false; false; false; true]]) (Stub Byte 16)))
+           〈\snd  (half_add 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 1)),
+           V@@[[true; false; false; false; true]]〉 in 
+    eq_instruction (\fst  instr_pc))
+   (ACALL (ADDR11 (V@@b2)))) ?)
+     whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
+     >half_add_SO
+