include "utilities/extralib.ma".
include "common/IOMonad.ma".
include "common/Integers.ma".
include "common/Events.ma".

record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
{ global : Type[1]
; state  : global → Type[0]
; is_final : ∀g. state g → option int
; step : ∀g. state g → IO outty inty (trace×(state g))
}.

let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
               (g:global ?? exec) (s:state ?? exec g)
 : IO outty inty (trace × (state ?? exec g)) ≝
match n with
[ O ⇒ Value ??? 〈E0, s〉
| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
         ! 〈tn,sn〉 ← repeat n' ?? exec g s1;
         Value ??? 〈t1⧺tn,sn〉
].

(* We take care here to check that we're not at the final state.  It is not
   necessarily the case that a success step guarantees this (e.g., because
   there may be no way to stop a processor, so an infinite loop is used
   instead). *)
inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
| plus_one : ∀s1,tr,s2.
    is_final … TS ge s1 = None ? →
    step … TS ge s1 = OK … 〈tr,s2〉 →
    plus … ge s1 tr s2
| plus_succ : ∀s1,tr,s2,tr',s3.
    is_final … TS ge s1 = None ? →
    step … TS ge s1 = OK … 〈tr,s2〉 →
    plus … ge s2 tr' s3 →
    plus … ge s1 (tr⧺tr') s3.

lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
  plus O I FE gl s tr s' →
  is_final … FE gl s = None ?.
#O #I #FE #gl #s0 #tr0 #s0' * //
qed.

let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
                  (l:list A) on l : res (trace × (list B)) ≝
match l with
[ nil ⇒ OK ? 〈E0, [ ]〉
| cons h t ⇒
    do 〈tr,h'〉 ← f h;
    do 〈tr',t'〉 ← trace_map … f t;
    OK ? 〈tr ⧺ tr',h'::t'〉
].

(* A third version of making several steps (!)

   The idea here is to have a computational definition of reducing serveral
   steps then showing some property about the resulting trace and state.  By
   careful use of let rec we can ensure that reduction stops in a sensible
   way whenever the number of steps or the step currently being executed is
   not (reducible to) a value.

   For example, we state a property to prove by something like

     ∃n. after_n_steps n … clight_exec ge s (λtr,s'. <some property>)

   then start reducing by giving the number of steps and reducing the
   definition

     %{3} whd

   and then whenever the reduction gets stuck, the currently reducing step is
   the third subterm, which we can reduce and unblock with (for example)
   rewriting

     whd in ⊢ (??%?); >EXe'

   and at the end reduce with whd to get the property as the goal.

   There's an inversion-like result to get back the information contained in
   the proof in Executions.ma.

  *)

record await_value_stuff : Type[2] ≝ {
 avs_O : Type[0];
 avs_I : avs_O → Type[0];
 avs_exec : trans_system avs_O avs_I;
 avs_g : global ?? avs_exec
}.

let rec await_value (avs:await_value_stuff)
 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
match v with
[ Value ts ⇒ P (\fst ts) (\snd ts)
| _ ⇒ False
].

let rec after_aux (avs:await_value_stuff)
  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
on n : Prop ≝
match n with
[ O ⇒ P tr s
| S n' ⇒
  match is_final … s with
  [ None ⇒ 
    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
      after_aux avs n' s (tr ⧺ tr') P)
  | _ ⇒ False
  ]
].

definition after_n_steps : nat →
 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
 state ?? exec g →
 (trace → state ?? exec g → Prop) → Prop ≝
λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P.

lemma after_n_covariant : ∀n,O,I,exec,g,P,Q.
  (∀tr,s. P tr s → Q tr s) →
  ∀s.
  after_n_steps n O I exec g s P →
  after_n_steps n O I exec g s Q.
#n #O #I #exec #g #P #Q #H whd in ⊢ (? → % → %); generalize in match E0; elim n
[ normalize /2/
| #n' #IH #tr #s
  normalize cases (is_final … s) normalize [ 2: #_ * ] cases (step O I exec g s) normalize /4/
] qed.

(* for joining a couple of these together *)

lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'.
  after_n_steps m O I exec g s' Q →
  after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
  after_n_steps (n+m) O I exec g s P.
#n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
  generalize in match s; -s
  elim m
  [ #s #tr' whd in ⊢ (% → %); @H2
  | #m' #IH #s #tr' whd in ⊢ (% → %);
    cases (is_final … s) [2: #r * ]
    whd in ⊢ (% → %);
    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ]
| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
  cases (is_final … s) [2: #r * ]
  whd in ⊢ (% → %);
  cases (step O I exec g s) [1,3: normalize // ]
  * #tr1 #s1 whd in ⊢ (% → %); @IH @H
] qed.


(* A (possibly non-terminating) execution.   *)
coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
| e_stop : trace → int → state → execution state output input
| e_step : trace → state → execution state output input → execution state output input
| e_wrong : errmsg → execution state output input
| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.

(* This definition is slightly awkward because of the need to provide resumptions.
   It records the last trace/state passed in, then recursively processes the next
   state. *)

let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
                       (exec:trans_system output input) (g:global ?? exec)
                       (s:IO output input (trace×(state ?? exec g)))
                       : execution ??? ≝
match s with
[ Wrong m ⇒ e_wrong ??? m
| Value v ⇒ let 〈t,s'〉 ≝ v in 
    match is_final ?? exec g s' with
    [ Some r ⇒ e_stop ??? t r s'
    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
].

lemma execution_cases: ∀o,i,s.∀e:execution s o i.
 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
 | e_step tr s e ⇒ e_step ??? tr s e
 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
  here, used reflexivity instead *)

axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
match s with
[ Wrong m ⇒ e_wrong ??? m
| Value v ⇒ let 〈t,s'〉 ≝ v in
    match is_final ?? exec g s' with
    [ Some r ⇒ e_stop ??? t r s'
    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
].
(*
#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
[ #o #k
| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
| ] 
whd in ⊢ (??%%); //;
qed.
*)

lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
  step … ge s = Value … 〈tr, s'〉 ∧
  is_final … s' = Some ? r.
#O #I #TS #ge #s #s' #tr #r
>exec_inf_aux_unfold
cases (step … ge s)
[ 1,3: normalize #H1 #H2 try #H3 destruct
| * #tr' #s''
  whd in ⊢ (??%? → ?);
  lapply (refl ? (is_final … s''))
  cases (is_final … s'') in ⊢ (???% → %);
  [ #_ whd in ⊢ (??%? → ?); #E destruct
  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
  ]
] qed.

lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
#O #I #TS #ge #s #s' #tr #e
>exec_inf_aux_unfold
cases (step … s)
[ 1,3: normalize #H1 #H2 try #H3 destruct
| * #tr' #s''
  whd in ⊢ (??%? → ?);
  cases (is_final … s'')
  [ #E normalize in E; destruct /2/
  | #r #E normalize in E; destruct
  ]
] qed.

lemma extract_interact : ∀O,I,TS,ge,s,o,k.
  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
cases (step … s)
[ #o' #k' normalize #E destruct %{k'} /2/
| * #x #y normalize cases (is_final ?????) normalize
  #X try #Y destruct
| normalize #m #E destruct
] qed.

lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
  is_final … s' = None ?.
#O #I #TS #ge #s #s' #tr #e
>exec_inf_aux_unfold
cases (step … s)
[ 1,3: normalize #H1 #H2 try #H3 destruct
| * #tr' #s''
  whd in ⊢ (??%? → ?);
  lapply (refl ? (is_final … s''))
  cases (is_final … s'') in ⊢ (???% → %);
  [ #F whd in ⊢ (??%? → ?); #E destruct @F
  | #r' #_ #E whd in E:(??%?);  destruct
  ]
] qed.



record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
{ program : Type[0]
; es1 :> trans_system outty inty
; make_global : program → global ?? es1
; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
}.

definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
λo,i,fx,p.
  match make_initial_state ?? fx p with 
  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
  | Error m ⇒ e_wrong ??? m
  ].