Ignore:
Timestamp:
Nov 27, 2012, 5:17:17 PM (7 years ago)
Author:
piccolo
Message:

continuing lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2484 r2495  
    135135 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
    136136 λp,p',graph_prog,sigma,bv.opt_safe ….
     137
     138definition sigma_is_opt :
     139 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
     140  ((Σi.is_internal_function_of_program … graph_prog i) →
     141    code_point (mk_graph_params p) → option ℕ) →
     142  internal_stack → option internal_stack ≝
     143λp,p',graph_prog,sigma,is.
     144match is with
     145[ empty_is ⇒ return empty_is
     146| one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv'
     147| both_is bv1 bv2 ⇒
     148  ! bv1' ← sigma_beval_opt p p' … sigma bv1 ;
     149  ! bv2' ← sigma_beval_opt p p' … sigma bv2 ;
     150  return both_is bv1' bv2'
     151].
     152
     153definition sigma_is :
     154 ∀p,p',graph_prog,sigma,is.
     155 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
     156 λp,p',graph_prog,sigma,is.opt_safe ….
     157
     158lemma sigma_is_pop_commute :
     159 ∀p,p',graph_prog,sigma,is,bv,is'.
     160 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
     161 is_pop is = return 〈bv, is'〉 →
     162 ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
     163 ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
     164 is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉.
     165cases daemon qed.
     166
     167definition well_formed_mem :
     168 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
     169  ((Σi.is_internal_function_of_program … graph_prog i) →
     170    code_point (mk_graph_params p) → option ℕ) →
     171 bemem → Prop ≝
     172λp,p',graph_prog,sigma,m.
     173∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
     174  sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?.
     175
     176definition sigma_mem :
     177 ∀p,p',graph_prog,sigma,m.
     178 well_formed_mem p p' graph_prog sigma m →
     179 bemem ≝
     180 λp,p',graph_prog,sigma,m,prf.
     181 mk_mem
     182  (λb.
     183    If Zltb (block_id b) (nextblock m) then with prf' do   
     184      let l ≝ low_bound m b in
     185      let h ≝ high_bound m b in
     186      mk_block_contents l h
     187      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
     188        sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ?
     189      else BVundef)
     190    else empty_block OZ OZ)
     191  (nextblock m)
     192  (nextblock_pos m).
     193@hide_prf
     194lapply prf'' lapply prf' -prf' -prf''
     195@Zltb_elim_Type0 [2: #_ * ]
     196#bid_ok *
     197@Zleb_elim_Type0 [2: #_ * ]
     198@Zltb_elim_Type0 [2: #_ #_ * ]
     199#zh #zl * @(prf … bid_ok zl zh)
     200qed.
     201
     202lemma beloadv_sigma_commute:
     203∀p,p',graph_prog,sigma,m,ptr,bv,prf1.
     204beloadv m ptr = return bv →
     205∃ prf2.
     206beloadv (sigma_mem p p' graph_prog sigma m prf1) ptr =
     207               return sigma_beval p p' graph_prog sigma bv prf2.
     208#p #p' #graph_prog #sigma #m #ptr #bv #prf1
     209whd in match beloadv in ⊢ (%→?); normalize nodelta
     210whd in match do_if_in_bounds in ⊢ (%→?); normalize nodelta
     211@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
     212#block_id_ok
     213@Zleb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
     214#zh
     215@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
     216#zl #EQ whd in EQ : (???%); destruct(EQ)
     217% [ @(prf1 ?? block_id_ok zh zl) ]
     218whd in match beloadv; normalize nodelta
     219whd in match do_if_in_bounds; normalize nodelta
     220@Zltb_elim_Type0 normalize nodelta [2: * #ABS @⊥ @ABS assumption]
     221#block_id_lin_ok
     222@Zleb_elim_Type0 normalize nodelta
     223[
     224| * #ABS @⊥ @ABS whd in match sigma_mem; normalize nodelta
     225
     226lemma bestorev_sigma_commute :
     227∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2.
     228bestorev m ptr bv = return m' →
     229∃prf3.
     230bestorev (sigma_mem p p' graph_prog sigma m prf1)
     231          ptr
     232          (sigma_beval p p' graph_prog sigma bv prf2)
     233=
     234return (sigma_mem p p' graph_prog sigma m' prf3).
     235cases daemon qed.
     236
     237record good_sem_state_sigma
     238  (p : unserialized_params)
     239  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
     240 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
     241    graph_prog i) →
     242      label → option ℕ) : Type[0] ≝
     243{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
     244; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
     245; sigma_empty_frames_commute :
     246  ∃prf.
     247  empty_framesT (make_sem_lin_params p p') =
     248  sigma_frames (empty_framesT (make_sem_graph_params p p')) prf
     249
     250; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
     251; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
     252; sigma_empty_regsT_commute :
     253  ∀ptr.∃ prf.
     254  empty_regsT (make_sem_lin_params p p') ptr =
     255  sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
     256; sigma_load_sp_commute :
     257  ∀reg,ptr.
     258  load_sp (make_sem_graph_params p p') reg = return ptr →
     259  ∃prf.
     260  load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr
     261; sigma_save_sp_commute :
     262  ∀reg,ptr,prf1. ∃prf2.
     263  save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr =
     264  sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
     265}.
     266
     267definition well_formed_state :
     268 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
     269 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
     270    code_point (mk_graph_params p) → option ℕ).
     271 good_sem_state_sigma p p' graph_prog sigma →
     272 state (make_sem_graph_params p p') → Prop ≝
     273λp,p',graph_prog,sigma,gsss,st.
     274well_formed_frames … gsss (st_frms … st) ∧
     275sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧
     276well_formed_regs … gsss (regs … st) ∧
     277well_formed_mem p p' graph_prog sigma (m … st).
     278
     279definition sigma_state :
     280 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
     281 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
     282    code_point (mk_graph_params p) → option ℕ).
     283 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
     284 ∀st : state (make_sem_graph_params p p').
     285 well_formed_state … gsss st →
     286 state (make_sem_lin_params p p') ≝
     287λp,p',graph_prog,sigma,gsss,st,prf.
     288mk_state …
     289  (sigma_frames … gsss (st_frms … st) (proj1 … (proj1 … (proj1 … prf))))
     290  (sigma_is p p' graph_prog sigma (istack … st) (proj2 … (proj1 … (proj1 … prf))))
     291  (carry … st)
     292  (sigma_regs … gsss (regs … st) (proj2 … (proj1 … prf)))
     293  (sigma_mem p p' graph_prog sigma (m … st) (proj2 … prf)).
     294
     295
     296(*
     297lemma sigma_is_pop_wf :
     298 ∀p,p',graph_prog,sigma,is,bv,is'.
     299 is_pop is = return 〈bv, is'〉 →
     300 sigma_is_opt p p' graph_prog sigma is ≠ None ? →
     301 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧
     302 sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
     303cases daemon qed.
     304*)
    137305
    138306(*
     
    180348    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
    181349
     350definition well_formed_state_pc :
     351 ∀p,p',graph_prog,sigma.
     352  good_sem_state_sigma p p' graph_prog sigma →
     353  state_pc (make_sem_graph_params p p') → Prop ≝
     354 λp,p',prog,sigma,gsss,st.
     355 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st.
     356 
     357definition sigma_state_pc :
     358 ∀p.
     359 ∀p':∀F.sem_unserialized_params p F.
     360 ∀graph_prog.
     361  ∀sigma.
     362(*   let lin_prog ≝ linearise ? graph_prog in *)
     363  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
     364    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     365     well_formed_state_pc p p' graph_prog sigma gsss s →
     366      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
     367
     368 λp,p',graph_prog,sigma,gsss,s,prf.
     369 let pc' ≝ sigma_pc … (proj1 … prf) in
     370 let st' ≝ sigma_state … (proj2 … prf) in
     371 mk_state_pc ? st' pc'.
     372
    182373definition sigma_function_name :
    183374 ∀p,graph_prog.
     
    187378λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
    188379
    189 record good_sigma_state (p : unserialized_params)
     380lemma m_list_map_All_ok :
     381  ∀M : MonadProps.∀X,Y,f,l.
     382  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
     383  cases daemon qed.
     384
     385(*
     386inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝
     387 | isMemberHead : ∀ tl.isMember A x (x :: tl)
     388 | isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).
     389(*
     390definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl →
     391      (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.
     392      #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]
     393    @(isMemberTail ? x y l tl l_spec tl_member)
     394    qed.
     395  *)             
     396
     397let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝
     398match l with [ nil ⇒ λprf : l = nil ?.nil ?
     399             | cons x tl ⇒ λprf : l = cons ? x tl.
     400              f x ? :: ext_map ?? tl (λy,prf'.f y ?)
     401             ] (refl …).
     402@hide_prf
     403>prf
     404[ %1
     405| %2 assumption
     406] qed.
     407              (f x (isMemberHead A x l tl prf)) ::   
     408              ext_map A B tl (lift_f_tail A B l tl x prf f) ]
     409              (refl ? l).
     410*)
     411
     412definition helper_def_store__commute :
     413  ∀p,p',graph_prog,sigma.
     414  ∀X : ? → Type[0].
     415  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
     416  ∀store : ∀p,F.∀p' : sem_unserialized_params p F.
     417    X p → beval → regsT p' →
     418    res (regsT p').
     419  Prop ≝
     420  λp,p',graph_prog,sigma,X,gsss,store.
     421  ∀a : X ?.∀bv,r,r',prf1,prf1'.
     422  store … a bv r = return r' →
     423  ∃prf2.
     424  store ??? a
     425    (sigma_beval p p' graph_prog sigma bv prf1')
     426    (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.
     427
     428definition helper_def_retrieve__commute :
     429  ∀p,p',graph_prog,sigma.
     430  ∀X : ? → Type[0].
     431  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
     432  ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F.
     433    regsT p' → X p → res beval.
     434  Prop ≝
     435  λp,p',graph_prog,sigma,X,gsss,retrieve.
     436  ∀a : X p.∀r,bv,prf1.
     437  retrieve … r a = return bv →
     438  ∃prf2.
     439  retrieve … (sigma_regs … gsss r prf1) a
     440     = return sigma_beval p p' graph_prog sigma bv prf2.
     441 
     442record good_state_sigma
     443  (p : unserialized_params)
    190444  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
    191445 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
     
    193447      label → option ℕ)
    194448: Type[0] ≝
    195 { well_formed_state : state (make_sem_graph_params p p') → Prop
    196 ; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p')
    197 
    198 ; acca_store_ok :
    199   ∀a,bv,bv',st,st',prf1,prf2.
    200   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     449{ gsss :> good_sem_state_sigma p p' graph_prog sigma
     450
     451; acca_store__commute : helper_def_store__commute … gsss acca_store_
     452
     453; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
     454
     455}.
     456
     457lemma store_commute :
     458  ∀p,p',graph_prog,sigma.
     459  ∀X : ? → Type[0].
     460  ∀store.
     461  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
     462  ∀H : helper_def_store__commute … gsss store.
     463  ∀a : X p.∀bv,st,st',prf1,prf1'.
     464  helper_def_store ? store … a bv st = return st' →
     465  ∃prf2.
     466  helper_def_store ? store … a
     467    (sigma_beval p p' graph_prog sigma bv prf1')
     468    (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
     469cases daemon qed.
     470
     471lemma retrieve_commute :
     472 ∀p,p',graph_prog,sigma.
     473 ∀X : ? → Type[0].
     474 ∀retrieve.
     475 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
     476 ∀H : helper_def_retrieve__commute … gsss retrieve.
     477 ∀a : X p .∀st,bv,prf1.
     478 helper_def_retrieve ? retrieve … st a = return bv →
     479 ∃prf2.
     480     helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
     481     return sigma_beval p p' graph_prog sigma bv prf2.
     482cases daemon qed.
     483
     484(*
     485definition acca_store_commute :
     486  ∀p,p',graph_prog,sigma.
     487  ∀gss : good_state_sigma p p' graph_prog sigma.
     488  ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'.
     489  acca_store … a bv st = return st' →
     490  ∃prf2.
     491  acca_store … a
     492    (sigma_beval p p' graph_prog sigma bv prf1')
     493    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2
     494 ≝
     495λp,p',graph_prog,sigma.
     496λgss : good_state_sigma p p' graph_prog sigma.
     497store_commute … gss (acca_store__commute … gss).*)
     498 
     499   
     500lemma acca_store_commute :
     501  ∀p,p',graph_prog,sigma.
     502  ∀gss : good_state_sigma p p' graph_prog sigma.
     503  ∀a,bv,st,st',prf1,prf1'.
    201504  acca_store ?? (p' ?) a bv st = return st' →
    202   acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
    203 ; acca_store_wf :  ∀a,bv,bv',st,st'.
    204   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
     505  ∃prf2.
     506  acca_store ?? (p' ?) a
     507    (sigma_beval p p' graph_prog sigma bv prf1')
     508    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝
     509λp,p',graph_prog,sigma,gss,a,bv.?.
     510* #frms #is #carry #regs #m
     511* #frms' #is' #carry' #regs' #m'
     512*** #frms_ok #is_ok #regs_ok #mem_ok
     513#bv_ok #EQ1 elim (bind_inversion ????? EQ1)
     514#regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
     515elim (acca_store__commute … gss … EQ1)
     516[ #prf2 #EQ2
     517  % [ whd /4 by conj/ ]
     518  change with (! r ← ? ; ? = ?) >EQ2
     519  whd in match (sigma_state ???????); normalize nodelta
     520   >m_return_bind
     521
     522
     523st,st',prf1,prf2,prf3.?.
     524
     525
     526#p #p' #
     527(*
     528; acca_store_wf :  ∀a,bv,st,st'.
     529  sigma_beval_opt p p' graph_prog sigma bv ≠ None ? →
    205530  acca_store ?? (p' ?) a bv st = return st' →
    206531  well_formed_state st → well_formed_state st'
    207532
    208 ; acca_retrieve_ok :
    209   ∀a,st,bv,prf1,prf2.
    210   acca_retrieve ?? (p' ?) st a = return bv →
    211   acca_retrieve ?? (p' ?) (sigma_state st prf1) a =
    212   return sigma_beval p p' graph_prog sigma bv prf2
    213533; acca_retrieve_wf :  ∀a,st,bv.
    214534  acca_retrieve ?? (p' ?) st a = return bv →
     
    373693  well_formed_state st1 → well_formed_state st2
    374694
     695; setup_call_ok :
     696  ∀ n , parsT, call_args , st1 , st2 , prf1, prf2.
     697  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
     698  setup_call ?? (p' ?) n parsT call_args (sigma_state st1 prf1) =
     699  return (sigma_state st2 prf2)
     700; setup_call_wf :
     701  ∀ n , parsT, call_args , st1 , st2.
     702  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
     703  well_formed_state st1 → well_formed_state st2
     704 
     705; fetch_external_args_ok : (* TO BE CHECKED *)
     706  ∀ex_fun,st1,prf1,call_args.
     707  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
     708  fetch_external_args ?? (p' ?) ex_fun (sigma_state st1 prf1) call_args
     709; fetch_external_args_wf :
     710  ∀ex_fun,st1,call_args.
     711  well_formed_state st1 → ∃ l.
     712  fetch_external_args ?? (p' ?) ex_fun st1 call_args = OK ? l
     713 
     714; set_result_ok :
     715  ∀ l , call_dest , st1 , st2 , prf1 , prf2 .
     716  set_result ?? (p' ?) l call_dest st1 = return st2 →
     717  set_result ?? (p' ?) l call_dest (sigma_state st1 prf1) =
     718  return (sigma_state st2 prf2)
     719; set_result_wf :
     720  ∀ l , call_dest , st1 , st2  .
     721  set_result ?? (p' ?) l call_dest st1 = return st2 →
     722  well_formed_state st1 → well_formed_state st2 
     723 
     724; read_result_ok :
     725  let lin_prog ≝ linearise p graph_prog in
     726  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     727  let stack_sizes' ≝
     728   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     729     ? graph_prog stack_sizes in
     730  ∀call_dest , st1 , prf1, l1.
     731  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     732    call_dest st1 = return l1 →
     733  ∀prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
     734  read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     735    call_dest (sigma_state st1 prf1) = return opt_safe … prf
     736; read_result_wf :
     737  let lin_prog ≝ linearise p graph_prog in
     738  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     739  let stack_sizes' ≝
     740   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     741     ? graph_prog stack_sizes in
     742  ∀call_dest , st1 , l1.
     743  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     744    call_dest st1 = return l1 →
     745  well_formed_state st1 →
     746  m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?
     747 
     748; pop_frame_ok :
     749  let lin_prog ≝ linearise p graph_prog in
     750  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     751  let stack_sizes' ≝
     752   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     753     ? graph_prog stack_sizes in
     754  ∀ st1 , prf1, curr_id ,st2, prf2.
     755  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     756            curr_id st1 = return st2 →
     757 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
     758 let st2' ≝ sigma_state (st_no_pc ? st2) (proj2 … prf2) in
     759  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     760            (sigma_function_name p graph_prog curr_id) (sigma_state st1 prf1) =
     761            return mk_state_pc ? st2' pc'
     762; pop_frame_wf :
     763  let lin_prog ≝ linearise p graph_prog in
     764  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     765  let stack_sizes' ≝
     766   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     767     ? graph_prog stack_sizes in
     768  ∀ st1, curr_id ,st2.
     769  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     770            curr_id st1 = return st2 →
     771  well_formed_state st1 → well_formed_pc p p' graph_prog sigma (pc ? st2) ∧
     772      well_formed_state (st_no_pc ? st2)
    375773}.
    376774
     
    388786  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
    389787*)
    390 
    391 definition well_formed_state_pc :
    392  ∀p,p',graph_prog,sigma.
    393   good_sigma_state p p' graph_prog sigma →
    394   state_pc (make_sem_graph_params p p') → Prop ≝
    395  λp,p',prog,sigma,gss,st.
    396  well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st.
    397  
    398 definition sigma_state_pc :
    399  ∀p.
    400  ∀p':∀F.sem_unserialized_params p F.
    401  ∀graph_prog.
    402   ∀sigma.
    403 (*   let lin_prog ≝ linearise ? graph_prog in *)
    404   ∀gss : good_sigma_state p p' graph_prog sigma.
    405     ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
    406      well_formed_state_pc p p' graph_prog sigma gss s →
    407       state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
    408 
    409  λp,p',graph_prog,sigma,gss,s,prf.
    410  let pc' ≝ sigma_pc … (proj1 … prf) in
    411  let st' ≝ sigma_state … (proj2 … prf) in
    412  mk_state_pc ? st' pc'.
     788*)
    413789
    414790(*
     
    8291205  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    8301206    ? graph_prog stack_sizes in
    831  ∀sigma.∀gss : good_sigma_state … graph_prog sigma.
     1207 ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
    8321208 ∀fn,st,stmt,st'.
    8331209 ∀prf : well_formed_state … gss st.∀prf'.
     
    8401216  #fn #st #stmt
    8411217  #st' #prf #prf'
    842   cases daemon (*
    8431218  whd in match eval_seq_no_pc;
    8441219  cases stmt normalize nodelta
    845   [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) //
    846   | #mv_sig whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
     1220  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     1221  | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
     1222    >(pair_reg_move_ok ?????????? H) [% | skip]
     1223  | (* POP *)
     1224    #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
     1225    * #val #st1 * #vals_spec #H
     1226    cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ]
     1227    #wf_st1
     1228    lapply(acca_store_wf ????????? H wf_st1)
     1229    * #_ #sigma_val_spec
     1230    lapply vals_spec -vals_spec
     1231    whd in match pop; normalize nodelta
     1232    #H1 elim (bind_inversion ????? H1) -H1 * #g_bev #g_is * #ispop_spec
     1233    whd in ⊢ ((??%%) → ?); #EQ (*to be destructed*)
     1234    lapply ispop_spec -ispop_spec
     1235    whd in match is_pop; normalize nodelta
     1236    cases (istack ? st) normalize nodelta
     1237    [ #ABS whd in ABS : (???%); destruct(ABS)
     1238    | #one whd in ⊢ ((??%%) → ?); #EQ1 destruct(EQ1)
     1239      cases (istack ? (sigma_state … st prf)) normalize nodelta
     1240   
     1241    lapply (acca_store_ok ?????????????? H)
     1242
     1243   
     1244     -val_spec * #bv #is * #bv_is_spec
     1245    #EQ whd in EQ : (??%%); destruct(EQ)
     1246    whd in match is_pop in bv_is_spec; normalize nodelta in bv_is_spec;
     1247    inversion (istack ? st) in bv_is_spec;
     1248    [ #_ normalize nodelta whd in ⊢ ((???%) → ?); #ABS destruct(ABS)
     1249    | #bv1 #bv1_spec normalize nodelta whd in ⊢ ((??%%) → ?); #EQ destruct(EQ)
     1250    lapply(acca_store_wf ????????? H prf) check acca_store_ok check(acca_store_ok ?????????????? H)
     1251 
     1252  @(pair_reg_move_ok ? ? ? ? gss mv_sig st st' ? ?) whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
    8471253    #H
    848   ] *)
    8491254qed.       
    8501255       
Note: See TracChangeset for help on using the changeset viewer.