source: src/common/SmallstepExec.ma @ 2533

Last change on this file since 2533 was 2487, checked in by campbell, 7 years ago

Set up "after_n_steps" to enforce an invariant on states.

File size: 11.7 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   An invariant is also asserted on every state other than the initial one.
63
64   For example, we state a property to prove by something like
65
66     ∃n. after_n_steps n … clight_exec ge s inv (λtr,s'. <some property>)
67
68   then start reducing by giving the number of steps and reducing the
69   definition
70
71     %{3} whd
72
73   and then whenever the reduction gets stuck, the currently reducing step is
74   the third subterm, which we can reduce and unblock with (for example)
75   rewriting
76
77     whd in ⊢ (??%?); >EXe'
78
79   and at the end reduce with whd to get the property as the goal.
80
81   There are a few inversion-like results to get back the information contained in
82   the proof below, and other that provides all the steps in an inductive form
83   in Executions.ma.
84
85  *)
86
87record await_value_stuff : Type[2] ≝ {
88 avs_O : Type[0];
89 avs_I : avs_O → Type[0];
90 avs_exec : trans_system avs_O avs_I;
91 avs_g : global ?? avs_exec;
92 avs_inv : state ?? avs_exec avs_g → bool
93}.
94
95let rec await_value (avs:await_value_stuff)
96 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
97 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
98match v with
99[ Value ts ⇒ P (\fst ts) (\snd ts)
100| _ ⇒ False
101].
102
103let rec assert (b:bool) (P:Prop) on b ≝
104if b then P else False.
105
106let rec after_aux (avs:await_value_stuff)
107  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
108  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
109on n : Prop ≝
110match n with
111[ O ⇒ P tr s
112| S n' ⇒
113  match is_final … s with
114  [ None ⇒
115    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
116      assert (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P))
117  | _ ⇒ False
118  ]
119].
120
121definition after_n_steps : nat →
122 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
123 state ?? exec g →
124 (state ?? exec g → bool) →
125 (trace → state ?? exec g → Prop) → Prop ≝
126λn,O,I,exec,g,s,inv,P. after_aux (mk_await_value_stuff O I exec g inv) n s E0 P.
127
128lemma after_aux_covariant : ∀avs,P,Q,tr'.
129  (∀tr,s. P (tr'⧺tr) s → Q tr s) →
130  ∀n,s,tr.
131  after_aux avs n s (tr'⧺tr) P →
132  after_aux avs n s tr Q.
133#avs #P #Q #tr' #H #n elim n
134[ normalize /2/
135| #n' #IH #s #tr
136  whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ]
137  whd in ⊢ (% → %);
138  cases (step … s) [1,3: normalize /2/ ]
139  * #tr'' #s''
140  whd in ⊢ (% → %);
141  cases (avs_inv avs s'') [ 2: * ]
142  whd in ⊢ (% → %);
143  >Eapp_assoc @IH
144] qed.
145
146lemma after_n_covariant : ∀n,O,I,exec,g,P,inv,Q.
147  (∀tr,s. P tr s → Q tr s) →
148  ∀s.
149  after_n_steps n O I exec g s inv P →
150  after_n_steps n O I exec g s inv Q.
151normalize /3/
152qed.
153
154(* for joining a couple of these together *)
155
156lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'.
157  after_n_steps m O I exec g s' inv Q →
158  after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
159  after_n_steps (n+m) O I exec g s inv P.
160#n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
161[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
162  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
163  generalize in match s; -s
164  elim m
165  [ #s #tr' whd in ⊢ (% → %); @H2
166  | #m' #IH #s #tr' whd in ⊢ (% → %);
167    cases (is_final … s) [2: #r * ]
168    whd in ⊢ (% → %);
169    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %);
170    cases (inv s'') [2: * ]
171    >Eapp_assoc @IH ]
172| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
173  cases (is_final … s) [2: #r * ]
174  whd in ⊢ (% → %);
175  cases (step O I exec g s) [1,3: normalize // ]
176  * #tr1 #s1 whd in ⊢ (% → %);
177  cases (inv s1) [2:*]
178  @IH @H
179] qed.
180
181(* Inversion lemmas. *)
182
183lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s.
184  after_n_steps (S n) O I exec g s inv P →
185  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧
186  bool_to_Prop (inv s') ∧
187  after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s'').
188#n #O #I #exec #g #inv #P #s
189whd in ⊢ (% → ?);
190cases (is_final … s)
191[ whd in ⊢ (% → ?);
192  cases (step … s)
193  [ #o #k *
194  | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
195    %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /2/ cases AFTER
196  | #m *
197  ]
198| #r *
199] qed.
200
201lemma after_1_step : ∀O,I,exec,g,inv,P,s.
202  after_n_steps 1 O I exec g s inv P →
203  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ bool_to_Prop (inv s') ∧ P tr s'.
204#O #I #exec #g #inv #P #s #AFTER
205cases (after_1_of_n_steps … AFTER)
206#tr * #s' * * #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //
207qed.
208
209(* A typical way to use the following:
210
211   With a hypothesis
212     EX : after_n_steps n ... (State ...) ...
213   reduce it [whd in EX;] to
214     EX : await_value ...
215   then perform inversion
216   [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX]
217      x : T
218     E1 : f = return x
219     EX : await_value ...
220 *)
221
222lemma await_value_bind_inv : ∀avs,T,f,g,P.
223  await_value avs (m_bind … f g) P →
224  ∃x:T. (f = return x) ∧ await_value avs (g x) P.
225#avs #T *
226[ #o #k #g #P *
227| #x #g #P #AWAIT %{x} % //
228| #m #g #P *
229] qed.
230
231(* A (possibly non-terminating) execution.   *)
232coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
233| e_stop : trace → int → state → execution state output input
234| e_step : trace → state → execution state output input → execution state output input
235| e_wrong : errmsg → execution state output input
236| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
237
238(* This definition is slightly awkward because of the need to provide resumptions.
239   It records the last trace/state passed in, then recursively processes the next
240   state. *)
241
242let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
243                       (exec:trans_system output input) (g:global ?? exec)
244                       (s:IO output input (trace×(state ?? exec g)))
245                       : execution ??? ≝
246match s with
247[ Wrong m ⇒ e_wrong ??? m
248| Value v ⇒ let 〈t,s'〉 ≝ v in
249    match is_final ?? exec g s' with
250    [ Some r ⇒ e_stop ??? t r s'
251    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
252| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
253].
254
255lemma execution_cases: ∀o,i,s.∀e:execution s o i.
256 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
257 | e_step tr s e ⇒ e_step ??? tr s e
258 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
259#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
260 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
261  here, used reflexivity instead *)
262
263axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
264match s with
265[ Wrong m ⇒ e_wrong ??? m
266| Value v ⇒ let 〈t,s'〉 ≝ v in
267    match is_final ?? exec g s' with
268    [ Some r ⇒ e_stop ??? t r s'
269    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
270| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
271].
272(*
273#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
274[ #o #k
275| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
276| ]
277whd in ⊢ (??%%); //;
278qed.
279*)
280
281lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
282  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
283  step … ge s = Value … 〈tr, s'〉 ∧
284  is_final … s' = Some ? r.
285#O #I #TS #ge #s #s' #tr #r
286>exec_inf_aux_unfold
287cases (step … ge s)
288[ 1,3: normalize #H1 #H2 try #H3 destruct
289| * #tr' #s''
290  whd in ⊢ (??%? → ?);
291  lapply (refl ? (is_final … s''))
292  cases (is_final … s'') in ⊢ (???% → %);
293  [ #_ whd in ⊢ (??%? → ?); #E destruct
294  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
295  ]
296] qed.
297
298lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
299  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
300  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
301#O #I #TS #ge #s #s' #tr #e
302>exec_inf_aux_unfold
303cases (step … s)
304[ 1,3: normalize #H1 #H2 try #H3 destruct
305| * #tr' #s''
306  whd in ⊢ (??%? → ?);
307  cases (is_final … s'')
308  [ #E normalize in E; destruct /2/
309  | #r #E normalize in E; destruct
310  ]
311] qed.
312
313lemma extract_interact : ∀O,I,TS,ge,s,o,k.
314  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
315  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
316#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
317cases (step … s)
318[ #o' #k' normalize #E destruct %{k'} /2/
319| * #x #y normalize cases (is_final ?????) normalize
320  #X try #Y destruct
321| normalize #m #E destruct
322] qed.
323
324lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
325  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
326  is_final … s' = None ?.
327#O #I #TS #ge #s #s' #tr #e
328>exec_inf_aux_unfold
329cases (step … s)
330[ 1,3: normalize #H1 #H2 try #H3 destruct
331| * #tr' #s''
332  whd in ⊢ (??%? → ?);
333  lapply (refl ? (is_final … s''))
334  cases (is_final … s'') in ⊢ (???% → %);
335  [ #F whd in ⊢ (??%? → ?); #E destruct @F
336  | #r' #_ #E whd in E:(??%?);  destruct
337  ]
338] qed.
339
340
341
342record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
343{ program : Type[0]
344; es1 :> trans_system outty inty
345; make_global : program → global ?? es1
346; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
347}.
348
349definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
350λo,i,fx,p.
351  match make_initial_state ?? fx p with
352  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
353  | Error m ⇒ e_wrong ??? m
354  ].
355
356
Note: See TracBrowser for help on using the repository browser.