GV109 assurance

GV109 makes Govenv.Project.purpose the single canonical public project statement. The same value is projected into the README hero and the GitHub repository description, and its governed character limit is the GitHub description limit. Website and topics remain canonical project metadata with target-specific read-back verification.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV109 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
import Govenv.Materialization.Github.Repository.Description as Description
import Govenv.Materialization.Github.Repository.Topics as Topics
import Govenv.Materialization.Github.Repository.Website as Website
import Govenv.Materialization.Readme as Readme
open import Govenv.Materialization.Readme using
  (Document; Block; comment; heading; paragraph; centered; strong)
open import Govenv.Project using
  (purpose; purposeCharacterLimit; website; topics)
open import Govenv.Projection.Github.Repository.Description using
  (renderDescription)

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

record Proposition : Set where
  constructor satisfied
  field
    publicPurposeUsesGithubLimit :
      purposeCharacterLimit ≡ 
    githubDescriptionIsPurpose :
      renderDescription ≡ purpose
    readmeHeroIsPurpose :
      readmePurpose (Materialization.state Readme.materialization) ≡ just purpose
    websiteRemainsCanonical :
      Materialization.state Website.materialization ≡ website
    topicsRemainCanonical :
      Materialization.state Topics.materialization ≡ topics
    descriptionKeepsReadBack :
      Materialization.verification Description.materialization ≡
        descriptionReadBackEquality
    websiteKeepsReadBack :
      Materialization.verification Website.materialization ≡
        websiteReadBackEquality
    topicsKeepReadBack :
      Materialization.verification Topics.materialization ≡
        topicsReadBackSetEquality

proof : Proposition
proof = satisfied refl refl refl refl refl refl refl refl

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof