source: src/joint/semantics.ma @ 1457

Last change on this file since 1457 was 1457, checked in by sacerdot, 8 years ago

Bug fixed: when calling an internal function, the pc block is now set to
the block allocated for the internal function. However, so far this was
not an invariant used inside joint/semantics.ma, but only in the instantiation
of the different languages.

File size: 18.3 KB
RevLine 
[1173]1include "utilities/lists.ma".
[1408]2include "joint/BEGlobalenvs.ma".
[1173]3include "common/IO.ma".
4include "common/SmallstepExec.ma".
5include "joint/Joint.ma".
[1415]6include "ASM/I8051bis.ma".
[1213]7
[1173]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
[1289]13record more_sem_params (p:params_): Type[1] ≝
[1233]14 { framesT: Type[0]
[1408]15 ; empty_framesT: framesT
[1281]16 ; regsT: Type[0]
[1415]17 ; empty_regsT: address → regsT (* Stack pointer *)
[1408]18 ; call_args_for_main: call_args p
19 ; call_dest_for_main: call_dest p
[1233]20
[1213]21 ; greg_store_: generic_reg p → beval → regsT → res regsT
22 ; greg_retrieve_: regsT → generic_reg p → res beval
23 ; acca_store_: acc_a_reg p → beval → regsT → res regsT
24 ; acca_retrieve_: regsT → acc_a_reg p → res beval
25 ; accb_store_: acc_b_reg p → beval → regsT → res regsT
26 ; accb_retrieve_: regsT → acc_b_reg p → res beval
27 ; dpl_store_: dpl_reg p → beval → regsT → res regsT
28 ; dpl_retrieve_: regsT → dpl_reg p → res beval
29 ; dph_store_: dph_reg p → beval → regsT → res regsT
30 ; dph_retrieve_: regsT → dph_reg p → res beval
[1294]31 ; pair_reg_move_: regsT → pair_reg p → res regsT
[1173]32 }.
33
[1233]34record sem_params: Type[1] ≝
[1247]35 { spp :> params_
[1233]36 ; more_sem_pars :> more_sem_params spp
37 }.
[1217]38
[1173]39record state (p: sem_params): Type[0] ≝
[1233]40 { st_frms: framesT ? p
[1173]41 ; pc: address
[1215]42 ; sp: pointer
[1430]43 ; isp: pointer
[1213]44 ; carry: beval
[1233]45 ; regs: regsT ? p
[1213]46 ; m: bemem
[1173]47 }.
48
[1408]49(*
50definition empty_state: ∀p. more_sem_params p → state p ≝
51 mk_state … (empty_framesT …)
52*)
53
[1247]54definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
[1176]55
[1411]56record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] ≝
57 { more_sparams :> more_sem_params p
[1289]58
[1451]59 (*CSC: XXXX succ_pc, pointer_of_label and fetch_statement all deal with fetching
60   should we take 'em out in a different record to simplify the code? *)
61 ; succ_pc: succ p → address → res address
62 ; pointer_of_label: genv … p → pointer → label → res (Σp:pointer. ptype p = Code)
[1411]63 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
[1384]64
[1411]65 ; fetch_ra: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
66 ; result_regs: genv globals p → state (mk_sem_params … more_sparams) → res (list (generic_reg p))
[1294]67
[1411]68 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
[1386]69   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
70     type of arguments. To be fixed using a dependent type *)
[1411]71 ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
72 ; pop_frame: genv globals p → state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))
[1385]73
[1411]74 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
75 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
76 }.
[1186]77
[1411]78record sem_params1 (globals: list ident): Type[1] ≝
79 { p1:> params globals
80 ; more_sparams1:> more_sem_params1 globals p1
[1176]81 }.
82
[1411]83record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
84 { more_sparams_1 :> more_sem_params1 … p
85 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams_1) → succ p → state (mk_sem_params … more_sparams_1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams_1)))
86 }.
87
[1233]88record sem_params2 (globals: list ident): Type[1] ≝
[1247]89 { p2:> params globals
90 ; more_sparams2:> more_sem_params2 globals p2
[1233]91 }.
92
[1411]93definition sem_params_of_sem_params1 ≝ λglobals. λsp1: sem_params1 globals. mk_sem_params sp1 sp1.
94coercion sem_params_of_sem_params1 : ∀globals. ∀_x:sem_params1 globals. sem_params
95 ≝ sem_params_of_sem_params1 on _x: sem_params1 ? to sem_params.
[1386]96
[1411]97definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 … sp2 sp2.
98coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1 globals
99 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1 ?.
100
[1213]101definition set_m: ∀p. bemem → state p → state p ≝
[1430]102 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
[1173]103
[1233]104definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
[1430]105 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
[1173]106
[1215]107definition set_sp: ∀p. pointer → state p → state p ≝
[1430]108 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
[1173]109
[1430]110definition set_isp: ∀p. pointer → state p → state p ≝
111 λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
112
[1213]113definition set_carry: ∀p. beval → state p → state p ≝
[1430]114 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
[1173]115
116definition set_pc: ∀p. address → state p → state p ≝
[1430]117 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
[1173]118
[1233]119definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
[1430]120 λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
[1174]121
[1173]122
[1451]123definition address_of_label: ∀globals. ∀p:sem_params1 globals. genv globals p → pointer → label → res address ≝
124 λglobals,p,ge,ptr,l.
125  do newptr ← pointer_of_label … p ge … ptr l ;
126  OK … (address_of_code_pointer newptr).
127
128definition goto: ∀globals. ∀p:sem_params1 globals. genv globals p → label → state p → res (state p) ≝
129 λglobals,p,ge,l,st.
130  do oldpc ← pointer_of_address (pc … st) ;
131  do newpc ← address_of_label … ge oldpc l ;
132  OK … (set_pc … newpc st).
133
134definition next: ∀globals. ∀p:sem_params1 globals. succ … p → state p → res (state p) ≝
135 λglobals,p,l,st.
136  do l' ← succ_pc … p l (pc … st) ;
[1382]137  OK … (set_pc … l' st).
[1233]138
[1213]139definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
[1173]140 λp,dst,v,st.
[1213]141  do regs  ← greg_store_ … dst v (regs … st);
142  OK ? (set_regs … regs st).
[1173]143
[1213]144definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
[1173]145 λp,st,dst.greg_retrieve_ … (regs … st) dst.
146
[1213]147definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
[1173]148 λp,dst,v,st.
[1213]149  do regs ← acca_store_ … dst v (regs … st);
150  OK ? (set_regs … regs st).
[1173]151
[1213]152definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
[1173]153 λp,st,dst.acca_retrieve_ … (regs … st) dst.
154
[1213]155definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
[1173]156 λp,dst,v,st.
[1213]157  do regs ← accb_store_ … dst v (regs … st);
158  OK ? (set_regs … regs st).
[1173]159
[1213]160definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
[1173]161 λp,st,dst.accb_retrieve_ … (regs … st) dst.
162
[1213]163definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
[1173]164 λp,dst,v,st.
[1213]165  do regs ← dpl_store_ … dst v (regs … st);
166  OK ? (set_regs … regs st).
[1173]167
[1213]168definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
[1173]169 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
170
[1213]171definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
[1173]172 λp,dst,v,st.
[1213]173  do regs ← dph_store_ … dst v (regs … st);
174  OK ? (set_regs … regs st).
[1173]175
[1213]176definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
[1173]177 λp,st,dst.dph_retrieve_ … (regs … st) dst.
178
[1294]179definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → res (state p) ≝
180 λp,st,rs.
181  do regs ← pair_reg_move_ … (regs … st) rs;
182  OK … (set_regs … regs st).
[1173]183
184axiom FailedStore: String.
185
[1215]186definition push: ∀p. state p → beval → res (state p) ≝
[1173]187 λp,st,v.
[1430]188  let isp ≝ isp … st in
189  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
190  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
191  OK … (set_m … m (set_sp … isp st)).
[1173]192
[1215]193definition pop: ∀p. state p → res (state p × beval) ≝
[1173]194 λp,st.
[1430]195  let isp ≝ isp ? st in
196  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
197  let ist ≝ set_sp … isp st in
198  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
[1215]199  OK ? 〈st,v〉.
[1173]200
[1377]201definition save_ra : ∀p. state p → address → res (state p) ≝
[1174]202 λp,st,l.
[1377]203  let 〈addrl,addrh〉 ≝ l in
[1214]204  do st ← push … st addrl;
205  push … st addrh.
[1173]206
[1384]207definition load_ra : ∀p.state p → res (state p × address) ≝
[1176]208 λp,st.
[1214]209  do 〈st,addrh〉 ← pop … st;
210  do 〈st,addrl〉 ← pop … st;
211  OK ? 〈st, 〈addrl,addrh〉〉.
[1176]212
[1173]213axiom MissingSymbol : String.
214axiom FailedLoad : String.
215axiom BadFunction : String.
[1408]216axiom BadPointer : String.
[1173]217
[1408]218definition eval_call_block:
[1411]219 ∀globals.∀p:sem_params1 globals. genv globals p → state p →
[1408]220  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
221 λglobals,p,ge,st,b,args,dest,ra.
222  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
223    match fd with
224    [ Internal fn ⇒
225      ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
226      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
227      let l' ≝ joint_if_entry … fn in
[1457]228      let st ≝ set_regs p regs st in
229      let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
230      ! newpc ← address_of_label … ge pointer_in_fn l' ;
231      let st ≝ set_pc … newpc st in
[1451]232       ret ? 〈 E0, st〉
[1408]233    | External fn ⇒
234      ! params ← fetch_external_args … fn st;
235      ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
236      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
237      (* CSC: XXX bug here; I think I should split it into Byte-long
238         components; instead I am making a singleton out of it. To be
239         fixed once we fully implement external functions. *)
[1457]240      let vs ≝ [mk_val ? evres] in
[1408]241      ! st ← set_result … vs st;
242      let st ≝ set_pc … ra st in
243        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
244     ].
[1457]245% qed.
[1408]246
247definition eval_call_id:
[1411]248 ∀globals.∀p:sem_params1 globals. genv globals p → state p →
[1408]249  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
250 λglobals,p,ge,st,id,args,dest,ra.
251  ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
252  eval_call_block … ge st b args dest ra.
253 
[1247]254definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
[1233]255 λglobals,p,ge,st.
[1298]256  ! s ← fetch_statement … ge st;
[1173]257  match s with
[1451]258    [ GOTO l ⇒
259       ! st ← goto … p ge l st ;
260       ret ? 〈E0, st〉
[1289]261    | sequential seq l ⇒
[1173]262      match seq with
[1324]263      [ extension c ⇒ exec_extended … p ge c l st
[1382]264      | COST_LABEL cl ⇒
[1451]265         ! st ← next … p l st ;
[1382]266         ret ? 〈Echarge cl, st〉
267      | COMMENT c ⇒
[1451]268         ! st ← next … p l st ;
[1382]269         ret ? 〈E0, st〉
[1289]270      | INT dest v ⇒
[1382]271         ! st ← greg_store p dest (BVByte v) st;
[1451]272         ! st ← next … p l st ;
[1382]273          ret ? 〈E0, st〉
[1289]274      | LOAD dst addrl addrh ⇒
[1173]275        ! vaddrh ← dph_retrieve … st addrh;
276        ! vaddrl ← dpl_retrieve … st addrl;
[1329]277        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
[1213]278        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
[1289]279        ! st ← acca_store p … dst v st;
[1451]280        ! st ← next … p l st ;
[1382]281          ret ? 〈E0, st〉
[1289]282      | STORE addrl addrh src ⇒
[1174]283        ! vaddrh ← dph_retrieve … st addrh;
284        ! vaddrl ← dpl_retrieve … st addrl;
[1329]285        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
[1174]286        ! v ← acca_retrieve … st src;
[1213]287        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
[1382]288        let st ≝ set_m … m' st in
[1451]289        ! st ← next … p l st ;
[1382]290          ret ? 〈E0, st〉
[1289]291      | COND src ltrue ⇒
[1174]292        ! v ← acca_retrieve … st src;
[1213]293        ! b ← bool_of_beval v;
[1382]294        if b then
[1451]295         ! st ← goto … p ge ltrue st ;
296         ret ? 〈E0, st〉
[1382]297        else
[1451]298         ! st ← next … p l st ;
[1382]299         ret ? 〈E0, st〉
[1289]300      | ADDRESS ident prf ldest hdest ⇒
[1173]301        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
[1329]302        ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
[1289]303        ! st ← dpl_store p ldest laddr st;
304        ! st ← dph_store p hdest haddr st;
[1451]305        ! st ← next … p l st ;
[1382]306          ret ? 〈E0, st〉
[1289]307      | OP1 op dacc_a sacc_a ⇒
308        ! v ← acca_retrieve … st sacc_a;
[1173]309        ! v ← Byte_of_val v;
[1213]310          let v' ≝ BVByte (op1 eval op v) in
[1289]311        ! st ← acca_store p dacc_a v' st;
[1451]312        ! st ← next … p l st ;
[1382]313          ret ? 〈E0, st〉
[1289]314      | OP2 op dacc_a sacc_a src ⇒
315        ! v1 ← acca_retrieve … st sacc_a;
[1173]316        ! v1 ← Byte_of_val v1;
[1176]317        ! v2 ← greg_retrieve … st src;
[1173]318        ! v2 ← Byte_of_val v2;
[1213]319        ! carry ← bool_of_beval (carry … st);
[1173]320          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
[1213]321          let v' ≝ BVByte v' in
322          let carry ≝ beval_of_bool carry in
[1289]323        ! st ← acca_store p dacc_a v' st;
[1382]324          let st ≝ set_carry … carry st in
[1451]325        ! st ← next … p l st ;
[1382]326          ret ? 〈E0, st〉
327      | CLEAR_CARRY ⇒
[1451]328        ! st ← next … p l (set_carry … BVfalse st) ;
[1382]329         ret ? 〈E0, st〉
330      | SET_CARRY ⇒
[1451]331        ! st ← next … p l (set_carry … BVtrue st) ;
[1382]332         ret ? 〈E0, st〉
[1289]333      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
334        ! v1 ← acca_retrieve … st sacc_a_reg;
[1173]335        ! v1 ← Byte_of_val v1;
[1289]336        ! v2 ← accb_retrieve … st sacc_b_reg;
[1173]337        ! v2 ← Byte_of_val v2;
338          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
[1213]339          let v1' ≝ BVByte v1' in
340          let v2' ≝ BVByte v2' in
[1289]341        ! st ← acca_store p dacc_a_reg v1' st;
342        ! st ← accb_store p dacc_b_reg v2' st;
[1451]343        ! st ← next … p l st ;
[1382]344          ret ? 〈E0, st〉
[1289]345      | POP dst ⇒
[1174]346        ! 〈st,v〉 ← pop … st;
[1289]347        ! st ← acca_store p dst v st;
[1451]348        ! st ← next … p l st ;
[1382]349          ret ? 〈E0, st〉
[1289]350      | PUSH src ⇒
[1174]351        ! v ← acca_retrieve … st src;
352        ! st ← push … st v;
[1451]353        ! st ← next … p l st ;
[1382]354          ret ? 〈E0, st〉
[1289]355      | MOVE dst_src ⇒
[1294]356        ! st ← pair_reg_move … st dst_src ;
[1451]357        ! st ← next … p l st ;
[1382]358          ret ? 〈E0, st〉
[1371]359      | CALL_ID id args dest ⇒
[1451]360        ! ra ← succ_pc … p l (pc … st) ;         
[1411]361          eval_call_id … p ge st id args dest ra ]
[1289]362    | RETURN ⇒
[1384]363      ! 〈st,ra〉 ← fetch_ra … st;
[1385]364      ! st ← pop_frame … ge st;
[1377]365        ret ? 〈E0,set_pc … ra st〉].
[1213]366cases addr //
367qed.
[1173]368
[1359]369definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → state p → option int ≝
370 λglobals,p,ge,exit,st.res_to_opt ? (
[1298]371  do s ← fetch_statement … ge st;
[1214]372  match s with
[1289]373   [ RETURN ⇒
[1384]374      do 〈st,ra〉 ← fetch_ra … st;
375      if eq_address ra exit then
[1390]376       do regs ← result_regs … ge st ;
377       do vals ← mmap … (λreg.greg_retrieve … st reg) regs ;
[1359]378       Word_of_list_beval vals
[1214]379      else
380       Error ? []
381   | _ ⇒ Error ? []]).
[1173]382
[1233]383record evaluation_parameters : Type[1] ≝
384 { globals: list ident
385 ; sparams2: sem_params2 globals
386 ; exit: address
[1247]387 ; genv2: genv globals sparams2
[1233]388 }.
[1173]389
[1233]390definition joint_exec: trans_system io_out io_in ≝
391  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
[1359]392   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G))
[1233]393   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
394
395definition make_global :
[1247]396 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
[1233]397  joint_program pars → evaluation_parameters
398
399 λpars,sparams.
[1395]400 (* Invariant: a -1 block is unused in common/Globalenvs *)
401 let b ≝ mk_block Code (-1) in
402 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
403 let addr ≝ address_of_code_pointer ptr in
[1408]404  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv Genv … p)).
[1395]405% qed.
[1233]406
[1408]407axiom ExternalMain: String.
[1220]408definition make_initial_state :
[1247]409 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
410 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
[1233]411λpars,sparams,p.
[1408]412  let sem_globals ≝ make_global pars sparams p in
413  let ge ≝ genv2 sem_globals in
414  let m ≝ init_mem Genv … p in
[1415]415  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
[1430]416  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
[1415]417  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
418  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
[1430]419  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
[1415]420  do sp ← address_of_pointer spp ;
[1220]421  let main ≝ prog_main … p in
[1430]422  let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
[1408]423  let trace_state ≝
[1411]424   eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
425    (call_dest_for_main … (sparams …)) (exit sem_globals) in
[1408]426  match trace_state with
427  [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
428  | Wrong msg ⇒ Error … msg
429  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
430  ].
[1430]431[3: % | cases ispb | cases spb] *; #r #off #E >E %
[1415]432qed.
[1233]433
[1186]434definition joint_fullexec :
[1247]435 ∀pars:∀globals.params globals.
436 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
[1233]437 fullexec io_out io_in ≝
438 λpars,sparams.
[1430]439  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracBrowser for help on using the repository browser.