source: src/RTLabs/Traces.ma @ 1559

Last change on this file since 1559 was 1559, checked in by campbell, 8 years ago

Add a notion of flat traces with evidence for RTLabs.

File size: 6.0 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
5discriminator status_class.
6
7(* NB: we do not consider jumps in the traces of RTLabs programs. *)
8
9inductive RTLabs_classify : state → status_class → Prop ≝
10| rtla_other : ∀f,fs,m.    RTLabs_classify (State f fs m)        cl_other
11| rtla_call  : ∀a,b,c,d,e. RTLabs_classify (Callstate a b c d e) cl_call
12| rtla_ret   : ∀a,b,c,d.   RTLabs_classify (Returnstate a b c d) cl_return
13.
14
15inductive RTLabs_stmt_cost : statement → Prop ≝
16| stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l).
17
18inductive RTLabs_cost : state → Prop ≝
19| cost_instr : ∀f,fs,m.
20    RTLabs_stmt_cost (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) →
21    RTLabs_cost (State f fs m).
22
23definition RTLabs_status : genv → abstract_status ≝
24λge.
25  mk_abstract_status
26    state
27    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
28    RTLabs_classify
29    RTLabs_cost
30    (λs,s'. match s with
31      [ dp s p ⇒
32        match s return λs. RTLabs_classify s cl_call → ? with
33        [ Callstate fd args dst stk m ⇒
34          λ_. match s' with
35          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
36          | _ ⇒ False
37          ]
38        | State f fs m ⇒ λH.⊥
39        | _ ⇒ λH.⊥
40        ] p
41      ]).
42inversion H try #a try #b try #c try #d try #e try #f destruct
43qed.
44
45(* Before attempting to construct a structured trace, let's show that we can
46   form flat traces with evidence that they were constructed from an execution.
47   
48   For now we don't consider I/O. *)
49
50
51coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
52| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
53| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
54| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
55
56(* add I/O? *)
57coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
58| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
59| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
60| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
61
62let corec make_flat_trace ge s
63  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
64  flat_trace io_out io_in ge s ≝
65let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
66match e return λx. e = x → ? with
67[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
68| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
69| e_wrong m ⇒ λE. ft_wrong … s m ?
70| e_interact o f ⇒ λE. ⊥
71] (refl ? e).
72[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
73  cases (eval_statement ge s)
74  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
75  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
76    >(?:is_final ????? = RTLabs_is_final s1) //
77    lapply (refl ? (RTLabs_is_final s1))
78    cases (RTLabs_is_final s1) in ⊢ (???% → %);
79    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
80    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
81    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
82    ]
83  | *: #m whd in ⊢ (??%? → ?); #E destruct
84  ]
85| whd in E:(??%?); >exec_inf_aux_unfold in E;
86  cases (eval_statement ge s)
87  [ #O #K whd in ⊢ (??%? → ?); #E destruct
88  | * #tr #s1 whd in ⊢ (??%? → ?);
89    cases (is_final ?????)
90    [ whd in ⊢ (??%? → ?); #E destruct @refl
91    | #i whd in ⊢ (??%? → ?); #E destruct
92    ]
93  | #m whd in ⊢ (??%? → ?); #E destruct
94  ]
95| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
96  cases (eval_statement ge s)
97  [ #O #K whd in ⊢ (??%? → ?); #E destruct
98  | * #tr #s1 whd in ⊢ (??%? → ?);
99    cases (is_final ?????)
100    [ whd in ⊢ (??%? → ?); #E
101      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
102      destruct
103      inversion H
104      [ #a #b #c #E1 destruct
105      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
106      | #m #E1 destruct
107      ]
108    | #i whd in ⊢ (??%? → ?); #E destruct
109    ]
110  | #m whd in ⊢ (??%? → ?); #E destruct
111  ]
112| whd in E:(??%?); >exec_inf_aux_unfold in E;
113  cases (eval_statement ge s)
114  [ #O #K whd in ⊢ (??%? → ?); #E destruct
115  | * #tr1 #s1 whd in ⊢ (??%? → ?);
116    cases (is_final ?????)
117    [ whd in ⊢ (??%? → ?); #E destruct
118    | #i whd in ⊢ (??%? → ?); #E destruct
119    ]
120  | #m whd in ⊢ (??%? → ?); #E destruct @refl
121  ]
122| whd in E:(??%?); >E in H; #H
123  inversion H
124  [ #a #b #c #E destruct
125  | #a #b #c #d #E1 destruct
126  | #m #E1 destruct
127  ]
128] qed.
129
130let corec make_whole_flat_trace p s
131  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
132  (I:make_initial_state ??? p = OK ? s) :
133  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
134let ge ≝ make_global … p in
135let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
136match e return λx. e = x → ? with
137[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
138| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
139| e_wrong m ⇒ λE. ⊥
140| e_interact o f ⇒ λE. ⊥
141] (refl ? e).
142[ whd in E:(??%?); >exec_inf_aux_unfold in E;
143  whd in ⊢ (??%? → ?);
144  >(?:is_final ????? = RTLabs_is_final s) //
145  lapply (refl ? (RTLabs_is_final s))
146  cases (RTLabs_is_final s) in ⊢ (???% → %);
147  [ #_ whd in ⊢ (??%? → ?); #E destruct
148  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
149  ]
150| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
151  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
152  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
153    [ #a #b #c #E1 destruct
154    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
155      @H1
156    | #m #E1 destruct
157    ]
158  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
159  ]
160| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
161  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
162| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
163  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
164] qed.
165
Note: See TracBrowser for help on using the repository browser.