GV50 assurance

GV50 is statically satisfied by structural BelongsTo evidence over generic typed identifiers and by construction of a declarative roadmap tree through the public DSL.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV50 where

open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Identifier using (P; GV)
open import Govenv.Kernel.Roadmap using
  ( BelongsTo; belongs; Roadmap
  ; roadmapOf; _■; _▣; _□; _◇; _×; _╟_ )

syntheticRoadmap : Roadmap
syntheticRoadmap = roadmapOf (
    ((P 0 "assurance-finished" ■) (GV 900 "closed" ×))
  ╟ ((P 1 "assurance-active" ▣) (GV 901 "active" ◇))
  ╟ ((P 2 "assurance-future" □) (GV 902 "future" ◇)))

record Proposition : Set where
  constructor satisfied
  field
    relation : BelongsTo (GV 50 "assurance-governance") (P 1 "assurance-phase")
    declarativeRoadmap : Roadmap

proof : Proposition
proof = satisfied belongs syntheticRoadmap

evidence : StaticEvidence 50
evidence = staticEvidence Proposition proof