{-# OPTIONS --safe --cubical #-}

module Spartan6.Foundation.MemoryModel where

open import Spartan6.Prelude

import Cubical.Data.Empty as Empty
import Spartan6.Foundation.Memory as Dense

-- The laws used by state-resource semantics do not commit a memory family to
-- a particular storage representation.

record MemoryModel (Address Value State : Type₀) : Type₀ where
  constructor memoryModel
  field
    readMemory  : Address → State → Value
    writeMemory : Address → Value → State → State

    read-after-write-same :
      ∀ address value state
      → readMemory address (writeMemory address value state) ≡ value

    read-after-write-distinct :
      ∀ read-address write-address value state
      → (read-address ≡ write-address → Empty.⊥)
      → readMemory read-address
          (writeMemory write-address value state)
      ≡ readMemory read-address state

    last-write-wins :
      ∀ address old-value new-value state
      → writeMemory address new-value
          (writeMemory address old-value state)
      ≡ writeMemory address new-value state

open MemoryModel public

dense-read-after-write-distinct :
  ∀ {depth width}
    (read-address write-address : Fin depth)
    (value : Word width) (state : Dense.Memory depth width)
  → (read-address ≡ write-address → Empty.⊥)
  → Dense.read read-address (Dense.write write-address value state)
  ≡ Dense.read read-address state
dense-read-after-write-distinct fzero fzero value (current ∷ state) distinct =
  Empty.rec (distinct refl)
dense-read-after-write-distinct fzero (fsuc write-address)
  value (current ∷ state) distinct = refl
dense-read-after-write-distinct (fsuc read-address) fzero
  value (current ∷ state) distinct = refl
dense-read-after-write-distinct (fsuc read-address) (fsuc write-address)
  value (current ∷ state) distinct =
  dense-read-after-write-distinct read-address write-address value state
    (λ path → distinct (cong fsuc path))

dense-last-write-wins :
  ∀ {depth width}
    (address : Fin depth) (old-value new-value : Word width)
    (state : Dense.Memory depth width)
  → Dense.write address new-value
      (Dense.write address old-value state)
  ≡ Dense.write address new-value state
dense-last-write-wins fzero old-value new-value (current ∷ state) = refl
dense-last-write-wins (fsuc address) old-value new-value (current ∷ state) =
  cong (λ rest → current ∷ rest)
    (dense-last-write-wins address old-value new-value state)

denseMemoryModel : (depth width : ℕ)
  → MemoryModel
      (Fin depth)
      (Word width)
      (Dense.Memory depth width)
readMemory (denseMemoryModel depth width) = Dense.read
writeMemory (denseMemoryModel depth width) = Dense.write
read-after-write-same (denseMemoryModel depth width) =
  Dense.read-after-write-same
read-after-write-distinct (denseMemoryModel depth width) =
  dense-read-after-write-distinct
last-write-wins (denseMemoryModel depth width) =
  dense-last-write-wins