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

module Spartan6.Hierarchy.Flatten where

open import Spartan6.Prelude
open import Spartan6.Hierarchy.Interface
open import Cubical.Foundations.Transport using (subst⁻; substSubst⁻)

import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Hierarchy.StableCompose as Compose
import Spartan6.Netlist.Provenance as Netlist
import Spartan6.Netlist.StableDAG as Stable
import Spartan6.Semantics.Design as Flat
import Spartan6.Semantics.Machine as Machine
import Spartan6.Semantics.Refinement as Refinement

record FlatLeaf (Input Output : Interface) : Type₀ where
  constructor flatLeaf
  field
    leafStableId : ℕ
    leafName : String
    leafOrigin : Provenance.SourceOrigin
    leafStateCount : ℕ
    leafLocalCount : ℕ
    leafNetlist : Stable.StableNetlist
      (interfaceWidth Input) (interfaceWidth Output)
      leafStateCount leafLocalCount
    leafNodeOrigins : Vec Provenance.NodeOrigin leafLocalCount

open FlatLeaf public

replaceLeafNodeOrigins : ∀ {Input Output}
  -> (leaf : FlatLeaf Input Output)
  -> Vec Provenance.NodeOrigin (leafLocalCount leaf)
  -> FlatLeaf Input Output
replaceLeafNodeOrigins
  (flatLeaf stable-id name origin state-count local-count netlist old-origins)
  new-origins =
  flatLeaf stable-id name origin state-count local-count netlist new-origins

stableLeafMachine : ∀ {Input Output}
  -> (leaf : FlatLeaf Input Output)
  -> Machine.Machine
      (Environment Input) (Environment Output) Flat.Event
      (Vec Bit (leafStateCount leaf))
stableLeafMachine {Input = Input} {Output = Output} leaf =
  Machine.machine
    (Stable.stableInitial (leafNetlist leaf))
    (λ input state ->
      unflattenEnvironment {Output}
        (Stable.stableDirectOutputs
          (leafNetlist leaf) (flattenEnvironment {Input} input) state))
    step-leaf
  where
  step-leaf : Flat.Event
    -> Environment Input
    -> Vec Bit (leafStateCount leaf)
    -> Vec Bit (leafStateCount leaf)
  step-leaf Flat.idle input state = state
  step-leaf Flat.risingEdge input state =
    Stable.stableDirectNext
      (leafNetlist leaf) (flattenEnvironment {Input} input) state

leafComponent : ∀ {Input Output}
  -> (leaf : FlatLeaf Input Output)
  -> Component.Component Input Output Flat.Event
      (Vec Bit (leafStateCount leaf))
leafComponent leaf =
  Component.leafComponent
    (leafStableId leaf) (leafName leaf) (leafOrigin leaf)
    (stableLeafMachine leaf)

replaceLeafNodeOrigins-observe : ∀ {Input Output}
  (leaf : FlatLeaf Input Output)
  (origins : Vec Provenance.NodeOrigin (leafLocalCount leaf))
  input state
  -> Component.componentObserve
      (leafComponent (replaceLeafNodeOrigins leaf origins)) input state
    ≡ Component.componentObserve (leafComponent leaf) input state
replaceLeafNodeOrigins-observe
  (flatLeaf stable-id name origin state-count local-count netlist old-origins)
  origins input state = refl

replaceLeafNodeOrigins-step : ∀ {Input Output}
  (leaf : FlatLeaf Input Output)
  (origins : Vec Provenance.NodeOrigin (leafLocalCount leaf))
  event input state
  -> Component.componentStep
      (leafComponent (replaceLeafNodeOrigins leaf origins))
      event input state
    ≡ Component.componentStep (leafComponent leaf) event input state
replaceLeafNodeOrigins-step
  (flatLeaf stable-id name origin state-count local-count netlist old-origins)
  origins Flat.idle input state = refl
replaceLeafNodeOrigins-step
  (flatLeaf stable-id name origin state-count local-count netlist old-origins)
  origins Flat.risingEdge input state = refl

leaf-observation-flat : ∀ {Input Output}
  (leaf : FlatLeaf Input Output)
  (input : Environment Input)
  (state : Vec Bit (leafStateCount leaf))
  -> flattenEnvironment
      (Component.componentObserve (leafComponent leaf) input state)
    ≡ Stable.stableDirectOutputs
        (leafNetlist leaf) (flattenEnvironment input) state
leaf-observation-flat {Input = Input} {Output = Output} leaf input state =
  flatten-unflatten {Output}
    (Stable.stableDirectOutputs
      (leafNetlist leaf) (flattenEnvironment {Input} input) state)

leaf-rising-transition-flat : ∀ {Input Output}
  (leaf : FlatLeaf Input Output)
  (input : Environment Input)
  (state : Vec Bit (leafStateCount leaf))
  -> Component.componentStep (leafComponent leaf)
      Flat.risingEdge input state
    ≡ Stable.stableDirectNext
        (leafNetlist leaf) (flattenEnvironment input) state
leaf-rising-transition-flat leaf input state = refl

leaf-idle-transition-holds : ∀ {Input Output}
  (leaf : FlatLeaf Input Output)
  (input : Environment Input)
  (state : Vec Bit (leafStateCount leaf))
  -> Component.componentStep (leafComponent leaf) Flat.idle input state
    ≡ state
leaf-idle-transition-holds leaf input state = refl

record CertifiedFlattening
  {Input Output : Interface} {State : Type₀}
  (hierarchy : Component.Component Input Output Flat.Event State)
  : Type₁ where
  field
    flattenedLeaf : FlatLeaf Input Output
    StateRelation :
      State -> Vec Bit (leafStateCount flattenedLeaf) -> Type₀
    initialRelated :
      StateRelation
        (Component.componentInitial hierarchy)
        (Component.componentInitial (leafComponent flattenedLeaf))
    observationPreserved :
      ∀ input hierarchy-state flat-state
      -> StateRelation hierarchy-state flat-state
      -> Component.componentObserve hierarchy input hierarchy-state
        ≡ Component.componentObserve
            (leafComponent flattenedLeaf) input flat-state
    transitionPreserved :
      ∀ event input hierarchy-state flat-state
      -> StateRelation hierarchy-state flat-state
      -> StateRelation
          (Component.componentStep hierarchy event input hierarchy-state)
          (Component.componentStep
            (leafComponent flattenedLeaf) event input flat-state)

open CertifiedFlattening public

replaceFlatteningNodeOrigins :
  ∀ {Input Output State}
  {hierarchy : Component.Component Input Output Flat.Event State}
  -> (certificate : CertifiedFlattening hierarchy)
  -> Vec Provenance.NodeOrigin
      (leafLocalCount (flattenedLeaf certificate))
  -> CertifiedFlattening hierarchy
flattenedLeaf (replaceFlatteningNodeOrigins certificate origins) =
  replaceLeafNodeOrigins (flattenedLeaf certificate) origins
StateRelation (replaceFlatteningNodeOrigins certificate origins) =
  StateRelation certificate
initialRelated (replaceFlatteningNodeOrigins certificate origins) =
  initialRelated certificate
observationPreserved
  (replaceFlatteningNodeOrigins certificate origins)
  input hierarchy-state flat-state related =
  observationPreserved certificate
    input hierarchy-state flat-state related
  ∙ sym
      (replaceLeafNodeOrigins-observe
        (flattenedLeaf certificate) origins input flat-state)
transitionPreserved
  (replaceFlatteningNodeOrigins
    {hierarchy = hierarchy} certificate origins)
  event input hierarchy-state flat-state related =
  subst
    (StateRelation certificate
      (Component.componentStep hierarchy event input hierarchy-state))
    (sym
      (replaceLeafNodeOrigins-step
        (flattenedLeaf certificate) origins event input flat-state))
    (transitionPreserved certificate
      event input hierarchy-state flat-state related)

leafFlattens : ∀ {Input Output}
  (leaf : FlatLeaf Input Output)
  -> CertifiedFlattening (leafComponent leaf)
flattenedLeaf (leafFlattens leaf) = leaf
StateRelation (leafFlattens leaf) left right = left ≡ right
initialRelated (leafFlattens leaf) = refl
observationPreserved (leafFlattens leaf)
  input hierarchy-state flat-state related =
  cong (Component.componentObserve (leafComponent leaf) input) related
transitionPreserved (leafFlattens leaf)
  event input hierarchy-state flat-state related =
  cong (Component.componentStep (leafComponent leaf) event input) related

certificateImplements :
  ∀ {Input Output State}
  {hierarchy : Component.Component Input Output Flat.Event State}
  -> (certificate : CertifiedFlattening hierarchy)
  -> Refinement.Implements
      (Component.componentMachine hierarchy)
      (Machine.machineSystem
        (Component.componentMachine
          (leafComponent (flattenedLeaf certificate))))
Refinement.StateRelation (certificateImplements certificate) =
  StateRelation certificate
Refinement.specificationInitial (certificateImplements certificate) =
  Component.componentInitial (leafComponent (flattenedLeaf certificate))
Refinement.initialAllowed (certificateImplements certificate) = refl
Refinement.initialRelated (certificateImplements certificate) =
  initialRelated certificate
Refinement.observationPreserved (certificateImplements certificate)
  input hierarchy-state flat-state related =
  sym
    (observationPreserved certificate
      input hierarchy-state flat-state related)
Refinement.transitionPreserved (certificateImplements certificate)
  event input hierarchy-state flat-state related =
  Component.componentStep
      (leafComponent (flattenedLeaf certificate))
      event input flat-state
  , refl
  , transitionPreserved certificate
      event input hierarchy-state flat-state related

instantiateFlatLeaf : ∀ {Input Output}
  -> Netlist.OccurrenceId -> String
  -> FlatLeaf Input Output -> FlatLeaf Input Output
instantiateFlatLeaf occurrence name leaf =
  flatLeaf
    (Netlist.occurrenceOrdinal occurrence)
    name
    (Provenance.prependInstance occurrence (leafOrigin leaf))
    (leafStateCount leaf)
    (leafLocalCount leaf)
    (leafNetlist leaf)
    (Provenance.mapNodeOrigins occurrence (leafNodeOrigins leaf))

instantiateFlatLeaf-observe : ∀ {Input Output}
  (occurrence : Netlist.OccurrenceId) (name : String)
  (leaf : FlatLeaf Input Output)
  (input : Environment Input)
  (state : Vec Bit (leafStateCount leaf))
  -> Component.componentObserve
      (leafComponent (instantiateFlatLeaf occurrence name leaf)) input state
    ≡ Component.componentObserve (leafComponent leaf) input state
instantiateFlatLeaf-observe occurrence name
  (flatLeaf stable-id leaf-name origin state-count local-count
    netlist node-origins)
  input state = refl

instantiateFlatLeaf-step : ∀ {Input Output}
  (occurrence : Netlist.OccurrenceId) (name : String)
  (leaf : FlatLeaf Input Output)
  (event : Flat.Event)
  (input : Environment Input)
  (state : Vec Bit (leafStateCount leaf))
  -> Component.componentStep
      (leafComponent (instantiateFlatLeaf occurrence name leaf))
      event input state
    ≡ Component.componentStep (leafComponent leaf) event input state
instantiateFlatLeaf-step occurrence name
  (flatLeaf stable-id leaf-name origin state-count local-count
    netlist node-origins)
  Flat.idle input state = refl
instantiateFlatLeaf-step occurrence name
  (flatLeaf stable-id leaf-name origin state-count local-count
    netlist node-origins)
  Flat.risingEdge input state = refl

instantiatedLeafFlattens : ∀ {Input Output}
  (occurrence : Netlist.OccurrenceId) (name : String)
  (leaf : FlatLeaf Input Output)
  -> CertifiedFlattening
      (Component.instantiate occurrence name (leafComponent leaf))
flattenedLeaf (instantiatedLeafFlattens occurrence name leaf) =
  instantiateFlatLeaf occurrence name leaf
StateRelation (instantiatedLeafFlattens occurrence name leaf) left right =
  left ≡ right
initialRelated (instantiatedLeafFlattens occurrence name leaf) = refl
observationPreserved (instantiatedLeafFlattens occurrence name leaf)
  input hierarchy-state flat-state related =
  cong (Component.componentObserve (leafComponent leaf) input) related
  ∙ sym
      (instantiateFlatLeaf-observe occurrence name leaf input flat-state)
transitionPreserved (instantiatedLeafFlattens occurrence name leaf)
  event input hierarchy-state flat-state related =
  cong (Component.componentStep (leafComponent leaf) event input) related
  ∙ sym
      (instantiateFlatLeaf-step
        occurrence name leaf event input flat-state)

instantiateFlattens :
  ∀ {Input Output State}
  (occurrence : Netlist.OccurrenceId) (name : String)
  {hierarchy : Component.Component Input Output Flat.Event State}
  -> CertifiedFlattening hierarchy
  -> CertifiedFlattening (Component.instantiate occurrence name hierarchy)
flattenedLeaf (instantiateFlattens occurrence name certificate) =
  instantiateFlatLeaf occurrence name (flattenedLeaf certificate)
StateRelation (instantiateFlattens occurrence name certificate) =
  StateRelation certificate
initialRelated (instantiateFlattens occurrence name certificate) =
  initialRelated certificate
observationPreserved
  (instantiateFlattens occurrence name certificate)
  input hierarchy-state flat-state related =
  observationPreserved certificate
    input hierarchy-state flat-state related
  ∙ sym
      (instantiateFlatLeaf-observe occurrence name
        (flattenedLeaf certificate) input flat-state)
transitionPreserved
  (instantiateFlattens occurrence name
    {hierarchy = hierarchy} certificate)
  event input hierarchy-state flat-state related =
  subst
    (StateRelation certificate
      (Component.componentStep hierarchy
        event input hierarchy-state))
    (sym
      (instantiateFlatLeaf-step occurrence name
        (flattenedLeaf certificate) event input flat-state))
    (transitionPreserved certificate
      event input hierarchy-state flat-state related)

-- Certified structural flattening -----------------------------------------

combinedNodeOrigins : ∀ {leftCount rightCount targetCount}
  -> targetCount ≡ leftCount + rightCount
  -> Netlist.OccurrenceId -> Netlist.OccurrenceId
  -> Vec Provenance.NodeOrigin leftCount
  -> Vec Provenance.NodeOrigin rightCount
  -> Vec Provenance.NodeOrigin targetCount
combinedNodeOrigins count-correct left-occurrence right-occurrence
  left-origins right-origins =
  subst⁻ (Vec Provenance.NodeOrigin) count-correct
    (appendVec
      (Provenance.mapNodeOrigins left-occurrence left-origins)
      (Provenance.mapNodeOrigins right-occurrence right-origins))

combinedNodeOrigins-normalize : ∀ {leftCount rightCount targetCount}
  (count-correct : targetCount ≡ leftCount + rightCount)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left-origins : Vec Provenance.NodeOrigin leftCount)
  (right-origins : Vec Provenance.NodeOrigin rightCount)
  -> subst (Vec Provenance.NodeOrigin) count-correct
      (combinedNodeOrigins count-correct
        left-occurrence right-occurrence left-origins right-origins)
    ≡ appendVec
        (Provenance.mapNodeOrigins left-occurrence left-origins)
        (Provenance.mapNodeOrigins right-occurrence right-origins)
combinedNodeOrigins-normalize count-correct
  left-occurrence right-occurrence left-origins right-origins =
  substSubst⁻ (Vec Provenance.NodeOrigin) count-correct
    (appendVec
      (Provenance.mapNodeOrigins left-occurrence left-origins)
      (Provenance.mapNodeOrigins right-occurrence right-origins))

serialFlatLeaf : ∀ {Input Middle Output}
  -> ℕ -> String -> Provenance.SourceOrigin
  -> Netlist.OccurrenceId -> Netlist.OccurrenceId
  -> FlatLeaf Input Middle -> FlatLeaf Middle Output
  -> FlatLeaf Input Output
serialFlatLeaf stable-id name origin
  left-occurrence right-occurrence left right =
  flatLeaf stable-id name origin
    (leafStateCount left + leafStateCount right)
    (Compose.serialLocalCount
      (leafNetlist left) (leafNetlist right))
    (Compose.serialNetlist (leafNetlist left) (leafNetlist right))
    (combinedNodeOrigins
      (Compose.serialLocalCount-correct
        (leafNetlist left) (leafNetlist right))
      left-occurrence right-occurrence
      (leafNodeOrigins left) (leafNodeOrigins right))

parallelFlatLeaf :
  ∀ {LeftInput RightInput LeftOutput RightOutput}
  -> ℕ -> String -> Provenance.SourceOrigin
  -> Netlist.OccurrenceId -> Netlist.OccurrenceId
  -> FlatLeaf LeftInput LeftOutput
  -> FlatLeaf RightInput RightOutput
  -> FlatLeaf
      (LeftInput ∥ᵢ RightInput)
      (LeftOutput ∥ᵢ RightOutput)
parallelFlatLeaf stable-id name origin
  left-occurrence right-occurrence left right =
  flatLeaf stable-id name origin
    (leafStateCount left + leafStateCount right)
    (Compose.parallelLocalCount
      (leafNetlist left) (leafNetlist right))
    (Compose.parallelNetlist (leafNetlist left) (leafNetlist right))
    (combinedNodeOrigins
      (Compose.parallelLocalCount-correct
        (leafNetlist left) (leafNetlist right))
      left-occurrence right-occurrence
      (leafNodeOrigins left) (leafNodeOrigins right))

serialFlatLeaf-local-count : ∀ {Input Middle Output}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf Input Middle) (right : FlatLeaf Middle Output)
  -> leafLocalCount
      (serialFlatLeaf stable-id name origin
        left-occurrence right-occurrence left right)
    ≡ leafLocalCount left + leafLocalCount right
serialFlatLeaf-local-count stable-id name origin
  left-occurrence right-occurrence left right =
  Compose.serialLocalCount-correct
    (leafNetlist left) (leafNetlist right)

parallelFlatLeaf-local-count :
  ∀ {LeftInput RightInput LeftOutput RightOutput}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf LeftInput LeftOutput)
  (right : FlatLeaf RightInput RightOutput)
  -> leafLocalCount
      (parallelFlatLeaf stable-id name origin
        left-occurrence right-occurrence left right)
    ≡ leafLocalCount left + leafLocalCount right
parallelFlatLeaf-local-count stable-id name origin
  left-occurrence right-occurrence left right =
  Compose.parallelLocalCount-correct
    (leafNetlist left) (leafNetlist right)

serialLeaf-observation : ∀ {Input Middle Output}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf Input Middle) (right : FlatLeaf Middle Output)
  (input : Environment Input)
  (left-state : Vec Bit (leafStateCount left))
  (right-state : Vec Bit (leafStateCount right))
  -> Component.componentObserve
      (Component.serial stable-id name
        (leafComponent left) (leafComponent right))
      input (left-state , right-state)
    ≡ Component.componentObserve
        (leafComponent
          (serialFlatLeaf stable-id name origin
            left-occurrence right-occurrence left right))
        input (appendVec left-state right-state)
serialLeaf-observation stable-id name origin
  left-occurrence right-occurrence left right
  input left-state right-state =
  environment-from-flat
    (leaf-observation-flat right middle right-state
    ∙ cong
        (λ middle-flat ->
          Stable.stableDirectOutputs (leafNetlist right)
            middle-flat right-state)
        (leaf-observation-flat left input left-state)
    ∙ sym
        (Compose.serialOutputs-evaluation
          (leafNetlist left) (leafNetlist right)
          (flattenEnvironment input) left-state right-state)
    ∙ sym
        (leaf-observation-flat composed input
          (appendVec left-state right-state)))
  where
  middle = Component.componentObserve (leafComponent left) input left-state
  composed = serialFlatLeaf stable-id name origin
    left-occurrence right-occurrence left right

serialLeaf-transition : ∀ {Input Middle Output}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf Input Middle) (right : FlatLeaf Middle Output)
  (event : Flat.Event) (input : Environment Input)
  (left-state : Vec Bit (leafStateCount left))
  (right-state : Vec Bit (leafStateCount right))
  -> Component.componentStep
      (leafComponent
        (serialFlatLeaf stable-id name origin
          left-occurrence right-occurrence left right))
      event input (appendVec left-state right-state)
    ≡ appendVec
        (Component.componentStep (leafComponent left)
          event input left-state)
        (Component.componentStep (leafComponent right)
          event
          (Component.componentObserve (leafComponent left)
            input left-state)
          right-state)
serialLeaf-transition stable-id name origin
  left-occurrence right-occurrence left right
  Flat.idle input left-state right-state = refl
serialLeaf-transition stable-id name origin
  left-occurrence right-occurrence left right
  Flat.risingEdge input left-state right-state =
  leaf-rising-transition-flat composed input
    (appendVec left-state right-state)
  ∙ Compose.serialNext-evaluation
      (leafNetlist left) (leafNetlist right)
      (flattenEnvironment input) left-state right-state
  ∙ cong₂ appendVec
      (sym (leaf-rising-transition-flat left input left-state))
      (cong
        (λ middle-flat ->
          Stable.stableDirectNext (leafNetlist right)
            middle-flat right-state)
        (sym (leaf-observation-flat left input left-state))
      ∙ sym
          (leaf-rising-transition-flat right middle right-state))
  where
  middle = Component.componentObserve (leafComponent left) input left-state
  composed = serialFlatLeaf stable-id name origin
    left-occurrence right-occurrence left right

parallelLeaf-observation :
  ∀ {LeftInput RightInput LeftOutput RightOutput}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf LeftInput LeftOutput)
  (right : FlatLeaf RightInput RightOutput)
  (left-input : Environment LeftInput)
  (right-input : Environment RightInput)
  (left-state : Vec Bit (leafStateCount left))
  (right-state : Vec Bit (leafStateCount right))
  -> Component.componentObserve
      (Component.parallel stable-id name
        (leafComponent left) (leafComponent right))
      (left-input , right-input) (left-state , right-state)
    ≡ Component.componentObserve
        (leafComponent
          (parallelFlatLeaf stable-id name origin
            left-occurrence right-occurrence left right))
        (left-input , right-input)
        (appendVec left-state right-state)
parallelLeaf-observation stable-id name origin
  left-occurrence right-occurrence left right
  left-input right-input left-state right-state =
  environment-from-flat
    (cong₂ appendVec
      (leaf-observation-flat left left-input left-state)
      (leaf-observation-flat right right-input right-state)
    ∙ sym
        (Compose.parallelOutputs-evaluation
          (leafNetlist left) (leafNetlist right)
          (flattenEnvironment left-input) (flattenEnvironment right-input)
          left-state right-state)
    ∙ sym
        (leaf-observation-flat composed
          (left-input , right-input)
          (appendVec left-state right-state)))
  where
  composed = parallelFlatLeaf stable-id name origin
    left-occurrence right-occurrence left right

parallelLeaf-transition :
  ∀ {LeftInput RightInput LeftOutput RightOutput}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf LeftInput LeftOutput)
  (right : FlatLeaf RightInput RightOutput)
  (event : Flat.Event)
  (left-input : Environment LeftInput)
  (right-input : Environment RightInput)
  (left-state : Vec Bit (leafStateCount left))
  (right-state : Vec Bit (leafStateCount right))
  -> Component.componentStep
      (leafComponent
        (parallelFlatLeaf stable-id name origin
          left-occurrence right-occurrence left right))
      event (left-input , right-input)
      (appendVec left-state right-state)
    ≡ appendVec
        (Component.componentStep (leafComponent left)
          event left-input left-state)
        (Component.componentStep (leafComponent right)
          event right-input right-state)
parallelLeaf-transition stable-id name origin
  left-occurrence right-occurrence left right
  Flat.idle left-input right-input left-state right-state = refl
parallelLeaf-transition stable-id name origin
  left-occurrence right-occurrence left right
  Flat.risingEdge left-input right-input left-state right-state =
  leaf-rising-transition-flat composed
    (left-input , right-input) (appendVec left-state right-state)
  ∙ Compose.parallelNext-evaluation
      (leafNetlist left) (leafNetlist right)
      (flattenEnvironment left-input) (flattenEnvironment right-input)
      left-state right-state
  ∙ cong₂ appendVec
      (sym (leaf-rising-transition-flat left left-input left-state))
      (sym (leaf-rising-transition-flat right right-input right-state))
  where
  composed = parallelFlatLeaf stable-id name origin
    left-occurrence right-occurrence left right

serialLeafFlattens : ∀ {Input Middle Output}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf Input Middle) (right : FlatLeaf Middle Output)
  -> CertifiedFlattening
      (Component.serial stable-id name
        (leafComponent left) (leafComponent right))
flattenedLeaf
  (serialLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right) =
  serialFlatLeaf stable-id name origin
    left-occurrence right-occurrence left right
StateRelation
  (serialLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right)
  (left-state , right-state) flat-state =
  flat-state ≡ appendVec left-state right-state
initialRelated
  (serialLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right) = refl
observationPreserved
  (serialLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right)
  input (left-state , right-state) flat-state related =
  serialLeaf-observation stable-id name origin
    left-occurrence right-occurrence left right
    input left-state right-state
  ∙ cong
      (Component.componentObserve
        (leafComponent
          (serialFlatLeaf stable-id name origin
            left-occurrence right-occurrence left right))
        input)
      (sym related)
transitionPreserved
  (serialLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right)
  event input (left-state , right-state) flat-state related =
  cong
    (Component.componentStep
      (leafComponent
        (serialFlatLeaf stable-id name origin
          left-occurrence right-occurrence left right))
      event input)
    related
  ∙ serialLeaf-transition stable-id name origin
      left-occurrence right-occurrence left right
      event input left-state right-state

parallelLeafFlattens :
  ∀ {LeftInput RightInput LeftOutput RightOutput}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  (left : FlatLeaf LeftInput LeftOutput)
  (right : FlatLeaf RightInput RightOutput)
  -> CertifiedFlattening
      (Component.parallel stable-id name
        (leafComponent left) (leafComponent right))
flattenedLeaf
  (parallelLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right) =
  parallelFlatLeaf stable-id name origin
    left-occurrence right-occurrence left right
StateRelation
  (parallelLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right)
  (left-state , right-state) flat-state =
  flat-state ≡ appendVec left-state right-state
initialRelated
  (parallelLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right) = refl
observationPreserved
  (parallelLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right)
  (left-input , right-input)
  (left-state , right-state) flat-state related =
  parallelLeaf-observation stable-id name origin
    left-occurrence right-occurrence left right
    left-input right-input left-state right-state
  ∙ cong
      (Component.componentObserve
        (leafComponent
          (parallelFlatLeaf stable-id name origin
            left-occurrence right-occurrence left right))
        (left-input , right-input))
      (sym related)
transitionPreserved
  (parallelLeafFlattens stable-id name origin
    left-occurrence right-occurrence left right)
  event (left-input , right-input)
  (left-state , right-state) flat-state related =
  cong
    (Component.componentStep
      (leafComponent
        (parallelFlatLeaf stable-id name origin
          left-occurrence right-occurrence left right))
      event (left-input , right-input))
    related
  ∙ parallelLeaf-transition stable-id name origin
      left-occurrence right-occurrence left right
      event left-input right-input left-state right-state

SerialCertificateRelation :
  ∀ {Input Middle Output LeftState RightState}
  {left-hierarchy : Component.Component
    Input Middle Flat.Event LeftState}
  {right-hierarchy : Component.Component
    Middle Output Flat.Event RightState}
  (left-certificate : CertifiedFlattening left-hierarchy)
  (right-certificate : CertifiedFlattening right-hierarchy)
  -> (LeftState × RightState)
  -> Vec Bit
      (leafStateCount (flattenedLeaf left-certificate)
      + leafStateCount (flattenedLeaf right-certificate))
  -> Type₀
SerialCertificateRelation left-certificate right-certificate
  (left-state , right-state) flat-state =
  Σ[ left-flat ∈ Vec Bit
      (leafStateCount (flattenedLeaf left-certificate)) ]
  Σ[ right-flat ∈ Vec Bit
      (leafStateCount (flattenedLeaf right-certificate)) ]
    ((StateRelation left-certificate left-state left-flat
    × StateRelation right-certificate right-state right-flat)
    × (flat-state ≡ appendVec left-flat right-flat))

serialFlattens :
  ∀ {Input Middle Output LeftState RightState}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  {left-hierarchy : Component.Component
    Input Middle Flat.Event LeftState}
  {right-hierarchy : Component.Component
    Middle Output Flat.Event RightState}
  -> CertifiedFlattening left-hierarchy
  -> CertifiedFlattening right-hierarchy
  -> CertifiedFlattening
      (Component.serial stable-id name left-hierarchy right-hierarchy)
flattenedLeaf
  (serialFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate) =
  serialFlatLeaf stable-id name origin
    left-occurrence right-occurrence
    (flattenedLeaf left-certificate)
    (flattenedLeaf right-certificate)
StateRelation
  (serialFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate) =
  SerialCertificateRelation left-certificate right-certificate
initialRelated
  (serialFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate) =
  (Component.componentInitial
      (leafComponent (flattenedLeaf left-certificate)))
  , ((Component.componentInitial
        (leafComponent (flattenedLeaf right-certificate)))
    , (((initialRelated left-certificate)
      , (initialRelated right-certificate))
      , refl))
observationPreserved
  (serialFlattens stable-id name origin
    left-occurrence right-occurrence
    {left-hierarchy = left-hierarchy}
    {right-hierarchy = right-hierarchy}
    left-certificate right-certificate)
  input (left-state , right-state) flat-state
  (left-flat , (right-flat
    , ((left-related , right-related) , flat-combined))) =
  observationPreserved right-certificate
    hierarchy-middle right-state right-flat right-related
  ∙ cong
      (λ middle ->
        Component.componentObserve flat-right middle right-flat)
      middle-agreement
  ∙ serialLeaf-observation stable-id name origin
      left-occurrence right-occurrence
      (flattenedLeaf left-certificate)
      (flattenedLeaf right-certificate)
      input left-flat right-flat
  ∙ cong
      (Component.componentObserve composed-flat input)
      (sym flat-combined)
  where
  flat-left = leafComponent (flattenedLeaf left-certificate)
  flat-right = leafComponent (flattenedLeaf right-certificate)
  composed-flat =
    leafComponent
      (serialFlatLeaf stable-id name origin
        left-occurrence right-occurrence
        (flattenedLeaf left-certificate)
        (flattenedLeaf right-certificate))
  hierarchy-middle =
    Component.componentObserve left-hierarchy input left-state
  middle-agreement =
    observationPreserved left-certificate
      input left-state left-flat left-related
transitionPreserved
  (serialFlattens stable-id name origin
    left-occurrence right-occurrence
    {left-hierarchy = left-hierarchy}
    {right-hierarchy = right-hierarchy}
    left-certificate right-certificate)
  event input (left-state , right-state) flat-state
  (left-flat , (right-flat
    , ((left-related , right-related) , flat-combined))) =
  left-next-flat
  , (right-next-flat
    , ((left-next-related , right-next-related)
      , (cong
          (Component.componentStep composed-flat event input)
          flat-combined
        ∙ serialLeaf-transition stable-id name origin
            left-occurrence right-occurrence
            (flattenedLeaf left-certificate)
            (flattenedLeaf right-certificate)
            event input left-flat right-flat)))
  where
  flat-left = leafComponent (flattenedLeaf left-certificate)
  flat-right = leafComponent (flattenedLeaf right-certificate)
  composed-flat =
    leafComponent
      (serialFlatLeaf stable-id name origin
        left-occurrence right-occurrence
        (flattenedLeaf left-certificate)
        (flattenedLeaf right-certificate))
  hierarchy-middle =
    Component.componentObserve left-hierarchy input left-state
  flat-middle = Component.componentObserve flat-left input left-flat
  middle-agreement =
    observationPreserved left-certificate
      input left-state left-flat left-related
  left-next-flat =
    Component.componentStep flat-left event input left-flat
  right-next-flat =
    Component.componentStep flat-right event flat-middle right-flat
  left-next-related =
    transitionPreserved left-certificate
      event input left-state left-flat left-related
  right-before-transport =
    transitionPreserved right-certificate
      event hierarchy-middle right-state right-flat right-related
  right-step-input-agreement :
    Component.componentStep flat-right event hierarchy-middle right-flat
    ≡ right-next-flat
  right-step-input-agreement =
    cong
      (λ middle ->
        Component.componentStep flat-right event middle right-flat)
      middle-agreement
  right-next-related =
    subst
      (StateRelation right-certificate
        (Component.componentStep right-hierarchy
          event hierarchy-middle right-state))
      right-step-input-agreement right-before-transport

ParallelCertificateRelation :
  ∀ {LeftInput RightInput LeftOutput RightOutput LeftState RightState}
  {left-hierarchy : Component.Component
    LeftInput LeftOutput Flat.Event LeftState}
  {right-hierarchy : Component.Component
    RightInput RightOutput Flat.Event RightState}
  (left-certificate : CertifiedFlattening left-hierarchy)
  (right-certificate : CertifiedFlattening right-hierarchy)
  -> (LeftState × RightState)
  -> Vec Bit
      (leafStateCount (flattenedLeaf left-certificate)
      + leafStateCount (flattenedLeaf right-certificate))
  -> Type₀
ParallelCertificateRelation left-certificate right-certificate
  (left-state , right-state) flat-state =
  Σ[ left-flat ∈ Vec Bit
      (leafStateCount (flattenedLeaf left-certificate)) ]
  Σ[ right-flat ∈ Vec Bit
      (leafStateCount (flattenedLeaf right-certificate)) ]
    ((StateRelation left-certificate left-state left-flat
    × StateRelation right-certificate right-state right-flat)
    × (flat-state ≡ appendVec left-flat right-flat))

parallelFlattens :
  ∀ {LeftInput RightInput LeftOutput RightOutput LeftState RightState}
  (stable-id : ℕ) (name : String) (origin : Provenance.SourceOrigin)
  (left-occurrence right-occurrence : Netlist.OccurrenceId)
  {left-hierarchy : Component.Component
    LeftInput LeftOutput Flat.Event LeftState}
  {right-hierarchy : Component.Component
    RightInput RightOutput Flat.Event RightState}
  -> CertifiedFlattening left-hierarchy
  -> CertifiedFlattening right-hierarchy
  -> CertifiedFlattening
      (Component.parallel stable-id name left-hierarchy right-hierarchy)
flattenedLeaf
  (parallelFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate) =
  parallelFlatLeaf stable-id name origin
    left-occurrence right-occurrence
    (flattenedLeaf left-certificate)
    (flattenedLeaf right-certificate)
StateRelation
  (parallelFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate) =
  ParallelCertificateRelation left-certificate right-certificate
initialRelated
  (parallelFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate) =
  (Component.componentInitial
      (leafComponent (flattenedLeaf left-certificate)))
  , ((Component.componentInitial
        (leafComponent (flattenedLeaf right-certificate)))
    , (((initialRelated left-certificate)
      , (initialRelated right-certificate))
      , refl))
observationPreserved
  (parallelFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate)
  (left-input , right-input) (left-state , right-state) flat-state
  (left-flat , (right-flat
    , ((left-related , right-related) , flat-combined))) =
  cong₂ _,_
    (observationPreserved left-certificate
      left-input left-state left-flat left-related)
    (observationPreserved right-certificate
      right-input right-state right-flat right-related)
  ∙ parallelLeaf-observation stable-id name origin
      left-occurrence right-occurrence
      (flattenedLeaf left-certificate)
      (flattenedLeaf right-certificate)
      left-input right-input left-flat right-flat
  ∙ cong
      (Component.componentObserve composed-flat
        (left-input , right-input))
      (sym flat-combined)
  where
  composed-flat =
    leafComponent
      (parallelFlatLeaf stable-id name origin
        left-occurrence right-occurrence
        (flattenedLeaf left-certificate)
        (flattenedLeaf right-certificate))
transitionPreserved
  (parallelFlattens stable-id name origin
    left-occurrence right-occurrence left-certificate right-certificate)
  event (left-input , right-input) (left-state , right-state) flat-state
  (left-flat , (right-flat
    , ((left-related , right-related) , flat-combined))) =
  left-next-flat
  , (right-next-flat
    , ((left-next-related , right-next-related)
      , (cong
          (Component.componentStep composed-flat event
            (left-input , right-input))
          flat-combined
        ∙ parallelLeaf-transition stable-id name origin
            left-occurrence right-occurrence
            (flattenedLeaf left-certificate)
            (flattenedLeaf right-certificate)
            event left-input right-input left-flat right-flat)))
  where
  flat-left = leafComponent (flattenedLeaf left-certificate)
  flat-right = leafComponent (flattenedLeaf right-certificate)
  composed-flat =
    leafComponent
      (parallelFlatLeaf stable-id name origin
        left-occurrence right-occurrence
        (flattenedLeaf left-certificate)
        (flattenedLeaf right-certificate))
  left-next-flat =
    Component.componentStep flat-left event left-input left-flat
  right-next-flat =
    Component.componentStep flat-right event right-input right-flat
  left-next-related =
    transitionPreserved left-certificate
      event left-input left-state left-flat left-related
  right-next-related =
    transitionPreserved right-certificate
      event right-input right-state right-flat right-related