Changeset 1695


Ignore:
Timestamp:
Feb 15, 2012, 2:10:39 PM (6 years ago)
Author:
mulligan
Message:

Progress on CostsProof?.ma file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1693 r1695  
    265265qed.
    266266
    267 (*
    268 let rec compute_paid_trace_label_return
    269   (cost_labels: BitVectorTrie costlabel 16)
    270   (start_status: Status) (final_status: Status)
    271     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    272       on the_trace: nat ≝
    273  match the_trace with
    274   [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label … trace_to_lift
    275   | tlr_step initial labelled final labelled_trace ret_trace ⇒
    276       let labelled_cost ≝ compute_paid_trace_label_label … labelled_trace in
    277       let return_cost ≝ compute_paid_trace_label_return … ret_trace in
    278         labelled_cost + return_cost
    279   ].
    280 *)
    281 
    282267include alias "ASM/BitVectorTrie.ma".
    283268
     
    338323 | // ]
    339324qed.
    340 
    341 (* XXX: commented out in favour of above
    342 let rec trace_label_label_length
    343   (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
    344     (start_status: Status) (final_status: Status)
    345       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    346         on the_trace: nat ≝
    347   match the_trace with
    348   [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
    349   ]
    350 and trace_any_label_length
    351   (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
    352     (start_status: Status) (final_status: Status)
    353       (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    354         on the_trace: nat ≝
    355   match the_trace with
    356   [ tal_base_not_return the_status _ _ _ _ ⇒ ?
    357   | tal_base_return the_status _ _ _ ⇒ ?
    358   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒ ?
    359   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ ?
    360   ]
    361 and trace_label_return_length
    362   (cost_labels: BitVectorTrie costlabel 16) (start_status: Status) (final_status: Status)
    363     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    364       on the_trace: nat ≝
    365   match the_trace with
    366   [ tlr_base before after trace_to_lift ⇒ ?
    367   | tlr_step initial labelled final labelled_trace ret_trace ⇒ ?
    368   ].
    369   cases daemon
    370 qed.
    371 *)
    372 
    373 (* Experiments with block_cost first!
    374 lemma reachable_program_counter_to_compute_trace_any_label_length_le_program_size:
    375   ∀start_status, final_status: Status.
    376   ∀code_memory: BitVectorTrie Byte 16.
    377   ∀program_size: nat.
    378   ∀cost_labels: BitVectorTrie costlabel 16.
    379   ∀trace_ends_flag: trace_ends_with_ret.
    380   ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
    381   let start_program_counter ≝ program_counter … start_status in
    382   let final_program_counter ≝ program_counter … final_status in
    383     reachable_program_counter code_memory program_size start_program_counter →
    384       nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter).
    385   cases daemon
    386 qed.
    387 
    388 lemma reachable_program_counter_to_compute_trace_label_label_length_le_program_size:
    389   ∀start_status, final_status: Status.
    390   ∀code_memory: BitVectorTrie Byte 16.
    391   ∀program_size: nat.
    392   ∀cost_labels: BitVectorTrie costlabel 16.
    393   ∀trace_ends_flag: trace_ends_with_ret.
    394   ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
    395   let start_program_counter ≝ program_counter … start_status in
    396   let final_program_counter ≝ program_counter … final_status in
    397     reachable_program_counter code_memory program_size start_program_counter →
    398       nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter).
    399   #start_status #final_status #code_memory #program_size #cost_labels #trace_ends_flag #the_trace
    400   cases daemon
    401 qed.
    402 
    403 corollary reachable_program_counter_to_compute_trace_length_le_program_size:
    404   ∀start_status, final_status: Status.
    405   ∀code_memory: BitVectorTrie Byte 16.
    406   ∀program_size: nat.
    407   ∀cost_labels: BitVectorTrie costlabel 16.
    408   ∀trace_ends_flag: trace_ends_with_ret.
    409   ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
    410   let program_counter ≝ program_counter … start_status in
    411     reachable_program_counter code_memory program_size program_counter →
    412       trace_length start_status final_status ≤ program_size.
    413   cases daemon
    414 qed. *)
    415325
    416326include alias "arithmetics/nat.ma".
     
    478388  ]
    479389qed.
    480 
    481 (*
    482 (* To be moved elsewhere*)
    483 lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m.
    484  #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) //
    485 qed.
    486 *)
    487390
    488391include alias "arithmetics/bigops.ma".
     
    622525qed.
    623526
     527lemma shift_nth_prefix:
     528 ∀T,l1,i,l2,K1,K2.
     529  nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
     530  #T #l1 elim l1 normalize
     531  [
     532    #i #l1 #K1 cases(lt_to_not_zero … K1)
     533  |
     534    #hd #tl #IH #i #l2
     535    cases i
     536    [
     537      //
     538    |
     539      #i' #K1 #K2 whd in ⊢ (??%%);
     540      @IH
     541    ]
     542  ]
     543qed.
     544
    624545lemma tech_cost_of_label_shift:
    625546 ∀cost_labels,cost_map,codom_dom,l1,l2,i.
     
    643564qed.
    644565
    645 let rec compute_max_trace_label_return_cost_ok_with_trace
     566lemma tech_cost_of_label_prefix:
     567 ∀cost_labels,cost_map,codom_dom,l1,l2,i.
     568  i < |l1| →
     569   tech_cost_of_label cost_labels cost_map codom_dom l1 i =
     570   tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) i.
     571 #cost_labels #cost_map #codom_dom #l1 #l2 #i #H
     572 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
     573 [1:
     574   whd in match ltb; normalize nodelta
     575   >(le_to_leb_true … H) applyS le_to_leb_true
     576   >length_append whd in H; >commutative_plus @le_plus_a assumption
     577 |2:
     578   #K1 #K2
     579   generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
     580   <(shift_nth_prefix … l1 i l2 K1 K2) //
     581 |3:
     582   #_ #_ %
     583 ]
     584qed.
     585   
     586(* XXX: here *)
     587let rec compute_trace_label_return_using_paid_ok_with_trace
    646588 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
    647589 (cost_labels: BitVectorTrie costlabel 16)
     
    655597   pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
    656598  let ctrace ≝ compute_cost_trace_label_return cm … trace in
    657   compute_max_trace_label_return_cost cm … trace =
     599  compute_trace_label_return_cost_using_paid cm … trace =
    658600   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    659601    ≝ ?
    660 and compute_max_trace_label_label_cost_ok_with_trace
     602and compute_trace_any_label_using_paid_ok_with_trace
     603 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
     604 (cost_labels: BitVectorTrie costlabel 16)
     605 (trace_ends_flag: trace_ends_with_ret)
     606 (cost_map: identifier_map CostTag nat)
     607 (initial: Status cm) (final: Status cm)
     608 (trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
     609 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
     610 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
     611   ∃reachable_witness: reachable_program_counter cm total_program_size pc.
     612   pi1 … (block_cost cm pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres))
     613 on trace:
     614  let ctrace ≝ compute_cost_trace_any_label … trace in
     615  compute_trace_any_label_cost_using_paid … trace =
     616   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     617    ≝ ?
     618and compute_trace_label_label_using_paid_ok_with_trace
    661619 (cm: ?) (total_program_size: nat) (good_program_witness: good_program cm total_program_size)
    662620 (cost_labels: BitVectorTrie costlabel 16)
     
    671629 on trace:
    672630  let ctrace ≝ compute_cost_trace_label_label … trace in
    673   compute_max_trace_label_label_cost … trace =
     631  compute_trace_label_label_cost_using_paid … trace =
    674632   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    675633    ≝ ?.
    676 cases trace normalize nodelta
    677 [ #sb #sa #tr #dom_codom whd in ⊢ (??%?);
    678   whd in match (compute_cost_trace_label_return ?????);
    679   @(compute_max_trace_label_label_cost_ok_with_trace … good_program_witness) @dom_codom
    680 | #si #sl #sf #tr1 #tr2 #dom_codom
    681   whd in ⊢ (??%?);
    682   whd in match (compute_cost_trace_label_return ?????);
    683   >append_length >bigop_sum_rev >commutative_plus @eq_f2
    684   [ >(compute_max_trace_label_return_cost_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
    685     -compute_max_trace_label_return_cost_ok_with_trace
    686     @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
    687   | >(compute_max_trace_label_label_cost_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
    688     -compute_max_trace_label_return_cost_ok_with_trace
    689     @same_bigop [//] #i #H #_
    690 ]
    691 (*
    692 lemma
    693  compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
    694   final_status the_trace =
    695  
    696 
    697 let rec compute_paid_trace_label_label_cost
    698   (cost_labels: BitVectorTrie Byte 16)
    699    (trace_ends_flag: trace_ends_with_ret)
    700     (start_status: Status) (final_status: Status)
    701       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    702         start_status final_status) on the_trace: nat ≝
    703   match the_trace with
    704   [ tll_base _ _ _ given_trace _ ⇒
    705       compute_paid_trace_any_label_cost … given_trace
    706   ]
    707 and compute_paid_trace_any_label_cost
    708   (cost_labels: BitVectorTrie Byte 16)
    709   (trace_ends_flag: trace_ends_with_ret)
    710    (start_status: Status) (final_status: Status)
    711      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    712        on the_trace: nat ≝
    713   match the_trace with
    714   [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
    715   | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
    716   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    717      _ _ _ call_trace final_trace ⇒
    718       let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    719       let final_trace_cost ≝ compute_paid_trace_any_label_cost cost_labels end_flag … final_trace in
    720         current_instruction_cost + final_trace_cost
    721   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    722       let current_instruction_cost ≝ current_instruction_cost status_pre in
    723       let tail_trace_cost ≝
    724        compute_paid_trace_any_label_cost cost_labels end_flag
    725         status_init status_end tail_trace
    726       in
    727         current_instruction_cost + tail_trace_cost
    728   ]
    729 and compute_paid_trace_label_return_cost
    730   (cost_labels: BitVectorTrie Byte 16)
    731   (start_status: Status) (final_status: Status)
    732     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
    733       on the_trace: nat ≝
    734   match the_trace with
    735   [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label_cost … trace_to_lift
    736   | tlr_step initial labelled final labelled_trace ret_trace ⇒
    737       let labelled_cost ≝ compute_paid_trace_label_label_cost … labelled_trace in
    738       let return_cost ≝ compute_paid_trace_label_return_cost … ret_trace in
    739         labelled_cost + return_cost
    740   ].
    741 
    742 let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
    743  | (call b bf tr af tl) as self ⇒
    744     trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
    745     trace_lab_rec_cost' tl
    746 
    747 theorem main_lemma:
    748  ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
    749 
    750 axiom lemma1:
    751  ∀p: simple_path.
    752   traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
    753 
    754 axiom lemma2:
    755  ∀s,l,cost_map.
    756   is_labelled l s →
    757    traverse_cost_internal s = cost_map l.
    758 
    759 axiom main_statement:
    760  ∀s.
    761  ∀cost_map.
    762  let p ≝ compute_simple_path0 s in
    763  ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
    764 
    765 axiom main_statement:
    766  ∀s.
    767  ∀cost_map.
    768  let p ≝ compute_simple_path0 s in
    769   execute' (path_length p) s = 〈s',τ〉 →
    770    Timer s' - Timer s = ∑ τ cost_map. *)
     634  cases trace normalize nodelta
     635  [ #sb #sa #tr #dom_codom whd in ⊢ (??%?);
     636    whd in match (compute_cost_trace_label_return ?????);
     637    @(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness) @dom_codom
     638  | #si #sl #sf #tr1 #tr2 #dom_codom
     639    whd in ⊢ (??%?);
     640    whd in match (compute_cost_trace_label_return ?????);
     641    >append_length >bigop_sum_rev >commutative_plus @eq_f2
     642    [ >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     643      -compute_trace_label_return_using_paid_ok_with_trace
     644      @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
     645    | >(compute_trace_label_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     646      -compute_trace_label_label_using_paid_ok_with_trace
     647      @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H)
     648    ]
     649  |8:
     650    #end_flag #start_status #end_status #trace_any_label #costed_assm
     651    whd in ⊢ (??%?); whd in ⊢ (??(?%?)?);
     652    >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     653    >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
     654    [1:
     655      @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
     656      <(tech_cost_of_label_shift ??? [?] ? i) //
     657    |2:
     658      whd in ⊢ (???%); (* XXX: should be easy *)
     659      cases daemon
     660    ]
     661  |3:
     662    #start_status #final_status #execute_assm #classifier_assm #costed_assm
     663    %
     664  |4:
     665    #start_status #final_status #execute_assm #classifier_assm %
     666  |5:
     667    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     668    #classifier_assm #after_return_assm #trace_label_return #costed_assm
     669    whd in ⊢ (??%?);
     670    @(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     671  |6:
     672    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     673    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     674    #costed_assm #trace_any_label
     675    whd in ⊢ (??%?);
     676    >(compute_trace_label_return_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom dom_codom)
     677    >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     678    >length_append >bigop_sum_rev >commutative_plus @eq_f2
     679    [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
     680                  |1: #i #H % ]
     681    | @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H)
     682    ]
     683  |7:
     684    #end_flag #status_pre_fun_call #status_start_fun_call #status_final
     685    #execute_assm #trace_any_label #classifier_assm #costed_assm
     686    whd in ⊢ (??%?);
     687    @(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     688  ]
     689qed.
     690 
     691lemma compute_max_trace_label_return_cost_ok_with_trace:
     692  ∀code_memory: BitVectorTrie Byte 16.
     693  ∀total_program_size: nat.
     694  ∀good_program_witness: good_program code_memory total_program_size.
     695  ∀cost_labels: BitVectorTrie costlabel 16.
     696  ∀cost_map: identifier_map CostTag nat.
     697  ∀initial: Status code_memory.
     698  ∀final: Status code_memory.
     699  ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     700  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     701  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
     702    ∃reachable_witness: reachable_program_counter code_memory total_program_size pc.
     703      pi1 … (block_cost code_memory pc total_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres).
     704        let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
     705          clock … code_memory … final =
     706            clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
     707  #code_memory #total_program_size #good_program_witness #cost_labels #cost_map
     708  #initial #final #trace #codom_dom #dom_codom normalize nodelta
     709  <compute_trace_label_return_using_paid_ok_with_trace try assumption
     710  >commutative_plus >compute_trace_label_return_cost_using_paid_ok //
     711qed.
Note: See TracChangeset for help on using the changeset viewer.