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

module Spartan6.Validation.Raw where

open import Spartan6.Prelude
open import Spartan6.Evidence using
  (SupportStatus; fullySupported; conditionallySupported; partiallySupported;
   assumptionSupported; unsupportedFeature; planned)

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Architecture.Profile as Profile
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter

open import Cubical.Data.Nat using (_≡ᵇ_)
open import Agda.Builtin.String using (primShowNat; primStringEquality)

singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton item = item ∷ᴸ []ᴸ

issue : Diagnostic.DiagnosticCode → String → String → String → String
      → Diagnostic.Diagnostic
issue code subject expected observed detail =
  Diagnostic.diagnostic code Diagnostic.reject subject expected observed detail

concatMapDiagnostics : ∀ {A : Type₀}
                     → (A → Diagnostic.Diagnostics)
                     → List A
                     → Diagnostic.Diagnostics
concatMapDiagnostics check []ᴸ = []ᴸ
concatMapDiagnostics check (item ∷ᴸ items) =
  check item ++ᴸ concatMapDiagnostics check items

concatMapList : ∀ {A B : Type₀} → (A → List B) → List A → List B
concatMapList collect []ᴸ = []ᴸ
concatMapList collect (item ∷ᴸ items) =
  collect item ++ᴸ concatMapList collect items

connectionNets : List Raw.Connection → List Raw.NetId
connectionNets []ᴸ = []ᴸ
connectionNets (Raw.net net-id ∷ᴸ connections) =
  net-id ∷ᴸ connectionNets connections
connectionNets (Raw.constant bit ∷ᴸ connections) =
  connectionNets connections
connectionNets (Raw.disconnected ∷ᴸ connections) =
  connectionNets connections

containsNet : Raw.NetId → List Raw.NetId → Bool
containsNet net-id []ᴸ = false
containsNet net-id (candidate ∷ᴸ candidates) =
  (net-id ≡ᵇ candidate) or containsNet net-id candidates

primitivePortDrivers : Raw.RawPort → List Raw.NetId
primitivePortDrivers port with Raw.rawPortDirection port
... | Raw.outputPort = connectionNets (Raw.rawPortConnections port)
... | direction = []ᴸ

primitivePortSinks : Raw.RawPort → List Raw.NetId
primitivePortSinks port with Raw.rawPortDirection port
... | Raw.inputPort = connectionNets (Raw.rawPortConnections port)
... | direction = []ᴸ

instanceDrivers : Raw.RawInstance → List Raw.NetId
instanceDrivers item =
  concatMapList primitivePortDrivers (Raw.rawInstancePorts item)

instanceSinks : Raw.RawInstance → List Raw.NetId
instanceSinks item =
  concatMapList primitivePortSinks (Raw.rawInstancePorts item)

topPortDrivers : Raw.RawTopPort → List Raw.NetId
topPortDrivers port with Raw.rawTopPortDirection port
... | Raw.inputPort = connectionNets (Raw.rawTopPortConnections port)
... | direction = []ᴸ

topPortSinks : Raw.RawTopPort → List Raw.NetId
topPortSinks port with Raw.rawTopPortDirection port
... | Raw.outputPort = connectionNets (Raw.rawTopPortConnections port)
... | direction = []ᴸ

designDrivers : Raw.RawDesign → List Raw.NetId
designDrivers design =
  concatMapList topPortDrivers (Raw.rawTopPorts design)
  ++ᴸ concatMapList instanceDrivers (Raw.rawInstances design)

designSinks : Raw.RawDesign → List Raw.NetId
designSinks design =
  concatMapList topPortSinks (Raw.rawTopPorts design)
  ++ᴸ concatMapList instanceSinks (Raw.rawInstances design)

record Dependency : Type₀ where
  constructor dependency
  field
    dependencySource : Raw.NetId
    dependencyTarget : Raw.NetId

open Dependency

dependenciesTo : Raw.NetId → List Raw.NetId → List Dependency
dependenciesTo source []ᴸ = []ᴸ
dependenciesTo source (target ∷ᴸ targets) =
  dependency source target ∷ᴸ dependenciesTo source targets

allDependencies : List Raw.NetId → List Raw.NetId → List Dependency
allDependencies []ᴸ targets = []ᴸ
allDependencies (source ∷ᴸ sources) targets =
  dependenciesTo source targets ++ᴸ allDependencies sources targets

kindIsCombinational : Architecture.PrimitiveKind → Bool
kindIsCombinational Architecture.LUT1 = true
kindIsCombinational Architecture.LUT2 = true
kindIsCombinational Architecture.LUT3 = true
kindIsCombinational Architecture.LUT4 = true
kindIsCombinational Architecture.LUT5 = true
kindIsCombinational Architecture.LUT6 = true
kindIsCombinational Architecture.MUXF7 = true
kindIsCombinational Architecture.MUXF8 = true
kindIsCombinational Architecture.CARRY4 = true
kindIsCombinational Architecture.FDRE = false
kindIsCombinational Architecture.FDSE = false
kindIsCombinational Architecture.SRL16E = false
kindIsCombinational Architecture.RAM64X1S = false
kindIsCombinational Architecture.IBUF = true
kindIsCombinational Architecture.OBUF = true
kindIsCombinational Architecture.OBUFDS = true
kindIsCombinational Architecture.OBUFT = true
kindIsCombinational Architecture.BUFG = true
kindIsCombinational Architecture.BUFGCE = true

instanceDependencies : Raw.RawInstance → List Dependency
instanceDependencies item with Raw.rawInstanceKind item
... | Raw.unknownPrimitive name = []ᴸ
... | Raw.knownPrimitive kind =
  if kindIsCombinational kind
  then allDependencies (instanceSinks item) (instanceDrivers item)
  else []ᴸ

designDependencies : Raw.RawDesign → List Dependency
designDependencies design =
  concatMapList instanceDependencies (Raw.rawInstances design)

targetsFrom : Raw.NetId → List Dependency → List Raw.NetId
targetsFrom source []ᴸ = []ᴸ
targetsFrom source (edge ∷ᴸ edges) =
  if (source ≡ᵇ dependencySource edge)
  then dependencyTarget edge ∷ᴸ targetsFrom source edges
  else targetsFrom source edges

mutual
  reachable : ℕ → Raw.NetId → Raw.NetId → List Dependency → Bool
  reachable zero target current edges = current ≡ᵇ target
  reachable (suc fuel) target current edges =
    (current ≡ᵇ target)
    or explore fuel target (targetsFrom current edges) edges

  explore : ℕ → Raw.NetId → List Raw.NetId → List Dependency → Bool
  explore fuel target []ᴸ edges = false
  explore fuel target (next ∷ᴸ nexts) edges =
    reachable fuel target next edges or explore fuel target nexts edges

someDependencyCycles : ℕ → List Dependency → List Dependency → Bool
someDependencyCycles fuel all-edges []ᴸ = false
someDependencyCycles fuel all-edges (edge ∷ᴸ edges) =
  reachable fuel
            (dependencySource edge)
            (dependencyTarget edge)
            all-edges
  or someDependencyCycles fuel all-edges edges

combinationalCycle? : Raw.RawDesign → Bool
combinationalCycle? design =
  someDependencyCycles (suc (lengthList edges)) edges edges
  where
  edges : List Dependency
  edges = designDependencies design

cycleDiagnostics : Raw.RawDesign → Diagnostic.Diagnostics
cycleDiagnostics design =
  if combinationalCycle? design
  then singleton
    (issue Diagnostic.combinationalLoop
           "combinational dependency graph"
           "an acyclic graph"
           "a dependency cycle"
           "Dependencies through explicit storage state are excluded; purely combinational cycles are rejected.")
  else []ᴸ

duplicateDriverDiagnostics : List Raw.NetId → Diagnostic.Diagnostics
duplicateDriverDiagnostics []ᴸ = []ᴸ
duplicateDriverDiagnostics (net-id ∷ᴸ net-ids) =
  (if containsNet net-id net-ids
   then singleton
     (issue Diagnostic.multipleDriver
            (primShowNat net-id)
            "exactly one driver"
            "multiple drivers"
            "The initial profile uses ordinary single-driver nets.")
   else []ᴸ)
  ++ᴸ duplicateDriverDiagnostics net-ids

undrivenNetDiagnostics : List Raw.NetId → List Raw.NetId
                       → Diagnostic.Diagnostics
undrivenNetDiagnostics drivers []ᴸ = []ᴸ
undrivenNetDiagnostics drivers (sink ∷ᴸ sinks) =
  (if containsNet sink drivers
   then []ᴸ
   else singleton
     (issue Diagnostic.undrivenInput
            (primShowNat sink)
            "a top-level input or primitive output driver"
            "no driver"
            "Every referenced net in the guaranteed core must have a driver."))
  ++ᴸ undrivenNetDiagnostics drivers sinks

connectivityDiagnostics : Raw.RawDesign → Diagnostic.Diagnostics
connectivityDiagnostics design =
  duplicateDriverDiagnostics drivers
  ++ᴸ undrivenNetDiagnostics drivers (designSinks design)
  ++ᴸ cycleDiagnostics design
  where
  drivers : List Raw.NetId
  drivers = designDrivers design

portShapeDiagnostics : Architecture.PortSpecification
                     → Raw.RawPort → Diagnostic.Diagnostics
portShapeDiagnostics specification port =
  name-diagnostics ++ᴸ declared-width-diagnostics
  ++ᴸ connection-count-diagnostics
  where
  expected-name : String
  expected-name = Architecture.canonicalPortName specification

  expected-width : ℕ
  expected-width = Architecture.canonicalPortWidth specification

  name-diagnostics : Diagnostic.Diagnostics
  name-diagnostics =
    if primStringEquality (Raw.rawPortName port) expected-name
    then []ᴸ
    else singleton
      (issue Diagnostic.unknownPort
             (Raw.rawPortName port)
             expected-name
             (Raw.rawPortName port)
             "Primitive port names and order must both match the canonical architecture schema; equal widths do not make ports interchangeable.")

  declared-width-diagnostics : Diagnostic.Diagnostics
  declared-width-diagnostics =
    if (Raw.rawPortWidth port ≡ᵇ expected-width)
    then []ᴸ
    else singleton
      (issue Diagnostic.widthMismatch
             (Raw.rawPortName port)
             "the architecture-declared port width"
             "a different raw declared width"
             "Port widths are checked against the primitive's canonical schema.")

  connection-count-diagnostics : Diagnostic.Diagnostics
  connection-count-diagnostics =
    if (lengthList (Raw.rawPortConnections port) ≡ᵇ expected-width)
    then []ᴸ
    else singleton
      (issue Diagnostic.widthMismatch
             (Raw.rawPortName port)
             "connection count equal to the architecture port width"
             "connection count differs from the architecture width"
             "Every bit of a primitive port must have an explicit raw binding.")

hasDisconnected : List Raw.Connection → Bool
hasDisconnected []ᴸ = false
hasDisconnected (Raw.disconnected ∷ᴸ connections) = true
hasDisconnected (connection ∷ᴸ connections) = hasDisconnected connections

hasConstant : List Raw.Connection → Bool
hasConstant []ᴸ = false
hasConstant (Raw.constant bit ∷ᴸ connections) = true
hasConstant (connection ∷ᴸ connections) = hasConstant connections

inputBindingDiagnostics : Raw.RawPort → Diagnostic.Diagnostics
inputBindingDiagnostics port =
  if hasDisconnected (Raw.rawPortConnections port)
  then singleton
    (issue Diagnostic.undrivenInput
           (Raw.rawPortName port)
           "a net or two-valued constant for every bit"
           "at least one disconnected bit"
           "Required semantic inputs may not be silently unconstrained.")
  else []ᴸ

outputBindingDiagnostics : Raw.RawPort → Diagnostic.Diagnostics
outputBindingDiagnostics port =
  if hasConstant (Raw.rawPortConnections port)
  then singleton
    (issue Diagnostic.directionMismatch
           (Raw.rawPortName port)
           "driven nets or explicit disconnections"
           "a constant used as an output binding"
           "A primitive output drives connectivity; it is not driven by a constant.")
  else []ᴸ

inputPortDiagnostics : Architecture.PortSpecification
                     → Raw.RawPort → Diagnostic.Diagnostics
inputPortDiagnostics specification port with Raw.rawPortDirection port
... | Raw.inputPort =
  portShapeDiagnostics specification port ++ᴸ inputBindingDiagnostics port
... | direction =
  portShapeDiagnostics specification port ++ᴸ singleton
    (issue Diagnostic.directionMismatch
           (Raw.rawPortName port)
           "input direction"
           "non-input direction"
           "Raw primitive ports are ordered according to the architecture schema.")

outputPortDiagnostics : Architecture.PortSpecification
                      → Raw.RawPort → Diagnostic.Diagnostics
outputPortDiagnostics specification port with Raw.rawPortDirection port
... | Raw.outputPort =
  portShapeDiagnostics specification port ++ᴸ outputBindingDiagnostics port
... | direction =
  portShapeDiagnostics specification port ++ᴸ singleton
    (issue Diagnostic.directionMismatch
           (Raw.rawPortName port)
           "output direction"
           "non-output direction"
           "Raw primitive ports are ordered according to the architecture schema.")

orderedPortDiagnostics : List Architecture.PortSpecification
                       → List Architecture.PortSpecification
                       → List Raw.RawPort
                       → Diagnostic.Diagnostics
orderedPortDiagnostics []ᴸ []ᴸ []ᴸ = []ᴸ
orderedPortDiagnostics []ᴸ []ᴸ (port ∷ᴸ ports) =
  singleton
    (issue Diagnostic.unknownPort
           (Raw.rawPortName port)
           "no additional primitive ports"
           "additional port"
           "Unknown ports are never silently ignored.")
  ++ᴸ orderedPortDiagnostics []ᴸ []ᴸ ports
orderedPortDiagnostics (specification ∷ᴸ inputs) outputs []ᴸ =
  singleton
    (issue Diagnostic.missingPort
           "primitive instance"
           "all ordered input and output ports"
           "port list ended early"
           "At least one required input port is missing.")
orderedPortDiagnostics []ᴸ (specification ∷ᴸ outputs) []ᴸ =
  singleton
    (issue Diagnostic.missingPort
           "primitive instance"
           "all ordered output ports"
           "port list ended early"
           "At least one required output port is missing.")
orderedPortDiagnostics (specification ∷ᴸ inputs) outputs (port ∷ᴸ ports) =
  inputPortDiagnostics specification port
  ++ᴸ orderedPortDiagnostics inputs outputs ports
orderedPortDiagnostics []ᴸ (specification ∷ᴸ outputs) (port ∷ᴸ ports) =
  outputPortDiagnostics specification port
  ++ᴸ orderedPortDiagnostics []ᴸ outputs ports

instanceStructuralDiagnostics : Raw.RawInstance → Diagnostic.Diagnostics
instanceStructuralDiagnostics item with Raw.rawInstanceKind item
... | Raw.unknownPrimitive name =
  singleton
    (issue Diagnostic.unknownPrimitive
           (Raw.rawInstanceName item)
           "a primitive kind in the selected architecture profile"
           name
           "Unknown kinds are rejected rather than approximated.")
... | Raw.knownPrimitive kind =
  orderedPortDiagnostics
    (Architecture.inputPortSpecifications kind)
    (Architecture.outputPortSpecifications kind)
    (Raw.rawInstancePorts item)

topPortDiagnostics : Raw.RawTopPort → Diagnostic.Diagnostics
topPortDiagnostics port = direction-diagnostics ++ᴸ width-diagnostics
  where
  direction-diagnostics : Diagnostic.Diagnostics
  direction-diagnostics with Raw.rawTopPortDirection port
  ... | Raw.inputPort = []ᴸ
  ... | Raw.outputPort = []ᴸ
  ... | Raw.bidirectionalPort =
    singleton
      (issue Diagnostic.unsupportedMode
             (Raw.rawTopPortName port)
             "input or output direction"
             "bidirectional direction"
             "Resolved bidirectional I/O is outside the initial two-valued profile.")

  width-diagnostics : Diagnostic.Diagnostics
  width-diagnostics =
    if (Raw.rawTopPortWidth port
        ≡ᵇ lengthList (Raw.rawTopPortConnections port))
    then []ᴸ
    else singleton
      (issue Diagnostic.widthMismatch
             (Raw.rawTopPortName port)
             "declared width equal to connection count"
             "declared width and connection count differ"
             "Top-level bit indexing is preserved by the raw boundary.")

structureDiagnostics : Raw.RawDesign → Diagnostic.Diagnostics
structureDiagnostics design =
  concatMapDiagnostics topPortDiagnostics (Raw.rawTopPorts design)
  ++ᴸ concatMapDiagnostics
         instanceStructuralDiagnostics
         (Raw.rawInstances design)
  ++ᴸ connectivityDiagnostics design

supportStatusDiagnostics : String → SupportStatus → Diagnostic.Diagnostics
supportStatusDiagnostics subject fullySupported = []ᴸ
supportStatusDiagnostics subject conditionallySupported =
  singleton
    (issue Diagnostic.unsupportedMode subject "fully supported mode"
           "conditionally supported mode"
           "The raw artefact does not yet carry the required precondition evidence.")
supportStatusDiagnostics subject partiallySupported =
  singleton
    (issue Diagnostic.unsupportedMode subject "fully supported mode"
           "partially supported mode"
           "Semantic code exists, but raw decoding/admission obligations remain incomplete.")
supportStatusDiagnostics subject assumptionSupported =
  singleton
    (issue Diagnostic.unresolvedBlackBox subject "assumption-free mode"
           "assumption-supported mode"
           "The guaranteed core does not silently admit assumptions.")
supportStatusDiagnostics subject unsupportedFeature =
  singleton
    (issue Diagnostic.unsupportedMode subject "supported primitive mode"
           "unsupported feature"
           "No executable guaranteed-core semantics is assigned.")
supportStatusDiagnostics subject planned =
  singleton
    (issue Diagnostic.unsupportedMode subject "supported primitive mode"
           "planned feature"
           "The feature remains outside the admitted profile.")

instanceProfileDiagnosticsFor : Profile.ArchitectureProfile
                              → Raw.RawInstance → Diagnostic.Diagnostics
instanceProfileDiagnosticsFor profile item with Raw.rawInstanceKind item
... | Raw.unknownPrimitive name = []ᴸ
... | Raw.knownPrimitive kind =
  supportStatusDiagnostics
    (Raw.rawInstanceName item)
    (Profile.primitiveSupport profile kind)
  ++ᴸ parameter-diagnostics
  where
  parameter-diagnostics : Diagnostic.Diagnostics
  parameter-diagnostics with
    Parameter.normaliseCoreParameters
      kind
      (Raw.rawInstanceName item)
      (Raw.rawInstanceParameters item)
      (Raw.rawInstanceInitialBit item)
  ... | Diagnostic.accepted configuration = []ᴸ
  ... | Diagnostic.rejected diagnostics = diagnostics

targetDiagnosticsFor : Profile.ArchitectureProfile
                     → Raw.RawDesign → Diagnostic.Diagnostics
targetDiagnosticsFor profile design with Raw.rawTargetProfile design
... | nothing = []ᴸ
... | just claimed =
  if primStringEquality claimed (Profile.profileName profile)
  then []ᴸ
  else singleton
    (issue Diagnostic.contradictoryTarget
           "raw target profile"
           (Profile.profileName profile)
           claimed
           "An explicit raw target must match the selected validation profile; an absent architecture-only target remains permitted.")

profileDiagnosticsFor : Profile.ArchitectureProfile
                      → Raw.RawDesign → Diagnostic.Diagnostics
profileDiagnosticsFor profile design =
  structureDiagnostics design
  ++ᴸ targetDiagnosticsFor profile design
  ++ᴸ concatMapDiagnostics
         (instanceProfileDiagnosticsFor profile)
         (Raw.rawInstances design)

profileDiagnostics : Raw.RawDesign → Diagnostic.Diagnostics
profileDiagnostics design =
  profileDiagnosticsFor Profile.developmentProfile design

StructurallyValid : Raw.RawDesign → Type₀
StructurallyValid design = structureDiagnostics design ≡ []ᴸ

ProfileValid : Raw.RawDesign → Type₀
ProfileValid design = profileDiagnostics design ≡ []ᴸ

ProfileValidFor : Profile.ArchitectureProfile → Raw.RawDesign → Type₀
ProfileValidFor profile design = profileDiagnosticsFor profile design ≡ []ᴸ

StructurallyChecked : Type₀
StructurallyChecked = Σ Raw.RawDesign StructurallyValid

AdmittedRawDesign : Type₀
AdmittedRawDesign = Σ Raw.RawDesign ProfileValid

AdmittedFor : Profile.ArchitectureProfile → Type₀
AdmittedFor profile = Σ Raw.RawDesign (ProfileValidFor profile)

structureResult : (design : Raw.RawDesign)
                → (diagnostics : Diagnostic.Diagnostics)
                → structureDiagnostics design ≡ diagnostics
                → Diagnostic.CheckResult StructurallyChecked
structureResult design []ᴸ diagnostics-path =
  Diagnostic.accepted (design , diagnostics-path)
structureResult design (problem ∷ᴸ problems) diagnostics-path =
  Diagnostic.rejected (problem ∷ᴸ problems)

validateStructure : Raw.RawDesign → Diagnostic.CheckResult StructurallyChecked
validateStructure design =
  structureResult design (structureDiagnostics design) refl

profileResult : (design : Raw.RawDesign)
              → (diagnostics : Diagnostic.Diagnostics)
              → profileDiagnostics design ≡ diagnostics
              → Diagnostic.CheckResult AdmittedRawDesign
profileResult design []ᴸ diagnostics-path =
  Diagnostic.accepted (design , diagnostics-path)
profileResult design (problem ∷ᴸ problems) diagnostics-path =
  Diagnostic.rejected (problem ∷ᴸ problems)

validateForProfile : Raw.RawDesign → Diagnostic.CheckResult AdmittedRawDesign
validateForProfile design =
  profileResult design (profileDiagnostics design) refl

profileResultFor : (profile : Profile.ArchitectureProfile)
                 → (design : Raw.RawDesign)
                 → (diagnostics : Diagnostic.Diagnostics)
                 → profileDiagnosticsFor profile design ≡ diagnostics
                 → Diagnostic.CheckResult (AdmittedFor profile)
profileResultFor profile design []ᴸ diagnostics-path =
  Diagnostic.accepted (design , diagnostics-path)
profileResultFor profile design (problem ∷ᴸ problems) diagnostics-path =
  Diagnostic.rejected (problem ∷ᴸ problems)

validateWithProfile : (profile : Profile.ArchitectureProfile)
                    → Raw.RawDesign
                    → Diagnostic.CheckResult (AdmittedFor profile)
validateWithProfile profile design =
  profileResultFor profile design (profileDiagnosticsFor profile design) refl