GV54 assurance

GV54 is statically satisfied by release-evolution checks that reject removal, definition mutation, phase mutation, completion regression, and terminal-state rewriting.
{-# OPTIONS --safe #-}

module Govenv.Assurance.GV54 where

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.Identifier using (P; GV; GVR; someIdentifier)
open import Govenv.Kernel.Release using
  ( governanceDelta; roadmapSnapshot; snapshotActive; snapshotItem
  ; invalidDelta; governanceRemoved; governanceDefinitionChanged
  ; governancePhaseChanged; itemRegressed; terminalItemChanged )
open import Govenv.Kernel.Roadmap using
  ( Roadmap; done; todo; cancelled; superseded; roadmapOf
  ; _▣; _◇; _↪_; _├_ )

sameTodo : Roadmap
sameTodo = roadmapOf
  ((P 1 "phase" ▣) (GV 1 "same" ◇))

changedDescription : Roadmap
changedDescription = roadmapOf
  ((P 1 "phase" ▣) (GV 1 "new" ◇))

changedPhase : Roadmap
changedPhase = roadmapOf
  ((P 2 "phase" ▣) (GV 1 "same" ◇))

removedItemRoadmap : Roadmap
removedItemRoadmap = roadmapOf
  ((P 1 "phase" ▣) (GV 2 "other" ◇))

currentSuperseded : Roadmap
currentSuperseded = roadmapOf
  ((P 1 "phase" ▣)
    ((GV 1 "same" ↪ GVR 3) ├ (GV 3 "replacement" ◇)))

previousTodo = roadmapSnapshot
  (snapshotActive 1)
  (snapshotItem 1 1 "same" todo ∷ [])

previousDone = roadmapSnapshot
  (snapshotActive 1)
  (snapshotItem 1 1 "same" done ∷ [])

previousCancelled = roadmapSnapshot
  (snapshotActive 1)
  (snapshotItem 1 1 "same" cancelled ∷ [])

previousSuperseded = roadmapSnapshot
  (snapshotActive 1)
  (snapshotItem 1 1 "same" (superseded (GVR 2)) ∷ [])

record GV54Proposition : Set where
  constructor gv54Satisfied
  field
    removalRejected :
      governanceDelta previousTodo [] removedItemRoadmap ≡
      invalidDelta (governanceRemoved 1)
    definitionChangeRejected :
      governanceDelta previousTodo [] changedDescription ≡
      invalidDelta
        (governanceDefinitionChanged (someIdentifier (GV 1 "new")))
    phaseChangeRejected :
      governanceDelta previousTodo [] changedPhase ≡
      invalidDelta
        (governancePhaseChanged (someIdentifier (GV 1 "same")) 1 2)
    completionRegressionRejected :
      governanceDelta previousDone [] sameTodo ≡
      invalidDelta (itemRegressed (someIdentifier (GV 1 "same")))
    cancelledRewriteRejected :
      governanceDelta previousCancelled [] sameTodo ≡
      invalidDelta (terminalItemChanged (someIdentifier (GV 1 "same")))
    supersessionRewriteRejected :
      governanceDelta previousSuperseded [] currentSuperseded ≡
      invalidDelta (terminalItemChanged (someIdentifier (GV 1 "same")))

proposition : Set
proposition = GV54Proposition

evidence : StaticEvidence 54
evidence = staticEvidence proposition
  (gv54Satisfied refl refl refl refl refl refl)