Changeset 3007


Ignore:
Timestamp:
Mar 28, 2013, 2:59:43 PM (4 years ago)
Author:
campbell
Message:

Sketch out how Cminor to RTLabs correctness would fit into the
front-end measurable traces proof.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/Cminor_abstract.ma

    r2737 r3007  
    4242definition CmCallstate ≝ Callstate.
    4343
     44lemma Cminor_notailcalls : ∀s. Cminor_classify s ≠ cl_tailcall.
     45* #a try #b try #c try #d try #e try #f try #g try #h try #i try #j
     46normalize % #E destruct
     47qed.
  • src/Cminor/toRTLabsCorrectness.ma

    r2601 r3007  
    44include "Cminor/toRTLabs.ma".
    55
    6 record cminor_rtlabs_inv : Type[0] ≝ {
    7   ge_cm : cm_genv;
    8   ge_ra : RTLabs_genv
     6record cminor_rtlabs_inv (ge_cm:cm_genv) (ge_ra:RTLabs_genv) : Type[0] ≝ {
    97}.
    10 axiom cminor_rtlabs_rel : cminor_rtlabs_inv → Cminor_state → RTLabs_state → Prop.
     8axiom cminor_rtlabs_rel : ∀gc,gr. cminor_rtlabs_inv gc gr → Cminor_state → RTLabs_state → Prop.
     9
     10axiom cminor_rtlabs_rel_labelled : ∀gc,gr,INV,s,s'.
     11  cminor_rtlabs_rel gc gr INV s s' →
     12  Cminor_labelled s = RTLabs_cost s'.
    1113
    1214(* Conjectured simulation results
     
    1416   We split these based on the start state:
    1517   
    16    1. ‘normal’ states take some [S n] normal steps and simulates them by [m]
    17       normal steps in RTLabs ([m] can be zero if the Cminor program executed an
    18       St_skip);
    19    2. call and return steps are simulated by a call/return step plus [m] normal
    20       steps (to copy stack allocated parameters / results); and
     18   1. from a ‘normal’ state we simulate a step by [n] normal steps in RTLabs
     19      ([n] can be zero if the Cminor program executed an St_skip);
     20   2. call and return state steps are simulated by a call/return state step (we
     21      don't add anything extra in this stage, it happens in Clight to Cminor);
     22      and
    2123   3. lone cost label steps are simulates by a lone cost label step
     24
     25   Most of the work in this stage is splitting the execution of complex Cminor
     26   statements into individual RTLabs steps.  This doesn't contradict 2 above -
     27   the expansion of function parameters, return expressions, etc is done for
     28   the function call / return *statement*, whereas the call / return *state* is
     29   a Callstate / Returnstate that is the second half of the operation.
    2230
    2331   Note that we'll need something more to show that non-termination is
     
    3644λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
    3745
     46axiom cminor_measure : Cminor_state → nat.
     47
    3848axiom cminor_rtlabs_normal :
    39   ∀INV:cminor_rtlabs_inv.
     49  ∀ge_cm,ge_ra.
     50  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
    4051  ∀s1,s1',s2,tr.
    41   cminor_rtlabs_rel INV s1 s1' →
     52  cminor_rtlabs_rel INV s1 s1' →
    4253  cminor_normal s1 →
    4354  ¬ Cminor_labelled s1 →
    44   ∃n. after_n_steps (S n) … Cminor_exec (ge_cm INV) s1 (λs.cminor_normal s ∧ ¬ Cminor_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉)
    45   ∃m. after_n_steps m … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'.
     55  step ?? Cminor_exec ge_cm s1 = Value … 〈tr,s2〉
     56  ∃n. after_n_steps n … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
    4657    tr = tr' ∧
    47     cminor_rtlabs_rel INV s2 s2'
     58    (n = 0 → lt (cminor_measure s2) (cminor_measure s1)) ∧
     59    cminor_rtlabs_rel … INV s2 s2'
    4860  ).
    4961
    5062axiom cminor_rtlabs_call_return :
    51   ∀INV:cminor_rtlabs_inv.
     63  ∀ge_cm,ge_ra.
     64  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
    5265  ∀s1,s1',s2,tr.
    53   cminor_rtlabs_rel INV s1 s1' →
     66  cminor_rtlabs_rel INV s1 s1' →
    5467  match Cminor_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
    55   after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉)
    56   ∃m. after_n_steps (S m) … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'.
     68  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉
     69  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
    5770    tr = tr' ∧
    58     cminor_rtlabs_rel INV s2 s2'
     71    cminor_rtlabs_rel INV s2 s2'
    5972  ).
    6073
    6174axiom cminor_rtlabs_cost :
    62   ∀INV:cminor_rtlabs_inv.
     75  ∀ge_cm,ge_ra.
     76  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
    6377  ∀s1,s1',s2,tr.
    64   cminor_rtlabs_rel INV s1 s1' →
     78  cminor_rtlabs_rel INV s1 s1' →
    6579  Cminor_labelled s1 →
    66   after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉)
    67   after_n_steps 1 … RTLabs_exec (ge_ra INV) s1' (λs.true) (λtr',s2'.
     80  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉
     81  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.true) (λtr',s2'.
    6882    tr = tr' ∧
    69     cminor_rtlabs_rel INV s2 s2'
     83    cminor_rtlabs_rel INV s2 s2'
    7084  ).
    7185
    72 (* Note that we start from the "no initialisation" version of the Cminor
    73    semantics.  I plan to prove the initialisation generation separately. *)
     86axiom cminor_rtlabs_init :
     87  ∀p,s.
     88  make_initial_state … Cminor_fullexec p = OK … s →
     89  let p' ≝ cminor_to_rtlabs p in
     90  ∃INV:cminor_rtlabs_inv (make_global … Cminor_fullexec p) (make_global … RTLabs_fullexec p').
     91  ∃s'. make_initial_state … RTLabs_fullexec p' = OK … s' ∧
     92  cminor_rtlabs_rel … INV s s'.
    7493
    75 axiom cminor_noinit_rtlabs_init : ∀cm_program,ra_program,s,s'.
    76   cminor_noinit_to_rtlabs cm_program = ra_program →
    77   make_initial_state ?? Cminor_noinit_fullexec cm_program = OK ? s →
    78   make_initial_state ?? RTLabs_fullexec ra_program = OK ? s' →
    79   ∃INV. cminor_rtlabs_rel INV s s'.
     94include "common/FEMeasurable.ma".
     95include "Cminor/Cminor_classified_system.ma".
     96include "RTLabs/RTLabs_classified_system.ma".
    8097
     98include "common/ExtraMonads.ma".
     99
     100lemma Cminor_return_E0 : ∀ge,s,tr,s'.
     101  step … Cminor_exec ge s = Value … 〈tr,s'〉 →
     102  Cminor_classify s = cl_return →
     103  tr = E0.
     104#ge *
     105[ #f #s #en #H1 #H2 #m #b #k #K #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
     106| #id #fd #args #m #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
     107| #v #m *
     108  [ #tr #s' #STEP #_
     109    cases v in STEP; [ #E whd in E:(??%?); destruct ]
     110    * [1,3,4: normalize #A try #B destruct ]
     111    * #v #STEP whd in STEP:(??%?); destruct %
     112  | cases v
     113    [ * [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct //
     114        | normalize #A #B #C #D #E #F #G #H #I #J #K #L destruct
     115        ]
     116    | #v' *
     117      [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct
     118      | #A #B #C #D #E #F #G #H #I #J #K #L whd in L:(??%?); destruct //
     119      ]
     120    ]
     121  ]
     122| #r #tr #s' #ST #CL normalize in CL; destruct
     123] qed.
     124
     125definition cminor_rtlabs_meas_sim : meas_sim ≝
     126mk_meas_sim
     127  Cminor_pcs
     128  RTLabs_pcs
     129  (λcmp,rap. cminor_to_rtlabs cmp = rap)
     130  cminor_rtlabs_inv
     131  cminor_rtlabs_rel
     132  ? (* rel_normal *)
     133  ? (* rel_labelled *)
     134  ? (* rel_classify_call *)
     135  ? (* rel_classify_return *)
     136  ? (* rel_callee *)
     137  ? (* labelled_normal_1 *)
     138  ? (* labelled_normal_2 *)
     139  ? (* notailcalls *)
     140  (λ_.cminor_measure)
     141  ? (* sim_normal *)
     142  ? (* sim_call_nolabel *)
     143  ? (* sim_call_label *)
     144  ? (* sim_return *)
     145  ? (* sim_cost *)
     146  ? (* sim_init *)
     147.
     148[ (* rel_normal *)
     149| (* rel_labelled *)
     150  @cminor_rtlabs_rel_labelled
     151| (* rel_classify_call *)
     152| (* rel_classify_return *)
     153| (* rel_callee *)
     154| (* labelled_normal_1 *)
     155  #g * //
     156| (* labelled_normal_2 *)
     157  #g * // #f #fs #m whd in ⊢ (?% → ?%); whd in match (pcs_classify ???);
     158  cases (next_instruction f) //
     159| (* notailcalls *)
     160  #g @Cminor_notailcalls
     161| (* sim_normal *)
     162  #g1 #g2 #INV #s1 #s1' #R1 #N1 #NCS1 #s2 #tr #STEP
     163  cases (cminor_rtlabs_normal … R1 N1 NCS1 STEP)
     164  #m #AFTER %{m} @(after_n_covariant … AFTER)
     165  #tr' #s * * #H1 #H2 #H3 /3/
     166| (* sim_call_nolabel *)
     167  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP #NCS2 %{0}
     168  @(cminor_rtlabs_call_return … R1 … STEP)
     169  change with (Cminor_classify ?) in CL1:(??%?); >CL1 %
     170| (* sim_call_label *)
     171  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #STEP1 #CS2 #STEP2 %{1}
     172  lapply (cminor_rtlabs_call_return … R1 … STEP1)
     173  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
     174  #AFTER1 @(after_n_covariant … AFTER1) #tr' #s' * #E #R' destruct
     175  % [ %
     176  [  %
     177  |  change with (RTLabs_cost s') in ⊢ (?%); <(cminor_rtlabs_rel_labelled … R') @CS2
     178  ]| lapply (cminor_rtlabs_cost … R' … CS2 STEP2)
     179     #AFTER2 cases (after_1_step … AFTER2)
     180     #trx * #sx * * #NFx #STEPx * #E #Rx destruct
     181     whd >NFx whd >STEPx whd /3/
     182  ]
     183| (* sim_return *)
     184  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP %{0}
     185  lapply (cminor_rtlabs_call_return … R1 … STEP)
     186  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
     187  >(Cminor_return_E0 … STEP CL1)
     188  #AFTER %{(refl ??)} @AFTER
     189| (* sim_cost *)
     190  #g1 #g2 #INV #s1 #s1' #s2 #tr #R1 #CS1 #STEP
     191  @(cminor_rtlabs_cost … R1 … STEP)
     192  @CS1
     193| (* sim_init *)
     194  #p #p' #s #COMPILE destruct #INIT
     195  cases (cminor_rtlabs_init … INIT) #INV * #s' * #INIT' #R
     196  %{s'} % [ @INIT' | %{INV} @R ]
     197] cases daemon qed.
  • src/common/FEMeasurable.ma

    r2990 r3007  
    2222   Note: as we're interested in measurable subtraces, we don't have to worry
    2323   about the execution "going wrong."
     24   
     25   For call and return states we only allow the addition of extra steps *after*
     26   the corresponding call or return state (i.e., the simulation must always
     27   start with it).  This is true in the front-end: Callstate and Returnstate
     28   are the second half of calls and returns, the first is the instruction for
     29   the call or return which is translated as a "normal" step, where any extra
     30   instructions for before the action are added.
    2431    *)
    2532
     
    2936  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
    3037  ms_inv : ? → ? → Type[0];
    31   ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
    3238  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
    3339  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2;
     
    192198      ms_rel MS g g' INV sr sr'.
    193199
    194 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
     200* #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
    195201#g #g' #INV #s1 #s1' #REL
    196202#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     
    447453       measurable trace, so the end is no longer in the relation. ☹ *)
    448454   
    449 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
     455* #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
    450456#g #g' #INV #s1 #s1' #depth #callstack #REL
    451457#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
Note: See TracChangeset for help on using the changeset viewer.