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
frontend measurable traces proof.

File size:
1.2 KB

Line  

1  include "Cminor/Cminor_semantics.ma". 

2  

3  (* Avoid aliasing in interstage proofs *) 

4  

5  definition 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  

11  definition 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 *) 

20  include "common/StructuredTraces.ma". 

21  

22  definition 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  

30  definition cm_genv ≝ genv. 

31  

32  definition cm_env ≝ env. 

33  

34  definition cm_cont ≝ cont. 

35  

36  definition cm_eval_expr ≝ eval_expr. 

37  

38  definition CmState ≝ State. 

39  

40  definition CmReturnstate ≝ Returnstate. 

41  

42  definition CmCallstate ≝ Callstate. 

43  

44  lemma 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 

46  normalize % #E destruct 

47  qed. 

Note: See
TracBrowser
for help on using the repository browser.