Changeset 2003

Timestamp:

May 28, 2012, 1:10:50 PM (6 years ago)

Author:

campbell

Message:

Some discussion of correctness statements.

File:

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

src/correctness.ma

@@ -9 +9 @@
 
 ∀input_program.
-! 〈labelled,output〉 ← compile input_program
+! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
 
 exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
@@ -20 +20 @@
 
 
-∀___.
-Σ_{l∈|___|} F(k)(l) = δ
-→ σ_0 -obj→ σ_f
-→ clock σ_f = clock σ_0 + δ
+∀i,f : clight_status.  [i,f labelled, at same level]
+i clight~> f →
+∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' asm~> f' ∧
+  clock f - clock i = 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 ])).