Changeset 3115

Timestamp:

Apr 10, 2013, 1:28:46 PM (8 years ago)

Author:

campbell

Message:

Clean up some left-over lemmas and move comment back into place.

File:

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

src/correctness.ma

@@ -15 +15 @@
    and those observables will include the stack space costs.
  *)
-
-definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
-λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
-
-let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝
-match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
-[ nil ⇒ λ_. a
-| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
-]. 
-[ %1 %
-| #b #H' @H %2 @H'
-] qed.
-
-definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝ 
-λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
-
-lemma Exists_lift : ∀A,P,Q,l.
-  (∀x. P x → Q x) →
-  Exists A P l →
-  Exists A Q l.
-#A #P #Q #l elim l
-[ //
-| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
-] qed.
 
 include "RTLabs/MeasurableToStructured.ma".
@@ -197 +173 @@
   #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
   >OBS -ra_meas
+    
+  (* So, after the front-end 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]
+   *)
+
   cases (produce_rtlabs_flat_trace … ra_exec_prefix)
   #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
@@ -276 +261 @@
   cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr.
     exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 →
-    
-  (* 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〉 →
-            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
-            tlr_observables … tlr (function_of … s1) = obs2 →
-            (* maybe instead of function_of the called id can rather be obtained from execution? *)
-     ∃m,p,s_fin.
-   observables (OC_preclassified_system (c_labelled_object_code … p))
-    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
-    *)
+