GV44 assurance

GV44 is statically satisfied only when the versioned Materialize workflow preserves the authorizing run across its own derived push. Automated materializer pushes are identified at the GitHub event boundary by the governed materializer commit identity plus the derived protocol marker, isolated from authorizing concurrency, and rejected as fresh materializer authority. Runs 35641826439, 35642153023, and 35645948292 preserve the counterexamples that require this boundary; generated workflow syntax is additionally validated before candidate acceptance.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV44 where

open import Agda.Builtin.Bool using (true)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([]; _∷_)
open import Agda.Builtin.Maybe using (Maybe; just; nothing)
open import Agda.Builtin.String using (String)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Materialization.Github.Workflows.Materialize using
  ( state
  ; materializerCommitName
  ; materializerCommitEmail
  ; materializerPushIdentityCondition
  ; derivedPushCondition
  ; materializeConcurrencyGroup
  ; authorizedMaterializeOnly )
open import Govenv.Materialization.Github.Workflows.Workflow using
  (Workflow; Job; Concurrency; workflow; job; reusableJob; concurrency)

workflowConcurrency : Workflow → Maybe Concurrency
workflowConcurrency (workflow name triggers policy jobs) = policy

firstJobCondition : Workflow → Maybe String
firstJobCondition
  (workflow name triggers policy
    (job identifier security condition needs outputs environment runner timeout steps ∷ rest)) =
      condition
firstJobCondition value = nothing

record Proposition : Set where
  constructor satisfied
  field
    materializerNameIsGoverned :
      materializerCommitName ≡ "govenv-materializer"
    materializerEmailIsGoverned :
      materializerCommitEmail ≡ "govenv-materializer@users.noreply.github.com"
    materializerPushIdentityIsExplicit :
      materializerPushIdentityCondition ≡
        "github.event_name == 'push' && github.event.head_commit.author.name == 'govenv-materializer' && github.event.head_commit.author.email == 'govenv-materializer@users.noreply.github.com' && github.event.head_commit.committer.name == 'govenv-materializer' && github.event.head_commit.committer.email == 'govenv-materializer@users.noreply.github.com'"
    derivedPushIsExplicit :
      derivedPushCondition ≡
        "github.event_name == 'push' && github.event.head_commit.author.name == 'govenv-materializer' && github.event.head_commit.author.email == 'govenv-materializer@users.noreply.github.com' && github.event.head_commit.committer.name == 'govenv-materializer' && github.event.head_commit.committer.email == 'govenv-materializer@users.noreply.github.com' && startsWith(github.event.head_commit.message, 'chore(materialize): update governed materializations') && contains(github.event.head_commit.message, 'Derived-From-Parent: true')"
    derivedPushHasSeparateConcurrency :
      materializeConcurrencyGroup ≡
        "materialize-${{ github.event_name }}-${{ github.event_name == 'push' && github.event.head_commit.author.name == 'govenv-materializer' && github.event.head_commit.author.email == 'govenv-materializer@users.noreply.github.com' && github.event.head_commit.committer.name == 'govenv-materializer' && github.event.head_commit.committer.email == 'govenv-materializer@users.noreply.github.com' }}"
    derivedPushIsNotFreshAuthority :
      authorizedMaterializeOnly ≡
        "(github.event_name != 'workflow_dispatch' || github.ref == 'refs/heads/main') && !(github.event_name == 'push' && github.event.head_commit.author.name == 'govenv-materializer' && github.event.head_commit.author.email == 'govenv-materializer@users.noreply.github.com' && github.event.head_commit.committer.name == 'govenv-materializer' && github.event.head_commit.committer.email == 'govenv-materializer@users.noreply.github.com' && startsWith(github.event.head_commit.message, 'chore(materialize): update governed materializations') && contains(github.event.head_commit.message, 'Derived-From-Parent: true'))"
    workflowUsesSeparatedConcurrency :
      workflowConcurrency state ≡ just (concurrency materializeConcurrencyGroup true)
    workflowUsesAuthorityGuard :
      firstJobCondition state ≡ just authorizedMaterializeOnly

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

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof