Improve hashing

src/Ledger/Abstract.agda

@@ -6,6 +6,7 @@ open import Ledger.Transaction
 module Ledger.Abstract (txs : TransactionStructure) where
 
 open TransactionStructure txs
+open import Ledger.Delegation govStructure
 
 record indexOf : Type where
   field

src/Ledger/Certs.lagda

@@ -6,67 +6,25 @@
 open import Ledger.Prelude
 open import Ledger.Types.GovStructure
 
-module Ledger.Certs (gs : _) (open GovStructure gs) where
+module Ledger.Certs
+  (gs : _) (open GovStructure gs)
+  where
 
 open import Tactic.Derive.DecEq
 
 open import Ledger.GovernanceActions gs
 open RwdAddr
+open import Ledger.Delegation gs
 \end{code}
 
 \begin{figure*}[h]
 \emph{Derived types}
-\begin{code}
-data DepositPurpose : Type where
-  CredentialDeposit  : Credential   → DepositPurpose
-  PoolDeposit        : KeyHash      → DepositPurpose
-  DRepDeposit        : Credential   → DepositPurpose
-  GovActionDeposit   : GovActionID  → DepositPurpose
-
-Deposits = DepositPurpose ⇀ Coin
-\end{code}
-\begin{code}[hide]
-instance
-  unquoteDecl DecEq-DepositPurpose = derive-DecEq
-    ((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])
-\end{code}
 \caption{Deposit types}
 \end{figure*}
 
 \begin{figure*}[h!]
 \begin{AgdaMultiCode}
 \begin{NoConway}
-\begin{code}
-record PoolParams : Type where
-\end{code}
-\begin{code}[hide]
-  field
-\end{code}
-\begin{code}
-    rewardAddr : Credential
-\end{code}
-\end{NoConway}
-\begin{code}
-data DCert : Type where
-  delegate    : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
-  dereg       : Credential → Coin → DCert
-  regpool     : KeyHash → PoolParams → DCert
-  retirepool  : KeyHash → Epoch → DCert
-  regdrep     : Credential → Coin → Anchor → DCert
-  deregdrep   : Credential → Coin → DCert
-  ccreghot    : Credential → Maybe Credential → DCert
-\end{code}
-\begin{NoConway}
-\begin{code}
-cwitness : DCert → Credential
-cwitness (delegate c _ _ _)  = c
-cwitness (dereg c _)         = c
-cwitness (regpool kh _)      = KeyHashObj kh
-cwitness (retirepool kh _)   = KeyHashObj kh
-cwitness (regdrep c _ _)     = c
-cwitness (deregdrep c _)     = c
-cwitness (ccreghot c _)      = c
-\end{code}
 \end{NoConway}
 \end{AgdaMultiCode}
 \caption{Delegation definitions}
@@ -147,7 +105,6 @@ record DelegEnv : Type where
     pools    : KeyHash ⇀ PoolParams
     deposits : Deposits
 
-GovCertEnv  = CertEnv
 PoolEnv     = PParams
 \end{code}
 \end{AgdaMultiCode}
@@ -278,7 +235,7 @@ data
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,GOVCERT⦈_   : GovCertEnv → GState → DCert → GState → Type
+  _⊢_⇀⦇_,GOVCERT⦈_   : CertEnv → GState → DCert → GState → Type
 \end{code}
 \begin{code}[hide]
 data
@@ -441,3 +398,23 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
 \caption{CERTS rules}
 \label{fig:sts:certs}
 \end{figure*}
+\begin{code}[hide]
+open import Ledger.Types.CertsStructure gs
+open import Agda.Builtin.FromNat
+
+CertsStructureˢ : CertsStructure
+CertsStructureˢ = record
+  { CertEnv = CertEnv
+  ; DelegEnv = DelegEnv
+  ; CertState = CertState
+  ; _⊢_⇀⦇_,CERTS⦈_ = _⊢_⇀⦇_,CERTS⦈_
+  ; DState = DState
+  ; stakeDelegs = DState.stakeDelegs
+  ; rewards = DState.rewards
+  ; dState = CertState.dState
+  ; pState = CertState.pState
+  ; PState = PState
+  ; retiring = PState.retiring
+  ; voteDelegs = DState.voteDelegs
+  }
+\end{code}

src/Ledger/Certs/Haskell.agda

@@ -7,15 +7,15 @@ module Ledger.Certs.Haskell
   (gs : _) (open GovStructure gs)
   where
 
+open import Ledger.Delegation gs
 open import Ledger.Certs gs
-  using (Deposits; PState; PoolParams; DCert; DepositPurpose; _⊢_⇀⦇_,POOL⦈_; DecEq-DepositPurpose; PoolEnv)
-open DCert
-open DepositPurpose
+  using (PState; _⊢_⇀⦇_,POOL⦈_; PoolEnv; ⟦_,_⟧ᵖ)
 
 open import Tactic.Derive.DecEq
 
 open import Ledger.GovernanceActions gs
 open RwdAddr
+open import Agda.Builtin.FromNat
 
 record CertEnv : Type where
   constructor ⟦_,_,_,_⟧ᶜ
@@ -187,3 +187,21 @@ data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState →
 
 _⊢_⇀⦇_,CERTS⦈_     : CertEnv → CertState → List DCert → CertState → Type
 _⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ _⊢_⇀⦇_,CERTBASE⦈_ _⊢_⇀⦇_,CERT⦈_
+
+open import Ledger.Types.CertsStructure gs
+
+CertsStructureʰ : CertsStructure
+CertsStructureʰ = record
+  { CertEnv = CertEnv
+  ; DelegEnv = DelegEnv
+  ; CertState = CertState
+  ; _⊢_⇀⦇_,CERTS⦈_ = _⊢_⇀⦇_,CERTS⦈_
+  ; DState = DState
+  ; stakeDelegs = DState.stakeDelegs
+  ; rewards = DState.rewards
+  ; dState = CertState.dState
+  ; pState = CertState.pState
+  ; PState = PState
+  ; retiring = PState.retiring
+  ; voteDelegs = DState.voteDelegs
+  }

src/Ledger/Certs/Properties.agda

@@ -12,6 +12,7 @@ module Ledger.Certs.Properties (gs : _) (open GovStructure gs) where
 
 open import Ledger.GovernanceActions gs hiding (yes; no)
 open import Ledger.Certs gs
+open import Ledger.Delegation gs
 
 open Computational ⦃...⦄
 

src/Ledger/Delegation.lagda

@@ -0,0 +1,62 @@
+\begin{code}
+{-# OPTIONS --safe #-}
+
+open import Prelude using (Type)
+open import Ledger.Types.GovStructure
+
+module Ledger.Delegation
+  (gs : _) (open GovStructure gs)
+  where
+
+open import Data.Maybe
+import Data.Integer as ℤ
+
+open import Ledger.GovernanceActions gs
+open import Ledger.Prelude
+open import Ledger.Prelude.Base
+
+open import Agda.Builtin.FromNat
+
+open import Tactic.Derive.DecEq
+
+record PoolParams : Type where
+  field
+    rewardAddr : Credential
+
+data DepositPurpose : Type where
+  CredentialDeposit  : Credential   → DepositPurpose
+  PoolDeposit        : KeyHash      → DepositPurpose
+  DRepDeposit        : Credential   → DepositPurpose
+  GovActionDeposit   : GovActionID  → DepositPurpose
+
+instance
+  unquoteDecl DecEq-DepositPurpose = derive-DecEq
+    ((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])
+
+Deposits = DepositPurpose ⇀ Coin
+
+data DCert : Type where
+  delegate    : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
+  dereg       : Credential → Coin → DCert
+  regpool     : KeyHash → PoolParams → DCert
+  retirepool  : KeyHash → Epoch → DCert
+  regdrep     : Credential → Coin → Anchor → DCert
+  deregdrep   : Credential → Coin → DCert
+  ccreghot    : Credential → Maybe Credential → DCert
+
+cwitness : DCert → Credential
+cwitness (delegate c _ _ _)  = c
+cwitness (dereg c _)         = c
+cwitness (regpool kh _)      = KeyHashObj kh
+cwitness (retirepool kh _)   = KeyHashObj kh
+cwitness (regdrep c _ _)     = c
+cwitness (deregdrep c _)     = c
+cwitness (ccreghot c _)      = c
+
+record RewardUpdate : Set where
+  constructor ⟦_,_,_,_⟧ʳᵘ
+  field
+    Δt Δr Δf : ℤ
+    rs : Credential ⇀ Coin
+    {zeroSum} : Δt + Δr + Δf + ℤ.+ ∑[ x ← rs ] x ≡ ℤ.0ℤ
+\end{code}