Changeset 3145 for src/correctness.ma
 Timestamp:
 Apr 15, 2013, 4:31:50 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r3115 r3145 21 21 definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝ 22 22 λcostmap,itrace. 23 let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl  _ ⇒ None ? ])itrace in23 let ctrace ≝ costlabels_of_observables itrace in 24 24 Σ_{l ∈ ctrace}(costmap l). 25 25 … … 46 46 qed. 47 47 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. 48 include "ASM/CostsProof.ma". 54 49 55 50 lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs. … … 62 57 whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2 63 58 whd 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 60 qed. 72 61 73 62 definition simulates ≝ … … 76 65 ∀m1,m2. 77 66 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) → 79 68 ∀c1,c2. 80 69 clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 → … … 85 74 (c_labelled_object_code … p) n1 n2 86 75 ∧ 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). 88 78 89 79 include "Clight/SwitchAndLabel.ma". … … 103 93 include "LTL/LTLToLINAxiom.ma". 104 94 include "LIN/LINToASMAxiom.ma". 95 105 96 include "ASM/AssemblyAxiom.ma". 97 include "ASM/OC_traces_to_exec.ma". 106 98 107 99 lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max. … … 116 108 whd in ⊢ (??%?); @breakup_pair % 117 109  skip ] skip ] 110 qed. 111 112 record 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 125 lemma front_end_correct : 126 ∀observe, input_program, init_cost, labelled, p_rtlabs. 127 front_end observe input_program = return 〈init_cost, labelled, p_rtlabs〉 → 128 not_wrong … (exec_inf … clight_fullexec input_program) → 129 sim_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 140 whd in EQ_front_end:(??%?); 141 letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end; 142 inversion (clight_label cl_switch_removed) 143 #cl_labelled #init_cost #CL_LABELLED 144 whd in ⊢ (??%? → ?); 145 letin 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 #_ 149 letin rtlabs ≝ (cminor_to_rtlabs cminor) 150 whd 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 160 cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS 161 cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas) 162 #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; 163 cases (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 165 cases (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 170 cases (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 176 qed. 177 178 lemma back_end_correct : 179 ∀observe,init_cost,p_rtlabs,p_asm,init_cost',stack_m,max_stack,prefix,subtrace,fn. 180 back_end observe init_cost p_rtlabs = return 〈〈p_asm, init_cost'〉,stack_m,max_stack〉 → 181 back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn → 182 init_cost = init_cost' ∧ 183 ∀sigma,pol. 184 ft_and_tlr (ASM_status p_asm sigma pol) 185 prefix 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 194 whd in ⊢ (??%%→?); #EQ destruct(EQ) 195 letin p_rtl ≝ (rtlabs_to_rtl init_cost p_rtlabs) 196 letin p_ertl ≝ (rtl_to_ertl p_rtl) 197 letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl))) 198 letin p_lin ≝ (ltl_to_lin p_ltl) 199 letin stack_model ≝ (\snd (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl))) 200 letin stack_sizes ≝ (stack_sizes stack_model) 201 * 202 #ra_init #ra_init_ok #ra_max #ra_ft_tlr %[%] 203 #sigma #pol 204 205 cases (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 210 cases (status_simulation_produce_ft_and_tlr … prefix subtrace fn … simul_ra_rtl ra_ft_tlr) 211 change with (state_pc RTL_semantics_separate) in rtl_init; 212 change 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 217 lapply (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 225 cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok) 226 #rtl_init' * #rtl_init_ok' * #R_rtl #simul_rtl 227 lapply (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 230 cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok') 231 #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl 232 lapply (status_simulation_produce_ft_and_tlr … simul_rtl_ertl rtl_ft_tlr) 233 rtl_init rtl_init' R_rtl_ertl #ertl_ft_tlr 234 235 lapply (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 238 lapply (status_simulation_produce_ft_and_tlr … simul_ertl_ltl ertl_ft_tlr) 239 ertl_init R_ertl_ltl #ltl_ft_tlr 240 241 cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok) 242 #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin 243 lapply (status_simulation_produce_ft_and_tlr … simul_ltl_lin ltl_ft_tlr) 244 ltl_init R_ltl_lin #lin_ft_tlr 245 246 cases (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) 249 qed. 250 251 lemma assembler_correct : 252 ∀observe,input_program,output_program,prefix,subtrace,fn. 253 assembler 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)) → 256 ft_and_tlr (OC_abstract_status output_program) 257 prefix 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 261 whd in ⊢ (??%%→?); #H lapply (sym_eq ??? H) H #EQ destruct(EQ) 262 #H lapply (H sigma pol) H 263 264 cases (assembly_ok p_asm … jump_expansion_ok) 265 #R_asm_oc #simul_asm_oc 266 @(status_simulation_produce_ft_and_tlr … simul_asm_oc) 118 267 qed. 119 268 … … 132 281 ** #init_cost #labelled #p_rtlabs #EQ_front_end 133 282 #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 frontend 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 285 whd in ⊢ (??%%→?); #EQ destruct(EQ) #NOT_WRONG 286 287 cases (front_end_correct … EQ_front_end NOT_WRONG) #H1 #H2 288 %{H1} #m1 #m2 #m1_m2_meas 289 #c1 #c2 #c1_prf #c2_prf 290 cases (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 294 cases (back_end_correct … EQ_back_end back_end_pre) #EQ destruct(EQ) 295 #assembler_pre 296 cases (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 ] 308 qed.
Note: See TracChangeset
for help on using the changeset viewer.