From 251fd8a1480b8c6024682d7da92981f32d3568bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Fri, 3 Oct 2025 13:13:54 +0200 Subject: [PATCH 01/13] Proof that EPOCH not depends on expired dreps --- .../Enact/Properties/Computational.agda | 15 + .../Conway/Specification/Epoch.lagda.md | 250 ++++---- .../Epoch/Properties/ExpiredDReps.agda | 560 ++++++++++++++++++ src/Ledger/Conway/Specification/Ratify.lagda | 247 ++++---- 4 files changed, 833 insertions(+), 239 deletions(-) create mode 100644 src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda diff --git a/src/Ledger/Conway/Specification/Enact/Properties/Computational.agda b/src/Ledger/Conway/Specification/Enact/Properties/Computational.agda index be14f0eab7..67d1f50dad 100644 --- a/src/Ledger/Conway/Specification/Enact/Properties/Computational.agda +++ b/src/Ledger/Conway/Specification/Enact/Properties/Computational.agda @@ -13,6 +13,21 @@ open EnactState open Computational ⦃...⦄ +module _ {Γ : EnactEnv} {eSt : EnactState} {ga : GovAction} where + + -- TODO: Make this follow from computationalness or viceversa + ENACT-deterministic : ∀ {eSt' eSt''} + → Γ ⊢ eSt ⇀⦇ ga ,ENACT⦈ eSt' + → Γ ⊢ eSt ⇀⦇ ga ,ENACT⦈ eSt'' + → eSt' ≡ eSt'' + ENACT-deterministic Enact-NoConf Enact-NoConf = refl + ENACT-deterministic (Enact-UpdComm _) (Enact-UpdComm _) = refl + ENACT-deterministic Enact-NewConst Enact-NewConst = refl + ENACT-deterministic Enact-HF Enact-HF = refl + ENACT-deterministic Enact-PParams Enact-PParams = refl + ENACT-deterministic (Enact-Wdrl _) (Enact-Wdrl _) = refl + ENACT-deterministic Enact-Info Enact-Info = refl + instance Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_ String Computational-ENACT .computeProof Γᵉ s = diff --git a/src/Ledger/Conway/Specification/Epoch.lagda.md b/src/Ledger/Conway/Specification/Epoch.lagda.md index 6a051b984a..1c3c6ebf71 100644 --- a/src/Ledger/Conway/Specification/Epoch.lagda.md +++ b/src/Ledger/Conway/Specification/Epoch.lagda.md @@ -17,6 +17,7 @@ import Data.Integer as ℤ open import Data.Integer.Properties using (module ≤-Reasoning; +-mono-≤; neg-mono-≤; +-identityˡ) renaming (nonNegative⁻¹ to nonNegative⁻¹ℤ) open import Data.Nat.GeneralisedArithmetic using (iterate) +open import Data.Maybe using (fromMaybe) open import Data.Rational using (ℚ; floor; _*_; _÷_; _/_; _⊓_; _≟_; ≢-nonZero) open import Data.Rational.Literals using (number; fromℤ) open import Data.Rational.Properties using (nonNegative⁻¹; pos⇒nonNeg; ⊓-glb) @@ -88,6 +89,9 @@ instance HasDeposits-EpochState : HasDeposits EpochState HasDeposits-EpochState .DepositsOf = DepositsOf ∘ LStateOf + HasDReps-EpochState : HasDReps EpochState + HasDReps-EpochState .DRepsOf = DRepsOf ∘ CertStateOf ∘ LStateOf + HasTreasury-EpochState : HasTreasury EpochState HasTreasury-EpochState .TreasuryOf = Acnt.treasury ∘ EpochState.acnt @@ -445,46 +449,47 @@ each governance action, maps its `returnAddr` (as a staking credential) to the deposit. ```agda - calculateVDelegDelegatedStake - : Epoch - → UTxOState - → GovState - → GState - → DState - → VDeleg ⇀ Coin - calculateVDelegDelegatedStake currentEpoch utxoSt govSt gState dState - = aggregate₊ (((activeVoteDelegs ˢ) ⁻¹ʳ - ∘ʳ (stakePerCredential ∪⁺ stakeFromGADeposits govSt utxoSt) ˢ) ᶠˢ) - where - open UTxOState utxoSt - open DState dState - open GState gState +module VDelegDelegatedStake + (currentEpoch : Epoch) + (utxoSt : UTxOState) + (govSt : GovState) + (gState : GState) + (dState : DState) + where - -- active DReps - activeDReps : ℙ Credential - activeDReps = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) dreps) + open UTxOState utxoSt + open DState dState + open GState gState - -- active vote delegations - activeVoteDelegs : VoteDelegs - activeVoteDelegs = voteDelegs ∣^ ((mapˢ vDelegCredential activeDReps) - ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵) + -- active DReps + activeDReps : ℙ Credential + activeDReps = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) dreps) - -- stake per delegated credential - stakePerCredential : Stake - stakePerCredential = mapFromFun (λ c → cbalance (utxo ∣^' λ txout → getStakeCred txout ≡ just c)) - (dom activeVoteDelegs) + -- active vote delegations + activeVDelegs : ℙ VDeleg + activeVDelegs = mapˢ vDelegCredential activeDReps ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵ -``` + -- compute the stake for a credential + stakePerCredential : Credential → Coin + stakePerCredential c = cbalance (utxo ∣^' λ txout → getStakeCred txout ≡ just c) + + fromMaybe 0 (lookupᵐ? (stakeFromGADeposits govSt utxoSt) c) + calculate : VDeleg ⇀ Coin + calculate = mapFromFun (λ vd → ∑ˢ[ c ← voteDelegs ⁻¹ vd ] (stakePerCredential c)) + activeVDelegs +``` + ```agda calculatePoolDelegatedStakeForVoting : Snapshot → UTxOState → GovState - → GState - → DState → KeyHash ⇀ Coin - calculatePoolDelegatedStakeForVoting ss utxoSt govSt gState dState + calculatePoolDelegatedStakeForVoting ss utxoSt govSt = calculatePoolDelegatedStake ss ∪⁺ (stakeFromDeposits ∣ dom (PoolsOf ss)) where stakeFromDeposits : KeyHash ⇀ Coin @@ -515,17 +520,17 @@ governance actions. `SPO`{.AgdaInductiveConstructor}s as well. ```agda - mkStakeDistrs - : Snapshot - → Epoch - → UTxOState - → GovState - → GState - → DState - → StakeDistrs - mkStakeDistrs ss currentEpoch utxoSt govSt gState dState = - ⟦ calculateVDelegDelegatedStake currentEpoch utxoSt govSt gState dState - , calculatePoolDelegatedStakeForVoting ss utxoSt govSt gState dState ⟧ +mkStakeDistrs + : Snapshot + → Epoch + → UTxOState + → GovState + → GState + → DState + → StakeDistrs +mkStakeDistrs ss currentEpoch utxoSt govSt gState dState = + ⟦ VDelegDelegatedStake.calculate currentEpoch utxoSt govSt gState dState + , calculatePoolDelegatedStakeForVoting ss utxoSt govSt ⟧ ``` ```agda let - EPOCHUpdates es govSt' dState'' pState' gState' utxoSt' acnt'' = - EPOCH-updates fut ls dState' acnt' + eu0@(EPOCHUpdates0 es govSt' _ pState' gState' utxoSt' _) = EPOCHUpdates0.updates fut ls + EPOCHUpdates dState'' acnt'' = EPOCHUpdates.updates eu0 ls dState' acnt' stakeDistrs : StakeDistrs stakeDistrs = mkStakeDistrs (Snapshots.mark ss') e utxoSt' diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda new file mode 100644 index 0000000000..fdbb2e8477 --- /dev/null +++ b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda @@ -0,0 +1,560 @@ +-- {-# OPTIONS --without-K #-} +open import Ledger.Conway.Specification.Transaction +open import Ledger.Conway.Specification.Abstract + +module Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps + (txs : _) (open TransactionStructure txs) + (abs : AbstractFunctions txs) (open AbstractFunctions abs) + where + +open import Ledger.Core.Specification.Epoch +open import Ledger.Conway.Specification.Certs govStructure +open import Ledger.Conway.Specification.Epoch txs abs +open import Ledger.Prelude hiding (cong) +import Ledger.Prelude as P +import Relation.Binary.Core as B +open import Relation.Binary.Definitions +open import Ledger.Conway.Specification.Ratify txs +open import Ledger.Conway.Specification.Enact govStructure +open import Ledger.Conway.Specification.Enact.Properties.Computational govStructure +open import Ledger.Conway.Specification.Ledger txs abs +open import Ledger.Conway.Specification.Rewards txs abs +open import Ledger.Conway.Specification.PoolReap txs abs +open import Ledger.Conway.Specification.Utxo txs abs +open import Ledger.Conway.Specification.Gov txs +open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote) +open import Axiom.Set.Properties th +open import Relation.Binary.PropositionalEquality hiding (cong) + +postulate + e e - then nothing -- credential has expired - else case lookupᵐ? ccHotKeys c of + getCCHotCred : Credential × Epoch → Maybe Credential + getCCHotCred (c , e) = + if currentEpoch > e + then nothing -- credential has expired + else case lookupᵐ? ccHotKeys c of \end{code} \begin{code}[hide] λ where \end{code} \begin{code} - (just (just c')) → just c' - _ → nothing -- hot key not registered or resigned + (just (just c')) → just c' + _ → nothing -- hot key not registered or resigned - actualVote : Credential → Epoch → Vote - actualVote c e = case getCCHotCred (c , e) of + actualVote : Credential → Epoch → Vote + actualVote c e = case getCCHotCred (c , e) of \end{code} \begin{code}[hide] - λ where + λ where \end{code} \begin{code} - (just c') → maybe id Vote.no (lookupᵐ? castVotes c') - _ → Vote.abstain + (just c') → maybe id Vote.no (lookupᵐ? castVotes c') + _ → Vote.abstain - actualVotes : Credential ⇀ Vote - actualVotes = case proj₁ cc of + actualVotes : Credential ⇀ Vote + actualVotes = case proj₁ cc of \end{code} \begin{code}[hide] - λ where + λ where \end{code} \begin{code} - nothing → ∅ - (just (m , _)) → if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ)) - then mapWithKey actualVote m - else constMap (dom m) Vote.no + nothing → ∅ + (just (m , _)) → if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ)) + then mapWithKey actualVote m + else constMap (dom m) Vote.no + + mT : Maybe ℚ + mT = threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action CC - mT : Maybe ℚ - mT = threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action CC + t : ℚ + t = maybe id 0ℚ mT - t : ℚ - t = maybe id 0ℚ mT + stakeDistr : Credential ⇀ Coin + stakeDistr = constMap (dom actualVotes) 1 - stakeDistr : Credential ⇀ Coin - stakeDistr = constMap (dom actualVotes) 1 + acceptedStake totalStake : Coin + acceptedStake = ∑[ x ← stakeDistr ∣ actualVotes ⁻¹ Vote.yes ] x + totalStake = ∑[ x ← stakeDistr ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x - acceptedStake totalStake : Coin - acceptedStake = ∑[ x ← stakeDistr ∣ actualVotes ⁻¹ Vote.yes ] x - totalStake = ∑[ x ← stakeDistr ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x + accepted : Type + accepted = (acceptedStake /₀ totalStake) ≥ t + × (maybe (λ (m , _) → lengthˢ m) 0 (proj₁ cc) ≥ ccMinSize ⊎ Is-nothing mT) + +acceptedByCC + : RatifyEnv + → EnactState + → GovActionState + → Type +acceptedByCC Γ = AcceptedByCC.accepted currentEpoch ccHotKeys + where open RatifyEnv Γ using (currentEpoch; ccHotKeys) \end{code} \end{AgdaMultiCode} \caption{Vote counting for CC} @@ -388,52 +399,60 @@ In addition, it has to be the case that either \begin{figure*}[!ht] \begin{AgdaMultiCode} \begin{code} -acceptedByDRep - : RatifyEnv - → EnactState - → GovActionState - → Type -acceptedByDRep Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t - where +module AcceptedByDRep (Γ : RatifyEnv) + (eSt : EnactState) + (gaSt : GovActionState) where + \end{code} \begin{code}[hide] - open EnactState eSt using (cc; pparams) - open RatifyEnv Γ - open PParams (proj₁ pparams) - open StakeDistrs stakeDistrs - open GovActionState gaSt - open GovVotes votes using (gvDRep) + open EnactState eSt using (cc; pparams) + open RatifyEnv Γ using (currentEpoch; dreps; stakeDistrs) + open PParams (proj₁ pparams) + open StakeDistrs stakeDistrs + open GovActionState gaSt + open GovVotes votes using (gvDRep) \end{code} \begin{code} - castVotes : VDeleg ⇀ Vote - castVotes = mapKeys vDelegCredential gvDRep + castVotes : VDeleg ⇀ Vote + castVotes = mapKeys vDelegCredential gvDRep - activeDReps : ℙ Credential - activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps) + activeDReps : ℙ Credential + activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps) - predeterminedDRepVotes : VDeleg ⇀ Vote - predeterminedDRepVotes = case gaType action of -\end{code} -\begin{code}[hide] + predeterminedDRepVotes : VDeleg ⇀ Vote + predeterminedDRepVotes = case gaType action of λ where -\end{code} -\begin{code} NoConfidence → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.yes ❵ _ → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.no ❵ - defaultDRepCredentialVotes : VDeleg ⇀ Vote - defaultDRepCredentialVotes = constMap (mapˢ vDelegCredential activeDReps) Vote.no + defaultDRepCredentialVotes : VDeleg ⇀ Vote + defaultDRepCredentialVotes = constMap (mapˢ vDelegCredential activeDReps) Vote.no - actualVotes : VDeleg ⇀ Vote - actualVotes = castVotes ∪ˡ defaultDRepCredentialVotes - ∪ˡ predeterminedDRepVotes + actualVotes : VDeleg ⇀ Vote + actualVotes = castVotes ∪ˡ defaultDRepCredentialVotes + ∪ˡ predeterminedDRepVotes - t : ℚ - t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action DRep) + t : ℚ + t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action DRep) - acceptedStake totalStake : Coin - acceptedStake = ∑[ x ← stakeDistrVDeleg ∣ actualVotes ⁻¹ Vote.yes ] x - totalStake = ∑[ x ← stakeDistrVDeleg ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x + acceptedStake totalStake : Coin + acceptedStake = ∑[ x ← stakeDistrVDeleg ∣ actualVotes ⁻¹ Vote.yes ] x + totalStake = ∑[ x ← stakeDistrVDeleg ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x + + accepted = (acceptedStake /₀ totalStake) ≥ t + +acceptedByDRep + : RatifyEnv + → EnactState + → GovActionState + → Type +acceptedByDRep = AcceptedByDRep.accepted +\end{code} +\begin{code}[hide] +\end{code} +\begin{code} +\end{code} +\begin{code}[hide] \end{code} \end{AgdaMultiCode} \caption{Vote counting for DReps} @@ -469,53 +488,61 @@ auxiliary definitions: \begin{figure*}[!ht] \begin{AgdaMultiCode} \begin{code} -acceptedBySPO - : RatifyEnv - → EnactState - → GovActionState - → Type -acceptedBySPO Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t - where +module AcceptedBySPO (delegatees : VoteDelegs) + (pools : Pools) + (stakeDistrPools : KeyHash ⇀ Coin) + (eSt : EnactState) + (gaSt : GovActionState) where \end{code} \begin{code}[hide] - open EnactState eSt using (cc; pparams) - open RatifyEnv Γ - open StakeDistrs stakeDistrs - open GovActionState gaSt - open GovVotes votes using (gvSPO) + open EnactState eSt using (cc; pparams) + open GovActionState gaSt + open GovVotes votes using (gvSPO) \end{code} \begin{code} - castVotes : KeyHash ⇀ Vote - castVotes = gvSPO + castVotes : KeyHash ⇀ Vote + castVotes = gvSPO - defaultVote : KeyHash → Vote - defaultVote kh = case lookupᵐ? pools kh of + defaultVote : KeyHash → Vote + defaultVote kh = case lookupᵐ? pools kh of \end{code} \begin{code}[hide] - λ where + λ where \end{code} \begin{code} - nothing → Vote.no - (just p) → case lookupᵐ? delegatees (StakePoolParams.rewardAccount p) , gaType action of + nothing → Vote.no + (just p) → case lookupᵐ? delegatees (StakePoolParams.rewardAccount p) , gaType action of \end{code} \begin{code}[hide] - λ where + λ where \end{code} \begin{code} - (_ , TriggerHardFork) → Vote.no - (just vDelegNoConfidence , NoConfidence ) → Vote.yes - (just vDelegAbstain , _ ) → Vote.abstain - _ → Vote.no + (_ , TriggerHardFork) → Vote.no + (just vDelegNoConfidence , NoConfidence ) → Vote.yes + (just vDelegAbstain , _ ) → Vote.abstain + _ → Vote.no + + actualVotes : KeyHash ⇀ Vote + actualVotes = castVotes ∪ˡ mapFromFun defaultVote (dom stakeDistrPools) - actualVotes : KeyHash ⇀ Vote - actualVotes = castVotes ∪ˡ mapFromFun defaultVote (dom stakeDistrPools) + t : ℚ + t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action SPO) - t : ℚ - t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action SPO) + acceptedStake totalStake : Coin + acceptedStake = ∑[ x ← stakeDistrPools ∣ actualVotes ⁻¹ Vote.yes ] x + totalStake = ∑[ x ← stakeDistrPools ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x - acceptedStake totalStake : Coin - acceptedStake = ∑[ x ← stakeDistrPools ∣ actualVotes ⁻¹ Vote.yes ] x - totalStake = ∑[ x ← stakeDistrPools ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x + accepted : Type + accepted = (acceptedStake /₀ totalStake) ≥ t + +acceptedBySPO + : RatifyEnv + → EnactState + → GovActionState + → Type +acceptedBySPO Γ = AcceptedBySPO.accepted delegatees pools stakeDistrPools + where open RatifyEnv Γ + open StakeDistrs stakeDistrs \end{code} \end{AgdaMultiCode} \caption{Vote counting for SPOs} @@ -584,7 +611,7 @@ used for voting. \begin{figure*}[!ht] \begin{code}[hide] -abstract +opaque \end{code} \begin{code} accepted : RatifyEnv → EnactState → GovActionState → Type @@ -638,7 +665,9 @@ acceptConds Γ stʳ (id , st) = open RatifyState stʳ open GovActionState st -abstract +opaque + unfolding accepted + verifyPrev? : ∀ a h es → Dec (verifyPrev a h es) verifyPrev? NoConfidence h es = dec verifyPrev? UpdateCommittee h es = dec From 9405c281e9bf07a89a325332118edbff5d20a2b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 14 Oct 2025 15:10:50 +0200 Subject: [PATCH 02/13] trigger hydra From f0f68e5a21873bb546c552849553f210e102550a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 14 Oct 2025 16:11:44 +0200 Subject: [PATCH 03/13] Fix broken computational EPOCH module --- .../Epoch/Properties/Computational.agda | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda index 05afc485b4..2cce05551c 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda @@ -55,13 +55,15 @@ module _ {eps : EpochState} {e : Epoch} where open EpochState eps hiding (es) - prs = ⟦ u0 .utxoSt' , acnt , cs .dState , u0 .pState' ⟧ + u0 = EPOCHUpdates0.updates fut ls + module u0 = EPOCH-Updates0 u0 + + prs = ⟦ u0 .utxoSt' , acnt , cs .dState , cs .pState ⟧ where open LState open CertState open EPOCH-Updates0 cs = ls .certState - u0 = EPOCH-updates0 fut ls EPOCH-total : ∃[ eps' ] _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps' EPOCH-total = @@ -74,15 +76,15 @@ module _ {eps : EpochState} {e : Epoch} where EPOCH-state : Snapshots → RatifyState → PoolReapState → EpochState EPOCH-state ss fut' (⟦ utxoSt'' , acnt' , dState' , pState'' ⟧ᵖ) = let - EPOCHUpdates es govSt' dState'' _ gState' _ acnt'' = - EPOCH-updates fut ls dState' acnt' - certState' = ⟦ dState'' , pState'' , gState' ⟧ᶜˢ + EPOCHUpdates dState'' acnt'' = + EPOCHUpdates.updates u0 ls dState' acnt' + certState' = ⟦ dState'' , pState' , u0.gState' ⟧ᶜˢ in record { acnt = acnt'' ; ss = ss - ; ls = ⟦ utxoSt'' , govSt' , certState' ⟧ˡ - ; es = es + ; ls = ⟦ utxoSt'' , u0.govSt' , certState' ⟧ˡ + ; es = u0.es ; fut = fut' } @@ -115,7 +117,7 @@ module _ {eps : EpochState} {e : Epoch} where fut'≡fut'' : EpochState.fut eps' ≡ EpochState.fut eps'' fut'≡fut'' = RATIFIES-deterministic-≡ (cong (λ x → record - { stakeDistrs = mkStakeDistrs (Snapshots.mark x) _ _ _ _ _ + { stakeDistrs = mkStakeDistrs (Snapshots.mark x) _ _ _ (GStateOf ls) (DStateOf ls) ; currentEpoch = _ ; dreps = _ ; ccHotKeys = _ From 4425f04c1d36ca830e33f53ad5a199af11b2339f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 14 Oct 2025 16:20:57 +0200 Subject: [PATCH 04/13] Fix GovDepsMatch --- .../Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md index fd0efa2065..d53adb8a8d 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md +++ b/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md @@ -180,7 +180,7 @@ For the formal statement of the lemma, a ∈ˡ map' (GovActionDeposit ∘ proj₁) (filter P? govSt) ∼⟨ ∈-fromList ⟩ a ∈ fromList (map' (GovActionDeposit ∘ proj₁) (filter P? govSt)) ∎ - u0 = EPOCH-updates0 (RatifyStateOf eps) (LStateOf eps) + u0 = EPOCHUpdates0.updates (RatifyStateOf eps) (LStateOf eps) ls₁ = record (LStateOf eps') { utxoSt = EPOCH-Updates0.utxoSt' u0 } From d9265a39aac67702a312f18608a0f9d577251bdf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 16 Oct 2025 09:38:25 +0200 Subject: [PATCH 05/13] Remove postulates; import module from Epoch.Properties --- src/Ledger/Conway/Specification/Epoch/Properties.agda | 1 + .../Specification/Epoch/Properties/ExpiredDReps.agda | 7 ++----- src/Ledger/Core/Specification/Epoch.agda | 11 +++++++++-- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties.agda b/src/Ledger/Conway/Specification/Epoch/Properties.agda index 4d53ecb037..d8bd306085 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties.agda @@ -4,5 +4,6 @@ module Ledger.Conway.Specification.Epoch.Properties where open import Ledger.Conway.Specification.Epoch.Properties.Computational open import Ledger.Conway.Specification.Epoch.Properties.ConstRwds +open import Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps open import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch open import Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda index fdbb2e8477..53cb7c4bb3 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda @@ -1,4 +1,5 @@ --- {-# OPTIONS --without-K #-} +{-# OPTIONS --safe #-} + open import Ledger.Conway.Specification.Transaction open import Ledger.Conway.Specification.Abstract @@ -26,10 +27,6 @@ open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote) open import Axiom.Set.Properties th open import Relation.Binary.PropositionalEquality hiding (cong) -postulate - e-nonZero⁻¹ SlotsPerEpochᶜ) + .≤-predᵉ → [ (λ p → inj₁ (+-cancelˡ-< _ _ _ p)) , (λ p → inj₂ (suc-injective p)) ]′ ._+ᵉ'_ → _+_ .+ᵉ≡+ᵉ' {a} {b} → ℕ+ᵉ≡+ᵉ' {a} {b} From 7f56f45ec3234c7af5ebf302657bd998560eb2ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 16 Oct 2025 09:49:05 +0200 Subject: [PATCH 06/13] Add temporary overlay to overwrite agda-sets --- flake.lock | 20 +++++++++++++++++++- flake.nix | 16 ++++++++++++++++ 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/flake.lock b/flake.lock index 6557a10b71..252510f2fb 100644 --- a/flake.lock +++ b/flake.lock @@ -1,6 +1,23 @@ { "nodes": { "abstract-set-theory": { + "flake": false, + "locked": { + "lastModified": 1760446691, + "narHash": "sha256-L+wHrHLqdv9oY8LtqQFsOeZNoCiiCAg/KhsB/M7lHe4=", + "owner": "input-output-hk", + "repo": "agda-sets", + "rev": "de39823e91d845232bbf22058565d0553f5da2ac", + "type": "github" + }, + "original": { + "owner": "input-output-hk", + "repo": "agda-sets", + "rev": "de39823e91d845232bbf22058565d0553f5da2ac", + "type": "github" + } + }, + "abstract-set-theory_2": { "inputs": { "flake-utils": "flake-utils", "nixpkgs": [ @@ -36,7 +53,7 @@ }, "agda-nix": { "inputs": { - "abstract-set-theory": "abstract-set-theory", + "abstract-set-theory": "abstract-set-theory_2", "flake-utils": "flake-utils_2", "iog-prelude": "iog-prelude", "nixpkgs": [ @@ -325,6 +342,7 @@ }, "root": { "inputs": { + "abstract-set-theory": "abstract-set-theory", "agda-nix": "agda-nix", "flake-utils": "flake-utils_6", "fls-agda": "fls-agda", diff --git a/flake.nix b/flake.nix index 7d3f228f85..10ac8c139d 100644 --- a/flake.nix +++ b/flake.nix @@ -6,6 +6,11 @@ nixpkgs.url = "github:NixOs/nixpkgs"; flake-utils.url = "github:numtide/flake-utils"; + abstract-set-theory = { + url = "github:input-output-hk/agda-sets/de39823e91d845232bbf22058565d0553f5da2ac"; + flake = false; + }; + agda-nix = { url = "github:input-output-hk/agda.nix"; inputs.nixpkgs.follows = "nixpkgs"; @@ -38,6 +43,16 @@ ); }; + overlay-abstract-set-theory = final: prev: { + agdaPackages = prev.agdaPackages.overrideScope ( + afinal: aprev: { + abstract-set-theory = aprev.abstract-set-theory.overrideAttrs (_: { + src = inputs.abstract-set-theory; + }); + } + ); + }; + perSystem = flake-utils.lib.eachSystem systems ( system: let @@ -48,6 +63,7 @@ # (see https://github.com/NixOS/nixpkgs/issues/447012) inputs.fls-agda.overlays.default inputs.agda-nix.overlays.default + overlay-abstract-set-theory overlay-formal-ledger ]; }; From 45cb06030d1840619779b6be925dfc0ded03b83e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Mon, 20 Oct 2025 13:51:55 +0200 Subject: [PATCH 07/13] use opaque to improve tc time --- src/Ledger/Conway/Specification/Epoch.lagda.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/src/Ledger/Conway/Specification/Epoch.lagda.md b/src/Ledger/Conway/Specification/Epoch.lagda.md index 1c3c6ebf71..36b25a67d2 100644 --- a/src/Ledger/Conway/Specification/Epoch.lagda.md +++ b/src/Ledger/Conway/Specification/Epoch.lagda.md @@ -483,6 +483,21 @@ module VDelegDelegatedStake opaque ``` --> +```agda + calculateVDelegDelegatedStake + : Epoch + → UTxOState + → GovState + → GState + → DState + → VDeleg ⇀ Coin + calculateVDelegDelegatedStake = VDelegDelegatedStake.calculate +``` + ```agda calculatePoolDelegatedStakeForVoting : Snapshot @@ -529,7 +544,7 @@ mkStakeDistrs → DState → StakeDistrs mkStakeDistrs ss currentEpoch utxoSt govSt gState dState = - ⟦ VDelegDelegatedStake.calculate currentEpoch utxoSt govSt gState dState + ⟦ calculateVDelegDelegatedStake currentEpoch utxoSt govSt gState dState , calculatePoolDelegatedStakeForVoting ss utxoSt govSt ⟧ ``` From cb6e546cf1c8277082334b878d8a793aeba0ffef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Mon, 20 Oct 2025 14:45:26 +0200 Subject: [PATCH 08/13] Fix tc error --- .../Specification/Epoch/Properties/ExpiredDReps.agda | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda index 53cb7c4bb3..43bc5ab5f7 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda @@ -489,6 +489,16 @@ module VDelegDelegatedStake-≈ calculate : vds.calculate ≡ᵐ vds'.calculate calculate = mapFromFun-cong _ activeVDelegs +opaque + unfolding calculateVDelegDelegatedStake + + calculateVDelegDelegatedStake-≈ + : (e : Epoch) → (utxoSt : UTxOState) → (govSt : GovState) + → {gState gState' : GState} (gState≈gState' : GState-[ e ] gState ≈ gState') + → (dState : DState) + → calculateVDelegDelegatedStake e utxoSt govSt gState dState ≡ᵐ calculateVDelegDelegatedStake e utxoSt govSt gState' dState + calculateVDelegDelegatedStake-≈ e utxoSt govSt gState≈gState' dState = VDelegDelegatedStake-≈.calculate e utxoSt govSt gState≈gState' dState + module mkStakeDistrs {s s' : Snapshot} {utxoSt utxoSt' : UTxOState} {govSt govSt' : GovState} {gState gState' : GState} {dState dState' : DState} where @@ -498,7 +508,7 @@ module mkStakeDistrs {s s' : Snapshot} {utxoSt utxoSt' : UTxOState} {govSt govSt cong refl e refl refl gState≈gState' refl = record { R } where module R where - stakeDistrVDeleg = VDelegDelegatedStake-≈.calculate e utxoSt govSt gState≈gState' dState + stakeDistrVDeleg = calculateVDelegDelegatedStake-≈ e utxoSt govSt gState≈gState' dState stakeDistrPools = refl module EPOCH {epSt epSt' : EpochState} (e : Epoch) (epSt≈epSt' : EpochState-[ e ] epSt ≈ epSt') where From 9b55dfe5d9f7329ea26b1bcdec2fbf3b66a194f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Mon, 20 Oct 2025 17:49:27 +0200 Subject: [PATCH 09/13] Implement agda-sets properties locally --- flake.lock | 20 +------ flake.nix | 16 ------ .../Axiom/Set/Properties.agda | 56 +++++++++++++++++++ .../Epoch/Properties/ExpiredDReps.agda | 4 +- 4 files changed, 60 insertions(+), 36 deletions(-) create mode 100644 src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda diff --git a/flake.lock b/flake.lock index 252510f2fb..6557a10b71 100644 --- a/flake.lock +++ b/flake.lock @@ -1,23 +1,6 @@ { "nodes": { "abstract-set-theory": { - "flake": false, - "locked": { - "lastModified": 1760446691, - "narHash": "sha256-L+wHrHLqdv9oY8LtqQFsOeZNoCiiCAg/KhsB/M7lHe4=", - "owner": "input-output-hk", - "repo": "agda-sets", - "rev": "de39823e91d845232bbf22058565d0553f5da2ac", - "type": "github" - }, - "original": { - "owner": "input-output-hk", - "repo": "agda-sets", - "rev": "de39823e91d845232bbf22058565d0553f5da2ac", - "type": "github" - } - }, - "abstract-set-theory_2": { "inputs": { "flake-utils": "flake-utils", "nixpkgs": [ @@ -53,7 +36,7 @@ }, "agda-nix": { "inputs": { - "abstract-set-theory": "abstract-set-theory_2", + "abstract-set-theory": "abstract-set-theory", "flake-utils": "flake-utils_2", "iog-prelude": "iog-prelude", "nixpkgs": [ @@ -342,7 +325,6 @@ }, "root": { "inputs": { - "abstract-set-theory": "abstract-set-theory", "agda-nix": "agda-nix", "flake-utils": "flake-utils_6", "fls-agda": "fls-agda", diff --git a/flake.nix b/flake.nix index 10ac8c139d..7d3f228f85 100644 --- a/flake.nix +++ b/flake.nix @@ -6,11 +6,6 @@ nixpkgs.url = "github:NixOs/nixpkgs"; flake-utils.url = "github:numtide/flake-utils"; - abstract-set-theory = { - url = "github:input-output-hk/agda-sets/de39823e91d845232bbf22058565d0553f5da2ac"; - flake = false; - }; - agda-nix = { url = "github:input-output-hk/agda.nix"; inputs.nixpkgs.follows = "nixpkgs"; @@ -43,16 +38,6 @@ ); }; - overlay-abstract-set-theory = final: prev: { - agdaPackages = prev.agdaPackages.overrideScope ( - afinal: aprev: { - abstract-set-theory = aprev.abstract-set-theory.overrideAttrs (_: { - src = inputs.abstract-set-theory; - }); - } - ); - }; - perSystem = flake-utils.lib.eachSystem systems ( system: let @@ -63,7 +48,6 @@ # (see https://github.com/NixOS/nixpkgs/issues/447012) inputs.fls-agda.overlays.default inputs.agda-nix.overlays.default - overlay-abstract-set-theory overlay-formal-ledger ]; }; diff --git a/src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda b/src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda new file mode 100644 index 0000000000..204de96787 --- /dev/null +++ b/src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda @@ -0,0 +1,56 @@ +{-# OPTIONS --safe --no-import-sorts #-} +open import Axiom.Set using (Theory) + +module abstract-set-theory.Axiom.Set.Properties {ℓ} (th : Theory {ℓ}) where + +open import abstract-set-theory.Prelude hiding (isEquivalence; trans; map; map₂) +open Theory th + +open import Axiom.Set.Properties th hiding (filter-⇒-⊆; filter-map ) + +import Function.Related.Propositional as R +open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Lattice +open import Relation.Binary.Morphism using (IsOrderHomomorphism) + +open Equivalence + +private variable + A B C : Type ℓ + X Y Z : Set A + +module _ {P Q : A → Type} {sp-P : specProperty P} {sp-Q : specProperty Q} where + + import Relation.Unary as U + + 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-⊇ + where + filter-map-⊆ : filter sp-Q (map f X) ⊆ filter sp-Q (map f (filter sp-P X)) + filter-map-⊆ p with from ∈-filter p + ... | Qa , p with from ∈-map p + ... | (a , refl , p) = to ∈-filter (Qa , (to ∈-map (_ , (refl , (to ∈-filter (Qf⇒P a Qa , p)))))) + + filter-map-⊇ : filter sp-Q (map f (filter sp-P X)) ⊆ filter sp-Q (map f X) + filter-map-⊇ p with from ∈-filter p + ... | Qfa , p with from ∈-map p + ... | (a , refl , p) with from ∈-filter p + ... | (Pa , p) = to ∈-filter (Qfa , (to ∈-map (a , (refl , p)))) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda index 43bc5ab5f7..95a3e6a392 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda @@ -24,9 +24,11 @@ open import Ledger.Conway.Specification.PoolReap txs abs open import Ledger.Conway.Specification.Utxo txs abs open import Ledger.Conway.Specification.Gov txs open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote) -open import Axiom.Set.Properties th open import Relation.Binary.PropositionalEquality hiding (cong) +open import Axiom.Set.Properties th hiding (filter-map) +open import abstract-set-theory.Axiom.Set.Properties th + -- | Epoch indexed relation. -- Two DReps (Map Credential Epoch) are related iff: Non-expired DReps are the same. DReps-[_]_≈_ : Epoch → B.Rel DReps 0ℓ From 3c20f8f577b42c61d57345abb5dc38fa127c4cef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 21 Oct 2025 09:32:23 +0200 Subject: [PATCH 10/13] Fix typechecking --- flake.lock | 24 +++++++++---------- src-lib-exts/stdlib-meta/Reflection.agda | 2 +- .../Epoch/Properties/Computational.agda | 2 +- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/flake.lock b/flake.lock index 6557a10b71..bb45f9062b 100644 --- a/flake.lock +++ b/flake.lock @@ -21,11 +21,11 @@ ] }, "locked": { - "lastModified": 1760101453, - "narHash": "sha256-ACyo6WhFzNDak6dE2V0JEO4bnc/bXerqKnKnCRgGl+M=", + "lastModified": 1760957267, + "narHash": "sha256-xhU/YozvQL7I3Krw/VySqwbkOTpU6rDJQb810/YdBxg=", "owner": "input-output-hk", "repo": "agda-sets", - "rev": "82554d7b901749e0a36e5cecd23751002b979d67", + "rev": "60324463819e514bca0c39d0c39146069cc381cd", "type": "github" }, "original": { @@ -47,11 +47,11 @@ "standard-library-meta": "standard-library-meta" }, "locked": { - "lastModified": 1760347420, - "narHash": "sha256-0eYDkEhkbcFIlFJFfz1bUDJK4z4+r0n4ta5EzR+mv9c=", + "lastModified": 1760976118, + "narHash": "sha256-FF0oNtU7XaWKxi5XNgyyc0/F+PLB73Vo4OOfzrfFvq0=", "owner": "input-output-hk", "repo": "agda.nix", - "rev": "01bd2223ea377113f50a9688b5610a579ceb37f9", + "rev": "acc1da6d9d84dda2e7e95715e0ab5ee6ea8ea4ef", "type": "github" }, "original": { @@ -379,11 +379,11 @@ "standard-library-classes_2": { "flake": false, "locked": { - "lastModified": 1754406591, - "narHash": "sha256-tuXuZcwu6XNFP979oSZg0yfFY9eMyqpkUNddk+QchVc=", + "lastModified": 1754382520, + "narHash": "sha256-NaxK37VVO1Jrc4F9B5v+/yo0Pjnp4CwpH1us4Oxgby0=", "owner": "agda", "repo": "agda-stdlib-classes", - "rev": "e732956fb01eb616bb3429f290d9434f4ab59b6a", + "rev": "454d18c76b0baf4095006e46cbf094e628d7d31a", "type": "github" }, "original": { @@ -424,11 +424,11 @@ "standard-library-meta_2": { "flake": false, "locked": { - "lastModified": 1754406588, - "narHash": "sha256-YH8OqGsQ2DKhKqhSUWBDTimQSZsNCnqwZqNqQwnnVS0=", + "lastModified": 1754389036, + "narHash": "sha256-ir4BxJ+XjYhB0RdBKVPd+YBaIMWzjRCq+188qKZjgdg=", "owner": "agda", "repo": "agda-stdlib-meta", - "rev": "ba0159a198c99185bda86541362f8e0a4a82538a", + "rev": "d80dc70374f9d33c15889c2cf0c8048b4f697c4c", "type": "github" }, "original": { diff --git a/src-lib-exts/stdlib-meta/Reflection.agda b/src-lib-exts/stdlib-meta/Reflection.agda index 9f19c763b6..5a76ea403c 100644 --- a/src-lib-exts/stdlib-meta/Reflection.agda +++ b/src-lib-exts/stdlib-meta/Reflection.agda @@ -13,7 +13,7 @@ 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 ⦃...⦄ diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda index 2cce05551c..324b96b76b 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda @@ -78,7 +78,7 @@ module _ {eps : EpochState} {e : Epoch} where let EPOCHUpdates dState'' acnt'' = EPOCHUpdates.updates u0 ls dState' acnt' - certState' = ⟦ dState'' , pState' , u0.gState' ⟧ᶜˢ + certState' = ⟦ dState'' , pState'' , u0.gState' ⟧ᶜˢ in record { acnt = acnt'' From 77500fc240fc6e057a18ed94a774760adc345710 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 28 Oct 2025 12:05:00 +0100 Subject: [PATCH 11/13] Incorporate William's suggestions --- .../Axiom/Set/Properties.agda | 42 ++++++++----------- 1 file changed, 17 insertions(+), 25 deletions(-) diff --git a/src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda b/src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda index 204de96787..42addd4efd 100644 --- a/src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda +++ b/src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda @@ -6,13 +6,6 @@ module abstract-set-theory.Axiom.Set.Properties {ℓ} (th : Theory {ℓ}) where open import abstract-set-theory.Prelude hiding (isEquivalence; trans; map; map₂) open Theory th -open import Axiom.Set.Properties th hiding (filter-⇒-⊆; filter-map ) - -import Function.Related.Propositional as R -open import Relation.Binary hiding (_⇔_) -open import Relation.Binary.Lattice -open import Relation.Binary.Morphism using (IsOrderHomomorphism) - open Equivalence private variable @@ -21,9 +14,9 @@ private variable module _ {P Q : A → Type} {sp-P : specProperty P} {sp-Q : specProperty Q} where - import Relation.Unary as U + open import Relation.Unary using (_⇒_; Universal) - filter-⇒ : (P⇒Q : U.Universal (P U.⇒ Q)) → filter sp-P (filter sp-Q X) ≡ᵉ filter sp-P X + filter-⇒ : (P⇒Q : Universal (P ⇒ 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 @@ -37,20 +30,19 @@ module _ {P Q : A → Type} {sp-P : specProperty P} {sp-Q : specProperty Q} wher 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 + open import Relation.Unary using (_⇒_; Universal) - filter-map : filter sp-Q (map f X) ≡ᵉ filter sp-Q (map f (filter sp-P X)) - filter-map = filter-map-⊆ , filter-map-⊇ - where - filter-map-⊆ : filter sp-Q (map f X) ⊆ filter sp-Q (map f (filter sp-P X)) - filter-map-⊆ p with from ∈-filter p - ... | Qa , p with from ∈-map p - ... | (a , refl , p) = to ∈-filter (Qa , (to ∈-map (_ , (refl , (to ∈-filter (Qf⇒P a Qa , p)))))) - - filter-map-⊇ : filter sp-Q (map f (filter sp-P X)) ⊆ filter sp-Q (map f X) - filter-map-⊇ p with from ∈-filter p - ... | Qfa , p with from ∈-map p - ... | (a , refl , p) with from ∈-filter p - ... | (Pa , p) = to ∈-filter (Qfa , (to ∈-map (a , (refl , p)))) + filter-map : ∀ {f : A → B} (Qf⇒P : Universal ((Q ∘ f) ⇒ P)) + → filter sp-Q (map f X) ≡ᵉ filter sp-Q (map f (filter sp-P X)) + filter-map {f = f} Qf⇒P = filter-map-⊆ , filter-map-⊇ + where + filter-map-⊆ : filter sp-Q (map f X) ⊆ filter sp-Q (map f (filter sp-P X)) + filter-map-⊆ p with from ∈-filter p + ... | Qa , p with from ∈-map p + ... | (a , refl , p) = to ∈-filter (Qa , (to ∈-map (_ , (refl , (to ∈-filter (Qf⇒P a Qa , p)))))) + + filter-map-⊇ : filter sp-Q (map f (filter sp-P X)) ⊆ filter sp-Q (map f X) + filter-map-⊇ p with from ∈-filter p + ... | Qfa , p with from ∈-map p + ... | (a , refl , p) with from ∈-filter p + ... | (Pa , p) = to ∈-filter (Qfa , (to ∈-map (a , (refl , p)))) From 0b21e85f7026001de2fcb21bf1bb52295cbf90ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Tue, 28 Oct 2025 14:26:44 +0100 Subject: [PATCH 12/13] Fill leftover goal --- .../Conway/Specification/Epoch/Properties/ExpiredDReps.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda index c23a98a65e..b0d0f9cf64 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda @@ -589,6 +589,6 @@ module EPOCH {epSt epSt' : EpochState} (e : Epoch) (epSt≈epSt' : EpochState-[ ls = record {LS} es : record (EnactStateOf (RatifyStateOf epSt)) { withdrawals = ∅ } ≡ record (EnactStateOf (RatifyStateOf epSt')) { withdrawals = ∅ } - es rewrite (P.cong EnactStateOf epSt≈epSt'.fut) = {!refl!} + es rewrite (P.cong EnactStateOf epSt≈epSt'.fut) = refl fut = fut≡fut' From 128558d4aef0c0cd86e28e990c16950fe159fcf0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Wed, 29 Oct 2025 08:37:14 +0100 Subject: [PATCH 13/13] Make literate agda file; add explanation --- ...xpiredDReps.agda => ExpiredDReps.lagda.md} | 161 +++++++++++------- 1 file changed, 101 insertions(+), 60 deletions(-) rename src/Ledger/Conway/Specification/Epoch/Properties/{ExpiredDReps.agda => ExpiredDReps.lagda.md} (97%) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md similarity index 97% rename from src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda rename to src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md index b0d0f9cf64..eb417dddd4 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md @@ -1,3 +1,5 @@ + --- | Epoch indexed relation. --- Two DReps (Map Credential Epoch) are related iff: Non-expired DReps are the same. +The EPOCH`{.AgdaDatatype} transition system behaves parametrically w.r.t. the +set of expired `DReps`{.AgdaInductiveConstructor} that are part of the +`EpochState`{.AgdaRecord}. + +The following family of equivalence relations indexed by `Epoch` formalize the +concept of two maps of `DReps`{.AgdaInductiveConstructor} being the same on +non-expired `DReps`{.AgdaInductiveConstructor}: + +```agda DReps-[_]_≈_ : Epoch → B.Rel DReps 0ℓ DReps-[_]_≈_ e dreps₁ dreps₂ = filterᵐ (λ (c , e') → e ≤ e') dreps₁ ≡ᵐ filterᵐ (λ (c , e') → e ≤ e') dreps₂ +``` + +This family of relations is monotonic w.r.t. increment on `Epoch`{.AgdaDatatype} +and respects `sucᵉ`{.AgdaFunction}: + +```agda +DReps-≈-mono : ∀ (e : Epoch) {dreps₁ dreps₂ : DReps} → DReps-[ e ] dreps₁ ≈ dreps₂ → DReps-[ sucᵉ e ] dreps₁ ≈ dreps₂ +DReps-≈-mono e {dreps₁} {dreps₂} dreps₁≈dreps₂ = + begin + filterᵐ (λ (_ , e') → sucᵉ e ≤ e') dreps₁ ˢ + ≈⟨ filter-⇒ P⇒Q ⟨ + filterᵐ (λ (_ , e') → sucᵉ e ≤ e') (filterᵐ (λ (_ , e') → e ≤ e') dreps₁) ˢ + ≈⟨ filter-cong dreps₁≈dreps₂ ⟩ + filterᵐ (λ (_ , e') → sucᵉ e ≤ e') (filterᵐ (λ (_ , e') → e ≤ e') dreps₂) ˢ + ≈⟨ filter-⇒ P⇒Q ⟩ + filterᵐ (λ (_ , e') → sucᵉ e ≤ e') dreps₂ ˢ + ∎ + where + open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid + 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')) + P⇒Q _ p = esp.≤-trans (proj₁ (esp.<⇒≤∧≉ e -DReps-≈-mono : ∀ (e : Epoch) {dreps₁ dreps₂ : DReps} → DReps-[ e ] dreps₁ ≈ dreps₂ → DReps-[ sucᵉ e ] dreps₁ ≈ dreps₂ -DReps-≈-mono e {dreps₁} {dreps₂} dreps₁≈dreps₂ = - begin - filterᵐ (λ (_ , e') → sucᵉ e ≤ e') dreps₁ ˢ - ≈⟨ filter-⇒ P⇒Q ⟨ - filterᵐ (λ (_ , e') → sucᵉ e ≤ e') (filterᵐ (λ (_ , e') → e ≤ e') dreps₁) ˢ - ≈⟨ filter-cong dreps₁≈dreps₂ ⟩ - filterᵐ (λ (_ , e') → sucᵉ e ≤ e') (filterᵐ (λ (_ , e') → e ≤ e') dreps₂) ˢ - ≈⟨ filter-⇒ P⇒Q ⟩ - filterᵐ (λ (_ , e') → sucᵉ e ≤ e') dreps₂ ˢ - ∎ - where - open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid - 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')) - P⇒Q _ p = esp.≤-trans (proj₁ (esp.<⇒≤∧≉ e + +The main property states that `EPOCH`{.AgdaDatatype} "preserves" the above +relation on `EpochState`{.AgdaRecord}: +```agda module EPOCH {epSt epSt' : EpochState} (e : Epoch) (epSt≈epSt' : EpochState-[ e ] epSt ≈ epSt') where module epSt≈epSt' = EpochState-[_]_≈_ epSt≈epSt' @@ -535,6 +569,11 @@ module EPOCH {epSt epSt' : EpochState} (e : Epoch) (epSt≈epSt' : EpochState-[ → tt ⊢ epSt' ⇀⦇ e ,EPOCH⦈ epSt''' → EpochState-[ sucᵉ e ] epSt'' ≈ epSt''' cong eps'' eps''' (EPOCH (snap₁ , poolreap₁ , ratify₁)) (EPOCH (snap₂ , poolreap₂ , ratify₂)) +``` +(Proof ommited from rendering) + +