import Wasm.Isa

/-!
# Wasm.Mem

Byte-level memory facts: a write of eight bytes is read back by a read at the same address, and
leaves every read at a disjoint address unchanged. These replace any "word cell" memory assumption.
-/

namespace WordDialect
namespace Wasm

theorem rdBytes_congr {b b' : Nat → Nat} {a : Nat} :
    ∀ {n : Nat}, (∀ i, i < n → b (a + i) = b' (a + i)) → rdBytes b a n = rdBytes b' a n := by
  intro n
  induction n with
  | zero => intro _; rfl
  | succ n ih =>
    intro h
    simp only [rdBytes]
    rw [ih (fun i hi => h i (by omega)), h n (by omega)]

theorem rdBytes_pow (v : Nat) : ∀ n : Nat,
    rdBytes (fun p => (v / 256 ^ p) % 256) 0 n = v % 256 ^ n := by
  intro n
  induction n with
  | zero => simp [rdBytes, Nat.mod_one]
  | succ n ih =>
    simp only [rdBytes, Nat.zero_add]
    rw [ih, Nat.pow_succ, Nat.mod_mul]
    simp [Nat.mod_mod, Nat.mul_comm]

theorem write64_size {m m' : WMem} {a : Nat} {v : W} (h : m.write64 a v = some m') :
    m'.size = m.size ∧ a + 8 ≤ m.size := by
  unfold WMem.write64 at h
  split at h
  · rename_i hlt; simp at h; subst h; exact ⟨rfl, hlt⟩
  · simp at h

theorem write64_some {m : WMem} {a : Nat} {v : W} (h : a + 8 ≤ m.size) :
    ∃ m', m.write64 a v = some m' := by
  simp [WMem.write64, h]

theorem read64_write64_same {m m' : WMem} {a : Nat} {v : W} (h : m.write64 a v = some m') :
    m'.read64 a = some v := by
  obtain ⟨hs, hlt⟩ := write64_size h
  unfold WMem.write64 at h
  rw [if_pos hlt] at h
  simp at h
  subst h
  unfold WMem.read64
  rw [if_pos (by simpa using hlt)]
  congr 1
  have hc : rdBytes (fun p => if a ≤ p ∧ p < a + 8 then (v.toNat / 256 ^ (p - a)) % 256 else m.bytes p) a 8
      = rdBytes (fun p => (v.toNat / 256 ^ p) % 256) 0 8 := by
    rw [show rdBytes (fun p => (v.toNat / 256 ^ p) % 256) 0 8 =
        rdBytes (fun p => (v.toNat / 256 ^ (p - a)) % 256) a 8 from ?_]
    · apply rdBytes_congr
      intro i hi
      have h1 : a ≤ a + i := by omega
      have h2 : a + i < a + 8 := by omega
      simp [h1, h2]
    · simp only [rdBytes]
      simp [Nat.add_sub_cancel_left]
  rw [hc, rdBytes_pow]
  have : v.toNat < 256 ^ 8 := by have := v.isLt; simpa using this
  rw [Nat.mod_eq_of_lt this]
  simp

theorem read64_write64_other {m m' : WMem} {a b : Nat} {v : W} (h : m.write64 a v = some m')
    (hd : b + 8 ≤ a ∨ a + 8 ≤ b) : m'.read64 b = m.read64 b := by
  obtain ⟨hs, hlt⟩ := write64_size h
  unfold WMem.write64 at h
  rw [if_pos hlt] at h
  simp at h
  subst h
  unfold WMem.read64
  simp only []
  by_cases hb : b + 8 ≤ m.size
  · rw [if_pos hb, if_pos hb]
    congr 2
    apply rdBytes_congr
    intro i hi
    have : ¬ (a ≤ b + i ∧ b + i < a + 8) := by omega
    simp [this]
  · rw [if_neg hb, if_neg hb]

end Wasm
end WordDialect