source: src/common/SmallstepExec.ma @ 2474

Last change on this file since 2474 was 2459, checked in by campbell, 7 years ago

Syntax update

File size: 11.2 KB
Line 
1include "utilities/extralib.ma".
2include "common/IOMonad.ma".
3include "common/Integers.ma".
4include "common/Events.ma".
5
6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
7{ global : Type[1]
8; state  : global → Type[0]
9; is_final : ∀g. state g → option int
10; step : ∀g. state g → IO outty inty (trace×(state g))
11}.
12
13let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
14               (g:global ?? exec) (s:state ?? exec g)
15 : IO outty inty (trace × (state ?? exec g)) ≝
16match n with
17[ O ⇒ Value ??? 〈E0, s〉
18| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
19         ! 〈tn,sn〉 ← repeat n' ?? exec g s1;
20         Value ??? 〈t1⧺tn,sn〉
21].
22
23(* We take care here to check that we're not at the final state.  It is not
24   necessarily the case that a success step guarantees this (e.g., because
25   there may be no way to stop a processor, so an infinite loop is used
26   instead). *)
27inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
28| plus_one : ∀s1,tr,s2.
29    is_final … TS ge s1 = None ? →
30    step … TS ge s1 = OK … 〈tr,s2〉 →
31    plus … ge s1 tr s2
32| plus_succ : ∀s1,tr,s2,tr',s3.
33    is_final … TS ge s1 = None ? →
34    step … TS ge s1 = OK … 〈tr,s2〉 →
35    plus … ge s2 tr' s3 →
36    plus … ge s1 (tr⧺tr') s3.
37
38lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
39  plus O I FE gl s tr s' →
40  is_final … FE gl s = None ?.
41#O #I #FE #gl #s0 #tr0 #s0' * //
42qed.
43
44let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
45                  (l:list A) on l : res (trace × (list B)) ≝
46match l with
47[ nil ⇒ OK ? 〈E0, [ ]〉
48| cons h t ⇒
49    do 〈tr,h'〉 ← f h;
50    do 〈tr',t'〉 ← trace_map … f t;
51    OK ? 〈tr ⧺ tr',h'::t'〉
52].
53
54(* A third version of making several steps (!)
55
56   The idea here is to have a computational definition of reducing serveral
57   steps then showing some property about the resulting trace and state.  By
58   careful use of let rec we can ensure that reduction stops in a sensible
59   way whenever the number of steps or the step currently being executed is
60   not (reducible to) a value.
61
62   For example, we state a property to prove by something like
63
64     ∃n. after_n_steps n … clight_exec ge s (λtr,s'. <some property>)
65
66   then start reducing by giving the number of steps and reducing the
67   definition
68
69     %{3} whd
70
71   and then whenever the reduction gets stuck, the currently reducing step is
72   the third subterm, which we can reduce and unblock with (for example)
73   rewriting
74
75     whd in ⊢ (??%?); >EXe'
76
77   and at the end reduce with whd to get the property as the goal.
78
79   There are a few inversion-like results to get back the information contained in
80   the proof below, and other that provides all the steps in an inductive form
81   in Executions.ma.
82
83  *)
84
85record await_value_stuff : Type[2] ≝ {
86 avs_O : Type[0];
87 avs_I : avs_O → Type[0];
88 avs_exec : trans_system avs_O avs_I;
89 avs_g : global ?? avs_exec
90}.
91
92let rec await_value (avs:await_value_stuff)
93 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
94 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
95match v with
96[ Value ts ⇒ P (\fst ts) (\snd ts)
97| _ ⇒ False
98].
99
100let rec after_aux (avs:await_value_stuff)
101  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
102  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
103on n : Prop ≝
104match n with
105[ O ⇒ P tr s
106| S n' ⇒
107  match is_final … s with
108  [ None ⇒
109    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
110      after_aux avs n' s (tr ⧺ tr') P)
111  | _ ⇒ False
112  ]
113].
114
115definition after_n_steps : nat →
116 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
117 state ?? exec g →
118 (trace → state ?? exec g → Prop) → Prop ≝
119λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P.
120
121lemma after_aux_covariant : ∀avs,P,Q,tr'.
122  (∀tr,s. P (tr'⧺tr) s → Q tr s) →
123  ∀n,s,tr.
124  after_aux avs n s (tr'⧺tr) P →
125  after_aux avs n s tr Q.
126#avs #P #Q #tr' #H #n elim n
127[ normalize /2/
128| #n' #IH #s #tr
129  whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ]
130  whd in ⊢ (% → %);
131  cases (step … s) [1,3: normalize /2/ ]
132  * #tr'' #s''
133  whd in ⊢ (% → %); >Eapp_assoc @IH
134] qed.
135
136lemma after_n_covariant : ∀n,O,I,exec,g,P,Q.
137  (∀tr,s. P tr s → Q tr s) →
138  ∀s.
139  after_n_steps n O I exec g s P →
140  after_n_steps n O I exec g s Q.
141normalize /3/
142qed.
143
144(* for joining a couple of these together *)
145
146lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'.
147  after_n_steps m O I exec g s' Q →
148  after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
149  after_n_steps (n+m) O I exec g s P.
150#n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
151[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
152  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
153  generalize in match s; -s
154  elim m
155  [ #s #tr' whd in ⊢ (% → %); @H2
156  | #m' #IH #s #tr' whd in ⊢ (% → %);
157    cases (is_final … s) [2: #r * ]
158    whd in ⊢ (% → %);
159    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ]
160| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
161  cases (is_final … s) [2: #r * ]
162  whd in ⊢ (% → %);
163  cases (step O I exec g s) [1,3: normalize // ]
164  * #tr1 #s1 whd in ⊢ (% → %); @IH @H
165] qed.
166
167(* Inversion lemmas. *)
168
169lemma after_1_of_n_steps : ∀n,O,I,exec,g,P,s.
170  after_n_steps (S n) O I exec g s P →
171  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧
172  after_n_steps n O I exec g s' (λtr'',s''. P (tr⧺tr'') s'').
173#n #O #I #exec #g #P #s
174whd in ⊢ (% → ?);
175cases (is_final … s)
176[ whd in ⊢ (% → ?);
177  cases (step … s)
178  [ #o #k *
179  | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
180    %{tr} %{s'} % // whd @(after_aux_covariant … AFTER)
181    #tr' #s'' //
182  | #m *
183  ]
184| #r *
185] qed.
186
187lemma after_1_step : ∀O,I,exec,g,P,s.
188  after_n_steps 1 O I exec g s P →
189  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ P tr s'.
190#O #I #exec #g #P #s #AFTER
191cases (after_1_of_n_steps … AFTER)
192#tr * #s' * #STEP #FIN %{tr} %{s'} % // whd in FIN; >E0_right in FIN; //
193qed.
194
195(* A typical way to use the following:
196
197   With a hypothesis
198     EX : after_n_steps n ... (State ...) ...
199   reduce it [whd in EX;] to
200     EX : await_value ...
201   then perform inversion
202   [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX]
203      x : T
204     E1 : f = return x
205     EX : await_value ...
206 *)
207
208lemma await_value_bind_inv : ∀avs,T,f,g,P.
209  await_value avs (m_bind … f g) P →
210  ∃x:T. (f = return x) ∧ await_value avs (g x) P.
211#avs #T *
212[ #o #k #g #P *
213| #x #g #P #AWAIT %{x} % //
214| #m #g #P *
215] qed.
216
217(* A (possibly non-terminating) execution.   *)
218coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
219| e_stop : trace → int → state → execution state output input
220| e_step : trace → state → execution state output input → execution state output input
221| e_wrong : errmsg → execution state output input
222| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
223
224(* This definition is slightly awkward because of the need to provide resumptions.
225   It records the last trace/state passed in, then recursively processes the next
226   state. *)
227
228let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
229                       (exec:trans_system output input) (g:global ?? exec)
230                       (s:IO output input (trace×(state ?? exec g)))
231                       : execution ??? ≝
232match s with
233[ Wrong m ⇒ e_wrong ??? m
234| Value v ⇒ let 〈t,s'〉 ≝ v in
235    match is_final ?? exec g s' with
236    [ Some r ⇒ e_stop ??? t r s'
237    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
238| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
239].
240
241lemma execution_cases: ∀o,i,s.∀e:execution s o i.
242 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
243 | e_step tr s e ⇒ e_step ??? tr s e
244 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
245#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
246 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
247  here, used reflexivity instead *)
248
249axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
250match s with
251[ Wrong m ⇒ e_wrong ??? m
252| Value v ⇒ let 〈t,s'〉 ≝ v in
253    match is_final ?? exec g s' with
254    [ Some r ⇒ e_stop ??? t r s'
255    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
256| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
257].
258(*
259#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
260[ #o #k
261| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
262| ]
263whd in ⊢ (??%%); //;
264qed.
265*)
266
267lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
268  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
269  step … ge s = Value … 〈tr, s'〉 ∧
270  is_final … s' = Some ? r.
271#O #I #TS #ge #s #s' #tr #r
272>exec_inf_aux_unfold
273cases (step … ge s)
274[ 1,3: normalize #H1 #H2 try #H3 destruct
275| * #tr' #s''
276  whd in ⊢ (??%? → ?);
277  lapply (refl ? (is_final … s''))
278  cases (is_final … s'') in ⊢ (???% → %);
279  [ #_ whd in ⊢ (??%? → ?); #E destruct
280  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
281  ]
282] qed.
283
284lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
285  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
286  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
287#O #I #TS #ge #s #s' #tr #e
288>exec_inf_aux_unfold
289cases (step … s)
290[ 1,3: normalize #H1 #H2 try #H3 destruct
291| * #tr' #s''
292  whd in ⊢ (??%? → ?);
293  cases (is_final … s'')
294  [ #E normalize in E; destruct /2/
295  | #r #E normalize in E; destruct
296  ]
297] qed.
298
299lemma extract_interact : ∀O,I,TS,ge,s,o,k.
300  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
301  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
302#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
303cases (step … s)
304[ #o' #k' normalize #E destruct %{k'} /2/
305| * #x #y normalize cases (is_final ?????) normalize
306  #X try #Y destruct
307| normalize #m #E destruct
308] qed.
309
310lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
311  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
312  is_final … s' = None ?.
313#O #I #TS #ge #s #s' #tr #e
314>exec_inf_aux_unfold
315cases (step … s)
316[ 1,3: normalize #H1 #H2 try #H3 destruct
317| * #tr' #s''
318  whd in ⊢ (??%? → ?);
319  lapply (refl ? (is_final … s''))
320  cases (is_final … s'') in ⊢ (???% → %);
321  [ #F whd in ⊢ (??%? → ?); #E destruct @F
322  | #r' #_ #E whd in E:(??%?);  destruct
323  ]
324] qed.
325
326
327
328record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
329{ program : Type[0]
330; es1 :> trans_system outty inty
331; make_global : program → global ?? es1
332; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
333}.
334
335definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
336λo,i,fx,p.
337  match make_initial_state ?? fx p with
338  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
339  | Error m ⇒ e_wrong ??? m
340  ].
341
342
Note: See TracBrowser for help on using the repository browser.