Merge branch 'master' into master-markdown

Author: williamdemeo

lib-exts/stdlib/Data/Rational/Properties.agda

@@ -0,0 +1,90 @@
+{-# OPTIONS --safe #-}
+module stdlib.Data.Rational.Properties where
+
+open import Data.Integer using (ℤ; _/ℕ_; +≤+)
+import      Data.Integer as ℤ
+open import Data.Integer.DivMod using (div-pos-is-/ℕ; 0≤n⇒0≤n/ℕd)
+open import Data.Integer.Properties using (module ≤-Reasoning; *-identityʳ; *-zeroˡ)
+open import Data.Nat using (ℕ; z≤n)
+open import Data.Rational
+open import Data.Rational.Properties renaming (module ≤-Reasoning to ≤ℚ-Reasoning)
+                                     using (*-monoˡ-≤-nonNeg; *-zeroʳ; 1/pos⇒pos; nonNeg∧nonZero⇒pos;
+                                           nonNeg*nonNeg⇒nonNeg; pos⇒nonNeg; nonNegative⁻¹)
+open import Data.Unit.Base using (⊤)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+
+-- Natural number literals
+open import Agda.Builtin.FromNat
+import      Data.Integer.Literals as ℤ
+import      Data.Rational.Literals as ℚ
+open import Data.Rational.Literals using (fromℤ)
+instance Number-ℤ = ℤ.number
+instance Number-ℚ = ℚ.number
+open Number ℚ.number using () renaming (fromNat to fromℕ)
+
+-- Properties of 'floor'
+
+-- 'floor' is defined such that it typically does not normalize,
+-- but we can use its definition as a propositional equality.
+floor-def : ∀ (x : ℚ) → floor x ≡ ↥ x ℤ./ ↧ x
+floor-def x@record{} = refl
+
+-- A non-negative rational number has a non-negative numerator.
+0≤⇒0≤numerator : ∀ (x : ℚ) → 0 ≤ x → 0 ℤ.≤ ↥ x
+0≤⇒0≤numerator x 0≤x =
+  begin
+    0         ≡⟨ sym (*-zeroˡ (↧ x)) ⟩
+    0 ℤ.* ↧ x ≤⟨ drop-*≤* 0≤x ⟩
+    ↥ x ℤ.* 1 ≡⟨ *-identityʳ _ ⟩
+    ↥ x       ∎
+  where open ≤-Reasoning
+
+-- The 'floor' of a non-negative number is again non-negative.
+0≤⇒0≤floor : ∀ (x : ℚ) → 0 ≤ x → 0 ℤ.≤ floor x
+0≤⇒0≤floor x 0≤x =
+  begin
+    0             ≤⟨ 0≤n⇒0≤n/ℕd _ _ (0≤⇒0≤numerator x 0≤x) ⟩
+    (↥ x /ℕ ↧ₙ x) ≡⟨ sym (div-pos-is-/ℕ (↥ x) (↧ₙ x)) ⟩
+    (↥ x ℤ./ ↧ x) ≡⟨ sym (floor-def x) ⟩
+    floor x       ∎
+  where open ≤-Reasoning
+
+-- Properties related to non-negativity
+
+-- Any non-negative integer is a non-negative rational number.
+fromℤ-0≤ : ∀ (i : ℤ) → 0 ℤ.≤ i → 0 ≤ fromℤ i
+fromℤ-0≤ i 0≤i = *≤* (begin
+    0 ℤ.* i ≡⟨ sym (*-zeroˡ i) ⟩
+    0       ≤⟨ 0≤i ⟩
+    i       ≡⟨ sym (*-identityʳ i) ⟩
+    i ℤ.* 1 ∎)
+  where open ≤-Reasoning
+
+-- Any natural number is a non-negative rational number.
+fromℕ-0≤ : ∀ (n : ℕ) → 0 ≤ fromℕ n
+fromℕ-0≤ n = fromℤ-0≤ (ℤ.+ n) (+≤+ z≤n)
+
+-- The product of 2 non-negative numbers is non-negative.
+*-0≤⇒0≤ : ∀ (x y : ℚ) → 0 ≤ x → 0 ≤ y → 0 ≤ (x * y) 
+*-0≤⇒0≤ x y 0≤x 0≤y =
+  begin
+    0      ≡⟨ sym (*-zeroʳ x) ⟩
+    x * 0  ≤⟨ *-monoˡ-≤-nonNeg x ⦃ nonNegative 0≤x ⦄ 0≤y ⟩
+    x * y  ∎
+  where open ≤ℚ-Reasoning
+
+-- The product of 3 non-negative numbers is non-negative.
+*-0≤-3⇒0≤ : ∀ (x y z : ℚ) → 0 ≤ x → 0 ≤ y → 0 ≤ z → 0 ≤ (x * y * z) 
+*-0≤-3⇒0≤ x y z 0≤x 0≤y 0≤z =
+  *-0≤⇒0≤ (x * y) z (*-0≤⇒0≤ x y 0≤x 0≤y) 0≤z
+
+-- Division by a non-negative number 
+÷-0≤⇒0≤ : ∀ (x y : ℚ) → .{{_ : NonZero y}} → 0 ≤ x → 0 ≤ y → 0 ≤ x ÷ y 
+÷-0≤⇒0≤ x y 0≤x 0≤y = nonNegative⁻¹ (x ÷ y)
+  where
+    instance
+      lemma-1/y : Positive (1/ y)
+      lemma-1/y = 1/pos⇒pos y {{nonNeg∧nonZero⇒pos y {{nonNegative 0≤y}}}}
+
+      lemma-x÷y : NonNegative (x * 1/ y)
+      lemma-x÷y = nonNeg*nonNeg⇒nonNeg x {{nonNegative 0≤x}} (1/ y) {{pos⇒nonNeg (1/ y)}}

src/Ledger/Conway/Epoch.lagda

@@ -5,16 +5,21 @@
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 
-open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid)
 open import Data.Integer using () renaming (+_ to pos)
+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.Rational using (ℚ; floor; _*_; _÷_; _/_)
+open import Data.Rational using (ℚ; floor; _*_; _÷_; _/_; _⊓_; _≟_; ≢-nonZero)
 open import Data.Rational.Literals using (number; fromℤ)
-import      Data.Rational as ℚ renaming (_⊓_ to min)
+open import Data.Rational.Properties using (nonNegative⁻¹; pos⇒nonNeg; ⊓-glb)
+open import stdlib.Data.Rational.Properties using (0≤⇒0≤floor; ÷-0≤⇒0≤; fromℕ-0≤; *-0≤⇒0≤; fromℤ-0≤)
+
+open import Data.Integer.Tactic.RingSolver using (solve-∀)
 
 open import Agda.Builtin.FromNat
 
-open import Ledger.Prelude hiding (iterate; _/_; _*_)
+open import Ledger.Prelude hiding (iterate; _/_; _*_; _⊓_; _≟_; ≢-nonZero)
 open Filter using (filter)
 open import Ledger.Conway.Abstract
 open import Ledger.Conway.Transaction
@@ -71,6 +76,12 @@ instance
 
   Hastreasury-EpochState : Hastreasury EpochState
   Hastreasury-EpochState .treasuryOf = Acnt.treasury ∘ EpochState.acnt
+
+  Hasreserves-EpochState : Hasreserves EpochState
+  Hasreserves-EpochState .reservesOf = Acnt.reserves ∘ EpochState.acnt
+
+  HasPParams-EpochState : HasPParams EpochState
+  HasPParams-EpochState .PParamsOf = PParamsOf ∘ EnactStateOf
 \end{code}
 \begin{NoConway}
 \begin{code}
@@ -117,13 +128,10 @@ instance
   HasRewards-NewEpochState : HasRewards NewEpochState
   HasRewards-NewEpochState .RewardsOf = RewardsOf ∘ CertStateOf
 
-  unquoteDecl HasCast-RewardUpdate HasCast-EpochState HasCast-NewEpochState = derive-HasCast
-    (   (quote RewardUpdate   , HasCast-RewardUpdate)
-    ∷   (quote EpochState     , HasCast-EpochState)
+  unquoteDecl HasCast-EpochState HasCast-NewEpochState = derive-HasCast
+    ( (quote EpochState     , HasCast-EpochState)
     ∷ [ (quote NewEpochState  , HasCast-NewEpochState)])
 
-instance _ = +-0-monoid; _ = +-0-commutativeMonoid
-
 toRwdAddr : Credential → RwdAddr
 toRwdAddr x = record { net = NetworkId ; stake = x }
 
@@ -175,35 +183,85 @@ described in \textcite[\sectionname~6.4]{shelley-delegation-design}.
 \begin{figure*}[h]
 \begin{AgdaMultiCode}
 \begin{code}
-
 createRUpd : ℕ → BlocksMade → EpochState → Coin → RewardUpdate
-createRUpd slotsPerEpoch b es total
-  = ⟦ Δt₁ , 0 - Δr₁ + Δr₂ , 0 - feeSS , rs ⟧
+createRUpd slotsPerEpoch b es total =
+  record  { Δt = Δt₁
+          ; Δr = 0 - Δr₁ + Δr₂
+          ; Δf = 0 - pos feeSS
+          ; rs = rs
+\end{code}
+\begin{code}[hide]
+          ; flowConservation = flowConservation
+          ; Δt-nonnegative = Δt-nonneg
+          ; Δf-nonpositive = Δf-nonpos
+\end{code}
+\begin{code}
+          }
   where
-    prevPp      = PParamsOf (es .EpochState.es)
-    reserves    = es .EpochState.acnt .Acnt.reserves
-    pstakego    = es .EpochState.ss .Snapshots.go
-    feeSS       = es .EpochState.ss .Snapshots.feeSS
-    stake       = pstakego .Snapshot.stake
-    delegs      = pstakego .Snapshot.delegations
-    poolParams  = pstakego .Snapshot.poolParameters
-
-    blocksMade = ∑[ m ← b ] m
-
-    rho = fromUnitInterval (prevPp .PParams.monetaryExpansion)
-    η = fromℕ blocksMade ÷₀ (fromℕ slotsPerEpoch * ActiveSlotCoeff)
-    Δr₁ = floor (ℚ.min 1 η * rho * fromℕ reserves)
-
-    rewardPot = pos feeSS + Δr₁
-    tau = fromUnitInterval (prevPp .PParams.treasuryCut)
-    Δt₁ = floor (tau * fromℤ rewardPot)
-    R = posPart (rewardPot - Δt₁)
-    circulation = total - reserves
-
-    rs = reward prevPp b R poolParams stake delegs circulation
-    Δr₂ = R - ∑[ c ← rs ] c
+    prevPp       = PParamsOf es
+    reserves     = reservesOf es
+    pstakego     = es .EpochState.ss .Snapshots.go
+    feeSS        = es .EpochState.ss .Snapshots.feeSS
+    stake        = pstakego .Snapshot.stake
+    delegs       = pstakego .Snapshot.delegations
+    poolParams   = pstakego .Snapshot.poolParameters
+    blocksMade   = ∑[ m ← b ] m
+    ρ            = fromUnitInterval (prevPp .PParams.monetaryExpansion)
+    η            = fromℕ blocksMade ÷₀ (fromℕ slotsPerEpoch * ActiveSlotCoeff)
+    Δr₁          = floor (1 ⊓ η * ρ * fromℕ reserves)
+    rewardPot    = pos feeSS + Δr₁
+    τ            = fromUnitInterval (prevPp .PParams.treasuryCut)
+    Δt₁          = floor (fromℤ rewardPot * τ)
+    R            = rewardPot - Δt₁
+    circulation  = total - reserves
+    rs           = reward prevPp b (posPart R) poolParams stake delegs circulation
+    Δr₂          = R - pos (∑[ c ← rs ] c)
 
 \end{code}
+\begin{code}[hide]
+    -- Proofs
+    -- Note: Overloading of + and - seems to interfere with
+    -- the ring solver.
+    lemmaFlow : ∀ (t₁ r₁ f z : ℤ)
+      → (t₁ ℤ.+ (0 ℤ.- r₁ ℤ.+ ((f ℤ.+ r₁ ℤ.- t₁) ℤ.- z)) ℤ.+ (0 ℤ.- f) ℤ.+ z) ≡ 0
+    lemmaFlow = solve-∀
+    flowConservation = lemmaFlow Δt₁ Δr₁ (pos feeSS) (pos (∑[ c ← rs ] c))
+
+    ÷₀-0≤⇒0≤ : ∀ (x y : ℚ) → 0 ≤ x → 0 ≤ y → 0 ≤ (x ÷₀ y)
+    ÷₀-0≤⇒0≤ x y 0≤x 0≤y with y ≟ 0
+    ... | (yes y≡0) = nonNegative⁻¹ 0
+    ... | (no y≢0)  = ÷-0≤⇒0≤ x y {{≢-nonZero y≢0}} 0≤x 0≤y
+
+    η-nonneg : 0 ≤ η
+    η-nonneg = ÷₀-0≤⇒0≤ _ _ (fromℕ-0≤ blocksMade)
+      (*-0≤⇒0≤ _ _
+        (fromℕ-0≤ slotsPerEpoch)
+        (nonNegative⁻¹ ActiveSlotCoeff {{pos⇒nonNeg ActiveSlotCoeff}}))
+
+    min1η-nonneg : 0 ≤ 1 ⊓ η
+    min1η-nonneg = ⊓-glb (nonNegative⁻¹ 1) η-nonneg
+
+    Δr₁-nonneg : 0 ≤ Δr₁
+    Δr₁-nonneg = 0≤⇒0≤floor _
+      (*-0≤⇒0≤ (1 ⊓ η * ρ) (fromℕ reserves)
+        (UnitInterval-*-0≤ (1 ⊓ η) (prevPp .PParams.monetaryExpansion) min1η-nonneg)
+        (fromℕ-0≤ reserves))
+
+    rewardPot-nonneg : 0 ≤ rewardPot
+    rewardPot-nonneg = +-mono-≤ (nonNegative⁻¹ℤ (pos feeSS)) Δr₁-nonneg
+
+    Δt-nonneg : 0 ≤ Δt₁
+    Δt-nonneg = 0≤⇒0≤floor _
+      (UnitInterval-*-0≤ (fromℤ rewardPot) (prevPp .PParams.treasuryCut)
+        (fromℤ-0≤ rewardPot rewardPot-nonneg))
+
+    Δf-nonpos : (0 - pos feeSS) ≤ 0
+    Δf-nonpos = begin
+        0 - pos feeSS ≡⟨ +-identityˡ _ ⟩
+        ℤ.- pos feeSS ≤⟨ neg-mono-≤ (ℤ.+≤+ z≤n) ⟩
+        0             ∎
+      where open ≤-Reasoning
+\end{code}
 \end{AgdaMultiCode}
 \caption{RewardUpdate Creation}
 \label{fig:functions:createRUpd}
@@ -215,7 +273,7 @@ createRUpd slotsPerEpoch b es total
 {\small
 \begin{code}
 applyRUpd : RewardUpdate → EpochState → EpochState
-applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
+applyRUpd rewardUpdate
   ⟦ ⟦ treasury , reserves ⟧ᵃ
   , ss
   , ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ
@@ -233,6 +291,7 @@ applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
   , es
   , fut ⟧
   where
+    open RewardUpdate rewardUpdate using (Δt; Δr; Δf; rs)
     regRU     = rs ∣ dom rewards
     unregRU   = rs ∣ dom rewards ᶜ
     unregRU'  = ∑[ x ← unregRU ] x

src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda

@@ -2,6 +2,8 @@ open import Ledger.Conway.Foreign.ExternalFunctions
 
 module Ledger.Conway.Foreign.HSLedger.ExternalStructures (externalFunctions : ExternalFunctions) where
 
+import      Data.Rational as ℚ using (pos) -- import an instance
+
 open import Ledger.Conway.Crypto
 open import Ledger.Conway.Types.Epoch
 open import Ledger.Conway.Foreign.HSLedger.Core

src/Ledger/Conway/PParams.lagda

@@ -56,6 +56,10 @@ record Hastreasury {a} (A : Type a) : Type a where
   field treasuryOf : A → Coin
 open Hastreasury ⦃...⦄ public
 
+record Hasreserves {a} (A : Type a) : Type a where
+  field reservesOf : A → Coin
+open Hasreserves ⦃...⦄ public
+
 ProtVer : Type
 ProtVer = ℕ × ℕ