Changeset 3074


Ignore:
Timestamp:
Apr 2, 2013, 7:25:22 PM (4 years ago)
Author:
campbell
Message:

Put some kind of high level proof in for front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r3047 r3074  
    4141
    4242include "RTLabs/MeasurableToStructured.ma".
    43 
    44 definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝
    45 λp,n,costmap.
    46   ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n;
     43include "common/ExtraMonads.ma".
     44
     45definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝
     46λcostmap,itrace.
    4747  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
    48   return Σ_{l ∈ ctrace}(costmap l).
     48  Σ_{l ∈ ctrace}(costmap l).
     49
     50definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝
     51λC,p,n,costmap.
     52  ! 〈s,itrace〉 ← exec_steps_with_obs C p n;
     53  return exec_cost_of_trace costmap itrace.
     54
     55lemma obs_exec_steps_with_obs : ∀pcs,p,m1,m2,obs1,obs2.
     56  observables pcs p m1 m2 = return 〈obs1,obs2〉 →
     57  ∃s1,s2.
     58    exec_steps_with_obs pcs p m1 = return 〈s1,obs1〉 ∧
     59    exec_steps_with_obs pcs p (m1+m2) = return 〈s2,obs1@obs2〉.
     60#pcs #p #m1 #m2 #obs1 #obs2 #OBS
     61@('bind_inversion OBS) -OBS #s0 #INIT #OBS
     62@('bind_inversion OBS) -OBS * #tr1 #s1 #EXEC1 #OBS
     63@('bind_inversion OBS) -OBS * #tr2 #s2 #EXEC2 @breakup_pair #OBS
     64whd in OBS:(??%%); destruct
     65%{s1} %{s2}
     66whd in ⊢ (?(??%?)(??%?)); >INIT
     67whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2)
     68whd in ⊢ (?(??%?)(??%?));
     69% [ % | >int_trace_append' @breakup_pair @breakup_pair % ]
     70qed.
     71
     72lemma bigsum_append : ∀A,l1,l2. ∀f:A → ℕ.
     73  (Σ_{l ∈ (l1@l2)}(f l)) = (Σ_{l ∈ l1}(f l)) + (Σ_{l ∈ l2}(f l)).
     74#A #l1 elim l1
     75[ #l2 #f %
     76| #h #tl #IH #l2 #f whd in ⊢ (??%(?%?)); >IH //
     77] qed.
     78
     79lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs.
     80  observables pcs p m1 m2 = return 〈obs1,obs2〉 →
     81  clock_after pcs p m1 costs = return c1 →
     82  clock_after pcs p (m1+m2) costs = return c2 →
     83  c2 - c1 = exec_cost_of_trace costs obs2.
     84#pcs #p #m1 #m2 #obs1 #obs2 #c1 #c2 #costs #OBS
     85cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2
     86whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
     87whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
     88>filter_map_append >bigsum_append /2/
     89qed.
    4990
    5091include "common/AssocList.ma".
     
    61102    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
    62103  ∀c1,c2.
    63    clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
    64    clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = OK … c2 →
     104   clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
     105   clock_after Clight_pcs (c_labelled_clight … p) (m1+m2) (c_clight_cost_map … p) = OK … c2 →
    65106  ∃n1,n2.
    66107   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
     
    70111   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    71112
    72 include "common/ExtraMonads.ma".
    73 
    74113include "Clight/SwitchAndLabel.ma".
     114
     115include "common/FEMeasurable.ma".
     116include "Clight/SimplifyCastsMeasurable.ma".
     117include "Clight/toCminorMeasurable.ma".
     118include "Cminor/toRTLabsCorrectness.ma".
     119
     120lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
     121  measurable pcs p m1 m2 stack_cost max →
     122  ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉.
     123#pcs #p #m1 #m2 #stack_cost #max
     124* #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_
     125% [2: % [2:
     126  whd in ⊢ (??%?); >INIT in ⊢ (??%?);
     127  whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?);
     128  whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?);
     129  whd in ⊢ (??%?); @breakup_pair %
     130| skip ]| skip ]
     131qed.
    75132
    76133theorem correct :
     
    115172  #E >E
    116173  @switch_and_labelling_sim @NOT_WRONG
    117 | #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
    118 
     174| cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ]
     175  #El >El
     176  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
     177  cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
     178  >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
     179  cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
     180  #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; -m1 -m2
     181  cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
     182  #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
     183  cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
     184  #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
     185  #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
     186  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
     187  >OBS -ra_meas
     188 
     189  (* So, we have for RTLabs:
     190     ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
     191     ra_tlr         - structured trace from [ra_s1] to some [ra_s2],
     192     ra_unrepeating - PCs don't repeat locally in [ra_tlr]
     193     ra_obs'        - the observables from [ra_tlr] are [subtrace]
     194     ra_max         - the stack bound is respected in [prefix@subtrace]
     195   *)
     196
     197
     198(* Old, semiformal cut
    119199cut (∀n,s1,s2,obs1,obs2.
    120200          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
     
    125205   observables (OC_preclassified_system (c_labelled_object_code … p))
    126206    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
    127    
     207    *)
    128208     
    129209             
    130210             
    131  
    132 (* start of old simulates 
    133 
    134 (* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
    135    [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
    136    according to the [stack_cost] function. *)
    137 axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
    138 axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
    139 
    140 
    141   let cl_trace ≝ exec_inf … clight_fullexec labelled in
    142   let asm_trace ≝ exec_inf … ASM_fullexec object_code in
    143   not_wrong ? cl_trace →
    144   ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
    145   𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
    146 
    147 *)
    148 
    149 (* TODO
    150 
    151 
    152 ∀input_program.
    153 ! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
    154 
    155 exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
    156 
    157 
    158 
    159 exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
    160 (* Should we be lifting labels in some way here? *)
    161 
    162 
    163 
    164 ∀i,f : clight_status.
    165   Clight_labelled i →
    166   Clight_labelled f →
    167 ∀mx,time.
    168   let trace ≝ exec_inf_aux … clight_fullexec labelled i in
    169   will_return O O mx time f trace →
    170   mx < max_allowed_stack →
    171 ∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
    172   time = clock f' - clock i'.
    173 
    174 
    175 ∀s,flat.
    176 let ge ≝ (globalenvs … labelled) in
    177 subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
    178 RTLabs_cost s = true →
    179 ∀WR : will_return ge 0 s flat.
    180 let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
    181 let labels_rtlabs ≝ flat_label_trace … flat WR in
    182 ∃!initial,final,structured_trace_asm.
    183   structured_trace_rtlabs ≈ structured_trace_asm ∧ 
    184   clock … code_memory … final = clock … code_memory … initial +
    185      (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
    186 
    187 
    188 
    189 What is ≃l?  Must show that "labelled" does everything that
    190 "input_program" does, without getting lost in some
    191 non-terminating loop part way.
    192 
    193 *)
    194 
Note: See TracChangeset for help on using the changeset viewer.