Governance assurance

Governance completion is not an editorial checkbox. Completed governance must be backed by an assurance mechanism. Historical completions that predate evidence-bearing lifecycle semantics are explicitly enumerated as inherited migration debt; no pending or future governance identity can use that escape hatch.

Static assurances carry an Agda proposition and proof. Observed assurances carry a governed Rule whose verdict must be established from candidate-state facts. GV74 remains pending until every inherited completion has been migrated and candidate validation requires all live completed assurances to hold.

{-# OPTIONS --safe #-}

module Govenv.Assurance where

open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using (List; []; _∷_)
open import Agda.Builtin.Nat using (Nat)
import Govenv.Assurance.GV1 as GV1
import Govenv.Assurance.GV1.Counterexample.SourcePlacement
import Govenv.Assurance.GV3 as GV3
import Govenv.Assurance.GV4 as GV4
import Govenv.Assurance.GV5 as GV5
import Govenv.Assurance.GV6 as GV6
import Govenv.Assurance.GV15 as GV15
import Govenv.Assurance.GV16 as GV16
import Govenv.Assurance.GV18 as GV18
import Govenv.Assurance.GV20 as GV20
import Govenv.Assurance.GV21 as GV21
import Govenv.Assurance.GV44 as GV44
import Govenv.Assurance.GV50 as GV50
import Govenv.Assurance.GV52 as GV52
import Govenv.Assurance.GV54 as GV54
import Govenv.Assurance.GV68 as GV68
import Govenv.Assurance.GV69 as GV69
import Govenv.Assurance.GV70 as GV70
import Govenv.Assurance.GV95 as GV95
import Govenv.Assurance.GV101 as GV101
import Govenv.Assurance.GV108 as GV108
import Govenv.Assurance.GV109 as GV109
import Govenv.Assurance.GV110 as GV110
import Govenv.Assurance.GV110.Counterexample.MechanicalBump
import Govenv.Assurance.GV111 as GV111
import Govenv.Assurance.GV111.Counterexample.StaleTarget
import Govenv.Assurance.GV112 as GV112
import Govenv.Assurance.GV116
import Govenv.Assurance.GV119 as GV119
import Govenv.Assurance.GV122 as GV122
import Govenv.Assurance.GV122.Counterexample.UngatedCandidate
import Govenv.Assurance.GV123 as GV123
import Govenv.Assurance.GV123.Counterexample.ProspectiveOnly
import Govenv.Assurance.GV123.Counterexample.UnclosableBootstrap
import Govenv.Assurance.GV124 as GV124
import Govenv.Assurance.GV124.Counterexample.SemanticOnlyProgress
import Govenv.Assurance.GV125 as GV125
import Govenv.Assurance.GV125.Counterexample.StackedPullRequestHardGate
import Govenv.Assurance.GV125.Counterexample.BoundaryReownedByLegacyChecks
open import Govenv.Kernel.Assurance
open import Govenv.Kernel.Identifier using (P; GV)
open import Govenv.Kernel.Roadmap using (Roadmap; roadmapOf; _▣; _◇; _✓; _├_)
open import Govenv.Roadmap using (roadmap)

data LegacyCompletion : Nat → Set where
  legacyGV0 : LegacyCompletion 
  legacyGV1 : LegacyCompletion 
  legacyGV2 : LegacyCompletion 
  legacyGV19 : LegacyCompletion 
  legacyGV22 : LegacyCompletion 
  legacyGV45 : LegacyCompletion 
  legacyGV51 : LegacyCompletion 
  legacyGV60 : LegacyCompletion 

assurances : List (AssuranceSpec LegacyCompletion)
assurances =
    assures (inherited legacyGV0)
  ∷ assures (inherited legacyGV1)
  ∷ assures (inherited legacyGV2)
  ∷ assures (statically GV3.evidence)
  ∷ assures (statically GV4.evidence)
  ∷ assures (statically GV5.evidence)
  ∷ assures (statically GV6.evidence)
  ∷ assures (statically GV15.evidence)
  ∷ assures (statically GV16.evidence)
  ∷ assures (statically GV18.evidence)
  ∷ assures (inherited legacyGV19)
  ∷ assures (statically GV20.evidence)
  ∷ assures (statically GV21.evidence)
  ∷ assures (inherited legacyGV22)
  ∷ assures (statically GV44.evidence)
  ∷ assures (inherited legacyGV45)
  ∷ assures (statically GV50.evidence)
  ∷ assures (inherited legacyGV51)
  ∷ assures (statically GV52.evidence)
  ∷ assures (statically GV54.evidence)
  ∷ assures (inherited legacyGV60)
  ∷ assures (statically GV68.evidence)
  ∷ assures (statically GV69.evidence)
  ∷ assures (statically GV70.evidence)
  ∷ assures (statically GV95.evidence)
  ∷ assures (statically GV101.evidence)
  ∷ assures (statically GV108.evidence)
  ∷ assures (statically GV109.evidence)
  ∷ assures (statically GV110.evidence)
  ∷ assures (statically GV111.evidence)
  ∷ assures (statically GV112.evidence)
  ∷ assures (statically GV119.evidence)
  ∷ assures (statically GV122.evidence)
  ∷ assures (statically GV123.evidence)
  ∷ assures (statically GV124.evidence)
  ∷ assures (statically GV125.evidence)
  ∷ []

pendingRoadmap : Roadmap
pendingRoadmap = roadmapOf
  ((P  "assurance-test" ▣) (GV  "assurance-test" ◇))

unassuredDoneRoadmap : Roadmap
unassuredDoneRoadmap = roadmapOf
  ((P  "assurance-test" ▣)
    ((GV  "unassured-done" ✓) ├ (GV  "pending" ◇)))

pendingNeedsNoAssurance :
  completionCoverage assurances pendingRoadmap ≡ true
pendingNeedsNoAssurance = refl

unassuredDoneIsRejected :
  completionCoverage assurances unassuredDoneRoadmap ≡ false
unassuredDoneIsRejected = refl

projectCompletionCovered : completionCoverage assurances roadmap ≡ true
projectCompletionCovered = refl

legacyMigrationIsPending : migrationComplete assurances ≡ false
legacyMigrationIsPending = refl