tweak speculation section

Author: JTurcotti

KLR/Compile/Dataflow.lean

@@ -1251,14 +1251,21 @@ section ConcreteMapImpl
     -/
 
     /-======================================================
+
       HEY THIS IS IMPORTANT:
 
       SPECULATION ON USAGE OF `(𝕏 : SolutionT).props` OUTPUT VALUE
       IN LARGER PROOFS
 
       ======================================================
 
-      of course, the point of this dataflow solver as a modular
+      In particular...
+
+      Reasoning about execution traces by bisimulation to the dataflow type!
+
+      ======================================================
+
+      Of course, the point of this dataflow solver as a modular
       component is to return not just the solution `ν` but propositional
       satisfaction of the dataflow inequalities by the `ν`.
 
@@ -1281,11 +1288,15 @@ section ConcreteMapImpl
       (corresponding to value at program entry)
       that relates to the `⊥{β}` for `β`
       satisfying `⊥{α} ∼ ⊥{β}`.
+      (but note that `α` need not have any lattice
+      structure for the bisimulation to be established)
 
       For our above example, we can choose `α := ⟦ℕ, Option ℕ⟧`
         (concrete program states)
-      and `α₀ ∼ β₀` lifting from a corresponding canonical
-        `(_:Option ℕ) ∼  (_:ℂ)` relation (e.g. `some n ∼ 𝕊 n`)
+      and `α₀ ∼ β₀`
+          `α₀` is the concrete/runtime time "refining" `β₀`
+          (lifted from a corresponding canonical refinement
+          `(_:Option ℕ) ∼  (_:ℂ)` relation (e.g. `some n ∼ 𝕊 n`))
       Once the associated properties are proven...
 
       We can now define "program states" `π := (α₀ : α) × (n : ℕ)` (interpreted
@@ -1294,35 +1305,36 @@ section ConcreteMapImpl
       We can now define "program stepping":
        `π₀ ⊑ π₁ := (edge π₀.n π₁.n) ∧ (n:=π₀.n; τₙ) π₀.α₀ = π₁.α₀`
 
-      We can now define a type for "paths" `ℓ` as a list of
-      `N` `α × ℕ` entries (corresponding to program states at unit times)
-      where `ℓ[0] = (⊥{α}, 0)`
-        (assuming 0 is the "entry block"),
-      and `∀ n < N - 1, l[n] ⊑ l[n+1]` (successive entries constitute valid steps)
+      We can now define a type for "traces" `𝕥` as a list of
+      `N` `α × ℕ` entries
+        (corresponding to program states at successive times)
+      where `𝕥[0] = (⊥{α}, 0)`
+        (sound entry to trace (assuming 0 is the "entry block")),
+      and `∀ n < N - 1, 𝕥[n] ⊑ 𝕥[n+1]`
+        (successive entries in trace constitute valid steps)
 
       Now if `ν := 𝕏.vals` is a dataflow solution,
-      and `ℓₙ := (n, _) := ℓ; n`
-      and `ℓₐ := (_, α₀) := ℓ; α₀`
+      and `𝕥ₙ := (n, _) := 𝕥; n`
+      and `𝕥ₐ := (_, α₀) := 𝕥; α₀`
       it is provable inductively from `𝕏.props` that:
-      `∀ ℓ, ℓₐ ∼ ν[ℓₙ]`.
+      `∀ 𝕥, 𝕥ₐ ∼ ν[𝕥ₙ]`.
 
       In the case of our concrete example, this means that we can prove
-      that any program state `αₙ` at node `n` reached through stepping
-      from the entry state is constrained by
-      `αₙ ∼ βₙ` for the abstract state `βₙ := ν[n]`.
-      For various values of `αₙ` and `βₙ`,
+      that any program state `αₙ` at node `n` reached in a trace satifies
+      `αₙ ∼ ν[n]` (the concrete state refines the abstract state)
+      For various values of `αₙ` and `ν[n]`,
       this could mean (for all keys `k`),
 
       `αₙ ∼ 𝕄` : no information
       `αₙ ∼ 𝔸` : `k` is defined
       `αₙ ∼ 𝕊 m` : `k` is defined and equal to `m`
-      `αₙ ∼ 𝕌` : impossible (which implies that `∄ ℓ, ℓₐ ∼ 𝕌)`,
+      `αₙ ∼ 𝕌` : impossible (which implies that `∄ 𝕥, 𝕥ₐ ∼ 𝕌)`,
                   i.e., no node `n` satisfying `ν[n] = 𝕌` will
                   ever be reached by a path
 
-      These are powerful results, for which much
-      thought has gone into generating and
-      presenting conveniently.
+      These are powerful results, hopefully
+      presented in sufficiently accessible
+      datatypes to yield modular use.
     -/
   end ConcreteSolution
 end ConcreteMapImpl