GV111 assurance

GV111 makes project direction an explicit governed review instead of deriving a single pending item as human-facing status. The typed construction requires bounded Current/Next summaries, exact Purpose + Roadmap source binding, disposition of both authoritative source dimensions, typed gap disposition, and valid roadmap references. Protocol vigilance is checked against predecessor snapshots by DirectionReviewVigilance; freshness requires both the expected counter transition and fresh explicit review rationale.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV111 where

open import Agda.Builtin.Bool using (false; true)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Nat using (zero; suc)
open import Govenv.DirectionReview using
  ( source; currentSummary; currentSourceCoverage
  ; nextSummary; nextGapCoverage; review )
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.DirectionReview
open import Govenv.Kernel.Protocol using (protocolReviewFresh)
open import Govenv.Kernel.Release using (snapshotRoadmap)
open import Govenv.Materialization.DirectionReviewSnapshot using (snapshot)
open import Govenv.Materialization.Readme using
  (Current; directionCurrent; directionStatus)
open import Govenv.Project using (purpose)
open import Govenv.Roadmap using (roadmap)

record Proposition : Set where
  constructor satisfied
  field
    sourceIsExact :
      DirectionReview.source review ≡
        directionSource purpose (snapshotRoadmap roadmap)
    currentDisposesBothSources :
      Current.coverage (DirectionReview.current review) ≡
        currentSourceCoverage
    nextDisposesPurposeAndCurrentGap :
      Next.coverage (DirectionReview.next review) ≡
        nextGapCoverage
    readmeUsesReviewedDirection :
      directionStatus ≡
        directionCurrent
          (BoundedText.value currentSummary)
          (BoundedText.value nextSummary)
    snapshotIsCanonical :
      snapshot ≡ snapshotDirectionReview review
    mechanicalReaffirmationIsRejected :
      protocolReviewFresh true false false zero (suc zero) ≡ false
    reaffirmedReviewRequiresRationale :
      protocolReviewFresh true false true zero (suc zero) ≡ true
    changedReviewRequiresRationale :
      protocolReviewFresh true true true (suc zero) zero ≡ true
    changedReviewWithoutRationaleIsRejected :
      protocolReviewFresh true true false (suc zero) zero ≡ false

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

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof