Changeset 2186


Ignore:
Timestamp:
Jul 16, 2012, 4:59:09 PM (5 years ago)
Author:
tranquil
Message:

updated joint semantics

Location:
src
Files:
6 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r2155 r2186  
    5959definition rtl_statement ≝ joint_statement rtl_params.
    6060
    61 interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
     61interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? rtl_argument r a)).
    6262
    6363(* aid unification *)
  • src/common/StructuredTraces.ma

    r2129 r2186  
    334334qed.
    335335
    336 (* an uncalling, unreturning and *unjumping*,
    337   as well as unlabelled (but possibly for the first and last statuses)
    338   possibly empty trace segment *)
    339 inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
    340   | taa_base :
     336(*
     337(* an trace of unlabeled and cl_other states, possibly empty *)
     338inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝
     339  | tna_base :
    341340      ∀start_status: S.
    342         trace_any_any S start_status start_status
    343   | taa_step :
     341      ¬as_costed … start_status →
     342      trace_no_label_any S start_status start_status
     343  | tna_step :
    344344      ∀status_pre: S.
    345345      ∀status_init: S.
    346346      ∀status_end: S.
    347347        as_execute S status_pre status_init →
    348         trace_any_any S status_init status_end →
    349348        as_classifier S status_pre cl_other →
    350         ¬as_costed … status_init →
    351           trace_any_any S status_pre status_end.
    352 
    353 let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
     349        ¬as_costed … status_pre →
     350        trace_no_label_any S status_init status_end →
     351          trace_no_label_any S status_pre status_end.
     352
     353let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2)
     354  on taa1 :
     355    trace_no_label_any S st2 st3 →
     356    trace_no_label_any S st1 st3 ≝
     357  match taa1 with
     358  [ tna_base st1' H ⇒ λtaa2.taa2
     359  | tna_step st1' st2' st3' H G K tl ⇒
     360    λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2)
     361  ].
     362
     363definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2.
     364  match tna with
     365  [ tna_base _ _ ⇒ false
     366  | tna_step _ _ _ _ _ _ _ ⇒ true
     367  ].
     368
     369coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝
     370 tna_non_empty on _tna : trace_no_label_any ??? to bool.
     371
     372lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1.
     373#S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed.
     374
     375let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2)
     376  on tna :
     377  trace_any_label S fl st2 st3 →
     378  if tna then Not (as_costed … st2) else True →
     379  trace_any_label S fl st1 st3 ≝
     380  match tna return λst1,st2.λx : trace_no_label_any S st1 st2.
     381    ∀fl,st3.
     382    trace_any_label S fl st2 st3 →
     383    if x then Not (as_costed … st2) else True →
     384    trace_any_label S fl st1 st3
     385  with
     386  [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2
     387  | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf.
     388    tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl)
     389  ] fl st3.
     390  cases (tna_non_empty … tl) [@prf|%]
     391  qed.
     392*)
     393
     394inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝
     395  | taa_base : ∀st.trace_any_any S st st
     396  | taa_step : ∀st1,st2,st3.
     397    as_execute S st1 st2 →
     398    as_classifier S st1 cl_other →
     399    ¬as_costed S st2 →
     400    trace_any_any S st2 st3 →
     401    trace_any_any S st1 st3.
     402
     403definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2.
    354404  match taa with
    355   [ taa_base st1' ⇒ [st1']
    356   | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
     405  [ taa_base _ ⇒ false
     406  | taa_step _ _ _ _ _ _ _ ⇒ true
    357407  ].
    358408
    359 let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
    360   on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
    361   match taa1
    362   return λst1,st2.λx : trace_any_any S st1 st2.
    363     trace_any_any S st2 st3 → trace_any_any S st1 st3
    364   with
    365   [ taa_base _ ⇒ λtaa2.taa2
    366   | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
    367       taa_step … H (taa_append_taa … tl taa2) G K
    368   ].
    369 
    370 let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
    371   on taa :
     409coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝
     410 taa_non_empty on _taa : trace_any_any ??? to bool.
     411
     412let rec taa_append_tal S st1 fl st2 st3
     413  (taa : trace_any_any S st1 st2) on taa :
    372414  trace_any_label S fl st2 st3 →
    373415  trace_any_label S fl st1 st3 ≝
    374   match taa
    375   return λst1,st2.λx : trace_any_any S st1 st2.
    376     trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
     416  match taa return λst1,st2.λx : trace_any_any S st1 st2.
     417    ∀fl,st3.
     418    trace_any_label S fl st2 st3 →
     419    trace_any_label S fl st1 st3
    377420  with
    378   [ taa_base _ ⇒ λtaa2.taa2
    379   | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
    380       tal_step_default … H (taa_append_tal … tl taa2) G K
    381   ].
     421  [ taa_base st1' ⇒ λfl,st3,tal2.tal2
     422  | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2.
     423    tal_step_default ????? H (taa_append_tal ????? tl tal2) G K
     424  ] fl st3.
     425
     426interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal).
    382427
    383428let rec tlr_rel S1 st1 st1' S2 st2 st2'
     
    416461    fl2 = doesnt_end_with_ret ∧
    417462    ∃st2mid,taa,H,G,K.
    418     tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     463    tal2 ≃ taa_append_tal ? st2 ??? taa
    419464      (tal_base_not_return ? st2mid st2' H G K)
    420465  | tal_base_return st1 st1' _ _ ⇒
     
    437482    tal_rel … tl1 tal2 (* <- this makes it many to many *)
    438483  ].
    439  
     484
    440485interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
    441486interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
    442 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2).
    443 
     487interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2).
     488
     489let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2'
     490  (taa1 : trace_any_any S1 st1 st1mid) on taa1 :
     491  ∀tal1 : trace_any_label S1 fl1 st1mid st1'.
     492  ∀tal2 : trace_any_label S2 fl2 st2 st2'.
     493  tal_rel … (taa1 @ tal1) tal2 →
     494  tal_rel … tal1 tal2 ≝ ?.
     495cases taa1 -taa1
     496[ -taa_rel_inv //
     497| #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?);
     498  @(taa_rel_inv … tl)
     499]
     500qed.
     501
     502let rec tlr_rel_transitive S1 st1 st1' S2 st2 st2' S3 st3 st3'
     503  (tlr1 : trace_label_return S1 st1 st1')
     504  (tlr2 : trace_label_return S2 st2 st2')
     505  (tlr3 : trace_label_return S3 st3 st3') on tlr1 :
     506  tlr_rel … tlr1 tlr2 → tlr_rel … tlr2 tlr3 → tlr_rel … tlr1 tlr3 ≝
     507match tlr1 with
     508  [ tlr_base st1' st1'' tll1 ⇒ ?
     509  | tlr_step st1' st1'' st1''' tll1 tl1 ⇒ ?
     510  ]
     511and tll_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
     512  (tll1 : trace_label_label S1 fl1 st1 st1')
     513  (tll2 : trace_label_label S2 fl2 st2 st2')
     514  (tll3 : trace_label_label S3 fl3 st3 st3') on tll1 :
     515  tll1 ≈ tll2 → tll2 ≈ tll3 → tll1 ≈ tll3 ≝
     516  match tll1 with
     517  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
     518  ]
     519and tal_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
     520  (tal1 : trace_any_label S1 fl1 st1 st1')
     521  (tal2 : trace_any_label S2 fl2 st2 st2')
     522  (tal3 : trace_any_label S3 fl3 st3 st3') on tal1 :
     523  tal1 ≈ tal2 → tal2 ≈ tal3 → tal1 ≈ tal3 ≝
     524  match tal1 with
     525  [ tal_base_not_return st1' st1'' H G K ⇒ ?
     526  | tal_base_return st1' st1'' H G ⇒ ?
     527  | tal_base_call st1' st1'' st1''' H G K tlr1 L ⇒ ?
     528  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
     529  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
     530  ].
     531[1,2: cases tlr2 #st2' #st2'' [1,3: #tllhd2 |2,4: #st2''' #tllhd2 #tlrtl2]
     532  [2,3: *] normalize in ⊢ (%→?); [ #Rhd12 | * #Rhd12 #Rtl12 ]
     533  cases tlr3 #st3' #st3'' [1,3: #tllhd3 |2,4: #st3''' #tllhd3 #tlrtl3]
     534  [2,3: *] normalize in ⊢ (%→?); [ #Rhd23 | * #Rhd23 #Rtl23 ] whd
     535  [ @(tll_rel_transitive … Rhd12 Rhd23) |
     536    %{(tll_rel_transitive … Rhd12 Rhd23)}
     537    @(tlr_rel_transitive … Rtl12 Rtl23)
     538  ]
     539|3:
     540  cases tll2 #fl2' #st2' #st2'' #tal2 #H2 * #G2 #R12
     541  cases tll3 #fl3' #st3' #st3'' #tal3 #H3 * #G3 #R23
     542  %{(tal_rel_transitive … R12 R23)} //
     543|*:
     544  [1,2,3: * #EQ]
     545  [5: whd in ⊢ (%→?→%); @tal_rel_transitive]
     546  *#st2mid *#taa2
     547  [ *#H2 *#G2 *#K2 #R12
     548  | *#H2 *#G2 #R12
     549  | *#st2' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12'
     550  | *#st2' *#st2'' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12''
     551  ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // |3: *#EQ destruct]
     552  *#st3mid *#taa3
     553  [ *#st3' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23'
     554    %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{G3} %{K3} %{tlr3} %{L3}
     555    %{R23} @(tlr_rel_transitive … R12' R23')
     556  | *#st3' *#st3'' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23''
     557    %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{G3} %{K3} %{tlr3} %{L3} %{tl3}
     558    %{(tal_rel_transitive … R12'' R23'')}
     559    %{R23} @(tlr_rel_transitive … R12' R23')
     560  ]
     561]
     562qed.
    444563
    445564let rec flatten_trace_label_label
     
    507626  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
    508627  ∀tal : trace_any_label S fl st2 st3.
    509     flatten_trace_any_label … (taa_append_tal … taa tal) =
     628    flatten_trace_any_label … (taa @ tal) =
    510629      flatten_trace_any_label … tal ≝ ?.
    511630cases taa -st1 -st2
    512 [ #st1 #tal %
    513 | #st_pre #st_init #st2 #H #taa #G #K #tal
    514   whd in match (taa_append_tal ???????);
     631[ //
     632| #st_pre #st_init #st2 #H #G #K #taa' #tal
     633  whd in match (? @ ?);
    515634  whd in ⊢ (??%?); //
    516635]
    517 qed. 
    518 
     636qed.
    519637
    520638let rec tll_rel_to_traces_same_flatten
     
    606724  λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
    607725
    608 definition lift_cost_map_id :
    609   ∀S_in, S_out: abstract_status.
    610    (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) +
    611        ¬(∃pc.as_label_of_pc S_out pc = Some … l)) →
    612   (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig.
    613    match dec l_sig with
    614    [ inl prf ⇒ m «l_sig, prf»
    615    | inr _ ⇒ 0 (* labels not present in out code get 0 *)
     726definition lift_sigma_map_id :
     727  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
     728    (∀a.P_out a + ¬ P_out a) →
     729  ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
     730   match dec a_sig with
     731   [ inl prf ⇒ m «a_sig, prf»
     732   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
    616733   ].
    617734
    618 lemma lift_cost_map_id_eq :
    619   ∀S_in, S_out, dec, m, l_in, l_out.
    620   pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out.
    621 #S_in #S_out #dec #m #l_in * #l_out #prf #EQ
    622 whd in match lift_cost_map_id; normalize nodelta
    623 cases (dec l_in) normalize nodelta >EQ
    624 [2: #H @⊥] /2 by refl, absurd/
     735lemma lift_sigma_map_id_eq :
     736  ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
     737  pi1 ?? a_in = pi1 ?? a_out →
     738  lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
     739#A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
     740whd in match lift_sigma_map_id; normalize nodelta
     741cases (dec a_in) normalize nodelta >EQ cases a_out
     742#a #H #G [ % | @⊥ /2 by absurd/ ]
    625743qed.
    626744
     
    631749  with precedence 20
    632750for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
     751
     752definition lift_cost_map_id :
     753  ∀S_in,S_out : abstract_status.? →
     754  as_cost_map S_out → as_cost_map S_in
     755  ≝
     756 λS_in,S_out : abstract_status.
     757  lift_sigma_map_id costlabel ℕ
     758    (λl.∃pc.as_label_of_pc S_in pc = Some ? l)
     759    (λl.∃pc.as_label_of_pc S_out pc = Some ? l)
     760    0.
    633761
    634762lemma lift_cost_map_same_cost :
     
    645773  #EQ destruct
    646774  whd in ⊢(??%%);
    647   >(lift_cost_map_id_eq … e0)
     775  whd in match lift_cost_map_id; normalize nodelta
     776  >(lift_sigma_map_id_eq ????????? e0)
    648777  >e0 in e1; normalize in ⊢(%→?); #EQ
    649778  >(IH … EQ) %
  • src/joint/Joint_paolo.ma

    r2182 r2186  
    181181  match s with
    182182  [ GOTO l ⇒ Labels … [l]
    183   | _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *)
     183  | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *)
     184  | _ ⇒ Labels … [ ]
    184185  ].
    185186
  • src/joint/Traces.ma

    r1976 r2186  
    11include "joint/semantics_paolo.ma".
    2 include "common/StructuredTraces.ma".
    32
    4 definition stmt_classifier :
    5   ∀p : params.∀globals.
    6     (ext_step p → status_class) →
    7     (ext_fin_stmt p → status_class) →
    8     joint_statement p globals → status_class
    9   ≝ λp,globals,ext_step_classifier,ext_fin_step_classifier,s.
    10   match s with
    11   [ sequential stp _ ⇒
    12     match stp with
    13     [ COND _ _ ⇒ cl_jump
    14     | extension ext_s ⇒ ext_step_classifier ext_s
    15     | CALL_ID _ _ _ ⇒ cl_call (* Paolo : this does not take into account external calls! *)
    16     | _ ⇒ cl_other
    17     ]
    18   | final stp ⇒
    19     match stp with
    20     [ RETURN ⇒ cl_return
    21     | extension_fin ext_s ⇒ ext_fin_step_classifier ext_s
    22     | _ ⇒ cl_other
    23     ]
    24   ].
     3record evaluation_params : Type[1] ≝
     4 { globals: list ident
     5 ; sparams:> sem_params
     6 ; exit: cpointer
     7 ; ev_genv: genv globals sparams
     8 ; io_env : state sparams → ∀o:io_out.res (io_in o)
     9 } .
     10
     11(*record classifier_params : Type[1] ≝
     12  { cl_pars :> evaluation_parameters
     13  ; cl_ext_step : ext_step cl_pars → status_class
     14  ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class
     15  }.*)
     16
    2517
    2618definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
     
    3022]
    3123qed.
    32  
     24
     25let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
     26  match c with
     27  [ Value x ⇒ OK … x
     28  | Interact o f ⇒
     29    ! i ← env o ;
     30    io_evaluate O I X env (f i)
     31  | Wrong e ⇒ Error … e
     32  ].
     33
     34definition cost_label_of_stmt :
     35  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
     36  λp,s.match s with
     37  [ sequential s _ ⇒
     38    match s with
     39    [ step_seq s ⇒
     40      match s with
     41      [ COST_LABEL lbl ⇒ Some ? lbl
     42      | _ ⇒ None ?
     43      ]
     44    | _ ⇒ None ?
     45    ]
     46  | _ ⇒ None ?
     47  ].
     48
    3349definition joint_abstract_status :
    34  ∀p : evaluation_parameters.
    35  (ext_step p → status_class) →
    36  (ext_fin_stmt p → status_class) →
    37  abstract_status ≝
    38  λp,ext_step_cl,ext_fin_step_cl.
     50 ∀p : evaluation_params.
     51 abstract_status ≝
     52 λp.
    3953 mk_abstract_status
    4054   (* as_status ≝ *) (state_pc p)
    41    (* as_execute ≝ *) (λs1,s2.eval_state … p (genv2 p) s1 = return s2)
     55   (* as_execute ≝ *)
     56    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
    4257   (* as_pc ≝ *) cpointerDeq
    4358   (* as_pc_of ≝ *) (pc …)
    4459   (* as_classifier ≝ *)
    45     (λs,cl.∃stmt.fetch_statement ? p … (genv2 p) (pc … s) = return stmt ∧
    46      stmt_classifier … ext_step_cl ext_fin_step_cl stmt = cl)
     60    (λs,cl.∃stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return stmt ∧
     61     stmt_classifier … stmt = cl)
    4762   (* as_label_of_pc ≝ *)
    4863    (λpc.
    49       match fetch_statement ? p … (genv2 p) pc with
    50       [ OK stmt ⇒
    51         match stmt with
    52         [ sequential s _ ⇒
    53           match s with
    54           [ COST_LABEL l ⇒ Some ? l
    55           | _ ⇒ None ?
    56           ]
    57         | _ ⇒ None ?
    58         ]
     64      match fetch_statement ? p … (ev_genv p) pc with
     65      [ OK stmt ⇒ cost_label_of_stmt … stmt
    5966      | _ ⇒ None ?
    6067      ])
    6168   (* as_after_return ≝ *)
    62     (λs1,s2. (* Paolo: considering sequential calls, tailcalls are out of the picture for now *)
    63       ∃stp,nxt.fetch_statement ? p … (genv2 p) (pc … s1) = return (sequential ?? stp nxt) ∧
     69    (λs1,s2.
     70      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
     71      ∃stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return (sequential ?? stp nxt) ∧
    6472      succ_pc p p (pc … s1) nxt = return pc … s2)
    65    (* as_final ≝ *) (λs.is_final (globals ?) p (genv2 p) (exit p) s ≠ None ?).
     73   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).
  • src/joint/blocks.ma

    r2155 r2186  
    176176  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
    177177  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
     178
     179notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
     180  @{'block_in_code $c $x $B $l $y}.
     181 
     182notation < "hvbox(x ~❨ B , l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
     183  @{'block_in_code $c $x $B $l $y}.
     184
     185definition step_in_code ≝
     186  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
     187  λdst : code_point p.
     188  ∃nxt.stmt_at … c src = Some ? (sequential … s nxt) ∧
     189       point_of_succ … src nxt = dst.
     190
     191definition fin_step_in_code ≝
     192  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_fin_step p.
     193  stmt_at … c src = Some ? (final … s).
     194
     195let rec seq_list_in_code p globals (c : codeT p globals)
     196  (src : code_point p) (B : list (joint_seq p globals))
     197  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
     198  match B with
     199  [ nil ⇒
     200    match l with
     201    [ nil ⇒ src = dst
     202    | _ ⇒ False
     203    ]
     204  | cons hd tl ⇒
     205    match l with
     206    [ nil ⇒ False
     207    | cons mid rest ⇒
     208      step_in_code …  c src hd mid ∧ seq_list_in_code … c mid tl rest dst
     209    ]
     210  ].
     211
     212interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).
     213
     214lemma seq_list_in_code_append :
     215  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
     216  src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c →
     217  src ~❨B1@B2,l1@l2❩~> dst in c.
     218#p #globals #c #src #B1 lapply src -src elim B1
     219[ #src * [2: #mid' #rest] #mid #B2 #l2 #dst [*] #EQ normalize in EQ; destruct(EQ)
     220  #H @H
     221| #hd #tl #IH #src * [2: #mid' #rest] #mid #B2 #l2 #dst * #H1 #H2
     222  #H3 %{H1 (IH … H2 H3)}
     223]
     224qed.
     225
     226lemma seq_list_in_code_append_inv :
     227  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
     228  src ~❨B1@B2,l❩~> dst in c →
     229  ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c.
     230#p #globals #c #src #B1 lapply src -src elim B1
     231[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
     232| #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
     233  elim (IH … H2) #l1 * #mid' * #l2 ** #G1 #G2 #G3
     234  %{(mid::l1)} %{mid'} %{l2} %{G3} >G1 %{(refl …)}
     235  %{H1 G2}
     236]
     237qed.
     238
     239definition seq_block_step_in_code ≝
     240  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
     241  src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst.
     242
     243definition seq_block_fin_step_in_code ≝
     244  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
     245  src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B).
     246
     247(* generates ambiguity even if it shouldn't
     248interpretation "seq block step in code" 'block_in_code c x B l y = (seq_block_step_in_code ?? c x B l y).
     249interpretation "seq block fin step in code" 'block_in_code c x B l y = (seq_block_fin_step_in_code ?? c x B l y).
     250*)
    178251
    179252(*
  • src/joint/semantics_blocks.ma

    r2043 r2186  
    11include "joint/blocks.ma".
    2 include "joint/semantics_paolo.ma".
    3 
    4 
    5 axiom ExecutingInternalCallInBlock : String.
    6 
    7 let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     2include "joint/Traces.ma".
     3
     4(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
    85  match b with
    96  [ nil ⇒ [ ]
    107  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
    11   ].
    12 
    13 definition step_flow_change_labels :
    14   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    15     step_flow p g lbls1 → step_flow p g lbls2 ≝
    16   λp,g,lbls1,lbls2,prf,flow.
    17   match flow with
    18   [ Redirect l ⇒ Redirect ??? «l, prf ? (pi2 … l)»
    19   | Init id b args dest ⇒ Init … id b args dest
    20   | Proceed ⇒ Proceed ???
    21   ].
    22 
    23 coercion step_flow_diff_lbls :
    24   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    25   ∀flow : step_flow p g lbls1.step_flow p g lbls2 ≝
    26   step_flow_change_labels on _flow : step_flow ??? to step_flow ???.
    27 
    28 definition monad_step_flow_times_coerc :
    29   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    30     monad M ((step_flow p g lbls1) × A) → monad M ((step_flow p g lbls2) × A) ≝
    31     λp,g,lbls1,lbls2,M,A,H,m.
    32     ! 〈flow,a〉 ← m ;
    33     return 〈(flow : step_flow ?? lbls2),a〉. assumption qed.
    34 
    35 coercion step_flow_monad_times :
    36   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    37     ∀m : monad M ((step_flow p g lbls1) × A).monad M ((step_flow p g lbls2) × A) ≝
    38   monad_step_flow_times_coerc on _m : monad ? ((step_flow ???) × ?) to monad ? ((step_flow ???) × ?).
    39 
    40 let rec eval_seq_list globals (p:sem_params) (ge : genv globals p)
    41   (st : state p) (b : list (joint_step p globals)) on b :
    42     IO io_out io_in ((step_flow p globals (seq_list_labels … b)) × (state p)) ≝
    43     match b return λx.IO ?? ((step_flow ?? (seq_list_labels … x)) × ?) with
    44     [ nil ⇒ return 〈Proceed ???, st〉
    45     | cons hd tl ⇒
    46       ! 〈flow, st'〉 ← eval_step … ge st hd ;
    47       match flow return λ_.IO ?? ((step_flow ?? (seq_list_labels … (hd :: tl))) × ?) with
    48       [ Proceed ⇒ eval_seq_list globals p ge st' tl
    49       | _ ⇒ return 〈flow, st'〉
    50       ]
    51     ]. /2 by Exists_append_r, Exists_append_l/ qed.
    52 
    53 definition fin_step_flow_change_labels :
    54   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    55     fin_step_flow p g lbls1 → fin_step_flow p g lbls2 ≝
    56   λp,g,lbls1,lbls2,prf,flow.
    57   match flow with
    58   [ FRedirect l ⇒ FRedirect ??? «l, prf ? (pi2 … l)»
    59   | FTailInit id b args ⇒ FTailInit … id b args
    60   | FEnd ⇒ FEnd ???
    61   ].
    62 
    63 coercion fin_step_flow_diff_lbls :
    64   ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
    65   ∀flow : fin_step_flow p g lbls1.fin_step_flow p g lbls2 ≝
    66   fin_step_flow_change_labels on _flow : fin_step_flow ??? to fin_step_flow ???.
    67 
    68 definition monad_fin_step_flow_times_coerc :
    69   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    70     monad M ((fin_step_flow p g lbls1) × A) → monad M ((fin_step_flow p g lbls2) × A) ≝
    71     λp,g,lbls1,lbls2,M,A,H,m.
    72     ! 〈flow,a〉 ← m ;
    73     return 〈(flow : fin_step_flow ?? lbls2),a〉. assumption qed.
    74 
    75 coercion fin_step_flow_monad_times :
    76   ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
    77     ∀m : monad M ((fin_step_flow p g lbls1) × A).monad M ((fin_step_flow p g lbls2) × A) ≝
    78   monad_fin_step_flow_times_coerc on _m : monad ? ((fin_step_flow ???) × ?) to monad ? ((fin_step_flow ???) × ?).
    79 
    80 definition block_cont_labels ≝ λp,g,ty.λb : block_cont p g ty.
    81   seq_list_labels … (\fst b) @
    82   match ty return λx.stmt_type_if ? x ??? → ? with
    83   [ SEQ ⇒ step_labels …
    84   | FIN ⇒ fin_step_labels …
    85   ] (\snd b).
    86 
    87 definition eval_block_cont :
    88   ∀globals.∀p : sem_params.∀ty.genv globals p →
    89   state p → ∀b : block_cont p globals ty.
    90   IO io_out io_in (
    91     (stmt_type_if ? ty step_flow fin_step_flow p globals (block_cont_labels … b)) ×
    92     (state p)) ≝ λglobals,p,ty,ge,st.
    93   match ty return λx.∀b : block_cont p globals x.
    94     IO io_out io_in (
    95       (stmt_type_if ? x step_flow fin_step_flow p globals (block_cont_labels … b)) ×
    96       (state p))
    97   with
    98   [ SEQ ⇒ λb.
    99     ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
    100     match flow return λ_.IO ?? (step_flow … ((block_cont_labels … b))×?) with
    101     [ Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
    102     | Proceed ⇒ eval_step … ge st' (\snd b)
    103     | Init _ _ _ _ ⇒
    104       Error … (msg ExecutingInternalCallInBlock)
    105     ]
    106   | FIN ⇒ λb.
    107     ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
    108     match flow return λ_.IO ?? ((fin_step_flow … (block_cont_labels … b))×?) with
    109     [ Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
    110     | Proceed ⇒ eval_fin_step … ge st' (\snd b)
    111     | Init _ _ _ _ ⇒
    112       Error … (msg ExecutingInternalCallInBlock)
    113     ]
    114   ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.
    115 
    116 (*
    117 lemma m_pred
    118 
    119 lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X.
    120   ∀f : X → monad M Y.m_pred MP P … m →
    121   ! x ← m ; f x = ! x ← 
    122 *)
    123 
    124 definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
    125   λp,globals,lbls,A,flp.
    126   match \fst flp with
    127   [ Init _ _ _ _ ⇒ False
    128   | _ ⇒ True
    129   ].
    130 
    131 definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
    132   λp,globals,lbls,A,flp.
    133   match \fst flp with
    134   [ Proceed ⇒ True
    135   | _ ⇒ False
    136   ].
    137 
    138 definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝
    139 λp,globals,ge,s.match s with
    140 [ CALL_ID f args dest ⇒
    141   Try
    142     ! b ← find_symbol … ge f ;
    143     ! fd ← find_funct_ptr … ge b ;
    144     match fd with
    145     [ Internal _ ⇒ return False
    146     | External _ ⇒ return True
    147     ]
    148   catch ⇒
    149     True
    150 | extension c ⇒
    151   ∀st : state p.
    152   pred_io … (λ_.True) (no_init …) (exec_extended … ge c st)
    153 | _ ⇒ True
    154 ].
    155 
    156 definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ].
    157 
    158 lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y.
    159   err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x.
    160 #O #I #X #Y * //
    161 qed.
    162 
    163 lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
    164 #O #I #X #m elim m // qed.
    165 
    166 (*
    167 lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
    168 #X #m elim m // qed.
    169 *)
    170 
    171 (*
    172 lemma never_calls_no_init : ∀p,globals,ge,s.
    173   never_calls p globals ge s →
    174   ∀st : state p.
    175   pred_io … (λ_.True) (no_init …) (eval_step … ge st s).
    176 #p#g#ge * //
    177 [10,12:
    178 |*:
    179   #a #b #c try #d try #e try #f try #g
    180   @res_io_pred
    181   @(mp_bind … (λ_.True) … (pred_res_True …))
    182   #st *  try (@mp_return @I)
    183   @(mp_bind … (λ_.True) … (pred_res_True …))
    184   #st * [9: elim st] normalize nodelta try (@mp_return @I)
    185   @(mp_bind … (λ_.True) … (pred_res_True …))
    186   #st *  try (@mp_return @I)
    187   @(mp_bind … (λ_.True) … (pred_res_True …))
    188   #st * [elim (opaccs ????) #by1 #by2 normalize nodelta]
    189   @(mp_bind … (λ_.True) … (pred_res_True …))
    190   #st * [2: elim (op2 ?????) #by #bit  normalize nodelta]
    191   try (@mp_return @I)
    192   @(mp_bind … (λ_.True) … (pred_res_True …))
    193   #st * @mp_return @I
    194 ]
    195 [ #id #args #dest #H whd in H;
    196   #st change with (! x ← ? ; ?) in match (eval_step ?????);
    197   elim (find_symbol ???) in H ⊢ %; [//]
    198   #b >m_return_bind  >m_return_bind
    199   change with (! x ← ? ; ?) in match (eval_call_block ?????????);
    200   elim (find_funct_ptr ???) [//]
    201   #fd >m_return_bind  >m_return_bind
    202   elim fd #fn normalize nodelta *
    203   @(mp_bind … (λ_.True)) [//]
    204   #st * @(mp_bind … (λ_.True) … (pred_io_True …))
    205   #st * @(mp_bind … (λ_.True) … (pred_io_True …))
    206   #st * @(mp_bind … (λ_.True) … (pred_io_True …))
    207   #st * @mp_return %
    208 | #s #H @H
    209 ]
    210 qed.
    211 
    212 lemma unbranching_truly_sequential : ∀p,globals,ge,s.
    213   unbranching p globals ge s →
    214   ∀st : state p.
    215   pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s).
    216 #p#globals#ge#s * #H #G #st
    217 lapply (never_calls_no_init … H st) @m_pred_mp
    218 >G * *
    219 [ * #lbl * | #id #fd #args #dest ] #st * %
    220 qed.
    221 *)
    222 
    223 lemma seq_list_labels_append : ∀p,globals,b1,b2.
    224   seq_list_labels p globals (b1 @ b2) =
    225   seq_list_labels … b1 @ seq_list_labels … b2.
    226 #p #g #b1 elim b1
    227 [ //
    228 | #hd #tl #IH #b2 whd in ⊢ (??%%);
    229   >associative_append <IH %
    230 ]
    231 qed.
    232 
    233 (*
    234 lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
    235   eval_seq_list globals p ge st (b1@b2) =
    236   ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
    237   match flow with
    238   [ Proceed ⇒
    239     ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ;
    240     return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉
    241   | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉
    242   ].
    243 [2,3,4:
    244   #lbl #H >seq_list_labels_append
    245   [1,2: @Exists_append_l | @Exists_append_r ] @H ]
    246 #globals#p#ge#st#b1 lapply st -st elim b1
    247 [ #st #b2 >m_return_bind normalize nodelta
    248   <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?);
    249   @m_bind_ext_eq **
    250   [ * #lbl #H | #id #fd #args #dest ] #st' %
    251 | #hd #tl #IH #st #b2
    252   whd in match (? @ b2);
    253   whd in match (eval_seq_list ?????);
    254   whd in match (eval_seq_list ???? (hd :: tl));
    255   >m_bind_bind
    256   @m_bind_ext_eq
    257   ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta
    258   [1,2: @m_return_bind]
    259   >m_bind_bind
    260   >IH >m_bind_bind
    261   @m_bind_ext_eq **
    262   [#lbl | #id #fd #args #dest ] #st' normalize nodelta
    263   >m_return_bind
    264   [1,2: @m_return_bind ]
    265   >m_bind_bind normalize nodelta
    266   @m_bind_ext_eq **
    267   [#lbl|#id #fd #args #dest] #st'' >m_return_bind %
    268 ]
    269 qed.
    270 
    271 lemma eval_seq_list_unbranching :
    272 ∀globals,p,ge,st,b.
    273   All ? (unbranching … ge) b →
    274   pred_io … (λ_.True) (truly_sequential …)
    275     (eval_seq_list globals p ge st b).
    276 #globals#p#ge#st #b lapply st -st elim b
    277 [ #st * %
    278 | #hd #tl #IH #st * #hd_ok #tl_ok
    279   @mp_bind
    280   [2: @(unbranching_truly_sequential … hd_ok st) |]
    281   ** [#lbl|#id#fd#args#dest] #st' *
    282   normalize nodelta
    283   @mp_bind [2: @(IH st' tl_ok)|]
    284   ** [#lbl|#id#fd#args#dest] #st'' * %
    285 ]
    286 qed.
    287 
    288 lemma io_pred_as_rel : ∀O,I,A,Perr,P,v.
    289   pred_io O I A Perr P v →
    290   rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v.
    291 #O #I #A #Perr #P #v elim v
    292 [ #o #f #IH whd in ⊢ (%→%);
    293   #H %{(refl …)} #i @IH @H
    294 |*: /2/
    295 ]
    296 qed.
    297 
    298 lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2.
    299   All ? (unbranching … ge) b1 →
    300   eval_seq_list globals p ge st (b1@b2) =
    301   ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
    302   ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ;
    303   return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉.
    304 [2: #lbl #H >seq_list_labels_append @Exists_append_r @H ]
    305 #globals #p #ge #st #b1 #b2 #H
    306 >eval_seq_list_append
    307 @mr_bind
    308 [2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |]
    309 ** [#lbl|#id#fd#args#dest] #st
    310 #y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
    311 qed.
    312 *)
    313 lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
    314   block_cont_labels p globals ty (b1 @ b2) =
    315   block_cont_labels … b1 @ block_cont_labels … b2.
    316 #p #g #ty * #l1 #s1 * #l2 #s2
    317 whd in match (〈?,?〉@?); whd in ⊢ (??%?);
    318 >seq_list_labels_append
    319 >associative_append
    320 >associative_append
    321 >associative_append %
    322 qed.
    323 (*
    324 lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
    325   ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
    326   eval_block_cont ??? ge st (b1@b2) =
    327   ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ;
    328   match ty return λx.
    329     block_cont p globals x → IO ?? ((stmt_type_if ? x  step_flow fin_step_flow ???) × ?) with
    330   [ SEQ ⇒ λb2.
    331     match flow with
    332     [ Proceed ⇒
    333       ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
    334       return 〈?, st''〉
    335     | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
    336     | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    337     ]
    338   | FIN ⇒ λb2.
    339     match flow with
    340     [ Proceed ⇒
    341       ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
    342       return 〈?, st''〉
    343     | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
    344     | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    345     ]
    346   ] b2.
    347 [3,5: whd in flow'; @flow'
    348   #lbl >block_cont_labels_append @Exists_append_r
    349 |2,4: cases l -l #l >block_cont_labels_append @Exists_append_l
    350 ]
    351 #globals#p * whd in match stmt_type_if; normalize nodelta
    352 #ge#st * #l1 #s1 * #l2 #s2
    353 whd in match (〈?,?〉@?);
    354 whd in match eval_block_cont; normalize nodelta
    355 >m_bind_bind
    356 >eval_seq_list_append
    357 >m_bind_bind
    358 @m_bind_ext_eq
    359 
    360  whd in ⊢ (??%?);
    361     match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with
    362     [ SEQ ⇒
    363     | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉
    364     ]
    365   | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    366   ].
    367 #globals#p#ty#ge#st*#l1#s1*#l2#s2
    368 whd in match (〈?,?〉@?);
    369 whd in match eval_block_cont; normalize nodelta
    370 >m_bind_bind
    371 >eval_seq_list_append
    372 >m_bind_bind
    373 @m_bind_ext_eq
    374 ** [#l|#id#fd#args#dest] normalize nodelta #st'
    375 [1,2:>m_return_bind normalize nodelta
    376   [ >m_return_bind ] % ]
    377 change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?));
    378 >m_bind_bind whd in match stmt_type_if;
    379 normalize nodelta
    380 >m_bind_bind
    381 @m_bind_ext_eq
    382 **[#l|#id#fd#args#dest] normalize nodelta #st''
    383 [1,2: >m_return_bind normalize nodelta % | % ]
    384 qed.
    385 *)
    386 
    387 
    388 (* just like repeat, but without the full_exec infrastructure, and it
    389    stops upon a non-proceed flow cmd *)
    390 let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p)
    391   (st : state_pc p) on n :
    392     IO io_out io_in (bool × (state_pc p)) ≝
    393 match n with
    394 [ O ⇒ return 〈false,st〉
    395 | S k ⇒
    396   ! 〈flag,st'〉 ← eval_state_flag globals p ge st ;
    397   if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st'
    398 ].
    399 
    400 definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝
    401 λp,g,ty,b.S (|\fst b|).
    402 
    403 interpretation "block cont size" 'norm b = (block_size ??? b).
    404 
    405 lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st.
    406   repeat_eval_state_flag (n1 + n2) globals p ge st =
    407   ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ;
    408   if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st.
    409 #n1 elim n1 -n1 [| #n1 #IH]
    410 #n2 #globals #p #ge #st
    411 [ @m_return_bind
    412 | change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
    413   change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????);
    414   >m_bind_bind in ⊢ (???%);
    415   @m_bind_ext_eq ** #st' normalize nodelta
    416   [ % | @IH ]
    417 ]
    418 qed.
    419 
    420 lemma repeat_eval_state_flag_one : ∀globals, p, ge, st.
    421   repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st.
    422 #globals #p #ge #st
    423 change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
    424 <(m_bind_return … (eval_state_flag ????)) in ⊢ (???%);
    425 @m_bind_ext_eq ** #st %
    426 qed.
    427 
    428 lemma eval_tunnel_step :
    429   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
    430   fetch_function … ge (pc … st) = OK … fn →
    431   point_of_pointer ? p … (pc … st) = OK … src →
    432   src ~~> dst in joint_if_code … fn →
    433   eval_state_flag g p ge st =
    434     return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    435 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
    436 change with (! s ← ? ; ?) in match (eval_state_flag ????);
    437 change with (! fn ← ? ; ?) in match (fetch_statement ?????);
    438 >pc_pt in ⊢ (??%?); >m_return_bind
    439 >fetch_fn in ⊢ (??%?); >m_return_bind
    440 >EQ1 in ⊢ (??%?);  >m_return_bind
    441 >EQ2 in ⊢ (??%?);
    442 change with (! st ← ? ; ?) in match (eval_statement ?????);
    443 whd in match eval_fin_step; normalize nodelta
    444 >m_return_bind
    445 whd in match eval_fin_step_flow; normalize nodelta
    446 change with (! ptr ← ? ; ?) in match (goto ??????);
    447 whd in match pointer_of_label_in_block; normalize nodelta
    448 whd in match fetch_function in fetch_fn;
    449 normalize nodelta in fetch_fn;
    450 >fetch_fn in ⊢ (??%?); >m_return_bind
    451 >EQ2 in ⊢ (??%?); >m_return_bind
    452 cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ)
    453 elim (pointer_compat_from_ind … H) %
    454 qed.
    455 
    456 lemma fetch_function_from_block_eq :
    457   ∀p,g,ge.
    458   ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
    459   fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
    460 #p #g #ge #ptr1 #ptr2 #EQ
    461 whd in match fetch_function; normalize nodelta >EQ
    462 @m_bind_ext_eq // qed.
    463 
    464 (*
    465 lemma eval_tunnel :
    466   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
    467   fetch_function … ge (pc … st) = OK … fn →
    468   point_of_pointer ? p … (pc … st) = OK … src →
    469   src ~~>^* dst in joint_if_code … fn →
    470   ∃n.repeat_eval_state n g p ge st =
    471     return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    472 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
    473 lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
    474 elim through [2: #hd #tl #IH]
    475 #st #src #fetch_fn #pc_pt
    476 [2: #EQ <EQ %{0}
    477   >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // ]
    478 * #H1 #H2
    479 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) hd) st)
    480 elim (IH st' … H2)
    481 [3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
    482   @pointer_of_point_block
    483 |2:
    484   whd in match st'; >point_of_pointer_of_point %
    485 ]
    486 #n' #EQ %{(S n')}
    487 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    488 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    489 >EQ %
    490 qed.
    491 
    492 lemma eval_tunnel_plus :
    493   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
    494   fetch_function … ge (pc … st) = OK … fn →
    495   point_of_pointer ? p … (pc … st) = OK … src →
    496   src ~~>^+ dst in joint_if_code … fn →
    497   ∃n.repeat_eval_state (S n) g p ge st =
    498     return set_pc … (pointer_of_point ? p (pc … st) dst) st.
    499 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
    500 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
    501 elim (eval_tunnel … ge st' … H2)
    502 [3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
    503   @pointer_of_point_block
    504 |2:
    505   whd in match st'; >point_of_pointer_of_point %
    506 ]
    507 #n #EQ %{n}
    508 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    509 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    510 >EQ %
    511 qed.
    512 *)
     8  ].*)
    5139
    51410lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
     
    52218>EQ1 >m_return_bind >EQ3 %
    52319qed.
    524 (*
    525 lemma eval_seq_list_in_code :
    526   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
    527   fetch_function … ge (pc … st) = OK … fn →
    528   point_of_pointer ? p … (pc … st) = OK … src →
    529   All ? (never_calls … ge) B →
    530   seq_list_in_code … (joint_if_code … fn) src B dst →
    531   repeat_eval_state_flag (|B|) g p ge st =
    532    ! 〈flow,st'〉 ← eval_seq_list g p ge st B ;
    533    match flow with
    534    [ Redirect l ⇒
    535      ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ;
    536      return 〈true, st''〉
    537    | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock)
    538        (* dummy, never happens *)
    539    | Proceed ⇒
    540      let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in
    541      return 〈false, mk_state_pc ? st' nxt_ptr〉
    542    ].
    543 #p #g #ge #st #fn #src #B lapply src -src
    544 lapply st -st elim B [|#hd #tl #IH]
    545 #st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok]
    546 [2: #EQ normalize in EQ; <EQ
    547   whd in match (eval_seq_list ???? [ ]);
    548   >m_return_bind normalize nodelta
    549   >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st //
    550 |1: * #n * #EQat #H
    551   change with (! st' ← ? ; ?) in match (eval_seq_list ?????);
    552   change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????);
    553   >m_bind_bind
    554   >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind
    555   >m_bind_bind >m_bind_bind
    556   lapply (never_calls_no_init … hd_ok st) #hd_ok'
    557   @(mr_bind …
    558     (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1))
    559   [ lapply hd_ok' elim (eval_step ?????)
    560     [ #o #f #IH'
    561       whd in ⊢ (%→%); #G
    562       %{(refl …)} #i @IH' @G
    563     |*: #v whd in ⊢ (%→%); #H
    564       % [ % ] @H
     20
     21include alias "basics/logic.ma".
     22lemma io_evaluate_bind : ∀O,I,X,Y,env.
     23∀m : IO O I X.∀f : X → IO O I Y.
     24io_evaluate O I Y env (! x ← m ; f x) =
     25! x ← io_evaluate O I X env m ;
     26io_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]
     34qed.
     35
     36lemma 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
     41whd in match fetch_function; normalize nodelta >EQ
     42@m_bind_ext_eq // qed.
     43
     44let rec repeat_eval_seq_no_pc
     45  (p : evaluation_params) env
     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 (globals p) p (ev_genv p) st hd) ;
     52    repeat_eval_seq_no_pc p env tl st'
     53  ].
     54
     55lemma 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.
     58
     59definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
     60
     61definition 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
     69lemma no_call_nor_label_proceed : ∀p : evaluation_params.
     70∀st : state p. ∀s.
     71no_call_nor_label p (globals p) s →
     72eval_seq_pc (globals p) p (ev_genv p) st s = return Proceed ???.
     73#p #st * // [ #f #args #dest | #c ] *
     74qed.
     75
     76lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
     77no_call_nor_label p (globals p) s →
     78step_classifier … s = cl_other.
     79#p * // [ #f #args #dest | #c ] *
     80qed.
     81
     82lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
     83no_call_nor_label p (globals p) s →
     84cost_label_of_stmt … (sequential … s nxt) = None ?.
     85#p * // #lbl#next *
     86qed.
     87
     88let rec produce_trace_any_any
     89  (p : evaluation_params)
     90  (st : state_pc p) fd
     91  (src : code_point p)
     92  (b : list (joint_seq p (globals p))) on b :
     93  ∀l : list (code_point p).
     94  ∀dst : code_point p.
     95  ∀st' : state p.
     96  fetch_function p ? (ev_genv p) (pc … st) = return fd →
     97  point_of_pointer p p (pc … st) = return src →
     98  if list_not_empty ? b then
     99    ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
     100  else
     101    True →
     102  src ~❨b, l❩~> dst in joint_if_code … fd →
     103  All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
     104  repeat_eval_seq_no_pc p (io_env p) b st = return st' →
     105  trace_any_any (joint_abstract_status p) st
     106    (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ≝
     107  match b
     108  return λx.?→?→?→?→?→?→?→?→?→?
     109  with
     110  [ nil ⇒
     111    λl,dst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
     112    (taa_base (joint_abstract_status p) st)
     113      ⌈trace_any_any (joint_abstract_status p) st st ↦
     114       trace_any_any (joint_abstract_status p) st
     115        (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst))⌉
     116  | cons hd tl ⇒
     117    λl.
     118    match l return λx.?→?→?→?→?→?→?→?→? with
     119    [ nil ⇒ λdst,st',fd_prf,src_prf,dst_prf,in_code.⊥
     120    | cons mid rest ⇒
     121      λdst,st',fd_prf,src_prf,dst_prf,in_code,all_other,EQ1.
     122      match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd)
     123      return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) st hd) = x → ?
     124      with
     125      [ OK st_mid ⇒ λEQ2.
     126        taa_step (joint_abstract_status p) st ?
     127          (mk_state_pc ? st' (pointer_of_point ? p (pc ? st) dst)) ???
     128          (produce_trace_any_any ?
     129            (mk_state_pc ? st_mid (pointer_of_point ? p (pc ? st) mid))
     130            fd mid tl rest dst ???????)
     131      | Error _ ⇒ λEQ2.⊥
     132      ] (refl …)
    565133    ]
    566   | ** [#lbl | #id #fd #args #dest ] #st'
    567     #y * #EQ <EQ -y * normalize nodelta @rel_io_eq
    568     whd in match succ_pc; normalize nodelta
    569     >pc_pt >m_return_bind
    570     letin src' ≝ (point_of_succ p src n) in H ⊢ %;
    571     letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H
    572     [>m_return_bind whd in match eval_step_flow; normalize nodelta
    573      whd in match (pblock ?);
    574      elim (goto … ge lbl st' ?)
    575      [ #st'' >m_return_bind %
    576      | #e %
    577      ]
    578     | normalize nodelta in IH ⊢ %; @(IH … tl_ok H)
    579       [ @fetch_fn
    580       | @point_of_pointer_of_point
     134  ].
     135  [ cases l in in_code; [2: #mid #rest *] normalize in ⊢ (%→?); #EQ
     136    cases st in src_prf EQ1; -st #st #pc
     137    #src_prf normalize in ⊢ (%→?); #EQ1 destruct
     138    >(pointer_of_point_of_pointer … src_prf) %
     139  | elim in_code
     140  |12: lapply EQ1 whd in ⊢ (??%?→?);
     141    >EQ2 normalize #ABS destruct(ABS)
     142  |*:
     143    elim in_code
     144    * #nxt * #EQ3 #EQ4 #Hrest
     145    elim all_other
     146    #hd_other #tl_other
     147    [ whd whd in match eval_state; normalize nodelta
     148      >(fetch_statement_eq … fd_prf src_prf EQ3) >m_return_bind
     149      whd in match eval_statement; normalize nodelta
     150      whd in match eval_step; normalize nodelta
     151      >m_bind_bind
     152      >(no_call_nor_label_proceed … hd_other) >m_return_bind
     153      >m_bind_bind
     154      >io_evaluate_bind >EQ2 >m_return_bind
     155      >m_return_bind
     156      whd in match succ_pc; normalize nodelta
     157      >m_bind_bind >src_prf >m_return_bind >m_return_bind
     158      whd in match eval_step_flow; normalize nodelta
     159      whd in ⊢ (??%%); >EQ4
     160      >EQ2 %
     161    | %{(sequential … hd nxt)} %{(fetch_statement_eq … fd_prf src_prf EQ3)}
     162      cases all_other #hd_other #_
     163      whd in match stmt_classifier; normalize nodelta
     164      @no_call_nor_label_other assumption
     165    | %* #H @H -H whd in ⊢ (??%?);
     166      cases tl in Hrest tl_other;
     167      [ cases rest [2: #hd' #tl' *] normalize in ⊢ (%→?); #EQ' destruct(EQ') *
     168        lapply dst_prf
     169        whd in match (as_pc_of ??);
     170        whd in match fetch_statement; normalize nodelta
     171        whd in match point_of_pointer; normalize nodelta
     172        >point_of_offset_of_point
     173        >m_return_bind
     174        >fetch_function_from_block_eq
     175        [ >fd_prf
     176          >m_return_bind
     177          cases (stmt_at ????)
     178          [ #_ %
     179          | #stmt #H @H
     180          ]
     181        | %
     182        |
     183        ]
     184      | #hd' #tl' cases rest [*] #mid' #rest' * * #next' * #EQ5 #EQ6
     185        #_ * #hd_other' #_
     186        >fetch_statement_eq try assumption
     187        [ @no_call_nor_label_uncosted assumption
     188        | whd in match (as_pc_of ??);
     189          whd in ⊢ (??%?);
     190          >point_of_offset_of_point %
     191        ]
    581192      ]
     193    | change with (! x ← ?;?) in EQ1 : (??%?);
     194      >EQ2 in EQ1; #H @H
     195    | assumption
     196    | assumption
     197    | cases (list_not_empty ??) [ assumption | % ]
     198    | @point_of_pointer_of_point
     199    | <fd_prf @fetch_function_from_block_eq %
    582200    ]
    583201  ]
    584 ]
    585 qed.
    586 
    587 definition eval_block_cont_pc :
    588   ∀globals.∀p : sem_params.∀ty.genv globals p →
    589   state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit →
    590   IO io_out io_in (bool × (state_pc p)) ≝
    591   λglobals,p,ty,ge,st,b,nxt.
    592   ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ;
    593   match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with
    594   [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st'
    595         (pointer_of_point ? p (pc ? st) nxt) flow
    596   | FIN ⇒ λflow.λ_.
    597     ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ;
    598     return 〈true, st'〉
    599   ] flow nxt.
    600 
    601 lemma eval_block_cont_in_code :
    602   ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
    603   fetch_function … ge (pc … st) = OK … fn →
    604   point_of_pointer ? p … (pc … st) = OK … src →
    605   All ? (never_calls … ge) (\fst B) →
    606   src ~❨B❩~> dst in joint_if_code … fn →
    607   repeat_eval_state_flag (|B|) g p ge st =
    608     eval_block_cont_pc g p ty ge st B dst.
    609 #p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok
    610 * #mid * #l_in_code #s_in_code
    611 change with (1 + |l|) in match (|?|);
    612 >commutative_plus
    613 >repeat_eval_state_flag_plus
    614 change with (! x ← ? ; ?) in ⊢ (???%);
    615 >m_bind_bind
    616 >(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code)
    617 >m_bind_bind
    618 @m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st'
    619 normalize nodelta
    620 [ -s_in_code lapply dst -dst cases ty
    621   whd in match stmt_type_if; normalize nodelta
    622   #dst >m_return_bind
    623   [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ]
    624   normalize nodelta
    625   whd in match (pblock ?);
    626   elim (goto g p ge lbl st' ?) #x //
    627 | %
    628 | >m_return_bind normalize nodelta
    629   >repeat_eval_state_flag_one
    630   >m_bind_bind
    631   lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty
    632   whd in match stmt_type_if; normalize nodelta
    633   #s #dst [* #n * ] #s_in_code [ #n_is_dst ]
    634   whd in match eval_state_flag; normalize nodelta
    635   letin pc' ≝ (pointer_of_point p p (pc ? st) mid)
    636   letin st_pc' ≝ (mk_state_pc ? st' pc')
    637   >(fetch_statement_eq … ?? s_in_code)
    638   [2,5: @point_of_pointer_of_point
    639   |3,6: @fetch_fn
    640   |*: >m_return_bind
    641     whd in match eval_statement; normalize nodelta
    642     @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%]
    643     whd in match succ_pc; normalize nodelta
    644     >point_of_pointer_of_point >m_return_bind
    645     >pointer_of_point_of_pointer [2: @refl |*:]
    646     [ >point_of_pointer_of_point >n_is_dst %
    647     | %
    648     ]
    649   ]
    650 ]
    651 qed.
    652      cases dst [*] #z @eval_tunnel assumption
    653 | cases dst [2: #z *]]
    654 * #mid * #tunn [#H | * #n * #H #G ]
    655   elim (eval_tunnel … fetch_fn pc_pt tunn)
    656   #n
    657   letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
    658   #EQ1
    659   cut (point_of_pointer ? p … (pc … st') = OK … mid)
    660   [1,3:
    661     whd in match st'; >point_of_pointer_of_point % ] #pc_pt'
    662   cut (fetch_function p … ge (pc … st') = OK … fn)
    663   [1,3: >fetch_function_from_block_eq [1,4:@fetch_fn |*:] whd in match st';
    664     @pointer_of_point_block] #fetch_fn'
    665   [ %{(n + 1)}
    666   >repeat_eval_state_plus >EQ1 >m_return_bind
    667   >repeat_eval_state_one change with (None ?) in match (! x ← None ? ; ?);
    668   change with (! 〈flow,tr,st〉 ← ? ; ?) in match (eval_block_cont ??????);
    669   change with (! s ← ? ; ?) in match (eval_state ????);
    670   >(fetch_statement_eq … fetch_fn' pc_pt' H) >m_return_bind
    671   >m_bind_bind
    672   change with ( ! x ← ? ; ?) in match (eval_block_cont ???????);
    673   cases s *
    674  
    675   @m_bind_ext_eq' ** #flow #tr1 #st1 normalize nodelta
    676   >m_bind_bind change with st' in match (set_pc ???); @m_bind_ext_eq
    677   change with (! fn ← ? ; ?) in match (fetch_statement ?????);
    678   >m_bind_bind in ⊢ (??%?);
    679   change with (pointer_of_point ????) in match (pc ??);
    680   >point_of_pointer_of_point >m_return_bind
    681   >(fetch_function_from_block_eq ???? (pc … st))
    682   [2: @pointer_of_point_block ]
    683   >fetch_fn >m_return_bind >H2 >m_return_bind
    684   >m_bind_bind
    685   change with (! x ← ? ; ?) in ⊢ (???%);
    686   >fetch_fn n ⊢ (??(????%?)?); >m_return_bind
    687   >(stmt_at_to_safe … src_prf) in ⊢ (??(????%?)?);
    688   >H1 in ⊢ (??(????%?)?);
    689   whd in ⊢ (??(λ_.???%));
    690 elim b
    691 [ #st #dst #fetch_fn #prf #through
    692   #H elim (block_cont_to_tunnel … H) #dst'
    693   * #EQdst >EQdst >m_return_bind #G
    694   elim (eval_tunnel … fetch_fn prf … G) #x #EQ %{x}
    695   >EQ %
    696 |
    697 
    698  #dst #fetch_fn #prf #through
    699 lapply prf -prf lapply fetch_fn -fetch_fn
    700 lapply b -b lapply st -st
    701 elim through [2: #hd #tl #IH]
    702 [2:
    703  
    704 #st * [1,4,7,10:|2,5,8,11:#s|3,6,9,12:#s#b'] #fetch_fn #prf
    705 normalize in ⊢(%→?);
    706 [8: #EQ1 |*: * [5: |*: *] #lbl [ |*: *] * #H1 #H2 [|*: #H3] #x [ *
    707 [ * || * | * #lbl
    708  * #lbl * [*] #H1 #H2 [#H3]
    709  
    710 let rec block_cont_in_code (p : sem_params) g (b : block_cont p g)
    711   (following : option (succ p)) (c : codeT p g) (at : cpointer) on b : Prop ≝
    712   match b with
    713   [ Skip ⇒
    714     match following with
    715     [ Some l ⇒ succ_pc p p
    716 *)
     202qed.
  • src/joint/semantics_paolo.ma

    r1999 r2186  
    1616definition xpointer ≝ Σp.ptype p = XData.
    1717unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
    18 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).
     18unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
    1919
    2020record sem_state_params : Type[1] ≝
     
    8686 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    8787
    88 inductive step_flow (p : params) (globals : list ident) (labels : list label) : Type[0] ≝
    89   | Redirect : (Σl.In ? labels l) → step_flow p globals labels (* used for goto-like flow alteration *)
    90   | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals labels (* call a function with given id, then proceed *)
    91   | Proceed  : step_flow p globals labels. (* go to implicit successor *)
    92 
     88inductive step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
     89  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p globals (Labels lbls) (* used for goto-like flow alteration *)
     90  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals Call (* call a function with given id, then proceed *)
     91  | Proceed  : ∀flows.step_flow p globals flows. (* go to implicit successor *)
     92
     93(*
    9394definition step_flow_cons : ∀p,globals,l,lbls.
    9495  step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
     
    120121coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
    121122  step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).
    122 
    123 inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
    124   | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
    125   | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
    126   | FEnd  : fin_step_flow p globals labels. (* end flow *)
    127 
     123*)
     124
     125inductive fin_step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
     126  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p globals (Labels lbls)
     127  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals Call
     128  | FEnd1  : fin_step_flow p globals (Labels [ ]) (* end flow *)
     129  | FEnd2  : fin_step_flow p globals Call. (* end flow *)
     130
     131(*
    128132definition fin_step_flow_cons : ∀p,globals,l,lbls.
    129133  fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
     
    155159coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
    156160  fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
     161*)
    157162
    158163record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
     
    230235   serialization and on whether the call is a tail one. *)
    231236definition eval_call_block:
    232  ∀globals.∀p : params.∀p':more_sem_unserialized_params p.∀lbls.
     237 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
    233238  genv globals p → state p' → block → call_args p → call_dest p →
    234     IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝
    235  λglobals,p,p',lbls,ge,st,b,args,dest.
     239    IO io_out io_in ((step_flow p globals Call)×(state p')) ≝
     240 λglobals,p,p',ge,st,b,args,dest.
    236241  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge b) : IO ? io_in ?);
    237242    match fd with
     
    258263  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
    259264  return set_m … m (set_isp … isp'' st).
    260   normalize elim (isp p st) //
     265  normalize elim (isp p st) #p #H @H
    261266qed.
    262267
     
    268273  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
    269274  OK ? 〈ist,v〉.
    270   normalize elim (isp p st) //
     275  normalize elim (isp p st) #p #H @H
    271276qed.
    272277 
     
    290295  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    291296  (* change of pc must be left to *_flow execution *)
    292   ; exec_extended: ∀globals.genv globals pp → ∀s : ext_step pp.
     297  ; eval_ext_seq: ∀globals.genv globals pp → ext_seq pp →
     298      state msu_pars → IO io_out io_in (state msu_pars)
     299  ; eval_ext_tailcall : ∀globals.genv globals pp → ext_tailcall pp →
     300      state msu_pars → IO io_out io_in ((fin_step_flow pp globals Call)×(state msu_pars))
     301  ; eval_ext_call: ∀globals.genv globals pp →∀s : ext_call pp.
    293302      state msu_pars →
    294       IO io_out io_in ((step_flow pp globals (ext_step_labels … s))× (state msu_pars))
    295   ; exec_fin_extended: ∀globals.genv globals pp → ∀s : ext_fin_stmt pp.
    296       state msu_pars →
    297       IO io_out io_in ((fin_step_flow pp globals (ext_fin_stmt_labels … s))×(state msu_pars))
     303      IO io_out io_in ((step_flow pp globals Call)×(state msu_pars))
    298304  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    299305  }.
     
    311317  cpointer→ code_point p → cpointer ≝
    312318  λp,msp,ptr,pt.
    313     mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
    314 [ elim ptr #ptr' #EQ <EQ @pok
    315 | %] qed.
     319    mk_pointer (pblock ptr) (offset_of_point p msp pt).
     320elim ptr #ptr' #EQ <EQ % qed.
    316321
    317322axiom BadOffsetForCodePoint : String.
     
    335340lemma pointer_of_point_uses_block :
    336341  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
    337 #p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
    338         ** #ty2 #bl2 #H2 #o2 #EQ2
     342#p #msp ** #b1 #o1 #EQ1
     343        ** #b2 #o2 #EQ2
    339344#pt #EQ3 destruct normalize //
    340345qed.
     
    344349    pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
    345350    pointer_of_point p msp ptr2 pt = ptr1.
    346 #p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
    347         ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
     351#p #msp ** #b1 #o1 #EQ1
     352        ** #b2 #o2 #EQ2
     353#pt #EQ3
    348354destruct
    349355lapply (offset_of_point_of_offset p msp o1)
     
    365371  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
    366372 
    367 definition pointer_of_label_in_block : ∀p : params.∀ msp : more_sem_params p.∀globals.
    368   genv globals p → block → label → res cpointer ≝
    369   λp,msp,globals,ge,b,lbl.
    370   ! fn ← function_of_block … ge b ;
     373definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     374  genv globals p → cpointer → label → res cpointer ≝
     375  λp,msp,globals,ge,ptr,lbl.
     376  ! fn ← fetch_function … ge ptr ;
    371377  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    372378            (point_of_label … (joint_if_code … fn) lbl) ;
    373   return (mk_pointer Code (mk_block Code (block_id b)) ? (offset_of_point p msp pt) : Σp.?). // qed.
    374 
    375 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    376   genv globals p → cpointer → label → res cpointer ≝
    377   λp,msp,globals,ge,ptr.
    378   pointer_of_label_in_block p msp globals ge (pblock ptr).
     379  return (mk_pointer(mk_block Code (block_id (pblock ptr)))
     380    (offset_of_point p msp pt) : Σp.?). // qed.
    379381
    380382definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     
    396398
    397399definition goto: ∀globals. ∀p:sem_params.
    398   genv globals p → label → state p → block → res (state_pc p) ≝
     400  genv globals p → label → state p → cpointer → res (state_pc p) ≝
    399401 λglobals,p,ge,l,st,b.
    400   ! newpc ← pointer_of_label_in_block ? p … ge b l ;
     402  ! newpc ← pointer_of_label ? p … ge b l ;
    401403  return mk_state_pc ? st newpc.
    402404
     
    416418axiom SuccessorNotProvided : String.
    417419
    418 (* the optional point must be given only for calls *)
    419 definition eval_step :
     420definition eval_seq_no_pc :
    420421 ∀globals.∀p:sem_params. genv globals p → state p →
    421   ∀s:joint_step p globals.
    422   IO io_out io_in ((step_flow p globals (step_labels … s))×(state p)) ≝
     422  ∀s:joint_seq p globals.
     423  IO io_out io_in (state p) ≝
    423424 λglobals,p,ge,st,seq.
    424   match seq return λx.IO ?? ((step_flow ?? (step_labels … x) × ?)) with
    425   [ extension c ⇒
    426     exec_extended … ge c st
    427   | COST_LABEL cl ⇒
    428     return 〈Proceed ???, st〉
    429   | COMMENT c ⇒
    430     return 〈Proceed ???, st〉
     425  match seq return λx.IO ??? with
     426  [ extension_seq c ⇒
     427    eval_ext_seq ??? ge c st
    431428  | LOAD dst addrl addrh ⇒
    432429    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    434431    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    435432    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    436     ! st ← acca_store p … dst v st ;
    437     return 〈Proceed ???, st〉
     433    acca_store p … dst v st
    438434  | STORE addrl addrh src ⇒
    439435    ! vaddrh ← dph_arg_retrieve … st addrh;
     
    442438    ! v ← acca_arg_retrieve … st src;
    443439    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    444     return 〈Proceed ???, set_m … m' st〉
    445   | COND src ltrue ⇒
    446     ! v ← acca_retrieve … st src;
    447     ! b ← bool_of_beval v;
    448     if b then
    449       return 〈Redirect ??? ltrue, st〉
    450     else
    451       return 〈Proceed ???, st〉
     440    return set_m … m' st
    452441  | ADDRESS ident prf ldest hdest ⇒
    453442    let addr ≝ opt_safe ? (find_symbol … ge ident) ? in
    454     ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
     443    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
    455444    ! st' ← dpl_store … ldest laddr st;
    456     ! st'' ← dph_store … hdest haddr st';
    457     return 〈Proceed ???, st''〉
     445    dph_store … hdest haddr st'
    458446  | OP1 op dacc_a sacc_a ⇒
    459447    ! v ← acca_retrieve … st sacc_a;
    460448    ! v ← Byte_of_val v;
    461449    let v' ≝ BVByte (op1 eval op v) in
    462     ! st ← acca_store … dacc_a v' st;
    463     return 〈Proceed ???, st〉
     450    acca_store … dacc_a v' st
    464451  | OP2 op dacc_a sacc_a src ⇒
    465452    ! v1 ← acca_arg_retrieve … st sacc_a;
     
    472459      let carry ≝ beval_of_bool carry in
    473460    ! st' ← acca_store … dacc_a v' st;
    474       let st'' ≝ set_carry … carry st' in
    475     return 〈Proceed ???, st''〉
     461    return set_carry … carry st'
    476462  | CLEAR_CARRY ⇒
    477     let st' ≝ set_carry … BVfalse st in
    478     return 〈Proceed ???, st'〉
     463    return set_carry … BVfalse st
    479464  | SET_CARRY ⇒
    480     let st' ≝ set_carry … BVtrue st in
    481     return 〈Proceed ???, st'〉
     465    return set_carry … BVtrue st
    482466  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    483467    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     
    489473    let v2' ≝ BVByte v2' in
    490474    ! st' ← acca_store … dacc_a_reg v1' st;
    491     ! st'' ← accb_store … dacc_b_reg v2' st';
    492     return 〈Proceed ???, st''〉
     475    accb_store … dacc_b_reg v2' st'
    493476  | POP dst ⇒
    494477    ! 〈st',v〉 ← pop p st;
    495     ! st'' ← acca_store p p dst v st';
    496     return 〈Proceed ???, st''〉
     478    acca_store p p dst v st'
    497479  | PUSH src ⇒
    498480    ! v ← acca_arg_retrieve … st src;
    499     ! st ← push … st v;
    500     return 〈Proceed ???, st〉
     481    push … st v
    501482  | MOVE dst_src ⇒
    502     ! st ← pair_reg_move … st dst_src ;
    503     return 〈Proceed ???, st〉
     483    pair_reg_move … st dst_src
    504484  | CALL_ID id args dest ⇒
    505485    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    506     eval_call_block … ge st b args dest
     486    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
     487    return st'
     488  | extension_call s ⇒
     489    !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
     490    return st'
     491  | _ ⇒ return st
    507492  ].
    508   [ cases addr //
    509   | (* TODO: to prove *)
    510     elim daemon
    511   | %1 %
    512   ] qed.
    513 
    514 definition eval_fin_step : ∀globals: list ident.∀p:sem_params. genv globals p →
    515   state p → ∀s : joint_fin_step … p globals.
    516   IO io_out io_in ((fin_step_flow p globals (fin_step_labels … s))×(state p)) ≝
     493  (* TODO: to prove *)
     494  elim daemon
     495  qed.
     496
     497definition eval_seq_pc :
     498 ∀globals.∀p:sem_params. genv globals p → state p →
     499  ∀s:joint_seq p globals.
     500  IO io_out io_in (step_flow p globals (step_flows … s)) ≝
     501  λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
     502  [ CALL_ID id args dest ⇒
     503    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     504    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
     505    return flow
     506  | extension_call s ⇒
     507    !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
     508    return flow
     509  | _ ⇒ return Proceed ???
     510  ].
     511
     512definition eval_step :
     513 ∀globals.∀p:sem_params. genv globals p → state p →
     514  ∀s:joint_step p globals.
     515  IO io_out io_in ((step_flow p globals (step_flows … s))×(state p)) ≝
     516  λglobals,p,ge,st,s.
     517  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
     518  [ step_seq s ⇒
     519    ! flow ← eval_seq_pc ?? ge st s ;
     520    ! st' ← eval_seq_no_pc ?? ge st s ;
     521    return 〈flow,st'〉
     522  | COND src ltrue ⇒
     523    ! v ← acca_retrieve … st src;
     524    ! b ← bool_of_beval v;
     525    if b then
     526      return 〈Redirect ??? ltrue, st〉
     527    else
     528      return 〈Proceed ???, st〉
     529  ].
     530  %1 % qed.
     531
     532definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv globals p →
     533  state p → ∀s : joint_fin_step p.
     534  IO io_out io_in (state p) ≝
    517535 λglobals,p,ge,st,s.
    518   match s return λx.IO ?? ((fin_step_flow ?? (fin_step_labels … x)) × ?) with
    519     [ GOTO l ⇒ return 〈FRedirect ??? l, st〉
    520     | RETURN ⇒ return 〈FEnd ???, st〉
    521     | extension_fin c ⇒ exec_fin_extended … ge c st
    522     ]. %1 % qed.
    523 
     536  match s return λx.IO ??? with
     537    [ tailcall c ⇒
     538      !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
     539      return st'
     540    | _ ⇒ return st
     541    ].
     542
     543definition eval_fin_step_pc :
     544 ∀globals.∀p:sem_params. genv globals p → state p →
     545  ∀s:joint_fin_step p.
     546  IO io_out io_in (fin_step_flow p globals (fin_step_flows … s)) ≝
     547  λg,p,ge,st,s.
     548  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
     549  [ tailcall c ⇒
     550    !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
     551    return flow 
     552  | GOTO l ⇒ return FRedirect … l
     553  | RETURN ⇒ return FEnd1 ??
     554  ]. %1 % qed.
    524555
    525556definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
     
    532563    let l' ≝ joint_if_entry … fn in
    533564    let st' ≝ set_regs p regs st in
    534     let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in
     565    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
    535566    let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
    536567    return mk_state_pc ? st' pc. % qed.
    537568
    538 (* The pointer provided is the one to the *next* instruction.
    539    The boolean tells wether a flow changement has occurred (i.e.
    540    a non Proceed cmd was issued). Used in linking block evaluation
    541    with regular one *)
     569(* The pointer provided is the one to the *next* instruction. *)
    542570definition eval_step_flow :
    543  ∀globals.∀p:sem_params.∀lbls.genv globals p →
    544   state p → cpointer → step_flow p globals lbls →
    545     res (bool × (state_pc p)) ≝
    546  λglobals,p,lbls,ge,st,nxt,cmd.
     571 ∀globals.∀p:sem_params.∀flows.genv globals p →
     572 state p → cpointer → step_flow p globals flows → res (state_pc p) ≝
     573 λglobals,p,flows,ge,st,nxt,cmd.
    547574 match cmd with
    548   [ Redirect l ⇒
    549     ! st ← goto … ge l st (pblock nxt) ; return 〈true, st〉
     575  [ Redirect _ l ⇒
     576    goto … ge l st nxt
    550577  | Init id fn args dest ⇒
    551578    let st' ≝ set_frms … (save_frame … nxt dest st) st in
    552     ! st ← do_call ?? ge st' id fn args ;
    553     return 〈true, st〉
    554   | Proceed ⇒
    555     return 〈false, mk_state_pc ? st nxt〉
     579    do_call ?? ge st' id fn args
     580  | Proceed _ ⇒
     581    return mk_state_pc ? st nxt
    556582  ].
    557583
    558 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀lbls. genv globals p →
    559   state p → block → fin_step_flow p globals lbls → res (state_pc p) ≝
    560   λglobals,p,lbls,ge,st,b,cmd.
     584definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv globals p →
     585  state p → cpointer → fin_step_flow p globals flows → res (state_pc p) ≝
     586  λglobals,p,lbls,ge,st,curr,cmd.
    561587  match cmd with
    562   [ FRedirect l ⇒ goto … ge l st b
     588  [ FRedirect _ l ⇒ goto … ge l st curr
    563589  | FTailInit id fn args ⇒
    564590    do_call … ge st id fn args
    565   | FEnd
     591  | _
    566592    ! 〈st',ra〉 ← fetch_ra … st ;
    567593    ! st'' ← pop_frame … ge st;
     
    572598 ∀globals.∀p:sem_params.genv globals p →
    573599  state_pc p → joint_statement p globals →
    574     IO io_out io_in (bool × (state_pc p)) ≝
     600    IO io_out io_in (state_pc p) ≝
    575601 λglobals,p,ge,st,stmt.
    576602 match stmt with
    577603 [ sequential s nxt ⇒
    578    ! 〈flow, st'〉 ← eval_step … ge st s ;
     604   ! 〈flow,st'〉 ← eval_step … ge st s ;
    579605   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
    580606   eval_step_flow … ge st' nxtptr flow
    581607 | final s ⇒
    582    ! 〈flow, st'〉 ← eval_fin_step … ge st s ;
    583    ! st ← eval_fin_step_flow … ge st' (pblock … (pc … st)) flow ;
    584    return 〈true, st〉
     608   ! st' ← eval_fin_step_no_pc … ge st s ;
     609   ! flow ← eval_fin_step_pc … ge st s ;
     610   eval_fin_step_flow … ge st' (pc … st) flow
    585611 ].
    586612
    587 definition eval_state_flag : ∀globals: list ident.∀p:sem_params. genv globals p →
    588   state_pc p → IO io_out io_in (bool × (state_pc p)) ≝
     613definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
     614  state_pc p → IO io_out io_in (state_pc p) ≝
    589615  λglobals,p,ge,st.
    590616  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
    591617  eval_statement … ge st s.
    592 
    593 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
    594   state_pc p → IO io_out io_in (state_pc p) ≝
    595   λglobals,p,ge,st.
    596   ! 〈flag,st'〉 ← eval_state_flag … ge st ;
    597   return st'.
    598618
    599619(* Paolo: what if in an intermediate language main finishes with an external
     
    618638 | _ ⇒ Error ? [ ]
    619639 ]).
    620  
     640
     641(*
    621642record evaluation_parameters : Type[1] ≝
    622643 { globals: list ident
     
    681702 ∀pars:sem_params.fullexec io_out io_in ≝
    682703 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
     704*)
Note: See TracChangeset for help on using the changeset viewer.