GV108 assurance

GV108 separates the one human-facing administrative bootstrap/recovery boundary from ordinary post-authorization materialization. The administrative setup has no repository-metadata constructor, its checkout observes full Git history, and repository metadata is automatic while remaining admin-privileged and read-back verified. The automatic metadata job is gated by the main-only administrative environment and consumes the governed root credential name.

GitHub Actions run 35778439538 exposed the checkout-history regression: the manual Admin Materialize run failed in govenv:check before any effect because a shallow checkout hid the published release tag. adminCheckoutFetchDepth therefore remains part of the static assurance below.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV108 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([]; _∷_)
import Govenv.Materialization.Github.Repository.Description as Description
import Govenv.Materialization.Github.Repository.Website as Website
import Govenv.Materialization.Github.Repository.Topics as Topics
open import Govenv.Administration using (adminEnvironment; adminTokenSecret)
open import Govenv.Github.Authorization using
  ( WorkflowSecurityProfile; authorizedRepositoryAdministrationJob
  ; authorizedEnvironment )
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Materialization using
  ( Materialization; automatic; admin )
open import Govenv.Materialization.Github.Administration.Setup using
  ( plan; adminEnvironmentStep; materializerEnvironmentBoundaryStep
  ; materializerCredentialStep; materializerEnvironmentStep
  ; authorizedEffectsEnvironmentStep; pagesEnvironmentStep )
open import Govenv.Materialization.Github.Workflows.AdminMaterialize using
  (adminCheckoutFetchDepth)
open import Govenv.Materialization.Github.Workflows.Materialize using
  (repositoryMetadataCredentialSecret)

record Proposition : Set where
  constructor satisfied
  field
    setupContainsOnlyAuthoritySteps :
      plan ≡
        (adminEnvironmentStep
        ∷ materializerEnvironmentBoundaryStep
        ∷ materializerCredentialStep
        ∷ materializerEnvironmentStep
        ∷ authorizedEffectsEnvironmentStep
        ∷ pagesEnvironmentStep
        ∷ [])
    adminCheckObservesFullHistory : adminCheckoutFetchDepth ≡ "0"
    descriptionIsAutomatic :
      Materialization.application Description.materialization ≡ automatic
    websiteIsAutomatic :
      Materialization.application Website.materialization ≡ automatic
    topicsAreAutomatic :
      Materialization.application Topics.materialization ≡ automatic
    descriptionRemainsAdminPrivileged :
      Materialization.privilege Description.materialization ≡ admin
    websiteRemainsAdminPrivileged :
      Materialization.privilege Website.materialization ≡ admin
    topicsRemainAdminPrivileged :
      Materialization.privilege Topics.materialization ≡ admin
    metadataUsesAdministrativeBoundary :
      WorkflowSecurityProfile.environmentGate authorizedRepositoryAdministrationJob ≡
        authorizedEnvironment adminEnvironment
    metadataUsesGovernedRootCredential :
      repositoryMetadataCredentialSecret ≡ adminTokenSecret

proof : Proposition
proof = satisfied refl refl refl refl refl refl refl refl refl refl

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof