Changeset 2529


Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2484 r2529  
    1515 { prog_spars : sem_params
    1616 ; prog : joint_program prog_spars
    17  ; stack_sizes : (Σi.is_internal_function_of_program … prog i) →
     17 ; stack_sizes : ident → option
    1818(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1919 }.
     
    7878  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    7979  let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
    80   let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
     80  let spp : xpointer ≝
     81    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
     82     pi2 … spb» in
    8183(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    8284  let main ≝ prog_main … p in
     
    8688  ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ;
    8789  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    88   ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
    89   match ? return λx.description_of_function … main = x → ? with
    90   [ Internal fn ⇒ λprf.
    91     let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in
    92     ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
    93     let pc' ≝ eval_internal_call_pc … ge main in
     90  ! bl ← block_of_call … ge st_pc0 (inl … main) ;
     91  ! 〈i, fn〉 ← fetch_function … ge bl ;
     92  match fn with
     93  [ Internal ifn ⇒
     94    ! st' ← eval_internal_call_no_pc … ge i ifn (call_args_for_main … pars) st_pc0 ;
     95    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    9496    return mk_state_pc … st' pc'
    95   | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    96   ] (refl …).
    97   [ @(description_of_internal_function … prf)
    98   | cases spb normalize //
    99   ]
    100 qed.
     97  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
     98  ].
    10199
    102100definition joint_classify_seq :
     
    105103  match stmt with
    106104  [ CALL f args dest ⇒
    107     match function_of_call ?? (ev_genv p) st f with
    108     [ OK fn ⇒
    109       match description_of_function … fn with
     105    match (! bl ← block_of_call … (ev_genv p) st f ;
     106            fetch_function … (ev_genv p) bl) with
     107    [ OK id_fn ⇒
     108      match \snd id_fn with
    110109      [ Internal _ ⇒ cl_call
    111110      | External _ ⇒ cl_other
     
    136135  ∀p : evaluation_params.state_pc p → status_class ≝
    137136  λp,st.
    138   match fetch_statement ? p … (ev_genv p) (pc … st) with
    139   [ OK f_s ⇒
    140     match \snd f_s with
     137  match fetch_statement … (ev_genv p) (pc … st) with
     138  [ OK i_f_s ⇒
     139    match \snd i_f_s with
    141140    [ sequential s _ ⇒ joint_classify_step p st s
    142141    | final s ⇒ joint_classify_final p s
     
    145144  ].
    146145
     146definition no_call : ∀p,g.joint_seq p g → Prop ≝
     147  λp,g,s.match s with
     148  [ CALL _ _ _ ⇒ False
     149  | _ ⇒ True
     150  ].
     151
     152definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
     153  λp,g,s.match s with
     154  [ COST_LABEL _ ⇒ False
     155  | _ ⇒ True
     156  ].
     157
     158lemma no_call_advance : ∀p : evaluation_params.
     159∀s,nxt.∀st : state_pc p.
     160no_call p (globals p) s →
     161eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st.
     162#p * // #f #args #dest #nxt #st *
     163qed.
     164
     165lemma no_call_other : ∀p : evaluation_params.∀st,s.
     166no_call p (globals p) s →
     167joint_classify_seq … st s = cl_other.
     168#p #st * // #f #args #dest *
     169qed.
     170
     171lemma cond_call_other :
     172  ∀p,globals.∀P : joint_step p globals → Prop.
     173  (∀a,lbltrue.P (COND … a lbltrue)) →
     174  (∀f,args,dest.P (CALL … f args dest)) →
     175  (∀s.no_call ?? s → P s) →
     176  ∀s.P s.
     177#p #globals #P #H1 #H2 #H3 * // * /2 by / qed.
     178
    147179lemma joint_classify_call : ∀p : evaluation_params.∀st.
    148180  joint_classify p st = cl_call →
    149   ∃f,f',args,dest,next,fn,fd.
    150   fetch_statement ? p … (ev_genv p) (pc … st) =
    151     OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
    152   function_of_call … (ev_genv p) st f' = OK ? fn
    153   description_of_function … (ev_genv p) fn = Internal … fd.
     181  ∃i_f,f',args,dest,next,bl,i',fd'.
     182  fetch_statement … (ev_genv p) (pc … st) =
     183    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
     184  block_of_call … (ev_genv p) st f' = OK ? bl
     185  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
    154186#p #st
    155187whd in match joint_classify; normalize nodelta
    156 inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta
    157 [ * #f * [| * [ #lbl || #b #f #args ]]
    158   [ * [| #a #lbl #next ]
    159     [ *
    160       [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
    161       | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
    162       | #ext ] #next
    163       [ whd in match joint_classify_step; whd in match joint_classify_seq;
    164         normalize nodelta
    165         inversion (function_of_call ?????) normalize nodelta
    166         [ #fn
    167           inversion (description_of_function ?? fn) #fd
    168           #EQfd
    169         | #e
    170         ] #EQfn
    171       ]
     188inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta
     189[2: #e #_ #ABS destruct(ABS) ]
     190* #i_f * [2: * [ #lbl | | #fl #f #args ] #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     191@cond_call_other
     192[ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
     193|3: #s #no_call #nxt #_ whd in match joint_classify_step;
     194  normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS)
     195]
     196#f' #args #dest #nxt #fetch
     197whd in match joint_classify_step; whd in match joint_classify_seq;
     198normalize nodelta
     199inversion (block_of_call ?????)
     200[ #bl #block_of_c  >m_return_bind
     201  inversion (fetch_function ???)
     202  [ * #i' *
     203    [ #fd' #fetch' #_
     204      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
     205      % [ %{block_of_c} % ]
     206      whd in match fetch_internal_function; normalize nodelta
     207      >fetch' %
    172208    ]
    173209  ]
    174 | #e
    175 ] #EQfetch
    176 [|*: #ABS normalize in ABS; destruct(ABS) ]
    177 normalize nodelta #_
    178 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd}
    179 %{EQfd} %{EQfn} %
     210]
     211#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
    180212qed.
    181213
     
    183215  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
    184216λp,s1,s2.
    185 match fetch_statement ? p … (ev_genv p) (pc … s1) with
     217match fetch_statement … (ev_genv p) (pc … s1) with
    186218[ OK x ⇒
    187219  match \snd x with
    188220  [ sequential s next ⇒
    189     pc … s2 = succ_pc p p (pc … s1) next
     221    pc … s2 = succ_pc p (pc … s1) next
    190222  | _ ⇒ False (* never happens *)
    191223  ]
     
    225257   I think handling of the function is easier *)
    226258λp,st.
    227 let dummy : ident ≝ an_identifier ? one in
    228 match fetch_statement ? p … (ev_genv p) (pc … st) with
     259let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     260match fetch_statement … (ev_genv p) (pc … st) with
    229261[ OK x ⇒
    230262  match \snd x with
     
    234266      match s with
    235267      [ CALL f' args dest ⇒
    236         match function_of_call … (ev_genv p) st f' with
    237         [ OK f ⇒ f
     268        match
     269          (! bl ← block_of_call … (ev_genv p) st f' ;
     270           fetch_internal_function … (ev_genv p) bl) with
     271        [ OK i_f ⇒ \fst i_f
    238272        | _ ⇒ dummy
    239273        ]
     
    279313  | _ ⇒ None ?
    280314  ].
     315
     316
     317lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
     318no_cost_label p (globals p) s →
     319cost_label_of_stmt … (sequential … s nxt) = None ?.
     320#p * // #lbl #next *
     321qed.
    281322
    282323definition joint_abstract_status :
     
    293334   (* as_label_of_pc ≝ *)
    294335    (λpc.
    295       match fetch_statement ? p … (ev_genv p) pc with
     336      match fetch_statement … (ev_genv p) pc with
    296337      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
    297338      | _ ⇒ None ?
     
    300341   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
    301342   (* as_call_ident ≝ *) (joint_call_ident p).
     343
  • src/joint/linearise.ma

    r2481 r2529  
    173173    ] n_prf
    174174  ] (chop_ok ? (λx.x∈visited) visiting).
    175 (*cases daemon qed. *)
     175(* cases daemon qed. *)
    176176whd
    177177[ (* base case, visiting is all visited *)
     
    555555qed.
    556556
    557 
    558557definition good_local_sigma :
    559558  ∀p:unserialized_params.
     
    565564  λp,globals,g,entry,c,sigma.
    566565    sigma entry = Some ? 0 ∧
     566    (∀l,n.point_of_label … c l = Some ? n → sigma l = Some ? n) ∧
    567567    ∀l,n.sigma l = Some ? n →
    568       ∃s. lookup … g l = Some ? s ∧
    569         opt_Exists ?
    570           (λls.let 〈lopt, ts〉 ≝ ls in
    571             opt_All ? (eq ? l) lopt ∧
    572             ts = graph_to_lin_statement … s ∧
    573             opt_All ?
    574               (λnext.Or (sigma next = Some ? (S n))
    575               (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    576               (stmt_implicit_label … s)) (nth_opt … n c).
     568      ∃s. stmt_at … g l = Some ? s ∧
     569        All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
     570        opt_All ?
     571            (λnext.Or (sigma next = Some ? (S n))
     572            (stmt_at … c (S n) = Some ? (GOTO … next)))
     573            (stmt_implicit_label … s) ∧
     574        stmt_at … c n = Some ? (graph_to_lin_statement … s).
    577575
    578576definition linearise_code:
     
    624622#entry_O #req_vis #last_fin #labels_in_req #sigma_prop
    625623%
    626 [ % [assumption]
    627   #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
    628   #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
    629   % [2: % [ assumption ] |]
    630   >nth_opt_filter_labels in ⊢ (???%);
    631   >nth_opt_is_stmt >m_return_bind whd >m_return_bind
    632   % [ % ]
    633   [ elim (lbl ∈ required) %
    634   | %
    635   | lapply succ_is_in
    636     lapply (refl … (stmt_implicit_label … stmt))
    637     cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %]
    638     #next #EQ_next *
    639     [ #H %1{H} ]
    640     #H %2
    641     >nth_opt_filter_labels >H %
     624[ % [ % [assumption]]
     625  #lbl #n
     626  [ change with (If ? then with prf do ? else ? = ? → ?)
     627    @If_elim [2: #_ #ABS destruct(ABS) ]
     628    #H lapply H
     629    >occurs_exactly_once_filter_labels
     630    elim (true_or_false_Prop … (occurs_exactly_once ?? lbl ?))
     631    [1,2: #H1 >H1 |*:] [2: * ]
     632    elim (true_or_false_Prop … (lbl ∈ required)) #H2 >H2 *
     633    lapply (in_map_domain … visited lbl) >(req_vis … H2)
     634    * #n_lbl #EQsigma
     635    elim (sigma_prop … EQsigma) #_ * #stmt ** #_ #EQnth_opt #_
     636    >(nth_opt_index_of_label ???? n_lbl (graph_to_lin_statement … stmt) H)
     637    [ normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption
     638    | >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind
     639      >H2 %
     640    ]
     641  | #eq_lookup elim (sigma_prop ?? eq_lookup)
     642    #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
     643    % [2: % [ % [ % [ assumption ]]] |]
     644    [ @All_append
     645      [ lapply succ_is_in elim (stmt_implicit_label ???) [ * % ]
     646        #nxt #nxt_spec % [2: %] cases nxt_spec -nxt_spec
     647        [ #EQ >EQ % #ABS destruct(ABS)
     648        | #goto_in lapply (in_map_domain … visited nxt)
     649          >req_vis [ * #n #EQ >EQ % #ABS destruct(ABS) ]
     650          @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
     651          whd in ⊢ (??%?); >goto_in %
     652        ]
     653      | <graph_to_lin_labels @(All_mp … (labels_in_req …))
     654        [ #lbl #H
     655          lapply (in_map_domain … visited lbl) >(req_vis … H) * #n #EQ >EQ % #ABS destruct(ABS)
     656        | whd in ⊢ (??%?); >nth_opt_is_stmt % |
     657        ]
     658      ]
     659    | lapply succ_is_in
     660      cases (stmt_implicit_label … stmt) [#_ %]
     661      #next *
     662      [ #H %1{H} ]
     663      #H %2
     664      >stmt_at_filter_labels whd in ⊢ (??%?); >H %
     665    | >stmt_at_filter_labels whd in ⊢ (??%?); >nth_opt_is_stmt %
     666    ]
    642667  ]
    643668| #i #s
     
    711736[ @H2
    712737| @H1
    713 | cases H1 #H3 #H4 elim (H4 … H3)
    714   #s * #_ >lin_code_has_point cases code
    715   [ * | #hd #tl #_ % ]
     738| cases H1 * #H3 #H4 #H5 elim (H5 … H3)
     739  #s *** #_ #_ #_ >lin_code_has_point cases code
     740  [ #ABS normalize in ABS; destruct(ABS) | #hd #tl #_ % ]
    716741]
    717742qed.
     
    724749    (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).
    725750
    726 
     751(*
    727752definition good_sigma :
    728753  ∀p:unserialized_params.
     
    742767#p #prog
    743768letin sigma ≝
    744   (λi : Σi.is_internal_function_of_program … prog i.
    745     let fn_in ≝ if_of_function … i in
     769  (λi : Σi.is_internal_function_of_program … prog i.    let fn_in ≝ if_of_function … i in
    746770    \snd (linearise_int_fun … fn_in))
    747771%{sigma}
     
    751775normalize nodelta #prf @prf
    752776qed.
     777*)
  • src/joint/lineariseProof.ma

    r2528 r2529  
    2626  (∀F.sem_unserialized_params p F) →
    2727    ∀prog : joint_program (mk_graph_params p).
    28   ((Σi.is_internal_function_of_program … prog i) → ℕ) →
     28  (ident → option ℕ) →
    2929     abstract_status
    3030 ≝
     
    4040  (∀F.sem_unserialized_params p F) →
    4141    ∀prog : joint_program (mk_lin_params p).
    42   ((Σi.is_internal_function_of_program … prog i) → ℕ) →
     42  (ident → option ℕ) →
    4343     abstract_status
    4444 ≝
     
    9797*)
    9898
     99definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p).
     100  joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) →
     101    label → option ℕ.
     102   
    99103definition sigma_pc_opt:
    100  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    101   ((Σi.is_internal_function_of_program … graph_prog i) →
    102     code_point (mk_graph_params p) → option ℕ) →
     104 ∀p,p'.∀graph_prog.
     105  sigma_map p graph_prog →
    103106   program_counter → option program_counter
    104107 ≝
     
    106109  let pars ≝ make_sem_graph_params p p' in
    107110  let ge ≝ globalenv_noinit … prog in
    108   ! f ← int_funct_of_block ? ge (pc_block pc) ;
    109   ! lin_point ← sigma f (point_of_pc ? pars pc) ;
    110   return pc_of_point ? (make_sem_lin_params ? p') pc lin_point.
     111  ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
     112  ! lin_point ← sigma fd (point_of_pc pars pc) ;
     113  return pc_of_point
     114  (make_sem_lin_params ? p') (pc_block pc) lin_point.
    111115
    112116definition well_formed_pc:
    113117 ∀p,p',graph_prog.
    114   ((Σi.is_internal_function_of_program … graph_prog i) →
    115     label → option ℕ) →
     118  sigma_map p graph_prog →
    116119   program_counter → Prop
    117120 ≝
     
    122125definition sigma_beval_opt :
    123126 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    124   ((Σi.is_internal_function_of_program … graph_prog i) →
    125     code_point (mk_graph_params p) → option ℕ) →
     127  sigma_map p graph_prog →
    126128  beval → option beval ≝
    127129λp,p',graph_prog,sigma,bv.
     
    138140definition sigma_is_opt :
    139141 ∀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  sigma_map p graph_prog →
    142143  internal_stack → option internal_stack ≝
    143144λp,p',graph_prog,sigma,is.
     
    167168definition well_formed_mem :
    168169 ∀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 ℕ) →
     170  sigma_map p graph_prog →
    171171 bemem → Prop ≝
    172172λp,p',graph_prog,sigma,m.
     
    311311  (p : unserialized_params)
    312312  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
    313  (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
    314     graph_prog i) →
    315       label → option ℕ) : Type[0] ≝
     313  (sigma : sigma_map p graph_prog) : Type[0] ≝
    316314{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
    317315; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
     
    340338definition well_formed_state :
    341339 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    342  ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
    343     code_point (mk_graph_params p) → option ℕ).
     340 ∀sigma.
    344341 good_sem_state_sigma p p' graph_prog sigma →
    345342 state (make_sem_graph_params p p') → Prop ≝
     
    352349definition sigma_state :
    353350 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    354  ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
    355     code_point (mk_graph_params p) → option ℕ).
     351 ∀sigma.
    356352 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    357353 ∀st : state (make_sem_graph_params p p').
     
    409405definition sigma_pc :
    410406∀p,p',graph_prog.
    411 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
    412     label → option ℕ).
     407∀sigma.
    413408∀pc.
    414409∀prf : well_formed_pc p p' graph_prog sigma pc.
     
    447442 let st' ≝ sigma_state … (proj2 … prf) in
    448443 mk_state_pc ? st' pc'.
    449 
     444(*
    450445definition sigma_function_name :
    451446 ∀p,graph_prog.
     
    454449  (Σf.is_internal_function_of_program … lin_prog f) ≝
    455450λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
    456 
     451*)
    457452lemma m_list_map_All_ok :
    458453  ∀M : MonadProps.∀X,Y,f,l.
     
    520515  (p : unserialized_params)
    521516  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
    522  (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
    523     graph_prog i) →
    524       label → option ℕ)
     517  (sigma : sigma_map p graph_prog)
    525518: Type[0] ≝
    526519{ gsss :> good_sem_state_sigma p p' graph_prog sigma
     
    557550; eval_ext_seq_commute :
    558551  let lin_prog ≝ linearise p graph_prog in
    559   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    560   let stack_sizes' ≝
    561    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    562      ? graph_prog stack_sizes in
    563   ∀ext,fn,st1,st2,prf1.
    564   eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    565     ext fn st1 = return st2 →
     552  ∀stack_sizes.
     553  ∀ext,i,fn,st1,st2,prf1.
     554  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     555    ext i fn st1 = return st2 →
    566556  ∃prf2.
    567557  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    568     ext (sigma_function_name … fn) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     558    ext i (\fst (linearise_int_fun … fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    569559   return sigma_state p p' graph_prog sigma gsss st2 prf2
    570560; setup_call_commute :
     
    586576; read_result_commute :
    587577  let lin_prog ≝ linearise p graph_prog in
    588   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    589   let stack_sizes' ≝
    590    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    591      ? graph_prog stack_sizes in
     578  ∀stack_sizes.
    592579  ∀call_dest , st1 , prf1, l1.
    593   read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
     580  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
    594581    call_dest st1 = return l1 →
    595582  ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
     
    598585; pop_frame_commute :
    599586  let lin_prog ≝ linearise p graph_prog in
    600   ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    601   let stack_sizes' ≝
    602    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    603      ? graph_prog stack_sizes in
    604   ∀ st1 , prf1, curr_id ,st2.
    605   pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
    606             curr_id st1 = return st2 →
     587  ∀stack_sizes.
     588  ∀ st1 , prf1, curr_id , curr_fn ,st2.
     589  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     590            curr_id curr_fn st1 = return st2 →
    607591 ∃prf2.
    608592 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
    609593 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in
    610594  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    611             (sigma_function_name p graph_prog curr_id) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
     595            curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    612596            return mk_state_pc ? st2' pc'
    613597}.
     
    672656λgss : good_state_sigma p p' graph_prog sigma.
    673657store_commute … gss (acca_store__commute … gss).
    674  
    675    
    676 lemma acca_store_commute :
    677   ∀p,p',graph_prog,sigma.
    678   ∀gss : good_state_sigma p p' graph_prog sigma.
    679   ∀a,bv,st,st',prf1,prf1'.
    680   acca_store ?? (p' ?) a bv st = return st' →
    681   ∃prf2.
    682   acca_store ?? (p' ?) a
    683     (sigma_beval p p' graph_prog sigma bv prf1')
    684     (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝
    685 λp,p',graph_prog,sigma,gss,a,bv.?.
    686 * #frms #is #carry #regs #m
    687 * #frms' #is' #carry' #regs' #m'
    688 *** #frms_ok #is_ok #regs_ok #mem_ok
    689 #bv_ok #EQ1 elim (bind_inversion ????? EQ1)
    690 #regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
    691 elim (acca_store__commute … gss … EQ1)
    692 [ #prf2 #EQ2
    693   % [ whd /4 by conj/ ]
    694   change with (! r ← ? ; ? = ?) >EQ2
    695   whd in match (sigma_state ???????); normalize nodelta
    696    >m_return_bind
    697 
    698 
    699 st,st',prf1,prf2,prf3.?.
    700 
    701 
    702 #p #p' #
     658
    703659*)
    704660
     
    729685#A * #x #v normalize #EQ destruct % qed.
    730686
     687(*
    731688lemma if_of_function_commute:
    732689 ∀p.
     
    739696 #p #graph_prog #graph_fun whd
    740697 @prog_if_of_function_transform % qed.
    741 
    742 lemma bind_opt_inversion:
    743   ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
    744   (! x ← f ; g x = Some … y) →
    745   ∃x. (f = Some … x) ∧ (g x = Some … y).
    746 #A #B #f #g #y cases f normalize
    747 [ #H destruct (H)
    748 | #a #e %{a} /2 by conj/
    749 ] qed.
     698*)
     699lemma bind_option_inversion_star:
     700  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
     701  (∀x.f = Some … x → g x = Some … y → P) →
     702  (! x ← f ; g x = Some … y) → P.
     703#A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
     704
     705interpretation "option bind inversion" 'bind_inversion =
     706  (bind_option_inversion_star ???????).
    750707
    751708lemma sigma_pblock_eq_lemma :
     
    758715 #p #p' #graph_prog #sigma #pc #prf
    759716 whd in match sigma_pc; normalize nodelta
    760  @opt_safe_elim #x #x_spec
    761  whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
    762  normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
    763  #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
     717 @opt_safe_elim #x @'bind_inversion * #i #fn #_
     718 @'bind_inversion #n #_ whd in ⊢ (??%?→?);
     719 #EQ destruct %
    764720qed.
    765721
     
    780736*)
    781737
     738(*
    782739lemma funct_of_block_transf :
    783740∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
     
    887844#A #B #progr #transf #bl #f #prf
    888845whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
    889 #H
    890 elim (bind_opt_inversion ??? ?? H) -H #x
    891 * #x_spec
     846@'bind_inversion #x #x_spec
    892847@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
    893848#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
     
    899854>(description_of_function_transf) [2: @x_prf ]
    900855>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
    901 
    902 
    903 lemma fetch_function_sigma_commute :
    904  ∀p,p',graph_prog.
    905  let lin_prog ≝ linearise p graph_prog in
    906  ∀sigma,pc_st,f.
    907   ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
    908  fetch_function … (globalenv_noinit … graph_prog) pc_st =
    909   return f
    910 → fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
    911   return sigma_function_name … f.
    912  #p #p' #graph_prog #sigma #st #f #prf
     856*)
     857
     858axiom symbol_for_block_transf :
     859 ∀A,B,V,init.∀prog_in : program A V.
     860 ∀trans : ∀vars.A vars → B vars.
     861 let prog_out ≝ transform_program … prog_in trans in
     862 ∀bl, i.
     863 symbol_for_block … (globalenv … init prog_in) bl = Some ? i →
     864 symbol_for_block … (globalenv … init prog_out) bl = Some ? i.
     865
     866lemma fetch_function_transf :
     867 ∀A,B,V,init.∀prog_in : program A V.
     868 ∀trans : ∀vars.A vars → B vars.
     869 let prog_out ≝ transform_program … prog_in trans in
     870 ∀bl,i,f.
     871 fetch_function … (globalenv … init prog_in) bl =
     872  return 〈i, f〉
     873→ fetch_function … (globalenv … init prog_out) bl =
     874  return 〈i, trans … f〉.
     875#A #B #V #init #prog_in #trans #bl #i #f
    913876 whd in match fetch_function; normalize nodelta
    914  >(sigma_pblock_eq_lemma … prf) #H
    915  lapply (opt_eq_from_res ???? H) -H #H
    916  >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
    917  //
     877 #H lapply (opt_eq_from_res ???? H) -H
     878 @'bind_inversion #id #eq_symbol_for_block
     879 @'bind_inversion #fd #eq_find_funct
     880 whd in ⊢ (??%?→?); #EQ destruct(EQ)
     881 >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind
     882 >(find_funct_ptr_transf A B …  eq_find_funct) >m_return_bind %
     883qed.
     884
     885lemma bind_inversion_star : ∀X,Y.∀P : Prop.
     886∀m : res X.∀f : X → res Y.∀v : Y.
     887(∀x. m = return x → f x = return v → P) →
     888! x ← m ; f x = return v → P.
     889#X #Y #P #m #f #v #H #G
     890elim (bind_inversion ????? G) #x * @H qed.
     891
     892interpretation "res bind inversion" 'bind_inversion =
     893  (bind_inversion_star ???????).
     894
     895lemma fetch_internal_function_transf :
     896 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
     897 ∀trans : ∀vars.A vars → B vars.
     898 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
     899 ∀bl,i,f.
     900 fetch_internal_function … (globalenv_noinit … prog_in) bl =
     901  return 〈i, f〉
     902→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
     903  return 〈i, trans … f〉.
     904#A #B #prog #trans #bl #i #f
     905 whd in match fetch_internal_function; normalize nodelta
     906 @'bind_inversion * #id * #fd normalize nodelta #EQfetch
     907 whd in ⊢ (??%%→?); #EQ destruct(EQ)
     908 >(fetch_function_transf … EQfetch) %
    918909qed.
    919910 
     
    978969qed. *)
    979970
    980 lemma opt_Exists_elim:
    981  ∀A:Type[0].∀P:A → Prop.
    982   ∀o:option A.
    983    opt_Exists A P o →
    984     ∃v:A. o = Some … v ∧ P v.
    985  #A #P * normalize /3/ *
    986 qed.
    987 
    988 
    989971lemma stmt_at_sigma_commute:
    990  ∀p,graph_prog,graph_fun,lbl,pt.
    991  let lin_prog ≝ linearise ? graph_prog in
    992  let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
    993  ∀sigma.good_sigma p graph_prog sigma →
    994  sigma graph_fun lbl = return pt →
     972 ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma.
     973 good_local_sigma p globals graph_code entry lin_code sigma →
     974 sigma lbl = return pt →
    995975 ∀stmt.
    996    stmt_at …
    997     (joint_if_code ?? (if_of_function ?? graph_fun)) 
     976   stmt_at … graph_code
    998977    lbl = return stmt →
    999    stmt_at ??
    1000     (joint_if_code ?? (if_of_function ?? lin_fun))
    1001     pt = return (graph_to_lin_statement … stmt). 
    1002  #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
    1003 cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
    1004 #sigma_entry_is_zero #lin_stmt_spec
    1005 lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
    1006 #EQlookup_stmt1 #H
    1007 elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt
    1008 * #EQnth_opt_graph_stmt normalize nodelta
    1009 * #optEQlbl_optlbl_graph_stmt #next_spec
    1010 whd in match (stmt_at ????) in ⊢ (% → ?);
    1011 normalize nodelta
    1012 >EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
    1013 whd in match (stmt_at ????); > EQnth_opt_graph_stmt
    1014 normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
    1015 qed.
     978 stmt_at ?? lin_code
     979  pt = return graph_to_lin_statement … stmt ∧
     980  All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧
     981 match stmt with
     982 [ final stmt ⇒ True
     983 | sequential stmt nxt ⇒
     984   (sigma nxt = Some ? (S pt) ∨
     985    (stmt_at ?? lin_code
     986     (S pt) = return final (mk_lin_params p) … (GOTO … nxt)))
     987 ]. 
     988 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
     989 * #_ #lin_stmt_spec #prf
     990elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 *** #EQstmt_at
     991#All_succs_in #next_spec
     992#EQstmt_at_graph_stmt
     993#stmt >EQstmt_at
     994whd in ⊢ (??%%→?); #EQ destruct(EQ)
     995% [ % assumption ]
     996cases stmt in next_spec; -stmt normalize nodelta [2: // ]
     997#stmt #nxt
     998whd in match opt_All;
     999whd in match stmt_implicit_label;
     1000normalize nodelta //
     1001qed.
     1002 
    10161003(*
    10171004
     
    10361023 <sigma_pc_commute >lin_lookup_ok // *)
    10371024
    1038 lemma fetch_statement_sigma_commute:
    1039   ∀p,p',graph_prog,pc,fn,stmt.
     1025definition good_sigma :
     1026  ∀p.∀graph_prog : joint_program (mk_graph_params p).
     1027  (joint_closed_internal_function ? (prog_var_names … graph_prog) →
     1028    label → option ℕ) → Prop ≝
     1029  λp,graph_prog,sigma.
     1030  ∀fn : joint_closed_internal_function (mk_graph_params p) ?.
     1031  good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn)
     1032    (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn).
     1033
     1034lemma pc_of_label_sigma_commute :
     1035  ∀p,p',graph_prog,pc,lbl,i,fn.
    10401036  let lin_prog ≝ linearise ? graph_prog in
    10411037  ∀sigma.good_sigma p graph_prog sigma →
    10421038  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    1043   fetch_statement ? (make_sem_graph_params p p') …
    1044     (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
    1045   fetch_statement ? (make_sem_lin_params p p') …
     1039  fetch_internal_function …
     1040    (globalenv_noinit … graph_prog) (pc_block pc) = return 〈i, fn〉 →
     1041  let pc' ≝ pc_of_point (make_sem_graph_params p p') … (pc_block pc) lbl in
     1042  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
     1043  ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
     1044    (pc_block (sigma_pc … pc prf)) lbl =
     1045        return sigma_pc p p' graph_prog sigma pc' prf'.
     1046#p #p' #graph_prog #pc #lbl #i #fn
     1047#sigma #good cases (good fn) -good * #_ #all_labels_in
     1048#good #prf #fetchfn >lin_code_has_label #lbl_in
     1049whd in match pc_of_label; normalize nodelta
     1050>sigma_pblock_eq_lemma
     1051> (fetch_internal_function_transf … fetchfn) >m_return_bind
     1052inversion (point_of_label ????)
     1053[ (*
     1054  change with (If ? then with prf do ? else ? = ? → ?)
     1055  @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ]
     1056  *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS)
     1057| #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind
     1058  %
     1059  [ @hide_prf whd %
     1060  | whd in match sigma_pc; normalize nodelta
     1061    @opt_safe_elim #pc'
     1062  ]
     1063  whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
     1064  >point_of_pc_of_point
     1065  >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) %
     1066]
     1067qed.
     1068
     1069lemma graph_pc_of_label :
     1070  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
     1071  ∀globals,ge,bl,i_fn,lbl.
     1072  fetch_internal_function ? ge bl = return i_fn →
     1073  pc_of_label pars globals ge bl lbl =
     1074    OK ? (pc_of_point pars bl lbl).
     1075#p #p' #globals #ge #bl #fn #lbl #fetchfn
     1076whd in match pc_of_label; normalize nodelta
     1077>fetchfn %
     1078qed.
     1079
     1080lemma graph_succ_pc :
     1081  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
     1082  ∀pc,lbl.
     1083  succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl.
     1084normalize //
     1085qed.
     1086
     1087lemma fetch_statement_sigma_commute:
     1088  ∀p,p',graph_prog,pc,f,fn,stmt.
     1089  let lin_prog ≝ linearise ? graph_prog in
     1090  ∀sigma.good_sigma p graph_prog sigma →
     1091  ∀prf : well_formed_pc p p' graph_prog sigma pc.
     1092  fetch_statement (make_sem_graph_params p p') …
     1093    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
     1094  fetch_statement (make_sem_lin_params p p') …
    10461095    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    1047     return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
    1048  #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf
    1049  whd in match fetch_statement; normalize nodelta #H
    1050  cases (bind_inversion ????? H) #id * -H #fetchfn
    1051  >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
    1052  #H cases (bind_inversion ????? H) #fstmt * -H #H
    1053  lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
    1054  >(stmt_at_sigma_commute … good … H) [%]
    1055  whd in match sigma_pc; normalize nodelta
    1056  @opt_safe_elim #pc' #H
    1057  cases (bind_opt_inversion ????? H)
    1058  #i * #EQ1 -H #H
    1059  cases (bind_opt_inversion ????? H)
    1060  #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
    1061  whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
    1062  lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
    1063 qed.
     1096  return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧
     1097  All ? (λlbl.well_formed_pc p p' graph_prog sigma
     1098      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
     1099    (stmt_explicit_labels … stmt) ∧
     1100  match stmt with
     1101  [ sequential stmt nxt ⇒
     1102    ∃prf'.
     1103    let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
     1104    let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
     1105    (nxt_pc = sigma_nxt ∨
     1106     fetch_statement (make_sem_lin_params p p') …
     1107      (globalenv_noinit … lin_prog) nxt_pc =
     1108      return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
     1109  | final stmt ⇒ True
     1110  ].
     1111#p #p' #graph_prog #pc #f #fn #stmt #sigma #good
     1112elim (good fn) * #_ #all_labels_in #good_local #wfprf
     1113#H
     1114elim (fetch_statement_inv … H)
     1115#fetchfn #graph_stmt
     1116whd in match fetch_statement; normalize nodelta
     1117>sigma_pblock_eq_lemma
     1118>(fetch_internal_function_transf … fetchfn) >m_return_bind
     1119whd in match sigma_pc; normalize nodelta @opt_safe_elim
     1120#lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta
     1121>fetchfn in ⊢ (%→?); >m_return_bind
     1122inversion (sigma ??)
     1123[ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     1124#lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1125cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) *
     1126#H1 #H2 #H3 % [ % ]
     1127[ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
     1128  >H1 %
     1129| @(All_mp … (All_append_r … H2)) #lbl #prf'
     1130 whd whd in match sigma_pc_opt; normalize nodelta
     1131 >fetchfn >m_return_bind >point_of_pc_of_point
     1132 >(opt_to_opt_safe … prf') % normalize
     1133 #ABS destruct(ABS)
     1134| cases stmt in H2 H3; normalize nodelta [2: // ]
     1135  -stmt #stmt #nxt * #next_in #_ #nxt_spec
     1136  % 
     1137  [ @hide_prf whd %
     1138  | @opt_safe_elim #pc'
     1139  ]
     1140  >graph_succ_pc whd in ⊢ (??%?→?);
     1141  >fetchfn normalize nodelta >point_of_pc_of_point
     1142  >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1143  cases nxt_spec
     1144  [ #EQsigma_nxt %1
     1145    whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta
     1146    >point_of_offset_of_point lapply next_in >EQsigma_nxt #N %
     1147  | #EQstmt_at_nxt %2
     1148    whd in match (succ_pc ???);
     1149    >(fetch_internal_function_transf … fetchfn) >m_return_bind
     1150    whd in match point_of_pc;
     1151    normalize nodelta >point_of_offset_of_point >point_of_offset_of_point
     1152    whd in match (point_of_succ ???);
     1153    >EQstmt_at_nxt %
     1154  ]
     1155]
     1156qed. 
    10641157
    10651158lemma point_of_pc_sigma_commute :
    10661159 ∀p,p',graph_prog.
    10671160 let lin_prog ≝ linearise p graph_prog in
    1068  ∀sigma,pc,fn,n.
     1161 ∀sigma,pc,f,fn,n.
    10691162  ∀prf : well_formed_pc p p' graph_prog sigma pc.
    1070  int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn
    1071  sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n →
    1072  point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
    1073 #p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma
     1163 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉
     1164 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
     1165 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
     1166#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
    10741167whd in match sigma_pc; normalize nodelta
    10751168@opt_safe_elim #pc' whd in match sigma_pc_opt;
    10761169normalize nodelta >EQfetch >m_return_bind >EQsigma
    1077 >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
    1078 change with (point_of_offset ??? = ?) @point_of_offset_of_point
     1170whd in ⊢ (??%?→?); #EQ destruct(EQ)
     1171@point_of_offset_of_point
    10791172qed.
    10801173
     
    10821175 ∀p,p',graph_prog.
    10831176 let lin_prog ≝ linearise p graph_prog in
    1084  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    1085  let stack_sizes' ≝
    1086   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    1087     ? graph_prog stack_sizes in
     1177 ∀stack_sizes.
    10881178 ∀sigma,gss.
    10891179 good_sigma p graph_prog sigma →
    10901180   status_rel
    1091     (graph_abstract_status p p' graph_prog stack_sizes')
     1181    (graph_abstract_status p p' graph_prog stack_sizes)
    10921182    (lin_abstract_status p p' lin_prog stack_sizes)
    10931183 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
     
    11141204
    11151205lemma IO_bind_inversion:
    1116   ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    1117   (! x ← f ; g x = return y) →
    1118   ∃x. (f = return x) ∧ (g x = return y).
    1119 #O #I #A #B #f #g #y cases f normalize
    1120 [ #o #f #H destruct
    1121 | #a #e %{a} /2 by conj/
    1122 | #m #H destruct (H)
     1206  ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
     1207  (∀x.f = return x → g x = return y → P) →
     1208  (! x ← f ; g x = return y) → P.
     1209#O #I #A #B #P #f #g #y cases f normalize
     1210[ #o #f #_ #H destruct
     1211| #a #G #H @(G ? (refl …) H)
     1212| #e #_ #H destruct
    11231213] qed.
     1214
     1215interpretation "IO bind inversion" 'bind_inversion =
     1216  (IO_bind_inversion ?????????).
    11241217
    11251218lemma err_eq_from_io : ∀O,I,X,m,v.
     
    11441237cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
    11451238#EQ >EQ //
     1239qed.
     1240
     1241(* this should make things easier for ops using memory (where pc cant happen) *)
     1242definition bv_no_pc : beval → Prop ≝
     1243λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
     1244
     1245lemma bv_pc_other :
     1246  ∀P : beval → Prop.
     1247  (∀pc,p.P (BVpc pc p)) →
     1248  (∀bv.bv_no_pc bv → P bv) →
     1249  ∀bv.P bv.
     1250#P #H1 #H2 * /2/ qed.
     1251
     1252lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
     1253  bv_no_pc bv →
     1254  sigma_beval p p' graph_prog sigma bv prf = bv.
     1255#p #p' #graph_prog #sigma *
     1256[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
     1257#prf * whd in match sigma_beval; normalize nodelta
     1258@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
    11461259qed.
    11471260
     
    12541367 ∀p,p',graph_prog.
    12551368 let lin_prog ≝ linearise p graph_prog in
    1256  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    1257  let stack_sizes' ≝
    1258   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    1259     ? graph_prog stack_sizes in
    1260  ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
    1261  ∀fn,st,stmt,st'.
     1369 ∀stack_sizes.
     1370 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     1371 ∀f,fn,st,stmt,st'.
    12621372 ∀prf : well_formed_state … gss st.
    1263   eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
    1264    fn st stmt = return st' →
     1373  eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1374   f fn stmt st = return st' →
    12651375  ∃prf'.
    1266   eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
    1267     (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
     1376  eval_seq_no_pc (ev_genv … (lin_prog_params … lin_prog stack_sizes))
     1377    f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) =
    12681378  return sigma_state … gss st' prf'.
    12691379  #p #p' #graph_prog #stack_sizes #sigma #gss
     
    13931503          inversion(sigma_beval_opt ???? y)
    13941504          [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
     1505         xxxxxxxxxxxxxxxxxx
     1506       
     1507 qed.       
     1508
     1509lemma eval_statement_no_pc_sigma_commute :
     1510 ∀p,p',graph_prog.
     1511 let lin_prog ≝ linearise p graph_prog in
     1512 ∀stack_sizes.
     1513 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     1514 ∀f,fn,st,stmt,st'.
     1515 ∀prf : well_formed_state … gss st.
     1516  eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1517   f fn stmt st = return st' →
     1518  ∃prf'.
     1519  eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
     1520    f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)
     1521       (sigma_state … gss st prf) =
     1522  return sigma_state … gss st' prf'.
     1523  #p #p' #graph_prog #stack_sizes #sigma #gss
     1524  #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]]
     1525  #st' #prf
     1526  whd in match eval_statement_no_pc; normalize nodelta
     1527  [ @eval_seq_no_pc_sigma_commute
     1528  |2,3,4: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
     1529  | (* tailcall, follow proof of CALL in previous lemma *)
     1530    cases daemon
     1531  ]
     1532qed.
     1533
     1534=======
    13951535           whd in match sigma_is_opt; >H normalize nodelta >ABS
    13961536           whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
     
    15811721  | (*C_OP1*)
    15821722   
     1723>>>>>>> .r2528
    15831724inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    15841725    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
     
    15881729 ∀p,p',graph_prog.
    15891730  let lin_prog ≝ linearise ? graph_prog in
    1590  ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    1591  let graph_stack_sizes ≝
    1592   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    1593     ? graph_prog lin_stack_sizes in
    1594  (∀sigma.good_sigma_state p p' graph_prog sigma) →
     1731 ∀stack_sizes.
     1732 (∀sigma.good_state_sigma p p' graph_prog sigma) →
    15951733   ex_Type1 … (λR.
    15961734   status_simulation
    1597     (graph_abstract_status p p' graph_prog graph_stack_sizes)
    1598     (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
     1735    (graph_abstract_status p p' graph_prog stack_sizes)
     1736    (lin_abstract_status p p' lin_prog stack_sizes) R).
    15991737 #p #p' #graph_prog
    1600  cases (linearise_spec … graph_prog) #sigma #good
    1601  #lin_stack_sizes
     1738 letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog)
     1739 cut (∀fn.good_local_sigma … (sigma fn))
     1740  [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:]
     1741 #good
     1742 #stack_sizes
    16021743 #gss lapply (gss sigma) -gss #gss
    1603  %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}
     1744 %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)}
    16041745whd in match graph_abstract_status;
    16051746whd in match lin_abstract_status;
     
    16161757  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
    16171758whd in match eval_state in ⊢ (%→?); normalize nodelta
    1618 change with (Σi.is_internal_function_of_program ? graph_prog i) in
    1619 match (Sig ??) in ⊢ (%→?);
    1620 letin globals ≝ (prog_var_names ?? graph_prog)
    1621 change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
    1622   match (fetch_statement ?????) in ⊢ (%→?);
    1623 #ex
    1624 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
    1625 #EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
    1626 #EQfetch
    1627 cases (bind_inversion ????? EQfetch)
    1628 #f_id * #H lapply (opt_eq_from_res ???? H) -H
    1629 #EQfunc_of_block
    1630 #H elim (bind_inversion ????? H) -H #stmt' *
    1631 #H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
    1632 whd in ⊢ (??%%→?); #EQ destruct(EQ)
    1633 #EQeval
    1634 cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
    1635 letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
    1636 #entry_0
    1637 #good_local
    1638 * * #wf_pc #wf_state #EQst2
     1759@'bind_inversion
     1760** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt
     1761cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_
     1762@'bind_inversion
     1763#st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance
     1764* #wf_prf #st2_EQ
     1765
     1766cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt)
     1767* #EQfetch_stmt' #all_labels_in
     1768
     1769letin lin_prog ≝ (linearise … graph_prog)
     1770lapply (refl … (eval_state …  (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2))
     1771whd in match eval_state in ⊢ (???%→?);
     1772>st2_EQ in ⊢ (???%→?); normalize nodelta
     1773>EQfetch_stmt' in ⊢ (%→?); >m_return_bind in ⊢ (???%→?);
     1774cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?;
     1775#wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?);
     1776
     1777whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1778>EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1779normalize nodelta
     1780
     1781cases stmt in ex ex_advance; -stmt whd in match graph_to_lin_statement;
     1782normalize nodelta
     1783[ whd in match joint_classify_step; @cond_call_other
     1784  [ (* COND *) #a #lbltrue #nxt
     1785    #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta
     1786    #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other
     1787    [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
     1788    #bv #bv_no_pc #EQretrieve
     1789    cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve)
     1790    #ignore >(sigma_bv_no_pc … bv_no_pc)
     1791    change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?)
     1792    #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?);
     1793    #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv
     1794    >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta
     1795    [ whd in match goto; normalize nodelta
     1796      >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?);
     1797      #EQ destruct(EQ) #ex_advance #ex_advance'
     1798      % [2: %{(tal_base_not_return …)} [3: @ex_advance'
     1799  | (* CALL *) #f #args #dest #nxt
     1800  | (* other *) #stmt #no_call #nxt
     1801  ] normalize nodelta
     1802  [ #ex
     1803    #ex_advance #ex_advance'
     1804  | whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1805    #H @('bind_inversion H) -H #called_block
     1806    #H lapply (err_eq_from_io ????? H) -H #EQcalled_block
     1807    #H @('bind_inversion H) -H * #called * #called_fn
     1808    #H lapply (err_eq_from_io ????? H) -H #EQcalled
     1809    normalize nodelta
     1810    [ #H lapply (err_eq_from_io ????? H) -H ]
     1811    #H @('bind_inversion H) -H
     1812     | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ]
     1813    #ex_advance #ex_advance'
     1814    whd in match joint_classify_seq; normalize nodelta
     1815    >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1816   
     1817    cut (∀p,p',graph_prog,sigma,gss,st,f,bl.
     1818        ∀prf : well_formed_state p p' graph_prog sigma gss st.
     1819        block_of_call (make_sem_graph_params p p') ?
     1820          (globalenv_noinit ? graph_prog) st f = return bl →
     1821        block_of_call (make_sem_lin_params p p') ?
     1822          (globalenv_noinit ? (linearise … graph_prog))
     1823          (sigma_state … st prf) f = return bl)
     1824      [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute
     1825      whd in match eval_seq_advance; normalize nodelta
     1826      >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?);
     1827      >m_return_bind in ⊢ (???%→?);
     1828      >(fetch_function_transf … EQcalled :
     1829        fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?);
     1830      >m_return_bind in ⊢ (???%→?);
     1831      whd in match (transf_fundef); normalize nodelta
     1832       
     1833       
     1834      #block_of_call_sigma_commute
     1835    @match_int_fun #called_descr #EQcalled_descr
     1836    [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ]
     1837    #ex_advance
     1838    cut
     1839      (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ.
     1840      ∀trans : ∀vars.A vars → B vars.
     1841      let prog_out : program (λvars.fundef (B vars)) ℕ ≝
     1842        transform_program ??? prog (λvars.transf_fundef … (trans vars)) in
     1843      ∀i.is_function … (globalenv_noinit … prog) i →
     1844       is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ]
     1845    #f_propagate
     1846    letin sigma_function ≝ (λA,B,prog,trans.
     1847      λf : Σi.is_function ? (globalenv_noinit ? prog) i.
     1848      «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *)
     1849    cut (∀p,p',graph_prog.
     1850      let lin_prog ≝ linearise ? graph_prog in
     1851      ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
     1852      ∀f,st,fn.
     1853      ∀prf : well_formed_state … gss st.
     1854      function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog)
     1855        st f = return fn →
     1856      function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
     1857        (sigma_state … gss st prf) f = return sigma_function … fn)
     1858        [1,3: (* TODO lemma *) cases daemon ]
     1859    #function_of_call_sigma_commute
     1860    whd in match joint_classify_step; whd in match joint_classify_seq;
     1861    normalize nodelta #next_spec
     1862    >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?);
     1863    >m_return_bind in ⊢ (%→?);
     1864    @match_int_fun
     1865    [2,3: #EQdescr' lapply EQdescr'
     1866      >description_of_function_transf in EQdescr';
     1867     
     1868   
     1869    whd in match sigma_beval; normalize nodelta
     1870    cases bv
     1871    [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ]
     1872    whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?);
     1873    [7: #ignore #_
     1874    #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve
     1875    whd in match (bool_of_beval ?) in ⊢ (% → ?);
     1876    3: >no_call_advance [2: @no_call]
     1877 
     1878
     1879
    16391880generalize in match wf_pc in ⊢ ?;
    16401881whd in ⊢ (%→?);
     
    16561897*
    16571898#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
    1658 letin lin_prog ≝ (linearise … graph_prog)
    1659 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
    16601899destruct(EQst2)
    16611900whd in match eval_state in ⊢ (???%→?); normalize nodelta
    1662 letin st2 ≝ (sigma_state_pc ????? st1 ?)
    1663 >(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
    1664 >m_return_bind in ⊢ (%→?);
    1665 #ex'
    16661901(* resolve classifier *)
    1667 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    1668 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
    1669 normalize nodelta
    1670 cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
    16711902[ *
    16721903  [ #stmt #nxt
  • src/joint/semantics.ma

    r2491 r2529  
    1616{ ge :> genv_t (fundef (F globals))
    1717; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
    18 ; stack_sizes : (Σi.is_internal_function ? ge i) →
     18; stack_sizes : ident → option
    1919}.
    20 
    21 definition stack_sizes_lift :
    22 ∀pars_in, pars_out : params.
    23 ∀trans : ∀globals.joint_closed_internal_function pars_in globals →
    24                   joint_closed_internal_function pars_out globals.
    25 ∀prog_in : program (joint_function pars_in) ℕ.
    26 let prog_out ≝
    27   transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
    28 ((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
    29 ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
    30 λpars_in,pars_out,prog_in,trans,stack_sizes.
    31 λi.stack_sizes «i, if_propagate … (pi2 … i)».
    3220
    3321definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
     
    122110*)
    123111
    124 (* bevals hold a function pointer (BVptr) *)
    125 definition funct_of_bevals : ∀F,ge.
    126   beval → beval → option (Σi.is_function F ge i) ≝
    127 λF,ge,dpl,dph.
    128 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
    129 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *)
    130    match ptype ptr with [ Code ⇒ true | _ ⇒ false] then (* ← already checked in funct_of_block? *)
    131    funct_of_block … (pblock ptr)
    132 else None ?.
    133 
    134112axiom ProgramCounterOutOfCode : String.
    135113axiom PointNotFound : String.
     
    144122definition fetch_function:
    145123 ∀F.
     124 ∀ge : genv_t F.
     125  (Σb.block_region b = Code) →
     126  res (ident×F) ≝
     127 λF,ge,bl.
     128 opt_to_res … [MSG BadFunction]
     129  (! id ← symbol_for_block … ge bl ;
     130   ! fd ← find_funct_ptr … ge bl ;
     131   return 〈id, fd〉).
     132
     133definition fetch_internal_function :
     134 ∀F.
    146135 ∀ge : genv_t (fundef F).
    147   program_counter →
    148   res (Σi.is_internal_function … ge i) ≝
    149  λpars,ge,p.
    150  opt_to_res … [MSG BadFunction; MSG BadPointer]
    151     (int_funct_of_block … ge (pc_block p)).
     136  (Σb.block_region b = Code) →
     137  res (ident×F) ≝
     138 λF,ge,bl.
     139 ! 〈id, fd〉 ← fetch_function … ge bl ;
     140 match fd with
     141 [ Internal ifd ⇒ return 〈id, ifd〉
     142 | _ ⇒ Error … [MSG BadFunction]
     143 ].
    152144
    153145record sem_unserialized_params
     
    171163  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    172164
     165  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    173166  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
    174   (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    175167  ; save_frame: call_dest uns_pars → state_pc st_pars → res (state st_pars)
    176168   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
     
    187179  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
    188180  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    189     (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
     181    ident → F globals (* current *) → state st_pars → res (state st_pars)
    190182  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    191     (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state_pc st_pars)
     183    ident → F globals (* current *) → state st_pars → res (state_pc st_pars)
    192184  }.
    193185
     
    241233 return 〈bv, set_istack … is st〉.
    242234
    243 definition save_ra : ∀p. state p → program_counter → res (state p) ≝
     235definition push_ra : ∀p. state p → program_counter → res (state p) ≝
    244236 λp,st,l.
    245237  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
     
    247239  push … st' addrh.
    248240
    249 definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
     241definition pop_ra : ∀p.state p → res (program_counter × (state p)) ≝
    250242 λp,st.
    251243  ! 〈addrh, st'〉 ← pop … st;
     
    255247
    256248(* parameters that are defined by serialization *)
    257 record more_sem_params (pp : params) : Type[1] ≝
    258   { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
    259   ; offset_of_point : code_point pp → Pos
    260   ; point_of_offset : Pos → code_point pp
     249record sem_params : Type[1] ≝
     250  { spp :> params
     251  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
     252  ; offset_of_point : code_point spp → Pos
     253  ; point_of_offset : Pos → code_point spp
    261254  ; point_of_offset_of_point :
    262255    ∀pt.point_of_offset (offset_of_point pt) = pt
     
    278271ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
    279272
    280 definition pc_of_point : ∀p.more_sem_params p
    281   program_counter → code_point p → program_counter ≝
    282   λp,msp,ptr,pt.
    283   mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).
     273definition pc_of_point : ∀p:sem_params.(Σb.block_region b = Code)
     274  code_point p → program_counter ≝
     275  λp,bl,pt.
     276  mk_program_counter bl (offset_of_point p pt).
    284277
    285278definition point_of_pc :
    286   ∀p.more_sem_params p → program_counter → code_point p ≝
    287   λp,msp,ptr.point_of_offset p msp (pc_offset ptr).
    288 
    289 lemma point_of_pointer_of_point :
    290   ∀p,msp.∀ptr,pt.
    291   point_of_pc ? msp (pc_of_point p msp ptr pt) = pt.
    292 #p #msp #ptr #pt normalize // qed.
    293 
    294 lemma pointer_of_point_block :
    295   ∀p,msp,ptr,pt.
    296   pc_block (pc_of_point p msp ptr pt) = pc_block ptr.
    297 #p #msp #ptr #pt % qed. (* can probably do without *)
    298 
    299 lemma pointer_of_point_uses_block :
    300   ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 →
    301     pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt.
    302 #p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed.
    303 
    304 lemma pointer_of_point_of_pointer :
    305   ∀p,msp.∀ptr1,ptr2.
    306     pc_block ptr1 = pc_block ptr2 →
    307     pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2.
    308 #p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed.
    309 
    310 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
     279  ∀p:sem_params.program_counter → code_point p ≝
     280  λp,ptr.point_of_offset p (pc_offset ptr).
     281
     282lemma point_of_pc_of_point :
     283  ∀p,bl,pt.
     284  point_of_pc p (pc_of_point p bl pt) = pt.
     285#p #bl #pt normalize // qed.
     286
     287lemma pc_of_point_of_pc :
     288  ∀p,ptr.
     289    pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr.
     290#p * #bl #off normalize >offset_of_point_of_offset % qed.
     291
     292definition fetch_statement: ∀p : sem_params.∀globals.
    311293  ∀ge : genv_t (joint_function p globals). program_counter →
    312   res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
    313   λp,msp,globals,ge,ptr.
    314   ! f ← fetch_function … ge ptr ;
    315   let fn ≝ if_of_function … f in
    316   let pt ≝ point_of_pc ? msp ptr in
     294  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
     295  λp,globals,ge,ptr.
     296  ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ;
     297  let pt ≝ point_of_pc p ptr in
    317298  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
    318   return 〈f, stmt〉.
    319 
    320 definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    321   genv_t (joint_function p globals) → program_counter → label → res program_counter ≝
    322   λp,msp,globals,ge,ptr,lbl.
    323   ! f ← fetch_function … ge ptr ;
    324   let fn ≝ if_of_function …  ge f in
     299  return 〈id, fn, stmt〉.
     300
     301definition pc_of_label : ∀p : sem_params.∀globals.
     302  genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝
     303  λp,globals,ge,bl,lbl.
     304  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
    325305  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    326306            (point_of_label … (joint_if_code … fn) lbl) ;
    327   return pc_of_point p msp ptr pt.
    328 
    329 definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     307  return mk_program_counter bl (offset_of_point p pt).
     308
     309definition succ_pc : ∀p : sem_params.
    330310  program_counter → succ p → program_counter ≝
    331   λp,msp,ptr,nxt.
    332   let curr ≝ point_of_pc p msp ptr in
    333   pc_of_point p msp ptr (point_of_succ p curr nxt).
    334 
     311  λp,ptr,nxt.
     312  let curr ≝ point_of_pc p ptr in
     313  pc_of_point p (pc_block ptr) (point_of_succ p curr nxt).
     314
     315(*
    335316record sem_params : Type[1] ≝
    336317  { spp :> params
    337318  ; more_sem_pars :> more_sem_params spp
    338319  }.
    339 
     320*)
    340321(* definition msu_pars_of_s_pars :
    341322∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
     
    371352
    372353definition goto: ∀p : sem_params.∀globals.
    373   genv_t (joint_function p globals) → label → state p → program_counter → res (state_pc p) ≝
    374  λp,globals,ge,l,st,b.
    375   ! newpc ← pc_of_label ? p … ge b l ;
    376   return mk_state_pc ? st newpc.
     354  genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝
     355 λp,globals,ge,l,st.
     356  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
     357  return mk_state_pc st newpc.
    377358
    378359(*
     
    383364definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝
    384365 λp,l,st.
    385  let newpc ≝ succ_pc ? p … (pc … st) l in
     366 let newpc ≝ succ_pc … (pc … st) l in
    386367 mk_state_pc … st newpc.
    387368
    388 
    389 definition function_of_call ≝ λp:sem_params.λglobals.
     369definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
     370λbl.match block_region bl
     371  return λx.block_region bl = x → option (Σb.block_region b = Code) with
     372  [ Code ⇒ λprf.Some ? «bl, prf»
     373  | XData ⇒ λ_.None ?
     374  ] (refl …).
     375
     376definition block_of_call ≝ λp:sem_params.λglobals.
    390377  λge: genv_t (joint_function p globals).λst : state p.λf.
    391   match f with
    392   [ inl id ⇒
    393     opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
    394   | inr addr ⇒
    395     ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    396     ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    397     opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
    398   ].
     378  ! bl ← match f with
     379    [ inl id ⇒ opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id)
     380    | inr addr ⇒
     381      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
     382      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
     383      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
     384      if eq_bv … (bv_zero …) (offv (poff ptr)) then
     385        return (pblock … ptr)
     386      else
     387        Error … [MSG BadFunction; MSG BadPointer]
     388    ] ;
     389  opt_to_res … [MSG BadFunction; MSG BadPointer] (code_block_of_block bl).
    399390
    400391(* Paolo: why external calls do not need args?? *)
    401392definition eval_external_call ≝
    402 λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
    403       ! params ← fetch_external_args … p' fn st args : IO ???;
     393λp : sem_params.λfn,args,dest,st.
     394      ! params ← fetch_external_args … p fn st args : IO ???;
    404395      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    405396      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     
    408399         fixed once we fully implement external functions. *)
    409400      let vs ≝ [mk_val ? evres] in
    410       set_result … p' vs dest st.
    411 
    412 definition eval_internal_call_pc ≝
    413 λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi.
    414 let fn ≝ if_of_function … ge i in
    415 let l' ≝ joint_if_entry ?? fn in
    416 mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l').
    417 [ @block_of_funct_ident_is_code
    418 | cases i /2 by internal_function_is_function/
    419 ]
    420 qed.
     401      set_result … p vs dest st.
     402
     403axiom MissingStackSize : String.
    421404
    422405definition eval_internal_call_no_pc ≝
    423 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
    424 let fn ≝ if_of_function … ge i in
    425 let stack_size ≝ stack_sizes … ge i in
    426 ! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
     406λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
     407! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
     408! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    427409return allocate_locals … p (joint_if_locals … fn) st.
    428410
     411axiom NoSuccessor : String.
     412definition next_of_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
     413  program_counter → res (succ p) ≝
     414λp,globals,ge,pc.
     415  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
     416  match stmt with
     417  [ sequential _ nxt ⇒ return nxt
     418  | _ ⇒ Error … [MSG NoSuccessor]
     419  ].
     420
    429421definition eval_seq_no_pc :
    430  ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
    431   state p → joint_seq p globals →
    432   IO io_out io_in (state p) ≝
    433  λp,globals,ge,curr_fn,st,seq.
    434  match seq return λx.IO ??? with
     422 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
     423 joint_closed_internal_function p globals →
     424  joint_seq p globals → state p →
     425  res (state p) ≝
     426 λp,globals,ge,curr_id,curr_fn,seq,st.
     427 match seq with
    435428  [ extension_seq c ⇒
    436     eval_ext_seq … ge c curr_fn st
     429    eval_ext_seq … ge c curr_id curr_fn st
    437430  | LOAD dst addrl addrh ⇒
    438431    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    481474  | MOVE dst_src ⇒
    482475    pair_reg_move … st dst_src
    483   | CALL f args dest ⇒
    484     ! fn ← function_of_call … ge st f : IO ???;
    485     match description_of_function … fn return λx.description_of_function … fn = x → ? with
    486     [ Internal fd ⇒ λprf.
    487       eval_internal_call_no_pc … ge «fn, ?» args st  (* only pc changes *)
    488     | External fd ⇒ λ_.eval_external_call … fd args dest st
    489     ] (refl …)
    490   | _ ⇒ return st
     476  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
    491477  ].
    492 [ @hide_prf
     478  @hide_prf
    493479  @find_symbol_in_globals
    494480  lapply prf
     
    497483  [@eq_identifier_elim #H * >H %1 % ]
    498484  #G %2 @IH @G
    499 | @(description_of_internal_function … prf)
    500 ]
    501485qed.
    502486
    503 definition eval_seq_pc :
     487definition eval_seq_call ≝
     488λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
     489λst : state_pc p.
     490! bl ← block_of_call … ge st f : IO ???;
     491! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
     492match fd with
     493[ Internal ifd ⇒
     494  ! st' ← save_frame … dest st ;
     495  ! st'' ← eval_internal_call_no_pc p globals ge i ifd args st' ;
     496  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     497  return mk_state_pc … st'' pc
     498| External efd ⇒
     499  ! st' ← eval_external_call … efd args dest st ;
     500  return mk_state_pc … st' (succ_pc p (pc … st) nxt)
     501].
     502
     503definition eval_seq_advance :
    504504 ∀p:sem_params.∀globals.∀ge:genv p globals.
    505   state_pc p → ? → joint_seq p globals
    506   res (state_pc p) ≝
    507   λp,globals,ge,st,nxt,s.
     505  joint_seq p globals → succ p → state_pc p
     506  IO io_out io_in (state_pc p) ≝
     507  λp,globals,ge,s,nxt,st.
    508508  match s with
    509509  [ CALL f args dest ⇒
    510     ! fn ← function_of_call … ge st f;
    511     match ? return λx.description_of_function … fn = x → ? with
    512     [ Internal _ ⇒ λprf.
    513       let pc ≝ eval_internal_call_pc … ge «fn, ?» in
    514       ! st' ← save_frame … dest st ;
    515       return mk_state_pc … st' pc
    516     | External _ ⇒ λ_.return next p nxt st
    517     ] (refl …)
    518   | _ ⇒ return next p nxt st
     510    eval_seq_call … ge f args dest nxt st
     511  | _ ⇒ return next … nxt st
    519512  ].
    520 @(description_of_internal_function … prf)
    521 qed.
    522 
    523 definition eval_statement :
     513
     514definition eval_statement_no_pc :
    524515 ∀p:sem_params.∀globals.∀ge:genv p globals.
    525  (Σi.is_internal_function … ge i) → state_pc p →
    526   ∀s:joint_statement p globals.
    527   IO io_out io_in (state_pc p) ≝
    528   λp,g,ge,curr_fn,st,s.
     516 ident → joint_closed_internal_function p globals (* current *) →
     517 joint_statement p globals → state p → res (state p) ≝
     518 λp,globals,ge,curr_id,curr_fn,s,st.
    529519  match s with
    530520  [ sequential s next ⇒
     521    match s with
     522    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st
     523    | COND a l ⇒ return st
     524    ]
     525  | final s ⇒ return st
     526  ].
     527
     528definition eval_return ≝
     529λp : sem_params.λglobals : list ident.λge : genv p globals.
     530λcurr_id.λcurr_fn : joint_closed_internal_function ??.
     531λst : state p.
     532! st' ← pop_frame … ge curr_id curr_fn st ;
     533! nxt ← next_of_pc … ge (pc … st') ;
     534return next … nxt st' (* now address pushed on stack are calling ones! *).
     535
     536definition eval_tailcall ≝
     537λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
     538λcurr_fn : joint_closed_internal_function ??.
     539λst : state_pc p.
     540! bl ← block_of_call … ge st f : IO ???;
     541! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
     542match fd with
     543[ Internal ifd ⇒
     544  ! st' ← eval_internal_call_no_pc p globals ge i ifd args st ;
     545  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     546  return mk_state_pc … st' pc
     547| External efd ⇒
     548  let curr_dest ≝ joint_if_result ?? curr_fn in
     549  ! st' ← eval_external_call … efd args curr_dest st ;
     550  eval_return … ge curr_f curr_fn st
     551].
     552
     553definition eval_statement_advance :
     554 ∀p:sem_params.∀globals.∀ge:genv p globals.
     555 ident → joint_closed_internal_function p globals →
     556  joint_statement p globals → state_pc p →
     557  IO io_out io_in (state_pc p) ≝
     558  λp,g,ge,curr_id,curr_fn,s,st.
     559  match s with
     560  [ sequential s nxt ⇒
    531561    match s return λ_.IO ??? with
    532562    [ step_seq s ⇒
    533       ! st' ← eval_seq_no_pc … ge curr_fn st s ;
    534       let st'' ≝ mk_state_pc … st' (pc … st) in
    535       eval_seq_pc ?? ge st'' next s
     563      eval_seq_advance … ge s nxt st
    536564    | COND a l ⇒
    537565      ! v ← acca_retrieve … st a ;
    538566      ! b ← bool_of_beval … v ;
    539       ! pc' ←
    540         if b then
    541           pc_of_label ? p … ge (pc … st) l
    542         else
    543           return succ_pc ? p (pc … st) next ;
    544       return mk_state_pc … st pc'
     567      if b then
     568        goto … ge l st
     569      else
     570        return next … nxt st
    545571    ]
    546572  | final s ⇒
    547573    match s with
    548     [ GOTO l ⇒
    549       ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
    550       return mk_state_pc … st pc'
    551     | RETURN ⇒ pop_frame … curr_fn st
     574    [ GOTO l ⇒ goto … ge l st
     575    | RETURN ⇒ eval_return … ge curr_id curr_fn st
    552576    | TAILCALL _ f args ⇒
    553       ! fn ← function_of_call … ge st f : IO ???;
    554       match ? return λx.description_of_function … fn = x → ? with
    555       [ Internal _ ⇒ λprf.
    556         let pc' ≝ eval_internal_call_pc … ge «fn, ?» in
    557         return mk_state_pc … st pc'
    558       | External fd ⇒ λ_.
    559         let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
    560         ! st' ← eval_external_call ??? fd args curr_dest st ;
    561         pop_frame … curr_fn st'
    562       ] (refl …)
     577      eval_tailcall … ge f args curr_id curr_fn st
    563578    ]
    564579  ].
    565 @(description_of_internal_function … prf)
    566 qed.
    567580
    568581definition eval_state : ∀p:sem_params. ∀globals: list ident.
     
    570583  state_pc p → IO io_out io_in (state_pc p) ≝
    571584  λp,globals,ge,st.
    572   ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
    573   eval_statement … ge fn st s.
     585  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
     586  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
     587  let st'' ≝ mk_state_pc … st' (pc … st) in
     588  eval_statement_advance … ge id fn s st''.
    574589
    575590(* Paolo: what if in an intermediate language main finishes with an external
     
    579594  genv p globals → program_counter → state_pc p → option int ≝
    580595 λp,globals,ge,exit,st.res_to_opt ? (
    581   do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
    582   let fn ≝ if_of_function … f in
     596  do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
    583597  match s with
    584598  [ final s' ⇒
    585599    match s' with
    586600    [ RETURN ⇒
    587       do st' ← pop_frame … ge f st;
    588       if eq_program_counter (pc … st') exit then
    589        do vals ← read_result … ge (joint_if_result … fn) st' ;
     601      do st' ← pop_frame … ge id fn st;
     602      ! nxt ← next_of_pc … ge (pc … st') ;
     603      let pc' ≝ succ_pc … (pc … st') nxt in
     604      if eq_program_counter pc' exit then
     605       do vals ← read_result … ge (joint_if_result … fn) st ;
    590606       Word_of_list_beval vals
    591607      else
  • src/joint/semanticsUtils.ma

    r2470 r2529  
    7575  mk_sem_params
    7676    g_pars
    77     (mk_more_sem_params
    78       g_pars
    79       (spars ?)
    80       (word_of_identifier ?)
    81       (an_identifier ?)
    82       ? (refl …)
    83     ).
     77    (spars ?)
     78    (word_of_identifier ?)
     79    (an_identifier ?)
     80    ? (refl …).
    8481* #p % qed.
    8582
     
    8986@pos_elim [%]
    9087#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
    91 
    9288
    9389definition make_sem_lin_params :
     
    9995  mk_sem_params
    10096    lin_pars
    101     (mk_more_sem_params
    102       lin_pars
    103       (spars ?)
    104       succ_pos_of_nat
    105       (λp.pred (nat_of_pos p))
    106       ??
    107     ).
    108 [ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
    109 | #n >nat_succ_pos %
     97    (spars ?)
     98    succ_pos_of_nat
     99    (λp.pred (nat_of_pos p))
     100    ??.
     101[ #n >nat_succ_pos %
     102| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
    110103] qed.
     104
     105
     106
     107
     108lemma fetch_statement_eq : ∀p:sem_params.∀g.
     109  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
     110  ∀i,fn,s.
     111  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
     112  let pt ≝ point_of_pc … ptr in
     113  stmt_at … (joint_if_code … fn) pt = Some ? s →
     114  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
     115#p #g #ge #ptr #i #f #s #EQ1 #EQ2
     116whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
     117>EQ2 %
     118qed.
     119
     120lemma fetch_statement_inv : ∀p:sem_params.∀g.
     121  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
     122  ∀i,fn,s.
     123  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
     124  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
     125  let pt ≝ point_of_pc p ptr in
     126  stmt_at … (joint_if_code … fn) pt = Some ? s.
     127#p #g #ge #ptr #i #fn #s #H
     128elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
     129elim (bind_inversion ????? H) #s' * #H
     130lapply (opt_eq_from_res ???? H) -H #EQ2
     131whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
     132qed.
     133
  • src/joint/semantics_blocks.ma

    r2422 r2529  
    11include "joint/blocks.ma".
    22include "joint/Traces.ma".
     3include "joint/semanticsUtils.ma".
    34
    45(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     
    89  ].*)
    910
    10 lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv p g.∀ptr : cpointer.
    11   ∀fn,pt,s.
    12   fetch_function … ge ptr = OK … fn →
    13   point_of_pointer ? p … ptr = pt →
    14   stmt_at … (joint_if_code … fn) pt = Some ? s →
    15   fetch_statement ? p … ge ptr = OK … 〈fn, s〉.
    16 #p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
    17 whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
    18 >EQ2 >EQ3 >m_return_bind %
    19 qed.
    20 
    21 include alias "basics/logic.ma".
    22 lemma io_evaluate_bind : ∀O,I,X,Y,env.
    23 ∀m : IO O I X.∀f : X → IO O I Y.
    24 io_evaluate O I Y env (! x ← m ; f x) =
    25 ! x ← io_evaluate O I X env m ;
    26 io_evaluate O I Y env (f x).
    27 #O #I #X #Y #env #m elim m
    28 [ #o #g #IH #f whd in match (! x ← Interact ????? ; ?);
    29   change with (! y ← ? ; ?) in ⊢ (??%(????%?));
    30   >m_bind_bind @m_bind_ext_eq #i @IH
    31 | #x #f %
    32 | #e #f %
    33 ]
    34 qed.
    35 
    36 lemma fetch_function_from_block_eq :
    37   ∀p,g,ge.
    38   ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
    39   fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
    40 #p #g #ge #ptr1 #ptr2 #EQ
    41 whd in match fetch_function; normalize nodelta >EQ
    42 @m_bind_ext_eq // qed.
    43 
    44 let rec repeat_eval_seq_no_pc
    45   (p : evaluation_params) env curr_fn
    46   (l : list (joint_seq p (globals p))) on l :
    47   state p → res (state p) ≝
    48   λst.match l with
    49   [ nil ⇒ return st
    50   | cons hd tl ⇒
    51     ! st' ← io_evaluate … (env st) (eval_seq_no_pc p (globals p) (ev_genv p) curr_fn st hd) ;
    52     repeat_eval_seq_no_pc p env curr_fn tl st'
    53   ].
    54 
    55 lemma err_to_io_evaluate : ∀O,I,X,env,m.
    56   io_evaluate O I X env (err_to_io … m) = m.
    57 #O#I#X#env * // qed.
     11definition repeat_eval_seq_no_pc ≝
     12  λp : evaluation_params.λcurr_id,curr_fn.
     13  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
    5814
    5915definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
    6016
    61 definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝
    62   λp,g,s.match s with
    63   [ COST_LABEL _ ⇒ false
    64   | CALL_ID _ _ _ ⇒ false
    65   | extension_call _ ⇒ false
    66   | _ ⇒ true
    67   ].
    68 
    69 lemma no_call_nor_label_proceed : ∀p : evaluation_params.
    70 ∀st : state p. ∀s.
    71 no_call_nor_label p (globals p) s →
    72 eval_seq_pc p (globals p) (ev_genv p) st s = return Proceed ???.
    73 #p #st * // [ #f #args #dest | #c ] *
    74 qed.
    75 
    76 lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
    77 no_call_nor_label p (globals p) s →
    78 step_classifier … s = cl_other.
    79 #p * // [ #f #args #dest | #c ] *
    80 qed.
    81 
    82 lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
    83 no_call_nor_label p (globals p) s →
    84 cost_label_of_stmt … (sequential … s nxt) = None ?.
    85 #p * // #lbl#next *
    86 qed.
    87 
    88 definition code_compact : ∀p:sem_params.∀g.codeT p g → Prop ≝
    89   λp,g,c.code_closed … c∧
    90     ∀pt,ptr.code_has_point … c pt → ∃ptr'.pointer_of_point p p ptr pt = return ptr'.
    91 
    92 definition pointer_of_point_step_in_code : ∀p:sem_params.∀g.
    93   ∀c,pc,step,dst.
    94   code_compact p g c → step_in_code … c (point_of_pointer p p pc) step dst →
    95   Σpc'.pointer_of_point p p pc dst = return pc' ≝
    96   λp,g,c,pc,step,dst,c_compact,step_in.
    97   match pointer_of_point p p pc dst
    98   return λx.pointer_of_point p p pc dst = x → ?
    99   with
    100   [ OK pc' ⇒ mk_Sig ?? pc'
    101   | Error e ⇒ λEQ.⊥
    102   ] (refl …).
    103 cases step_in #nxt * #EQ1 #EQ2
    104 cases c_compact -c_compact #c_closed #c_compact
    105 elim (c_compact dst pc ?)
    106 [ >EQ #pc' normalize #ABS destruct(ABS)
    107 | elim (c_closed … EQ1) #_ whd in ⊢ (%→?);
    108   >EQ2 #H @H
    109 ]
    110 qed.
    111 
    112 let rec pointer_of_point_in_code
    113   p g c pc dst b on b :
    114   ∀l.code_compact p g c → point_of_pointer p p pc ~❨b,l❩~> dst in c →
    115   Σpc'.pointer_of_point p p pc dst = return pc' ≝
    116 match b
    117 return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr'
    118 with
    119 [ nil ⇒
    120   λl,c_compact,in_code.
    121   match pointer_of_point p p pc dst
    122   return λx.pointer_of_point p p pc dst = x → ? with
    123   [ OK ptr' ⇒ mk_Sig ?? ptr'
    124   | Error e ⇒ λEQ.⊥
    125   ] (refl …)
    126 | cons hd tl ⇒
    127   λl.match l return λl.? → ? → Σptr'.? with
    128   [ nil ⇒ λc_compact,in_code.⊥
    129   | cons mid rest ⇒ λc_compact,in_code.
    130     let mid_pc ≝ pointer_of_point_step_in_code … c pc hd mid c_compact ? in
    131     pi1 … (pointer_of_point_in_code ?? c mid_pc dst tl rest c_compact ?)
    132   ]
    133 ].
    134 [ cases l in in_code; [2: #mid #rest * ]
    135   whd in ⊢ (%→?); #EQ' <EQ' in EQ; >pointer_of_point_of_pointer [2: %]
    136   normalize #ABS destruct(ABS)
    137 | cases (pointer_of_point_in_code ?????????)
    138   #ptr' >pointer_of_point_uses_block
    139   [ #H @H |*:]
    140   cases mid_pc -mid_pc #mid_pc @pointer_of_point_block
    141 | elim in_code
    142 | cases mid_pc -mid_pc #mid_pc #EQ
    143   >(point_of_pointer_of_point … EQ)
    144   cases in_code #_ #H @H
    145 | cases in_code #H #_ @H
    146 ]
    147 qed.
    148 
    14917let rec produce_trace_any_any
    15018  (p : evaluation_params)
    151   (st : state_pc p) fd
     19  (st : state_pc p)
     20  curr_id curr_fn
    15221  (b : list (joint_seq p (globals p))) on b :
    15322  ∀l : list (code_point p).
    15423  ∀dst : code_point p.
    15524  ∀st' : state p.
    156   fetch_function p ? (ev_genv p) (pc … st) = return fd →
    157   ∀prf1 : code_compact p (globals p) (joint_if_code … fd).
    158   let src ≝ point_of_pointer p p (pc … st) in
     25  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     26    return 〈curr_id, curr_fn〉 →
     27  let src ≝ point_of_pc p (pc … st) in
    15928  if list_not_empty ? b then
    160     ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
     29    ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
    16130  else
    16231    True →
    163   ∀prf2 : src ~❨b, l❩~> dst in joint_if_code … fd.
    164   All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
    165   repeat_eval_seq_no_pc p (io_env p) fd b st = return st' →
     32  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     33  All ? (λx.And (no_call … x) (no_cost_label … x)) b →
     34  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
    16635  trace_any_any (joint_abstract_status p) st
    167     (mk_state_pc ? st' (pointer_of_point_in_code … prf1 prf2)) ≝
    168   match b
    169   return λx.∀l,dst.?→?→?→?→?→?→?→?
     36    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
     37  return λb.∀l,dst.?→?→?→?→?→?→?
    17038  with
    17139  [ nil ⇒
    172     λl,dst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
     40    λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
    17341    (taa_base (joint_abstract_status p) st)
    174       ⌈trace_any_any (joint_abstract_status p) st st ↦ ?⌉
     42    ⌈trace_any_any ??? ↦ ?⌉
    17543  | cons hd tl ⇒
    17644    λl.
    177     match l return λx.?→?→?→?→?→?→?→?→? with
    178     [ nil ⇒ λdst_pc,st',fd_prf,src_prf,dst_prf,in_code.⊥
     45    match l return λx.∀dst,st'.?→?→?→?→?→? with
     46    [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
    17947    | cons mid rest ⇒
    180       λdst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
    181       let mid_pc ≝
    182         pointer_of_point_step_in_code p ? (joint_if_code … fd) (pc … st)
    183           hd mid c_compact ? in
    184       match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd)
    185       return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) = x → ?
    186       with
    187       [ OK st_mid ⇒ λEQ2.
     48      λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
     49      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
     50      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
     51      return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
     52      trace_any_any (joint_abstract_status p) st
     53        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with
     54      [ Value st_mid ⇒ λEQ2.
    18855        let tr_tl ≝ produce_trace_any_any ?
    18956            (mk_state_pc ? st_mid mid_pc)
    190             fd tl rest dst ??????? in
    191         (* works fast only in interactive mode:
    192         taa_step … tr_tl *) ?
    193       | Error _ ⇒ λEQ2.⊥
     57            curr_id curr_fn tl rest dst ?????? in
     58        taa_step … tr_tl
     59      | _ ⇒ λEQ2.⊥
    19460      ] (refl …)
    19561    ]
    196   ].[3: @(taa_step … tr_tl) |*:]
    197 try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc)
    198 try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code)
    199 try (cases all_other #hd_other #tl_other)
     62  ].
     63[ whd in EQ1 : (??%%);
     64  cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct
     65  >pc_of_point_of_pc cases st //
     66| @in_code
     67|3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
     68]
     69change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
     70>EQ2 in EQ1; >m_return_bind
     71cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
     72cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
     73#EQ1
     74try assumption
    20075[ whd whd in match eval_state; normalize nodelta
    201   >(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
     76  >(fetch_statement_eq … fd_prf EQ_stmt_at)
    20277  >m_return_bind
    203   whd in match eval_statement; normalize nodelta
    204   whd in match eval_step; normalize nodelta
    205   >m_bind_bind
    206   >(no_call_nor_label_proceed … hd_other) >m_return_bind
    207   >m_bind_bind
    208   >io_evaluate_bind >EQ2 >m_return_bind
    209   >m_return_bind
     78  whd in match eval_statement_no_pc; normalize nodelta
     79  >EQ2 >m_return_bind
     80  whd in match eval_statement_advance; normalize nodelta
     81  >(no_call_advance … hd_no_call)
     82  whd in match next; normalize nodelta
    21083  whd in match succ_pc; normalize nodelta
    211   >EQ_mid >EQ_mid_pc >m_return_bind %
    212 | whd %{fd} %{(sequential … hd nxt)}
    213   %{(no_call_nor_label_other … hd_other)}
    214   @(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
    215 |4: cases (pointer_of_point_in_code ?????????)
    216   #dst_pc
    217   cases l in in_code; [2: #mid #rest * ]
    218   whd in ⊢ (%→?); #EQ' <EQ'
    219   >pointer_of_point_of_pointer [2: %] lapply EQ1 -EQ1
    220   normalize in ⊢ (%→%→?);
    221   #EQ1 #EQ'' destruct cases st //
    222 |5: >fetch_function_from_block_eq [ @fd_prf |*: ]
    223   @(pointer_of_point_block … EQ_mid_pc)
    224 |6: cases tl [ % ] #hd' #tl' @dst_prf
    225 |7: assumption
    226 |8,9:
    227   lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize nodelta
    228   [ #H @H
    229   | normalize #ABS destruct(ABS)
     84  >EQ_mid %
     85| whd whd in ⊢ (??%?);
     86  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta
     87  @(no_call_other … hd_no_call)
     88| whd in ⊢ (?%);
     89  whd in match as_label; normalize nodelta
     90  %* #H @H -H whd in ⊢ (??%?);
     91  whd in match (as_pc_of ??);
     92  inversion (fetch_statement ????) normalize nodelta
     93  [2: // ]
     94  ** #i' #f' #stmt' #EQ
     95  elim (fetch_statement_inv … EQ)
     96  >fd_prf
     97  whd in ⊢ (??%?→?); #EQ destruct(EQ)
     98  whd in ⊢ (%→?);
     99  whd in match (point_of_pc ??); >point_of_offset_of_point
     100  #EQ'
     101  cases tl in tl_other rest_in_code;
     102  [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ)
     103    >EQ' in dst_prf; >m_return_bind #H @H
     104  | #hd' #tl' ** #_ #hd_no_cost' #_
     105    cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_
     106    >EQ_stmt_at' in EQ'; #EQ' destruct(EQ')
     107    @(no_label_uncosted … hd_no_cost')
    230108  ]
    231 |3:
    232   %* #H @H -H
    233   lapply tl_other lapply rest_in_code
    234   cases tl [2: #hd' #tl' ]
    235   cases rest [2,4: #mid' #rest']
    236   [2,3: * ]
    237   [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
    238   | ** #nxt' * #at_mid #_ #_ * #mid_other #_
    239   ]
    240   whd in ⊢ (??%?);
    241   [ lapply dst_prf ]
    242   whd in match as_label;
    243   whd in match (as_pc_of ??);
    244   whd in match fetch_statement;
    245   normalize nodelta
    246   >(point_of_pointer_of_point … EQ_mid_pc)
    247   >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc))
    248   >fd_prf >m_return_bind
    249   [ cases (stmt_at ????) [ #_ % ]
    250     #stmt #H @H
    251   | >at_mid >m_return_bind normalize nodelta
    252     @(no_call_nor_label_uncosted … mid_other)
    253   ]
     109| >dst_prf cases (list_not_empty ??) %
     110| normalize nodelta >point_of_pc_of_point assumption
    254111]
    255112qed.
  • src/utilities/monad.ma

    r2453 r2529  
    211211  λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y.
    212212
     213let rec m_fold (M : Monad)
     214  X Y (f : X → Y → M Y) (l : list X) (init : Y) on l : M Y ≝
     215match l with
     216[ nil ⇒ return init
     217| cons hd tl ⇒
     218  ! y ← f hd init ;
     219  m_fold M X Y f tl y
     220].
     221
     222lemma m_fold_append : ∀M : MonadProps.∀X,Y,f,l1,l2,init.
     223  m_fold M X Y f (l1@l2) init =
     224  ! y ← m_fold … f l1 init ;
     225  m_fold … f l2 y.
     226#M #X #Y #f #l1 elim l1 -l1
     227[ #l2 #init >m_return_bind %
     228| #hd #tl #IH #l2 #init >m_bind_bind @m_bind_ext_eq #y @IH
     229]
     230qed.
     231
    213232unification hint 0 ≔ M, X, Y, Z, m, f ;
    214233  P ≟ Prod X Y, F ≟ λp.f (\fst p) (\snd p) ⊢
Note: See TracChangeset for help on using the changeset viewer.