diff --git a/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda b/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda
index d3cdb1b358..4b8622f60e 100644
--- a/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda
+++ b/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda
@@ -4,16 +4,14 @@
 -- TODO: The following should be likely located in Common.
 open import Ledger.Prelude
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 
 module InterfaceLibrary.Ledger
   (crypto : Crypto)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
   where
 
-open import Ledger.PParams crypto es ss using (PParams)
+open import Ledger.PParams using (PParams)
 open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr)
 
 \end{code}
diff --git a/docs/agda-spec/src/Ledger/PParams.lagda b/docs/agda-spec/src/Ledger/PParams.lagda
index 0667fb3b83..39cd3acd6b 100644
--- a/docs/agda-spec/src/Ledger/PParams.lagda
+++ b/docs/agda-spec/src/Ledger/PParams.lagda
@@ -1,59 +1,37 @@
 \section{Protocol Parameters}
 \label{sec:protocol-parameters}
-This section defines the adjustable protocol parameters of the Cardano ledger.
-These parameters are used in block validation and can affect various features of the system,
-such as minimum fees, maximum and minimum sizes of certain components, and more.
+This section defines the adjustable protocol parameters of the Cardano consensus.
+These parameters are used in block header validation and can affect various features
+of the system, such as maximum and minimum sizes of certain components, and more.
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 
 open import Data.Product.Properties
 open import Data.Nat.Properties using (m+1+n≢m)
-open import Data.Rational using (ℚ)
-open import Relation.Nullary.Decidable
-open import Data.List.Relation.Unary.Any using (Any; here; there)
 
 open import Tactic.Derive.DecEq
 open import Tactic.Derive.Show
 
 open import Ledger.Prelude
-open import Ledger.Crypto
-open import Ledger.Script
-open import Ledger.Types.Epoch
 
-module Ledger.PParams
-  (crypto : Crypto )
-  (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  where
+module Ledger.PParams where
 
 private variable
   m n : ℕ
 \end{code}
 
-\begin{NoConway}
-The \AgdaRecord{Acnt} record has two fields, \AgdaField{treasury} and \AgdaField{reserves}, so
-the \AgdaBound{acnt} field in \AgdaRecord{NewEpochState} keeps track of the total assets that
-remain in treasury and reserves.
-
 \begin{figure*}[ht]
 \begin{AgdaMultiCode}
 \begin{code}
-record Acnt : Type where
-\end{code}
-\begin{code}[hide]
-  constructor ⟦_,_⟧ᵃ
-  field
-\end{code}
-\begin{code}
-    treasury reserves : Coin
-
 ProtVer : Type
 ProtVer = ℕ × ℕ
-
+\end{code}
+\begin{code}[hide]
 instance
   Show-ProtVer : Show ProtVer
   Show-ProtVer = Show-×
-
+\end{code}
+\begin{code}
 data pvCanFollow : ProtVer → ProtVer → Type where
   canFollowMajor : pvCanFollow (m , n) (m + 1 , 0)
   canFollowMinor : pvCanFollow (m , n) (m , n + 1)
@@ -62,34 +40,12 @@ data pvCanFollow : ProtVer → ProtVer → Type where
 \caption{Definitions related to protocol parameters}
 \label{fig:protocol-parameter-defs}
 \end{figure*}
-\end{NoConway}
 
 \begin{figure*}[ht]
 \begin{AgdaMultiCode}
 \begin{code}
 data PParamGroup : Type where
-  NetworkGroup     : PParamGroup
-  EconomicGroup    : PParamGroup
-  TechnicalGroup   : PParamGroup
-  GovernanceGroup  : PParamGroup
-  SecurityGroup    : PParamGroup
-
-record DrepThresholds : Type where
-\end{code}
-\begin{code}[hide]
-  field
-\end{code}
-\begin{code}
-    P1 P2a P2b P3 P4 P5a P5b P5c P5d P6 : ℚ
-
-record PoolThresholds : Type where
-\end{code}
-\begin{code}[hide]
-  field
-\end{code}
-\begin{code}
-    Q1 Q2a Q2b Q4 Q5e : ℚ
-
+  NetworkGroup : PParamGroup
 record PParams : Type where
 \end{code}
 \begin{code}[hide]
@@ -97,57 +53,9 @@ record PParams : Type where
 \end{code}
 \emph{Network group}
 \begin{code}
-        maxBlockSize                  : ℕ
-        maxTxSize                     : ℕ
-        maxHeaderSize                 : ℕ
-        maxTxExUnits                  : ExUnits
-        maxBlockExUnits               : ExUnits
-        maxValSize                    : ℕ
-        maxCollateralInputs           : ℕ
-\end{code}
-\begin{code}[hide]
-        pv                            : ProtVer -- retired, keep for now
-\end{code}
-\emph{Economic group}
-\begin{code}
-        a                             : ℕ
-        b                             : ℕ
-        keyDeposit                    : Coin
-        poolDeposit                   : Coin
-        coinsPerUTxOByte              : Coin
-        prices                        : Prices
-        minFeeRefScriptCoinsPerByte   : ℚ
-        maxRefScriptSizePerTx         : ℕ
-        maxRefScriptSizePerBlock      : ℕ
-        refScriptCostStride           : ℕ
-        refScriptCostMultiplier       : ℚ
-\end{code}
-\begin{code}[hide]
-        minUTxOValue                  : Coin -- retired, keep for now
-\end{code}
-\emph{Technical group}
-\begin{code}
-        Emax                          : Epoch
-        nopt                          : ℕ
-        a0                            : ℚ
-        collateralPercentage          : ℕ
-\end{code}
-\begin{code}[hide]
-        -- costmdls                   : Language →/⇀ CostModel (Does not work with DecEq)
-\end{code}
-\begin{code}
-        costmdls                      : CostModel
-\end{code}
-\emph{Governance group}
-\begin{code}
-        poolThresholds                : PoolThresholds
-        drepThresholds                : DrepThresholds
-        ccMinSize                     : ℕ
-        ccMaxTermLength               : ℕ
-        govActionLifetime             : ℕ
-        govActionDeposit              : Coin
-        drepDeposit                   : Coin
-        drepActivity                  : Epoch
+    maxHeaderSize : ℕ
+    maxBlockSize  : ℕ
+    pv            : ProtVer
 \end{code}
 \end{AgdaMultiCode}
 \caption{Protocol parameter definitions}
@@ -157,9 +65,7 @@ record PParams : Type where
 \begin{AgdaMultiCode}
 \begin{code}
 positivePParams : PParams → List ℕ
-positivePParams pp =  ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize ∷ refScriptCostStride
-                      ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
-                      ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
+positivePParams pp = maxHeaderSize ∷ maxBlockSize ∷ []
 \end{code}
 \begin{code}[hide]
   where open PParams pp
@@ -174,9 +80,6 @@ paramsWF-elim : (pp : PParams) → paramsWellFormed pp → (n : ℕ) → n ∈ˡ
 paramsWF-elim pp pwf (suc n) x = z<s
 paramsWF-elim pp pwf 0 0∈ = ⊥-elim (pwf (to ∈-fromList 0∈))
   where open Equivalence
-
-refScriptCostStride>0 : (pp : PParams) → paramsWellFormed pp → (PParams.refScriptCostStride pp) > 0
-refScriptCostStride>0 pp pwf = paramsWF-elim pp pwf (PParams.refScriptCostStride pp) (there (there (there (there (here refl)))))
 \end{code}
 \end{AgdaMultiCode}
 \caption{Protocol parameter well-formedness}
@@ -186,229 +89,17 @@ refScriptCostStride>0 pp pwf = paramsWF-elim pp pwf (PParams.refScriptCostStride
 instance
   Show-ℚ = Show _ ∋ record {M}
     where import Data.Rational.Show as M
-  unquoteDecl DecEq-DrepThresholds = derive-DecEq
-    ((quote DrepThresholds , DecEq-DrepThresholds) ∷ [])
-  unquoteDecl DecEq-PoolThresholds = derive-DecEq
-    ((quote PoolThresholds , DecEq-PoolThresholds) ∷ [])
   unquoteDecl DecEq-PParams        = derive-DecEq
     ((quote PParams , DecEq-PParams) ∷ [])
-  unquoteDecl DecEq-PParamGroup    = derive-DecEq
-    ((quote PParamGroup , DecEq-PParamGroup) ∷ [])
-  unquoteDecl Show-DrepThresholds = derive-Show
-    ((quote DrepThresholds , Show-DrepThresholds) ∷ [])
-  unquoteDecl Show-PoolThresholds = derive-Show
-    ((quote PoolThresholds , Show-PoolThresholds) ∷ [])
   unquoteDecl Show-PParams        = derive-Show
     ((quote PParams , Show-PParams) ∷ [])
-
-module PParamsUpdate where
-  record PParamsUpdate : Type where
-    field
-          maxBlockSize maxTxSize        : Maybe ℕ
-          maxHeaderSize maxValSize      : Maybe ℕ
-          maxCollateralInputs           : Maybe ℕ
-          maxTxExUnits maxBlockExUnits  : Maybe ExUnits
-          pv                            : Maybe ProtVer -- retired, keep for now
-          a b                           : Maybe ℕ
-          keyDeposit                    : Maybe Coin
-          poolDeposit                   : Maybe Coin
-          coinsPerUTxOByte              : Maybe Coin
-          prices                        : Maybe Prices
-          minFeeRefScriptCoinsPerByte   : Maybe ℚ
-          maxRefScriptSizePerTx         : Maybe ℕ
-          maxRefScriptSizePerBlock      : Maybe ℕ
-          refScriptCostStride           : Maybe ℕ
-          refScriptCostMultiplier       : Maybe ℚ
-          minUTxOValue                  : Maybe Coin -- retired, keep for now
-          a0                            : Maybe ℚ
-          Emax                          : Maybe Epoch
-          nopt                          : Maybe ℕ
-          collateralPercentage          : Maybe ℕ
-          costmdls                      : Maybe CostModel
-          drepThresholds                : Maybe DrepThresholds
-          poolThresholds                : Maybe PoolThresholds
-          govActionLifetime             : Maybe ℕ
-          govActionDeposit drepDeposit  : Maybe Coin
-          drepActivity                  : Maybe Epoch
-          ccMinSize ccMaxTermLength     : Maybe ℕ
-  
-  paramsUpdateWellFormed : PParamsUpdate → Type
-  paramsUpdateWellFormed ppu =
-       just 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize
-                         ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
-                         ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
-    where open PParamsUpdate ppu
-  
-  paramsUpdateWellFormed? : ( u : PParamsUpdate ) → Dec (paramsUpdateWellFormed u)
-  paramsUpdateWellFormed? u = ¿ paramsUpdateWellFormed u ¿
-  
-  modifiesNetworkGroup : PParamsUpdate → Bool
-  modifiesNetworkGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just maxBlockSize
-      ∷ is-just maxTxSize
-      ∷ is-just maxHeaderSize
-      ∷ is-just maxValSize
-      ∷ is-just maxCollateralInputs
-      ∷ is-just maxTxExUnits
-      ∷ is-just maxBlockExUnits
-      ∷ is-just pv
-      ∷ [])
-  
-  modifiesEconomicGroup : PParamsUpdate → Bool
-  modifiesEconomicGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just a
-      ∷ is-just b
-      ∷ is-just keyDeposit
-      ∷ is-just poolDeposit
-      ∷ is-just coinsPerUTxOByte
-      ∷ is-just minFeeRefScriptCoinsPerByte
-      ∷ is-just maxRefScriptSizePerTx
-      ∷ is-just maxRefScriptSizePerBlock
-      ∷ is-just refScriptCostStride
-      ∷ is-just refScriptCostMultiplier
-      ∷ is-just prices
-      ∷ is-just minUTxOValue
-      ∷ [])
-  
-  modifiesTechnicalGroup : PParamsUpdate → Bool
-  modifiesTechnicalGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just a0
-      ∷ is-just Emax
-      ∷ is-just nopt
-      ∷ is-just collateralPercentage
-      ∷ is-just costmdls
-      ∷ [])
-  
-  modifiesGovernanceGroup : PParamsUpdate → Bool
-  modifiesGovernanceGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just drepThresholds
-      ∷ is-just poolThresholds
-      ∷ is-just govActionLifetime
-      ∷ is-just govActionDeposit
-      ∷ is-just drepDeposit
-      ∷ is-just drepActivity
-      ∷ is-just ccMinSize
-      ∷ is-just ccMaxTermLength
-      ∷ [])
-  
-  modifiedUpdateGroups : PParamsUpdate → ℙ PParamGroup
-  modifiedUpdateGroups ppu =
-    ( modifiesNetworkGroup    ?═⇒ NetworkGroup
-    ∪ modifiesEconomicGroup   ?═⇒ EconomicGroup
-    ∪ modifiesTechnicalGroup  ?═⇒ TechnicalGroup
-    ∪ modifiesGovernanceGroup ?═⇒ GovernanceGroup
-    )
-    where
-      _?═⇒_ : (PParamsUpdate → Bool) → PParamGroup → ℙ PParamGroup
-      pred ?═⇒ grp = if pred ppu then ❴ grp ❵ else ∅
-  
-  _?↗_ : ∀ {A : Type} → Maybe A → A → A
-  just x ?↗ _ = x
-  nothing ?↗ x = x
-  
-  ≡-update : ∀ {A : Type} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x ⇔ (u ≡ just x ⊎ (p ≡ x × u ≡ nothing))
-  ≡-update {u} {p} {x} = mk⇔ to from
-    where
-      to : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x → (u ≡ just x ⊎ (p ≡ x × u ≡ nothing))
-      to {u = just x} refl = inj₁ refl
-      to {u = nothing} refl = inj₂ (refl , refl)
-  
-      from : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ≡ just x ⊎ (p ≡ x × u ≡ nothing) → u ?↗ p ≡ x
-      from (inj₁ refl) = refl
-      from (inj₂ (refl , refl)) = refl
-  
-  applyPParamsUpdate : PParams → PParamsUpdate → PParams
-  applyPParamsUpdate pp ppu =
-    record
-      { maxBlockSize                = U.maxBlockSize ?↗ P.maxBlockSize
-      ; maxTxSize                   = U.maxTxSize ?↗ P.maxTxSize
-      ; maxHeaderSize               = U.maxHeaderSize ?↗ P.maxHeaderSize
-      ; maxValSize                  = U.maxValSize ?↗ P.maxValSize
-      ; maxCollateralInputs         = U.maxCollateralInputs ?↗ P.maxCollateralInputs
-      ; maxTxExUnits                = U.maxTxExUnits ?↗ P.maxTxExUnits
-      ; maxBlockExUnits             = U.maxBlockExUnits ?↗ P.maxBlockExUnits
-      ; pv                          = U.pv ?↗ P.pv
-      ; a                           = U.a ?↗ P.a
-      ; b                           = U.b ?↗ P.b
-      ; keyDeposit                  = U.keyDeposit ?↗ P.keyDeposit
-      ; poolDeposit                 = U.poolDeposit ?↗ P.poolDeposit
-      ; coinsPerUTxOByte            = U.coinsPerUTxOByte ?↗ P.coinsPerUTxOByte
-      ; minFeeRefScriptCoinsPerByte = U.minFeeRefScriptCoinsPerByte ?↗ P.minFeeRefScriptCoinsPerByte
-      ; maxRefScriptSizePerTx       = U.maxRefScriptSizePerTx ?↗ P.maxRefScriptSizePerTx
-      ; maxRefScriptSizePerBlock    = U.maxRefScriptSizePerBlock ?↗ P.maxRefScriptSizePerBlock
-      ; refScriptCostStride         = U.refScriptCostStride ?↗ P.refScriptCostStride
-      ; refScriptCostMultiplier     = U.refScriptCostMultiplier ?↗ P.refScriptCostMultiplier
-      ; prices                      = U.prices ?↗ P.prices
-      ; minUTxOValue                = U.minUTxOValue ?↗ P.minUTxOValue
-      ; a0                          = U.a0 ?↗ P.a0
-      ; Emax                        = U.Emax ?↗ P.Emax
-      ; nopt                        = U.nopt ?↗ P.nopt
-      ; collateralPercentage        = U.collateralPercentage ?↗ P.collateralPercentage
-      ; costmdls                    = U.costmdls ?↗ P.costmdls
-      ; drepThresholds              = U.drepThresholds ?↗ P.drepThresholds
-      ; poolThresholds              = U.poolThresholds ?↗ P.poolThresholds
-      ; govActionLifetime           = U.govActionLifetime ?↗ P.govActionLifetime
-      ; govActionDeposit            = U.govActionDeposit ?↗ P.govActionDeposit
-      ; drepDeposit                 = U.drepDeposit ?↗ P.drepDeposit
-      ; drepActivity                = U.drepActivity ?↗ P.drepActivity
-      ; ccMinSize                   = U.ccMinSize ?↗ P.ccMinSize
-      ; ccMaxTermLength             = U.ccMaxTermLength ?↗ P.ccMaxTermLength
-      }
-    where
-      open module P = PParams pp
-      open module U = PParamsUpdate ppu
-
-  instance
-    unquoteDecl DecEq-PParamsUpdate  = derive-DecEq
-      ((quote PParamsUpdate , DecEq-PParamsUpdate) ∷ [])
 \end{code}
-% Retiring ProtVer's documentation since ProtVer is retired.
-% \ProtVer represents the protocol version used in the Cardano ledger.
-% It is a pair of natural numbers, representing the major and minor version,
-% respectively.
 
-\PParams contains parameters used in the Cardano ledger, which we group according
+\PParams contains parameters used in the Cardano consensus, which we group according
 to the general purpose that each parameter serves.
-\begin{itemize}
-  \item \NetworkGroup: parameters related to the network settings;
-  \item \EconomicGroup: parameters related to the economic aspects of the ledger;
-  \item \TechnicalGroup: parameters related to technical settings;
-  \item \GovernanceGroup: parameters related to governance settings;
-  \item \SecurityGroup: parameters that can impact the security of the system.
-\end{itemize}
-
-The first four groups have the property that every protocol parameter
-is associated to precisely one of these groups. The \SecurityGroup is
-special: a protocol parameter may or may not be in the
-\SecurityGroup. So, each protocol parameter belongs to at least one
-and at most two groups. Note that in \cite{cip1694} there is no
-\SecurityGroup, but there is the concept of security-relevant protocol
-parameters. The difference between these notions is only social, so we
-implement security-relevant protocol parameters as a group.
-
-The purpose of the groups is to determine voting thresholds for
-proposals aiming to change parameters. The thresholds depend on the
-groups of the parameters contained in such a proposal.
-
-These new parameters are declared in
-Figure~\ref{fig:protocol-parameter-declarations} and denote the
-following concepts.
 
 \begin{itemize}
-  \item \drepThresholds: governance thresholds for \DReps; these are rational numbers
-  named \Pone, \Ptwoa, \Ptwob, \Pthree, \Pfour, \Pfivea, \Pfiveb, \Pfivec, \Pfived, and \Psix;
-  \item \poolThresholds: pool-related governance thresholds; these are rational numbers named \Qone, \Qtwoa, \Qtwob, \Qfour and \Qfivee;
-  \item \ccMinSize: minimum constitutional committee size;
-  \item \ccMaxTermLength: maximum term limit (in epochs) of constitutional committee members;
-  \item \govActionLifetime: governance action expiration;
-  \item \govActionDeposit: governance action deposit;
-  \item \drepDeposit: \DRep deposit amount;
-  \item \drepActivity: \DRep activity period;
-  \item \minimumAVS: the minimum active voting threshold.
+  \item \NetworkGroup: parameters related to the network settings;
 \end{itemize}
 
 Figure~\ref{fig:protocol-parameter-declarations} also defines the
@@ -425,45 +116,3 @@ instance
   ... | yes refl | no ¬p    = yes canFollowMajor
   ... | yes refl | yes p    = ⊥-elim $ m+1+n≢m m $ ×-≡,≡←≡ p .proj₁
 \end{code}
-
-Finally, to update parameters we introduce an abstract type. An update
-can be applied and it has a set of groups associated with it. An
-update is well formed if it has at least one group (i.e. if it updates
-something) and if it preserves well-formedness.
-
-\begin{figure*}[ht]
-\begin{AgdaMultiCode}
-\begin{code}[hide]
-record PParamsDiff : Type₁ where
-  field
-\end{code}
-\emph{Abstract types \& functions}
-\begin{code}
-    UpdateT : Type
-    applyUpdate : PParams → UpdateT → PParams
-    updateGroups : UpdateT → ℙ PParamGroup
-
-\end{code}
-\begin{code}[hide]
-    ⦃ ppWF? ⦄ : ∀ {u} → (∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)) ⁇
-\end{code}
-\emph{Well-formedness condition}
-\begin{code}
-
-  ppdWellFormed : UpdateT → Type
-  ppdWellFormed u = updateGroups u ≢ ∅
-    × ∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)
-\end{code}
-\end{AgdaMultiCode}
-\caption{Abstract type for parameter updates}
-\label{fig:pp-update-type}
-\end{figure*}
-\begin{code}[hide]
-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/docs/agda-spec/src/Ledger/Script.lagda b/docs/agda-spec/src/Ledger/Script.lagda
deleted file mode 100644
index b82be2f127..0000000000
--- a/docs/agda-spec/src/Ledger/Script.lagda
+++ /dev/null
@@ -1,184 +0,0 @@
-\section{Scripts}
-\begin{code}[hide]
-{-# OPTIONS --safe #-}
-
-open import Algebra using (CommutativeMonoid)
-open import Algebra.Morphism
-open import Data.List.Relation.Unary.All using (All; []; _∷_; all?; uncons)
-open import Data.List.Relation.Unary.Any
-open import Data.Nat.Properties using (+-0-commutativeMonoid; suc-injective)
-
-open import Data.List.Relation.Unary.MOf
-
-open import Tactic.Derive.DecEq
-open import Tactic.Inline
-
-open import Ledger.Prelude hiding (All; Any; all?; any?; _∷ʳ_; uncons; _⊆_)
-open import Ledger.Crypto
-open import Ledger.Types.Epoch
-
-module Ledger.Script
-  (crypto : _) (open Crypto crypto)
-  (es     : _) (open EpochStructure es)
-  where
-
-record P1ScriptStructure : Type₁ where
-  field P1Script : Type
-        validP1Script : ℙ KeyHashˢ → Maybe Slot × Maybe Slot → P1Script → Type
-        ⦃ Dec-validP1Script ⦄ : validP1Script ⁇³
-        ⦃ Hashable-P1Script ⦄ : Hashable P1Script ScriptHash
-        ⦃ DecEq-P1Script    ⦄ : DecEq P1Script
-
-record PlutusStructure : Type₁ where
-  field Dataʰ : HashableSet
-        Language PlutusScript CostModel Prices LangDepView ExUnits : Type
-        PlutusV1 PlutusV2 PlutusV3   : Language
-        ⦃ ExUnit-CommutativeMonoid ⦄ : IsCommutativeMonoid' 0ℓ 0ℓ ExUnits
-        ⦃ Hashable-PlutusScript    ⦄ : Hashable PlutusScript ScriptHash
-        ⦃ DecEq-Language           ⦄ : DecEq Language
-        ⦃ DecEq-CostModel          ⦄ : DecEq CostModel
-        ⦃ DecEq-LangDepView        ⦄ : DecEq LangDepView
-        ⦃ Show-CostModel           ⦄ : Show CostModel
-
-  field  _≥ᵉ_              : ExUnits → ExUnits → Type
-         ⦃ DecEq-ExUnits ⦄ : DecEq ExUnits
-         ⦃ DecEQ-Prices  ⦄ : DecEq Prices
-         ⦃ Show-ExUnits  ⦄ : Show ExUnits
-         ⦃ Show-Prices   ⦄ : Show Prices
-
-  open HashableSet Dataʰ renaming (T to Data; THash to DataHash) public
-
-  -- Type aliases for Data
-  Datum    = Data
-  Redeemer = Data
-
-  field validPlutusScript : CostModel → List Data → ExUnits → PlutusScript → Type
-        ⦃ Dec-validPlutusScript ⦄ : ∀ {x} → (validPlutusScript x ⁇³)
-        language : PlutusScript → Language
-        toData : ∀ {A : Type} → A → Data
-\end{code}
-We define \Timelock scripts here. They can verify the presence of keys and whether a transaction happens in a certain slot interval. These scripts are executed as part of the regular witnessing.
-\begin{figure*}[h]
-\begin{code}
-data Timelock : Type where
-  RequireAllOf       : List Timelock      → Timelock
-  RequireAnyOf       : List Timelock      → Timelock
-  RequireMOf         : ℕ → List Timelock  → Timelock
-  RequireSig         : KeyHashˢ           → Timelock
-  RequireTimeStart   : Slot               → Timelock
-  RequireTimeExpire  : Slot               → Timelock
-\end{code}
-\begin{code}[hide]
-unquoteDecl DecEq-Timelock = derive-DecEq ((quote Timelock , DecEq-Timelock) ∷ [])
-
-private variable
-  s : Timelock
-  ss ss' : List Timelock
-  m : ℕ
-  x : KeyHashˢ
-  a l r : Slot
-
-open import Data.List.Relation.Binary.Sublist.Ext
-open import Data.List.Relation.Binary.Sublist.Propositional as S
-import Data.Maybe.Relation.Unary.Any as M
-\end{code}
-\begin{code}[hide]
-data
-\end{code}
-\begin{code}
-  evalTimelock (khs : ℙ KeyHashˢ) (I : Maybe Slot × Maybe Slot) : Timelock → Type where
-  evalAll  : All (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireAllOf ss)
-  evalAny  : Any (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireAnyOf ss)
-  evalMOf  : MOf m (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireMOf m ss)
-  evalSig  : x ∈ khs
-           → (evalTimelock khs I) (RequireSig x)
-  evalTSt  : M.Any (a ≤_) (I .proj₁)
-           → (evalTimelock khs I) (RequireTimeStart a)
-  evalTEx  : M.Any (_≤ a) (I .proj₂)
-           → (evalTimelock khs I) (RequireTimeExpire a)
-\end{code}
-\caption{Timelock scripts and their evaluation}
-\label{fig:defs:timelock}
-\end{figure*}
-
-\begin{code}[hide]
-instance
-  Dec-evalTimelock : evalTimelock ⁇³
-  Dec-evalTimelock {khs} {I} {tl} .dec = go? tl
-    where mutual
-      go = evalTimelock khs I
-
-      -- ** inversion principles for `evalTimelock`
-      evalAll˘ : ∀ {ss} → go (RequireAllOf ss) → All go ss
-      evalAll˘ (evalAll p) = p
-
-      evalAny˘ : ∀ {ss} → go (RequireAnyOf ss) → Any go ss
-      evalAny˘ (evalAny p) = p
-
-      evalTSt˘ : go (RequireTimeStart a) → M.Any (a ≤_) (I .proj₁)
-      evalTSt˘ (evalTSt p) = p
-
-      evalTEx˘ : go (RequireTimeExpire a) → M.Any (_≤ a) (I .proj₂)
-      evalTEx˘ (evalTEx p) = p
-
-      evalSig˘ : go (RequireSig x) → x ∈ khs
-      evalSig˘ (evalSig p) = p
-
-      evalMOf˘ : ∀ {m xs}
-        → go (RequireMOf m xs)
-        → MOf m go xs
-      evalMOf˘ (evalMOf p) = p
-
-      -- ** inlining recursive decision procedures to please the termination checker
-      MOf-go? : ∀ m xs → Dec (MOf m go xs)
-      unquoteDef MOf-go? = inline MOf-go? (quoteTerm (MOf? go?))
-
-      all-go? : Decidable¹ (All go)
-      unquoteDef all-go? = inline all-go? (quoteTerm (all? go?))
-
-      any-go? : Decidable¹ (Any go)
-      unquoteDef any-go? = inline any-go? (quoteTerm (any? go?))
-
-      -- ** the actual decision procedure
-      go? : Decidable¹ go
-      go? = λ where
-        (RequireAllOf ss)     → mapDec evalAll evalAll˘ (all-go? ss)
-        (RequireAnyOf ss)     → mapDec evalAny evalAny˘ (any-go? ss)
-        (RequireSig x)        → mapDec evalSig evalSig˘ dec
-        (RequireTimeStart a)  → mapDec evalTSt evalTSt˘ dec
-        (RequireTimeExpire a) → mapDec evalTEx evalTEx˘ dec
-        (RequireMOf m xs)     → mapDec evalMOf evalMOf˘ (MOf-go? m xs)
-
-P1ScriptStructure-TL : ⦃ Hashable Timelock ScriptHash ⦄ → P1ScriptStructure
-P1ScriptStructure-TL = record
-  { P1Script = Timelock
-  ; validP1Script = evalTimelock }
-
-record ScriptStructure : Type₁ where
-  field hashRespectsUnion :
-          {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
-        ⦃ Hash-Timelock ⦄ : Hashable Timelock ScriptHash
-
-  p1s : P1ScriptStructure
-  p1s = P1ScriptStructure-TL
-  open P1ScriptStructure p1s public
-
-  field ps : PlutusStructure
-  open PlutusStructure ps public
-    renaming ( PlutusScript       to P2Script
-             ; validPlutusScript  to validP2Script
-             )
-
-  Script = P1Script ⊎ P2Script
-
-  open import Data.Empty
-  open import Agda.Builtin.Equality
-  open import Relation.Binary.PropositionalEquality
-
-  instance
-    Hashable-Script : Hashable Script ScriptHash
-    Hashable-Script = hashRespectsUnion Hashable-P1Script Hashable-PlutusScript
-\end{code}
diff --git a/docs/agda-spec/src/Spec/BlockDefinitions.lagda b/docs/agda-spec/src/Spec/BlockDefinitions.lagda
index 0a728a4830..b94acc3a0b 100644
--- a/docs/agda-spec/src/Spec/BlockDefinitions.lagda
+++ b/docs/agda-spec/src/Spec/BlockDefinitions.lagda
@@ -7,17 +7,15 @@
 open import Spec.BaseTypes using (Nonces)
 open import Ledger.Prelude
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 
 module Spec.BlockDefinitions
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)  
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
   where
 
-open import Ledger.PParams crypto es ss using (ProtVer)
+open import Ledger.PParams using (ProtVer)
 
 record BlockStructure : Type₁ where
   field
diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda
index f1adba653a..18c8d18887 100644
--- a/docs/agda-spec/src/Spec/ChainHead.lagda
+++ b/docs/agda-spec/src/Spec/ChainHead.lagda
@@ -27,7 +27,6 @@ open import InterfaceLibrary.Ledger
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -35,18 +34,17 @@ module Spec.ChainHead
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   (rs     : _) (open RationalExtStructure rs)  
   where
 
 open import Spec.BaseTypes crypto using (OCertCounters)
-open import Spec.TickForecast crypto es ss li
+open import Spec.TickForecast crypto es li
 open import Spec.TickNonce crypto es nonces
-open import Spec.Protocol crypto nonces es ss bs af rs
-open import Ledger.PParams crypto es ss using (PParams; ProtVer)
+open import Spec.Protocol crypto nonces es bs af rs
+open import Ledger.PParams using (PParams; ProtVer)
 open import Ledger.Prelude
 
 \end{code}
diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda
index af6b1d58cb..13fe48fad7 100644
--- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda
+++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda
@@ -4,7 +4,6 @@ open import InterfaceLibrary.Ledger
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -12,23 +11,22 @@ module Spec.ChainHead.Properties
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   (rs     : _) (open RationalExtStructure rs)
   where
 
 open import Tactic.GenError
 open import Ledger.Prelude
-open import Ledger.PParams crypto es ss using (PParams; ProtVer)
-open import Spec.TickForecast crypto es ss li
-open import Spec.TickForecast.Properties crypto es ss li
+open import Ledger.PParams using (PParams; ProtVer)
+open import Spec.TickForecast crypto es li
+open import Spec.TickForecast.Properties crypto es li
 open import Spec.TickNonce crypto es nonces
 open import Spec.TickNonce.Properties crypto es nonces
-open import Spec.Protocol crypto nonces es ss bs af rs
-open import Spec.Protocol.Properties crypto nonces es ss bs af rs
-open import Spec.ChainHead crypto nonces es ss bs af li rs
+open import Spec.Protocol crypto nonces es bs af rs
+open import Spec.Protocol.Properties crypto nonces es bs af rs
+open import Spec.ChainHead crypto nonces es bs af li rs
 
 instance
 
diff --git a/docs/agda-spec/src/Spec/OperationalCertificate.lagda b/docs/agda-spec/src/Spec/OperationalCertificate.lagda
index ea8f02ece7..c1a4661ffa 100644
--- a/docs/agda-spec/src/Spec/OperationalCertificate.lagda
+++ b/docs/agda-spec/src/Spec/OperationalCertificate.lagda
@@ -10,7 +10,6 @@ and consists of the mapping of operation certificate issue numbers. Its signal i
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
@@ -19,8 +18,7 @@ module Spec.OperationalCertificate
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   where
 
diff --git a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda
index 53cce7cd4e..5373f3b03d 100644
--- a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda
+++ b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
@@ -10,14 +9,13 @@ module Spec.OperationalCertificate.Properties
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   where
 
 open import Ledger.Prelude
 open import Data.Maybe.Relation.Unary.Any as M
-open import Spec.OperationalCertificate crypto nonces es ss bs af
+open import Spec.OperationalCertificate crypto nonces es bs af
 
 instance
 
diff --git a/docs/agda-spec/src/Spec/Protocol.lagda b/docs/agda-spec/src/Spec/Protocol.lagda
index c145fbaf2d..e472fef9bd 100644
--- a/docs/agda-spec/src/Spec/Protocol.lagda
+++ b/docs/agda-spec/src/Spec/Protocol.lagda
@@ -23,7 +23,6 @@ Its state is shown in Figure~\ref{fig:ts-types:prtcl} and consists of
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -31,14 +30,13 @@ module Spec.Protocol
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   (rs     : _) (open RationalExtStructure rs)
   where
 
 open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr; lookupPoolDistr)
-open import Spec.OperationalCertificate crypto nonces es ss bs af
+open import Spec.OperationalCertificate crypto nonces es bs af
 open import Spec.UpdateNonce crypto nonces es
 open import Spec.BaseTypes crypto using (OCertCounters)
 open import Data.Rational as ℚ using (ℚ; 0ℚ; 1ℚ)
diff --git a/docs/agda-spec/src/Spec/Protocol/Properties.agda b/docs/agda-spec/src/Spec/Protocol/Properties.agda
index b682a7f83d..624bc64424 100644
--- a/docs/agda-spec/src/Spec/Protocol/Properties.agda
+++ b/docs/agda-spec/src/Spec/Protocol/Properties.agda
@@ -3,7 +3,6 @@
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -11,8 +10,7 @@ module Spec.Protocol.Properties
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   (rs     : _) (open RationalExtStructure rs)
   where
@@ -20,12 +18,12 @@ module Spec.Protocol.Properties
 open import Data.Rational as ℚ using (1ℚ)
 open import Ledger.Prelude
 open import Tactic.GenError
-open import Spec.Protocol crypto nonces es ss bs af rs
+open import Spec.Protocol crypto nonces es bs af rs
 open import Spec.BaseTypes crypto using (OCertCounters)
 open import Spec.UpdateNonce crypto nonces es
 open import Spec.UpdateNonce.Properties crypto nonces es
-open import Spec.OperationalCertificate crypto nonces es ss bs af
-open import Spec.OperationalCertificate.Properties crypto nonces es ss bs af
+open import Spec.OperationalCertificate crypto nonces es bs af
+open import Spec.OperationalCertificate.Properties crypto nonces es bs af
 open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr; lookupPoolDistr)
 
 private
diff --git a/docs/agda-spec/src/Spec/TickForecast.lagda b/docs/agda-spec/src/Spec/TickForecast.lagda
index 53c648e112..c4350e4bca 100644
--- a/docs/agda-spec/src/Spec/TickForecast.lagda
+++ b/docs/agda-spec/src/Spec/TickForecast.lagda
@@ -9,15 +9,13 @@ and its signal is the current slot.
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import InterfaceLibrary.Ledger
 
 module Spec.TickForecast
   (crypto : Crypto)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   where
 
 open import Ledger.Prelude
diff --git a/docs/agda-spec/src/Spec/TickForecast/Properties.agda b/docs/agda-spec/src/Spec/TickForecast/Properties.agda
index 8eea212058..7e890d1055 100644
--- a/docs/agda-spec/src/Spec/TickForecast/Properties.agda
+++ b/docs/agda-spec/src/Spec/TickForecast/Properties.agda
@@ -1,19 +1,17 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import InterfaceLibrary.Ledger
 
 module Spec.TickForecast.Properties
   (crypto : Crypto)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   where
 
 open import Ledger.Prelude
-open import Spec.TickForecast crypto es ss li
+open import Spec.TickForecast crypto es li
 
 instance
 
diff --git a/docs/agda-spec/src/Spec/TickNonce.lagda b/docs/agda-spec/src/Spec/TickNonce.lagda
index 663a09e12b..c3da798baf 100644
--- a/docs/agda-spec/src/Spec/TickNonce.lagda
+++ b/docs/agda-spec/src/Spec/TickNonce.lagda
@@ -11,7 +11,6 @@ Its state consists of the epoch nonce \afld{η₀} and the previous epoch's last
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)
 
diff --git a/docs/agda-spec/src/Spec/TickNonce/Properties.agda b/docs/agda-spec/src/Spec/TickNonce/Properties.agda
index 52d49cbcaf..46ccfc7edb 100644
--- a/docs/agda-spec/src/Spec/TickNonce/Properties.agda
+++ b/docs/agda-spec/src/Spec/TickNonce/Properties.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)