Add monetary and treasury expansion to `PParams` (old) #707

HeinrichApfelmus · 2025-03-08T14:53:13Z

Description

This pull request adds the monetary expansion rho and treasury expansion tau protocol parameters to the PParams type.

In order to be able to prove that the treasury and reserves are not negative, it is necessary to constrain these parameters need to the unit interval [0, 1]. These conditions need to be stored somewhere — I have chosen to make them part of the PParams type by refining the parameters to a new type UnitInterval. (This is similar to how the previous specification of the Shelley ledger encodes these parameters.)

Context: #706

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

HeinrichApfelmus · 2025-03-08T15:01:43Z

One problem introduced by the definition UnitInterval = Refinement ℚ … is that I can no longer use the autoHsType and autoConvert macros, which are presumably needed by the conformance test suite.

However, this is a symptom of an underlying problem: The Refinement type mixes computational and logical aspects: The invariant that the number is constraint to the unit interval is now mixed into the code. There is no direct Haskell equivalent for this type!

We could try to avoid Refinement altogether, but that doesn't eliminate the problem that we have to store the invariant somewhere. It could be part of an environment or part of a precondition for a rule, but putting it in right in the definition of PParams seemed like a good idea to me, also because it matches the definition in the original Shelley specification.

(While working with agda2hs, I found that such invariants typically require irrelevance . and erasure @0 to work well with Haskell code. If you ask me, the merging of code and logic in Agda has swung a bit too far into the "everything is code" direction.)

@WhatisRT — thoughts?

carlostome · 2025-03-10T07:54:35Z

One problem introduced by the definition UnitInterval = Refinement ℚ … is that I can no longer use the autoHsType and autoConvert macros, which are presumably needed by the conformance test suite.

They are not needed, these macros are convenient to derive the Haskell datatypes but it could be done "by hand".

However, this is a symptom of an underlying problem: The Refinement type mixes computational and logical aspects: The invariant that the number is constraint to the unit interval is now mixed into the code. There is no direct Haskell equivalent for this type!

This problem already occurs in some places in the codebase. For example see GovProposal in the Ledger and in conformance:

formal-ledger-specifications/src/Ledger/GovernanceActions.lagda

Line 174 in 2cd9668

record GovProposal : Type where
formal-ledger-specifications/src/Ledger/Conway/Foreign/HSLedger/Gov.agda

Line 49 in 2cd9668

-- Then we define non-dependent versions of the types that use

In a nutshell, the current approach is to define a nondependent version of the type, which can be compiled to Haskell, and define conversion functions from and to the dependent version.

formal-ledger-specifications/src/Ledger/Conway/Foreign/HSLedger/Gov.agda

Line 73 in 2cd9668

mkGovProposal' : Convertible GovProposal GovProposal'

HeinrichApfelmus · 2025-03-10T12:12:29Z

Thanks @carlostome !

In a nutshell, the current approach is to define a nondependent version of the type, which can be compiled to Haskell, and define conversion functions from and to the dependent version.

Sounds good, I can try to do that — but I think that I will get a problem with the Convertible A B class. 🤔

Actually, I think that there are two issues:

Convertible A B consists of two total functions A → B and B → A. But I cannot choose A = UnitInterval and B = ℚ, because even though I do have a function UnitInterval → ℚ, I only have a function ℚ → Maybe UnitInterval.
The conversion UnitInterval → UnitInterval' will "bubble up" to PParams, i.e. I will have to rewrite the definition Conv-PParams = autoConvert PParams as well.

The first issue is a general issue with Refinement types: For any predicate P, we can at best convert between the types Maybe [ x ∈ ℚ ∣ P x ] and Maybe ℚ, but we cannot convert between [ x ∈ ℚ ∣ P x ] and ℚ.

Unfortunately, I think that the underlying problem remains the same: The statement "the dependent type A has no direct Haskell equivalent" is equivalent to "there is no non-dependent type B for which there exist functions A → B and B → A". 😅 (EDIT: Strictly speaking: bijections.) In the case of Refinement types, the best we can hope for is an embedding A → B with inverse B → Maybe A, but I would need to change the definition of Convertible for that. 😅 — Should I?

EDIT: In this particular case, there is a workaround: I can define from : ℚ → UnitInterval by clamping the value, i.e. from x = min 1 (max 0 x). More generally, I can assign an arbitrary value to those values that fail the predicate — should I do that instead?

The second issues adds boilerplate, but seems otherwise benign to me.

WhatisRT · 2025-03-11T12:44:06Z

In these cases, we've usually just embraced that the FFI part is unsafe anyway, see e.g. here. This would work just fine in that case as well. That way, the code is neatly split into a safe part that has the required invariants and an unsafe part that will just crash if you actually do anything bad. If we want the caller to be able to handle that error we'd have to restructure Convertible, but I don't think we care right now (and maybe will never).

We even have some occurances of coerce ⦃ TrustMe ⦄ (unsafeCoerce) in our FFI, so this is relatively harmless.

HeinrichApfelmus · 2025-03-12T14:24:35Z

In these cases, we've usually just embraced that the FFI part is unsafe anyway, see e.g. here. This would work just fine in that case as well. That way, the code is neatly split into a safe part that has the required invariants and an unsafe part that will just crash if you actually do anything bad

Thanks! I will try it this way, then.

I agree that restructuring Convertible is probably not worth it.

carlostome

Good work, here are some comments:

I think the name UnitInterval is a bit misleading since it is using rationals and not reals. The best alternative I can come up atm is to use the symbol ℚ withing the name: UnitIntervalℚ or ℚUnitInterval.
Regarding the module structure, I suggest to add another level in the hierarchy, Ledger.Types.Numeric.UnitInterval, since in the future we might want to use a similar approach for positive naturals etc.

src/Ledger/Types/Numeric.agda

carlostome · 2025-03-20T13:29:49Z

src/Ledger/Types/Numeric.agda

+prop-inUnitInterval-*
+  : ∀ (x y : ℚ)
+  → inUnitInterval x
+  → inUnitInterval y
+  → inUnitInterval (x ℚ.* y)
+--
+prop-inUnitInterval-* x y ux (0≤y , y≤1) =
+  ( prop-inUnitInterval-*-0≤ x y ux 0≤y , x*y≤1)
+  where
+  x*y≤1 = ℚ.≤-trans (prop-inUnitInterval-*-≤y x y ux 0≤y) y≤1


I'm surprised this property exists without defining multiplication of UnitInterval numbers.
If its not going to be used I suggest not to include it (and the lemmas it depends on)

I will probably need this lemma when proving that the rewards update is nonnegative and bounded by the available rewards, that's why I have added it in advance.

carlostome · 2025-03-20T13:31:09Z

src/Ledger/Types/Numeric.agda

+-- Multiplying with a number from the unit interval stays positive.
+prop-inUnitInterval-*-0≤
+  : ∀ (x y : ℚ)
+  → inUnitInterval x
+  → 0ℚ ≤ y
+  → 0ℚ ≤ x ℚ.* y


I feel this prop is just plumbing and thus should be inlined or placed in a where clause within prop-inUnitInterval-*

I will need this property when proving that the reward pot is nonnegative. I can try to inline it at the proof site, but the proof of this property is slightly too complicated for inlining for my taste.

src/Ledger/Types/Numeric.agda

carlostome · 2025-03-20T13:34:07Z

src/Ledger/Types/Numeric.agda

+  with isInUnitInterval x
+... | yes p = x , [ p ]
+


I get an Agda warning in this line:

Incomplete pattern matching for Ledger.Types.Numeric.with-. Missing cases: mkUnitInterval x evidence | .false because ofⁿ ¬a when checking the definition of Ledger.Types.Numeric.with-

I don't remember seeing this warning before — it's probably due to the change of definition of isInUnitInterval? 🤔 But I can discharge the proof obligation.

My bad, I should have double checked I didn't introduce the warning

src/Ledger/Types/Numeric.agda

carlostome · 2025-03-20T13:53:37Z

src/ScriptVerification/Lib.agda

+                               ; tau = mkUnitInterval (+ 2 / 10) refl
+                               ; rho = mkUnitInterval (+ 3 / 1000) refl


Would be nice if we can make mkUnitInterval deduce (or use a tactic) for the refl part

I like to think of refl as a tactic that proves equality ≡ by computation. From that viewpoint, refl is the tactic.

You can give mkUnitInterval a tactic argument:

open import Tactic.Defaults open import Tactic.Constrs mkUnitInterval : ∀ (x : ℚ) → {@(tactic tryConstrs 10) : does (isInUnitInterval x) ≡ true} → UnitInterval

Then you can write mkUnitInterval (+ 3 / 1000) and it'll find refl automatically. And in case refl doesn't work, you can still supply the proof manually: mkUnitInterval x {myProof}.

Do you want me to add this implicit tactic argument?

The tryConst tactic does not quite work — the argument to the tactic annotation must be of type Term → TC ⊤. I'll stick to refl for now.

HeinrichApfelmus · 2025-03-20T16:10:01Z

Thanks for the review, @carlostome ! 😊

Regarding the module structure, I suggest to add another level in the hierarchy, Ledger.Types.Numeric.UnitInterval, since in the future we might want to use a similar approach for positive naturals etc.

Ok, done.

I think the name UnitInterval is a bit misleading since it is using rationals and not reals. The best alternative I can come up atm is to use the symbol ℚ withing the name: UnitIntervalℚ or ℚUnitInterval.

I can do that if you really want me to, but I'm not sure if that's a good idea:

As far as I can tell, agda-stdlib currently does not try to define constructive real numbers (but see Real numbers, based on Cauchy sequences agda/agda-stdlib#2487). I think it's fair to tacitly assume that the real numbers are not used in software, and that any type with this name will have an "obvious" finite representation, here rational numbers.
The cardano-ledger Haskell code uses a type called UnitInterval for the same purpose — though that type contains an additional size restriction.

williamdemeo · 2025-03-21T18:28:22Z

@HeinrichApfelmus this looks good overall. Nice work! I'm just going to push some style mods to your branch. I hope you don't mind. (Just some things to make the code more consistent with the existing code.) If you don't agree with any of the changes, feel free to comment and/or revert them.

src/Ledger/BaseTypes.lagda

WhatisRT · 2025-03-24T11:39:06Z

src/Class/DecEq/Instances/Extra.agda

+
+-- Equality for a Refinement type is decide if the equality
+-- for the type to be refined is decidable.
+DeqEq-Refinement


It'd be fantastic to upstream this to https://github.com/agda/agda-stdlib-classes

Ok, but not in the present pull request in order to keep the scope limited.

I have created an issue agda/agda-stdlib-classes#17

WhatisRT · 2025-03-24T11:48:28Z

src/ScriptVerification/Lib.agda

+                               ; tau = mkUnitInterval (+ 2 / 10) refl
+                               ; rho = mkUnitInterval (+ 3 / 1000) refl


You can give mkUnitInterval a tactic argument:

open import Tactic.Defaults open import Tactic.Constrs mkUnitInterval : ∀ (x : ℚ) → {@(tactic tryConstrs 10) : does (isInUnitInterval x) ≡ true} → UnitInterval

Then you can write mkUnitInterval (+ 3 / 1000) and it'll find refl automatically. And in case refl doesn't work, you can still supply the proof manually: mkUnitInterval x {myProof}.

WhatisRT · 2025-03-24T11:53:17Z

src/Ledger/PParams.lagda

+        tau                           : UnitInterval -- treasury expansion
+        rho                           : UnitInterval -- monetary expansion


I think it might be best to change those to the more approachable names. People are already complaining about short meaningless names.

Suggested change

tau : UnitInterval -- treasury expansion

rho : UnitInterval -- monetary expansion

treasuryCut : UnitInterval

monetaryExpansion : UnitInterval

Ok, I can do that — the only trouble is that this would be incompatible with the existing nomenclature in the Shelley genesis file, though, so people will have to be instructed to use the new names.

HeinrichApfelmus · 2025-03-26T12:38:22Z

Thanks @williamdemeo and @WhatisRT !

I'm just going to push some style mods to your branch. I hope you don't mind. (Just some things to make the code more consistent with the existing code.) If you don't agree with any of the changes, feel free to comment and/or revert them.

Thanks! I am only going to change

overly long indentation in the body of inUnitInterval-*

As for the prop- prefix — I have converged on prefixing all logical statements with prop- in order to make them more easily distinguishable from computations, but that was in the context of adga2hs where I had a clear separation between target language (Haskell) and metalanguage (Agda). I'll use what you prefer here.

HeinrichApfelmus · 2025-03-26T15:07:29Z

For technical reasons (CI step "MAlonzo"), I'm closing this pull request and I'm opening a new one with the code after review at #732.

HeinrichApfelmus marked this pull request as ready for review March 18, 2025 13:55

carlostome reviewed Mar 20, 2025

View reviewed changes

HeinrichApfelmus requested a review from carlostome March 21, 2025 09:27

WhatisRT reviewed Mar 24, 2025

View reviewed changes

carlostome mentioned this pull request Mar 25, 2025

Remaining Shelley features/proofs #675

Open

7 tasks

HeinrichApfelmus added 7 commits March 26, 2025 15:21

Add Ledger.Types.Numeric.UnitInterval

251629f

Add instance for DecEq UnitInterval

3820973

Add instance for Show UnitInterval

c8b0177

Add Convertible instances for UnitInterval

9279127

Document UnitInterval in Ledger.BaseTypes

caa4d0c

Add treasuryCut and monetaryExpansion to PParams

f8eed12

Update CHANGELOG.md

ca1d950

HeinrichApfelmus changed the title ~~Add monetary and treasury expansion to PParams~~ Add monetary and treasury expansion to PParams (old) Mar 26, 2025

HeinrichApfelmus mentioned this pull request Mar 26, 2025

Add monetary and treasury expansion to PParams #732

Merged

4 tasks

HeinrichApfelmus closed this Mar 26, 2025

		; tau = mkUnitInterval (+ 2 / 10) refl
		; rho = mkUnitInterval (+ 3 / 1000) refl

		tau : UnitInterval -- treasury expansion
		rho : UnitInterval -- monetary expansion

Add monetary and treasury expansion to PParams (old) #707

Add monetary and treasury expansion to PParams (old) #707

Uh oh!

Conversation

HeinrichApfelmus commented Mar 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Checklist

Uh oh!

HeinrichApfelmus commented Mar 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

carlostome commented Mar 10, 2025

Uh oh!

HeinrichApfelmus commented Mar 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

WhatisRT commented Mar 11, 2025

Uh oh!

HeinrichApfelmus commented Mar 12, 2025

Uh oh!

carlostome left a comment

Choose a reason for hiding this comment

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!

Choose a reason for hiding this comment

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!

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!

HeinrichApfelmus commented Mar 20, 2025

Uh oh!

williamdemeo commented Mar 21, 2025

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

HeinrichApfelmus commented Mar 26, 2025

Uh oh!

HeinrichApfelmus commented Mar 26, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Add monetary and treasury expansion to `PParams` (old) #707

Add monetary and treasury expansion to `PParams` (old) #707

HeinrichApfelmus commented Mar 8, 2025 •

edited

Loading

HeinrichApfelmus commented Mar 8, 2025 •

edited

Loading

HeinrichApfelmus commented Mar 10, 2025 •

edited

Loading