Changeset 2279 for src/ASM/Test.ma

Timestamp:

Jul 30, 2012, 11:44:50 PM (9 years ago)

Author:

sacerdot

Message:

1. Bug fixed in the semantics of PUSH (no indirection performed)
2. Proved write_at_stack_pointer_status_of_pseudo_status
3. PUSH case of main lemma almost done

File:

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

src/ASM/Test.ma

@@ -1945 +1945 @@
 *)
 
-(*
+definition internal_pseudo_address_map_equal_up_to_low ≝
+ λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M').
+
+lemma set_low_internal_ram_status_of_pseudo_status:
+ ∀cm,sigma,policy,M,M',s,s',ram,ram'.
+  internal_pseudo_address_map_equal_up_to_low M M' →
+  s' = status_of_pseudo_status M' cm s sigma policy →
+  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
+  set_low_internal_ram (BitVectorTrie Byte 16)
+  (code_memory_of_pseudo_assembly_program cm sigma policy)
+  s'
+  ram'
+  = status_of_pseudo_status M cm
+    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
+  #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
+  cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
+  #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
+qed.
+
+definition internal_pseudo_address_map_equal_up_to_high ≝
+ λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \fst (\fst M) = \fst (\fst M').
+
+lemma set_high_internal_ram_status_of_pseudo_status:
+ ∀cm,sigma,policy,M,M',s,s',ram,ram'.
+  internal_pseudo_address_map_equal_up_to_high M M' →
+  s' = status_of_pseudo_status M' cm s sigma policy →
+  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\snd (\fst M)) →
+  set_high_internal_ram (BitVectorTrie Byte 16)
+  (code_memory_of_pseudo_assembly_program cm sigma policy)
+  s'
+  ram'
+  = status_of_pseudo_status M cm
+    (set_high_internal_ram pseudo_assembly_program cm s ram) sigma policy.
+  #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
+  cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
+  #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
+qed.
+
+definition internal_pseudo_address_map_equal_up_to_address ≝
+ λM,M',sigma,addr,v,v'.
+  let 〈low,high,accA〉 ≝ M in
+  let 〈low',high',accA'〉 ≝ M' in
+  let 〈bit_one,seven_bits〉 ≝ vsplit bool 1 7 addr in
+   if head' … 0 bit_one then
+    (internal_pseudo_address_map_equal_up_to_high M' M ∧
+     internal_half_pseudo_address_map_equal_up_to_address high high' sigma
+      seven_bits v v')
+   else
+    (internal_pseudo_address_map_equal_up_to_low M' M ∧
+      internal_half_pseudo_address_map_equal_up_to_address low low' sigma
+       seven_bits v v').
+  
 lemma write_at_stack_pointer_status_of_pseudo_status:
   ∀M, M'.
@@ -1952 +2003 @@
   ∀policy.
   ∀s, s'.
-  ∀new_b, new_b'.
-    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
-    status_of_pseudo_status M cm s sigma policy = s' →
-    write_at_stack_pointer ?? s' new_b' =
-    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
-  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
-  #new_b_refl #s_refl <new_b_refl <s_refl
+  ∀v, v'.
+    internal_pseudo_address_map_equal_up_to_address M M' sigma
+     (get_8051_sfr ?? s SFR_SP) v v' →
+    s' = status_of_pseudo_status M cm s sigma policy →
+    write_at_stack_pointer ?? s' v' =
+    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s v) sigma policy.
+  ** #low #high #accA ** #low' #high' #accA'
+  #cm #sigma #policy #s #s' #v #v' #H whd in H; #s_refl >s_refl
   whd in match write_at_stack_pointer; normalize nodelta
-  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
-  @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
-  [1:
-    @eq_f
-    whd in match get_8051_sfr; normalize nodelta
-    whd in match sfr_8051_index; normalize nodelta
+  >(get_8051_sfr_status_of_pseudo_status … (refl …) … (refl …)) lapply H; -H
+  @vsplit_elim #bit_one #seven_bits cases (Vector_Sn … bit_one) #bitone * #tl
+  >(Vector_O … tl) #EQbit_one >EQbit_one -bit_one normalize nodelta cases bitone
+  #bit_one_seven_bits_refl normalize nodelta * #H1 #H2
+  [ @(set_high_internal_ram_status_of_pseudo_status … 〈low',high',accA'〉 〈low,high,accA〉)
+    try @refl try assumption
     whd in match status_of_pseudo_status; normalize nodelta
-    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
-    cases (\snd M) [2: * #address ] normalize nodelta
-    [1,2:
-      cases (vsplit bool ???) #high #low normalize nodelta
-      whd in match sfr_8051_index; normalize nodelta
-      >get_index_v_set_index_miss %
-      #absurd destruct(absurd)
-    |3:
-      %
-    ]
-  |2:
-    @if_then_else_status_of_pseudo_status try %
-    [2:
-      @sym_eq <set_low_internal_ram_status_of_pseudo_status
-      [1:
-        @eq_f2
-        [2:
-          @insert_low_internal_ram_of_pseudo_low_internal_ram'
-    @sym_eq
-    [2:
-      <set_low_internal_ram_status_of_pseudo_status
-      [1:
-        @eq_f2
-        [2:
-          @sym_eq
-          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
-          [2:
-            >new_b_refl
-    ]
+    whd in match high_internal_ram_of_pseudo_high_internal_ram; normalize nodelta
+    @insert_internal_ram_of_pseudo_internal_ram assumption
+  | @(set_low_internal_ram_status_of_pseudo_status … 〈low',high',accA'〉 〈low,high,accA〉)
+    try @refl try assumption
+    whd in match status_of_pseudo_status; normalize nodelta
+    whd in match low_internal_ram_of_pseudo_low_internal_ram; normalize nodelta
+    @insert_internal_ram_of_pseudo_internal_ram assumption
   ]
-qed.*)
+qed.
+
+(*CSC: move elsewhere and generalize*)
+axiom lookup_opt_delete_miss:
+ ∀n.∀M:BitVectorTrie address_entry n.∀addr,addr': BitVector n.
+  addr' ≠ addr →
+     lookup_opt address_entry n addr' (delete address_entry n addr M)
+   = lookup_opt address_entry n addr' M.
+
+(*CSC: move elsewhere and generalize*)
+axiom lookup_opt_delete_hit:
+ ∀n.∀M:BitVectorTrie address_entry n.∀addr: BitVector n.
+  lookup_opt address_entry n addr (delete address_entry n addr M) = None ….
+
+lemma internal_pseudo_address_map_equal_up_to_address_delete_from_internal_ram:
+ ∀M,sigma,addr,v1,v2.
+  v2=v1 →
+  internal_pseudo_address_map_equal_up_to_address M
+   (delete_from_internal_ram addr M) sigma addr v1 v2.
+ ** #low #high #accA #sigma #addr #v1 #v2 * whd in match delete_from_internal_ram;
+ normalize nodelta @vsplit_elim #bit_one #seven_bits
+ cases (Vector_Sn … bit_one) ** #tl >(Vector_O … tl) #EQ >EQ #EQ2 normalize nodelta
+ >EQ2 whd whd in match (tail ???); % % try %
+ [2,4: #addr #addr' >lookup_opt_delete_miss try assumption %
+ |1,3: >lookup_opt_delete_hit % ]
+qed.
+
+lemma internal_pseudo_address_map_equal_up_to_address_insert_into_internal_ram:
+ ∀M,sigma,addr,entry,v1,v2.
+  v2=map_value_using_opt_address_entry sigma v1 (Some address_entry entry) →
+  internal_pseudo_address_map_equal_up_to_address M
+   (insert_into_internal_ram addr entry M) sigma addr v1 v2.
+ ** #low #high #accA #sigma #addr #entry #v1 #v2 #H whd in match insert_into_internal_ram;
+ normalize nodelta whd in match internal_pseudo_address_map_equal_up_to_address;
+ normalize nodelta @vsplit_elim #bit_one cases (Vector_Sn … bit_one) ** #tl
+ >(Vector_O … tl) #EQ >EQ #seven_bits #EQ2 normalize nodelta >EQ2 % % try %
+ [2,4: #addr' #NEQ >lookup_opt_insert_miss try % >eq_bv_false try % #EQ @(absurd … EQ NEQ)
+ |1,3: >lookup_opt_insert_hit assumption ]
+qed.
+
+lemma internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram:
+ ∀M,sigma,addr,v1,v2,entry.
+  v2=map_value_using_opt_address_entry sigma v1 entry →
+  internal_pseudo_address_map_equal_up_to_address M
+  (overwrite_or_delete_from_internal_ram addr entry M) sigma addr v1 v2.
+ ** #low #high #accA #sigma #addr #v1 #v2 #entry
+ whd in match overwrite_or_delete_from_internal_ram; normalize nodelta
+ cases entry normalize nodelta
+ [ @internal_pseudo_address_map_equal_up_to_address_delete_from_internal_ram
+ | #addr_entry @internal_pseudo_address_map_equal_up_to_address_insert_into_internal_ram ]
+qed.