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

module Spartan6.Semantics.Contract where

open import Spartan6.Prelude
open import Spartan6.Evidence
open import Spartan6.Semantics.Design

import Spartan6.Semantics.DesignMachine as DesignMachine
import Spartan6.Semantics.Machine as Machine
import Spartan6.Semantics.Refinement as Refinement
import Spartan6.Semantics.System as System
import Spartan6.Semantics.Trace as Trace

-- A contract is relational on purpose: documented uncertainty and explicit
-- black-box assumptions need not be forced into an executable Boolean
-- function.  Every contract fixes its typed interface and state size.

record Contract
  {ℓ : Level}
  (inputCount outputCount stateCount : ℕ) : Type (ℓ-suc ℓ) where
  field
    Initial : Vec Bit stateCount → Type ℓ
    ObservationAllowed : Vec Bit inputCount
                       → Vec Bit stateCount
                       → Vec Bit outputCount
                       → Type ℓ
    TransitionAllowed : Event
                      → Vec Bit inputCount
                      → Vec Bit stateCount
                      → Vec Bit stateCount
                      → Type ℓ

open Contract public

contractSystem : ∀ {inputCount outputCount stateCount}
  → Contract {ℓ-zero} inputCount outputCount stateCount
  → System.System
      (Vec Bit inputCount) (Vec Bit outputCount) Event (Vec Bit stateCount)
System.Initial (contractSystem contract) = Initial contract
System.ObservationAllowed (contractSystem contract) =
  ObservationAllowed contract
System.TransitionAllowed (contractSystem contract) =
  TransitionAllowed contract

-- This is the authoritative contract execution notion.  Unlike the legacy
-- transition-only relation below, it retains initial and observation evidence.
StrongContractExecution : ∀ {inputCount outputCount stateCount}
  → (contract : Contract {ℓ-zero} inputCount outputCount stateCount)
  → List (Machine.Stimulus (Vec Bit inputCount) Event)
  → Vec Bit stateCount → Type₀
StrongContractExecution contract samples final =
  Trace.Trace (contractSystem contract) samples final

data ContractExecutes
  {ℓ inputCount outputCount stateCount}
  (contract : Contract {ℓ} inputCount outputCount stateCount)
  : Vec Bit stateCount
  → List (Stimulus inputCount)
  → Vec Bit stateCount
  → Type ℓ where

  contractDone : ∀ {state}
               → ContractExecutes contract state []ᴸ state

  contractStep : ∀ {state after final samples}
               → (sample : Stimulus inputCount)
               → TransitionAllowed contract
                   (stimulusEvent sample)
                   (stimulusInputs sample)
                   state
                   after
               → ContractExecutes contract after samples final
               → ContractExecutes contract state (sample ∷ᴸ samples) final

record ContractDeterministic
  {ℓ inputCount outputCount stateCount}
  (contract : Contract {ℓ} inputCount outputCount stateCount) : Type ℓ where
  field
    initialUnique : ∀ {left right}
                  → Initial contract left → Initial contract right
                  → left ≡ right
    observationUnique : ∀ {external state left right}
                      → ObservationAllowed contract external state left
                      → ObservationAllowed contract external state right
                      → left ≡ right
    transitionUnique : ∀ {event external state left right}
                     → TransitionAllowed contract event external state left
                     → TransitionAllowed contract event external state right
                     → left ≡ right

open ContractDeterministic public

designContract : ∀ {inputCount outputCount registerCount}
               → Design inputCount outputCount registerCount
               → Contract {ℓ-zero} inputCount outputCount registerCount
Initial (designContract design) state = initial design ≡ state
ObservationAllowed (designContract design) external state observation =
  observe design external state ≡ observation
TransitionAllowed (designContract design) event external before after =
  step design event external before ≡ after

design-contract-deterministic :
  ∀ {inputCount outputCount registerCount}
    (design : Design inputCount outputCount registerCount)
  → ContractDeterministic (designContract design)
initialUnique (design-contract-deterministic design) left right = sym left ∙ right
observationUnique (design-contract-deterministic design) left right =
  sym left ∙ right
transitionUnique (design-contract-deterministic design) left right =
  sym left ∙ right

design-contract-run :
  ∀ {inputCount outputCount registerCount}
    (design : Design inputCount outputCount registerCount)
    (state : Vec Bit registerCount)
    (samples : List (Stimulus inputCount))
  → ContractExecutes (designContract design)
      state samples (run design state samples)
design-contract-run design state []ᴸ = contractDone
design-contract-run design state (sample ∷ᴸ samples) =
  contractStep sample refl
    (design-contract-run design
      (step design
            (stimulusEvent sample)
            (stimulusInputs sample)
            state)
      samples)

design-contract-implements :
  ∀ {inputCount outputCount registerCount}
    (design : Design inputCount outputCount registerCount)
  → Refinement.Implements
      (DesignMachine.asMachine design)
      (contractSystem (designContract design))
design-contract-implements design = DesignMachine.designImplements design

design-contract-trace :
  ∀ {inputCount outputCount registerCount}
    (design : Design inputCount outputCount registerCount)
    (samples : List (Machine.Stimulus (Vec Bit inputCount) Event))
  → StrongContractExecution (designContract design) samples
      (Machine.run (DesignMachine.asMachine design)
        (initial design) samples)
design-contract-trace design samples =
  Trace.machineTrace (DesignMachine.asMachine design) samples

-- Quarantine is a wrapper with explicit assumptions and traceability.  It is
-- intentionally a different type from an assumption-free Design.

record QuarantinedDesign
  (inputCount outputCount stateCount : ℕ) : Type₁ where
  constructor quarantinedDesign
  field
    contractName      : String
    contractEvidence  : RuleTraceability
    visibleAssumptions : List String
    behaviorContract  : Contract {ℓ-zero} inputCount outputCount stateCount

open QuarantinedDesign public