GV110 assurance

GV110 keeps Protocol judgment non-constitutional while making review freshness explicitly checkable. Counter transitions remain necessary but are no longer sufficient: every triggered review must also change explicit review evidence, so a contributor cannot satisfy vigilance by mechanically incrementing a counter. The project-purpose snapshot is derived from the canonical purpose, review rationale, and review index.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV110 where

open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.ProjectPurpose using (projectPurposeSnapshot)
open import Govenv.Kernel.Protocol using
  (protocolVigilanceFresh; protocolReviewFresh)
open import Govenv.Materialization using (Materialization)
import Govenv.Materialization.ProjectPurposeSnapshot as PurposeSnapshot
open import Govenv.Project using
  (purpose; purposeReviewRationale; purposeReviewIndex)

record Proposition : Set where
  constructor satisfied
  field
    noTriggerPreserves :
      protocolVigilanceFresh false false   ≡ true
    noTriggerRejectsBump :
      protocolVigilanceFresh false false   ≡ false
    mechanicalBumpIsNotReview :
      protocolReviewFresh true false false   ≡ false
    reaffirmationRequiresEvidence :
      protocolReviewFresh true false true   ≡ true
    unchangedStateRejectsEvidenceNoise :
      protocolReviewFresh false false true   ≡ false
    revisionRequiresEvidence :
      protocolReviewFresh false true true   ≡ true
    revisionWithoutEvidenceIsRejected :
      protocolReviewFresh false true false   ≡ false
    purposeSnapshotIsCanonical :
      Materialization.state PurposeSnapshot.materialization ≡
        projectPurposeSnapshot
          purpose
          purposeReviewRationale
          purposeReviewIndex

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

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof