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

module Spartan6.Examples.GenericSemantics where

open import Spartan6.Prelude

import Spartan6.Examples.Toggle as Toggle
import Spartan6.Semantics.Contract as Contract
import Spartan6.Semantics.Design as Flat
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

open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty

genericTwoTicks :
  List (Machine.Stimulus (Vec Bit 1) Flat.Event)
genericTwoTicks = mapList DesignMachine.toGenericStimulus Toggle.twoTicks

toggle-generic-reduction :
  Machine.run (DesignMachine.asMachine Toggle.toggle)
    (Machine.initialState (DesignMachine.asMachine Toggle.toggle))
    genericTwoTicks
  ≡ low ∷ []
toggle-generic-reduction = refl

toggle-whole-example-preserved :
  Machine.run (DesignMachine.asMachine Toggle.toggle)
    (Flat.initial Toggle.toggle) genericTwoTicks
  ≡ Flat.run Toggle.toggle (Flat.initial Toggle.toggle) Toggle.twoTicks
toggle-whole-example-preserved =
  DesignMachine.run-preserved Toggle.toggle
    (Flat.initial Toggle.toggle) Toggle.twoTicks

toggle-strong-contract-trace :
  Contract.StrongContractExecution
    (Contract.designContract Toggle.toggle) genericTwoTicks
    (low ∷ [])
toggle-strong-contract-trace =
  subst
    (Contract.StrongContractExecution
      (Contract.designContract Toggle.toggle) genericTwoTicks)
    toggle-generic-reduction
    (Contract.design-contract-trace Toggle.toggle genericTwoTicks)

-- A compact different-state proof probe: the executable state is one bit,
-- while the relational specification retains two synchronized copies.

edgeStep : Bit → Bit → Bit
edgeStep false state = state
edgeStep true state = not state

singleToggle : Machine.Machine Unit Bit Bit Bit
singleToggle = Machine.machine low (λ input state → state)
  (λ event input state → edgeStep event state)

duplicatedSystem : System.System Unit Bit Bit (Bit × Bit)
System.Initial duplicatedSystem state = (low , low) ≡ state
System.ObservationAllowed duplicatedSystem input state output =
  fst state ≡ output
System.TransitionAllowed duplicatedSystem event input before after =
  (edgeStep event (fst before) , edgeStep event (fst before)) ≡ after

singleImplementsDuplicated :
  Refinement.Implements singleToggle duplicatedSystem
Refinement.StateRelation singleImplementsDuplicated machine-state system-state =
  (machine-state ≡ fst system-state)
  × (machine-state ≡ snd system-state)
Refinement.specificationInitial singleImplementsDuplicated = low , low
Refinement.initialAllowed singleImplementsDuplicated = refl
Refinement.initialRelated singleImplementsDuplicated = refl , refl
Refinement.observationPreserved singleImplementsDuplicated
  input machine-state system-state related = sym (fst related)
Refinement.transitionPreserved singleImplementsDuplicated
  event input machine-state system-state related =
  (edgeStep event machine-state , edgeStep event machine-state)
  , sym (cong
      (λ state →
        edgeStep event state , edgeStep event state)
      (fst related))
  , (refl , refl)

different-state-trace :
  Σ[ final ∈ (Bit × Bit) ]
    Trace.Trace duplicatedSystem
      (Machine.stimulus tt true ∷ᴸ []ᴸ) final
different-state-trace =
  Refinement.implementation-trace singleImplementsDuplicated
    (Machine.stimulus tt true ∷ᴸ []ᴸ)

duplicated-high-is-not-initial :
  System.Initial duplicatedSystem (high , high) → Empty.⊥
duplicated-high-is-not-initial path =
  false≢true (cong fst path)