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

module Spartan6.Examples.StateMemory where

open import Spartan6.Prelude
open import Spartan6.Foundation.MemoryModel
open import Spartan6.Semantics.StateAdapters
open import Spartan6.Semantics.StateResource

open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty
import Spartan6.Foundation.Memory as Dense
import Spartan6.Primitive.BlockRAM as BlockRAM
import Spartan6.Primitive.RAM32X1S as RAM32X1S

oneBitLow oneBitHigh : Word 1
oneBitLow  = low ∷ []
oneBitHigh = high ∷ []

first second : Fin 2
first  = fzero
second = fsuc fzero

twoWordMemory : Dense.Memory 2 1
twoWordMemory = oneBitLow ∷ oneBitHigh ∷ []

firstTest : Fin 2 → Bit
firstTest fzero      = high
firstTest (fsuc idx) = low

first-is-not-second : first ≡ second → Empty.⊥
first-is-not-second path =
  false≢true (sym (cong firstTest path))

twoWordModel : MemoryModel (Fin 2) (Word 1) (Dense.Memory 2 1)
twoWordModel = denseMemoryModel 2 1

read-after-write-same-law :
  readMemory twoWordModel first
    (writeMemory twoWordModel first oneBitHigh twoWordMemory)
  ≡ oneBitHigh
read-after-write-same-law =
  read-after-write-same
    twoWordModel first oneBitHigh twoWordMemory

read-after-write-distinct-law :
  readMemory twoWordModel first
    (writeMemory twoWordModel second oneBitLow twoWordMemory)
  ≡ readMemory twoWordModel first twoWordMemory
read-after-write-distinct-law =
  read-after-write-distinct
    twoWordModel first second oneBitLow twoWordMemory
    first-is-not-second

last-write-law :
  writeMemory twoWordModel first oneBitLow
    (writeMemory twoWordModel first oneBitHigh twoWordMemory)
  ≡ writeMemory twoWordModel first oneBitLow twoWordMemory
last-write-law =
  last-write-wins
    twoWordModel first oneBitHigh oneBitLow twoWordMemory

-- Concrete reductions ensure the dense instance computes, in addition to
-- satisfying the abstract laws above.

dense-same-address-reduction :
  readMemory twoWordModel first
    (writeMemory twoWordModel first oneBitHigh twoWordMemory)
  ≡ oneBitHigh
dense-same-address-reduction = refl

dense-other-address-reduction :
  readMemory twoWordModel second
    (writeMemory twoWordModel first oneBitHigh twoWordMemory)
  ≡ oneBitHigh
dense-other-address-reduction = refl

-- The distributed-RAM observation remains asynchronous: changing only the
-- input address changes the observation of one unchanged semantic state.

ram32ProbeResource :
  StateResource
    RAM32X1SInitial RAM32X1SInput Bit Unit RAM32X1S.RAM32X1SState
ram32ProbeResource = ram32x1sResource tt

ram32ReadZero ram32ReadOne ram32WriteOne : RAM32X1SInput
ram32ReadZero =
  ram32x1sInput RAM32X1S.allLowAddress low low
ram32ReadOne =
  ram32x1sInput RAM32X1S.onlyA0HighAddress low low
ram32WriteOne =
  ram32x1sInput RAM32X1S.onlyA0HighAddress high high

distributed-asynchronous-address-change :
  (observeResource ram32ProbeResource
      ram32ReadZero RAM32X1S.exampleState ≡ low)
  ×
  (observeResource ram32ProbeResource
      ram32ReadOne RAM32X1S.exampleState ≡ high)
distributed-asynchronous-address-change = refl , refl

distributed-owned-edge-write-is-visible :
  observeResource ram32ProbeResource ram32ReadOne
    (stepResource ram32ProbeResource allEdges
      ram32WriteOne RAM32X1S.defaultInitialState)
  ≡ high
distributed-owned-edge-write-is-visible = refl

-- Block RAM observes the primitive's output latch.  These resources differ
-- only in their fixed write mode and reuse the same typed command/state.

BlockRAMProbeResource : Type₀
BlockRAMProbeResource =
  StateResource
    (BlockRAM.SinglePortState 2 2)
    (BlockRAM.PortCommand 2 2)
    (Word 2)
    Unit
    (BlockRAM.SinglePortState 2 2)

writeFirstResource readFirstResource noChangeResource :
  BlockRAMProbeResource
writeFirstResource = blockRAMResource tt BlockRAM.WRITE_FIRST
readFirstResource  = blockRAMResource tt BlockRAM.READ_FIRST
noChangeResource   = blockRAMResource tt BlockRAM.NO_CHANGE

blockRAM-write-first-output :
  observeResource writeFirstResource BlockRAM.exampleWrite
    (stepResource writeFirstResource allEdges
      BlockRAM.exampleWrite BlockRAM.exampleState)
  ≡ high ∷ high ∷ []
blockRAM-write-first-output = refl

blockRAM-read-first-output :
  observeResource readFirstResource BlockRAM.exampleWrite
    (stepResource readFirstResource allEdges
      BlockRAM.exampleWrite BlockRAM.exampleState)
  ≡ low ∷ low ∷ []
blockRAM-read-first-output = refl

blockRAM-no-change-output :
  observeResource noChangeResource BlockRAM.exampleWrite
    (stepResource noChangeResource allEdges
      BlockRAM.exampleWrite BlockRAM.exampleState)
  ≡ low ∷ high ∷ []
blockRAM-no-change-output = refl

blockRAM-write-still-updates-memory :
  Dense.read fzero
    (BlockRAM.memoryContents
      (stepResource noChangeResource allEdges
        BlockRAM.exampleWrite BlockRAM.exampleState))
  ≡ high ∷ high ∷ []
blockRAM-write-still-updates-memory = refl