GV21 assurance

GV21 remains statically satisfied after its supersession by GV109 because the repository-facing description target and README project statement both consume the canonical Govenv.Project.purpose value directly.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV21 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([]; _∷_)
open import Agda.Builtin.Maybe using (Maybe; just; nothing)
open import Agda.Builtin.String using (String)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Materialization using (Materialization)
open Materialization
open import Govenv.Materialization.Readme using
  (Document; Block; comment; heading; paragraph; centered; strong; materialization)
import Govenv.Materialization.Github.Repository.Description as GithubDescription
open import Govenv.Project using (purpose)
open import Govenv.Projection.Github.Repository.Description using (renderDescription)

readmeDescription : Document → Maybe String
readmeDescription
  (comment _ ∷ heading _ _ _ ∷ paragraph centered (strong value ∷ []) ∷ _) =
    just value
readmeDescription _ = nothing

record Proposition : Set where
  constructor satisfied
  field
    githubProjection : renderDescription ≡ purpose
    readmeProjection : readmeDescription (state materialization) ≡ just purpose

proposition : Set
proposition = Proposition

evidence : StaticEvidence 21
evidence = staticEvidence proposition (satisfied refl refl)