WIP

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/Properties.agda

@@ -15,17 +15,19 @@ 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)
                                 × (c ∈ dom rwds → d ≡ 0)
                                 × mc ∈ mapˢ just (dom pools) ¿ 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)
@@ -37,8 +39,8 @@ instance
   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)
+      (yes p) → failure (genErrors p)
+      (no ¬p)  → success (-, POOL-regpool ¬p)
   Computational-POOL .computeProof _ _ (retirepool c e) = success (-, POOL-retirepool)
   Computational-POOL .computeProof _ _ _ = failure "Failed in POOL"
   Computational-POOL .completeness _ ⟦ pools , _ ⟧ᵖ (regpool c _) _ (POOL-regpool ¬p)
@@ -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)
+      (yes p) → failure (genErrors p)
+      (no ¬p)  → success (-, GOVCERT-ccreghot ¬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/Foreign/HSLedger.agda

@@ -163,8 +163,6 @@ HSGovStructure = record
   }
 instance _ = HSGovStructure
 
-open import Ledger.Deleg it hiding (PoolParams; DCert)
-
 HSTransactionStructure : TransactionStructure
 HSTransactionStructure = record
   { Implementation
@@ -446,6 +444,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 +502,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 +531,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 #-}

src/Ledger/Foreign/LedgerTypes.agda

@@ -454,3 +454,68 @@ GovState = List (Pair GovActionID GovActionState)
 {-# COMPILE GHC GovVote = data GovVote (MkGovVote) #-}
 {-# COMPILE GHC GovProposal = data GovProposal (MkGovProposal) #-}
 {-# COMPILE GHC GovSignal = data GovSignal (GovSignalVote|GovSignalProposal) #-}
+
+record CertEnv : Set where
+  field epoch  : Epoch
+        pp     : PParams
+        votes  : List GovVote
+        wdrls  : HSMap RwdAddr Coin
+{-# FOREIGN GHC
+  data CertEnv = MkCertEnv
+    { epoch :: Epoch
+    , pp    :: PParams
+    , votes :: [GovVote]
+    , wdrls :: [(RwdAddr, Coin)]
+    }
+#-}
+{-# COMPILE GHC CertEnv = data CertEnv (MkCertEnv) #-}
+
+record DState : Set where
+  field
+    voteDelegs   : HSMap Credential VDeleg
+    stakeDelegs  : HSMap Credential Credential
+    rewards      : HSMap Credential Coin
+{-# FOREIGN GHC
+  data DState = MkDState
+    { voteDelegs  :: [(Credential, VDeleg)]
+    , stakeDelegs :: [(Credential, Credential)]
+    , rewards     :: [(Credential, Coin)]
+    }
+#-}
+{-# COMPILE GHC DState = data DState (MkDState) #-}
+
+record PState : Set where
+  field pools     : HSMap Credential PoolParams
+        retiring  : HSMap Credential Epoch
+{-# FOREIGN GHC
+  data PState = MkPState
+    { pools :: [(Credential, PoolParams)]
+    , retiring :: [(Credential, Epoch)]
+    }
+#-}
+{-# COMPILE GHC PState = data PState (MkPState) #-}
+
+record GState : Set where
+  field dreps      : HSMap Credential Epoch
+        ccHotKeys  : HSMap Credential (Maybe Credential)
+{-# FOREIGN GHC
+  data GState = MkGState
+    { dreps     :: [(Credential, Epoch)]
+    , ccHotKeys :: [(Credential, Maybe Credential)]
+    }
+#-}
+{-# COMPILE GHC GState = data GState (MkGState) #-}
+
+record CertState : Set where
+  field dState : DState
+        pState : PState
+        gState : GState
+{-# FOREIGN GHC
+  data CertState = MkCertState
+    { dState :: DState
+    , pState :: PState
+    , gState :: GState
+    }
+#-}
+{-# COMPILE GHC CertState = data CertState (MkCertState) #-}
+

src/Ledger/Gov/Properties.agda

@@ -152,7 +152,7 @@ instance
       completeness (inj₁ s) = GoVote.completeness s
       completeness (inj₂ s) = GoProp.completeness s
 
-Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_ (⊥ ⊎ String)
+Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_ String
 Computational-GOV = it
 
 allEnactable-singleton : ∀ {aid s es} → getHash (s .prevAction) ≡ getHashES es (s .action)

src/Ledger/Ledger/Properties.agda

@@ -48,8 +48,8 @@ instance
       computeProof = case isValid ≟ true of λ where
         (yes p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
-          (certSt' , certStep) ← map₁ (λ where (inj₁ x) → x; (inj₂ x) → x) $ computeCerts certΓ certSt txcerts
-          (govSt'  , govStep)  ← map₁ (λ where (inj₁ ());    (inj₂ x) → x) $ computeGov   govΓ  govSt  (txgov txb)
+          (certSt' , certStep) ← computeCerts certΓ certSt txcerts
+          (govSt'  , govStep)  ← computeGov   govΓ  govSt  (txgov txb)
           success (_ , LEDGER-V⋯ p utxoStep certStep govStep)
         (no ¬p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
@@ -73,7 +73,7 @@ instance
         with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
       ... | success (utxoSt' , _) | refl = refl
 
-Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ (⊥ ⊎ String)
+Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String
 Computational-LEDGERS = it
 
 instance

src/Ledger/Ratify/Properties.agda

@@ -72,12 +72,12 @@ instance
   Computational-RATIFY' : Computational _⊢_⇀⦇_,RATIFY'⦈_ ⊥
   Computational-RATIFY' = record {Implementation}
 
-Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_ (⊥ ⊎ ⊥)
+Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_ ⊥
 Computational-RATIFY = it
 
 RATIFY-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s'
 RATIFY-total = ReflexiveTransitiveClosure-total (Implementation.RATIFY'-total _ _ _)
 
 RATIFY-complete : ∀ {Γ s sig s'} →
   Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total {Γ} {s} {sig} .proj₁ ≡ s'
-RATIFY-complete = computational⇒rightUnique it (RATIFY-total .proj₂)
+RATIFY-complete = computational⇒rightUnique Computational-RATIFY (RATIFY-total .proj₂)