Changeset 3096 for src/correctness.ma


Ignore:
Timestamp:
Apr 5, 2013, 6:04:14 PM (7 years ago)
Author:
tranquil
Message:

preliminary work on closing correctness.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r3074 r3096  
    8686whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
    8787whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
    88 >filter_map_append >bigsum_append /2/
     88>filter_map_append >bigsum_append >commutative_plus @sym_eq @minus_plus_m_m
    8989qed.
    9090
     
    117117include "Clight/toCminorMeasurable.ma".
    118118include "Cminor/toRTLabsCorrectness.ma".
     119
     120(* atm they are all axioms *)
     121include "RTLabs/RTLabsExecToTrace.ma".
     122include "RTLabs/RTLabsToRTLAxiom.ma".
     123include "RTL/RTL_separate_to_overflow.ma".
     124include "RTL/RTL_overflow_to_unique.ma".
     125include "RTL/RTLToERTLAxiom.ma".
     126include "ERTL/ERTLToLTLAxiom.ma".
     127include "LTL/LTLToLINAxiom.ma".
     128include "LIN/LINToASMAxiom.ma".
     129include "ASM/AssemblyAxiom.ma".
    119130
    120131lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
     
    186197  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
    187198  >OBS -ra_meas
    188  
     199  cases (produce_rtlabs_flat_trace … ra_exec_prefix)
     200  #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
     201  letin p_rtl ≝ (rtlabs_to_rtl init_cost (cminor_to_rtlabs cminor))
     202  letin p_ertl ≝ (rtl_to_ertl p_rtl)
     203  letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
     204  letin p_lin ≝ (ltl_to_lin p_ltl)
     205  letin stack_sizes ≝ (lookup_stack_cost (\snd (\fst
     206    (ertl_to_ltl compute_fixpoint colour_graph p_ertl))))
     207  cases (RTLabsToRTL_ok stack_sizes init_cost … ra_init_ok)
     208  [2: cases daemon ]
     209  #rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl
     210  cases (status_simulation_produce_ft_and_tlr … ra_ft ra_tlr simul_ra_rtl)
     211  change with (state_pc RTL_semantics_separate) in rtl_init;
     212  change with (state_pc RTL_semantics_separate → ?)
     213  #rtl_st2 * change with (state_pc RTL_semantics_separate → ?)
     214  #rtl_st3 * change with (state_pc RTL_semantics_separate → ?)
     215  #rtl_st4 * #rtl_ft * #rtl_tlr * #rtl_taaf ** #_ -rtl_st4
     216  #rtl_ft_ok #rtl_tlr_ok
     217  cases (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
     218    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
     219  [2,3: cases daemon (* good stack usage, consequence of ra_max *) ]
     220  #rtl_ft' * #rtl_tlr' * #rtl_ft_ok' #rtl_tlr_ok'
     221  cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
     222  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
     223  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
     224  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
     225  #rtl_ft_ok'' #rtl_tlr_ok''
     226  cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok'')
     227  #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
     228  cases (status_simulation_produce_ft_and_tlr … rtl_ft'' rtl_tlr'' simul_rtl_ertl)
     229  #ertl_st2 * #ertl_st3 * #ertl_st4 * #ertl_ft * #ertl_tlr * #ertl_taaf ** #_ -ertl_st4
     230  #ertl_ft_ok #ertl_tlr_ok
     231  lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl)
     232  @pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux
     233  #ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl
     234  cases (status_simulation_produce_ft_and_tlr … ertl_ft ertl_tlr simul_ertl_ltl)
     235  #ltl_st2 * #ltl_st3 * #ltl_st4 * #ltl_ft * #ltl_tlr * #ltl_taaf ** #_ -ltl_st4
     236  #ltl_ft_ok #ltl_tlr_ok
     237  cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_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  @('bind_inversion EQ_assembler) ** #sigma #pol #sigma_pol_ok -EQ_assembler
     243  #EQ lapply (opt_eq_from_res ???? EQ) #jump_expansion_ok -EQ
     244  whd in ⊢ (??%%→?); #EQ
     245  cut (p_loc = assembly p_asm' (λx.sigma x) (λx.pol x))
     246  [ -EQ_ra_pref_obs -ra_obs' -ra_exec_prefix -ltl_init_ok -jump_expansion_ok
     247    -rtl_init -rtl_ft'' -ltl_ft -lin_init -ltl_init -ertl_init -rtl_init'
     248    -El destruct(EQ) % ] #EQ_p_loc -EQ
     249   
     250  @@@@
     251   
     252  cases (LINToASM_ok stack_sizes p_lin p_asm' sigma pol EQ_lin_to_asm lin_init lin_init_ok)
     253  #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
     254  cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
     255  #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
     256  #lin_ft_ok #lin_tlr_ok
     257 
     258 
     259 
     260 
     261  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
     262  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
     263  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
     264  #rtl_ft_ok'' #rtl_tlr_ok''
     265 
     266 
     267  [2: @rtl_init_ok
     268  RTL_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
     269    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
     270  )
     271  #aux lapply (aux rtl_init rtl_st2 rtl_st3) -aux #aux
     272  lapply (aux rtl_ft rtl_tlr) ??)
     273  cases (RTLToERTL_ok stack_sizes init_cost … ra_init_ok)
     274 
     275  [5:
     276  cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr.
     277    exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 →
     278   
    189279  (* So, we have for RTLabs:
    190280     ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
Note: See TracChangeset for help on using the changeset viewer.