Changeset 2501


Ignore:
Timestamp:
Nov 29, 2012, 10:12:48 AM (7 years ago)
Author:
piccolo
Message:

working on lineariseProof. Not yet finished.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2495 r2501  
    200200qed.
    201201
     202lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.
     203** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed.
     204
     205axiom mem_ext_eq :
     206  ∀m1,m2 : mem.
     207  (∀b.let bc1 ≝ blocks m1 b in
     208      let bc2 ≝ blocks m2 b in
     209      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
     210      ∀z.contents bc1 z = contents bc2 z) →
     211  nextblock m1 = nextblock m2 → m1 = m2.
     212
    202213lemma beloadv_sigma_commute:
    203214∀p,p',graph_prog,sigma,m,ptr,bv,prf1.
     
    207218               return sigma_beval p p' graph_prog sigma bv prf2.
    208219#p #p' #graph_prog #sigma #m #ptr #bv #prf1
    209 whd in match beloadv in ⊢ (%→?); normalize nodelta
    210 whd 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) ]
    218 whd in match beloadv; normalize nodelta
    219 whd 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
     220whd in match beloadv;
     221whd in match do_if_in_bounds;
     222whd in match sigma_mem;
     223normalize nodelta
     224@If_elim #block_ok >block_ok normalize nodelta
     225[2: whd in ⊢ (???%→?); #ABS destruct(ABS) ]
     226@If_elim #H
     227[ elim (andb_true … H)
     228  #H1 #H2
     229  whd in match sigma_beval; normalize nodelta
     230  @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta
     231  whd in ⊢ (???%→?); #EQ' destruct
     232  >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe
     233| elim (andb_false … H) -H #H >H
     234  [2: >commutative_andb ] normalize nodelta
     235  whd in ⊢ (???%→?); #ABS destruct(ABS)
     236]
     237qed.
    225238
    226239lemma bestorev_sigma_commute :
    227240∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2.
    228241bestorev m ptr bv = return m' →
    229 ∃prf3.
     242∃prf3. 
    230243bestorev (sigma_mem p p' graph_prog sigma m prf1)
    231244          ptr
     
    233246=
    234247return (sigma_mem p p' graph_prog sigma m' prf3).
    235 cases daemon qed.
     248#p #p' #graph_prog #sigma #m #ptr #bv #m' #prf1 #prf2
     249whd in match bestorev;
     250whd in match do_if_in_bounds;
     251whd in match sigma_mem;
     252whd in match update_block;
     253 normalize nodelta
     254@If_elim #block_ok >block_ok normalize nodelta
     255[2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)]
     256@Zleb_elim_Type0 #H1
     257[ @Zltb_elim_Type0 #H2 ]
     258[2,3: #ABS normalize in ABS; destruct(ABS) ]
     259normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ)
     260%
     261[2: whd in ⊢ (???%);
     262  cut (∀X,a,b.a = b → Some X a = Some X b) [ // ]
     263  #aux @aux
     264  @mem_ext_eq [2: % ]
     265  #b @if_elim
     266  [2: #B
     267    @If_elim #prf1 @If_elim #prf2
     268    [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ]
     269    whd in match low_bound; whd in match high_bound;
     270    normalize nodelta
     271    cut (Not (bool_to_Prop (eq_block b (pblock ptr))))
     272    [ % #ABS >ABS in B; * ]
     273    -B #B % [ >B %% ] #z
     274    @If_elim #prf3 
     275    @If_elim #prf4
     276    [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ]
     277    whd in match sigma_beval in ⊢ (??%%); normalize nodelta
     278    @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
     279    >EQ2 #EQ destruct(EQ) %
     280  | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ]
     281    #EQ destruct(EQ)
     282    @If_elim whd in match low_bound; whd in match high_bound;
     283    normalize nodelta
     284    [2: >block_ok * #ABS elim (ABS I) ]
     285    #prf3 % [ >B %% ]
     286    #z whd in match update; normalize nodelta
     287    @eqZb_elim normalize nodelta #prf4
     288    [2: @If_elim #prf5 @If_elim #prf6
     289      [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ]
     290      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
     291      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
     292      normalize nodelta >(eqZb_false … prf4) >EQ2
     293      #EQ destruct(EQ) %
     294    | @If_elim #prf5
     295      [2: >B in prf5; normalize nodelta
     296        >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ]
     297      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
     298      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
     299      normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) %
     300    ]
     301  ]
     302| whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta
     303  @eq_block_elim #H normalize nodelta destruct
     304  #h2 #h3 whd in match update; normalize nodelta
     305  [ @eqZb_elim #H destruct normalize nodelta [ assumption ]]
     306  @prf1 assumption
     307]
     308qed.
    236309
    237310record good_sem_state_sigma
     
    330403qed.
    331404 *)
    332  definition sigma_pc :
     405definition sigma_pc :
    333406∀p,p',graph_prog.
    334407∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
     
    450523
    451524; acca_store__commute : helper_def_store__commute … gsss acca_store_
    452 
    453525; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
    454 
     526; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_
     527; accb_store_commute : helper_def_store__commute … gsss accb_store_
     528; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_
     529; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_
     530; dpl_store_commute : helper_def_store__commute … gsss dpl_store_
     531; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_
     532; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_
     533; dph_store_commute : helper_def_store__commute … gsss dph_store_
     534; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_
     535; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_
     536; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_
     537; pair_reg_move_commute : ∀mv,r1,r2,prf1.
     538  pair_reg_move_ ? ? (p' ?) r1 mv = return r2 →
     539  ∃prf2 .
     540  pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv =
     541    return sigma_regs p p' graph_prog sigma gsss r2 prf2
     542; allocate_locals_commute :
     543  ∀ loc, r1, prf1. ∃ prf2.
     544  allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
     545  sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
     546; save_frame_commute :
     547  ∀dest,st1,st2,prf1.
     548  save_frame ?? (p' ?) dest st1 = return st2 →
     549  let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1))
     550    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
     551  ∃prf2.
     552  save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2
     553; eval_ext_seq_commute :
     554  let lin_prog ≝ linearise p graph_prog in
     555  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     556  let stack_sizes' ≝
     557   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     558     ? graph_prog stack_sizes in
     559  ∀ext,fn,st1,st2,prf1.
     560  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     561    ext fn st1 = return st2 →
     562  ∃prf2.
     563  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     564    ext (sigma_function_name … fn) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     565   return sigma_state p p' graph_prog sigma gsss st2 prf2
     566; setup_call_commute :
     567  ∀ n , parsT, call_args , st1 , st2 , prf1.
     568  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
     569  ∃prf2.
     570  setup_call ?? (p' ?) n parsT call_args (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     571  return (sigma_state p p' graph_prog sigma gsss st2 prf2)
     572; fetch_external_args_commute : (* TO BE CHECKED *)
     573  ∀ex_fun,st1,prf1,call_args.
     574  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
     575  fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args
     576; set_result_commute :
     577  ∀ l , call_dest , st1 , st2 , prf1.
     578  set_result ?? (p' ?) l call_dest st1 = return st2 →
     579  ∃prf2.
     580  set_result ?? (p' ?) l call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     581  return (sigma_state p p' graph_prog sigma gsss st2 prf2) 
     582; read_result_commute :
     583  let lin_prog ≝ linearise p graph_prog in
     584  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     585  let stack_sizes' ≝
     586   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     587     ? graph_prog stack_sizes in
     588  ∀call_dest , st1 , prf1, l1.
     589  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     590    call_dest st1 = return l1 →
     591  ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
     592  read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     593    call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = return opt_safe … prf 
     594; pop_frame_commute :
     595  let lin_prog ≝ linearise p graph_prog in
     596  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
     597  let stack_sizes' ≝
     598   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
     599     ? graph_prog stack_sizes in
     600  ∀ st1 , prf1, curr_id ,st2.
     601  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     602            curr_id st1 = return st2 →
     603 ∃prf2.
     604 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
     605 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in
     606  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     607            (sigma_function_name p graph_prog curr_id) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     608            return mk_state_pc ? st2' pc'
    455609}.
    456610
     
    467621    (sigma_beval p p' graph_prog sigma bv prf1')
    468622    (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
    469 cases daemon qed.
     623#p #p' #graph_prog #sigma #X #store #gsss #H #a #bv #st #st #prf1 #prf2
     624whd in match helper_def_store; normalize nodelta
     625#H1 elim(bind_inversion ????? H1) -H1 #graph_reg * #store_spec
     626#EQ whd in EQ : (??%%); destruct(EQ)
     627elim(H a bv ?? (proj2 … (proj1 … prf1)) prf2 store_spec)
     628#wf_graph_reg #store_spec1 %
     629[ % [ % ] [%] ]
     630[ @(proj1 … (proj1 … (proj1 … prf1)))
     631| @(proj2 … (proj1 … (proj1 … prf1)))
     632| @wf_graph_reg
     633| @(proj2 … prf1)
     634] >store_spec1 >m_return_bind %
     635qed.
     636
     637
    470638
    471639lemma retrieve_commute :
     
    480648     helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
    481649     return sigma_beval p p' graph_prog sigma bv prf2.
    482 cases daemon qed.
     650#p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #bv #prf1
     651whd in match helper_def_retrieve; normalize nodelta
     652#retrieve_spec elim(H … (proj2 … (proj1 … prf1)) … retrieve_spec)
     653#wf_bv #retrieve_spec1 %{wf_bv} >retrieve_spec1 %
     654qed.
    483655
    484656(*
     
    495667λp,p',graph_prog,sigma.
    496668λgss : good_state_sigma p p' graph_prog sigma.
    497 store_commute … gss (acca_store__commute … gss).*)
     669store_commute … gss (acca_store__commute … gss).
    498670 
    499671   
     
    525697
    526698#p #p' #
    527 (*
    528 ; acca_store_wf :  ∀a,bv,st,st'.
    529   sigma_beval_opt p p' graph_prog sigma bv ≠ None ? →
    530   acca_store ?? (p' ?) a bv st = return st' →
    531   well_formed_state st → well_formed_state st'
    532 
    533 ; acca_retrieve_wf :  ∀a,st,bv.
    534   acca_retrieve ?? (p' ?) st a = return bv →
    535   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    536 
    537 ; acca_arg_retrieve_ok :
    538   ∀a,st,bv,prf1,prf2.
    539   acca_arg_retrieve ?? (p' ?) st a = return bv →
    540   acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
    541   return sigma_beval p p' graph_prog sigma bv prf2
    542 ; acca_arg_retrieve_wf :  ∀a,st,bv.
    543   acca_arg_retrieve ?? (p' ?) st a = return bv →
    544   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    545 
    546 ; accb_store_ok :
    547   ∀a,bv,bv',st,st',prf1,prf2.
    548   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
    549   accb_store ?? (p' ?) a bv st = return st' →
    550   accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
    551 ; accb_store_wf :  ∀a,bv,bv',st,st'.
    552   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
    553   accb_store ?? (p' ?) a bv st = return st' →
    554   well_formed_state st → well_formed_state st'
    555 
    556 ; accb_retrieve_ok :
    557   ∀a,st,bv,prf1,prf2.
    558   accb_retrieve ?? (p' ?) st a = return bv →
    559   accb_retrieve ?? (p' ?) (sigma_state st prf1) a =
    560   return sigma_beval p p' graph_prog sigma bv prf2
    561 ; accb_retrieve_wf :  ∀a,st,bv.
    562   accb_retrieve ?? (p' ?) st a = return bv →
    563   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    564 
    565 ; accb_arg_retrieve_ok :
    566   ∀a,st,bv,prf1,prf2.
    567   acca_arg_retrieve ?? (p' ?) st a = return bv →
    568   acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
    569   return sigma_beval p p' graph_prog sigma bv prf2
    570 ; accb_arg_retrieve_wf :  ∀a,st,bv.
    571   accb_arg_retrieve ?? (p' ?) st a = return bv →
    572   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    573 
    574 
    575 ; dpl_store_ok :
    576   ∀a,bv,bv',st,st',prf1,prf2.
    577   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
    578   dpl_store ?? (p' ?) a bv st = return st' →
    579   dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
    580 ; dpl_store_wf :  ∀a,bv,bv',st,st'.
    581   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
    582   dpl_store ?? (p' ?) a bv st = return st' →
    583   well_formed_state st → well_formed_state st'
    584 
    585 ; dpl_retrieve_ok :
    586   ∀a,st,bv,prf1,prf2.
    587   dpl_retrieve ?? (p' ?) st a = return bv →
    588   dpl_retrieve ?? (p' ?) (sigma_state st prf1) a =
    589   return sigma_beval p p' graph_prog sigma bv prf2
    590 ; dpl_retrieve_wf :  ∀a,st,bv.
    591   dpl_retrieve ?? (p' ?) st a = return bv →
    592   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    593 
    594 ; dpl_arg_retrieve_ok :
    595   ∀a,st,bv,prf1,prf2.
    596   acca_arg_retrieve ?? (p' ?) st a = return bv →
    597   acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
    598   return sigma_beval p p' graph_prog sigma bv prf2
    599 ; dpl_arg_retrieve_wf :  ∀a,st,bv.
    600   dpl_arg_retrieve ?? (p' ?) st a = return bv →
    601   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    602 
    603 
    604 ; dph_store_ok :
    605   ∀a,bv,bv',st,st',prf1,prf2.
    606   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
    607   dph_store ?? (p' ?) a bv st = return st' →
    608   dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
    609 ; dph_store_wf :  ∀a,bv,bv',st,st'.
    610   sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
    611   dph_store ?? (p' ?) a bv st = return st' →
    612   well_formed_state st → well_formed_state st'
    613 
    614 ; dph_retrieve_ok :
    615   ∀a,st,bv,prf1,prf2.
    616   dph_retrieve ?? (p' ?) st a = return bv →
    617   dph_retrieve ?? (p' ?) (sigma_state st prf1) a =
    618   return sigma_beval p p' graph_prog sigma bv prf2
    619 ; dph_retrieve_wf :  ∀a,st,bv.
    620   dph_retrieve ?? (p' ?) st a = return bv →
    621   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    622 
    623 ; dph_arg_retrieve_ok :
    624   ∀a,st,bv,prf1,prf2.
    625   acca_arg_retrieve ?? (p' ?) st a = return bv →
    626   acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
    627   return sigma_beval p p' graph_prog sigma bv prf2
    628 ; dph_arg_retrieve_wf :  ∀a,st,bv.
    629   dph_arg_retrieve ?? (p' ?) st a = return bv →
    630   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    631 
    632 
    633 ; snd_arg_retrieve_ok :
    634   ∀a,st,bv,prf1,prf2.
    635   snd_arg_retrieve ?? (p' ?) st a = return bv →
    636   snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
    637   return sigma_beval p p' graph_prog sigma bv prf2
    638 ; snd_arg_retrieve_wf :  ∀a,st,bv.
    639   snd_arg_retrieve ?? (p' ?) st a = return bv →
    640   well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
    641 
    642 ; pair_reg_move_ok :
    643   ∀mv,st1,st2,prf1,prf2.
    644   pair_reg_move ?? (p' ?) st1 mv = return st2 →
    645   pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv =
    646     return sigma_state st2 prf2
    647 ; pair_reg_move_wf :
    648   ∀mv,st1,st2.
    649   pair_reg_move ?? (p' ?) st1 mv = return st2 →
    650   well_formed_state st1 → well_formed_state st2
    651 
    652 ; allocate_locals_ok :
    653   ∀l,st1,prf1,prf2.
    654   allocate_locals ?? (p' ?) l (sigma_state st1 prf1) =
    655     sigma_state (allocate_locals ?? (p' ?) l st1) prf2
    656 ; allocate_locals_wf :
    657   ∀l,st1.
    658   well_formed_state st1 →
    659     well_formed_state (allocate_locals ?? (p' ?) l st1)
    660 
    661 ; save_frame_ok :
    662   ∀dest,st1,st2,prf1,prf2.
    663   save_frame ?? (p' ?) dest st1 = return st2 →
    664   let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1))
    665     (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
    666   save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2
    667 ; save_frame_wf :
    668   ∀dest,st1,st2.
    669   save_frame ?? (p' ?) dest st1 = return st2 →
    670   (well_formed_pc p p' graph_prog sigma (pc … st1) ∧
    671    well_formed_state st1) → well_formed_state st2
    672 
    673 ; eval_ext_seq_ok :
    674   let lin_prog ≝ linearise p graph_prog in
    675   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    676   let stack_sizes' ≝
    677    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    678      ? graph_prog stack_sizes in
    679   ∀ext,fn,st1,st2,prf1,prf2.
    680   eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    681     ext fn st1 = return st2 →
    682   eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    683     ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2
    684 ; eval_ext_seq_wf :
    685   let lin_prog ≝ linearise p graph_prog in
    686   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    687   let stack_sizes' ≝
    688    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    689      ? graph_prog stack_sizes in
    690   ∀ext,fn,st1,st2.
    691   eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    692     ext fn st1 = return st2 →
    693   well_formed_state st1 → well_formed_state st2
    694 
    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)
    773 }.
     699*)
    774700
    775701(* restano:
     
    785711; pop_frame: ∀globals.∀ge : genv_gen F globals.
    786712  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
    787 *)
    788713*)
    789714
     
    12071132 ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
    12081133 ∀fn,st,stmt,st'.
    1209  ∀prf : well_formed_state … gss st.∀prf'.
     1134 ∀prf : well_formed_state … gss st.
    12101135  eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
    12111136   fn st stmt = return st' →
     1137  ∃prf'.
    12121138  eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
    12131139    (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
     
    12151141  #p #p' #graph_prog #stack_sizes #sigma #gss
    12161142  #fn #st #stmt
    1217   #st' #prf #prf'
     1143  #st' #prf
    12181144  whd in match eval_seq_no_pc;
    12191145  cases stmt normalize nodelta
    1220   [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) //
     1146  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
    12211147  | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
    1222     >(pair_reg_move_ok ?????????? H) [% | skip]
     1148    change with
     1149     (pair_reg_move p (joint_closed_internal_function (make_sem_graph_params p p'))
     1150                      (make_sem_graph_params p p') ??) in H : (??%?);
     1151    lapply H -H
     1152    whd in match pair_reg_move; normalize nodelta #H
     1153    elim(bind_inversion ????? H) -H #reg * #reg_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1154    elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec)
     1155    #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %]
     1156    % [ 2: @(proj2 … prf)
     1157      |    % [2: assumption] %
     1158             [ @(proj1 … (proj1 … (proj1 … prf)))
     1159             | @(proj2 … (proj1 … (proj1 … prf)))
     1160             ]
     1161      ]
    12231162  | (* POP *)
    12241163    #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
    12251164    * #val #st1 * #vals_spec #H
     1165    change with (acca_store p
     1166                          (joint_closed_internal_function (make_sem_graph_params p p'))
     1167                          (make_sem_graph_params p p') a val st1 = ?) in H;
     1168    change with (pop (make_sem_graph_params p p') ? = ?) in vals_spec;
     1169    lapply vals_spec -vals_spec
     1170    whd in match pop; normalize nodelta
     1171    whd in match is_pop; normalize nodelta
     1172    lapply(proj2 … (proj1 … (proj1 … prf))) #wf_is
     1173    inversion (istack (make_sem_graph_params p p') st) normalize nodelta
     1174    [#_ #ABS normalize in ABS; destruct(ABS)]
     1175    [ #Bv | #Bv_not_used #Bv] #is_stack_st_spec >m_return_bind
     1176    #EQ whd in EQ : (??%%); destruct(EQ)
     1177    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ?????? H)
     1178    [ 2,5: @hide_prf >is_stack_st_spec in wf_is; #wf_is
     1179           whd in match sigma_is_opt in wf_is; normalize nodelta in wf_is;
     1180           inversion(sigma_beval_opt ?????)
     1181           [1,3 : #EQ >EQ in wf_is; whd in ⊢ ((?(??%?)) → ?); * #ABS @⊥ @ABS //
     1182                  inversion(sigma_beval_opt ?????) normalize nodelta
     1183                  [ #bev %
     1184                  | #bev #bev_s >bev_s in ABS; normalize nodelta
     1185                    #ABS @⊥ @ABS normalize %
     1186                  ]
     1187           ]
     1188           [#H1 #H2 % #ABS destruct(ABS) | #H1 #H2 % #ABS destruct(ABS)]
     1189    ]
     1190    [ 2,4: @hide_prf % [2,4 : @(proj2 … prf)] % [2,4 : @(proj2 … (proj1 … prf))]
     1191             % [1,3 : @(proj1 … (proj1 … (proj1 … prf)))]
     1192             whd in match sigma_is_opt; normalize nodelta
     1193             [ whd in ⊢ (? (??%?)); % #ABS destruct(ABS)]
     1194             >is_stack_st_spec in wf_is;
     1195             whd in match sigma_is_opt; normalize nodelta
     1196             cases(sigma_beval_opt ?????)
     1197             [ normalize * #ABS @⊥ @ABS %
     1198             | #bev #_ normalize % #ABS destruct(ABS)
     1199             ]
     1200     ] 
     1201     #prf' #acca_store_commute %{prf'}     
     1202    whd in match sigma_state in ⊢ (??(????(?????(?????%?)?))?);
     1203    whd in match sigma_is; normalize nodelta
     1204    @opt_safe_elim #int_stack #int_stack_sigma_spec
     1205    >is_stack_st_spec in int_stack_sigma_spec;
     1206    whd in match sigma_is_opt; normalize nodelta
     1207    #IS_SPEC elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
     1208    [ #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1209    | #sigma_bv_not_used * #sigma_bv_not_used_spec #IS_SPEC
     1210      elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
     1211      #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]
     1212      normalize nodelta >m_return_bind
     1213     
     1214     
     1215     
     1216      #INUTILE #H <H
     1217     
     1218     
     1219     
     1220    inversion(istack ??) normalize nodelta [
     1221    whd in match (istack ??);
     1222    whd in match sigma_state in ⊢ (??%?); normalize nodelta
     1223  acca_store p(joint_closed_internal_function
     1224   (make_sem_lin_params p p'))
     1225  (make_sem_lin_params p p') a v st1
     1226  =return sigma_state p p' graph_prog sigma gss st' prf')
     1227
     1228   
     1229   
    12261230    cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ]
    12271231    #wf_st1
     
    12391243      cases (istack ? (sigma_state … st prf)) normalize nodelta
    12401244   
    1241     lapply (acca_store_ok ?????????????? H)
     1245    lapply (acca_store_ ???????????????????????? H)
    12421246
    12431247   
Note: See TracChangeset for help on using the changeset viewer.