GV18 assurance

GV18 is satisfied when candidate validation permits semantic authority to be one commit ahead of versioned materializations without granting the candidate a write capability. The Test workflow must materialize only in its ephemeral workspace before checking the resulting state, while the post-authorization Materialize workflow retains the canonical derived-commit identity and parent provenance marker.

GitHub Actions Test run 35996248284 is the preserved counterexample: commit 5770bc3 was semantically valid, but the old Test workflow rejected it solely because CHANGELOG.md still reflected its semantic parent. The fix must keep that case valid without requiring candidate authors or agents to create the derived commit themselves.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV18 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([]; _∷_)
open import Agda.Builtin.Maybe using (just; nothing)
open import Govenv.Github.Authorization using
  ( WorkflowSecurityProfile; candidateSource; ungatedCandidate
  ; readOnlyToken; testJob )
open import Govenv.Administration using (authorizedBranch)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Materialization.Github.Workflows.Materialize using
  (materializerCommitSubject; derivedFromParentMarker)
open import Govenv.Materialization.Github.Workflows.Test using
  ( candidateValidationSteps; materializeCommand; previewCommand
  ; candidateLearningCommand; checkCommand; testCommand )
open import Govenv.Materialization.Github.Workflows.Workflow using
  (binding; expression; literal; runStep)

record Proposition : Set where
  constructor satisfied
  field
    candidateMaterializesBeforeValidation :
      candidateValidationSteps ≡
        ( runStep "Materialize candidate transiently" nothing nothing
            materializeCommand []
        ∷ runStep "Record candidate materialization preview" nothing nothing
            previewCommand []
        ∷ runStep "Check candidate learning gate" nothing
            (just "github.event_name == 'pull_request'")
            candidateLearningCommand
            ( binding "GOVENV_CANDIDATE_COMPARISON_BASE_SHA"
                (expression "github.event.pull_request.base.sha")
            ∷ binding "GOVENV_CANDIDATE_TARGET_BRANCH"
                (expression "github.event.pull_request.base.ref")
            ∷ binding "GOVENV_AUTHORIZED_BRANCH"
                (literal authorizedBranch)
            ∷ [])
        ∷ runStep "Check materialized candidate" nothing nothing
            checkCommand []
        ∷ runStep "Run tests" nothing nothing testCommand []
        ∷ [] )
    candidateSourceRemainsUnprivileged :
      WorkflowSecurityProfile.sourceAuthority testJob ≡ candidateSource
    candidateHasNoPrivilegedEnvironment :
      WorkflowSecurityProfile.environmentGate testJob ≡ ungatedCandidate
    candidateTokenRemainsReadOnly :
      WorkflowSecurityProfile.githubToken testJob ≡ readOnlyToken
    postAuthorizationCommitIdentity :
      materializerCommitSubject ≡
        "chore(materialize): update governed materializations"
    postAuthorizationCommitRetainsParentProvenance :
      derivedFromParentMarker ≡ "Derived-From-Parent: true"

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

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof