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

module Spartan6.Architecture.Refinement where

open import Spartan6.Prelude

import Spartan6.Architecture.Profile as LegacyProfile

-- Refinement stages are evidence carriers, not validators and not device
-- claims.  Evidence is an explicit project-owned type supplied by the caller;
-- the carrier never turns a Boolean, tool success, name, or digest into a
-- theorem.  Provenance records the mapping between stage identities without
-- asserting that either identity denotes a particular FPGA.

record RefinementProvenance : Type₀ where
  constructor refinementProvenance
  field
    sourceIdentity : String
    resultIdentity : String
    transformationIdentity : String
    provenanceMap : List (String × String)

open RefinementProvenance public

record LogicalRefinement
  (Source Logical LogicalEvidence : Type₀) : Type₀ where
  constructor logicalRefinement
  field
    logicalSource : Source
    logicalResult : Logical
    logicalEvidence : LogicalEvidence
    logicalProvenance : RefinementProvenance

open LogicalRefinement public

record PlacedRefinement
  (LogicalStage Placed PlacementEvidence : Type₀) : Type₀ where
  constructor placedRefinement
  field
    placedSource : LogicalStage
    placedResult : Placed
    placementEvidence : PlacementEvidence
    placementProvenance : RefinementProvenance

open PlacedRefinement public

record RoutedRefinement
  (PlacedStage Routed RoutingEvidence : Type₀) : Type₀ where
  constructor routedRefinement
  field
    routedSource : PlacedStage
    routedResult : Routed
    routingEvidence : RoutingEvidence
    routingProvenance : RefinementProvenance

open RoutedRefinement public

record ConfiguredRefinement
  (RoutedStage Configuration ConfigurationEvidence : Type₀) : Type₀ where
  constructor configuredRefinement
  field
    configuredSource : RoutedStage
    configuredResult : Configuration
    configurationEvidence : ConfigurationEvidence
    configurationProvenance : RefinementProvenance

open ConfiguredRefinement public

-- Phase 9 deliberately leaves part, package, revision, and errata selection
-- outside these carriers.

migration-selects-no-device :
  LegacyProfile.selectedDeviceProfile ≡ nothing
migration-selects-no-device = refl