include "common/Events.ma".
include "common/Mem.ma".
include "common/IO.ma".
include "common/Globalenvs.ma".
include "common/SmallstepExec.ma".

include "Cminor/syntax.ma".
include alias "basics/logic.ma".

definition env ≝ identifier_map SymbolTag val.
definition genv ≝ (genv_t Genv) (fundef internal_function).

definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
  stmt_P (λs.stmt_vars (λid,ty. present ?? en id) s ∧
             stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s.

lemma stmt_inv_update : ∀f,en,s,l,v.
  stmt_inv f en s →
  ∀H:present ?? en l.
  stmt_inv f (update_present ?? en l H v) s.
#f #en #s #l #v #Inv #H
@(stmt_P_mp … Inv)
#s * #H1 #H2 %
[ @(stmt_vars_mp … H1)
  #l #ty #H @update_still_present @H
| @H2
] qed.

(* continuations within a function. *)
inductive cont : Type[0] ≝
| Kend : cont
| Kseq : stmt → cont → cont
| Kblock : cont → cont.

let rec cont_inv (f:internal_function) (en:env) (k:cont) on k : Prop ≝
match k with
[ Kend ⇒ True
| Kseq s k' ⇒ stmt_inv f en s ∧ cont_inv f en k'
| Kblock k' ⇒ cont_inv f en k'
].

lemma cont_inv_update : ∀f,en,k,l,v.
  cont_inv f en k →
  ∀H:present ?? en l.
  cont_inv f (update_present ?? en l H v) k.
#f #en #k elim k /2/
#s #k #IH #l #v #Inv #H whd %
[ @stmt_inv_update @(π1 Inv)
| @IH @(π2 Inv)
] qed.

(* a stack of function calls *)
inductive stack : Type[0] ≝
| SStop : stack
| Scall : ∀dest:option (ident×typ). ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty)] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.

inductive state : Type[0] ≝
| State:
    ∀    f: internal_function.
    ∀    s: stmt.
    ∀   en: env.
    ∀ fInv: stmt_inv f en (f_body f).
    ∀  Inv: stmt_inv f en s.
    ∀    m: mem.
    ∀   sp: block.
    ∀    k: cont.
    ∀ kInv: cont_inv f en k.
    ∀   st: stack.
            state
| Callstate:
    ∀   fd: fundef internal_function.
    ∀ args: list val.
    ∀    m: mem.
    ∀   st: stack.
            state
| Returnstate:
    ∀    v: option val.
    ∀    m: mem.
    ∀   st: stack.
            state.

definition mem_of_state : state → mem ≝
λst. match st with
[ State _ _ _ _ _ m _ _ _ _ ⇒ m
| Callstate _ _ m _ ⇒ m
| Returnstate _ m _ ⇒ m
].

axiom UnknownLocal : String.
axiom FailedConstant : String.
axiom FailedOp : String.
axiom FailedLoad : String.

let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (λid,ty. present ?? en id)) (sp:block) (m:mem) on e : res (trace × val) ≝
match e return λt,e.expr_vars t e (λid,ty. present ?? en id) → res (trace × val) with
[ Id _ i ⇒ λEnv.
    let r ≝ lookup_present ?? en i ? in
    OK ? 〈E0, r〉
| Cst _ c ⇒ λEnv.
    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    OK ? 〈E0, r〉
| Op1 ty ty' op e' ⇒ λEnv.
    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    do r ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
    OK ? 〈tr, r〉
| Op2 ty1 ty2 ty' op e1 e2 ⇒ λEnv.
    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    OK ? 〈tr1 ⧺ tr2, r〉
| Mem rg ty chunk e ⇒ λEnv.
    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    OK ? 〈tr, r〉
| Cond sz sg ty e' e1 e2 ⇒ λEnv.
    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    do b ← eval_bool_of_val v;
    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en ? sp m;
    OK ? 〈tr ⧺ tr', r〉
| Ecost ty l e' ⇒ λEnv.
    do 〈tr,r〉 ← eval_expr ge ty e' en ? sp m;
    OK ? 〈Echarge l ⧺ tr, r〉
] Env.
try @Env
try @(π1 Env)
try @(π2 Env)
try @(π1 (π1 Env))
cases b
try @(π2 (π1 Env))
try @(π2 Env)
qed.

axiom BadState : String.

let rec k_exit (n:nat) (k:cont) f en (kInv:cont_inv f en k) on k : res (Σk':cont. cont_inv f en k') ≝
match k return λk.cont_inv f en k → ? with
[ Kend ⇒ λ_. Error ? (msg BadState)
| Kseq _ k' ⇒ λkInv. k_exit n k' f en ?
| Kblock k' ⇒ λkInv. match n with [ O ⇒ OK ? «k',?» | S m ⇒ k_exit m k' f en ? ]
] kInv.
[ @(π2 kInv) | @kInv | @kInv ]
qed.

let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
match cs with
[ nil ⇒ default
| cons h t ⇒
    let 〈hi,a〉 ≝ h in
    if eq_bv ? i hi then a else find_case A sz i t default
].

let rec find_label (l:identifier Label) (s:stmt) (k:cont) f en (Inv:stmt_inv f en s) (kInv:cont_inv f en k) on s : option (Σsk:(stmt × cont). stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk)) ≝
match s return λs. stmt_inv f en s → ? with
[ St_seq s1 s2 ⇒ λInv.
    match find_label l s1 (Kseq s2 k) f en ?? with
    [ None ⇒ find_label l s2 k f en ??
    | Some sk ⇒ Some ? sk
    ]
| St_ifthenelse _ _ _ s1 s2 ⇒ λInv.
    match find_label l s1 k f en ?? with
    [ None ⇒ find_label l s2 k f en ??
    | Some sk ⇒ Some ? sk
    ]
| St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??
| St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??
| St_label l' s' ⇒ λInv.
    match identifier_eq ? l l' with
    [ inl _ ⇒ Some ? 〈s',k〉
    | inr _ ⇒ find_label l s' k f en ??
    ]
| St_cost _ s' ⇒ λInv. find_label l s' k f en ??
| _ ⇒ λ_. None ?
] Inv.
//
try @(π2 Inv)
try @(π2 (π1 Inv))
[ % [ @(π2 Inv) | @kInv ]
| % [ @Inv | @kInv ]
| % [ @(π2 Inv) | @kInv ]
] qed. 

lemma find_label_none : ∀l,s,k,f,en,Inv,kInv.
  find_label l s k f en Inv kInv = None ? →
  ¬Exists ? (λl'.l' = l) (labels_of s).
#l #s elim s
try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) ) 
[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
  lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
  cases (find_label l s1 (Kseq s2 k) f en ??)
  [ #H1 whd in ⊢ (??%? → ?);
    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
    [ #H2 #_ % #H cases (Exists_append … H)
      [ #H' cases (H1 (refl ??)) /2/
      | #H' cases (H2 (refl ??)) /2/
      ]
    | #sk #_ #E destruct
    ]
  | #sk #_ #E whd in E:(??%?); destruct
  ]
| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
  lapply (IH1 k f en (π2 (π1 Inv)) kInv)
  cases (find_label l s1 k f en ??)
  [ #H1 whd in ⊢ (??%? → ?);
    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
    [ #H2 #_ % #H cases (Exists_append … H)
      [ #H' cases (H1 (refl ??)) /2/
      | #H' cases (H2 (refl ??)) /2/
      ]
    | #sk #_ #E destruct
    ]
  | #sk #_ #E whd in E:(??%?); destruct
  ]
| #s1 #IH #k #f #en #Inv #kInv @IH
| #s1 #IH #k #f #en #Inv #kInv @IH
| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
| whd in i:(??%?); cases (identifier_eq Label l a) in i;
  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
| #cl #s1 #IH #k #f #en #Inv #kInv @IH
] qed.

definition find_label_always : ∀l,s,k. Exists ? (λl'.l' = l) (labels_of s) → 
  ∀f,en. stmt_inv f en s → cont_inv f en k →
  Σsk:stmt × cont. stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk) ≝
λl,s,k,H,f,en,Inv,kInv.
  match find_label l s k f en Inv kInv return λx.find_label l s k f en Inv kInv = x → ? with
  [ Some sk ⇒ λ_. sk
  | None ⇒ λE. ⊥
  ] (refl ? (find_label l s k f en Inv kInv)).
cases (find_label_none … E)
#H1 @(H1 H)
qed.

axiom WrongNumberOfParameters : String.

(* TODO: perhaps should do a little type checking? *)
let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝
match vs with
[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
| cons v vt ⇒
    match ids return λids.res (Σen. All ?? ids) with
    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    | cons idh idt ⇒
        let 〈id,ty〉 ≝ idh in
        do en ← bind_params vt idt;
        OK ? «add ?? en (\fst idh) v, ?»
    ]
].
[ @I
| % [ whd >lookup_add_hit % #E destruct
    | @(All_mp … (pi2 ?? en)) #a #H whd @lookup_add_oblivious @H
    ]
] qed.

(* TODO: perhaps should do a little type checking? *)
definition init_locals : env → list (ident×typ) → env ≝
foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).

lemma init_locals_preserves : ∀en,vars,l.
  present ?? en l →
  present ?? (init_locals en vars) l.
#en #vars elim vars
[ #l #H @H
| #idt #tl #IH #l #H whd
  @lookup_add_oblivious @IH @H
] qed.

lemma init_locals_env : ∀en,vars.
  All ? (λidt. present ?? (init_locals en vars) (\fst idt)) vars.
#en #vars elim vars
[ @I
| #idt #tl #IH %
  [ whd >lookup_add_hit % #E destruct
  | @(All_mp … IH) #a #H @lookup_add_oblivious @H
  ]
] qed.

let rec trace_map_inv (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → res (trace × B))
                  (l:list A) (p:All A P l) on l : res (trace × (list B)) ≝
match l return λl. All A P l → ? with
[ nil ⇒ λ_. OK ? 〈E0, [ ]〉
| cons h t ⇒ λp.
    do 〈tr,h'〉 ← f h ?;
    do 〈tr',t'〉 ← trace_map_inv … f t ?;
    OK ? 〈tr ⧺ tr',h'::t'〉
] p.
[ @(π1 p) | @(π2 p) ] qed.

axiom FailedStore : String.
axiom BadFunctionValue : String.
axiom BadSwitchValue : String.
axiom UnknownLabel : String.
axiom ReturnMismatch : String.

definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
λge,st.
match st return λ_. IO ??? with
[ State f s en fInv Inv m sp k kInv st ⇒ err_to_io ??? (
    match s return λs. stmt_inv f en s → res (trace × state) with
    [ St_skip ⇒ λInv.
        match k return λk. cont_inv f en k → res ? with
        [ Kseq s' k' ⇒ λkInv. return 〈E0, State f s' en fInv ? m sp k' ? st〉
        | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
          (* cminor allows functions without an explicit return statement *)
        | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
        ] kInv
    | St_assign _ id e ⇒ λInv.
        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
        let en' ≝ update_present ?? en id ? v in
        return 〈tr, State f St_skip en' ? ? m sp k ? st〉
    | St_store _ _ chunk edst e ⇒ λInv.
        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
        return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉

    | St_call dst ef args ⇒ λInv.
        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
    | St_tailcall ef args ⇒ λInv.
        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
        return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
        
    | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
        ! b ← eval_bool_of_val v;
        return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
    | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
    | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
    | St_exit n ⇒ λInv.
        ! k' ← k_exit n k ?? kInv;
        return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    | St_switch sz _ e cs default ⇒ λInv.
        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
        match v with
        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
            ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
            return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
            (Error ? (msg BadSwitchValue))
        | _ ⇒ Error ? (msg BadSwitchValue)
        ]
    | St_return eo ⇒
        match eo return λeo. stmt_inv f en (St_return eo) → ? with
        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
        | Some e ⇒
            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
              return 〈tr, Returnstate (Some ? v) (free m sp) st〉
            ]
        ]
    | St_label l s' ⇒ λInv. return 〈E0, State f s' en fInv ? m sp k ? st〉
    | St_goto l ⇒ λInv.
        match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒
          return 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
        ]
    | St_cost l s' ⇒ λInv.
        return 〈Echarge l, State f s' en fInv ? m sp k ? st〉
    ] Inv)
| Callstate fd args m st ⇒
    match fd with
    [ Internal f ⇒ err_to_io ?? (trace × state) (
        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
        ! en ← bind_params args (f_params f);
        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
    | External fn ⇒
        ! evargs ← err_to_io ??? (check_eventval_list args (sig_args (ef_sig fn)));
        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
    ]
| Returnstate result m st ⇒ err_to_io ??? (
    match st with
    [ Scall dst f sp en dstP fInv k Inv st' ⇒
        match result with
        [ None ⇒ match dst with
                 [ None ⇒ return 〈E0, State f St_skip en ? ? m sp k ? st'〉
                 | Some _ ⇒ Error ? (msg ReturnMismatch)]
        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty) ] → res (trace × state) with
                   [ None ⇒ λ_. Error ? (msg ReturnMismatch)
                   | Some idty ⇒ λdstP. return 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
                   ] dstP
        ]
    | _ ⇒ Error ? (msg BadState)
    ])
].
try @(π1 kInv)
try @(π2 kInv)
try @(conj ?? I I)
try @kInv
try @(π2 (π1 Inv))
try @kInv
try @(π1 (π1 Inv))
try (@cont_inv_update @kInv)
try @(π2 (π1 (π1 Inv)))
try @(π1 (π1 (π1 Inv)))
try @(π1 Inv)
try @(π2 Inv)
[ @fInv
| @(π2 Inv')
| @(π1 Inv')
| @(pi2 … k')
| @(pi2 … k')
| % [ @Inv | @kInv ]
| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
| % [ @(π2 Inv) | @kInv ]
| @stmt_inv_update @fInv
| 10,11:
  @(stmt_P_mp … (f_inv f))
  #s * #V #L %
  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
      * #id' #ty * #E1 destruct #H @H
    | *: #H cases (Exists_All … H (init_locals_env … en …))
      * #id' #ty * #E1 destruct #H @H
    ]
  | 2,4: @L
  ]
| @I
| @cont_inv_update @Inv
| @stmt_inv_update @fInv
| @Inv
| @fInv
] qed.

definition is_final : state → option int ≝
λs. match s with
[ Returnstate res m st ⇒
    match st with
    [ SStop ⇒
        match res with
        [ None ⇒ None ?
        | Some v ⇒
            match v with
            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
            | _ ⇒ None ?
            ]
        ]
    | _ ⇒ None ?
    ]
| _ ⇒ None ?
].

definition Cminor_exec : trans_system io_out io_in ≝
  mk_trans_system … ? (λ_.is_final) eval_step.

axiom MainMissing : String.

definition make_global : Cminor_program → genv ≝
λp. globalenv Genv ?? (λx.x) p.

definition make_initial_state : Cminor_program → res state ≝
λp.
  let ge ≝ make_global p in
  do m ← init_mem Genv ?? (λx.x) p;
  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
  OK ? (Callstate f (nil ?) m SStop).

definition Cminor_fullexec : fullexec io_out io_in ≝
  mk_fullexec … Cminor_exec make_global make_initial_state.

definition make_noinit_global : Cminor_noinit_program → genv ≝
λp. globalenv Genv ?? (λx.[Init_space x]) p.

definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
λp.
  let ge ≝ make_noinit_global p in
  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
  OK ? (Callstate f (nil ?) m SStop).

definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
  mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state.