Make all STSs in the Agda spec executable (#1270)

As the first task in implementing conformance testing with respect to
the formal specification, we shall focus on making all the State
Transition Systems (STSs) within the formal spec executable.

Author: javierdiaz72

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

@@ -64,7 +64,7 @@ module _ {a} {A : Set a} where
       <-asymmetric : Asymmetric _<_
       <-asymmetric = ≤-antisym⇒<-asym ≤-antisym
 
-      open IsEquivalence ≈-isEquivalence renaming (sym to ≈-sym)
+      open IsEquivalence ≈-isEquivalence using () renaming (sym to ≈-sym) public
 
       <-trans : Transitive _<_
       <-trans i<j j<k =
@@ -78,20 +78,51 @@ module _ {a} {A : Set a} where
       <⇒¬>⊎≈ x<y (inj₁ y<x) = <-asymmetric x<y y<x
       <⇒¬>⊎≈ x<y (inj₂ x≈y) = <-irrefl (≈-sym x≈y) x<y
 
+      ≥⇒≮ : ∀ {x y} → y ≤ x → ¬ (x < y)
+      ≥⇒≮ y≤x x<y = contradiction (to ≤⇔<∨≈ y≤x) (<⇒¬>⊎≈ x<y)
+
+    open HasPartialOrder ⦃...⦄
+
     record HasDecPartialOrder : Set (sucˡ a) where
       field
         ⦃ hasPartialOrder ⦄ : HasPartialOrder
         ⦃ dec-≤ ⦄ : _≤_ ⁇²
         ⦃ dec-< ⦄ : _<_ ⁇²
 
+    record HasTotalOrder : Set (sucˡ a) where
+      field
+        ⦃ hasPartialOrder ⦄ : HasPartialOrder
+        ≤-total : Total _≤_
+
+      ≤-isTotalOrder : IsTotalOrder _≈_ _≤_
+      ≤-isTotalOrder = record { isPartialOrder = ≤-isPartialOrder ; total = ≤-total }
+
+      ≮⇒≥ : Decidable _≈_ → ∀ {x y} → ¬ (x < y) → y ≤ x
+      ≮⇒≥ _≈?_ {x} {y} x≮y with x ≈? y | ≤-total y x
+      ... | yes x≈y  | _        = IsPreorder.reflexive ≤-isPreorder (≈-sym x≈y)
+      ... | _        | inj₁ y≤x = y≤x
+      ... | no  x≉y  | inj₂ x≤y = contradiction (≤∧≉⇒< (x≤y , x≉y)) x≮y
+
+    open HasTotalOrder ⦃...⦄
+
+    record HasDecTotalOrder : Set (sucˡ a) where
+      field
+        ⦃ hasTotalOrder ⦄ : HasTotalOrder
+        ⦃ dec-≤ ⦄ : _≤_ ⁇²
+        ⦃ dec-< ⦄ : _<_ ⁇²
+
   HasPreorder≡ = HasPreorder {_≈_ = _≡_}
   HasDecPreorder≡ = HasDecPreorder {_≈_ = _≡_}
   HasPartialOrder≡ = HasPartialOrder {_≈_ = _≡_}
   HasDecPartialOrder≡ = HasDecPartialOrder {_≈_ = _≡_}
+  HasTotalOrder≡ = HasTotalOrder {_≈_ = _≡_}
+  HasDecTotalOrder≡ = HasDecTotalOrder {_≈_ = _≡_}
 
 open HasPreorder ⦃...⦄ public
 open HasPartialOrder ⦃...⦄ public hiding (hasPreorder)
 open HasDecPartialOrder ⦃...⦄ public hiding (hasPartialOrder)
+open HasTotalOrder ⦃...⦄ public hiding (hasPartialOrder)
+open HasDecTotalOrder ⦃...⦄ public hiding (hasTotalOrder)
 
 module _ {a} {A : Set a} {_≈_ : Rel A a} where
 

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

@@ -16,6 +16,9 @@ instance
   ℕ-hasPartialOrder = HasPartialOrder ∋ record
     { ≤-antisym = Nat.≤-antisym }
   ℕ-hasDecPartialOrder = HasDecPartialOrder {A = ℕ} ∋ record {}
+  ℕ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Nat.≤-total }
+  ℕ-hasDecTotalOrder = HasDecTotalOrder {A = ℕ} ∋ record {}
 
   import Data.Integer.Properties as Int hiding (_≟_)
   ℤ-hasPreorder = HasPreorder ∋ record {Int; ≤⇔<∨≈ = let open Int in mk⇔
@@ -29,3 +32,6 @@ instance
   ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
   ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
   ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}
+  ℚ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Rat.≤-total }
+  ℚ-hasDecTotalOrder = HasDecTotalOrder {A = ℚ} ∋ record {}

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/InterfaceLibrary/Ledger.lagda

@@ -27,10 +27,13 @@ record LedgerInterface : Type₁ where
     NewEpochState      : Type
     getPParams         : NewEpochState → PParams
     getEpoch           : NewEpochState → Epoch
-    getPoolDistr       : NewEpochState → PoolDistr 
+    getPoolDistr       : NewEpochState → PoolDistr
     adoptGenesisDelegs : NewEpochState → Slot → NewEpochState
     _⊢_⇀⦇_,NEWEPOCH⦈_  : ⊤ → NewEpochState → Epoch → NewEpochState → Type
 \end{code}
+\begin{code}[hide]
+    ⦃ Computational-NEWEPOCH ⦄ : Computational _⊢_⇀⦇_,NEWEPOCH⦈_ String
+\end{code}
 \caption{Ledger interface}
 \label{fig:interface:ledger}
 \end{figure*}

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

@@ -5,6 +5,12 @@ module Ledger.Crypto where
 
 open import Ledger.Prelude hiding (T)
 
+module _ (M : Type↑) where
+  _⁴ : ∀ {ℓ} {A B C D : Type ℓ} → (A → B → C → D → Type ℓ) → Type _
+  _⁴ _~_~_~_ = ∀ {x y z w} → M (x ~ y ~ z ~ w)
+
+_⁇⁴ = _⁇ ⁴
+
 \end{code}
 
 \subsection{Serialization}
@@ -20,7 +26,7 @@ record Serializer : Type₁ where
 \begin{code}
         Ser             : Type
         encode          : {T : Type} → T → Ser
-        decode          : {T : Type} → Ser → T
+        decode          : {T : Type} → Ser → Maybe T
         _∥_             : Ser → Ser → Ser
 \end{code}
 \emph{Properties}
@@ -29,7 +35,7 @@ record Serializer : Type₁ where
         enc-dec-correct :
 \end{code}
 \begin{code}
-          ∀ {T : Type} (x : T) → decode (encode x) ≡ x
+          ∀ {T : Type} (x : T) → decode (encode x) ≡ just x
 \end{code}
 \caption{Definitions for serialization}
 \label{fig:defs:serialization}
@@ -44,6 +50,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
@@ -135,7 +142,7 @@ record KESScheme (srl : Serializer) : Type₁ where
 \end{code}
 \emph{Properties}
 \begin{code}[hide]
-  field -- ⦃ Dec-isSigned ⦄ : isSigned ⁇⁴ -- TODO: Define ⁇⁴ if needed
+  field ⦃ Dec-isSigned ⦄ : isSigned ⁇⁴
         isSigned-correct :
 \end{code}
 \begin{code}