source: src/RTLabs/RTLabs_classified_system.ma @ 3128

include "RTLabs/RTLabs_abstract.ma".
include "RTLabs/RTLabs_semantics.ma".
include "common/Measurable.ma".

(* First, plain RTLabs.  This for for the front-end, the back-end will get a
   prefix for its structured trace in terms of the version with the shadow
   stack below. *)

definition RTLabs_stack_ident :
  genv →
  ∀s:RTLabs_state.
  match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
  ident ≝
λge,s.
match s return λs. match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
[ Callstate id _ _ _ _ _ ⇒ λ_. id
| _ ⇒ λH.⊥
].
try @H whd in match (RTLabs_classify …) in H; normalize nodelta in H;
cases (next_instruction ?) in H; normalize nodelta //
qed.

definition RTLabs_pcs : preclassified_system ≝
mk_preclassified_system
  RTLabs_fullexec
  (λ_.RTLabs_cost)
  (λ_.RTLabs_classify)
  RTLabs_stack_ident.

(* Now the version extended with a shadow stack.  This is the one the back-end
   will see, because it matches the RTLabs abstract status for the
   structured traces. *)

definition RTLabs_ext_pcs ≝ mk_preclassified_system
  RTLabs_ext_fullexec
  (λg,s. RTLabs_cost (Ras_state … s))
  (λg,s. RTLabs_classify (Ras_state … s))
  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).