source: src/RTLabs/semantics.ma @ 2499

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

Separate out the RTLabs abstract status record from the proofs about
structured traces. Tidy up "next instruction" references from
the semantics.

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/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.