State.lean

import Verified.Locals
import Verified.HeapStep
import Verified.TreeHeader
import Verified.Bytes.Represent
import LeanExe.Pipeline.Rebuilt
import LeanExe.Pipeline.RecordPointers
import LeanExe.Pipeline.Allocation
import LeanExe.TalosCompat

/-! The states of the verified compiler's proof: how locals hold words, how words represent values
in a heap and store, the steps that a heap and store take, and `Holds`, the facts about the
variables in scope. -/

namespace Verified

open Wasm LeanExe.Pipeline LeanExe.Runtime

theorem Ty.scalar_pair {a b : Ty} (h : (Ty.pair a b).scalar = true) :
    a.scalar = true ∧ b.scalar = true := by
  simpa [Ty.scalar] using h

/-- The array `xs` at `ptr` in `heap` at `store`, borrowed or owned. -/
def Mode.array : Mode → Heap → Store Unit → UInt64 → Array UInt64 → Prop
  | .borrowed, heap, store, ptr, xs => heap.Borrowed store ptr xs
  | .owned, heap, store, ptr, xs => heap.Owned store ptr xs

/-- The words that hold the elements of an array of element type `e`, as `Implements` stores
them: an array of words as itself, an array of floats as their bit patterns, an array of `Bool`s
as its `flatWords`, 1 or 0 each, and an array of tuples as its elements' words in order. -/
def Elem.words : (e : Elem) → Array e.denote → Array UInt64
  | .word, xs => xs
  | .bool, xs => flatWords xs
  | .float, xs => xs.map Float.toBits
  | .float32, xs => xs.map fun x : Float32 => x.toBits.toUInt64
  | .prod a b, xs => (xs.toList.flatMap (Elem.toWords (.prod a b))).toArray

theorem Elem.words_eq : (e : Elem) → (xs : Array e.denote) →
    e.words xs = (xs.toList.flatMap e.toWords).toArray
  | .word, xs => by
    apply Array.ext'
    rw [List.toList_toArray]
    show xs.toList = xs.toList.flatMap fun x => [x]
    induction xs.toList with
    | nil => rfl
    | cons x l ih => rw [List.flatMap_cons, ← ih]; rfl
  | .bool, xs => by
    show (xs.toList.flatMap fun x => (Scalar.values x).map Value.word).toArray = _
    rw [show (fun x : Bool => (Scalar.values x).map Value.word) = Elem.toWords .bool from
      funext fun b => by cases b <;> rfl]
  | .float, xs | .float32, xs => by
    apply Array.ext'
    simp only [Elem.words, Array.toList_map, List.toList_toArray, Elem.toWords]
    exact List.map_eq_flatMap
  | .prod _ _, _ => rfl

theorem Elem.width_pos : (e : Elem) → 0 < e.width
  | .word | .bool | .float | .float32 => Nat.one_pos
  | .prod a _ => by have := a.width_pos; simp only [Elem.width]; omega

theorem Elem.toWords_length : (e : Elem) → (v : e.denote) → (e.toWords v).length = e.width
  | .word, _ | .bool, _ | .float, _ | .float32, _ => rfl
  | .prod a b, v => by
    simp only [Elem.toWords, List.length_append, a.toWords_length, b.toWords_length, Elem.width]

theorem Elem.types_length : (e : Elem) → e.types.length = e.width
  | .word | .bool | .float | .float32 => rfl
  | .prod a b => by simp only [Elem.types, List.length_append, a.types_length, b.types_length,
      Elem.width]

theorem flatMap_length_const {α : Type} {f : α → List UInt64} {k : Nat}
    (hf : ∀ x, (f x).length = k) : (l : List α) → (l.flatMap f).length = l.length * k
  | [] => by simp
  | x :: l => by
    rw [List.flatMap_cons, List.length_append, hf, flatMap_length_const hf l, List.length_cons,
      Nat.succ_mul, Nat.add_comm]

theorem flatMap_getElem!_const {α : Type} [Inhabited α] {f : α → List UInt64} {k : Nat}
    (hf : ∀ x, (f x).length = k) : (l : List α) → {i j : Nat} → i < l.length → j < k →
      (l.flatMap f)[i * k + j]! = (f l[i]!)[j]!
  | [], _, _, h, _ => absurd h (by simp)
  | x :: l, i, j, hi, hj => by
    rw [List.flatMap_cons]
    cases i with
    | zero =>
      simp only [Nat.zero_mul, Nat.zero_add, List.getElem!_cons_zero]
      rw [getElem!_pos _ _ (by rw [List.length_append, hf]; omega),
        getElem!_pos _ _ (by rw [hf]; omega), List.getElem_append_left (by rw [hf]; omega)]
    | succ i =>
      simp only [List.getElem!_cons_succ]
      have hi' : i < l.length := by simpa using hi
      have hrest := flatMap_getElem!_const hf l hi' hj
      rw [show (i + 1) * k + j = (f x).length + (i * k + j) by rw [hf, Nat.succ_mul]; omega]
      rw [← hrest, getElem!_pos _ _ (by
          rw [List.length_append, flatMap_length_const hf]
          have := Nat.mul_le_mul_right k (Nat.succ_le_of_lt hi')
          rw [Nat.succ_mul] at this; omega),
        List.getElem_append_right (by omega), getElem!_pos _ _ (by
          rw [flatMap_length_const hf]
          have := Nat.mul_le_mul_right k (Nat.succ_le_of_lt hi')
          rw [Nat.succ_mul] at this; omega)]
      simp

theorem Elem.words_size (e : Elem) (xs : Array e.denote) :
    (e.words xs).size = xs.size * e.width := by
  rw [Elem.words_eq, List.size_toArray, flatMap_length_const e.toWords_length, Array.length_toList]

/-- Word `j` of element `i` of an array is word `j` of the element. -/
theorem Elem.words_getElem! (e : Elem) (xs : Array e.denote) {i j : Nat} (hi : i < xs.size)
    (hj : j < e.width) : (e.words xs)[i * e.width + j]! = (e.toWords xs[i])[j]! := by
  have h := flatMap_getElem!_const e.toWords_length xs.toList (i := i) (j := j)
    (by simpa using hi) hj
  rw [show xs.toList[i]! = xs[i] by rw [Array.getElem!_toList, getElem!_pos xs i hi]] at h
  rw [Elem.words_eq, List.getElem!_toArray, h]

theorem Elem.words_append (e : Elem) (xs ys : Array e.denote) :
    e.words (xs ++ ys) = e.words xs ++ e.words ys := by
  simp only [Elem.words_eq, Array.toList_append, List.flatMap_append, List.append_toArray]

theorem Elem.words_push (e : Elem) (xs : Array e.denote) (v : e.denote) :
    e.words (xs.push v) = e.words xs ++ (e.toWords v).toArray := by
  simp only [Elem.words_eq, Array.toList_push, List.flatMap_append, List.flatMap_cons,
    List.flatMap_nil, List.append_nil, List.append_toArray]

/-- The words of Lean's default element are 0, which a read past the end of an array gives. -/
theorem Elem.toWords_default : (e : Elem) → e.toWords default = List.replicate e.width 0
  | .word | .bool => rfl
  | .float => by decide
  | .float32 => by decide
  | .prod a b => by
    show a.toWords default ++ b.toWords default = _
    rw [a.toWords_default, b.toWords_default, Elem.width, List.replicate_add]

/-- The value of type `ty` with the bits of `w`: an f64, an f32 from the low 32 bits, or an i64. -/
def typedValue : ValueType → UInt64 → Value
  | .f64, w => .f64 w
  | .f32, w => .f32 w.toUInt32
  | _, w => .i64 w

/-- The values that hold an element, in order: a word or a `Bool` in an i64, a float in its native type,
and a tuple as its first part's values followed by its second's. -/
def Elem.values : (e : Elem) → e.denote → List Value
  | .word, x => [.i64 x]
  | .bool, b => [.i64 (boolWord b)]
  | .float, x => [.f64 x.toBits]
  | .float32, x => [.f32 x.toBits]
  | .prod a b, v => a.values v.1 ++ b.values v.2

@[simp] theorem Elem.values_word (x : UInt64) : Elem.values .word x = [.i64 x] := rfl
@[simp] theorem Elem.values_bool (b : Bool) : Elem.values .bool b = [.i64 (boolWord b)] := rfl
@[simp] theorem Elem.values_float (x : Float) : Elem.values .float x = [.f64 x.toBits] := rfl

theorem Elem.values_length (e : Elem) (v : e.denote) : (e.values v).length = e.width := by
  induction e with
  | word | bool | float | float32 => rfl
  | prod a b iha ihb => simp only [Elem.values, List.length_append, iha, ihb, Elem.width]

/-- An element's values are its words with its types. -/
theorem Elem.values_typed : (e : Elem) → (v : e.denote) →
    List.zipWith typedValue e.types (e.toWords v) = e.values v
  | .word, _ | .bool, _ | .float, _ => rfl
  | .float32, v => by simp [Elem.types, Elem.toWords, Elem.values, typedValue]
  | .prod a b, v => by
    simp only [Elem.types, Elem.toWords, Elem.values]
    rw [List.zipWith_append (by rw [a.types_length, a.toWords_length]), a.values_typed,
      b.values_typed]

/-- The array `ws` with the words `vals` written from position `w0` on. -/
def writeWords (ws : Array UInt64) (w0 : Nat) : List UInt64 → Array UInt64
  | [] => ws
  | v :: vals => writeWords (ws.set! w0 v) (w0 + 1) vals

theorem writeWords_size : (ws : Array UInt64) → (w0 : Nat) → (vals : List UInt64) →
    (writeWords ws w0 vals).size = ws.size
  | _, _, [] => rfl
  | ws, w0, v :: vals => by rw [writeWords, writeWords_size, Array.size_set!]

theorem writeWords_getElem! : (ws : Array UInt64) → (w0 : Nat) → (vals : List UInt64) →
    w0 + vals.length ≤ ws.size → (w : Nat) →
    (writeWords ws w0 vals)[w]! =
      if w0 ≤ w ∧ w < w0 + vals.length then vals[w - w0]! else ws[w]!
  | ws, w0, [], _, w => by simp [writeWords]
  | ws, w0, v :: vals, hfit, w => by
    simp only [List.length_cons] at hfit
    rw [writeWords, writeWords_getElem! _ _ _ (by rw [Array.size_set!]; omega)]
    by_cases h1 : w0 + 1 ≤ w ∧ w < w0 + 1 + vals.length
    · rw [if_pos h1, if_pos (by simp only [List.length_cons]; omega),
        show w - w0 = (w - (w0 + 1)) + 1 by omega, List.getElem!_cons_succ]
    · rw [if_neg h1]
      by_cases h2 : w = w0
      · subst h2
        rw [Array.getElem!_set!_self _ _ _ (by omega), if_pos (by simp), Nat.sub_self,
          List.getElem!_cons_zero]
      · rw [Array.getElem!_set!_ne _ _ _ _ (Ne.symm h2),
          if_neg (by simp only [List.length_cons]; omega)]

/-- An array of words that holds each element's words in order is the array's words. -/
theorem Elem.words_ext (e : Elem) {xs : Array e.denote} {ws : Array UInt64}
    (hSize : ws.size = xs.size * e.width)
    (hWords : ∀ i, i < xs.size → ∀ j, j < e.width →
      ws[i * e.width + j]! = (e.toWords xs[i]!)[j]!) :
    ws = e.words xs := by
  have hk := e.width_pos
  apply Array.ext (by rw [hSize, Elem.words_size])
  intro w h1 h2
  have hq : w / e.width < xs.size := by
    rw [hSize] at h1
    exact Nat.div_lt_of_lt_mul (by rwa [Nat.mul_comm] at h1)
  have hr : w % e.width < e.width := Nat.mod_lt _ hk
  have hw : w = w / e.width * e.width + w % e.width := (Nat.div_add_mod' w e.width).symm
  rw [← getElem!_pos ws w h1, ← getElem!_pos (e.words xs) w h2, hw, hWords _ hq _ hr,
    Elem.words_getElem! e xs hq hr, getElem!_pos xs _ hq]

/-- An update writes the new element's words over the old one's. -/
theorem Elem.words_set (e : Elem) {xs : Array e.denote} {i : Nat} (hi : i < xs.size)
    (v : e.denote) :
    writeWords (e.words xs) (i * e.width) (e.toWords v) = e.words (xs.set! i v) := by
  have hk := e.width_pos
  have hfit : i * e.width + (e.toWords v).length ≤ (e.words xs).size := by
    rw [e.toWords_length, Elem.words_size]
    have := Nat.mul_le_mul_right e.width (Nat.succ_le_of_lt hi)
    rw [Nat.succ_mul] at this; omega
  apply Elem.words_ext e (by rw [writeWords_size, Elem.words_size, Array.size_set!])
  intro i' hi' j hj
  rw [Array.size_set!] at hi'
  rw [writeWords_getElem! _ _ _ hfit, e.toWords_length]
  by_cases he : i' = i
  · subst he
    rw [if_pos (by omega), show i' * e.width + j - i' * e.width = j by omega,
      Array.getElem!_set!_self _ _ _ hi]
  · have hout : ¬(i * e.width ≤ i' * e.width + j ∧ i' * e.width + j < i * e.width + e.width) := by
      intro ⟨h1, h2⟩
      rcases Nat.lt_or_gt_of_ne he with hlt | hgt
      · have := Nat.mul_le_mul_right e.width (Nat.succ_le_of_lt hlt)
        rw [Nat.succ_mul] at this; omega
      · have := Nat.mul_le_mul_right e.width (Nat.succ_le_of_lt hgt)
        rw [Nat.succ_mul] at this; omega
    rw [if_neg hout, Elem.words_getElem! e xs hi' hj, Array.getElem!_set!_ne _ _ _ _ (Ne.symm he),
      getElem!_pos xs _ hi']

/-- The words of an array with room for one more element, with that element's words written
after the old words, are the words of the array with the element pushed. -/
theorem Elem.words_push_into (e : Elem) {xs : Array e.denote} {ws : Array UInt64} (v : e.denote)
    (hSize : ws.size = xs.size * e.width + e.width)
    (hPrefix : ∀ w, w < xs.size * e.width → ws[w]! = (e.words xs)[w]!) :
    writeWords ws (xs.size * e.width) (e.toWords v) = e.words (xs.push v) := by
  have hk := e.width_pos
  apply Elem.words_ext e (by rw [writeWords_size, hSize, Array.size_push, Nat.succ_mul])
  intro i hi j hj
  rw [Array.size_push] at hi
  rw [writeWords_getElem! _ _ _ (by rw [e.toWords_length, hSize]), e.toWords_length]
  by_cases he : i = xs.size
  · subst he
    rw [if_pos (by omega), show xs.size * e.width + j - xs.size * e.width = j by omega,
      getElem!_pos (xs.push v) _ (by rw [Array.size_push]; omega), Array.getElem_push_eq]
  · have hlt : i < xs.size := by omega
    have hw : i * e.width + j < xs.size * e.width := by
      have := Nat.mul_le_mul_right e.width (Nat.succ_le_of_lt hlt)
      rw [Nat.succ_mul] at this; omega
    rw [if_neg (by omega), hPrefix _ hw, Elem.words_getElem! e xs hlt hj,
      getElem!_pos (xs.push v) i (by rw [Array.size_push]; omega), Array.getElem_push_lt hlt]

/-- An element's words are the bits of its values. -/
theorem Elem.values_words : (e : Elem) → (v : e.denote) → (e.values v).map Value.word = e.toWords v
  | .word, _ | .bool, _ | .float, _ | .float32, _ => rfl
  | .prod a b, v => by
    simp only [Elem.values, Elem.toWords, List.map_append, a.values_words, b.values_words]

theorem Elem.typed_words (e : Elem) (v : e.denote) :
    (List.zipWith typedValue e.types (e.toWords v)).map Value.word = e.toWords v := by
  rw [e.values_typed, e.values_words]

/-- The blocks of the objects that an owned value's arrays occupy, each as its start and
length. -/
def Ty.blocks (store : Store Unit) : (t : Ty) → List Value → t.denote → List (Nat × Nat)
  | .elem _, _, _ => []
  | .bytes, ws, _ => (Bytes.roots ws).map (block store)
  | .pair a b, ws, p =>
    a.blocks store (ws.take a.width) p.1 ++ b.blocks store (ws.drop a.width) p.2
  | .array _, ws, _ | .treeHeader _ _, ws, _ => match ws with
    | [.i64 ptr] => [block store ptr]
    | _ => []
  | .tree _, ws, value => match ws with
    | [.i64 ptr] => value.toNode.blocks store ptr
    | _ => []

/-- The addresses of a value's arrays. -/
def Ty.pointers (store : Store Unit) : (t : Ty) → List Value → t.denote → List UInt64
  | .elem _, _, _ => []
  | .bytes, ws, _ => Bytes.roots ws
  | .pair a b, ws, value =>
    a.pointers store (ws.take a.width) value.1 ++ b.pointers store (ws.drop a.width) value.2
  | .array _, ws, _ | .treeHeader _ _, ws, _ => match ws with
    | [.i64 ptr] => [ptr]
    | _ => []
  | .tree _, ws, value => match ws with
    | [.i64 ptr] => value.toNode.pointers store ptr
    | _ => []

/-- The regions protected by a borrowed value. -/
def Ty.reads (store : Store Unit) : (t : Ty) → List Value → t.denote → List (Nat × Nat)
  | .elem _, _, _ => []
  | .bytes, ws, _ => (Bytes.roots ws).map (block store)
  | .pair a b, ws, p =>
    a.reads store (ws.take a.width) p.1 ++ b.reads store (ws.drop a.width) p.2
  | .array e, ws, xs => match ws with
    | [.i64 ptr] => [(ptr.toNat, 8 * ((e.words xs).size + 1))]
    | _ => []
  | .tree _, ws, value => match ws with
    | [.i64 ptr] => value.toNode.slotRegions store ptr
    | _ => []
  | .treeHeader _ _, _, _ => []

def Mode.node : Mode → Heap → Store Unit → UInt64 → Node → Prop
  | .borrowed, heap, store, ptr, value => NodeBorrowed heap store ptr value
  | .owned, heap, store, ptr, value =>
    NodeOwned heap store ptr value ∧ (value.blocks store ptr).Pairwise regionsDisjoint

def Mode.header : Mode → (shape : TreeShape) → Fin shape.records → Heap → Store Unit → UInt64 →
    Prop
  | .borrowed, _, _, _, _, _ => True
  | .owned, shape, r, heap, store, ptr => TreeHeader.Owned shape r heap store ptr

/-- The regions that a value occupies: its blocks when owned, and its arrays' regions when
borrowed. -/
def Ty.regions (mode : Mode) (store : Store Unit) (t : Ty) (ws : List Value) (v : t.denote) :
    List (Nat × Nat) :=
  match mode with
  | .owned => t.blocks store ws v
  | .borrowed => t.reads store ws v

/-- The words `ws` represent the value `v` of type `t` in `heap` at `store`, with the arrays that
the value contains held in mode `mode`: a word as itself, a `Bool` as 1 or 0, a pair as its first
component's words followed by its second's, and an array as its address.  The components of an
owned pair occupy disjoint blocks. -/
def Ty.Rep (mode : Mode) (heap : Heap) (store : Store Unit) :
    (t : Ty) → List Value → t.denote → Prop
  | .elem e, ws, v => ws = e.values v
  | .bytes, ws, v => Bytes.represented heap store ws v
  | .pair a b, ws, p =>
    ∃ first second, ws = first ++ second ∧ a.Rep mode heap store first p.1 ∧
      b.Rep mode heap store second p.2 ∧
      (mode = .owned → ∀ x ∈ a.blocks store first p.1, ∀ y ∈ b.blocks store second p.2,
        regionsDisjoint x y)
  | .array e, ws, xs => ∃ ptr, ws = [.i64 ptr] ∧ mode.array heap store ptr (e.words xs)
  | .tree _, ws, value => ∃ ptr, ws = [.i64 ptr] ∧ mode.node heap store ptr value.toNode
  | .treeHeader shape r, ws, _ => ∃ ptr, ws = [.i64 ptr] ∧ mode.header shape r heap store ptr

theorem Mode.array.borrow {mode : Mode} {heap : Heap} {store : Store Unit} {ptr : UInt64}
    {xs : Array UInt64} (h : mode.array heap store ptr xs) : heap.Borrowed store ptr xs := by
  cases mode
  · exact h
  · exact Heap.Owned.borrowed h

@[simp] theorem Ty.rep_word {mode : Mode} {heap : Heap} {store : Store Unit} {ws : List Value}
    {v : UInt64} : Ty.Rep mode heap store .word ws v ↔ ws = [.i64 v] := Iff.rfl

@[simp] theorem Ty.rep_bool {mode : Mode} {heap : Heap} {store : Store Unit} {ws : List Value}
    {b : Bool} : Ty.Rep mode heap store .bool ws b ↔ ws = [.i64 (boolWord b)] := Iff.rfl

theorem Ty.rep_elem {mode : Mode} {heap : Heap} {store : Store Unit} {ws : List Value}
    {e : Elem} {x : e.denote} : Ty.Rep mode heap store (.elem e) ws x ↔ ws = e.values x := Iff.rfl

theorem Ty.Rep.length {mode : Mode} {heap : Heap} {store : Store Unit} :
    {t : Ty} → {ws : List Value} → {v : t.denote} → t.Rep mode heap store ws v →
      ws.length = t.width
  | .elem e, _, v, h => by subst h; exact e.values_length v
  | .bytes, _, _, h => Bytes.represented_length h
  | .pair _ _, _, _, ⟨_, _, h, h1, h2, _⟩ => by
    subst h; simp [Ty.width, h1.length, h2.length]
  | .array _, _, _, ⟨_, h, _⟩ | .tree _, _, _, ⟨_, h, _⟩
  | .treeHeader _ _, _, _, ⟨_, h, _⟩ => by subst h; rfl

theorem Ty.blocks_append {store : Store Unit} {a b : Ty} {first second : List Value}
    {p : a.denote × b.denote} (h : first.length = a.width) :
    (Ty.pair a b).blocks store (first ++ second) p =
      a.blocks store first p.1 ++ b.blocks store second p.2 := by
  simp [Ty.blocks, ← h]

theorem Ty.reads_append {store : Store Unit} {a b : Ty} {first second : List Value} {p : a.denote × b.denote}
    (h : first.length = a.width) :
    (Ty.pair a b).reads store (first ++ second) p = a.reads store first p.1 ++ b.reads store second p.2 := by
  simp [Ty.reads, ← h]

theorem Ty.regions_append {mode : Mode} {store : Store Unit} {a b : Ty}
    {first second : List Value} {p : a.denote × b.denote} (h : first.length = a.width) :
    (Ty.pair a b).regions mode store (first ++ second) p =
      a.regions mode store first p.1 ++ b.regions mode store second p.2 := by
  cases mode
  · exact Ty.reads_append h
  · exact Ty.blocks_append h

theorem Ty.blocks_scalar {store : Store Unit} :
    (t : Ty) → t.scalar = true → (ws : List Value) → (v : t.denote) → t.blocks store ws v = []
  | .elem _, _, _, _ => rfl
  | .pair a b, h, ws, p => by
    simp only [Ty.blocks, a.blocks_scalar (Ty.scalar_pair h).1,
      b.blocks_scalar (Ty.scalar_pair h).2, List.append_nil]
  | .array _, h, _, _ => absurd h Bool.false_ne_true

theorem Ty.regions_scalar {mode : Mode} {store : Store Unit} :
    (t : Ty) → t.scalar = true → (ws : List Value) → (v : t.denote) → t.regions mode store ws v = []
  | .elem _, _, _, _ => by cases mode <;> rfl
  | .pair a b, h, ws, p => by
    cases mode
    · simp only [Ty.regions, Ty.reads]
      have ha := a.regions_scalar (mode := .borrowed) (store := store) (Ty.scalar_pair h).1
        (ws.take a.width) p.1
      have hb := b.regions_scalar (mode := .borrowed) (store := store) (Ty.scalar_pair h).2
        (ws.drop a.width) p.2
      simp only [Ty.regions] at ha hb
      rw [ha, hb]; rfl
    · exact Ty.blocks_scalar _ h ws p
  | .array _, h, _, _ => absurd h Bool.false_ne_true

theorem Ty.reads_scalar {store : Store Unit} :
    (t : Ty) → t.scalar = true → (ws : List Value) → (v : t.denote) → t.reads store ws v = []
  | .elem _, _, _, _ => rfl
  | .pair a b, h, ws, p => by
    simp only [Ty.reads, a.reads_scalar (Ty.scalar_pair h).1 _ p.1,
      b.reads_scalar (Ty.scalar_pair h).2 _ p.2, List.append_nil]
  | .array _, h, _, _ => absurd h Bool.false_ne_true

theorem Ty.pointers_scalar {store : Store Unit} :
    (t : Ty) → t.scalar = true → (ws : List Value) → (v : t.denote) → t.pointers store ws v = []
  | .elem _, _, _, _ => rfl
  | .pair a b, h, ws, v => by
    simp only [Ty.pointers, a.pointers_scalar (Ty.scalar_pair h).1,
      b.pointers_scalar (Ty.scalar_pair h).2, List.append_nil]
  | .array _, h, _, _ => absurd h Bool.false_ne_true

/-- A value's blocks are those at its arrays' addresses. -/
theorem Ty.blocks_pointers {store : Store Unit} :
    (t : Ty) → (ws : List Value) → (v : t.denote) →
      t.blocks store ws v = (t.pointers store ws v).map (block store)
  | .elem _, _, _ => rfl
  | .bytes, _, _ => rfl
  | .pair a b, ws, p => by
    simp only [Ty.blocks, Ty.pointers, List.map_append, a.blocks_pointers, b.blocks_pointers]
  | .array _, ws, _ | .treeHeader _ _, ws, _ => by
    simp only [Ty.blocks, Ty.pointers]
    split <;> rfl
  | .tree _, ws, value => by
    simp only [Ty.blocks, Ty.pointers]
    split
    · exact (Node.pointers_blocks ..).symm
    · rfl

/-- The blocks of an owned value are pairwise disjoint. -/
theorem Ty.Rep.pairwise {heap : Heap} {store : Store Unit} :
    {t : Ty} → {ws : List Value} → {v : t.denote} → t.Rep .owned heap store ws v →
      (t.blocks store ws v).Pairwise regionsDisjoint
  | .elem _, _, _, _ => List.Pairwise.nil
  | .bytes, _, _, ⟨root, length, rfl, _⟩ => by
    simp only [Ty.blocks, Bytes.roots]
    split <;> simp
  | .pair _ _, _, _, ⟨first, second, h, h1, h2, hd⟩ => by
    subst h
    rw [Ty.blocks_append h1.length]
    exact List.pairwise_append.mpr ⟨h1.pairwise, h2.pairwise, hd rfl⟩
  | .array _, _, _, ⟨_, h, _⟩ => by subst h; simp [Ty.blocks]
  | .tree _, _, _, ⟨_, rfl, h⟩ => h.2
  | .treeHeader _ _, _, _, ⟨_, rfl, _⟩ => by simp [Ty.blocks]

/-- A region apart from a value's regions lies apart from its arrays' words. -/
theorem Ty.Rep.reads_apart {mode : Mode} {heap : Heap} {store : Store Unit} :
    {t : Ty} → {ws : List Value} → {v : t.denote} → t.Rep mode heap store ws v →
      ∀ r, (∀ c ∈ t.regions mode store ws v, regionsDisjoint r c) →
      ∀ c ∈ t.reads store ws v, regionsDisjoint r c
  | .elem _, _, _, _, _, _, _, hc => by
    simp [Ty.reads] at hc
  | .bytes, _, _, _, r, hr, c, hc => by
    cases mode <;> exact hr c hc
  | .pair _ _, _, _, ⟨first, second, h, h1, h2, _⟩, r, hr, c, hc => by
    subst h
    rw [Ty.reads_append h1.length] at hc
    rw [Ty.regions_append h1.length] at hr
    rcases List.mem_append.mp hc with hc | hc
    · exact h1.reads_apart r (fun c' h' => hr c' (List.mem_append_left _ h')) c hc
    · exact h2.reads_apart r (fun c' h' => hr c' (List.mem_append_right _ h')) c hc
  | .array _, _, _, ⟨ptr, h, ha⟩, r, hr, c, hc => by
    subst h
    simp only [Ty.reads, List.mem_singleton] at hc
    subst hc
    cases mode
    · exact hr _ (by simp [Ty.regions, Ty.reads])
    · have := hr (block store ptr) (by simp [Ty.regions, Ty.blocks])
      exact regionsDisjoint_symm (Heap.Owned.region_apart ha (regionsDisjoint_symm this))
  | .tree _, _, value, ⟨ptr, rfl, ha⟩, r, hr, c, hc => by
    cases mode
    · exact hr c hc
    · exact regionsDisjoint_symm (NodeOwned.slotRegions_apart ptr value.toNode ha.1
        (fun b hb => regionsDisjoint_symm (hr b hb)) c hc)
  | .treeHeader _ _, _, _, _, _, _, _, hc => nomatch hc

/-- A value read where a borrowed one suffices. -/
theorem Ty.Rep.borrow {mode : Mode} {heap : Heap} {store : Store Unit} :
    {t : Ty} → {ws : List Value} → {v : t.denote} → t.Rep mode heap store ws v →
      t.Rep .borrowed heap store ws v
  | .elem _, _, _, h => h
  | .bytes, _, _, h => h
  | .pair _ _, _, _, ⟨first, second, h, h1, h2, _⟩ =>
    ⟨first, second, h, h1.borrow, h2.borrow, nofun⟩
  | .array _, _, _, ⟨ptr, h, ha⟩ => ⟨ptr, h, ha.borrow⟩
  | .tree _, _, _, ⟨ptr, h, ha⟩ => by
    refine ⟨ptr, h, ?_⟩
    cases mode
    · exact ha
    · exact ha.1.borrowed
  | .treeHeader _ _, _, _, ⟨ptr, h, _⟩ => ⟨ptr, h, trivial⟩

/-- A value whose type holds no arrays has the same words in either mode. -/
theorem Ty.Rep.owned {mode : Mode} {heap : Heap} {store : Store Unit} :
    {t : Ty} → t.scalar = true → {ws : List Value} → {v : t.denote} →
      t.Rep mode heap store ws v → t.Rep .owned heap store ws v
  | .elem _, _, _, _, h => h
  | .pair a _, hs, _, _, ⟨first, second, h, h1, h2, _⟩ =>
    ⟨first, second, h, h1.owned (Ty.scalar_pair hs).1, h2.owned (Ty.scalar_pair hs).2,
      fun _ x hx => by rw [a.blocks_scalar (Ty.scalar_pair hs).1] at hx; exact nomatch hx⟩
  | .array _, hs, _, _, _ => absurd hs Bool.false_ne_true

/-- The words of the values of a context, in order, the value of variable `i` held in mode
`modes i`. -/
def Env.Rep (modes : Nat → Mode) (heap : Heap) (store : Store Unit) :
    {Γ : List Ty} → List Value → Env Γ → Prop
  | _, ws, .nil => ws = []
  | _, ws, .cons (t := t) v env =>
    ∃ first rest, ws = first ++ rest ∧ t.Rep (modes 0) heap store first v ∧
      Env.Rep (fun i => modes (i + 1)) heap store rest env

/-- The addresses of the arrays of the owned values among the words `ws` of a context's values,
in order. -/
def Env.moves (store : Store Unit) (modes : Nat → Mode) : {Γ : List Ty} → List Value → Env Γ → List UInt64
  | _, _, .nil => []
  | _, ws, .cons (t := t) v env =>
    (match modes 0 with
      | .owned => t.pointers store (ws.take t.width) v
      | .borrowed => []) ++ Env.moves store (fun i => modes (i + 1)) (ws.drop t.width) env

/-- The regions of the arrays of the borrowed values among the words `ws` of a context's values,
in order. -/
def Env.reads (store : Store Unit) (modes : Nat → Mode) : {Γ : List Ty} → List Value → Env Γ → List (Nat × Nat)
  | _, _, .nil => []
  | _, ws, .cons (t := t) v env =>
    (match modes 0 with
      | .owned => []
      | .borrowed => t.reads store (ws.take t.width) v) ++
      Env.reads store (fun i => modes (i + 1)) (ws.drop t.width) env

theorem Env.moves_cons {store : Store Unit} {modes : Nat → Mode} {t : Ty} {Γ : List Ty} {v : t.denote} {env : Env Γ}
    {first rest : List Value} (h : first.length = t.width) :
    Env.moves store modes (first ++ rest) (.cons v env) =
      (match modes 0 with
        | .owned => t.pointers store first v
        | .borrowed => []) ++ Env.moves store (fun i => modes (i + 1)) rest env := by
  simp [Env.moves, ← h]

theorem Env.reads_cons {store : Store Unit} {modes : Nat → Mode} {t : Ty} {Γ : List Ty} {v : t.denote} {env : Env Γ}
    {first rest : List Value} (h : first.length = t.width) :
    Env.reads store modes (first ++ rest) (.cons v env) =
      (match modes 0 with
        | .owned => []
        | .borrowed => t.reads store first v) ++ Env.reads store (fun i => modes (i + 1)) rest env := by
  simp [Env.reads, ← h]

theorem widthSum_cons (t : Ty) (ts : List Ty) : widthSum (t :: ts) = t.width + widthSum ts := by
  simp [widthSum]

theorem Env.Rep.length {modes : Nat → Mode} {heap : Heap} {store : Store Unit} :
    {Γ : List Ty} → {ws : List Value} → {env : Env Γ} → Env.Rep modes heap store ws env →
      ws.length = widthSum Γ
  | _, _, .nil, h => by subst h; rfl
  | _, _, .cons _ _, h => by
    obtain ⟨_, _, h, h1, h2⟩ := h
    subst h; simp [widthSum_cons, h1.length, h2.length]

/-- How the verified compiler passes arguments: as the words of their values, each held in the
mode that `paramMode Γ ms` gives.  The call reads the borrowed values' arrays and consumes the
owned values' arrays. -/
@[instance_reducible] def Env.represent (Γ : List Ty) (ms : List Mode) : Represent (Env Γ) where
  width _ := widthSum Γ
  borrowed heap store vs env := Env.Rep (paramMode Γ ms) heap store vs env
  owned heap store vs env := Env.Rep (paramMode Γ ms) heap store vs env
  blocks _ _ _ := []
  reads store vs env := Env.reads store (paramMode Γ ms) vs env
  moves store vs env := Env.moves store (paramMode Γ ms) vs env

/-- How the verified compiler returns a value: as its words, owned by the caller. -/
@[instance_reducible] def Ty.represent (t : Ty) : Represent t.denote where
  width _ := t.width
  borrowed heap store vs v := t.Rep .borrowed heap store vs v
  owned heap store vs v := t.Rep .owned heap store vs v
  blocks store vs v := t.blocks store vs v
  reads _ _ _ := []
  moves _ _ _ := []


/-- An array after a step that keeps its region: it is still held in its mode, its region is the
same, and the region lies apart from the step's fresh blocks. -/
theorem Mode.array.step {mode : Mode} {heap heap' : Heap} {store store' : Store Unit}
    {keep : Nat × Nat → Prop} {fresh : List (Nat × Nat)} {ptr : UInt64} {xs : Array UInt64}
    (hStep : Step heap store keep heap' store' fresh) (h : mode.array heap store ptr xs)
    (hKeep : ∀ r ∈ (Ty.array .word).regions mode store [.i64 ptr] xs, keep r) :
    mode.array heap' store' ptr xs ∧
      (Ty.array .word).regions mode store' [.i64 ptr] xs =
        (Ty.array .word).regions mode store [.i64 ptr] xs ∧
      ∀ r ∈ (Ty.array .word).regions mode store [.i64 ptr] xs, ∀ b ∈ fresh,
        regionsDisjoint r b := by
  cases mode
  · obtain ⟨h1, h2⟩ := hStep.borrowed h (hKeep _ (List.mem_singleton_self _))
    refine ⟨h1, rfl, fun r hr => ?_⟩
    rw [List.mem_singleton.mp hr]
    exact h2
  · obtain ⟨⟨h1, hCap⟩, h2⟩ := hStep.owned h (hKeep _ (List.mem_singleton_self _))
    refine ⟨h1, ?_, fun r hr => ?_⟩
    · simp [Ty.regions, Ty.blocks, block_eq hCap]
    · rw [List.mem_singleton.mp hr]
      exact h2

/-- A value after a step that keeps its regions: its words still represent it, its regions are
the same, and they lie apart from the step's fresh blocks. -/
theorem Ty.Rep.step {mode : Mode} {heap heap' : Heap} {store store' : Store Unit}
    {keep : Nat × Nat → Prop} {fresh : List (Nat × Nat)}
    (hStep : Step heap store keep heap' store' fresh) :
    {t : Ty} → {ws : List Value} → {v : t.denote} → t.Rep mode heap store ws v →
      (∀ r ∈ t.regions mode store ws v, keep r) →
      t.Rep mode heap' store' ws v ∧ t.regions mode store' ws v = t.regions mode store ws v ∧
        ∀ r ∈ t.regions mode store ws v, ∀ b ∈ fresh, regionsDisjoint r b
  | .elem _, _, _, h, _ => ⟨h, by cases mode <;> rfl, by cases mode <;> exact nofun⟩
  | .bytes, _, value, ⟨root, length, rfl, h⟩, hKeep => by
    have hRegions : ∀ st, (Ty.bytes).regions mode st [.i64 root, .i64 length] value =
        Bytes.regions st root := by
      intro st
      cases mode <;> exact Bytes.roots_regions st root length
    obtain ⟨hRep, hSame, hFresh⟩ := h.step hStep (by simpa only [hRegions] using hKeep)
    exact ⟨⟨root, length, rfl, hRep⟩, by simpa only [hRegions] using hSame,
      by simpa only [hRegions] using hFresh⟩
  | .pair a b, _, p, ⟨first, second, rfl, h1, h2, hd⟩, hKeep => by
    have hl := h1.length
    rw [Ty.regions_append hl] at hKeep
    obtain ⟨r1, e1, f1⟩ := h1.step hStep fun r hr => hKeep r (List.mem_append_left _ hr)
    obtain ⟨r2, e2, f2⟩ := h2.step hStep fun r hr => hKeep r (List.mem_append_right _ hr)
    refine ⟨⟨first, second, rfl, r1, r2, fun hm x hx y hy => ?_⟩, ?_, ?_⟩
    · subst hm
      have e1' : a.blocks store' first p.1 = a.blocks store first p.1 := e1
      have e2' : b.blocks store' second p.2 = b.blocks store second p.2 := e2
      rw [e1'] at hx
      rw [e2'] at hy
      exact hd rfl x hx y hy
    · rw [Ty.regions_append hl, Ty.regions_append hl, e1, e2]
    · rw [Ty.regions_append hl]
      intro r hr
      rcases List.mem_append.mp hr with hr | hr
      · exact f1 r hr
      · exact f2 r hr
  | .array _, _, _, ⟨ptr, rfl, ha⟩, hKeep => by
    obtain ⟨h1, h2, h3⟩ := ha.step hStep hKeep
    exact ⟨⟨ptr, rfl, h1⟩, h2, h3⟩
  | .tree shape, _, value, ⟨ptr, rfl, ha⟩, hKeep => by
    cases mode
    · have hKept := fun r (hr : r ∈ value.toNode.slotRegions store ptr) =>
        hStep.keeps r (NodeBorrowed.regions ptr value.toNode ha r hr)
          (Node.slotRegions_pos value.toNode_slotted r hr) (hKeep r hr)
      obtain ⟨hNode, hRegions⟩ := NodeBorrowed.frame ptr value.toNode ha
        (fun r hr => ⟨(hKept r hr).1, (hKept r hr).2.1⟩)
      exact ⟨⟨ptr, rfl, hNode⟩, hRegions, fun r hr => (hKept r hr).2.2⟩
    · have hKept := fun r (hr : r ∈ value.toNode.blocks store ptr) =>
        hStep.keeps r (NodeOwned.regions ptr value.toNode ha.1 r hr)
          (Node.blocks_pos store ptr value.toNode r hr) (hKeep r hr)
      obtain ⟨hNode, hBlocks⟩ := NodeOwned.frame ptr value.toNode ha.1
        (fun r hr => ⟨(hKept r hr).1, (hKept r hr).2.1⟩)
      exact ⟨⟨ptr, rfl, hNode, by rw [hBlocks]; exact ha.2⟩, hBlocks,
        fun r hr => (hKept r hr).2.2⟩
  | .treeHeader shape r, _, _, ⟨ptr, rfl, ha⟩, hKeep => by
    cases mode
    · exact ⟨⟨ptr, rfl, trivial⟩, rfl, nofun⟩
    · have hKept := hStep.keeps (block store ptr) ha.region
        (by simp [block]) (hKeep _ (List.mem_singleton_self _))
      obtain ⟨words, hLength, hHead, hSlots⟩ := ha
      have hBase := hHead.base
      obtain ⟨hHeader, hCapacity⟩ :=
        TreeHeader.Owned.frame ⟨words, hLength, hHead, hSlots⟩
          (fun a hLow hHigh => hKept.1 a (by simp only [block]; omega)
            (by simp only [block]; omega)) hKept.2.1
      refine ⟨⟨ptr, rfl, hHeader⟩, ?_, ?_⟩
      · simp only [Ty.regions, Ty.blocks, block_eq hCapacity]
      · intro r hr
        change r ∈ [block store ptr] at hr
        rw [List.mem_singleton] at hr
        subst r
        exact hKept.2.2

theorem Ty.Rep.pointers_from_blocks {heap : Heap} {store : Store Unit} :
    {t : Ty} → {ws : List Value} → {v : t.denote} → t.Rep .owned heap store ws v →
      (t.blocks store ws v).map (fun b => UInt64.ofNat (b.1 + 48)) = t.pointers store ws v
  | .elem _, _, _, _ => rfl
  | .bytes, _, _, ⟨root, length, rfl, h⟩ => by
    rcases h.buffer with ⟨rfl, _⟩ | hBuffer
    · simp [Ty.blocks, Ty.pointers, Bytes.roots]
    · have hBase := hBuffer.object.base
      simp only [Ty.blocks, Ty.pointers, Bytes.roots, ite_eq_right hBuffer.nonzero,
        List.map_cons, List.map_nil, block_pointer (by omega : 48 ≤ root.toNat)]
  | .pair a b, _, value, ⟨first, second, rfl, ha, hb, _⟩ => by
    simp only [Ty.blocks, Ty.pointers, List.take_left' ha.length, List.drop_left' ha.length,
      List.map_append, ha.pointers_from_blocks, hb.pointers_from_blocks]
  | .array _, _, _, ⟨ptr, rfl, hOwned⟩ => by
    have hBase := hOwned.base
    simp only [Ty.blocks, Ty.pointers, List.map_cons, List.map_nil,
      block_pointer (by omega : 48 ≤ ptr.toNat)]
  | .tree _, _, value, ⟨ptr, rfl, hOwned, _⟩ =>
    NodeOwned.pointers_from_blocks ptr value.toNode hOwned
  | .treeHeader _ _, _, _, ⟨ptr, rfl, words, _, hHeader, _⟩ => by
    have hBase := hHeader.base
    simp only [Ty.blocks, Ty.pointers, List.map_cons, List.map_nil,
      block_pointer (by omega : 48 ≤ ptr.toNat)]

theorem Ty.Rep.pointers_step {heap heap' : Heap} {store store' : Store Unit}
    {keep : Nat × Nat → Prop} {fresh : List (Nat × Nat)} {t : Ty} {ws : List Value}
    {v : t.denote} (hRep : t.Rep .owned heap store ws v)
    (hStep : Step heap store keep heap' store' fresh)
    (hKeep : ∀ r ∈ t.blocks store ws v, keep r) :
    t.pointers store' ws v = t.pointers store ws v := by
  obtain ⟨hRep', hSame, _⟩ := hRep.step hStep hKeep
  change t.blocks store' ws v = t.blocks store ws v at hSame
  rw [← hRep'.pointers_from_blocks, ← hRep.pointers_from_blocks, hSame]

theorem Ty.types_length : (t : Ty) → t.types.length = t.width
  | .elem e => e.types_length
  | .array _ | .tree _ | .treeHeader _ _ => rfl
  | .bytes => rfl
  | .pair a b => by simp [Ty.types, Ty.width, a.types_length, b.types_length]

theorem Ty.Rep.typed {mode : Mode} {heap : Heap} {store : Store Unit} {t : Ty} {ws : List Value}
    {v : t.denote} (h : t.Rep mode heap store ws v) : ws.length = t.types.length := by
  rw [Ty.types_length]; exact h.length

/-- Positions that hold two lists in a row hold each. -/
theorem LocalsHold.append {s : Locals} {loc : Nat} {tys1 tys2 : List ValueType}
    {first second : List Value} (hl : first.length = tys1.length) :
    LocalsHold s loc (tys1 ++ tys2) (first ++ second) ↔
      LocalsHold s loc tys1 first ∧ LocalsHold s (loc + first.length) tys2 second := by
  constructor
  · intro h
    refine ⟨fun k hk => ?_, fun k hk => ?_⟩
    · have := h k (by simp; omega)
      rwa [List.getElem_append_left hk, List.getD_eq_getElem?_getD,
        List.getElem?_append_left (by omega), ← List.getD_eq_getElem?_getD] at this
    · have := h (first.length + k) (by simp; omega)
      rw [List.getElem_append_right (by omega), List.getD_eq_getElem?_getD,
        List.getElem?_append_right (by omega), ← List.getD_eq_getElem?_getD] at this
      rw [Nat.add_assoc]
      simpa [hl] using this
  · rintro ⟨h1, h2⟩ k hk
    by_cases hk1 : k < first.length
    · rw [List.getElem_append_left hk1, List.getD_eq_getElem?_getD,
        List.getElem?_append_left (by omega), ← List.getD_eq_getElem?_getD]
      exact h1 k hk1
    · rw [List.getElem_append_right (by omega), List.getD_eq_getElem?_getD,
        List.getElem?_append_right (by omega), ← hl, ← List.getD_eq_getElem?_getD]
      have := h2 (k - first.length) (by simp at hk; omega)
      rw [show loc + first.length + (k - first.length) = loc + k by omega] at this
      exact this

/-- A position that holds one i64 word holds it in its own local. -/
theorem LocalsHold.word {s : Locals} {loc : Nat} {w : Value} (h : LocalsHold s loc [.i64] [w]) :
    s.get loc = some w := by
  simpa [slotIndex] using h 0 (by simp)

/-- The positions of a tuple that hold its component at path `p`. -/
theorem Path.holds {s : Locals} : {e e' : Elem} → (p : Path e e') → {loc : Nat} → {v : e.denote} →
    LocalsHold s loc e.types (e.values v) →
    LocalsHold s (loc + p.offset) e'.types (e'.values (p.get v))
  | _, _, .here, _, _, h => by simpa [Path.offset, Path.get] using h
  | _, _, .fst (a := a) (b := b) p, loc, v, h => by
    have h' := ((LocalsHold.append (tys2 := b.types) (second := b.values v.2)
      (by rw [a.values_length, a.types_length])).mp h).1
    simpa [Path.offset, Path.get] using p.holds h'
  | _, _, .snd (a := a) (b := b) p, loc, v, h => by
    have h' := ((LocalsHold.append (tys1 := a.types) (first := a.values v.1)
      (by rw [a.values_length, a.types_length])).mp h).2
    rw [a.values_length] at h'
    simpa [Path.offset, Path.get, Nat.add_assoc] using p.holds h'

/-- Locals that agree below `base` hold the same words at positions below `base`. -/
theorem LocalsHold.frame {base : Nat} {s s' : Locals} (hF : Frame base s s') {loc : Nat}
    {tys : List ValueType} {ws : List Value} (hl : ws.length = tys.length)
    (hb : loc + tys.length ≤ base) : LocalsHold s' loc tys ws ↔ LocalsHold s loc tys ws := by
  have hSame : ∀ k < ws.length, ∀ ty,
      s'.get (slotIndex s'.positions (loc + k) ty) = s.get (slotIndex s.positions (loc + k) ty) := by
    intro k hk ty
    rw [hF.positions]
    exact hF.slot (by omega) ty
  constructor
  · intro hold k hk
    rw [← hSame k hk]
    exact hold k hk
  · intro hold k hk
    rw [hSame k hk]
    exact hold k hk

/-- Words at positions that a change of locals keeps stay held. -/
theorem LocalsHold.keep {s s' : Locals} {lo loc : Nat} {tys : List ValueType} {ws : List Value}
    (hold : LocalsHold s loc tys ws) (hHalf : s'.positions = s.positions)
    (hKeep : ∀ j, lo ≤ j → j < s.positions →
      s'.get j = s.get j ∧ s'.get (j + s.positions) = s.get (j + s.positions) ∧
        s'.get (j + 2 * s.positions) = s.get (j + 2 * s.positions))
    (hLo : lo ≤ loc) (hHi : loc + ws.length ≤ s.positions) : LocalsHold s' loc tys ws := by
  intro k hk
  have ha := hKeep (loc + k) (by omega) (by omega)
  have hk' := hold k hk
  rw [hHalf]
  revert hk'
  cases tys.getD k .i64 <;> simp only [slotIndex] <;> intro hk' <;>
    first | (rw [ha.1]; exact hk') | (rw [ha.2.1]; exact hk') | (rw [ha.2.2]; exact hk')

/-- Positions that hold words of given types and length determine them. -/
theorem LocalsHold.unique {s : Locals} {loc : Nat} {tys : List ValueType} {ws1 ws2 : List Value}
    (h1 : LocalsHold s loc tys ws1) (h2 : LocalsHold s loc tys ws2)
    (hl : ws1.length = ws2.length) : ws1 = ws2 := by
  apply List.ext_getElem hl
  intro k hk1 hk2
  have := (h1 k hk1).symm.trans (h2 k hk2)
  exact Option.some.inj this

theorem Var.index_lt {Γ : List Ty} {t : Ty} (x : Var Γ t) : x.index < Γ.length := by
  induction x with
  | here => simp [Var.index]
  | there y ih => simp [Var.index]; omega

theorem Var.getElem?_index {Γ : List Ty} {t : Ty} : (x : Var Γ t) → Γ[x.index]? = some t
  | .here => rfl
  | .there x => by simp [Var.index, x.getElem?_index]

theorem Var.index_ofIndex : (Γ : List Ty) → (i : Nat) → {t : Ty} → (h : Γ[i]? = some t) →
    (Var.ofIndex Γ i h).index = i
  | _ :: _, 0, _, h => by simp at h; subst h; rfl
  | _ :: Γ, i + 1, _, h => by
    simp only [Var.ofIndex, Var.index]
    rw [Var.index_ofIndex Γ i]
  | [], _, _, h => by simp at h

/-- The facts about the variables live in `live`.  Each starts at its slot's local, its words end
below `base`, and its locals hold words that represent its value in its mode in `heap` at
`store`.  The blocks of a live owned variable lie apart from the regions of every other live
variable: from its blocks when it is owned and from its arrays when it is borrowed. -/
def Holds {Γ : List Ty} (env : Env Γ) (slots : List Slot) (live : Nat → Bool) (base : Nat)
    (heap : Heap) (store : Store Unit) (s : Locals) : Prop :=
  (∀ (t : Ty) (x : Var Γ t), live x.index = true →
    (slots.getD x.index default).loc + t.width ≤ base ∧
    ∃ ws, LocalsHold s (slots.getD x.index default).loc t.types ws ∧
      t.Rep (slots.getD x.index default).mode heap store ws (env.get x)) ∧
  ∀ (t u : Ty) (x : Var Γ t) (y : Var Γ u), live x.index = true → live y.index = true →
    x.index ≠ y.index → (slots.getD x.index default).mode = .owned →
    ∀ wx wy, LocalsHold s (slots.getD x.index default).loc t.types wx → wx.length = t.width →
      LocalsHold s (slots.getD y.index default).loc u.types wy → wy.length = u.width →
      ∀ b ∈ t.blocks store wx (env.get x),
        ∀ c ∈ u.regions (slots.getD y.index default).mode store wy (env.get y), regionsDisjoint b c

/-- A value lies apart from the variables live in `live`: its regions lie apart from those of
each live variable when either is owned. -/
def Holds.Apart {Γ : List Ty} (env : Env Γ) (slots : List Slot) (live : Nat → Bool)
    (store : Store Unit) (s : Locals) (t : Ty) (mode : Mode) (ws : List Value) (v : t.denote) :
    Prop :=
  ∀ (u : Ty) (y : Var Γ u), live y.index = true →
    (mode = .owned ∨ (slots.getD y.index default).mode = .owned) →
    ∀ wy, LocalsHold s (slots.getD y.index default).loc u.types wy → wy.length = u.width →
      ∀ b ∈ t.regions mode store ws v,
        ∀ c ∈ u.regions (slots.getD y.index default).mode store wy (env.get y), regionsDisjoint b c

/-- The region `r` lies apart from the blocks of the owned variables live in `liveIn` and not in
`liveOut`, those that die between the two. -/
def Holds.KeepDying {Γ : List Ty} (env : Env Γ) (slots : List Slot) (liveIn liveOut : Nat → Bool)
    (store : Store Unit) (s : Locals) (r : Nat × Nat) : Prop :=
  ∀ (t : Ty) (x : Var Γ t), liveIn x.index = true → liveOut x.index = false →
    (slots.getD x.index default).mode = .owned →
    ∀ wx, LocalsHold s (slots.getD x.index default).loc t.types wx → wx.length = t.width →
      ∀ b ∈ t.blocks store wx (env.get x), regionsDisjoint r b

namespace Holds

variable {Γ : List Ty} {env : Env Γ} {slots : List Slot} {live : Nat → Bool} {base : Nat}
  {heap : Heap} {store : Store Unit} {s : Locals}

/-- The words of a live variable. -/
theorem get (h : Holds env slots live base heap store s) {t : Ty} (x : Var Γ t)
    (hx : live x.index = true) :
    (slots.getD x.index default).loc + t.width ≤ base ∧
    ∃ ws, LocalsHold s (slots.getD x.index default).loc t.types ws ∧
      t.Rep (slots.getD x.index default).mode heap store ws (env.get x) :=
  h.1 t x hx

/-- `Holds` for fewer variables. -/
theorem live_mono (h : Holds env slots live base heap store s) {live' : Nat → Bool}
    (hLive : ∀ i, live' i = true → live i = true) : Holds env slots live' base heap store s :=
  ⟨fun t x hx => h.1 t x (hLive _ hx),
    fun t u x y hx hy => h.2 t u x y (hLive _ hx) (hLive _ hy)⟩

/-- `Holds` for fewer variables, compared on the indices of variables. -/
theorem live_mono' (h : Holds env slots live base heap store s) {live' : Nat → Bool}
    (hLive : ∀ i < Γ.length, live' i = true → live i = true) :
    Holds env slots live' base heap store s :=
  ⟨fun t x hx => h.1 t x (hLive _ x.index_lt hx),
    fun t u x y hx hy => h.2 t u x y (hLive _ x.index_lt hx) (hLive _ y.index_lt hy)⟩

theorem mono (h : Holds env slots live base heap store s) {base' : Nat} (hb : base ≤ base') :
    Holds env slots live base' heap store s :=
  ⟨fun t x hx => ⟨by have := (h.1 t x hx).1; omega, (h.1 t x hx).2⟩, h.2⟩

/-- Locals that agree below `base` hold the same words for a live variable. -/
theorem hold_agree (h : Holds env slots live base heap store s) {s' : Locals}
    (hF : Frame base s s') {t : Ty} {x : Var Γ t} (hx : live x.index = true)
    {ws : List Value} (hl : ws.length = t.width) :
    LocalsHold s' (slots.getD x.index default).loc t.types ws ↔
      LocalsHold s (slots.getD x.index default).loc t.types ws := by
  have hBelow := (h.1 t x hx).1
  have hSame : ∀ k < ws.length, ∀ ty,
      s'.get (slotIndex s'.positions ((slots.getD x.index default).loc + k) ty) =
        s.get (slotIndex s.positions ((slots.getD x.index default).loc + k) ty) := by
    intro k hk ty
    rw [hF.positions]
    exact hF.slot (by omega) ty
  constructor
  · intro hold k hk
    rw [← hSame k hk]
    exact hold k hk
  · intro hold k hk
    rw [hSame k hk]
    exact hold k hk

/-- `Holds` with a lower bound for the variables' locals, which another `Holds` gives. -/
theorem lower {base' : Nat} (h : Holds env slots live base' heap store s) {live0 : Nat → Bool}
    {heap0 : Heap} {store0 : Store Unit} {s0 : Locals}
    (h0 : Holds env slots live0 base heap0 store0 s0)
    (hLive : ∀ i, live i = true → live0 i = true) : Holds env slots live base heap store s :=
  ⟨fun t x hx => ⟨(h0.1 t x (hLive _ hx)).1, (h.1 t x hx).2⟩, h.2⟩

/-- `Holds` depends only on the locals below `base`. -/
theorem agree (h : Holds env slots live base heap store s) {s' : Locals}
    (hs : Frame base s s') : Holds env slots live base heap store s' := by
  refine ⟨fun t x hx => ?_, fun t u x y hx hy hxy hm wx wy hwx hlx hwy hly => ?_⟩
  · obtain ⟨hBelow, ws, hold, hRep⟩ := h.1 t x hx
    exact ⟨hBelow, ws, (h.hold_agree hs hx hRep.length).mpr hold, hRep⟩
  · exact h.2 t u x y hx hy hxy hm wx wy ((h.hold_agree hs hx hlx).mp hwx) hlx
      ((h.hold_agree hs hy hly).mp hwy) hly

theorem frame (h : Holds env slots live base heap store s) {base' : Nat} {s' : Locals}
    (hf : Frame base' s s') (hb : base ≤ base') : Holds env slots live base heap store s' :=
  h.agree (hf.mono hb)

theorem setLocal (h : Holds env slots live base heap store s) {i : Nat} {v : Value}
    (hi : base ≤ i) (hLow : s.params.length ≤ i) (hHigh : i < s.positions) :
    Holds env slots live base heap store (Verified.setLocal s i v) :=
  h.agree (Frame.set hLow hi hHigh)

/-- The regions of each variable live in `live` lie apart from the blocks of the owned variables
that die between `liveIn` and `live`. -/
theorem keepDying {liveIn : Nat → Bool} (h : Holds env slots liveIn base heap store s)
    (hLive : ∀ i, live i = true → liveIn i = true) {u : Ty} {y : Var Γ u}
    (hy : live y.index = true) {wy : List Value}
    (hwy : LocalsHold s (slots.getD y.index default).loc u.types wy) (hly : wy.length = u.width) :
    ∀ c ∈ u.regions (slots.getD y.index default).mode store wy (env.get y),
      KeepDying env slots liveIn live store s c := by
  intro c hc t x hx hxOut hm wx hwx hlx b hb
  have hne : x.index ≠ y.index := fun he => by rw [he, hy] at hxOut; exact nomatch hxOut
  exact regionsDisjoint_symm (h.2 t u x y hx (hLive _ hy) hne hm wx wy hwx hlx hwy hly b hb c hc)

/-- `Holds` after a step that keeps the regions of the live variables. -/
theorem step (h : Holds env slots live base heap store s) {keep : Nat × Nat → Prop}
    {heap' : Heap} {store' : Store Unit} {fresh : List (Nat × Nat)}
    (hStep : Step heap store keep heap' store' fresh)
    (hKeep : ∀ (u : Ty) (y : Var Γ u), live y.index = true → ∀ wy,
      LocalsHold s (slots.getD y.index default).loc u.types wy → wy.length = u.width →
      ∀ c ∈ u.regions (slots.getD y.index default).mode store wy (env.get y), keep c) :
    Holds env slots live base heap' store' s := by
  -- The regions of each live variable are the same after the step.
  have hSame : ∀ (u : Ty) (y : Var Γ u), live y.index = true → ∀ wy,
      LocalsHold s (slots.getD y.index default).loc u.types wy → wy.length = u.width →
      u.regions (slots.getD y.index default).mode store' wy (env.get y) =
        u.regions (slots.getD y.index default).mode store wy (env.get y) := by
    intro u y hy wy hwy hly
    obtain ⟨_, ws, hold, hRep⟩ := h.1 u y hy
    obtain rfl := LocalsHold.unique hwy hold (hly.trans hRep.length.symm)
    exact (hRep.step hStep (hKeep u y hy _ hwy hly)).2.1
  refine ⟨fun t x hx => ?_, fun t u x y hx hy hxy hm wx wy hwx hlx hwy hly b hb c hc => ?_⟩
  · obtain ⟨hBelow, ws, hold, hRep⟩ := h.1 t x hx
    exact ⟨hBelow, ws, hold, (hRep.step hStep (hKeep t x hx ws hold hRep.length)).1⟩
  · have hbx := hSame t x hx wx hwx hlx
    have hcy := hSame u y hy wy hwy hly
    simp only [Ty.regions, hm] at hbx
    rw [hbx] at hb
    rw [hcy] at hc
    exact h.2 t u x y hx hy hxy hm wx wy hwx hlx hwy hly b hb c hc

/-- A binding adds its value, in the locals from `base` on in mode `mode`, as variable 0, when
the value lies apart from the variables live in the body. -/
theorem push {t : Ty} {v : t.denote} {mode : Mode} {live' : Nat → Bool}
    (h : Holds env slots (fun i => live' (i + 1)) base heap store s) {ws : List Value}
    (hold : LocalsHold s base t.types ws) (hRep : t.Rep mode heap store ws v)
    (hApart : Holds.Apart env slots (fun i => live' (i + 1)) store s t mode ws v) :
    Holds (Env.cons v env) (⟨base, mode⟩ :: slots) live' (base + t.width) heap store s := by
  refine ⟨fun t' x hx => ?_, fun t1 t2 x y hx hy hxy hm wx wy hwx hlx hwy hly => ?_⟩
  · cases x with
    | here => exact ⟨by simp [Var.index], ws, by simpa [Var.index] using hold,
        by simpa [Var.index, Env.get] using hRep⟩
    | there y =>
      simp only [Var.index, Env.get, List.getD_cons_succ]
      obtain ⟨hBelow, rest⟩ := h.1 _ y hx
      exact ⟨by omega, rest⟩
  · cases x with
    | here =>
      cases y with
      | here => exact absurd rfl hxy
      | there y =>
        change mode = .owned at hm
        change LocalsHold s base t.types wx at hwx
        change LocalsHold s (slots.getD y.index default).loc t2.types wy at hwy
        obtain rfl := LocalsHold.unique hwx hold (hlx.trans hRep.length.symm)
        subst hm
        exact hApart _ y hy (Or.inl rfl) wy hwy hly
    | there x =>
      cases y with
      | here =>
        change (slots.getD x.index default).mode = .owned at hm
        change LocalsHold s (slots.getD x.index default).loc t1.types wx at hwx
        change LocalsHold s base t.types wy at hwy
        obtain rfl := LocalsHold.unique hwy hold (hly.trans hRep.length.symm)
        intro b hb c hc
        have hRegions : t1.regions (slots.getD x.index default).mode store wx (env.get x) =
            t1.blocks store wx (env.get x) := by rw [hm]; rfl
        exact regionsDisjoint_symm (hApart _ x hx (Or.inr hm) wx hwx hlx c hc b
          (hRegions ▸ hb))
      | there y =>
        change (slots.getD x.index default).mode = .owned at hm
        change LocalsHold s (slots.getD x.index default).loc t1.types wx at hwx
        change LocalsHold s (slots.getD y.index default).loc t2.types wy at hwy
        exact h.2 t1 t2 x y hx hy (fun he => hxy (by simp [Var.index, he])) hm wx wy hwx hlx hwy
          hly

/-- The facts about the variables of a context without its first variable. -/
theorem pop {t : Ty} {v : t.denote} {sl : Slot} {live' : Nat → Bool}
    (h : Holds (Env.cons v env) (sl :: slots) live' base heap store s) :
    Holds env slots (fun i => live' (i + 1)) base heap store s :=
  ⟨fun t' x hx => h.1 t' (.there x) hx,
    fun t1 t2 x y hx hy hxy hm => h.2 t1 t2 (.there x) (.there y) hx hy
      (fun he => hxy (Nat.succ.inj he)) hm⟩

/-- The regions of a live variable after a step that keeps them are the same, and the variable
still holds its value. -/
theorem regions_after (h : Holds env slots live base heap store s) {keep : Nat × Nat → Prop}
    {heap' : Heap} {store' : Store Unit} {fresh : List (Nat × Nat)}
    (hStep : Step heap store keep heap' store' fresh) {u : Ty} {y : Var Γ u}
    (hy : live y.index = true) {wy : List Value}
    (hwy : LocalsHold s (slots.getD y.index default).loc u.types wy) (hly : wy.length = u.width)
    (hKeep : ∀ c ∈ u.regions (slots.getD y.index default).mode store wy (env.get y), keep c) :
    u.regions (slots.getD y.index default).mode store' wy (env.get y) =
        u.regions (slots.getD y.index default).mode store wy (env.get y) ∧
      ∀ c ∈ u.regions (slots.getD y.index default).mode store wy (env.get y),
        ∀ b ∈ fresh, regionsDisjoint c b := by
  obtain ⟨_, ws, hold, hRep⟩ := h.1 u y hy
  obtain rfl := LocalsHold.unique hwy hold (hly.trans hRep.length.symm)
  obtain ⟨-, h2, h3⟩ := hRep.step hStep hKeep
  exact ⟨h2, h3⟩

end Holds

/-- The blocks that a value occupies when owned, and none when borrowed: those that its holder
must consume. -/
def Mode.fresh (mode : Mode) (store : Store Unit) (t : Ty) (ws : List Value) (v : t.denote) :
    List (Nat × Nat) :=
  match mode with
  | .owned => t.blocks store ws v
  | .borrowed => []

namespace Holds

variable {Γ : List Ty} {env : Env Γ} {slots : List Slot} {live : Nat → Bool} {base : Nat}
  {heap : Heap} {store : Store Unit} {s : Locals}

/-- `Holds` for live sets that agree on the indices of variables. -/
theorem congr_live (h : Holds env slots live base heap store s) {live' : Nat → Bool}
    (hL : ∀ i < Γ.length, live' i = true → live i = true) :
    Holds env slots live' base heap store s :=
  h.live_mono' hL

theorem KeepDying.congr {liveIn liveOut liveIn' liveOut' : Nat → Bool} {r : Nat × Nat}
    (h : KeepDying env slots liveIn liveOut store s r)
    (hSub : ∀ i < Γ.length, liveIn' i = true → liveOut' i = false →
      liveIn i = true ∧ liveOut i = false) :
    KeepDying env slots liveIn' liveOut' store s r :=
  fun t x hx hxo hm => let ⟨a, b⟩ := hSub _ x.index_lt hx hxo; h t x a b hm

theorem Apart.live_mono {t : Ty} {mode : Mode} {ws : List Value} {v : t.denote}
    (h : Holds.Apart env slots live store s t mode ws v) {live' : Nat → Bool}
    (hLive : ∀ i, live' i = true → live i = true) :
    Holds.Apart env slots live' store s t mode ws v :=
  fun u y hy => h u y (hLive _ hy)

/-- A value apart from the variables of a context is apart from those after its first. -/
theorem Apart.pop {t u : Ty} {v : u.denote} {sl : Slot} {live' : Nat → Bool} {mode : Mode}
    {ws : List Value} {w : t.denote}
    (h : Holds.Apart (Env.cons v env) (sl :: slots) live' store s t mode ws w) :
    Holds.Apart env slots (fun i => live' (i + 1)) store s t mode ws w :=
  fun u y hy => h u (.there y) hy

/-- A value without arrays lies apart from every variable. -/
theorem Apart.ofScalar {t : Ty} {mode : Mode} {ws : List Value} {v : t.denote}
    (h : t.scalar = true) : Holds.Apart env slots live store s t mode ws v :=
  fun _ _ _ _ _ _ _ b hb => by rw [Ty.regions_scalar t h] at hb; exact nomatch hb

/-- A pair apart from the live variables has each component apart from them. -/
theorem Apart.fst {a b : Ty} {mode : Mode} {first second : List Value}
    {p : a.denote × b.denote}
    (h : Holds.Apart env slots live store s (.pair a b) mode (first ++ second) p)
    (hl : first.length = a.width) : Holds.Apart env slots live store s a mode first p.1 :=
  fun u y hy hm wy hwy hly x hx c hc => h u y hy hm wy hwy hly x
    (by rw [Ty.regions_append hl]; exact List.mem_append_left _ hx) c hc

theorem Apart.snd {a b : Ty} {mode : Mode} {first second : List Value}
    {p : a.denote × b.denote}
    (h : Holds.Apart env slots live store s (.pair a b) mode (first ++ second) p)
    (hl : first.length = a.width) : Holds.Apart env slots live store s b mode second p.2 :=
  fun u y hy hm wy hwy hly x hx c hc => h u y hy hm wy hwy hly x
    (by rw [Ty.regions_append hl]; exact List.mem_append_right _ hx) c hc

/-- A value apart from the variables of a context and from a new variable 0, in the locals from
`loc` on in mode `mv`, is apart from the variables of the context with it. -/
theorem Apart.push {t u : Ty} {v : u.denote} {loc : Nat} {mv mode : Mode} {live' : Nat → Bool}
    {ws wv : List Value} {w : t.denote}
    (h : Holds.Apart env slots (fun i => live' (i + 1)) store s t mode ws w)
    (hold : LocalsHold s loc u.types wv) (hl : wv.length = u.width)
    (hHere : mode = .owned ∨ mv = .owned →
      ∀ b ∈ t.regions mode store ws w, ∀ c ∈ u.regions mv store wv v, regionsDisjoint b c) :
    Holds.Apart (Env.cons v env) (⟨loc, mv⟩ :: slots) live' store s t mode ws w := by
  intro u' y hy hm wy hwy hly
  cases y with
  | here =>
    change LocalsHold s loc u.types wy at hwy
    obtain rfl := LocalsHold.unique hwy hold (hly.trans hl.symm)
    exact hHere hm
  | there y => exact h u' y hy hm wy hwy hly

/-- A value apart from the live variables stays apart in locals that agree below `base`. -/
theorem Apart.agree (h : Holds env slots live base heap store s) {t : Ty} {mode : Mode}
    {ws : List Value} {v : t.denote} (hApart : Holds.Apart env slots live store s t mode ws v)
    {s' : Locals} (hs : Frame base s s') :
    Holds.Apart env slots live store s' t mode ws v :=
  fun u y hy hm wy hwy hly => hApart u y hy hm wy ((h.hold_agree hs hy hly).mp hwy) hly

/-- Every region lies apart from the blocks of the variables that die where none dies. -/
theorem KeepDying.none {live : Nat → Bool} {r : Nat × Nat} :
    KeepDying env slots live live store s r :=
  fun _ _ hx hxo => by rw [hx] at hxo; exact nomatch hxo

theorem KeepDying.mono {liveIn liveOut liveIn' liveOut' : Nat → Bool} {r : Nat × Nat}
    (h : KeepDying env slots liveIn liveOut store s r)
    (hSub : ∀ i, liveIn' i = true → liveOut' i = false → liveIn i = true ∧ liveOut i = false) :
    KeepDying env slots liveIn' liveOut' store s r :=
  fun t x hx hxo hm => let ⟨a, b⟩ := hSub _ hx hxo; h t x a b hm

/-- The facts that carry from a state to the one after a subexpression's step: when the step
keeps the regions of the variables live after it, those regions are unchanged.  So a region
apart from the blocks of variables that die later is apart from them in either state. -/
theorem KeepDying.transfer (h : Holds env slots live base heap store s)
    {liveIn liveOut liveMid : Nat → Bool} {heap1 : Heap} {store1 : Store Unit} {s1 : Locals}
    {fresh : List (Nat × Nat)}
    (hStep : Step heap store (KeepDying env slots live liveMid store s) heap1 store1 fresh)
    (hFrame : Frame base s s1) (hMid : ∀ i, liveMid i = true → live i = true)
    (hSub : ∀ i, liveIn i = true → liveOut i = false → liveMid i = true) {r : Nat × Nat}
    (hr : KeepDying env slots liveIn liveOut store s r) :
    KeepDying env slots liveIn liveOut store1 s1 r := by
  intro t x hx hxo hm wx hwx hlx b hb
  have hxMid := hSub _ hx hxo
  have hwx' := (h.live_mono hMid |>.hold_agree hFrame hxMid hlx).mp hwx
  have hSame := (h.regions_after hStep (hMid _ hxMid) hwx' hlx
    (h.keepDying hMid hxMid hwx' hlx)).1
  simp only [Ty.regions, hm] at hSame
  rw [hSame] at hb
  exact hr t x hx hxo hm wx hwx' hlx b hb

/-- A value apart from the live variables stays apart after a step that keeps its regions and
theirs. -/
theorem Apart.transfer (h : Holds env slots live base heap store s) {t : Ty} {mode : Mode}
    {ws : List Value} {v : t.denote} (hApart : Holds.Apart env slots live store s t mode ws v)
    {keep : Nat × Nat → Prop} {heap1 : Heap} {store1 : Store Unit} {s1 : Locals}
    {fresh : List (Nat × Nat)} (hStep : Step heap store keep heap1 store1 fresh)
    (hFrame : Frame base s s1)
    (hKeep : ∀ (u : Ty) (y : Var Γ u), live y.index = true → ∀ wy,
      LocalsHold s (slots.getD y.index default).loc u.types wy → wy.length = u.width →
      ∀ c ∈ u.regions (slots.getD y.index default).mode store wy (env.get y), keep c)
    (hSame : t.regions mode store1 ws v = t.regions mode store ws v) :
    Holds.Apart env slots live store1 s1 t mode ws v := by
  intro u y hy hm wy hwy hly b hb c hc
  have hwy' := (h.hold_agree hFrame hy hly).mp hwy
  have := (h.regions_after hStep hy hwy' hly (hKeep u y hy wy hwy' hly)).1
  rw [this] at hc
  rw [hSame] at hb
  exact hApart u y hy hm wy hwy' hly b hb c hc

end Holds


/-! The instances that Lean synthesizes for the source types, rebuilt by recursion over `Ty`, and
their agreement with the verified compiler's representation.  A function's theorem for Lean's
types follows from them, for every signature, without a proof per signature. -/

/-- The `Scalar` instance that Lean synthesizes for an element type. -/
@[instance_reducible] def Elem.scalarInst : (e : Elem) → Scalar e.denote
  | .word => instScalarUInt64
  | .bool => @instScalarOfFlat Bool UInt64 instFlatBoolUInt64 instScalarUInt64
  | .float => instScalarFloat
  | .float32 => instScalarFloat32
  | .prod a b => @instScalarProd a.denote b.denote a.scalarInst b.scalarInst

theorem Elem.scalar_values : (e : Elem) → (v : e.denote) →
    @Scalar.values _ e.scalarInst v = e.values v
  | .word, _ | .bool, _ | .float, _ | .float32, _ => rfl
  | .prod a b, v => by
    show @Scalar.values _ a.scalarInst v.1 ++ @Scalar.values _ b.scalarInst v.2 = _
    rw [a.scalar_values, b.scalar_values]
    rfl

/-- The instance for an array of tuples, for which Lean has none: the array of its elements'
words, as for an array of a `Flat` type. -/
@[instance_reducible] def Elem.wordsInst (e : Elem) : Represent (Array e.denote) where
  width _ := 1
  borrowed heap store vs xs := Represent.borrowed heap store vs (e.words xs)
  owned heap store vs xs := Represent.owned heap store vs (e.words xs)
  blocks store vs xs := Represent.blocks store vs (e.words xs)
  reads store vs xs := Represent.reads store vs (e.words xs)
  moves _ _ _ := []

/-- The instance for an array of tuples that the caller hands over. -/
@[instance_reducible] def Elem.movedWordsInst (e : Elem) : Represent (Moved (Array e.denote)) where
  width _ := 1
  borrowed heap store vs xs := Represent.borrowed heap store vs (Moved.mk (e.words xs.val))
  owned heap store vs xs := Represent.owned heap store vs (Moved.mk (e.words xs.val))
  blocks store vs xs := Represent.blocks store vs (Moved.mk (e.words xs.val))
  reads _ _ _ := []
  moves store vs xs := Represent.moves store vs (Moved.mk (e.words xs.val))

/-- The `Represent` instance for an array of element type `e`: Lean's for arrays of words, `Bool`s,
and floats, and `wordsInst` for arrays of tuples. -/
@[instance_reducible] def Elem.arrayInst : (e : Elem) → Represent (Array e.denote)
  | .word => instRepresentArrayUInt64
  | .bool => @instRepresentArrayOfFlatOfScalar Bool UInt64 instFlatBoolUInt64 instScalarUInt64
  | .float => instRepresentArrayFloat
  | .float32 => instRepresentArrayFloat32
  | .prod a b => Elem.wordsInst (.prod a b)

/-- The `Represent` instance for an owned array argument of element type `e`. -/
@[instance_reducible] def Elem.movedInst : (e : Elem) → Represent (Moved (Array e.denote))
  | .word => instRepresentMovedArrayUInt64
  | .bool => @instRepresentMovedArrayOfFlatOfScalar Bool UInt64 instFlatBoolUInt64 instScalarUInt64
  | .float => instRepresentMovedArrayFloat
  | .float32 => instRepresentMovedArrayFloat32
  | .prod a b => Elem.movedWordsInst (.prod a b)

theorem Elem.arrayInst_borrowed {heap : Heap} {store : Store Unit} {ws : List Value} :
    (e : Elem) → {xs : Array e.denote} →
      (@Represent.borrowed _ e.arrayInst heap store ws xs ↔
        (Ty.array e).Rep .borrowed heap store ws xs)
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => Iff.rfl

theorem Elem.arrayInst_owned {heap : Heap} {store : Store Unit} {ws : List Value} :
    (e : Elem) → {xs : Array e.denote} →
      (@Represent.owned _ e.arrayInst heap store ws xs ↔ (Ty.array e).Rep .owned heap store ws xs)
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => Iff.rfl

theorem Elem.arrayInst_width : (e : Elem) → (xs : Array e.denote) →
    @Represent.width _ e.arrayInst xs = 1
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => rfl

theorem Elem.arrayInst_blocks {store : Store Unit} {ws : List Value} : (e : Elem) →
    {xs : Array e.denote} →
      @Represent.blocks _ e.arrayInst store ws xs = (Ty.array e).blocks store ws xs
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => rfl

theorem Elem.arrayInst_reads {store : Store Unit} {ws : List Value} : (e : Elem) →
    {xs : Array e.denote} → @Represent.reads _ e.arrayInst store ws xs = (Ty.array e).reads store ws xs
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => rfl

theorem Elem.arrayInst_moves {store : Store Unit} {ws : List Value} : (e : Elem) →
    {xs : Array e.denote} → @Represent.moves _ e.arrayInst store ws xs = []
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => rfl

theorem Elem.movedInst_borrowed {heap : Heap} {store : Store Unit} {ws : List Value} :
    (e : Elem) → {xs : Moved (Array e.denote)} →
      (@Represent.borrowed _ e.movedInst heap store ws xs ↔
        (Ty.array e).Rep .owned heap store ws xs.val)
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => Iff.rfl

theorem Elem.movedInst_width : (e : Elem) → (xs : Moved (Array e.denote)) →
    @Represent.width _ e.movedInst xs = 1
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => rfl

theorem Elem.movedInst_moves {store : Store Unit} {ws : List Value} : (e : Elem) →
    {xs : Moved (Array e.denote)} →
      @Represent.moves _ e.movedInst store ws xs = (Ty.array e).pointers store ws xs.val
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => rfl

theorem Elem.movedInst_reads {store : Store Unit} {ws : List Value} : (e : Elem) →
    {xs : Moved (Array e.denote)} → @Represent.reads _ e.movedInst store ws xs = []
  | .word, _ | .bool, _ | .float, _ | .float32, _ | .prod _ _, _ => rfl

/-- The `Scalar` instance that Lean synthesizes for a type without arrays. -/
@[instance_reducible] def Ty.scalarInst : (t : Ty) → t.scalar = true → Scalar t.denote
  | .elem e, _ => e.scalarInst
  | .pair a b, h => @instScalarProd a.denote b.denote (a.scalarInst (Ty.scalar_pair h).1)
      (b.scalarInst (Ty.scalar_pair h).2)
  | .array _, h => absurd h Bool.false_ne_true

/-- The `Represent` instance that Lean synthesizes for a type: the one from `Scalar` for a type
without arrays, and the instances for pairs and arrays otherwise. -/
@[instance_reducible] def Ty.leanInst : (t : Ty) → Represent t.denote
  | .elem e => @instRepresentOfScalar _ e.scalarInst
  | .pair a b =>
    if h : (Ty.pair a b).scalar = true then
      @instRepresentOfScalar _ ((Ty.pair a b).scalarInst h)
    else @instRepresentProd _ _ a.leanInst b.leanInst
  | .array e => e.arrayInst
  | .bytes => inferInstanceAs (Represent LeanExe.Bytes)
  | .tree shape => inferInstanceAs (Represent (Tree shape))
  | .treeHeader shape r => inferInstanceAs (Represent (TreeHeader shape r))

/-- The words of a value of a type without arrays. -/
theorem Ty.scalar_rep {mode : Mode} {heap : Heap} {store : Store Unit} :
    (t : Ty) → (h : t.scalar = true) → {ws : List Value} → {v : t.denote} →
      (ws = @Scalar.values _ (t.scalarInst h) v ↔ t.Rep mode heap store ws v)
  | .elem e, _, ws, v => by
    show ws = @Scalar.values _ e.scalarInst v ↔ ws = e.values v
    rw [e.scalar_values]
  | .pair a b, h, ws, p => by
    constructor
    · rintro rfl
      exact ⟨_, _, rfl, (a.scalar_rep (Ty.scalar_pair h).1).mp rfl,
        (b.scalar_rep (Ty.scalar_pair h).2).mp rfl, fun _ x hx => by
          rw [a.blocks_scalar (Ty.scalar_pair h).1] at hx; exact nomatch hx⟩
    · rintro ⟨first, second, rfl, h1, h2, -⟩
      rw [(a.scalar_rep (Ty.scalar_pair h).1).mpr h1, (b.scalar_rep (Ty.scalar_pair h).2).mpr h2]
      rfl
  | .array _, h, _, _ => absurd h Bool.false_ne_true

theorem Ty.leanInst_scalar : (t : Ty) → (h : t.scalar = true) →
    t.leanInst = @instRepresentOfScalar _ (t.scalarInst h)
  | .elem _, _ => rfl
  | .pair _ _, h => by rw [Ty.leanInst, dite_eq_left h]
  | .array _, h => absurd h Bool.false_ne_true

/-- Lean's instance agrees with the verified compiler's representation of a borrowed value. -/
theorem Ty.leanInst_borrowed {heap : Heap} {store : Store Unit} :
    (t : Ty) → {ws : List Value} → {v : t.denote} →
      (@Represent.borrowed _ t.leanInst heap store ws v ↔ t.Rep .borrowed heap store ws v)
  | .elem e, _, _ => Ty.scalar_rep (.elem e) rfl
  | .array e, _, _ => e.arrayInst_borrowed
  | .bytes, _, _ => Iff.rfl
  | .tree _, _, _ => Iff.rfl
  | .treeHeader _ _, _, _ => by
    change (∃ p, _ = [Value.i64 p]) ↔ ∃ p, _ = [Value.i64 p] ∧ True
    simp only [and_true]
  | .pair a b, ws, p => by
    by_cases h : (Ty.pair a b).scalar = true
    · rw [(Ty.pair a b).leanInst_scalar h]
      exact (Ty.pair a b).scalar_rep h
    · rw [Ty.leanInst, dite_eq_right h]
      constructor
      · rintro ⟨first, second, rfl, h1, h2⟩
        exact ⟨first, second, rfl, a.leanInst_borrowed.mp h1, b.leanInst_borrowed.mp h2, nofun⟩
      · rintro ⟨first, second, rfl, h1, h2, -⟩
        exact ⟨first, second, rfl, a.leanInst_borrowed.mpr h1, b.leanInst_borrowed.mpr h2⟩

theorem Ty.scalarInst_length : (t : Ty) → (h : t.scalar = true) → (v : t.denote) →
    (@Scalar.values _ (t.scalarInst h) v).length = t.width
  | .elem e, _, v => by
    show (@Scalar.values _ e.scalarInst v).length = e.width
    rw [e.scalar_values, e.values_length]
  | .pair a b, h, p => by
    show (@Scalar.values _ (a.scalarInst (Ty.scalar_pair h).1) p.1 ++
      @Scalar.values _ (b.scalarInst (Ty.scalar_pair h).2) p.2).length = _
    rw [List.length_append, a.scalarInst_length, b.scalarInst_length]
    rfl
  | .array _, h, _ => absurd h Bool.false_ne_true

/-- Lean's instance gives a value the verified compiler's width. -/
theorem Ty.leanInst_width : (t : Ty) → (v : t.denote) → @Represent.width _ t.leanInst v = t.width
  | .elem e, v => (Ty.elem e).scalarInst_length rfl v
  | .array e, xs => e.arrayInst_width xs
  | .tree _, _ | .treeHeader _ _, _ => rfl
  | .bytes, _ => rfl
  | .pair a b, p => by
    by_cases h : (Ty.pair a b).scalar = true
    · rw [(Ty.pair a b).leanInst_scalar h]
      exact (Ty.pair a b).scalarInst_length h p
    · rw [Ty.leanInst, dite_eq_right h]
      show @Represent.width _ a.leanInst p.1 + @Represent.width _ b.leanInst p.2 = _
      rw [a.leanInst_width, b.leanInst_width]
      rfl

/-- Lean's instance gives a value the verified compiler's blocks. -/
theorem Ty.leanInst_blocks {store : Store Unit} :
    (t : Ty) → {ws : List Value} → {v : t.denote} →
      @Represent.blocks _ t.leanInst store ws v = t.blocks store ws v
  | .elem _, _, _ => rfl
  | .array e, _, _ => e.arrayInst_blocks
  | .tree _, _, _ | .treeHeader _ _, _, _ => rfl
  | .bytes, _, _ => rfl
  | .pair a b, ws, p => by
    by_cases h : (Ty.pair a b).scalar = true
    · rw [(Ty.pair a b).leanInst_scalar h, Ty.blocks_scalar _ h]
      rfl
    · rw [Ty.leanInst, dite_eq_right h]
      show @Represent.blocks _ a.leanInst store (ws.take (@Represent.width _ a.leanInst p.1)) p.1 ++
        @Represent.blocks _ b.leanInst store (ws.drop (@Represent.width _ a.leanInst p.1)) p.2 = _
      rw [a.leanInst_width, a.leanInst_blocks, b.leanInst_blocks]
      rfl

/-- Lean's instance agrees with the verified compiler's representation of an owned value. -/
theorem Ty.leanInst_owned {heap : Heap} {store : Store Unit} :
    (t : Ty) → {ws : List Value} → {v : t.denote} →
      (@Represent.owned _ t.leanInst heap store ws v ↔ t.Rep .owned heap store ws v)
  | .elem e, _, _ => Ty.scalar_rep (.elem e) rfl
  | .array e, _, _ => e.arrayInst_owned
  | .tree _, _, _ | .treeHeader _ _, _, _ => Iff.rfl
  | .bytes, _, _ => Iff.rfl
  | .pair a b, ws, p => by
    by_cases h : (Ty.pair a b).scalar = true
    · rw [(Ty.pair a b).leanInst_scalar h]
      exact (Ty.pair a b).scalar_rep h
    · rw [Ty.leanInst, dite_eq_right h]
      constructor
      · rintro ⟨first, second, rfl, h1, h2, hd⟩
        refine ⟨first, second, rfl, a.leanInst_owned.mp h1, b.leanInst_owned.mp h2,
          fun _ x hx y hy => ?_⟩
        rw [← a.leanInst_blocks] at hx
        rw [← b.leanInst_blocks] at hy
        exact hd x hx y hy
      · rintro ⟨first, second, rfl, h1, h2, hd⟩
        refine ⟨first, second, rfl, a.leanInst_owned.mpr h1, b.leanInst_owned.mpr h2,
          fun x hx y hy => ?_⟩
        rw [a.leanInst_blocks] at hx
        rw [b.leanInst_blocks] at hy
        exact hd rfl x hx y hy

theorem Ty.leanInst_moves {store : Store Unit} :
    (t : Ty) → {ws : List Value} → {v : t.denote} → @Represent.moves _ t.leanInst store ws v = []
  | .elem _, _, _ => rfl
  | .bytes, _, _ => rfl
  | .array e, _, _ => e.arrayInst_moves
  | .tree _, _, _ | .treeHeader _ _, _, _ => rfl
  | .pair a b, ws, p => by
    by_cases h : (Ty.pair a b).scalar = true
    · rw [(Ty.pair a b).leanInst_scalar h]
      rfl
    · rw [Ty.leanInst, dite_eq_right h]
      show @Represent.moves _ a.leanInst store _ p.1 ++
        @Represent.moves _ b.leanInst store _ p.2 = []
      rw [a.leanInst_moves, b.leanInst_moves]
      rfl

theorem Ty.leanInst_reads {store : Store Unit} :
    (t : Ty) → {ws : List Value} → {v : t.denote} →
      @Represent.reads _ t.leanInst store ws v = t.reads store ws v
  | .elem _, _, _ => rfl
  | .bytes, _, _ => rfl
  | .array e, _, _ => e.arrayInst_reads
  | .tree _, _, _ | .treeHeader _ _, _, _ => rfl
  | .pair a b, ws, p => by
    by_cases h : (Ty.pair a b).scalar = true
    · rw [(Ty.pair a b).leanInst_scalar h, Ty.reads_scalar _ h]
      rfl
    · rw [Ty.leanInst, dite_eq_right h]
      show @Represent.reads _ a.leanInst store (ws.take (@Represent.width _ a.leanInst p.1)) p.1 ++
        @Represent.reads _ b.leanInst store (ws.drop (@Represent.width _ a.leanInst p.1)) p.2 = _
      rw [a.leanInst_width, a.leanInst_reads, b.leanInst_reads]
      rfl

theorem Ty.paramMode_scalar : (t : Ty) → t.scalar = true → (m : Mode) → t.paramMode m = .borrowed
  | .elem _, _, _ | .pair _ _, _, _ => rfl
  | .array _, h, _ => absurd h Bool.false_ne_true

/-- The Lean type of an argument of type `t` at a parameter for which the mode `m` was chosen:
`Moved` for an owned array. -/
abbrev Ty.argTy : Ty → Mode → Type
  | .bytes, .owned => Moved LeanExe.Bytes
  | .array e, .owned => Moved (Array e.denote)
  | .tree shape, .owned => Moved (Tree shape)
  | .treeHeader shape r, .owned => Moved (TreeHeader shape r)
  | t, _ => t.denote

/-- The value of an argument. -/
def Ty.argVal : (t : Ty) → (m : Mode) → t.argTy m → t.denote
  | .bytes, .owned, x => x.val
  | .bytes, .borrowed, x => x
  | .array _, .owned, x => x.val
  | .array _, .borrowed, x => x
  | .tree _, .owned, x | .treeHeader _ _, .owned, x => x.val
  | .tree _, .borrowed, x | .treeHeader _ _, .borrowed, x => x
  | .elem _, _, x | .pair _ _, _, x => x

/-- The `Represent` instance that Lean synthesizes for an argument. -/
@[instance_reducible] def Ty.argInst : (t : Ty) → (m : Mode) → Represent (t.argTy m)
  | .bytes, .owned => inferInstanceAs (Represent (Moved LeanExe.Bytes))
  | .bytes, .borrowed => Ty.leanInst .bytes
  | .array e, .owned => e.movedInst
  | .array e, .borrowed => Ty.leanInst (.array e)
  | .elem e, _ => Ty.leanInst (.elem e)
  | .pair a b, _ => Ty.leanInst (.pair a b)
  | .tree shape, .owned => inferInstanceAs (Represent (Moved (Tree shape)))
  | .tree shape, .borrowed => Ty.leanInst (.tree shape)
  | .treeHeader shape r, .owned => inferInstanceAs (Represent (Moved (TreeHeader shape r)))
  | .treeHeader shape r, .borrowed => Ty.leanInst (.treeHeader shape r)

/-- The `Scalar` instance that Lean synthesizes for an argument without arrays. -/
@[instance_reducible] def Ty.argScalarInst : (t : Ty) → (m : Mode) → t.scalar = true →
    Scalar (t.argTy m)
  | .elem e, _, h => Ty.scalarInst (.elem e) h
  | .pair a b, _, h => Ty.scalarInst (.pair a b) h
  | .array _, _, h => absurd h Bool.false_ne_true

theorem Ty.argScalar_values : (t : Ty) → (m : Mode) → (h : t.scalar = true) → (x : t.argTy m) →
    @Scalar.values _ (t.argScalarInst m h) x = @Scalar.values _ (t.scalarInst h) (t.argVal m x)
  | .elem _, _, _, _ | .pair _ _, _, _, _ => rfl
  | .array _, _, h, _ => absurd h Bool.false_ne_true

theorem Ty.argInst_scalar : (t : Ty) → (m : Mode) → (h : t.scalar = true) →
    t.argInst m = @instRepresentOfScalar _ (t.argScalarInst m h)
  | .elem _, _, h | .pair _ _, _, h => Ty.leanInst_scalar _ h
  | .array _, _, h => absurd h Bool.false_ne_true

theorem Ty.argInst_width : (t : Ty) → (m : Mode) → (x : t.argTy m) →
    @Represent.width _ (t.argInst m) x = t.width
  | .array e, .owned, x => e.movedInst_width x
  | .array e, .borrowed, x => e.arrayInst_width x
  | .tree _, _, _ | .treeHeader _ _, _, _ => by cases ‹Mode› <;> rfl
  | .bytes, _, _ => by cases ‹Mode› <;> rfl
  | .elem _, _, x | .pair _ _, _, x => Ty.leanInst_width _ x

/-- Lean's instance for an argument agrees with the verified compiler's representation. -/
theorem Ty.argInst_borrowed {heap : Heap} {store : Store Unit} :
    (t : Ty) → (m : Mode) → {ws : List Value} → {x : t.argTy m} →
      (@Represent.borrowed _ (t.argInst m) heap store ws x ↔
        t.Rep (t.paramMode m) heap store ws (t.argVal m x))
  | .array e, .owned, _, _ => e.movedInst_borrowed
  | .array e, .borrowed, _, _ => e.arrayInst_borrowed
  | .bytes, .owned, _, _ | .bytes, .borrowed, _, _ => Iff.rfl
  | .tree _, .owned, _, _ | .treeHeader _ _, .owned, _, _ => Iff.rfl
  | .tree shape, .borrowed, _, _ => (Ty.tree shape).leanInst_borrowed
  | .treeHeader shape r, .borrowed, _, _ => (Ty.treeHeader shape r).leanInst_borrowed
  | .elem _, _, _, _ | .pair _ _, _, _, _ => Ty.leanInst_borrowed _

theorem Ty.argInst_moves {store : Store Unit} :
    (t : Ty) → (m : Mode) → {ws : List Value} → {x : t.argTy m} →
      @Represent.moves _ (t.argInst m) store ws x =
        match t.paramMode m with
        | .owned => t.pointers store ws (t.argVal m x)
        | .borrowed => []
  | .array e, .owned, _, _ => e.movedInst_moves
  | .array e, .borrowed, _, _ => e.arrayInst_moves
  | .bytes, .owned, _, _ | .bytes, .borrowed, _, _ => rfl
  | .tree _, .owned, _, _ | .treeHeader _ _, .owned, _, _ => rfl
  | .tree shape, .borrowed, _, _ => (Ty.tree shape).leanInst_moves
  | .treeHeader shape r, .borrowed, _, _ => (Ty.treeHeader shape r).leanInst_moves
  | .elem _, _, _, _ | .pair _ _, _, _, _ => Ty.leanInst_moves _

theorem Ty.argInst_reads {store : Store Unit} :
    (t : Ty) → (m : Mode) → {ws : List Value} → {x : t.argTy m} →
      @Represent.reads _ (t.argInst m) store ws x =
        match t.paramMode m with
        | .owned => []
        | .borrowed => t.reads store ws (t.argVal m x)
  | .array e, .owned, _, _ => e.movedInst_reads
  | .array e, .borrowed, _, _ => (Ty.array e).leanInst_reads
  | .bytes, .owned, _, _ | .bytes, .borrowed, _, _ => rfl
  | .tree _, .owned, _, _ | .treeHeader _ _, .owned, _, _ => rfl
  | .tree shape, .borrowed, _, _ => (Ty.tree shape).leanInst_reads
  | .treeHeader shape r, .borrowed, _, _ => (Ty.treeHeader shape r).leanInst_reads
  | .elem _, _, _, _ | .pair _ _, _, _, _ => Ty.leanInst_reads _

/-- The Lean type of a function's arguments, for parameters of types `ps` for which the modes `ms`
were chosen: `Unit` for none, the argument's type for one, and the right-nested product of the
arguments' types for more. -/
abbrev argsTy : List Ty → List Mode → Type
  | [], _ => Unit
  | [t], ms => t.argTy (ms.headD .borrowed)
  | t :: u :: ts, ms => t.argTy (ms.headD .borrowed) × argsTy (u :: ts) ms.tail

/-- The `Scalar` instance that Lean synthesizes for arguments without arrays. -/
@[instance_reducible] def argsScalarInst : (ps : List Ty) → (ms : List Mode) →
    ps.all Ty.scalar = true → Scalar (argsTy ps ms)
  | [], _, _ => instScalarUnit
  | [t], _, h => t.argScalarInst _ (by simpa using h)
  | t :: u :: ts, ms, h =>
    @instScalarProd (t.argTy (ms.headD .borrowed)) (argsTy (u :: ts) ms.tail)
      (t.argScalarInst _ (by simp at h; exact h.1))
      (argsScalarInst (u :: ts) ms.tail (by simp at h ⊢; exact h.2))

/-- The `Represent` instance that Lean synthesizes for a function's arguments. -/
@[instance_reducible] def argsInst : (ps : List Ty) → (ms : List Mode) → Represent (argsTy ps ms)
  | [], _ => @instRepresentOfScalar Unit instScalarUnit
  | [t], ms => t.argInst (ms.headD .borrowed)
  | t :: u :: ts, ms =>
    if h : (t :: u :: ts).all Ty.scalar = true then
      @instRepresentOfScalar _ (argsScalarInst (t :: u :: ts) ms h)
    else @instRepresentProd _ _ (t.argInst (ms.headD .borrowed)) (argsInst (u :: ts) ms.tail)

/-- The values of a function's arguments, from Lean's argument tuple. -/
def Env.ofArgs : (ps : List Ty) → (ms : List Mode) → argsTy ps ms → Env ps
  | [], _, _ => .nil
  | [t], _, x => .cons (t.argVal _ x) .nil
  | t :: _ :: _, ms, x => .cons (t.argVal _ x.1) (Env.ofArgs _ ms.tail x.2)

theorem argsScalar_rep {heap : Heap} {store : Store Unit} :
    (ps : List Ty) → (ms : List Mode) → (h : ps.all Ty.scalar = true) → {ws : List Value} →
      {y : argsTy ps ms} →
      (ws = @Scalar.values _ (argsScalarInst ps ms h) y ↔
        Env.Rep (paramMode ps ms) heap store ws (Env.ofArgs ps ms y))
  | [], _, _, _, _ => Iff.rfl
  | [t], ms, h, ws, y => by
    have ht : t.scalar = true := by simpa using h
    rw [show (@Scalar.values _ (argsScalarInst [t] ms h) y) =
      @Scalar.values _ (t.argScalarInst _ ht) y from rfl, t.argScalar_values, t.scalar_rep ht]
    constructor
    · intro hy; exact ⟨ws, [], by simp, hy, rfl⟩
    · rintro ⟨first, rest, rfl, h1, rfl⟩; rw [List.append_nil]; exact h1
  | t :: u :: ts, ms, h, ws, y => by
    have ht : t.scalar = true := by simp at h; exact h.1
    have hv : @Scalar.values _ (argsScalarInst (t :: u :: ts) ms h) y =
        @Scalar.values _ (t.scalarInst ht) (t.argVal _ y.1) ++
          @Scalar.values _ (argsScalarInst (u :: ts) ms.tail (by simp at h ⊢; exact h.2)) y.2 := by
      rw [← t.argScalar_values _ ht]
      rfl
    rw [hv]
    constructor
    · rintro rfl
      exact ⟨_, _, rfl, (t.scalar_rep ht).mp rfl, (argsScalar_rep (u :: ts) ms.tail _).mp rfl⟩
    · rintro ⟨first, rest, rfl, h1, h2⟩
      rw [(t.scalar_rep ht).mpr h1, (argsScalar_rep (u :: ts) ms.tail _).mpr h2]

theorem argsInst_scalar : (ps : List Ty) → (ms : List Mode) → (h : ps.all Ty.scalar = true) →
    argsInst ps ms = @instRepresentOfScalar _ (argsScalarInst ps ms h)
  | [], _, _ => rfl
  | [t], _, h => t.argInst_scalar _ (by simpa using h)
  | _ :: _ :: _, _, h => by rw [argsInst, dite_eq_left h]

/-- Lean's instance for the arguments agrees with the verified compiler's representation. -/
theorem argsInst_borrowed {heap : Heap} {store : Store Unit} :
    (ps : List Ty) → (ms : List Mode) → {ws : List Value} → {y : argsTy ps ms} →
      (@Represent.borrowed _ (argsInst ps ms) heap store ws y ↔
        Env.Rep (paramMode ps ms) heap store ws (Env.ofArgs ps ms y))
  | [], _, _, _ => Iff.rfl
  | [t], ms, ws, y => by
    rw [show (@Represent.borrowed _ (argsInst [t] ms) heap store ws y) =
      @Represent.borrowed _ (t.argInst _) heap store ws y from rfl, t.argInst_borrowed]
    constructor
    · intro hy; exact ⟨ws, [], by simp, hy, rfl⟩
    · rintro ⟨first, rest, rfl, h1, rfl⟩; rw [List.append_nil]; exact h1
  | t :: u :: ts, ms, ws, y => by
    by_cases h : (t :: u :: ts).all Ty.scalar = true
    · rw [argsInst_scalar _ _ h]
      exact argsScalar_rep _ _ h
    · rw [argsInst, dite_eq_right h]
      constructor
      · rintro ⟨first, rest, rfl, h1, h2⟩
        exact ⟨first, rest, rfl, (t.argInst_borrowed _).mp h1,
          (argsInst_borrowed (u :: ts) ms.tail).mp h2⟩
      · rintro ⟨first, rest, rfl, h1, h2⟩
        exact ⟨first, rest, rfl, (t.argInst_borrowed _).mpr h1,
          (argsInst_borrowed (u :: ts) ms.tail).mpr h2⟩

theorem Env.moves_scalar {store : Store Unit} : {ps : List Ty} → (ms : List Mode) → ps.all Ty.scalar = true →
    (ws : List Value) → (env : Env ps) → Env.moves store (paramMode ps ms) ws env = []
  | [], _, _, _, .nil => rfl
  | t :: _, ms, h, ws, .cons _ env => by
    simp only [List.all_cons, Bool.and_eq_true] at h
    simp only [Env.moves, paramMode, paramModes, List.getD_cons_zero,
      t.paramMode_scalar h.1, List.nil_append]
    exact Env.moves_scalar ms.tail h.2 _ env

theorem Env.reads_scalar {store : Store Unit} : {ps : List Ty} → (ms : List Mode) → ps.all Ty.scalar = true →
    (ws : List Value) → (env : Env ps) → Env.reads store (paramMode ps ms) ws env = []
  | [], _, _, _, .nil => rfl
  | t :: _, ms, h, ws, .cons v env => by
    simp only [List.all_cons, Bool.and_eq_true] at h
    simp only [Env.reads, paramMode, paramModes, List.getD_cons_zero,
      t.paramMode_scalar h.1, t.reads_scalar h.1, List.nil_append]
    exact Env.reads_scalar ms.tail h.2 _ env

theorem argsInst_moves {store : Store Unit} :
    (ps : List Ty) → (ms : List Mode) → {ws : List Value} → {y : argsTy ps ms} →
      ws.length = widthSum ps →
      @Represent.moves _ (argsInst ps ms) store ws y =
        Env.moves store (paramMode ps ms) ws (Env.ofArgs ps ms y)
  | [], _, _, _, _ => rfl
  | [t], ms, ws, y, hl => by
    rw [show (@Represent.moves _ (argsInst [t] ms) store ws y) =
      @Represent.moves _ (t.argInst _) store ws y from rfl, t.argInst_moves]
    simp only [Env.ofArgs, Env.moves, paramMode, paramModes, List.getD_cons_zero, List.append_nil]
    rw [List.take_of_length_le (show ws.length ≤ t.width by simp [widthSum] at hl; omega)]
  | t :: u :: ts, ms, ws, y, hl => by
    by_cases h : (t :: u :: ts).all Ty.scalar = true
    · rw [argsInst_scalar _ _ h, Env.moves_scalar _ h]
      rfl
    · rw [argsInst, dite_eq_right h]
      show @Represent.moves _ (t.argInst _) store
          (ws.take (@Represent.width _ (t.argInst _) y.1)) y.1 ++
        @Represent.moves _ (argsInst (u :: ts) ms.tail) store
          (ws.drop (@Represent.width _ (t.argInst _) y.1)) y.2 = _
      rw [t.argInst_width, t.argInst_moves, argsInst_moves (u :: ts) ms.tail
        (by rw [List.length_drop, hl, widthSum_cons]; omega)]
      rfl

theorem argsInst_reads {store : Store Unit} :
    (ps : List Ty) → (ms : List Mode) → {ws : List Value} → {y : argsTy ps ms} →
      ws.length = widthSum ps →
      @Represent.reads _ (argsInst ps ms) store ws y =
        Env.reads store (paramMode ps ms) ws (Env.ofArgs ps ms y)
  | [], _, _, _, _ => rfl
  | [t], ms, ws, y, hl => by
    rw [show (@Represent.reads _ (argsInst [t] ms) store ws y) =
      @Represent.reads _ (t.argInst _) store ws y from rfl, t.argInst_reads]
    simp only [Env.ofArgs, Env.reads, paramMode, paramModes, List.getD_cons_zero, List.append_nil]
    rw [List.take_of_length_le (show ws.length ≤ t.width by simp [widthSum] at hl; omega)]
  | t :: u :: ts, ms, ws, y, hl => by
    by_cases h : (t :: u :: ts).all Ty.scalar = true
    · rw [argsInst_scalar _ _ h, Env.reads_scalar _ h]
      rfl
    · rw [argsInst, dite_eq_right h]
      show @Represent.reads _ (t.argInst _) store
          (ws.take (@Represent.width _ (t.argInst _) y.1)) y.1 ++
        @Represent.reads _ (argsInst (u :: ts) ms.tail) store
          (ws.drop (@Represent.width _ (t.argInst _) y.1)) y.2 = _
      rw [t.argInst_width, t.argInst_reads, argsInst_reads (u :: ts) ms.tail
        (by rw [List.length_drop, hl, widthSum_cons]; omega)]
      rfl

#print axioms Ty.Rep.step
#print axioms Ty.blocks_pointers
#print axioms Ty.argInst_borrowed
#print axioms argsInst_moves

end Verified