GV122 assurance

GV122 closes the candidate-boundary enforcement gap left by GV119. Candidate classification remains a Protocol judgment, while the pure learning decision classifies the recorded assessment, evidence, debt, and bypass. Candidate-specific acceptance is applied at the observed pull-request boundary rather than embedded as a static requirement of the repository assurance closure.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV122 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.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Learning

sampleDebt : LearningDebt
sampleDebt =
  learningRequirement
    "Explain the candidate learning boundary."
    "base-revision"
  ∷ []

record Proposition : Set where
  constructor satisfied
  field
    expandingCandidateRequiresRequirements :
      candidateLearningAllowed
        feature expands false true true [] noBypass ≡ false
    featureCannotCarryUnlearnedRequirements :
      candidateLearningAllowed
        feature expands true false true sampleDebt noBypass ≡ false
    correctiveBypassMayPreserveDebt :
      candidateLearningAllowed
        corrective expands true false true sampleDebt urgentCorrective ≡ true
    correctiveBypassCannotLoseDebt :
      candidateLearningAllowed
        corrective expands true false false sampleDebt urgentCorrective ≡ false

proof : Proposition
proof = satisfied refl refl refl refl

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof