Relocate ExternalStructures

IntersectMBO · Dec 12, 2024 · fdee730 · fdee730
1 parent a98ba32
commit fdee730
Show file tree

Hide file tree

Showing 4 changed files with 90 additions and 83 deletions.
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda
@@ -64,7 +64,7 @@ instance -- TODO: Complete
   Conv-ComputationResult : ConvertibleType ComputationResult F.ComputationResult
   Conv-ComputationResult = autoConvertible
 
-open ExternalStructures dummyExternalFunctions
+open import Spec.Foreign.HSConsensus.ExternalStructures dummyExternalFunctions
   renaming
     ( HSEpochStructure to DummyEpochStructure
     ; HSCrypto to DummyCrypto

diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda
@@ -11,14 +11,12 @@ open import Foreign.HaskellTypes          public
 open import Foreign.HaskellTypes.Deriving public
 
 open import Ledger.Crypto
-open import Ledger.Types.Epoch
 
 open import Spec.Foreign.Util public
 
 open import Data.Rational using (1ℚ; ½; Positive; positive; _<_) renaming (_≤_ to _≤ℚ_)
 open import Data.Rational.Ext using (PosUnitInterval)
 open import Data.Integer using (_≤_; _<_)
-open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
 
 ½-positive : Positive ½
 ½-positive = positive {½} (_<_.*<* (_<_.+<+ (s≤s z≤n)))
@@ -55,82 +53,3 @@ module Implementation where
   Seed = ℕ
 
 module ExternalStructures (externalFunctions : ExternalFunctions) where
-  HSGlobalConstants = GlobalConstants ∋ record {Implementation}
-  instance
-    HSEpochStructure = EpochStructure ∋ ℕEpochStructure HSGlobalConstants
-
-    -- NOTE: Dummy for now.
-    HSSerializer : Serializer
-    HSSerializer = record
-      { Ser             = String
-      ; encode          = const ""
-      ; decode          = const nothing
-      ; _∥_             = _+ˢ_
-      ; enc-dec-correct = error "enc-dec-correct evaluated"
-      }
-
-    -- NOTE: Dummy for now.
-    HSPKScheme : PKScheme
-    HSPKScheme = record
-      { SKey      = ℕ
-      ; VKey      = ℕ
-      ; isKeyPair = _≡_
-      }
-
-    -- Note: Dummy for now.
-    HSDSigScheme : DSigScheme HSSerializer
-    HSDSigScheme = record
-      { pks              = HSPKScheme
-      ; isSigned         = λ _ _ _ → ⊤
-      ; sign             = λ _ _ → 0
-      ; isSigned-correct = error "isSigned-correct evaluated"
-      ; Dec-isSigned     = λ {_} {_} {_} → ⁇ (true because ofʸ tt)
-      }
-
-    -- NOTE: Dummy for now.
-    HSKESScheme : KESScheme HSSerializer
-    HSKESScheme = record
-      { pks              = HSPKScheme
-      ; Sig              = ℕ
-      ; isSigned         = λ _ _ _ _ → ⊤
-      ; sign             = λ _ _ _ → 0
-      ; isSigned-correct = error "isSigned-correct evaluated"
-      ; Dec-isSigned     = λ {_} {_} {_} {_} → ⁇ (true because ofʸ tt)
-      }
-
-    -- NOTE: Dummy for now.
-    HSVRFScheme : VRFScheme
-    HSVRFScheme = record
-      { Implementation
-      ; pks            = HSPKScheme
-      ; Proof          = ℕ
-      ; verify         = λ _ _ _ → ⊤
-      ; evaluate       = error "evaluate evaluated"
-      ; _XOR_          = _+_
-      ; verify-correct = error "verify-correct evaluated"
-      ; Dec-verify     = λ {T = _} {_} {_} {_} → ⁇ (true because ofʸ tt)
-      }
-
-    HSCrypto : Crypto
-    HSCrypto = record
-      { srl        = HSSerializer
-      ; dsig       = HSDSigScheme
-      ; kes        = HSKESScheme
-      ; vrf        = HSVRFScheme
-      ; ScriptHash = ℕ
-      }
-
-    open import Spec.BaseTypes HSCrypto
-
-    -- NOTE: Dummy for now.
-    HSNonces : Nonces
-    HSNonces = record
-      { Implementation
-      ; Nonce       = ℕ
-      ; _⋆_         = _+_
-      ; nonceToSeed = id
-      }
-
-    open EpochStructure HSEpochStructure public
-    open Crypto HSCrypto public
-    open Nonces HSNonces public
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda
@@ -0,0 +1,88 @@
+open import Spec.Foreign.ExternalFunctions
+
+module Spec.Foreign.HSConsensus.ExternalStructures (externalFunctions : ExternalFunctions) where
+
+open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
+open import Ledger.Crypto
+open import Ledger.Types.Epoch
+open import Spec.Foreign.HSConsensus.Core
+
+HSGlobalConstants = GlobalConstants ∋ record {Implementation}
+instance
+  HSEpochStructure = EpochStructure ∋ ℕEpochStructure HSGlobalConstants
+
+  -- NOTE: Dummy for now.
+  HSSerializer : Serializer
+  HSSerializer = record
+    { Ser             = String
+    ; encode          = const ""
+    ; decode          = const nothing
+    ; _∥_             = _+ˢ_
+    ; enc-dec-correct = error "enc-dec-correct evaluated"
+    }
+
+  -- NOTE: Dummy for now.
+  HSPKScheme : PKScheme
+  HSPKScheme = record
+    { SKey      = ℕ
+    ; VKey      = ℕ
+    ; isKeyPair = _≡_
+    }
+
+  -- Note: Dummy for now.
+  HSDSigScheme : DSigScheme HSSerializer
+  HSDSigScheme = record
+    { pks              = HSPKScheme
+    ; isSigned         = λ _ _ _ → ⊤
+    ; sign             = λ _ _ → 0
+    ; isSigned-correct = error "isSigned-correct evaluated"
+    ; Dec-isSigned     = λ {_} {_} {_} → ⁇ (true because ofʸ tt)
+    }
+
+  -- NOTE: Dummy for now.
+  HSKESScheme : KESScheme HSSerializer
+  HSKESScheme = record
+    { pks              = HSPKScheme
+    ; Sig              = ℕ
+    ; isSigned         = λ _ _ _ _ → ⊤
+    ; sign             = λ _ _ _ → 0
+    ; isSigned-correct = error "isSigned-correct evaluated"
+    ; Dec-isSigned     = λ {_} {_} {_} {_} → ⁇ (true because ofʸ tt)
+    }
+
+  -- NOTE: Dummy for now.
+  HSVRFScheme : VRFScheme
+  HSVRFScheme = record
+    { Implementation
+    ; pks            = HSPKScheme
+    ; Proof          = ℕ
+    ; verify         = λ _ _ _ → ⊤
+    ; evaluate       = error "evaluate evaluated"
+    ; _XOR_          = _+_
+    ; verify-correct = error "verify-correct evaluated"
+    ; Dec-verify     = λ {T = _} {_} {_} {_} → ⁇ (true because ofʸ tt)
+    }
+
+  HSCrypto : Crypto
+  HSCrypto = record
+    { srl        = HSSerializer
+    ; dsig       = HSDSigScheme
+    ; kes        = HSKESScheme
+    ; vrf        = HSVRFScheme
+    ; ScriptHash = ℕ
+    }
+
+  open import Spec.BaseTypes HSCrypto
+
+  -- NOTE: Dummy for now.
+  HSNonces : Nonces
+  HSNonces = record
+    { Implementation
+    ; Nonce       = ℕ
+    ; _⋆_         = _+_
+    ; nonceToSeed = id
+    }
+
+  open EpochStructure HSEpochStructure public
+  open Crypto HSCrypto public
+  open Nonces HSNonces public
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda
@@ -18,7 +18,7 @@ instance
   Conv-UpdateNonceState = autoConvert UpdateNonceState
 
 module _ (ext : ExternalFunctions) where
-  open ExternalStructures ext hiding (Slot)
+  open import Spec.Foreign.HSConsensus.ExternalStructures ext hiding (Slot)
   open import Spec.UpdateNonce.Properties HSCrypto HSNonces HSEpochStructure
 
   updn-step : HsType (UpdateNonceEnv → UpdateNonceState → Slot → ComputationResult String UpdateNonceState)