include "RTLabs/RTLabs_semantics.ma".

(* Avoid aliasing in interstage proofs *)

definition RTLabs_state ≝ state.
definition RTLabs_genv ≝ genv.

(* Build a full abstract status record that can be used with structured traces. *)

include "common/StructuredTraces.ma".
include "RTLabs/CostSpec.ma". (* TODO: relocate definitions? *)
include "utilities/deqsets_extra.ma".
discriminator status_class.

(* We augment states with a stack of function blocks (i.e. pointers) so that we
   can make sensible "program counters" for the abstract state definition, along
   with a proof that we will get the correct code when we do the lookup (which
   is done to find cost labels given a pc).
   
   Adding them to the semantics is an alternative, more direct approach.
   However, it makes animating the semantics extremely difficult, because it
   is hard to avoid normalising and displaying irrelevant parts of the global
   environment and proofs.
   
   We use blocks rather than identifiers because the global environments go

     identifier → block → definition
   
   and we'd have to introduce backwards lookups to find identifiers for
   function pointers.
 *)

definition Ras_Fn_Match ≝
λge,state,fn_stack.
  match state with
  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
  | Callstate fid fd _ _ fs _ ⇒
      match fn_stack with
      [ nil ⇒ False
      | cons h t ⇒
          find_symbol … ge fid = Some ? h ∧
          find_funct_ptr ? ge h = Some ? fd ∧
          All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
      ]
  | Returnstate _ _ fs _ ⇒ 
      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
  | Finalstate _ ⇒ fn_stack = [ ]
  ].

record RTLabs_ext_state (ge:genv) : Type[0] ≝ {
  Ras_state :> state;
  Ras_fn_stack : list block;
  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
}.

(* Given a plain step of the RTLabs semantics, give the next state along with
   the shadow stack of function block numbers.  Carefully defined so that the
   coercion back to the plain state always reduces. *)
definition next_state : ∀ge. ∀s:RTLabs_ext_state ge. ∀s':state. ∀t.
  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_ext_state ge ≝
λge,s,s',t,EX. mk_RTLabs_ext_state ge s' 
 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
 ?.
cases s' in EX ⊢ %;
[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    whd cases stk in mtc ⊢ %; [ * ]
    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
    | @M2 ]
  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    whd cases stk in mtc ⊢ %; [ * ]
    #hd #tl * * /3/
  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
  ]
| -s' #fid #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
  | #ge' #vf1 #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
  ]
| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H 
  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
  ]
| #r #EX whd @refl
] qed.


(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
       will be added later (LTL → LIN). *)

definition RTLabs_classify : state → status_class ≝
λs. match s with
[ State f _ _ ⇒
    match next_instruction f with
    [ St_cond _ _ _ ⇒ cl_jump
(*    | St_jumptable _ _ ⇒ cl_jump*)
    | _ ⇒ cl_other
    ]
| Callstate _ _ _ _ _ _ ⇒ cl_call
| Returnstate _ _ _ _ ⇒ cl_return
| Finalstate _ ⇒ cl_other
].

(* As with is_cost_label/cost_label_of we define a boolean function as well
   as one which extracts the cost label so that we can use it in hypotheses
   without naming the cost label. *)

definition RTLabs_cost : state → bool ≝
λs. match s with
[ State f fs m ⇒
    is_cost_label (next_instruction f)
| _ ⇒ false
].

definition RTLabs_cost_label : state → option costlabel ≝
λs. match s with
[ State f fs m ⇒
    cost_label_of (next_instruction f)
| _ ⇒ None ?
].

(* "Program counters" need to identify the current state, either as a pair of
   the function and current instruction, or the function being entered or
   left.  Functions are identified by their function pointer block because 
   this avoids introducing functions to map back pointers to function ids using
   the global environment.  (See the comment at the start of this file, too.)
   
   Calls also get the caller's instruction label (or None for the initial call)
   so that we can distinguish different calls.  This is used only for the
   t.*_unrepeating property, which includes the pc for call states.
    *)

inductive RTLabs_pc : Type[0] ≝
| rapc_state : block → label → RTLabs_pc
| rapc_call : option label → block → RTLabs_pc
| rapc_ret : option block → RTLabs_pc
| rapc_fin : RTLabs_pc
.

definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
λx,y. match x with
[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
| rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒
    eqb ? o1 o2
    ∧ eq_block b1 b2
  | _ ⇒ false ]
| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ]
| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
].

definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
whd in match RTLabs_pc_eq;
* [ #b1 #l1 | #bl1 #b1 | #ob1 | ]
* [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ]
normalize nodelta
[ @eq_block_elim [ #E destruct | * #NE ] ]
[ @eq_identifier_elim [ #E destruct | *: * #NE ] ]
[ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ]
[ @eq_block_elim [ #E destruct | * #NE ] ]
normalize % #E destruct try (cases (NE (refl ??))) @refl
qed.

definition RTLabs_ext_state_to_pc : ∀ge. RTLabs_ext_state ge → RTLabs_deqset ≝
λge,s. match s with [ mk_RTLabs_ext_state s' stk mtc0 ⇒
match s' return λs'. Ras_Fn_Match ? s' ? → ? with
[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
| Callstate _ _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
| Finalstate _ ⇒ λmtc. rapc_fin
] mtc0 ].
whd in mtc; cases mtc
qed.

definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
λge,pc.
match pc with
[ rapc_state b l ⇒
  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
| _ ⇒ None ?
].

(* After returning from a function, we should be ready to execute the next
   instruction of the caller and the shadow stack should be preserved (we have
   to take the top element off because the Callstate includes the callee); *or*
   we're in the final state.
 *)

definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → RTLabs_ext_state ge → Prop ≝
λge,s,s'.
  match s with
  [ mk_Sig s p ⇒
    match s return λs. RTLabs_classify s = cl_call → ? with
    [ Callstate _ fd args dst stk m ⇒
      λ_. match s' with
      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
          next h = next f ∧
          f_graph (func h) = f_graph (func f) ∧
          match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]
      | Finalstate r ⇒ stk = [ ]
      | _ ⇒ False
      ]
   | State f fs m ⇒ λH.⊥
   | _ ⇒ λH.⊥
   ] p
 ].
[ whd in H:(??%?);
  cases (next_instruction f) in H;
  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
| normalize in H; destruct
| normalize in H; destruct
] qed.

definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge.RTLabs_classify s = cl_call) → ident ≝
λge,s.
  match s with
  [ mk_Sig s p ⇒
    match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
      match s' return λs'. RTLabs_classify s' = cl_call → ident with
      [ Callstate fid _ _ _ _ _ ⇒ λ_. fid
      | State f _ _ ⇒ λH.⊥
      | _ ⇒ λH.⊥
      ]
    ] p
  ].
[ whd in H:(??%?);
  cases (next_instruction f) in H;
  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
| *: normalize in H; destruct (H)
] qed.

lemma RTLabs_notail : ∀s.
  RTLabs_classify s = cl_tailcall →
  False.
* [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ]
normalize
#a try #b try #c try #d try #e try #g try #h try #i try #j destruct
qed.

(* Roughly corresponding to as_classifier *)
lemma RTLabs_notail' : ∀s.
  RTLabs_classify s = cl_tailcall →
  False.
#s #E @(RTLabs_notail … s)
generalize in match (RTLabs_classify s) in E ⊢ %;
#c #E' destruct %
qed.

definition RTLabs_status : genv → abstract_status ≝
λge.
  mk_abstract_status
    (RTLabs_ext_state ge)
    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
    RTLabs_deqset
    (RTLabs_ext_state_to_pc ge)
    (RTLabs_classify)
    (RTLabs_pc_to_cost_label ge)
    (RTLabs_after_return ge)
    (RTLabs_is_final)
    (RTLabs_call_ident ge)
    (λs. ⊥).
(* No tailcalls here for now. *)
cases s @RTLabs_notail'
qed.

(* Allow us to move between the different notions of when a state is cost
   labelled. *)

lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
  RTLabs_cost s = true ↔
  as_costed (RTLabs_status ge) s.
cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
#ge * *
[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
  whd in match (as_pc_of ??);
  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
  whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
  >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
  % cases (lookup_present ?? (f_graph func) ??) normalize
  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
  try (% #E' destruct)
  cases (NONE ?) assumption
| #vf #fd #args #dst #fs #m #stk #mtc %
  [ #E normalize in E; destruct
  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
    #H cases (NONE H)
  ]
| #v #dst #fs #m #stk #mtc %
  [ #E normalize in E; destruct
  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
    #H cases (NONE H)
  ]
| #r #stk #mtc %
  [ #E normalize in E; destruct
  | #E normalize in E; cases (NONE E)
  ]
] qed.

lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
  RTLabs_cost s = false →
  ¬ as_costed (RTLabs_status ge) s.
#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
qed.