Changeset 3145 for src/correctness.ma


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

Legend:

Unmodified
Added
Removed
  • 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.
Note: See TracChangeset for help on using the changeset viewer.