Skip to content

Commit

Permalink
Post-rebase fixing
Browse files Browse the repository at this point in the history
  • Loading branch information
WhatisRT committed Jan 10, 2025
1 parent 3513775 commit b7a55a3
Show file tree
Hide file tree
Showing 5 changed files with 177 additions and 166 deletions.
2 changes: 1 addition & 1 deletion formal-spec/Leios/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ record BaseAbstract : Type₁ where
initSlot : VTy
V-chkCerts : List PubKey EndorserBlock × Cert Bool

data Input : Type where
data Input : Type where
INIT : (EndorserBlock × Cert Bool) Input
SUBMIT : RankingBlock Input
FTCH-LDG : Input
Expand Down
1 change: 1 addition & 0 deletions formal-spec/Leios/Protocol.agda
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ record LeiosState : Type where

addUpkeep : LeiosState SlotUpkeep LeiosState
addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ }
{-# INJECTIVE_FOR_INFERENCE addUpkeep #-}

initLeiosState : VTy StakeDistr B.State LeiosState
initLeiosState V SD bs = record
Expand Down
44 changes: 22 additions & 22 deletions formal-spec/Leios/Simple/Deterministic.agda
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,11 @@ open import Data.List.Relation.Unary.Any using (here)

open import Leios.SpecStructure

module Leios.Simple.Deterministic (⋯ : SpecStructure) (let open SpecStructure ⋯) where
module Leios.Simple.Deterministic (⋯ : SpecStructure 2) (let open SpecStructure) (Λ μ :) where

import Leios.Simple
open import Leios.Simple hiding (_-⟦_/_⟧⇀_)
module ND = Leios.Simple ⋯
import Leios.Simplified
open import Leios.Simplified ⋯ Λ μ hiding (_-⟦_/_⟧⇀_)
module ND = Leios.Simplified ⋯ Λ μ

open import Class.Computational
open import Class.Computational22
Expand All @@ -37,7 +37,7 @@ private variable s s' s0 s1 s2 s3 s4 s5 : LeiosState
ks ks' : K.State
msgs : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract)
eb : EndorserBlock
ebs : List EndorserBlock
rbs : List RankingBlock
txs : List Tx
V : VTy
SD : StakeDistr
Expand All @@ -61,15 +61,15 @@ data _-⟦Base⟧⇀_ : LeiosState → LeiosState → Type where

Base₂a : {ebs} let open LeiosState s renaming (BaseState to bs) in
∙ needsUpkeep Base
∙ eb ∷ ebs ≡ filter (λ eb isVote2Certified votingState eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (inj₁ eb) / B.EMPTY ⟧⇀ bs'
∙ eb ∷ ebs ≡ filter (λ eb isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs'
───────────────────────────────────────────────────────────────────────
s -⟦Base⟧⇀ addUpkeep record s { BaseState = bs' } Base

Base₂b : let open LeiosState s renaming (BaseState to bs) in
∙ needsUpkeep Base
∙ [] ≡ filter (λ eb isVote2Certified votingState eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (inj₂ ToPropose) / B.EMPTY ⟧⇀ bs'
∙ [] ≡ filter (λ eb isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs'
───────────────────────────────────────────────────────────────────────
s -⟦Base⟧⇀ addUpkeep record s { BaseState = bs' } Base

Expand All @@ -80,7 +80,7 @@ Base⇒ND (Base₂b x x₁ x₂) = Base₂b x x₁ x₂
opaque
Base-total : LeiosState.needsUpkeep s Base ∃[ s' ] s -⟦Base⟧⇀ s'
Base-total {s = s} needsUpkeep with
(let open LeiosState s in filter (λ eb isVote2Certified votingState eb × eb ∈ᴮ slice L slot 2) EBs)
(let open LeiosState s in filter (λ eb isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs)
in eq
... | [] = -, Base₂b needsUpkeep (sym eq) (proj₂ B.SUBMIT-total)
... | x ∷ l = -, Base₂a needsUpkeep (sym eq) (proj₂ B.SUBMIT-total)
Expand Down Expand Up @@ -108,8 +108,8 @@ data _-⟦IB-Role⟧⇀_ : LeiosState → LeiosState → Type where
s -⟦IB-Role⟧⇀ addUpkeep s IB-Role

IB-Role⇒ND : s -⟦IB-Role⟧⇀ s' just s ND.-⟦ SLOT / EMPTY ⟧⇀ s'
IB-Role⇒ND (IB-Role x x₁ x₂) = IB-Role x x₁ x₂
IB-Role⇒ND (No-IB-Role x x₁) = No-IB-Role x x₁
IB-Role⇒ND (IB-Role x x₁ x₂) = Roles (IB-Role x x₁ x₂)
IB-Role⇒ND (No-IB-Role x x₁) = Roles (No-IB-Role x x₁)

opaque
IB-Role-total : LeiosState.needsUpkeep s IB-Role ∃[ s' ] s -⟦IB-Role⟧⇀ s'
Expand All @@ -125,7 +125,7 @@ data _-⟦EB-Role⟧⇀_ : LeiosState → LeiosState → Type where

EB-Role : let open LeiosState s renaming (FFDState to ffds)
LI = map getIBRef $ filter (_∈ᴮ slice L slot (Λ + 1)) IBs
LE = map getEBRef $ filter (isVote1Certified votingState) $
LE = map getEBRef $ filter (isVote1Certified s) $
filter (_∈ᴮ slice L slot (μ + 2)) EBs
h = mkEB slot id π sk-EB LI LE
in
Expand All @@ -142,8 +142,8 @@ data _-⟦EB-Role⟧⇀_ : LeiosState → LeiosState → Type where
s -⟦EB-Role⟧⇀ addUpkeep s EB-Role

EB-Role⇒ND : s -⟦EB-Role⟧⇀ s' just s ND.-⟦ SLOT / EMPTY ⟧⇀ s'
EB-Role⇒ND (EB-Role x x₁ x₂) = EB-Role x x₁ x₂
EB-Role⇒ND (No-EB-Role x x₁) = No-EB-Role x x₁
EB-Role⇒ND (EB-Role x x₁ x₂) = Roles (EB-Role x x₁ x₂)
EB-Role⇒ND (No-EB-Role x x₁) = Roles (No-EB-Role x x₁)

opaque
EB-Role-total : LeiosState.needsUpkeep s EB-Role ∃[ s' ] s -⟦EB-Role⟧⇀ s'
Expand Down Expand Up @@ -172,8 +172,8 @@ data _-⟦V1-Role⟧⇀_ : LeiosState → LeiosState → Type where
s -⟦V1-Role⟧⇀ addUpkeep s V1-Role

V1-Role⇒ND : s -⟦V1-Role⟧⇀ s' just s ND.-⟦ SLOT / EMPTY ⟧⇀ s'
V1-Role⇒ND (V1-Role x x₁ x₂) = V1-Role x x₁ x₂
V1-Role⇒ND (No-V1-Role x x₁) = No-V1-Role x x₁
V1-Role⇒ND (V1-Role x x₁ x₂) = Roles (V1-Role x x₁ x₂)
V1-Role⇒ND (No-V1-Role x x₁) = Roles (No-V1-Role x x₁)

V1-Role-Upkeep : s -⟦V1-Role⟧⇀ s' LeiosState.needsUpkeep s V1-Role × ¬ LeiosState.needsUpkeep s' V1-Role
V1-Role-Upkeep (V1-Role x x₁ x₂) = x , addUpkeep⇒¬needsUpkeep
Expand All @@ -198,8 +198,8 @@ data _-⟦V2-Role⟧⇀_ : LeiosState → LeiosState → Type where
s -⟦V2-Role⟧⇀ addUpkeep s V2-Role

V2-Role⇒ND : s -⟦V2-Role⟧⇀ s' just s ND.-⟦ SLOT / EMPTY ⟧⇀ s'
V2-Role⇒ND (V2-Role x x₁ x₂) = V2-Role x x₁ x₂
V2-Role⇒ND (No-V2-Role x x₁) = No-V2-Role x x₁
V2-Role⇒ND (V2-Role x x₁ x₂) = Roles (V2-Role x x₁ x₂)
V2-Role⇒ND (No-V2-Role x x₁) = Roles (No-V2-Role x x₁)

V2-Role-Upkeep : s -⟦V2-Role⟧⇀ s' LeiosState.needsUpkeep s V2-Role × ¬ LeiosState.needsUpkeep s' V2-Role
V2-Role-Upkeep (V2-Role x x₁ x₂) = x , addUpkeep⇒¬needsUpkeep
Expand All @@ -215,14 +215,14 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState
Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs)
s0 = record s
{ FFDState = ffds'
; Ledger = constructLedger ebs
; Ledger = constructLedger rbs
; slot = suc slot
; Upkeep =
; BaseState = bs'
} ↑ L.filter isValid? msgs
in
∙ Upkeep ≡ᵉ allUpkeep
∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG ebs ⟧⇀ bs'
∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs'
∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds'
∙ s0 -⟦Base⟧⇀ s1
∙ s1 -⟦IB-Role⟧⇀ s2
Expand All @@ -244,7 +244,7 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState

Base₁ :
──────────────────────────────────────────────────────────────
s -⟦ SUBMIT txs / EMPTY ⟧⇀ record s { ToPropose = txs }
s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs }

-- Protocol rules

Expand Down
Loading

0 comments on commit b7a55a3

Please sign in to comment.