GV125 assurance

GV125 separates candidate composition from semantic authorization. A stacked child pull request is still required to carry a fresh assessment against its immediate comparison base and may not lose unsatisfied learning requirements, but open learning debt does not by itself make the child candidate untestable. The hard GV119/GV122 debt-closure decision applies at the authorization boundary.

Authorization is tightened at the same time: a human pull-request merge carries an explicit target classification, and only a merge into authorizedTarget can construct an AuthorizedRevision. A merge into another candidate branch remains human-reviewed candidate composition, not semantic authority.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV125 where

open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([]; _∷_)
open import Govenv.Assurance.GV125.Counterexample.StackedPullRequestHardGate
open import Govenv.Authorization
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Learning
open import Govenv.Learning using
  (carriedDebt; containsRequirement; stackedCandidateRequirement)

data Impossible : Set where

reviewerPrincipal : Principal
reviewerPrincipal =
  observedPrincipal "human-reviewer" human

reviewer : HumanPrincipal
reviewer =
  humanPrincipal reviewerPrincipal refl

candidateMerge : HumanPullRequestMerge
candidateMerge =
  humanPullRequestMerge
    
    reviewer
    (identifiedRevision "stacked-child")
    candidateTarget

authorizedMerge : HumanPullRequestMerge
authorizedMerge =
  humanPullRequestMerge
    
    reviewer
    (identifiedRevision "authorized-head")
    authorizedTarget

authorized : AuthorizedRevision
authorized =
  authorizedRevision authorizedMerge refl

candidateTargetCannotAuthorize :
  HumanPullRequestMerge.target candidateMerge ≡ authorizedTarget →
  Impossible
candidateTargetCannotAuthorize ()

record Proposition : Set where
  constructor satisfied
  field
    observedOldGateBlocksStack :
      candidateLearningAllowed
        feature expands true false true openDebt noBypass ≡ false
    stackCompositionAllowsPreservedDebt :
      candidateCompositionAllowed
        feature expands true false true noBypass ≡ true
    stackCompositionRejectsLostDebt :
      candidateCompositionAllowed
        feature expands true false false noBypass ≡ false
    compositionBoundaryDoesNotRequireAuthorizationClosure :
      candidateBoundaryAllowed
        candidateComposition true false ≡ true
    authorizationBoundaryRequiresHardGate :
      candidateBoundaryAllowed
        authorizationBoundary true false ≡ false
    authorizedBoundaryAcceptsClosedCandidate :
      candidateBoundaryAllowed
        authorizationBoundary true true ≡ true
    candidateMergeHasNoAuthorizationTarget :
      HumanPullRequestMerge.target candidateMerge ≡ authorizedTarget →
      Impossible
    authorizedMergeTargetsAuthority :
      HumanPullRequestMerge.target
        (AuthorizedRevision.authorization authorized) ≡
      authorizedTarget
    newLearningRequirementRemainsDebt :
      containsRequirement stackedCandidateRequirement carriedDebt ≡ true

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

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof