Changeset 2495

Timestamp:

Nov 27, 2012, 5:17:17 PM (9 years ago)

Author:

piccolo

Message:

continuing lineariseProof

File:

• src/joint/lineariseProof.ma (modified) (8 diffs)

src/joint/lineariseProof.ma

@@ -135 +135 @@
  sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
  λp,p',graph_prog,sigma,bv.opt_safe ….
+
+definition sigma_is_opt :
+ ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
+  ((Σi.is_internal_function_of_program … graph_prog i) → 
+    code_point (mk_graph_params p) → option ℕ) →
+  internal_stack → option internal_stack ≝
+λp,p',graph_prog,sigma,is.
+match is with
+[ empty_is ⇒ return empty_is
+| one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv'
+| both_is bv1 bv2 ⇒
+  ! bv1' ← sigma_beval_opt p p' … sigma bv1 ;
+  ! bv2' ← sigma_beval_opt p p' … sigma bv2 ;
+  return both_is bv1' bv2'
+].
+
+definition sigma_is :
+ ∀p,p',graph_prog,sigma,is.
+ sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
+ λp,p',graph_prog,sigma,is.opt_safe ….
+
+lemma sigma_is_pop_commute :
+ ∀p,p',graph_prog,sigma,is,bv,is'.
+ ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
+ is_pop is = return 〈bv, is'〉 →
+ ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
+ ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
+ is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉.
+cases daemon qed.
+
+definition well_formed_mem :
+ ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
+  ((Σi.is_internal_function_of_program … graph_prog i) → 
+    code_point (mk_graph_params p) → option ℕ) →
+ bemem → Prop ≝
+λp,p',graph_prog,sigma,m.
+∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
+  sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?. 
+
+definition sigma_mem :
+ ∀p,p',graph_prog,sigma,m.
+ well_formed_mem p p' graph_prog sigma m →
+ bemem ≝
+ λp,p',graph_prog,sigma,m,prf.
+ mk_mem
+  (λb.
+    If Zltb (block_id b) (nextblock m) then with prf' do    
+      let l ≝ low_bound m b in
+      let h ≝ high_bound m b in
+      mk_block_contents l h
+      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
+        sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ?
+      else BVundef)
+    else empty_block OZ OZ)
+  (nextblock m)
+  (nextblock_pos m).
+@hide_prf
+lapply prf'' lapply prf' -prf' -prf''
+@Zltb_elim_Type0 [2: #_ * ]
+#bid_ok *
+@Zleb_elim_Type0 [2: #_ * ]
+@Zltb_elim_Type0 [2: #_ #_ * ]
+#zh #zl * @(prf … bid_ok zl zh)
+qed.
+
+lemma beloadv_sigma_commute:
+∀p,p',graph_prog,sigma,m,ptr,bv,prf1.
+beloadv m ptr = return bv → 
+∃ prf2.
+beloadv (sigma_mem p p' graph_prog sigma m prf1) ptr = 
+               return sigma_beval p p' graph_prog sigma bv prf2.
+#p #p' #graph_prog #sigma #m #ptr #bv #prf1
+whd in match beloadv in ⊢ (%→?); normalize nodelta
+whd in match do_if_in_bounds in ⊢ (%→?); normalize nodelta
+@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
+#block_id_ok
+@Zleb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
+#zh
+@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
+#zl #EQ whd in EQ : (???%); destruct(EQ)
+% [ @(prf1 ?? block_id_ok zh zl) ]
+whd in match beloadv; normalize nodelta
+whd in match do_if_in_bounds; normalize nodelta
+@Zltb_elim_Type0 normalize nodelta [2: * #ABS @⊥ @ABS assumption]
+#block_id_lin_ok
+@Zleb_elim_Type0 normalize nodelta 
+[ 
+| * #ABS @⊥ @ABS whd in match sigma_mem; normalize nodelta
+
+lemma bestorev_sigma_commute :
+∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2.
+bestorev m ptr bv = return m' → 
+∃prf3.
+bestorev (sigma_mem p p' graph_prog sigma m prf1) 
+          ptr 
+          (sigma_beval p p' graph_prog sigma bv prf2)
+=
+return (sigma_mem p p' graph_prog sigma m' prf3).
+cases daemon qed.
+
+record good_sem_state_sigma
+  (p : unserialized_params)
+  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
+ (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
+    graph_prog i) → 
+      label → option ℕ) : Type[0] ≝
+{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
+; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
+; sigma_empty_frames_commute :
+  ∃prf.
+  empty_framesT (make_sem_lin_params p p') =
+  sigma_frames (empty_framesT (make_sem_graph_params p p')) prf 
+
+; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
+; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
+; sigma_empty_regsT_commute :
+  ∀ptr.∃ prf.
+  empty_regsT (make_sem_lin_params p p') ptr =
+  sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
+; sigma_load_sp_commute : 
+  ∀reg,ptr.
+  load_sp (make_sem_graph_params p p') reg = return ptr →
+  ∃prf.
+  load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr
+; sigma_save_sp_commute :
+  ∀reg,ptr,prf1. ∃prf2.
+  save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr = 
+  sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
+}.
+
+definition well_formed_state : 
+ ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
+ ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
+    code_point (mk_graph_params p) → option ℕ).
+ good_sem_state_sigma p p' graph_prog sigma →
+ state (make_sem_graph_params p p') → Prop ≝
+λp,p',graph_prog,sigma,gsss,st.
+well_formed_frames … gsss (st_frms … st) ∧
+sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧
+well_formed_regs … gsss (regs … st) ∧
+well_formed_mem p p' graph_prog sigma (m … st).
+
+definition sigma_state : 
+ ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
+ ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
+    code_point (mk_graph_params p) → option ℕ).
+ ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
+ ∀st : state (make_sem_graph_params p p').
+ well_formed_state … gsss st →
+ state (make_sem_lin_params p p') ≝
+λp,p',graph_prog,sigma,gsss,st,prf.
+mk_state …
+  (sigma_frames … gsss (st_frms … st) (proj1 … (proj1 … (proj1 … prf))))
+  (sigma_is p p' graph_prog sigma (istack … st) (proj2 … (proj1 … (proj1 … prf))))
+  (carry … st)
+  (sigma_regs … gsss (regs … st) (proj2 … (proj1 … prf)))
+  (sigma_mem p p' graph_prog sigma (m … st) (proj2 … prf)).
+
+
+(*
+lemma sigma_is_pop_wf :
+ ∀p,p',graph_prog,sigma,is,bv,is'.
+ is_pop is = return 〈bv, is'〉 →
+ sigma_is_opt p p' graph_prog sigma is ≠ None ? →
+ sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧
+ sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
+cases daemon qed.
+*)
 
 (* 
@@ -180 +348 @@
     #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
 
+definition well_formed_state_pc :
+ ∀p,p',graph_prog,sigma.
+  good_sem_state_sigma p p' graph_prog sigma → 
+  state_pc (make_sem_graph_params p p') → Prop ≝
+ λp,p',prog,sigma,gsss,st.
+ well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st.
+ 
+definition sigma_state_pc :
+ ∀p.
+ ∀p':∀F.sem_unserialized_params p F.
+ ∀graph_prog.
+  ∀sigma.
+(*   let lin_prog ≝ linearise ? graph_prog in *)
+  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
+    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
+     well_formed_state_pc p p' graph_prog sigma gsss s →
+      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
+≝
+ λp,p',graph_prog,sigma,gsss,s,prf.
+ let pc' ≝ sigma_pc … (proj1 … prf) in
+ let st' ≝ sigma_state … (proj2 … prf) in
+ mk_state_pc ? st' pc'.
+
 definition sigma_function_name :
  ∀p,graph_prog.
@@ -187 +378 @@
 λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
 
-record good_sigma_state (p : unserialized_params)
+lemma m_list_map_All_ok :
+  ∀M : MonadProps.∀X,Y,f,l.
+  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
+  cases daemon qed.
+
+(*
+inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝
+ | isMemberHead : ∀ tl.isMember A x (x :: tl) 
+ | isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).
+(* 
+definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl → 
+      (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.
+      #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]
+    @(isMemberTail ? x y l tl l_spec tl_member)
+    qed.
+  *)             
+
+let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝ 
+match l with [ nil ⇒ λprf : l = nil ?.nil ?
+             | cons x tl ⇒ λprf : l = cons ? x tl.
+              f x ? :: ext_map ?? tl (λy,prf'.f y ?)
+             ] (refl …).
+@hide_prf
+>prf
+[ %1
+| %2 assumption
+] qed. 
+              (f x (isMemberHead A x l tl prf)) ::   
+              ext_map A B tl (lift_f_tail A B l tl x prf f) ] 
+              (refl ? l).
+*)
+
+definition helper_def_store__commute :
+  ∀p,p',graph_prog,sigma.
+  ∀X : ? → Type[0].
+  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
+  ∀store : ∀p,F.∀p' : sem_unserialized_params p F.
+    X p → beval → regsT p' →
+    res (regsT p').
+  Prop ≝
+  λp,p',graph_prog,sigma,X,gsss,store.
+  ∀a : X ?.∀bv,r,r',prf1,prf1'.
+  store … a bv r = return r' → 
+  ∃prf2.
+  store ??? a
+    (sigma_beval p p' graph_prog sigma bv prf1')
+    (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.
+
+definition helper_def_retrieve__commute :
+  ∀p,p',graph_prog,sigma.
+  ∀X : ? → Type[0].
+  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
+  ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F.
+    regsT p' → X p → res beval.
+  Prop ≝
+  λp,p',graph_prog,sigma,X,gsss,retrieve.
+  ∀a : X p.∀r,bv,prf1.
+  retrieve … r a = return bv → 
+  ∃prf2.
+  retrieve … (sigma_regs … gsss r prf1) a
+     = return sigma_beval p p' graph_prog sigma bv prf2.
+  
+record good_state_sigma
+  (p : unserialized_params)
   (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 
  (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
@@ -193 +447 @@
       label → option ℕ)
 : Type[0] ≝
-{ well_formed_state : state (make_sem_graph_params p p') → Prop
-; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p')
-
-; acca_store_ok :
-  ∀a,bv,bv',st,st',prf1,prf2.
-  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
+{ gsss :> good_sem_state_sigma p p' graph_prog sigma 
+
+; acca_store__commute : helper_def_store__commute … gsss acca_store_
+
+; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
+
+}.
+
+lemma store_commute :
+  ∀p,p',graph_prog,sigma.
+  ∀X : ? → Type[0].
+  ∀store.
+  ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 
+  ∀H : helper_def_store__commute … gsss store.
+  ∀a : X p.∀bv,st,st',prf1,prf1'.
+  helper_def_store ? store … a bv st = return st' → 
+  ∃prf2.
+  helper_def_store ? store … a
+    (sigma_beval p p' graph_prog sigma bv prf1')
+    (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
+cases daemon qed.
+
+lemma retrieve_commute :
+ ∀p,p',graph_prog,sigma.
+ ∀X : ? → Type[0].
+ ∀retrieve.
+ ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 
+ ∀H : helper_def_retrieve__commute … gsss retrieve.
+ ∀a : X p .∀st,bv,prf1.
+ helper_def_retrieve ? retrieve … st a = return bv →
+ ∃prf2.
+     helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
+     return sigma_beval p p' graph_prog sigma bv prf2.
+cases daemon qed.
+
+(*
+definition acca_store_commute :
+  ∀p,p',graph_prog,sigma.
+  ∀gss : good_state_sigma p p' graph_prog sigma. 
+  ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'.
+  acca_store … a bv st = return st' → 
+  ∃prf2.
+  acca_store … a
+    (sigma_beval p p' graph_prog sigma bv prf1')
+    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2
+ ≝
+λp,p',graph_prog,sigma.
+λgss : good_state_sigma p p' graph_prog sigma.
+store_commute … gss (acca_store__commute … gss).*)
+  
+    
+lemma acca_store_commute :
+  ∀p,p',graph_prog,sigma.
+  ∀gss : good_state_sigma p p' graph_prog sigma.
+  ∀a,bv,st,st',prf1,prf1'.
   acca_store ?? (p' ?) a bv st = return st' → 
-  acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
-; acca_store_wf :  ∀a,bv,bv',st,st'.
-  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
+  ∃prf2.
+  acca_store ?? (p' ?) a
+    (sigma_beval p p' graph_prog sigma bv prf1')
+    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝
+λp,p',graph_prog,sigma,gss,a,bv.?.
+* #frms #is #carry #regs #m
+* #frms' #is' #carry' #regs' #m'
+*** #frms_ok #is_ok #regs_ok #mem_ok
+#bv_ok #EQ1 elim (bind_inversion ????? EQ1)
+#regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
+elim (acca_store__commute … gss … EQ1)
+[ #prf2 #EQ2
+  % [ whd /4 by conj/ ]
+  change with (! r ← ? ; ? = ?) >EQ2
+  whd in match (sigma_state ???????); normalize nodelta
+   >m_return_bind
+
+
+st,st',prf1,prf2,prf3.?.
+
+
+#p #p' #
+(*
+; acca_store_wf :  ∀a,bv,st,st'.
+  sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → 
   acca_store ?? (p' ?) a bv st = return st' → 
   well_formed_state st → well_formed_state st'
 
-; acca_retrieve_ok :
-  ∀a,st,bv,prf1,prf2.
-  acca_retrieve ?? (p' ?) st a = return bv → 
-  acca_retrieve ?? (p' ?) (sigma_state st prf1) a =
-  return sigma_beval p p' graph_prog sigma bv prf2
 ; acca_retrieve_wf :  ∀a,st,bv.
   acca_retrieve ?? (p' ?) st a = return bv → 
@@ -373 +693 @@
   well_formed_state st1 → well_formed_state st2
 
+; setup_call_ok : 
+  ∀ n , parsT, call_args , st1 , st2 , prf1, prf2.
+  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
+  setup_call ?? (p' ?) n parsT call_args (sigma_state st1 prf1) = 
+  return (sigma_state st2 prf2)
+; setup_call_wf :
+  ∀ n , parsT, call_args , st1 , st2.
+  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
+  well_formed_state st1 → well_formed_state st2
+  
+; fetch_external_args_ok : (* TO BE CHECKED *)
+  ∀ex_fun,st1,prf1,call_args.
+  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
+  fetch_external_args ?? (p' ?) ex_fun (sigma_state st1 prf1) call_args
+; fetch_external_args_wf : 
+  ∀ex_fun,st1,call_args.
+  well_formed_state st1 → ∃ l.
+  fetch_external_args ?? (p' ?) ex_fun st1 call_args = OK ? l
+  
+; set_result_ok :
+  ∀ l , call_dest , st1 , st2 , prf1 , prf2 .
+  set_result ?? (p' ?) l call_dest st1 = return st2 → 
+  set_result ?? (p' ?) l call_dest (sigma_state st1 prf1) = 
+  return (sigma_state st2 prf2)
+; set_result_wf :
+  ∀ l , call_dest , st1 , st2  .
+  set_result ?? (p' ?) l call_dest st1 = return st2 → 
+  well_formed_state st1 → well_formed_state st2  
+  
+; read_result_ok :
+  let lin_prog ≝ linearise p graph_prog in
+  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+  let stack_sizes' ≝
+   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+     ? graph_prog stack_sizes in
+  ∀call_dest , st1 , prf1, l1.
+  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
+    call_dest st1 = return l1 →
+  ∀prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
+  read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
+    call_dest (sigma_state st1 prf1) = return opt_safe … prf
+; read_result_wf :
+  let lin_prog ≝ linearise p graph_prog in
+  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+  let stack_sizes' ≝
+   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+     ? graph_prog stack_sizes in
+  ∀call_dest , st1 , l1.
+  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
+    call_dest st1 = return l1 →
+  well_formed_state st1 → 
+  m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?
+  
+; pop_frame_ok :
+  let lin_prog ≝ linearise p graph_prog in
+  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+  let stack_sizes' ≝
+   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+     ? graph_prog stack_sizes in
+  ∀ st1 , prf1, curr_id ,st2, prf2.
+  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 
+            curr_id st1 = return st2 →
+ let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
+ let st2' ≝ sigma_state (st_no_pc ? st2) (proj2 … prf2) in
+  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
+            (sigma_function_name p graph_prog curr_id) (sigma_state st1 prf1) =
+            return mk_state_pc ? st2' pc' 
+; pop_frame_wf :
+  let lin_prog ≝ linearise p graph_prog in
+  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+  let stack_sizes' ≝
+   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+     ? graph_prog stack_sizes in
+  ∀ st1, curr_id ,st2.
+  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 
+            curr_id st1 = return st2 → 
+  well_formed_state st1 → well_formed_pc p p' graph_prog sigma (pc ? st2) ∧ 
+      well_formed_state (st_no_pc ? st2)
 }.
 
@@ -388 +786 @@
   (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
 *)
-
-definition well_formed_state_pc :
- ∀p,p',graph_prog,sigma.
-  good_sigma_state p p' graph_prog sigma → 
-  state_pc (make_sem_graph_params p p') → Prop ≝
- λp,p',prog,sigma,gss,st.
- well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st.
- 
-definition sigma_state_pc :
- ∀p.
- ∀p':∀F.sem_unserialized_params p F.
- ∀graph_prog.
-  ∀sigma.
-(*   let lin_prog ≝ linearise ? graph_prog in *)
-  ∀gss : good_sigma_state p p' graph_prog sigma.
-    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
-     well_formed_state_pc p p' graph_prog sigma gss s →
-      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
-≝
- λp,p',graph_prog,sigma,gss,s,prf.
- let pc' ≝ sigma_pc … (proj1 … prf) in
- let st' ≝ sigma_state … (proj2 … prf) in
- mk_state_pc ? st' pc'.
+*)
 
 (*
@@ -829 +1205 @@
   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     ? graph_prog stack_sizes in
- ∀sigma.∀gss : good_sigma_state … graph_prog sigma.
+ ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
  ∀fn,st,stmt,st'.
  ∀prf : well_formed_state … gss st.∀prf'.
@@ -840 +1216 @@
   #fn #st #stmt
   #st' #prf #prf'
-  cases daemon (*
   whd in match eval_seq_no_pc;
   cases stmt normalize nodelta
-  [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) //
-  | #mv_sig whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
+  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) //
+  | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
+    >(pair_reg_move_ok ?????????? H) [% | skip]
+  | (* POP *)
+    #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
+    * #val #st1 * #vals_spec #H
+    cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ]
+    #wf_st1 
+    lapply(acca_store_wf ????????? H wf_st1)
+    * #_ #sigma_val_spec
+    lapply vals_spec -vals_spec
+    whd in match pop; normalize nodelta
+    #H1 elim (bind_inversion ????? H1) -H1 * #g_bev #g_is * #ispop_spec
+    whd in ⊢ ((??%%) → ?); #EQ (*to be destructed*)
+    lapply ispop_spec -ispop_spec
+    whd in match is_pop; normalize nodelta
+    cases (istack ? st) normalize nodelta
+    [ #ABS whd in ABS : (???%); destruct(ABS)
+    | #one whd in ⊢ ((??%%) → ?); #EQ1 destruct(EQ1)
+      cases (istack ? (sigma_state … st prf)) normalize nodelta
+    
+    lapply (acca_store_ok ?????????????? H)
+
+    
+     -val_spec * #bv #is * #bv_is_spec
+    #EQ whd in EQ : (??%%); destruct(EQ) 
+    whd in match is_pop in bv_is_spec; normalize nodelta in bv_is_spec;
+    inversion (istack ? st) in bv_is_spec; 
+    [ #_ normalize nodelta whd in ⊢ ((???%) → ?); #ABS destruct(ABS)
+    | #bv1 #bv1_spec normalize nodelta whd in ⊢ ((??%%) → ?); #EQ destruct(EQ)
+    lapply(acca_store_wf ????????? H prf) check acca_store_ok check(acca_store_ok ?????????????? H)
+ 
+  @(pair_reg_move_ok ? ? ? ? gss mv_sig st st' ? ?) whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
     #H
-  ] *)
 qed.