source: src/RTLabs/RTLabs_semantics.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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