Changeset 3145


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (4 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
Files:
3 added
17 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.
  • src/ERTL/ERTLToLTL.ma

    r3072 r3145  
    33include "ASM/Arithmetic.ma".
    44include "joint/TranslateUtils.ma".
     5include "joint/joint_stacksizes.ma".
    56
    67(* Note: translation is complicated by having to preserve the carry bit and
     
    441442%
    442443qed.
     444
     445lemma ERTLToLTL_monotone_stacksizes :
     446∀fix,col.
     447∀p_in.
     448let cost_m ≝ \snd (\fst (ertl_to_ltl fix col p_in)) in
     449stack_cost_model_le (stack_cost ? p_in) cost_m.
     450#fix #col #p_in whd
     451@list_map_opt_All2
     452[ @(λid_def1,id_def2.
     453   match \snd id_def1 with
     454   [ Internal f1 ⇒
     455     match \snd id_def2 with
     456     [ Internal f2 ⇒
     457       \fst id_def1 = \fst id_def2 ∧
     458       le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
     459     | _ ⇒ False
     460     ]
     461   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
     462   ])
     463| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
     464  ** #H %{H} % ]
     465@All2_of_map * #id * #f normalize nodelta [2: %]
     466% [%]
     467cases (b_graph_translate ?????) #f_out * #data **
     468[2: #hd #tl ] * #f_lbls * #f_regs * [*] whd in ⊢ (%→?); #EQ_data
     469#props >(ss_def_out_eq … props) >EQ_data
     470generalize in match (joint_if_stacksize ???); generalize in match (spilled_no ??);
     471-p_in //
     472qed.
     473
  • src/ERTL/ERTLToLTLAxiom.ma

    r3096 r3145  
    66include "common/AssocList.ma".
    77
    8 (* Inefficient, replace with Trie lookup *)
    9 definition lookup_stack_cost ≝
    10  λp.λid : ident.
    11   assoc_list_lookup ? ℕ id (eq_identifier …) p.
    12 
    138axiom ERTLToLTL_ok :
    149∀fix_comp : fixpoint_computer.
     
    1712let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
    1813(* what should we do with n? *)
    19 let stacksizes ≝ lookup_stack_cost m in
     14let stacksizes ≝ stack_sizes m in
    2015∀init_in.make_initial_state
    2116  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
  • src/RTL/RTLToERTL.ma

    r3037 r3145  
    44include "ERTL/ERTL.ma".
    55include "joint/TranslateUtils.ma".
     6include "joint/joint_stacksizes.ma".
    67
    78include alias "basics/lists/list.ma".
     
    384385definition rtl_to_ertl : rtl_program → ertl_program ≝
    385386  b_graph_transform_program … translate_data.
     387
     388lemma RTLToERTL_monotone_stacksizes :
     389∀p_in.let p_out ≝ rtl_to_ertl p_in in
     390stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out).
     391#p_in whd
     392@list_map_opt_All2
     393[ @(λid_def1,id_def2.
     394   match \snd id_def1 with
     395   [ Internal f1 ⇒
     396     match \snd id_def2 with
     397     [ Internal f2 ⇒
     398       \fst id_def1 = \fst id_def2 ∧
     399       le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
     400     | _ ⇒ False
     401     ]
     402   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
     403   ])
     404| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
     405  ** #H %{H} % ]
     406@All2_of_map * #id * #f normalize nodelta [2: %]
     407% [%]
     408cases (b_graph_translate ?????) #f_out * #data
     409* *[2:#r1*[2:#r2*[2:#r3*[2:#r4*[2:#r5*[2:#r6*[2:#r7*[2:#r8*
     410  [2:#r9*[2:#r10*[2:#r11*[2:#r12*[2:#r13*[2:#r14 #tl]]]]]]]]]]]]]]
     411* #f_lbls * #f_regs * try ( * @False) whd in ⊢ (%→?); #EQ_data
     412#props >(ss_def_out_eq … props) >EQ_data
     413generalize in match (joint_if_stacksize ???); generalize in match (length ??-length ??);
     414-p_in //
     415qed.
  • src/RTL/RTL_separate_to_overflow.ma

    r3096 r3145  
    88  extract_call_ud_from_observables … (ft_observables … ft).
    99
    10 definition good_stack_usage_ft :
    11   ∀p, stacksizes.
    12   ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
    13   flat_trace … st1 st2 → Prop ≝
    14   λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λft.
    15   ∀m : ℕ.m < 2^16
    16   let info ≝ mk_stacksize_info (stack_usage … st1) m in
    17   let info' ≝ update_stacksize_info stacksizes info
    18     (extract_call_ud_from_ft … ft) in
    19   maximum info' < 2^16.
     10definition good_stack_usage_ft_tlr :
     11  ∀pars, p, stacksizes.
     12  ∀st1,st2,st3 : joint_status pars p stacksizes.
     13  ∀f.
     14  ∀ft : flat_trace … st1 st2.trace_label_return … st2 st3 →
     15  make_initial_state … (mk_prog_params pars p stacksizes) = return st1
     16  ft_current_function … ft = Some ? f → Prop ≝
     17  λpars, p, stacksizes.λst1,st2,st3,f.λft,tlr,st1_prf,f_prf.
     18  le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0)
     19    (extract_call_ud_from_ft … ft @ extract_call_ud_from_tlr … tlr f ))) (2^16 - globals_stacksize … p).
    2020
    21 definition good_stack_usage_tlr :
    22   ∀p, stacksizes.
    23   ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
    24   ident → trace_label_return … st1 st2 → Prop ≝
    25   λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tlr.
    26   ∀m : ℕ.m < 2^16 →
    27   let info ≝ mk_stacksize_info (stack_usage … st1) m in
    28   let info' ≝ update_stacksize_info stacksizes info
    29     (extract_call_ud_from_tlr … tlr curr_id) in
    30   maximum info' < 2^16.
    31 
     21(*
    3222definition good_stack_usage_tll :
    3323  ∀p, stacksizes.∀fl.
     
    5646    (extract_call_ud_from_tal … tal curr_id) in
    5747  maximum info' < 2^16.
     48*)
    5849
    5950axiom RTL_separate_to_overflow_produce_ft_and_tlr :
     
    6556∀ft1 : flat_trace S1 st1 st1'.
    6657∀tlr1 : trace_label_return S1 st1' st1''.
    67 good_stack_usage_ft … ft1 →
    68 good_stack_usage_tlr … fn tlr1 →
    69 ∃ft2 : flat_trace S2 st1 st1'.
    70 ∃tlr2 : trace_label_return S2 st1' st1''.
    71 ft_observables … ft1 = ft_observables … ft2 ∧
    72 tlr_rel … tlr1 tlr2.
     58∀st1_prf,fn_prf.
     59good_stack_usage_ft_tlr … fn ft1 tlr1 st1_prf fn_prf →
     60tlr_unrepeating … tlr1 →
     61ft_and_tlr S2 (ft_observables … ft1) (observables_trace_label_return … tlr1 fn) fn st1.
    7362
    7463(*
  • src/RTLabs/MeasurableToStructured.ma

    r3031 r3145  
    514514  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 →
    515515  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace' = 〈cs',obs〉 →
    516   pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
     516  observables_trace_label_return (RTLabs_status ge) s s' tlr fn = obs ∧ cs = cs' ≝ ?
    517517and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
    518518  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
    519519  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 →
    520   pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
     520  observables_trace_label_label (RTLabs_status ge) ends s s' tll fn = obs ∧ cs_change ends fn cs cs' ≝ ?
    521521and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
    522522  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
    523523  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 →
    524   maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
     524  maybe_label ge s (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn) = obs ∧ cs_change ends fn cs cs' ≝ ?.
    525525[ cases tlr
    526526  [ #s1 #s2 #tll @eq_obs_tll
     
    648648  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    649649  le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧
    650   pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
     650  observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn = interesting.
    651651#p #m #n #stack_cost #max #prefix #interesting
    652652#WCLP cases (well_cost_labelled_make_global p WCLP)
  • src/RTLabs/RTLabsToRTL.ma

    r3037 r3145  
    44include "common/Graphs.ma".
    55include "joint/TranslateUtils.ma".
     6include "joint/joint_stacksizes.ma".
    67include alias "ASM/BitVector.ma".
    78include alias "arithmetics/nat.ma".
     
    10841085  let entry' ≝ pi1 … (f_entry def) in
    10851086  let init ≝ mk_joint_internal_function RTL globals
    1086     luniverse' runiverse' [ ] [ ] stack_size' stack_size'
     1087    luniverse' runiverse' [ ] [ ] 0 0
    10871088    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
    10881089  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
     
    10961097    | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def
    10971098    ] (dpi2 … pr) in
    1098   foldi … f_trans (f_graph def) init'.
     1099  let def ≝ foldi … f_trans (f_graph def) init' in
     1100  mk_joint_internal_function ??
     1101    (joint_if_luniverse … def)
     1102    (joint_if_runiverse … def)
     1103    (joint_if_result … def)
     1104    (joint_if_params … def)
     1105    stack_size' stack_size'
     1106    (joint_if_code … def)
     1107    (joint_if_entry … def).
    10991108(* TODO *) cases daemon
    11001109qed.
     
    11111120    ?.
    11121121@hide_prf @transform_prog_funct_names qed.
     1122
     1123definition rtlabs_stack_cost : RTLabs_program → stack_cost_model ≝
     1124λp.list_map_opt … (λi_f.
     1125  match \snd i_f with [ Internal def ⇒ Some ? 〈\fst i_f, f_stacksize def〉
     1126                      | External _ ⇒ None ?]) (prog_funct … p).
     1127
     1128lemma RTLabsToRTL_monotone_stacksizes :
     1129∀cost,p_in.let p_out ≝ rtlabs_to_rtl cost p_in in
     1130stack_cost_model_le (rtlabs_stack_cost p_in) (stack_cost ? p_out).
     1131#cost #p_in whd
     1132@list_map_opt_All2
     1133[ @(λid_def1,id_def2.
     1134   match \snd id_def1 with
     1135   [ Internal f1 ⇒
     1136     match \snd id_def2 with
     1137     [ Internal f2 ⇒
     1138       \fst id_def1 = \fst id_def2 ∧
     1139       le (f_stacksize … f1) (joint_if_stacksize … f2)
     1140     | _ ⇒ False
     1141     ]
     1142   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
     1143   ])
     1144| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
     1145  ** #H %{H} % ]
     1146@All2_of_map * #id * #f normalize nodelta [2: %]
     1147% [%] whd in match translate_internal; normalize nodelta
     1148cases (initialize_locals_params_ret ?????) normalize nodelta #a #b %1
     1149qed.
  • src/RTLabs/RTLabsToRTLAxiom.ma

    r3096 r3145  
    2020include "RTLabs/MeasurableToStructured.ma". (* for make_ext_initial_state *)
    2121
    22 definition RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop ≝
    23 λstack_sizes,p.
    24 All …
    25   (λi_f.let 〈i, f〉 ≝ i_f in
    26     match f with
    27     [ External _ ⇒ True
    28     | Internal def ⇒
    29       ∃sz.stack_sizes i = Some ? sz ∧ f_stacksize … def ≤ sz
    30     ]) (prog_funct … p).
     22definition RTLabsToRTLstacksizes_ok : RTLabs_program → stack_cost_model → Prop ≝
     23λp.stack_cost_model_le (rtlabs_stack_cost p).
    3124
    3225axiom RTLabsToRTL_ok :
    33 ∀stacksizes : ident → option ℕ.
     26∀stack_model : stack_cost_model.
    3427∀cost.
    3528∀p_in : RTLabs_program.
    36 RTLabsToRTLstacksizes_ok stacksizes p_in
     29RTLabsToRTLstacksizes_ok p_in stack_model
    3730let p_out ≝ rtlabs_to_rtl cost p_in in
     31let stacksizes ≝ stack_sizes stack_model in
    3832∀init_in.make_ext_initial_state p_in = OK … init_in →
    3933∃init_out : state_pc RTL_semantics_separate.
  • src/common/StatusSimulation.ma

    r3096 r3145  
    1414
    1515include "common/StructuredTraces.ma".
     16include "common/FlatTraces.ma".
    1617
    1718(* We work with two relations on states in parallel, as well as two derived ones.
     
    149150    ]
    150151; sim_final :
    151   ∀st1,st2,res.as_result S1 st1 = Some ? res → sim_status_rel st1 st2 →
    152   as_result S2 st2 = Some ? res
     152  ∀st1,st2.as_result S1 st1 = as_result S2 st2
    153153}.
    154154
     
    160160; sim_step_final :> status_simulation S1 S2 R
    161161}.
    162 
    163 (* some useful lemmas *)
    164 
    165 let rec taa_append_tal_rel S1 fl1 st1 st1'
    166   (tal1 : trace_any_label S1 fl1 st1 st1')
    167   S2 st2 st2mid fl2 st2'
    168   (taa2 : trace_any_any S2 st2 st2mid)
    169   (tal2 : trace_any_label S2 fl2 st2mid st2')
    170   on tal1 :
    171   tal_rel … tal1 tal2 →
    172   tal_rel … tal1 (taa2 @ tal2) ≝
    173 match tal1 return λfl1,st1,st1',tal1.? with
    174   [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
    175   | tal_base_return st1 st1' _ _ ⇒ ?
    176   | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
    177   | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
    178   | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
    179   | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
    180   ].
    181 [ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
    182 | * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
    183 | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
    184   [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
    185   | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
    186   ]
    187 | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
    188 | * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
    189   [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
    190   | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
    191   ]
    192 | whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
    193 ]
    194 destruct
    195 <associative_taa_append_tal
    196   [1,2,3,4,5:%{(refl …)}] %{st2mid}
    197   [1,2:|*: %{G2} %{EQcall} ]
    198   %{(taa_append_taa … taa2 taa2')}
    199   [1,2: %{H2} %{G2} [%{K2}] %
    200   |5: %{st2mid'} %{H2} %{tlr2} % //
    201   |*: %{st2mid'} %{H2}
    202     [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
    203     %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
    204   ]
    205 qed.
    206162
    207163(*
     
    222178*)
    223179
    224 lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
    225   if taa_non_empty … taa then ¬as_costed … s2 else True.
    226 #S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
    227 [ #s1 %
    228 | #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
    229   [ #s2 #H #K #_ assumption
    230   | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
    231   ]
    232 ]
    233 qed.
    234 
    235 let rec tal_collapsable_to_rel S fl st1 st2
    236   (tal : trace_any_label S fl st1 st2) on tal :
    237   tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
    238   tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
    239   match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
    240   tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
    241   with
    242   [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
    243   | tal_base_not_return _ st2' _ _ K ⇒ ?
    244   | _ ⇒ Ⓧ
    245   ].
    246 * #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
    247 qed.
    248 
    249 let rec tal_collapsable_eq_flag S fl st1 st2
    250   (tal : trace_any_label S fl st1 st2) on tal :
    251   tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
    252   match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
    253   with
    254   [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
    255   | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
    256   | _ ⇒ Ⓧ
    257   ].
    258 
    259 let rec tal_collapsable_split S fl st1 st2
    260   (tal : trace_any_label S fl st1 st2) on tal :
    261   tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
    262   tal ≃ taa @ tal_base_not_return … st2 H I J ≝
    263   match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
    264   tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
    265   with
    266   [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
    267   | tal_base_not_return st1' st2' H I J ⇒ ?
    268   | _ ⇒ Ⓧ
    269   ].
    270 [ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
    271 | #coll
    272   elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
    273   #EQ %{st2_mid} %{(taa_step … taa)} try assumption
    274   %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
    275   #EQ >EQ %
    276 ]
    277 qed.
    278 
    279 lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
    280 tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
    281   tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
    282 #S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
    283 elim (tal_collapsable_split … coll) lapply tal
    284  >(tal_collapsable_eq_flag … coll) -tal #tal
    285 #st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
    286 %[|%[|%[|%[|%[| % ]]]]]
    287 qed.
    288 
    289 lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
    290   tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
    291   tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
    292 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize
    293 [ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ]
    294 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
    295 change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
    296 /2 by taa_append_tal_rel/
    297 qed.
    298180
    299181(* little helpers *)
     
    306188
    307189let rec status_simulation_produce_tlr S1 S2 R
     190(* NB: the axiomatized part about unrepeatingness is imprecise, as further
     191  hypotheses are surely needed for the taa prefix. Left for when it is
     192  rendered more precise. *)
    308193(* we start from this situation
    309194     st1 →→→→tlr→→→→ st1'
     
    325210  (taa2_pre : trace_any_any S2 st2_lab st2)
    326211  (sim_execute : status_simulation S1 S2 R)
    327   on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
     212  on tlr1 : tlr_unrepeating … tlr1 → R st1 st2 → label_rel … st1 st2_lab →
    328213  ∃st2_mid.∃st2'.
    329214  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
     
    331216  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
    332217  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
    333   tlr_rel … tlr1 tlr2
     218  tlr_rel … tlr1 tlr2 ∧ tlr_unrepeating … tlr2
    334219 match tlr1 with
    335220 [ tlr_base st1 st1' tll1 ⇒ ?
     
    356241  (taa2_pre : trace_any_any S2 st2_lab st2)
    357242  (sim_execute : status_simulation S1 S2 R)
    358    on tll1 : R st1 st2 → label_rel … st1 st2_lab →
     243   on tll1 : tll_unrepeating … tll1 → R st1 st2 → label_rel … st1 st2_lab →
    359244    match fl with
    360245    [ ends_with_ret ⇒
     
    364249      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
    365250      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
    366       tll_rel … tll1 tll2
     251      tll_rel … tll1 tll2 ∧ tll_unrepeating … tll2
    367252    | doesnt_end_with_ret ⇒
    368253      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
    369       R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2
     254      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2 ∧
     255      tll_unrepeating … tll2
    370256    ] ≝
    371257  match tll1 with
     
    401287  (tal1 : trace_any_label S1 fl st1 st1')
    402288  (sim_execute : status_simulation S1 S2 R)
    403    on tal1 : R st1 st2 →
     289   on tal1 : tal_unrepeating … tal1 → R st1 st2 →
    404290    match fl with
    405291    [ ends_with_ret ⇒
     
    409295      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
    410296      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
    411       tal_rel … tal1 tal2
     297      tal_rel … tal1 tal2 ∧ tal_unrepeating … tal2
    412298    | doesnt_end_with_ret ⇒
    413299      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
    414        R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨
     300       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2 ∧
     301       tal_unrepeating … tal2) ∨
    415302      (* empty *)
    416303      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
     
    424311  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
    425312  ].
    426 #st1_R_st2
    427 [1,2,3: #st1_L_st2_lab ]
     313#unrpt #st1_R_st2
     314[1,2,3: #st1_L_st2_lab]
    428315[ (* tlr_base *)
    429   elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
     316  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute unrpt st1_R_st2 st1_L_st2_lab)
    430317  #st2_mid * #st2' * #tll2 #H
    431318  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
    432319| (* tlr_step *)
    433   elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
    434   #st2_mid * #tll2 ** #H1 #H2 #H3
    435   elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
    436   #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
     320  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute (proj1 … unrpt) st1_R_st2 st1_L_st2_lab)
     321  #st2_mid * #tll2 *** #H1 #H2 #H3 #H4
     322  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute (proj2 … unrpt) H1 H2)
     323  #st2_mid' * #st2' * #tl2 * #taa2 ** #H5 #H6 #H7
    437324  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
    438   %{H4} %{H3 H5}
     325  % [ %{H5} %{H3 H6} | %{H4 H7} ]
    439326| (* tll_base *)
    440   lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
     327  lapply (status_simulation_produce_tal … st2 tal1 sim_execute unrpt st1_R_st2)
    441328  cases fl1' in tal1; normalize nodelta #tal1 *
    442329  [3: * #_ #ABS elim (absurd … H ABS) ]
    443   [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2
     330  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] ** #H1 #H2 #unrpt'
    444331  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
    445332  [1,3: whd <st1_L_st2_lab assumption
    446   |*: [%{taa2} ] %{H1} %
    447     [1,3: change with (opt_safe ??? = opt_safe ???)
    448       @opt_safe_elim #a #EQ1
    449       @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
    450     |*: @taa_append_tal_rel assumption
    451     ]
     333  |*: [%{taa2} ] %
     334    [1,3: %{H1} %
     335      [1,3: change with (opt_safe ??? = opt_safe ???)
     336        @opt_safe_elim #a #EQ1
     337        @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
     338      |*: @taa_append_tal_rel assumption
     339      ]
     340    |*: whd (* unrepeatingness... *) cases daemon
     341    ]
    452342  ]
    453343| (* tal_base_non_return *) whd
     
    467357    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))}
    468358    [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd <st1_L_st2' assumption ]
    469     % /2 by conj/
    470     % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
     359    %
     360    [1,3,5,7:
     361      % /2 by conj/
     362      % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
     363    |*: (* unrepeatingness... *) cases daemon
     364    ]
    471365  ]
    472366| (* tal_base_return *) whd
     
    477371  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
    478372  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
    479   % [ /4 by conj/ ]
    480   %[ % | %[|%[|%[|%[| % ]]]]]]]
     373  %
     374  [ % [ /4 by conj/ ]
     375    %[ % | %[|%[|%[|%[| % ]]]]]
     376  |*: (* unrepeatingness... *) cases daemon
     377  ]]]
    481378| (* tal_base_call *) whd
    482379  lapply (sim_execute … H st1_R_st2)
     
    485382  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    486383  #st1_R_st2_mid #st1_L_st2_after_call
    487   elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     384  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute unrpt st1_R_st2_mid st1_L_st2_after_call)
    488385  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
    489   [ #st2' #tlr2 *****
     386  [ #st2' #tlr2 ******
    490387  |*: #st2_after_ret #st2_after_ret' #st2' #taa2''
    491     #I2 #J2 [2: #K2 ] #tlr2 **** #ncost
    492   ]
    493   #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
     388    #I2 #J2 [2: #K2 ] #tlr2 ***** #ncost
     389  ]
     390  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S #unrpt' %1
    494391  %{st2'}
    495392  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
    496     [3: % [ % assumption ]
    497       % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
     393    [3: %
     394      [ % [ % assumption ]
     395        % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
     396      |  (* unrepeatingness... *) cases daemon
     397      ]
    498398    ]
    499399  |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))}
    500400    [2: %1{J2} |6: %2{J2}
    501     |4,8: % try (% assumption)
    502       % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
    503         % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
    504       ]]]]]]]]]]
     401    |4,8: %
     402      [1,3: % try (% assumption)
     403        % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
     404          % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
     405        ]]]]]]]]]]
     406      |*: (* unrepeatingness... *) cases daemon
     407      ]
    505408    ]
    506409  ]
     
    514417  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    515418  #st1_R_st2_mid #st1_L_st2_after_call
    516   elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     419  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute unrpt st1_R_st2_mid st1_L_st2_after_call)
    517420  #st2_after_ret * #st2' * #tlr2 * #taa2''
    518   * #props #S
     421  ** #props #S #unrpt'
    519422  %{st2_after_ret} %{st2'}
    520423  %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)}
    521424  %{taa2''}
    522   %{props}
    523   % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
     425  %
     426  [ %{props}
     427    % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
     428  | (* unrepeatingness... *) cases daemon
     429  ]
    524430| (* tal_step_call *)
    525431  lapply (sim_execute … H st1_R_st2)
     
    528434  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    529435  #st1_R_st2_mid #st1_L_st2_after_call
    530   elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
     436  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute (proj2 … unrpt) st1_R_st2_mid st1_L_st2_after_call)
    531437  #st2_after_ret * #st2' * #tlr2 * #taa2''
    532   ****
    533   #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
    534   lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
     438  *****
     439  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S #unrpt'
     440  lapply (status_simulation_produce_tal … tl1 sim_execute (proj2 … (proj1 … unrpt)) st1_R_st2')
    535441  cases fl1' in tl1; #tl1 *
    536   [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
     442  [ #st2'' * #st2''' * #tl2 * #taa2''' ***** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S' #unrpt''
    537443    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    538     [4: %{taa2'''} % [ /4 by conj/ ]
    539       %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     444    [4: %{taa2'''} %
     445      [ % [ /4 by conj/ ]
     446        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     447      | (* unrepeatingness... *) cases daemon
     448      ]
    540449    ]]]
    541   | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
     450  | *#st2'' *#tl2 *** #st1_R_st2'' #st1_L_st2'' #S' #unrpt'' %1
    542451    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
    543     [4: % [ /2 by conj/ ]
    544       %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     452    [4: %
     453      [ % [ /2 by conj/ ]
     454        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
     455      | (* unrepeatingness... *) cases daemon
     456      ]
    545457    ]]
    546458  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
     
    549461      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
    550462      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
    551       [3: % [ /2 by conj/ ]
    552       %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
     463      [3: %
     464        [ % [ /2 by conj/ ]
     465          %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]
     466        | (* unrepeatingness... *) cases daemon
     467      ]]]
    553468    |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost
    554469      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
     
    556471      %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))}
    557472      [2: %1{J2'} |6: %2{J2'}
    558       |4,8: % [1,3: /2 by conj/]
    559         %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
    560           %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
    561         ]]]]]]]]]]
     473      |4,8: %
     474        [ % [1,3: /2 by conj/]
     475          %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
     476            %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
     477          ]]]]]]]]]]
     478        |*: (* unrepeatingness... *) cases daemon
     479        ]
    562480      ]]
    563481    ]
     
    575493  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    576494  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    577   lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
     495  lapply (status_simulation_produce_tal … tl1 sim_execute (proj2 … unrpt) st1_R_st2_mid)
    578496  cases fl1' in tl1; #tl1 *
    579   [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
     497  [ #st2_mid' *#st2' *#tal2 *#taa2' ** #H #G #unrpt'
    580498    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
    581       [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ]
     499      [2: %{taa2'} %
     500        [ % [/4 by conj/ ] @taaf_append_tal_rel @G
     501        |  (* unrepeatingness... *) cases daemon
     502        ]
     503      ]
    582504    ]]
    583   | *#st2' *#tal2 *#H #G %1
     505  | *#st2' *#tal2 ** #H #G #unrpt' %1
    584506    %[| %{(taaf_append_tal … taa2 ? tal2)}
    585       [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
     507      [2: %
     508        [ % [/2 by conj/] @taaf_append_tal_rel @G
     509        | (* unrepeatingness... *) cases daemon
     510        ]
     511      ]
    586512    ]
    587513  | (* can't happen *)
     
    592518]
    593519qed.
    594 
    595 definition is_cl_jump : ∀S : abstract_status.S → bool ≝
    596 λS,s.match as_classify … s with [ cl_jump ⇒ true | _ ⇒ false ].
    597 
    598 definition enforce_costedness : ∀S : abstract_status.S → S → Prop ≝
    599 λS,s1,s2.if is_cl_jump … s1 then as_costed … s2 else True.
    600 
    601 (* finite flat traces, with recursive structure right to left. The list of
    602    identifiers represents the call stack *)
    603 inductive flat_trace (S : abstract_status) (start : S) : S → Type[0] ≝
    604 | ft_start : flat_trace S start start
    605 | ft_advance :
    606   ∀st1,st2.flat_trace S start st1 → as_execute S st1 st2 →
    607   enforce_costedness … st1 st2 → flat_trace S start st2.
    608 
    609 (*
    610   ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
    611   flat_trace S start st2 stack
    612 | ft_advance_call :
    613   ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
    614   ∀prf : as_classifier ? st1 cl_call.
    615   flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
    616 | ft_advance_tailcall :
    617   ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
    618   ∀prf : as_classifier ? st1 cl_tailcall.
    619   flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack)
    620 | ft_advance_ret :
    621   ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
    622   as_classifier ? st1 cl_return →
    623   flat_trace S start st2 stack.
    624 *)
    625 
    626 let rec ft_extend_taa S st1 st2 st3 (ft : flat_trace S st1 st2)
    627   (taa : trace_any_any S st2 st3)
    628 on taa : flat_trace S st1 st3 ≝
    629 match taa return λst2,st3,taa.flat_trace ?? st2 → flat_trace ?? st3 with
    630 [ taa_base s ⇒ λacc.acc
    631 | taa_step st1 st2 st3 H G _ tl ⇒
    632   λacc.ft_extend_taa ???? (ft_advance ???? acc H ?) tl
    633 ] ft.
    634 @hide_prf whd whd in match is_cl_jump; normalize nodelta >G % qed.
    635 
    636 lemma ft_extend_extend_taa : ∀S,st1,st2,st3,st4,ft,taa1,taa2.
    637   ft_extend_taa S st1 st3 st4 (ft_extend_taa … st2 … ft taa1) taa2 =
    638   ft_extend_taa … ft (taa_append_taa … taa1 taa2).
    639 #S #st1 #st2 #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
    640 /2/
    641 qed.
    642 
    643 definition ft_extend_taaf ≝ λS,st1,st2,st3.λft : flat_trace S st1 st2.
    644   λtaaf : trace_any_any_free S st2 st3.
    645   match taaf return λst2,st3,taaf.flat_trace ?? st2 → flat_trace ?? st3 with
    646   [ taaf_base s ⇒ λft.ft
    647   | taaf_step s1 s2 s3 pre H G ⇒
    648     λft.ft_advance … (ft_extend_taa … ft pre) H ?
    649   | taaf_step_jump s1 s2 s3 pre H G K ⇒
    650     λft.ft_advance … (ft_extend_taa … ft pre) H ?
    651   ] ft.
    652 @hide_prf whd whd in match is_cl_jump; normalize nodelta >G // qed.
    653 
    654 definition option_to_list : ∀A.option A → list A ≝ λA,x.
    655   match x with
    656   [ Some x ⇒ [x]
    657   | None ⇒ [ ]
    658   ].
    659 
    660 (*
    661 let rec ft_stack S st st' (ft : flat_trace S st st') on ft : list ident ≝
    662 match ft with
    663 [ ft_start ⇒ [ ]
    664 | ft_advance st1_mid st1' pre1 _ _ ⇒
    665   match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
    666   [ cl_call ⇒ λprf.
    667     let id ≝ as_call_ident ? «st1_mid, prf» in
    668     id :: ft_stack … pre1
    669   | cl_tailcall ⇒ λprf.
    670     let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    671     match ft_stack … pre1 with
    672     [ nil ⇒ (* should never happen in correct programs *)
    673       [id]
    674     | cons _ stack' ⇒
    675       id :: stack'
    676     ]
    677   | cl_return ⇒ λ_.
    678     match ft_stack … pre1 with
    679     [ nil ⇒ (* should never happen in correct programs *)
    680       [ ]
    681     | cons _ stack' ⇒ stack'
    682     ]
    683   | _ ⇒ λ_.ft_stack … pre1
    684   ] (refl …)
    685 ].
    686 *)
    687 
    688 (* the observables of a flat trace (for the moment, only labels, calls and returns) *)
    689 (* inefficient, but used only in correctness proofs *)
    690 let rec ft_stack_observables S st st'
    691   (ft : flat_trace S st st') on ft : list ident × (list intensional_event) ≝
    692 match ft with
    693 [ ft_start ⇒ 〈[ ], [ ]〉
    694 | ft_advance st1_mid st1' pre1 _ _ ⇒
    695   let 〈stack, tr〉 ≝ ft_stack_observables … pre1 in
    696   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    697   match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
    698   [ cl_call ⇒ λprf.
    699     let id ≝ as_call_ident ? «st1_mid, prf» in
    700     let tr' ≝ tr @ add @ [IEVcall id] in
    701     〈id :: stack, tr'〉
    702   | cl_tailcall ⇒ λprf.
    703     let id ≝ as_tailcall_ident ? «st1_mid, prf» in
    704     match stack with
    705     [ nil ⇒ (* should never happen in correct programs *)
    706       〈[ ], tr @ add〉
    707     | cons f stack' ⇒
    708       let tr' ≝ tr @ add @ [IEVtailcall f id] in
    709       〈id :: stack', tr'〉
    710     ]
    711   | cl_return ⇒ λ_.
    712     match stack with
    713     [ nil ⇒ (* should never happen in correct programs *)
    714       〈[ ], tr @ add〉
    715     | cons f stack' ⇒
    716       let tr' ≝ tr @ add @ [IEVret f] in
    717       〈stack', tr'〉
    718     ]
    719   | _ ⇒ λ_.〈stack, tr @ add〉
    720   ] (refl …)
    721 ].
    722 
    723 definition ft_observables ≝ λS,st1,st2,ft.\snd (ft_stack_observables S st1 st2 ft).
    724 definition ft_stack ≝ λS,st1,st2,ft.\fst (ft_stack_observables S st1 st2 ft).
    725 
    726 definition ft_current_function : ∀S,st1,st2.flat_trace S st1 st2 → option ident ≝
    727 λS,st1,st2,ft.
    728 match ft_stack … ft with [ nil ⇒ None ? | cons hd _ ⇒ Some ? hd ].
    729 
    730 lemma status_class_dep_match_elim :
    731 ∀A : Type[0].∀P : A → Prop.
    732 ∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
    733 (∀prf : cl = cl_call.P (c_call prf)) →
    734 (∀prf : cl = cl_return.P (c_return prf)) →
    735 (∀prf : cl = cl_tailcall.P (c_tailcall prf)) →
    736 (∀prf : cl = cl_other.P (c_other prf)) →
    737 (∀prf : cl = cl_jump.P (c_jump prf)) →
    738 P (match cl return λx.cl = x → ? with
    739    [ cl_call ⇒ c_call
    740    | cl_return ⇒ c_return
    741    | cl_tailcall ⇒ c_tailcall
    742    | cl_other ⇒ c_other
    743    | cl_jump ⇒ c_jump
    744    ] (refl …)).
    745 #A #P * normalize // qed.
    746 
    747 lemma status_class_dep_match_rewrite :
    748 ∀A : Type[0].
    749 ∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
    750 ∀cl'.
    751 ∀prf : cl = cl'.
    752 match cl return λx.cl = x → A with
    753  [ cl_call ⇒ c_call
    754  | cl_return ⇒ c_return
    755  | cl_tailcall ⇒ c_tailcall
    756  | cl_other ⇒ c_other
    757  | cl_jump ⇒ c_jump
    758  ] (refl …) =
    759 match cl' return λx.cl = x → A with
    760  [ cl_call ⇒ c_call
    761  | cl_return ⇒ c_return
    762  | cl_tailcall ⇒ c_tailcall
    763  | cl_other ⇒ c_other
    764  | cl_jump ⇒ c_jump
    765  ] prf.
    766 #A * #c1 #c2 #c3 #c4 #c5 * #prf destruct % qed.
    767 
    768 lemma pair_elim' :
    769   ∀A,B,C : Type[0].∀T : A → B → C.∀t : A × B.
    770   ∀P : (A×B) → C → Prop.
    771   P 〈\fst t, \snd t〉 (T (\fst t) (\snd t)) →
    772   P t (let 〈a, b〉 ≝ t in T a b).
    773 #A #B #C #T * // qed.
    774 
    775 lemma ft_extend_taa_obs : ∀S,st1,st2,st3,ft,taa.
    776   ft_stack_observables … (ft_extend_taa S st1 st2 st3 ft taa) =
    777     〈ft_stack … ft, ft_observables … ft @
    778     if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
    779 #S #st1 #st2 #st3 #ft #taa lapply ft elim taa -st2 -st3
    780 [ #st2 #ft >append_nil @eq_pair_fst_snd ]
    781 #st2 #st3 #st4 #H #K #G #taa #IH #ft
    782 whd in ⊢ (??(????%)?); >IH normalize nodelta
    783 -IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
    784 [ #st3 #H #G
    785 | #st3 #st4 #st5 #ex #H' #G' #taa #H #G
    786   >(not_costed_no_label … G)
    787 ]
    788 >append_nil whd in ⊢ (??(???%%)(????(??%?)));
    789 whd in match (ft_stack_observables ????) ;
    790 @(pair_elim' … (ft_stack_observables … ft))
    791 >(status_class_dep_match_rewrite … K) %
    792 qed.
    793 
    794 lemma ft_extend_taa_advance_obs : ∀S,st1,st2,st3,st4.
    795   ∀ft : flat_trace S st1 st2.
    796   ∀taa : trace_any_any S st2 st3.
    797   ∀H : as_execute S st3 st4.∀G.
    798   ft_stack_observables … (ft_advance … (ft_extend_taa … ft taa) H G) =
    799   (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
    800    let 〈stack, tr〉 ≝ ft_stack_observables … ft in
    801    match as_classify … st3 return λx.as_classifier … st3 x → ? with
    802     [ cl_call ⇒ λprf.
    803       let id ≝ as_call_ident ? «st3, prf» in
    804       let tr' ≝ tr @ add @ [IEVcall id] in
    805       〈id :: ft_stack … ft, tr'〉
    806     | cl_tailcall ⇒ λprf.
    807       let id ≝ as_tailcall_ident ? «st3, prf» in
    808       match stack with
    809       [ nil ⇒ (* should never happen in correct programs *)
    810         〈[ ], tr @ add〉
    811       | cons f stack' ⇒
    812         let tr' ≝ tr @ add @ [IEVtailcall f id] in
    813         〈id :: stack', tr'〉
    814       ]
    815     | cl_return ⇒ λ_.
    816       match stack with
    817       [ nil ⇒ (* should never happen in correct programs *)
    818         〈[ ], tr @ add〉
    819       | cons f stack' ⇒
    820         let tr' ≝ tr @ add @ [IEVret f] in
    821         〈stack', tr'〉
    822       ]
    823     | _ ⇒ λ_.〈stack, tr @ add〉
    824     ] (refl …)).
    825 #S #st1 #st2 #st3 #st4 #ft #taa #H #G normalize nodelta
    826 whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
    827 @status_class_dep_match_elim #prf
    828 @status_class_dep_match_elim #prf'
    829 try(@⊥ >prf in prf'; #prf' -prf destruct @False)
    830 >ft_extend_taa_obs whd in match ft_stack; whd in match ft_observables; normalize nodelta
    831 [2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
    832 @eq_f >associative_append @eq_f
    833 lapply prf lapply prf' lapply (taa_end_not_costed … taa)
    834 cases taa -st3 -st2 normalize nodelta
    835 [1,3,5,7,9,11,13: #st2 * #prf #prf' % ]
    836 #st2 #st2' #st3 #H' #G' #K' #taa' #K #prf #prf'
    837 >(not_costed_no_label … K) try % >append_nil %
    838 qed.
    839 
    840 lemma ft_extend_taaf_obs : ∀S,st1,st2,st3,ft,taaf.
    841   ft_stack_observables … (ft_extend_taaf S st1 st2 st3 ft taaf) =
    842     〈ft_stack … ft,
    843      ft_observables … ft @
    844       if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
    845 #S #st1 #st2 #st3 #ft #taa lapply ft cases taa -st2 -st3
    846 [ #st2 #ft >append_nil @eq_pair_fst_snd ]
    847 #st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
    848 whd in match ft_extend_taaf; normalize nodelta
    849 >ft_extend_taa_advance_obs @pair_elim'
    850 >(status_class_dep_match_rewrite … G) %
    851 qed.
    852 
    853 (*
    854 lemma ft_extend_taaf_advance_obs : ∀S,st1,st2,st3,st4.
    855   ∀ft : flat_trace S st1 st2.
    856   ∀taaf : trace_any_any_free S st2 st3.
    857   ∀H : as_execute S st3 st4.∀G.
    858   ft_stack_observables … (ft_advance … (ft_extend_taaf … ft taaf) H G) =
    859   (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
    860    let 〈stack, tr〉 ≝ ft_stack_observables … ft in
    861    match as_classify … st3 return λx.as_classifier … st3 x → ? with
    862     [ cl_call ⇒ λprf.
    863       let id ≝ as_call_ident ? «st3, prf» in
    864       let tr' ≝ tr @ add @ [IEVcall id] in
    865       〈id :: ft_stack … ft, tr'〉
    866     | cl_tailcall ⇒ λprf.
    867       let id ≝ as_tailcall_ident ? «st3, prf» in
    868       match stack with
    869       [ nil ⇒ (* should never happen in correct programs *)
    870         〈[ ], tr @ add〉
    871       | cons f stack' ⇒
    872         let tr' ≝ tr @ add @ [IEVtailcall f id] in
    873         〈id :: stack', tr'〉
    874       ]
    875     | cl_return ⇒ λ_.
    876       match stack with
    877       [ nil ⇒ (* should never happen in correct programs *)
    878         〈[ ], tr @ add〉
    879       | cons f stack' ⇒
    880         let tr' ≝ tr @ add @ [IEVret f] in
    881         〈stack', tr'〉
    882       ]
    883     | _ ⇒ λ_.〈stack, tr @ add〉
    884     ] (refl …)).
    885 #S #st1 #st2 #st3 #st4 #ft #taaf lapply ft cases taaf
    886 whd in match ft_extend_taaf; normalize nodelta
    887 [ #st #ft #H #G whd in ⊢ (??%?); @pair_elim' normalize nodelta % ]
    888 #st2 #st2' #st3 #taa' #H' #G' [2: #K' ] #ft #H #G
    889 whd in ⊢ (??%?); >ft_extend_taa_advance_obs normalize nodelta
    890 @(pair_elim' … (ft_stack_observables … ft)) normalize nodelta
    891 >(status_class_dep_match_rewrite … G') normalize nodelta
    892 @status_class_dep_match_elim #prf
    893 @status_class_dep_match_elim #prf'
    894 try(@⊥ >prf in prf'; #prf' -prf destruct @False)
    895 [ >associative_append
    896 whd in match ft_stack; whd in match ft_observables; normalize nodelta
    897 [2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
    898 @eq_f >associative_append @eq_f
    899 lapply prf lapply prf' lapply G
    900 cases taaf -st3 -st2 normalize nodelta
    901 [1,4,7,10,13,16,19: #st2 #_ #prf #prf' % ]
    902 
    903 >(not_costed_no_label … K) try % >append_nil %
    904 qed.
    905 *)
    906520
    907521(* little helper to avoid splitting equal cases *)
     
    1068682qed.
    1069683
     684definition call_stack_from_obs : list intensional_event → list ident ≝
     685let f ≝ λacc,ev.match ev with
     686  [ IEVcall id ⇒ id :: acc
     687  | IEVret _ ⇒ match acc with [ nil ⇒ [ ] | cons _ tl ⇒ tl ]
     688  | IEVtailcall _ id ⇒ match acc with [ nil ⇒ [ ] | cons _ tl ⇒ id :: tl ]
     689  | _ ⇒ acc
     690  ] in
     691foldl ?? f [ ].
     692
     693lemma ft_stack_from_observables :
     694∀S1,st1,st1'.∀ft : flat_trace S1 st1 st1'.
     695  ft_stack … ft = call_stack_from_obs … (ft_observables … ft).
     696#S1 #st1 #st1' #ft elim ft -st1'
     697[ % ] #st1' #st1'' #pre #ex #ncost #IH whd in match ft_stack; whd in match ft_observables; normalize nodelta
     698whd in match (ft_stack_observables ????); @pair_elim' normalize nodelta
     699@status_class_dep_match_elim #cl [2,3: inversion (\fst (ft_stack_observables ????))
     700  [2,4: #f #stak' #_ ] #EQ_stack normalize nodelta ] whd in match call_stack_from_obs; normalize nodelta
     701[1,2,5: <associative_append >foldl_append whd in ⊢ (???%); ]
     702>foldl_append cases (as_label ??) [2,4,6,8,10,12,14: #lbl]
     703whd in match option_to_list; normalize nodelta
     704whd in match (foldl ?????);
     705change with (call_stack_from_obs ?) in match (foldl ?????);
     706whd in match ft_stack in IH; whd in match ft_observables; normalize nodelta in IH; <IH
     707try >EQ_stack %
     708qed.
     709 
     710lemma ft_stack_observables_eq : ∀S1,S2,st1,st1',st2,st2'.
     711∀ft1 : flat_trace S1 st1 st1'.∀ft2 : flat_trace S2 st2 st2'.
     712ft_observables … ft1 = ft_observables … ft2 →
     713ft_stack_observables … ft1 = ft_stack_observables … ft2.
     714#S1 #S2 #st1 #st1' #st2 #st2' #ft1 #ft2 #EQ
     715>(eq_pair_fst_snd … (ft_stack_observables … ft1))
     716>(eq_pair_fst_snd … (ft_stack_observables … ft2))
     717change with (〈ft_stack … ft1, ft_observables … ft1〉 = 〈ft_stack … ft2, ft_observables … ft2〉)
     718>ft_stack_from_observables >ft_stack_from_observables >EQ %
     719qed.
     720
     721record ft_and_tlr (S : abstract_status) (prefix, subtrace : list intensional_event)
     722(fn : ident) (st1 : S) : Prop ≝
     723{ st2 : S
     724; st3 : S
     725; ft : flat_trace S st1 st2
     726; tlr : trace_label_return S st2 st3
     727; tlr_unrpt : tlr_unrepeating … tlr
     728; ft_is_prefix : ft_observables … ft = prefix
     729; fn_is_current : ft_current_function … ft = Some ? fn
     730; tlr_is_subtrace : observables_trace_label_return … tlr fn = subtrace
     731}.
     732
    1070733theorem status_simulation_produce_ft_and_tlr :
    1071734∀S1,S2.
    1072735∀R.
    1073 ∀st1,st1',st1'',st2.
    1074 ∀ft1 : flat_trace S1 st1 st1'.
    1075 ∀tlr1 : trace_label_return S1 st1' st1''.
     736∀prefix,subtrace,fn.
     737∀st1,st2.
    1076738status_simulation_with_init S1 S2 R st1 st2 →
    1077 ∃st2',st2'',st2'''.
    1078 ∃ft2 : flat_trace S2 st2 st2'.
    1079 ∃tlr2 : trace_label_return S2 st2' st2''.
    1080 ∃taaf : trace_any_any_free S2 st2'' st2'''.
    1081 (∀x.as_result … st1'' = Some ? x → as_result … st2''' = Some ? x) ∧
    1082 ft_observables … ft1 = ft_observables … ft2 ∧
    1083 tlr_rel … tlr1 tlr2.
    1084 #S1 #S2 #R #st1 #st1' #st1'' #st2 #ft1 #tlr1 * #S #L #simul
     739ft_and_tlr S1 prefix subtrace fn st1 →
     740ft_and_tlr S2 prefix subtrace fn st2.
     741#S1 #S2 #R #pref #subtr #fn #st1 #st2
     742* #S #L #simul *
     743#st1' #st1'' #ft1 #tlr1 #unrpt #EQ1 #EQ2 #EQ3
    1085744cases (status_simulation_produce_ft … ft1 simul S L)
    1086 #st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ1
    1087 cases (status_simulation_produce_tlr … tlr1 taa2 simul S' L')
    1088 #st2'' * #st2''' * #tlr2 * #taa2' **** #_ #S'' #_ #_ #EQ2
    1089 %{st2'} %{st2''} %{st2'''} %{ft2} %{tlr2} %{taa2'} %{EQ2} %
    1090 [ #res #EQ @(sim_final … simul … EQ S'')
    1091 | whd in ⊢ (??%%); @eq_f assumption
     745#st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ4
     746cases (status_simulation_produce_tlr … tlr1 taa2 simul unrpt S' L')
     747#st2'' * #st2''' * #tlr2 * #taa2' ***** #_ #S'' #_ #_ #EQ5 #unrpt'
     748%{st2' st2'' ft2 tlr2 unrpt' ???}
     749[ whd in ⊢ (??%?); <EQ4 assumption
     750| whd in ⊢ (??%?); whd in match ft_stack; normalize nodelta <EQ4 assumption
     751| <(tlr_rel_to_traces_same_observables … EQ5) assumption
    1092752]
    1093753qed.
  • src/common/StructuredTraces.ma

    r2869 r3145  
    1414  | cl_tailcall: status_class
    1515  | cl_other: status_class.
     16
     17
     18(* helper lemmas in presence of matches on status_class with dependent types *)
     19lemma status_class_dep_match_elim :
     20∀A : Type[0].∀P : A → Prop.
     21∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
     22(∀prf : cl = cl_call.P (c_call prf)) →
     23(∀prf : cl = cl_return.P (c_return prf)) →
     24(∀prf : cl = cl_tailcall.P (c_tailcall prf)) →
     25(∀prf : cl = cl_other.P (c_other prf)) →
     26(∀prf : cl = cl_jump.P (c_jump prf)) →
     27P (match cl return λx.cl = x → ? with
     28   [ cl_call ⇒ c_call
     29   | cl_return ⇒ c_return
     30   | cl_tailcall ⇒ c_tailcall
     31   | cl_other ⇒ c_other
     32   | cl_jump ⇒ c_jump
     33   ] (refl …)).
     34#A #P * normalize // qed.
     35
     36lemma status_class_dep_match_rewrite :
     37∀A : Type[0].
     38∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
     39∀cl'.
     40∀prf : cl = cl'.
     41match cl return λx.cl = x → A with
     42 [ cl_call ⇒ c_call
     43 | cl_return ⇒ c_return
     44 | cl_tailcall ⇒ c_tailcall
     45 | cl_other ⇒ c_other
     46 | cl_jump ⇒ c_jump
     47 ] (refl …) =
     48match cl' return λx.cl = x → A with
     49 [ cl_call ⇒ c_call
     50 | cl_return ⇒ c_return
     51 | cl_tailcall ⇒ c_tailcall
     52 | cl_other ⇒ c_other
     53 | cl_jump ⇒ c_jump
     54 ] prf.
     55#A * #c1 #c2 #c3 #c4 #c5 * #prf destruct % qed.
     56
     57lemma status_class_dep_match_elim' :
     58∀A : Type[0].∀P : A → Prop.∀Q : status_class → Type[0].
     59∀c_return,c_jump,c_call,c_tailcall,c_other.
     60∀cl.∀d : Q cl.
     61(cl = cl_return → ∀d : Q cl_return. P (c_return d)) →
     62(cl = cl_jump → ∀d : Q cl_jump.P (c_jump d)) →
     63(cl = cl_call → ∀d : Q cl_call.P (c_call d)) →
     64(cl = cl_tailcall → ∀d : Q cl_tailcall.P (c_tailcall d)) →
     65(cl = cl_other → ∀d : Q cl_other.P (c_other d)) →
     66P (match cl return λcl.Q cl → A with
     67   [ cl_return ⇒ c_return
     68   | cl_jump ⇒ c_jump
     69   | cl_call ⇒ c_call
     70   | cl_tailcall ⇒ c_tailcall
     71   | cl_other ⇒ c_other
     72   ] d).
     73#A #P #Q #c1 #c2 #c3 #c4 #c5 * /2 by / qed.
    1674
    1775record abstract_status : Type[1] ≝
     
    60118  λS : abstract_status. λl.∃pc.as_cost_labelled_at S l pc.
    61119
     120(*
    62121definition as_cost_label ≝
    63122  λS : abstract_status. Σl.as_cost_labelled S l.
     
    76135  λS : abstract_status. map … (as_cost_get_label S).
    77136*)
    78 
     137*)
    79138definition as_cost_map ≝
    80   λS : abstract_status. (as_cost_label S) → ℕ.
     139  λS : abstract_status. costlabel → ℕ.
    81140 
    82141definition as_label_safe : ∀a_s : abstract_status.
    83   (Σs : a_s.as_costed ? s) → as_cost_label a_s ≝
    84   λa_s,st_sig.«opt_safe ?? (pi2 … st_sig), ?».
    85 @hide_prf
    86 @opt_safe_elim #c #EQ %{EQ} qed.
    87  
     142  (Σs : a_s.as_costed ? s) → costlabel ≝
     143  λa_s,st_sig.opt_safe ?? (pi2 … st_sig).
     144
     145(* 
    88146definition lift_sigma_map_id :
    89147  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
     
    134192]
    135193qed.
    136 
     194*)
    137195
    138196(* structured traces: down to business *)
     
    225283          trace_any_label S end_flag status_pre status_end.
    226284
     285let rec tlr_length St st1 st2 (tlr : trace_label_return St st1 st2) on tlr : ℕ ≝
     286  match tlr with
     287  [ tlr_base _ _ tll ⇒ tll_length … tll
     288  | tlr_step _ _ _ tll tl ⇒ tll_length … tll + tlr_length … tl
     289  ]
     290and tll_length St fl st1 st2 (tll : trace_label_label St fl st1 st2) on tll : ℕ ≝
     291  match tll with
     292  [ tll_base _ _ _ tal _ ⇒ tal_length … tal
     293  ]
     294and tal_length St fl st1 st2 (tal : trace_any_label St fl st1 st2) on tal : ℕ ≝
     295  match tal with
     296  [ tal_step_call _ _ _ _ _ _ _ _ tlr _ tl ⇒ S (tlr_length … tlr + tal_length … tl)
     297  | tal_step_default _ _ _ _ _ tl _ _ ⇒ S (tal_length … tl)
     298  | tal_base_call _ _ _ _ _ _ trace _ ⇒ S (tlr_length … trace)
     299  | tal_base_tailcall _ _ _ _ _ trace ⇒ S (tlr_length … trace)
     300  | tal_base_return _ _ _ _ ⇒ 1
     301  | tal_base_not_return _ _ _ _ _ ⇒ 1
     302  ].
     303
     304
    227305let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
    228306  on tal : list (as_pc S) ≝
     
    236314 ].
    237315
     316(* watch out, this length does not count all states but only same-level ones *)
    238317definition as_trace_any_label_length':
    239318    ∀S: abstract_status.
     
    601680    match tll2 with
    602681    [ tll_base fl2 st2 st2 tal2 G ⇒
    603       pi1 … (as_label_safe … («?, H»)) = pi1 … (as_label_safe … («?, G»)) ∧
     682      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
    604683      tal_rel … tal1 tal2
    605684    ]
     
    734813| IEVret : ident → intensional_event.
    735814
    736 (* NB: we don't restrict call idents, because it would need some more tinkering
    737    with abstract_status *)
    738 definition as_emittable : abstract_status → intensional_event → Prop ≝
    739 λS,ev.
    740 match ev with
    741 [ IEVcost c ⇒ as_cost_labelled S c
    742 | _ ⇒ True
    743 ].
    744  
    745 definition as_trace ≝
    746 λS : abstract_status.
    747 Σl : list intensional_event.All … (as_emittable S) l.
    748 
    749 unification hint 0 ≔ S ⊢ as_trace S ≡ Sig (list intensional_event) (λl.All … (as_emittable S) l).
    750 
    751 definition cons_safe : ∀A,P.(Σx.P x) → (Σl.All A P l) → Σl.All A P l ≝
    752 λA,P,x,l.«x::l, conj … (pi2 … x) (pi2 … l)».
    753 
    754 definition append_safe : ∀A,P.(Σl.All A P l) → (Σl.All A P l) → Σl.All A P l ≝
    755 λA,P,l1,l2.«l1@l2,
    756   cic:/matita/cerco/utilities/lists/All_append.def(2) … (pi2 … l1) (pi2 … l2)».
    757 
    758 definition nil_safe : ∀A,P.(Σl.All A P l) ≝ λA,P.«[ ], I».
    759 
    760 interpretation "safe consing" 'vcons hd tl = (cons_safe ?? hd tl).
    761 interpretation "safe appending" 'vappend l1 l2 = (append_safe ?? l1 l2).
    762 interpretation "safe nil" 'vnil = (nil_safe ??).
    763 
    764 definition emittable_cost : ∀S.as_cost_label S → Σev.as_emittable S ev ≝
    765 λS,l.«IEVcost l, pi2 … l».
    766 
    767815let rec observables_trace_label_label
    768816  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     
    770818      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    771819      (curr : ident)
    772         on the_trace: as_trace S
     820        on the_trace: list intensional_event
    773821  match the_trace with
    774822  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    775823      let label ≝ as_label_safe … «?, labelled_proof» in
    776       emittable_cost … label ::: observables_trace_any_label S ends_flag initial final given_trace curr
     824      IEVcost label :: observables_trace_any_label S ends_flag initial final given_trace curr
    777825  ]
    778826and observables_trace_any_label
     
    781829      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
    782830      (curr : ident)
    783         on the_trace: as_trace S
     831        on the_trace: list intensional_event
    784832  match the_trace with
    785   [ tal_base_not_return the_status _ _ _ _ ⇒ [[ ]]
     833  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    786834  | tal_base_call pre_fun_call start_fun_call final _ cl _ call_trace _ ⇒
    787835      let id ≝ as_call_ident ? «?, cl» in
    788       IEVcall id ::: observables_trace_label_return ??? call_trace id
     836      IEVcall id :: observables_trace_label_return ??? call_trace id
    789837  | tal_base_tailcall pre_fun_call start_fun_call final _ cl call_trace ⇒
    790838      let id ≝ as_tailcall_ident ? «?, cl» in
    791       IEVtailcall curr id ::: observables_trace_label_return … call_trace id
    792   | tal_base_return the_status _ _ _ ⇒ [[ IEVret curr]]
     839      IEVtailcall curr id :: observables_trace_label_return … call_trace id
     840  | tal_base_return the_status _ _ _ ⇒ [ IEVret curr]
    793841  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    794842    _ cl _ call_trace _ final_trace ⇒
     
    796844    let call_cost_trace ≝ observables_trace_label_return … call_trace id in
    797845    let final_cost_trace ≝ observables_trace_any_label … end_flag … final_trace curr in
    798     IEVcall id ::: call_cost_trace @@ final_cost_trace
     846    IEVcall id :: call_cost_trace @ final_cost_trace
    799847  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    800848    observables_trace_any_label … tail_trace curr
     
    805853      (the_trace: trace_label_return S start_status final_status)
    806854      (curr : ident)
    807         on the_trace: as_trace S
     855        on the_trace: list intensional_event
    808856  match the_trace with
    809857  [ tlr_base before after trace_to_lift ⇒
     
    812860    let labelled_cost ≝ observables_trace_label_label … doesnt_end_with_ret … labelled_trace curr in
    813861    let return_cost ≝ observables_trace_label_return … ret_trace curr in
    814         labelled_cost @@ return_cost
    815   ]. % qed.
     862        labelled_cost @ return_cost
     863  ].
    816864 
    817865let rec filter_map X Y (f : X → option Y) (l : list X) on l : list Y ≝
     
    848896#X #Y #f #g #l #H elim l normalize [%] #hd #tl #IH >H @eq_f @IH qed.
    849897
    850 let rec list_distribute_sig_aux X P (l : list X) on l : All X P l → list (Σx.P x) ≝
    851 match l return λl.All X P l → list (Σx.P x) with
    852 [ nil ⇒ λ_.[ ]
    853 | cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_distribute_sig_aux X P tl (proj2 … prf)
    854 ].
    855 
    856 definition list_distribute_sig : ∀A,P.(Σl.All A P l) → list (Σx.P x) ≝
    857 λA,P,l.list_distribute_sig_aux … l (pi2 … l).
    858 
    859 lemma list_distribute_sig_append:
    860  ∀A,P,l1,l2,prf1,prf2,prf3.
    861   list_distribute_sig A P «l1@l2,prf3» =
    862    list_distribute_sig … «l1,prf1» @ list_distribute_sig … «l2,prf2».
    863  #A #P #l1 whd in match list_distribute_sig; normalize nodelta elim l1 //
    864  #hd #tl #IH normalize #l2 #prf1 #prf2 #prf3 <IH //
    865 qed.
    866 
    867 let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
    868 match l with
    869 [ nil ⇒ [[ ]]
    870 | cons hd tl ⇒ hd ::: list_factor_sig … tl
    871 ].
    872 
    873 definition costlabels_of_observables : ∀S.as_trace S → list (as_cost_label S) ≝
    874 λS,l.filter_map (Σev.as_emittable S ev) ?
    875   (λev.match ev return λev.as_emittable S ev → option ? with
    876     [ IEVcost c ⇒ λprf.Some ? «c, prf»
    877     | _ ⇒ λ_.None ?
    878     ] (pi2 … ev)) (list_distribute_sig … l).
     898definition costlabels_of_observables : list intensional_event →
     899   list costlabel ≝
     900filter_map ??
     901  (λev.match ev with
     902    [ IEVcost c ⇒ Some ? c
     903    | _ ⇒ None ?
     904    ]).
    879905
    880906axiom costlabels_of_observables_trace_label_return_id_irrelevant:
    881907 ∀S,s1,s2,tr,id1,id2.
    882   costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id1) =
    883   costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id2).
     908  costlabels_of_observables (observables_trace_label_return S s1 s2 tr id1) =
     909  costlabels_of_observables (observables_trace_label_return S s1 s2 tr id2).
    884910
    885911lemma costlabels_of_observables_append:
    886  ∀S:abstract_status. ∀tr1,tr2: as_trace S.
    887   costlabels_of_observables S (tr1 @ tr2) =
    888    costlabels_of_observables … tr1 @ costlabels_of_observables … tr2.
    889 [ #S #tr1 #tr2 whd in match costlabels_of_observables; normalize nodelta
    890   <filter_map_append <list_distribute_sig_append //
    891 | @All_append [ @(pi2 … tr1) | @(pi2 … tr2) ]]
    892 qed.
     912 ∀tr1,tr2.
     913  costlabels_of_observables (tr1 @ tr2) =
     914   costlabels_of_observables … tr1 @ costlabels_of_observables … tr2 ≝
     915filter_map_append ….
    893916
    894917(* JHM: base case now passes the termination checker *)
     
    929952          on the_trace_l:
    930953            tll_rel … the_trace_l the_trace_r →
    931               pi1 … (observables_trace_label_label … the_trace_l curr) =
    932                 pi1 … (observables_trace_label_label … the_trace_r curr)
     954               observables_trace_label_label … the_trace_l curr =
     955                 observables_trace_label_label … the_trace_r curr
    933956  match the_trace_l with
    934957  [ tll_base fl1 st1 st1' tal1 H ⇒
     
    946969          on the_trace_l:
    947970            tal_rel … the_trace_l the_trace_r →
    948               pi1 … (observables_trace_any_label … the_trace_l curr) =
    949                 pi1 … (observables_trace_any_label … the_trace_r curr)
     971              observables_trace_any_label … the_trace_l curr =
     972                observables_trace_any_label … the_trace_r curr
    950973  match the_trace_l with
    951974  [ tal_base_not_return st1 st1' H G K ⇒ ?
     
    964987        on the_trace_l:
    965988          tlr_rel … the_trace_l the_trace_r →
    966             pi1 … (observables_trace_label_return … the_trace_l curr) =
    967               pi1 … (observables_trace_label_return … the_trace_r curr)
     989            observables_trace_label_return … the_trace_l curr =
     990              observables_trace_label_return … the_trace_r curr
    968991  match the_trace_l with
    969992  [ tlr_base before after tll_l ⇒ ?
     
    971994  ]. 
    972995[ * #EQ #H_tal
    973   whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)]
    974   cases (as_label_safe ??) in EQ; #c1 #H1
    975   cases (as_label_safe ??) #c2 #H2 #EQ destruct %
     996  whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)] cases EQ %
    976997|2,3,4,5,6,7:
    977998  [1,2,3,4: * #EQ destruct(EQ)]
     
    9861007      [| *#tl2] ** #EQ #H_tl #H_tlr
    9871008    ] >EQ >taa_append_tal_same_observables
    988   | whd in ⊢ (%→??(???%)?); @tal_rel_to_traces_same_observables
     1009  | whd in ⊢ (%→??%?); @tal_rel_to_traces_same_observables
    9891010  ]
    9901011  whd in ⊢ (??%%);
     
    10401061*)
    10411062
    1042 lemma map_pi1_distribute_sig : ∀A,P,l.
    1043   map ?? (pi1 ??) (list_distribute_sig A P l) = pi1 ?? l.
    1044 #A #P * #l elim l -l normalize // qed.
    1045 
    10461063definition flatten_trace_label_return ≝
    10471064  λS,st1,st2.λtlr : trace_label_return S st1 st2.
     
    10641081  let dummy ≝ an_identifier ? one in
    10651082  costlabels_of_observables … (observables_trace_any_label … tll dummy).
    1066 
    1067 lemma lift_cost_map_same_cost_tlr :
    1068   ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
    1069   ∀the_trace_in : trace_label_return S_in start_in end_in.
    1070   ∀the_trace_out : trace_label_return S_out start_out end_out.
    1071   tlr_rel … the_trace_in the_trace_out →
    1072   (Σ_{l ∈ flatten_trace_label_return … the_trace_in}
    1073     (lift_cost_map_id … dec m_out l)) =
    1074   (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)).
    1075 #S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
    1076 #tlr_in #tlr_out #H_tlr
    1077 @lift_cost_map_same_cost
    1078 whd in match flatten_trace_label_return; normalize nodelta
    1079 >map_to_filter_map >map_to_filter_map >filter_map_compose
    1080 >filter_map_compose
    1081 cut (∀S.∀x: (Σev.as_emittable S ev).
    1082   ! y ←
    1083     match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
    1084     [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
    1085   Some ? (pi1 ?? y) =
    1086   ! ev ← Some ? (pi1 ?? x) ;
    1087   match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
    1088 [ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
    1089 #EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
    1090 <filter_map_compose <filter_map_compose @eq_f
    1091 <map_to_filter_map <map_to_filter_map
    1092 >map_pi1_distribute_sig >map_pi1_distribute_sig
    1093 @(tlr_rel_to_traces_same_observables … H_tlr) %
    1094 qed.
    1095 
    1096 lemma lift_cost_map_same_cost_tll :
    1097   ∀S_in, S_out, dec, m_out, fl_in, fl_out, start_in, start_out, end_in, end_out.
    1098   ∀the_trace_in : trace_label_label S_in fl_in start_in end_in.
    1099   ∀the_trace_out : trace_label_label S_out fl_out start_out end_out.
    1100   tll_rel … the_trace_in the_trace_out →
    1101   (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
    1102     (lift_cost_map_id … dec m_out l)) =
    1103   (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
    1104 #S_in #S_out #dec #m_out #fl_in #fl_out #start_in #start_out #end_in #end_out
    1105 #tlr_in #tlr_out #H_tlr
    1106 @lift_cost_map_same_cost
    1107 whd in match flatten_trace_label_label; normalize nodelta
    1108 >map_to_filter_map >map_to_filter_map >filter_map_compose
    1109 >filter_map_compose
    1110 cut (∀S.∀x: (Σev.as_emittable S ev).
    1111   ! y ←
    1112     match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
    1113     [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
    1114   Some ? (pi1 ?? y) =
    1115   ! ev ← Some ? (pi1 ?? x) ;
    1116   match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
    1117 [ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
    1118 #EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
    1119 <filter_map_compose <filter_map_compose @eq_f
    1120 <map_to_filter_map <map_to_filter_map
    1121 >map_pi1_distribute_sig >map_pi1_distribute_sig
    1122 @(tll_rel_to_traces_same_observables … H_tlr) %
    1123 qed.
    11241083
    11251084(* the equivalent of a collapsable trace_any_label where we do not force
     
    12431202  taaf_step_jump … (taaf_append_taa … taaf1 ? taa) H' I' K'
    12441203] taaf1. @prf qed.
     1204
     1205lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
     1206  if taa_non_empty … taa then ¬as_costed … s2 else True.
     1207#S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
     1208[ #s1 %
     1209| #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
     1210  [ #s2 #H #K #_ assumption
     1211  | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
     1212  ]
     1213]
     1214qed.
     1215
     1216let rec tal_collapsable_to_rel S fl st1 st2
     1217  (tal : trace_any_label S fl st1 st2) on tal :
     1218  tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
     1219  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
     1220  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
     1221  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
     1222  with
     1223  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
     1224  | tal_base_not_return _ st2' _ _ K ⇒ ?
     1225  | _ ⇒ Ⓧ
     1226  ].
     1227* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
     1228qed.
     1229
     1230let rec tal_collapsable_eq_flag S fl st1 st2
     1231  (tal : trace_any_label S fl st1 st2) on tal :
     1232  tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
     1233  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
     1234  with
     1235  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
     1236  | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
     1237  | _ ⇒ Ⓧ
     1238  ].
     1239
     1240let rec tal_collapsable_split S fl st1 st2
     1241  (tal : trace_any_label S fl st1 st2) on tal :
     1242  tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
     1243  tal ≃ taa @ tal_base_not_return … st2 H I J ≝
     1244  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
     1245  tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
     1246  with
     1247  [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
     1248  | tal_base_not_return st1' st2' H I J ⇒ ?
     1249  | _ ⇒ Ⓧ
     1250  ].
     1251[ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
     1252| #coll
     1253  elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
     1254  #EQ %{st2_mid} %{(taa_step … taa)} try assumption
     1255  %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
     1256  #EQ >EQ %
     1257]
     1258qed.
     1259
     1260lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
     1261tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
     1262  tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
     1263#S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
     1264elim (tal_collapsable_split … coll) lapply tal
     1265 >(tal_collapsable_eq_flag … coll) -tal #tal
     1266#st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
     1267%[|%[|%[|%[|%[| % ]]]]]
     1268qed.
     1269
     1270
     1271let rec taa_append_tal_rel S1 fl1 st1 st1'
     1272  (tal1 : trace_any_label S1 fl1 st1 st1')
     1273  S2 st2 st2mid fl2 st2'
     1274  (taa2 : trace_any_any S2 st2 st2mid)
     1275  (tal2 : trace_any_label S2 fl2 st2mid st2')
     1276  on tal1 :
     1277  tal_rel … tal1 tal2 →
     1278  tal_rel … tal1 (taa2 @ tal2) ≝
     1279match tal1 return λfl1,st1,st1',tal1.? with
     1280  [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
     1281  | tal_base_return st1 st1' _ _ ⇒ ?
     1282  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
     1283  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
     1284  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
     1285  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
     1286  ].
     1287[ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
     1288| * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
     1289| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
     1290  [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
     1291  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
     1292  ]
     1293| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
     1294| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
     1295  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
     1296  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
     1297  ]
     1298| whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
     1299]
     1300destruct
     1301<associative_taa_append_tal
     1302  [1,2,3,4,5:%{(refl …)}] %{st2mid}
     1303  [1,2:|*: %{G2} %{EQcall} ]
     1304  %{(taa_append_taa … taa2 taa2')}
     1305  [1,2: %{H2} %{G2} [%{K2}] %
     1306  |5: %{st2mid'} %{H2} %{tlr2} % //
     1307  |*: %{st2mid'} %{H2}
     1308    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
     1309    %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
     1310  ]
     1311qed.
     1312
     1313lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
     1314  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
     1315  tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
     1316#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize
     1317[ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ]
     1318#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
     1319change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
     1320/2 by taa_append_tal_rel/
     1321qed.
  • src/common/stacksize.ma

    r2755 r3145  
    1515    λf.match stacksizes f with
    1616      [ Some n ⇒ n | None ⇒ 0 (* should never happen *) ] in
    17   let f ≝ λud,acc.
     17  let f ≝ λacc,ud.
    1818    match ud with
    1919    [ up i ⇒
     
    2525      mk_stacksize_info new_stack (maximum acc)
    2626    ] in
    27   foldr ?? f.
     27  foldl ?? f.
     28
     29lemma foldr_append : ∀A,B,f,b,l1,l2.
     30foldr A B f b (l1@l2) = foldr A B f (foldr A B f b l2) l1.
     31#A #B #f #b #l1 elim l1 -l1 [#l2 %]
     32#hd #tl #IH #l2 whd in ⊢ (??%%); >IH %
     33qed.
     34
     35lemma foldl_append : ∀A,B,f,b,l1,l2.
     36foldl A B f b (l1@l2) = foldl A B f (foldl A B f b l1) l2.
     37#A #B #f #b #l1 lapply b -b elim l1 -l1 [#b #l2 %]
     38#hd #tl #IH #b #l2 whd in ⊢ (??%(????%?)); >IH %
     39qed.
     40
     41lemma update_stacksize_info_append :
     42∀ss,info,l1,l2.
     43update_stacksize_info ss info (l1 @ l2) =
     44update_stacksize_info ss (update_stacksize_info ss info l1) l2.
     45#ss #info @foldl_append qed.
    2846
    2947definition extract_call_ud_from_observables :
     
    3250[ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in
    3351foldr ?? (λev.append ? (f ev)) [ ].
     52
     53lemma extract_call_ud_from_observables_append :
     54∀l1,l2.extract_call_ud_from_observables (l1@l2) =
     55  extract_call_ud_from_observables l1 @ extract_call_ud_from_observables l2.
     56#l1 elim l1 -l1 [ #l2 % ]
     57#hd #tl #IH #l2 whd in ⊢ (??%(??%?)); >associative_append @eq_f @IH qed.
     58
     59lemma update_stacksize_info_max_monotone :
     60∀ss,info,l.maximum info ≤ maximum (update_stacksize_info ss info l).
     61#ss #info #l lapply info elim l -l [ #info % ]
     62* #id #tl #IH #info
     63whd in match (update_stacksize_info ???); normalize nodelta
     64change with (update_stacksize_info ???) in ⊢ (??(?%));
     65@(transitive_le ???? (IH …))
     66[ whd in ⊢ (??%); @(leb_elim (?:ℕ)) #H ] //
     67qed.
    3468
    3569definition extract_call_ud_from_tlr :
  • src/compiler.ma

    r3083 r3145  
    8282(* Inefficient, replace with Trie lookup *)
    8383definition lookup_stack_cost ≝
    84  λP,p,id.
    85   assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p).
     84 λP,p.stack_sizes … (stack_cost P p).
    8685
    8786definition back_end :
     
    121120  OK ? p.
    122121
    123 (* Cost lifting *)
    124 include "ASM/ASMCosts.ma".
    125 
    126 definition lift_out_of_sigma :
    127   ∀A,B : Type[0].∀P_out : A → Prop.B →
    128     (∀a.P_out a + ¬ P_out a) →
    129   ((Σa.P_out a) → B) → A → B ≝ λA,B,P_out,dflt,dec,m,a_sig.
    130    match dec a_sig with
    131    [ inl prf ⇒ m «a_sig, prf»
    132    | inr _ ⇒ dflt (* labels not present in out code get 0 *)
    133    ].
    134 
    135 definition lift_cost_map_back_to_front :
    136   ∀oc.
    137     let abstat ≝ OC_abstract_status oc in
    138   as_cost_map abstat → clight_cost_map ≝
    139   λoc,asm_cost_map.
    140   lift_out_of_sigma … 0 (* labels not present in out code get 0 *)
    141     (strong_decidable_in_codomain …) asm_cost_map.
    142 
    143122(* Cost model computation *)
    144123include "ASM/ASMCostsSplit.ma".
     
    160139  ! p ← assembler observe p;
    161140  let k ≝ ASM_cost_map p in
    162   let k' ≝
    163    lift_cost_map_back_to_front p k in
    164   return mk_compiler_output p stack_cost max_stack init_costlabel p' k'.
     141  return mk_compiler_output p stack_cost max_stack init_costlabel p' k.
  • src/correctness.ma

    r3115 r3145  
    2121definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝
    2222λcostmap,itrace.
    23   let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
     23  let ctrace ≝ costlabels_of_observables itrace in
    2424  Σ_{l ∈ ctrace}(costmap l).
    2525
     
    4646qed.
    4747
    48 lemma bigsum_append : ∀A,l1,l2. ∀f:A → ℕ.
    49   (Σ_{l ∈ (l1@l2)}(f l)) = (Σ_{l ∈ l1}(f l)) + (Σ_{l ∈ l2}(f l)).
    50 #A #l1 elim l1
    51 [ #l2 #f %
    52 | #h #tl #IH #l2 #f whd in ⊢ (??%(?%?)); >IH //
    53 ] qed.
     48include "ASM/CostsProof.ma".
    5449
    5550lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs.
     
    6257whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
    6358whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
    64 >filter_map_append >bigsum_append >commutative_plus @sym_eq @minus_plus_m_m
    65 qed.
    66 
    67 include "common/AssocList.ma".
    68 
    69 definition lookup_stack_cost : stack_cost_model → ident → option nat ≝
    70  λstack_cost,id.
    71   assoc_list_lookup ?? id (eq_identifier …) stack_cost.
     59>costlabels_of_observables_append >fold_sum' >commutative_plus @sym_eq @minus_plus_m_m
     60qed.
    7261
    7362definition simulates ≝
     
    7665  ∀m1,m2.
    7766   measurable Clight_pcs (c_labelled_clight … p) m1 m2
    78     (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
     67    (stack_sizes (c_stack_cost … p)) (c_max_stack … p) →
    7968  ∀c1,c2.
    8069   clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
     
    8574    (c_labelled_object_code … p) n1 n2
    8675  ∧
    87    minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
     76   clock ?? (execute (n1 + n2) ? initial_status) =
     77    plus (clock ?? (execute n1 ? initial_status)) (minus c2 c1).
    8878
    8979include "Clight/SwitchAndLabel.ma".
     
    10393include "LTL/LTLToLINAxiom.ma".
    10494include "LIN/LINToASMAxiom.ma".
     95
    10596include "ASM/AssemblyAxiom.ma".
     97include "ASM/OC_traces_to_exec.ma".
    10698
    10799lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
     
    116108  whd in ⊢ (??%?); @breakup_pair %
    117109| skip ]| skip ]
     110qed.
     111
     112record back_end_preconditions (p_rtlabs : RTLabs_program)
     113(stacksizes : ident → option ℕ) (max_stack : ℕ)
     114(prefix, subtrace : list intensional_event) (fn : ident)
     115: Prop ≝
     116{ ra_init : RTLabs_status (make_global p_rtlabs)
     117; ra_init_ok : make_ext_initial_state p_rtlabs = return ra_init
     118; ra_max :
     119  le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0)
     120    (extract_call_ud_from_observables (prefix @ subtrace)))) max_stack
     121; ra_ft_tlr : ft_and_tlr (RTLabs_status (make_global p_rtlabs))
     122    prefix subtrace fn ra_init
     123}.
     124
     125lemma front_end_correct :
     126∀observe, input_program, init_cost, labelled, p_rtlabs.
     127front_end observe input_program = return 〈init_cost, labelled, p_rtlabs〉 →
     128not_wrong … (exec_inf … clight_fullexec input_program) →
     129sim_with_labels
     130 (exec_inf … clight_fullexec input_program)
     131 (exec_inf … clight_fullexec labelled)
     132
     133  ∀m1,m2,stacksizes,max_stack.
     134   measurable Clight_pcs labelled m1 m2 stacksizes max_stack →
     135  ∃prefix, subtrace, fn.
     136  observables Clight_pcs labelled m1 m2 = return 〈prefix, subtrace〉 ∧
     137  back_end_preconditions p_rtlabs stacksizes max_stack
     138    prefix subtrace fn.
     139#observe #p_in #init_cost' #labelled #p_rtlabs #EQ_front_end
     140whd in EQ_front_end:(??%?);
     141letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
     142inversion (clight_label cl_switch_removed)
     143#cl_labelled #init_cost #CL_LABELLED
     144whd in ⊢ (??%? → ?);
     145letin cl_simplified ≝ (simplify_program ?)
     146#H @('bind_inversion H) -H #cminor #CMINOR
     147#H @('bind_inversion H) -H #WCL #_
     148#H @('bind_inversion H) -H #INJ #_
     149letin rtlabs ≝ (cminor_to_rtlabs cminor)
     150whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     151
     152#NOT_WRONG %
     153[ cut (cl_labelled = \fst (clight_label cl_switch_removed))
     154  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
     155  #E >E
     156  @switch_and_labelling_sim @NOT_WRONG
     157]
     158
     159#m1 #m2 #stacksizes #max_stack #m1_m2_meas
     160cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
     161cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
     162#simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %;
     163cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
     164#cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
     165cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
     166#ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
     167#OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
     168#ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
     169>OBS -ra_meas
     170cases (produce_rtlabs_flat_trace … ra_exec_prefix)
     171#ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
     172%{prefix} %{subtrace} %{fn} %[%]
     173%{ra_init_ok ra_max}
     174%{ra_unrepeating EQ_ra_pref_obs ra_obs'}
     175(* fn is the current function ... *) cases daemon
     176qed.
     177
     178lemma back_end_correct :
     179∀observe,init_cost,p_rtlabs,p_asm,init_cost',stack_m,max_stack,prefix,subtrace,fn.
     180back_end observe init_cost p_rtlabs = return 〈〈p_asm, init_cost'〉,stack_m,max_stack〉 →
     181back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn →
     182init_cost = init_cost' ∧
     183∀sigma,pol.
     184ft_and_tlr (ASM_status p_asm sigma pol)
     185prefix subtrace fn
     186(initialise_status ? p_asm).
     187#observe #init_cost #p_rtlabs #p_asm' #init_cost #stack_model #max_stack
     188#prefix #subtrace #fn
     189#H @('bind_inversion H) -H
     190#p_asm
     191#H lapply (opt_eq_from_res ???? H) -H
     192#EQ_lin_to_asm
     193#H lapply (sym_eq ??? H) -H
     194whd in ⊢ (??%%→?); #EQ destruct(EQ)
     195letin p_rtl ≝ (rtlabs_to_rtl init_cost p_rtlabs)
     196letin p_ertl ≝ (rtl_to_ertl p_rtl)
     197letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
     198letin p_lin ≝ (ltl_to_lin p_ltl)
     199letin stack_model ≝ (\snd (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
     200letin stack_sizes ≝ (stack_sizes stack_model)
     201*
     202#ra_init #ra_init_ok #ra_max #ra_ft_tlr %[%]
     203#sigma #pol
     204
     205cases (RTLabsToRTL_ok stack_model init_cost … ra_init_ok)
     206[2: @(transitive_stack_cost_model_le … (RTLabsToRTL_monotone_stacksizes init_cost …))
     207   @(transitive_stack_cost_model_le … (RTLToERTL_monotone_stacksizes …))
     208   @ERTLToLTL_monotone_stacksizes ]
     209#rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl
     210cases (status_simulation_produce_ft_and_tlr … prefix subtrace fn … simul_ra_rtl ra_ft_tlr)
     211change with (state_pc RTL_semantics_separate) in rtl_init;
     212change with
     213  (state_pc RTL_semantics_separate → state_pc RTL_semantics_separate → ?)
     214#rtl_st2 #rtl_st3 #rtl_ft #rtl_tlr #rtl_unrepeating #rtl_ft_ok
     215#current_is_fn #rtl_tlr_ok
     216
     217lapply (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes
     218  p_rtl fn … rtl_ft rtl_tlr ??? rtl_unrepeating) try assumption
     219[ whd whd in match extract_call_ud_from_ft; whd in match extract_call_ud_from_tlr;
     220  normalize nodelta >rtl_ft_ok >rtl_tlr_ok
     221  <extract_call_ud_from_observables_append assumption
     222]
     223>rtl_ft_ok >rtl_tlr_ok #rtl_ft_tlr
     224
     225cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
     226#rtl_init' * #rtl_init_ok' * #R_rtl #simul_rtl
     227lapply (status_simulation_produce_ft_and_tlr … simul_rtl rtl_ft_tlr)
     228-rtl_ft_tlr #rtl_ft_tlr -R_rtl -rtl_st2 -rtl_st3 -R_ra_rtl -ra_init -ra_max
     229
     230cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok')
     231#ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
     232lapply (status_simulation_produce_ft_and_tlr … simul_rtl_ertl rtl_ft_tlr)
     233-rtl_init -rtl_init' -R_rtl_ertl #ertl_ft_tlr
     234
     235lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl)
     236@pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux
     237#ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl
     238lapply (status_simulation_produce_ft_and_tlr … simul_ertl_ltl ertl_ft_tlr)
     239-ertl_init -R_ertl_ltl #ltl_ft_tlr
     240
     241cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok)
     242#lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
     243lapply (status_simulation_produce_ft_and_tlr … simul_ltl_lin ltl_ft_tlr)
     244-ltl_init -R_ltl_lin #lin_ft_tlr
     245
     246cases (LINToASM_ok stack_sizes p_lin p_asm sigma pol EQ_lin_to_asm lin_init lin_init_ok)
     247#R_lin_asm #simul_lin_asm
     248@(status_simulation_produce_ft_and_tlr … simul_lin_asm lin_ft_tlr)
     249qed.
     250
     251lemma assembler_correct :
     252∀observe,input_program,output_program,prefix,subtrace,fn.
     253assembler observe input_program = return output_program →
     254(∀sigma,pol.ft_and_tlr (ASM_status input_program sigma pol) prefix subtrace fn
     255  (initialise_status ? input_program)) →
     256ft_and_tlr (OC_abstract_status output_program)
     257prefix subtrace fn (initialise_status ? (cm output_program)).
     258#observe #p_asm #p_oc #prefix #subtrace #fn
     259#H @('bind_inversion H) -H ** #sigma #pol normalize nodelta #sigma_pol_ok
     260#H lapply (opt_eq_from_res ???? H) -H #jump_expansion_ok
     261whd in ⊢ (??%%→?); #H lapply (sym_eq ??? H) -H #EQ destruct(EQ)
     262#H lapply (H sigma pol) -H
     263
     264cases (assembly_ok p_asm … jump_expansion_ok)
     265#R_asm_oc #simul_asm_oc
     266@(status_simulation_produce_ft_and_tlr … simul_asm_oc)
    118267qed.
    119268
     
    132281** #init_cost #labelled #p_rtlabs #EQ_front_end
    133282#H @('bind_inversion H) -H
    134 ** #p_asm #stack_costs #globals_size
    135 #H @('bind_inversion H) -H
    136 #p_asm'
    137 #H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
    138 whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
    139 #H @('bind_inversion H) -H
    140 #p_loc #EQ_assembler
    141 whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
    142 
    143 whd in EQ_front_end:(??%?);
    144 letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
    145 lapply (refl ? (clight_label cl_switch_removed))
    146 cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED
    147 whd in ⊢ (??%? → ?);
    148 letin cl_simplified ≝ (simplify_program ?)
    149 #H @('bind_inversion H) -H #cminor #CMINOR
    150 #H @('bind_inversion H) -H #WCL #_
    151 #H @('bind_inversion H) -H #INJ #_
    152 letin rtlabs ≝ (cminor_to_rtlabs cminor)
    153 #EQ_front_end
    154 
    155 #NOT_WRONG %
    156 [ whd in EQ_front_end:(??%%); destruct
    157   cut (labelled = \fst (clight_label cl_switch_removed))
    158   [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
    159   #E >E
    160   @switch_and_labelling_sim @NOT_WRONG
    161 | cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ]
    162   #El >El
    163   #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
    164   cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
    165   >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
    166   cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
    167   #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; -m1 -m2
    168   cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
    169   #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
    170   cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
    171   #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
    172   #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
    173   #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
    174   >OBS -ra_meas
    175    
    176   (* So, after the front-end we have for RTLabs:
    177      ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
    178      ra_tlr         - structured trace from [ra_s1] to some [ra_s2],
    179      ra_unrepeating - PCs don't repeat locally in [ra_tlr]
    180      ra_obs'        - the observables from [ra_tlr] are [subtrace]
    181      ra_max         - the stack bound is respected in [prefix@subtrace]
    182    *)
    183 
    184   cases (produce_rtlabs_flat_trace … ra_exec_prefix)
    185   #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
    186   letin p_rtl ≝ (rtlabs_to_rtl init_cost (cminor_to_rtlabs cminor))
    187   letin p_ertl ≝ (rtl_to_ertl p_rtl)
    188   letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
    189   letin p_lin ≝ (ltl_to_lin p_ltl)
    190   letin stack_sizes ≝ (lookup_stack_cost (\snd (\fst
    191     (ertl_to_ltl compute_fixpoint colour_graph p_ertl))))
    192   cases (RTLabsToRTL_ok stack_sizes init_cost … ra_init_ok)
    193   [2: cases daemon ]
    194   #rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl
    195   cases (status_simulation_produce_ft_and_tlr … ra_ft ra_tlr simul_ra_rtl)
    196   change with (state_pc RTL_semantics_separate) in rtl_init;
    197   change with (state_pc RTL_semantics_separate → ?)
    198   #rtl_st2 * change with (state_pc RTL_semantics_separate → ?)
    199   #rtl_st3 * change with (state_pc RTL_semantics_separate → ?)
    200   #rtl_st4 * #rtl_ft * #rtl_tlr * #rtl_taaf ** #_ -rtl_st4
    201   #rtl_ft_ok #rtl_tlr_ok
    202   cases (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
    203     rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
    204   [2,3: cases daemon (* good stack usage, consequence of ra_max *) ]
    205   #rtl_ft' * #rtl_tlr' * #rtl_ft_ok' #rtl_tlr_ok'
    206   cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
    207   #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
    208   cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
    209   #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
    210   #rtl_ft_ok'' #rtl_tlr_ok''
    211   cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok'')
    212   #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
    213   cases (status_simulation_produce_ft_and_tlr … rtl_ft'' rtl_tlr'' simul_rtl_ertl)
    214   #ertl_st2 * #ertl_st3 * #ertl_st4 * #ertl_ft * #ertl_tlr * #ertl_taaf ** #_ -ertl_st4
    215   #ertl_ft_ok #ertl_tlr_ok
    216   lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl)
    217   @pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux
    218   #ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl
    219   cases (status_simulation_produce_ft_and_tlr … ertl_ft ertl_tlr simul_ertl_ltl)
    220   #ltl_st2 * #ltl_st3 * #ltl_st4 * #ltl_ft * #ltl_tlr * #ltl_taaf ** #_ -ltl_st4
    221   #ltl_ft_ok #ltl_tlr_ok
    222   cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok)
    223   #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
    224   cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
    225   #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
    226   #lin_ft_ok #lin_tlr_ok
    227   @('bind_inversion EQ_assembler) ** #sigma #pol #sigma_pol_ok -EQ_assembler
    228   #EQ lapply (opt_eq_from_res ???? EQ) #jump_expansion_ok -EQ
    229   whd in ⊢ (??%%→?); #EQ
    230   cut (p_loc = assembly p_asm' (λx.sigma x) (λx.pol x))
    231   [ -EQ_ra_pref_obs -ra_obs' -ra_exec_prefix -ltl_init_ok -jump_expansion_ok
    232     -rtl_init -rtl_ft'' -ltl_ft -lin_init -ltl_init -ertl_init -rtl_init'
    233     -El destruct(EQ) % ] #EQ_p_loc -EQ
    234    
    235   @@@@
    236    
    237   cases (LINToASM_ok stack_sizes p_lin p_asm' sigma pol EQ_lin_to_asm lin_init lin_init_ok)
    238   #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
    239   cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
    240   #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
    241   #lin_ft_ok #lin_tlr_ok
    242  
    243  
    244  
    245  
    246   #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
    247   cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
    248   #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
    249   #rtl_ft_ok'' #rtl_tlr_ok''
    250  
    251  
    252   [2: @rtl_init_ok
    253   RTL_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
    254     rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
    255   )
    256   #aux lapply (aux rtl_init rtl_st2 rtl_st3) -aux #aux
    257   lapply (aux rtl_ft rtl_tlr) ??)
    258   cases (RTLToERTL_ok stack_sizes init_cost … ra_init_ok)
    259  
    260   [5:
    261   cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr.
    262     exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 →
    263 
    264      
    265              
    266              
     283*** #p_asm' #init_cost' #stack_costs #max_stack #EQ_back_end normalize nodelta
     284#H @('bind_inversion H) -H #p_oc #EQ_assembler
     285whd in ⊢ (??%%→?); #EQ destruct(EQ) #NOT_WRONG
     286
     287cases (front_end_correct … EQ_front_end NOT_WRONG) #H1 #H2
     288%{H1} #m1 #m2 #m1_m2_meas
     289#c1 #c2 #c1_prf #c2_prf
     290cases (H2 … m1_m2_meas)
     291#prefix * #subtrace * #fn * #OBS #back_end_pre >OBS
     292>(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
     293
     294cases (back_end_correct … EQ_back_end back_end_pre) #EQ destruct(EQ)
     295#assembler_pre
     296cases (assembler_correct … EQ_assembler assembler_pre)
     297#oc_st2 #oc_st3 #oc_ft #oc_tlr #oc_unrepeating #oc_ft_ok #fn_ok #oc_tlr_ok
     298
     299%{(ft_length … oc_ft)}
     300%{(tlr_length … oc_tlr)}
     301%
     302[ >(OC_traces_to_observables … fn_ok) >oc_ft_ok >oc_tlr_ok %
     303| >execute_plus >OC_ft_to_execute >OC_tlr_to_execute
     304  whd in match exec_cost_of_trace; normalize nodelta <oc_tlr_ok
     305  >costlabels_of_observables_trace_label_return_id_irrelevant [2: %{one}]
     306  @(compute_max_trace_label_return_cost_ok_with_trace … oc_unrepeating)
     307]
     308qed.
  • src/joint/Joint.ma

    r3037 r3145  
    630630definition stack_cost_model ≝ list (ident × nat).
    631631
     632(* move! *)
     633let rec list_map_opt A B (f : A → option B) (l : list A) on l : list B ≝
     634match l with
     635[ nil ⇒ [ ]
     636| cons hd tl ⇒
     637  (match f hd with [ Some x ⇒ [ x ] | None ⇒ [ ]]) @ list_map_opt … f tl
     638].
     639
    632640definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝
    633641 λp,pr.
    634   foldr …
    635    (λid_fun,acc. let 〈id,fun〉 ≝ id_fun in
    636      match fun with
    637      [ Internal jif ⇒ 〈id,joint_if_stacksize ?? (pi1 … jif)〉::acc
    638      | External _ ⇒ acc ])
    639    [ ] (prog_funct ?? pr).
     642  list_map_opt …
     643    (λid_fun.match \snd id_fun with
     644      [ Internal jif ⇒ Some ? 〈\fst id_fun, joint_if_stacksize ?? (pi1 … jif)〉
     645      | _ ⇒ None ?
     646      ]) (prog_funct ?? pr).
     647
     648definition stack_sizes : stack_cost_model → ident → option ℕ ≝
     649λm,id.find …
     650  (λpr.if eq_identifier … id (\fst pr) then Some ? (\snd pr) else None ?) m.
    640651
    641652include "common/Globalenvs.ma". (* for size_init_data_list, probably to be moved to AST.ma *)
  • src/joint/Traces.ma

    r3041 r3145  
    4545    (* regs ≝ *)(empty_regsT … spp)
    4646    (* mem ≝ *)m
    47     (* stack_usage ≝ *)globals_size in
     47    (* stack_usage ≝ *)0 in
    4848  return
    4949  mk_state_pc ?
Note: See TracChangeset for help on using the changeset viewer.