Changeset 2443 for src/joint

Timestamp:

Nov 8, 2012, 2:27:54 PM (9 years ago)

Author:

tranquil

Message:

changed joint's stack pointer and internal stack

Location:

src/joint

Files:

• SemanticUtils.ma (modified) (5 diffs)
• Traces.ma (modified) (10 diffs)
• TranslateUtils.ma (modified) (3 diffs)
• lineariseProof.ma (modified) (3 diffs)
• semantics.ma (modified) (15 diffs)

src/joint/SemanticUtils.ma

@@ -6 +6 @@
 record hw_register_env : Type[0] ≝
   { reg_env : BitVectorTrie beval 6
-  ; carry_bit : bebit
   ; other_bit : bebit
   }.
 
 definition empty_hw_register_env: hw_register_env ≝
-  mk_hw_register_env (Stub …) BBundef BBundef.
+  mk_hw_register_env (Stub …) BBundef.
 
 include alias "ASM/BitVectorTrie.ma".
@@ -20 +19 @@
 definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
  λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
-  (carry_bit env) (other_bit env).
-
-definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
-λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
+  (other_bit env).
 
 definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
-λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
-
+λv,env.mk_hw_register_env (reg_env env) v.
+
+definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
+λenv.
+let spl ≝ hwreg_retrieve env RegisterSPL in
+let sph ≝ hwreg_retrieve env RegisterSPH in
+! ptr ← pointer_of_address 〈spl, sph〉 ;
+match ptype ptr return λx.ptype ptr = x → res xpointer with
+[ XData ⇒ λprf.return «ptr, prf»
+| _ ⇒ λ_.Error … [MSG BadPointer]
+] (refl …).
+
+definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
+λenv,sp.
+let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
+hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
 
 (*** Store/retrieve on pseudo-registers ***)
 include alias "common/Identifiers.ma".
 
+record reg_sp : Type[0] ≝
+{ reg_sp_env :> identifier_map RegisterTag beval
+; stackp : xpointer
+}.
+
 axiom BadRegister : String.
 
@@ -39 +54 @@
  λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
 
+definition reg_sp_store ≝ λreg,v,locals.
+! locals' ← reg_store reg v (reg_sp_env locals) ;
+return mk_reg_sp locals' (stackp locals).
+
+definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
+
 (*** Store/retrieve on hardware registers ***)
 
 definition init_hw_register_env: xpointer → hw_register_env ≝
- λsp.
-  let 〈dpl,dph〉 ≝
-    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
-    [ OK p ⇒ λ_.p
-    | _ ⇒ λprf.⊥
-    ] (refl …) in
-  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
-   hwreg_store RegisterDPL dpl env.
-@hide_prf
-normalize in prf; destruct(prf)
-qed.
+ λsp.hwreg_store_sp empty_hw_register_env sp.
 
 (******************************** GRAPHS **************************************)
@@ -150 +161 @@
 
 definition make_sem_graph_params :
-  ∀pars : graph_params.
-  ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
+  ∀pars : unserialized_params.
+  ∀g_pars : ∀F.sem_unserialized_params pars F.
   sem_params ≝
-  λpars,g_pars.
+  λpars,spars.
+  let g_pars ≝ mk_graph_params pars in
   mk_sem_params
-    pars
+    g_pars
     (mk_more_sem_params
-      pars
       g_pars
+      (spars ?)
       graph_offset_of_label
       graph_label_of_offset
@@ -187 +199 @@
   λo.nat_of_bitvector ? (offv o).
 
-
 definition make_sem_lin_params :
-  ∀pars : lin_params.
-  ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
+  ∀pars : unserialized_params.
+  (∀F.sem_unserialized_params pars F) →
   sem_params ≝
-  λpars,g_pars.
+  λpars,spars.
+  let lin_pars ≝ mk_lin_params pars in
   mk_sem_params
-    pars
+    lin_pars
     (mk_more_sem_params
-      pars
-      g_pars
+      lin_pars
+      (spars ?)
       lin_offset_of_nat
       lin_nat_of_offset

src/joint/Traces.ma

@@ -7 +7 @@
  ; exit: cpointer
  ; ev_genv: genv sparams globals
- ; io_env : state sparams → ∀o:io_out.res (io_in o)
+(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
  }.
  
@@ -13 +13 @@
  { prog_spars : sem_params
  ; prog : joint_program prog_spars
- ; prog_io : state prog_spars → ∀o.res (io_in o)
+(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
  }.
 
@@ -28 +28 @@
   «ptr, refl …»
   (mk_genv_gen ?? (globalenv_noinit ? p) ?)
-  (prog_io pars).
+ (* (prog_io pars) *).
 (* TODO or TOBEFOUND *)
 cases daemon
@@ -49 +49 @@
   let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
   let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
-  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in
+(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
   let main ≝ prog_main … p in
-  let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in
+  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
+  let st0' ≝ set_sp … spp st0 in
   (* use exit sem_globals as ra and call_dest_for_main as dest *)
-  ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
-  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
+  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
+  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
   ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
   ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; 
@@ -63 +64 @@
   ].
   [ %
-  | cases ispb
-  | cases spb
-  ] normalize //
+  | cases spb normalize //
+  ]
 qed.
 
@@ -114 +114 @@
 qed.
 
+(*
 let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
   match c with
@@ -122 +123 @@
   | Wrong e ⇒ Error … e
   ].
+*)
 
 definition cost_label_of_stmt :
@@ -145 +147 @@
    (* as_status ≝ *) (state_pc p)
    (* as_execute ≝ *)
-    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
+    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
    (* as_pc ≝ *) cpointerDeq
    (* as_pc_of ≝ *) (pc …)
@@ -151 +153 @@
     (λs.
       match (
-        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;
+        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
         match stmt with
         [ sequential stp nxt ⇒
-          ! 〈flow, s'〉  ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ;
+          ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
           return step_flow_classifier … flow
         | final stp ⇒
-          ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
+          ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
           return fin_step_flow_classifier … flow
         ]) with
-      [ OK c ⇒ c
-      | Error _ ⇒ cl_other
+      [ Value c ⇒ c
+      | _ ⇒ cl_other
       ])
    (* as_label_of_pc ≝ *)
@@ -175 +177 @@
       succ_pc p p (pc … s1) nxt = return pc … s2)
    (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
-   (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed.
+   (* as_call_ident_≝ *)
+   (λst.?). cases daemon (* TODO *) qed.

src/joint/TranslateUtils.ma

@@ -2 +2 @@
 include "joint/blocks.ma".
 include "utilities/hide.ma".
+include "utilities/deqsets.ma".
 
 (* general type of functions generating fresh things *)
@@ -64 +65 @@
     add_graph … mid (final … (\snd b)) def
   ].
+
+(* ignoring register allocation for now *)
+
+definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
+λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
+
+lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
+#tag #A * #l * #m whd in ⊢ (%→?%);
+elim (lookup tag ???)
+[ * #ABS elim (ABS ?) %
+| #a #_ %
+] qed.
+
+lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
+#tag #A * #l * #m whd in ⊢ (?%→%);
+elim (lookup tag ???)
+[ * | #a * % #ABS destruct(ABS) ] qed.
+
+(*
+lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
+  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
+  〈id, u'〉 = fresh tag u →
+  ¬id ∈ l.
+#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
+[ #hd_fresh #tl_fresh #EQfresh
+  whd in ⊢ (?(?%));
+  change with (eq_identifier ???) in match (?==?);
+  >eq_identifier_sym
+  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
+  normalize nodelta @(IH … tl_fresh EQfresh)
+| #_ %
+]
+qed.
+*)
+
+lemma fresh_was_fresh : ∀tag,id,id',u,u'.
+〈id,u'〉 = fresh tag u →
+fresh_for_univ tag id' u' →
+id' ≠ id →
+fresh_for_univ tag id' u.
+#tag * #id * #id' * #u * #u'
+normalize #EQfresh destruct
+#H #NEQ
+elim (le_to_or_lt_eq … H)
+[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
+#H >(succ_injective … H) in NEQ;
+* #G elim (G (refl …))
+qed.
+
+
+(* use Russell? *)
+axiom adds_graph_list_ok :
+  ∀g_pars,globals,b,src,def.
+  fresh_for_univ … src (joint_if_luniverse … def) →
+  luniverse_ok ?? def →
+  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
+  luniverse_ok ?? def' ∧
+  ∃l.bool_to_Prop (uniqueb … l) ∧
+     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
+                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
+     src ~❨b,l❩~> dst in joint_if_code … def'.
+(* #p #g #l elim l
+[ #src #def #_ #Hdef whd
+  %{Hdef} %{[ ]} %%%
+| #hd #tl #IH #src #def #src_fresh #Hdef
+  whd in match (adds_graph_list ?????);
+  whd in match (fresh_label ???);
+  @(pair_elim … (fresh ??)) normalize nodelta
+  #mid #luniverse' #EQfresh
+  whd in ⊢ (match % with [ _ ⇒ ?]);
+  letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
+  cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
+  [ cases def // ] #EQ_aux
+  lapply (IH mid def' ??)
+  [ #l whd in match def'; #Hpres
+    lapply (present_to_memb … Hpres) -Hpres
+    >mem_set_add @eq_identifier_elim
+    [ #EQ destruct(EQ) *
+    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
+      #l_in
+    ]
+    @(fresh_remains_fresh … (sym_eq … EQfresh))
+    [2: @Hdef @memb_to_present ] assumption
+  | whd in match def';
+    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
+    whd in match (set_luniverse ????);
+    @(fresh_is_fresh … (sym_eq … EQfresh))
+  ]
+  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
+  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
+  % [ % ]
+  [ whd in ⊢ (?%);
+    elim (true_or_false_Prop (mid∈l)) #H >H normalize nodelta
+    [ elim (All_memb … Hl2 H)
+      cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in ⊢ (%→?);
+      #H #_ @(absurd ?? H)
+      @(fresh_remains_fresh … (eqEQfresh)
+      normalize #H10 #H11
+      
+    >(All_fresh_not_memb … (sym_eq … EQfresh))
+    [ assumption ]
+    @(All_mp … Hl2) #lbl *
+    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
+    normalize #EQfresh #H #lbl_not_mid
+    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
+    
+    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
+    [ normalize
+*)
 
 (* preserves first statement if a cost label (should be an invariant) *)
@@ -132 +242 @@
   ].
 
+  
+
 (* translation with inline fresh register allocation *)
 definition b_graph_translate :

src/joint/lineariseProof.ma

@@ -20 +20 @@
 definition graph_abstract_status:
  ∀p:unserialized_params. 
-  (∀F.more_sem_unserialized_params p F) →
+  (∀F.sem_unserialized_params p F) →
     joint_program (mk_graph_params p) →
      abstract_status
@@ -27 +27 @@
   joint_abstract_status
    (mk_prog_params
-    (make_sem_graph_params (mk_graph_params p) (p' ?))
-    prog ⊥).
-@daemon (* I/O, TODO *)
-qed.
+    (make_sem_graph_params p p')
+    prog).
 
 definition lin_abstract_status:
  ∀p:unserialized_params. 
-  (∀F.more_sem_unserialized_params p F) →
+  (∀F.sem_unserialized_params p F) →
     joint_program (mk_lin_params p) →
      abstract_status
@@ -41 +39 @@
   joint_abstract_status
    (mk_prog_params
-    (make_sem_lin_params (mk_lin_params p) (p' ?))
-    prog ⊥).
-@daemon (* I/O, TODO *)
-qed.
+    (make_sem_lin_params p p')
+    prog).
 
 definition linearise_status_rel:

src/joint/semantics.ma

@@ -33 +33 @@
  ; empty_framesT: framesT
  ; regsT : Type[0]
- ; empty_regsT: xpointer → regsT (* Stack pointer *)
+ ; empty_regsT: xpointer → regsT (* initial stack pointer *)
+ ; load_sp : regsT → res xpointer
+ ; save_sp : regsT → xpointer → regsT
  }.
+
+inductive internal_stack : Type[0] ≝
+| empty_is : internal_stack
+| one_is : beval → internal_stack
+| both_is : beval → beval → internal_stack.
+
+axiom InternalStackFull : String.
+axiom InternalStackEmpty : String.
+
+definition is_push : internal_stack → beval → res internal_stack ≝
+λis,bv.match is with
+[ empty_is ⇒ return one_is bv
+| one_is bv' ⇒ return both_is bv' bv
+| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
+].
+
+definition is_pop : internal_stack → res (beval × internal_stack) ≝
+λis.match is with
+[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
+| one_is bv' ⇒ return 〈bv', empty_is〉
+| both_is bv bv' ⇒ return 〈bv', one_is bv〉
+].
 
 record state (semp: sem_state_params): Type[0] ≝
  { st_frms: framesT semp 
- ; sp: xpointer
- ; isp: xpointer
+ ; istack : internal_stack
  ; carry: bebit
  ; regs: regsT semp
@@ -45 +68 @@
  }.
 
-coercion sem_state_params_to_state nocomposites:
-  ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
+definition sp ≝ λp,st.load_sp p (regs ? st).
 
 record state_pc (semp : sem_state_params) : Type[0] ≝
@@ -54 +76 @@
 
 definition set_m: ∀p. bemem → state p → state p ≝
- λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
+ λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
 
 definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
- λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
+ λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
 
 definition set_sp: ∀p. ? → state p → state p ≝
- λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
-
-definition set_isp: ∀p. ? → state p → state p ≝
- λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
+ λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
+ mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
 
 definition set_carry: ∀p. bebit → state p → state p ≝
- λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
+ λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
+
+definition set_istack: ∀p. internal_stack → state p → state p ≝
+ λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
 
 definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
@@ -75 +98 @@
 
 definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
- λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
+ λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
 
 axiom BadProgramCounter : String.
@@ -111 +134 @@
   | FEnd2  : fin_step_flow p F Call. (* end flow *)
 
-record more_sem_unserialized_params
+record sem_unserialized_params
   (uns_pars : unserialized_params)
   (F : list ident → Type[0]) : Type[1] ≝
-  { st_pars :> sem_state_params (* automatic coercion has issues *)
+  { st_pars :> sem_state_params
   ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
   ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
@@ -129 +152 @@
   ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
   ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
-  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
+  ; fetch_ra: state st_pars → res (cpointer × (state st_pars))
 
   ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
@@ -169 +192 @@
 definition helper_def_retrieve : 
   ∀X : ? → ? → ? → Type[0].
-  (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
-  ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
+  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
+  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     λX,f,up,F,p,st.f ?? p (regs … st).
 
 definition helper_def_store :
   ∀X : ? → ? → ? → Type[0].
-  (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
-  ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
+  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
+  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
   λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
 
@@ -193 +216 @@
 definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
 definition pair_reg_move ≝
-  λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
+  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     ! r ← pair_reg_move_ ?? p (regs ? st) pm;
     return set_regs ? r st.
-
  
 axiom BadPointer : String.
@@ -208 +230 @@
    serialization and on whether the call is a tail one. *)
 definition eval_call_block:
- ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
+ ∀p,F.∀p':sem_unserialized_params p F.∀globals.
   genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
     IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
@@ -232 +254 @@
 definition push: ∀p.state p → beval → res (state p) ≝
  λp,st,v.
-  let isp' ≝ isp ? st in
-  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
-  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
-  return set_m … m (set_isp … isp'' st).
-  normalize elim (isp p st) #p #H @H
-qed.
-
-definition pop: ∀p. state p → res ((state p ) × beval) ≝
+ ! is ← is_push (istack … st) v ;
+ return set_istack … is st.
+
+definition pop: ∀p. state p → res (beval × (state p)) ≝
  λp,st.
-  let isp' ≝ isp ? st in
-  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
-  let ist ≝ set_isp … isp'' st in
-  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
-  OK ? 〈ist,v〉.
-  normalize elim (isp p st) #p #H @H
-qed.
+ ! 〈bv, is〉 ← is_pop (istack … st) ;
+ return 〈bv, set_istack … is st〉.
 
 definition save_ra : ∀p. state p → cpointer → res (state p) ≝
  λp,st,l.
-  ! 〈addrl,addrh〉 ← beval_pair_of_pointer l ; (* always succeeds *)
+  let 〈addrl,addrh〉 ≝  beval_pair_of_pointer l in
   ! st' ← push … st addrl;
   push … st' addrh.
 
-definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
+definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝
  λp,st.
-  do 〈st',addrh〉 ← pop … st;
-  do 〈st'',addrl〉 ← pop … st';
+  do 〈addrh, st'〉 ← pop … st;
+  do 〈addrl, st''〉 ← pop … st';
   do pr ← pointer_of_address 〈addrh, addrl〉;
-  match ptype pr return λx.ptype pr = x → res (? × cpointer) with
-  [ Code ⇒ λprf.return 〈st'', «pr,prf»〉
+  match ptype pr return λx.ptype pr = x → res (cpointer × ?) with
+  [ Code ⇒ λprf.return 〈«pr,prf», st''〉
   | _ ⇒ λ_.Error … [MSG BadPointer]
   ] (refl …).
@@ -267 +280 @@
 (* parameters that are defined by serialization *)
 record more_sem_params (pp : params) : Type[1] ≝
-  { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp)
+  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
   ; offset_of_point : code_point pp → option offset (* can overflow *)
   ; point_of_offset : offset → code_point pp
@@ -463 +476 @@
     return set_m … m' st
   | ADDRESS id prf ldest hdest ⇒
-    let addr ≝ opt_safe ? (find_symbol … ge id) ? in
-    ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer addr zero_offset) ;
+    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
+    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
     ! st' ← dpl_store … ldest laddr st;
     dph_store … hdest haddr st'
@@ -488 +501 @@
     accb_store … dacc_b_reg v2' st'
   | POP dst ⇒
-    ! 〈st',v〉 ← pop p st;
+    ! 〈v, st'〉 ← pop p st;
     acca_store … p dst v st'
   | PUSH src ⇒
@@ -601 +614 @@
     do_call … ge st id fn args
   | _ ⇒
-    ! 〈st',ra〉 ← fetch_ra … st ;
+    ! 〈ra, st'〉 ← fetch_ra … st ;
     ! fn ← fetch_function … ge curr ;
     ! st'' ← pop_frame … ge fn st';
@@ -640 +653 @@
     match s' with
     [ RETURN ⇒ 
-      do 〈st',ra〉 ← fetch_ra … st;
+      do 〈ra, st'〉 ← fetch_ra … st;
       if eq_pointer ra exit then 
        do vals ← read_result … ge (joint_if_result … fn) st' ;