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

module Spartan6.Validation.ProfileSoundness where

open import Spartan6.Prelude

import Spartan6.Architecture.EvidenceRegistry as Registry
import Spartan6.Architecture.ModeCapability as Capability
import Spartan6.Architecture.Profile as LegacyProfile
import Spartan6.Architecture.ProfileDeclaration as Profile
import Spartan6.Import.Artifact as Artifact
import Spartan6.Validation.CheckResult as Result
import Spartan6.Validation.DecodedDesign as Decoded
import Spartan6.Validation.Design as Validated
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Profile as Validation
import Spartan6.Validation.Raw as LegacyValidation

-- The strong result exposes each policy obligation without re-running any
-- checker.  These projection lemmas are the contract consumed downstream.

admission-retains-authoritative-clock-bindings :
  ∀ {profile artifact} {validated : Validated.ValidatedDesign artifact}
  → (admission : Validation.StrongProfileAdmission profile validated)
  → Validation.ClockBoundOccurrences
      (Decoded.decodedOccurrences (Validated.decoded validated))
admission-retains-authoritative-clock-bindings =
  Validation.retainedClockBindings

admission-respects-domain-bound :
  ∀ {profile artifact} {validated : Validated.ValidatedDesign artifact}
  → (admission : Validation.StrongProfileAdmission profile validated)
  → Validation.withinDomainBound?
      (Profile.maximumClockDomains profile)
      (Validation.retainedClockDomains admission)
    ≡ true
admission-respects-domain-bound = Validation.retainedDomainBound

admission-respects-bidirectional-policy :
  ∀ {profile artifact} {validated : Validated.ValidatedDesign artifact}
  → (admission : Validation.StrongProfileAdmission profile validated)
  → Validation.bidirectionalAccepted?
      (Profile.allowsBidirectional profile)
      (Validation.retainedBidirectionalUse admission)
    ≡ true
admission-respects-bidirectional-policy =
  Validation.retainedBidirectionalPolicy

admission-respects-target :
  ∀ {profile artifact} {validated : Validated.ValidatedDesign artifact}
  → (admission : Validation.StrongProfileAdmission profile validated)
  → Validation.targetAccepted?
      (Profile.profileTarget profile)
      (Validation.retainedTarget admission)
    ≡ true
admission-respects-target = Validation.retainedTargetPolicy

profile-validation-accepted-is-unique :
  ∀ {profile artifact} {validated : Validated.ValidatedDesign artifact}
  {left right : Validation.StrongProfileAdmission profile validated}
  → Diagnostic.accepted left ≡ Diagnostic.accepted right
  → left ≡ right
profile-validation-accepted-is-unique = Result.accepted-injective

occurrence-retains-exact-premise :
  ∀ {profile identifier source}
    {decoded : Decoded.DecodedOccurrence identifier source}
  → (admission : Validation.OccurrenceCapability profile decoded)
  → Capability.conditionalPremise
      (Validation.exactModeCapability admission)
    ≡ Capability.modePremise (Decoded.decodedMode decoded)
occurrence-retains-exact-premise admission =
  Capability.premise-is-exact
    (Validation.exactModeCapability admission)

occurrence-retains-canonical-traceability :
  ∀ {profile identifier source}
    {decoded : Decoded.DecodedOccurrence identifier source}
  → (admission : Validation.OccurrenceCapability profile decoded)
  → Capability.traceability
      (Validation.exactModeCapability admission)
    ≡ Registry.modeTraceability
        (Decoded.decodedKind decoded) (Decoded.decodedMode decoded)
occurrence-retains-canonical-traceability admission =
  Capability.traceability-is-canonical
    (Validation.exactModeCapability admission)

-- Compatibility is deliberately one way and evidence preserving.  A caller
-- may package an independently proved legacy AdmittedFor value alongside the
-- strong result, but the new checker does not synthesize the legacy proof from
-- weaker kind-wide labels.  The equality prevents a wrapper from silently
-- switching to a different raw design.

record LegacyAdmissionWrapper
  (profile : Profile.EnforceableProfile)
  {artifact : Artifact.RawArtifact}
  {validated : Validated.ValidatedDesign artifact}
  (strong : Validation.StrongProfileAdmission profile validated)
  (legacyProfile : LegacyProfile.ArchitectureProfile) : Type₀ where
  constructor legacyAdmissionWrapper
  field
    legacyAdmission : LegacyValidation.AdmittedFor legacyProfile
    legacy-source-is-validated :
      fst legacyAdmission ≡ Artifact.decodedDesign artifact

open LegacyAdmissionWrapper public

legacy-wrapper-retains-strong-result :
  ∀ {profile artifact}
    {validated : Validated.ValidatedDesign artifact}
    {strong : Validation.StrongProfileAdmission profile validated}
    {legacyProfile}
  → LegacyAdmissionWrapper profile strong legacyProfile
  → Validation.StrongProfileAdmission profile validated
legacy-wrapper-retains-strong-result {strong = strong} wrapper = strong

legacy-wrapper-requires-legacy-evidence :
  ∀ {profile artifact}
    {validated : Validated.ValidatedDesign artifact}
    {strong : Validation.StrongProfileAdmission profile validated}
    {legacyProfile}
  → (wrapper : LegacyAdmissionWrapper profile strong legacyProfile)
  → LegacyValidation.AdmittedFor legacyProfile
legacy-wrapper-requires-legacy-evidence = legacyAdmission