Changeset 1711 for src/ASM/ASMCosts.ma

Timestamp:

Feb 20, 2012, 11:15:52 AM (8 years ago)

Author:

mulligan

Message:

finished block_cost' proof: 1.5 minutes to typecheck qed.

File:

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

src/ASM/ASMCosts.ma

@@ -1114 +1114 @@
     @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
     destruct %
-  |62,63,64,65,66,67,68,69,99,101,102:
+  |60,61,62,63,64,65,66,67,68,69,99,101,100,102:
     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl 
     @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
@@ -1211 +1211 @@
     >(le_to_leb_true … program_counter_lt') %
     (* XXX: got to here *)
-  |6,9,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,73,76,79,82,85,88,91,
-   94:
+  |6,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
+   92:
     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     lapply(good_program_witness program_counter' reachable_program_counter_witness)
@@ -1229 +1229 @@
         nat_of_bitvector … program_counter'')
     assumption
-  |62,63,64,65,66,67,68,69,70,101,102,103:
-    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
-    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
-      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
-    try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl …) destruct %)
-    cases daemon (* XXX: ???, same as above case *)
-  |96,99:
-    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
-    ]
-  |98,104,107:
-    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
-    cases(block_cost' ?????????) -block_cost'
-    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness first_time_around … recursive_case … FETCH … the_trace program_counter_refl …)
-    destruct %
-  |105:
-    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
-    ]
-  |106:
-    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'
-    @(transitive_le
-      total_program_size
-      ((S program_size') + nat_of_bitvector … program_counter')
-      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
-    normalize in match (S program_size' + nat_of_bitvector … program_counter');
-    >plus_n_Sm
-    @monotonic_le_plus_r
-    change with (
-      nat_of_bitvector … program_counter' <
-        nat_of_bitvector … program_counter'')
-    assumption
-  |108:
-    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
-    ]
-  |109:
-    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'
-    @(transitive_le
-      total_program_size
-      ((S program_size') + nat_of_bitvector … program_counter')
-      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
-    normalize in match (S program_size' + nat_of_bitvector … program_counter');
-    >plus_n_Sm
-    @monotonic_le_plus_r
-    change with (
-      nat_of_bitvector … program_counter' <
-        nat_of_bitvector … program_counter'')
-    assumption
-  |97,100:
+  |95,98:
     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     lapply(good_program_witness program_counter' reachable_program_counter_witness)
@@ -1341 +1248 @@
   ]
 qed.
-
-(*
-  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
-    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
-      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
-        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
-          on program_size:
-          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
-          Σcost_of_block: nat.
-          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
-            ∀start_status: Status code_memory'.
-            ∀final_status: Status code_memory'.
-            ∀trace_ends_flag.
-            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
-              program_counter' = program_counter … start_status →
-                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
-                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
-          else
-            (cost_of_block = 0)
-*)
 
 definition block_cost: