Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Formal specification: abstract base functionality #61

Merged
merged 3 commits into from
Nov 1, 2024
Merged

Formal specification: abstract base functionality #61

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f5632e8
Abstract base functionality
yveshauser Oct 31, 2024
25684eb
Formatting
yveshauser Oct 31, 2024
428f8eb
Dropping nested module
yveshauser Oct 31, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 23 additions & 0 deletions formal-spec/Leios/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
open import Leios.Prelude
open import Leios.Abstract

module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) where

open import Leios.Blocks a using (EndorserBlock)

StakeDistr : Type
StakeDistr = PoolID ⇀ ℕ

record BaseAbstract : Type₁ where
field Cert : Type

data Input : Type₁ where
INIT : (EndorserBlock × Cert → Type) → Input
SUBMIT : EndorserBlock ⊎ List Tx → Input -- maybe we have both

data Output : Type where
STAKE : StakeDistr → Output

record Functionality : Type₁ where
field State : Type
_⇀⟦_⟧_ : State → Input → State × Output → Type
21 changes: 0 additions & 21 deletions formal-spec/Leios/BaseFunctionality.agda
View file
Open in desktop

This file was deleted.

35 changes: 18 additions & 17 deletions formal-spec/Leios/SimpleSpec.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,17 @@ open import Leios.Prelude
open import Leios.Abstract
open import Leios.FFD
open import Leios.VRF
import Leios.Base
import Leios.Blocks

module Leios.SimpleSpec (a : LeiosAbstract) (let open LeiosAbstract a) (let open Leios.Blocks a)
(id : PoolID) (pKey : PrivKey) (FFD : FFDAbstract.Functionality ffdAbstract)
(vrf : LeiosVRF a) (let open LeiosVRF vrf) (pubKey : PubKey) where
(id : PoolID) (pKey : PrivKey) (FFD' : FFDAbstract.Functionality ffdAbstract)
(vrf : LeiosVRF a) (let open LeiosVRF vrf) (pubKey : PubKey)
(let open Leios.Base a) (B' : BaseAbstract) (BF' : BaseAbstract.Functionality B') where

import Leios.BaseFunctionality

module FFD' = FFDAbstract.Functionality FFD using (State) renaming (stepRel to _⇀⟦_⟧_)
module B = Leios.BaseFunctionality a
module B = BaseAbstract B'
module BF = BaseAbstract.Functionality BF'
module FFD = FFDAbstract.Functionality FFD' using (State) renaming (stepRel to _⇀⟦_⟧_)

-- High level structure:

Expand All @@ -28,7 +29,7 @@ module B = Leios.BaseFunctionality a

postulate VTy FTCHTy : Type
initSlot : VTy → ℕ
initFFDState : FFD'.State
initFFDState : FFD.State

data LeiosInput : Type where
INIT : VTy → LeiosInput
Expand All @@ -41,16 +42,16 @@ data LeiosOutput : Type where

record LeiosState : Type where
field V : VTy
SD : B.StakeDistr
FFDState : FFD'.State
SD : StakeDistr
FFDState : FFD.State
Ledger : List Tx
MemPool : List Tx
IBs : List InputBlock
EBs : List EndorserBlock
Vs : List (List Vote)
slot : ℕ

initLeiosState : VTy → B.StakeDistr → LeiosState
initLeiosState : VTy → StakeDistr → LeiosState
initLeiosState V SD = record
{ V = V
; SD = SD
Expand Down Expand Up @@ -85,7 +86,7 @@ module _ (s : LeiosState) (eb : EndorserBlock) where
postulate instance isVote1Certified? : ∀ {s eb} → isVote1Certified s eb ⁇

private variable s : LeiosState
ffds' : FFD'.State
ffds' : FFD.State
π : VrfPf

open LeiosState using (FFDState; MemPool)
Expand All @@ -98,15 +99,15 @@ stake record { SD = SD } = case lookupᵐ? SD id of λ where
data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutput → Type where
Init : ∀ {V bs bs' SD} →
∙ {!!} -- create & register the IB/EB lottery and voting keys with key reg
∙ bs B.⇀⟦ B.INIT {!V_chkCerts!} ⟧ (bs' , B.STAKE SD)
∙ bs BF.⇀⟦ B.INIT {!V_chkCerts!} ⟧ (bs' , B.STAKE SD)
───────────────────────────────────────────────────
nothing ⇀⟦ INIT V ⟧ (initLeiosState V SD , EMPTY)

-- fix: we need to do Slot before every other SLOT transition
Slot : ∀ {msgs} → let ffds = s .FFDState
l = {!!} -- construct ledger l
in
∙ FFDAbstract.Fetch FFD'.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.FetchRes msgs)
∙ FFDAbstract.Fetch FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.FetchRes msgs)
──────────────────────────────────────────────────────────────────────
just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' ; Ledger = l } , EMPTY)

Expand All @@ -123,7 +124,7 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu
h = GenFFD.ibHeader (mkIBHeader slot id π pKey txs)
in
∙ canProduceIB slot pKey (stake s)
∙ FFDAbstract.Send h (just b) FFD'.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
∙ FFDAbstract.Send h (just b) FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
─────────────────────────────────────────────────────────────────────────
just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY)

Expand All @@ -135,7 +136,7 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu
ffds = s .FFDState
in
∙ canProduceEB slot pKey (stake s)
∙ FFDAbstract.Send (GenFFD.ebHeader h) nothing FFD'.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
∙ FFDAbstract.Send (GenFFD.ebHeader h) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
──────────────────────────────────────────────────────────────────────────────────────────
just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY)

Expand All @@ -145,7 +146,7 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu
ffds = s .FFDState
in
∙ canProduceV1 slot
∙ FFDAbstract.Send (GenFFD.vHeader votes) nothing FFD'.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
∙ FFDAbstract.Send (GenFFD.vHeader votes) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
─────────────────────────────────────────────────────────────────────────────────────────────
just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY)

Expand All @@ -155,6 +156,6 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu
ffds = s .FFDState
in
∙ canProduceV2 slot
∙ FFDAbstract.Send (GenFFD.vHeader votes) nothing FFD'.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
∙ FFDAbstract.Send (GenFFD.vHeader votes) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
─────────────────────────────────────────────────────────────────────────────────────────────
just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY)
Loading