Changeset 3007 for src/Cminor

Timestamp:

Mar 28, 2013, 2:59:43 PM (8 years ago)

Author:

campbell

Message:

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

Location:

src/Cminor

Files:

• Cminor_abstract.ma (modified) (1 diff)
• toRTLabsCorrectness.ma (modified) (3 diffs)

src/Cminor/Cminor_abstract.ma

@@ -42 +42 @@
 definition CmCallstate ≝ Callstate.
 
+lemma Cminor_notailcalls : ∀s. Cminor_classify s ≠ cl_tailcall.
+* #a try #b try #c try #d try #e try #f try #g try #h try #i try #j
+normalize % #E destruct
+qed.

src/Cminor/toRTLabsCorrectness.ma

@@ -4 +4 @@
 include "Cminor/toRTLabs.ma".
 
-record cminor_rtlabs_inv : Type[0] ≝ {
-  ge_cm : cm_genv;
-  ge_ra : RTLabs_genv
+record cminor_rtlabs_inv (ge_cm:cm_genv) (ge_ra:RTLabs_genv) : Type[0] ≝ {
 }.
-axiom cminor_rtlabs_rel : cminor_rtlabs_inv → Cminor_state → RTLabs_state → Prop.
+axiom cminor_rtlabs_rel : ∀gc,gr. cminor_rtlabs_inv gc gr → Cminor_state → RTLabs_state → Prop.
+
+axiom cminor_rtlabs_rel_labelled : ∀gc,gr,INV,s,s'.
+  cminor_rtlabs_rel gc gr INV s s' →
+  Cminor_labelled s = RTLabs_cost s'.
 
 (* Conjectured simulation results
@@ -14 +16 @@
    We split these based on the start state:
    
-   1. ‘normal’ states take some [S n] normal steps and simulates them by [m]
-      normal steps in RTLabs ([m] can be zero if the Cminor program executed an
-      St_skip);
-   2. call and return steps are simulated by a call/return step plus [m] normal
-      steps (to copy stack allocated parameters / results); and
+   1. from a ‘normal’ state we simulate a step by [n] normal steps in RTLabs
+      ([n] can be zero if the Cminor program executed an St_skip);
+   2. call and return state steps are simulated by a call/return state step (we
+      don't add anything extra in this stage, it happens in Clight to Cminor);
+      and
    3. lone cost label steps are simulates by a lone cost label step
+
+   Most of the work in this stage is splitting the execution of complex Cminor
+   statements into individual RTLabs steps.  This doesn't contradict 2 above -
+   the expansion of function parameters, return expressions, etc is done for
+   the function call / return *statement*, whereas the call / return *state* is
+   a Callstate / Returnstate that is the second half of the operation.
 
    Note that we'll need something more to show that non-termination is
@@ -36 +44 @@
 λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
 
+axiom cminor_measure : Cminor_state → nat.
+
 axiom cminor_rtlabs_normal :
-  ∀INV:cminor_rtlabs_inv.
+  ∀ge_cm,ge_ra.
+  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
   ∀s1,s1',s2,tr.
-  cminor_rtlabs_rel INV s1 s1' →
+  cminor_rtlabs_rel … INV s1 s1' →
   cminor_normal s1 →
   ¬ Cminor_labelled s1 →
-  ∃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〉) →
-  ∃m. after_n_steps m … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'.
+  step ?? Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
+  ∃n. after_n_steps n … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
     tr = tr' ∧
-    cminor_rtlabs_rel INV s2 s2'
+    (n = 0 → lt (cminor_measure s2) (cminor_measure s1)) ∧
+    cminor_rtlabs_rel … INV s2 s2'
   ).
 
 axiom cminor_rtlabs_call_return :
-  ∀INV:cminor_rtlabs_inv.
+  ∀ge_cm,ge_ra.
+  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
   ∀s1,s1',s2,tr.
-  cminor_rtlabs_rel INV s1 s1' →
+  cminor_rtlabs_rel … INV s1 s1' →
   match Cminor_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
-  after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
-  ∃m. after_n_steps (S m) … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'.
+  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
+  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'.
     tr = tr' ∧
-    cminor_rtlabs_rel INV s2 s2'
+    cminor_rtlabs_rel … INV s2 s2'
   ).
 
 axiom cminor_rtlabs_cost :
-  ∀INV:cminor_rtlabs_inv.
+  ∀ge_cm,ge_ra.
+  ∀INV:cminor_rtlabs_inv ge_cm ge_ra.
   ∀s1,s1',s2,tr.
-  cminor_rtlabs_rel INV s1 s1' →
+  cminor_rtlabs_rel … INV s1 s1' →
   Cminor_labelled s1 →
-  after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
-  after_n_steps 1 … RTLabs_exec (ge_ra INV) s1' (λs.true) (λtr',s2'.
+  step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 →
+  after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.true) (λtr',s2'.
     tr = tr' ∧
-    cminor_rtlabs_rel INV s2 s2'
+    cminor_rtlabs_rel … INV s2 s2'
   ).
 
-(* Note that we start from the "no initialisation" version of the Cminor
-   semantics.  I plan to prove the initialisation generation separately. *)
+axiom cminor_rtlabs_init :
+  ∀p,s.
+  make_initial_state … Cminor_fullexec p = OK … s →
+  let p' ≝ cminor_to_rtlabs p in
+  ∃INV:cminor_rtlabs_inv (make_global … Cminor_fullexec p) (make_global … RTLabs_fullexec p').
+  ∃s'. make_initial_state … RTLabs_fullexec p' = OK … s' ∧
+  cminor_rtlabs_rel … INV s s'.
 
-axiom cminor_noinit_rtlabs_init : ∀cm_program,ra_program,s,s'.
-  cminor_noinit_to_rtlabs cm_program = ra_program →
-  make_initial_state ?? Cminor_noinit_fullexec cm_program = OK ? s →
-  make_initial_state ?? RTLabs_fullexec ra_program = OK ? s' →
-  ∃INV. cminor_rtlabs_rel INV s s'.
+include "common/FEMeasurable.ma".
+include "Cminor/Cminor_classified_system.ma".
+include "RTLabs/RTLabs_classified_system.ma".
 
+include "common/ExtraMonads.ma".
+
+lemma Cminor_return_E0 : ∀ge,s,tr,s'.
+  step … Cminor_exec ge s = Value … 〈tr,s'〉 →
+  Cminor_classify s = cl_return →
+  tr = E0.
+#ge *
+[ #f #s #en #H1 #H2 #m #b #k #K #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
+| #id #fd #args #m #st #tr #s' #STEP #CL whd in CL:(??%?); destruct
+| #v #m *
+  [ #tr #s' #STEP #_
+    cases v in STEP; [ #E whd in E:(??%?); destruct ]
+    * [1,3,4: normalize #A try #B destruct ]
+    * #v #STEP whd in STEP:(??%?); destruct %
+  | cases v
+    [ * [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct //
+        | normalize #A #B #C #D #E #F #G #H #I #J #K #L destruct
+        ]
+    | #v' *
+      [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct
+      | #A #B #C #D #E #F #G #H #I #J #K #L whd in L:(??%?); destruct //
+      ]
+    ]
+  ]
+| #r #tr #s' #ST #CL normalize in CL; destruct
+] qed.
+
+definition cminor_rtlabs_meas_sim : meas_sim ≝
+mk_meas_sim
+  Cminor_pcs
+  RTLabs_pcs
+  (λcmp,rap. cminor_to_rtlabs cmp = rap)
+  cminor_rtlabs_inv
+  cminor_rtlabs_rel
+  ? (* rel_normal *)
+  ? (* rel_labelled *)
+  ? (* rel_classify_call *)
+  ? (* rel_classify_return *)
+  ? (* rel_callee *)
+  ? (* labelled_normal_1 *)
+  ? (* labelled_normal_2 *)
+  ? (* notailcalls *)
+  (λ_.cminor_measure)
+  ? (* sim_normal *)
+  ? (* sim_call_nolabel *)
+  ? (* sim_call_label *)
+  ? (* sim_return *)
+  ? (* sim_cost *)
+  ? (* sim_init *)
+.
+[ (* rel_normal *)
+| (* rel_labelled *)
+  @cminor_rtlabs_rel_labelled
+| (* rel_classify_call *)
+| (* rel_classify_return *)
+| (* rel_callee *)
+| (* labelled_normal_1 *)
+  #g * //
+| (* labelled_normal_2 *)
+  #g * // #f #fs #m whd in ⊢ (?% → ?%); whd in match (pcs_classify ???);
+  cases (next_instruction f) //
+| (* notailcalls *)
+  #g @Cminor_notailcalls
+| (* sim_normal *)
+  #g1 #g2 #INV #s1 #s1' #R1 #N1 #NCS1 #s2 #tr #STEP
+  cases (cminor_rtlabs_normal … R1 N1 NCS1 STEP)
+  #m #AFTER %{m} @(after_n_covariant … AFTER)
+  #tr' #s * * #H1 #H2 #H3 /3/
+| (* sim_call_nolabel *)
+  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP #NCS2 %{0}
+  @(cminor_rtlabs_call_return … R1 … STEP)
+  change with (Cminor_classify ?) in CL1:(??%?); >CL1 %
+| (* sim_call_label *)
+  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #STEP1 #CS2 #STEP2 %{1}
+  lapply (cminor_rtlabs_call_return … R1 … STEP1)
+  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
+  #AFTER1 @(after_n_covariant … AFTER1) #tr' #s' * #E #R' destruct
+  % [ %
+  [  %
+  |  change with (RTLabs_cost s') in ⊢ (?%); <(cminor_rtlabs_rel_labelled … R') @CS2
+  ]| lapply (cminor_rtlabs_cost … R' … CS2 STEP2)
+     #AFTER2 cases (after_1_step … AFTER2)
+     #trx * #sx * * #NFx #STEPx * #E #Rx destruct
+     whd >NFx whd >STEPx whd /3/
+  ]
+| (* sim_return *)
+  #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP %{0}
+  lapply (cminor_rtlabs_call_return … R1 … STEP)
+  [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ]
+  >(Cminor_return_E0 … STEP CL1)
+  #AFTER %{(refl ??)} @AFTER
+| (* sim_cost *)
+  #g1 #g2 #INV #s1 #s1' #s2 #tr #R1 #CS1 #STEP
+  @(cminor_rtlabs_cost … R1 … STEP)
+  @CS1
+| (* sim_init *)
+  #p #p' #s #COMPILE destruct #INIT
+  cases (cminor_rtlabs_init … INIT) #INV * #s' * #INIT' #R
+  %{s'} % [ @INIT' | %{INV} @R ]
+] cases daemon qed.