SemanticExplanation.Industry.Spartan

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

module SemanticExplanation.Industry.Spartan where

open import Agda.Builtin.Reflection using (Name)
open import Agda.Builtin.List
  renaming ([] to []L ; _∷_ to _∷L_)
open import SemanticExplanation
open import Spartan6.Prelude
open import Spartan6.Netlist.Expression
open import Spartan6.Semantics.Design

import Spartan6.Examples.StateDomains as StateDomains
import Spartan6.Semantics.Invariant as Invariant
import Spartan6.Semantics.Simulation as Simulation

------------------------------------------------------------------------
-- A concrete application of the checked, untimed Spartan-6 semantics.
--
-- This is a synchronous, redundant motor-permit interlock.  It is intended
-- to illustrate logic-level assurance for an industrial control design.  It
-- does not model contactor mechanics, analogue emergency-stop circuitry,
-- clock-domain crossing, metastability, propagation delay, or timing closure.

guardDoorClosedSignal : Expr 3 2
guardDoorClosedSignal = input fzero

emergencyStopLoopHealthySignal : Expr 3 2
emergencyStopLoopHealthySignal = input (fsuc fzero)

restartCommandSignal : Expr 3 2
restartCommandSignal = input (fsuc (fsuc fzero))

motorPermitNext : Expr 3 2
motorPermitNext =
  (guardDoorClosedSignal andE emergencyStopLoopHealthySignal)
  andE restartCommandSignal

firstMotorPermit secondMotorPermit : Expr 3 2
firstMotorPermit = register fzero
secondMotorPermit = register (fsuc fzero)

redundantMotorInterlock : Design 3 2 2
redundantMotorInterlock =
  mkDesign
    (low ∷ low ∷ [])
    (firstMotorPermit ∷ secondMotorPermit ∷ [])
    (motorPermitNext ∷ motorPermitNext ∷ [])

MotorPermitChannelsSynchronized :
  State redundantMotorInterlock → Type₀
MotorPermitChannelsSynchronized (first ∷ second ∷ []) = first ≡ second

motorPermitChannelsInvariant :
  Invariant.Invariant
    redundantMotorInterlock MotorPermitChannelsSynchronized
Invariant.initially motorPermitChannelsInvariant = refl
Invariant.preserved motorPermitChannelsInvariant idle
  (guardClosed ∷ stopLoopHealthy ∷ restartRequested ∷ [])
  (first ∷ second ∷ []) synchronized = synchronized
Invariant.preserved motorPermitChannelsInvariant risingEdge
  (guardClosed ∷ stopLoopHealthy ∷ restartRequested ∷ [])
  (first ∷ second ∷ []) synchronized = refl

------------------------------------------------------------------------
-- Application-level statement vocabulary.  Each proposition below expands
-- to a checked fact about the concrete Design; the explainer dispatches on
-- its quoted Name and does not infer meaning from the printed identifier.

record AuditedControlSequence : Type₀ where
  constructor audited-control-sequence
  field
    samples : List (Stimulus 3)

open AuditedControlSequence public

RedundantChannelsRemainSynchronized :
  AuditedControlSequence → Type₀
RedundantChannelsRemainSynchronized trace =
  MotorPermitChannelsSynchronized
    (run redundantMotorInterlock
      (initial redundantMotorInterlock) (samples trace))

allAuditedControlSequencesPreserveRedundancy :
  (trace : AuditedControlSequence) →
  RedundantChannelsRemainSynchronized trace
allAuditedControlSequencesPreserveRedundancy
  (audited-control-sequence controlSamples) =
  Invariant.initial-run-preserves
    motorPermitChannelsInvariant controlSamples

record SafetyPanelInput : Type₀ where
  constructor safety-panel-input
  field
    guardDoorClosed : Bit
    emergencyStopLoopHealthy : Bit
    restartCommandPresent : Bit

open SafetyPanelInput public

panelBits : SafetyPanelInput → Vec Bit 3
panelBits panel =
  guardDoorClosed panel
  ∷ emergencyStopLoopHealthy panel
  ∷ restartCommandPresent panel
  ∷ []

record MotorInterlockState : Type₀ where
  constructor motor-interlock-state
  field
    stateBits : Vec Bit 2

open MotorInterlockState public

record RecordedMotorControlCycle : Type₀ where
  constructor recorded-motor-control-cycle
  field
    panel : SafetyPanelInput
    before : MotorInterlockState
    after : MotorInterlockState

open RecordedMotorControlCycle public

PerimeterGuardDoorIsClosed : RecordedMotorControlCycle → Type₀
PerimeterGuardDoorIsClosed cycle =
  guardDoorClosed (panel cycle) ≡ high

EmergencyStopSafetyLoopIsHealthy : RecordedMotorControlCycle → Type₀
EmergencyStopSafetyLoopIsHealthy cycle =
  emergencyStopLoopHealthy (panel cycle) ≡ high

RestartCommandIsPresent : RecordedMotorControlCycle → Type₀
RestartCommandIsPresent cycle =
  restartCommandPresent (panel cycle) ≡ high

EmergencyStopSafetyLoopIsTripped : RecordedMotorControlCycle → Type₀
EmergencyStopSafetyLoopIsTripped cycle =
  emergencyStopLoopHealthy (panel cycle) ≡ low

RecordedRisingEdgeUpdateIsValid : RecordedMotorControlCycle → Type₀
RecordedRisingEdgeUpdateIsValid cycle =
  Transition redundantMotorInterlock risingEdge
    (panelBits (panel cycle))
    (stateBits (before cycle))
    (stateBits (after cycle))

BothMotorPermitChannelsAreEnergized :
  RecordedMotorControlCycle → Type₀
BothMotorPermitChannelsAreEnergized cycle =
  stateBits (after cycle) ≡ high ∷ high ∷ []

BothMotorPermitChannelsAreDeEnergized :
  RecordedMotorControlCycle → Type₀
BothMotorPermitChannelsAreDeEnergized cycle =
  stateBits (after cycle) ≡ low ∷ low ∷ []

permitBit : Bit → Bit → Bit → Bit
permitBit guardClosed stopLoopHealthy restartRequested =
  (guardClosed and stopLoopHealthy) and restartRequested

healthyPermitIsHigh : ∀ guardClosed stopLoopHealthy restartRequested →
  guardClosed ≡ high →
  stopLoopHealthy ≡ high →
  restartRequested ≡ high →
  permitBit guardClosed stopLoopHealthy restartRequested ≡ high
healthyPermitIsHigh guardClosed stopLoopHealthy restartRequested
  guardClosedProof stopLoopHealthyProof restartRequestedProof =
  cong (λ guard → permitBit guard stopLoopHealthy restartRequested)
    guardClosedProof
  ∙ cong (λ stopLoop → permitBit high stopLoop restartRequested)
    stopLoopHealthyProof
  ∙ cong (permitBit high high) restartRequestedProof

trippedPermitIsLow : ∀ guardClosed stopLoopHealthy restartRequested →
  stopLoopHealthy ≡ low →
  permitBit guardClosed stopLoopHealthy restartRequested ≡ low
trippedPermitIsLow false stopLoopHealthy restartRequested tripProof =
  cong (λ stopLoop → permitBit false stopLoop restartRequested) tripProof
trippedPermitIsLow true stopLoopHealthy restartRequested tripProof =
  cong (λ stopLoop → permitBit true stopLoop restartRequested) tripProof

healthyRestartEnergizesBothMotorPermitChannels :
  (event : RecordedMotorControlCycle) →
  PerimeterGuardDoorIsClosed event →
  EmergencyStopSafetyLoopIsHealthy event →
  RestartCommandIsPresent event →
  RecordedRisingEdgeUpdateIsValid event →
  BothMotorPermitChannelsAreEnergized event
healthyRestartEnergizesBothMotorPermitChannels
  (recorded-motor-control-cycle
    (safety-panel-input guardClosed stopLoopHealthy restartRequested)
    (motor-interlock-state stateBefore)
  (motor-interlock-state stateAfter))
  guardClosedProof stopLoopHealthyProof restartRequestedProof transitionProof =
  sym transitionProof
  ∙ cong (λ permit → permit ∷ permit ∷ [])
      (healthyPermitIsHigh
        guardClosed stopLoopHealthy restartRequested
        guardClosedProof stopLoopHealthyProof restartRequestedProof)

emergencyStopTripDropsBothMotorPermitChannels :
  (event : RecordedMotorControlCycle) →
  EmergencyStopSafetyLoopIsTripped event →
  RecordedRisingEdgeUpdateIsValid event →
  BothMotorPermitChannelsAreDeEnergized event
emergencyStopTripDropsBothMotorPermitChannels
  (recorded-motor-control-cycle
    (safety-panel-input guardClosed stopLoopHealthy restartRequested)
    (motor-interlock-state stateBefore)
    (motor-interlock-state stateAfter))
  stopLoopTripped transitionProof =
  sym transitionProof
  ∙ cong (λ permit → permit ∷ permit ∷ [])
      (trippedPermitIsLow
        guardClosed stopLoopHealthy restartRequested stopLoopTripped)

------------------------------------------------------------------------
-- Audited semantic adapter and finite deterministic readings.

spartanIndustrialDomain : DomainSpec
spartanIndustrialDomain =
  domain-spec
    "ff-spartan6-industrial-motor-interlock-v1"
    ( entity-rule "spartan.industry.entity.audit-trace"
        (quote AuditedControlSequence) []L "audited control sequence"
    ∷L entity-rule "spartan.industry.entity.motor-cycle"
        (quote RecordedMotorControlCycle) []L "recorded motor-control cycle"
    ∷L []L )
    ( predicate-rule "spartan.industry.predicate.redundancy-preserved"
        (quote RedundantChannelsRemainSynchronized)
        (semanticExpression ∷L []L)
        (unarySuffix
          "leaves the two motor-permit register channels synchronized in the final state reached after its sampled control sequence")
    ∷L predicate-rule "spartan.industry.predicate.guard-closed"
        (quote PerimeterGuardDoorIsClosed)
        (semanticExpression ∷L []L)
        (unarySuffix "reports the perimeter guard door closed")
    ∷L predicate-rule "spartan.industry.predicate.estop-healthy"
        (quote EmergencyStopSafetyLoopIsHealthy)
        (semanticExpression ∷L []L)
        (unarySuffix "reports the emergency-stop safety loop healthy")
    ∷L predicate-rule "spartan.industry.predicate.restart-present"
        (quote RestartCommandIsPresent)
        (semanticExpression ∷L []L)
        (unarySuffix "contains an operator restart command")
    ∷L predicate-rule "spartan.industry.predicate.estop-tripped"
        (quote EmergencyStopSafetyLoopIsTripped)
        (semanticExpression ∷L []L)
        (unarySuffix "reports the emergency-stop safety loop tripped")
    ∷L predicate-rule "spartan.industry.predicate.valid-rising-update"
        (quote RecordedRisingEdgeUpdateIsValid)
        (semanticExpression ∷L []L)
        (unarySuffix
          "is a valid rising-edge update of the redundant motor interlock")
    ∷L predicate-rule "spartan.industry.predicate.both-permits-high"
        (quote BothMotorPermitChannelsAreEnergized)
        (semanticExpression ∷L []L)
        (unarySuffix "leaves both redundant motor-permit channels energized")
    ∷L predicate-rule "spartan.industry.predicate.both-permits-low"
        (quote BothMotorPermitChannelsAreDeEnergized)
        (semanticExpression ∷L []L)
        (unarySuffix "leaves both redundant motor-permit channels de-energized")
    ∷L []L )
    []L []L []L 512

-- These quoted target declarations are the live formalisation evidence used
-- by the application.  They also make the direct-vs-adapter boundary explicit.
liveInitialRunInvariantTheorem : Name
liveInitialRunInvariantTheorem = quote Invariant.initial-run-preserves

liveSimulationRunTheorem : Name
liveSimulationRunTheorem = quote Simulation.initial-runs-related

liveSimultaneousDomainExample : Name
liveSimultaneousDomainExample = quote StateDomains.two-domain-simultaneous-update

finiteRunExplanation : Explanation
finiteRunExplanation =
  explainNameCompact spartanIndustrialDomain
    allAuditedControlSequencesPreserveRedundancy

finiteRunExplanationText :
  Explanation.text finiteRunExplanation ≡
  "For every audited control sequence trace, trace leaves the two motor-permit register channels synchronized in the final state reached after its sampled control sequence."
finiteRunExplanationText = refl

healthyRestartExplanation : Explanation
healthyRestartExplanation =
  explainNameCompact spartanIndustrialDomain
    healthyRestartEnergizesBothMotorPermitChannels

healthyRestartExplanationText :
  Explanation.text healthyRestartExplanation ≡
  "For every recorded motor-control cycle event, if event reports the perimeter guard door closed, event reports the emergency-stop safety loop healthy, event contains an operator restart command, and event is a valid rising-edge update of the redundant motor interlock, then event leaves both redundant motor-permit channels energized."
healthyRestartExplanationText = refl

emergencyStopTripExplanation : Explanation
emergencyStopTripExplanation =
  explainNameCompact spartanIndustrialDomain
    emergencyStopTripDropsBothMotorPermitChannels

emergencyStopTripExplanationText :
  Explanation.text emergencyStopTripExplanation ≡
  "For every recorded motor-control cycle event, if event reports the emergency-stop safety loop tripped and event is a valid rising-edge update of the redundant motor interlock, then event leaves both redundant motor-permit channels de-energized."
emergencyStopTripExplanationText = refl

finiteRunExplanationProvenance :
  Explanation.provenance finiteRunExplanation ≡
  ( ruleUsed "spartan.industry.entity.audit-trace"
  ∷L ruleUsed "spartan.industry.predicate.redundancy-preserved"
  ∷L []L )
finiteRunExplanationProvenance = refl

healthyRestartExplanationProvenance :
  Explanation.provenance healthyRestartExplanation ≡
  ( ruleUsed "spartan.industry.entity.motor-cycle"
  ∷L ruleUsed "spartan.industry.predicate.guard-closed"
  ∷L ruleUsed "spartan.industry.predicate.estop-healthy"
  ∷L ruleUsed "spartan.industry.predicate.restart-present"
  ∷L ruleUsed "spartan.industry.predicate.valid-rising-update"
  ∷L ruleUsed "spartan.industry.predicate.both-permits-high"
  ∷L []L )
healthyRestartExplanationProvenance = refl

emergencyStopTripExplanationProvenance :
  Explanation.provenance emergencyStopTripExplanation ≡
  ( ruleUsed "spartan.industry.entity.motor-cycle"
  ∷L ruleUsed "spartan.industry.predicate.estop-tripped"
  ∷L ruleUsed "spartan.industry.predicate.valid-rising-update"
  ∷L ruleUsed "spartan.industry.predicate.both-permits-low"
  ∷L []L )
emergencyStopTripExplanationProvenance = refl