Changeset 2272 for src/ASM/Test.ma

Timestamp:

Jul 27, 2012, 5:53:25 PM (8 years ago)

Author:

mulligan

Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:

• src/ASM/Test.ma (modified) (14 diffs)

src/ASM/Test.ma

@@ -96 +96 @@
   λM, sigma, v.
   match \snd M with
-  [ data ⇒ v
-  | address upper_lower word ⇒
-    let mapped ≝ sigma word in
-    let 〈high, low〉 ≝ vsplit bool 8 8 mapped in
+  [ None ⇒ v
+  | Some upper_lower_addr ⇒
+    let 〈upper_lower, addr〉 ≝ upper_lower_addr in
       if eq_upper_lower upper_lower upper then
-        high
+        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
+          high
       else
-        low
+        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
+          low
   ].
 
@@ -113 +114 @@
   λaddress: Byte.
   λvalue: Byte.
-  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
+  match lookup_from_internal_ram … address M with
   [ None ⇒ value
   | Some upper_lower_word ⇒
     let 〈upper_lower, word〉 ≝ upper_lower_word in
-    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
       if eq_upper_lower upper_lower upper then
-        high
+        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
+          high
       else
-        low
+        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
+          low
   ].
 
@@ -216 +218 @@
 qed.
 
+lemma get_index_v_set_index_hit:
+  ∀A: Type[0].
+  ∀n: nat.
+  ∀v: Vector A n.
+  ∀i: nat.
+  ∀e: A.
+  ∀i_lt_n_proof: i < n.
+  ∀i_lt_n_proof': i < n.
+    get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
+  #A #n #v elim v
+  [1:
+    #i #e #i_lt_n_proof
+    cases (lt_to_not_zero … i_lt_n_proof)
+  |2:
+    #n' #hd #tl #inductive_hypothesis #i #e
+    cases i
+    [1:
+      #i_lt_n_proof #i_lt_n_proof' %
+    |2:
+      #i' #i_lt_n_proof' #i_lt_n_proof''
+      whd in ⊢ (??%?); @inductive_hypothesis
+    ]
+  ]
+qed.
+
 lemma set_index_status_of_pseudo_status:
   ∀M, code_memory, sigma, policy, s, sfr, v, v'.
@@ -230 +257 @@
   whd in match status_of_pseudo_status; normalize nodelta
   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
-  inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
+  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
   [1:
     <sfr_neq_acc_a_assm cases sfr
@@ -240 +267 @@
     %
   |2:
+    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
     @pair_elim #high #low #high_low_refl normalize nodelta
-    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
-    <sfr_neq_acc_a_assm cases sfr
+    whd in match set_8051_sfr; normalize nodelta
+    <sfr_neq_acc_a_assm
+    cases sfr in high_low_refl sfr_neq_acc_a_assm; 
     [18,37:
+      @pair_elim #high' #low' #high_low_refl'
+      #high_low_refl
       whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
       whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
-      >sndM_refl normalize nodelta >high_low_refl normalize nodelta 
+      >sndM_refl normalize nodelta
       >eq_upper_lower_refl normalize nodelta
-      whd in match (set_8051_sfr ?????);
       [1:
+        #relevant >relevant
         <set_index_set_index_overwrite in ⊢ (??%?);
-        <set_index_set_index_overwrite in ⊢ (???%); %
+        <set_index_set_index_overwrite in ⊢ (???%);
+        >get_index_v_set_index_hit in high_low_refl'; 
+        #assm >assm in relevant; normalize nodelta * %
       |2:
+        #relevant >relevant
         <set_index_set_index_overwrite in ⊢ (??%?);
-        <set_index_set_index_overwrite in ⊢ (???%); %
+        <set_index_set_index_overwrite in ⊢ (???%);
+        >get_index_v_set_index_hit in high_low_refl'; 
+        #assm >assm in relevant; normalize nodelta * %
       ]
     ]
     whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
-    whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize
-    @nmk #absurd destruct(absurd)
+    #relevant * >get_index_v_set_index_miss
+    try (% #absurd normalize in absurd; destruct(absurd))
+    >relevant normalize nodelta
+    @set_index_set_index_commutation % #absurd normalize in absurd; destruct(absurd)
   ]
 qed.
 
+(*
 lemma get_index_v_status_of_pseudo_status:
   ∀M, code_memory, sigma, policy, s, s', sfr.
@@ -301 +340 @@
   ]
 qed.
+*)
 
 lemma set_8051_sfr_status_of_pseudo_status:
@@ -313 +353 @@
 qed.
 
+(*
 lemma get_8051_sfr_status_of_pseudo_status:
   ∀M, code_memory, sigma, policy, s, s', s'', sfr.
@@ -324 +365 @@
   whd in match get_8051_sfr; normalize nodelta
   @get_index_v_status_of_pseudo_status %
-qed.
+qed.*)
 
 lemma get_8052_sfr_status_of_pseudo_status:
@@ -424 +465 @@
   (code_memory_of_pseudo_assembly_program cm sigma policy)
   s'
-  (low_internal_ram_of_pseudo_low_internal_ram M ram)
+  (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
   = status_of_pseudo_status M cm
     (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
@@ -435 +476 @@
  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
   insert Byte 7 addr v'
-  (low_internal_ram_of_pseudo_low_internal_ram M
+  (low_internal_ram_of_pseudo_low_internal_ram M sigma
    (low_internal_ram pseudo_assembly_program cm s))
-  =low_internal_ram_of_pseudo_low_internal_ram M
+  =low_internal_ram_of_pseudo_low_internal_ram M sigma
    (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
                
@@ -447 +488 @@
     (code_memory_of_pseudo_assembly_program cm sigma policy)
     (status_of_pseudo_status M cm s sigma policy))
-  = low_internal_ram_of_pseudo_low_internal_ram M
+  = low_internal_ram_of_pseudo_low_internal_ram M sigma
      (insert Byte 7 addr v
       (low_internal_ram pseudo_assembly_program cm s)).
@@ -458 +499 @@
  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
   insert Byte 7 addr v'
-  (high_internal_ram_of_pseudo_high_internal_ram M
+  (high_internal_ram_of_pseudo_high_internal_ram M sigma
    (high_internal_ram pseudo_assembly_program cm s))
-  =high_internal_ram_of_pseudo_high_internal_ram M
+  =high_internal_ram_of_pseudo_high_internal_ram M sigma
    (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
 
@@ -470 +511 @@
     (code_memory_of_pseudo_assembly_program cm sigma policy)
     (status_of_pseudo_status M cm s sigma policy))
-  = high_internal_ram_of_pseudo_high_internal_ram M
+  = high_internal_ram_of_pseudo_high_internal_ram M sigma
      (insert Byte 7 addr v
       (high_internal_ram pseudo_assembly_program cm s)).
@@ -1374 +1415 @@
   >get_index_v_set_index_miss [2,4: /2/] %
 qed.
+
+lemma get_8051_sfr_status_of_pseudo_status:
+  ∀M.
+  ∀cm, ps, sigma, policy.
+  ∀sfr.
+    (sfr = SFR_ACC_A → \snd M = None …) →
+    get_8051_sfr (BitVectorTrie Byte 16)
+      (code_memory_of_pseudo_assembly_program cm sigma policy)
+      (status_of_pseudo_status M cm ps sigma policy) sfr =
+    get_8051_sfr pseudo_assembly_program cm ps sfr.
+  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
+  [18:
+     >relevant %
+  ]
+  cases sndM try % * #address
+  whd in match get_8051_sfr;
+  whd in match status_of_pseudo_status; normalize nodelta
+  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
+  cases (eq_upper_lower ??) normalize nodelta
+  @pair_elim #upper #lower #upper_lower_refl
+  @get_index_v_set_index_miss @nmk #relevant
+  normalize in relevant; destruct(relevant)
+qed.
+
+lemma get_arg_8_pseudo_addressing_mode_ok:
+  ∀M: internal_pseudo_address_map.
+  ∀cm: pseudo_assembly_program.
+  ∀ps: PreStatus pseudo_assembly_program cm.
+  ∀sigma: Word → Word.
+  ∀policy: Word → bool.
+  ∀addr1: [[registr; direct]].
+    assert_data pseudo_assembly_program M cm ps addr1 = true →
+      get_arg_8 (BitVectorTrie Byte 16)
+        (code_memory_of_pseudo_assembly_program cm sigma policy)
+        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
+      get_arg_8 pseudo_assembly_program cm ps true addr1.
+  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
+  #M #cm #ps #sigma #policy #addr1
+  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
+  [1:
+    whd in ⊢ (??%? → ??%?);
+    whd in match bit_address_of_register; normalize nodelta
+    @pair_elim #un #ln #un_ln_refl
+    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
+    @(pair_replace ?????????? un_ln_refl)
+    [1:
+      whd in match get_8051_sfr; normalize nodelta
+      whd in match sfr_8051_index; normalize nodelta
+      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
+      try % #absurd destruct(absurd)
+    |2:
+      #assembly_mode_ok_refl
+      >low_internal_ram_of_pseudo_internal_ram_miss
+      [1:
+        %
+      |2:
+        cases (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta
+        [1:
+          #absurd destruct(absurd)
+        |2:
+          * normalize nodelta
+          [1:
+          |2:
+            #_ #absurd destruct(absurd)
+          ]
+        #absurd try % @sym_eq assumption
+      ]
+    ]
+  |2:
+    #addressing_mode_ok_refl whd in ⊢ (??%?);
+    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
+    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
+    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
+    [1:
+      whd in ⊢ (??%%); normalize nodelta
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1: % ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ]
+      inversion (eqb ??) #eqb_refl normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
+        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
+        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
+        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
+        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
+      ]
+      cases (eqb ??) normalize nodelta [1:
+        @get_8051_sfr_status_of_pseudo_status
+        #absurd destruct(absurd)
+      ] %
+    |2:
+      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
+      whd in match status_of_pseudo_status; normalize nodelta
+      >low_internal_ram_of_pseudo_internal_ram_miss try %
+      cut(arg = false:::(three_bits@@nl))
+      [1:
+        <get_index_v_refl
+        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
+        [1:
+          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
+          [1:
+            @le_S_S @le_O_n
+          |2:
+            cut(ignore = \fst (vsplit bool 1 3 nu))
+            [1:
+              >ignore_three_bits_refl %
+            |2:
+              #ignore_refl >ignore_refl
+              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
+              >nu_refl %
+            ]
+          |3:
+            #ignore_refl >ignore_refl in ignore_three_bits_refl;
+            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
+            #nu_refl <nu_refl %
+          ]
+        |2:
+          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
+          @sym_eq @vsplit_ok >nu_nl_refl %
+        ]
+      |2:
+        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
+        normalize nodelta
+        [1:
+          cases (eq_bv ???) normalize #absurd destruct(absurd)
+        |2:
+          #_ %
+        ]
+      ]
+    ]
+  ] *)
+qed.