This module assures the current GV116 migration boundaries: the proposition-first, append-only constitutional-history kernel, lifecycle and supersession lineage derived from that history, append-only phase identity with Current derived from non-terminal governance without permitting completed phases to reopen, a validated one-time genesis boundary for legacy cutover, typed revision-bound snapshots that preserve an exact append-only history prefix, a constitutional release-delta classifier over that exact suffix, audit-only snapshot/release materialization boundaries that cannot serialize proof terms, and an authorization-bound activation harness deriving snapshots and release plans only from typed Constitution prefixes. It does not mark GV116 complete: the remaining non-generic step is to freeze Govenv’s real genesis at the final human-authorized roadmap revision and activate these already-assured boundaries.
The kernel deliberately separates decidable structural readiness from
formal evidence. An establishment names only a previously declared
PropositionId; its evidence type is recovered from that
exact historical declaration. A caller therefore cannot establish a
different statement merely by constructing another proposition with the
same numeric identity. A valid governance predecessor may also be
superseded only once, making its successor lineage deterministic. The
transitional roadmap projection consumes legacy Membership
only for identity and structural membership: stored
ItemState and stored successor claims cannot override the
lifecycle, glyph, or lineage derived from Constitution.
Existing human contracts may also enter the migration before their
formal truth is known: propose can append a fresh
Proposition to a still-pending, non-superseded GV, without mutating its
GovernanceId or allowing completed work to regress.
{-# OPTIONS --safe #-}
module Govenv.Assurance.GV116 where
import Govenv.Assurance.GV116.Activation
import Govenv.Assurance.GV116.Counterexample.PhaseReopen
import Govenv.Assurance.GV116.Genesis
import Govenv.Assurance.GV116.MaterializationBoundary
import Govenv.Assurance.GV116.Phase
import Govenv.Assurance.GV116.ReleaseDelta
import Govenv.Assurance.GV116.Snapshot
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([]; _∷_)
open import Agda.Builtin.Maybe using (just; nothing)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Data.Product.Base using (_,_)
open import Data.List.Relation.Unary.All
using (All)
renaming ([] to all[]; _∷_ to _all∷_)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Decidable using (From-yes; from-yes; from-no)
open import Govenv.Kernel.Identifier using (P; GV; GVR)
open import Govenv.Kernel.Constitution
open import Govenv.Kernel.Roadmap using
(Membership; membership; belongs; done; todo; superseded)
open import Govenv.Projection.Roadmap using
(GovernanceView; projectMembership)
valid : (h : History) → (entry : HistoryEntry) →
EntryReady h entry → EntryEvidence h entry → ValidEntry h entry
valid h entry isReady evidence = isReady , evidence
extendWith : {h : History} → ValidHistory h → (entry : HistoryEntry) →
EntryReady h entry → EntryEvidence h entry →
ValidHistory (h ▻ entry)
extendWith {h} validHistory entry isReady evidence =
extend validHistory entry (valid h entry isReady evidence)
notReadyMeansInvalid : (h : History) → (entry : HistoryEntry) →
¬ EntryReady h entry → ¬ ValidEntry h entry
notReadyMeansInvalid h entry notReady (isReady , evidence) = notReady isReady
prop : (n : Nat) → Proposition n
prop n = proposition (Prop n) ⊤
-- Simple establishment becomes an obligation only after exact evidence exists.
p1 : Proposition 1
p1 = prop 1
g1 : GovernanceDeclaration
g1 = governanceDeclaration
(GV 1 "simple establishment")
(P 1 "formal governance model")
(someProposition p1 ∷ [])
e1 : Establishment
e1 = establishment 1
h1 : History
h1 = ε ▻ declare g1 ▻ establish e1
h1-valid : ValidHistory h1
h1-valid =
extendWith
(extendWith
empty
(declare g1)
(from-yes (entryReady? ε (declare g1)))
tt)
(establish e1)
(from-yes (entryReady? (ε ▻ declare g1) (establish e1)))
tt
c1 : Constitution
c1 = constitution h1 h1-valid
p1-is-obligation : Obligation c1 1
p1-is-obligation = from-yes (active? h1 1)
h1-lifecycle : constitutionLifecycle c1 1 ≡ completed
h1-lifecycle = refl
h1-glyph : constitutionGlyph c1 1 ≡ check
h1-glyph = refl
legacyDoneMembership : Membership (P 99 "projection-test")
legacyDoneMembership =
membership (GV 1 "simple establishment") done belongs
legacyTodoMembership : Membership (P 99 "projection-test")
legacyTodoMembership =
membership (GV 1 "simple establishment") todo belongs
storedItemStateCannotOverrideConstitution :
projectMembership c1 legacyDoneMembership ≡
projectMembership c1 legacyTodoMembership
storedItemStateCannotOverrideConstitution = refl
-- Established plus abandoned propositions resolve to the mixed glyph.
p2 : Proposition 2
p2 = prop 2
p3 : Proposition 3
p3 = prop 3
g2 : GovernanceDeclaration
g2 = governanceDeclaration
(GV 2 "mixed resolution")
(P 1 "formal governance model")
(someProposition p2 ∷ someProposition p3 ∷ [])
e2 : Establishment
e2 = establishment 2
h2 : History
h2 = ε ▻ declare g2 ▻ establish e2 ▻ abandon 3
h2-valid : ValidHistory h2
h2-valid =
extendWith
(extendWith
(extendWith
empty
(declare g2)
(from-yes (entryReady? ε (declare g2)))
tt)
(establish e2)
(from-yes (entryReady? (ε ▻ declare g2) (establish e2)))
tt)
(abandon 3)
(from-yes (entryReady? (ε ▻ declare g2 ▻ establish e2) (abandon 3)))
tt
c2 : Constitution
c2 = constitution h2 h2-valid
h2-lifecycle : constitutionLifecycle c2 2 ≡ mixedCompleted
h2-lifecycle = refl
h2-glyph : constitutionGlyph c2 2 ≡ mixed
h2-glyph = refl
-- GV47 reformulates established Prop17 into Prop23 owned by GV68 and
-- establishes the replacement atomically with the supersession.
p17 : Proposition 17
p17 = prop 17
p23 : Proposition 23
p23 = prop 23
g47 : GovernanceDeclaration
g47 = governanceDeclaration
(GV 47 "old contract")
(P 1 "formal governance model")
(someProposition p17 ∷ [])
g68 : GovernanceDeclaration
g68 = governanceDeclaration
(GV 68 "reformulated contract")
(P 1 "formal governance model")
(someProposition p23 ∷ [])
e17 : Establishment
e17 = establishment 17
e23 : Establishment
e23 = establishment 23
s47-68 : Supersession
s47-68 = supersession (GVR 47) (GVR 68)
(e23 ∷ [])
(dispositionOf 17 (reformulated (23 ∷ [])) ∷ [])
h47-68 : History
h47-68 =
ε
▻ declare g47
▻ declare g68
▻ establish e17
▻ supersede s47-68
h47-68-valid : ValidHistory h47-68
h47-68-valid =
extendWith
(extendWith
(extendWith
(extendWith
empty
(declare g47)
(from-yes (entryReady? ε (declare g47)))
tt)
(declare g68)
(from-yes (entryReady? (ε ▻ declare g47) (declare g68)))
tt)
(establish e17)
(from-yes (entryReady? (ε ▻ declare g47 ▻ declare g68) (establish e17)))
tt)
(supersede s47-68)
(from-yes (entryReady? (ε ▻ declare g47 ▻ declare g68 ▻ establish e17) (supersede s47-68)))
(tt all∷ all[])
c47-68 : Constitution
c47-68 = constitution h47-68 h47-68-valid
gv47-lifecycle : constitutionLifecycle c47-68 47 ≡ completed
gv47-lifecycle = refl
gv47-successor : constitutionSuccessor c47-68 47 ≡ just (GVR 68)
gv47-successor = refl
legacyWrongLineage : Membership (P 99 "projection-test")
legacyWrongLineage =
membership (GV 47 "old contract") (superseded (GVR 999)) belongs
legacyPendingLineage : Membership (P 99 "projection-test")
legacyPendingLineage =
membership (GV 47 "old contract") todo belongs
storedSuccessorCannotOverrideConstitution :
projectMembership c47-68 legacyWrongLineage ≡
projectMembership c47-68 legacyPendingLineage
storedSuccessorCannotOverrideConstitution = refl
projectedSuccessorIsConstitutional :
GovernanceView.successor (projectMembership c47-68 legacyWrongLineage) ≡
just (GVR 68)
projectedSuccessorIsConstitutional = refl
gv47-glyph : constitutionGlyph c47-68 47 ≡ check
gv47-glyph = refl
gv68-glyph : constitutionGlyph c47-68 68 ≡ check
gv68-glyph = refl
gv68-has-no-successor : constitutionSuccessor c47-68 68 ≡ nothing
gv68-has-no-successor = refl
s47-68-repeated : Supersession
s47-68-repeated = supersession (GVR 47) (GVR 68) [] []
repeatedSupersessionRejected :
¬ ValidEntry h47-68 (supersede s47-68-repeated)
repeatedSupersessionRejected =
notReadyMeansInvalid
h47-68
(supersede s47-68-repeated)
(from-no (entryReady? h47-68 (supersede s47-68-repeated)))
-- A pending predecessor proposition may be abandoned while its successor
-- introduces independent pending work. Establishing the successor proposition
-- later yields a mixed resolution because the successor owns that disposition.
p41 : Proposition 41
p41 = prop 41
p60 : Proposition 60
p60 = prop 60
g77 : GovernanceDeclaration
g77 = governanceDeclaration
(GV 77 "superseded pending contract")
(P 1 "formal governance model")
(someProposition p41 ∷ [])
g95 : GovernanceDeclaration
g95 = governanceDeclaration
(GV 95 "successor contract")
(P 1 "formal governance model")
(someProposition p60 ∷ [])
s77-95 : Supersession
s77-95 = supersession (GVR 77) (GVR 95) []
(dispositionOf 41 abandoned ∷ [])
h77-95 : History
h77-95 = ε ▻ declare g77 ▻ declare g95 ▻ supersede s77-95
h77-95-valid : ValidHistory h77-95
h77-95-valid =
extendWith
(extendWith
(extendWith
empty
(declare g77)
(from-yes (entryReady? ε (declare g77)))
tt)
(declare g95)
(from-yes (entryReady? (ε ▻ declare g77) (declare g95)))
tt)
(supersede s77-95)
(from-yes (entryReady? (ε ▻ declare g77 ▻ declare g95) (supersede s77-95)))
all[]
c77-95 : Constitution
c77-95 = constitution h77-95 h77-95-valid
gv77-lifecycle : constitutionLifecycle c77-95 77 ≡ abandoned
gv77-lifecycle = refl
gv77-successor : constitutionSuccessor c77-95 77 ≡ just (GVR 95)
gv77-successor = refl
gv77-glyph : constitutionGlyph c77-95 77 ≡ cross
gv77-glyph = refl
gv95-lifecycle : constitutionLifecycle c77-95 95 ≡ pending
gv95-lifecycle = refl
gv95-glyph : constitutionGlyph c77-95 95 ≡ diamond
gv95-glyph = refl
e60 : Establishment
e60 = establishment 60
h95-established : History
h95-established = h77-95 ▻ establish e60
h95-established-valid : ValidHistory h95-established
h95-established-valid =
extendWith
h77-95-valid
(establish e60)
(from-yes (entryReady? h77-95 (establish e60)))
tt
c95-established : Constitution
c95-established = constitution h95-established h95-established-valid
gv95-established-lifecycle :
constitutionLifecycle c95-established 95 ≡ mixedCompleted
gv95-established-lifecycle = refl
gv95-established-glyph : constitutionGlyph c95-established 95 ≡ mixed
gv95-established-glyph = refl
-- Duplicate PropositionId declarations are rejected.
p70a : Proposition 70
p70a = prop 70
p70b : Proposition 70
p70b = prop 70
duplicatePropositionDeclaration : GovernanceDeclaration
duplicatePropositionDeclaration = governanceDeclaration
(GV 70 "duplicate proposition ids")
(P 1 "formal governance model")
(someProposition p70a ∷ someProposition p70b ∷ [])
duplicatePropositionIdsRejected :
¬ ValidEntry ε (declare duplicatePropositionDeclaration)
duplicatePropositionIdsRejected =
notReadyMeansInvalid ε (declare duplicatePropositionDeclaration)
(from-no (entryReady? ε (declare duplicatePropositionDeclaration)))
-- GovernanceId identity is append-only too: an index cannot be redeclared with
-- a different human contract after its first declaration.
g1-redeclared : GovernanceDeclaration
g1-redeclared = governanceDeclaration
(GV 1 "mutated contract")
(P 1 "formal governance model")
(someProposition (prop 101) ∷ [])
governanceRedeclarationRejected :
¬ ValidEntry (ε ▻ declare g1) (declare g1-redeclared)
governanceRedeclarationRejected =
notReadyMeansInvalid
(ε ▻ declare g1)
(declare g1-redeclared)
(from-no (entryReady? (ε ▻ declare g1) (declare g1-redeclared)))
-- Supersession coverage is set-like rather than list-order-sensitive.
p80 : Proposition 80
p80 = prop 80
p81 : Proposition 81
p81 = prop 81
g80 : GovernanceDeclaration
g80 = governanceDeclaration
(GV 80 "two pending propositions")
(P 1 "formal governance model")
(someProposition p80 ∷ someProposition p81 ∷ [])
g81 : GovernanceDeclaration
g81 = governanceDeclaration
(GV 81 "disposition-only successor")
(P 1 "formal governance model")
[]
s80-81-reordered : Supersession
s80-81-reordered = supersession (GVR 80) (GVR 81) []
( dispositionOf 81 abandoned
∷ dispositionOf 80 abandoned
∷ [])
h80-81-reordered : History
h80-81-reordered = ε ▻ declare g80 ▻ declare g81 ▻ supersede s80-81-reordered
h80-81-reordered-valid : ValidHistory h80-81-reordered
h80-81-reordered-valid =
extendWith
(extendWith
(extendWith
empty
(declare g80)
(from-yes (entryReady? ε (declare g80)))
tt)
(declare g81)
(from-yes (entryReady? (ε ▻ declare g80) (declare g81)))
tt)
(supersede s80-81-reordered)
(from-yes (entryReady? (ε ▻ declare g80 ▻ declare g81) (supersede s80-81-reordered)))
all[]
s80-81-duplicate-disposition : Supersession
s80-81-duplicate-disposition = supersession (GVR 80) (GVR 81) []
( dispositionOf 80 abandoned
∷ dispositionOf 80 abandoned
∷ dispositionOf 81 abandoned
∷ [])
duplicateDispositionRejected :
¬ ValidEntry
(ε ▻ declare g80 ▻ declare g81)
(supersede s80-81-duplicate-disposition)
duplicateDispositionRejected =
notReadyMeansInvalid
(ε ▻ declare g80 ▻ declare g81)
(supersede s80-81-duplicate-disposition)
(from-no
(entryReady?
(ε ▻ declare g80 ▻ declare g81)
(supersede s80-81-duplicate-disposition)))
-- Embedded establishments are constitutional establishments too: they must be
-- pending before the cutover, unique, and carry exact declaration evidence.
s47-68-duplicate-establishment : Supersession
s47-68-duplicate-establishment = supersession (GVR 47) (GVR 68)
(e23 ∷ e23 ∷ [])
(dispositionOf 17 (reformulated (23 ∷ [])) ∷ [])
duplicateEmbeddedEstablishmentRejected :
¬ ValidEntry
(ε ▻ declare g47 ▻ declare g68 ▻ establish e17)
(supersede s47-68-duplicate-establishment)
duplicateEmbeddedEstablishmentRejected =
notReadyMeansInvalid
(ε ▻ declare g47 ▻ declare g68 ▻ establish e17)
(supersede s47-68-duplicate-establishment)
(from-no
(entryReady?
(ε ▻ declare g47 ▻ declare g68 ▻ establish e17)
(supersede s47-68-duplicate-establishment)))
h47-68-preestablished : History
h47-68-preestablished =
ε ▻ declare g47 ▻ declare g68 ▻ establish e17 ▻ establish e23
s47-68-reestablish-active : Supersession
s47-68-reestablish-active = supersession (GVR 47) (GVR 68)
(e23 ∷ [])
(dispositionOf 17 (reformulated (23 ∷ [])) ∷ [])
activeEmbeddedEstablishmentRejected :
¬ ValidEntry h47-68-preestablished (supersede s47-68-reestablish-active)
activeEmbeddedEstablishmentRejected =
notReadyMeansInvalid
h47-68-preestablished
(supersede s47-68-reestablish-active)
(from-no
(entryReady?
h47-68-preestablished
(supersede s47-68-reestablish-active)))
-- Reformulation means one-to-many or many-to-many replacement, never
-- disappearance. An empty replacement set is therefore invalid.
s47-68-empty-reformulation : Supersession
s47-68-empty-reformulation = supersession (GVR 47) (GVR 68) []
(dispositionOf 17 (reformulated []) ∷ [])
emptyReformulationRejected :
¬ ValidEntry
(ε ▻ declare g47 ▻ declare g68 ▻ establish e17)
(supersede s47-68-empty-reformulation)
emptyReformulationRejected =
notReadyMeansInvalid
(ε ▻ declare g47 ▻ declare g68 ▻ establish e17)
(supersede s47-68-empty-reformulation)
(from-no
(entryReady?
(ε ▻ declare g47 ▻ declare g68 ▻ establish e17)
(supersede s47-68-empty-reformulation)))
-- Effective supersession requires two existing, distinct governance identities.
selfSupersession : Supersession
selfSupersession = supersession (GVR 1) (GVR 1) []
(dispositionOf 1 preserved ∷ [])
selfSupersessionRejected : ¬ ValidEntry h1 (supersede selfSupersession)
selfSupersessionRejected =
notReadyMeansInvalid h1 (supersede selfSupersession)
(from-no (entryReady? h1 (supersede selfSupersession)))
missingSuccessor : Supersession
missingSuccessor = supersession (GVR 1) (GVR 999) []
(dispositionOf 1 preserved ∷ [])
missingSuccessorRejected : ¬ ValidEntry h1 (supersede missingSuccessor)
missingSuccessorRejected =
notReadyMeansInvalid h1 (supersede missingSuccessor)
(from-no (entryReady? h1 (supersede missingSuccessor)))
-- Evidence is recovered from the proposition declaration, not supplied together
-- with an arbitrary proposition value. Declaring an uninhabited Statement makes
-- establishment impossible even if a caller can construct another Proposition
-- with the same numeric identity and a different Statement.
p90 : Proposition 90
p90 = proposition (Prop 90) ⊥
g90 : GovernanceDeclaration
g90 = governanceDeclaration
(GV 90 "uninhabited proposition")
(P 1 "formal governance model")
(someProposition p90 ∷ [])
h90 : History
h90 = ε ▻ declare g90
e90 : Establishment
e90 = establishment 90
sameIdDifferentStatement : Proposition 90
sameIdDifferentStatement = prop 90
sameIdDifferentEvidence : Evidence sameIdDifferentStatement
sameIdDifferentEvidence = tt
falseEvidenceImpossible : ¬ EntryEvidence h90 (establish e90)
falseEvidenceImpossible evidence = evidence
falseEstablishmentRejected : ¬ ValidEntry h90 (establish e90)
falseEstablishmentRejected (isReady , evidence) = evidence
-- A human governance contract may exist before its formal proposition is known.
-- `propose` adds that proposition later without mutating the GovernanceId.
g120 : GovernanceDeclaration
g120 = governanceDeclaration
(GV 120 "late-bound formal proposition")
(P 1 "formal governance model")
[]
p120 : Proposition 120
p120 = prop 120
proposal120 : PropositionDeclaration
proposal120 = propositionDeclaration (GVR 120) (someProposition p120)
h120-declared : History
h120-declared = ε ▻ declare g120
h120-proposed : History
h120-proposed = h120-declared ▻ propose proposal120
h120-proposed-valid : ValidHistory h120-proposed
h120-proposed-valid =
extendWith
(extendWith
empty
(declare g120)
(from-yes (entryReady? ε (declare g120)))
tt)
(propose proposal120)
(from-yes (entryReady? h120-declared (propose proposal120)))
tt
latePropositionIsPending :
governanceLifecycle h120-proposed 120 ≡ pending
latePropositionIsPending = refl
e120 : Establishment
e120 = establishment 120
h120-established : History
h120-established = h120-proposed ▻ establish e120
h120-established-valid : ValidHistory h120-established
h120-established-valid =
extendWith
h120-proposed-valid
(establish e120)
(from-yes (entryReady? h120-proposed (establish e120)))
tt
latePropositionCanEstablishContract :
governanceLifecycle h120-established 120 ≡ completed
latePropositionCanEstablishContract = refl
-- Proposition identity remains global even when propositions are declared late.
duplicateLateProposalRejected :
¬ ValidEntry h120-proposed (propose proposal120)
duplicateLateProposalRejected =
notReadyMeansInvalid
h120-proposed
(propose proposal120)
(from-no (entryReady? h120-proposed (propose proposal120)))
-- A completed governance contract cannot silently regress by acquiring new work.
p121 : Proposition 121
p121 = prop 121
proposal121 : PropositionDeclaration
proposal121 = propositionDeclaration (GVR 120) (someProposition p121)
proposalAfterCompletionRejected :
¬ ValidEntry h120-established (propose proposal121)
proposalAfterCompletionRejected =
notReadyMeansInvalid
h120-established
(propose proposal121)
(from-no (entryReady? h120-established (propose proposal121)))
-- Superseded governance cannot receive new formal responsibility either.
g130 : GovernanceDeclaration
g130 = governanceDeclaration
(GV 130 "superseded contract")
(P 1 "formal governance model")
[]
g131 : GovernanceDeclaration
g131 = governanceDeclaration
(GV 131 "successor contract")
(P 1 "formal governance model")
[]
s130-131 : Supersession
s130-131 = supersession (GVR 130) (GVR 131) [] []
h130-131 : History
h130-131 = ε ▻ declare g130 ▻ declare g131 ▻ supersede s130-131
h130-131-valid : ValidHistory h130-131
h130-131-valid =
extendWith
(extendWith
(extendWith
empty
(declare g130)
(from-yes (entryReady? ε (declare g130)))
tt)
(declare g131)
(from-yes (entryReady? (ε ▻ declare g130) (declare g131)))
tt)
(supersede s130-131)
(from-yes
(entryReady?
(ε ▻ declare g130 ▻ declare g131)
(supersede s130-131)))
all[]
p130 : Proposition 130
p130 = prop 130
proposal130 : PropositionDeclaration
proposal130 = propositionDeclaration (GVR 130) (someProposition p130)
proposalAfterSupersessionRejected :
¬ ValidEntry h130-131 (propose proposal130)
proposalAfterSupersessionRejected =
notReadyMeansInvalid
h130-131
(propose proposal130)
(from-no (entryReady? h130-131 (propose proposal130)))