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

module Spartan6.Validation.Profile where

open import Spartan6.Prelude
open import Spartan6.Evidence

import Spartan6.Architecture.ModeCapability as Capability
import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Architecture.ProfileDeclaration as Profile
import Spartan6.Import.Artifact as Artifact
import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.DecodedDesign as Decoded
import Spartan6.Validation.Design as Validated
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Mode
import Spartan6.Validation.Raw as LegacyValidation

open import Agda.Builtin.String using (primShowNat; primStringEquality)
open import Cubical.Foundations.Path using (inspect; [_]ᵢ)

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

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

missing-capability : Raw.RawInstance → Diagnostic.Diagnostics
missing-capability source = singleton
  (issue Diagnostic.unsupportedMode
    (Raw.rawInstanceName source)
    "an exact-mode capability with semantic evidence"
    "a rejected or incomplete mode declaration"
    "A support label cannot admit an occurrence without the exact executable or relational evidence and canonical premise.")

missing-premise : Raw.RawInstance → Diagnostic.Diagnostics
missing-premise source = singleton
  (issue Diagnostic.unsupportedMode
    (Raw.rawInstanceName source)
    "one CARRY4 entry source selected while the other is literally low"
    "a missing or false conditional premise"
    "Conditional mode admission retains a source-indexed proof; the profile declaration alone cannot discharge it.")

unaccepted-evidence : Raw.RawInstance → Diagnostic.Diagnostics
unaccepted-evidence source = singleton
  (issue Diagnostic.unresolvedBlackBox
    (Raw.rawInstanceName source)
    "traceability accepted by the profile evidence policy"
    "traceability outside the accepted evidence classes"
    "Semantic code and an evidence claim are checked independently.")

domain-overflow : ℕ → ℕ → Diagnostic.Diagnostics
domain-overflow maximum observed = singleton
  (issue Diagnostic.unsupportedEvent
    "profile clock domains"
    (primShowNat maximum)
    (primShowNat observed)
    "The number of distinct decoded register clock nets exceeds the enforceable profile bound.")

invalid-register-clock : Raw.RawInstance → Diagnostic.Diagnostics
invalid-register-clock source = singleton
  (issue Diagnostic.unsupportedEvent
    (Raw.rawInstanceName source)
    "exactly one raw net on the canonical C port"
    "a constant, disconnected, or malformed clock binding"
    "Every decoded FDRE/FDSE contributes a proved clock net before the profile domain bound is evaluated.")

bidirectional-forbidden : Diagnostic.Diagnostics
bidirectional-forbidden = singleton
  (issue Diagnostic.unsupportedMode
    "top-level interface"
    "no bidirectional top port"
    "a bidirectional top port"
    "The selected profile does not provide a resolution contract for bidirectional behaviour.")

targetLabel : Maybe String → String
targetLabel nothing = "<no target>"
targetLabel (just target) = target

target-mismatch : Maybe String → Maybe String → Diagnostic.Diagnostics
target-mismatch expected observed = singleton
  (issue Diagnostic.contradictoryTarget
    "raw target profile"
    (targetLabel expected)
    (targetLabel observed)
    "A target claim must match the enforceable architecture target exactly; it is not evidence of a concrete device.")

-- The same syntactic restriction used by the checked CARRY4 builder, stated
-- here without bindings because profile validation only has to establish
-- which entry is selected.  Resolution of the selected connection remains a
-- scheduler/builder obligation.

carryEntryConnectionsAllowed? :
  List Raw.Connection → List Raw.Connection → Bool
carryEntryConnectionsAllowed?
  (connection ∷ᴸ []ᴸ)
  (Raw.constant false ∷ᴸ []ᴸ) = true
carryEntryConnectionsAllowed?
  (Raw.constant false ∷ᴸ []ᴸ)
  (connection ∷ᴸ []ᴸ) = true
carryEntryConnectionsAllowed? ci cyinit = false

carryEntryAllowedPorts? : List Raw.RawPort → Bool
carryEntryAllowedPorts?
  (ci ∷ᴸ cyinit ∷ᴸ di ∷ᴸ select
   ∷ᴸ output ∷ᴸ carry-output ∷ᴸ []ᴸ) =
  carryEntryConnectionsAllowed?
    (Raw.rawPortConnections ci)
    (Raw.rawPortConnections cyinit)
carryEntryAllowedPorts? ports = false

carryEntryAllowed? : Raw.RawInstance → Bool
carryEntryAllowed? source =
  carryEntryAllowedPorts? (Raw.rawInstancePorts source)

PremiseEvidence : Raw.RawInstance
  → Capability.ConditionalPremise → Type₀
PremiseEvidence source Capability.noAdditionalPremise = Unit
PremiseEvidence source Capability.nonselectedCarryEntryIsLow =
  carryEntryAllowed? source ≡ true

checkPremise : (source : Raw.RawInstance)
  → (premise : Capability.ConditionalPremise)
  → Diagnostic.CheckResult (PremiseEvidence source premise)
checkPremise source Capability.noAdditionalPremise =
  Diagnostic.accepted tt
checkPremise source Capability.nonselectedCarryEntryIsLow with
  carryEntryAllowed? source | inspect carryEntryAllowed? source
... | false | [ path ]ᵢ = Diagnostic.rejected (missing-premise source)
... | true | [ path ]ᵢ = Diagnostic.accepted refl

officialEvidenceAccepted? : Bool → RuleTraceability → Bool
officialEvidenceAccepted? false trace = true
officialEvidenceAccepted? true trace = traceOfficial? trace

record OccurrenceCapability
  (profile : Profile.EnforceableProfile)
  {identifier : Provenance.OccurrenceId}
  {source : Raw.RawInstance}
  (decoded : Decoded.DecodedOccurrence identifier source) : Type₀ where
  constructor occurrenceCapability
  field
    exactModeCapability :
      Capability.ExactModeCapability (Decoded.decodedMode decoded)
    capability-was-selected :
      Profile.capabilityFor profile
        (Decoded.decodedKind decoded) (Decoded.decodedMode decoded)
      ≡ just exactModeCapability
    conditionalPremiseEvidence :
      PremiseEvidence source
        (Capability.conditionalPremise exactModeCapability)
    profileEvidenceAccepted :
      officialEvidenceAccepted?
        (Profile.requiresOfficialEvidence profile)
        (Capability.traceability exactModeCapability)
      ≡ true

open OccurrenceCapability public

checkOccurrence :
  (profile : Profile.EnforceableProfile)
  → ∀ {identifier source}
  → (decoded : Decoded.DecodedOccurrence identifier source)
  → Diagnostic.CheckResult (OccurrenceCapability profile decoded)
checkOccurrence profile {source = source} decoded with
  Profile.capabilityFor profile
    (Decoded.decodedKind decoded) (Decoded.decodedMode decoded)
  | inspect
      (Profile.capabilityFor profile (Decoded.decodedKind decoded))
      (Decoded.decodedMode decoded)
... | nothing | [ capability-path ]ᵢ =
  Diagnostic.rejected (missing-capability source)
... | just capability | [ capability-path ]ᵢ with
  checkPremise source (Capability.conditionalPremise capability)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted premise-evidence with
  officialEvidenceAccepted?
    (Profile.requiresOfficialEvidence profile)
    (Capability.traceability capability)
  | inspect
      (officialEvidenceAccepted?
        (Profile.requiresOfficialEvidence profile))
      (Capability.traceability capability)
...     | false | [ evidence-path ]ᵢ =
  Diagnostic.rejected (unaccepted-evidence source)
...     | true | [ evidence-path ]ᵢ =
  Diagnostic.accepted
    (occurrenceCapability
      capability capability-path premise-evidence evidence-path)

data ProfiledOccurrences (profile : Profile.EnforceableProfile) :
  ∀ {next sources}
  → Decoded.DecodedOccurrences next sources → Type₀ where
  profiledDone : ∀ {next}
    → ProfiledOccurrences profile (Decoded.decodedDone {next = next})
  profiledNext : ∀ {next source sources}
    {decoded : Decoded.DecodedOccurrence
      (Provenance.occurrenceId next) source}
    {rest : Decoded.DecodedOccurrences (suc next) sources}
    → OccurrenceCapability profile decoded
    → ProfiledOccurrences profile rest
    → ProfiledOccurrences profile (Decoded.decodedNext decoded rest)

checkOccurrences : (profile : Profile.EnforceableProfile)
  → ∀ {next sources}
  → (decoded : Decoded.DecodedOccurrences next sources)
  → Diagnostic.CheckResult (ProfiledOccurrences profile decoded)
checkOccurrences profile Decoded.decodedDone =
  Diagnostic.accepted profiledDone
checkOccurrences profile (Decoded.decodedNext decoded rest) with
  checkOccurrence profile decoded
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted capability with checkOccurrences profile rest
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted capabilities =
  Diagnostic.accepted (profiledNext capability capabilities)

registerClockNetFromPorts : List Raw.RawPort → Maybe Raw.NetId
registerClockNetFromPorts
  (data-input ∷ᴸ clock ∷ᴸ enable ∷ᴸ control
   ∷ᴸ output ∷ᴸ []ᴸ) with Raw.rawPortConnections clock
... | Raw.net net-id ∷ᴸ []ᴸ = just net-id
... | connections = nothing
registerClockNetFromPorts ports = nothing

registerClockNet : Raw.RawInstance → Maybe Raw.NetId
registerClockNet source with Raw.rawInstanceKind source
... | Raw.knownPrimitive Architecture.FDRE =
  registerClockNetFromPorts (Raw.rawInstancePorts source)
... | Raw.knownPrimitive Architecture.FDSE =
  registerClockNetFromPorts (Raw.rawInstancePorts source)
... | Raw.knownPrimitive kind = nothing
... | Raw.unknownPrimitive name = nothing

RegisterClockBinding : Raw.RawInstance → Type₀
RegisterClockBinding source =
  Σ Raw.NetId (λ net-id → registerClockNet source ≡ just net-id)

checkRegisterClockBinding : (source : Raw.RawInstance)
  → Diagnostic.CheckResult (RegisterClockBinding source)
checkRegisterClockBinding source with
  registerClockNet source | inspect registerClockNet source
... | nothing | [ clock-path ]ᵢ =
  Diagnostic.rejected (invalid-register-clock source)
... | just net-id | [ clock-path ]ᵢ =
  Diagnostic.accepted (net-id , refl)

ClockBindingEvidence : ∀ {identifier source}
  → Decoded.DecodedOccurrence identifier source → Type₀
ClockBindingEvidence {source = source} decoded with
  Decoded.decodedMode decoded
... | Mode.lut1Parameters table = Unit
... | Mode.lut2Parameters table = Unit
... | Mode.lut3Parameters table = Unit
... | Mode.lut4Parameters table = Unit
... | Mode.lut5Parameters table = Unit
... | Mode.lut6Parameters table = Unit
... | Mode.muxf7Parameters = Unit
... | Mode.muxf8Parameters = Unit
... | Mode.carry4Parameters = Unit
... | Mode.fdreParameters initial = RegisterClockBinding source
... | Mode.fdseParameters initial = RegisterClockBinding source
... | Mode.ibufParameters = Unit
... | Mode.obufParameters = Unit
... | Mode.obufdsParameters = Unit
... | Mode.bufgParameters = Unit
... | Mode.bufgceParameters = Unit

checkClockBinding : ∀ {identifier source}
  → (decoded : Decoded.DecodedOccurrence identifier source)
  → Diagnostic.CheckResult (ClockBindingEvidence decoded)
checkClockBinding {source = source} decoded with Decoded.decodedMode decoded
... | Mode.lut1Parameters table = Diagnostic.accepted tt
... | Mode.lut2Parameters table = Diagnostic.accepted tt
... | Mode.lut3Parameters table = Diagnostic.accepted tt
... | Mode.lut4Parameters table = Diagnostic.accepted tt
... | Mode.lut5Parameters table = Diagnostic.accepted tt
... | Mode.lut6Parameters table = Diagnostic.accepted tt
... | Mode.muxf7Parameters = Diagnostic.accepted tt
... | Mode.muxf8Parameters = Diagnostic.accepted tt
... | Mode.carry4Parameters = Diagnostic.accepted tt
... | Mode.fdreParameters initial = checkRegisterClockBinding source
... | Mode.fdseParameters initial = checkRegisterClockBinding source
... | Mode.ibufParameters = Diagnostic.accepted tt
... | Mode.obufParameters = Diagnostic.accepted tt
... | Mode.obufdsParameters = Diagnostic.accepted tt
... | Mode.bufgParameters = Diagnostic.accepted tt
... | Mode.bufgceParameters = Diagnostic.accepted tt

data ClockBoundOccurrences : ∀ {next sources}
  → Decoded.DecodedOccurrences next sources → Type₀ where
  clockBoundDone : ∀ {next}
    → ClockBoundOccurrences (Decoded.decodedDone {next = next})
  clockBoundNext : ∀ {next source sources}
    {decoded : Decoded.DecodedOccurrence
      (Provenance.occurrenceId next) source}
    {rest : Decoded.DecodedOccurrences (suc next) sources}
    → ClockBindingEvidence decoded
    → ClockBoundOccurrences rest
    → ClockBoundOccurrences (Decoded.decodedNext decoded rest)

checkClockBindings : ∀ {next sources}
  → (decoded : Decoded.DecodedOccurrences next sources)
  → Diagnostic.CheckResult (ClockBoundOccurrences decoded)
checkClockBindings Decoded.decodedDone = Diagnostic.accepted clockBoundDone
checkClockBindings (Decoded.decodedNext decoded rest) with
  checkClockBinding decoded
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted binding with checkClockBindings rest
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted bindings =
  Diagnostic.accepted (clockBoundNext binding bindings)

insertClockNet : Raw.NetId → List Raw.NetId → List Raw.NetId
insertClockNet net-id net-ids =
  if LegacyValidation.containsNet net-id net-ids
  then net-ids
  else net-id ∷ᴸ net-ids

clockNets : List Raw.RawInstance → List Raw.NetId
clockNets []ᴸ = []ᴸ
clockNets (source ∷ᴸ sources) with registerClockNet source
... | nothing = clockNets sources
... | just net-id = insertClockNet net-id (clockNets sources)

clockDomainCount : Raw.RawDesign → ℕ
clockDomainCount design =
  lengthList (clockNets (Raw.rawInstances design))

withinDomainBound? : ℕ → ℕ → Bool
withinDomainBound? zero zero = true
withinDomainBound? zero (suc observed) = false
withinDomainBound? (suc maximum) zero = true
withinDomainBound? (suc maximum) (suc observed) =
  withinDomainBound? maximum observed

hasBidirectionalTop? : List Raw.RawTopPort → Bool
hasBidirectionalTop? []ᴸ = false
hasBidirectionalTop? (port ∷ᴸ ports) with Raw.rawTopPortDirection port
... | Raw.bidirectionalPort = true
... | Raw.inputPort = hasBidirectionalTop? ports
... | Raw.outputPort = hasBidirectionalTop? ports

bidirectionalAccepted? : Bool → Bool → Bool
bidirectionalAccepted? true observed = true
bidirectionalAccepted? false false = true
bidirectionalAccepted? false true = false

targetAccepted? : Maybe String → Maybe String → Bool
targetAccepted? nothing nothing = true
targetAccepted? nothing (just observed) = false
targetAccepted? (just expected) nothing = false
targetAccepted? (just expected) (just observed) =
  primStringEquality expected observed

record StrongProfileAdmission
  (profile : Profile.EnforceableProfile)
  {artifact : Artifact.RawArtifact}
  (validated : Validated.ValidatedDesign artifact) : Type₀ where
  constructor strongProfileAdmission
  field
    occurrenceCapabilities :
      ProfiledOccurrences profile
        (Decoded.decodedOccurrences (Validated.decoded validated))
    retainedClockBindings :
      ClockBoundOccurrences
        (Decoded.decodedOccurrences (Validated.decoded validated))
    retainedProfileName : String
    retainedProfileName-is-source :
      retainedProfileName ≡ Profile.profileName profile
    retainedClockDomains : ℕ
    retainedClockDomains-are-source :
      retainedClockDomains
      ≡ clockDomainCount (Artifact.decodedDesign artifact)
    retainedDomainBound :
      withinDomainBound?
        (Profile.maximumClockDomains profile) retainedClockDomains
      ≡ true
    retainedBidirectionalUse : Bool
    retainedBidirectionalUse-is-source :
      retainedBidirectionalUse
      ≡ hasBidirectionalTop?
          (Raw.rawTopPorts (Artifact.decodedDesign artifact))
    retainedBidirectionalPolicy :
      bidirectionalAccepted?
        (Profile.allowsBidirectional profile) retainedBidirectionalUse
      ≡ true
    retainedTarget : Maybe String
    retainedTarget-is-source :
      retainedTarget
      ≡ Raw.rawTargetProfile (Artifact.decodedDesign artifact)
    retainedTargetPolicy :
      targetAccepted? (Profile.profileTarget profile) retainedTarget ≡ true

open StrongProfileAdmission public

validateProfile :
  (profile : Profile.EnforceableProfile)
  → ∀ {artifact}
  → (validated : Validated.ValidatedDesign artifact)
  → Diagnostic.CheckResult (StrongProfileAdmission profile validated)
validateProfile profile {artifact} validated with
  checkOccurrences profile
    (Decoded.decodedOccurrences (Validated.decoded validated))
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted capabilities with
  checkClockBindings
    (Decoded.decodedOccurrences (Validated.decoded validated))
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted clock-bindings with
  withinDomainBound?
    (Profile.maximumClockDomains profile)
    (clockDomainCount (Artifact.decodedDesign artifact))
  | inspect
      (withinDomainBound? (Profile.maximumClockDomains profile))
      (clockDomainCount (Artifact.decodedDesign artifact))
...     | false | [ domain-path ]ᵢ =
  Diagnostic.rejected
    (domain-overflow
      (Profile.maximumClockDomains profile)
      (clockDomainCount (Artifact.decodedDesign artifact)))
...     | true | [ domain-path ]ᵢ with
  bidirectionalAccepted?
    (Profile.allowsBidirectional profile)
    (hasBidirectionalTop?
      (Raw.rawTopPorts (Artifact.decodedDesign artifact)))
  | inspect
      (bidirectionalAccepted? (Profile.allowsBidirectional profile))
      (hasBidirectionalTop?
        (Raw.rawTopPorts (Artifact.decodedDesign artifact)))
...       | false | [ bidirectional-path ]ᵢ =
  Diagnostic.rejected bidirectional-forbidden
...       | true | [ bidirectional-path ]ᵢ with
  targetAccepted?
    (Profile.profileTarget profile)
    (Raw.rawTargetProfile (Artifact.decodedDesign artifact))
  | inspect
      (targetAccepted? (Profile.profileTarget profile))
      (Raw.rawTargetProfile (Artifact.decodedDesign artifact))
...         | false | [ target-path ]ᵢ =
  Diagnostic.rejected
    (target-mismatch
      (Profile.profileTarget profile)
      (Raw.rawTargetProfile (Artifact.decodedDesign artifact)))
...         | true | [ target-path ]ᵢ =
  Diagnostic.accepted
    (strongProfileAdmission capabilities clock-bindings
      (Profile.profileName profile) refl
      (clockDomainCount (Artifact.decodedDesign artifact)) refl domain-path
      (hasBidirectionalTop?
        (Raw.rawTopPorts (Artifact.decodedDesign artifact)))
      refl bidirectional-path
      (Raw.rawTargetProfile (Artifact.decodedDesign artifact))
      refl target-path)