Changeset 2209

Timestamp:

Jul 18, 2012, 2:56:12 PM (7 years ago)

Author:

mulligan

Message:

Closed major daemons in the supporting lemmas of the main lemma.

Location:

src/ASM

Files:

• AssemblyProof.ma (modified) (1 diff)
• AssemblyProofSplit.ma (modified) (5 diffs)

src/ASM/AssemblyProof.ma

@@ -473 +473 @@
          ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
     | INDIRECT i ⇒
-       let d ≝ get_register … s [[false;false;i]] in
-       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
+        let d ≝ get_register … s [[false;false;i]] in
+        let address ≝ bit_address_of_register … s [[false;false;i]] in
+          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧
+            ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
     | EXT_INDIRECT _ ⇒ true
     | REGISTER r ⇒

src/ASM/AssemblyProofSplit.ma

@@ -98 +98 @@
 qed.
 
-lemma lookup_low_internal_ram_false:
-  ∀cm: pseudo_assembly_program.
-  ∀status.
-  ∀b, b': BitVector 7.
-    b = b' →
-    lookup … b (low_internal_ram … cm status) (zero 8) = false:::b'.
-  #cm * #low_internal_ram #high_internal_ram #external_ram #program_counter
-  #sfr_8051 #sfr_8052 #p1_latch #p3_latch #clock #b #b' #b_refl
-  cases daemon (* XXX: cannot eliminate, case analyse or invert the BitVectorTrie *)
-qed.
-
 lemma sfr_psw_eq_to_bit_address_of_register_eq:
   ∀A: Type[0].
@@ -148 +137 @@
     #_
     @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
-    whd in match get_register; normalize nodelta
-    cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false
-    @sfr_psw_eq_to_bit_address_of_register_eq assumption (* XXX: dubious *)
+    <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption
   ]
 qed.
-(* XXX: indirect case false above *)
 
+lemma not_b_c_to_b_not_c:
+  ∀b, c: bool.
+    (¬b) = c → b = (¬c).
+  //
+qed.
+(* XXX: move above elsewhere *)
+
+lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
+  ∀M.
+  ∀sigma.
+  ∀sfr8051.
+  ∀b.
+    sfr8051 ≠ SFR_ACC_A →
+      map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
+  #M #sigma * #b
+  [18:
+    #relevant cases (absurd … (refl ??) relevant)
+  ]
+  #_ %
+qed.
+
+lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
+  ∀M.
+  ∀sigma: Word → Word.
+  ∀w: BitVector 8.
+  ∀b.
+    w ≠ bitvector_of_nat … 224 →
+      map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
+  #M #sigma #w #b #w_neq_assm
+  whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
+  [1:
+    #sfr_of_Byte_refl %
+  |2:
+    * #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
+    @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
+    #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
+    @(absurd ?? w_neq_assm)
+    lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
+    whd in match sfr_of_Byte; normalize nodelta
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
+    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
+    #absurd destruct(absurd)
+qed.
+
+lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
+  ∀M, sigma, w, b.
+    assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst  M) = false →
+      map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
+  #M #sigma #w #b #assoc_list_exists_assm
+  whd in ⊢ (??%?);
+  >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
+qed.
+    
 lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
   ∀M', cm.
@@ -184 +247 @@
       normalize nodelta %
     |4:
-      #_
+      #assoc_list_exists_assm lapply (not_b_c_to_b_not_c … assoc_list_exists_assm)
+      -assoc_list_exists_assm #assoc_list_exists_assm
       <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl)
-      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
+      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm)
       normalize nodelta %
     ]
   |3:
     #w whd in ⊢ (??%? → ??%?);
-    cases daemon (* XXX: ??? *)
+    @eq_bv_elim #eq_bv_refl normalize nodelta
+    [1:
+      #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm)
+      #assoc_list_exists_refl #eq_accumulator_refl
+      >eq_bv_refl change with (map_address_Byte_using_internal_pseudo_address_map M' sigma (bitvector_of_nat 8 224) b = b)
+      whd in ⊢ (??%?); >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_refl)
+      %
+    |2:
+      #assoc_list_exists_assm
+      @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
+      cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl
+      <head_head' inversion bit #bit_refl normalize nodelta
+      >bit_one_refl in bit_one_seven_bits_refl; >bit_refl #w_refl normalize in w_refl;
+      [1:
+        @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map <w_refl assumption
+      |2:
+        @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map
+        <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm)
+      ]
+    ]
   |5,6:
     #w #_ %
@@ -700 +783 @@
       change with (set_arg_8 ????? = ?)
       @set_arg_8_status_of_pseudo_status try %
-      [ @sym_eq @set_clock_status_of_pseudo_status
-        [ @sym_eq >EQs @set_program_counter_status_of_pseudo_status %
-        | >EQs >EQticks <instr_refl >addr_refl @eq_f2 %
-        ]
-      | @(subaddressing_mode_elim … acc_a) @I
-      | >EQs >EQticks <instr_refl >addr_refl
+      >EQs >EQticks <instr_refl >addr_refl
+      [1:
+        @sym_eq @set_clock_status_of_pseudo_status
+        [1:
+          @sym_eq @set_program_counter_status_of_pseudo_status %
+        |2:
+          @eq_f2 %
+        ]
+      |2:
+        @(subaddressing_mode_elim … acc_a) @I
+      |3:
         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
         [1:
           @(subaddressing_mode_elim … acc_a) %
-        |2:
-          %
-        |3:
-          %
         |4:
           @eq_f2
@@ -719 +803 @@
           [1:
             @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
-            [1:
-              @(subaddressing_mode_elim … acc_a) %
-            |*:
-              %
-            ]
+            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
           |3:
             @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
-            [1:
-              /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
-            |*:
-              %
-            ]
+            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
           |2:
             @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
-            [1:
-              @(subaddressing_mode_elim … acc_a) %
-            |2:
-              %
-            ]
+            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
           |4:
             @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
-            [1:
-              /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
-            |*:
-              %
-            ]
+            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
           ]
+        |*:
+          %
         ]
       ]