Prove that EPOCH not depends on expired dreps #941

carlostome · 2025-10-03T11:15:35Z

Description

First step towards addressing #929.

Blocked by input-output-hk/agda-sets#16

~~There are a couple of postulates at the beginning of the file that should be taken as assumptions of the EpochStructure type (discuss in meeting)~~

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

williamdemeo

Looks great! Just some (mostly minor) comments you might find helpful.

williamdemeo · 2025-10-22T02:25:37Z

src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda

+  filter-⇒ : (P⇒Q : U.Universal (P U.⇒ Q)) → filter sp-P (filter sp-Q X) ≡ᵉ filter sp-P X
+  filter-⇒ P⇒Q = filter-⇒-⊆ , filter-⇒-⊇
+    where
+      filter-⇒-⊆ : filter sp-P (filter sp-Q X) ⊆ filter sp-P X
+      filter-⇒-⊆ p with from ∈-filter p
+      ... | (q , p) with from ∈-filter p
+      ... | (_ , p) = to ∈-filter (q , p)
+
+      filter-⇒-⊇ : filter sp-P X ⊆ filter sp-P (filter sp-Q X)
+      filter-⇒-⊇ p with from ∈-filter p
+      ... | (q , p) = to ∈-filter (q , (to ∈-filter (P⇒Q _ q , p)))
+
+module _ {P : A → Type} {sp-P : specProperty P} {Q : B → Type} {sp-Q : specProperty Q} where
+
+  import Relation.Unary as U
+
+  module _ {f : A → B} (Qf⇒P : U.Universal ((Q ∘ f) U.⇒ P)) where
+
+    filter-map : filter sp-Q (map f X) ≡ᵉ filter sp-Q (map f (filter sp-P X))
+    filter-map = filter-map-⊆ , filter-map-⊇


I love these theorems and the straight-forward way you prove them---nice work! ...although I'm wondering why the function f and the premise of the filter-map theorem are pulled out as module parameters instead of just making them part of the statement (type signature) of the filter-map theorem.

williamdemeo · 2025-10-22T02:48:52Z

src-lib-exts/stdlib-meta/Reflection.agda

 open import Data.Bool using (if_then_else_)
 open import Data.Nat using (_≤ᵇ_)
 open import Data.List using (map)
 open import Class.Monad hiding (Monad-TC)
 open import Class.MonadTC
  hiding (extendContext)
 open import Class.MonadError
  using (MonadError; MonadError-TC)
 open import Class.Show
 open import Meta.Prelude
 open import Meta.Init public
  renaming (TC to TCI)
-  hiding (Monad-TC; MonadError-TC; toℕ)
+  hiding (Monad-TC; MonadError-TC)
 open import Reflection using (TC; extendContext)

 open MonadTC ⦃...⦄
 open MonadError ⦃...⦄ using (error; catch)


Suggested change

open import Data.Nat using (_≤ᵇ_)

open import Data.List using (map)

open import Class.Monad hiding (Monad-TC)

open import Class.MonadTC

hiding (extendContext)

open import Class.MonadError

using (MonadError; MonadError-TC)

open import Class.Show

open import Meta.Prelude

open import Meta.Init public

renaming (TC to TCI)

hiding (Monad-TC; MonadError-TC)

open import Reflection using (TC; extendContext)

open MonadTC ⦃...⦄

Apparently, the following lines can be omitted:

open import Data.Bool using (if_then_else_)

and

open MonadError ⦃...⦄ using (error; catch)

src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda

williamdemeo · 2025-10-22T04:02:47Z

src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md

+      import Relation.Unary as U
+      P⇒Q : U.Universal ((λ ((_ , e') : Credential × Epoch)  → sucᵉ e ≤ sucᵉ e') U.⇒ (λ (_ , e') → e ≤ e'))


Suggested change

import Relation.Unary as U

P⇒Q : U.Universal ((λ ((_ , e') : Credential × Epoch) → sucᵉ e ≤ sucᵉ e') U.⇒ (λ (_ , e') → e ≤ e'))

P⇒Q : Π[ (λ ((_ , e') : Credential × Epoch) → sucᵉ e ≤ sucᵉ e') ⇒ (λ (_ , e') → e ≤ e') ]

williamdemeo · 2025-10-22T04:05:43Z

src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda

+      import Relation.Unary as U
+      module esp = HasPreorder (EpochStructure.preoEpoch epochStructure)
+      P⇒Q : U.Universal ((λ ((_ , e') : Credential × Epoch)  → sucᵉ e ≤ e') U.⇒ (λ (_ , e') → e ≤ e'))


Suggested change

import Relation.Unary as U

module esp = HasPreorder (EpochStructure.preoEpoch epochStructure)

P⇒Q : U.Universal ((λ ((_ , e') : Credential × Epoch) → sucᵉ e ≤ e') U.⇒ (λ (_ , e') → e ≤ e'))

module esp = HasPreorder (EpochStructure.preoEpoch epochStructure)

P⇒Q : Π[ (λ ((_ , e') : Credential × Epoch) → sucᵉ e ≤ e') ⇒ (λ (_ , e') → e ≤ e') ]

williamdemeo · 2025-10-22T04:45:54Z

src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md

+  cong
+    : ∀ {rSt rSt' : RatifyState} (rSt≡rSt' : rSt ≡ rSt') {govSt govSt' : GovState} (govSt≡govSt' : govSt ≡ govSt') {rSt'' rSt''' : RatifyState}
+       → Γ  ⊢ rSt  ⇀⦇ govSt  ,RATIFIES⦈ rSt''
+       → Γ' ⊢ rSt' ⇀⦇ govSt' ,RATIFIES⦈ rSt'''
+       → rSt'' ≡ rSt'''
+  cong refl refl (BS-base Id-nop) (BS-base Id-nop) = refl
+  cong refl refl (BS-ind {sig = a} p ps) (BS-ind {sig = a'} q qs)
+    with RATIFY.cong Γ≈Γ' {a = a} {a' = a'} refl p q
+  ... | refl = cong refl refl ps  qs


I'm a bit surprised RATIFIES-deterministic isn't used here... I suppose because the gammas are not identical. 🤔

Also, I wonder if some of the cong lemmas should be factored out into their respective Properties modules; e.g., the congs for RATIFY and RATIFIES could go somewhere under Ratify/Properties/.

src/Ledger/Conway/Specification/Epoch.lagda.md

williamdemeo · 2025-10-22T04:55:53Z

src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md

@@ -0,0 +1,569 @@
+{-# OPTIONS --safe #-}


Don't you want to make this new file an .lagda.md file?

carlostome · 2025-10-23T14:11:34Z

Blocked by #964

williamdemeo

Awesome. Nice work!! ...before you merge, would you mind converting your new ExpiredDReps.agda file to .lagda.md? Also, while it's fresh in your mind, please add some documentation that states the purpose of the module and explains the property you're proving. 🙏🏼

* Update ExpiredDReps.lagda.md

WhatisRT · 2025-10-30T13:27:36Z

src/Ledger/Conway/Specification/Enact/Properties/Computational.lagda.md


+module _ {Γ : EnactEnv} {eSt : EnactState} {ga : GovAction} where
+
+  -- TODO: Make this follow from computationalness or viceversa


I just happened to see this PR, we actually have a lemma for this already: computational⇒rightUnique in Interface.ComputationalRelation.

carlostome force-pushed the bisimulation-expired-dreps branch from 185e3ef to c242176 Compare October 14, 2025 13:05

carlostome changed the title ~~WIP: prove that EPOCH not depends on expired dreps~~ Prove that EPOCH not depends on expired dreps Oct 14, 2025

carlostome force-pushed the bisimulation-expired-dreps branch 4 times, most recently from 850ff61 to 6c43c81 Compare October 16, 2025 07:49

carlostome marked this pull request as ready for review October 16, 2025 07:49

carlostome force-pushed the bisimulation-expired-dreps branch 2 times, most recently from 6c43c81 to d590f39 Compare October 17, 2025 12:03

carlostome mentioned this pull request Oct 20, 2025

Improve Ledger.Core.Specification.Epoch #956

Open

carlostome added 9 commits October 20, 2025 17:53

Proof that EPOCH not depends on expired dreps

251fd8a

trigger hydra

9405c28

Fix broken computational EPOCH module

f0f68e5

Fix GovDepsMatch

4425f04

Remove postulates; import module from Epoch.Properties

d9265a3

Add temporary overlay to overwrite agda-sets

7f56f45

use opaque to improve tc time

45cb060

Fix tc error

cb6e546

Implement agda-sets properties locally

9b55dfe

carlostome force-pushed the bisimulation-expired-dreps branch from 5b54a15 to 9b55dfe Compare October 20, 2025 15:53

Fix typechecking

3c20f8f

carlostome requested a review from williamdemeo October 21, 2025 11:48

williamdemeo requested changes Oct 22, 2025

View reviewed changes

williamdemeo mentioned this pull request Oct 22, 2025

Move Carlos's new ledger type relations to their respective Properties files #963

Open

carlostome mentioned this pull request Oct 23, 2025

Refactor EPOCH into more conceptually related modules #964

Merged

4 tasks

carlostome added 3 commits October 28, 2025 11:59

Merge branch 'master' into bisimulation-expired-dreps

5c7ef72

Incorporate William's suggestions

77500fc

Fill leftover goal

0b21e85

carlostome requested a review from williamdemeo October 28, 2025 14:32

carlostome mentioned this pull request Oct 28, 2025

Export equivalence relation for conformance testing #968

Open

williamdemeo approved these changes Oct 29, 2025

View reviewed changes

Make literate agda file; add explanation

128558d

carlostome merged commit e8eac02 into master Oct 29, 2025
12 of 14 checks passed

carlostome deleted the bisimulation-expired-dreps branch October 29, 2025 14:10

carlostome added a commit that referenced this pull request Oct 30, 2025

Follow up to #941 (#969)

dccc0ce

* Update ExpiredDReps.lagda.md

WhatisRT reviewed Oct 30, 2025

View reviewed changes

		import Relation.Unary as U
		P⇒Q : U.Universal ((λ ((_ , e') : Credential × Epoch) → sucᵉ e ≤ sucᵉ e') U.⇒ (λ (_ , e') → e ≤ e'))

	import Relation.Unary as U
	P⇒Q : U.Universal ((λ ((_ , e') : Credential × Epoch) → sucᵉ e ≤ sucᵉ e') U.⇒ (λ (_ , e') → e ≤ e'))
	P⇒Q : Π[ (λ ((_ , e') : Credential × Epoch) → sucᵉ e ≤ sucᵉ e') ⇒ (λ (_ , e') → e ≤ e') ]


		module _ {Γ : EnactEnv} {eSt : EnactState} {ga : GovAction} where

		-- TODO: Make this follow from computationalness or viceversa

Prove that EPOCH not depends on expired dreps #941

Prove that EPOCH not depends on expired dreps #941

Uh oh!

Conversation

carlostome commented Oct 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Checklist

Uh oh!

williamdemeo left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

carlostome commented Oct 23, 2025

Uh oh!

williamdemeo left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

carlostome commented Oct 3, 2025 •

edited

Loading