Stake distribution as parameter

formal-spec/Everything.agda

@@ -5,6 +5,7 @@ open import Class.Computational22
 open import Leios.Abstract
 open import Leios.Base
 open import Leios.Blocks
+open import Leios.Config
 open import Leios.Defaults
 open import Leios.FFD
 open import Leios.Foreign.BaseTypes
@@ -16,15 +17,15 @@ open import Leios.Network
 open import Leios.Prelude
 open import Leios.Protocol
 open import Leios.Short
+open import Leios.Short.Decidable
 open import Leios.Short.Deterministic
+open import Leios.Short.Trace.Verifier
+open import Leios.Short.Trace.Verifier.Test
 open import Leios.Simplified
 open import Leios.Simplified.Deterministic
-open import Leios.Simplified.Deterministic.Test
+-- open import Leios.Simplified.Deterministic.Test
 open import Leios.SpecStructure
 open import Leios.Traces
-open import Leios.Trace.Decidable
-open import Leios.Trace.Verifier
-open import Leios.Trace.Verifier.Test
 open import Leios.Voting
 open import Leios.VRF
 open import StateMachine

formal-spec/Leios/Blocks.agda

@@ -137,7 +137,7 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
   data Header : Type where
     ibHeader : IBHeader → Header
     ebHeader : EndorserBlock → Header
-    vHeader  : List Vote → Header
+    vtHeader : List Vote → Header
 
   data Body : Type where
     ibBody : IBBody → Body
@@ -164,7 +164,7 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
   msgID : Header → ID
   msgID (ibHeader h) = (slotNumber h , producerID h)
   msgID (ebHeader h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper
-  msgID (vHeader  h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper
+  msgID (vtHeader  h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper
 
 ffdAbstract : ⦃ _ : IsBlock (List Vote) ⦄ → FFDAbstract
 ffdAbstract = record { GenFFD }

formal-spec/Leios/Config.agda

@@ -0,0 +1,10 @@
+open import Leios.Prelude
+
+module Leios.Config where
+
+record Params : Type where
+  field numberOfParties : ℕ
+        sutId : Fin numberOfParties
+        stakeDistribution : TotalMap (Fin numberOfParties) ℕ
+        stageLength : ℕ
+        ⦃ NonZero-stageLength ⦄ : NonZero stageLength

formal-spec/Leios/Defaults.agda

@@ -1,10 +1,9 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-
 open import Leios.Prelude
 open import Leios.Abstract
+open import Leios.Config
 open import Leios.SpecStructure
-open import Axiom.Set.Properties th
 
+open import Axiom.Set.Properties th
 open import Data.Nat.Show as N
 open import Data.Integer hiding (_≟_)
 open import Data.String as S using (intersperse)
@@ -22,26 +21,26 @@ open Equivalence
 -- As parameters the module expects
 -- * numberOfParties: the total number of participants
 -- * SUT-id: the number of the SUT (system under test)
-module Leios.Defaults (numberOfParties : ℕ) (SUT-id : Fin numberOfParties) where
+module Leios.Defaults (params : Params) (let open Params params) where
 
 instance
-  htx : Hashable (List ℕ) String
-  htx = record { hash = S.intersperse "#" ∘ L.map N.show }
+  htx : Hashable (List ℕ) (List ℕ)
+  htx = record { hash = id }
 
 d-Abstract : LeiosAbstract
 d-Abstract =
   record
     { Tx = ℕ
     ; PoolID = Fin numberOfParties
-    ; BodyHash = ⊤
+    ; BodyHash = List ℕ
     ; VrfPf = ⊤
     ; PrivKey = ⊤
     ; Sig = ⊤
-    ; Hash = String
+    ; Hash = List ℕ
     ; Vote = ⊤
     ; vote = λ _ _ → tt
     ; sign = λ _ _ → tt
-    ; L = 5
+    ; L = stageLength
     }
 
 open LeiosAbstract d-Abstract public
@@ -52,12 +51,15 @@ d-VRF : LeiosVRF
 d-VRF =
   record
     { PubKey     = ⊤
-    ; vrf        = record { isKeyPair = λ _ _ → ⊤ ; eval = λ x x₁ → x₁ , x ; verify = λ _ _ _ _ → ⊤ }
+    ; vrf        = record { isKeyPair = λ _ _ → ⊤ ; eval = λ x x₁ → x₁ , x ; verify = λ _ _ _ _ → ⊤  ; verify? = λ _ _ _ _ → yes tt }
     ; genIBInput = id
     ; genEBInput = id
     ; genVInput  = id
     ; genV1Input = id
     ; genV2Input = id
+    ; poolID     = λ _ → sutId
+    ; verifySig  = λ _ _ → ⊤
+    ; verifySig? = λ _ _ → yes tt
     }
 
 open LeiosVRF d-VRF public
@@ -102,15 +104,15 @@ instance
   isb =
     record
       { slotNumber = λ _ → 0
-      ; producerID = λ _ → SUT-id
+      ; producerID = λ _ → sutId
       ; lotteryPf = λ _ → tt
       }
 
-  hhs : Hashable PreIBHeader String
-  hhs = record { hash = IBHeaderOSig.bodyHash }
+  hhs : Hashable PreIBHeader (List ℕ)
+  hhs .hash = IBHeaderOSig.bodyHash
 
-  hpe : Hashable PreEndorserBlock String
-  hpe = record { hash = S.intersperse "#" ∘ EndorserBlockOSig.ibRefs }
+  hpe : Hashable PreEndorserBlock (List ℕ)
+  hpe .hash = L.concat ∘ EndorserBlockOSig.ibRefs
 
 record FFDState : Type where
   field inIBs : List InputBlock
@@ -129,7 +131,7 @@ open FFDState
 
 flushIns : FFDState → List (GenFFD.Header ⊎ GenFFD.Body)
 flushIns record { inIBs = ibs ; inEBs = ebs ; inVTs = vts } =
-  flushIBs ibs ++ L.map (inj₁ ∘ ebHeader) ebs ++ L.map (inj₁ ∘ vHeader) vts
+  flushIBs ibs ++ L.map (inj₁ ∘ ebHeader) ebs ++ L.map (inj₁ ∘ vtHeader) vts
   where
     flushIBs : List InputBlock → List (GenFFD.Header ⊎ GenFFD.Body)
     flushIBs [] = []
@@ -138,22 +140,22 @@ flushIns record { inIBs = ibs ; inEBs = ebs ; inVTs = vts } =
 data SimpleFFD : FFDState → FFDAbstract.Input ffdAbstract → FFDAbstract.Output ffdAbstract → FFDState → Type where
   SendIB : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (ibHeader h) (just (ibBody b))) FFDAbstract.SendRes (record s { outIBs = record {header = h; body = b} ∷ outIBs s})
   SendEB : ∀ {s eb} → SimpleFFD s (FFDAbstract.Send (ebHeader eb) nothing) FFDAbstract.SendRes (record s { outEBs = eb ∷ outEBs s})
-  SendVS : ∀ {s vs} → SimpleFFD s (FFDAbstract.Send (vHeader vs) nothing) FFDAbstract.SendRes (record s { outVTs = vs ∷ outVTs s})
+  SendVS : ∀ {s vs} → SimpleFFD s (FFDAbstract.Send (vtHeader vs) nothing) FFDAbstract.SendRes (record s { outVTs = vs ∷ outVTs s})
 
   BadSendIB : ∀ {s h} → SimpleFFD s (FFDAbstract.Send (ibHeader h) nothing) FFDAbstract.SendRes s
   BadSendEB : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (ebHeader h) (just b)) FFDAbstract.SendRes s
-  BadSendVS : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (vHeader h) (just b)) FFDAbstract.SendRes s
+  BadSendVS : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (vtHeader h) (just b)) FFDAbstract.SendRes s
 
   Fetch : ∀ {s} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes (flushIns s)) (record s { inIBs = [] ; inEBs = [] ; inVTs = [] })
 
 send-total : ∀ {s h b} → ∃[ s' ] (SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s')
 send-total {s} {ibHeader h} {just (ibBody b)} = record s { outIBs = record {header = h; body = b} ∷ outIBs s} , SendIB
 send-total {s} {ebHeader eb} {nothing} = record s { outEBs = eb ∷ outEBs s} , SendEB
-send-total {s} {vHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS
+send-total {s} {vtHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS
 
 send-total {s} {ibHeader h} {nothing} = s , BadSendIB
 send-total {s} {ebHeader eb} {just _} = s , BadSendEB
-send-total {s} {vHeader vs} {just _} = s , BadSendVS
+send-total {s} {vtHeader vs} {just _} = s , BadSendVS
 
 fetch-total : ∀ {s} → ∃[ x ] (∃[ s' ] (SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes x) s'))
 fetch-total {s} = flushIns s , (record s { inIBs = [] ; inEBs = [] ; inVTs = [] } , Fetch)
@@ -214,12 +216,12 @@ d-VotingAbstract-2 =
     ; isVoteCertified = λ _ _ → ⊤
     }
 
-st : SpecStructure 1
-st = record
+d-SpecStructure : SpecStructure 1
+d-SpecStructure = record
       { a = d-Abstract
       ; Hashable-PreIBHeader = hhs
       ; Hashable-PreEndorserBlock = hpe
-      ; id = SUT-id
+      ; id = sutId
       ; FFD' = d-FFDFunctionality
       ; vrf' = d-VRF
       ; sk-IB = tt
@@ -236,12 +238,12 @@ st = record
       ; va = d-VotingAbstract
       }
 
-st-2 : SpecStructure 2
-st-2 = record
+d-SpecStructure-2 : SpecStructure 2
+d-SpecStructure-2 = record
       { a = d-Abstract
       ; Hashable-PreIBHeader = hhs
       ; Hashable-PreEndorserBlock = hpe
-      ; id = SUT-id
+      ; id = sutId
       ; FFD' = d-FFDFunctionality
       ; vrf' = d-VRF
       ; sk-IB = tt
@@ -258,62 +260,4 @@ st-2 = record
       ; va = d-VotingAbstract-2
       }
 
-open import Leios.Short st public
-
-completeFin : ∀ (n : ℕ) → ℙ (Fin n)
-completeFin zero = ∅
-completeFin (ℕ.suc n) = singleton (F.fromℕ n) ∪ mapˢ F.inject₁ (completeFin n)
-
-m≤n∧n≤m⇒m≡n : ∀ {n m : ℕ} → n N.≤ m → m N.≤ n → m ≡ n
-m≤n∧n≤m⇒m≡n z≤n z≤n = refl
-m≤n∧n≤m⇒m≡n (s≤s n≤m) (s≤s m≤n) = cong N.suc (m≤n∧n≤m⇒m≡n n≤m m≤n)
-
-toℕ-fromℕ : ∀ {n} {a : Fin (N.suc n)} → toℕ a ≡ n → a ≡ F.fromℕ n
-toℕ-fromℕ {zero} {fzero} x = refl
-toℕ-fromℕ {N.suc n} {fsuc a} x = cong fsuc (toℕ-fromℕ {n} {a} (N.suc-injective x))
-
-maximalFin : ∀ (n : ℕ) → isMaximal (completeFin n)
-maximalFin (ℕ.suc n) {a} with toℕ a N.<? n
-... | yes p =
-  let n≢toℕ = ≢-sym (N.<⇒≢ p)
-      fn = F.lower₁ a n≢toℕ
-      fn≡a = F.inject₁-lower₁ a n≢toℕ
-  in (to ∈-∪) (inj₂ ((to ∈-map) (fn , (sym fn≡a , maximalFin n))))
-... | no ¬p with a F.≟ F.fromℕ n
-... | yes q = (to ∈-∪) (inj₁ ((to ∈-singleton) q))
-... | no ¬q =
-  let n≢toℕ = N.≰⇒> ¬p
-      a<sucn = F.toℕ<n a
-  in ⊥-elim $ (¬q ∘ toℕ-fromℕ) (N.suc-injective (m≤n∧n≤m⇒m≡n n≢toℕ a<sucn))
-
-open FunTot (completeFin numberOfParties) (maximalFin numberOfParties)
-
-sd : TotalMap (Fin numberOfParties) ℕ
-sd = Fun⇒TotalMap (const 100000000)
-
-open import Class.Computational
-open import Class.Computational22
-
-open Computational22
-open BaseAbstract
-open FFDAbstract
-
-open GenFFD.Header using (ibHeader; ebHeader; vHeader)
-open GenFFD.Body using (ibBody)
-open FFDState
-
-instance
-  Computational-B : Computational22 (BaseAbstract.Functionality._-⟦_/_⟧⇀_ d-BaseFunctionality) String
-  Computational-B .computeProof s (INIT x) = success ((STAKE sd , tt) , tt)
-  Computational-B .computeProof s (SUBMIT x) = success ((EMPTY , tt) , tt)
-  Computational-B .computeProof s FTCH-LDG = success (((BASE-LDG []) , tt) , tt)
-  Computational-B .completeness _ _ _ _ _ = {!!} -- TODO: Completeness proof
-
-  Computational-FFD : Computational22 (FFDAbstract.Functionality._-⟦_/_⟧⇀_ d-FFDFunctionality) String
-  Computational-FFD .computeProof s (Send (ibHeader h) (just (ibBody b))) = success ((SendRes , record s {outIBs = record {header = h; body = b} ∷ outIBs s}) , SendIB)
-  Computational-FFD .computeProof s (Send (ebHeader h) nothing) = success ((SendRes , record s {outEBs = h ∷ outEBs s}) , SendEB)
-  Computational-FFD .computeProof s (Send (vHeader h) nothing) = success ((SendRes , record s {outVTs = h ∷ outVTs s}) , SendVS)
-  Computational-FFD .computeProof s Fetch = success ((FetchRes (flushIns s) , record s {inIBs = []; inEBs = []; inVTs = []}) , Fetch)
-
-  Computational-FFD .computeProof _ _ = failure "FFD error"
-  Computational-FFD .completeness _ _ _ _ _ = {!!} -- TODO:Completeness proof
+open import Leios.Short d-SpecStructure public

formal-spec/Leios/Foreign/BaseTypes.agda

@@ -82,21 +82,6 @@ instance
     .to   → F.MkHSMap ∘ to
     .from → from ∘ F.HSMap.assocList
 
-record Listable (A : Type) : Type where
-  field
-    listing  : ℙ A
-    complete : ∀ {a : A} → a ∈ listing
-
-totalDec : ∀ {A B : Type} → ⦃ DecEq A ⦄ → ⦃ Listable A ⦄ → {R : Rel A B} → Dec (total R)
-totalDec {A} {B} {R} with all? (_∈? dom R)
-... | yes p = yes λ {a} → p {a} ((Listable.complete it) {a})
-... | no ¬p = no λ x → ¬p λ {a} _ → x {a}
-
-instance
-
-  total? : ∀ {A B : Type} → ⦃ DecEq A ⦄ → ⦃ Listable A ⦄ → {R : Rel A B} → ({a : A} → a ∈ dom R) ⁇
-  total? = ⁇ totalDec
-
   Convertible-TotalMap : ∀ {K K' V V'} → ⦃ DecEq K ⦄ → ⦃ Listable K ⦄
     → ⦃ Convertible K K' ⦄ → ⦃ Convertible V V' ⦄
     → Convertible (TotalMap K V) (List $ Pair K' V')

formal-spec/Leios/Foreign/Types.agda

@@ -19,6 +19,9 @@ module Leios.Foreign.Types where
   {-# LANGUAGE DuplicateRecordFields #-}
 #-}
 
+-- TODO: Get rid of hardcoded parameters in this module
+
+{-
 numberOfParties : ℕ
 numberOfParties = 2
 
@@ -38,7 +41,7 @@ instance
 record IBHeader : Type where
   field slotNumber : ℕ
         producerID : ℕ
-        bodyHash : String
+        bodyHash : List ℕ
 
 {-# FOREIGN GHC
 data IBHeader = IBHeader {slotNumber :: Integer, producerID :: Integer, bodyHash :: Data.Text.Text }
@@ -72,7 +75,7 @@ instance
 record EndorserBlock : Type where
   field slotNumber : ℕ
         producerID : ℕ
-        ibRefs     : List String
+        ibRefs     : List (List IBRef)
 
 {-# FOREIGN GHC
 data EndorserBlock = EndorserBlock { slotNumber :: Integer, producerID :: Integer, ibRefs :: [Data.Text.Text] }
@@ -95,30 +98,6 @@ instance
           (no _) → error "Conversion to Fin not possible!"
       }
 
-  Listable-Fin : ∀ {n} → Listable (Fin n)
-  Listable-Fin {zero} = record { listing = ∅ ; complete = λ {a} → ⊥-elim $ (Inverse.to F.0↔⊥) a }
-  Listable-Fin {suc n} =
-    let record { listing = l ; complete = c } = Listable-Fin {n}
-    in record
-         { listing = singleton (F.fromℕ n) ∪ mapˢ F.inject₁ l
-         ; complete = complete
-         }
-       where
-         complete : ∀ {a} → a ∈ singleton (F.fromℕ n) ∪ mapˢ F.inject₁ (let record { listing = l } = Listable-Fin {n} in l)
-         complete {a} with F.toℕ a N.<? n
-         ... | yes p =
-           let record { listing = l ; complete = c } = Listable-Fin {n}
-               n≢toℕ = ≢-sym (N.<⇒≢ p)
-               fn = F.lower₁ a n≢toℕ
-               fn≡a = F.inject₁-lower₁ a n≢toℕ
-           in (Equivalence.to ∈-∪) (inj₂ ((Equivalence.to ∈-map) (fn , (sym fn≡a , c))))
-         ... | no ¬p with a F.≟ F.fromℕ n
-         ... | yes q = (Equivalence.to ∈-∪) (inj₁ ((Equivalence.to ∈-singleton) q))
-         ... | no ¬q =
-           let n≢toℕ = N.≰⇒> ¬p
-               a<sucn = F.toℕ<n a
-           in ⊥-elim $ (¬q ∘ toℕ-fromℕ) (N.suc-injective (m≤n∧n≤m⇒m≡n n≢toℕ a<sucn))
-
   HsTy-FFDState = autoHsType FFDState
   Conv-FFDState = autoConvert FFDState
 
@@ -151,13 +130,35 @@ open Computational22
 open BaseAbstract
 open FFDAbstract
 
-open GenFFD.Header using (ibHeader; ebHeader; vHeader)
+open GenFFD.Header using (ibHeader; ebHeader; vtHeader)
 open GenFFD.Body using (ibBody)
 open FFDState
 
-open import Leios.Short.Deterministic st public
+open import Leios.Short.Deterministic d-SpecStructure public
+
+open FunTot (completeFin numberOfParties) (maximalFin numberOfParties)
+
+d-StakeDistribution : TotalMap (Fin numberOfParties) ℕ
+d-StakeDistribution = Fun⇒TotalMap (const 100000000)
+
+instance
+  Computational-B : Computational22 (BaseAbstract.Functionality._-⟦_/_⟧⇀_ d-BaseFunctionality) String
+  Computational-B .computeProof s (INIT x) = success ((STAKE d-StakeDistribution , tt) , tt)
+  Computational-B .computeProof s (SUBMIT x) = success ((EMPTY , tt) , tt)
+  Computational-B .computeProof s FTCH-LDG = success (((BASE-LDG []) , tt) , tt)
+  Computational-B .completeness _ _ _ _ _ = {!!} -- TODO: Completeness proof
+
+  Computational-FFD : Computational22 (FFDAbstract.Functionality._-⟦_/_⟧⇀_ d-FFDFunctionality) String
+  Computational-FFD .computeProof s (Send (ibHeader h) (just (ibBody b))) = success ((SendRes , record s {outIBs = record {header = h; body = b} ∷ outIBs s}) , SendIB)
+  Computational-FFD .computeProof s (Send (ebHeader h) nothing) = success ((SendRes , record s {outEBs = h ∷ outEBs s}) , SendEB)
+  Computational-FFD .computeProof s (Send (vtHeader h) nothing) = success ((SendRes , record s {outVTs = h ∷ outVTs s}) , SendVS)
+  Computational-FFD .computeProof s Fetch = success ((FetchRes (flushIns s) , record s {inIBs = []; inEBs = []; inVTs = []}) , Fetch)
+
+  Computational-FFD .computeProof _ _ = failure "FFD error"
+  Computational-FFD .completeness _ _ _ _ _ = {!!} -- TODO:Completeness proof
 
 stepHs : HsType (LeiosState → LeiosInput → C.ComputationResult String (LeiosOutput × LeiosState))
 stepHs = to (compute Computational--⟦/⟧⇀)
 
 {-# COMPILE GHC stepHs as step #-}
+-}