1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
import RoleFlow.Prog

/-! # Recipes (`docs/roleflow.tex`, `sec:typing`, `sec:inverse`)

A recipe is executable (`XRecipe`): the line that computes its targets from its arguments. The
recipes of lines under roles (`xrecs`) are one per conditioner, its own line, and one per spine
step, the line of its semi-inverse, from the results and the parameters to the consumed
arguments. `Known R B` is the least set containing `B` and closed under firing recipes of `R`.

Every recipe holds on every trace (`xrecs_holds`), conditioners by the trace and spine steps by
the left law. The typing (`Recov`), the density theorem and the schedule all use these recipes
and this one fact. -/

namespace RoleFlow

variable {S : Type} {Sg : Sig S}

/-- The results of a line at scope `n`. -/
def Line.ys (l : Line Sg) (n : ℕ) : List ℕ := List.range' n l.bs.length

theorem Line.mem_ys {l : Line Sg} {n v : ℕ} : v ∈ l.ys n ↔ n ≤ v ∧ v < n + l.bs.length := by
  simp only [Line.ys, List.mem_range']
  exact ⟨fun ⟨i, hi, h⟩ => by omega, fun h => ⟨v - n, by omega, by omega⟩⟩

/-- An executable recipe `tgt ← o(args)`: the line that computes the targets `tgt` from its
arguments. -/
structure XRecipe (Sg : Sig S) where
  line : Line Sg
  tgt : List ℕ

/-- The executable recipes of lines under roles at scope `n`, in the order of the lines. -/
def xrecs : ℕ → List (Line Sg) → List Role → List (XRecipe Sg)
  | n, l :: ls, .cond :: ρ => ⟨l, l.ys n⟩ :: xrecs (n + l.bs.length) ls ρ
  | n, l :: ls, .spine :: ρ =>
    match Sg.inv l.op with
    | some si =>
      ⟨⟨si.op, l.ys n ++ l.args.drop si.k⟩, l.args.take si.k⟩ :: xrecs (n + l.bs.length) ls ρ
    | none => xrecs (n + l.bs.length) ls ρ
  | _, _, _ => []

theorem xrecs_cond (n : ℕ) (l : Line Sg) (ls : List (Line Sg)) (ρ : List Role) :
    xrecs n (l :: ls) (.cond :: ρ) = ⟨l, l.ys n⟩ :: xrecs (n + l.bs.length) ls ρ := rfl

theorem xrecs_spine (n : ℕ) (l : Line Sg) (ls : List (Line Sg)) (ρ : List Role)
    {si : SemiInv Sg.Op l.as l.bs} (hsi : Sg.inv l.op = some si) :
    xrecs n (l :: ls) (.spine :: ρ) =
      ⟨⟨si.op, l.ys n ++ l.args.drop si.k⟩, l.args.take si.k⟩ :: xrecs (n + l.bs.length) ls ρ := by
  simp only [xrecs, hsi]

/-- **Membership inversion**: an executable recipe of `l :: ls` is one of the remaining lines,
the line's own (a conditioner) or that of its semi-inverse (a spine step). -/
theorem mem_xrecs {n : ℕ} {l : Line Sg} {ls : List (Line Sg)} {ρ : List Role} {x : XRecipe Sg}
    (h : x ∈ xrecs n (l :: ls) ρ) : x ∈ xrecs (n + l.bs.length) ls ρ.tail ∨ x = ⟨l, l.ys n⟩ ∨
      ∃ si, Sg.inv l.op = some si ∧
        x = ⟨⟨si.op, l.ys n ++ l.args.drop si.k⟩, l.args.take si.k⟩ := by
  rcases ρ with _ | ⟨_ | _, ρ⟩
  · simp [xrecs] at h
  · cases hsi : Sg.inv l.op <;> simp_all [xrecs]; tauto
  · simp_all [xrecs]; tauto

/-- The executable recipes are well formed in the context after the lines. -/
theorem xrecs_wf {Γ : List S} {ls : List (Line Sg)} (h : LinesWF Γ ls) (ρ : List Role) {n : ℕ}
    (hn : Γ.length = n) : ∀ x ∈ xrecs n ls ρ,
      Args (ctxAfter Γ ls) x.line.args x.line.as ∧ Args (ctxAfter Γ ls) x.tgt x.line.bs := by
  induction ls generalizing Γ ρ n with
  | nil => intro x hx; cases ρ <;> simp [xrecs] at hx
  | cons l ls ih =>
    subst hn
    have hy : Args (ctxAfter Γ (l :: ls)) (l.ys Γ.length) l.bs :=
      (Args.range' Γ l.bs).ctxAfter ls
    have hx : Args (ctxAfter Γ (l :: ls)) l.args l.as := (h.1.append l.bs).ctxAfter ls
    intro x hmem
    rcases mem_xrecs hmem with hmem | rfl | ⟨si, -, rfl⟩
    · exact ih h.2 _ (by simp) x hmem
    · exact ⟨hx, hy⟩
    · exact ⟨hy.append' (si.args_drop hx), si.args_take hx⟩

/-- The executable recipes of `P` under the roles `ρ`. -/
def Prog.xrecs (P : Prog Sg) (ρ : List Role) : List (XRecipe Sg) :=
  RoleFlow.xrecs P.ctx₀.length P.lines ρ

theorem Prog.wf_xrecs {P : Prog Sg} {ρ : List Role} (h : P.WF) : ∀ x ∈ P.xrecs ρ,
    Args P.ctx x.line.args x.line.as ∧ Args P.ctx x.tgt x.line.bs :=
  xrecs_wf h.1 ρ rfl

/-! ## Recomputability -/

/-- `Known R B`: the least set containing `B` and closed under firing recipes of `R`. -/
inductive Known (R : List (XRecipe Sg)) (B : Set ℕ) : ℕ → Prop
  | base {v : ℕ} : v ∈ B → Known R B v
  | fire {r : XRecipe Sg} {v : ℕ} : r ∈ R → (∀ w ∈ r.line.args, Known R B w) → v ∈ r.tgt →
      Known R B v

/-- Known values may serve as the base. -/
theorem Known.trans {R : List (XRecipe Sg)} {B B' : Set ℕ} (hB : ∀ w ∈ B', Known R B w) {v : ℕ}
    (h : Known R B' v) : Known R B v := by
  induction h with
  | base hv => exact hB _ hv
  | fire hr _ hv ih => exact .fire hr ih hv

theorem Known.mono {R : List (XRecipe Sg)} {B B' : Set ℕ} (hB : B ⊆ B') {v : ℕ}
    (h : Known R B v) : Known R B' v :=
  h.trans fun _ hw => .base (hB hw)

/-! ## The recipes hold -/

section Holds
variable [Sorts S] (M : Model Sg)

/-- **Every executable recipe holds on every trace**: conditioners by the trace, spine steps by
the left law. -/
theorem xrecs_holds {Γ : List S} {ls : List (Line Sg)} (h : LinesWF Γ ls) (ρ : List Role)
    {n : ℕ} (hn : Γ.length = n) (v : Val Γ) : ∀ x ∈ xrecs n ls ρ,
      ∀ (h₁ : Args (ctxAfter Γ ls) x.line.args x.line.as) (h₂ : Args (ctxAfter Γ ls) x.tgt x.line.bs),
      M.sem x.line.op ((trace M ls h v).pick _ h₁) = (trace M ls h v).pick _ h₂ := by
  induction ls generalizing Γ ρ n with
  | nil => intro x hx; cases ρ <;> simp [xrecs] at hx
  | cons l ls ih =>
    subst hn
    have hy : Args (ctxAfter Γ (l :: ls)) (l.ys Γ.length) l.bs :=
      (Args.range' Γ l.bs).ctxAfter ls
    have hx : Args (ctxAfter Γ (l :: ls)) l.args l.as := (h.1.append l.bs).ctxAfter ls
    have hres : (trace M (l :: ls) h v).pick _ hy = M.sem l.op (v.pick l.args h.1) :=
      pick_trace_results M l ls h v hy
    have hargs : ∀ {xs : List ℕ} {as : List S} (h₀ : Args Γ xs as)
        (h₁ : Args (ctxAfter Γ (l :: ls)) xs as), (trace M (l :: ls) h v).pick xs h₁ = v.pick xs h₀ :=
      fun h₀ h₁ => pick_trace M (l :: ls) h v h₀ h₁
    intro x hmem h₁ h₂
    rcases mem_xrecs hmem with hmem | rfl | ⟨si, hsi, rfl⟩
    · exact ih h.2 _ (by simp) (stepLine M l h.1 v) x hmem h₁ h₂
    · dsimp only at h₁ h₂ ⊢
      rw [hres, hargs h.1]
    · dsimp only at h₁ h₂ ⊢
      rw [Val.pick_append _ hy (si.args_drop hx), hres, hargs (si.args_drop h.1),
        hargs (si.args_take h.1), ← si.glue_pick v h.1]
      exact M.left l.op si hsi _ _

end Holds

end RoleFlow