Changeset 2457 for src/common


Ignore:
Timestamp:
Nov 13, 2012, 11:30:23 AM (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?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2436 r2457  
    3131     necessary for as_after_return (typically just the program counter)
    3232     maybe what function is called too? *)
    33   ; call_rel : (Σs.as_classifier S1 s cl_call) →
    34                (Σs.as_classifier S2 s cl_call) → Prop
     33  ; ret_rel : S1 → S2 → Prop
    3534  ; sim_final :
    3635    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
     
    4847definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
    4948
    50 definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2.
    51   ∀s1_pre,s2_pre.call_rel … R s1_pre s2_pre →
    52                  as_after_return S1 s1_pre s1 →
    53                  as_after_return S2 s2_pre s2.
     49definition call_rel ≝ λS1,S2.λR : status_rel S1 S2.
     50  λs1_pre,s2_pre.
     51  ∀s1_ret,s2_ret.as_after_return S1 s1_pre s1_ret →
     52                 ret_rel ?? R s1_ret s2_ret →
     53                 as_after_return S2 s2_pre s2_ret.
    5454
    5555(* the equivalent of a collapsable trace_any_label where we do not force
     
    7070   S will mark semantic relation, C call relation, L label relation, R return relation *)
    7171
    72 record status_simulation
    73   (S1 : abstract_status)
    74   (S2 : abstract_status)
    75   : Type[1] ≝
    76   { sim_status_rel :> status_rel S1 S2
    77   ; sim_execute :
     72definition status_simulation ≝
     73  λS1 : abstract_status.
     74  λS2 : abstract_status.
     75  λsim_status_rel : status_rel S1 S2.
    7876    ∀st1,cl,st1',st2.as_execute S1 st1 st1' →
    7977    sim_status_rel st1 st2 →
     
    141139      sim_status_rel st1' st2' ∧
    142140      label_rel … st1' st2'
    143     ] prf
    144   }.
     141    ] prf.
    145142
    146143
     
    287284include alias "basics/logic.ma".
    288285
    289 let rec status_simulation_produce_tlr S1 S2 (R : status_simulation S1 S2)
     286let rec status_simulation_produce_tlr S1 S2 R
    290287(* we start from this situation
    291288     st1 →→→→tlr→→→→ st1'
     
    306303  (tlr1 : trace_label_return S1 st1 st1')
    307304  (taa2_pre : trace_any_any S2 st2_lab st2)
     305  (sim_execute : status_simulation S1 S2 R)
    308306  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
    309307  ∃st2_mid.∃st2'.
     
    317315 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
    318316 ]
    319 and status_simulation_produce_tll S1 S2 (R : status_simulation S1 S2)
     317and status_simulation_produce_tll S1 S2 R
    320318(* we start from this situation
    321319     st1 →→→→tll→→→ st1'
     
    336334  (tll1 : trace_label_label S1 fl st1 st1')
    337335  (taa2_pre : trace_any_any S2 st2_lab st2)
    338   on tll1 : R st1 st2 → label_rel … st1 st2_lab →
     336  (sim_execute : status_simulation S1 S2 R)
     337   on tll1 : R st1 st2 → label_rel … st1 st2_lab →
    339338    match fl with
    340339    [ ends_with_ret ⇒
     
    352351  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
    353352  ]
    354 and status_simulation_produce_tal S1 S2 (R : status_simulation S1 S2)
     353and status_simulation_produce_tal S1 S2 R
    355354(* we start from this situation
    356355     st1 →→tal→→ st1'
     
    380379  fl st1 st1' st2
    381380  (tal1 : trace_any_label S1 fl st1 st1')
    382   on tal1 : R st1 st2 →
     381  (sim_execute : status_simulation S1 S2 R)
     382   on tal1 : R st1 st2 →
    383383    match fl with
    384384    [ ends_with_ret ⇒
     
    405405[1,2,3: #st1_L_st2_lab ]
    406406[ (* tlr_base *)
    407   elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
     407  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
    408408  #st2_mid * #st2' * #tll2 #H
    409409  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
    410410| (* tlr_step *)
    411   elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
     411  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
    412412  #st2_mid * #tll2 ** #H1 #H2 #H3
    413   elim (status_simulation_produce_tlr … tl1 (taa_base …) H1 H2)
     413  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
    414414  #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
    415415  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
    416416  %{H4} %{H3 H5}
    417417| (* tll_base *)
    418   lapply (status_simulation_produce_tal ?? R ??? st2 tal1 st1_R_st2)
     418  lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
    419419  cases fl1' in tal1; normalize nodelta #tal1 *
    420420  [3: * #_ #ABS elim (absurd … H ABS) ]
     
    431431| (* tal_base_non_return *) whd
    432432  cases G #G'
    433   elim (sim_execute … R … H st1_R_st2 G')
     433  elim (sim_execute … H st1_R_st2 G')
    434434  #st2' ** -st2 -st2'
    435435  [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
     
    445445  ]
    446446| (* tal_base_return *) whd
    447   elim (sim_execute … R … H st1_R_st2 G)
     447  elim (sim_execute … H st1_R_st2 G)
    448448  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    449449  ***** #ncost #J2 #K2
     
    453453  %[ % | %[|%[|%[|%[| % ]]]]]]]
    454454| (* tal_base_call *) whd
    455   elim (sim_execute … R … H st1_R_st2 G)
     455  elim (sim_execute … H st1_R_st2 G)
    456456  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    457457  #st1_R_st2_mid #st1_L_st2_after_call
    458   elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
     458  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
    459459  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
    460460  [ #st2' #tlr2 *****
     
    474474    ]
    475475  ]
    476   [1,3: @(st1_Rret_st2' … st1_C_st2) assumption
     476  [1,3: @(st1_C_st2 … st1_Rret_st2') assumption
    477477  |*: whd <st1_L_st2' assumption
    478478  ]
    479479| (* tal_step_call *)
    480   elim (sim_execute … R … H st1_R_st2 G)
     480  elim (sim_execute … H st1_R_st2 G)
    481481  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
    482482  #st1_R_st2_mid #st1_L_st2_after_call
    483   elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
     483  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
    484484  #st2_after_ret * #st2' * #tlr2 * #taa2''
    485485  ****
    486486  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
    487   lapply (status_simulation_produce_tal … tl1 st1_R_st2')
     487  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
    488488  cases fl1' in tl1; #tl1 *
    489489  [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
     
    514514    ]
    515515  ]
    516   [1,4,7,9: @(st1_Rret_st2' … st1_C_st2) assumption
     516  [1,4,7,9: @(st1_C_st2 … st1_Rret_st2') assumption
    517517  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
    518518    [1,3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
     
    523523  ]
    524524| (* step_default *)
    525   elim (sim_execute … R … H st1_R_st2 G)
     525  elim (sim_execute … H st1_R_st2 G)
    526526  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    527   lapply (status_simulation_produce_tal … tl1 st1_R_st2_mid)
     527  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
    528528  cases fl1' in tl1; #tl1 *
    529529  [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
     
    728728*)
    729729  ∀S1,S2.
    730   ∀R : status_simulation S1 S2.
     730  ∀R.
    731731  ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
    732   label_rel … st1 st2 → R st1 st2 →
     732  status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
    733733  ∃st2_lab,st2'.
    734734  ∃ft2 : flat_trace S2 st2 st2_lab stack.
    735735  ∃taa : trace_any_any S2 st2_lab st2'.
    736736  label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
    737 #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #H #G elim ft1 -st1' -stack
     737#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
    738738[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
    739739|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
Note: See TracChangeset for help on using the changeset viewer.