Changeset 3145 for src/ASM


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
Location:
src/ASM
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r3112 r3145  
    2929
    3030 λprog,cm,s0.
     31 let dummy : ident ≝ an_identifier … one in
    3132  let pc ≝ program_counter ?? (execute_1' cm s0) in
    3233  match lookup_opt ?? pc (symboltable prog) with
    33   [ None ⇒ ⊥ | Some id ⇒ id ].
    34 cases daemon (*CSC: we need a specification of the symboltable for this *)
     34  [ None ⇒ dummy (* in order to avoid this case we need a specification of the symboltable for this *)
     35  | Some id ⇒ id ].
     36
     37definition OC_result : ∀loc.Status (cm loc) → option int ≝
     38λprog,st. as_result_of_finaladdr … st (final_pc prog).
     39
     40lemma OC_exclude_tailcall :
     41∀p : labelled_object_code.
     42∀st : Status (cm p).
     43OC_classify … st ≠ cl_tailcall.
     44#p #st whd in ⊢ (?(??%?));
     45cases current_instruction [7: * ] normalize
     46try #x try #y % #ABS destruct
    3547qed.
    3648
     
    3951    mk_abstract_status
    4052      (Status (cm prog))
    41       (λs1,s2. execute_1 … s1 = s2)
     53      (λs1,s2.OC_result … s1 = None ? ∧ execute_1 … s1 = s2)
    4254      word_deqset
    4355      (program_counter …)
     
    4557      (λpc.lookup_opt … pc (costlabels prog))
    4658      (next_instruction_properly_relates_program_counters …)
    47       (λst. as_result_of_finaladdr … st (final_pc prog))
     59      (OC_result ?)
    4860      (OC_as_call_ident prog …)
    49       ?.
    50  * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
    51  try (#x #y #abs) try (#x #abs) try #abs destruct
    52 qed.
     61      (λst.⊥).
     62@hide_prf cases st -st #st #ABS @(absurd … ABS) @OC_exclude_tailcall qed.
    5363
    5464lemma OC_costed_is_nop : ∀loc.
     
    312322  @(trace_any_label_inv_ind … the_trace)
    313323    [2:
    314       #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     324      #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    315325      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    316326    |3:
    317       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     327      #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    318328      #classifier_assm #after_return_assm #trace_label_return #costed_assm
    319329      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    320330      destruct @⊥
    321331    |4:
    322       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     332      #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    323333      #classifier_assm #trace_label_return
    324334      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    326336    |5:
    327337      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    328       #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     338      #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    329339      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    330340      #final_status_refl #the_trace_refl destruct @⊥
    331341    |6:
    332       #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     342      #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    333343      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    334344      #the_trace_refl
     
    371381      ]
    372382    |1:
    373       #status_start #status_final #execute_assm #classifier_assm #costed_assm
     383      #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    374384      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    375385      destruct
     
    450460  @(trace_any_label_inv_ind … the_trace)
    451461  [6:
    452     #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     462    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    453463    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    454464    #the_trace_refl destruct @⊥
    455465  |1:
    456     #status_start #status_final #execute_assm #classifier_assm #costed_assm
     466    #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    457467    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    458468    destruct
     
    461471    <FETCH %
    462472  |2:
    463     #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     473    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    464474    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    465475  |3:
    466     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     476    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    467477    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    468478    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    469479    destruct @⊥
    470480  |4:
    471     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     481    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    472482    #classifier_assm #trace_label_return
    473483    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    475485  |5:
    476486    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    477     #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     487    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    478488    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    479489    #final_status_refl #the_trace_refl destruct @⊥
     
    524534  @(trace_any_label_inv_ind … the_trace)
    525535  [6:
    526     #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     536    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    527537    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    528538    #the_trace_refl destruct @⊥
    529539  |1:
    530     #status_start #status_final #execute_assm #classifier_assm #costed_assm
     540    #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    531541    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    532542    destruct @⊥
    533543  |2:
    534     #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     544    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    535545    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    536546  |3:
    537     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     547    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    538548    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    539549    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    571581    ]
    572582  |4:
    573     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     583    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    574584    #classifier_assm #trace_label_return
    575585    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     
    577587  |5:
    578588    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    579     #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     589    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    580590    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    581591    #final_status_refl #the_trace_refl
     
    643653  @(trace_any_label_inv_ind … the_trace)
    644654  [1:
    645     #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     655    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #costed_assm
    646656    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    647657    destruct @⊥
    648658  |2:
    649     #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
     659    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_flag_refl
    650660    #start_status_refl #final_status_refl #the_trace_refl destruct
    651661    whd in match (trace_any_label_length … (tal_base_return …));
     
    653663    <FETCH %
    654664  |3:
    655     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     665    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    656666    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    657667    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    658668    destruct @⊥
    659669  |4:
    660     #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     670    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    661671    #classifier_assm
    662672    destruct @⊥
     
    669679  |5:
    670680    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    671     #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     681    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    672682    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    673683    #final_status_refl #the_trace_refl
    674684    destruct @⊥
    675685  |6:
    676     #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     686    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    677687    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    678688    #final_status_refl #the_trace_refl destruct @⊥
  • src/ASM/ASMCostsSplit.ma

    r2999 r3145  
    320320  λp.
    321321  let cost_map ≝ compute_costs p in
    322   λl_sig.
    323   lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
    324   cases cost_map #m * #prf #_ cases l_sig
    325   #l * #pc #Hl whd in Hl; whd whd in match (as_cost_get_label ??);
    326   whd in Hl:(??%?); lapply (prf … Hl) //
    327 qed.
     322  λl.
     323  lookup_def … cost_map l 0.
  • src/ASM/CostsProof.ma

    r2999 r3145  
    9999      #start_status #final_status #is_next #is_not_return try (#is_costed)
    100100      change with (current_instruction_cost … start_status) in ⊢ (???(?%?));
    101       cases(is_next) @execute_1_ok_clock
     101      cases(proj2 … is_next) @execute_1_ok_clock
    102102    |3:
    103103      #status_pre_fun_call #status_start_fun_call #status_final #is_next
     
    105105      whd in match (compute_max_trace_any_label_cost … (tal_base_call …));
    106106      >(compute_max_trace_label_return_cost_is_ok prog … call_trace)
    107       >associative_plus @eq_f cases(is_next)
     107      >associative_plus @eq_f cases(proj2 … is_next)
    108108      @execute_1_ok_clock
    109109    |4:
     
    112112      whd in match (compute_max_trace_any_label_cost … (tal_base_tailcall …));
    113113      >(compute_max_trace_label_return_cost_is_ok … call_trace)
    114       >associative_plus @eq_f cases(is_next)
     114      >associative_plus @eq_f cases(proj2 … is_next)
    115115      @execute_1_ok_clock
    116116    |5:
     
    127127      >(compute_max_trace_label_return_cost_is_ok prog status_start_fun_call
    128128        status_after_fun_call call_trace)
    129       cases(is_next) in match (clock … (cm prog) status_start_fun_call);
     129      cases(proj2 … is_next) in match (clock … (cm prog) status_start_fun_call);
    130130      >(execute_1_ok_clock … status_pre_fun_call)
    131131      <associative_plus in ⊢ (??%?);
     
    149149      >(compute_max_trace_any_label_cost_is_ok prog end_flag
    150150         status_init status_end trace_any_label)
    151       cases(is_next) in match (clock … (cm prog) status_init);
     151      cases(proj2 … is_next) in match (clock … (cm prog) status_init);
    152152      >(execute_1_ok_clock … status_pre)
    153153      >commutative_plus >associative_plus >associative_plus @eq_f
     
    286286include alias "arithmetics/bigops.ma".
    287287
     288(*
    288289(* This shoudl go in bigops! *)
    289290theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B.
     
    296297 | #H1 #H2 #H3 <plus_minus_m_m //]
    297298qed.
    298 
     299*)
    299300(* This is taken by sigma_pi.ma that does not compile now *)
    300301definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
     
    327328(* ---------------------------------------- *) ⊢
    328329   times ≡ prod ? ? S.
    329 
     330(*
    330331notation > "Σ_{ ident i < n } f"
    331332  with precedence 20
     
    347348 % #abs destruct (abs)
    348349qed.
    349 
     350*)
    350351include alias "arithmetics/nat.ma".
    351352include alias "basics/logic.ma".
    352 
     353(*
    353354lemma ltb_rect:
    354355 ∀P:Type[0].∀n,m. (n < m → P) → (¬ n < m → P) → P.
     
    450451 ]
    451452qed.
     453*)
     454
     455(* in the standard library there are two Aop's!!! *)
     456lemma fold_sum' : ∀A,B.∀nil : B.∀op : Aop B nil.∀I,J,p.∀f : A → B.
     457\fold[op, nil]_{i ∈ I@J | p i} (f i) =
     458op (\fold[op, nil]_{i ∈ I | p i} (f i))
     459 (\fold[op, nil]_{i ∈ J | p i} (f i)).
     460#A #B #nil #op #I elim I -I [ #J #p #g >nill % ]
     461#hd #tl #IH #J #p #f whd in ⊢ (??%(????%?)); cases p normalize nodelta
     462[ <assoc @eq_f ] @IH
     463qed.
     464
     465lemma lookup_present_to_lookup_def : ∀tag,A,m,x,x_prf,def.
     466lookup_def tag A m x def = lookup_present tag A m x x_prf.
     467#tag #A #m #x #x_prf #def
     468whd in ⊢ (??%%); whd in x_prf; cases (lookup … m x) in x_prf;
     469[ * #ABS cases (ABS ?) % ]
     470#y #prf % qed.
    452471
    453472let rec compute_trace_label_return_using_paid_ok_with_trace
    454473 (prog: labelled_object_code)
    455  (cost_map: identifier_map CostTag nat)
    456474 (initial: Status (cm prog))
    457475 (final: Status (cm prog))
    458476 (trace: trace_label_return (OC_abstract_status prog) initial final)
    459  (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
    460477 on trace:
    461478 ∀unrepeating_witness: tlr_unrepeating … trace.
    462  ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
    463    pi1 … (block_cost prog pc) = lookup_present … k_pres).
    464479  let ctrace ≝ flatten_trace_label_return (OC_abstract_status prog) … trace in
    465480  compute_trace_label_return_cost_using_paid prog … trace =
    466    (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
     481   (Σ_{i ∈ ctrace} (ASM_cost_map prog i))
    467482    ≝ ?
    468483and compute_trace_any_label_using_paid_ok_with_trace
    469484 (prog: labelled_object_code)
    470485 (trace_ends_flag: trace_ends_with_ret)
    471  (cost_map: identifier_map CostTag nat)
    472486 (initial: Status (cm prog))
    473487 (final: Status (cm prog))
    474488 (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final)
    475  (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
    476  (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
    477    pi1 … (block_cost prog pc) = lookup_present … k_pres))
    478489 on trace:
    479490  ∀unrepeating_witness: tal_unrepeating … trace.
    480491  let ctrace ≝ flatten_trace_any_label (OC_abstract_status prog) … trace_ends_flag … trace in
    481492  compute_trace_any_label_cost_using_paid … trace =
    482    (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
     493   (Σ_{i ∈ ctrace} (ASM_cost_map prog i))
    483494    ≝ ?
    484495and compute_trace_label_label_using_paid_ok_with_trace
    485496 (prog: labelled_object_code)
    486497 (trace_ends_flag: trace_ends_with_ret)
    487  (cost_map: identifier_map CostTag nat)
    488498 (initial: Status (cm prog))
    489499 (final: Status (cm prog))
    490500 (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final)
    491501 (unrepeating_witness: tll_unrepeating … trace)
    492  (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
    493  (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
    494    pi1 … (block_cost prog pc) = lookup_present … k_pres))
    495502 on trace:
    496503 ∀unrepeating_witness: tll_unrepeating … trace.
    497504  let ctrace ≝ flatten_trace_label_label (OC_abstract_status prog) … trace in
    498505  compute_trace_label_label_cost_using_paid … trace =
    499    (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
     506   (Σ_{i ∈ ctrace} (ASM_cost_map prog i))
    500507    ≝ ?.
    501508  cases trace normalize nodelta
    502   [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?);
     509  [ #sb #sa #tr #unrepeating_witness whd in ⊢ (??%?);
    503510    whd in match (flatten_trace_label_return ????);
    504511    @compute_trace_label_label_using_paid_ok_with_trace
    505512    assumption
    506   | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
     513  | #si #sl #sf #tr1 #tr2 #unrepeating_witness
    507514    whd in ⊢ (??%?);
    508515    whd in match flatten_trace_label_return; normalize nodelta
    509516    whd in match (observables_trace_label_return ?????);
    510517    >costlabels_of_observables_append
    511     >append_length >bigop_sum_rev >commutative_plus @eq_f2
    512     [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     518    change with (? = \fold[natAop,0]_{i ∈ ?}(?)) >fold_sum' @eq_f2
     519    [ @compute_trace_label_label_using_paid_ok_with_trace
     520      -compute_trace_label_label_using_paid_ok_with_trace
     521      inversion unrepeating_witness
     522      #tll_unrepeating #tlr_unrepeating #_ assumption
     523    | @(compute_trace_label_return_using_paid_ok_with_trace)
    513524      -compute_trace_label_return_using_paid_ok_with_trace
    514       [1:
    515         @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
    516       |2:
    517         inversion unrepeating_witness
    518         #tll_unrepeating #tlr_unrepeating #_ assumption
    519       ]
    520     | >(compute_trace_label_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    521       -compute_trace_label_label_using_paid_ok_with_trace
    522       [1:
    523         @same_bigop [//] #i #H #_ @(tech_cost_of_label_prefix … H)
    524       |2,3:
    525         inversion unrepeating_witness
    526         #tll_unrepeating #tlr_unrepeating #_ assumption
    527       ]
     525      inversion unrepeating_witness
     526      #tll_unrepeating #tlr_unrepeating #_ assumption
    528527    ]
    529528  |9:
     
    531530    #unrepeating_witness'
    532531    whd in ⊢ (??%?); whd in ⊢ (??(?%?)?);
    533     >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
     532    whd in match flatten_trace_label_label; normalize nodelta
     533    whd in match (observables_trace_label_label ??????);
     534    >compute_trace_any_label_using_paid_ok_with_trace
    534535    [1:
    535       whd in match (flatten_trace_label_label ?????);
    536       >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
    537       [1:
    538         @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
    539         <(tech_cost_of_label_shift ??? [?] ? i) try assumption <(plus_n_O i) %
    540       |2:
    541         change with (? = lookup_present ? ? ? ? ?)
    542         generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
    543         whd in ⊢ (∀p:????%.???(????%?));
    544         whd in costed_assm; lapply costed_assm whd in match (as_label ??);
    545         inversion (lookup_opt ? ? (program_counter … start_status) (costlabels prog))
    546         [1:
    547           #_ #absurd @⊥ cases absurd #absurd @absurd %
    548         |2:
    549           normalize nodelta #cost_label #Some_assm #_ #p
    550           cases (dom_codom ? p ? Some_assm)
    551           cases (block_cost ??)
    552           #cost #block_cost_assm
    553           cases (block_cost_assm ??? trace_any_label ??)
    554           try @refl assumption
    555         ]
    556       ]
     536      change with (? = ? + ?) @eq_f2 [2: %]
     537      change with (? = lookup_def ? ? ? ? ?)
     538      whd in match (as_label_safe); normalize nodelta
     539      @opt_safe_elim #cost_lbl whd in ⊢ (??%?→?); #Some_assm
     540      cases (compute_costs ?) #m * #A #B
     541      >(lookup_present_to_lookup_def … (A … Some_assm)) [2: //]
     542      <(B … (Some_assm))
     543      cases (pi2 ?? (block_cost ??)) try % assumption
    557544    |2:
    558545      assumption
     
    569556    #classifier_assm #after_return_assm #trace_label_return #costed_assm #unrepeating_witness
    570557    whd in ⊢ (??%?);
    571     >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    572     //
    573558    whd in match flatten_trace_any_label; normalize nodelta
    574559    whd in match (observables_trace_any_label ??????);
    575     >(costlabels_of_observables_append … [?]) [2: normalize /2/]
    576     >length_append whd in match (? + ?);
    577     whd in match flatten_trace_label_return; normalize nodelta
    578     >costlabels_of_observables_trace_label_return_id_irrelevant //
     560    >(costlabels_of_observables_append … [?])
     561    >costlabels_of_observables_trace_label_return_id_irrelevant [2: %{one} ]
     562    @compute_trace_label_return_using_paid_ok_with_trace
     563    //
    579564  |6:
    580565    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    581566    #classifier_assm #trace_label_return #unrepeating_witness
    582567    whd in ⊢ (??%?);
    583     >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    584     //
    585568    whd in match flatten_trace_any_label; normalize nodelta
    586569    whd in match (observables_trace_any_label ??????);
    587     >(costlabels_of_observables_append … [?]) [2: normalize /2/]
    588     >length_append whd in match (? + ?);
    589     whd in match flatten_trace_label_return; normalize nodelta
    590     >costlabels_of_observables_trace_label_return_id_irrelevant //
     570    >(costlabels_of_observables_append … [?])
     571    >costlabels_of_observables_trace_label_return_id_irrelevant [2: %{one} ]
     572    @compute_trace_label_return_using_paid_ok_with_trace
     573    //
    591574  |7:
    592575    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    594577    #costed_assm #trace_any_label #unrepeating_witness
    595578    whd in ⊢ (??%?);
    596     >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    597     [1:
    598       >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    599       [1:
    600         whd in match flatten_trace_any_label in ⊢ (???%); normalize nodelta
    601         whd in match (observables_trace_any_label ??????);
    602         >costlabels_of_observables_append
    603         >(costlabels_of_observables_append … [?]) [2: normalize /2/]
    604         >length_append >bigop_sum_rev >commutative_plus @eq_f2
    605         [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
    606                       |1: #i #H % ]
    607         | >length_append whd in match (|?|+?);
    608           >costlabels_of_observables_trace_label_return_id_irrelevant
    609           [@same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H) | skip]
    610         ]
    611       |2:
    612         inversion unrepeating_witness
    613         * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption
    614       ]
    615     |2:
    616       inversion unrepeating_witness
    617       * #memb_1 #tal_unrepeating #tlr_unrepeating #_ assumption
    618     ]
     579    whd in match flatten_trace_any_label in ⊢ (???%); normalize nodelta
     580    whd in match (observables_trace_any_label ??????);
     581    >(costlabels_of_observables_append … [?])
     582    >costlabels_of_observables_append
     583    >costlabels_of_observables_trace_label_return_id_irrelevant [2: %{one} ]
     584    >fold_sum' change with (? = \fold[plus,0]_{i∈?@?}?) >fold_sum'
     585    cases unrepeating_witness * #H1 #H2 #H3 @eq_f2
     586    [ @compute_trace_label_return_using_paid_ok_with_trace
     587    | @compute_trace_any_label_using_paid_ok_with_trace
     588    ] assumption
    619589  |8:
    620590    #end_flag #status_pre_fun_call #status_start_fun_call #status_final
    621591    #execute_assm #trace_any_label #classifier_assm #costed_assm #unrepeating_witness
    622592    whd in ⊢ (??%?);
    623     @(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    624     inversion unrepeating_witness
    625     #memb_1 #tal_unrepeating #_ assumption
     593    @compute_trace_any_label_using_paid_ok_with_trace
     594    cases unrepeating_witness
     595    #memb_1 #tal_unrepeating assumption
    626596  ]
    627597qed.
    628  
    629 lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
    630   ∀prog: labelled_object_code.
    631   ∀cost_map: identifier_map CostTag nat.
    632   ∀initial: Status (cm prog).
    633   ∀final: Status (cm prog).
    634   ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    635   ∀unrepeating_witness: tlr_unrepeating … trace.
    636   ∀codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k).
    637   ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
    638       pi1 … (block_cost prog pc) = lookup_present … k_pres).
    639         let ctrace ≝ flatten_trace_label_return … trace in
    640           clock … (cm prog) … final =
    641             clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
    642   #prog #cost_map
    643   #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
    644   <compute_trace_label_return_using_paid_ok_with_trace try assumption
    645   >commutative_plus >compute_trace_label_return_cost_using_paid_ok //
    646 qed.
    647 
    648 theorem compute_max_trace_label_return_cost_ok_with_trace:
     598
     599lemma compute_max_trace_label_return_cost_ok_with_trace :
    649600  ∀prog: labelled_object_code.
    650601  ∀initial: Status (cm prog).
     
    652603  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    653604  ∀unrepeating_witness: tlr_unrepeating … trace.
    654     let cost_map ≝ traverse_code prog in
     605    let cost_map ≝ ASM_cost_map … prog in
    655606    let ctrace ≝ flatten_trace_label_return … trace in
    656       clock … (cm prog) … final = clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
    657   [1:
    658     #prog #initial #final #trace #unrepeating_witness
    659     @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
    660   |2:
    661     skip
    662   ]
    663   normalize nodelta
    664   cases (traverse_code ?)
    665   #cost_map * #dom_codom #codom_dom try assumption
    666   #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)
    667   lapply (sym_eq ? ? ? lookup_opt_assm)
    668   -lookup_opt_assm #lookup_opt_assm
    669   @nat_of_bitvector_lt_bound
    670 qed.
    671  
    672 include "utilities/permutations.ma".
    673 
    674 definition map_of_sigma_map:
    675  ∀P.
    676   (Σmap:identifier_map CostTag ℕ.P map) → identifier_map CostTag ℕ
    677  ≝ λP,x.x.
    678 
    679 lemma costlabel_map_of_as_cost_labels_map_ok:
    680  ∀prog,tl,Htl,PRF,PRF2.
    681   lookup_present CostTag ℕ (compute_costs prog) tl
    682   PRF
    683   =
    684    lookup_present CostTag ℕ (compute_costs prog)
    685    (as_cost_get_label (OC_abstract_status prog)
    686     «tl,Htl») PRF2.
    687 //
    688 qed.
    689 
    690 lemma tech_cost_sum_eq_as_cost :
    691   ∀compiled_code: labelled_object_code.
    692   let cost_labels ≝ costlabels compiled_code in
    693   let cost_map ≝ compute_costs compiled_code in
    694   ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    695   ∀trace.
    696   (Σ_{i < |trace|}(tech_cost_of_label cost_labels (map_of_sigma_map … cost_map) codom_dom trace i)) =
    697   (Σ_{l ∈ trace}(ASM_cost_map compiled_code l)).
    698 #ccode #codom_dom #trace
    699 @(list_elim_left … trace)
    700 [ %
    701 | #tl #hd #IH >append_length >commutative_plus
    702   >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
    703   whd in ⊢ (??%%); <IH
    704   <tech_cost_of_label_shift [2: //]
    705   cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
    706   [ cases tl -tl #tl #Htl @costlabel_map_of_as_cost_labels_map_ok
    707   | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
    708   ]
    709 ]
    710 qed.
     607      clock … (cm prog) … final = clock … (cm prog) … initial +
     608        (Σ_{i ∈ ctrace} (cost_map i)).
     609  #prog #initial #final #trace #unrepeating_witness normalize nodelta
     610  <compute_trace_label_return_using_paid_ok_with_trace try assumption
     611  >compute_trace_label_return_cost_using_paid_ok >commutative_plus //
     612qed.
Note: See TracChangeset for help on using the changeset viewer.