[1996] | 1 | |
---|
| 2 | include "compiler.ma". |
---|
| 3 | |
---|
| 4 | include "ASM/Interpret2.ma". |
---|
| 5 | |
---|
[2802] | 6 | include "Clight/Clight_classified_system.ma". |
---|
[2322] | 7 | |
---|
[2323] | 8 | (* From measurable on Clight, we will end up with an RTLabs flat trace where |
---|
| 9 | we know that there are some m' and n' such that the prefix in Clight matches |
---|
| 10 | the prefix in RTLabs given by m', the next n steps in Clight are equivalent |
---|
| 11 | to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs |
---|
| 12 | for those n' steps so that we can build a corresponding structured trace. |
---|
| 13 | |
---|
| 14 | "Equivalent" here means, in particular, that the observables will be the same, |
---|
| 15 | and those observables will include the stack space costs. |
---|
| 16 | *) |
---|
| 17 | |
---|
[3021] | 18 | include "RTLabs/MeasurableToStructured.ma". |
---|
[3074] | 19 | include "common/ExtraMonads.ma". |
---|
[2399] | 20 | |
---|
[3074] | 21 | definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝ |
---|
| 22 | λcostmap,itrace. |
---|
[3145] | 23 | let ctrace ≝ costlabels_of_observables itrace in |
---|
[3074] | 24 | Σ_{l ∈ ctrace}(costmap l). |
---|
[2399] | 25 | |
---|
[3156] | 26 | definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝ |
---|
| 27 | λC,p,m. |
---|
| 28 | let g ≝ make_global … (pcs_exec … C) p in |
---|
| 29 | let C' ≝ pcs_to_cs C g in |
---|
| 30 | ! s0 ← make_initial_state … p; |
---|
| 31 | ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0; |
---|
| 32 | return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉. |
---|
| 33 | |
---|
[3074] | 34 | definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝ |
---|
| 35 | λC,p,n,costmap. |
---|
| 36 | ! 〈s,itrace〉 ← exec_steps_with_obs C p n; |
---|
| 37 | return exec_cost_of_trace costmap itrace. |
---|
| 38 | |
---|
| 39 | lemma obs_exec_steps_with_obs : ∀pcs,p,m1,m2,obs1,obs2. |
---|
| 40 | observables pcs p m1 m2 = return 〈obs1,obs2〉 → |
---|
| 41 | ∃s1,s2. |
---|
| 42 | exec_steps_with_obs pcs p m1 = return 〈s1,obs1〉 ∧ |
---|
| 43 | exec_steps_with_obs pcs p (m1+m2) = return 〈s2,obs1@obs2〉. |
---|
| 44 | #pcs #p #m1 #m2 #obs1 #obs2 #OBS |
---|
| 45 | @('bind_inversion OBS) -OBS #s0 #INIT #OBS |
---|
| 46 | @('bind_inversion OBS) -OBS * #tr1 #s1 #EXEC1 #OBS |
---|
| 47 | @('bind_inversion OBS) -OBS * #tr2 #s2 #EXEC2 @breakup_pair #OBS |
---|
| 48 | whd in OBS:(??%%); destruct |
---|
| 49 | %{s1} %{s2} |
---|
| 50 | whd in ⊢ (?(??%?)(??%?)); >INIT |
---|
| 51 | whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2) |
---|
| 52 | whd in ⊢ (?(??%?)(??%?)); |
---|
| 53 | % [ % | >int_trace_append' @breakup_pair @breakup_pair % ] |
---|
| 54 | qed. |
---|
| 55 | |
---|
[3145] | 56 | include "ASM/CostsProof.ma". |
---|
[3074] | 57 | |
---|
| 58 | lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs. |
---|
| 59 | observables pcs p m1 m2 = return 〈obs1,obs2〉 → |
---|
| 60 | clock_after pcs p m1 costs = return c1 → |
---|
| 61 | clock_after pcs p (m1+m2) costs = return c2 → |
---|
| 62 | c2 - c1 = exec_cost_of_trace costs obs2. |
---|
| 63 | #pcs #p #m1 #m2 #obs1 #obs2 #c1 #c2 #costs #OBS |
---|
| 64 | cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2 |
---|
| 65 | whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2 |
---|
| 66 | whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct |
---|
[3145] | 67 | >costlabels_of_observables_append >fold_sum' >commutative_plus @sym_eq @minus_plus_m_m |
---|
[3074] | 68 | qed. |
---|
| 69 | |
---|
[2322] | 70 | definition simulates ≝ |
---|
[2774] | 71 | λp: compiler_output. |
---|
[3003] | 72 | let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in |
---|
[2774] | 73 | ∀m1,m2. |
---|
| 74 | measurable Clight_pcs (c_labelled_clight … p) m1 m2 |
---|
[3145] | 75 | (stack_sizes (c_stack_cost … p)) (c_max_stack … p) → |
---|
[2774] | 76 | ∀c1,c2. |
---|
[3074] | 77 | clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 → |
---|
| 78 | clock_after Clight_pcs (c_labelled_clight … p) (m1+m2) (c_clight_cost_map … p) = OK … c2 → |
---|
[2774] | 79 | ∃n1,n2. |
---|
| 80 | observables Clight_pcs (c_labelled_clight … p) m1 m2 = |
---|
[2875] | 81 | observables (OC_preclassified_system (c_labelled_object_code … p)) |
---|
| 82 | (c_labelled_object_code … p) n1 n2 |
---|
[2774] | 83 | ∧ |
---|
[3145] | 84 | clock ?? (execute (n1 + n2) ? initial_status) = |
---|
| 85 | plus (clock ?? (execute n1 ? initial_status)) (minus c2 c1). |
---|
[2322] | 86 | |
---|
[3047] | 87 | include "Clight/SwitchAndLabel.ma". |
---|
| 88 | |
---|
[3074] | 89 | include "common/FEMeasurable.ma". |
---|
| 90 | include "Clight/SimplifyCastsMeasurable.ma". |
---|
| 91 | include "Clight/toCminorMeasurable.ma". |
---|
| 92 | include "Cminor/toRTLabsCorrectness.ma". |
---|
| 93 | |
---|
[3096] | 94 | (* atm they are all axioms *) |
---|
| 95 | include "RTLabs/RTLabsToRTLAxiom.ma". |
---|
| 96 | include "RTL/RTL_separate_to_overflow.ma". |
---|
| 97 | include "RTL/RTL_overflow_to_unique.ma". |
---|
| 98 | include "RTL/RTLToERTLAxiom.ma". |
---|
| 99 | include "ERTL/ERTLToLTLAxiom.ma". |
---|
| 100 | include "LTL/LTLToLINAxiom.ma". |
---|
| 101 | include "LIN/LINToASMAxiom.ma". |
---|
[3145] | 102 | |
---|
[3096] | 103 | include "ASM/AssemblyAxiom.ma". |
---|
[3145] | 104 | include "ASM/OC_traces_to_exec.ma". |
---|
[3096] | 105 | |
---|
[3074] | 106 | lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max. |
---|
| 107 | measurable pcs p m1 m2 stack_cost max → |
---|
| 108 | ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉. |
---|
| 109 | #pcs #p #m1 #m2 #stack_cost #max |
---|
| 110 | * #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_ |
---|
| 111 | % [2: % [2: |
---|
| 112 | whd in ⊢ (??%?); >INIT in ⊢ (??%?); |
---|
| 113 | whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?); |
---|
| 114 | whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?); |
---|
| 115 | whd in ⊢ (??%?); @breakup_pair % |
---|
| 116 | | skip ]| skip ] |
---|
| 117 | qed. |
---|
| 118 | |
---|
[3145] | 119 | record back_end_preconditions (p_rtlabs : RTLabs_program) |
---|
| 120 | (stacksizes : ident → option ℕ) (max_stack : ℕ) |
---|
| 121 | (prefix, subtrace : list intensional_event) (fn : ident) |
---|
| 122 | : Prop ≝ |
---|
| 123 | { ra_init : RTLabs_status (make_global p_rtlabs) |
---|
| 124 | ; ra_init_ok : make_ext_initial_state p_rtlabs = return ra_init |
---|
| 125 | ; ra_max : |
---|
| 126 | le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0) |
---|
| 127 | (extract_call_ud_from_observables (prefix @ subtrace)))) max_stack |
---|
| 128 | ; ra_ft_tlr : ft_and_tlr (RTLabs_status (make_global p_rtlabs)) |
---|
| 129 | prefix subtrace fn ra_init |
---|
| 130 | }. |
---|
| 131 | |
---|
| 132 | lemma front_end_correct : |
---|
| 133 | ∀observe, input_program, init_cost, labelled, p_rtlabs. |
---|
| 134 | front_end observe input_program = return 〈init_cost, labelled, p_rtlabs〉 → |
---|
| 135 | not_wrong … (exec_inf … clight_fullexec input_program) → |
---|
| 136 | sim_with_labels |
---|
| 137 | (exec_inf … clight_fullexec input_program) |
---|
| 138 | (exec_inf … clight_fullexec labelled) |
---|
| 139 | ∧ |
---|
| 140 | ∀m1,m2,stacksizes,max_stack. |
---|
| 141 | measurable Clight_pcs labelled m1 m2 stacksizes max_stack → |
---|
| 142 | ∃prefix, subtrace, fn. |
---|
| 143 | observables Clight_pcs labelled m1 m2 = return 〈prefix, subtrace〉 ∧ |
---|
| 144 | back_end_preconditions p_rtlabs stacksizes max_stack |
---|
| 145 | prefix subtrace fn. |
---|
| 146 | #observe #p_in #init_cost' #labelled #p_rtlabs #EQ_front_end |
---|
| 147 | whd in EQ_front_end:(??%?); |
---|
| 148 | letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end; |
---|
| 149 | inversion (clight_label cl_switch_removed) |
---|
| 150 | #cl_labelled #init_cost #CL_LABELLED |
---|
| 151 | whd in ⊢ (??%? → ?); |
---|
| 152 | letin cl_simplified ≝ (simplify_program ?) |
---|
| 153 | #H @('bind_inversion H) -H #cminor #CMINOR |
---|
| 154 | #H @('bind_inversion H) -H #WCL #_ |
---|
| 155 | #H @('bind_inversion H) -H #INJ #_ |
---|
| 156 | letin rtlabs ≝ (cminor_to_rtlabs cminor) |
---|
| 157 | whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) |
---|
| 158 | |
---|
| 159 | #NOT_WRONG % |
---|
| 160 | [ cut (cl_labelled = \fst (clight_label cl_switch_removed)) |
---|
| 161 | [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ] |
---|
| 162 | #E >E |
---|
| 163 | @switch_and_labelling_sim @NOT_WRONG |
---|
| 164 | ] |
---|
| 165 | |
---|
| 166 | #m1 #m2 #stacksizes #max_stack #m1_m2_meas |
---|
| 167 | cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS |
---|
| 168 | cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas) |
---|
| 169 | #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; |
---|
| 170 | cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas) |
---|
| 171 | #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2 |
---|
| 172 | cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas) |
---|
| 173 | #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2 |
---|
| 174 | #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS) |
---|
[3156] | 175 | #ra_s0 * #ra_s1 * #ra_s2 * #fn * #ra_init * #ra_ft * * #ra_ft_fn #ra_ft_obs * #ra_tlr * * #ra_unrepeating #ra_max #ra_obs' |
---|
[3145] | 176 | >OBS -ra_meas |
---|
| 177 | %{prefix} %{subtrace} %{fn} %[%] |
---|
[3156] | 178 | %{ra_init ra_max} |
---|
| 179 | %{ra_unrepeating ra_ft_obs ra_ft_fn ra_obs'} |
---|
[3145] | 180 | qed. |
---|
| 181 | |
---|
| 182 | lemma back_end_correct : |
---|
| 183 | ∀observe,init_cost,p_rtlabs,p_asm,init_cost',stack_m,max_stack,prefix,subtrace,fn. |
---|
| 184 | back_end observe init_cost p_rtlabs = return 〈〈p_asm, init_cost'〉,stack_m,max_stack〉 → |
---|
| 185 | back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn → |
---|
| 186 | init_cost = init_cost' ∧ |
---|
| 187 | ∀sigma,pol. |
---|
| 188 | ft_and_tlr (ASM_status p_asm sigma pol) |
---|
| 189 | prefix subtrace fn |
---|
| 190 | (initialise_status ? p_asm). |
---|
| 191 | #observe #init_cost #p_rtlabs #p_asm' #init_cost #stack_model #max_stack |
---|
| 192 | #prefix #subtrace #fn |
---|
| 193 | #H @('bind_inversion H) -H |
---|
| 194 | #p_asm |
---|
| 195 | #H lapply (opt_eq_from_res ???? H) -H |
---|
| 196 | #EQ_lin_to_asm |
---|
| 197 | #H lapply (sym_eq ??? H) -H |
---|
| 198 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 199 | letin p_rtl ≝ (rtlabs_to_rtl init_cost p_rtlabs) |
---|
| 200 | letin p_ertl ≝ (rtl_to_ertl p_rtl) |
---|
| 201 | letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl))) |
---|
| 202 | letin p_lin ≝ (ltl_to_lin p_ltl) |
---|
| 203 | letin stack_model ≝ (\snd (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl))) |
---|
| 204 | letin stack_sizes ≝ (stack_sizes stack_model) |
---|
| 205 | * |
---|
| 206 | #ra_init #ra_init_ok #ra_max #ra_ft_tlr %[%] |
---|
| 207 | #sigma #pol |
---|
| 208 | |
---|
| 209 | cases (RTLabsToRTL_ok stack_model init_cost … ra_init_ok) |
---|
| 210 | [2: @(transitive_stack_cost_model_le … (RTLabsToRTL_monotone_stacksizes init_cost …)) |
---|
| 211 | @(transitive_stack_cost_model_le … (RTLToERTL_monotone_stacksizes …)) |
---|
| 212 | @ERTLToLTL_monotone_stacksizes ] |
---|
| 213 | #rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl |
---|
| 214 | cases (status_simulation_produce_ft_and_tlr … prefix subtrace fn … simul_ra_rtl ra_ft_tlr) |
---|
| 215 | change with (state_pc RTL_semantics_separate) in rtl_init; |
---|
| 216 | change with |
---|
| 217 | (state_pc RTL_semantics_separate → state_pc RTL_semantics_separate → ?) |
---|
| 218 | #rtl_st2 #rtl_st3 #rtl_ft #rtl_tlr #rtl_unrepeating #rtl_ft_ok |
---|
| 219 | #current_is_fn #rtl_tlr_ok |
---|
| 220 | |
---|
| 221 | lapply (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes |
---|
| 222 | p_rtl fn … rtl_ft rtl_tlr ??? rtl_unrepeating) try assumption |
---|
| 223 | [ whd whd in match extract_call_ud_from_ft; whd in match extract_call_ud_from_tlr; |
---|
| 224 | normalize nodelta >rtl_ft_ok >rtl_tlr_ok |
---|
| 225 | <extract_call_ud_from_observables_append assumption |
---|
| 226 | ] |
---|
| 227 | >rtl_ft_ok >rtl_tlr_ok #rtl_ft_tlr |
---|
| 228 | |
---|
| 229 | cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok) |
---|
| 230 | #rtl_init' * #rtl_init_ok' * #R_rtl #simul_rtl |
---|
| 231 | lapply (status_simulation_produce_ft_and_tlr … simul_rtl rtl_ft_tlr) |
---|
| 232 | -rtl_ft_tlr #rtl_ft_tlr -R_rtl -rtl_st2 -rtl_st3 -R_ra_rtl -ra_init -ra_max |
---|
| 233 | |
---|
| 234 | cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok') |
---|
| 235 | #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl |
---|
| 236 | lapply (status_simulation_produce_ft_and_tlr … simul_rtl_ertl rtl_ft_tlr) |
---|
| 237 | -rtl_init -rtl_init' -R_rtl_ertl #ertl_ft_tlr |
---|
| 238 | |
---|
| 239 | lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl) |
---|
| 240 | @pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux |
---|
| 241 | #ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl |
---|
| 242 | lapply (status_simulation_produce_ft_and_tlr … simul_ertl_ltl ertl_ft_tlr) |
---|
| 243 | -ertl_init -R_ertl_ltl #ltl_ft_tlr |
---|
| 244 | |
---|
| 245 | cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok) |
---|
| 246 | #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin |
---|
| 247 | lapply (status_simulation_produce_ft_and_tlr … simul_ltl_lin ltl_ft_tlr) |
---|
| 248 | -ltl_init -R_ltl_lin #lin_ft_tlr |
---|
| 249 | |
---|
| 250 | cases (LINToASM_ok stack_sizes p_lin p_asm sigma pol EQ_lin_to_asm lin_init lin_init_ok) |
---|
| 251 | #R_lin_asm #simul_lin_asm |
---|
| 252 | @(status_simulation_produce_ft_and_tlr … simul_lin_asm lin_ft_tlr) |
---|
| 253 | qed. |
---|
| 254 | |
---|
| 255 | lemma assembler_correct : |
---|
| 256 | ∀observe,input_program,output_program,prefix,subtrace,fn. |
---|
| 257 | assembler observe input_program = return output_program → |
---|
| 258 | (∀sigma,pol.ft_and_tlr (ASM_status input_program sigma pol) prefix subtrace fn |
---|
| 259 | (initialise_status ? input_program)) → |
---|
| 260 | ft_and_tlr (OC_abstract_status output_program) |
---|
| 261 | prefix subtrace fn (initialise_status ? (cm output_program)). |
---|
| 262 | #observe #p_asm #p_oc #prefix #subtrace #fn |
---|
| 263 | #H @('bind_inversion H) -H ** #sigma #pol normalize nodelta #sigma_pol_ok |
---|
| 264 | #H lapply (opt_eq_from_res ???? H) -H #jump_expansion_ok |
---|
| 265 | whd in ⊢ (??%%→?); #H lapply (sym_eq ??? H) -H #EQ destruct(EQ) |
---|
| 266 | #H lapply (H sigma pol) -H |
---|
| 267 | |
---|
| 268 | cases (assembly_ok p_asm … jump_expansion_ok) |
---|
| 269 | #R_asm_oc #simul_asm_oc |
---|
| 270 | @(status_simulation_produce_ft_and_tlr … simul_asm_oc) |
---|
| 271 | qed. |
---|
| 272 | |
---|
[3030] | 273 | theorem correct : |
---|
[2852] | 274 | ∀observe. |
---|
[2774] | 275 | ∀input_program,output. |
---|
[2852] | 276 | compile observe input_program = return output → |
---|
[2322] | 277 | not_wrong … (exec_inf … clight_fullexec input_program) → |
---|
[2774] | 278 | sim_with_labels |
---|
| 279 | (exec_inf … clight_fullexec input_program) |
---|
| 280 | (exec_inf … clight_fullexec (c_labelled_clight … output)) |
---|
[2322] | 281 | ∧ |
---|
[2774] | 282 | simulates output. |
---|
[2928] | 283 | #observe #p_in #out |
---|
| 284 | #H @('bind_inversion H) -H |
---|
| 285 | ** #init_cost #labelled #p_rtlabs #EQ_front_end |
---|
| 286 | #H @('bind_inversion H) -H |
---|
[3145] | 287 | *** #p_asm' #init_cost' #stack_costs #max_stack #EQ_back_end normalize nodelta |
---|
| 288 | #H @('bind_inversion H) -H #p_oc #EQ_assembler |
---|
| 289 | whd in ⊢ (??%%→?); #EQ destruct(EQ) #NOT_WRONG |
---|
[3022] | 290 | |
---|
[3145] | 291 | cases (front_end_correct … EQ_front_end NOT_WRONG) #H1 #H2 |
---|
| 292 | %{H1} #m1 #m2 #m1_m2_meas |
---|
| 293 | #c1 #c2 #c1_prf #c2_prf |
---|
| 294 | cases (H2 … m1_m2_meas) |
---|
| 295 | #prefix * #subtrace * #fn * #OBS #back_end_pre >OBS |
---|
| 296 | >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2 |
---|
[3022] | 297 | |
---|
[3145] | 298 | cases (back_end_correct … EQ_back_end back_end_pre) #EQ destruct(EQ) |
---|
| 299 | #assembler_pre |
---|
| 300 | cases (assembler_correct … EQ_assembler assembler_pre) |
---|
| 301 | #oc_st2 #oc_st3 #oc_ft #oc_tlr #oc_unrepeating #oc_ft_ok #fn_ok #oc_tlr_ok |
---|
[3115] | 302 | |
---|
[3145] | 303 | %{(ft_length … oc_ft)} |
---|
| 304 | %{(tlr_length … oc_tlr)} |
---|
| 305 | % |
---|
| 306 | [ >(OC_traces_to_observables … fn_ok) >oc_ft_ok >oc_tlr_ok % |
---|
| 307 | | >execute_plus >OC_ft_to_execute >OC_tlr_to_execute |
---|
| 308 | whd in match exec_cost_of_trace; normalize nodelta <oc_tlr_ok |
---|
| 309 | >costlabels_of_observables_trace_label_return_id_irrelevant [2: %{one}] |
---|
| 310 | @(compute_max_trace_label_return_cost_ok_with_trace … oc_unrepeating) |
---|
| 311 | ] |
---|
| 312 | qed. |
---|