diff --git a/shell.nix b/shell.nix
index 5a37091e7..8d202d91a 100644
--- a/shell.nix
+++ b/shell.nix
@@ -22,10 +22,6 @@ in {
     nativeBuildInputs = [
       specs.agda
       cabal-install
-      (haskellPackages.ghcWithPackages (pkgs: with pkgs; [
-        specs.ledger.hsExe
-        specs.midnight.hsExe
-      ]))
     ];
   };
 }
diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda
index d7c33844b..167743666 100644
--- a/src/Ledger/Conway/Conformance/Certs.agda
+++ b/src/Ledger/Conway/Conformance/Certs.agda
@@ -43,6 +43,7 @@ record CertState : Type where
 certDeposit : DCert → PParams → Deposits
 certDeposit (delegate c _ _ v) _   = ❴ CredentialDeposit c , v ❵
 certDeposit (regdrep c v _)    _   = ❴ DRepDeposit c , v ❵
+certDeposit (reg c v)          pp  = ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵
 certDeposit _                  _   = ∅
 -- handled in the Utxo module:
 -- certDeposit (regpool kh _)     pp  = ❴ PoolDeposit kh , pp .poolDeposit ❵
@@ -137,6 +138,14 @@ data _⊢_⇀⦇_,DELEG⦈_ where
       ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ
       , updateCertDeposit pp (dereg c d) dep ⟧ᵈ
 
+  DELEG-reg : let open PParams pp in
+    ∙ c ∉ dom rwds
+    ∙ d ≡ keyDeposit
+      ────────────────────────────────
+      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
+        ⟦ vDelegs , sDelegs , rwds , dep ⟧ᵈ ⇀⦇ reg c d ,DELEG⦈
+        ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵ 
+        , updateCertDeposit pp (reg c d) dep ⟧ᵈ
 
 data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type where
   GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
diff --git a/src/Ledger/Conway/Conformance/Certs/Properties.agda b/src/Ledger/Conway/Conformance/Certs/Properties.agda
index 46a6a9132..69261b354 100644
--- a/src/Ledger/Conway/Conformance/Certs/Properties.agda
+++ b/src/Ledger/Conway/Conformance/Certs/Properties.agda
@@ -30,6 +30,9 @@ instance
     (dereg c d) → case ¿ (c , 0) ∈ rwds × (CredentialDeposit c , d) ∈ dep ¿ of λ where
       (yes p) → success (-, DELEG-dereg p)
       (no ¬p) → failure (genErrors ¬p)
+    (reg c d) → case ¿ c ∉ dom rwds × d ≡ pp .PParams.keyDeposit ¿ of λ where
+      (yes p) → success (-, DELEG-reg p)
+      (no ¬p) → failure (genErrors ¬p)
     _ → failure "Unexpected certificate in DELEG"
 
   Computational-DELEG .completeness ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (delegate c mv mc d)
@@ -40,6 +43,8 @@ instance
                                            × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ¿) p .proj₂ = refl
   Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (dereg c d) _ (DELEG-dereg p)
     rewrite dec-yes (¿ (c , 0) ∈ rwds × (CredentialDeposit c , d) ∈ dep ¿) p .proj₂ = refl
+  Computational-DELEG .completeness ⟦ pp , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (reg c d) _ (DELEG-reg p)
+    rewrite dec-yes (¿ c ∉ dom rwds × d ≡ pp .PParams.keyDeposit ¿) p .proj₂ = refl
 
   Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
   Computational-POOL .computeProof _ ps (regpool c _) =
@@ -94,6 +99,10 @@ instance
     dCert@(delegate c mv mc d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
+  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+    dCert@(reg c d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
+    with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
+  ... | success _ | refl = refl
   Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(dereg c _) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
diff --git a/src/Ledger/Conway/Conformance/Utxo.agda b/src/Ledger/Conway/Conformance/Utxo.agda
index 7dcccab7c..9fa1353ee 100644
--- a/src/Ledger/Conway/Conformance/Utxo.agda
+++ b/src/Ledger/Conway/Conformance/Utxo.agda
@@ -44,6 +44,8 @@ updateCertDeposits pp (dereg c v ∷ certs) deposits
   = updateCertDeposits pp certs (deposits ∣ certRefund (dereg c v)ᶜ)
 updateCertDeposits pp (deregdrep c v ∷ certs) deposits
   = updateCertDeposits pp certs (deposits ∣ certRefund (deregdrep c v)ᶜ)
+updateCertDeposits pp (reg c v ∷ certs) deposits
+  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (reg c v) pp)
 updateCertDeposits pp (_ ∷ certs) deposits
   = updateCertDeposits pp certs deposits
 
diff --git a/src/Ledger/Conway/Foreign/HSLedger/BaseTypes.agda b/src/Ledger/Conway/Foreign/HSLedger/BaseTypes.agda
index 5b8a3c30d..15a2157ea 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/BaseTypes.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/BaseTypes.agda
@@ -64,7 +64,7 @@ instance
   Conv-ComputationResult : ConvertibleType ComputationResult F.ComputationResult
   Conv-ComputationResult = autoConvertible
 
-open ExternalStructures dummyExternalFunctions
+open import Ledger.Conway.Foreign.HSLedger.ExternalStructures dummyExternalFunctions
   renaming
     ( HSTransactionStructure to DummyTransactionStructure
     ; HSAbstractFunctions to DummyAbstractFunctions
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Core.agda b/src/Ledger/Conway/Foreign/HSLedger/Core.agda
index 53f71af7b..df80f54d9 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Core.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Core.agda
@@ -25,24 +25,37 @@ open import Ledger.Conway.Foreign.Util public
 open import Tactic.Derive.DecEq
 open import Tactic.Derive.Show
 
-module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance
-  ∀Hashable : Hashable A A
-  ∀Hashable = λ where .hash → id
-
-  ∀isHashableSet : isHashableSet A
-  ∀isHashableSet = mkIsHashableSet A
-
 instance
   Hashable-⊤ : Hashable ⊤ ℕ
   Hashable-⊤ = λ where .hash tt → 0
 
 record HSVKey : Type where
   constructor MkHSVKey
-  field vkey       : ℕ
-        storedHash : ℕ
+  field hvkVKey       : ℕ
+        hvkStoredHash : ℕ
+
+{-# FOREIGN GHC
+  data HSVKey = MkHSVKey
+    { hvkVKey :: Integer
+    , hvkStoredHash :: Integer
+    }
+#-}
+{-# COMPILE GHC HSVKey = data HSVKey (MkHSVKey) #-}
+
+unquoteDecl DecEq-HSVKey = derive-DecEq ((quote HSVKey , DecEq-HSVKey) ∷ [])
+
+instance
+  Hashable-HSVKey : Hashable HSVKey ℕ
+  Hashable-HSVKey = λ where .hash → HSVKey.hvkStoredHash
+
+  isHashableSet-HSVKey : isHashableSet HSVKey
+  isHashableSet-HSVKey = mkIsHashableSet ℕ
 
-unquoteDecl DecEq-HSVKey = derive-DecEq
-  ((quote HSVKey , DecEq-HSVKey) ∷ [])
+  Hashable-ℕ : Hashable ℕ ℕ
+  Hashable-ℕ = λ where .hash → id
+
+  isHashableSet-ℕ : isHashableSet ℕ
+  isHashableSet-ℕ = mkIsHashableSet ℕ
 
 unquoteDecl Show-HSVKey = derive-Show
   ((quote HSVKey , Show-HSVKey) ∷ [])
@@ -59,12 +72,12 @@ module Implementation where
   Sig  = ℕ
   Ser  = ℕ
 
-  isKeyPair  = λ sk vk → sk ≡ HSVKey.vkey vk
+  isKeyPair  = λ sk vk → sk ≡ HSVKey.hvkVKey vk
   sign       = _+_
   ScriptHash = ℕ
 
   Data         = ℕ
-  Dataʰ        = mkHashableSet Data
+  Dataʰ        = mkHashableSet ℕ
   toData : ∀ {A : Type} → A → Data
   toData _ = 0
 
@@ -113,124 +126,3 @@ module Implementation where
   AuxiliaryData   = ℕ
   DocHash         = ℕ
   tokenAlgebra    = coinTokenAlgebra
-
-module ExternalStructures (externalFunctions : ExternalFunctions) where
-  HSGlobalConstants = GlobalConstants ∋ record {Implementation}
-  instance
-    HSEpochStructure = EpochStructure  ∋ ℕEpochStructure HSGlobalConstants
-  
-    HSCrypto : Crypto
-    HSCrypto = record
-      { Implementation
-      ; pkk = HSPKKScheme
-      }
-      where
-      open ExternalFunctions externalFunctions
-      HSPKKScheme : PKKScheme
-      HSPKKScheme = record
-        { Implementation
-        ; isSigned         = λ a b m → extIsSigned (HSVKey.vkey a) b m ≡ true
-        ; sign             = λ _ _ → zero
-          -- we can't prove these properties since the functions are provided by the Haskell implementation
-        ; isSigned-correct = error "isSigned-correct evaluated"
-        ; Dec-isSigned     = λ { {vk} {ser} {sig} → ⁇ (extIsSigned (HSVKey.vkey vk) ser sig because error "Dec-isSigned evaluated") }
-        }
-  
-  -- No P2 scripts for now
-  
-  open import Ledger.Script it it
-  open import Ledger.Conway.Conformance.Script it it public
-  
-  instance
-    HSScriptStructure : ScriptStructure
-    HSScriptStructure = record
-      { p1s = P1ScriptStructure-HTL
-      ; hashRespectsUnion = hashRespectsUnion
-      ; ps = HSP2ScriptStructure
-      }
-      where
-        hashRespectsUnion : ∀ {A B ℍ}
-          → Hashable A ℍ → Hashable B ℍ
-          → Hashable (A ⊎ B) ℍ
-        hashRespectsUnion a _ .hash (inj₁ x) = hash ⦃ a ⦄ x
-        hashRespectsUnion _ b .hash (inj₂ y) = hash ⦃ b ⦄ y
-  
-        HSP2ScriptStructure : PlutusStructure
-        HSP2ScriptStructure = record
-          { Implementation
-          ; validPlutusScript = λ _ _ _ _ → ⊤
-          }
-  
-  open import Ledger.PParams it it it hiding (Acnt; DrepThresholds; PoolThresholds)
-  
-  HsGovParams : GovParams
-  HsGovParams = record
-    { Implementation
-    ; ppUpd = let open PParamsDiff in λ where
-        .UpdateT      → PParamsUpdate
-        .updateGroups → modifiedUpdateGroups
-        .applyUpdate  → applyPParamsUpdate
-        .ppWF? {u}    → ppWF u
-    ; ppHashingScheme = it
-    }
-    where
-      open PParamsUpdate
-      -- FIXME Replace `trustMe` with an actual proof
-      ppWF : (u : PParamsUpdate) →
-        ((pp : PParams) →
-        paramsWellFormed pp →
-        paramsWellFormed (applyPParamsUpdate pp u))
-        ⁇
-      ppWF u with paramsUpdateWellFormed? u
-      ... | yes _ = ⁇ (yes trustMe)
-        where
-          postulate
-            trustMe :
-              ((pp : PParams) →
-              paramsWellFormed pp →
-              paramsWellFormed (applyPParamsUpdate pp u))
-      ... | no _  = ⁇ (no trustMe)
-        where
-          postulate
-            trustMe :
-              ¬((pp : PParams) →
-              paramsWellFormed pp →
-              paramsWellFormed (applyPParamsUpdate pp u))
-  
-  instance
-    HSTransactionStructure : TransactionStructure
-    HSTransactionStructure = record
-      { Implementation
-      ; epochStructure  = HSEpochStructure
-      ; globalConstants = HSGlobalConstants
-      ; adHashingScheme = it
-      ; crypto          = HSCrypto
-      ; govParams       = HsGovParams
-      ; txidBytes       = id
-      ; scriptStructure = HSScriptStructure
-      }
-  
-  open TransactionStructure HSTransactionStructure public
-  open import Ledger.Certs govStructure public
-  
-  open import Ledger.Abstract it
-  
-  instance
-    HSAbstractFunctions : AbstractFunctions
-    HSAbstractFunctions = record
-      { Implementation
-      ; txscriptfee = λ tt y → 0
-      ; serSize     = λ v → v
-      ; indexOfImp  = record
-        { indexOfDCert    = λ _ _ → nothing
-        ; indexOfRwdAddr  = λ _ _ → nothing
-        ; indexOfTxIn     = λ _ _ → nothing
-        ; indexOfPolicyId = λ _ _ → nothing
-        ; indexOfVote     = λ _ _ → nothing
-        ; indexOfProposal = λ _ _ → nothing
-        }
-      ; runPLCScript = λ _ _ _ _ → false
-      ; scriptSize = λ _ → 0
-      }
-  
-  open import Ledger.Address Network KeyHash ScriptHash using () public
diff --git a/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda
new file mode 100644
index 000000000..5bdb97903
--- /dev/null
+++ b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda
@@ -0,0 +1,126 @@
+open import Ledger.Conway.Foreign.ExternalFunctions
+
+module Ledger.Conway.Foreign.HSLedger.ExternalStructures (externalFunctions : ExternalFunctions) where
+
+open import Ledger.Crypto
+open import Ledger.Types.Epoch
+open import Ledger.Conway.Foreign.HSLedger.Core
+
+HSGlobalConstants = GlobalConstants ∋ record {Implementation}
+instance
+  HSEpochStructure = EpochStructure  ∋ ℕEpochStructure HSGlobalConstants
+
+  HSCrypto : Crypto
+  HSCrypto = record
+    { Implementation
+    ; pkk = HSPKKScheme
+    }
+    where
+    open ExternalFunctions externalFunctions
+    HSPKKScheme : PKKScheme
+    HSPKKScheme = record
+      { Implementation
+      ; isSigned         = λ a b m → extIsSigned (HSVKey.hvkVKey a) b m ≡ true
+      ; sign             = λ _ _ → zero
+        -- we can't prove these properties since the functions are provided by the Haskell implementation
+      ; isSigned-correct = error "isSigned-correct evaluated"
+      ; Dec-isSigned     = λ { {vk} {ser} {sig} → ⁇ (extIsSigned (HSVKey.hvkVKey vk) ser sig because error "Dec-isSigned evaluated") }
+      }
+
+-- No P2 scripts for now
+
+open import Ledger.Script it it
+open import Ledger.Conway.Conformance.Script it it public
+
+instance
+  HSScriptStructure : ScriptStructure
+  HSScriptStructure = record
+    { p1s = P1ScriptStructure-HTL
+    ; hashRespectsUnion = hashRespectsUnion
+    ; ps = HSP2ScriptStructure
+    }
+    where
+      hashRespectsUnion : ∀ {A B ℍ}
+        → Hashable A ℍ → Hashable B ℍ
+        → Hashable (A ⊎ B) ℍ
+      hashRespectsUnion a _ .hash (inj₁ x) = hash ⦃ a ⦄ x
+      hashRespectsUnion _ b .hash (inj₂ y) = hash ⦃ b ⦄ y
+
+      HSP2ScriptStructure : PlutusStructure
+      HSP2ScriptStructure = record
+        { Implementation
+        ; validPlutusScript = λ _ _ _ _ → ⊤
+        }
+
+open import Ledger.PParams it it it hiding (Acnt; DrepThresholds; PoolThresholds)
+
+HsGovParams : GovParams
+HsGovParams = record
+  { Implementation
+  ; ppUpd = let open PParamsDiff in λ where
+      .UpdateT      → PParamsUpdate
+      .updateGroups → modifiedUpdateGroups
+      .applyUpdate  → applyPParamsUpdate
+      .ppWF? {u}    → ppWF u
+  }
+  where
+    open PParamsUpdate
+    -- FIXME Replace `trustMe` with an actual proof
+    ppWF : (u : PParamsUpdate) →
+      ((pp : PParams) →
+      paramsWellFormed pp →
+      paramsWellFormed (applyPParamsUpdate pp u))
+      ⁇
+    ppWF u with paramsUpdateWellFormed? u
+    ... | yes _ = ⁇ (yes trustMe)
+      where
+        postulate
+          trustMe :
+            ((pp : PParams) →
+            paramsWellFormed pp →
+            paramsWellFormed (applyPParamsUpdate pp u))
+    ... | no _  = ⁇ (no trustMe)
+      where
+        postulate
+          trustMe :
+            ¬((pp : PParams) →
+            paramsWellFormed pp →
+            paramsWellFormed (applyPParamsUpdate pp u))
+
+instance
+  HSTransactionStructure : TransactionStructure
+  HSTransactionStructure = record
+    { Implementation
+    ; epochStructure  = HSEpochStructure
+    ; globalConstants = HSGlobalConstants
+    ; crypto          = HSCrypto
+    ; govParams       = HsGovParams
+    ; txidBytes       = id
+    ; scriptStructure = HSScriptStructure
+    ; adHashingScheme = isHashableSet-ℕ
+    }
+
+open TransactionStructure HSTransactionStructure public
+open import Ledger.Certs govStructure public
+
+open import Ledger.Abstract it
+
+instance
+  HSAbstractFunctions : AbstractFunctions
+  HSAbstractFunctions = record
+    { Implementation
+    ; txscriptfee = λ tt y → 0
+    ; serSize     = λ v → v
+    ; indexOfImp  = record
+      { indexOfDCert    = λ _ _ → nothing
+      ; indexOfRwdAddr  = λ _ _ → nothing
+      ; indexOfTxIn     = λ _ _ → nothing
+      ; indexOfPolicyId = λ _ _ → nothing
+      ; indexOfVote     = λ _ _ → nothing
+      ; indexOfProposal = λ _ _ → nothing
+      }
+    ; runPLCScript = λ _ _ _ _ → false
+    ; scriptSize = λ _ → 0
+    }
+
+open import Ledger.Address Network KeyHash ScriptHash using () public
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
index f1418a8b9..004c027c4 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
@@ -32,7 +32,7 @@ unquoteDecl = do
   hsTypeAlias Redeemer
 
 module _ (ext : ExternalFunctions) where
-  open ExternalStructures ext hiding (Tx; TxBody; inject)
+  open import Ledger.Conway.Foreign.HSLedger.ExternalStructures ext hiding (Tx; TxBody; inject)
   open import Ledger.Conway.Conformance.Utxow.Properties HSTransactionStructure HSAbstractFunctions
   open import Ledger.Conway.Conformance.Utxo.Properties HSTransactionStructure HSAbstractFunctions
 
@@ -81,8 +81,6 @@ module _ (ext : ExternalFunctions) where
        ∷ show (LW.witsVKeyNeeded utxo body)
        ∷ "\nwitsKeyHashes = "
        ∷ show (mapˢ hash (dom vkSigs))
-       --∷ "\ncredsNeeded = "
-       --∷ show (credsNeeded utxo body)
        ∷ []
 
   {-# COMPILE GHC utxow-debug as utxowDebug #-}
diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda
index 0667fb3b8..b51b75a3b 100644
--- a/src/Ledger/PParams.lagda
+++ b/src/Ledger/PParams.lagda
@@ -462,8 +462,6 @@ record PParamsDiff : Type₁ where
 record GovParams : Type₁ where
   field ppUpd : PParamsDiff
   open PParamsDiff ppUpd renaming (UpdateT to PParamsUpdate) public
-  field ppHashingScheme : isHashableSet PParams
-  open isHashableSet ppHashingScheme renaming (THash to PPHash) public
   field ⦃ DecEq-UpdT ⦄ : DecEq PParamsUpdate
 --         ⦃ Show-UpdT ⦄ : Show PParamsUpdate
 \end{code}
diff --git a/src/Ledger/hs-src/Lib.hs b/src/Ledger/hs-src/Lib.hs
index b2aeec46f..9a765c548 100644
--- a/src/Ledger/hs-src/Lib.hs
+++ b/src/Ledger/hs-src/Lib.hs
@@ -6,7 +6,7 @@ module Lib
 import MAlonzo.Code.Ledger.Conway.Foreign.HSTypes              as X
   (HSSet(..), HSMap(..), ComputationResult(..), Rational(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Address     as X
-  (Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..), Addr)
+  (Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..), Addr, HSVKey (..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.PParams     as X
   (DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Transaction as X
diff --git a/src/ScriptVerification/LedgerImplementation.agda b/src/ScriptVerification/LedgerImplementation.agda
index 007e80b15..6aa681026 100644
--- a/src/ScriptVerification/LedgerImplementation.agda
+++ b/src/ScriptVerification/LedgerImplementation.agda
@@ -154,7 +154,6 @@ SVGovParams = record
       .updateGroups           → λ _ → ∅
       .applyUpdate            → λ p _ → p
       .ppWF?                  → ⁇ yes λ _ → id
-  ; ppHashingScheme = it
   }
 
 SVGovStructure : GovStructure