Add IsSet typeclass

src/Interface/IsSet.agda

@@ -0,0 +1,45 @@
+{-# OPTIONS --safe --no-import-sorts #-}
+
+open import Agda.Primitive renaming (Set to Type)
+open import Axiom.Set
+
+module Interface.IsSet (th : Theory) where
+
+import Axiom.Set.Rel th as Rel
+open import Axiom.Set.Map th as Map
+open import Axiom.Set.TotalMap th as TotalMap
+open import Data.Product
+
+open Theory th renaming (_∈_ to _∈ᵗ_; _∉_ to _∉ᵗ_)
+
+private variable A B X : Type
+
+record IsSet (A B : Type) : Type where
+  field
+    toSet : A → Set B
+
+open IsSet ⦃...⦄ public
+
+infix 4 _∈_ _∉_
+
+_∈_ : ⦃ IsSet X A ⦄ → A → X → Type
+a ∈ X = a ∈ᵗ (toSet X)
+
+_∉_ : ⦃ IsSet X A ⦄ → A → X → Type
+a ∉ X = a ∉ᵗ (toSet X)
+
+dom : ⦃ IsSet X (A × B) ⦄ → X → Set A
+dom X = Rel.dom (toSet X)
+
+range : ⦃ IsSet X (A × B) ⦄ → X → Set B
+range X = Rel.range (toSet X)
+
+instance
+  IsSet-Set : IsSet (Set A) A
+  IsSet-Set .toSet A = A
+
+  IsSet-Map : IsSet (Map A B) (A × B)
+  IsSet-Map .toSet = _ˢ
+
+  IsSet-TotalMap : IsSet (TotalMap A B) (A × B)
+  IsSet-TotalMap .toSet = TotalMap.rel

src/Ledger/Chain.lagda

@@ -79,8 +79,8 @@ data _⊢_⇀⦇_,NEWEPOCH⦈_ : NewEpochEnv → NewEpochState → Epoch → New
 
       es        = record esW { withdrawals = ∅ᵐ }
       retired   = retiring ⁻¹ e
-      refunds   = govActionReturns ∪⁺ trWithdrawals ∣ dom (rewards ˢ)
-      unclaimed = govActionReturns ∪⁺ trWithdrawals ∣ dom (rewards ˢ) ᶜ
+      refunds   = govActionReturns ∪⁺ trWithdrawals ∣ dom rewards
+      unclaimed = govActionReturns ∪⁺ trWithdrawals ∣ dom rewards ᶜ
 
       govSt' = filter (λ x → ¿ ¬ proj₁ x ∈ mapˢ proj₁ removed ¿) govSt
 

src/Ledger/Deleg.lagda

@@ -121,7 +121,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
-    c ∉ dom (pools ˢ)
+    c ∉ dom pools
     ────────────────────────────────
     pp ⊢  ⟦ pools , retiring ⟧ᵖ ⇀⦇ regpool c poolParams ,POOL⦈
           ⟦ ❴ c , poolParams ❵ᵐ ∪ᵐˡ pools , retiring ⟧ᵖ
@@ -132,19 +132,19 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set whe
 
 data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Set where
   GOVCERT-regdrep : let open PParams pp in
-    (d ≡ drepDeposit × c ∉ dom (dReps ˢ)) ⊎ (d ≡ 0 × c ∈ dom (dReps ˢ))
+    (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
     ────────────────────────────────
     ⟦ e , pp , vs ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
                         ⟦ ❴ c , e + drepActivity ❵ᵐ ∪ᵐˡ dReps , ccKeys ⟧ᵛ
 
   GOVCERT-deregdrep :
-    c ∈ dom (dReps ˢ)
+    c ∈ dom dReps
     ────────────────────────────────
     Γ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ deregdrep c ,GOVCERT⦈
          ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ᵛ
 
   GOVCERT-ccreghot :
-    (c , nothing) ∉ ccKeys ˢ
+    (c , nothing) ∉ ccKeys
     ────────────────────────────────
     Γ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈
          ⟦ dReps , singletonᵐ c mc ∪ᵐˡ ccKeys ⟧ᵛ
@@ -208,24 +208,24 @@ instance
 instance
   Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_
   Computational-POOL .computeProof _ ⟦ pools , _ ⟧ᵖ (regpool c _) =
-    case c ∈? dom (pools ˢ) of λ where
+    case c ∈? dom pools of λ where
       (yes _) → nothing
       (no p)  →  just (-, POOL-regpool p)
   Computational-POOL .computeProof _ _ (retirepool c e) = just (-, POOL-retirepool)
   Computational-POOL .computeProof _ _ _ = nothing
   Computational-POOL .completeness _ ⟦ pools , _ ⟧ᵖ (regpool c _) _ (POOL-regpool ¬p)
-    rewrite dec-no (c ∈? dom (pools ˢ)) ¬p = refl
+    rewrite dec-no (c ∈? dom pools) ¬p = refl
   Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_
   Computational-GOVCERT .computeProof ⟦ _ , pp , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ (regdrep c d _) =
     let open PParams pp in
-    case ¿ (d ≡ drepDeposit × c ∉ dom (dReps ˢ))
-         ⊎ (d ≡ 0 × c ∈ dom (dReps ˢ)) ¿ of λ where
+    case ¿ (d ≡ drepDeposit × c ∉ dom dReps)
+         ⊎ (d ≡ 0 × c ∈ dom dReps) ¿ of λ where
       (yes p) → just (-, GOVCERT-regdrep p)
       (no _)  → nothing
   Computational-GOVCERT .computeProof _ ⟦ dReps , _ ⟧ᵛ (deregdrep c) =
-    case c ∈? dom (dReps ˢ) of λ where
+    case c ∈? dom dReps of λ where
       (yes p) → just (-, GOVCERT-deregdrep p)
       (no _)  → nothing
   Computational-GOVCERT .computeProof _ ⟦ _ , ccKeys ⟧ᵛ (ccreghot c _) =
@@ -237,11 +237,11 @@ instance
     (regdrep c d _) _ (GOVCERT-regdrep p)
     rewrite dec-yes
       ¿ (let open PParams pp in
-        (d ≡ drepDeposit × c ∉ dom (dReps ˢ)) ⊎ (d ≡ 0 × c ∈ dom (dReps ˢ)))
+        (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps))
       ¿ p .proj₂ = refl
   Computational-GOVCERT .completeness _ ⟦ dReps , _ ⟧ᵛ
     (deregdrep c) _ (GOVCERT-deregdrep p)
-    rewrite dec-yes (c ∈? dom (dReps ˢ)) p .proj₂ = refl
+    rewrite dec-yes (c ∈? dom dReps) p .proj₂ = refl
   Computational-GOVCERT .completeness _ ⟦ _ , ccKeys ⟧ᵛ
     (ccreghot c _) _ (GOVCERT-ccreghot ¬p)
     rewrite dec-no ((c , nothing) ∈? (ccKeys ˢ)) ¬p = refl

src/Ledger/Gov.lagda

@@ -89,7 +89,7 @@ data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovPropo
     actionWellFormed a ≡ true
     → d ≡ govActionDeposit
     →  (∀ {new rem q} → a ≡ NewCommittee new rem q
-       → ∀[ e ∈ range (new ˢ) ] epoch < e × dom (new ˢ) ∩ rem ≡ᵉ ∅)
+       → ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅)
     ────────────────────────────────
     let sig = inj₂ record { returnAddr = addr ; action = a ; anchor = x
                           ; deposit = d ; prevAction = prev }
@@ -139,7 +139,7 @@ instance
     case ¿ actionWellFormed a ≡ true × d ≡ pparams .PParams.govActionDeposit ¿
          ,′ isNewCommittee a of λ where
       (yesᵈ (wf , dep) , yesᵈ (new , rem , q , refl)) →
-        case ¿ ∀[ e ∈ range (new ˢ) ] epoch < e × dom (new ˢ) ∩ rem ≡ᵉ ∅ ¿ of λ where
+        case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
           (yesᵈ newOk) → just (_ , GOV-Propose wf dep λ where refl → newOk)
           (noᵈ _)      → nothing
       (yesᵈ (wf , dep) , noᵈ notNewComm) → just (_ , GOV-Propose wf dep λ isNewComm → ⊥-elim (notNewComm (_ , _ , _ , isNewComm)))
@@ -154,7 +154,7 @@ instance
   ... | noᵈ ¬p | _ = ⊥-elim (¬p (wf , dep))
   ... | yesᵈ _ | noᵈ notNewComm = refl
   ... | yesᵈ _ | yesᵈ (new , rem , q , refl)
-    rewrite dec-yes ¿ ∀[ e ∈ range (new ˢ) ] epoch < e × dom (new ˢ) ∩ rem ≡ᵉ ∅ ¿ (newOk refl) .proj₂ = refl
+    rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (newOk refl) .proj₂ = refl
 
 Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_
 Computational-GOV = it

src/Ledger/GovernanceActions.lagda

@@ -266,7 +266,7 @@ record EnactState : Set where
         withdrawals   : RwdAddr ⇀ Coin
 
 ccCreds : HashProtected (Maybe (Credential ⇀ Epoch × ℚ)) → ℙ Credential
-ccCreds (just x  , _)  = dom (x .proj₁ ˢ)
+ccCreds (just x  , _)  = dom (x .proj₁)
 ccCreds (nothing , _)  = ∅
 \end{code}
 } %% end small
@@ -312,7 +312,7 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta
                  record  s { cc = nothing , gid }
 
   Enact-NewComm : let old = maybe proj₁ ∅ᵐ (s .EnactState.cc .proj₁) in
-    ∀[ term ∈ range (new ˢ) ] term ≤ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e)
+    ∀[ term ∈ range new ] term ≤ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e)
     ────────────────────────────────
     ⟦ gid , t , e ⟧ᵉ ⊢  s ⇀⦇ NewCommittee new rem q ,ENACT⦈
                 record  s { cc = just ((new ∪ᵐˡ old) ∣ rem ᶜ , q) , gid }
@@ -351,7 +351,7 @@ instance
   Computational-ENACT .computeProof ⟦ _ , t , e ⟧ᵉ s = λ where
     NoConfidence             → just (_ , Enact-NoConf)
     (NewCommittee new rem q) →
-      case ¿ ∀[ term ∈ range (new ˢ) ]
+      case ¿ ∀[ term ∈ range new ]
                term ≤ᵉ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e) ¿ of λ where
       (yesᵈ p) → just (-, Enact-NewComm p)
       (noᵈ ¬p) → nothing
@@ -368,7 +368,7 @@ instance
   ... | .NoConfidence           | Enact-NoConf   = refl
   ... | .NewCommittee new rem q | Enact-NewComm p
     rewrite dec-yes
-      (¿ ∀[ term ∈ range (new ˢ) ] term
+      (¿ ∀[ term ∈ range new ] term
            ≤ᵉ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e) ¿) p .proj₂
       = refl
   ... | .NewConstitution dh sh  | Enact-NewConst = refl

src/Ledger/Ledger.lagda

@@ -73,7 +73,7 @@ data
        record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
     →  ⟦ epoch slot , pparams , txvote ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
     →  ⟦ txid , epoch slot , pparams ⟧ᵗ ⊢ govSt ⇀⦇ txgov txb ,GOV⦈ govSt'
-    →  mapˢ stake (dom (txwdrls ˢ)) ⊆ dom (certState' .dState .voteDelegs ˢ)
+    →  mapˢ stake (dom txwdrls) ⊆ dom (certState' .dState .voteDelegs)
        ────────────────────────────────
        Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧ˡ
 \end{code}

src/Ledger/Ledger/Properties.agda

@@ -34,8 +34,8 @@ instance
 
       module _ (cs : CertState) where
         LEDGER-premises : Set
-        LEDGER-premises = mapˢ RwdAddr.stake (dom (txwdrls ˢ))
-                        ⊆ dom (cs .CertState.dState .DState.voteDelegs ˢ)
+        LEDGER-premises = mapˢ RwdAddr.stake (dom txwdrls)
+                        ⊆ dom (cs .CertState.dState .DState.voteDelegs)
 
         LEDGER-premises? = ¿ LEDGER-premises ¿
 
@@ -72,7 +72,7 @@ private variable
   l : List Tx
 
 FreshTx : Tx → LState → Set
-FreshTx tx ls = tx .body .txid ∉ mapˢ proj₁ (dom (ls .utxoSt .utxo ˢ))
+FreshTx tx ls = tx .body .txid ∉ mapˢ proj₁ (dom (ls .utxoSt .utxo))
   where open Tx; open TxBody; open UTxOState; open LState
 
 LEDGER-pov : FreshTx tx s → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'

src/Ledger/NewPP.lagda

@@ -24,13 +24,13 @@ record NewPParamState : Set where
 
 updatePPUp : PParams → PPUpdateState → PPUpdateState
 updatePPUp pparams record { fpup = fpup }
-  with allᵇ (isViableUpdate? pparams) (range (fpup ˢ))
+  with allᵇ (isViableUpdate? pparams) (range fpup)
 ... | false  = record { pup = ∅ᵐ    ; fpup = ∅ᵐ }
 ... | true   = record { pup = fpup  ; fpup = ∅ᵐ }
 
 votedValue : ProposedPPUpdates → PParams → ℕ → Maybe PParamsUpdate
 votedValue pup pparams quorum =
-  case any? (λ u → lengthˢ ((pup ↾ fromList [ u ]) ˢ) ≥? quorum) (range (pup ˢ)) of λ where
+  case any? (λ u → lengthˢ (pup ↾ fromList [ u ]) ≥? quorum) (range pup) of λ where
     (no  _)        → nothing
     (yes (u , _))  → just u
 \end{code}

src/Ledger/PDF.lagda

@@ -48,11 +48,11 @@ open import Ledger.Chain
 \end{code}
 
 \include{Ledger/Introduction}
-% \include{Ledger/Crypto}
-% \include{Ledger/BaseTypes}
-% \include{Ledger/TokenAlgebra}
-% \include{Ledger/Address}
-% \include{Ledger/Script}
+\include{Ledger/Crypto}
+\include{Ledger/BaseTypes}
+\include{Ledger/TokenAlgebra}
+\include{Ledger/Address}
+\include{Ledger/Script}
 \include{Ledger/GovernanceActions}
 \include{Ledger/PParams}
 \include{Ledger/Gov}

src/Ledger/PPUp.lagda

@@ -90,17 +90,17 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update →
   PPUpdateEmpty : Γ ⊢ s ⇀⦇ nothing ,PPUP⦈ s
 
   PPUpdateCurrent : let open PPUpdateEnv Γ in
-    dom (pup ˢ) ⊆ dom (genDelegs ˢ)
-    → All (isViableUpdate pparams) (range (pup ˢ))
+    dom pup ⊆ dom genDelegs
+    → All (isViableUpdate pparams) (range pup)
     → (slot + (2 * StabilityWindow)) <ˢ firstSlot (sucᵉ (epoch slot))
     → epoch slot ≡ e
     ────────────────────────────────
     Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈
         record { pup = pup ∪ᵐˡ pupˢ ; fpup = fpupˢ }
 
   PPUpdateFuture : let open PPUpdateEnv Γ in
-    dom (pup ˢ) ⊆ dom (genDelegs ˢ)
-    → All (isViableUpdate pparams) (range (pup ˢ))
+    dom pup ⊆ dom genDelegs
+    → All (isViableUpdate pparams) (range pup)
     → firstSlot (sucᵉ (epoch slot)) ≤ (slot + (2 * StabilityWindow))
     → sucᵉ (epoch slot) ≡ e
     ────────────────────────────────

src/Ledger/PPUp/Properties.agda

@@ -16,15 +16,15 @@ private
 
   Current-Property : PPUpdateEnv → Update → Set
   Current-Property Γ (pup , e) = let open PPUpdateEnv Γ in
-      dom (pup ˢ) ⊆ dom (genDelegs ˢ)
-      × All (isViableUpdate pparams) (range (pup ˢ))
+      dom pup ⊆ dom genDelegs
+      × All (isViableUpdate pparams) (range pup)
       × (slot + (2 * StabilityWindow)) <ˢ firstSlot (sucᵉ (epoch slot))
       × epoch slot ≡ e
 
   Future-Property : PPUpdateEnv → Update → Set
   Future-Property Γ (pup , e) = let open PPUpdateEnv Γ in
-      dom (pup ˢ) ⊆ dom (genDelegs ˢ)
-      × All (isViableUpdate pparams) (range (pup ˢ))
+      dom pup ⊆ dom genDelegs
+      × All (isViableUpdate pparams) (range pup)
       × firstSlot (sucᵉ (epoch slot)) ≤ˢ (slot + (2 * StabilityWindow))
       × sucᵉ (epoch slot) ≡ e
 

src/Ledger/Prelude.agda

@@ -45,7 +45,10 @@ abstract
   List-Modelᵈ : Theoryᵈ
   List-Modelᵈ = L.List-Modelᵈ
 
-open Theoryᵈ List-Modelᵈ renaming (Set to ℙ_; filter to filterˢ; map to mapˢ) public
+open Theoryᵈ List-Modelᵈ renaming (Set to ℙ_; filter to filterˢ; map to mapˢ)
+                        hiding (_∈_; _∉_) public
+
+open import Interface.IsSet th public
 
 abstract
   open import Axiom.Set.Properties th using (card-≡ᵉ)
@@ -55,13 +58,13 @@ abstract
   finiteness : ∀ {A} (X : Theory.Set th A) → finite X
   finiteness = Theoryᶠ.finiteness List-Modelᶠ
 
-  lengthˢ : ∀ {A} ⦃ _ : DecEq A ⦄ (X : Theory.Set th A) → ℕ
-  lengthˢ = Theoryᶠ.lengthˢ List-Modelᶠ
+  lengthˢ : ∀ {A X} ⦃ _ : DecEq A ⦄ ⦃ _ : IsSet X A ⦄ → X → ℕ
+  lengthˢ X = Theoryᶠ.lengthˢ List-Modelᶠ (toSet X)
 
-  lengthˢ-≡ᵉ : ∀ {A} ⦃ _ : DecEq A ⦄ (X Y : Theory.Set th A)
-    → X ≡ᵉ Y
-    → lengthˢ X ≡ lengthˢ Y
-  lengthˢ-≡ᵉ X Y X≡Y =
+  lengthˢ-≡ᵉ : ∀ {A Z} ⦃ _ : DecEq A ⦄ ⦃ _ : IsSet Z A ⦄ (X Y : Z)
+    → toSet X ≡ᵉ toSet Y
+    → (lengthˢ X) ≡ (lengthˢ Y)
+  lengthˢ-≡ᵉ X Y X≡Y = let X = toSet X; Y = toSet Y in
     card-≡ᵉ (X , Theoryᶠ.DecEq⇒strongly-finite List-Modelᶠ X)
             (Y , Theoryᶠ.DecEq⇒strongly-finite List-Modelᶠ Y) X≡Y
 
@@ -76,7 +79,7 @@ abstract
     DecEq-ℙ = L.Decˡ.DecEq-Set
 
 open import Axiom.Set.Rel th public
-  hiding (_∣'_; _↾'_)
+  hiding (_∣'_; _↾'_; dom; range)
 
 open import Axiom.Set.Map th public
   renaming (Map to _⇀_)
@@ -126,7 +129,8 @@ X ᶠˢ = X , finiteness _
 
 
 infix 2 All-syntax
-All-syntax = All
+All-syntax : ∀ {A X} ⦃ _ : IsSet X A ⦄ → (A → Set) → X → Set
+All-syntax P X = All P (toSet X)
 syntax All-syntax (λ x → P) l = ∀[ x ∈ l ] P
 
 insertIfJust : ∀ {A B} → ⦃ DecEq A ⦄ → A → Maybe B → A ⇀ B → A ⇀ B