source: src/joint/semantics_paolo.ma @ 1651

Last change on this file since 1651 was 1643, checked in by tranquil, 8 years ago
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File size: 19.9 KB
Line 
1include "basics/lists/list.ma".
2include "joint/BEGlobalenvs.ma".
3include "common/IO.ma".
4include "common/SmallstepExec.ma".
5include "joint/Joint_paolo.ma".
6include "ASM/I8051bis.ma".
7
8(* CSC: external functions never fail (??) and always return something of the
9   size of one register, both in the frontend and in the backend.
10   Is this reasonable??? In OCaml it always return a list, but in the frontend
11   only the head is kept (or Undef if the list is empty) ??? *)
12
13definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
14
15record sem_state_params : Type[1] ≝
16 { framesT: Type[0]
17 ; empty_framesT: framesT
18 ; regsT : Type[0]
19 ; empty_regsT: address → regsT (* Stack pointer *)
20 }.
21 
22record state (semp: sem_state_params): Type[0] ≝
23 { st_frms: framesT semp
24 ; pc: address
25 ; sp: pointer
26 ; isp: pointer
27 ; carry: beval
28 ; regs: regsT semp
29 ; m: bemem
30 }.
31 
32definition set_m: ∀p. bemem → state p → state p ≝
33 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
34
35definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
36 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
37
38definition set_sp: ∀p. pointer → state p → state p ≝
39 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
40
41definition set_isp: ∀p. pointer → state p → state p ≝
42 λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
43
44definition set_carry: ∀p. beval → state p → state p ≝
45 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
46
47definition set_pc: ∀p. address → state p → state p ≝
48 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
49
50definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
51 λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
52
53axiom BadProgramCounter : String.
54(* this can replace graph_fetch function and lin_fetch_function *)
55definition fetch_function:
56 ∀pars : params.
57 ∀globals.
58  genv globals pars →
59  pointer →
60  res (joint_internal_function … pars) ≝
61 λpars,globals,ge,p.
62  let b ≝ pblock p in
63  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
64  match def with
65  [ Internal def' ⇒ OK … def'
66  | External _ ⇒ Error … [MSG BadProgramCounter]].
67 
68record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
69  { st_pars :> sem_state_params
70  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
71  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
72  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
73  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
74  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
75  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
76  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
77  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
78  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
79  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
80  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
81  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
82  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
83  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
84  ; fetch_ra: state st_pars →
85      res ((state st_pars) × address)
86
87  ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
88  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
89  ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars
90   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
91     type of arguments. To be fixed using a dependent type *)
92  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
93      state st_pars → res (state st_pars)
94  ; fetch_external_args: external_function → state st_pars →
95      res (list val)
96  ; set_result: list val → state st_pars →
97      res (state st_pars)
98  ; call_args_for_main: call_args uns_pars
99  ; call_dest_for_main: call_dest uns_pars
100 }.
101
102
103definition helper_def_retrieve :
104  ∀X : ? → ? → Type[0].
105  (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) →
106  ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝
107    λX,f,up,p,st.f ? p (regs … st).
108
109definition helper_def_store :
110  ∀X : ? → ? → Type[0].
111  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
112  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
113  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).
114
115definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
116definition acca_store ≝ helper_def_store ? acca_store_.
117definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
118definition accb_store ≝ helper_def_store ? accb_store_.
119definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
120definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
121definition dpl_store ≝ helper_def_store ? dpl_store_.
122definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
123definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
124definition dph_store ≝ helper_def_store ? dph_store_.
125definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
126definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
127definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
128definition pair_reg_move : ?→?→?→?→res ? ≝
129  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
130    ! r ← pair_reg_move_ ? p (regs ? st) pm;
131    return (set_regs ? r st).
132
133axiom BadPointer : String.
134
135(* this is preamble to all calls (including tail ones). The optional argument in
136   input tells the function whether it has to save the frame for internal
137   calls.
138   the first element of the triple is the label at the start of the function
139   in case of an internal call, or None in case of an external one.
140   The actual update of the pc is left to later, as it depends on
141   serialization and on whether the call is a tail one. *)
142definition eval_call_block_preamble:
143 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
144  genv globals p → state p' → block → call_args p → option ((call_dest p) × address) →
145    IO io_out io_in ((option label)×trace×(state p')) ≝
146 λglobals,p,p',ge,st,b,args,dest_ra.
147  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
148    match fd with
149    [ Internal fn ⇒
150      let st ≝ match dest_ra with
151        [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st
152        | None ⇒ st
153        ] in
154      ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
155              args st ;
156      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
157      let l' ≝ joint_if_entry … fn in
158      let st ≝ set_regs p' regs st in
159      return 〈Some label l', E0, st〉
160    | External fn ⇒
161      ! params ← fetch_external_args … p' fn st : IO ???;
162      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
163      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
164      (* CSC: XXX bug here; I think I should split it into Byte-long
165         components; instead I am making a singleton out of it. To be
166         fixed once we fully implement external functions. *)
167      let vs ≝ [mk_val ? evres] in
168      ! st ← set_result … p' vs st : IO ???;
169      return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
170      ].
171
172axiom FailedStore: String.
173
174definition push: ∀p. state p → beval → res (state p) ≝
175 λp,st,v.
176  let isp ≝ isp … st in
177  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
178  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
179  OK … (set_m … m (set_sp … isp st)).
180
181definition pop: ∀p. state p → res (state p × beval) ≝
182 λp,st.
183  let isp ≝ isp ? st in
184  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
185  let ist ≝ set_sp … isp st in
186  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
187  OK ? 〈st,v〉.
188
189definition save_ra : ∀p. state p → address → res (state p) ≝
190 λp,st,l.
191  let 〈addrl,addrh〉 ≝ l in
192  do st ← push … st addrl;
193  push … st addrh.
194
195definition load_ra : ∀p.state p → res (state p × address) ≝
196 λp,st.
197  do 〈st,addrh〉 ← pop … st;
198  do 〈st,addrl〉 ← pop … st;
199  OK ? 〈st, 〈addrl,addrh〉〉.
200
201
202(* parameters that need full params to have type of functions,
203   but are still independent of serialization
204   Paolo: the first element returned by exec extended is None if flow is
205   left to regular sequential one, otherwise a label.
206   The address input is the address of the next statement, to be provided to
207   accomodate extensions that make calls. *)
208record more_sem_genv_params (pp : params) : Type[1] ≝
209  { msu_pars :> more_sem_unserialized_params pp
210  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
211  ; exec_extended: ∀globals.genv globals pp → ext_instruction pp →
212      state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars))
213  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp →
214      state msu_pars → IO io_out io_in (trace × (state msu_pars))
215  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
216  }.
217 
218
219(* parameters that are defined by serialization *)
220record more_sem_params (pp : params) : Type[1] ≝
221  { msg_pars :> more_sem_genv_params pp
222  ; succ_pc: succ pp → address → res address
223  ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code)
224  ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals)
225  }.
226
227record sem_params : Type[1] ≝
228  { spp :> params
229  ; more_sem_pars :> more_sem_params spp
230  }.
231
232definition address_of_label: ∀globals. ∀p:sem_params.
233  genv globals p → pointer → label → res address ≝
234 λglobals,p,ge,ptr,l.
235  do newptr ← pointer_of_label … p ? ge … ptr l ;
236  OK … (address_of_code_pointer newptr).
237
238definition goto: ∀globals. ∀p:sem_params.
239  genv globals p → label → state p → res (state p) ≝
240 λglobals,p,ge,l,st.
241  ! oldpc ← pointer_of_address (pc … st);
242  ! newpc ← address_of_label … ge oldpc l ;
243  OK (state p) (set_pc … newpc st).
244
245(*
246definition empty_state: ∀p. more_sem_params p → state p ≝
247 mk_state … (empty_framesT …)
248*)
249
250definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
251 λp,l,st.
252  ! l' ← succ_pc … p l (pc … st) ;
253  OK … (set_pc … l' st).
254
255axiom MissingSymbol : String.
256axiom FailedLoad : String.
257axiom BadFunction : String.
258
259definition eval_call_block:
260 ∀globals.∀p:sem_params. genv globals p → state p →
261  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
262 λglobals,p,ge,st,b,args,dest,ra.
263 ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ;
264 ! new_pc ← match next with
265  [ Some lbl ⇒
266    let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
267    address_of_label globals p ge pointer_in_fn lbl
268  | None ⇒ return ra
269  ] ;
270 let st ≝ set_pc … new_pc st in
271 return 〈tr, st〉.
272% qed.
273
274definition eval_call_id:
275 ∀globals.∀p:sem_params. genv globals p → state p →
276  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
277 λglobals,p,ge,st,id,args,dest,ra.
278  ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
279  eval_call_block … ge st b args dest ra.
280
281
282(* defining because otherwise typechecker stalls *)
283definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p →
284  ∀i : ident.member i (eq_identifier SymbolTag) globals
285     →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝
286     λglobals,p,ge,st,ident,prf,ldest,hdest,l.
287     let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
288     ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
289     ! st ← dpl_store … ldest laddr st;
290     ! st ← dph_store … hdest haddr st;
291     ! st ← next … p l st ;
292     return 〈E0, st〉.
293  [ cases addr //
294  | (* TODO: to prove *)
295    elim daemon
296  ] qed.
297
298(* defining because otherwise typechecker stalls *)
299definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p →
300  acc_a_reg p → succ p → res (trace × (state p)) ≝
301  λglobals,p,ge,st,dst,l.
302        ! 〈st,v〉 ← pop p st;
303        ! st ← acca_store p p dst v st;
304        ! st ← next p l st ;
305        return 〈E0, st〉.
306
307(* defining because otherwise typechecker stalls *)
308definition eval_sequential :
309 ∀globals.∀p:sem_params. genv globals p → state p →
310  joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
311 λglobals,p,ge,st,seq,l.
312  match seq with
313  [ extension c ⇒
314    ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ;
315    ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr;
316    ! st ← match next_pc with
317      [ None ⇒ next … p l st
318      | Some lbl ⇒ goto … ge lbl st
319      ] ;
320    return 〈tr, st〉
321  | COST_LABEL cl ⇒
322    ! st ← next … p l st ;
323    return 〈Echarge cl, st〉
324  | COMMENT c ⇒
325    ! st ← next … p l st ;
326    return 〈E0, st〉
327  | LOAD dst addrl addrh ⇒
328    ! vaddrh ← dph_arg_retrieve … st addrh ;
329    ! vaddrl ← dpl_arg_retrieve … st addrl;
330    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
331    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
332    ! st ← acca_store p … dst v st ;
333    ! st ← next … p l st ;
334    return 〈E0, st〉
335  | STORE addrl addrh src ⇒
336    ! vaddrh ← dph_arg_retrieve … st addrh;
337    ! vaddrl ← dpl_arg_retrieve … st addrl;
338    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
339    ! v ← acca_arg_retrieve … st src;
340    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
341    let st ≝ set_m … m' st in
342    ! st ← next … p l st ;
343    return 〈E0, st〉
344  | COND src ltrue ⇒
345    ! v ← acca_retrieve … st src;
346    ! b ← bool_of_beval v;
347    if b then
348     ! st ← goto … p ge ltrue st ;
349     return 〈E0, st〉
350    else
351     ! st ← next … p l st ;
352     return 〈E0, st〉
353  | ADDRESS ident prf ldest hdest ⇒
354    eval_address … ge st ident prf ldest hdest l
355  | OP1 op dacc_a sacc_a ⇒
356    ! v ← acca_retrieve … st sacc_a;
357    ! v ← Byte_of_val v;
358    let v' ≝ BVByte (op1 eval op v) in
359    ! st ← acca_store … dacc_a v' st;
360    ! st ← next … l st ;
361    return 〈E0, st〉
362  | OP2 op dacc_a sacc_a src ⇒
363    ! v1 ← acca_arg_retrieve … st sacc_a;
364    ! v1 ← Byte_of_val v1;
365    ! v2 ← snd_arg_retrieve … st src;
366    ! v2 ← Byte_of_val v2;
367    ! carry ← bool_of_beval (carry … st);
368      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
369      let v' ≝ BVByte v' in
370      let carry ≝ beval_of_bool carry in
371    ! st ← acca_store … dacc_a v' st;
372      let st ≝ set_carry … carry st in
373    ! st ← next … l st ;
374    return 〈E0, st〉
375  | CLEAR_CARRY ⇒
376    ! st ← next … l (set_carry … BVfalse st) ;
377    return 〈E0, st〉
378  | SET_CARRY ⇒
379    ! st ← next … l (set_carry … BVtrue st) ;
380    return 〈E0, st〉
381  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
382    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
383    ! v1 ← Byte_of_val v1;
384    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
385    ! v2 ← Byte_of_val v2;
386    let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
387    let v1' ≝ BVByte v1' in
388    let v2' ≝ BVByte v2' in
389    ! st ← acca_store … dacc_a_reg v1' st;
390    ! st ← accb_store … dacc_b_reg v2' st;
391    ! st ← next … l st ;
392    return 〈E0, st〉
393  | POP dst ⇒
394    eval_pop … ge st dst l
395  | PUSH src ⇒
396    ! v ← acca_arg_retrieve … st src;
397    ! st ← push … st v;
398    ! st ← next … l st ;
399    return 〈E0, st〉
400  | MOVE dst_src ⇒
401    ! st ← pair_reg_move … st dst_src ;
402    ! st ← next … l st ;
403    return 〈E0, st〉
404  | CALL_ID id args dest ⇒
405    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
406    eval_call_id … ge st id args dest ra
407  ].
408
409definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
410  state p → IO io_out io_in (trace × (state p)) ≝
411 λglobals,p,ge,st.
412  ! s ← fetch_statement … ge st : IO ???;
413  match s return λ_.IO io_out io_in (trace × (state p)) with
414    [ GOTO l ⇒
415       ! st ← goto … ge l st ;
416       return 〈E0, st〉
417    | RETURN ⇒
418      ! 〈st,ra〉 ← fetch_ra … st ;
419      ! st ← pop_frame … ge st;
420      return 〈E0,set_pc … ra st〉
421   | sequential seq l ⇒ eval_sequential … ge st seq l
422   | extension_fin c ⇒ exec_fin_extended … ge c st
423   ].
424
425definition is_final: ∀globals:list ident. ∀p: sem_params.
426  genv globals p → address → state p → option int ≝
427 λglobals,p,ge,exit,st.res_to_opt ? (
428  do s ← fetch_statement … ge st;
429  match s with
430   [ RETURN ⇒
431      do 〈st,ra〉 ← fetch_ra … st;
432      if eq_address ra exit then
433       do vals ← read_result … ge st ;
434       Word_of_list_beval vals
435      else
436       Error ? [ ]
437   | _ ⇒ Error ? [ ]]).
438
439record evaluation_parameters : Type[1] ≝
440 { globals: list ident
441 ; sparams:> sem_params
442 ; exit: address
443 ; genv2: genv globals sparams
444 }.
445
446definition joint_exec: trans_system io_out io_in ≝
447  mk_trans_system … evaluation_parameters (λG. state G)
448   (λG.is_final (globals G) G (genv2 G) (exit G))
449   (λG.eval_statement (globals G) G (genv2 G)).
450
451definition make_global :
452 ∀pars: sem_params.
453  joint_program pars → evaluation_parameters
454
455 λpars.
456 (* Invariant: a -1 block is unused in common/Globalenvs *)
457 let b ≝ mk_block Code (-1) in
458 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
459 let addr ≝ address_of_code_pointer ptr in
460  (λp. mk_evaluation_parameters
461    (prog_var_names … p)
462    (mk_sem_params … pars)
463    addr
464    (globalenv Genv … p)
465  ).
466% qed.
467
468axiom ExternalMain: String.
469
470definition make_initial_state :
471 ∀pars: sem_params.
472 ∀p: joint_program … pars. res (state pars) ≝
473λpars,p.
474  let sem_globals ≝ make_global pars p in
475  let ge ≝ genv2 sem_globals in
476  let m ≝ init_mem Genv … p in
477  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
478  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
479  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
480  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
481  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
482  do sp ← address_of_pointer spp ;
483  let main ≝ prog_main … p in
484  let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
485  let trace_state ≝
486   eval_call_id … pars ge st0 main (call_args_for_main … pars)
487    (call_dest_for_main … pars) (exit sem_globals) in
488  match trace_state with
489  [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
490  | Wrong msg ⇒ Error … msg
491  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
492  ].
493[3: % | cases ispb | cases spb] * #r #off #E >E %
494qed.
495
496definition joint_fullexec :
497 ∀pars:sem_params.fullexec io_out io_in ≝
498 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
Note: See TracBrowser for help on using the repository browser.