Add governance action deposit vote delegation (#101)

src/Axiom/Set.agda

@@ -134,6 +134,9 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
   ∈-map : ∀ {f : A → B} {b} → (∃[ a ] b ≡ f a × a ∈ X) ⇔ b ∈ map f X
   ∈-map = proj₂ $ replacement _ _
 
+  ∈-map′ : ∀ {f : A → B} {a} → a ∈ X → f a ∈ map f X
+  ∈-map′ {a = a} a∈X = to ∈-map (a , refl , a∈X)
+
   -- don't know that there's a set containing all members of a type, which this is equivalent to
   -- _⁻¹_ : (A → B) → Set B → Set A
   -- f ⁻¹ X = {!!}
@@ -203,6 +206,11 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
     y ∈ mapPartial f X ∎
     where open R.EquationalReasoning
 
+  ⊆-mapPartial : ∀ {f : A → Maybe B} → map just (mapPartial f X) ⊆ map f X
+  ⊆-mapPartial {f = f} a∈m with from ∈-map a∈m
+  ... | x , refl , a∈mp with from (∈-mapPartial {f = f}) a∈mp
+  ... | x' , x'∈X , jx≡fx = to ∈-map (x' , sym jx≡fx , x'∈X)
+
   binary-unions : ∃[ Y ] ∀ {a} → (a ∈ X ⊎ a ∈ X') ⇔ a ∈ Y
   binary-unions {X = X} {X'} with unions (fromList (X ∷ [ X' ]))
   ... | (Y , h) = Y , mk⇔ (λ where

src/Axiom/Set/Map.agda

@@ -13,9 +13,11 @@ open import Prelude hiding (filter)
 
 import Data.Product
 import Data.Sum
+import Relation.Binary.PropositionalEquality as I
 open import Data.These
 open import Data.List.Ext.Properties
 open import Data.Product.Properties
+open import Data.Maybe.Base using () renaming (map to map?)
 open import Interface.DecEq
 open import Relation.Unary using () renaming (Decidable to Dec₁)
 
@@ -35,6 +37,10 @@ private macro
 private variable A A' B B' C D : Type
                  R R' : Rel A B
                  X Y : Set A
+                 a : A
+                 a' : A'
+                 b : B
+                 b' : B'
 
 left-unique : Rel A B → Type
 left-unique R = ∀ {a b b'} → (a , b) ∈ R → (a , b') ∈ R → b ≡ b'
@@ -154,16 +160,23 @@ disj-dom {m = m@(_ , uniq)} {m₁} {m₂} (m≡m₁∪m₂ , disj) a∈domm₁ a
     ∈mᵢ⇒∈m : ∀ {a} → a ∈ (m₁ ˢ) ⊎ a ∈ (m₂ ˢ) → a ∈ (m ˢ)
     ∈mᵢ⇒∈m = proj₂ m≡m₁∪m₂ ∘ to ∈-∪
 
-mapˡ-uniq : {f : A → A'} → Injective _≡_ _≡_ f → left-unique R → left-unique (mapˡ f R)
+InjectiveOn : Set A → (A → B) → Type
+InjectiveOn X f = ∀ {x y} → x ∈ X → y ∈ X → f x ≡ f y → x ≡ y
+
+weaken-Injective : ∀ {X : Set A} {f : A → B} → Injective _≡_ _≡_ f → InjectiveOn X f
+weaken-Injective p _ _ = p
+
+mapˡ-uniq : {f : A → A'} → InjectiveOn (dom R) f → left-unique R → left-unique (mapˡ f R)
 mapˡ-uniq inj uniq = λ h h' → case ∈⇔P h ,′ ∈⇔P h' of λ where
-  ((_ , refl , Ha) , (_ , eqb , Hb)) → uniq Ha $ subst _ (sym $ ×-≡,≡→≡ $ Data.Product.map₁ inj (×-≡,≡←≡ eqb)) Hb
+  (((_ , b) , refl , Ha) , ((_ , b') , eqb , Hb)) → uniq Ha
+    $ subst _ (sym $ ×-≡,≡→≡ $ Data.Product.map₁ (inj (from dom∈ (b , Ha)) (from dom∈ (b' , Hb))) (×-≡,≡←≡ eqb)) Hb
 
 mapʳ-uniq : {f : B → B'} → left-unique R → left-unique (mapʳ f R)
 mapʳ-uniq uniq = λ h h' → case ∈⇔P h ,′ ∈⇔P h' of λ where
   ((_ , refl , Ha) , (_ , refl , Hb)) → cong _ $ uniq Ha Hb
 
-mapKeys : (f : A → A') → Injective _≡_ _≡_ f → Map A B → Map A' B
-mapKeys f inj (R , uniq) = mapˡ f R , mapˡ-uniq inj uniq
+mapKeys : (f : A → A') → (m : Map A B) → InjectiveOn (dom (m ˢ)) f → Map A' B
+mapKeys f (R , uniq) inj = mapˡ f R , mapˡ-uniq inj uniq
 
 mapValues : (B → B') → Map A B → Map A B'
 mapValues f (R , uniq) = mapʳ f R , mapʳ-uniq uniq
@@ -184,6 +197,23 @@ m ∣' P? = filterᵐ (sp-∘ P? proj₁) m
 _∣^'_ : {P : B → Type} → Map A B → specProperty P → Map A B
 m ∣^' P? = filterᵐ (sp-∘ P? proj₂) m
 
+mapPartialLiftKey-just-uniq : ∀ {f : A → B → Maybe B'}
+  → left-unique R
+  → just (a , b) ∈ mapˢ (mapPartialLiftKey f) R
+  → just (a , b') ∈ mapˢ (mapPartialLiftKey f) R
+  → b ≡ b'
+mapPartialLiftKey-just-uniq {f = f} prop a∈ a'∈ with mapPartialLiftKey-map {f = f} a∈ | mapPartialLiftKey-map {f = f} a'∈
+... | _ , eq , ax∈r | _ , eq' , ax'∈r with prop ax∈r ax'∈r
+... | refl with trans eq (sym eq')
+... | refl = refl
+
+mapPartial-uniq : ∀ {r : Rel A B} {f : A → B → Maybe B' } → left-unique r → left-unique (mapPartial (mapPartialLiftKey f) r)
+mapPartial-uniq {f = f} prop {a} {b} {b'} p q with ∈-map′ p | ∈-map′ q
+... | p | q = mapPartialLiftKey-just-uniq {f = f} prop (⊆-mapPartial p) (⊆-mapPartial q)
+
+mapMaybeWithKeyᵐ : (A → B → Maybe B') → Map A B → Map A B'
+mapMaybeWithKeyᵐ f (rel , prop) = mapMaybeWithKey f rel , mapPartial-uniq {f = f} prop 
+
 module Restrictionᵐ (sp-∈ : spec-∈ A) where
   private module R = Restriction sp-∈
   open Unionᵐ sp-∈
@@ -244,5 +274,5 @@ module Corestrictionᵐ (sp-∈ : spec-∈ B) where
 
   -- f⁻¹(x)
   infix 25 _⁻¹_
-  _⁻¹_ : ⦃ DecEq B ⦄ → Map A B → B → Set A
+  _⁻¹_ : Map A B → B → Set A
   m ⁻¹ a = dom ((m ∣^ ❴ a ❵) ˢ)

src/Axiom/Set/Map/Dec.agda

@@ -24,6 +24,7 @@ private variable A B C D : Type
 
 module Lookupᵐᵈ (sp-∈ : spec-∈ A) where
   open Lookupᵐ sp-∈
+  infixr 6 _∪⁺_
 
   unionThese : ⦃ DecEq A ⦄ → (m : Map A B) → (m' : Map A C) → (x : A) → x ∈ dom (m ˢ) ∪ dom (m' ˢ) → These B C
   unionThese m m' x dp with x ∈? dom (m ˢ) | x ∈? dom (m' ˢ)

src/Axiom/Set/Rel.agda

@@ -17,10 +17,12 @@ import Data.Sum
 open import Data.These hiding (map)
 open import Data.List.Ext.Properties
 open import Data.Product.Properties
+open import Data.Maybe.Base using () renaming (map to map?)
 open import Interface.DecEq
 open import Relation.Unary using () renaming (Decidable to Dec₁)
 open import Relation.Nullary
 open import Relation.Binary hiding (Rel)
+import Relation.Binary.PropositionalEquality as I
 
 open Equivalence
 
@@ -98,6 +100,25 @@ mapʳ-dom = dom-⊆mapʳ , dom-mapʳ⊆
 dom-∅ : dom R ⊆ ∅ → R ≡ᵉ ∅
 dom-∅ dom⊆∅ = ∅-least (λ {x} x∈R → ⊥-elim $ ∉-∅ $ dom⊆∅ $ from dom∈ (-, x∈R))
 
+mapPartialLiftKey : (A → B → Maybe B') → A × B → Maybe (A × B')
+mapPartialLiftKey f (k , v) = map? (k ,_) (f k v)
+
+mapPartialLiftKey-map : ∀ {a : A} {b' : B'} {f : A → B → Maybe B'} {r : Rel A B}
+  → just (a , b') ∈ map (mapPartialLiftKey f) r
+  → ∃[ b ] just b' ≡ f a b × (a , b) ∈ r
+mapPartialLiftKey-map {f = f} ab∈m with from ∈-map ab∈m
+... | (a' , b') , ≡ , a'b'∈r with f a' b' | inspect (f a') b'
+mapPartialLiftKey-map {f = f} ab∈m | (a' , b') , refl , a'b'∈r | just x | I.[ eq ] = b' , sym eq , a'b'∈r
+
+mapMaybeWithKey : (A → B → Maybe B') → Rel A B → Rel A B'
+mapMaybeWithKey f r = mapPartial (mapPartialLiftKey f) r
+
+∈-mapMaybeWithKey : ∀ {a : A} {b' : B'} {f : A → B → Maybe B'} {r : Rel A B}
+  → (a , b') ∈ mapMaybeWithKey f r
+  → ∃[ b ] (just b' ≡ f a b × (a , b) ∈ r)
+∈-mapMaybeWithKey {a = a} {b'} {f} ab'∈ with to (∈-map {f = just}) ((a , b') , refl , ab'∈)
+... | p = mapPartialLiftKey-map {f = f} (⊆-mapPartial p)
+
 module Restriction (sp-∈ : spec-∈ A) where
 
   _∣_ : Rel A B → Set A → Rel A B

src/Ledger/Chain.lagda

@@ -17,6 +17,9 @@ open import Ledger.PPUp txs
 open import Ledger.Utxo txs
 open import Ledger.Ratify txs
 open import Ledger.Tally TxId Network ADHash epochStructure ppUpd ppHashingScheme crypto
+open Equivalence
+open import Data.Nat.Properties using (+-0-monoid)
+open import Data.Maybe.Base using () renaming (map to map?)
 
 \end{code}
 \begin{figure*}[h]
@@ -34,7 +37,6 @@ record NewEpochState : Set where
 
 record ChainState : Set where
   field newEpochState  : NewEpochState
-        stakeDistrs    : StakeDistrs -- TODO: compute this from LState instead
 
 record Block : Set where
   field ts   : List Tx
@@ -89,12 +91,51 @@ data _⊢_⇀⦇_,NEWEPOCH⦈_ : NewEpochEnv → NewEpochState → Epoch → New
 \end{figure*}
 
 \begin{code}[hide]
+maybePurpose : DepositPurpose → (DepositPurpose × Credential) → Coin → Maybe Coin
+maybePurpose prps (prps' , _) c with prps ≟ prps'
+... | yes _ = just c
+... | no _ = nothing
+
+maybePurpose-prop : ∀ {prps} {x} {y}
+  → (m : (DepositPurpose × Credential) ↛ Coin)
+  → (x , y) ∈ dom ((mapMaybeWithKeyᵐ (maybePurpose prps) m) ˢ)
+  → x ≡ prps
+maybePurpose-prop {prps = prps} {x} {y} _ xy∈dom with to dom∈ xy∈dom
+... | z , ∈mmwk with prps ≟ x | ∈-mapMaybeWithKey {f = maybePurpose prps} ∈mmwk
+... | yes refl | _ = refl
+
+filterPurpose : DepositPurpose → (DepositPurpose × Credential) ↛ Coin → Credential ↛ Coin
+filterPurpose prps m = mapKeys proj₂ (mapMaybeWithKeyᵐ (maybePurpose prps) m) λ where
+  {x , .z} {y , z} x∈dom y∈dom refl → case maybePurpose-prop {prps = prps} m x∈dom of λ where
+    x≡prps → case maybePurpose-prop {prps = prps} m y∈dom of λ where
+      refl → cong (_, z) x≡prps
+
+instance
+  _ = +-0-monoid
+
+calculateStakeDistrs : LState → StakeDistrs
+calculateStakeDistrs ls =
+  let open LState ls; open CertState certState; open PState pState; open UTxOState utxoSt; open DState dState
+      spoDelegs = ∅ᵐ -- TODO
+      drepDelegs = ∅ᵐ -- TODO
+      govActionDeposits = foldl _∪⁺_ ∅ᵐ $ setToList $
+        mapPartial
+          (λ where record { returnAddr = record {stake = c} ; deposit = v } → map? (λ vd → ❴ vd , v ❵ᵐ) (lookupᵐ? voteDelegs c ⦃ _ ∈? _ ⦄))
+          (range (tally ˢ))
+  in
+  record
+    { stakeDistr = govActionDeposits
+    }
+
 data _⊢_⇀⦇_,CHAIN⦈_ : ⊤ → ChainState → Block → ChainState → Set where
 \end{code}
 \begin{figure*}[h]
 \begin{code}
-  CHAIN : let open ChainState s; open Block b; open NewEpochState in
-    record { ChainState s } ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
+  CHAIN :
+    let open ChainState s; open Block b; open NewEpochState
+        stakeDistrs = calculateStakeDistrs (ls nes)
+    in
+    record { stakeDistrs = stakeDistrs ; ChainState s } ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
     → ⟦ slot , EnactState.pparams (es nes) ⟧ˡᵉ ⊢ ls nes ⇀⦇ ts ,LEDGERS⦈ ls'
     ────────────────────────────────
     _ ⊢ s ⇀⦇ b ,CHAIN⦈ record s { newEpochState = record nes { ls = ls' } }

src/Ledger/Deleg.lagda

@@ -31,7 +31,6 @@ open EpochStructure epochStructure
 \begin{code}
 record PoolParams : Set where
   field rewardAddr  : Credential
-        deposit     : Coin
 
 data DCert : Set where
   delegate   : Credential → Maybe VDeleg → Maybe Credential → Coin → DCert
@@ -117,8 +116,7 @@ data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Set w
 
 data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set where
   POOL-regpool : let open PParams pp ; open PoolParams poolParams in
-    deposit ≡ poolDeposit
-    → c ∉ dom (pools ˢ)
+    c ∉ dom (pools ˢ)
     ────────────────────────────────
     pp ⊢ ⟦ pools , retiring ⟧ᵖ ⇀⦇ regpool c poolParams ,POOL⦈ ⟦ ❴ c , poolParams ❵ᵐ ∪ᵐˡ pools , retiring ⟧ᵖ
 

src/Ledger/Ratify.lagda

@@ -124,7 +124,7 @@ module _ (ce : Epoch) (ccHotKeys : KeyHash ↛ Maybe KeyHash)
 
   actualCCVotes : Credential ↛ Vote
   actualCCVotes = case cc of λ where
-    (just (cc , _)) → mapKeys inj₁ (λ where refl → refl) $ mapWithKey actualCCVote cc
+    (just (cc , _)) → mapKeys inj₁ (mapWithKey actualCCVote cc) (λ where _ _ refl → refl)
     nothing         → ∅ᵐ
 
   actualPDRepVotes : VDeleg ↛ Vote
@@ -134,9 +134,9 @@ module _ (ce : Epoch) (ccHotKeys : KeyHash ↛ Maybe KeyHash)
                                            _            → Vote.no) ❵ᵐ
 
   actualVotes : VDeleg ↛ Vote
-  actualVotes = mapKeys (credVoter CC) (λ where refl → refl) actualCCVotes
+  actualVotes = mapKeys (credVoter CC) actualCCVotes (λ where _ _ refl → refl)
               ∪ᵐˡ (actualPDRepVotes
-              ∪ᵐˡ mapKeys (uncurry credVoter) (λ where refl → refl) votes) -- TODO: make `actualVotes` for DRep, SPO
+              ∪ᵐˡ mapKeys (uncurry credVoter) votes (λ where _ _ refl → refl)) -- TODO: make `actualVotes` for DRep, SPO
 
 votedHashes : Vote → (VDeleg ↛ Vote) → GovRole → ℙ VDeleg
 votedHashes v votes r = votes ⁻¹ v

src/Ledger/Utxo.lagda

@@ -78,7 +78,7 @@ The UTxO transition system is given in Figure~\ref{fig:rules:utxo-shelley}.
 \begin{figure*}[h]
 \begin{code}
 outs : TxBody → UTxO
-outs tx = mapKeys (txid tx ,_) (λ where refl → refl) $ txouts tx
+outs tx = mapKeys (txid tx ,_) (txouts tx) λ where _ _ refl → refl
 
 balance : UTxO → Value
 balance utxo = Σᵐ[ x ← utxo ᶠᵐ ] proj₂ (proj₂ x)
@@ -95,14 +95,14 @@ data DepositPurpose : Set where
   PoolDeposit        : DepositPurpose
   DRepDeposit        : DepositPurpose
 
-certDeposit : DCert → Maybe (DepositPurpose × Credential × Coin)
-certDeposit (delegate c _ _ v)                  = just (CredentialDeposit , c , v)
-certDeposit (regpool c record { deposit = v })  = just (PoolDeposit       , c , v)
-certDeposit (regdrep c v)                       = just (DRepDeposit       , c , v)
-certDeposit _                                   = nothing
+certDeposit : PParams → DCert → Maybe (DepositPurpose × Credential × Coin)
+certDeposit _  (delegate c _ _ v)  = just (CredentialDeposit , c , v)
+certDeposit pp (regpool c _)       = just (PoolDeposit       , c , PParams.poolDeposit pp)
+certDeposit _  (regdrep c v)       = just (DRepDeposit       , c , v)
+certDeposit _  _                   = nothing
 
-certDepositᵐ : DCert → (DepositPurpose × Credential) ↛ Coin
-certDepositᵐ cert = case certDeposit cert of λ where
+certDepositᵐ : PParams → DCert → (DepositPurpose × Credential) ↛ Coin
+certDepositᵐ pp cert = case certDeposit pp cert of λ where
   (just (p , c , v))  → ❴ (p , c) , v ❵ᵐ
   nothing             → ∅ᵐ
 
@@ -153,34 +153,34 @@ record UTxOState : Set where
         fees      : Coin
         deposits  : (DepositPurpose × Credential) ↛ Coin
 
-updateDeposits : List DCert → (DepositPurpose × Credential) ↛ Coin → (DepositPurpose × Credential) ↛ Coin
-updateDeposits []              deposits = deposits
-updateDeposits (cert ∷ certs)  deposits =
-  ((updateDeposits certs deposits) ∪⁺ certDepositᵐ cert) ∣ certRefundˢ cert ᶜ
+updateDeposits : PParams → List DCert → (DepositPurpose × Credential) ↛ Coin → (DepositPurpose × Credential) ↛ Coin
+updateDeposits _  []              deposits = deposits
+updateDeposits pp (cert ∷ certs)  deposits =
+  ((updateDeposits pp certs deposits) ∪⁺ certDepositᵐ pp cert) ∣ certRefundˢ cert ᶜ
 
-depositsChange : List DCert → (DepositPurpose × Credential) ↛ Coin → ℤ
-depositsChange certs deposits = getCoin (updateDeposits certs deposits) ⊖ getCoin deposits
+depositsChange : PParams → List DCert → (DepositPurpose × Credential) ↛ Coin → ℤ
+depositsChange pp certs deposits = getCoin (updateDeposits pp certs deposits) ⊖ getCoin deposits
 
 -- refundedDeposits : TxBody → ℙ (DepositPurpose × Credential)
 -- refundedDeposits = mapPartial certRefund ∘ fromList ∘ txcerts
 
-depositRefunds : UTxOState → TxBody → Coin
-depositRefunds st txb = negPart $ depositsChange (txcerts txb) deposits
+depositRefunds : PParams → UTxOState → TxBody → Coin
+depositRefunds pp st txb = negPart $ depositsChange pp (txcerts txb) deposits
   where open UTxOState st
 
-newDeposits : UTxOState → TxBody → Coin
-newDeposits st txb = posPart $ depositsChange (txcerts txb) deposits
+newDeposits : PParams → UTxOState → TxBody → Coin
+newDeposits pp st txb = posPart $ depositsChange pp (txcerts txb) deposits
   where open UTxOState st
 
 consumed : PParams → UTxOState → TxBody → Value
 consumed pp st txb = balance (UTxOState.utxo st ∣ txins txb)
                    +ᵛ mint txb
-                   +ᵛ inject (depositRefunds st txb)
+                   +ᵛ inject (depositRefunds pp st txb)
 
 produced : PParams → UTxOState → TxBody → Value
 produced pp st txb = balance (outs txb)
                    +ᵛ inject (txfee txb)
-                   +ᵛ inject (newDeposits st txb)
+                   +ᵛ inject (newDeposits pp st txb)
 \end{code}
 \emph{UTxO transitions}
 
@@ -270,7 +270,8 @@ data _⊢_⇀⦇_,UTXO⦈_ where
     Γ ⊢ s ⇀⦇ tx ,UTXO⦈
         ⟦ (utxo ∣ txins tx ᶜ) ∪ᵐˡ outs tx
         , fees + f
-        , updateDeposits (txcerts tx) deposits ⟧ᵘ
+        , updateDeposits pp (txcerts tx) deposits
+        ⟧ᵘ
 \end{code}
 \begin{code}[hide]
 -- TODO: This can't be moved into Properties because it breaks. Move