Synchronize local copy of the Ledger stuff to include latest changes

docs/agda-spec/src/Axiom/Set.agda

@@ -97,6 +97,9 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
   finite : Set A → Type ℓ
   finite X = ∃[ l ] ∀ {a} → a ∈ X ⇔ a ∈ˡ l
 
+  Show-finite : ⦃ Show A ⦄ → Show (Σ (Set A) finite)
+  Show.show Show-finite (X , (l , _)) = Show-List .show l
+
   weakly-finite : Set A → Type ℓ
   weakly-finite X = ∃[ l ] ∀ {a} → a ∈ X → a ∈ˡ l
 
@@ -291,6 +294,11 @@ record Theoryᶠ : Type₁ where
   lengthˢ : ⦃ DecEq A ⦄ → Set A → ℕ
   lengthˢ X = card (X , DecEq⇒strongly-finite X)
 
+  module _ {A : Type} ⦃ _ : Show A ⦄ where
+    instance
+      Show-Set : Show (Set A)
+      Show-Set .show = λ x → Show-finite .show (x , (finiteness x))
+
 -- set theories with an infinite set (containing all natural numbers)
 record Theoryⁱ : Type₁ where
   field theory : Theory
@@ -307,30 +315,32 @@ record Theoryᵈ : Type₁ where
   field
     ∈-sp : ⦃ DecEq A ⦄ → spec-∈ A
     _∈?_ : ⦃ DecEq A ⦄ → Decidable² (_∈_ {A = A})
-    all? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) {X : Set A} → Dec (All P X)
-    any? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) (X : Set A) → Dec (Any P X)
-
-  module _ {A : Type} ⦃ _ : DecEq A ⦄ where
+    all? : {P : A → Type} (P? : Decidable¹ P) {X : Set A} → Dec (All P X)
+    any? : {P : A → Type} (P? : Decidable¹ P) (X : Set A) → Dec (Any P X)
 
-    _∈ᵇ_ : A → Set A → Bool
-    a ∈ᵇ X = ⌊ a ∈? X ⌋
-
-    instance
-      Dec-∈ : _∈_ {A = A} ⁇²
-      Dec-∈ = ⁇² _∈?_
 
-    module _ {P : A → Type} ⦃ _ : P ⁇¹ ⦄ where instance
+  module _ {A : Type} {P : A → Type} where
+    module _ ⦃ _ : P ⁇¹ ⦄ where instance
       Dec-Allˢ : All P ⁇¹
       Dec-Allˢ = ⁇¹ λ x → all? dec¹ {x}
 
       Dec-Anyˢ : Any P ⁇¹
       Dec-Anyˢ = ⁇¹ any? dec¹
 
-    module _ {P : A → Type} (P? : Decidable¹ P) where
+    module _ (P? : Decidable¹ P) where
       allᵇ anyᵇ : (X : Set A) → Bool
       allᵇ X = ⌊ all? P? {X} ⌋
       anyᵇ X = ⌊ any? P? X   ⌋
 
+  module _ {A : Type} ⦃ _ : DecEq A ⦄ where
+
+    _∈ᵇ_ : A → Set A → Bool
+    a ∈ᵇ X = ⌊ a ∈? X ⌋
+
+    instance
+      Dec-∈ : _∈_ {A = A} ⁇²
+      Dec-∈ = ⁇² _∈?_
+
     _ = _∈_  {A = A} ⁇² ∋ it
     _ = _⊆_  {A = A} ⁇² ∋ it
     _ = _≡ᵉ_ {A = A} ⁇² ∋ it

docs/agda-spec/src/Axiom/Set/Map.agda

@@ -289,6 +289,9 @@ mapPartial-uniq {f = f} prop {a} {b} {b'} p q =
 mapMaybeWithKeyᵐ : (A → B → Maybe B') → Map A B → Map A B'
 mapMaybeWithKeyᵐ f (rel , prop) = mapMaybeWithKey f rel , mapPartial-uniq {f = f} prop
 
+mapFromPartialFun : (A → Maybe B) → Set A → Map A B
+mapFromPartialFun f s = mapMaybeWithKeyᵐ (λ _ → f) (idMap s)
+
 module Restrictionᵐ (sp-∈ : spec-∈ A) where
   private module R = Restriction sp-∈
   open Unionᵐ sp-∈

docs/agda-spec/src/Interface/ComputationalRelation.agda

@@ -161,13 +161,14 @@ module _ {STS : C → S → Sig → S → Type} (comp comp' : Computational STS
   compute-ext≡ = ExtendedRel-rightUnique comp
     (ExtendedRel-compute comp) (ExtendedRel-compute comp')
 
-Computational⇒Dec' :
-  ⦃ _ : DecEq S ⦄ {STS : C → S → Sig → S → Type} ⦃ comp : Computational STS Err ⦄
-  → Dec (STS c s sig s')
-Computational⇒Dec' ⦃ comp = comp ⦄ = Computational⇒Dec comp
-
 open Computational ⦃...⦄
 
+Computational⇒Dec' :
+  {STS : C → S → Sig → S → Type} ⦃ comp : Computational STS Err ⦄ → Dec (∃[ s' ] STS c s sig s')
+Computational⇒Dec' with computeProof _ _ _ in eq
+... | success x = yes x
+... | failure x = no λ (_ , h) → failure⇒∀¬STS (-, cong (map proj₁) eq) _ h
+
 record InjectError Err₁ Err₂ : Type where
   field injectError : Err₁ → Err₂
 

docs/agda-spec/src/Interface/HasAdd/Instance.agda

@@ -4,10 +4,14 @@ module Interface.HasAdd.Instance where
 open import Interface.HasAdd
 open import Data.Integer as ℤ using (ℤ)
 open import Data.Nat     as ℕ using (ℕ)
+open import Data.String  as Str
 
 instance
   addInt : HasAdd ℤ
   addInt ._+_ = ℤ._+_
 
   addNat : HasAdd ℕ
   addNat ._+_ = ℕ._+_
+
+  addString : HasAdd String
+  addString ._+_ = Str._++_

docs/agda-spec/src/Interface/IsSet.agda

@@ -31,6 +31,11 @@ All-syntax : ∀ {A X} ⦃ _ : IsSet X A ⦄ → (A → Type) → X → Type
 All-syntax P X = All P (toSet X)
 syntax All-syntax (λ x → P) l = ∀[ x ∈ l ] P
 
+infix 2 Ex-syntax
+Ex-syntax : ∀ {A X} ⦃ _ : IsSet X A ⦄ → (A → Type) → X → Type
+Ex-syntax P X = Any P (toSet X)
+syntax Ex-syntax (λ x → P) l = ∃[ x ∈ l ] P
+
 module _ ⦃ _ : IsSet X (A × B) ⦄ where
   dom : X → Set A
   dom = Rel.dom ∘ toSet

docs/agda-spec/src/Ledger/BaseTypes.lagda

@@ -1,4 +1,4 @@
-\section{Base types}
+\section{Base Types}
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 

docs/agda-spec/src/Ledger/Crypto.lagda

@@ -44,6 +44,7 @@ record isHashableSet (T : Type) : Set₁ where
   constructor mkIsHashableSet
   field THash : Type
         ⦃ DecEq-THash ⦄ : DecEq      THash
+        ⦃ Show-THash  ⦄ : Show       THash
         ⦃ DecEq-T     ⦄ : DecEq    T
         ⦃ T-Hashable  ⦄ : Hashable T THash
 open isHashableSet

docs/agda-spec/src/Ledger/PParams.lagda

@@ -1,4 +1,4 @@
-\section{Protocol parameters}
+\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,
@@ -12,6 +12,7 @@ open import Data.Rational using (ℚ)
 open import Relation.Nullary.Decidable
 
 open import Tactic.Derive.DecEq
+open import Tactic.Derive.Show
 
 open import Ledger.Prelude
 open import Ledger.Crypto
@@ -33,12 +34,13 @@ The \AgdaRecord{Acnt} record has two fields, \AgdaField{treasury} and \AgdaField
 the \AgdaBound{acnt} field in \AgdaRecord{NewEpochState} keeps track of the total assets that
 remain in treasury and reserves.
 
-\begin{figure*}[h!]
+\begin{figure*}[ht]
 \begin{AgdaMultiCode}
 \begin{code}
 record Acnt : Type where
 \end{code}
 \begin{code}[hide]
+  constructor ⟦_,_⟧ᵃ
   field
 \end{code}
 \begin{code}
@@ -47,6 +49,10 @@ record Acnt : Type where
 ProtVer : Type
 ProtVer = ℕ × ℕ
 
+instance
+  Show-ProtVer : Show ProtVer
+  Show-ProtVer = Show-×
+
 data pvCanFollow : ProtVer → ProtVer → Type where
   canFollowMajor : pvCanFollow (m , n) (m + 1 , 0)
   canFollowMinor : pvCanFollow (m , n) (m , n + 1)
@@ -57,11 +63,15 @@ data pvCanFollow : ProtVer → ProtVer → Type where
 \end{figure*}
 \end{NoConway}
 
-\begin{figure*}[h!]
+\begin{figure*}[ht]
 \begin{AgdaMultiCode}
 \begin{code}
 data PParamGroup : Type where
-  NetworkGroup EconomicGroup TechnicalGroup GovernanceGroup SecurityGroup : PParamGroup
+  NetworkGroup     : PParamGroup
+  EconomicGroup    : PParamGroup
+  TechnicalGroup   : PParamGroup
+  GovernanceGroup  : PParamGroup
+  SecurityGroup    : PParamGroup
 
 record DrepThresholds : Type where
 \end{code}
@@ -86,53 +96,74 @@ record PParams : Type where
 \end{code}
 \emph{Network group}
 \begin{code}
-        maxBlockSize maxTxSize        : ℕ
-        maxHeaderSize maxValSize      : ℕ
+        maxBlockSize                  : ℕ
+        maxTxSize                     : ℕ
+        maxHeaderSize                 : ℕ
+        maxTxExUnits                  : ExUnits
+        maxBlockExUnits               : ExUnits
+        maxValSize                    : ℕ
         maxCollateralInputs           : ℕ
-        maxTxExUnits maxBlockExUnits  : ExUnits
 \end{code}
 \begin{code}[hide]
         pv                            : ProtVer -- retired, keep for now
 \end{code}
 \emph{Economic group}
 \begin{code}
-        a b                           : ℕ
+        a                             : ℕ
+        b                             : ℕ
         keyDeposit                    : Coin
         poolDeposit                   : Coin
         coinsPerUTxOByte              : Coin
-        minFeeRefScriptCoinsPerByte   : ℚ
         prices                        : Prices
+        minFeeRefScriptCoinsPerByte   : ℚ
 \end{code}
 \begin{code}[hide]
         minUTxOValue                  : Coin -- retired, keep for now
 \end{code}
 \emph{Technical group}
 \begin{code}
-        a0                            : ℚ
         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}
-        drepThresholds                : DrepThresholds
         poolThresholds                : PoolThresholds
+        drepThresholds                : DrepThresholds
+        ccMinSize                     : ℕ
+        ccMaxTermLength               : ℕ
         govActionLifetime             : ℕ
-        govActionDeposit drepDeposit  : Coin
+        govActionDeposit              : Coin
+        drepDeposit                   : Coin
         drepActivity                  : Epoch
-        ccMinSize ccMaxTermLength     : ℕ
-
+\end{code}
+\end{AgdaMultiCode}
+\caption{Protocol parameter definitions}
+\label{fig:protocol-parameter-declarations}
+\end{figure*}
+\begin{figure*}
+\begin{code}
 paramsWellFormed : PParams → Type
 paramsWellFormed pp =
      0 ∉ fromList  ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize
                    ∷ minUTxOValue ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
                    ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
   where open PParams pp
 \end{code}
+\caption{Protocol parameter well-formedness}
+\label{fig:protocol-parameter-well-formedness}
+\end{figure*}
 \begin{code}[hide]
 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
@@ -141,6 +172,12 @@ instance
     ((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
@@ -296,10 +333,6 @@ module PParamsUpdate where
       ((quote PParamsUpdate , DecEq-PParamsUpdate) ∷ [])
 
 \end{code}
-\end{AgdaMultiCode}
-\caption{Protocol parameter declarations}
-\label{fig:protocol-parameter-declarations}
-\end{figure*}
 % 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,
@@ -365,7 +398,7 @@ 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*}[h!]
+\begin{figure*}[ht]
 \begin{AgdaMultiCode}
 \begin{code}[hide]
 record PParamsDiff : Type₁ where

docs/agda-spec/src/Ledger/Script.lagda

@@ -32,17 +32,19 @@ record P1ScriptStructure : Type₁ where
 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
-         -- GetPair              : ExUnits → Type × Type
-         -- coinIsMonoidMorphism : GetPair Is ExUnit-CommutativeMonoid
-         --                          -CommutativeMonoid⟶ +-0-commutativeMonoid
+         ⦃ Show-ExUnits  ⦄ : Show ExUnits
+         ⦃ Show-Prices   ⦄ : Show Prices
 
   open HashableSet Dataʰ renaming (T to Data; THash to DataHash) public
 

docs/agda-spec/src/Ledger/Set/Theory.agda

@@ -54,8 +54,13 @@ opaque
     DecEq-ℙ : ⦃ _ : DecEq A ⦄ → DecEq (ℙ A)
     DecEq-ℙ = L.Decˡ.DecEq-Set
 
-open import Axiom.Set.Rel th public
-  hiding (_∣'_; _∣^'_; dom; range)
+    Show-ℙ : ⦃ _ : Show A ⦄ → Show (ℙ A)
+    Show-ℙ .show = λ x → Show-finite .show (x , (finiteness x))
+
+import Axiom.Set.Rel
+module Rel = Axiom.Set.Rel th
+
+open Rel public hiding (_∣'_; _∣^'_; dom; range)
 
 open import Axiom.Set.Map th public
   renaming ( Map to infixr 1 _⇀_
@@ -76,7 +81,7 @@ module _ ⦃ _ : DecEq A ⦄ where
     renaming (_∣_ to _∣ʳ_; _∣_ᶜ to _∣ʳ_ᶜ)
 
   open Corestriction {A} ∈-sp public
-    hiding (_∣^_; _∣^_ᶜ) public
+    renaming (_∣^_ to _∣^ʳ_; _∣^_ᶜ to _∣^ʳ_ᶜ) public
 
   open Restrictionᵐ {A} ∈-sp public
   open Corestrictionᵐ {A} ∈-sp public
@@ -132,3 +137,7 @@ opaque
 
   singleton-≢-∅ : ∀ {a} {x : a} → ⦃ DecEq a ⦄ → singleton x ≢ ∅
   singleton-≢-∅ {x = x} ()
+
+aggregateBy : ⦃ DecEq A ⦄ → ⦃ DecEq B ⦄ → ⦃ DecEq C ⦄ → ⦃ IsCommutativeMonoid' 0ℓ 0ℓ C ⦄
+            → Rel A B → A ⇀ C → B ⇀ C
+aggregateBy R m = mapFromFun (λ b → ∑[ x ← m ∣ Rel.dom (R ∣^ʳ ❴ b ❵) ] x) (Rel.range R)