Changeset 1927 for src/ASM/ASMCosts.ma

Timestamp:

05/09/12 13:05:21 (13 months ago)

Author:

mulligan

Message:

Reduced complexity of good_program predicate, ported to new notion of as_label, reintroduced some deleted code from common/StructuredTraces.ma.

Files:

• src/ASM/ASMCosts.ma (modified) (15 diffs)

src/ASM/ASMCosts.ma

@@ -63 +63 @@
       ]
     | LCALL addr         ⇒
-      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
+      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
+        nat_of_bitvector … program_counter' < total_program_size
+      (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
       [ ADDR16 addr ⇒ λaddr16: True.
           reachable_program_counter code_memory total_program_size addr ∧
@@ -69 +71 @@
               nat_of_bitvector … program_counter' < total_program_size
       | _ ⇒ λother: False. ⊥
-      ] (subaddressing_modein … addr)
+      ] (subaddressing_modein … addr) *)
     | ACALL addr         ⇒
-      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
+      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
+        nat_of_bitvector … program_counter' < total_program_size
+      (* match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
       [ ADDR11 addr ⇒ λaddr11: True.
         let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
@@ -81 +85 @@
               nat_of_bitvector … program_counter' < total_program_size
       | _ ⇒ λother: False. ⊥
-      ] (subaddressing_modein … addr)
+      ] (subaddressing_modein … addr) *)
     | AJMP  addr         ⇒
       let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
@@ -98 +102 @@
           nat_of_bitvector … program_counter' < total_program_size
     ].
-  cases other
-qed.
-
-definition current_instruction_is_labelled ≝
+(*  cases other 
+qed. *)
+
+definition current_instruction_label ≝
   λcode_memory.
   λcost_labels: BitVectorTrie costlabel 16.
   λs: Status code_memory.
   let pc ≝ program_counter … code_memory s in
-    match lookup_opt … pc cost_labels with
-    [ None ⇒ False
-    | _    ⇒ True
-    ].
+    lookup_opt … pc cost_labels.
 
 definition next_instruction_properly_relates_program_counters ≝
@@ -159 +160 @@
       (program_counter …)
       (λs,class. ASM_classify … s = class)
-      (current_instruction_is_labelled … cost_labels)
+      (current_instruction_label code_memory cost_labels)
       (next_instruction_properly_relates_program_counters code_memory)
       ?.
@@ -373 +374 @@
     try (#assm1 #absurd destruct(absurd) @I)
     try (#absurd destruct(absurd) @I)
-    [1:
+    (* [1:
       #addr #_
       @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ]
@@ -385 +386 @@
     |3:
       #addr #_ *
-    ]
-    #relevant #pc_tps_assm'
+    ] *)
+    #_ #_ * #relevant #pc_tps_assm'
     whd cases reachable_program_counter_witness * #n
     #Some_assm #_ % try assumption
@@ -553 +554 @@
     #new_pc @ltn_to_ltO
   ]
+qed.
+
+lemma not_Some_neq_None_to_False:
+  ∀a: Type[0].
+  ∀e: a.
+    ¬ (Some a e ≠ None a) → False.
+  #a #e #absurd cases absurd -absurd
+  #absurd @absurd @nmk -absurd
+  #absurd destruct(absurd)
 qed.
 
@@ -612 +622 @@
       generalize in match costed_assm;
       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
+      whd in match (as_label ??);
       generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
-        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
+        in ⊢ (??%? → % → ?);
       #lookup_assm cases lookup_assm
       [1:
@@ -642 +653 @@
         ]
       |2:
-        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
-        #absurd cases absurd #absurd cases(absurd I)
+        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
+        #absurd
+        cases (not_Some_neq_None_to_False ?? absurd)
       ]
     |1:
@@ -654 +666 @@
       generalize in match costed_assm;
       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
+      whd in match (as_label ??);
       generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
-        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
+        in ⊢ (??%? → % → ?);
       #lookup_assm cases lookup_assm
       [1:
-        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
-        #absurd cases absurd
+        #None_lookup_opt_assm
+        #absurd @⊥ cases absurd -absurd #absurd @absurd %
       |2:
         #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
@@ -841 +854 @@
     generalize in match costed_assm;
     generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
+    whd in match (as_label ??);
     generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
-      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
+      in ⊢ (??%? → % → ?);
     #lookup_assm cases lookup_assm
     [1:
       #None_lookup_opt normalize nodelta #absurd cases absurd
+      -absurd #absurd @⊥ @absurd %
     |2:
       #costlabel #Some_lookup_opt normalize nodelta #ignore
@@ -876 +891 @@
     generalize in match costed_assm;
     generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
+    whd in match (as_label ??);
     generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
-      in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
+      in ⊢ (??%? → % → ?);
     #lookup_assm cases lookup_assm
     [1:
@@ -899 +915 @@
       ]
     |2:
-      #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
-      cases absurd #absurd cases (absurd I)
+      #cost_label #Some_lookup_opt_assm #absurd
+      cases (not_Some_neq_None_to_False ?? absurd)
     ]
   ]
@@ -1121 +1137 @@
   ]
   -block_cost'
-  [32:
-    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
-    lapply(good_program_witness program_counter' reachable_program_counter_witness)
-    <FETCH normalize nodelta <instr normalize nodelta
-    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
-    * * * * #n'
-    #_ #_ #program_counter_lt' #program_counter_lt_tps'
-    %
-    [1:
-      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
-      <FETCH normalize nodelta whd in match ltb; normalize nodelta
-      >(le_to_leb_true … program_counter_lt') %
-    |2:
-      assumption
-    ]
-  |33:
-    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
-    lapply(good_program_witness program_counter' reachable_program_counter_witness)
-    <FETCH normalize nodelta <instr normalize nodelta
-    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
-    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
-    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
-    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
-    #_ #_ #program_counter_lt' #program_counter_lt_tps'
-    %
-    [1:
-      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
-      <FETCH normalize nodelta whd in match ltb; normalize nodelta
-      >(le_to_leb_true … program_counter_lt') %
-    |2:
-      assumption
-    ]
-  |27,28:
-    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
-    lapply(good_program_witness program_counter' reachable_program_counter_witness)
-    <FETCH normalize nodelta <instr normalize nodelta *
-    #program_counter_lt' #program_counter_lt_tps' %
-    [1,3:
-      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
-      <FETCH normalize nodelta whd in match ltb; normalize nodelta
-      >(le_to_leb_true … program_counter_lt') %
-    |2,4:
-      assumption
-    ]
-  |1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26:
-    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
-    lapply(good_program_witness program_counter' reachable_program_counter_witness)
-    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
-    #program_counter_lt' #program_counter_lt_tps' %
-    try assumption
-    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
-    <FETCH normalize nodelta whd in match ltb; normalize nodelta
-    >(le_to_leb_true … program_counter_lt') %
-  |29,30,31: (* XXX: unconditional jumps *)
+  [29,30,31: (* XXX: unconditional jumps *)
     normalize nodelta
     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     lapply (good_program_witness program_counter' reachable_program_counter_witness)
     <FETCH normalize nodelta <instr normalize nodelta #assm assumption
+  |*:
+    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
+    lapply(good_program_witness program_counter' reachable_program_counter_witness)
+    <FETCH normalize nodelta destruct normalize nodelta
+    * #program_counter_lt' #program_counter_lt_tps'
+    % try assumption
+    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
+    <FETCH normalize nodelta whd in match ltb; normalize nodelta
+    >(le_to_leb_true … program_counter_lt') %
   ]
 qed.