Materialization

Materialization defines canonical semantic target state from governed project data. Projection only encodes that state for a concrete target format, while adapters only observe, apply, or verify effects. Application mode, privilege, authority requirement, and verification are governed properties of each materialization target. Computing or rendering a candidate materialization does not itself require authority; ApplicationPlan governs only application to an authoritative repository or persistent external target.

{-# OPTIONS --safe #-}

module Govenv.Materialization where

open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.String using (String)
open import Govenv.Authorization using (AuthorizedRevision)

data Application : Set where
  automatic manual : Application

data Privilege : Set where
  repository admin : Privilege

data ApplicationAuthority : Set where
  unprivileged authorizedOnly : ApplicationAuthority

data ApplicationAuthorization : ApplicationAuthority → Set where
  unprivilegedApplication : ApplicationAuthorization unprivileged
  authorizedApplication : AuthorizedRevision → ApplicationAuthorization authorizedOnly

data GithubRepositoryProperty : Set where
  repositoryDescription repositoryWebsite repositoryTopics : GithubRepositoryProperty

data RepositoryFileSection : Set where
  releaseGovernanceImpactInChangelog : RepositoryFileSection

data RepositoryFileSectionPlacement : Set where
  afterReleaseHeadingInFile : String → RepositoryFileSectionPlacement

data GithubPullRequestSection : Set where
  releaseGovernanceImpact : GithubPullRequestSection

data GithubReleaseSection : Set where
  releaseGovernanceImpactInRelease : GithubReleaseSection

data GithubPullRequestBodyPlacement : Set where
  afterReleaseHeadingInBody : String → GithubPullRequestBodyPlacement

data GithubReleaseBodyPlacement : Set where
  replaceCarriedChangelogSection : GithubReleaseBodyPlacement

data Target : Set where
  repositoryFile : String → Target
  repositoryFileSection :
    String → RepositoryFileSection → RepositoryFileSectionPlacement → Target
  githubRepository : GithubRepositoryProperty → Target
  githubRepositoryRuleset : String → Target
  githubRepositoryDeployKeys : Target
  githubActionsEnvironment : String → Target
  githubPullRequestBodySection :
    Nat → GithubPullRequestSection → GithubPullRequestBodyPlacement → Target
  githubReleaseBodySection :
    String → GithubReleaseSection → GithubReleaseBodyPlacement → Target

data Verification : Target → Set where
  trackedEquality : {path : String} → Verification (repositoryFile path)
  repositoryFileSectionEquality :
    {path : String} {section : RepositoryFileSection}
    {placement : RepositoryFileSectionPlacement} →
    Verification (repositoryFileSection path section placement)
  descriptionReadBackEquality :
    Verification (githubRepository repositoryDescription)
  websiteReadBackEquality :
    Verification (githubRepository repositoryWebsite)
  topicsReadBackSetEquality :
    Verification (githubRepository repositoryTopics)
  rulesetReadBackEquality : {name : String} →
    Verification (githubRepositoryRuleset name)
  deployKeySetReadBackEquality : Verification githubRepositoryDeployKeys
  environmentBoundaryReadBackEquality : {name : String} →
    Verification (githubActionsEnvironment name)
  pullRequestBodySectionEquality :
    {number : Nat} {section : GithubPullRequestSection}
    {placement : GithubPullRequestBodyPlacement} →
    Verification (githubPullRequestBodySection number section placement)
  githubReleaseBodySectionEquality :
    {tag : String} {section : GithubReleaseSection}
    {placement : GithubReleaseBodyPlacement} →
    Verification (githubReleaseBodySection tag section placement)

record Materialization (State : Set) : Set where
  constructor materialized
  field
    target : Target
    application : Application
    privilege : Privilege
    authority : ApplicationAuthority
    verification : Verification target
    state : State

record ApplicationPlan
  {State : Set}
  (materialization : Materialization State)
  : Set where
  constructor applicationPlan
  field
    authorization :
      ApplicationAuthorization (Materialization.authority materialization)

versionedApplication : Application
versionedApplication = automatic

versionedPrivilege : Privilege
versionedPrivilege = repository

versionedAuthority : ApplicationAuthority
versionedAuthority = authorizedOnly

authorizedEffectApplication : Application
authorizedEffectApplication = automatic

adminApplication : Application
adminApplication = manual

adminPrivilege : Privilege
adminPrivilege = admin

adminAuthority : ApplicationAuthority
adminAuthority = authorizedOnly