GV15 assurance

GV15 is statically satisfied by the README roadmap renderer: each phase is a collapsible details/summary block whose only visible children are rendered Membership items, and each item renders as a leaf line.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV15 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using (List)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.String using (String)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Identifier using
  (PhaseId; GovernanceId; descriptionOf)
open import Govenv.Kernel.Roadmap using
  (ItemState; active; BelongsTo; Membership; membership; phaseNode)
open import Govenv.Projection.Readme using
  (_++_; renderPhase; renderItems; renderPhaseId; renderMembership
  ; itemMark; renderGovernanceId; itemSuffix)

phaseExpected :
  {idx : Nat} {description : String} →
  (phaseId : PhaseId idx description) →
  List (Membership phaseId) → String
phaseExpected phaseId items =
  "<details" ++ " open" ++ ">\n" ++
  "<summary>" ++ "▣" ++ " <strong>" ++ renderPhaseId phaseId ++
  " — " ++ descriptionOf phaseId ++ "</strong></summary>\n\n" ++
  renderItems items ++ "\n</details>\n\n"

phaseLevel :
  {idx : Nat} {description : String} →
  (phaseId : PhaseId idx description) →
  (items : List (Membership phaseId)) →
  renderPhase "▣" " open" (phaseNode {state = active} phaseId items) ≡ phaseExpected phaseId items
phaseLevel phaseId items = refl

itemLevel :
  {gvIdx phaseIdx : Nat}
  {gvDescription phaseDescription : String} →
  (governanceId : GovernanceId gvIdx gvDescription) →
  (phaseId : PhaseId phaseIdx phaseDescription) →
  (state : ItemState) →
  (relation : BelongsTo governanceId phaseId) →
  renderMembership (membership governanceId state relation) ≡
    "- " ++ itemMark state ++ " **" ++ renderGovernanceId governanceId ++
    "** " ++ descriptionOf governanceId ++ itemSuffix state ++ "\n"
itemLevel governanceId phaseId state relation = refl

record Proposition : Set where
  constructor satisfied
  field
    phaseProjection :
      {idx : Nat} {description : String} →
      (phaseId : PhaseId idx description) →
      (items : List (Membership phaseId)) →
      renderPhase "▣" " open" (phaseNode {state = active} phaseId items) ≡
        phaseExpected phaseId items
    itemProjection :
      {gvIdx phaseIdx : Nat}
      {gvDescription phaseDescription : String} →
      (governanceId : GovernanceId gvIdx gvDescription) →
      (phaseId : PhaseId phaseIdx phaseDescription) →
      (state : ItemState) →
      (relation : BelongsTo governanceId phaseId) →
      renderMembership (membership governanceId state relation) ≡
        "- " ++ itemMark state ++ " **" ++ renderGovernanceId governanceId ++
        "** " ++ descriptionOf governanceId ++ itemSuffix state ++ "\n"

proposition : Set
proposition = Proposition

evidence : StaticEvidence 
evidence = staticEvidence proposition (satisfied phaseLevel itemLevel)