GV119 assurance

GV119 makes the learning-debt policy executable without pretending to prove human understanding. The compiler checks the gate matrix: open debt blocks feature/refactor work, a corrective pull request requires an explicit urgent bypass, patch releases may proceed with debt, and major/minor releases may not.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV119 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
open import Govenv.Kernel.Release using (major; minor; patch)

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

record Proposition : Set where
  constructor satisfied
  field
    featureWithDebtIsBlocked :
      prLearningAllowed feature sampleDebt noBypass ≡ false
    refactorWithDebtIsBlocked :
      prLearningAllowed refactor sampleDebt noBypass ≡ false
    correctiveNeedsExplicitBypass :
      prLearningAllowed corrective sampleDebt noBypass ≡ false
    correctiveBypassWorks :
      prLearningAllowed corrective sampleDebt urgentCorrective ≡ true
    patchMayCarryDebt :
      releaseLearningAllowed patch sampleDebt ≡ true
    minorMayNotCarryDebt :
      releaseLearningAllowed minor sampleDebt ≡ false
    majorMayNotCarryDebt :
      releaseLearningAllowed major sampleDebt ≡ false

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

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof