source: src/RTLabs/RTLabs_semantics.ma @ 2895

Last change on this file since 2895 was 2895, checked in by campbell, 6 years ago

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

File size: 17.9 KB
Line 
1
2include "basics/lists/list.ma".
3
4include "common/Errors.ma".
5include "common/Globalenvs.ma".
6include "common/IO.ma".
7include "common/SmallstepExec.ma".
8
9include "RTLabs/RTLabs_syntax.ma".
10
11definition genv ≝ genv_t (fundef internal_function).
12
13record frame : Type[0] ≝
14{ func   : internal_function
15; locals : register_env val
16; next   : label
17; next_ok: present ?? (f_graph func) next
18; sp     : block
19; retdst : option register
20}.
21
22definition adv : ∀l:label. ∀f:frame. present ?? (f_graph (func f)) l → frame ≝
23λl,f,p. mk_frame (func f) (locals f) l p (sp f) (retdst f).
24
25inductive state : Type[0] ≝
26| State :
27   ∀   f : frame.
28   ∀  fs : list frame.
29   ∀   m : mem.
30   state
31| Callstate :
32   ∀  id : ident. (* fn name; only used for instrumentation, not the semantics *)
33   ∀  fd : fundef internal_function.
34   ∀args : list val.
35   ∀ dst : option register.
36   ∀ stk : list frame.
37   ∀   m : mem.
38   state
39| Returnstate :
40   ∀ rtv : option val.
41   ∀ dst : option register.
42   ∀ stk : list frame.
43   ∀   m : mem.
44   state
45| Finalstate :
46   ∀   r : int.
47   state
48.
49
50definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
51
52definition next_instruction : frame → statement ≝
53λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f).
54
55definition init_locals : list (register × typ) → register_env val ≝
56foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
57
58definition reg_store ≝
59λreg,v,locals.
60  update RegisterTag val locals reg v.
61
62let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
63match rs with
64[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
65| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
66  let 〈r,ty〉 ≝ rt in
67  let locals' ≝ add RegisterTag val locals r v in
68  params_store rst vst locals'
69] ].
70
71
72definition reg_retrieve : register_env ? → register → res val ≝
73λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
74
75definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
76λge,st.
77match st return λ_. IO ??? with
78[ State f fs m ⇒
79  let s ≝ next_instruction f in
80  match s return λs. labels_present ? s → IO ??? with
81  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
82  | St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉
83  | St_const _ r cst l ⇒ λH.
84      ! v ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) (sp f) cst);
85      ! locals ← reg_store r v (locals f);
86      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
87  | St_op1 _ _ op dst src l ⇒ λH.
88      ! v ← reg_retrieve (locals f) src;
89      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
90      ! locals ← reg_store dst v' (locals f);
91      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
92  | St_op2 _ _ _  op dst src1 src2 l ⇒ λH.
93      ! v1 ← reg_retrieve (locals f) src1;
94      ! v2 ← reg_retrieve (locals f) src2;
95      ! v' ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
96      ! locals ← reg_store dst v' (locals f);
97      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
98  | St_load chunk addr dst l ⇒ λH.
99      ! vaddr ← reg_retrieve (locals f) addr;
100      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
101      ! locals ← reg_store dst v (locals f);
102      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
103  | St_store chunk addr src l ⇒ λH.
104      ! vaddr ← reg_retrieve (locals f) addr;
105      ! v ← reg_retrieve (locals f) src;
106      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
107      return 〈E0, build_state f fs m' l ?〉
108  | St_call_id id args dst l ⇒ λH.
109      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id);
110      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b);
111      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
112      return 〈E0, Callstate id fd vs dst (adv l f ?::fs) m〉
113  | St_call_ptr frs args dst l ⇒ λH.
114      ! fv ← reg_retrieve (locals f) frs;
115      ! 〈fd,id〉 ← opt_to_res … (msg BadFunction) (find_funct_id … ge fv);
116      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
117      return 〈E0, Callstate id fd vs dst (adv l f ?::fs) m〉
118(*
119  | St_tailcall_id id args ⇒ λH.
120      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id);
121      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b);
122      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
123      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
124  | St_tailcall_ptr frs args ⇒ λH.
125      ! fv ← reg_retrieve (locals f) frs;
126      ! fd ← opt_to_res … (msg BadFunction) (find_funct … ge fv);
127      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
128      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
129*)
130  | St_cond src ltrue lfalse ⇒ λH.
131      ! v ← reg_retrieve (locals f) src;
132      ! b ← eval_bool_of_val v;
133      return 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
134(*
135  | St_jumptable r ls ⇒ λH.
136      ! v ← reg_retrieve (locals f) r;
137      match v with
138      [ Vint _ i ⇒
139          match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with
140          [ None ⇒ λ_. Error ? (msg BadJumpTable)
141          | Some l ⇒ λE. return 〈E0, build_state f fs m l ?〉
142          ] (refl ??)
143      | _ ⇒ Error ? (msg BadJumpValue)
144      ]
145*)
146  | St_return ⇒ λH.
147      ! v ← match f_result (func f) with
148            [ None ⇒ return (None ?)
149            | Some rt ⇒
150                let 〈r,ty〉 ≝ rt in
151                ! v ← reg_retrieve (locals f) r;
152                return (Some ? v)
153            ];
154      return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
155  ] (f_closed (func f) (next f) s ?)
156| Callstate _ fd params dst fs m ⇒
157    match fd return λ_. IO ??? with
158    [ Internal fn ⇒
159        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
160        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
161           here *)
162        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) (* XData *) in
163        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
164    | External fn ⇒
165        ! evargs ← err_to_io … (check_eventval_list params (sig_args (ef_sig fn)));
166        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
167        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
168    ]
169| Returnstate v dst fs m ⇒
170    match fs with
171    [ nil ⇒
172        match v with
173        [ Some v' ⇒
174          match v' with
175          [ Vint sz r ⇒ match sz return λsz. bvint sz → monad Res ? with
176                        [ I32 ⇒ λr. return 〈E0, Finalstate r〉
177                        | _ ⇒ λ_. Error ? (msg ReturnMismatch)
178                        ] r
179          | _ ⇒ Error ? (msg ReturnMismatch)
180          ]
181        | _ ⇒ Error ? (msg ReturnMismatch)
182        ]
183    | cons f fs' ⇒
184        ! locals ← match dst with
185                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
186                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
187                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
188                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
189        return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
190    ]
191| Finalstate r ⇒ Error ? (msg FinalState) (* Already in final state *)
192]. try @(next_ok f) try @lookup_lookup_present try @H
193[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
194| cases (f_entry fn) //
195] qed.
196
197definition RTLabs_is_final : state → option int ≝
198λs. match s with
199[ Finalstate r ⇒ Some ? r
200| _ ⇒ None ?
201].
202
203definition RTLabs_exec : trans_system io_out io_in ≝
204  mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement.
205
206definition make_global : RTLabs_program → genv ≝
207λp. globalenv … (λx.[Init_space x]) p.
208
209definition make_initial_state : RTLabs_program → res state ≝
210λp.
211  let ge ≝ make_global p in
212  do m ← init_mem … (λx.[Init_space x]) p;
213  let main ≝ prog_main ?? p in
214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
215  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
216  OK ? (Callstate main f (nil ?) (None ?) (nil ?) m).
217
218definition RTLabs_fullexec : fullexec io_out io_in ≝
219  mk_fullexec … RTLabs_exec make_global make_initial_state.
220
221
222(* Some lemmas about the semantics. *)
223
224(* Note parts of frames and states that are preserved. *)
225
226inductive frame_rel : frame → frame → Prop ≝
227| mk_frame_rel :
228  ∀func,locals,next,next_ok,sp,retdst,locals',next',next_ok'. frame_rel
229   (mk_frame func locals next next_ok sp retdst)
230   (mk_frame func locals' next' next_ok' sp retdst)
231.
232
233inductive state_rel : genv → state → state → Prop ≝
234| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
235| to_call : ∀ge,f,fs,m,vf,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate vf fd args dst (f'::fs) m)
236(*
237| tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m')
238*)
239| from_call : ∀ge,vf,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate vf (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m')
240| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
241| from_ret : ∀ge,f,fs,rtv,dst,f',m. next f = next f' → frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
242| finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r)
243.
244
245lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Type[0].
246  (∀a. e = OK A a → f a = OK ? v → P v) →
247  (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v).
248#A #B *
249[ #a #f #v #P #H #E whd in E:(??%?); @(H a) //
250| #m #f #v #P #H #E whd in E:(??%?); destruct
251] qed.
252
253lemma eval_preserves : ∀ge,s,tr,s'.
254  eval_statement ge s = Value ??? 〈tr,s'〉 →
255  state_rel ge s s'.
256#ge *
257[ * #func #locals #next #next_ok #sp #retdst #fs #m
258  #tr #s'
259  whd in ⊢ (??%? → ?);
260  generalize in ⊢ (??(?%)? → ?);
261  cases (next_instruction ?)
262  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
263  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
264  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
265  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
266  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
267  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
268  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
269  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ???) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
270  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok * #fd #fid #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ? Efd) #b * #Ev' #Efn %2 [ % | @b | @Efn ]
271(*
272  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
273  | #r #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
274*)
275  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
276(*  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: [ 1,3: #vl ] #E whd in E:(??%?); destruct ]*)
277  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4
278  ]
279| #vf * #fn #args #retdst #stk #m #tr #s'
280  whd in ⊢ (??%? → ?);
281  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
282    #E destruct %3
283  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
284  ]
285| #v #r * [2: #f #fs ] #m #tr #s'
286  whd in ⊢ (??%? → ?);
287  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
288    %5 cases f #func #locals #next #next_ok #sp #retdst %
289  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct // | *: normalize #a try #b destruct ] ]
290  ]
291| #r #tr #s' normalize #E destruct
292] qed.
293
294(* Show that, in principle at least, we can calculate which function we called
295   on a transition. The proof is a functional inversion similar to eval_preserves,
296   above.  Note: this was originally done before the value was added to
297   Callstate. *)
298
299(* Hack due to lack of discriminator for large inductive types *)
300lemma jmeq_hackT : ∀T:Type[0]. ∀x,y:T. ∀P:Type[0].
301  (x ≃ y → P) →
302  (x = y → P).
303/2/
304qed.
305
306definition func_block_of_exec : ∀ge,s,t,fid,fd,args,dst,fs,m.
307  eval_statement ge s = Value ??? 〈t,Callstate fid fd args dst fs m〉 →
308  Σb:block. find_symbol … ge fid = Some ? b ∧ find_funct_ptr … ge b = Some ? fd.
309#ge *
310[ * #func #locals #next #nok #sp #dst #fs #m #tr #fid #fd #args #dst' #fs' #m'
311  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
312  cases (next_instruction ?)
313  (* Function call cases. *)
314  [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs @jmeq_hackT #E normalize in E; destruct
315    [ %{v} % assumption
316    | cases v in Efd;
317      [ 4: * #b #off cases fd' #fd'' #fid' #Efd %{b} cases (find_funct_id_ptr ????? Efd) #b' * * #E destruct #FS #FFPI %{FS} @FFPI
318      | *: normalize #A try #B try #C destruct
319      ]
320    ]
321  (* and everything else cannot occur, but we need to work through the
322     definition to find the resulting state to demonstrate that. *)
323  | #l #LP whd in ⊢ (??%? → ?); @jmeq_hackT #E destruct
324  | #c #l #LP whd in ⊢ (??%? → ?); @jmeq_hackT #E destruct
325  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
326  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
327  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
328  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
329  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
330  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb @jmeq_hackT #E whd in E:(??%??); destruct
331(*  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct ] | *: [1,3: #vl] #E whd in E:(??%?); destruct ]*)
332  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); @jmeq_hackT #E' whd in E':(??%??); destruct
333  ]
334| #vf * #fn #args #retdst #stk #m #tr #vf' #fd' #args' #dst' #fs' #m'
335  whd in ⊢ (??%? → ?);
336  [ @bind_res_value #loc #Eloc cases (alloc m O ?(*?*)) #m' #b whd in ⊢ (??%? → ?);
337    @jmeq_hackT #E destruct
338  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
339  ]
340| #v #r * [2: #f #fs ] #m #tr #vf' #fd' #args' #dst' #fs' #m'
341  whd in ⊢ (??%? → ?);
342  [ @bind_res_value #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
343  | cases v [ normalize #E destruct | * [ 2: * #r normalize @jmeq_hackT #E destruct | *: normalize #a try #b destruct ] ]
344  ]
345| #r #tr #vf' #fd' #args' #dst' #fs' #m'
346  normalize #E destruct
347] qed.
348
349lemma final_cannot_move : ∀ge,s.
350  RTLabs_is_final s ≠ None ? →
351  ∃err. eval_statement ge s = Wrong ??? err.
352#ge *
353[ #f #fs #m * #F cases (F ?) @refl
354| #a #b #c #d #e #f * #F cases (F ?) @refl
355| #a #b #c #d * #F cases (F ?) @refl
356| #r #F % [2: @refl | skip ]
357] qed.
358
359lemma step_not_final : ∀ge,s,tr,s'.
360  eval_statement ge s = Value … 〈tr,s'〉 →
361  RTLabs_is_final s = None ?.
362#ge #s #tr #s' #EX
363lapply (final_cannot_move ge s)
364cases (RTLabs_is_final s)
365[ // | #r #F cases (F ?) [ #m #E >E in EX; #EX destruct | % #E destruct ]
366qed.
367
368lemma initial_state_is_not_final : ∀p,s.
369  make_initial_state p = OK ? s →
370  RTLabs_is_final s = None ?.
371#p #s whd in ⊢ (??%? → ?);
372@bind_ok #m #Em
373@bind_ok #b #Eb
374@bind_ok #f #Ef
375#E destruct
376@refl
377qed.
Note: See TracBrowser for help on using the repository browser.