GV101 assurance

GV101 is statically satisfied by the exhaustive concern taxonomy in Govenv.Governance: constitutional subjects classify as Governance, contributor/agent process classifies as Protocol, and the irreducible boundary contains only observation, application, and verification operations.

The boundary therefore has no constructor through which an adapter can create semantic authority. This assurance concerns semantic authority classes only; concrete declaration classification remains GV98.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV101 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Govenv.Governance using
  ( BoundaryOperation; observe; apply; verify
  ; Concern; constitutional; process; boundary
  ; ConstitutionalSubject
  ; repositoryState; repositoryTransition; persistentEffect
  ; authorization; semanticOutput
  ; ProcessSubject; contributorProcess; agentProcess
  ; Domain; governanceDomain; protocolDomain; effectBoundaryDomain
  ; domainOf )
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)

record Proposition : Set where
  constructor satisfied
  field
    stateIsGovernance :
      domainOf (constitutional repositoryState) ≡ governanceDomain
    transitionIsGovernance :
      domainOf (constitutional repositoryTransition) ≡ governanceDomain
    effectPolicyIsGovernance :
      domainOf (constitutional persistentEffect) ≡ governanceDomain
    authorizationIsGovernance :
      domainOf (constitutional authorization) ≡ governanceDomain
    outputIsGovernance :
      domainOf (constitutional semanticOutput) ≡ governanceDomain
    contributorProcessIsProtocol :
      domainOf (process contributorProcess) ≡ protocolDomain
    agentProcessIsProtocol :
      domainOf (process agentProcess) ≡ protocolDomain
    observationIsBoundary :
      domainOf (boundary observe) ≡ effectBoundaryDomain
    applicationIsBoundary :
      domainOf (boundary apply) ≡ effectBoundaryDomain
    verificationIsBoundary :
      domainOf (boundary verify) ≡ effectBoundaryDomain

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

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof