diff --git a/src/Interface/ComputationalRelation.agda b/src/Interface/ComputationalRelation.agda index 708483367..c87e3c872 100644 --- a/src/Interface/ComputationalRelation.agda +++ b/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 diff --git a/src/Ledger/Chain/Properties.agda b/src/Ledger/Chain/Properties.agda index 40c56b09b..bba2e3cbc 100644 --- a/src/Ledger/Chain/Properties.agda +++ b/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 diff --git a/src/Ledger/Deleg/Properties.agda b/src/Ledger/Deleg/Properties.agda index ba56eab5e..2eb158b3f 100644 --- a/src/Ledger/Deleg/Properties.agda +++ b/src/Ledger/Deleg/Properties.agda @@ -15,6 +15,8 @@ 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 @@ -22,10 +24,10 @@ instance × (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 diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index 800c9a75d..f49200c0b 100644 --- a/src/Ledger/Foreign/HSLedger.agda +++ b/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 #-} diff --git a/src/Ledger/Foreign/LedgerTypes.agda b/src/Ledger/Foreign/LedgerTypes.agda index 2944b557e..d18c93c69 100644 --- a/src/Ledger/Foreign/LedgerTypes.agda +++ b/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) #-} + diff --git a/src/Ledger/Gov/Properties.agda b/src/Ledger/Gov/Properties.agda index 57644e658..0ce6af126 100644 --- a/src/Ledger/Gov/Properties.agda +++ b/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) diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda index 88a4c1b39..5a94f116c 100644 --- a/src/Ledger/Ledger/Properties.agda +++ b/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 diff --git a/src/Ledger/Ratify/Properties.agda b/src/Ledger/Ratify/Properties.agda index e19daa367..9e483acba 100644 --- a/src/Ledger/Ratify/Properties.agda +++ b/src/Ledger/Ratify/Properties.agda @@ -72,7 +72,7 @@ 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' @@ -80,4 +80,4 @@ 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₂)