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

module Spartan6.Hierarchy.StableCompose where

open import Spartan6.Prelude
open import Spartan6.Hierarchy.Interface using (appendVec)

open import Cubical.Data.FinData.Base using (weakenFin; fromℕ)
open import Cubical.Data.Nat.Properties using (+-zero; +-suc)

import Spartan6.Netlist.StableDAG as Stable
import Spartan6.Primitive.LUT as LUT

-- Resource arithmetic ------------------------------------------------------

leftFin : ∀ {leftCount} (rightCount : ℕ)
  -> Fin leftCount -> Fin (leftCount + rightCount)
leftFin {zero} rightCount ()
leftFin {suc leftCount} rightCount fzero = fzero
leftFin {suc leftCount} rightCount (fsuc index) =
  fsuc (leftFin rightCount index)

rightFin : ∀ (leftCount : ℕ) {rightCount}
  -> Fin rightCount -> Fin (leftCount + rightCount)
rightFin zero index = index
rightFin (suc leftCount) index = fsuc (rightFin leftCount index)

lookup-leftFin-append : ∀ {ℓ} {A : Type ℓ}
  {leftCount rightCount}
  (index : Fin leftCount)
  (left : Vec A leftCount) (right : Vec A rightCount)
  -> lookup (leftFin rightCount index) (appendVec left right)
    ≡ lookup index left
lookup-leftFin-append {leftCount = zero} () [] right
lookup-leftFin-append {leftCount = suc leftCount}
  fzero (item ∷ left) right = refl
lookup-leftFin-append {leftCount = suc leftCount}
  (fsuc index) (item ∷ left) right =
  lookup-leftFin-append index left right

lookup-rightFin-append : ∀ {ℓ} {A : Type ℓ}
  {leftCount rightCount}
  (index : Fin rightCount)
  (left : Vec A leftCount) (right : Vec A rightCount)
  -> lookup (rightFin leftCount index) (appendVec left right)
    ≡ lookup index right
lookup-rightFin-append {leftCount = zero} index [] right = refl
lookup-rightFin-append {leftCount = suc leftCount}
  index (item ∷ left) right =
  lookup-rightFin-append index left right

extendFinMap : ∀ {sourceCount targetCount}
  -> (Fin sourceCount -> Fin targetCount)
  -> Fin (suc sourceCount) -> Fin (suc targetCount)
extendFinMap {sourceCount = zero} {targetCount} mapping fzero =
  fromℕ targetCount
extendFinMap {sourceCount = suc sourceCount} mapping fzero =
  weakenFin (mapping fzero)
extendFinMap {sourceCount = suc sourceCount} mapping (fsuc index) =
  extendFinMap (λ old -> mapping (fsuc old)) index

lookup-extendFinMap-snoc : ∀ {ℓ} {A : Type ℓ}
  {sourceCount targetCount}
  (mapping : Fin sourceCount -> Fin targetCount)
  (source : Vec A sourceCount) (target : Vec A targetCount)
  -> (∀ index -> lookup (mapping index) target ≡ lookup index source)
  -> (source-new target-new : A)
  -> target-new ≡ source-new
  -> (index : Fin (suc sourceCount))
  -> lookup (extendFinMap mapping index) (Stable.snoc target target-new)
    ≡ lookup index (Stable.snoc source source-new)
lookup-extendFinMap-snoc {sourceCount = zero} {targetCount}
  mapping [] target old-agreement source-new target-new new-agreement
  fzero =
  Stable.lookup-last-snoc target target-new
  ∙ new-agreement
lookup-extendFinMap-snoc {sourceCount = suc sourceCount}
  mapping (item ∷ source) target old-agreement
  source-new target-new new-agreement fzero =
  Stable.lookup-weaken-snoc (mapping fzero) target target-new
  ∙ old-agreement fzero
lookup-extendFinMap-snoc {sourceCount = suc sourceCount}
  mapping (item ∷ source) target old-agreement
  source-new target-new new-agreement (fsuc index) =
  lookup-extendFinMap-snoc
    (λ old -> mapping (fsuc old)) source target
    (λ old -> old-agreement (fsuc old))
    source-new target-new new-agreement index

lookup-evaluateWires :
  ∀ {inputCount stateCount localCount count}
  (external : Vec Bit inputCount)
  (state : Vec Bit stateCount)
  (locals : Vec Bit localCount)
  (index : Fin count)
  (wires : Vec (Stable.StableWire inputCount stateCount localCount) count)
  -> lookup index
      (Stable.stableEvaluateWires external state locals wires)
    ≡ Stable.stableEvaluateWire external state locals
        (lookup index wires)
lookup-evaluateWires external state locals fzero (wire ∷ wires) = refl
lookup-evaluateWires external state locals (fsuc index) (wire ∷ wires) =
  lookup-evaluateWires external state locals index wires

weakenWire : ∀ {inputCount stateCount localCount}
  -> Stable.StableWire inputCount stateCount localCount
  -> Stable.StableWire inputCount stateCount (suc localCount)
weakenWire (Stable.stableExternal index) = Stable.stableExternal index
weakenWire (Stable.stableStored index) = Stable.stableStored index
weakenWire (Stable.stableLocal index) =
  Stable.stableLocal (weakenFin index)
weakenWire (Stable.stableLiteral bit) = Stable.stableLiteral bit

weakenWire-evaluation :
  ∀ {inputCount stateCount localCount}
  (external : Vec Bit inputCount)
  (state : Vec Bit stateCount)
  (locals : Vec Bit localCount)
  (new-local : Bit)
  (wire : Stable.StableWire inputCount stateCount localCount)
  -> Stable.stableEvaluateWire external state
      (Stable.snoc locals new-local) (weakenWire wire)
    ≡ Stable.stableEvaluateWire external state locals wire
weakenWire-evaluation external state locals new-local
  (Stable.stableExternal index) = refl
weakenWire-evaluation external state locals new-local
  (Stable.stableStored index) = refl
weakenWire-evaluation external state locals new-local
  (Stable.stableLocal index) =
  Stable.lookup-weaken-snoc index locals new-local
weakenWire-evaluation external state locals new-local
  (Stable.stableLiteral bit) = refl

evaluateMappedWires :
  ∀ {sourceInput sourceState sourceLocal
    targetInput targetState targetLocal count}
  (source-external : Vec Bit sourceInput)
  (source-state : Vec Bit sourceState)
  (source-locals : Vec Bit sourceLocal)
  (target-external : Vec Bit targetInput)
  (target-state : Vec Bit targetState)
  (target-locals : Vec Bit targetLocal)
  (mapping : Stable.StableWire sourceInput sourceState sourceLocal
    -> Stable.StableWire targetInput targetState targetLocal)
  -> (∀ wire ->
      Stable.stableEvaluateWire target-external target-state target-locals
        (mapping wire)
      ≡ Stable.stableEvaluateWire source-external source-state
          source-locals wire)
  -> (wires : Vec
      (Stable.StableWire sourceInput sourceState sourceLocal) count)
  -> Stable.stableEvaluateWires target-external target-state target-locals
      (map mapping wires)
    ≡ Stable.stableEvaluateWires source-external source-state
        source-locals wires
evaluateMappedWires source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement [] = refl
evaluateMappedWires source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement
  (wire ∷ wires) =
  cong₂ _∷_
    (wire-agreement wire)
    (evaluateMappedWires source-external source-state source-locals
      target-external target-state target-locals mapping wire-agreement
      wires)

evaluateWires-append :
  ∀ {inputCount stateCount localCount leftCount rightCount}
  (external : Vec Bit inputCount)
  (state : Vec Bit stateCount)
  (locals : Vec Bit localCount)
  (left : Vec (Stable.StableWire inputCount stateCount localCount)
    leftCount)
  (right : Vec (Stable.StableWire inputCount stateCount localCount)
    rightCount)
  -> Stable.stableEvaluateWires external state locals
      (appendVec left right)
    ≡ appendVec
        (Stable.stableEvaluateWires external state locals left)
        (Stable.stableEvaluateWires external state locals right)
evaluateWires-append external state locals [] right = refl
evaluateWires-append external state locals (wire ∷ left) right =
  cong
    (Stable.stableEvaluateWire external state locals wire ∷_)
    (evaluateWires-append external state locals left right)

mapNode :
  ∀ {sourceInput sourceState sourceLocal
    targetInput targetState targetLocal}
  -> (Stable.StableWire sourceInput sourceState sourceLocal
    -> Stable.StableWire targetInput targetState targetLocal)
  -> Stable.StableNode sourceInput sourceState sourceLocal
  -> Stable.StableNode targetInput targetState targetLocal
mapNode mapping (Stable.stableInvert wire) =
  Stable.stableInvert (mapping wire)
mapNode mapping (Stable.stableAnd left right) =
  Stable.stableAnd (mapping left) (mapping right)
mapNode mapping (Stable.stableOr left right) =
  Stable.stableOr (mapping left) (mapping right)
mapNode mapping (Stable.stableXor left right) =
  Stable.stableXor (mapping left) (mapping right)
mapNode mapping (Stable.stableMux select when-low when-high) =
  Stable.stableMux
    (mapping select) (mapping when-low) (mapping when-high)
mapNode mapping (Stable.stableLUT table arguments) =
  Stable.stableLUT table (map mapping arguments)

mapNode-evaluation :
  ∀ {sourceInput sourceState sourceLocal
    targetInput targetState targetLocal}
  (source-external : Vec Bit sourceInput)
  (source-state : Vec Bit sourceState)
  (source-locals : Vec Bit sourceLocal)
  (target-external : Vec Bit targetInput)
  (target-state : Vec Bit targetState)
  (target-locals : Vec Bit targetLocal)
  (mapping : Stable.StableWire sourceInput sourceState sourceLocal
    -> Stable.StableWire targetInput targetState targetLocal)
  -> (∀ wire ->
      Stable.stableEvaluateWire target-external target-state target-locals
        (mapping wire)
      ≡ Stable.stableEvaluateWire source-external source-state
          source-locals wire)
  -> (node : Stable.StableNode sourceInput sourceState sourceLocal)
  -> Stable.stableEvaluateNode target-external target-state target-locals
      (mapNode mapping node)
    ≡ Stable.stableEvaluateNode source-external source-state
        source-locals node
mapNode-evaluation source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement
  (Stable.stableInvert wire) = cong not (wire-agreement wire)
mapNode-evaluation source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement
  (Stable.stableAnd left right) =
  cong₂ _and_ (wire-agreement left) (wire-agreement right)
mapNode-evaluation source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement
  (Stable.stableOr left right) =
  cong₂ _or_ (wire-agreement left) (wire-agreement right)
mapNode-evaluation source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement
  (Stable.stableXor left right) =
  cong₂ _⊕_ (wire-agreement left) (wire-agreement right)
mapNode-evaluation source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement
  (Stable.stableMux select when-low when-high) =
  cong₃ mux
    (wire-agreement select)
    (wire-agreement when-low)
    (wire-agreement when-high)
mapNode-evaluation source-external source-state source-locals
  target-external target-state target-locals mapping wire-agreement
  (Stable.stableLUT table arguments) =
  cong (LUT.evalLUT table)
    (evaluateMappedWires source-external source-state source-locals
      target-external target-state target-locals mapping wire-agreement
      arguments)

-- The source `StableNodes` spine is snoc-indexed while natural addition is
-- left-recursive.  Keeping the target local count existential avoids a
-- transport at every appended node.  `serialLocalCount-correct` below exposes
-- the expected arithmetic fact once at the resource boundary.

record SerialSpine
  {inputCount middleCount leftStateCount rightStateCount leftLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  {rightLocalCount}
  (right-nodes : Stable.StableNodes middleCount
    rightStateCount rightLocalCount) : Type₀ where
  field
    serialTargetLocalCount : ℕ
    serialTargetNodes : Stable.StableNodes inputCount
      (leftStateCount + rightStateCount) serialTargetLocalCount
    serialLeftLocalMap : Fin leftLocalCount -> Fin serialTargetLocalCount
    serialRightLocalMap : Fin rightLocalCount -> Fin serialTargetLocalCount
    serialTargetCountCorrect :
      serialTargetLocalCount ≡ leftLocalCount + rightLocalCount

open SerialSpine public

serialSpineLeftWire :
  ∀ {inputCount middleCount leftStateCount rightStateCount
    leftLocalCount rightLocalCount}
  {left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount}
  {right-nodes : Stable.StableNodes middleCount
    rightStateCount rightLocalCount}
  (spine : SerialSpine left right-nodes)
  -> Stable.StableWire inputCount leftStateCount leftLocalCount
  -> Stable.StableWire inputCount (leftStateCount + rightStateCount)
      (serialTargetLocalCount spine)
serialSpineLeftWire spine (Stable.stableExternal index) =
  Stable.stableExternal index
serialSpineLeftWire {rightStateCount = rightStateCount}
  spine (Stable.stableStored index) =
  Stable.stableStored (leftFin rightStateCount index)
serialSpineLeftWire spine (Stable.stableLocal index) =
  Stable.stableLocal (serialLeftLocalMap spine index)
serialSpineLeftWire spine (Stable.stableLiteral bit) =
  Stable.stableLiteral bit

serialSpineRightWire :
  ∀ {inputCount middleCount leftStateCount rightStateCount
    leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  {right-nodes : Stable.StableNodes middleCount
    rightStateCount rightLocalCount}
  (spine : SerialSpine left right-nodes)
  -> Stable.StableWire middleCount rightStateCount rightLocalCount
  -> Stable.StableWire inputCount (leftStateCount + rightStateCount)
      (serialTargetLocalCount spine)
serialSpineRightWire left spine (Stable.stableExternal index) =
  serialSpineLeftWire spine (lookup index (Stable.stableOutputs left))
serialSpineRightWire {leftStateCount = leftStateCount}
  left spine (Stable.stableStored index) =
  Stable.stableStored (rightFin leftStateCount index)
serialSpineRightWire left spine (Stable.stableLocal index) =
  Stable.stableLocal (serialRightLocalMap spine index)
serialSpineRightWire left spine (Stable.stableLiteral bit) =
  Stable.stableLiteral bit

serialBaseWire :
  ∀ {inputCount leftStateCount rightStateCount localCount}
  -> Stable.StableWire inputCount leftStateCount localCount
  -> Stable.StableWire inputCount
      (leftStateCount + rightStateCount) localCount
serialBaseWire (Stable.stableExternal index) = Stable.stableExternal index
serialBaseWire {rightStateCount = rightStateCount}
  (Stable.stableStored index) =
  Stable.stableStored (leftFin rightStateCount index)
serialBaseWire (Stable.stableLocal index) = Stable.stableLocal index
serialBaseWire (Stable.stableLiteral bit) = Stable.stableLiteral bit

mapSerialBaseNodes :
  ∀ {inputCount leftStateCount rightStateCount localCount}
  -> Stable.StableNodes inputCount leftStateCount localCount
  -> Stable.StableNodes inputCount
      (leftStateCount + rightStateCount) localCount
mapSerialBaseNodes Stable.stableNoNodes = Stable.stableNoNodes
mapSerialBaseNodes (nodes Stable.▹ node) =
  mapSerialBaseNodes nodes Stable.▹ mapNode serialBaseWire node

buildSerialSpine :
  ∀ {inputCount middleCount leftStateCount rightStateCount
    leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right-nodes : Stable.StableNodes middleCount
    rightStateCount rightLocalCount)
  -> SerialSpine left right-nodes
serialTargetLocalCount
  (buildSerialSpine left Stable.stableNoNodes) = _
serialTargetNodes
  (buildSerialSpine left Stable.stableNoNodes) =
  mapSerialBaseNodes (Stable.stableNodeSpine left)
serialLeftLocalMap
  (buildSerialSpine left Stable.stableNoNodes) index = index
serialRightLocalMap
  (buildSerialSpine left Stable.stableNoNodes) ()
serialTargetCountCorrect
  (buildSerialSpine {leftLocalCount = leftLocalCount}
    left Stable.stableNoNodes) =
  sym (+-zero leftLocalCount)
serialTargetLocalCount
  (buildSerialSpine left (right-nodes Stable.▹ right-node)) =
  suc (serialTargetLocalCount prefix)
  where
  prefix = buildSerialSpine left right-nodes
serialTargetNodes
  (buildSerialSpine left (right-nodes Stable.▹ right-node)) =
  serialTargetNodes prefix Stable.▹
    mapNode (serialSpineRightWire left prefix) right-node
  where
  prefix = buildSerialSpine left right-nodes
serialLeftLocalMap
  (buildSerialSpine left (right-nodes Stable.▹ right-node)) index =
  weakenFin (serialLeftLocalMap prefix index)
  where
  prefix = buildSerialSpine left right-nodes
serialRightLocalMap
  (buildSerialSpine left (right-nodes Stable.▹ right-node)) index =
  extendFinMap (serialRightLocalMap prefix) index
  where
  prefix = buildSerialSpine left right-nodes
serialTargetCountCorrect
  (buildSerialSpine {leftLocalCount = leftLocalCount}
    left (right-nodes Stable.▹ right-node)) =
  cong suc (serialTargetCountCorrect prefix)
  ∙ sym (+-suc leftLocalCount _)
  where
  prefix = buildSerialSpine left right-nodes

serialSpineLeftWire-step :
  ∀ {inputCount middleCount leftStateCount rightStateCount
    leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right-nodes : Stable.StableNodes middleCount
    rightStateCount rightLocalCount)
  (right-node : Stable.StableNode middleCount
    rightStateCount rightLocalCount)
  (wire : Stable.StableWire inputCount leftStateCount leftLocalCount)
  -> serialSpineLeftWire
      (buildSerialSpine left (right-nodes Stable.▹ right-node)) wire
    ≡ weakenWire
        (serialSpineLeftWire (buildSerialSpine left right-nodes) wire)
serialSpineLeftWire-step left right-nodes right-node
  (Stable.stableExternal index) = refl
serialSpineLeftWire-step left right-nodes right-node
  (Stable.stableStored index) = refl
serialSpineLeftWire-step left right-nodes right-node
  (Stable.stableLocal index) = refl
serialSpineLeftWire-step left right-nodes right-node
  (Stable.stableLiteral bit) = refl

serialBaseWire-evaluation :
  ∀ {inputCount leftStateCount rightStateCount localCount}
  (external : Vec Bit inputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  (locals : Vec Bit localCount)
  (wire : Stable.StableWire inputCount leftStateCount localCount)
  -> Stable.stableEvaluateWire external
      (appendVec left-state right-state) locals
      (serialBaseWire wire)
    ≡ Stable.stableEvaluateWire external left-state locals wire
serialBaseWire-evaluation external left-state right-state locals
  (Stable.stableExternal index) = refl
serialBaseWire-evaluation external left-state right-state locals
  (Stable.stableStored index) =
  lookup-leftFin-append index left-state right-state
serialBaseWire-evaluation external left-state right-state locals
  (Stable.stableLocal index) = refl
serialBaseWire-evaluation external left-state right-state locals
  (Stable.stableLiteral bit) = refl

serialBaseNodes-evaluation :
  ∀ {inputCount leftStateCount rightStateCount localCount}
  (nodes : Stable.StableNodes inputCount leftStateCount localCount)
  (external : Vec Bit inputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> Stable.stableEvaluateNodes (mapSerialBaseNodes nodes)
      external (appendVec left-state right-state)
    ≡ Stable.stableEvaluateNodes nodes external left-state
serialBaseNodes-evaluation Stable.stableNoNodes
  external left-state right-state = refl
serialBaseNodes-evaluation (nodes Stable.▹ node)
  external left-state right-state =
  cong₂ Stable.snoc previous-agreement
    (cong
      (λ locals ->
        Stable.stableEvaluateNode external
          (appendVec left-state right-state) locals
          (mapNode serialBaseWire node))
      previous-agreement
    ∙ mapNode-evaluation external left-state
        (Stable.stableEvaluateNodes nodes external left-state)
        external (appendVec left-state right-state)
        (Stable.stableEvaluateNodes nodes external left-state)
        serialBaseWire
        (serialBaseWire-evaluation external left-state right-state
          (Stable.stableEvaluateNodes nodes external left-state))
        node)
  where
  previous-agreement =
    serialBaseNodes-evaluation nodes external left-state right-state

serialBaseCorrect :
  ∀ {inputCount middleCount leftStateCount rightStateCount
    leftLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (external : Vec Bit inputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  (wire : Stable.StableWire inputCount leftStateCount leftLocalCount)
  -> Stable.stableEvaluateWire external
      (appendVec left-state right-state)
      (Stable.stableEvaluateNodes
        (mapSerialBaseNodes (Stable.stableNodeSpine left))
        external (appendVec left-state right-state))
      (serialBaseWire wire)
    ≡ Stable.stableEvaluateWire external left-state
        (Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
          external left-state)
        wire
serialBaseCorrect left external left-state right-state wire =
  cong
    (λ locals ->
      Stable.stableEvaluateWire external
        (appendVec left-state right-state) locals
        (serialBaseWire wire))
    (serialBaseNodes-evaluation (Stable.stableNodeSpine left)
      external left-state right-state)
  ∙ serialBaseWire-evaluation external left-state right-state
      (Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
        external left-state)
      wire

record SerialSpineCorrect
  {inputCount middleCount leftStateCount rightStateCount leftLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  {rightLocalCount}
  (right-nodes : Stable.StableNodes middleCount
    rightStateCount rightLocalCount)
  (spine : SerialSpine left right-nodes)
  (external : Vec Bit inputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount) : Type₀ where
  private
    target-locals =
      Stable.stableEvaluateNodes (serialTargetNodes spine)
        external (appendVec left-state right-state)
    left-locals =
      Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
        external left-state
    middle =
      Stable.stableDirectOutputs left external left-state
    right-locals =
      Stable.stableEvaluateNodes right-nodes middle right-state
  field
    serialLeftWireCorrect : ∀ wire ->
      Stable.stableEvaluateWire external
        (appendVec left-state right-state) target-locals
        (serialSpineLeftWire spine wire)
      ≡ Stable.stableEvaluateWire external left-state left-locals wire
    serialRightWireCorrect : ∀ wire ->
      Stable.stableEvaluateWire external
        (appendVec left-state right-state) target-locals
        (serialSpineRightWire left spine wire)
      ≡ Stable.stableEvaluateWire middle right-state right-locals wire

open SerialSpineCorrect public

serialSpineCorrect :
  ∀ {inputCount middleCount leftStateCount rightStateCount
    leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right-nodes : Stable.StableNodes middleCount
    rightStateCount rightLocalCount)
  (external : Vec Bit inputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> SerialSpineCorrect left right-nodes
      (buildSerialSpine left right-nodes)
      external left-state right-state
serialLeftWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableExternal index) =
  serialBaseCorrect left external left-state right-state
    (Stable.stableExternal index)
serialLeftWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableStored index) =
  serialBaseCorrect left external left-state right-state
    (Stable.stableStored index)
serialLeftWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableLocal index) =
  serialBaseCorrect left external left-state right-state
    (Stable.stableLocal index)
serialLeftWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableLiteral bit) =
  serialBaseCorrect left external left-state right-state
    (Stable.stableLiteral bit)
serialRightWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableExternal index) =
  serialLeftWireCorrect
    (serialSpineCorrect left Stable.stableNoNodes
      external left-state right-state)
    (lookup index (Stable.stableOutputs left))
  ∙ sym
      (lookup-evaluateWires external left-state
        (Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
          external left-state)
        index (Stable.stableOutputs left))
serialRightWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableStored index) =
  lookup-rightFin-append index left-state right-state
serialRightWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableLocal ())
serialRightWireCorrect
  (serialSpineCorrect left Stable.stableNoNodes
    external left-state right-state)
  (Stable.stableLiteral bit) = refl
serialLeftWireCorrect
  (serialSpineCorrect left (right-nodes Stable.▹ right-node)
    external left-state right-state)
  wire =
  cong
    (Stable.stableEvaluateWire external
      (appendVec left-state right-state)
      (Stable.snoc prefix-target-locals target-new-value))
    (serialSpineLeftWire-step left right-nodes right-node wire)
  ∙ weakenWire-evaluation external (appendVec left-state right-state)
    prefix-target-locals target-new-value
    (serialSpineLeftWire prefix wire)
  ∙ serialLeftWireCorrect prefix-correct wire
  where
  prefix = buildSerialSpine left right-nodes
  prefix-correct =
    serialSpineCorrect left right-nodes external left-state right-state
  prefix-target-locals =
    Stable.stableEvaluateNodes (serialTargetNodes prefix)
      external (appendVec left-state right-state)
  target-new-value =
    Stable.stableEvaluateNode external
      (appendVec left-state right-state) prefix-target-locals
      (mapNode (serialSpineRightWire left prefix) right-node)
serialRightWireCorrect
  (serialSpineCorrect left (right-nodes Stable.▹ right-node)
    external left-state right-state)
  (Stable.stableExternal index) =
  cong
    (Stable.stableEvaluateWire external
      (appendVec left-state right-state)
      (Stable.snoc prefix-target-locals target-new-value))
    (serialSpineLeftWire-step left right-nodes right-node
      (lookup index (Stable.stableOutputs left)))
  ∙ weakenWire-evaluation external (appendVec left-state right-state)
      prefix-target-locals target-new-value
      (serialSpineLeftWire prefix
        (lookup index (Stable.stableOutputs left)))
  ∙ serialLeftWireCorrect prefix-correct
      (lookup index (Stable.stableOutputs left))
  ∙ sym
      (lookup-evaluateWires external left-state left-locals
        index (Stable.stableOutputs left))
  where
  prefix = buildSerialSpine left right-nodes
  prefix-correct =
    serialSpineCorrect left right-nodes external left-state right-state
  prefix-target-locals =
    Stable.stableEvaluateNodes (serialTargetNodes prefix)
      external (appendVec left-state right-state)
  target-new-value =
    Stable.stableEvaluateNode external
      (appendVec left-state right-state) prefix-target-locals
      (mapNode (serialSpineRightWire left prefix) right-node)
  left-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
      external left-state
serialRightWireCorrect
  (serialSpineCorrect left (right-nodes Stable.▹ right-node)
    external left-state right-state)
  (Stable.stableStored index) =
  lookup-rightFin-append index left-state right-state
serialRightWireCorrect
  (serialSpineCorrect left (right-nodes Stable.▹ right-node)
    external left-state right-state)
  (Stable.stableLocal index) =
  lookup-extendFinMap-snoc
    (serialRightLocalMap prefix)
    source-locals target-locals
    (λ old ->
      serialRightWireCorrect prefix-correct (Stable.stableLocal old))
    source-new-value target-new-value new-value-agreement index
  where
  prefix = buildSerialSpine left right-nodes
  prefix-correct =
    serialSpineCorrect left right-nodes external left-state right-state
  target-locals =
    Stable.stableEvaluateNodes (serialTargetNodes prefix)
      external (appendVec left-state right-state)
  middle = Stable.stableDirectOutputs left external left-state
  source-locals =
    Stable.stableEvaluateNodes right-nodes middle right-state
  source-new-value =
    Stable.stableEvaluateNode middle right-state source-locals right-node
  target-new-value =
    Stable.stableEvaluateNode external
      (appendVec left-state right-state) target-locals
      (mapNode (serialSpineRightWire left prefix) right-node)
  new-value-agreement =
    mapNode-evaluation middle right-state source-locals
      external (appendVec left-state right-state) target-locals
      (serialSpineRightWire left prefix)
      (serialRightWireCorrect prefix-correct) right-node
serialRightWireCorrect
  (serialSpineCorrect left (right-nodes Stable.▹ right-node)
    external left-state right-state)
  (Stable.stableLiteral bit) = refl

serialSpineFor :
  ∀ {inputCount middleCount outputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist middleCount outputCount
    rightStateCount rightLocalCount)
  -> SerialSpine left (Stable.stableNodeSpine right)
serialSpineFor left right =
  buildSerialSpine left (Stable.stableNodeSpine right)

serialLocalCount :
  ∀ {inputCount middleCount outputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist middleCount outputCount
    rightStateCount rightLocalCount)
  -> ℕ
serialLocalCount left right =
  serialTargetLocalCount (serialSpineFor left right)

serialLocalCount-correct :
  ∀ {inputCount middleCount outputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist middleCount outputCount
    rightStateCount rightLocalCount)
  -> serialLocalCount left right ≡ leftLocalCount + rightLocalCount
serialLocalCount-correct left right =
  serialTargetCountCorrect (serialSpineFor left right)

serialNetlist :
  ∀ {inputCount middleCount outputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist middleCount outputCount
    rightStateCount rightLocalCount)
  -> Stable.StableNetlist inputCount outputCount
      (leftStateCount + rightStateCount)
      (serialLocalCount left right)
serialNetlist left right =
  Stable.stableNetlist
    (appendVec (Stable.stableInitial left) (Stable.stableInitial right))
    (serialTargetNodes spine)
    (map (serialSpineRightWire left spine) (Stable.stableOutputs right))
    (appendVec
      (map (serialSpineLeftWire spine) (Stable.stableNext left))
      (map (serialSpineRightWire left spine) (Stable.stableNext right)))
  where
  spine = serialSpineFor left right

serialOutputs-evaluation :
  ∀ {inputCount middleCount outputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist middleCount outputCount
    rightStateCount rightLocalCount)
  (external : Vec Bit inputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> Stable.stableDirectOutputs (serialNetlist left right)
      external (appendVec left-state right-state)
    ≡ Stable.stableDirectOutputs right
        (Stable.stableDirectOutputs left external left-state)
        right-state
serialOutputs-evaluation left right external left-state right-state =
  evaluateMappedWires
    (Stable.stableDirectOutputs left external left-state)
    right-state right-locals
    external (appendVec left-state right-state) target-locals
    (serialSpineRightWire left spine)
    (serialRightWireCorrect correctness)
    (Stable.stableOutputs right)
  where
  spine = serialSpineFor left right
  correctness = serialSpineCorrect left (Stable.stableNodeSpine right)
    external left-state right-state
  target-locals =
    Stable.stableEvaluateNodes (serialTargetNodes spine)
      external (appendVec left-state right-state)
  right-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine right)
      (Stable.stableDirectOutputs left external left-state) right-state

serialNext-evaluation :
  ∀ {inputCount middleCount outputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist inputCount middleCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist middleCount outputCount
    rightStateCount rightLocalCount)
  (external : Vec Bit inputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> Stable.stableDirectNext (serialNetlist left right)
      external (appendVec left-state right-state)
    ≡ appendVec
        (Stable.stableDirectNext left external left-state)
        (Stable.stableDirectNext right
          (Stable.stableDirectOutputs left external left-state)
          right-state)
serialNext-evaluation left right external left-state right-state =
  evaluateWires-append target-external target-state target-locals
    (map (serialSpineLeftWire spine) (Stable.stableNext left))
    (map (serialSpineRightWire left spine) (Stable.stableNext right))
  ∙ cong₂ appendVec
      (evaluateMappedWires external left-state left-locals
        target-external target-state target-locals
        (serialSpineLeftWire spine)
        (serialLeftWireCorrect correctness)
        (Stable.stableNext left))
      (evaluateMappedWires middle right-state right-locals
        target-external target-state target-locals
        (serialSpineRightWire left spine)
        (serialRightWireCorrect correctness)
        (Stable.stableNext right))
  where
  spine = serialSpineFor left right
  correctness = serialSpineCorrect left (Stable.stableNodeSpine right)
    external left-state right-state
  target-external = external
  target-state = appendVec left-state right-state
  target-locals =
    Stable.stableEvaluateNodes (serialTargetNodes spine)
      target-external target-state
  left-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
      external left-state
  middle = Stable.stableDirectOutputs left external left-state
  right-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine right)
      middle right-state

-- Parallel composition -----------------------------------------------------

record ParallelSpine
  {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  {rightLocalCount}
  (right-nodes : Stable.StableNodes rightInputCount
    rightStateCount rightLocalCount) : Type₀ where
  field
    parallelTargetLocalCount : ℕ
    parallelTargetNodes : Stable.StableNodes
      (leftInputCount + rightInputCount)
      (leftStateCount + rightStateCount)
      parallelTargetLocalCount
    parallelLeftLocalMap : Fin leftLocalCount -> Fin parallelTargetLocalCount
    parallelRightLocalMap : Fin rightLocalCount -> Fin parallelTargetLocalCount
    parallelTargetCountCorrect :
      parallelTargetLocalCount ≡ leftLocalCount + rightLocalCount

open ParallelSpine public

parallelSpineLeftWire :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount rightLocalCount}
  {left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount}
  {right-nodes : Stable.StableNodes rightInputCount
    rightStateCount rightLocalCount}
  (spine : ParallelSpine left right-nodes)
  -> Stable.StableWire leftInputCount leftStateCount leftLocalCount
  -> Stable.StableWire
      (leftInputCount + rightInputCount)
      (leftStateCount + rightStateCount)
      (parallelTargetLocalCount spine)
parallelSpineLeftWire {rightInputCount = rightInputCount}
  spine (Stable.stableExternal index) =
  Stable.stableExternal (leftFin rightInputCount index)
parallelSpineLeftWire {rightStateCount = rightStateCount}
  spine (Stable.stableStored index) =
  Stable.stableStored (leftFin rightStateCount index)
parallelSpineLeftWire spine (Stable.stableLocal index) =
  Stable.stableLocal (parallelLeftLocalMap spine index)
parallelSpineLeftWire spine (Stable.stableLiteral bit) =
  Stable.stableLiteral bit

parallelSpineRightWire :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount rightLocalCount}
  {left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount}
  {right-nodes : Stable.StableNodes rightInputCount
    rightStateCount rightLocalCount}
  (spine : ParallelSpine left right-nodes)
  -> Stable.StableWire rightInputCount rightStateCount rightLocalCount
  -> Stable.StableWire
      (leftInputCount + rightInputCount)
      (leftStateCount + rightStateCount)
      (parallelTargetLocalCount spine)
parallelSpineRightWire {leftInputCount = leftInputCount}
  spine (Stable.stableExternal index) =
  Stable.stableExternal (rightFin leftInputCount index)
parallelSpineRightWire {leftStateCount = leftStateCount}
  spine (Stable.stableStored index) =
  Stable.stableStored (rightFin leftStateCount index)
parallelSpineRightWire spine (Stable.stableLocal index) =
  Stable.stableLocal (parallelRightLocalMap spine index)
parallelSpineRightWire spine (Stable.stableLiteral bit) =
  Stable.stableLiteral bit

parallelBaseWire :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    localCount}
  -> Stable.StableWire leftInputCount leftStateCount localCount
  -> Stable.StableWire
      (leftInputCount + rightInputCount)
      (leftStateCount + rightStateCount) localCount
parallelBaseWire {rightInputCount = rightInputCount}
  (Stable.stableExternal index) =
  Stable.stableExternal (leftFin rightInputCount index)
parallelBaseWire {rightStateCount = rightStateCount}
  (Stable.stableStored index) =
  Stable.stableStored (leftFin rightStateCount index)
parallelBaseWire (Stable.stableLocal index) = Stable.stableLocal index
parallelBaseWire (Stable.stableLiteral bit) = Stable.stableLiteral bit

mapParallelBaseNodes :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    localCount}
  -> Stable.StableNodes leftInputCount leftStateCount localCount
  -> Stable.StableNodes
      (leftInputCount + rightInputCount)
      (leftStateCount + rightStateCount) localCount
mapParallelBaseNodes Stable.stableNoNodes = Stable.stableNoNodes
mapParallelBaseNodes (nodes Stable.▹ node) =
  mapParallelBaseNodes nodes Stable.▹ mapNode parallelBaseWire node

buildParallelSpine :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right-nodes : Stable.StableNodes rightInputCount
    rightStateCount rightLocalCount)
  -> ParallelSpine left right-nodes
parallelTargetLocalCount
  (buildParallelSpine left Stable.stableNoNodes) = _
parallelTargetNodes
  (buildParallelSpine left Stable.stableNoNodes) =
  mapParallelBaseNodes (Stable.stableNodeSpine left)
parallelLeftLocalMap
  (buildParallelSpine left Stable.stableNoNodes) index = index
parallelRightLocalMap
  (buildParallelSpine left Stable.stableNoNodes) ()
parallelTargetCountCorrect
  (buildParallelSpine {leftLocalCount = leftLocalCount}
    left Stable.stableNoNodes) =
  sym (+-zero leftLocalCount)
parallelTargetLocalCount
  (buildParallelSpine left (right-nodes Stable.▹ right-node)) =
  suc (parallelTargetLocalCount prefix)
  where
  prefix = buildParallelSpine left right-nodes
parallelTargetNodes
  (buildParallelSpine left (right-nodes Stable.▹ right-node)) =
  parallelTargetNodes prefix Stable.▹
    mapNode (parallelSpineRightWire prefix) right-node
  where
  prefix = buildParallelSpine left right-nodes
parallelLeftLocalMap
  (buildParallelSpine left (right-nodes Stable.▹ right-node)) index =
  weakenFin (parallelLeftLocalMap prefix index)
  where
  prefix = buildParallelSpine left right-nodes
parallelRightLocalMap
  (buildParallelSpine left (right-nodes Stable.▹ right-node)) index =
  extendFinMap (parallelRightLocalMap prefix) index
  where
  prefix = buildParallelSpine left right-nodes
parallelTargetCountCorrect
  (buildParallelSpine {leftLocalCount = leftLocalCount}
    left (right-nodes Stable.▹ right-node)) =
  cong suc (parallelTargetCountCorrect prefix)
  ∙ sym (+-suc leftLocalCount _)
  where
  prefix = buildParallelSpine left right-nodes

parallelSpineLeftWire-step :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right-nodes : Stable.StableNodes rightInputCount
    rightStateCount rightLocalCount)
  (right-node : Stable.StableNode rightInputCount
    rightStateCount rightLocalCount)
  (wire : Stable.StableWire leftInputCount leftStateCount leftLocalCount)
  -> parallelSpineLeftWire
      (buildParallelSpine left (right-nodes Stable.▹ right-node)) wire
    ≡ weakenWire
        (parallelSpineLeftWire (buildParallelSpine left right-nodes) wire)
parallelSpineLeftWire-step left right-nodes right-node
  (Stable.stableExternal index) = refl
parallelSpineLeftWire-step left right-nodes right-node
  (Stable.stableStored index) = refl
parallelSpineLeftWire-step left right-nodes right-node
  (Stable.stableLocal index) = refl
parallelSpineLeftWire-step left right-nodes right-node
  (Stable.stableLiteral bit) = refl

parallelBaseWire-evaluation :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    localCount}
  (left-input : Vec Bit leftInputCount)
  (right-input : Vec Bit rightInputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  (locals : Vec Bit localCount)
  (wire : Stable.StableWire leftInputCount leftStateCount localCount)
  -> Stable.stableEvaluateWire
      (appendVec left-input right-input)
      (appendVec left-state right-state) locals
      (parallelBaseWire wire)
    ≡ Stable.stableEvaluateWire left-input left-state locals wire
parallelBaseWire-evaluation left-input right-input left-state right-state
  locals (Stable.stableExternal index) =
  lookup-leftFin-append index left-input right-input
parallelBaseWire-evaluation left-input right-input left-state right-state
  locals (Stable.stableStored index) =
  lookup-leftFin-append index left-state right-state
parallelBaseWire-evaluation left-input right-input left-state right-state
  locals (Stable.stableLocal index) = refl
parallelBaseWire-evaluation left-input right-input left-state right-state
  locals (Stable.stableLiteral bit) = refl

parallelBaseNodes-evaluation :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    localCount}
  (nodes : Stable.StableNodes leftInputCount leftStateCount localCount)
  (left-input : Vec Bit leftInputCount)
  (right-input : Vec Bit rightInputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> Stable.stableEvaluateNodes (mapParallelBaseNodes nodes)
      (appendVec left-input right-input)
      (appendVec left-state right-state)
    ≡ Stable.stableEvaluateNodes nodes left-input left-state
parallelBaseNodes-evaluation Stable.stableNoNodes
  left-input right-input left-state right-state = refl
parallelBaseNodes-evaluation (nodes Stable.▹ node)
  left-input right-input left-state right-state =
  cong₂ Stable.snoc previous-agreement
    (cong
      (λ locals ->
        Stable.stableEvaluateNode
          (appendVec left-input right-input)
          (appendVec left-state right-state) locals
          (mapNode parallelBaseWire node))
      previous-agreement
    ∙ mapNode-evaluation left-input left-state
        (Stable.stableEvaluateNodes nodes left-input left-state)
        (appendVec left-input right-input)
        (appendVec left-state right-state)
        (Stable.stableEvaluateNodes nodes left-input left-state)
        parallelBaseWire
        (parallelBaseWire-evaluation left-input right-input
          left-state right-state
          (Stable.stableEvaluateNodes nodes left-input left-state))
        node)
  where
  previous-agreement =
    parallelBaseNodes-evaluation nodes
      left-input right-input left-state right-state

parallelBaseCorrect :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (left-input : Vec Bit leftInputCount)
  (right-input : Vec Bit rightInputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  (wire : Stable.StableWire leftInputCount leftStateCount leftLocalCount)
  -> Stable.stableEvaluateWire
      (appendVec left-input right-input)
      (appendVec left-state right-state)
      (Stable.stableEvaluateNodes
        (mapParallelBaseNodes (Stable.stableNodeSpine left))
        (appendVec left-input right-input)
        (appendVec left-state right-state))
      (parallelBaseWire wire)
    ≡ Stable.stableEvaluateWire left-input left-state
        (Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
          left-input left-state)
        wire
parallelBaseCorrect left left-input right-input left-state right-state wire =
  cong
    (λ locals ->
      Stable.stableEvaluateWire
        (appendVec left-input right-input)
        (appendVec left-state right-state) locals
        (parallelBaseWire wire))
    (parallelBaseNodes-evaluation (Stable.stableNodeSpine left)
      left-input right-input left-state right-state)
  ∙ parallelBaseWire-evaluation left-input right-input
      left-state right-state
      (Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
        left-input left-state)
      wire

record ParallelSpineCorrect
  {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  {rightLocalCount}
  (right-nodes : Stable.StableNodes rightInputCount
    rightStateCount rightLocalCount)
  (spine : ParallelSpine left right-nodes)
  (left-input : Vec Bit leftInputCount)
  (right-input : Vec Bit rightInputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount) : Type₀ where
  private
    target-input = appendVec left-input right-input
    target-state = appendVec left-state right-state
    target-locals =
      Stable.stableEvaluateNodes (parallelTargetNodes spine)
        target-input target-state
    left-locals =
      Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
        left-input left-state
    right-locals =
      Stable.stableEvaluateNodes right-nodes right-input right-state
  field
    parallelLeftWireCorrect : ∀ wire ->
      Stable.stableEvaluateWire target-input target-state target-locals
        (parallelSpineLeftWire spine wire)
      ≡ Stable.stableEvaluateWire left-input left-state left-locals wire
    parallelRightWireCorrect : ∀ wire ->
      Stable.stableEvaluateWire target-input target-state target-locals
        (parallelSpineRightWire spine wire)
      ≡ Stable.stableEvaluateWire right-input right-state right-locals wire

open ParallelSpineCorrect public

parallelSpineCorrect :
  ∀ {leftInputCount rightInputCount leftStateCount rightStateCount
    leftOutputCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right-nodes : Stable.StableNodes rightInputCount
    rightStateCount rightLocalCount)
  (left-input : Vec Bit leftInputCount)
  (right-input : Vec Bit rightInputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> ParallelSpineCorrect left right-nodes
      (buildParallelSpine left right-nodes)
      left-input right-input left-state right-state
parallelLeftWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableExternal index) =
  parallelBaseCorrect left left-input right-input left-state right-state
    (Stable.stableExternal index)
parallelLeftWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableStored index) =
  parallelBaseCorrect left left-input right-input left-state right-state
    (Stable.stableStored index)
parallelLeftWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableLocal index) =
  parallelBaseCorrect left left-input right-input left-state right-state
    (Stable.stableLocal index)
parallelLeftWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableLiteral bit) =
  parallelBaseCorrect left left-input right-input left-state right-state
    (Stable.stableLiteral bit)
parallelRightWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableExternal index) =
  lookup-rightFin-append index left-input right-input
parallelRightWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableStored index) =
  lookup-rightFin-append index left-state right-state
parallelRightWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableLocal ())
parallelRightWireCorrect
  (parallelSpineCorrect left Stable.stableNoNodes
    left-input right-input left-state right-state)
  (Stable.stableLiteral bit) = refl
parallelLeftWireCorrect
  (parallelSpineCorrect left (right-nodes Stable.▹ right-node)
    left-input right-input left-state right-state)
  wire =
  cong
    (Stable.stableEvaluateWire target-input target-state
      (Stable.snoc prefix-target-locals target-new-value))
    (parallelSpineLeftWire-step left right-nodes right-node wire)
  ∙ weakenWire-evaluation target-input target-state
      prefix-target-locals target-new-value
      (parallelSpineLeftWire prefix wire)
  ∙ parallelLeftWireCorrect prefix-correct wire
  where
  prefix = buildParallelSpine left right-nodes
  prefix-correct = parallelSpineCorrect left right-nodes
    left-input right-input left-state right-state
  target-input = appendVec left-input right-input
  target-state = appendVec left-state right-state
  prefix-target-locals =
    Stable.stableEvaluateNodes (parallelTargetNodes prefix)
      target-input target-state
  target-new-value =
    Stable.stableEvaluateNode target-input target-state
      prefix-target-locals
      (mapNode (parallelSpineRightWire prefix) right-node)
parallelRightWireCorrect
  (parallelSpineCorrect left (right-nodes Stable.▹ right-node)
    left-input right-input left-state right-state)
  (Stable.stableExternal index) =
  lookup-rightFin-append index left-input right-input
parallelRightWireCorrect
  (parallelSpineCorrect left (right-nodes Stable.▹ right-node)
    left-input right-input left-state right-state)
  (Stable.stableStored index) =
  lookup-rightFin-append index left-state right-state
parallelRightWireCorrect
  (parallelSpineCorrect left (right-nodes Stable.▹ right-node)
    left-input right-input left-state right-state)
  (Stable.stableLocal index) =
  lookup-extendFinMap-snoc
    (parallelRightLocalMap prefix)
    source-locals target-locals
    (λ old ->
      parallelRightWireCorrect prefix-correct (Stable.stableLocal old))
    source-new-value target-new-value new-value-agreement index
  where
  prefix = buildParallelSpine left right-nodes
  prefix-correct = parallelSpineCorrect left right-nodes
    left-input right-input left-state right-state
  target-input = appendVec left-input right-input
  target-state = appendVec left-state right-state
  target-locals =
    Stable.stableEvaluateNodes (parallelTargetNodes prefix)
      target-input target-state
  source-locals =
    Stable.stableEvaluateNodes right-nodes right-input right-state
  source-new-value =
    Stable.stableEvaluateNode right-input right-state
      source-locals right-node
  target-new-value =
    Stable.stableEvaluateNode target-input target-state
      target-locals
      (mapNode (parallelSpineRightWire prefix) right-node)
  new-value-agreement =
    mapNode-evaluation right-input right-state source-locals
      target-input target-state target-locals
      (parallelSpineRightWire prefix)
      (parallelRightWireCorrect prefix-correct) right-node
parallelRightWireCorrect
  (parallelSpineCorrect left (right-nodes Stable.▹ right-node)
    left-input right-input left-state right-state)
  (Stable.stableLiteral bit) = refl

parallelSpineFor :
  ∀ {leftInputCount rightInputCount leftOutputCount rightOutputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist rightInputCount rightOutputCount
    rightStateCount rightLocalCount)
  -> ParallelSpine left (Stable.stableNodeSpine right)
parallelSpineFor left right =
  buildParallelSpine left (Stable.stableNodeSpine right)

parallelLocalCount :
  ∀ {leftInputCount rightInputCount leftOutputCount rightOutputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist rightInputCount rightOutputCount
    rightStateCount rightLocalCount)
  -> ℕ
parallelLocalCount left right =
  parallelTargetLocalCount (parallelSpineFor left right)

parallelLocalCount-correct :
  ∀ {leftInputCount rightInputCount leftOutputCount rightOutputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist rightInputCount rightOutputCount
    rightStateCount rightLocalCount)
  -> parallelLocalCount left right ≡ leftLocalCount + rightLocalCount
parallelLocalCount-correct left right =
  parallelTargetCountCorrect (parallelSpineFor left right)

parallelNetlist :
  ∀ {leftInputCount rightInputCount leftOutputCount rightOutputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist rightInputCount rightOutputCount
    rightStateCount rightLocalCount)
  -> Stable.StableNetlist
      (leftInputCount + rightInputCount)
      (leftOutputCount + rightOutputCount)
      (leftStateCount + rightStateCount)
      (parallelLocalCount left right)
parallelNetlist left right =
  Stable.stableNetlist
    (appendVec (Stable.stableInitial left) (Stable.stableInitial right))
    (parallelTargetNodes spine)
    (appendVec
      (map (parallelSpineLeftWire spine) (Stable.stableOutputs left))
      (map (parallelSpineRightWire spine) (Stable.stableOutputs right)))
    (appendVec
      (map (parallelSpineLeftWire spine) (Stable.stableNext left))
      (map (parallelSpineRightWire spine) (Stable.stableNext right)))
  where
  spine = parallelSpineFor left right

parallelOutputs-evaluation :
  ∀ {leftInputCount rightInputCount leftOutputCount rightOutputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist rightInputCount rightOutputCount
    rightStateCount rightLocalCount)
  (left-input : Vec Bit leftInputCount)
  (right-input : Vec Bit rightInputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> Stable.stableDirectOutputs (parallelNetlist left right)
      (appendVec left-input right-input)
      (appendVec left-state right-state)
    ≡ appendVec
        (Stable.stableDirectOutputs left left-input left-state)
        (Stable.stableDirectOutputs right right-input right-state)
parallelOutputs-evaluation left right
  left-input right-input left-state right-state =
  evaluateWires-append target-input target-state target-locals
    (map (parallelSpineLeftWire spine) (Stable.stableOutputs left))
    (map (parallelSpineRightWire spine) (Stable.stableOutputs right))
  ∙ cong₂ appendVec
      (evaluateMappedWires left-input left-state left-locals
        target-input target-state target-locals
        (parallelSpineLeftWire spine)
        (parallelLeftWireCorrect correctness)
        (Stable.stableOutputs left))
      (evaluateMappedWires right-input right-state right-locals
        target-input target-state target-locals
        (parallelSpineRightWire spine)
        (parallelRightWireCorrect correctness)
        (Stable.stableOutputs right))
  where
  spine = parallelSpineFor left right
  correctness = parallelSpineCorrect left (Stable.stableNodeSpine right)
    left-input right-input left-state right-state
  target-input = appendVec left-input right-input
  target-state = appendVec left-state right-state
  target-locals =
    Stable.stableEvaluateNodes (parallelTargetNodes spine)
      target-input target-state
  left-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
      left-input left-state
  right-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine right)
      right-input right-state

parallelNext-evaluation :
  ∀ {leftInputCount rightInputCount leftOutputCount rightOutputCount
    leftStateCount rightStateCount leftLocalCount rightLocalCount}
  (left : Stable.StableNetlist leftInputCount leftOutputCount
    leftStateCount leftLocalCount)
  (right : Stable.StableNetlist rightInputCount rightOutputCount
    rightStateCount rightLocalCount)
  (left-input : Vec Bit leftInputCount)
  (right-input : Vec Bit rightInputCount)
  (left-state : Vec Bit leftStateCount)
  (right-state : Vec Bit rightStateCount)
  -> Stable.stableDirectNext (parallelNetlist left right)
      (appendVec left-input right-input)
      (appendVec left-state right-state)
    ≡ appendVec
        (Stable.stableDirectNext left left-input left-state)
        (Stable.stableDirectNext right right-input right-state)
parallelNext-evaluation left right
  left-input right-input left-state right-state =
  evaluateWires-append target-input target-state target-locals
    (map (parallelSpineLeftWire spine) (Stable.stableNext left))
    (map (parallelSpineRightWire spine) (Stable.stableNext right))
  ∙ cong₂ appendVec
      (evaluateMappedWires left-input left-state left-locals
        target-input target-state target-locals
        (parallelSpineLeftWire spine)
        (parallelLeftWireCorrect correctness)
        (Stable.stableNext left))
      (evaluateMappedWires right-input right-state right-locals
        target-input target-state target-locals
        (parallelSpineRightWire spine)
        (parallelRightWireCorrect correctness)
        (Stable.stableNext right))
  where
  spine = parallelSpineFor left right
  correctness = parallelSpineCorrect left (Stable.stableNodeSpine right)
    left-input right-input left-state right-state
  target-input = appendVec left-input right-input
  target-state = appendVec left-state right-state
  target-locals =
    Stable.stableEvaluateNodes (parallelTargetNodes spine)
      target-input target-state
  left-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine left)
      left-input left-state
  right-locals =
    Stable.stableEvaluateNodes (Stable.stableNodeSpine right)
      right-input right-state