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

module Spartan6.Semantics.StateResource where

open import Spartan6.Prelude

-- All domains inspect one edge set for a system step.  The set is a function
-- rather than an ordered event list, so it cannot encode an execution order.

EdgeSet : Type₀ → Type₀
EdgeSet Domain = Domain → Bit

noEdges : ∀ {Domain} → EdgeSet Domain
noEdges domain = low

allEdges : ∀ {Domain} → EdgeSet Domain
allEdges domain = high

record StateResource
  (Initial Input Observation Domain State : Type₀) : Type₀ where
  constructor stateResource
  field
    decodeInitial    : Initial → Maybe State
    observeResource  : Input → State → Observation
    resourceDomain   : Domain
    transitionOnEdge : Input → State → State

open StateResource public

-- Domain handling is centralized here.  A resource implementation only
-- describes the transition for an edge that it owns.

stepResource :
  ∀ {Initial Input Observation Domain State}
  → StateResource Initial Input Observation Domain State
  → EdgeSet Domain → Input → State → State
stepResource resource edges input state =
  if edges (resourceDomain resource)
  then transitionOnEdge resource input state
  else state

no-edges-hold :
  ∀ {Initial Input Observation Domain State}
    (resource : StateResource Initial Input Observation Domain State)
    (input : Input) (state : State)
  → stepResource resource noEdges input state ≡ state
no-edges-hold resource input state = refl

all-edges-transition :
  ∀ {Initial Input Observation Domain State}
    (resource : StateResource Initial Input Observation Domain State)
    (input : Input) (state : State)
  → stepResource resource allEdges input state
  ≡ transitionOnEdge resource input state
all-edges-transition resource input state = refl

absent-owned-edge-holds :
  ∀ {Initial Input Observation Domain State}
    (resource : StateResource Initial Input Observation Domain State)
    (edges : EdgeSet Domain) (input : Input) (state : State)
  → edges (resourceDomain resource) ≡ low
  → stepResource resource edges input state ≡ state
absent-owned-edge-holds resource edges input state edge-absent =
  cong
    (λ active →
      if active
      then transitionOnEdge resource input state
      else state)
    edge-absent

present-owned-edge-transitions :
  ∀ {Initial Input Observation Domain State}
    (resource : StateResource Initial Input Observation Domain State)
    (edges : EdgeSet Domain) (input : Input) (state : State)
  → edges (resourceDomain resource) ≡ high
  → stepResource resource edges input state
  ≡ transitionOnEdge resource input state
present-owned-edge-transitions resource edges input state edge-present =
  cong
    (λ active →
      if active
      then transitionOnEdge resource input state
      else state)
    edge-present

-- A concrete bit layout is optional and kept out of StateResource.  This
-- record certifies a separately executable bit-level observation/transition
-- without constraining the semantic State carrier.

record CertifiedBitLowering
  {Initial Input Observation Domain State : Type₀}
  (resource : StateResource Initial Input Observation Domain State)
  (width : ℕ) : Type₀ where
  constructor certifiedBitLowering
  field
    encodeState : State → Vec Bit width
    decodeState : Vec Bit width → State

    decode-encode : ∀ state → decodeState (encodeState state) ≡ state

    observeBits : Input → Vec Bit width → Observation
    observe-preserved : ∀ input state
      → observeBits input (encodeState state)
      ≡ observeResource resource input state

    transitionBits : Input → Vec Bit width → Vec Bit width
    transition-preserved : ∀ input state
      → transitionBits input (encodeState state)
      ≡ encodeState (transitionOnEdge resource input state)

open CertifiedBitLowering public

stepBits :
  ∀ {Initial Input Observation Domain State width}
    {resource : StateResource Initial Input Observation Domain State}
  → CertifiedBitLowering resource width
  → EdgeSet Domain → Input → Vec Bit width → Vec Bit width
stepBits {resource = resource} lowering edges input state =
  if edges (resourceDomain resource)
  then transitionBits lowering input state
  else state

step-lowering-preserved :
  ∀ {Initial Input Observation Domain State width}
    {resource : StateResource Initial Input Observation Domain State}
    (lowering : CertifiedBitLowering resource width)
    (edges : EdgeSet Domain) (input : Input) (state : State)
  → stepBits lowering edges input (encodeState lowering state)
  ≡ encodeState lowering (stepResource resource edges input state)
step-lowering-preserved {resource = resource} lowering edges input state
  with edges (resourceDomain resource)
... | false = refl
... | true  = transition-preserved lowering input state