Administrative materialization

Administrative authority has one human-supplied root. GOVENV_ADMIN_TOKEN is the current credential representing that root; replacing or rotating the token changes the credential, never the identity of the administrative authority. Candidate, agent, release, Pages, and repository Git-materializer paths must never consume the root credential. After human authorization, a dedicated main-only repository-administration effect job may consume it solely for deterministic GitHub API effects that require Administration: write and cannot be exercised by the derived deploy-key credential.

Administrative root

The only irreducible human bootstrap is provisioning GOVENV_ADMIN_TOKEN into the main-only admin-materialization environment. The fine-grained token is repository-restricted and requires Administration: read/write plus Environments: read/write. It intentionally receives no Actions, Contents, or Workflows permission.

From an AuthorizedRevision, Admin Materialize uses that root credential to derive and reconcile subordinate authority. No GitHub App, client ID, private key, deploy key, environment secret, variable, ruleset mutation, or individual administrative target may require a second manual provisioning ceremony.

Convergent setup

GV92 requires the human-facing administrative operation to become one revision-bound setup, not a menu of independent targets. That setup is limited to bootstrap, recovery, authority-boundary reconciliation, and subordinate credential rotation. Ordinary project-state effects such as description, website, and topics are reconciled automatically after an AuthorizedRevision and are not setup steps. Re-running setup must converge partially configured authority state toward the canonical state and rotates the governed materializer keypair.

Every externally observable step retains apply → read-back → equality semantics. Secret values are not readable through GitHub and therefore are not constitutional data; governance owns their identity, placement, derivation procedure, and observable name boundary.

Authorized materializer

The GV92/GV93 materializer design uses one repository-scoped write deploy key named govenv-materializer. The current convergent setup rotates this keypair on every successful execution: it first hardens authorized-materialization to main, generates an ephemeral Ed25519 keypair, replaces the complete repository deploy-key set with the governed public key, streams the private key into the environment secret GOVENV_MATERIALIZER_SSH_KEY, and deletes the runner-local key material. Rotation is used because GitHub does not expose environment secret values for read-back; each successful setup therefore re-establishes the private/public correspondence from one generated pair rather than trusting an unreadable prior value.

GitHub rulesets grant bypass to the DeployKey actor class rather than to one deploy key identifier. Therefore the repository deploy-key set is governed as a closed set containing only the materializer key. Setup removes stale or unauthorized deploy keys and verifies the complete observed set before any DeployKey bypass may become active.

The materializer credential creates no semantic authority: it may apply only deterministic effects causally derived from an AuthorizedRevision.

Candidate authoring

Automated candidate authorship remains a distinct, unprivileged identity with ordinary content and pull-request capabilities but no authority to merge, bypass main, mutate persistent governed external state, or alter executable automation. GV92 forbids solving this boundary with another manually provisioned credential. The concrete platform mechanism remains intentionally abstract until those constraints are mechanically established.

Monotonic rollout

GV91 still controls activation order. Setup may prepare environments and subordinate credentials before stronger rulesets exist, but an enforcement may become active only when every path needed to operate, verify, and repair under it already exists in an AuthorizedRevision and its prerequisite capabilities have been read-back verified.

{-# OPTIONS --safe #-}

module Govenv.Administration where

open import Agda.Builtin.String using (String)

data AdministrativeRoot : Set where
  govenvAdministrativeRoot : AdministrativeRoot

record AdministrativeCredential (root : AdministrativeRoot) : Set where
  constructor administrativeCredential
  field
    secretName : String

adminCredential : AdministrativeCredential govenvAdministrativeRoot
adminCredential = administrativeCredential "GOVENV_ADMIN_TOKEN"

adminTokenSecret : String
adminTokenSecret = AdministrativeCredential.secretName adminCredential

adminEnvironment : String
adminEnvironment = "admin-materialization"

authorizedBranch : String
authorizedBranch = "main"

record DerivedCredential (root : AdministrativeRoot) : Set where
  constructor derivedCredential
  field
    identity : String

materializerCredential : DerivedCredential govenvAdministrativeRoot
materializerCredential = derivedCredential "govenv-materializer"

materializerDeployKeyTitle : String
materializerDeployKeyTitle = DerivedCredential.identity materializerCredential

candidateAuthorIdentity : String
candidateAuthorIdentity = "candidate-author"

materializerEnvironment : String
materializerEnvironment = "authorized-materialization"

materializerCredentialName : String
materializerCredentialName = "GOVENV_MATERIALIZER_SSH_KEY"

materializerBranch : String
materializerBranch = authorizedBranch

authorizedEffectsEnvironment : String
authorizedEffectsEnvironment = "authorized-effects"

pagesEnvironment : String
pagesEnvironment = "github-pages"

authorizationHumanLogin : String
authorizationHumanLogin = "klarkc"