source: src/common/SmallstepExec.ma @ 2338

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

Use much nicer definition for making several steps in the labelling
simulation.

File size: 9.6 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's an inversion-like result to get back the information contained in
80   the proof in Executions.ma.
81
82  *)
83
84record await_value_stuff : Type[2] ≝ {
85 avs_O : Type[0];
86 avs_I : avs_O → Type[0];
87 avs_exec : trans_system avs_O avs_I;
88 avs_g : global ?? avs_exec
89}.
90
91let rec await_value (avs:await_value_stuff)
92 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
93 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
94match v with
95[ Value ts ⇒ P (\fst ts) (\snd ts)
96| _ ⇒ False
97].
98
99let rec after_aux (avs:await_value_stuff)
100  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
101  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
102on n : Prop ≝
103match n with
104[ O ⇒ P tr s
105| S n' ⇒
106  match is_final … s with
107  [ None ⇒
108    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
109      after_aux avs n' s (tr ⧺ tr') P)
110  | _ ⇒ False
111  ]
112].
113
114definition after_n_steps : nat →
115 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
116 state ?? exec g →
117 (trace → state ?? exec g → Prop) → Prop ≝
118λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P.
119
120lemma after_n_covariant : ∀n,O,I,exec,g,P,Q.
121  (∀tr,s. P tr s → Q tr s) →
122  ∀s.
123  after_n_steps n O I exec g s P →
124  after_n_steps n O I exec g s Q.
125#n #O #I #exec #g #P #Q #H whd in ⊢ (? → % → %); generalize in match E0; elim n
126[ normalize /2/
127| #n' #IH #tr #s
128  normalize cases (is_final … s) normalize [ 2: #_ * ] cases (step O I exec g s) normalize /4/
129] qed.
130
131(* for joining a couple of these together *)
132
133lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'.
134  after_n_steps m O I exec g s' Q →
135  after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
136  after_n_steps (n+m) O I exec g s P.
137#n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
138[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
139  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
140  generalize in match s; -s
141  elim m
142  [ #s #tr' whd in ⊢ (% → %); @H2
143  | #m' #IH #s #tr' whd in ⊢ (% → %);
144    cases (is_final … s) [2: #r * ]
145    whd in ⊢ (% → %);
146    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ]
147| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
148  cases (is_final … s) [2: #r * ]
149  whd in ⊢ (% → %);
150  cases (step O I exec g s) [1,3: normalize // ]
151  * #tr1 #s1 whd in ⊢ (% → %); @IH @H
152] qed.
153
154
155(* A (possibly non-terminating) execution.   *)
156coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
157| e_stop : trace → int → state → execution state output input
158| e_step : trace → state → execution state output input → execution state output input
159| e_wrong : errmsg → execution state output input
160| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
161
162(* This definition is slightly awkward because of the need to provide resumptions.
163   It records the last trace/state passed in, then recursively processes the next
164   state. *)
165
166let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
167                       (exec:trans_system output input) (g:global ?? exec)
168                       (s:IO output input (trace×(state ?? exec g)))
169                       : execution ??? ≝
170match s with
171[ Wrong m ⇒ e_wrong ??? m
172| Value v ⇒ let 〈t,s'〉 ≝ v in
173    match is_final ?? exec g s' with
174    [ Some r ⇒ e_stop ??? t r s'
175    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
176| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
177].
178
179lemma execution_cases: ∀o,i,s.∀e:execution s o i.
180 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
181 | e_step tr s e ⇒ e_step ??? tr s e
182 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
183#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
184 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
185  here, used reflexivity instead *)
186
187axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
188match s with
189[ Wrong m ⇒ e_wrong ??? m
190| Value v ⇒ let 〈t,s'〉 ≝ v in
191    match is_final ?? exec g s' with
192    [ Some r ⇒ e_stop ??? t r s'
193    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
194| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
195].
196(*
197#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
198[ #o #k
199| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
200| ]
201whd in ⊢ (??%%); //;
202qed.
203*)
204
205lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
206  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
207  step … ge s = Value … 〈tr, s'〉 ∧
208  is_final … s' = Some ? r.
209#O #I #TS #ge #s #s' #tr #r
210>exec_inf_aux_unfold
211cases (step … ge s)
212[ 1,3: normalize #H1 #H2 try #H3 destruct
213| * #tr' #s''
214  whd in ⊢ (??%? → ?);
215  lapply (refl ? (is_final … s''))
216  cases (is_final … s'') in ⊢ (???% → %);
217  [ #_ whd in ⊢ (??%? → ?); #E destruct
218  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
219  ]
220] qed.
221
222lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
223  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
224  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
225#O #I #TS #ge #s #s' #tr #e
226>exec_inf_aux_unfold
227cases (step … s)
228[ 1,3: normalize #H1 #H2 try #H3 destruct
229| * #tr' #s''
230  whd in ⊢ (??%? → ?);
231  cases (is_final … s'')
232  [ #E normalize in E; destruct /2/
233  | #r #E normalize in E; destruct
234  ]
235] qed.
236
237lemma extract_interact : ∀O,I,TS,ge,s,o,k.
238  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
239  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
240#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
241cases (step … s)
242[ #o' #k' normalize #E destruct %{k'} /2/
243| * #x #y normalize cases (is_final ?????) normalize
244  #X try #Y destruct
245| normalize #m #E destruct
246] qed.
247
248lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
249  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
250  is_final … s' = None ?.
251#O #I #TS #ge #s #s' #tr #e
252>exec_inf_aux_unfold
253cases (step … s)
254[ 1,3: normalize #H1 #H2 try #H3 destruct
255| * #tr' #s''
256  whd in ⊢ (??%? → ?);
257  lapply (refl ? (is_final … s''))
258  cases (is_final … s'') in ⊢ (???% → %);
259  [ #F whd in ⊢ (??%? → ?); #E destruct @F
260  | #r' #_ #E whd in E:(??%?);  destruct
261  ]
262] qed.
263
264
265
266record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
267{ program : Type[0]
268; es1 :> trans_system outty inty
269; make_global : program → global ?? es1
270; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
271}.
272
273definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
274λo,i,fx,p.
275  match make_initial_state ?? fx p with
276  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
277  | Error m ⇒ e_wrong ??? m
278  ].
279
280
Note: See TracBrowser for help on using the repository browser.