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

module Spartan6.Hierarchy.CertifiedFlattening where

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

import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.Flatten as Semantic
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Hierarchy.StableCompose as Compose
import Spartan6.Semantics.Design as Flat
import Spartan6.Semantics.Machine as Machine
import Spartan6.Semantics.Refinement as Refinement

-- Transport node origins together with their hierarchy-accounting evidence.
-- This is the provenance analogue of the append-stable node spine: arithmetic
-- transport is consumed once and cannot separate metadata from its proof.

record AccountedOrigins
  (hierarchy : Provenance.HierarchyProvenance)
  (count : ℕ) : Type₀ where
  constructor accountedOrigins
  field
    originVector : Vec Provenance.NodeOrigin count
    originAccounting :
      Provenance.NodesAccountedFor hierarchy originVector

open AccountedOrigins public

-- `Semantic.CertifiedFlattening` is retained as the compatibility theorem for
-- behavior.  This stronger wrapper is the authoritative hierarchy-flattening
-- certificate: every flat node must also be accounted for by the exact
-- component provenance tree.

record ProvenanceCertifiedFlattening
  {Input Output : Interface} {State : Type₀}
  (hierarchy : Component.Component Input Output Flat.Event State)
  : Type₁ where
  constructor provenanceCertifiedFlattening
  field
    semanticCertificate : Semantic.CertifiedFlattening hierarchy
    provenancePreserved :
      Provenance.NodesAccountedFor
        (Component.componentProvenance hierarchy)
        (Semantic.leafNodeOrigins
          (Semantic.flattenedLeaf semanticCertificate))

open ProvenanceCertifiedFlattening public

certifiedLeaf :
  ∀ {Input Output State}
  {hierarchy : Component.Component Input Output Flat.Event State}
  -> ProvenanceCertifiedFlattening hierarchy
  -> Semantic.FlatLeaf Input Output
certifiedLeaf certificate =
  Semantic.flattenedLeaf (semanticCertificate certificate)

certificateImplements :
  ∀ {Input Output State}
  {hierarchy : Component.Component Input Output Flat.Event State}
  -> (certificate : ProvenanceCertifiedFlattening hierarchy)
  -> Refinement.Implements
      (Component.componentMachine hierarchy)
      (Machine.machineSystem
        (Component.componentMachine
          (Semantic.leafComponent (certifiedLeaf certificate))))
certificateImplements certificate =
  Semantic.certificateImplements (semanticCertificate certificate)

leafFlattens : ∀ {Input Output}
  (leaf : Semantic.FlatLeaf Input Output)
  -> Provenance.NodesAccountedFor
      (Provenance.leafProvenance (Semantic.leafOrigin leaf))
      (Semantic.leafNodeOrigins leaf)
  -> ProvenanceCertifiedFlattening (Semantic.leafComponent leaf)
semanticCertificate (leafFlattens leaf accounted) =
  Semantic.leafFlattens leaf
provenancePreserved (leafFlattens leaf accounted) = accounted

instantiateFlattens :
  ∀ {Input Output State}
  (identity : Provenance.InstanceIdentity)
  {hierarchy : Component.Component
    Input Output Flat.Event State}
  -> ProvenanceCertifiedFlattening hierarchy
  -> ProvenanceCertifiedFlattening
      (Component.instantiateWithIdentity identity hierarchy)
semanticCertificate (instantiateFlattens identity certificate) =
  Semantic.instantiateFlattens
    (Provenance.instanceOccurrence identity)
    (Provenance.instanceName identity)
    (semanticCertificate certificate)
provenancePreserved (instantiateFlattens identity certificate) =
  Provenance.mapNodeOrigins-accounted
    (Provenance.instanceOccurrence identity)
    (Provenance.instanceName identity)
    (provenancePreserved certificate)

serialFlattens :
  ∀ {Input Middle Output LeftState RightState}
  (identity : Provenance.ComponentIdentity)
  (summary-origin : Provenance.SourceOrigin)
  (left-identity right-identity : Provenance.InstanceIdentity)
  {left-hierarchy : Component.Component
    Input Middle Flat.Event LeftState}
  {right-hierarchy : Component.Component
    Middle Output Flat.Event RightState}
  -> ProvenanceCertifiedFlattening left-hierarchy
  -> ProvenanceCertifiedFlattening right-hierarchy
  -> ProvenanceCertifiedFlattening
      (Component.serialInstances identity
        left-identity right-identity left-hierarchy right-hierarchy)
semanticCertificate
  (serialFlattens identity summary-origin
    left-identity right-identity
    {left-hierarchy = left-hierarchy}
    {right-hierarchy = right-hierarchy}
    left-certificate right-certificate) =
  Semantic.replaceFlatteningNodeOrigins base-semantic
    (originVector transported-origins)
  where
  left-instantiated = instantiateFlattens left-identity left-certificate
  right-instantiated = instantiateFlattens right-identity right-certificate

  left-leaf = certifiedLeaf left-instantiated
  right-leaf = certifiedLeaf right-instantiated

  base-semantic =
    Semantic.serialFlattens
      (Provenance.identityStableId identity)
      (Provenance.identityName identity)
      summary-origin
      (Provenance.instanceOccurrence left-identity)
      (Provenance.instanceOccurrence right-identity)
      (semanticCertificate left-instantiated)
      (semanticCertificate right-instantiated)

  composite-provenance =
    Component.componentProvenance
      (Component.serialInstances identity
        left-identity right-identity left-hierarchy right-hierarchy)

  appended-origins : AccountedOrigins composite-provenance
    (Semantic.leafLocalCount left-leaf
    + Semantic.leafLocalCount right-leaf)
  appended-origins = accountedOrigins
    (appendVec
      (Semantic.leafNodeOrigins left-leaf)
      (Semantic.leafNodeOrigins right-leaf))
    (Provenance.append-accounted
      (Provenance.serial-left-accounted
        (provenancePreserved left-instantiated))
      (Provenance.serial-right-accounted
        (provenancePreserved right-instantiated)))

  transported-origins : AccountedOrigins composite-provenance
    (Compose.serialLocalCount
      (Semantic.leafNetlist left-leaf)
      (Semantic.leafNetlist right-leaf))
  transported-origins =
    subst⁻ (AccountedOrigins composite-provenance)
      (Compose.serialLocalCount-correct
        (Semantic.leafNetlist left-leaf)
        (Semantic.leafNetlist right-leaf))
      appended-origins
provenancePreserved
  (serialFlattens identity summary-origin
    left-identity right-identity
    {left-hierarchy = left-hierarchy}
    {right-hierarchy = right-hierarchy}
    left-certificate right-certificate) =
  originAccounting transported-origins
  where
  left-instantiated = instantiateFlattens left-identity left-certificate
  right-instantiated = instantiateFlattens right-identity right-certificate
  left-leaf = certifiedLeaf left-instantiated
  right-leaf = certifiedLeaf right-instantiated
  composite-provenance =
    Component.componentProvenance
      (Component.serialInstances identity
        left-identity right-identity left-hierarchy right-hierarchy)
  appended-origins : AccountedOrigins composite-provenance
    (Semantic.leafLocalCount left-leaf
    + Semantic.leafLocalCount right-leaf)
  appended-origins = accountedOrigins
    (appendVec
      (Semantic.leafNodeOrigins left-leaf)
      (Semantic.leafNodeOrigins right-leaf))
    (Provenance.append-accounted
      (Provenance.serial-left-accounted
        (provenancePreserved left-instantiated))
      (Provenance.serial-right-accounted
        (provenancePreserved right-instantiated)))
  transported-origins : AccountedOrigins composite-provenance
    (Compose.serialLocalCount
      (Semantic.leafNetlist left-leaf)
      (Semantic.leafNetlist right-leaf))
  transported-origins =
    subst⁻ (AccountedOrigins composite-provenance)
      (Compose.serialLocalCount-correct
        (Semantic.leafNetlist left-leaf)
        (Semantic.leafNetlist right-leaf))
      appended-origins

parallelFlattens :
  ∀ {LeftInput RightInput LeftOutput RightOutput LeftState RightState}
  (identity : Provenance.ComponentIdentity)
  (summary-origin : Provenance.SourceOrigin)
  (left-identity right-identity : Provenance.InstanceIdentity)
  {left-hierarchy : Component.Component
    LeftInput LeftOutput Flat.Event LeftState}
  {right-hierarchy : Component.Component
    RightInput RightOutput Flat.Event RightState}
  -> ProvenanceCertifiedFlattening left-hierarchy
  -> ProvenanceCertifiedFlattening right-hierarchy
  -> ProvenanceCertifiedFlattening
      (Component.parallelInstances identity
        left-identity right-identity left-hierarchy right-hierarchy)
semanticCertificate
  (parallelFlattens identity summary-origin
    left-identity right-identity
    {left-hierarchy = left-hierarchy}
    {right-hierarchy = right-hierarchy}
    left-certificate right-certificate) =
  Semantic.replaceFlatteningNodeOrigins base-semantic
    (originVector transported-origins)
  where
  left-instantiated = instantiateFlattens left-identity left-certificate
  right-instantiated = instantiateFlattens right-identity right-certificate
  left-leaf = certifiedLeaf left-instantiated
  right-leaf = certifiedLeaf right-instantiated
  base-semantic =
    Semantic.parallelFlattens
      (Provenance.identityStableId identity)
      (Provenance.identityName identity)
      summary-origin
      (Provenance.instanceOccurrence left-identity)
      (Provenance.instanceOccurrence right-identity)
      (semanticCertificate left-instantiated)
      (semanticCertificate right-instantiated)
  composite-provenance =
    Component.componentProvenance
      (Component.parallelInstances identity
        left-identity right-identity left-hierarchy right-hierarchy)
  appended-origins : AccountedOrigins composite-provenance
    (Semantic.leafLocalCount left-leaf
    + Semantic.leafLocalCount right-leaf)
  appended-origins = accountedOrigins
    (appendVec
      (Semantic.leafNodeOrigins left-leaf)
      (Semantic.leafNodeOrigins right-leaf))
    (Provenance.append-accounted
      (Provenance.parallel-left-accounted
        (provenancePreserved left-instantiated))
      (Provenance.parallel-right-accounted
        (provenancePreserved right-instantiated)))
  transported-origins : AccountedOrigins composite-provenance
    (Compose.parallelLocalCount
      (Semantic.leafNetlist left-leaf)
      (Semantic.leafNetlist right-leaf))
  transported-origins =
    subst⁻ (AccountedOrigins composite-provenance)
      (Compose.parallelLocalCount-correct
        (Semantic.leafNetlist left-leaf)
        (Semantic.leafNetlist right-leaf))
      appended-origins
provenancePreserved
  (parallelFlattens identity summary-origin
    left-identity right-identity
    {left-hierarchy = left-hierarchy}
    {right-hierarchy = right-hierarchy}
    left-certificate right-certificate) =
  originAccounting transported-origins
  where
  left-instantiated = instantiateFlattens left-identity left-certificate
  right-instantiated = instantiateFlattens right-identity right-certificate
  left-leaf = certifiedLeaf left-instantiated
  right-leaf = certifiedLeaf right-instantiated
  composite-provenance =
    Component.componentProvenance
      (Component.parallelInstances identity
        left-identity right-identity left-hierarchy right-hierarchy)
  appended-origins : AccountedOrigins composite-provenance
    (Semantic.leafLocalCount left-leaf
    + Semantic.leafLocalCount right-leaf)
  appended-origins = accountedOrigins
    (appendVec
      (Semantic.leafNodeOrigins left-leaf)
      (Semantic.leafNodeOrigins right-leaf))
    (Provenance.append-accounted
      (Provenance.parallel-left-accounted
        (provenancePreserved left-instantiated))
      (Provenance.parallel-right-accounted
        (provenancePreserved right-instantiated)))
  transported-origins : AccountedOrigins composite-provenance
    (Compose.parallelLocalCount
      (Semantic.leafNetlist left-leaf)
      (Semantic.leafNetlist right-leaf))
  transported-origins =
    subst⁻ (AccountedOrigins composite-provenance)
      (Compose.parallelLocalCount-correct
        (Semantic.leafNetlist left-leaf)
        (Semantic.leafNetlist right-leaf))
      appended-origins