(* Show that measurable subtraces are preserved in the front-end. *)

include "common/Measurable.ma".

definition normal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝
λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

(* A record giving the languages and simulation results necessary to show that
   measurability is preserved. *)

record meas_sim : Type[2] ≝ {
  ms_C1 : preclassified_system;
  ms_C2 : preclassified_system;
  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
  ms_inv : ? → ? → Type[0];
  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
  sim_normal :
    ∀g1,g2.
    ∀INV:ms_inv g1 g2.
    ∀s1,s1',s2,tr.
    ms_rel g1 g2 INV s1 s1' →
    normal_state ms_C1 g1 s1 →
    ¬ pcs_labelled ms_C1 g1 s1 →
    ∃n. after_n_steps (S n) … (pcs_exec ms_C1) g1 s1 (λs.normal_state ms_C1 g1 s ∧ ¬ pcs_labelled ms_C1 g1 s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
      tr = tr' ∧
      ms_rel g1 g2 INV s2 s2'
    );
  sim_call_return :
    ∀g1,g2.
    ∀INV:ms_inv g1 g2.
    ∀s1,s1',s2,tr.
    ms_rel g1 g2 INV s1 s1' →
    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
    ¬ pcs_labelled ms_C1 g1 s1 →
    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
      tr = tr' ∧
      ms_rel g1 g2 INV s2 s2'
    );
  sim_cost :
    ∀g1,g2.
    ∀INV:ms_inv g1 g2.
    ∀s1,s1',s2,tr.
    ms_rel g1 g2 INV s1 s1' →
    pcs_labelled ms_C1 g1 s1 →
    after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
      tr = tr' ∧
      ms_rel g1 g2 INV s2 s2'
    );
  sim_init :
    ∀p1,p2,s,s'.
    ms_compiled p1 p2 →
    make_initial_state ?? ms_C1 p1 = OK ? s →
    make_initial_state ?? ms_C2 p2 = OK ? s' →
    ∃INV. ms_rel ?? INV s s'
}.

(* TODO: obs eq *)

definition trace_starts : ∀S. execution S io_out io_in → S → Prop ≝
λS,t,s. match t with [ e_step _ s' _ ⇒ s = s' | _ ⇒ False ].

(* TODO: too many of these lemmas, slim it down*)

lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 →
  ∃a'. a = 〈tr,s〉::a' ∧
  ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨
  (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)).
#fx #g #tr #s #n #a #b
>exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?);
cases (is_final … s)
[ whd in ⊢ (??%? → ?); cases (split_trace ?????)
  [ #E whd in E:(??%%); destruct
  | * #a' #b' #E whd in E:(??%%); destruct
    %{a'} %{(refl ??)} %1 %{(refl ??)} %
  ]
| #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct
  %{[ ]} %{(refl ??)} %2 %{r} /4/
] qed.

lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b.
  split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 →
  ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧
  ∃a'. a = 〈tr,s'〉::a' ∧
  ((is_final … fx g s' = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s')) n = Some ? 〈a',b〉) ∨
  (∃r. is_final … fx g s' = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s')).
#fx #g #s #n #a #b
cases (step … fx g s)
[ #o #i whd in ⊢ (??%? → ?); #E destruct
| * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split
| #err #E whd in E:(??%%); destruct
] qed.

lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b.
  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 →
  a = [〈tr,s〉] ∧
  ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨
  (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)).
#fx #g #tr #s #a #b #split
cases (split_trace_S … split)
#a' * #E1 *
[ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)}
  %1 %{notfinal} %
| * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)}
  %2 %{r} %{final} %
] qed.
  

lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 →
  ∃a'. a = 〈tr,s〉::a' ∧
  is_final … fx g s = None ? ∧
  ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧
  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉.
#fx #g #tr #s #n #a #b #splitSS
cases (split_trace_S … splitSS)
#a' * #E1 *
[ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ]
  cases (step … s) in splitS ⊢ %;
  [ #o #i #E whd in E:(??%%); destruct
  | * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS
  | #m  #E whd in E:(??%%); destruct
  ]
| * #r * * * #final #En #Ea #Eb destruct
] qed.

(* WIP commented out
lemma prefix_preserved :
  ∀MS:meas_sim.
  ∀g1,g2.
  ∀INV:ms_inv MS g1 g2.
  ∀max_allowed_stack.
  ∀s1,s1',tr,tr'.
  ms_rel MS g1 g2 INV s1 s1' →
  
  let trace ≝ (exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr,s1〉)) in
  let trace' ≝ (exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr',s1'〉)) in
  
  ∀m,prefix,suffix.
  split_trace … trace m = Some ? 〈prefix,suffix〉 →
  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →

  ∃m',prefix',suffix'.
    split_trace … trace' m' = Some ? 〈prefix',suffix'〉 ∧
    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
  
  ∃s2,s2',tr2,tr2'.
    suffix = exec_inf_aux ?? (pcs_exec …  (ms_C1 MS)) g1 (Value … 〈tr2,s2〉) ∧
    suffix' = exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr2',s2'〉) ∧
    ms_rel MS g1 g2 INV s2 s2'.
* #C1 #C2 #compiled #inv #stack #rel #sim_normal #sim_call_return #sim_cost #sim_init
#g1 #g2 #INV #max #s1 #s1' #tr #tr' #REL
letin trace ≝ (exec_inf_aux ?????)
letin trace' ≝ (exec_inf_aux ?????)
#m0
@(nat_elim1 m0)
*
[ #_ #prefix #suffix #split whd in split:(??%?); destruct
  #max_ok %{0} %{[]} %{trace'}
  % [ % // | %{s1} %{s1'} %{tr} %{tr'} /3/ ]
| *
  [ (* m = 1; just extracts the current state *)
    #_ #prefix #suffix #split #max_ok
    cases (split_trace_1 … split) #E1 #foo
    %{1} %{[〈tr',s1'〉]} %{(exec_inf_aux … (step … s1'))}
    % [ %
 #m #IH #prefix #suffix #split #max_ok
  (* clean up first step? *)
  cases (true_or_false_Prop … (pcs_labelled … s1))
  [ #CS cases (split_trace_S … split) #trace1 * #Etrace *
    [ * #notfinal #split1
    lapply (sim_cost … REL CS)
    [ 3: whd in match (after_n_steps ????? s1 ??);
      >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?);
lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?);
[
| #CL

theorem measured_subtrace_preserved :
  ∀MS:meas_sim.
  ∀p1,p2,m,n,stack_cost,max.
  ms_compiled MS p1 p2 →
  measurable (ms_C1 MS) p1 m n stack_cost max →
  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
* #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init
#p1 #p2 #m #n #stack_cost #max #compiled
whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?)
* #prefix * #suffix * #subtrace * #remainder
* * * * #split1 #split2 #subtrace_ok #terminates #max_ok

*)