GV16 assurance

GV16 is statically satisfied because the README projection is defined solely as rendering the governed Govenv.Materialization.Readme state.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV16 where

open import Agda.Builtin.Equality using (_≡_; refl)
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; materialization)
open import Govenv.Projection.Readme using (renderDocument; renderReadme)

record Proposition : Set where
  constructor satisfied
  field
    canonical : Materialization Document
    projection : renderReadme ≡ renderDocument (state materialization)

proposition : Set
proposition = Proposition

evidence : StaticEvidence 16
evidence = staticEvidence proposition (satisfied materialization refl)