source: src/Cminor/Cminor_abstract.ma

Last change on this file was 3007, checked in by campbell, 7 years ago

Sketch out how Cminor to RTLabs correctness would fit into the
front-end measurable traces proof.

File size: 1.2 KB
Line 
1include "Cminor/Cminor_semantics.ma".
2
3(* Avoid aliasing in interstage proofs *)
4
5definition Cminor_state ≝ state.
6
7(* States about to execute a cost statement.  Other statements may also emit
8   cost labels due to expressions, but these are the only ones relevant for
9   defining measurable subtraces. *)
10
11definition Cminor_labelled : state → bool ≝
12λs. match s with
13[ State _ st _ _ _ _ _ _ _ _ ⇒ match st with [ St_cost _ _ ⇒ true | _ ⇒ false ]
14| _ ⇒ false
15].
16
17(* Usual classification *)
18
19(* only for classification type *)
20include "common/StructuredTraces.ma".
21
22definition Cminor_classify : state → status_class ≝
23λs. match s with
24[ State _ _ _ _ _ _ _ _ _ _ ⇒ cl_other
25| Callstate _ _ _ _ _ ⇒ cl_call
26| Returnstate _ _ _ ⇒ cl_return
27| Finalstate _ ⇒ cl_other
28].
29
30definition cm_genv ≝ genv.
31
32definition cm_env ≝ env.
33
34definition cm_cont ≝ cont.
35
36definition cm_eval_expr ≝ eval_expr.
37
38definition CmState ≝ State.
39
40definition CmReturnstate ≝ Returnstate.
41
42definition CmCallstate ≝ Callstate.
43
44lemma Cminor_notailcalls : ∀s. Cminor_classify s ≠ cl_tailcall.
45* #a try #b try #c try #d try #e try #f try #g try #h try #i try #j
46normalize % #E destruct
47qed.
Note: See TracBrowser for help on using the repository browser.