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

module Spartan6.Examples.ProfileValidation where

open import Spartan6.Prelude
open import Spartan6.Evidence

import Spartan6.Architecture.ModeCapability as Capability
import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Architecture.Profile as LegacyProfile
import Spartan6.Architecture.ProfileDeclaration as Profile
import Spartan6.Examples.ImportedYosys as Imported
import Spartan6.Examples.RawCarry4 as RawCarry4
import Spartan6.Fixtures.YosysArtifacts as ArtifactExample
import Spartan6.Netlist.AdmissionCore as Core
import Spartan6.Netlist.PrimitiveHandler as Handler
import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.Raw as Raw
import Spartan6.Semantics.Design as Semantics
import Spartan6.Validation.CheckResult as Result
import Spartan6.Validation.DecodedDesign as Decoded
import Spartan6.Validation.Parameter as Mode
import Spartan6.Validation.Profile as Validation

-- Minimal reduction probe: the exact IBUF mode carries the independently
-- proved identity handler, rather than inheriting executability from a label.

ibuf-capability-is-certified-identity :
  Capability.semanticEvidenceFor Mode.ibufParameters
  ≡ Capability.executableCombinational Handler.identityHandler refl
ibuf-capability-is-certified-identity = refl

ibufIdentityRelation : Capability.DecidableModeRelation   
ibufIdentityRelation = Capability.decidableModeRelation
  (λ { [] → true })
  (λ { (input ∷ []) [] (output ∷ []) → not (input ⊕ output) })
  (λ { input [] [] → true })

relationalIBUFDeclaration :
  Profile.DeclaredModeCapability Mode.ibufParameters
relationalIBUFDeclaration = Profile.declaredModeCapability
  fullySupported
  (just (Capability.relationalContract ibufIdentityRelation))
  (just Capability.noAdditionalPremise)

relational-contract-is-an-enforceable-alternative :
  Profile.capabilityAvailable?
    (Profile.compileDeclaredMode relationalIBUFDeclaration)
  ≡ true
relational-contract-is-an-enforceable-alternative = refl

-- Negative declaration probe 1: a fully-supported label without semantics is
-- rejected by the profile compiler.

fullySupportedWithoutSemantics :
  Profile.DeclaredModeCapability Mode.ibufParameters
fullySupportedWithoutSemantics =
  Profile.declaredModeCapability
    fullySupported nothing (just Capability.noAdditionalPremise)

fully-supported-without-semantics-is-rejected :
  Profile.compileDeclaredMode fullySupportedWithoutSemantics ≡ nothing
fully-supported-without-semantics-is-rejected = refl

-- Negative declaration probe 2: CARRY4 is conditional even though its local
-- handler is certified.  Omitting the premise keeps the declaration closed.

conditionalCarryWithoutPremise :
  Profile.DeclaredModeCapability Mode.carry4Parameters
conditionalCarryWithoutPremise =
  Profile.declaredModeCapability
    conditionallySupported
    (just (Capability.semanticEvidenceFor Mode.carry4Parameters))
    nothing

conditional-mode-without-premise-is-rejected :
  Profile.compileDeclaredMode conditionalCarryWithoutPremise ≡ nothing
conditional-mode-without-premise-is-rejected = refl

-- The declared premise is not enough by itself: it is discharged against the
-- occurrence.  The accepted and simultaneous-source CARRY4 probes agree with
-- the existing builder restriction.

restricted-carry-premise-is-accepted :
  Result.accepted?
    (Validation.checkPremise RawCarry4.positiveRawCarry4
      Capability.nonselectedCarryEntryIsLow)
  ≡ true
restricted-carry-premise-is-accepted = refl

simultaneous-carry-sources-fail-the-premise :
  Result.accepted?
    (Validation.checkPremise RawCarry4.simultaneousRawCarry4
      Capability.nonselectedCarryEntryIsLow)
  ≡ false
simultaneous-carry-sources-fail-the-premise = refl

registerInput : String → Raw.Connection → Raw.RawPort
registerInput name connection =
  Raw.rawPort name Raw.inputPort  (connection ∷ᴸ []ᴸ)

registerOutput : String → Raw.NetId → Raw.RawPort
registerOutput name net-id =
  Raw.rawPort name Raw.outputPort  (Raw.net net-id ∷ᴸ []ᴸ)

constantClockFDRE : Raw.RawInstance
constantClockFDRE = Raw.rawInstance
  "constant-clock-fdre"
  (Raw.knownPrimitive Architecture.FDRE)
  ( registerInput "D" (Raw.net )
  ∷ᴸ registerInput "C" (Raw.constant low)
  ∷ᴸ registerInput "CE" (Raw.constant high)
  ∷ᴸ registerInput "R" (Raw.constant low)
  ∷ᴸ registerOutput "Q" 
  ∷ᴸ []ᴸ )
  []ᴸ
  (just low)

constant-clock-register-still-decodes :
  Result.accepted?
    (Decoded.decodeOccurrence
      (Provenance.occurrenceId ) constantClockFDRE)
  ≡ true
constant-clock-register-still-decodes = refl

constantClockDecoded :
  Decoded.DecodedOccurrence
    (Provenance.occurrenceId ) constantClockFDRE
constantClockDecoded = Result.extractAccepted
  (Decoded.decodeOccurrence
    (Provenance.occurrenceId ) constantClockFDRE)
  constant-clock-register-still-decodes

constant-clock-register-is-rejected-before-domain-counting :
  Result.accepted? (Validation.checkClockBinding constantClockDecoded)
  ≡ false
constant-clock-register-is-rejected-before-domain-counting = refl

-- Remaining contradictory-policy probes are executable and definitionally
-- reduce to rejection.

excess-clock-domains-are-rejected :
  Validation.withinDomainBound?   ≡ false
excess-clock-domains-are-rejected = refl

forbidden-bidirectional-use-is-rejected :
  Validation.bidirectionalAccepted? false true ≡ false
forbidden-bidirectional-use-is-rejected = refl

target-mismatch-is-rejected :
  Validation.targetAccepted?
    (just "phase9-architecture-a")
    (just "phase9-architecture-b")
  ≡ false
target-mismatch-is-rejected = refl

-- A proof profile for the whole imported toggle.  This is not the development
-- profile and not a device profile: it exists only as a closed proof probe for
-- exact decoded modes, one clock domain, no bidirectional ports, official
-- traceability, and no target claim.

toggleProbeDeclaration : Profile.ProfileDeclaration
toggleProbeDeclaration = Profile.profileDeclaration
  "phase9-imported-toggle-proof-probe"
  nothing
   false true
  (λ kind mode → Profile.canonicalModeDeclaration mode)

toggleProbeProfile : Profile.EnforceableProfile
toggleProbeProfile = Profile.compileProfile toggleProbeDeclaration

toggle-profile-validation-succeeds :
  Result.accepted?
    (Validation.validateProfile
      toggleProbeProfile ArtifactExample.toggleValidated)
  ≡ true
toggle-profile-validation-succeeds = refl

toggleProfileAdmission :
  Validation.StrongProfileAdmission
    toggleProbeProfile ArtifactExample.toggleValidated
toggleProfileAdmission = Result.extractAccepted
  (Validation.validateProfile
    toggleProbeProfile ArtifactExample.toggleValidated)
  toggle-profile-validation-succeeds

toggle-profile-retains-one-domain :
  Validation.retainedClockDomains toggleProfileAdmission ≡ 
toggle-profile-retains-one-domain = refl

toggle-profile-retains-no-target :
  Validation.retainedTarget toggleProfileAdmission ≡ nothing
toggle-profile-retains-no-target = refl

-- Whole-example preservation: strengthening admission with profile evidence
-- does not alter the already-proved machine transition.

profiled-toggle-still-toggles-high :
  Semantics.step
    (Core.executableDesign Imported.importedExecutable)
    Semantics.risingEdge
    (high ∷ low ∷ high ∷ [])
    (low ∷ [])
  ≡ high ∷ []
profiled-toggle-still-toggles-high = Imported.enabled-edge-toggles-high

development-profile-remains-closed :
  Profile.capabilityFor Profile.developmentProfile
    _ Mode.ibufParameters ≡ nothing
development-profile-remains-closed =
  Profile.development-mode-is-closed _ Mode.ibufParameters

no-concrete-device-is-selected :
  LegacyProfile.selectedDeviceProfile ≡ nothing
no-concrete-device-is-selected = refl