include "Cminor/Cminor_semantics.ma".

(* Avoid aliasing in interstage proofs *)

definition Cminor_state ≝ state.

(* States about to execute a cost statement.  Other statements may also emit
   cost labels due to expressions, but these are the only ones relevant for
   defining measurable subtraces. *)

definition Cminor_labelled : state → bool ≝
λs. match s with
[ State _ st _ _ _ _ _ _ _ _ ⇒ match st with [ St_cost _ _ ⇒ true | _ ⇒ false ]
| _ ⇒ false
].

(* Usual classification *)

(* only for classification type *)
include "common/StructuredTraces.ma".

definition Cminor_classify : state → status_class ≝
λs. match s with
[ State _ _ _ _ _ _ _ _ _ _ ⇒ cl_other
| Callstate _ _ _ _ _ ⇒ cl_call
| Returnstate _ _ _ ⇒ cl_return
| Finalstate _ ⇒ cl_other
].

definition cm_genv ≝ genv.

definition cm_env ≝ env.

definition cm_cont ≝ cont.

definition cm_eval_expr ≝ eval_expr.

definition CmState ≝ State.

definition CmReturnstate ≝ Returnstate.

definition CmCallstate ≝ Callstate.

lemma Cminor_notailcalls : ∀s. Cminor_classify s ≠ cl_tailcall.
* #a try #b try #c try #d try #e try #f try #g try #h try #i try #j
normalize % #E destruct
qed.