Changeset 3096


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

preliminary work on closing correctness.ma

Location:
src
Files:
2 added
10 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r3065 r3096  
    157157   (λst. return (execute_1_pseudo_instruction' … addr_of_label addr_of_symbol sigma policy st))
    158158   (initialise_status … c).
     159
     160definition ASM_status:
     161 ∀prog:pseudo_assembly_program.
     162 ∀sigma,policy.abstract_status ≝
     163  λc,sigma,policy.
     164  let label_map ≝ \fst (create_label_cost_map (code … c)) in
     165  let symbol_map ≝ construct_datalabels (preamble … c) in
     166  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
     167  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
     168  ASM_abstract_status c addr_of_label addr_of_symbol sigma policy.
     169
  • src/ERTL/ERTLToLTLAxiom.ma

    r3014 r3096  
    1818(* what should we do with n? *)
    1919let stacksizes ≝ lookup_stack_cost m in
     20∀init_in.make_initial_state
     21  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
     22∃init_out.
     23  make_initial_state
     24   (mk_prog_params LTL_semantics p_out stacksizes) =
     25    OK ? init_out ∧
    2026∃[1] R.
    21   status_simulation
     27  status_simulation_with_init
    2228    (joint_status ERTL_semantics p_in stacksizes)
    2329    (joint_status LTL_semantics p_out stacksizes)
    24     R ∧
    25   ∀init_in.make_initial_state
    26     (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
    27   ∃init_out.
    28     make_initial_state
    29      (mk_prog_params LTL_semantics p_out stacksizes) =
    30       OK ? init_out ∧
    31    R init_in init_out.
     30    R init_in init_out.
  • src/LIN/LINToASMAxiom.ma

    r2946 r3096  
    1717include "joint/Traces.ma".
    1818include "common/StatusSimulation.ma".
    19 
    20 (* atm ASM_abstract_status is related to object code, not ASM... *)
    21 axiom ASM_status : pseudo_assembly_program → abstract_status.
    22 axiom make_ASM_initial_state : ∀p.res (ASM_status p).
     19include "ASM/Interpret2.ma".
    2320
    2421axiom LINToASM_ok :
     
    2623∀p_in : joint_program LIN.
    2724∀p_out : pseudo_assembly_program.
     25∀sigma,policy.
    2826lin_to_asm p_in = Some ? p_out →
     27∀init_in.make_initial_state
     28    (mk_prog_params LIN_semantics p_in stacksizes) = OK … init_in →
     29let init_out ≝ initialise_status … p_out in
    2930∃[1] R.
    30   status_simulation
     31  status_simulation_with_init
    3132    (joint_status LIN_semantics p_in stacksizes)
    32     (ASM_status p_out)
    33     R ∧
    34   ∀init_in.make_initial_state
    35     (mk_prog_params LIN_semantics p_in stacksizes) = OK … init_in →
    36   ∃init_out.
    37     make_ASM_initial_state p_out =
    38       OK ? init_out ∧
    39    R init_in init_out.
     33    (ASM_status p_out sigma policy)
     34    R init_in init_out.
  • src/LTL/LTLToLINAxiom.ma

    r2946 r3096  
    1010∀p_in : joint_program LTL.
    1111let p_out ≝ ltl_to_lin p_in in
     12∀init_in.make_initial_state
     13  (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in →
     14∃init_out.
     15  make_initial_state
     16   (mk_prog_params LIN_semantics p_out stacksizes) =
     17    OK ? init_out ∧
    1218∃[1] R.
    13   status_simulation
     19  status_simulation_with_init
    1420    (joint_status LTL_semantics p_in stacksizes)
    1521    (joint_status LIN_semantics p_out stacksizes)
    16     R ∧
    17   ∀init_in.make_initial_state
    18     (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in →
    19   ∃init_out.
    20     make_initial_state
    21      (mk_prog_params LIN_semantics p_out stacksizes) =
    22       OK ? init_out ∧
    23    R init_in init_out.
     22    R init_in init_out.
  • src/RTL/RTLToERTLAxiom.ma

    r2946 r3096  
    55include "common/StatusSimulation.ma".
    66
    7 axiom RTLabsToRTL_ok :
     7axiom RTLToERTL_ok :
    88∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
    99∀p_in : rtl_program.
    1010let p_out ≝ rtl_to_ertl p_in in
     11  ∀init_in.make_initial_state
     12    (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
     13∃init_out.
     14  make_initial_state
     15   (mk_prog_params ERTL_semantics p_out stacksizes) =
     16    OK ? init_out ∧
    1117∃[1] R.
    12   status_simulation
     18  status_simulation_with_init
    1319    (joint_status RTL_semantics_unique p_in stacksizes)
    1420    (joint_status ERTL_semantics p_out stacksizes)
    15     R ∧
    16   ∀init_in.make_initial_state
    17     (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
    18   ∃init_out.
    19     make_initial_state
    20      (mk_prog_params ERTL_semantics p_out stacksizes) =
    21       OK ? init_out ∧
    22    R init_in init_out.
     21    R init_in init_out.
  • src/RTL/RTL_overflow_to_unique.ma

    r2946 r3096  
    66∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
    77∀p_in : rtl_program.
     8∀init_in.make_initial_state
     9  (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in →
     10∃init_out.
     11  make_initial_state
     12   (mk_prog_params RTL_semantics_unique p_in stacksizes) =
     13    OK ? init_out ∧
    814∃[1] R.
    9   status_simulation
     15  status_simulation_with_init
    1016    (joint_status RTL_semantics_separate_overflow p_in stacksizes)
    1117    (joint_status RTL_semantics_unique p_in stacksizes)
    12     R ∧
    13   ∀init_in.make_initial_state
    14     (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in →
    15   ∃init_out.
    16     make_initial_state
    17      (mk_prog_params RTL_semantics_unique p_in stacksizes) =
    18       OK ? init_out ∧
    19    R init_in init_out.
     18    R init_in init_out.
  • src/RTL/RTL_separate_to_overflow.ma

    r2946 r3096  
    22include "joint/Traces.ma".
    33include "common/stacksize.ma".
     4include "common/StatusSimulation.ma".
     5
     6definition extract_call_ud_from_ft ≝
     7  λS : abstract_status.λs1,s2.λft :flat_trace S s1 s2.
     8  extract_call_ud_from_observables … (ft_observables … ft).
     9
     10definition good_stack_usage_ft :
     11  ∀p, stacksizes.
     12  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
     13  flat_trace … st1 st2 → Prop ≝
     14  λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λft.
     15  ∀m : ℕ.m < 2^16 →
     16  let info ≝ mk_stacksize_info (stack_usage … st1) m in
     17  let info' ≝ update_stacksize_info stacksizes info
     18    (extract_call_ud_from_ft … ft) in
     19  maximum info' < 2^16.
    420
    521definition good_stack_usage_tlr :
     
    4157  maximum info' < 2^16.
    4258
     59axiom RTL_separate_to_overflow_produce_ft_and_tlr :
     60∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
     61∀p_in : rtl_program.
     62let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
     63let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
     64∀fn.∀st1,st1',st1'' : state_pc RTL_semantics_separate.
     65∀ft1 : flat_trace S1 st1 st1'.
     66∀tlr1 : trace_label_return S1 st1' st1''.
     67good_stack_usage_ft … ft1 →
     68good_stack_usage_tlr … fn tlr1 →
     69∃ft2 : flat_trace S2 st1 st1'.
     70∃tlr2 : trace_label_return S2 st1' st1''.
     71ft_observables … ft1 = ft_observables … ft2 ∧
     72tlr_rel … tlr1 tlr2.
     73
     74(*
    4375axiom RTL_separate_to_overflow_produce_tlr :
    4476∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
     
    73105good_stack_usage_tal … curr_id tal →
    74106trace_any_label S2 fl s1 s2.
    75 
    76 
    77 
    78 
     107*)
  • src/RTLabs/RTLabsToRTLAxiom.ma

    r2946 r3096  
    1818include "RTLabs/RTLabs_abstract.ma".
    1919include "RTL/RTL_semantics.ma".
     20include "RTLabs/MeasurableToStructured.ma". (* for make_ext_initial_state *)
    2021
    21 (* this is in incomplete RTLabs/MeasurableToStructured.ma *)
    22 definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
    23 λp.
    24   let ge ≝ make_global p in
    25   do m ← init_mem … (λx.[Init_space x]) p;
    26   let main ≝ prog_main ?? p in
    27   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    28   do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
    29   let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
    30   return (mk_RTLabs_ext_state (make_global p) s [b] ?).
    31 % [ @Ef | % ]
    32 qed.
    33 
    34 (* this should say something like λf,p.∀〈i, Internal f〉 ∈ functs p.f i ≥ stacksize f. *)
    35 axiom RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop.
     22definition RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop ≝
     23λstack_sizes,p.
     24All …
     25  (λi_f.let 〈i, f〉 ≝ i_f in
     26    match f with
     27    [ External _ ⇒ True
     28    | Internal def ⇒
     29      ∃sz.stack_sizes i = Some ? sz ∧ f_stacksize … def ≤ sz
     30    ]) (prog_funct … p).
    3631
    3732axiom RTLabsToRTL_ok :
    3833∀stacksizes : ident → option ℕ.
     34∀cost.
    3935∀p_in : RTLabs_program.
    4036RTLabsToRTLstacksizes_ok stacksizes p_in →
    41 let p_out ≝ rtlabs_to_rtl p_in in
     37let p_out ≝ rtlabs_to_rtl cost p_in in
     38∀init_in.make_ext_initial_state p_in = OK … init_in →
     39∃init_out : state_pc RTL_semantics_separate.
     40  make_initial_state
     41   (mk_prog_params RTL_semantics_separate p_out stacksizes) =
     42    OK ? init_out ∧
    4243∃[1] R.
    43   status_simulation
     44  status_simulation_with_init
    4445    (RTLabs_status (make_global … p_in))
    45     (joint_status RTL_semantics_separate p_out stacksizes) R ∧
    46   ∀init_in.make_ext_initial_state p_in = OK … init_in →
    47   ∃init_out : state_pc RTL_semantics_separate.
    48     make_initial_state
    49      (mk_prog_params RTL_semantics_separate p_out stacksizes) =
    50       OK ? init_out ∧
    51    R init_in init_out.
     46    (joint_status RTL_semantics_separate p_out stacksizes) R
     47    init_in init_out.
  • src/common/StatusSimulation.ma

    r2991 r3096  
    3333  ; call_rel : (Σs.as_classifier S1 s cl_call) →
    3434               (Σs.as_classifier S2 s cl_call) → Prop
    35   ; sim_final :
    36     ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
    3735  }.
    3836
     
    5755   S will mark semantic relation, C call relation, L label relation, R return relation *)
    5856
    59 definition status_simulation ≝
    60   λS1 : abstract_status.
    61   λS2 : abstract_status.
    62   λsim_status_rel : status_rel S1 S2.
     57record status_simulation
     58  (S1, S2 : abstract_status)
     59  (sim_status_rel : status_rel S1 S2) : Prop ≝
     60{ one_step_sim :5>
    6361    ∀st1,st1',st2.as_execute S1 st1 st1' →
    6462    sim_status_rel st1 st2 →
     
    149147        sim_status_rel st1' st2' ∧
    150148        label_rel … st1' st2'
    151     ].
    152 
     149    ]
     150; sim_final :
     151  ∀st1,st2,res.as_result S1 st1 = Some ? res → sim_status_rel st1 st2 →
     152  as_result S2 st2 = Some ? res
     153}.
     154
     155record status_simulation_with_init (S1,S2 : abstract_status)
     156  (R : status_rel S1 S2)
     157  (init1 : S1) (init2 : S2) : Prop ≝
     158{ sim_init : R init1 init2
     159; sim_init_labels : label_rel … init1 init2
     160; sim_step_final :> status_simulation S1 S2 R
     161}.
    153162
    154163(* some useful lemmas *)
     
    584593qed.
    585594
     595definition is_cl_jump : ∀S : abstract_status.S → bool ≝
     596λS,s.match as_classify … s with [ cl_jump ⇒ true | _ ⇒ false ].
     597
     598definition enforce_costedness : ∀S : abstract_status.S → S → Prop ≝
     599λS,s1,s2.if is_cl_jump … s1 then as_costed … s2 else True.
     600
    586601(* finite flat traces, with recursive structure right to left. The list of
    587602   identifiers represents the call stack *)
    588 
    589 inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝
    590 | ft_start : flat_trace S start start [ ]
    591 | ft_advance_flat :
    592   ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
     603inductive flat_trace (S : abstract_status) (start : S) : S → Type[0] ≝
     604| ft_start : flat_trace S start start
     605| ft_advance :
     606  ∀st1,st2.flat_trace S start st1 → as_execute S st1 st2 →
     607  enforce_costedness … st1 st2 → flat_trace S start st2.
     608
     609(*
    593610  ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
    594611  flat_trace S start st2 stack
     
    605622  as_classifier ? st1 cl_return →
    606623  flat_trace S start st2 stack.
    607 
    608 let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack)
     624*)
     625
     626let rec ft_extend_taa S st1 st2 st3 (ft : flat_trace S st1 st2)
    609627  (taa : trace_any_any S st2 st3)
    610 on taa : flat_trace S st1 st3 stack
    611 match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
     628on taa : flat_trace S st1 st3
     629match taa return λst2,st3,taa.flat_trace ?? st2 → flat_trace ?? st3 with
    612630[ taa_base s ⇒ λacc.acc
    613631| taa_step st1 st2 st3 H G _ tl ⇒
    614   λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl
     632  λacc.ft_extend_taa ???? (ft_advance ???? acc H ?) tl
    615633] ft.
    616 
    617 lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2.
    618   ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 =
     634@hide_prf whd whd in match is_cl_jump; normalize nodelta >G % qed.
     635
     636lemma ft_extend_extend_taa : ∀S,st1,st2,st3,st4,ft,taa1,taa2.
     637  ft_extend_taa S st1 st3 st4 (ft_extend_taa … st2 … ft taa1) taa2 =
    619638  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
    620 #S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
     639#S #st1 #st2 #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
    621640/2/
    622641qed.
    623642
    624 definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack.
     643definition ft_extend_taaf ≝ λS,st1,st2,st3.λft : flat_trace S st1 st2.
    625644  λtaaf : trace_any_any_free S st2 st3.
    626   match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
     645  match taaf return λst2,st3,taaf.flat_trace ?? st2 → flat_trace ?? st3 with
    627646  [ taaf_base s ⇒ λft.ft
    628647  | taaf_step s1 s2 s3 pre H G ⇒
    629     λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G)
     648    λft.ft_advance … (ft_extend_taa … ft pre) H ?
    630649  | taaf_step_jump s1 s2 s3 pre H G K ⇒
    631     λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … (conj … G K))
     650    λft.ft_advance … (ft_extend_taa … ft pre) H ?
    632651  ] ft.
     652@hide_prf whd whd in match is_cl_jump; normalize nodelta >G // qed.
    633653
    634654definition option_to_list : ∀A.option A → list A ≝ λA,x.
     
    638658  ].
    639659
     660(*
     661let rec ft_stack S st st' (ft : flat_trace S st st') on ft : list ident ≝
     662match ft with
     663[ ft_start ⇒ [ ]
     664| ft_advance st1_mid st1' pre1 _ _ ⇒
     665  match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
     666  [ cl_call ⇒ λprf.
     667    let id ≝ as_call_ident ? «st1_mid, prf» in
     668    id :: ft_stack … pre1
     669  | cl_tailcall ⇒ λprf.
     670    let id ≝ as_tailcall_ident ? «st1_mid, prf» in
     671    match ft_stack … pre1 with
     672    [ nil ⇒ (* should never happen in correct programs *)
     673      [id]
     674    | cons _ stack' ⇒
     675      id :: stack'
     676    ]
     677  | cl_return ⇒ λ_.
     678    match ft_stack … pre1 with
     679    [ nil ⇒ (* should never happen in correct programs *)
     680      [ ]
     681    | cons _ stack' ⇒ stack'
     682    ]
     683  | _ ⇒ λ_.ft_stack … pre1
     684  ] (refl …)
     685].
     686*)
     687
    640688(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
    641 let rec ft_observables_aux acc S st st' stack
    642   (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
     689(* inefficient, but used only in correctness proofs *)
     690let rec ft_stack_observables S st st'
     691  (ft : flat_trace S st st') on ft : list ident × (list intensional_event) ≝
    643692match ft with
    644 [ ft_start ⇒ acc
    645 | ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒
     693[ ft_start ⇒ 〈[ ], [ ]〉
     694| ft_advance st1_mid st1' pre1 _ _ ⇒
     695  let 〈stack, tr〉 ≝ ft_stack_observables … pre1 in
    646696  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    647   ft_observables_aux (add @ acc) … pre1
    648 | ft_advance_call st1_mid st1' stack pre1 _ prf ⇒
    649   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    650   let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
    651   ft_observables_aux (add @ acc) … pre1
    652 | ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒
    653   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    654   let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in
    655   ft_observables_aux (add @ acc) … pre1
    656 | ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
    657   let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
    658   let add ≝ add @ [IEVret f] in
    659   ft_observables_aux (add @ acc) … pre1
     697  match as_classify … st1_mid return λx.as_classifier … st1_mid x → ? with
     698  [ cl_call ⇒ λprf.
     699    let id ≝ as_call_ident ? «st1_mid, prf» in
     700    let tr' ≝ tr @ add @ [IEVcall id] in
     701    〈id :: stack, tr'〉
     702  | cl_tailcall ⇒ λprf.
     703    let id ≝ as_tailcall_ident ? «st1_mid, prf» in
     704    match stack with
     705    [ nil ⇒ (* should never happen in correct programs *)
     706      〈[ ], tr @ add〉
     707    | cons f stack' ⇒
     708      let tr' ≝ tr @ add @ [IEVtailcall f id] in
     709      〈id :: stack', tr'〉
     710    ]
     711  | cl_return ⇒ λ_.
     712    match stack with
     713    [ nil ⇒ (* should never happen in correct programs *)
     714      〈[ ], tr @ add〉
     715    | cons f stack' ⇒
     716      let tr' ≝ tr @ add @ [IEVret f] in
     717      〈stack', tr'〉
     718    ]
     719  | _ ⇒ λ_.〈stack, tr @ add〉
     720  ] (refl …)
    660721].
    661722
    662 definition ft_observables ≝ ft_observables_aux [ ].
    663 
    664 lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft.
    665   ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc.
    666 #acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
    667 [ // ]
    668 #st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc
    669 whd in ⊢ (??%(??%?));
    670 >IH >IH >append_nil //
    671 qed.
    672 
    673 lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa.
    674   ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) =
    675     ft_observables … ft @
    676     if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
    677 #S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3
    678 [ #st2 #ft >append_nil % ]
     723definition ft_observables ≝ λS,st1,st2,ft.\snd (ft_stack_observables S st1 st2 ft).
     724definition ft_stack ≝ λS,st1,st2,ft.\fst (ft_stack_observables S st1 st2 ft).
     725
     726definition ft_current_function : ∀S,st1,st2.flat_trace S st1 st2 → option ident ≝
     727λS,st1,st2,ft.
     728match ft_stack … ft with [ nil ⇒ None ? | cons hd _ ⇒ Some ? hd ].
     729
     730lemma status_class_dep_match_elim :
     731∀A : Type[0].∀P : A → Prop.
     732∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
     733(∀prf : cl = cl_call.P (c_call prf)) →
     734(∀prf : cl = cl_return.P (c_return prf)) →
     735(∀prf : cl = cl_tailcall.P (c_tailcall prf)) →
     736(∀prf : cl = cl_other.P (c_other prf)) →
     737(∀prf : cl = cl_jump.P (c_jump prf)) →
     738P (match cl return λx.cl = x → ? with
     739   [ cl_call ⇒ c_call
     740   | cl_return ⇒ c_return
     741   | cl_tailcall ⇒ c_tailcall
     742   | cl_other ⇒ c_other
     743   | cl_jump ⇒ c_jump
     744   ] (refl …)).
     745#A #P * normalize // qed.
     746
     747lemma status_class_dep_match_rewrite :
     748∀A : Type[0].
     749∀cl,c_call,c_return,c_tailcall,c_other,c_jump.
     750∀cl'.
     751∀prf : cl = cl'.
     752match cl return λx.cl = x → A with
     753 [ cl_call ⇒ c_call
     754 | cl_return ⇒ c_return
     755 | cl_tailcall ⇒ c_tailcall
     756 | cl_other ⇒ c_other
     757 | cl_jump ⇒ c_jump
     758 ] (refl …) =
     759match cl' return λx.cl = x → A with
     760 [ cl_call ⇒ c_call
     761 | cl_return ⇒ c_return
     762 | cl_tailcall ⇒ c_tailcall
     763 | cl_other ⇒ c_other
     764 | cl_jump ⇒ c_jump
     765 ] prf.
     766#A * #c1 #c2 #c3 #c4 #c5 * #prf destruct % qed.
     767
     768lemma pair_elim' :
     769  ∀A,B,C : Type[0].∀T : A → B → C.∀t : A × B.
     770  ∀P : (A×B) → C → Prop.
     771  P 〈\fst t, \snd t〉 (T (\fst t) (\snd t)) →
     772  P t (let 〈a, b〉 ≝ t in T a b).
     773#A #B #C #T * // qed.
     774
     775lemma ft_extend_taa_obs : ∀S,st1,st2,st3,ft,taa.
     776  ft_stack_observables … (ft_extend_taa S st1 st2 st3 ft taa) =
     777    〈ft_stack … ft, ft_observables … ft @
     778    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
     779#S #st1 #st2 #st3 #ft #taa lapply ft elim taa -st2 -st3
     780[ #st2 #ft >append_nil @eq_pair_fst_snd ]
    679781#st2 #st3 #st4 #H #K #G #taa #IH #ft
    680 normalize in ⊢ (??(?????%)?); >IH
     782whd in ⊢ (??(????%)?); >IH normalize nodelta
    681783-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
    682784[ #st3 #H #G
    683785| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
    684786  >(not_costed_no_label … G)
    685 ] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
    686 qed.
    687 
    688 lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4.
    689   ∀ft : flat_trace S st1 st2 stack.
     787]
     788>append_nil whd in ⊢ (??(???%%)(????(??%?)));
     789whd in match (ft_stack_observables ????) ;
     790@(pair_elim' … (ft_stack_observables … ft))
     791>(status_class_dep_match_rewrite … K) %
     792qed.
     793
     794lemma ft_extend_taa_advance_obs : ∀S,st1,st2,st3,st4.
     795  ∀ft : flat_trace S st1 st2.
    690796  ∀taa : trace_any_any S st2 st3.
    691797  ∀H : as_execute S st3 st4.∀G.
    692   ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) =
    693   ft_observables … ft @
    694   option_to_list … (!l←as_label … st2;return IEVcost l) @
    695   [IEVcall (as_call_ident … «st3, G»)].
    696 #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
    697 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    698 >ft_extend_taa_obs
    699 lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    700 [ #st2 * #ft #H #G >append_nil %
    701 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
    702   >(not_costed_no_label … K)
    703   normalize nodelta //
    704 ]
    705 qed.
    706 
    707 lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4.
    708   ∀ft : flat_trace S st1 st2 (f :: stack).
    709   ∀taa : trace_any_any S st2 st3.
     798  ft_stack_observables … (ft_advance … (ft_extend_taa … ft taa) H G) =
     799  (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
     800   let 〈stack, tr〉 ≝ ft_stack_observables … ft in
     801   match as_classify … st3 return λx.as_classifier … st3 x → ? with
     802    [ cl_call ⇒ λprf.
     803      let id ≝ as_call_ident ? «st3, prf» in
     804      let tr' ≝ tr @ add @ [IEVcall id] in
     805      〈id :: ft_stack … ft, tr'〉
     806    | cl_tailcall ⇒ λprf.
     807      let id ≝ as_tailcall_ident ? «st3, prf» in
     808      match stack with
     809      [ nil ⇒ (* should never happen in correct programs *)
     810        〈[ ], tr @ add〉
     811      | cons f stack' ⇒
     812        let tr' ≝ tr @ add @ [IEVtailcall f id] in
     813        〈id :: stack', tr'〉
     814      ]
     815    | cl_return ⇒ λ_.
     816      match stack with
     817      [ nil ⇒ (* should never happen in correct programs *)
     818        〈[ ], tr @ add〉
     819      | cons f stack' ⇒
     820        let tr' ≝ tr @ add @ [IEVret f] in
     821        〈stack', tr'〉
     822      ]
     823    | _ ⇒ λ_.〈stack, tr @ add〉
     824    ] (refl …)).
     825#S #st1 #st2 #st3 #st4 #ft #taa #H #G normalize nodelta
     826whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
     827@status_class_dep_match_elim #prf
     828@status_class_dep_match_elim #prf'
     829try(@⊥ >prf in prf'; #prf' -prf destruct @False)
     830>ft_extend_taa_obs whd in match ft_stack; whd in match ft_observables; normalize nodelta
     831[2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
     832@eq_f >associative_append @eq_f
     833lapply prf lapply prf' lapply (taa_end_not_costed … taa)
     834cases taa -st3 -st2 normalize nodelta
     835[1,3,5,7,9,11,13: #st2 * #prf #prf' % ]
     836#st2 #st2' #st3 #H' #G' #K' #taa' #K #prf #prf'
     837>(not_costed_no_label … K) try % >append_nil %
     838qed.
     839
     840lemma ft_extend_taaf_obs : ∀S,st1,st2,st3,ft,taaf.
     841  ft_stack_observables … (ft_extend_taaf S st1 st2 st3 ft taaf) =
     842    〈ft_stack … ft,
     843     ft_observables … ft @
     844      if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]〉.
     845#S #st1 #st2 #st3 #ft #taa lapply ft cases taa -st2 -st3
     846[ #st2 #ft >append_nil @eq_pair_fst_snd ]
     847#st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
     848whd in match ft_extend_taaf; normalize nodelta
     849>ft_extend_taa_advance_obs @pair_elim'
     850>(status_class_dep_match_rewrite … G) %
     851qed.
     852
     853(*
     854lemma ft_extend_taaf_advance_obs : ∀S,st1,st2,st3,st4.
     855  ∀ft : flat_trace S st1 st2.
     856  ∀taaf : trace_any_any_free S st2 st3.
    710857  ∀H : as_execute S st3 st4.∀G.
    711   ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) =
    712   ft_observables … ft @
    713   option_to_list … (!l←as_label … st2;return IEVcost l) @
    714   [IEVtailcall f (as_tailcall_ident … «st3, G»)].
    715 #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
    716 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    717 >ft_extend_taa_obs
    718 lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    719 [ #st2 * #ft #H #G >append_nil %
    720 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
    721   >(not_costed_no_label … K)
    722   normalize nodelta //
    723 ]
    724 qed.
    725 
    726 lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4.
    727   ∀ft : flat_trace S st1 st2 (f :: stack).
    728   ∀taa : trace_any_any S st2 st3.
    729   ∀H : as_execute S st3 st4.∀G.
    730   ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) =
    731     ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f].
    732 #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
    733 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    734 >ft_extend_taa_obs
    735 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    736 [ #st2 * #ft #H >append_nil %
    737 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
    738   >(not_costed_no_label … K)
    739   normalize nodelta //
    740 ]
    741 qed.
    742 
    743 lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4.
    744   ∀ft : flat_trace S st1 st2 stack.
    745   ∀taa : trace_any_any S st2 st3.
    746   ∀H : as_execute S st3 st4.∀G.
    747   ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) =
    748     ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l).
    749 #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
    750 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    751 >ft_extend_taa_obs
    752 lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
    753 [ #st2 * #ft #H >append_nil %
    754 | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
    755   >(not_costed_no_label … K)
    756   normalize nodelta >append_nil //
    757 ]
    758 qed.
    759 
    760 lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf.
    761   ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) =
    762     ft_observables … ft @
    763     if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
    764 #S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
    765 [ #st2 #ft >append_nil % ]
    766 #st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
    767 @ft_extend_taa_advance_flat_obs
    768 qed.
     858  ft_stack_observables … (ft_advance … (ft_extend_taaf … ft taaf) H G) =
     859  (let add ≝ option_to_list … (! l ← as_label … st2 ; return IEVcost l) in
     860   let 〈stack, tr〉 ≝ ft_stack_observables … ft in
     861   match as_classify … st3 return λx.as_classifier … st3 x → ? with
     862    [ cl_call ⇒ λprf.
     863      let id ≝ as_call_ident ? «st3, prf» in
     864      let tr' ≝ tr @ add @ [IEVcall id] in
     865      〈id :: ft_stack … ft, tr'〉
     866    | cl_tailcall ⇒ λprf.
     867      let id ≝ as_tailcall_ident ? «st3, prf» in
     868      match stack with
     869      [ nil ⇒ (* should never happen in correct programs *)
     870        〈[ ], tr @ add〉
     871      | cons f stack' ⇒
     872        let tr' ≝ tr @ add @ [IEVtailcall f id] in
     873        〈id :: stack', tr'〉
     874      ]
     875    | cl_return ⇒ λ_.
     876      match stack with
     877      [ nil ⇒ (* should never happen in correct programs *)
     878        〈[ ], tr @ add〉
     879      | cons f stack' ⇒
     880        let tr' ≝ tr @ add @ [IEVret f] in
     881        〈stack', tr'〉
     882      ]
     883    | _ ⇒ λ_.〈stack, tr @ add〉
     884    ] (refl …)).
     885#S #st1 #st2 #st3 #st4 #ft #taaf lapply ft cases taaf
     886whd in match ft_extend_taaf; normalize nodelta
     887[ #st #ft #H #G whd in ⊢ (??%?); @pair_elim' normalize nodelta % ]
     888#st2 #st2' #st3 #taa' #H' #G' [2: #K' ] #ft #H #G
     889whd in ⊢ (??%?); >ft_extend_taa_advance_obs normalize nodelta
     890@(pair_elim' … (ft_stack_observables … ft)) normalize nodelta
     891>(status_class_dep_match_rewrite … G') normalize nodelta
     892@status_class_dep_match_elim #prf
     893@status_class_dep_match_elim #prf'
     894try(@⊥ >prf in prf'; #prf' -prf destruct @False)
     895[ >associative_append
     896whd in match ft_stack; whd in match ft_observables; normalize nodelta
     897[2,3: cases (\fst (ft_stack_observables … ft)) normalize nodelta [2,4: #f #stack']]
     898@eq_f >associative_append @eq_f
     899lapply prf lapply prf' lapply G
     900cases taaf -st3 -st2 normalize nodelta
     901[1,4,7,10,13,16,19: #st2 #_ #prf #prf' % ]
     902
     903>(not_costed_no_label … K) try % >append_nil %
     904qed.
     905*)
    769906
    770907(* little helper to avoid splitting equal cases *)
    771908lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
     909
     910lemma enforce_costedness_ok : ∀S,s1,s2.enforce_costedness S s1 s2 →
     911as_classifier S s1 cl_jump → as_costed … s2.
     912#S #s1 #s2 whd in ⊢ (%→%→?); whd in match (is_cl_jump ??); #H #G >G in H; #K @K qed.
     913
     914let rec taa_to_taaf S st1 st2 (taa : trace_any_any S st1 st2) on taa :
     915  trace_any_any_free S st1 st2 ≝
     916match taa return λst1,st2,taa.trace_any_any_free S st1 st2 with
     917[ taa_base s ⇒ taaf_base … s
     918| taa_step s1 s2 s3 ex cl ncost tl ⇒
     919  taaf_cons … ex cl (taa_to_taaf … tl) ?
     920]. @if_else_True assumption qed.
     921
     922definition taa_append_taaf : ∀S,st1,st2,st3.
     923  trace_any_any S st1 st2 → trace_any_any_free S st2 st3 →
     924  trace_any_any_free S st1 st3 ≝
     925λS,st1,st2,st3,taa,taaf.
     926match taaf return λst2,st3,taaf.trace_any_any S st1 st2 → trace_any_any_free S st1 st3 with
     927[ taaf_base s ⇒ taa_to_taaf …
     928| taaf_step s1 s2 s3 taa' ex cl ⇒
     929  λtaa.taaf_step … (taa_append_taa … taa taa') ex cl
     930| taaf_step_jump s1 s2 s3 taa' ex cl K ⇒
     931  λtaa.taaf_step_jump … (taa_append_taa … taa taa') ex cl K
     932] taa.
     933
     934lemma taa_to_taaf_non_empty : ∀S,st1,st2,taa.
     935taaf_non_empty … (taa_to_taaf S st1 st2 taa) = taa_non_empty … taa.
     936#S #st1 #st2 #taa elim taa -st1 -st2
     937[ #s % | #s1 #s2 #s3 #ex #cl #ncost #tl #IH
     938  change with (taaf_cons ????????) in match (taa_to_taaf ????);
     939  >taaf_cons_non_empty %
     940qed.
     941
     942lemma taa_append_taaf_non_empty : ∀S,st1,st2,st3,taa,taaf.
     943taaf_non_empty … (taa_append_taaf S st1 st2 st3 taa taaf) =
     944(taa_non_empty … taa ∨ taaf_non_empty … taaf).
     945#S #st1 #st2 #st3 #taa #taaf lapply taa cases taaf -st2 -st3
     946[ #s #taa whd in match (taa_append_taaf ??????); >taa_to_taaf_non_empty
     947  >commutative_orb %
     948|*: #s1 #s2 #s3 #taa' #ex #cl [2: #K] #taa >commutative_orb %
     949]
     950qed.
     951
     952lemma taa_empty_to_eq : ∀S,st1,st2,taa.
     953¬(bool_to_Prop (taa_non_empty S st1 st2 taa)) → st1 = st2.
     954#S #st1 #st2 * // #s1 #s2 #s3 #ex #cl #K #tl * #ABS cases (ABS ?) % qed.
     955
     956lemma taaf_empty_to_eq : ∀S,st1,st2,taaf.
     957¬(bool_to_Prop (taaf_non_empty S st1 st2 taaf)) → st1 = st2.
     958#S #st1 #st2 * // #s1 #s2 #s3 #pre #ex #cl [2: #K ] * #ABS cases (ABS ?) % qed.
    772959
    773960theorem status_simulation_produce_ft :
     
    793980  ∀S1,S2.
    794981  ∀R.
    795   ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
    796   status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
     982  ∀st1,st1',st2.∀ft1 : flat_trace S1 st1 st1'.
     983  status_simulation S1 S2 R → R st1 st2 → label_rel … st1 st2 →
    797984  ∃st2_lab,st2'.
    798   ∃ft2 : flat_trace S2 st2 st2_lab stack.
     985  ∃ft2 : flat_trace S2 st2 st2_lab.
    799986  ∃taa : trace_any_any S2 st2_lab st2'.
    800   label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
    801 #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
    802 [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
    803 |*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1']
    804   (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    805   [1,2: (* other/jump *)
    806     lapply (sim_execute … ex G')
    807     try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
    808     [ #H lapply (H ncost_st1') -H ] *
    809     #st2' *#taaf ** #ncost #G'' #H''
    810     %{st2'} %{st2'}
    811     %[1,3:
    812       @(ft_extend_taaf … taaf)
    813       @(ft_extend_taa … taa)
    814       assumption]
    815     %{(taa_base …)}
    816     % [1,3: %{H'' G''} ]
    817     whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    818     lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
    819     [1,4: #st2' #H'' #taa * #ncost
    820       >ft_extend_taa_obs <L'
    821       [1,3: >(not_costed_no_label … ncost) >if_eq >S %
    822       |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
    823         [1,3: #st2' #ft2 #S #H'' #L' >append_nil
    824           >not_costed_no_label
    825           [1,3: >append_nil @S ]
    826           whd in ⊢ (?%); >L' <H'' assumption
    827         |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_
    828           >S %
    829         ]
    830       ]
    831     |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa *
    832       whd in ⊢ (???(?????%));
    833       >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
    834       >S >L' %
    835     ]
    836   |3: (* tailcall *)
    837     lapply (sim_execute … ex G')
    838     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    839     * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
    840     * #taa2 * #taa2' ** #ex' #G'' #H''
    841     lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl))
    842     generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%);
    843     <EQcall in ⊢ (%→???%%→%);
    844     #ft1' #EQft1'
    845     %{st2_after_call} %{st2'}
    846     %[@(ft_advance_tailcall … f … ex' cl')
    847       @(ft_extend_taa … (taa_append_taa … taa taa2))
    848       assumption]
    849     %{taa2'}
    850     % [ %{H'' G''} ]
    851     >ft_extend_taa_advance_tailcall_obs
    852     lapply EQft1' lapply ft1' -ft1'
    853     >EQcall in ⊢ (%→???%%→%);
    854     #ft1' #EQft1' destruct (EQft1')
    855     whd in ⊢ (??%?);
    856     >ft_observables_aux_def >append_nil
    857     >S >L' %
    858   |4: (* ret *)
    859     lapply (sim_execute … ex G')
    860     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    861     #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    862     ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
    863     %[@(ft_extend_taaf … taa2')
    864       @(ft_advance_ret … f … ex' cl')
    865       @(ft_extend_taa … (taa_append_taa … taa taa2))
    866       assumption]
    867     %{(taa_base …)}
    868     % [ %{H'' G''} ]
    869     >ft_extend_taaf_obs
    870     >ft_extend_taa_advance_ret_obs
    871     whd in ⊢ (??%?);
    872     >ft_observables_aux_def >append_nil
    873     lapply ncost cases taa2' -st2_after_ret -st2'
    874     [ #st2' * >append_nil
    875     |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost
    876       >(not_costed_no_label … ncost)
    877       >if_eq >append_nil
    878     ]
    879     >S >L' %
    880   |5: (* call *)
    881     lapply (sim_execute … ex G')
    882     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    883     * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
    884     * #taa2 * #taa2' ** #ex' #G'' #H''
    885     %{st2_after_call} %{st2'}
    886     lapply (refl_jmeq … (ft_advance_call … ft1 ex cl))
    887     generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%);
    888     <EQcall in ⊢ (%→???%%→%);
    889     #ft1' #EQft1'
    890     %[@(ft_advance_call … ex' cl')
    891       @(ft_extend_taa … (taa_append_taa … taa taa2))
    892       assumption]
    893     %{taa2'}
    894     % [ %{H'' G''} ]
    895     >ft_extend_taa_advance_call_obs
    896     lapply EQft1' lapply ft1' -ft1'
    897     >EQcall in ⊢ (%→???%%→%);
    898     #ft1' #EQft1' destruct (EQft1')
    899     whd in ⊢ (??%?);
    900     >ft_observables_aux_def >append_nil
    901     >S >L' %
    902   ]
     987  R st1' st2' ∧ label_rel … st1' st2_lab ∧ ft_stack_observables … ft1 = ft_stack_observables … ft2.
     988#S1 #S2 #R #st1 #st1' #st2 #ft1 #sim_execute #H #G elim ft1 -st1'
     989[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % ]
     990#st1_mid #st1' #ft1 #ex #ncost_st1'
     991(* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #G' #L' #S
     992inversion (as_classify … st1_mid) #cl
     993[2,5: (* other/jump *)
     994  lapply (sim_execute … ex G')
     995  try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
     996  [ #H lapply (H (enforce_costedness_ok ??? ncost_st1' (jmeq_to_eq … cl))) -H ] *
     997  #st2' *#taaf ** #ncost #H'' #G''
     998  %{st2'} %{st2'}
     999  %[1,3:
     1000    @(ft_extend_taaf … (taa_append_taaf … taa taaf))
     1001    assumption]
     1002  %{(taa_base …)}
     1003  % [1,3: %{H'' G''} ]
     1004  >ft_extend_taaf_obs >taa_append_taaf_non_empty
     1005  whd in match ft_observables; whd in match ft_stack; normalize nodelta
     1006  <S whd in ⊢ (??%?); @pair_elim' normalize nodelta
     1007  >(status_class_dep_match_rewrite … cl) normalize nodelta @eq_f @eq_f
     1008  cases (true_or_false_Prop taa) #Htaa >Htaa
     1009  [2,4: lapply (taa_empty_to_eq … Htaa) #EQ destruct
     1010    cases (true_or_false_Prop (taaf_non_empty … taaf)) #Htaaf
     1011    >Htaaf in ncost ⊢ %;
     1012    [1,3: #_ |*: * #ncost lapply (taaf_empty_to_eq … Htaaf) #EQ destruct ]
     1013  ]
     1014  normalize nodelta in ncost ⊢ %; // >not_costed_no_label //
     1015  whd in ⊢ (?%); >L' <G'' assumption
     1016|4: (* tailcall *)
     1017  lapply (sim_execute … ex G')
     1018  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
     1019  * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
     1020  * #taa2 * #taa2' ** #ex' #H'' #G''
     1021  %{st2_after_call} %{st2'}
     1022  %[@(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
     1023    @(ft_extend_taa … (taa_append_taa … taa taa2))
     1024    assumption]
     1025  %{taa2'}
     1026  % [ %{H'' G''} ]
     1027  >ft_extend_taa_advance_obs
     1028  whd in ⊢ (??%?); @pair_elim' @pair_elim'
     1029  >(status_class_dep_match_rewrite … cl)
     1030  >(status_class_dep_match_rewrite … cl') normalize nodelta
     1031  >S <EQcall >L' %
     1032|1: (* ret *)
     1033  lapply (sim_execute … ex G')
     1034  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
     1035  #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
     1036  ***** #ncost #cl' #ex' #H'' #_ #G'' %{st2'} %{st2'}
     1037  %[@(ft_extend_taaf … taa2')
     1038    @(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
     1039    @(ft_extend_taa … (taa_append_taa … taa taa2))
     1040    assumption]
     1041  %{(taa_base …)}
     1042  % [ %{H'' G''} ]
     1043  >ft_extend_taaf_obs whd in match ft_observables; whd in match ft_stack; normalize nodelta
     1044  >ft_extend_taa_advance_obs
     1045  whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
     1046  >(status_class_dep_match_rewrite … cl)
     1047  >(status_class_dep_match_rewrite … cl') normalize nodelta
     1048  >S cases (\fst (ft_stack_observables … ft2)) [2: #f #stack']
     1049  normalize nodelta @eq_f >L' >associative_append @eq_f
     1050  cases (true_or_false_Prop (taaf_non_empty … taa2')) #H
     1051  >H in ncost ⊢ %; normalize nodelta [1,3: #ncost |*: lapply (taaf_empty_to_eq … H) #EQ destruct #_ ]
     1052  // >(not_costed_no_label … st2_after_ret) // >append_nil %
     1053|3: (* call *)
     1054  lapply (sim_execute … ex G')
     1055  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
     1056  * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
     1057  * #taa2 * #taa2' ** #ex' #H'' #G''
     1058  %{st2_after_call} %{st2'}
     1059  %[@(ft_advance … ex' ?) [2: @hide_prf  normalize >cl' % ]
     1060    @(ft_extend_taa … (taa_append_taa … taa taa2))
     1061    assumption]
     1062  %{taa2'}
     1063  % [ %{H'' G''} ]
     1064  >ft_extend_taa_advance_obs @pair_elim' >(status_class_dep_match_rewrite … cl') normalize nodelta
     1065  whd in ⊢ (??%?); @pair_elim' >(status_class_dep_match_rewrite … cl) normalize nodelta
     1066  >S <EQcall >L' %
    9031067]
    9041068qed.
     1069
     1070theorem status_simulation_produce_ft_and_tlr :
     1071∀S1,S2.
     1072∀R.
     1073∀st1,st1',st1'',st2.
     1074∀ft1 : flat_trace S1 st1 st1'.
     1075∀tlr1 : trace_label_return S1 st1' st1''.
     1076status_simulation_with_init S1 S2 R st1 st2 →
     1077∃st2',st2'',st2'''.
     1078∃ft2 : flat_trace S2 st2 st2'.
     1079∃tlr2 : trace_label_return S2 st2' st2''.
     1080∃taaf : trace_any_any_free S2 st2'' st2'''.
     1081(∀x.as_result … st1'' = Some ? x → as_result … st2''' = Some ? x) ∧
     1082ft_observables … ft1 = ft_observables … ft2 ∧
     1083tlr_rel … tlr1 tlr2.
     1084#S1 #S2 #R #st1 #st1' #st1'' #st2 #ft1 #tlr1 * #S #L #simul
     1085cases (status_simulation_produce_ft … ft1 simul S L)
     1086#st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ1
     1087cases (status_simulation_produce_tlr … tlr1 taa2 simul S' L')
     1088#st2'' * #st2''' * #tlr2 * #taa2' **** #_ #S'' #_ #_ #EQ2
     1089%{st2'} %{st2''} %{st2'''} %{ft2} %{tlr2} %{taa2'} %{EQ2} %
     1090[ #res #EQ @(sim_final … simul … EQ S'')
     1091| whd in ⊢ (??%%); @eq_f assumption
     1092]
     1093qed.
  • 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.