GV70 assurance

GV70 is statically satisfied by reduction over representative typed roadmap deltas. The assurance covers every governed item-progress class, phase progression, and the SemVer-independent type of governanceDelta.
{-# OPTIONS --safe #-}

module Govenv.Assurance.GV70 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using (List; []; _∷_)
open import Agda.Builtin.Nat using (Nat)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Identifier using (P; GV; GVR; someIdentifier)
open import Govenv.Kernel.Release using
  ( GovernanceDeltaResult; RoadmapSnapshot; governanceDelta
  ; roadmapSnapshot; snapshotAbsent; snapshotActive
  ; snapshotItem; validDelta; governanceDeltaValue; impact
  ; introduced; advanced; completed; cancelledProgress
  ; supersededProgress; phaseIntroduced; phaseUnchanged
  ; phaseAdvanced; roadmapCompleted )
open import Govenv.Kernel.Roadmap using
  ( Roadmap; done; todo; cancelled; superseded; roadmapOf
  ; _■; _▣; _✓; _◇; _×; _↪_; _├_ )

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

currentDone : Roadmap
currentDone = roadmapOf
  ((P 1 "phase" ▣)
    ((GV 1 "same" ✓) ├ (GV 99 "keep-active" ◇)))

currentCancelled : Roadmap
currentCancelled = roadmapOf
  ((P 1 "phase" ▣)
    ((GV 1 "same" ×) ├ (GV 99 "keep-active" ◇)))

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

currentPhase2 : Roadmap
currentPhase2 = roadmapOf
  ((P 2 "phase-2" ▣) (GV 3 "new" ◇))

completeRoadmap : Roadmap
completeRoadmap = roadmapOf
  ((P 1 "phase" ■) (GV 1 "same" ×))

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

previousTodoWithSentinel : RoadmapSnapshot
previousTodoWithSentinel = roadmapSnapshot
  (snapshotActive 1)
  ( snapshotItem 1 1 "same" todo
  ∷ snapshotItem 99 1 "keep-active" todo
  ∷ [] )

previousTwoTodos : RoadmapSnapshot
previousTwoTodos = roadmapSnapshot
  (snapshotActive 1)
  ( snapshotItem 1 1 "same" todo
  ∷ snapshotItem 2 1 "replacement" todo
  ∷ [] )

previousActiveEmpty : RoadmapSnapshot
previousActiveEmpty = roadmapSnapshot (snapshotActive 1) []

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

introducedExpected : GovernanceDeltaResult
introducedExpected = validDelta
  (governanceDeltaValue
    (impact (someIdentifier (GV 1 "same")) todo introduced ∷ [])
    (phaseIntroduced (someIdentifier (P 1 "phase"))))

advancedExpected : GovernanceDeltaResult
advancedExpected = validDelta
  (governanceDeltaValue
    (impact (someIdentifier (GV 1 "same")) todo advanced ∷ [])
    (phaseUnchanged (someIdentifier (P 1 "phase"))))

completedExpected : GovernanceDeltaResult
completedExpected = validDelta
  (governanceDeltaValue
    (impact (someIdentifier (GV 1 "same")) done completed ∷ [])
    (phaseUnchanged (someIdentifier (P 1 "phase"))))

cancelledExpected : GovernanceDeltaResult
cancelledExpected = validDelta
  (governanceDeltaValue
    (impact (someIdentifier (GV 1 "same")) cancelled cancelledProgress ∷ [])
    (phaseUnchanged (someIdentifier (P 1 "phase"))))

supersededExpected : GovernanceDeltaResult
supersededExpected = validDelta
  (governanceDeltaValue
    ( impact (someIdentifier (GV 1 "same"))
        (superseded (GVR 2)) (supersededProgress (GVR 2))
    ∷ [] )
    (phaseUnchanged (someIdentifier (P 1 "phase"))))

phaseAdvancedExpected : GovernanceDeltaResult
phaseAdvancedExpected = validDelta
  (governanceDeltaValue
    (impact (someIdentifier (GV 3 "new")) todo introduced ∷ [])
    (phaseAdvanced
      (someIdentifier (P 1 ""))
      (someIdentifier (P 2 "phase-2"))))

roadmapCompletedExpected : GovernanceDeltaResult
roadmapCompletedExpected = validDelta
  (governanceDeltaValue []
    (roadmapCompleted (someIdentifier (P 1 ""))))

record GV70Proposition : Set where
  constructor gv70Satisfied
  field
    introducedClassified :
      governanceDelta (roadmapSnapshot snapshotAbsent []) [] currentTodo ≡
      introducedExpected
    advancedClassified :
      governanceDelta previousTodo (1 ∷ []) currentTodo ≡ advancedExpected
    completedClassified :
      governanceDelta previousTodoWithSentinel [] currentDone ≡ completedExpected
    cancelledClassified :
      governanceDelta previousTodoWithSentinel [] currentCancelled ≡ cancelledExpected
    supersededClassified :
      governanceDelta previousTwoTodos [] currentSuperseded ≡
      supersededExpected
    phaseAdvanceClassified :
      governanceDelta previousActiveEmpty [] currentPhase2 ≡
      phaseAdvancedExpected
    roadmapCompletionClassified :
      governanceDelta previousCancelled [] completeRoadmap ≡
      roadmapCompletedExpected
    semverIndependent :
      RoadmapSnapshot → List Nat → Roadmap → GovernanceDeltaResult

proposition : Set
proposition = GV70Proposition

evidence : StaticEvidence 70
evidence = staticEvidence proposition
  (gv70Satisfied refl refl refl refl refl refl refl governanceDelta)