GV95 assurance

GV95 is statically backed by the typed release materialization model: the canonical changelog keeps the exact frozen ReleaseEntry, while the GitHub Release projects the same governed ReleaseDocument and requires githubReleaseBodySectionEquality. The external effect path was additionally exercised successfully by release v0.2.6 in Materialize run 35631873521, where published-release materialization and exact read-back both succeeded.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV95 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([])
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Identifier using (P; GV; someIdentifier)
open import Govenv.Kernel.Release using
  (GovernanceDelta; governanceDeltaValue; phaseUnchanged)
open import Govenv.Kernel.Roadmap using (Roadmap; roadmapOf; _▣; _◇)
open import Govenv.Materialization using
  (Materialization; repositoryFile; trackedEquality; githubReleaseBodySectionEquality)
open import Govenv.Materialization.ReleaseGovernance using
  ( CandidateBoundary; candidateBoundary
  ; ChangelogDocument; changelogDocument; ChangelogCurrent; frozenCandidate
  ; ReleaseDocument; ReleaseEntry; releaseEntry
  ; document; changelog; githubRelease )

sampleRoadmap : Roadmap
sampleRoadmap = roadmapOf ((P  "phase" ▣) (GV  "pending" ◇))

sampleDelta : GovernanceDelta
sampleDelta = governanceDeltaValue [] (phaseUnchanged (someIdentifier (P  "phase")))

sampleDocument : ReleaseDocument
sampleDocument = document "base" "head" sampleRoadmap sampleDelta

sampleEntry : ReleaseEntry
sampleEntry = releaseEntry sampleDocument []

sampleBoundary : CandidateBoundary
sampleBoundary = candidateBoundary "0.0.0" "## [0.0.0]" "v0.0.0" "authorized"

sampleChangelog = changelog (frozenCandidate sampleBoundary sampleEntry) []

sampleRelease = githubRelease "v0.0.0" "base" "head" sampleRoadmap sampleDelta

record Proposition : Set where
  constructor satisfied
  field
    canonicalChangelogTarget :
      Materialization.target sampleChangelog ≡ repositoryFile "CHANGELOG.md"
    frozenEntryPreserved :
      ChangelogDocument.current (Materialization.state sampleChangelog) ≡
        frozenCandidate sampleBoundary sampleEntry
    canonicalChangelogUsesTrackedEquality :
      Materialization.verification sampleChangelog ≡ trackedEquality
    publishedDocumentPreserved :
      Materialization.state sampleRelease ≡ sampleDocument
    publishedReleaseUsesReadBackEquality :
      Materialization.verification sampleRelease ≡ githubReleaseBodySectionEquality

proof : Proposition
proof = satisfied refl refl refl refl refl

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof