Changeset 3074

Timestamp:

Apr 2, 2013, 7:25:22 PM (8 years ago)

Author:

campbell

Message:

Put some kind of high level proof in for front-end.

File:

• src/correctness.ma (modified) (5 diffs)

src/correctness.ma

@@ -41 +41 @@
 
 include "RTLabs/MeasurableToStructured.ma".
-
-definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝
-λp,n,costmap.
-  ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n;
+include "common/ExtraMonads.ma".
+
+definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝
+λcostmap,itrace.
   let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
-  return Σ_{l ∈ ctrace}(costmap l).
+  Σ_{l ∈ ctrace}(costmap l).
+
+definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝
+λC,p,n,costmap.
+  ! 〈s,itrace〉 ← exec_steps_with_obs C p n;
+  return exec_cost_of_trace costmap itrace.
+
+lemma obs_exec_steps_with_obs : ∀pcs,p,m1,m2,obs1,obs2.
+  observables pcs p m1 m2 = return 〈obs1,obs2〉 →
+  ∃s1,s2.
+    exec_steps_with_obs pcs p m1 = return 〈s1,obs1〉 ∧
+    exec_steps_with_obs pcs p (m1+m2) = return 〈s2,obs1@obs2〉.
+#pcs #p #m1 #m2 #obs1 #obs2 #OBS
+@('bind_inversion OBS) -OBS #s0 #INIT #OBS
+@('bind_inversion OBS) -OBS * #tr1 #s1 #EXEC1 #OBS
+@('bind_inversion OBS) -OBS * #tr2 #s2 #EXEC2 @breakup_pair #OBS
+whd in OBS:(??%%); destruct
+%{s1} %{s2}
+whd in ⊢ (?(??%?)(??%?)); >INIT
+whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2)
+whd in ⊢ (?(??%?)(??%?));
+% [ % | >int_trace_append' @breakup_pair @breakup_pair % ]
+qed.
+
+lemma bigsum_append : ∀A,l1,l2. ∀f:A → ℕ.
+  (Σ_{l ∈ (l1@l2)}(f l)) = (Σ_{l ∈ l1}(f l)) + (Σ_{l ∈ l2}(f l)).
+#A #l1 elim l1
+[ #l2 #f %
+| #h #tl #IH #l2 #f whd in ⊢ (??%(?%?)); >IH //
+] qed.
+
+lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs.
+  observables pcs p m1 m2 = return 〈obs1,obs2〉 →
+  clock_after pcs p m1 costs = return c1 →
+  clock_after pcs p (m1+m2) costs = return c2 →
+  c2 - c1 = exec_cost_of_trace costs obs2.
+#pcs #p #m1 #m2 #obs1 #obs2 #c1 #c2 #costs #OBS
+cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2
+whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
+whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
+>filter_map_append >bigsum_append /2/
+qed.
 
 include "common/AssocList.ma".
@@ -61 +102 @@
     (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
   ∀c1,c2.
-   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
-   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = OK … c2 →
+   clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
+   clock_after Clight_pcs (c_labelled_clight … p) (m1+m2) (c_clight_cost_map … p) = OK … c2 →
   ∃n1,n2.
    observables Clight_pcs (c_labelled_clight … p) m1 m2 =
@@ -70 +111 @@
    minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
 
-include "common/ExtraMonads.ma".
-
 include "Clight/SwitchAndLabel.ma".
+
+include "common/FEMeasurable.ma".
+include "Clight/SimplifyCastsMeasurable.ma".
+include "Clight/toCminorMeasurable.ma".
+include "Cminor/toRTLabsCorrectness.ma".
+
+lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
+  measurable pcs p m1 m2 stack_cost max →
+  ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉.
+#pcs #p #m1 #m2 #stack_cost #max
+* #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_
+% [2: % [2:
+  whd in ⊢ (??%?); >INIT in ⊢ (??%?);
+  whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?);
+  whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?);
+  whd in ⊢ (??%?); @breakup_pair %
+| skip ]| skip ]
+qed.
 
 theorem correct :
@@ -115 +172 @@
   #E >E
   @switch_and_labelling_sim @NOT_WRONG
-| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
-
+| cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ]
+  #El >El
+  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
+  cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
+  >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
+  cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
+  #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; -m1 -m2
+  cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
+  #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
+  cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
+  #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
+  #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
+  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
+  >OBS -ra_meas
+  
+  (* So, we have for RTLabs:
+     ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
+     ra_tlr         - structured trace from [ra_s1] to some [ra_s2],
+     ra_unrepeating - PCs don't repeat locally in [ra_tlr]
+     ra_obs'        - the observables from [ra_tlr] are [subtrace]
+     ra_max         - the stack bound is respected in [prefix@subtrace]
+   *)
+
+
+(* Old, semiformal cut
 cut (∀n,s1,s2,obs1,obs2.
           exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
@@ -125 +205 @@
    observables (OC_preclassified_system (c_labelled_object_code … p))
     (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
-    
+    *)
      
              
              
-  
-(* start of old simulates  
-
-(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
-   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
-   according to the [stack_cost] function. *)
-axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
-axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
-
-
-  let cl_trace ≝ exec_inf … clight_fullexec labelled in
-  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
-  not_wrong ? cl_trace →
-  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
-  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
-
-*)
-
-(* TODO 
-
-
-∀input_program.
-! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
-
-exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
-
-∧
-
-exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
-(* Should we be lifting labels in some way here? *)
-
-∧
-
-∀i,f : clight_status.
-  Clight_labelled i →
-  Clight_labelled f →
-∀mx,time.
-  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
-  will_return O O mx time f trace →
-  mx < max_allowed_stack →
-∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
-  time = clock f' - clock i'.
-
-
-∀s,flat.
-let ge ≝ (globalenvs … labelled) in
-subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
-RTLabs_cost s = true →
-∀WR : will_return ge 0 s flat.
-let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
-let labels_rtlabs ≝ flat_label_trace … flat WR in
-∃!initial,final,structured_trace_asm. 
-  structured_trace_rtlabs ≈ structured_trace_asm ∧  
-  clock … code_memory … final = clock … code_memory … initial +
-     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
-
-
-
-What is ≃l?  Must show that "labelled" does everything that 
-"input_program" does, without getting lost in some
-non-terminating loop part way.
-
-*)
-