Complete support for dummy constants and cryptography

docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda

@@ -1,16 +1,59 @@
 module Spec.Foreign.HSConsensus.BaseTypes where
 
+open import Data.Rational
+
 open import Spec.Foreign.ExternalFunctions
 open import Spec.Foreign.HSConsensus.Core public
 import Spec.Foreign.HSTypes as F
 
-instance -- TODO: Complete
+instance
+  iConvTop    = Convertible-Refl {⊤}
   iConvNat    = Convertible-Refl {ℕ}
   iConvString = Convertible-Refl {String}
   iConvBool   = Convertible-Refl {Bool}
 
 instance -- TODO: Complete
 
+  -- * Unit and empty
+
+  HsTy-⊥ = MkHsType ⊥ F.Empty
+  Conv-⊥ = autoConvert ⊥
+
+  HsTy-⊤ = MkHsType ⊤ ⊤
+
+  -- * Rational numbers
+
+  HsTy-Rational = MkHsType ℚ F.Rational
+  Conv-Rational : HsConvertible ℚ
+  Conv-Rational = λ where
+    .to (mkℚ n d _)       → n F., suc d
+    .from (n F., zero)    → 0ℚ -- TODO is there a safer way to do this?
+    .from (n F., (suc d)) → n Data.Rational./ suc d
+
+  -- * Maps and Sets
+
+  HsTy-HSSet : ∀ {A} → ⦃ HasHsType A ⦄ → HasHsType (ℙ A)
+  HsTy-HSSet {A} = MkHsType _ (F.HSSet (HsType A))
+
+  Conv-HSSet : ∀ {A} ⦃ _ : HasHsType A ⦄
+             → ⦃ HsConvertible A ⦄
+             → HsConvertible (ℙ A)
+  Conv-HSSet = λ where
+    .to → F.MkHSSet ∘ to ∘ setToList
+    .from → fromListˢ ∘ from ∘ F.HSSet.elems
+
+  HsTy-Map : ∀ {A B} → ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⇀ B)
+  HsTy-Map {A} {B} = MkHsType _ (F.HSMap (HsType A) (HsType B))
+
+  Conv-HSMap : ∀ {A B} ⦃ _ : HasHsType A ⦄ ⦃ _ : HasHsType B ⦄
+    → ⦃ DecEq A ⦄
+    → ⦃ HsConvertible A ⦄
+    → ⦃ HsConvertible B ⦄
+    → HsConvertible (A ⇀ B)
+  Conv-HSMap = λ where
+    .to → F.MkHSMap ∘ to
+    .from → from ∘ F.HSMap.assocList
+
   -- * ComputationResult
 
   HsTy-ComputationResult : ∀ {l} {Err} {A : Type l}
@@ -21,5 +64,14 @@ instance -- TODO: Complete
   Conv-ComputationResult : ConvertibleType ComputationResult F.ComputationResult
   Conv-ComputationResult = autoConvertible
 
-open ExternalStructures dummyExternalFunctions -- TODO: Complete
+open ExternalStructures dummyExternalFunctions
+  renaming
+    ( HSEpochStructure to DummyEpochStructure
+    ; HSCrypto to DummyCrypto
+    ; HSNonces to DummyNonces
+    )
   public
+
+unquoteDecl = do
+  hsTypeAlias Slot
+  hsTypeAlias Epoch

docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda

@@ -1,5 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-} -- TODO: Remove when structs are fully implemented
-
 open import Spec.Foreign.ExternalFunctions
 
 module Spec.Foreign.HSConsensus.Core where
@@ -15,6 +13,19 @@ 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)))
+
+½≤1 : ½ ≤ℚ 1ℚ
+½≤1 = _≤ℚ_.*≤* (_≤_.+≤+ (s≤s z≤n))
+
 module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance
   ∀Hashable : Hashable A A
   ∀Hashable = λ where .hash → id
@@ -27,25 +38,97 @@ instance
   Hashable-⊤ = λ where .hash tt → 0
 
 module Implementation where
+  -- Global constants
+  Network                        = ℕ
+  SlotsPerEpochᶜ                 = 100
+  StabilityWindowᶜ               = 10
+  RandomnessStabilisationWindowᶜ = 20
+  Quorum                         = 1
+  NetworkId                      = 0
+  SlotsPerKESPeriodᶜ             = 5
+  MaxKESEvoᶜ                     = 30
+  ActiveSlotCoeffᶜ : PosUnitInterval
+  ActiveSlotCoeffᶜ               = ½ , ½-positive , ½≤1
+  MaxMajorPVᶜ                    = 1
 
-  -- TODO: Complete
+  -- VRFs and nonces
+  Seed = ℕ
 
 module ExternalStructures (externalFunctions : ExternalFunctions) where
   HSGlobalConstants = GlobalConstants ∋ record {Implementation}
   instance
     HSEpochStructure = EpochStructure ∋ ℕEpochStructure HSGlobalConstants
 
-    -- TODO: Complete
+    -- 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 {}
+    HSCrypto = record
+      { srl        = HSSerializer
+      ; dsig       = HSDSigScheme
+      ; kes        = HSKESScheme
+      ; vrf        = HSVRFScheme
+      ; ScriptHash = ℕ
+      }
 
     open import Spec.BaseTypes HSCrypto
 
-    -- TODO: Complete
+    -- NOTE: Dummy for now.
     HSNonces : Nonces
     HSNonces = record
-      { Nonce = ℕ
-      ; _⋆_ = _+_
+      { Implementation
+      ; Nonce       = ℕ
+      ; _⋆_         = _+_
+      ; nonceToSeed = id
       }
 
     open EpochStructure HSEpochStructure public

docs/agda-spec/src/Spec/Foreign/HSTypes.agda

@@ -19,6 +19,40 @@ open import Data.Rational.Base
   import GHC.Real (Ratio(..))
 #-}
 
+-- * The empty type
+
+data Empty : Type where
+{-# COMPILE GHC Empty = data Void () #-}
+
+-- * Rational
+
+data Rational : Type where
+  _,_ : ℤ → ℕ → Rational
+{-# COMPILE GHC Rational = data Rational ((:%)) #-}
+
+-- We'll generate code with qualified references to Rational in this
+-- module, so make sure to define it.
+{-# FOREIGN GHC type Rational = Ratio Integer #-}
+
+-- * Maps and Sets
+
+record HSMap K V : Type where
+  constructor MkHSMap
+  field assocList : List (Pair K V)
+
+record HSSet A : Type where
+  constructor MkHSSet
+  field elems : List A
+
+{-# FOREIGN GHC
+  newtype HSMap k v = MkHSMap [(k, v)]
+    deriving (Generic, Show, Eq, Ord)
+  newtype HSSet a = MkHSSet [a]
+    deriving (Generic, Show, Eq, Ord)
+#-}
+{-# COMPILE GHC HSMap = data HSMap (MkHSMap) #-}
+{-# COMPILE GHC HSSet = data HSSet (MkHSSet) #-}
+
 -- * ComputationResult
 
 data ComputationResult E A : Type where