Changeset 1900 for src/ASM/CostsProof.ma

Timestamp:

Apr 23, 2012, 6:22:28 PM (8 years ago)

Author:

mulligan

Message:

CostProof? complete, modulo some daemons and axioms in earlier files

File:

• src/ASM/CostsProof.ma (modified) (9 diffs)

src/ASM/CostsProof.ma

@@ -601 +601 @@
  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
  on trace:
- ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
+ ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
@@ -616 +616 @@
  (trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
- (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
+ (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
@@ -632 +632 @@
  (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
- (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
+ (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    ∃reachable_witness: reachable_program_counter cm total_program_size pc.
    pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
@@ -664 +664 @@
       <(tech_cost_of_label_shift ??? [?] ? i) //
     |2:
-      whd in ⊢ (???%); (* XXX: should be easy *)
-      cases daemon
+      change with (? = lookup_present ? ? ? ? ?)
+      generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
+      normalize in match (nth_safe ? ? ? ?);
+      whd in costed_assm; lapply costed_assm -costed_assm    
+      inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
+      [1:
+        #_ #absurd cases absurd
+      |2:
+        normalize nodelta #cost_label #Some_assm #_ #p
+        cases (dom_codom ? p ? Some_assm)
+        #reachable_witness #block_cost_assm <block_cost_assm
+        cases (block_cost ? ? ? ? ? ?)
+        #cost -block_cost_assm #block_cost_assm
+        cases (block_cost_assm ? ? ? trace_any_label (refl …))
+        #_ #assm >assm %
+      ]
     ]
   |3:
@@ -707 +721 @@
   ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
   ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
-  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
+  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
     ∃reachable_witness: reachable_program_counter code_memory total_program_size pc.
       pi1 … (block_cost code_memory pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
@@ -725 +739 @@
   ∀good_program_witness: good_program code_memory total_program_size.
   ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels_injective:
+   (∀pc,pc',l.
+     lookup_opt costlabel 16 pc cost_labels=Some costlabel l
+      →lookup_opt costlabel 16 pc' cost_labels=Some costlabel l→pc=pc').
   ∀reachable_program_counter_witness:
     ∀lbl: costlabel.
@@ -733 +751 @@
   ∀final: Status code_memory.
   ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
-    let cost_map ≝ traverse_code code_memory cost_labels total_program_size total_program_size_invariant
+    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective total_program_size total_program_size_invariant
       reachable_program_counter_witness good_program_witness in
     let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
@@ -739 +757 @@
   [1:
     #code_memory #total_program_size #total_program_size_invariant #good_program_witness
-    #cost_labels #reachable_program_counter_witness #initial #final #trace
+    #cost_labels #cost_labels_injective #reachable_program_counter_witness #initial #final #trace
     @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
   |2:
@@ -745 +763 @@
   ]
   normalize nodelta
-  cases (traverse_code ? ? ? ? ? ?)
+  cases (traverse_code ? ? ? ? ? ? ?)
   #cost_map * #dom_codom #codom_dom try assumption
   #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)