From 7a8846b1234427f59d8b98153fa53ea7234aacc5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 5 Dec 2024 19:25:39 +0000 Subject: [PATCH] Complete support for dummy constants and cryptography --- .../Spec/Foreign/HSConsensus/BaseTypes.agda | 56 ++++++++++- .../src/Spec/Foreign/HSConsensus/Core.agda | 99 +++++++++++++++++-- docs/agda-spec/src/Spec/Foreign/HSTypes.agda | 34 +++++++ 3 files changed, 179 insertions(+), 10 deletions(-) diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda index f47c6b36f4..f712b916d2 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda +++ b/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 diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda index 2032d57c9b..5a88468d9a 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda +++ b/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 diff --git a/docs/agda-spec/src/Spec/Foreign/HSTypes.agda b/docs/agda-spec/src/Spec/Foreign/HSTypes.agda index b4990a88b3..7c6d168ab7 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSTypes.agda +++ b/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