source: src/common/SmallstepExec.ma @ 2314

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

A general result about simulations of executions.

File size: 6.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         repeat n' ?? exec g s1
20].
21
22(* We take care here to check that we're not at the final state.  It is not
23   necessarily the case that a success step guarantees this (e.g., because
24   there may be no way to stop a processor, so an infinite loop is used
25   instead). *)
26inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
27| plus_one : ∀s1,tr,s2.
28    is_final … TS ge s1 = None ? →
29    step … TS ge s1 = OK … 〈tr,s2〉 →
30    plus … ge s1 tr s2
31| plus_succ : ∀s1,tr,s2,tr',s3.
32    is_final … TS ge s1 = None ? →
33    step … TS ge s1 = OK … 〈tr,s2〉 →
34    plus … ge s2 tr' s3 →
35    plus … ge s1 (tr⧺tr') s3.
36
37lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
38  plus O I FE gl s tr s' →
39  is_final … FE gl s = None ?.
40#O #I #FE #gl #s0 #tr0 #s0' * //
41qed.
42
43let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
44                  (l:list A) on l : res (trace × (list B)) ≝
45match l with
46[ nil ⇒ OK ? 〈E0, [ ]〉
47| cons h t ⇒
48    do 〈tr,h'〉 ← f h;
49    do 〈tr',t'〉 ← trace_map … f t;
50    OK ? 〈tr ⧺ tr',h'::t'〉
51].
52
53(* A (possibly non-terminating) execution.   *)
54coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
55| e_stop : trace → int → state → execution state output input
56| e_step : trace → state → execution state output input → execution state output input
57| e_wrong : errmsg → execution state output input
58| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
59
60(* This definition is slightly awkward because of the need to provide resumptions.
61   It records the last trace/state passed in, then recursively processes the next
62   state. *)
63
64let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
65                       (exec:trans_system output input) (g:global ?? exec)
66                       (s:IO output input (trace×(state ?? exec g)))
67                       : execution ??? ≝
68match s with
69[ Wrong m ⇒ e_wrong ??? m
70| Value v ⇒ let 〈t,s'〉 ≝ v in
71    match is_final ?? exec g s' with
72    [ Some r ⇒ e_stop ??? t r s'
73    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
74| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
75].
76
77lemma execution_cases: ∀o,i,s.∀e:execution s o i.
78 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
79 | e_step tr s e ⇒ e_step ??? tr s e
80 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
81#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
82 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
83  here, used reflexivity instead *)
84
85axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
86match s with
87[ Wrong m ⇒ e_wrong ??? m
88| Value v ⇒ let 〈t,s'〉 ≝ v in
89    match is_final ?? exec g s' with
90    [ Some r ⇒ e_stop ??? t r s'
91    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
92| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
93].
94(*
95#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
96[ #o #k
97| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
98| ]
99whd in ⊢ (??%%); //;
100qed.
101*)
102
103lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
104  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
105  step … ge s = Value … 〈tr, s'〉 ∧
106  is_final … s' = Some ? r.
107#O #I #TS #ge #s #s' #tr #r
108>exec_inf_aux_unfold
109cases (step … ge s)
110[ 1,3: normalize #H1 #H2 try #H3 destruct
111| * #tr' #s''
112  whd in ⊢ (??%? → ?);
113  lapply (refl ? (is_final … s''))
114  cases (is_final … s'') in ⊢ (???% → %);
115  [ #_ whd in ⊢ (??%? → ?); #E destruct
116  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
117  ]
118] qed.
119
120lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
121  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
122  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
123#O #I #TS #ge #s #s' #tr #e
124>exec_inf_aux_unfold
125cases (step … s)
126[ 1,3: normalize #H1 #H2 try #H3 destruct
127| * #tr' #s''
128  whd in ⊢ (??%? → ?);
129  cases (is_final … s'')
130  [ #E normalize in E; destruct /2/
131  | #r #E normalize in E; destruct
132  ]
133] qed.
134
135lemma extract_interact : ∀O,I,TS,ge,s,o,k.
136  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
137  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
138#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
139cases (step … s)
140[ #o' #k' normalize #E destruct %{k'} /2/
141| * #x #y normalize cases (is_final ?????) normalize
142  #X try #Y destruct
143| normalize #m #E destruct
144] qed.
145
146lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
147  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
148  is_final … s' = None ?.
149#O #I #TS #ge #s #s' #tr #e
150>exec_inf_aux_unfold
151cases (step … s)
152[ 1,3: normalize #H1 #H2 try #H3 destruct
153| * #tr' #s''
154  whd in ⊢ (??%? → ?);
155  lapply (refl ? (is_final … s''))
156  cases (is_final … s'') in ⊢ (???% → %);
157  [ #F whd in ⊢ (??%? → ?); #E destruct @F
158  | #r' #_ #E whd in E:(??%?);  destruct
159  ]
160] qed.
161
162
163
164record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
165{ program : Type[0]
166; es1 :> trans_system outty inty
167; make_global : program → global ?? es1
168; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
169}.
170
171definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
172λo,i,fx,p.
173  match make_initial_state ?? fx p with
174  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
175  | Error m ⇒ e_wrong ??? m
176  ].
177
178
Note: See TracBrowser for help on using the repository browser.