WIP

src/Axiom/Set.agda

@@ -164,6 +164,9 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
   ∈-fromList : ∀ {a} → a ∈ˡ l ⇔ a ∈ fromList l
   ∈-fromList = proj₂ $ listing _
 
+  listToFinSet : List A → FinSet A
+  listToFinSet l = fromList l , l , R.SK-sym ∈-fromList
+
   ∈-unions : {a : A} {U : Set (Set A)} → (∃[ T ] T ∈ U × a ∈ T) ⇔ a ∈ proj₁ (unions U)
   ∈-unions = proj₂ $ unions _
 

src/Axiom/Set/Map/Dec.agda

@@ -51,12 +51,12 @@ module Lookupᵐᵈ (sp-∈ : spec-∈ A) where
        helper _ _ | _ , _ , refl | _ , _ , refl | yes _ | yes _
          with refl ← trans (sym eq) eq' = refl
 
-  module _ {V : Type} ⦃ mon : IsCommutativeMonoid' 0ℓ 0ℓ V ⦄ ⦃ _ : DecEq A ⦄ where
-    infixr 6 _∪⁺_
-    open IsCommutativeMonoid' mon
+  open import Algebra
+  module OpUnion {V : Type} (_∙_ : V → V → V) where
+    infixr 6 _∪̇_
 
-    _∪⁺_ : Map A V → Map A V → Map A V
-    _∪⁺_ = unionWith (fold id id _◇_)
+    _∪̇_ : ⦃ DecEq A ⦄ → Map A V → Map A V → Map A V
+    _∪̇_ = unionWith (fold id id _∙_)
 
-    aggregate₊ : FinSet (A × V) → Map A V
-    aggregate₊ (_ , l , _) = foldl (λ m x → m ∪⁺ ❴ x ❵ᵐ) ∅ᵐ l
+    aggregate∙ : ⦃ DecEq A ⦄ → FinSet (A × V) → Map A V
+    aggregate∙ (_ , l , _) = foldl (λ m x → m ∪̇ ❴ x ❵ᵐ) ∅ᵐ l

src/Interface/ComputationalRelation.agda

@@ -168,20 +168,34 @@ Computational⇒Dec' ⦃ comp = comp ⦄ = Computational⇒Dec comp
 
 open Computational ⦃...⦄
 
+record InjectError Err₁ Err₂ : Set where
+  field injectError : Err₁ → Err₂
+
+open InjectError
+
 instance
+  InjectError-⊥ : InjectError ⊥ Err
+  InjectError-⊥ = λ where
+    .injectError ()
+
+  InjectError-Id : InjectError Err Err
+  InjectError-Id = λ where
+    .injectError → id
+
   Computational-Id : {C S : Set} → Computational (IdSTS {C} {S}) ⊥
   Computational-Id .computeProof _ s _ = success (s , Id-nop)
   Computational-Id .completeness _ _ _ _ Id-nop = refl
 
 module _ {BSTS : C → S → ⊤ → S → Set} ⦃ _ : Computational BSTS Err₁ ⦄ where
-  module _ {STS : C → S → Sig → S → Set} ⦃ _ : Computational STS Err₂ ⦄ where instance
-    Computational-ReflexiveTransitiveClosureᵇ : Computational (ReflexiveTransitiveClosureᵇ BSTS STS) (Err₁ ⊎ Err₂)
-    Computational-ReflexiveTransitiveClosureᵇ .computeProof c s [] = bimap inj₁ (map₂′ BS-base) (computeProof c s tt)
+  module _ {STS : C → S → Sig → S → Set} ⦃ _ : Computational STS Err₂ ⦄
+     ⦃ _ : InjectError Err₁ Err ⦄ ⦃ _ : InjectError Err₂ Err ⦄ where instance
+    Computational-ReflexiveTransitiveClosureᵇ : Computational (ReflexiveTransitiveClosureᵇ BSTS STS) (Err)
+    Computational-ReflexiveTransitiveClosureᵇ .computeProof c s [] = bimap (injectError it) (map₂′ BS-base) (computeProof c s tt)
     Computational-ReflexiveTransitiveClosureᵇ .computeProof c s (sig ∷ sigs) with computeProof c s sig 
     ... | success (s₁ , h) with computeProof c s₁ sigs
     ...   | success (s₂ , hs) = success (s₂ , BS-ind h hs)
-    ...   | failure a = failure a
-    Computational-ReflexiveTransitiveClosureᵇ .computeProof c s (sig ∷ sigs) | failure a = failure (inj₂ a)
+    ...   | failure a = failure (injectError it a)
+    Computational-ReflexiveTransitiveClosureᵇ .computeProof c s (sig ∷ sigs) | failure a = failure (injectError it a)
     Computational-ReflexiveTransitiveClosureᵇ .completeness c s [] s' (BS-base p)
       with computeProof {STS = BSTS} c s tt | completeness _ _ _ _ p
     ... | success x | refl = refl
@@ -191,15 +205,17 @@ module _ {BSTS : C → S → ⊤ → S → Set} ⦃ _ : Computational BSTS Err
       with computeProof ⦃ Computational-ReflexiveTransitiveClosureᵇ ⦄ c s₁ sigs | completeness _ _ _ _ hs
     ... | success (s₂ , _) | p = p
 
-  module _ {STS : C × ℕ → S → Sig → S → Set} ⦃ Computational-STS : Computational STS Err₂ ⦄ where instance
-    Computational-ReflexiveTransitiveClosureᵢᵇ' : Computational (_⊢_⇀⟦_⟧ᵢ*'_ BSTS STS) (Err₁ ⊎ Err₂)
+  module _ {STS : C × ℕ → S → Sig → S → Set} ⦃ Computational-STS : Computational STS Err₂ ⦄
+    ⦃ InjectError-Err₁ : InjectError Err₁ Err ⦄ ⦃ InjectError-Err₂ : InjectError Err₂ Err ⦄
+    where instance
+    Computational-ReflexiveTransitiveClosureᵢᵇ' : Computational (_⊢_⇀⟦_⟧ᵢ*'_ BSTS STS) Err
     Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s [] =
-      bimap inj₁ (map₂′ BS-base) (computeProof (proj₁ c) s tt)
+      bimap (injectError it) (map₂′ BS-base) (computeProof (proj₁ c) s tt)
     Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s (sig ∷ sigs) with computeProof c s sig
     ... | success (s₁ , h) with computeProof (proj₁ c , suc (proj₂ c)) s₁ sigs
     ... | success (s₂ , hs) = success (s₂ , BS-ind h hs)
     ... | failure a = failure a
-    Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s (sig ∷ sigs) | failure a = failure (inj₂ a)
+    Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s (sig ∷ sigs) | failure a = failure (injectError it a)
     Computational-ReflexiveTransitiveClosureᵢᵇ' .completeness c s [] s' (BS-base p)
       with computeProof {STS = BSTS} (proj₁ c) s tt | completeness _ _ _ _ p
     ... | success x | refl = refl
@@ -209,16 +225,16 @@ module _ {BSTS : C → S → ⊤ → S → Set} ⦃ _ : Computational BSTS Err
       with computeProof (proj₁ c , suc (proj₂ c)) s₁ sigs | completeness _ _ _ _ hs
     ...   | success (s₂ , _) | p = p
 
-    Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ BSTS STS) (Err₁ ⊎ Err₂)
+    Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ BSTS STS) Err
     Computational-ReflexiveTransitiveClosureᵢᵇ .computeProof c =
       Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof (c , 0)
     Computational-ReflexiveTransitiveClosureᵢᵇ .completeness c =
       Computational-ReflexiveTransitiveClosureᵢᵇ' .completeness (c , 0)
 
 Computational-ReflexiveTransitiveClosure : {STS : C → S → Sig → S → Set} → ⦃ Computational STS Err ⦄
-  → Computational (ReflexiveTransitiveClosure STS) (⊥ ⊎ Err)
+  → Computational (ReflexiveTransitiveClosure STS) Err
 Computational-ReflexiveTransitiveClosure = it
 
 Computational-ReflexiveTransitiveClosureᵢ : {STS : C × ℕ → S → Sig → S → Set} → ⦃ Computational STS Err ⦄
-  → Computational (ReflexiveTransitiveClosureᵢ STS) (⊥ ⊎ Err)
+  → Computational (ReflexiveTransitiveClosureᵢ STS) Err
 Computational-ReflexiveTransitiveClosureᵢ = it

src/Ledger/Chain/Properties.agda

@@ -22,7 +22,7 @@ instance
   Computational-CHAIN : Computational _⊢_⇀⦇_,CHAIN⦈_ String
   Computational-CHAIN .computeProof Γ s b = do
     _ , neStep ← map₁ ⊥-elim $ computeProof {STS = _⊢_⇀⦇_,NEWEPOCH⦈_} _ _ _
-    _ , lsStep ← map₁ (λ where (inj₁ ()); (inj₂ x) → x) $ computeProof _ _ _
+    _ , lsStep ← computeProof _ _ _
     success (_ , CHAIN neStep lsStep)
   Computational-CHAIN .completeness Γ s b s' (CHAIN neStep lsStep)
     with recomputeProof neStep | completeness _ _ _ _ neStep

src/Ledger/Deleg.lagda

@@ -148,9 +148,9 @@ data
 \begin{code}
 
   DELEG-delegate : let open PParams pp in
-    ∙ (c ∉ dom rwds → d ≡ poolDeposit)
+    ∙ (c ∉ dom rwds → d ≡ keyDeposit)
     ∙ (c ∈ dom rwds → d ≡ 0)
-    ∙ mc ∈ mapˢ just (dom pools)
+    ∙ mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
       ────────────────────────────────
       ⟦ pp , pools ⟧ᵈᵉ ⊢
         ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ delegate c mv mc d ,DELEG⦈

src/Ledger/Deleg/Properties.agda

@@ -15,32 +15,34 @@ open import Ledger.Deleg gs
 
 open Computational ⦃...⦄
 
+open import Tactic.GenError using (genErrors)
+
 instance
   Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String
   Computational-DELEG .computeProof ⟦ pp , pools ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ = λ where
-    (delegate c mv mc d) → case ¿ (c ∉ dom rwds → d ≡ pp .PParams.poolDeposit)
+    (delegate c mv mc d) → case ¿ (c ∉ dom rwds → d ≡ pp .PParams.keyDeposit)
                                 × (c ∈ dom rwds → d ≡ 0)
-                                × mc ∈ mapˢ just (dom pools) ¿ of λ where
+                                × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ¿ of λ where
       (yes p) → success (-, DELEG-delegate p)
-      _ → failure "Failed in DELEG at delegate"
+      (no ¬p) → failure (genErrors ¬p)
     (dereg c) → case ¿ (c , 0) ∈ rwds ¿ of λ where
       (yes p) → success (-, DELEG-dereg p)
-      _       → failure "Failed in DELEG at (c , 0) ∈ rwds"
+      (no ¬p) → failure (genErrors ¬p)
     _ → failure "Unexpected certificate in DELEG"
   Computational-DELEG .completeness ⟦ pp , pools ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (delegate c mv mc d)
-    s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom rwds → d ≡ pp .PParams.poolDeposit)
+    s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom rwds → d ≡ pp .PParams.keyDeposit)
                                 × (c ∈ dom rwds → d ≡ 0)
-                                × mc ∈ mapˢ just (dom pools) ¿) p .proj₂ = refl
+                                × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ¿) p .proj₂ = refl
   Computational-DELEG .completeness ⟦ _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (dereg c) _ (DELEG-dereg p)
     rewrite dec-yes (¿ (c , 0) ∈ rwds ¿) p .proj₂ = refl
 
   Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
   Computational-POOL .computeProof _ ⟦ pools , _ ⟧ᵖ (regpool c _) =
-    case c ∈? dom pools of λ where
-      (yes _) → failure "Pool already registered"
-      (no p)  → success (-, POOL-regpool p)
+    case ¬? (c ∈? dom pools) of λ where
+      (yes p) → success (-, POOL-regpool p)
+      (no ¬p) → failure (genErrors ¬p)
   Computational-POOL .computeProof _ _ (retirepool c e) = success (-, POOL-retirepool)
-  Computational-POOL .computeProof _ _ _ = failure "Failed in POOL"
+  Computational-POOL .computeProof _ _ _ = failure "Unexpected certificate in POOL"
   Computational-POOL .completeness _ ⟦ pools , _ ⟧ᵖ (regpool c _) _ (POOL-regpool ¬p)
     rewrite dec-no (c ∈? dom pools) ¬p = refl
   Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
@@ -51,15 +53,15 @@ instance
     case ¿ (d ≡ drepDeposit × c ∉ dom dReps)
          ⊎ (d ≡ 0 × c ∈ dom dReps) ¿ of λ where
       (yes p) → success (-, GOVCERT-regdrep p)
-      (no _)  → failure "GOVCERT failed at (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)"
+      (no ¬p)  → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ ⟦ dReps , _ ⟧ᵛ (deregdrep c) =
     case c ∈? dom dReps of λ where
       (yes p) → success (-, GOVCERT-deregdrep p)
-      (no _)  → failure "GOVCERT failed at (c ∈? dom dReps)"
+      (no ¬p)  → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ ⟦ _ , ccKeys ⟧ᵛ (ccreghot c _) =
-    case (c , nothing) ∈? (ccKeys ˢ) of λ where
-      (yes _) → failure "GOVCERT failed at (c , nothing) ∈? (ccKeys ˢ)"
-      (no p)  → success (-, GOVCERT-ccreghot p)
+    case ¬? ((c , nothing) ∈? (ccKeys ˢ)) of λ where
+      (yes p) → success (-, GOVCERT-ccreghot p)
+      (no ¬p) → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
   Computational-GOVCERT .completeness ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ
     (regdrep c d _) _ (GOVCERT-regdrep p)
@@ -81,7 +83,8 @@ instance
   ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
   ... | failure _       | success (_ , h) | _               = success (-, CERT-pool h)
   ... | failure _       | failure _       | success (_ , h) = success (-, CERT-vdel h)
-  ... | failure _       | failure _       | failure _       = failure "Failed at CERT"
+  ... | failure e₁      | failure e₂      | failure e₃      = failure $
+    "DELEG: " <> e₁ <> "\nPOOL: " <> e₂ <> "\nVDEL: " <> e₃
   Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(delegate c mv mc d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
@@ -119,11 +122,11 @@ instance
         wdrlCreds = mapˢ RwdAddr.stake (dom wdrls)
     in case ¿ wdrlCreds ⊆ dom voteDelegs × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
       (yes p) → success (-, CERT-base p)
-      (no ¬p) → failure "CERTBASE Failed at (mapˢ RwdAddr.stake (dom wdrls) ⊆ dom voteDelegs × wdrls ˢ ⊆ rewards ˢ)"
+      (no ¬p) → failure (genErrors ¬p)
   Computational-CERTBASE .completeness ⟦ e , pp , vs , wdrls ⟧ᶜ st _ st' (CERT-base p)
     rewrite let dState = CertState.dState st; open DState dState in
       dec-yes ¿ mapˢ RwdAddr.stake (dom wdrls) ⊆ dom voteDelegs × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
-Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ (String ⊎ String)
+Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it

src/Ledger/Enact.lagda

@@ -88,6 +88,10 @@ private variable
 
 instance
   _ = +-0-monoid
+
+_∪⁺_ : ∀ {A} → ⦃ DecEq A ⦄ → A ⇀ ℕ → A ⇀ ℕ → A ⇀ ℕ
+_∪⁺_ = OpUnion._∪̇_ _+_
+
 \end{code}
 
 Figure~\ref{fig:sts:enact} defines the rules of the ENACT transition

src/Ledger/Epoch.lagda

@@ -82,6 +82,7 @@ its results, i.e:
       open LState ls; open UTxOState utxoSt; open CertState certState
       open PState pState; open DState dState; open GState gState
       open Acnt acnt
+      open OpUnion _+_ renaming (aggregate∙ to aggregate₊)
 
       trWithdrawals   = esW .EnactState.withdrawals
       totWithdrawals  = ∑[ x ← trWithdrawals ] x

src/Ledger/Foreign/HSLedger.agda

@@ -163,8 +163,6 @@ HSGovStructure = record
   }
 instance _ = HSGovStructure
 
-open import Ledger.Deleg it hiding (PoolParams; DCert)
-
 HSTransactionStructure : TransactionStructure
 HSTransactionStructure = record
   { Implementation
@@ -206,11 +204,24 @@ open import Ledger.Utxo.Properties it it
 open import Ledger.Utxow.Properties it it
 open import Data.Rational
 
+open import Algebra
+
 instance
   _ = Convertible-Refl {⊤}
   _ = Convertible-Refl {ℕ}
   _ = Convertible-Refl {String}
 
+  Convertible-HSMap : ∀ {A B A′ B′}
+    → ⦃ DecEq A ⦄
+    → ⦃ Convertible A A′ ⦄
+    → ⦃ Convertible B B′ ⦄
+    → Convertible (A ⇀ B) (F.HSMap A′ B′)
+  Convertible-HSMap = λ where
+    .to (x , _) → record { assocList = to x }
+    .from record { assocList = x } →
+      let open OpUnion (flip const) renaming (aggregate∙ to aggregateʳ)
+       in aggregateʳ (listToFinSet (map (λ where (l F., r) → from l , from r) x))
+
   Convertible-Rational : Convertible ℚ F.Rational
   Convertible-Rational = λ where
     .to (mkℚ n d _) → n F., suc d
@@ -339,6 +350,7 @@ instance
       ; maxValSize          = maxValSize
       ; minUTxOValue        = minUTxOValue
       ; poolDeposit         = poolDeposit
+      ; keyDeposit          = keyDeposit
       ; Emax                = Emax
       ; nopt                = nopt
       ; pv                  = to pv
@@ -365,6 +377,7 @@ instance
       ; maxValSize                  = maxValSize
       ; minUTxOValue                = minUTxOValue
       ; poolDeposit                 = poolDeposit
+      ; keyDeposit                  = keyDeposit
       ; minFeeRefScriptCoinsPerByte = 0ℚ
       ; a0                          = 0ℚ
       ; Emax                        = Emax
@@ -446,6 +459,8 @@ fromNeedsHash {ChangePParams _} x = to x
 fromNeedsHash {TreasuryWdrl _} x = to 0 F., 0
 fromNeedsHash {Info} x = to 0 F., 0
 
+open import Ledger.Deleg.Properties govStructure
+
 instance
   Convertible-GovActionState : Convertible GovActionState F.GovActionState
   Convertible-GovActionState = λ where
@@ -502,6 +517,21 @@ instance
     .to (inj₂ y) → y
     .from → inj₂
 
+  Convertible-CertEnv : ConvertibleType CertEnv F.CertEnv
+  Convertible-CertEnv = autoConvertible
+
+  Convertible-GState : ConvertibleType GState F.GState
+  Convertible-GState = autoConvertible
+
+  Convertible-PState : ConvertibleType PState F.PState
+  Convertible-PState = autoConvertible
+
+  Convertible-DState : ConvertibleType DState F.DState
+  Convertible-DState = autoConvertible
+
+  Convertible-CertState : ConvertibleType CertState F.CertState
+  Convertible-CertState = autoConvertible
+
 utxo-step : F.UTxOEnv → F.UTxOState → F.Tx → F.ComputationResult String F.UTxOState
 utxo-step = to UTXO-step
 
@@ -516,3 +546,13 @@ gov-step : F.GovEnv → F.GovState → List F.GovSignal → F.ComputationResult
 gov-step = to (compute Computational-GOV)
 
 {-# COMPILE GHC gov-step as govStep #-}
+
+certs-step : F.CertEnv → F.CertState → List F.TxCert → F.ComputationResult String F.CertState
+certs-step = to (compute Computational-CERTS)
+
+{-# COMPILE GHC certs-step as certsStep #-}
+
+cert-step : F.CertEnv →  F.CertState → F.TxCert → F.ComputationResult String F.CertState
+cert-step = to (compute Computational-CERT)
+
+{-# COMPILE GHC cert-step as certStep #-}