From d7b352db7cbe5603dbfefcb93aac5e5eb661aca5 Mon Sep 17 00:00:00 2001 From: Yves Date: Thu, 27 Feb 2025 17:57:31 +0100 Subject: [PATCH 01/22] Initial trace verifier --- formal-spec/Leios/Abstract.agda | 4 + formal-spec/Leios/Blocks.agda | 49 +++++--- formal-spec/Leios/{Foreign => }/Defaults.agda | 67 +++++++++-- formal-spec/Leios/FFD.agda | 3 + formal-spec/Leios/Foreign/Types.agda | 2 +- formal-spec/Leios/Protocol.agda | 3 + .../Leios/Simplified/Deterministic/Test.agda | 2 +- formal-spec/Leios/SpecStructure.agda | 2 +- formal-spec/Leios/Trace/Verifier.agda | 108 ++++++++++++++++++ 9 files changed, 207 insertions(+), 33 deletions(-) rename formal-spec/Leios/{Foreign => }/Defaults.agda (70%) create mode 100644 formal-spec/Leios/Trace/Verifier.agda diff --git a/formal-spec/Leios/Abstract.agda b/formal-spec/Leios/Abstract.agda index f8fd193..af62ad8 100644 --- a/formal-spec/Leios/Abstract.agda +++ b/formal-spec/Leios/Abstract.agda @@ -6,11 +6,15 @@ open import Leios.Prelude record LeiosAbstract : Type₁ where field Tx : Type + ⦃ DecEq-Tx ⦄ : DecEq Tx PoolID : Type ⦃ DecEq-PoolID ⦄ : DecEq PoolID BodyHash VrfPf PrivKey Sig Hash : Type -- these could have been byte strings, but this is safer ⦃ DecEq-Hash ⦄ : DecEq Hash + ⦃ DecEq-VrfPf ⦄ : DecEq VrfPf + ⦃ DecEq-Sig ⦄ : DecEq Sig Vote : Type + ⦃ DecEq-Vote ⦄ : DecEq Vote vote : PrivKey → Hash → Vote sign : PrivKey → Hash → Sig ⦃ Hashable-Txs ⦄ : Hashable (List Tx) Hash diff --git a/formal-spec/Leios/Blocks.agda b/formal-spec/Leios/Blocks.agda index 29a2116..a2d509b 100644 --- a/formal-spec/Leios/Blocks.agda +++ b/formal-spec/Leios/Blocks.agda @@ -3,6 +3,8 @@ open import Leios.Prelude open import Leios.Abstract open import Leios.FFD +open import Tactic.Defaults +open import Tactic.Derive.DecEq module Leios.Blocks (a : LeiosAbstract) (let open LeiosAbstract a) where @@ -20,10 +22,6 @@ record IsBlock (B : Type) : Type where open IsBlock ⦃...⦄ public -OSig : Bool → Type -OSig true = Sig -OSig false = ⊤ - IBRef = Hash EBRef = Hash @@ -31,15 +29,15 @@ EBRef = Hash -- Input Blocks -------------------------------------------------------------------------------- -record IBHeaderOSig (b : Bool) : Type where +record IBHeaderOSig (sig : Type) : Type where field slotNumber : ℕ producerID : PoolID lotteryPf : VrfPf bodyHash : Hash - signature : OSig b + signature : sig -IBHeader = IBHeaderOSig true -PreIBHeader = IBHeaderOSig false +IBHeader = IBHeaderOSig Sig +PreIBHeader = IBHeaderOSig ⊤ record IBBody : Type where field txs : List Tx @@ -50,20 +48,30 @@ record InputBlock : Type where open IBHeaderOSig header public +unquoteDecl DecEq-IBBody DecEq-IBHeaderOSig DecEq-InputBlock = + derive-DecEq ( + (quote IBBody , DecEq-IBBody) + ∷ (quote IBHeaderOSig , DecEq-IBHeaderOSig) + ∷ (quote InputBlock , DecEq-InputBlock) ∷ []) + instance - IsBlock-IBHeaderOSig : ∀ {b} → IsBlock (IBHeaderOSig b) - IsBlock-IBHeaderOSig = record { IBHeaderOSig } + IsBlock-IBHeader : IsBlock IBHeader + IsBlock-IBHeader = record { IBHeaderOSig } Hashable-IBBody : Hashable IBBody Hash Hashable-IBBody .hash b = hash (b .IBBody.txs) + Hashable-IBHeader : ⦃ Hashable PreIBHeader Hash ⦄ → Hashable IBHeader Hash + Hashable-IBHeader .hash b = hash {T = PreIBHeader} + record { IBHeaderOSig b hiding (signature) ; signature = _ } + IsBlock-InputBlock : IsBlock InputBlock IsBlock-InputBlock = record { InputBlock } mkIBHeader : ⦃ Hashable PreIBHeader Hash ⦄ → ℕ → PoolID → VrfPf → PrivKey → List Tx → IBHeader mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHeaderOSig h } where - h : IBHeaderOSig false + h : IBHeaderOSig ⊤ h = record { slotNumber = slot ; producerID = id ; lotteryPf = π @@ -71,7 +79,7 @@ mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHea ; signature = _ } -getIBRef : ⦃ Hashable IBHeader Hash ⦄ → InputBlock → IBRef +getIBRef : ⦃ Hashable PreIBHeader Hash ⦄ → InputBlock → IBRef getIBRef = hash ∘ InputBlock.header -- TODO @@ -94,24 +102,26 @@ ibValid? record { header = h ; body = b } = ibHeaderValid? h ×-dec ibBodyValid? -- Endorser Blocks -------------------------------------------------------------------------------- -record EndorserBlockOSig (b : Bool) : Type where +record EndorserBlockOSig (sig : Type) : Type where field slotNumber : ℕ producerID : PoolID lotteryPf : VrfPf ibRefs : List IBRef ebRefs : List EBRef - signature : OSig b + signature : sig -EndorserBlock = EndorserBlockOSig true -PreEndorserBlock = EndorserBlockOSig false +EndorserBlock = EndorserBlockOSig Sig +PreEndorserBlock = EndorserBlockOSig ⊤ instance Hashable-EndorserBlock : ⦃ Hashable PreEndorserBlock Hash ⦄ → Hashable EndorserBlock Hash Hashable-EndorserBlock .hash b = hash {T = PreEndorserBlock} record { EndorserBlockOSig b hiding (signature) ; signature = _ } - IsBlock-EndorserBlockOSig : ∀ {b} → IsBlock (EndorserBlockOSig b) - IsBlock-EndorserBlockOSig {b} = record { EndorserBlockOSig } + IsBlock-EndorserBlock : IsBlock EndorserBlock + IsBlock-EndorserBlock = record { EndorserBlockOSig } + +unquoteDecl DecEq-EndorserBlockOSig = derive-DecEq ((quote EndorserBlockOSig , DecEq-EndorserBlockOSig) ∷ []) mkEB : ⦃ Hashable PreEndorserBlock Hash ⦄ → ℕ → PoolID → VrfPf → PrivKey → List IBRef → List EBRef → EndorserBlock mkEB slot id π pKey LI LE = record { signature = sign pKey (hash b) ; EndorserBlockOSig b } @@ -161,6 +171,9 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where data Body : Type where ibBody : IBBody → Body + unquoteDecl DecEq-Header DecEq-Body = + derive-DecEq ((quote Header , DecEq-Header) ∷ (quote Body , DecEq-Body) ∷ []) + ID : Type ID = ℕ × PoolID diff --git a/formal-spec/Leios/Foreign/Defaults.agda b/formal-spec/Leios/Defaults.agda similarity index 70% rename from formal-spec/Leios/Foreign/Defaults.agda rename to formal-spec/Leios/Defaults.agda index 3ca74fd..95ff3d5 100644 --- a/formal-spec/Leios/Foreign/Defaults.agda +++ b/formal-spec/Leios/Defaults.agda @@ -6,12 +6,13 @@ open import Leios.SpecStructure open import Axiom.Set.Properties th open import Data.Nat.Show as N -open import Data.Integer +open import Data.Integer hiding (_≟_) open import Data.String as S using (intersperse) open import Function.Related.TypeIsomorphisms open import Relation.Binary.Structures -import Data.Sum +open import Tactic.Defaults +open import Tactic.Derive.DecEq open Equivalence @@ -21,7 +22,7 @@ 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.Foreign.Defaults (numberOfParties : ℕ) (SUT-id : Fin numberOfParties) where +module Leios.Defaults (numberOfParties : ℕ) (SUT-id : Fin numberOfParties) where instance htx : Hashable (List ℕ) String @@ -85,11 +86,15 @@ d-Base = ; V-chkCerts = λ _ _ → true } + +-- data SimpleBase : ⊤ → BaseAbstract.Input d-Base → BaseAbstract.Output d-Base → ⊤ → Type where + d-BaseFunctionality : BaseAbstract.Functionality d-Base d-BaseFunctionality = record { State = ⊤ ; _-⟦_/_⟧⇀_ = λ _ _ _ _ → ⊤ +-- ; Dec-_-⟦_/_⟧⇀_ = ⁇ (yes tt) ; SUBMIT-total = tt , tt } @@ -104,7 +109,7 @@ instance ; lotteryPf = λ _ → tt } - hhs : ∀ {b} → Hashable (IBHeaderOSig b) String + hhs : Hashable PreIBHeader String hhs = record { hash = IBHeaderOSig.bodyHash } hpe : Hashable PreEndorserBlock String @@ -119,6 +124,8 @@ record FFDState : Type where outEBs : List EndorserBlock outVTs : List (List Vote) +unquoteDecl DecEq-FFDState = derive-DecEq ((quote FFDState , DecEq-FFDState) ∷ []) + open GenFFD.Header open GenFFD.Body open FFDState @@ -142,14 +149,45 @@ data SimpleFFD : FFDState → FFDAbstract.Input ffdAbstract → FFDAbstract.Outp Fetch : ∀ {s} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes (flushIns s)) (record s { inIBs = [] ; inEBs = [] ; inVTs = [] }) -simple-total : ∀ {s h b} → ∃[ s' ] (SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s') -simple-total {s} {ibHeader h} {just (ibBody b)} = record s { outIBs = record {header = h; body = b} ∷ outIBs s} , SendIB -simple-total {s} {ebHeader eb} {nothing} = record s { outEBs = eb ∷ outEBs s} , SendEB -simple-total {s} {vHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS +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} {ibHeader h} {nothing} = s , BadSendIB +send-total {s} {ebHeader eb} {just _} = s , BadSendEB +send-total {s} {vHeader 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) -simple-total {s} {ibHeader h} {nothing} = s , BadSendIB -simple-total {s} {ebHeader eb} {just _} = s , BadSendEB -simple-total {s} {vHeader vs} {just _} = s , BadSendVS +send-complete : ∀ {s h b s'} → SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s' → s' ≡ proj₁ (send-total {s} {h} {b}) +send-complete SendIB = refl +send-complete SendEB = refl +send-complete SendVS = refl +send-complete BadSendIB = refl +send-complete BadSendEB = refl +send-complete BadSendVS = refl + +fetch-complete₁ : ∀ {s r s'} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes r) s' → s' ≡ proj₁ (proj₂ (fetch-total {s})) +fetch-complete₁ Fetch = refl + +fetch-complete₂ : ∀ {s r s'} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes r) s' → r ≡ proj₁ (fetch-total {s}) +fetch-complete₂ Fetch = refl + +instance + Dec-SimpleFFD : ∀ {s i o s'} → SimpleFFD s i o s' ⁇ + Dec-SimpleFFD {s} {FFDAbstract.Send h b} {FFDAbstract.SendRes} {s'} with s' ≟ proj₁ (send-total {s} {h} {b}) + ... | yes p rewrite p = ⁇ yes (proj₂ send-total) + ... | no ¬p = ⁇ no λ x → ⊥-elim (¬p (send-complete x)) + Dec-SimpleFFD {_} {FFDAbstract.Send _ _} {FFDAbstract.FetchRes _} {_} = ⁇ no λ () + Dec-SimpleFFD {s} {FFDAbstract.Fetch} {FFDAbstract.FetchRes r} {s'} + with s' ≟ proj₁ (proj₂ (fetch-total {s})) + | r ≟ proj₁ (fetch-total {s}) + ... | yes p | yes q rewrite p rewrite q = ⁇ yes (proj₂ (proj₂ (fetch-total {s}))) + ... | yes p | no ¬q = ⁇ no λ x → ⊥-elim (¬q (fetch-complete₂ x)) + ... | no ¬p | _ = ⁇ no λ x → ⊥-elim (¬p (fetch-complete₁ x)) + Dec-SimpleFFD {_} {FFDAbstract.Fetch} {FFDAbstract.SendRes} {_} = ⁇ no λ () d-FFDFunctionality : FFDAbstract.Functionality ffdAbstract d-FFDFunctionality = @@ -157,7 +195,8 @@ d-FFDFunctionality = { State = FFDState ; initFFDState = record { inIBs = []; inEBs = []; inVTs = []; outIBs = []; outEBs = []; outVTs = [] } ; _-⟦_/_⟧⇀_ = SimpleFFD - ; FFD-Send-total = simple-total + ; Dec-_-⟦_/_⟧⇀_ = Dec-SimpleFFD + ; FFD-Send-total = send-total } open import Leios.Voting public @@ -181,6 +220,8 @@ d-VotingAbstract-2 = st : SpecStructure 1 st = record { a = d-Abstract + ; Hashable-PreIBHeader = hhs + ; Hashable-PreEndorserBlock = hpe ; id = SUT-id ; FFD' = d-FFDFunctionality ; vrf' = d-VRF @@ -201,6 +242,8 @@ st = record st-2 : SpecStructure 2 st-2 = record { a = d-Abstract + ; Hashable-PreIBHeader = hhs + ; Hashable-PreEndorserBlock = hpe ; id = SUT-id ; FFD' = d-FFDFunctionality ; vrf' = d-VRF diff --git a/formal-spec/Leios/FFD.agda b/formal-spec/Leios/FFD.agda index 23f9827..38277ed 100644 --- a/formal-spec/Leios/FFD.agda +++ b/formal-spec/Leios/FFD.agda @@ -6,6 +6,8 @@ open import Leios.Prelude record FFDAbstract : Type₁ where field Header Body ID : Type + ⦃ DecEq-Header ⦄ : DecEq Header + ⦃ DecEq-Body ⦄ : DecEq Body match : Header → Body → Type msgID : Header → ID @@ -21,6 +23,7 @@ record FFDAbstract : Type₁ where field State : Type initFFDState : State _-⟦_/_⟧⇀_ : State → Input → Output → State → Type + Dec-_-⟦_/_⟧⇀_ : {s : State} → {i : Input} → {o : Output} → {s' : State} → (s -⟦ i / o ⟧⇀ s') ⁇ FFD-Send-total : ∀ {ffds h b} → ∃[ ffds' ] ffds -⟦ Send h b / SendRes ⟧⇀ ffds' open Input public diff --git a/formal-spec/Leios/Foreign/Types.agda b/formal-spec/Leios/Foreign/Types.agda index 5a03def..a3b38bd 100644 --- a/formal-spec/Leios/Foreign/Types.agda +++ b/formal-spec/Leios/Foreign/Types.agda @@ -22,7 +22,7 @@ module Leios.Foreign.Types where numberOfParties : ℕ numberOfParties = 2 -open import Leios.Foreign.Defaults numberOfParties fzero +open import Leios.Defaults numberOfParties fzero renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda) dropDash : S.String → S.String diff --git a/formal-spec/Leios/Protocol.agda b/formal-spec/Leios/Protocol.agda index 9e40070..916fe07 100644 --- a/formal-spec/Leios/Protocol.agda +++ b/formal-spec/Leios/Protocol.agda @@ -67,6 +67,9 @@ record LeiosState : Type where needsUpkeep : SlotUpkeep → Set needsUpkeep = _∉ Upkeep + Dec-needsUpkeep : ∀ {u : SlotUpkeep} → ⦃ DecEq SlotUpkeep ⦄ → needsUpkeep u ⁇ + Dec-needsUpkeep {u} .dec = ¬? (u ∈? Upkeep) + addUpkeep : LeiosState → SlotUpkeep → LeiosState addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ } {-# INJECTIVE_FOR_INFERENCE addUpkeep #-} diff --git a/formal-spec/Leios/Simplified/Deterministic/Test.agda b/formal-spec/Leios/Simplified/Deterministic/Test.agda index a941eef..7ae4ce9 100644 --- a/formal-spec/Leios/Simplified/Deterministic/Test.agda +++ b/formal-spec/Leios/Simplified/Deterministic/Test.agda @@ -10,7 +10,7 @@ import Data.List as L open import Data.List.Relation.Unary.Any using (here) open import Leios.SpecStructure -open import Leios.Trace using (st-2) +open import Leios.Foreign.Defaults 2 fzero using (st-2) module Leios.Simplified.Deterministic.Test (Λ μ : ℕ) where diff --git a/formal-spec/Leios/SpecStructure.agda b/formal-spec/Leios/SpecStructure.agda index 0ab4317..5c14b9f 100644 --- a/formal-spec/Leios/SpecStructure.agda +++ b/formal-spec/Leios/SpecStructure.agda @@ -21,7 +21,7 @@ record SpecStructure (rounds : ℕ) : Type₁ where open Leios.Blocks a public field ⦃ IsBlock-Vote ⦄ : IsBlock (List Vote) - ⦃ Hashable-IBHeaderOSig ⦄ : ∀ {b} → Hashable (IBHeaderOSig b) Hash + ⦃ Hashable-PreIBHeader ⦄ : Hashable PreIBHeader Hash ⦃ Hashable-PreEndorserBlock ⦄ : Hashable PreEndorserBlock Hash id : PoolID FFD' : FFDAbstract.Functionality ffdAbstract diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda new file mode 100644 index 0000000..2aff8cd --- /dev/null +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -0,0 +1,108 @@ +open import Leios.Prelude +open import Leios.Defaults 2 fzero +open import Leios.SpecStructure + +module Leios.Trace.Verifier where + +--open SpecStructure ⦃ st ⦄ +open FFDAbstract + +module FFD = FFDAbstract.Functionality d-FFDFunctionality +module B = BaseAbstract.Functionality d-BaseFunctionality + +IB-Role? : ∀ {s π ffds' sk-IB} → + let open LeiosState s renaming (FFDState to ffds) + b = GenFFD.ibBody (record { txs = ToPropose }) + h = GenFFD.ibHeader (mkIBHeader slot fzero π sk-IB ToPropose) + in + { _ : auto∶ needsUpkeep IB-Role } + { _ : auto∶ canProduceIB slot sk-IB (stake s) π } + { _ : auto∶ ffds FFD.-⟦ Send h (just b) / SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } IB-Role +IB-Role? {_} {_} {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) + +No-IB-Role? : ∀ {s sk-IB} → let open LeiosState s + in + { _ : auto∶ needsUpkeep IB-Role } + { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } → + ───────────────────────────────────────────── + s ↝ addUpkeep s IB-Role +No-IB-Role? {_} {_} {p} {q} = No-IB-Role (toWitness p) (toWitness q) + +EB-Role? : ∀ {s π ffds' sk-EB} → + let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot fzero π sk-EB LI [] + in + { _ : auto∶ needsUpkeep EB-Role } + { _ : auto∶ canProduceEB slot sk-EB (stake s) π } + { _ : auto∶ ffds FFD.-⟦ Send (GenFFD.ebHeader h) nothing / SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } EB-Role +EB-Role? {_} {_} {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) + +No-EB-Role? : ∀ {s sk-IB} → let open LeiosState s + in + { _ : auto∶ needsUpkeep EB-Role } + { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-IB (stake s) π } → + ───────────────────────────────────────────── + s ↝ addUpkeep s EB-Role +No-EB-Role? {_} {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) + +V-Role? : ∀ {s ffds' sk-V} → + let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + in + { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ canProduceV slot sk-V (stake s) } + { _ : auto∶ ffds FFD.-⟦ Send (GenFFD.vHeader votes) nothing / SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } V-Role +V-Role? {_} {_} {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) + +{- +Init? : ∀ {ks pks ks' SD bs' V} → + { _ : auto∶ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' } + { _ : initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' } → + ──────────────────────────────────────────────────────────────── + nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' +Init? = ? +-} + +Base₂a? : ∀ {s eb bs'} → + let open LeiosState s renaming (BaseState to bs) + in + { _ : auto∶ needsUpkeep Base } + { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base +Base₂a? {_} {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) {!!} -- (toWitness r) + +Base₂b? : ∀ {s bs'} → + let open LeiosState s renaming (BaseState to bs) + in + { _ : auto∶ needsUpkeep Base } + { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base +Base₂b? {_} {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) {!!} -- (toWitness r) + +Slot? : ∀ {s rbs bs' msgs ffds'} → + let open LeiosState s renaming (FFDState to ffds; BaseState to bs) + in + { _ : auto∶ Upkeep ≡ᵉ allUpkeep } + { _ : auto∶ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' } + { _ : auto∶ ffds FFD.-⟦ FFDAbstract.Fetch / FFDAbstract.FetchRes msgs ⟧⇀ ffds' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ record s + { FFDState = ffds' + ; BaseState = bs' + ; Ledger = constructLedger rbs + ; slot = suc slot + ; Upkeep = ∅ + } ↑ L.filter GenFFD.isValid? msgs +Slot? {_} {_} {_} {_} {_} {p} {q} {r} = {!!} -- Slot (toWitness p) (toWitness q) (toWitness r) From 248bca0b1e68ab70039b08e88e597c3ccb134ded Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Thu, 27 Feb 2025 22:34:09 +0100 Subject: [PATCH 02/22] SpecStructure as parameter for verifier --- formal-spec/Leios/Base.agda | 1 + formal-spec/Leios/FFD.agda | 2 +- formal-spec/Leios/Trace/Verifier.agda | 57 +++++++++++++-------------- 3 files changed, 29 insertions(+), 31 deletions(-) diff --git a/formal-spec/Leios/Base.agda b/formal-spec/Leios/Base.agda index fc9cbbb..9987cd7 100644 --- a/formal-spec/Leios/Base.agda +++ b/formal-spec/Leios/Base.agda @@ -34,6 +34,7 @@ record BaseAbstract : Type₁ where record Functionality : Type₁ where field State : Type _-⟦_/_⟧⇀_ : State → Input → Output → State → Type + ⦃ Dec-_-⟦_/_⟧⇀_ ⦄ : {s : State} → {i : Input} → {o : Output} → {s' : State} → (s -⟦ i / o ⟧⇀ s') ⁇ SUBMIT-total : ∀ {s b} → ∃[ s' ] s -⟦ SUBMIT b / EMPTY ⟧⇀ s' open Input public diff --git a/formal-spec/Leios/FFD.agda b/formal-spec/Leios/FFD.agda index 38277ed..1ca95ae 100644 --- a/formal-spec/Leios/FFD.agda +++ b/formal-spec/Leios/FFD.agda @@ -23,7 +23,7 @@ record FFDAbstract : Type₁ where field State : Type initFFDState : State _-⟦_/_⟧⇀_ : State → Input → Output → State → Type - Dec-_-⟦_/_⟧⇀_ : {s : State} → {i : Input} → {o : Output} → {s' : State} → (s -⟦ i / o ⟧⇀ s') ⁇ + ⦃ Dec-_-⟦_/_⟧⇀_ ⦄ : {s : State} → {i : Input} → {o : Output} → {s' : State} → (s -⟦ i / o ⟧⇀ s') ⁇ FFD-Send-total : ∀ {ffds h b} → ∃[ ffds' ] ffds -⟦ Send h b / SendRes ⟧⇀ ffds' open Input public diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 2aff8cd..82db365 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -1,66 +1,63 @@ -open import Leios.Prelude -open import Leios.Defaults 2 fzero -open import Leios.SpecStructure +open import Leios.Prelude hiding (id) +open import Leios.SpecStructure using (SpecStructure) -module Leios.Trace.Verifier where +module Leios.Trace.Verifier (⋯ : SpecStructure 1) (let open SpecStructure ⋯) where ---open SpecStructure ⦃ st ⦄ -open FFDAbstract +open import Leios.Short ⋯ renaming (isVoteCertified to isVoteCertified') +open B hiding (_-⟦_/_⟧⇀_) +open FFD hiding (_-⟦_/_⟧⇀_) -module FFD = FFDAbstract.Functionality d-FFDFunctionality -module B = BaseAbstract.Functionality d-BaseFunctionality - -IB-Role? : ∀ {s π ffds' sk-IB} → +IB-Role? : ∀ {s π ffds'} → let open LeiosState s renaming (FFDState to ffds) b = GenFFD.ibBody (record { txs = ToPropose }) - h = GenFFD.ibHeader (mkIBHeader slot fzero π sk-IB ToPropose) + h = GenFFD.ibHeader (mkIBHeader slot id π sk-IB ToPropose) in { _ : auto∶ needsUpkeep IB-Role } { _ : auto∶ canProduceIB slot sk-IB (stake s) π } - { _ : auto∶ ffds FFD.-⟦ Send h (just b) / SendRes ⟧⇀ ffds' } → + { _ : auto∶ ffds FFD.-⟦ FFD.Send h (just b) / FFD.SendRes ⟧⇀ ffds' } → ───────────────────────────────────────────────────────────────────────── s ↝ addUpkeep record s { FFDState = ffds' } IB-Role -IB-Role? {_} {_} {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) +IB-Role? {_} {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) -No-IB-Role? : ∀ {s sk-IB} → let open LeiosState s +No-IB-Role? : ∀ {s} → let open LeiosState s in { _ : auto∶ needsUpkeep IB-Role } { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } → ───────────────────────────────────────────── s ↝ addUpkeep s IB-Role -No-IB-Role? {_} {_} {p} {q} = No-IB-Role (toWitness p) (toWitness q) +No-IB-Role? {_} {p} {q} = No-IB-Role (toWitness p) (toWitness q) -EB-Role? : ∀ {s π ffds' sk-EB} → +EB-Role? : ∀ {s π ffds'} → let open LeiosState s renaming (FFDState to ffds) LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs - h = mkEB slot fzero π sk-EB LI [] + h = mkEB slot id π sk-EB LI [] in { _ : auto∶ needsUpkeep EB-Role } { _ : auto∶ canProduceEB slot sk-EB (stake s) π } - { _ : auto∶ ffds FFD.-⟦ Send (GenFFD.ebHeader h) nothing / SendRes ⟧⇀ ffds' } → + { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds' } → ───────────────────────────────────────────────────────────────────────── s ↝ addUpkeep record s { FFDState = ffds' } EB-Role -EB-Role? {_} {_} {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) +EB-Role? {_} {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) -No-EB-Role? : ∀ {s sk-IB} → let open LeiosState s +No-EB-Role? : ∀ {s} → let open LeiosState s in { _ : auto∶ needsUpkeep EB-Role } { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-IB (stake s) π } → ───────────────────────────────────────────── s ↝ addUpkeep s EB-Role -No-EB-Role? {_} {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) +No-EB-Role? {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) -V-Role? : ∀ {s ffds' sk-V} → +V-Role? : ∀ {s ffds'} → let open LeiosState s renaming (FFDState to ffds) EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' in { _ : auto∶ needsUpkeep V-Role } { _ : auto∶ canProduceV slot sk-V (stake s) } - { _ : auto∶ ffds FFD.-⟦ Send (GenFFD.vHeader votes) nothing / SendRes ⟧⇀ ffds' } → + { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } → ───────────────────────────────────────────────────────────────────────── s ↝ addUpkeep record s { FFDState = ffds' } V-Role -V-Role? {_} {_} {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) +V-Role? {_} {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) {- Init? : ∀ {ks pks ks' SD bs' V} → @@ -75,28 +72,28 @@ Base₂a? : ∀ {s eb bs'} → let open LeiosState s renaming (BaseState to bs) in { _ : auto∶ needsUpkeep Base } - { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } { _ : auto∶ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' } → ─────────────────────────────────────────────────────────────────────── just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base -Base₂a? {_} {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) {!!} -- (toWitness r) +Base₂a? {_} {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) (toWitness r) Base₂b? : ∀ {s bs'} → let open LeiosState s renaming (BaseState to bs) in { _ : auto∶ needsUpkeep Base } - { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } { _ : auto∶ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' } → ─────────────────────────────────────────────────────────────────────── just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base -Base₂b? {_} {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) {!!} -- (toWitness r) +Base₂b? {_} {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) (toWitness r) Slot? : ∀ {s rbs bs' msgs ffds'} → let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in { _ : auto∶ Upkeep ≡ᵉ allUpkeep } { _ : auto∶ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' } - { _ : auto∶ ffds FFD.-⟦ FFDAbstract.Fetch / FFDAbstract.FetchRes msgs ⟧⇀ ffds' } → + { _ : auto∶ ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds' } → ─────────────────────────────────────────────────────────────────────── just s -⟦ SLOT / EMPTY ⟧⇀ record s { FFDState = ffds' @@ -105,4 +102,4 @@ Slot? : ∀ {s rbs bs' msgs ffds'} → ; slot = suc slot ; Upkeep = ∅ } ↑ L.filter GenFFD.isValid? msgs -Slot? {_} {_} {_} {_} {_} {p} {q} {r} = {!!} -- Slot (toWitness p) (toWitness q) (toWitness r) +Slot? {_} {_} {_} {_} {_} {p} {q} {r} = Slot (toWitness p) (toWitness q) (toWitness r) From 7016cc1303d174b520685d4dd281d101beb574a9 Mon Sep 17 00:00:00 2001 From: Yves Date: Fri, 28 Feb 2025 10:53:30 +0100 Subject: [PATCH 03/22] Code extraction parameters --- formal-spec/Leios/Foreign/Types.agda | 29 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/formal-spec/Leios/Foreign/Types.agda b/formal-spec/Leios/Foreign/Types.agda index a3b38bd..624f97d 100644 --- a/formal-spec/Leios/Foreign/Types.agda +++ b/formal-spec/Leios/Foreign/Types.agda @@ -19,10 +19,7 @@ module Leios.Foreign.Types where {-# LANGUAGE DuplicateRecordFields #-} #-} -numberOfParties : ℕ -numberOfParties = 2 - -open import Leios.Defaults numberOfParties fzero +open import Leios.Defaults 2 fzero -- TODO: parameters renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda) dropDash : S.String → S.String @@ -49,13 +46,14 @@ data IBHeader = IBHeader {slotNumber :: Integer, producerID :: Integer, bodyHash instance HsTy-IBHeader = MkHsType IBHeaderAgda IBHeader + Conv-IBHeader : Convertible IBHeaderAgda IBHeader Conv-IBHeader = record { to = λ (record { slotNumber = s ; producerID = p ; bodyHash = h }) → record { slotNumber = s ; producerID = toℕ p ; bodyHash = h} ; from = λ (record { slotNumber = s ; producerID = p ; bodyHash = h }) → - case p Date: Fri, 28 Feb 2025 13:37:53 +0100 Subject: [PATCH 04/22] Commented negative rules --- formal-spec/Leios/Trace/Verifier.agda | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 82db365..fe4a1be 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -19,13 +19,15 @@ IB-Role? : ∀ {s π ffds'} → s ↝ addUpkeep record s { FFDState = ffds' } IB-Role IB-Role? {_} {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) +{- No-IB-Role? : ∀ {s} → let open LeiosState s in { _ : auto∶ needsUpkeep IB-Role } { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } → ───────────────────────────────────────────── s ↝ addUpkeep s IB-Role -No-IB-Role? {_} {p} {q} = No-IB-Role (toWitness p) (toWitness q) +No-IB-Role? {_} {p} = No-IB-Role (toWitness p) (toWitness q) +-} EB-Role? : ∀ {s π ffds'} → let open LeiosState s renaming (FFDState to ffds) @@ -39,13 +41,15 @@ EB-Role? : ∀ {s π ffds'} → s ↝ addUpkeep record s { FFDState = ffds' } EB-Role EB-Role? {_} {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) +{- No-EB-Role? : ∀ {s} → let open LeiosState s in { _ : auto∶ needsUpkeep EB-Role } - { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-IB (stake s) π } → + { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-EB (stake s) π } → ───────────────────────────────────────────── s ↝ addUpkeep s EB-Role No-EB-Role? {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) +-} V-Role? : ∀ {s ffds'} → let open LeiosState s renaming (FFDState to ffds) @@ -59,6 +63,13 @@ V-Role? : ∀ {s ffds'} → s ↝ addUpkeep record s { FFDState = ffds' } V-Role V-Role? {_} {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) +No-V-Role? : ∀ {s} → let open LeiosState s in + { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } → + ───────────────────────────────────────────── + s ↝ addUpkeep s V-Role +No-V-Role? {_} {p} {q} = No-V-Role (toWitness p) (toWitness q) + {- Init? : ∀ {ks pks ks' SD bs' V} → { _ : auto∶ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' } From d4b16afdb886fec4b79537699879e9df7e115675 Mon Sep 17 00:00:00 2001 From: Yves Date: Fri, 28 Feb 2025 14:03:25 +0100 Subject: [PATCH 05/22] Updated Everything --- formal-spec/Everything.agda | 29 ++++++++++++++++--- formal-spec/Leios/Defaults.agda | 29 ++++++++++++++++++- formal-spec/Leios/Foreign/Types.agda | 25 +--------------- .../Leios/Simplified/Deterministic/Test.agda | 19 ++---------- 4 files changed, 57 insertions(+), 45 deletions(-) diff --git a/formal-spec/Everything.agda b/formal-spec/Everything.agda index 6024936..888e466 100644 --- a/formal-spec/Everything.agda +++ b/formal-spec/Everything.agda @@ -1,8 +1,29 @@ module Everything where -open import Leios.Simplified -open import Leios.Simplified.Deterministic +open import CategoricalCrypto +open import Class.Computational22 +open import Leios.Abstract +open import Leios.Base +open import Leios.Blocks +open import Leios.Defaults +open import Leios.FFD +open import Leios.Foreign.BaseTypes +open import Leios.Foreign.HsTypes +open import Leios.Foreign.Types +open import Leios.Foreign.Util +open import Leios.KeyRegistration +open import Leios.Network +open import Leios.Prelude +open import Leios.Protocol open import Leios.Short open import Leios.Short.Deterministic -open import Leios.Network -open import Leios.Foreign.Types +open import Leios.Simplified +open import Leios.Simplified.Deterministic +open import Leios.Simplified.Deterministic.Test +open import Leios.SpecStructure +open import Leios.Traces +open import Leios.Trace.Verifier +open import Leios.UniformShort +open import Leios.Voting +open import Leios.VRF +open import StateMachine diff --git a/formal-spec/Leios/Defaults.agda b/formal-spec/Leios/Defaults.agda index 95ff3d5..00abe9d 100644 --- a/formal-spec/Leios/Defaults.agda +++ b/formal-spec/Leios/Defaults.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --allow-unsolved-metas #-} open import Leios.Prelude open import Leios.Abstract @@ -293,3 +293,30 @@ open FunTot (completeFin numberOfParties) (maximalFin numberOfParties) sd : TotalMap (Fin numberOfParties) ℕ sd = Fun⇒TotalMap toℕ + +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 diff --git a/formal-spec/Leios/Foreign/Types.agda b/formal-spec/Leios/Foreign/Types.agda index 624f97d..70c978c 100644 --- a/formal-spec/Leios/Foreign/Types.agda +++ b/formal-spec/Leios/Foreign/Types.agda @@ -143,32 +143,9 @@ instance open import Class.Computational as C open import Class.Computational22 +open import Leios.Short.Deterministic st public 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 _ _ _ _ _ = error "Computational-B completeness" - - 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 _ _ _ _ _ = error "Computational-FFD completeness" - -open import Leios.Short.Deterministic st as D public stepHs : HsType (LeiosState → LeiosInput → C.ComputationResult String (LeiosOutput × LeiosState)) stepHs = to (compute Computational--⟦/⟧⇀) diff --git a/formal-spec/Leios/Simplified/Deterministic/Test.agda b/formal-spec/Leios/Simplified/Deterministic/Test.agda index 7ae4ce9..09f1d6a 100644 --- a/formal-spec/Leios/Simplified/Deterministic/Test.agda +++ b/formal-spec/Leios/Simplified/Deterministic/Test.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --allow-unsolved-metas #-} + -------------------------------------------------------------------------------- -- Deterministic variant of simple Leios -------------------------------------------------------------------------------- @@ -10,7 +12,7 @@ import Data.List as L open import Data.List.Relation.Unary.Any using (here) open import Leios.SpecStructure -open import Leios.Foreign.Defaults 2 fzero using (st-2) +open import Leios.Defaults 2 fzero using (st-2; isb; Computational-B; Computational-FFD) module Leios.Simplified.Deterministic.Test (Λ μ : ℕ) where @@ -47,21 +49,6 @@ private variable s s' s0 s1 s2 s3 s4 s5 : LeiosState open Computational22 ⦃...⦄ open import Leios.Simplified.Deterministic st-2 Λ μ -instance - Computational-B : Computational22 B._-⟦_/_⟧⇀_ String - Computational-B .computeProof s (BaseAbstract.Input.INIT x) = - success ((BaseAbstract.Output.STAKE {!!} , tt) , tt) - Computational-B .computeProof s (BaseAbstract.Input.SUBMIT x) = - success ((BaseAbstract.Output.EMPTY , tt) , tt) - Computational-B .computeProof s BaseAbstract.Input.FTCH-LDG = - success ((BaseAbstract.Output.BASE-LDG [] , tt) , tt) - Computational-B .completeness = {!!} - - Computational-FFD : Computational22 FFD._-⟦_/_⟧⇀_ String - Computational-FFD .computeProof s (FFDAbstract.Send x x₁) = success ((FFDAbstract.SendRes , tt) , tt) - Computational-FFD .computeProof s FFDAbstract.Fetch = success ((FFDAbstract.FetchRes [] , tt) , tt) - Computational-FFD .completeness = {!!} - comp = Computational--⟦/⟧⇀ ⦃ Computational-B ⦄ ⦃ Computational-FFD ⦄ initLeiosState : VTy → StakeDistr → B.State → LeiosState From 0137fe4642aa1eee74e9674ba33aaeb7a5c3a78c Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Tue, 4 Mar 2025 12:32:46 +0100 Subject: [PATCH 06/22] LeiosState as module parameter --- formal-spec/Leios/Trace/Verifier.agda | 187 ++++++++++++-------------- 1 file changed, 89 insertions(+), 98 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index fe4a1be..9240851 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -7,110 +7,101 @@ open import Leios.Short ⋯ renaming (isVoteCertified to isVoteCertified') open B hiding (_-⟦_/_⟧⇀_) open FFD hiding (_-⟦_/_⟧⇀_) -IB-Role? : ∀ {s π ffds'} → - let open LeiosState s renaming (FFDState to ffds) - b = GenFFD.ibBody (record { txs = ToPropose }) - h = GenFFD.ibHeader (mkIBHeader slot id π sk-IB ToPropose) - in - { _ : auto∶ needsUpkeep IB-Role } - { _ : auto∶ canProduceIB slot sk-IB (stake s) π } - { _ : auto∶ ffds FFD.-⟦ FFD.Send h (just b) / FFD.SendRes ⟧⇀ ffds' } → - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } IB-Role -IB-Role? {_} {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) +module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; BaseState to bs)) where -{- -No-IB-Role? : ∀ {s} → let open LeiosState s - in - { _ : auto∶ needsUpkeep IB-Role } - { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } → - ───────────────────────────────────────────── - s ↝ addUpkeep s IB-Role -No-IB-Role? {_} {p} = No-IB-Role (toWitness p) (toWitness q) --} + IB-Role? : ∀ {π ffds'} → + let b = GenFFD.ibBody (record { txs = ToPropose }) + h = GenFFD.ibHeader (mkIBHeader slot id π sk-IB ToPropose) + in + { _ : auto∶ needsUpkeep IB-Role } + { _ : auto∶ canProduceIB slot sk-IB (stake s) π } + { _ : auto∶ ffds FFD.-⟦ FFD.Send h (just b) / FFD.SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } IB-Role + IB-Role? {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) -EB-Role? : ∀ {s π ffds'} → - let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs - h = mkEB slot id π sk-EB LI [] - in - { _ : auto∶ needsUpkeep EB-Role } - { _ : auto∶ canProduceEB slot sk-EB (stake s) π } - { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds' } → - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } EB-Role -EB-Role? {_} {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) + {- + No-IB-Role? : + { _ : auto∶ needsUpkeep IB-Role } + { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } → + ───────────────────────────────────────────── + s ↝ addUpkeep s IB-Role + No-IB-Role? {p} {q} = No-IB-Role (toWitness p) (toWitness q) + -} -{- -No-EB-Role? : ∀ {s} → let open LeiosState s - in - { _ : auto∶ needsUpkeep EB-Role } - { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-EB (stake s) π } → - ───────────────────────────────────────────── - s ↝ addUpkeep s EB-Role -No-EB-Role? {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) --} + EB-Role? : ∀ {π ffds'} → + let LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id π sk-EB LI [] + in + { _ : auto∶ needsUpkeep EB-Role } + { _ : auto∶ canProduceEB slot sk-EB (stake s) π } + { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } EB-Role + EB-Role? {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) -V-Role? : ∀ {s ffds'} → - let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - in - { _ : auto∶ needsUpkeep V-Role } - { _ : auto∶ canProduceV slot sk-V (stake s) } - { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } → - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } V-Role -V-Role? {_} {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) + {- + No-EB-Role? : + { _ : auto∶ needsUpkeep EB-Role } + { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-EB (stake s) π } → + ───────────────────────────────────────────── + s ↝ addUpkeep s EB-Role + No-EB-Role? {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) + -} -No-V-Role? : ∀ {s} → let open LeiosState s in - { _ : auto∶ needsUpkeep V-Role } - { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } → - ───────────────────────────────────────────── - s ↝ addUpkeep s V-Role -No-V-Role? {_} {p} {q} = No-V-Role (toWitness p) (toWitness q) + V-Role? : ∀ {ffds'} → + let EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + in + { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ canProduceV slot sk-V (stake s) } + { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } V-Role + V-Role? {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) -{- -Init? : ∀ {ks pks ks' SD bs' V} → - { _ : auto∶ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' } - { _ : initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' } → - ──────────────────────────────────────────────────────────────── - nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' -Init? = ? --} + No-V-Role? : + { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } → + ───────────────────────────────────────────── + s ↝ addUpkeep s V-Role + No-V-Role? {p} {q} = No-V-Role (toWitness p) (toWitness q) -Base₂a? : ∀ {s eb bs'} → - let open LeiosState s renaming (BaseState to bs) - in - { _ : auto∶ needsUpkeep Base } - { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } - { _ : auto∶ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' } → - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base -Base₂a? {_} {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) (toWitness r) + {- + Init? : ∀ {ks pks ks' SD bs' V} → + { _ : auto∶ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' } + { _ : initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' } → + ──────────────────────────────────────────────────────────────── + nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' + Init? = ? + -} -Base₂b? : ∀ {s bs'} → - let open LeiosState s renaming (BaseState to bs) - in - { _ : auto∶ needsUpkeep Base } - { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } - { _ : auto∶ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' } → - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base -Base₂b? {_} {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) (toWitness r) + Base₂a? : ∀ {eb bs'} → + { _ : auto∶ needsUpkeep Base } + { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base + Base₂a? {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) (toWitness r) -Slot? : ∀ {s rbs bs' msgs ffds'} → - let open LeiosState s renaming (FFDState to ffds; BaseState to bs) - in - { _ : auto∶ Upkeep ≡ᵉ allUpkeep } - { _ : auto∶ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' } - { _ : auto∶ ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds' } → - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ record s - { FFDState = ffds' - ; BaseState = bs' - ; Ledger = constructLedger rbs - ; slot = suc slot - ; Upkeep = ∅ - } ↑ L.filter GenFFD.isValid? msgs -Slot? {_} {_} {_} {_} {_} {p} {q} {r} = Slot (toWitness p) (toWitness q) (toWitness r) + Base₂b? : ∀ {bs'} → + { _ : auto∶ needsUpkeep Base } + { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base + Base₂b? {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) (toWitness r) + + Slot? : ∀ {rbs bs' msgs ffds'} → + { _ : auto∶ Upkeep ≡ᵉ allUpkeep } + { _ : auto∶ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' } + { _ : auto∶ ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ record s + { FFDState = ffds' + ; BaseState = bs' + ; Ledger = constructLedger rbs + ; slot = suc slot + ; Upkeep = ∅ + } ↑ L.filter GenFFD.isValid? msgs + Slot? {_} {_} {_} {_} {p} {q} {r} = Slot (toWitness p) (toWitness q) (toWitness r) From 742f7c6fd232be14026e001f0677f425bd559084 Mon Sep 17 00:00:00 2001 From: Yves Date: Fri, 14 Mar 2025 12:11:09 +0100 Subject: [PATCH 07/22] Moved trace-verifier from `ouroboros-leios` repo --- formal-spec/Leios/Defaults.agda | 5 +- formal-spec/Leios/Trace/TraceVerifier.agda | 335 +++++++++++++++++++++ 2 files changed, 336 insertions(+), 4 deletions(-) create mode 100644 formal-spec/Leios/Trace/TraceVerifier.agda diff --git a/formal-spec/Leios/Defaults.agda b/formal-spec/Leios/Defaults.agda index 00abe9d..9506808 100644 --- a/formal-spec/Leios/Defaults.agda +++ b/formal-spec/Leios/Defaults.agda @@ -86,15 +86,12 @@ d-Base = ; V-chkCerts = λ _ _ → true } - --- data SimpleBase : ⊤ → BaseAbstract.Input d-Base → BaseAbstract.Output d-Base → ⊤ → Type where - d-BaseFunctionality : BaseAbstract.Functionality d-Base d-BaseFunctionality = record { State = ⊤ ; _-⟦_/_⟧⇀_ = λ _ _ _ _ → ⊤ --- ; Dec-_-⟦_/_⟧⇀_ = ⁇ (yes tt) + ; Dec-_-⟦_/_⟧⇀_ = ⁇ (yes tt) ; SUBMIT-total = tt , tt } diff --git a/formal-spec/Leios/Trace/TraceVerifier.agda b/formal-spec/Leios/Trace/TraceVerifier.agda new file mode 100644 index 0000000..d7e3c34 --- /dev/null +++ b/formal-spec/Leios/Trace/TraceVerifier.agda @@ -0,0 +1,335 @@ +open import Leios.Prelude hiding (id) + +module Leios.Trace.TraceVerifier where + +open import Leios.SpecStructure using (SpecStructure) +open import Leios.Defaults 2 fzero using (st; sd; LeiosState; initLeiosState; isb; hpe; hhs; htx; SendIB; FFDState; Dec-SimpleFFD; send-total; fetch-total) +open import Leios.Trace.Verifier st +open SpecStructure st hiding (Hashable-IBHeader; Hashable-EndorserBlock; isVoteCertified) + +open import Leios.Short st hiding (LeiosState; initLeiosState) +open import Prelude.Closures _↝_ +open GenFFD + +data Action : Type where + IB-Role-Action EB-Role-Action V-Role-Action : Action + No-IB-Role-Action No-EB-Role-Action No-V-Role-Action : Action + Ftch-Action Slot-Action : Action + -- Base₁-Action Base₂a-Action Base₂b-Action : Action + +Actions = List (Action × LeiosInput) + +private variable + s s′ : LeiosState + α : Action + +data ValidAction : Action → LeiosState → LeiosInput → Type where + + IB-Role : let open LeiosState s renaming (FFDState to ffds) + b = record { txs = ToPropose } + h = mkIBHeader slot id tt sk-IB ToPropose + ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)}) + in .(needsUpkeep IB-Role) → + .(canProduceIB slot sk-IB (stake s) tt) → + .(ffds FFD.-⟦ FFD.Send (ibHeader h) (just (ibBody b)) / FFD.SendRes ⟧⇀ ffds') → + ValidAction IB-Role-Action s SLOT + + EB-Role : let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id tt sk-EB LI [] + ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing}) + in .(needsUpkeep EB-Role) → + .(canProduceEB slot sk-EB (stake s) tt) → + .(ffds FFD.-⟦ FFD.Send (ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds') → + ValidAction EB-Role-Action s SLOT + + V-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) + in .(needsUpkeep V-Role) → + .(canProduceV slot sk-V (stake s)) → + .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → + ValidAction V-Role-Action s SLOT + + No-IB-Role : let open LeiosState s + in needsUpkeep IB-Role → + (∀ π → ¬ canProduceIB slot sk-IB (stake s) π) → + ValidAction No-IB-Role-Action s SLOT + + No-EB-Role : let open LeiosState s + in needsUpkeep EB-Role → + (∀ π → ¬ canProduceEB slot sk-EB (stake s) π) → + ValidAction No-EB-Role-Action s SLOT + + No-V-Role : let open LeiosState s + in needsUpkeep V-Role → + (¬ canProduceV slot sk-V (stake s)) → + ValidAction No-V-Role-Action s SLOT + + Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) + (msgs , (ffds' , _)) = fetch-total {ffds} + in .(Upkeep ≡ᵉ allUpkeep) → + .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) → -- TODO: rbs ≠ [] + .(ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds') → + ValidAction Slot-Action s SLOT + + Ftch : ValidAction Ftch-Action s FTCH-LDG + +{- + Base₁ : ∀ {txs} → ValidAction Base₁-Action s (SUBMIT (inj₂ txs)) + + Base₂a : ∀ {eb} → let open LeiosState s renaming (BaseState to bs) + in .(needsUpkeep Base) → + .(eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → + .(bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ tt) → + ValidAction Base₂a-Action s SLOT + + Base₂b : let open LeiosState s renaming (BaseState to bs) + in .(needsUpkeep Base) → + .([] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → + .(bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ tt) → + ValidAction Base₂b-Action s SLOT +-} + +private variable + i : LeiosInput + o : LeiosOutput + +⟦_⟧ : ValidAction α s i → LeiosState × LeiosOutput +⟦ IB-Role {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds) + b = record { txs = ToPropose } + h = mkIBHeader slot id tt sk-IB ToPropose + ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)}) + in addUpkeep record s { FFDState = ffds' } IB-Role , EMPTY +⟦ EB-Role {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id tt sk-EB LI [] + ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing}) + in addUpkeep record s { FFDState = ffds' } EB-Role , EMPTY +⟦ V-Role {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) + in addUpkeep record s { FFDState = ffds' } V-Role , EMPTY +⟦ No-IB-Role {s} x x₁ ⟧ = addUpkeep s IB-Role , EMPTY +⟦ No-EB-Role {s} x x₁ ⟧ = addUpkeep s EB-Role , EMPTY +⟦ No-V-Role {s} x x₁ ⟧ = addUpkeep s V-Role , EMPTY +⟦ Slot {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds; BaseState to bs) + (msgs , (ffds' , _)) = fetch-total {ffds} + in + (record s + { FFDState = ffds' + ; BaseState = tt -- bs' + ; Ledger = constructLedger [] -- rbs + ; slot = suc slot + ; Upkeep = ∅ + } ↑ L.filter isValid? msgs + , EMPTY) +⟦ Ftch {s} ⟧ = s , FTCH-LDG (LeiosState.Ledger s) +-- ⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY +-- ⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY +-- ⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY + +instance + Dec-ValidAction : ValidAction ⁇³ + Dec-ValidAction {IB-Role-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (IB-Role x y z) + ... | no ¬p | _ | _ = no λ where (IB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (IB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (IB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {IB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {IB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {IB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {EB-Role-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (EB-Role x y z) + ... | no ¬p | _ | _ = no λ where (EB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (EB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (EB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {EB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {V-Role-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (V-Role x y z) + ... | no ¬p | _ | _ = no λ where (V-Role p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (V-Role _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (V-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {V-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {V-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {V-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {No-IB-Role-Action} {s} {SLOT} .dec + with dec | dec + ... | yes p | yes q = yes (No-IB-Role p q) + ... | no ¬p | _ = no λ where (No-IB-Role p _) → ⊥-elim (¬p p) + ... | _ | no ¬q = no λ where (No-IB-Role _ q) → ⊥-elim (¬q q) + Dec-ValidAction {No-IB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {No-IB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {No-IB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {No-EB-Role-Action} {s} {SLOT} .dec + with dec | dec + ... | yes p | yes q = yes (No-EB-Role p q) + ... | no ¬p | _ = no λ where (No-EB-Role p _) → ⊥-elim (¬p p) + ... | _ | no ¬q = no λ where (No-EB-Role _ q) → ⊥-elim (¬q q) + Dec-ValidAction {No-EB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {No-EB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {No-EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {No-V-Role-Action} {s} {SLOT} .dec + with dec | dec + ... | yes p | yes q = yes (No-V-Role p q) + ... | no ¬p | _ = no λ where (No-V-Role p _) → ⊥-elim (¬p p) + ... | _ | no ¬q = no λ where (No-V-Role _ q) → ⊥-elim (¬q q) + Dec-ValidAction {No-V-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {No-V-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {No-V-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Slot-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (Slot x y z) + ... | no ¬p | _ | _ = no λ where (Slot p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Slot _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (Slot _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {Slot-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Slot-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Slot-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Ftch-Action} {s} {FTCH-LDG} .dec = yes Ftch + Dec-ValidAction {Ftch-Action} {s} {SLOT} .dec = no λ () + Dec-ValidAction {Ftch-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Ftch-Action} {s} {SUBMIT _} .dec = no λ () +{- + Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₁ ebs)} .dec = no λ () + Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₂ txs)} .dec = yes (Base₁ {s} {txs}) + Dec-ValidAction {Base₁-Action} {s} {SLOT} .dec = no λ () + Dec-ValidAction {Base₁-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Base₁-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Base₂a-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (Base₂a x y z) + ... | no ¬p | _ | _ = no λ where (Base₂a p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Base₂a _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (Base₂a _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {Base₂a-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Base₂a-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Base₂a-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Base₂b-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (Base₂b x y z) + ... | no ¬p | _ | _ = no λ where (Base₂b p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Base₂b _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (Base₂b _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {Base₂b-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Base₂b-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Base₂b-Action} {s} {INIT _} .dec = no λ () +-} + +mutual + data ValidTrace : Actions → Type where + [] : + ───────────── + ValidTrace [] + + _/_∷_⊣_ : ∀ α i {αs} → + ∀ (tr : ValidTrace αs) → + ∙ ValidAction α (proj₁ ⟦ tr ⟧∗) i + ─────────────────── + ValidTrace ((α , i) ∷ αs) + + ⟦_⟧∗ : ∀ {αs : Actions} → ValidTrace αs → LeiosState × LeiosOutput + ⟦_⟧∗ [] = initLeiosState tt sd tt , EMPTY + ⟦_⟧∗ (_ / _ ∷ _ ⊣ vα) = ⟦ vα ⟧ + +Irr-ValidAction : Irrelevant (ValidAction α s i) +Irr-ValidAction (IB-Role x x₁ x₂) (IB-Role x₃ x₄ x₅) = refl +Irr-ValidAction (EB-Role x x₁ x₂) (EB-Role x₃ x₄ x₅) = refl +Irr-ValidAction (V-Role x x₁ x₂) (V-Role x₃ x₄ x₅) = refl +Irr-ValidAction (No-IB-Role x x₁) (No-IB-Role x₂ x₃) = refl +Irr-ValidAction (No-EB-Role x x₁) (No-EB-Role x₂ x₃) = refl +Irr-ValidAction (No-V-Role _ _) (No-V-Role _ _) = refl +Irr-ValidAction (Slot x x₁ x₂) (Slot x₃ x₄ x₅) = refl +Irr-ValidAction Ftch Ftch = refl +-- Irr-ValidAction Base₁ Base₁ = refl +-- Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = {!refl!} +-- Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl + +Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs) +Irr-ValidTrace [] [] = refl +Irr-ValidTrace (α / i ∷ vαs ⊣ vα) (.α / .i ∷ vαs′ ⊣ vα′) + rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidAction vα vα′ + = refl + +instance + Dec-ValidTrace : ValidTrace ⁇¹ + Dec-ValidTrace {tr} .dec with tr + ... | [] = yes [] + ... | (α , i) ∷ αs + with ¿ ValidTrace αs ¿ + ... | no ¬vαs = no λ where (_ / _ ∷ vαs ⊣ _) → ¬vαs vαs + ... | yes vαs + with ¿ ValidAction α (proj₁ ⟦ vαs ⟧∗) i ¿ + ... | no ¬vα = no λ where + (_ / _ ∷ tr ⊣ vα) → ¬vα + $ subst (λ x → ValidAction α x i) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vα + ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα + +{- +getLabel : just s -⟦ i / o ⟧⇀ s′ → Action +getLabel (Slot _ _ _) = Slot-Action +getLabel Ftch = Ftch-Action +getLabel Base₁ = Base₁-Action +getLabel (Base₂a _ _ _) = Base₂a-Action +getLabel (Base₂b _ _ _) = Base₂b-Action +getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action +getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action +getLabel (Roles (V-Role _ _ _)) = V-Role-Action +getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action +getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action +getLabel (Roles (No-V-Role _ _)) = No-V-Role-Action +-} + +ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′ +ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound Ftch = Ftch +-- ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} +-- ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +-- ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (IB-Role {s} x x₁ x₂) = Roles (IB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (EB-Role {s} x x₁ x₂) = Roles (EB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (V-Role {s} x x₁ x₂) = Roles (V-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (No-IB-Role {s} x x₁) = Roles (No-IB-Role {s} x x₁) +ValidAction-sound (No-EB-Role {s} x x₁) = Roles (No-EB-Role {s} x x₁) +ValidAction-sound (No-V-Role {s} x x₁) = Roles (No-V-Role {s} x x₁) + +{- +ValidAction-complete : (st : just s -⟦ i / o ⟧⇀ s′) → ValidAction (getLabel st) s i +ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ x₂)) = + let open LeiosState s renaming (FFDState to ffds) + b = record { txs = ToPropose } + h = mkIBHeader slot id tt sk-IB ToPropose + pr = proj₂ (send-total {ffds} {ibHeader h} {just (ibBody b)}) + in IB-Role {s} x x₁ pr +ValidAction-complete {s} (Roles (EB-Role x x₁ x₂)) = + let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id tt sk-EB LI [] + pr = proj₂ (send-total {ffds} {ebHeader h} {nothing}) + in EB-Role {s} x x₁ pr +ValidAction-complete {s} (Roles (V-Role x x₁ x₂)) = + let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + pr = proj₂ (send-total {ffds} {vHeader votes} {nothing}) + in V-Role {s} x x₁ pr +ValidAction-complete {s} (Roles (No-IB-Role x x₁)) = No-IB-Role {s} x x₁ +ValidAction-complete {s} (Roles (No-EB-Role x x₁)) = No-EB-Role {s} x x₁ +ValidAction-complete {s} (Roles (No-V-Role x x₁)) = No-V-Role {s} x x₁ +ValidAction-complete {s} Ftch = Ftch {s} +-- ValidAction-complete {s} Base₁ = Base₁ {s} +-- ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂ +-- ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂ +ValidAction-complete {s} (Slot x x₁ x₂) = Slot {s} x x₁ {!!} +-} From 1bea2eaedf3cc38448a11819f3e2a7ab75b24735 Mon Sep 17 00:00:00 2001 From: Yves Date: Fri, 14 Mar 2025 12:15:27 +0100 Subject: [PATCH 08/22] Leios trace-verifier --- formal-spec/Everything.agda | 1 + formal-spec/Leios/Trace/Decidable.agda | 107 +++++ formal-spec/Leios/Trace/TraceVerifier.agda | 335 ---------------- formal-spec/Leios/Trace/Verifier.agda | 435 ++++++++++++++++----- 4 files changed, 439 insertions(+), 439 deletions(-) create mode 100644 formal-spec/Leios/Trace/Decidable.agda delete mode 100644 formal-spec/Leios/Trace/TraceVerifier.agda diff --git a/formal-spec/Everything.agda b/formal-spec/Everything.agda index 888e466..4420ba6 100644 --- a/formal-spec/Everything.agda +++ b/formal-spec/Everything.agda @@ -22,6 +22,7 @@ open import Leios.Simplified.Deterministic 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.UniformShort open import Leios.Voting diff --git a/formal-spec/Leios/Trace/Decidable.agda b/formal-spec/Leios/Trace/Decidable.agda new file mode 100644 index 0000000..6e50c2f --- /dev/null +++ b/formal-spec/Leios/Trace/Decidable.agda @@ -0,0 +1,107 @@ +open import Leios.Prelude hiding (id) +open import Leios.SpecStructure using (SpecStructure) + +module Leios.Trace.Decidable (⋯ : SpecStructure 1) (let open SpecStructure ⋯) where + +open import Leios.Short ⋯ renaming (isVoteCertified to isVoteCertified') +open B hiding (_-⟦_/_⟧⇀_) +open FFD hiding (_-⟦_/_⟧⇀_) + +module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; BaseState to bs)) where + + IB-Role? : ∀ {π ffds'} → + let b = GenFFD.ibBody (record { txs = ToPropose }) + h = GenFFD.ibHeader (mkIBHeader slot id π sk-IB ToPropose) + in + { _ : auto∶ needsUpkeep IB-Role } + { _ : auto∶ canProduceIB slot sk-IB (stake s) π } + { _ : auto∶ ffds FFD.-⟦ FFD.Send h (just b) / FFD.SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } IB-Role + IB-Role? {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) + + {- + No-IB-Role? : + { _ : auto∶ needsUpkeep IB-Role } + { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } → + ───────────────────────────────────────────── + s ↝ addUpkeep s IB-Role + No-IB-Role? {p} {q} = No-IB-Role (toWitness p) (toWitness q) + -} + + EB-Role? : ∀ {π ffds'} → + let LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id π sk-EB LI [] + in + { _ : auto∶ needsUpkeep EB-Role } + { _ : auto∶ canProduceEB slot sk-EB (stake s) π } + { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } EB-Role + EB-Role? {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) + + {- + No-EB-Role? : + { _ : auto∶ needsUpkeep EB-Role } + { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-EB (stake s) π } → + ───────────────────────────────────────────── + s ↝ addUpkeep s EB-Role + No-EB-Role? {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) + -} + + V-Role? : ∀ {ffds'} → + let EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + in + { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ canProduceV slot sk-V (stake s) } + { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } → + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } V-Role + V-Role? {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) + + No-V-Role? : + { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } → + ───────────────────────────────────────────── + s ↝ addUpkeep s V-Role + No-V-Role? {p} {q} = No-V-Role (toWitness p) (toWitness q) + + {- + Init? : ∀ {ks pks ks' SD bs' V} → + { _ : auto∶ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' } + { _ : initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' } → + ──────────────────────────────────────────────────────────────── + nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' + Init? = ? + -} + + Base₂a? : ∀ {eb bs'} → + { _ : auto∶ needsUpkeep Base } + { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base + Base₂a? {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) (toWitness r) + + Base₂b? : ∀ {bs'} → + { _ : auto∶ needsUpkeep Base } + { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } + { _ : auto∶ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base + Base₂b? {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) (toWitness r) + + Slot? : ∀ {rbs bs' msgs ffds'} → + { _ : auto∶ Upkeep ≡ᵉ allUpkeep } + { _ : auto∶ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' } + { _ : auto∶ ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds' } → + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ record s + { FFDState = ffds' + ; BaseState = bs' + ; Ledger = constructLedger rbs + ; slot = suc slot + ; Upkeep = ∅ + } ↑ L.filter GenFFD.isValid? msgs + Slot? {_} {_} {_} {_} {p} {q} {r} = Slot (toWitness p) (toWitness q) (toWitness r) diff --git a/formal-spec/Leios/Trace/TraceVerifier.agda b/formal-spec/Leios/Trace/TraceVerifier.agda deleted file mode 100644 index d7e3c34..0000000 --- a/formal-spec/Leios/Trace/TraceVerifier.agda +++ /dev/null @@ -1,335 +0,0 @@ -open import Leios.Prelude hiding (id) - -module Leios.Trace.TraceVerifier where - -open import Leios.SpecStructure using (SpecStructure) -open import Leios.Defaults 2 fzero using (st; sd; LeiosState; initLeiosState; isb; hpe; hhs; htx; SendIB; FFDState; Dec-SimpleFFD; send-total; fetch-total) -open import Leios.Trace.Verifier st -open SpecStructure st hiding (Hashable-IBHeader; Hashable-EndorserBlock; isVoteCertified) - -open import Leios.Short st hiding (LeiosState; initLeiosState) -open import Prelude.Closures _↝_ -open GenFFD - -data Action : Type where - IB-Role-Action EB-Role-Action V-Role-Action : Action - No-IB-Role-Action No-EB-Role-Action No-V-Role-Action : Action - Ftch-Action Slot-Action : Action - -- Base₁-Action Base₂a-Action Base₂b-Action : Action - -Actions = List (Action × LeiosInput) - -private variable - s s′ : LeiosState - α : Action - -data ValidAction : Action → LeiosState → LeiosInput → Type where - - IB-Role : let open LeiosState s renaming (FFDState to ffds) - b = record { txs = ToPropose } - h = mkIBHeader slot id tt sk-IB ToPropose - ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)}) - in .(needsUpkeep IB-Role) → - .(canProduceIB slot sk-IB (stake s) tt) → - .(ffds FFD.-⟦ FFD.Send (ibHeader h) (just (ibBody b)) / FFD.SendRes ⟧⇀ ffds') → - ValidAction IB-Role-Action s SLOT - - EB-Role : let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs - h = mkEB slot id tt sk-EB LI [] - ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing}) - in .(needsUpkeep EB-Role) → - .(canProduceEB slot sk-EB (stake s) tt) → - .(ffds FFD.-⟦ FFD.Send (ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds') → - ValidAction EB-Role-Action s SLOT - - V-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) - in .(needsUpkeep V-Role) → - .(canProduceV slot sk-V (stake s)) → - .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → - ValidAction V-Role-Action s SLOT - - No-IB-Role : let open LeiosState s - in needsUpkeep IB-Role → - (∀ π → ¬ canProduceIB slot sk-IB (stake s) π) → - ValidAction No-IB-Role-Action s SLOT - - No-EB-Role : let open LeiosState s - in needsUpkeep EB-Role → - (∀ π → ¬ canProduceEB slot sk-EB (stake s) π) → - ValidAction No-EB-Role-Action s SLOT - - No-V-Role : let open LeiosState s - in needsUpkeep V-Role → - (¬ canProduceV slot sk-V (stake s)) → - ValidAction No-V-Role-Action s SLOT - - Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) - (msgs , (ffds' , _)) = fetch-total {ffds} - in .(Upkeep ≡ᵉ allUpkeep) → - .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) → -- TODO: rbs ≠ [] - .(ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds') → - ValidAction Slot-Action s SLOT - - Ftch : ValidAction Ftch-Action s FTCH-LDG - -{- - Base₁ : ∀ {txs} → ValidAction Base₁-Action s (SUBMIT (inj₂ txs)) - - Base₂a : ∀ {eb} → let open LeiosState s renaming (BaseState to bs) - in .(needsUpkeep Base) → - .(eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → - .(bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ tt) → - ValidAction Base₂a-Action s SLOT - - Base₂b : let open LeiosState s renaming (BaseState to bs) - in .(needsUpkeep Base) → - .([] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → - .(bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ tt) → - ValidAction Base₂b-Action s SLOT --} - -private variable - i : LeiosInput - o : LeiosOutput - -⟦_⟧ : ValidAction α s i → LeiosState × LeiosOutput -⟦ IB-Role {s} x x₁ x₂ ⟧ = - let open LeiosState s renaming (FFDState to ffds) - b = record { txs = ToPropose } - h = mkIBHeader slot id tt sk-IB ToPropose - ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)}) - in addUpkeep record s { FFDState = ffds' } IB-Role , EMPTY -⟦ EB-Role {s} x x₁ x₂ ⟧ = - let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs - h = mkEB slot id tt sk-EB LI [] - ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing}) - in addUpkeep record s { FFDState = ffds' } EB-Role , EMPTY -⟦ V-Role {s} x x₁ x₂ ⟧ = - let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) - in addUpkeep record s { FFDState = ffds' } V-Role , EMPTY -⟦ No-IB-Role {s} x x₁ ⟧ = addUpkeep s IB-Role , EMPTY -⟦ No-EB-Role {s} x x₁ ⟧ = addUpkeep s EB-Role , EMPTY -⟦ No-V-Role {s} x x₁ ⟧ = addUpkeep s V-Role , EMPTY -⟦ Slot {s} x x₁ x₂ ⟧ = - let open LeiosState s renaming (FFDState to ffds; BaseState to bs) - (msgs , (ffds' , _)) = fetch-total {ffds} - in - (record s - { FFDState = ffds' - ; BaseState = tt -- bs' - ; Ledger = constructLedger [] -- rbs - ; slot = suc slot - ; Upkeep = ∅ - } ↑ L.filter isValid? msgs - , EMPTY) -⟦ Ftch {s} ⟧ = s , FTCH-LDG (LeiosState.Ledger s) --- ⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY --- ⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY --- ⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY - -instance - Dec-ValidAction : ValidAction ⁇³ - Dec-ValidAction {IB-Role-Action} {s} {SLOT} .dec - with dec | dec | dec - ... | yes x | yes y | yes z = yes (IB-Role x y z) - ... | no ¬p | _ | _ = no λ where (IB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (IB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | _ | no ¬p = no λ where (IB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {IB-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {IB-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {IB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {EB-Role-Action} {s} {SLOT} .dec - with dec | dec | dec - ... | yes x | yes y | yes z = yes (EB-Role x y z) - ... | no ¬p | _ | _ = no λ where (EB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (EB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | _ | no ¬p = no λ where (EB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {EB-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {EB-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {V-Role-Action} {s} {SLOT} .dec - with dec | dec | dec - ... | yes x | yes y | yes z = yes (V-Role x y z) - ... | no ¬p | _ | _ = no λ where (V-Role p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (V-Role _ p _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | _ | no ¬p = no λ where (V-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {V-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {V-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {V-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {No-IB-Role-Action} {s} {SLOT} .dec - with dec | dec - ... | yes p | yes q = yes (No-IB-Role p q) - ... | no ¬p | _ = no λ where (No-IB-Role p _) → ⊥-elim (¬p p) - ... | _ | no ¬q = no λ where (No-IB-Role _ q) → ⊥-elim (¬q q) - Dec-ValidAction {No-IB-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {No-IB-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {No-IB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {No-EB-Role-Action} {s} {SLOT} .dec - with dec | dec - ... | yes p | yes q = yes (No-EB-Role p q) - ... | no ¬p | _ = no λ where (No-EB-Role p _) → ⊥-elim (¬p p) - ... | _ | no ¬q = no λ where (No-EB-Role _ q) → ⊥-elim (¬q q) - Dec-ValidAction {No-EB-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {No-EB-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {No-EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {No-V-Role-Action} {s} {SLOT} .dec - with dec | dec - ... | yes p | yes q = yes (No-V-Role p q) - ... | no ¬p | _ = no λ where (No-V-Role p _) → ⊥-elim (¬p p) - ... | _ | no ¬q = no λ where (No-V-Role _ q) → ⊥-elim (¬q q) - Dec-ValidAction {No-V-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {No-V-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {No-V-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {Slot-Action} {s} {SLOT} .dec - with dec | dec | dec - ... | yes x | yes y | yes z = yes (Slot x y z) - ... | no ¬p | _ | _ = no λ where (Slot p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (Slot _ p _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | _ | no ¬p = no λ where (Slot _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {Slot-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {Slot-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {Slot-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {Ftch-Action} {s} {FTCH-LDG} .dec = yes Ftch - Dec-ValidAction {Ftch-Action} {s} {SLOT} .dec = no λ () - Dec-ValidAction {Ftch-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {Ftch-Action} {s} {SUBMIT _} .dec = no λ () -{- - Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₁ ebs)} .dec = no λ () - Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₂ txs)} .dec = yes (Base₁ {s} {txs}) - Dec-ValidAction {Base₁-Action} {s} {SLOT} .dec = no λ () - Dec-ValidAction {Base₁-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {Base₁-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {Base₂a-Action} {s} {SLOT} .dec - with dec | dec | dec - ... | yes x | yes y | yes z = yes (Base₂a x y z) - ... | no ¬p | _ | _ = no λ where (Base₂a p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (Base₂a _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) - ... | _ | _ | no ¬p = no λ where (Base₂a _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {Base₂a-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {Base₂a-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {Base₂a-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {Base₂b-Action} {s} {SLOT} .dec - with dec | dec | dec - ... | yes x | yes y | yes z = yes (Base₂b x y z) - ... | no ¬p | _ | _ = no λ where (Base₂b p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (Base₂b _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) - ... | _ | _ | no ¬p = no λ where (Base₂b _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {Base₂b-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {Base₂b-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {Base₂b-Action} {s} {INIT _} .dec = no λ () --} - -mutual - data ValidTrace : Actions → Type where - [] : - ───────────── - ValidTrace [] - - _/_∷_⊣_ : ∀ α i {αs} → - ∀ (tr : ValidTrace αs) → - ∙ ValidAction α (proj₁ ⟦ tr ⟧∗) i - ─────────────────── - ValidTrace ((α , i) ∷ αs) - - ⟦_⟧∗ : ∀ {αs : Actions} → ValidTrace αs → LeiosState × LeiosOutput - ⟦_⟧∗ [] = initLeiosState tt sd tt , EMPTY - ⟦_⟧∗ (_ / _ ∷ _ ⊣ vα) = ⟦ vα ⟧ - -Irr-ValidAction : Irrelevant (ValidAction α s i) -Irr-ValidAction (IB-Role x x₁ x₂) (IB-Role x₃ x₄ x₅) = refl -Irr-ValidAction (EB-Role x x₁ x₂) (EB-Role x₃ x₄ x₅) = refl -Irr-ValidAction (V-Role x x₁ x₂) (V-Role x₃ x₄ x₅) = refl -Irr-ValidAction (No-IB-Role x x₁) (No-IB-Role x₂ x₃) = refl -Irr-ValidAction (No-EB-Role x x₁) (No-EB-Role x₂ x₃) = refl -Irr-ValidAction (No-V-Role _ _) (No-V-Role _ _) = refl -Irr-ValidAction (Slot x x₁ x₂) (Slot x₃ x₄ x₅) = refl -Irr-ValidAction Ftch Ftch = refl --- Irr-ValidAction Base₁ Base₁ = refl --- Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = {!refl!} --- Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl - -Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs) -Irr-ValidTrace [] [] = refl -Irr-ValidTrace (α / i ∷ vαs ⊣ vα) (.α / .i ∷ vαs′ ⊣ vα′) - rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidAction vα vα′ - = refl - -instance - Dec-ValidTrace : ValidTrace ⁇¹ - Dec-ValidTrace {tr} .dec with tr - ... | [] = yes [] - ... | (α , i) ∷ αs - with ¿ ValidTrace αs ¿ - ... | no ¬vαs = no λ where (_ / _ ∷ vαs ⊣ _) → ¬vαs vαs - ... | yes vαs - with ¿ ValidAction α (proj₁ ⟦ vαs ⟧∗) i ¿ - ... | no ¬vα = no λ where - (_ / _ ∷ tr ⊣ vα) → ¬vα - $ subst (λ x → ValidAction α x i) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vα - ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα - -{- -getLabel : just s -⟦ i / o ⟧⇀ s′ → Action -getLabel (Slot _ _ _) = Slot-Action -getLabel Ftch = Ftch-Action -getLabel Base₁ = Base₁-Action -getLabel (Base₂a _ _ _) = Base₂a-Action -getLabel (Base₂b _ _ _) = Base₂b-Action -getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action -getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action -getLabel (Roles (V-Role _ _ _)) = V-Role-Action -getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action -getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action -getLabel (Roles (No-V-Role _ _)) = No-V-Role-Action --} - -ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′ -ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) -ValidAction-sound Ftch = Ftch --- ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} --- ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) --- ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) -ValidAction-sound (IB-Role {s} x x₁ x₂) = Roles (IB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) -ValidAction-sound (EB-Role {s} x x₁ x₂) = Roles (EB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) -ValidAction-sound (V-Role {s} x x₁ x₂) = Roles (V-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) -ValidAction-sound (No-IB-Role {s} x x₁) = Roles (No-IB-Role {s} x x₁) -ValidAction-sound (No-EB-Role {s} x x₁) = Roles (No-EB-Role {s} x x₁) -ValidAction-sound (No-V-Role {s} x x₁) = Roles (No-V-Role {s} x x₁) - -{- -ValidAction-complete : (st : just s -⟦ i / o ⟧⇀ s′) → ValidAction (getLabel st) s i -ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ x₂)) = - let open LeiosState s renaming (FFDState to ffds) - b = record { txs = ToPropose } - h = mkIBHeader slot id tt sk-IB ToPropose - pr = proj₂ (send-total {ffds} {ibHeader h} {just (ibBody b)}) - in IB-Role {s} x x₁ pr -ValidAction-complete {s} (Roles (EB-Role x x₁ x₂)) = - let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs - h = mkEB slot id tt sk-EB LI [] - pr = proj₂ (send-total {ffds} {ebHeader h} {nothing}) - in EB-Role {s} x x₁ pr -ValidAction-complete {s} (Roles (V-Role x x₁ x₂)) = - let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - pr = proj₂ (send-total {ffds} {vHeader votes} {nothing}) - in V-Role {s} x x₁ pr -ValidAction-complete {s} (Roles (No-IB-Role x x₁)) = No-IB-Role {s} x x₁ -ValidAction-complete {s} (Roles (No-EB-Role x x₁)) = No-EB-Role {s} x x₁ -ValidAction-complete {s} (Roles (No-V-Role x x₁)) = No-V-Role {s} x x₁ -ValidAction-complete {s} Ftch = Ftch {s} --- ValidAction-complete {s} Base₁ = Base₁ {s} --- ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂ --- ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂ -ValidAction-complete {s} (Slot x x₁ x₂) = Slot {s} x x₁ {!!} --} diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 9240851..eedabca 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -1,107 +1,334 @@ open import Leios.Prelude hiding (id) + +module Leios.Trace.Verifier where + open import Leios.SpecStructure using (SpecStructure) +open import Leios.Defaults 2 fzero using (st; sd; LeiosState; initLeiosState; isb; hpe; hhs; htx; SendIB; FFDState; Dec-SimpleFFD; send-total; fetch-total) +open SpecStructure st hiding (Hashable-IBHeader; Hashable-EndorserBlock; isVoteCertified) + +open import Leios.Short st hiding (LeiosState; initLeiosState) +open import Prelude.Closures _↝_ +open GenFFD + +data Action : Type where + IB-Role-Action EB-Role-Action V-Role-Action : Action + No-IB-Role-Action No-EB-Role-Action No-V-Role-Action : Action + Ftch-Action Slot-Action : Action + -- Base₁-Action Base₂a-Action Base₂b-Action : Action + +Actions = List (Action × LeiosInput) + +private variable + s s′ : LeiosState + α : Action + +data ValidAction : Action → LeiosState → LeiosInput → Type where + + IB-Role : let open LeiosState s renaming (FFDState to ffds) + b = record { txs = ToPropose } + h = mkIBHeader slot id tt sk-IB ToPropose + ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)}) + in .(needsUpkeep IB-Role) → + .(canProduceIB slot sk-IB (stake s) tt) → + .(ffds FFD.-⟦ FFD.Send (ibHeader h) (just (ibBody b)) / FFD.SendRes ⟧⇀ ffds') → + ValidAction IB-Role-Action s SLOT + + EB-Role : let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id tt sk-EB LI [] + ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing}) + in .(needsUpkeep EB-Role) → + .(canProduceEB slot sk-EB (stake s) tt) → + .(ffds FFD.-⟦ FFD.Send (ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds') → + ValidAction EB-Role-Action s SLOT + + V-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) + in .(needsUpkeep V-Role) → + .(canProduceV slot sk-V (stake s)) → + .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → + ValidAction V-Role-Action s SLOT + + No-IB-Role : let open LeiosState s + in needsUpkeep IB-Role → + (∀ π → ¬ canProduceIB slot sk-IB (stake s) π) → + ValidAction No-IB-Role-Action s SLOT + + No-EB-Role : let open LeiosState s + in needsUpkeep EB-Role → + (∀ π → ¬ canProduceEB slot sk-EB (stake s) π) → + ValidAction No-EB-Role-Action s SLOT + + No-V-Role : let open LeiosState s + in needsUpkeep V-Role → + (¬ canProduceV slot sk-V (stake s)) → + ValidAction No-V-Role-Action s SLOT + + Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) + (msgs , (ffds' , _)) = fetch-total {ffds} + in .(Upkeep ≡ᵉ allUpkeep) → + .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) → -- TODO: rbs ≠ [] + .(ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds') → + ValidAction Slot-Action s SLOT + + Ftch : ValidAction Ftch-Action s FTCH-LDG + +{- + Base₁ : ∀ {txs} → ValidAction Base₁-Action s (SUBMIT (inj₂ txs)) + + Base₂a : ∀ {eb} → let open LeiosState s renaming (BaseState to bs) + in .(needsUpkeep Base) → + .(eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → + .(bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ tt) → + ValidAction Base₂a-Action s SLOT + + Base₂b : let open LeiosState s renaming (BaseState to bs) + in .(needsUpkeep Base) → + .([] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → + .(bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ tt) → + ValidAction Base₂b-Action s SLOT +-} + +private variable + i : LeiosInput + o : LeiosOutput + +⟦_⟧ : ValidAction α s i → LeiosState × LeiosOutput +⟦ IB-Role {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds) + b = record { txs = ToPropose } + h = mkIBHeader slot id tt sk-IB ToPropose + ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)}) + in addUpkeep record s { FFDState = ffds' } IB-Role , EMPTY +⟦ EB-Role {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id tt sk-EB LI [] + ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing}) + in addUpkeep record s { FFDState = ffds' } EB-Role , EMPTY +⟦ V-Role {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) + in addUpkeep record s { FFDState = ffds' } V-Role , EMPTY +⟦ No-IB-Role {s} x x₁ ⟧ = addUpkeep s IB-Role , EMPTY +⟦ No-EB-Role {s} x x₁ ⟧ = addUpkeep s EB-Role , EMPTY +⟦ No-V-Role {s} x x₁ ⟧ = addUpkeep s V-Role , EMPTY +⟦ Slot {s} x x₁ x₂ ⟧ = + let open LeiosState s renaming (FFDState to ffds; BaseState to bs) + (msgs , (ffds' , _)) = fetch-total {ffds} + in + (record s + { FFDState = ffds' + ; BaseState = tt -- bs' + ; Ledger = constructLedger [] -- rbs + ; slot = suc slot + ; Upkeep = ∅ + } ↑ L.filter isValid? msgs + , EMPTY) +⟦ Ftch {s} ⟧ = s , FTCH-LDG (LeiosState.Ledger s) +-- ⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY +-- ⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY +-- ⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY + +instance + Dec-ValidAction : ValidAction ⁇³ + Dec-ValidAction {IB-Role-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (IB-Role x y z) + ... | no ¬p | _ | _ = no λ where (IB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (IB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (IB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {IB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {IB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {IB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {EB-Role-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (EB-Role x y z) + ... | no ¬p | _ | _ = no λ where (EB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (EB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (EB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {EB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {V-Role-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (V-Role x y z) + ... | no ¬p | _ | _ = no λ where (V-Role p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (V-Role _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (V-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {V-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {V-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {V-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {No-IB-Role-Action} {s} {SLOT} .dec + with dec | dec + ... | yes p | yes q = yes (No-IB-Role p q) + ... | no ¬p | _ = no λ where (No-IB-Role p _) → ⊥-elim (¬p p) + ... | _ | no ¬q = no λ where (No-IB-Role _ q) → ⊥-elim (¬q q) + Dec-ValidAction {No-IB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {No-IB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {No-IB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {No-EB-Role-Action} {s} {SLOT} .dec + with dec | dec + ... | yes p | yes q = yes (No-EB-Role p q) + ... | no ¬p | _ = no λ where (No-EB-Role p _) → ⊥-elim (¬p p) + ... | _ | no ¬q = no λ where (No-EB-Role _ q) → ⊥-elim (¬q q) + Dec-ValidAction {No-EB-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {No-EB-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {No-EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {No-V-Role-Action} {s} {SLOT} .dec + with dec | dec + ... | yes p | yes q = yes (No-V-Role p q) + ... | no ¬p | _ = no λ where (No-V-Role p _) → ⊥-elim (¬p p) + ... | _ | no ¬q = no λ where (No-V-Role _ q) → ⊥-elim (¬q q) + Dec-ValidAction {No-V-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {No-V-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {No-V-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Slot-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (Slot x y z) + ... | no ¬p | _ | _ = no λ where (Slot p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Slot _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (Slot _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {Slot-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Slot-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Slot-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Ftch-Action} {s} {FTCH-LDG} .dec = yes Ftch + Dec-ValidAction {Ftch-Action} {s} {SLOT} .dec = no λ () + Dec-ValidAction {Ftch-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Ftch-Action} {s} {SUBMIT _} .dec = no λ () +{- + Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₁ ebs)} .dec = no λ () + Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₂ txs)} .dec = yes (Base₁ {s} {txs}) + Dec-ValidAction {Base₁-Action} {s} {SLOT} .dec = no λ () + Dec-ValidAction {Base₁-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Base₁-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Base₂a-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (Base₂a x y z) + ... | no ¬p | _ | _ = no λ where (Base₂a p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Base₂a _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (Base₂a _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {Base₂a-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Base₂a-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Base₂a-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Base₂b-Action} {s} {SLOT} .dec + with dec | dec | dec + ... | yes x | yes y | yes z = yes (Base₂b x y z) + ... | no ¬p | _ | _ = no λ where (Base₂b p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Base₂b _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (Base₂b _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {Base₂b-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Base₂b-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Base₂b-Action} {s} {INIT _} .dec = no λ () +-} + +mutual + data ValidTrace : Actions → Type where + [] : + ───────────── + ValidTrace [] + + _/_∷_⊣_ : ∀ α i {αs} → + ∀ (tr : ValidTrace αs) → + ∙ ValidAction α (proj₁ ⟦ tr ⟧∗) i + ─────────────────── + ValidTrace ((α , i) ∷ αs) + + ⟦_⟧∗ : ∀ {αs : Actions} → ValidTrace αs → LeiosState × LeiosOutput + ⟦_⟧∗ [] = initLeiosState tt sd tt , EMPTY + ⟦_⟧∗ (_ / _ ∷ _ ⊣ vα) = ⟦ vα ⟧ + +Irr-ValidAction : Irrelevant (ValidAction α s i) +Irr-ValidAction (IB-Role x x₁ x₂) (IB-Role x₃ x₄ x₅) = refl +Irr-ValidAction (EB-Role x x₁ x₂) (EB-Role x₃ x₄ x₅) = refl +Irr-ValidAction (V-Role x x₁ x₂) (V-Role x₃ x₄ x₅) = refl +Irr-ValidAction (No-IB-Role x x₁) (No-IB-Role x₂ x₃) = refl +Irr-ValidAction (No-EB-Role x x₁) (No-EB-Role x₂ x₃) = refl +Irr-ValidAction (No-V-Role _ _) (No-V-Role _ _) = refl +Irr-ValidAction (Slot x x₁ x₂) (Slot x₃ x₄ x₅) = refl +Irr-ValidAction Ftch Ftch = refl +-- Irr-ValidAction Base₁ Base₁ = refl +-- Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = {!refl!} +-- Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl + +Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs) +Irr-ValidTrace [] [] = refl +Irr-ValidTrace (α / i ∷ vαs ⊣ vα) (.α / .i ∷ vαs′ ⊣ vα′) + rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidAction vα vα′ + = refl + +instance + Dec-ValidTrace : ValidTrace ⁇¹ + Dec-ValidTrace {tr} .dec with tr + ... | [] = yes [] + ... | (α , i) ∷ αs + with ¿ ValidTrace αs ¿ + ... | no ¬vαs = no λ where (_ / _ ∷ vαs ⊣ _) → ¬vαs vαs + ... | yes vαs + with ¿ ValidAction α (proj₁ ⟦ vαs ⟧∗) i ¿ + ... | no ¬vα = no λ where + (_ / _ ∷ tr ⊣ vα) → ¬vα + $ subst (λ x → ValidAction α x i) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vα + ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα + +{- +getLabel : just s -⟦ i / o ⟧⇀ s′ → Action +getLabel (Slot _ _ _) = Slot-Action +getLabel Ftch = Ftch-Action +getLabel Base₁ = Base₁-Action +getLabel (Base₂a _ _ _) = Base₂a-Action +getLabel (Base₂b _ _ _) = Base₂b-Action +getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action +getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action +getLabel (Roles (V-Role _ _ _)) = V-Role-Action +getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action +getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action +getLabel (Roles (No-V-Role _ _)) = No-V-Role-Action +-} + +ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′ +ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound Ftch = Ftch +-- ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} +-- ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +-- ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (IB-Role {s} x x₁ x₂) = Roles (IB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (EB-Role {s} x x₁ x₂) = Roles (EB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (V-Role {s} x x₁ x₂) = Roles (V-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (No-IB-Role {s} x x₁) = Roles (No-IB-Role {s} x x₁) +ValidAction-sound (No-EB-Role {s} x x₁) = Roles (No-EB-Role {s} x x₁) +ValidAction-sound (No-V-Role {s} x x₁) = Roles (No-V-Role {s} x x₁) -module Leios.Trace.Verifier (⋯ : SpecStructure 1) (let open SpecStructure ⋯) where - -open import Leios.Short ⋯ renaming (isVoteCertified to isVoteCertified') -open B hiding (_-⟦_/_⟧⇀_) -open FFD hiding (_-⟦_/_⟧⇀_) - -module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; BaseState to bs)) where - - IB-Role? : ∀ {π ffds'} → - let b = GenFFD.ibBody (record { txs = ToPropose }) - h = GenFFD.ibHeader (mkIBHeader slot id π sk-IB ToPropose) - in - { _ : auto∶ needsUpkeep IB-Role } - { _ : auto∶ canProduceIB slot sk-IB (stake s) π } - { _ : auto∶ ffds FFD.-⟦ FFD.Send h (just b) / FFD.SendRes ⟧⇀ ffds' } → - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } IB-Role - IB-Role? {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r) - - {- - No-IB-Role? : - { _ : auto∶ needsUpkeep IB-Role } - { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } → - ───────────────────────────────────────────── - s ↝ addUpkeep s IB-Role - No-IB-Role? {p} {q} = No-IB-Role (toWitness p) (toWitness q) - -} - - EB-Role? : ∀ {π ffds'} → - let LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs - h = mkEB slot id π sk-EB LI [] - in - { _ : auto∶ needsUpkeep EB-Role } - { _ : auto∶ canProduceEB slot sk-EB (stake s) π } - { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds' } → - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } EB-Role - EB-Role? {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r) - - {- - No-EB-Role? : - { _ : auto∶ needsUpkeep EB-Role } - { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-EB (stake s) π } → - ───────────────────────────────────────────── - s ↝ addUpkeep s EB-Role - No-EB-Role? {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q) - -} - - V-Role? : ∀ {ffds'} → - let EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - in - { _ : auto∶ needsUpkeep V-Role } - { _ : auto∶ canProduceV slot sk-V (stake s) } - { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } → - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } V-Role - V-Role? {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) - - No-V-Role? : - { _ : auto∶ needsUpkeep V-Role } - { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } → - ───────────────────────────────────────────── - s ↝ addUpkeep s V-Role - No-V-Role? {p} {q} = No-V-Role (toWitness p) (toWitness q) - - {- - Init? : ∀ {ks pks ks' SD bs' V} → - { _ : auto∶ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' } - { _ : initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' } → - ──────────────────────────────────────────────────────────────── - nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' - Init? = ? - -} - - Base₂a? : ∀ {eb bs'} → - { _ : auto∶ needsUpkeep Base } - { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } - { _ : auto∶ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' } → - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base - Base₂a? {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) (toWitness r) - - Base₂b? : ∀ {bs'} → - { _ : auto∶ needsUpkeep Base } - { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs } - { _ : auto∶ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' } → - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base - Base₂b? {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) (toWitness r) - - Slot? : ∀ {rbs bs' msgs ffds'} → - { _ : auto∶ Upkeep ≡ᵉ allUpkeep } - { _ : auto∶ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' } - { _ : auto∶ ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds' } → - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ record s - { FFDState = ffds' - ; BaseState = bs' - ; Ledger = constructLedger rbs - ; slot = suc slot - ; Upkeep = ∅ - } ↑ L.filter GenFFD.isValid? msgs - Slot? {_} {_} {_} {_} {p} {q} {r} = Slot (toWitness p) (toWitness q) (toWitness r) +{- +ValidAction-complete : (st : just s -⟦ i / o ⟧⇀ s′) → ValidAction (getLabel st) s i +ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ x₂)) = + let open LeiosState s renaming (FFDState to ffds) + b = record { txs = ToPropose } + h = mkIBHeader slot id tt sk-IB ToPropose + pr = proj₂ (send-total {ffds} {ibHeader h} {just (ibBody b)}) + in IB-Role {s} x x₁ pr +ValidAction-complete {s} (Roles (EB-Role x x₁ x₂)) = + let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs + h = mkEB slot id tt sk-EB LI [] + pr = proj₂ (send-total {ffds} {ebHeader h} {nothing}) + in EB-Role {s} x x₁ pr +ValidAction-complete {s} (Roles (V-Role x x₁ x₂)) = + let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + pr = proj₂ (send-total {ffds} {vHeader votes} {nothing}) + in V-Role {s} x x₁ pr +ValidAction-complete {s} (Roles (No-IB-Role x x₁)) = No-IB-Role {s} x x₁ +ValidAction-complete {s} (Roles (No-EB-Role x x₁)) = No-EB-Role {s} x x₁ +ValidAction-complete {s} (Roles (No-V-Role x x₁)) = No-V-Role {s} x x₁ +ValidAction-complete {s} Ftch = Ftch {s} +-- ValidAction-complete {s} Base₁ = Base₁ {s} +-- ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂ +-- ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂ +ValidAction-complete {s} (Slot x x₁ x₂) = Slot {s} x x₁ {!!} +-} From 0eb0552ac8e5a1b53a20fb1b0b1f4e3ac11b31a5 Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Fri, 14 Mar 2025 15:22:03 +0100 Subject: [PATCH 09/22] Completeness for ValidAction --- formal-spec/Leios/Trace/Verifier.agda | 59 +++++++++++++-------------- 1 file changed, 28 insertions(+), 31 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index eedabca..ef8ce80 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -14,7 +14,9 @@ data Action : Type where IB-Role-Action EB-Role-Action V-Role-Action : Action No-IB-Role-Action No-EB-Role-Action No-V-Role-Action : Action Ftch-Action Slot-Action : Action - -- Base₁-Action Base₂a-Action Base₂b-Action : Action + Base₁-Action : Action + Base₂a-Action : EndorserBlock → Action + Base₂b-Action : Action Actions = List (Action × LeiosInput) @@ -69,27 +71,25 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) (msgs , (ffds' , _)) = fetch-total {ffds} in .(Upkeep ≡ᵉ allUpkeep) → - .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) → -- TODO: rbs ≠ [] + .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) → .(ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds') → ValidAction Slot-Action s SLOT Ftch : ValidAction Ftch-Action s FTCH-LDG -{- Base₁ : ∀ {txs} → ValidAction Base₁-Action s (SUBMIT (inj₂ txs)) Base₂a : ∀ {eb} → let open LeiosState s renaming (BaseState to bs) in .(needsUpkeep Base) → .(eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → .(bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ tt) → - ValidAction Base₂a-Action s SLOT + ValidAction (Base₂a-Action eb) s SLOT Base₂b : let open LeiosState s renaming (BaseState to bs) in .(needsUpkeep Base) → .([] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs) → .(bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ tt) → ValidAction Base₂b-Action s SLOT --} private variable i : LeiosInput @@ -130,9 +130,9 @@ private variable } ↑ L.filter isValid? msgs , EMPTY) ⟦ Ftch {s} ⟧ = s , FTCH-LDG (LeiosState.Ledger s) --- ⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY --- ⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY --- ⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY +⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY +⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY +⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY instance Dec-ValidAction : ValidAction ⁇³ @@ -200,31 +200,29 @@ instance Dec-ValidAction {Ftch-Action} {s} {SLOT} .dec = no λ () Dec-ValidAction {Ftch-Action} {s} {INIT _} .dec = no λ () Dec-ValidAction {Ftch-Action} {s} {SUBMIT _} .dec = no λ () -{- Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₁ ebs)} .dec = no λ () Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₂ txs)} .dec = yes (Base₁ {s} {txs}) Dec-ValidAction {Base₁-Action} {s} {SLOT} .dec = no λ () Dec-ValidAction {Base₁-Action} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {Base₁-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {Base₂a-Action} {s} {SLOT} .dec + Dec-ValidAction {Base₂a-Action eb} {s} {SLOT} .dec with dec | dec | dec ... | yes x | yes y | yes z = yes (Base₂a x y z) ... | no ¬p | _ | _ = no λ where (Base₂a p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (Base₂a _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Base₂a {s} {eb} _ p _) → ⊥-elim (¬p (recompute dec p)) ... | _ | _ | no ¬p = no λ where (Base₂a _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {Base₂a-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {Base₂a-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {Base₂a-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Base₂a-Action _} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Base₂a-Action _} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Base₂a-Action _} {s} {INIT _} .dec = no λ () Dec-ValidAction {Base₂b-Action} {s} {SLOT} .dec with dec | dec | dec ... | yes x | yes y | yes z = yes (Base₂b x y z) ... | no ¬p | _ | _ = no λ where (Base₂b p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (Base₂b _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (Base₂b _ p _) → ⊥-elim (¬p (recompute dec p)) ... | _ | _ | no ¬p = no λ where (Base₂b _ _ p) → ⊥-elim (¬p (recompute dec p)) Dec-ValidAction {Base₂b-Action} {s} {SUBMIT _} .dec = no λ () Dec-ValidAction {Base₂b-Action} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {Base₂b-Action} {s} {INIT _} .dec = no λ () --} mutual data ValidTrace : Actions → Type where @@ -251,9 +249,9 @@ Irr-ValidAction (No-EB-Role x x₁) (No-EB-Role x₂ x₃) = refl Irr-ValidAction (No-V-Role _ _) (No-V-Role _ _) = refl Irr-ValidAction (Slot x x₁ x₂) (Slot x₃ x₄ x₅) = refl Irr-ValidAction Ftch Ftch = refl --- Irr-ValidAction Base₁ Base₁ = refl --- Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = {!refl!} --- Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl +Irr-ValidAction Base₁ Base₁ = refl +Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = refl +Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs) Irr-ValidTrace [] [] = refl @@ -275,12 +273,11 @@ instance $ subst (λ x → ValidAction α x i) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vα ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα -{- getLabel : just s -⟦ i / o ⟧⇀ s′ → Action getLabel (Slot _ _ _) = Slot-Action getLabel Ftch = Ftch-Action getLabel Base₁ = Base₁-Action -getLabel (Base₂a _ _ _) = Base₂a-Action +getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb getLabel (Base₂b _ _ _) = Base₂b-Action getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action @@ -288,14 +285,13 @@ getLabel (Roles (V-Role _ _ _)) = V-Role-Action getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action getLabel (Roles (No-V-Role _ _)) = No-V-Role-Action --} ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′ ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) ValidAction-sound Ftch = Ftch --- ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} --- ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) --- ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} +ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) ValidAction-sound (IB-Role {s} x x₁ x₂) = Roles (IB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) ValidAction-sound (EB-Role {s} x x₁ x₂) = Roles (EB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) ValidAction-sound (V-Role {s} x x₁ x₂) = Roles (V-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) @@ -303,7 +299,6 @@ ValidAction-sound (No-IB-Role {s} x x₁) = Roles (No-IB-Role {s} x x₁) ValidAction-sound (No-EB-Role {s} x x₁) = Roles (No-EB-Role {s} x x₁) ValidAction-sound (No-V-Role {s} x x₁) = Roles (No-V-Role {s} x x₁) -{- ValidAction-complete : (st : just s -⟦ i / o ⟧⇀ s′) → ValidAction (getLabel st) s i ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ x₂)) = let open LeiosState s renaming (FFDState to ffds) @@ -327,8 +322,10 @@ ValidAction-complete {s} (Roles (No-IB-Role x x₁)) = No-IB-Role {s} x x₁ ValidAction-complete {s} (Roles (No-EB-Role x x₁)) = No-EB-Role {s} x x₁ ValidAction-complete {s} (Roles (No-V-Role x x₁)) = No-V-Role {s} x x₁ ValidAction-complete {s} Ftch = Ftch {s} --- ValidAction-complete {s} Base₁ = Base₁ {s} --- ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂ --- ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂ -ValidAction-complete {s} (Slot x x₁ x₂) = Slot {s} x x₁ {!!} --} +ValidAction-complete {s} Base₁ = Base₁ {s} +ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂ +ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂ +ValidAction-complete {s} (Slot {s} x x₁ x₂) = + let open LeiosState s renaming (FFDState to ffds) + (_ , (_ , pr)) = fetch-total {ffds} + in Slot {s} x x₁ pr From f6773758535b7a4c8ed1d755da6f4a860935e7b9 Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Fri, 14 Mar 2025 15:24:28 +0100 Subject: [PATCH 10/22] Updated github workflow --- .github/workflows/formal-spec.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/formal-spec.yaml b/.github/workflows/formal-spec.yaml index c222ea7..20fd843 100644 --- a/.github/workflows/formal-spec.yaml +++ b/.github/workflows/formal-spec.yaml @@ -35,7 +35,7 @@ jobs: uses: actions/checkout@v4 - name: 💾 Cache Nix store - uses: actions/cache@v3.0.8 + uses: actions/cache@v4 id: nix-cache with: path: /tmp/nixcache From 858eb198bf2b3a744dd8cc706aca23d68f8ff45b Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Fri, 14 Mar 2025 15:49:24 +0100 Subject: [PATCH 11/22] Renaming, cleanup --- formal-spec/Leios/Short.lagda.md | 4 +- formal-spec/Leios/Short/Deterministic.agda | 4 +- formal-spec/Leios/Trace/Decidable.agda | 4 +- formal-spec/Leios/Trace/Verifier.agda | 142 ++++++++++----------- 4 files changed, 77 insertions(+), 77 deletions(-) diff --git a/formal-spec/Leios/Short.lagda.md b/formal-spec/Leios/Short.lagda.md index a3daf80..ddb2f99 100644 --- a/formal-spec/Leios/Short.lagda.md +++ b/formal-spec/Leios/Short.lagda.md @@ -84,7 +84,7 @@ data _↝_ : LeiosState → LeiosState → Type where s ↝ addUpkeep record s { FFDState = ffds' } EB-Role ``` ```agda - V-Role : let open LeiosState s renaming (FFDState to ffds) + VT-Role : let open LeiosState s renaming (FFDState to ffds) EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' in @@ -110,7 +110,7 @@ data _↝_ : LeiosState → LeiosState → Type where s ↝ addUpkeep s EB-Role ``` ```agda - No-V-Role : let open LeiosState s in + No-VT-Role : let open LeiosState s in ∙ needsUpkeep V-Role ∙ ¬ canProduceV slot sk-V (stake s) ───────────────────────────────────────────── diff --git a/formal-spec/Leios/Short/Deterministic.agda b/formal-spec/Leios/Short/Deterministic.agda index 33782ab..94b4c83 100644 --- a/formal-spec/Leios/Short/Deterministic.agda +++ b/formal-spec/Leios/Short/Deterministic.agda @@ -198,8 +198,8 @@ data _-⟦V-Role⟧⇀_ : LeiosState → LeiosState → Type where s -⟦V-Role⟧⇀ addUpkeep s V-Role V-Role⇒ND : LeiosState.needsUpkeep s V-Role → s -⟦V-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s' -V-Role⇒ND u (V-Role x₁ x₂) = Roles (V-Role u x₁ x₂) -V-Role⇒ND u (No-V-Role x₁) = Roles (No-V-Role u x₁) +V-Role⇒ND u (V-Role x₁ x₂) = Roles (VT-Role u x₁ x₂) +V-Role⇒ND u (No-V-Role x₁) = Roles (No-VT-Role u x₁) V-Role-Upkeep : ∀ {u} → u ≢ V-Role → LeiosState.needsUpkeep s u → s -⟦V-Role⟧⇀ s' → LeiosState.needsUpkeep s' u diff --git a/formal-spec/Leios/Trace/Decidable.agda b/formal-spec/Leios/Trace/Decidable.agda index 6e50c2f..1b03128 100644 --- a/formal-spec/Leios/Trace/Decidable.agda +++ b/formal-spec/Leios/Trace/Decidable.agda @@ -58,14 +58,14 @@ module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; Bas { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } → ───────────────────────────────────────────────────────────────────────── s ↝ addUpkeep record s { FFDState = ffds' } V-Role - V-Role? {_} {p} {q} {r} = V-Role (toWitness p) (toWitness q) (toWitness r) + V-Role? {_} {p} {q} {r} = VT-Role (toWitness p) (toWitness q) (toWitness r) No-V-Role? : { _ : auto∶ needsUpkeep V-Role } { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } → ───────────────────────────────────────────── s ↝ addUpkeep s V-Role - No-V-Role? {p} {q} = No-V-Role (toWitness p) (toWitness q) + No-V-Role? {p} {q} = No-VT-Role (toWitness p) (toWitness q) {- Init? : ∀ {ks pks ks' SD bs' V} → diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index ef8ce80..955e94f 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -11,8 +11,8 @@ open import Prelude.Closures _↝_ open GenFFD data Action : Type where - IB-Role-Action EB-Role-Action V-Role-Action : Action - No-IB-Role-Action No-EB-Role-Action No-V-Role-Action : Action + IB-Role-Action EB-Role-Action VT-Role-Action : Action + No-IB-Role-Action No-EB-Role-Action No-VT-Role-Action : Action Ftch-Action Slot-Action : Action Base₁-Action : Action Base₂a-Action : EndorserBlock → Action @@ -44,14 +44,14 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where .(ffds FFD.-⟦ FFD.Send (ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds') → ValidAction EB-Role-Action s SLOT - V-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) - in .(needsUpkeep V-Role) → - .(canProduceV slot sk-V (stake s)) → - .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → - ValidAction V-Role-Action s SLOT + VT-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) + in .(needsUpkeep V-Role) → + .(canProduceV slot sk-V (stake s)) → + .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → + ValidAction VT-Role-Action s SLOT No-IB-Role : let open LeiosState s in needsUpkeep IB-Role → @@ -63,10 +63,10 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where (∀ π → ¬ canProduceEB slot sk-EB (stake s) π) → ValidAction No-EB-Role-Action s SLOT - No-V-Role : let open LeiosState s - in needsUpkeep V-Role → - (¬ canProduceV slot sk-V (stake s)) → - ValidAction No-V-Role-Action s SLOT + No-VT-Role : let open LeiosState s + in needsUpkeep V-Role → + (¬ canProduceV slot sk-V (stake s)) → + ValidAction No-VT-Role-Action s SLOT Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) (msgs , (ffds' , _)) = fetch-total {ffds} @@ -96,43 +96,43 @@ private variable o : LeiosOutput ⟦_⟧ : ValidAction α s i → LeiosState × LeiosOutput -⟦ IB-Role {s} x x₁ x₂ ⟧ = +⟦ IB-Role {s} _ _ _ ⟧ = let open LeiosState s renaming (FFDState to ffds) b = record { txs = ToPropose } h = mkIBHeader slot id tt sk-IB ToPropose ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)}) in addUpkeep record s { FFDState = ffds' } IB-Role , EMPTY -⟦ EB-Role {s} x x₁ x₂ ⟧ = +⟦ EB-Role {s} _ _ _ ⟧ = let open LeiosState s renaming (FFDState to ffds) LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs h = mkEB slot id tt sk-EB LI [] ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing}) in addUpkeep record s { FFDState = ffds' } EB-Role , EMPTY -⟦ V-Role {s} x x₁ x₂ ⟧ = +⟦ VT-Role {s} _ _ _ ⟧ = let open LeiosState s renaming (FFDState to ffds) EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) in addUpkeep record s { FFDState = ffds' } V-Role , EMPTY -⟦ No-IB-Role {s} x x₁ ⟧ = addUpkeep s IB-Role , EMPTY -⟦ No-EB-Role {s} x x₁ ⟧ = addUpkeep s EB-Role , EMPTY -⟦ No-V-Role {s} x x₁ ⟧ = addUpkeep s V-Role , EMPTY -⟦ Slot {s} x x₁ x₂ ⟧ = +⟦ No-IB-Role {s} _ _ ⟧ = addUpkeep s IB-Role , EMPTY +⟦ No-EB-Role {s} _ _ ⟧ = addUpkeep s EB-Role , EMPTY +⟦ No-VT-Role {s} _ _ ⟧ = addUpkeep s V-Role , EMPTY +⟦ Slot {s} _ _ _ ⟧ = let open LeiosState s renaming (FFDState to ffds; BaseState to bs) (msgs , (ffds' , _)) = fetch-total {ffds} in (record s { FFDState = ffds' - ; BaseState = tt -- bs' - ; Ledger = constructLedger [] -- rbs + ; BaseState = tt + ; Ledger = constructLedger [] ; slot = suc slot ; Upkeep = ∅ } ↑ L.filter isValid? msgs , EMPTY) ⟦ Ftch {s} ⟧ = s , FTCH-LDG (LeiosState.Ledger s) ⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY -⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY -⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY +⟦ Base₂a {s} _ _ _ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY +⟦ Base₂b {s} _ _ _ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY instance Dec-ValidAction : ValidAction ⁇³ @@ -154,15 +154,15 @@ instance Dec-ValidAction {EB-Role-Action} {s} {INIT _} .dec = no λ () Dec-ValidAction {EB-Role-Action} {s} {SUBMIT _} .dec = no λ () Dec-ValidAction {EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {V-Role-Action} {s} {SLOT} .dec + Dec-ValidAction {VT-Role-Action} {s} {SLOT} .dec with dec | dec | dec - ... | yes x | yes y | yes z = yes (V-Role x y z) - ... | no ¬p | _ | _ = no λ where (V-Role p _ _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | no ¬p | _ = no λ where (V-Role _ p _) → ⊥-elim (¬p (recompute dec p)) - ... | _ | _ | no ¬p = no λ where (V-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {V-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {V-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {V-Role-Action} {s} {FTCH-LDG} .dec = no λ () + ... | yes x | yes y | yes z = yes (VT-Role x y z) + ... | no ¬p | _ | _ = no λ where (VT-Role p _ _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | no ¬p | _ = no λ where (VT-Role _ p _) → ⊥-elim (¬p (recompute dec p)) + ... | _ | _ | no ¬p = no λ where (VT-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) + Dec-ValidAction {VT-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {VT-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {VT-Role-Action} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {No-IB-Role-Action} {s} {SLOT} .dec with dec | dec ... | yes p | yes q = yes (No-IB-Role p q) @@ -179,14 +179,14 @@ instance Dec-ValidAction {No-EB-Role-Action} {s} {INIT _} .dec = no λ () Dec-ValidAction {No-EB-Role-Action} {s} {SUBMIT _} .dec = no λ () Dec-ValidAction {No-EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {No-V-Role-Action} {s} {SLOT} .dec + Dec-ValidAction {No-VT-Role-Action} {s} {SLOT} .dec with dec | dec - ... | yes p | yes q = yes (No-V-Role p q) - ... | no ¬p | _ = no λ where (No-V-Role p _) → ⊥-elim (¬p p) - ... | _ | no ¬q = no λ where (No-V-Role _ q) → ⊥-elim (¬q q) - Dec-ValidAction {No-V-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {No-V-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {No-V-Role-Action} {s} {FTCH-LDG} .dec = no λ () + ... | yes p | yes q = yes (No-VT-Role p q) + ... | no ¬p | _ = no λ where (No-VT-Role p _) → ⊥-elim (¬p p) + ... | _ | no ¬q = no λ where (No-VT-Role _ q) → ⊥-elim (¬q q) + Dec-ValidAction {No-VT-Role-Action} {s} {INIT _} .dec = no λ () + Dec-ValidAction {No-VT-Role-Action} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {No-VT-Role-Action} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {Slot-Action} {s} {SLOT} .dec with dec | dec | dec ... | yes x | yes y | yes z = yes (Slot x y z) @@ -241,17 +241,17 @@ mutual ⟦_⟧∗ (_ / _ ∷ _ ⊣ vα) = ⟦ vα ⟧ Irr-ValidAction : Irrelevant (ValidAction α s i) -Irr-ValidAction (IB-Role x x₁ x₂) (IB-Role x₃ x₄ x₅) = refl -Irr-ValidAction (EB-Role x x₁ x₂) (EB-Role x₃ x₄ x₅) = refl -Irr-ValidAction (V-Role x x₁ x₂) (V-Role x₃ x₄ x₅) = refl -Irr-ValidAction (No-IB-Role x x₁) (No-IB-Role x₂ x₃) = refl -Irr-ValidAction (No-EB-Role x x₁) (No-EB-Role x₂ x₃) = refl -Irr-ValidAction (No-V-Role _ _) (No-V-Role _ _) = refl -Irr-ValidAction (Slot x x₁ x₂) (Slot x₃ x₄ x₅) = refl +Irr-ValidAction (IB-Role _ _ _) (IB-Role _ _ _) = refl +Irr-ValidAction (EB-Role _ _ _) (EB-Role _ _ _) = refl +Irr-ValidAction (VT-Role _ _ _) (VT-Role _ _ _) = refl +Irr-ValidAction (No-IB-Role _ _) (No-IB-Role _ _) = refl +Irr-ValidAction (No-EB-Role _ _) (No-EB-Role _ _) = refl +Irr-ValidAction (No-VT-Role _ _) (No-VT-Role _ _) = refl +Irr-ValidAction (Slot _ _ _) (Slot _ _ _) = refl Irr-ValidAction Ftch Ftch = refl Irr-ValidAction Base₁ Base₁ = refl -Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = refl -Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl +Irr-ValidAction (Base₂a _ _ _) (Base₂a _ _ _) = refl +Irr-ValidAction (Base₂b _ _ _) (Base₂b _ _ _) = refl Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs) Irr-ValidTrace [] [] = refl @@ -274,58 +274,58 @@ instance ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα getLabel : just s -⟦ i / o ⟧⇀ s′ → Action -getLabel (Slot _ _ _) = Slot-Action -getLabel Ftch = Ftch-Action -getLabel Base₁ = Base₁-Action -getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb -getLabel (Base₂b _ _ _) = Base₂b-Action -getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action -getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action -getLabel (Roles (V-Role _ _ _)) = V-Role-Action +getLabel (Slot _ _ _) = Slot-Action +getLabel Ftch = Ftch-Action +getLabel Base₁ = Base₁-Action +getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb +getLabel (Base₂b _ _ _) = Base₂b-Action +getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action +getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action +getLabel (Roles (VT-Role _ _ _)) = VT-Role-Action getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action -getLabel (Roles (No-V-Role _ _)) = No-V-Role-Action +getLabel (Roles (No-VT-Role _ _)) = No-VT-Role-Action ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′ -ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) -ValidAction-sound Ftch = Ftch -ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} -ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) -ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound Ftch = Ftch +ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} +ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) ValidAction-sound (IB-Role {s} x x₁ x₂) = Roles (IB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) ValidAction-sound (EB-Role {s} x x₁ x₂) = Roles (EB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) -ValidAction-sound (V-Role {s} x x₁ x₂) = Roles (V-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (VT-Role {s} x x₁ x₂) = Roles (VT-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) ValidAction-sound (No-IB-Role {s} x x₁) = Roles (No-IB-Role {s} x x₁) ValidAction-sound (No-EB-Role {s} x x₁) = Roles (No-EB-Role {s} x x₁) -ValidAction-sound (No-V-Role {s} x x₁) = Roles (No-V-Role {s} x x₁) +ValidAction-sound (No-VT-Role {s} x x₁) = Roles (No-VT-Role {s} x x₁) ValidAction-complete : (st : just s -⟦ i / o ⟧⇀ s′) → ValidAction (getLabel st) s i -ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ x₂)) = +ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ _)) = let open LeiosState s renaming (FFDState to ffds) b = record { txs = ToPropose } h = mkIBHeader slot id tt sk-IB ToPropose pr = proj₂ (send-total {ffds} {ibHeader h} {just (ibBody b)}) in IB-Role {s} x x₁ pr -ValidAction-complete {s} (Roles (EB-Role x x₁ x₂)) = +ValidAction-complete {s} (Roles (EB-Role x x₁ _)) = let open LeiosState s renaming (FFDState to ffds) LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs h = mkEB slot id tt sk-EB LI [] pr = proj₂ (send-total {ffds} {ebHeader h} {nothing}) in EB-Role {s} x x₁ pr -ValidAction-complete {s} (Roles (V-Role x x₁ x₂)) = +ValidAction-complete {s} (Roles (VT-Role x x₁ _)) = let open LeiosState s renaming (FFDState to ffds) EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' pr = proj₂ (send-total {ffds} {vHeader votes} {nothing}) - in V-Role {s} x x₁ pr + in VT-Role {s} x x₁ pr ValidAction-complete {s} (Roles (No-IB-Role x x₁)) = No-IB-Role {s} x x₁ ValidAction-complete {s} (Roles (No-EB-Role x x₁)) = No-EB-Role {s} x x₁ -ValidAction-complete {s} (Roles (No-V-Role x x₁)) = No-V-Role {s} x x₁ +ValidAction-complete {s} (Roles (No-VT-Role x x₁)) = No-VT-Role {s} x x₁ ValidAction-complete {s} Ftch = Ftch {s} ValidAction-complete {s} Base₁ = Base₁ {s} ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂ ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂ -ValidAction-complete {s} (Slot {s} x x₁ x₂) = +ValidAction-complete {s} (Slot {s} x x₁ _) = let open LeiosState s renaming (FFDState to ffds) (_ , (_ , pr)) = fetch-total {ffds} in Slot {s} x x₁ pr From d73f582371e1585e7ddd5b8b3cb36e3f96184c35 Mon Sep 17 00:00:00 2001 From: Yves Date: Mon, 17 Mar 2025 15:41:41 +0100 Subject: [PATCH 12/22] Default stake distribution --- formal-spec/Leios/Defaults.agda | 2 +- formal-spec/Leios/Trace/Verifier.agda | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/formal-spec/Leios/Defaults.agda b/formal-spec/Leios/Defaults.agda index 9506808..7d799a7 100644 --- a/formal-spec/Leios/Defaults.agda +++ b/formal-spec/Leios/Defaults.agda @@ -289,7 +289,7 @@ maximalFin (ℕ.suc n) {a} with toℕ a N. Date: Tue, 18 Mar 2025 10:35:54 +0100 Subject: [PATCH 13/22] Renaming V-Role to VT-Role --- formal-spec/Leios/Short.lagda.md | 12 ++++----- formal-spec/Leios/Short/Deterministic.agda | 10 ++++---- formal-spec/Leios/Trace/Decidable.agda | 8 +++--- formal-spec/Leios/Trace/Verifier.agda | 30 ++++++++++++++++------ 4 files changed, 37 insertions(+), 23 deletions(-) diff --git a/formal-spec/Leios/Short.lagda.md b/formal-spec/Leios/Short.lagda.md index ddb2f99..696a9c3 100644 --- a/formal-spec/Leios/Short.lagda.md +++ b/formal-spec/Leios/Short.lagda.md @@ -27,12 +27,12 @@ module Leios.Short (⋯ : SpecStructure 1) ``` ```agda data SlotUpkeep : Type where - Base IB-Role EB-Role V-Role : SlotUpkeep + Base IB-Role EB-Role VT-Role : SlotUpkeep unquoteDecl DecEq-SlotUpkeep = derive-DecEq ((quote SlotUpkeep , DecEq-SlotUpkeep) ∷ []) allUpkeep : ℙ SlotUpkeep -allUpkeep = (((∅ ∪ ❴ IB-Role ❵) ∪ ❴ EB-Role ❵) ∪ ❴ V-Role ❵) ∪ ❴ Base ❵ +allUpkeep = fromList (IB-Role ∷ EB-Role ∷ VT-Role ∷ Base ∷ []) ``` ```agda open import Leios.Protocol (⋯) SlotUpkeep public @@ -88,11 +88,11 @@ data _↝_ : LeiosState → LeiosState → Type where EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' in - ∙ needsUpkeep V-Role + ∙ needsUpkeep VT-Role ∙ canProduceV slot sk-V (stake s) ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds' ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } V-Role + s ↝ addUpkeep record s { FFDState = ffds' } VT-Role ``` #### Negative Block/Vote production rules ```agda @@ -111,10 +111,10 @@ data _↝_ : LeiosState → LeiosState → Type where ``` ```agda No-VT-Role : let open LeiosState s in - ∙ needsUpkeep V-Role + ∙ needsUpkeep VT-Role ∙ ¬ canProduceV slot sk-V (stake s) ───────────────────────────────────────────── - s ↝ addUpkeep s V-Role + s ↝ addUpkeep s VT-Role ``` ### Uniform short-pipeline ```agda diff --git a/formal-spec/Leios/Short/Deterministic.agda b/formal-spec/Leios/Short/Deterministic.agda index 94b4c83..c5691e8 100644 --- a/formal-spec/Leios/Short/Deterministic.agda +++ b/formal-spec/Leios/Short/Deterministic.agda @@ -190,18 +190,18 @@ data _-⟦V-Role⟧⇀_ : LeiosState → LeiosState → Type where ∙ canProduceV slot sk-V (stake s) ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds' ──────────────────────────────────────────────────────────────────── - s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds' } V-Role + s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds' } VT-Role No-V-Role : let open LeiosState s in ∙ ¬ canProduceV slot sk-V (stake s) ──────────────────────────────────────── - s -⟦V-Role⟧⇀ addUpkeep s V-Role + s -⟦V-Role⟧⇀ addUpkeep s VT-Role -V-Role⇒ND : LeiosState.needsUpkeep s V-Role → s -⟦V-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s' +V-Role⇒ND : LeiosState.needsUpkeep s VT-Role → s -⟦V-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s' V-Role⇒ND u (V-Role x₁ x₂) = Roles (VT-Role u x₁ x₂) V-Role⇒ND u (No-V-Role x₁) = Roles (No-VT-Role u x₁) -V-Role-Upkeep : ∀ {u} → u ≢ V-Role → LeiosState.needsUpkeep s u → s -⟦V-Role⟧⇀ s' +V-Role-Upkeep : ∀ {u} → u ≢ VT-Role → LeiosState.needsUpkeep s u → s -⟦V-Role⟧⇀ s' → LeiosState.needsUpkeep s' u V-Role-Upkeep u≢V-Role h (V-Role _ _) u∈su = case Equivalence.from ∈-∪ u∈su of λ where (inj₁ x) → h x @@ -216,7 +216,7 @@ opaque (yes p) → -, V-Role p (proj₂ FFD.FFD-Send-total) (no ¬p) → -, No-V-Role ¬p - V-Role-total' : ∃[ ffds ] s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds } V-Role + V-Role-total' : ∃[ ffds ] s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds } VT-Role V-Role-total' {s = s} = let open LeiosState s in case Dec-canProduceV of λ where (yes p) → -, V-Role p (proj₂ FFD.FFD-Send-total) (no ¬p) → -, No-V-Role ¬p diff --git a/formal-spec/Leios/Trace/Decidable.agda b/formal-spec/Leios/Trace/Decidable.agda index 1b03128..2163a69 100644 --- a/formal-spec/Leios/Trace/Decidable.agda +++ b/formal-spec/Leios/Trace/Decidable.agda @@ -53,18 +53,18 @@ module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; Bas let EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' in - { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ needsUpkeep VT-Role } { _ : auto∶ canProduceV slot sk-V (stake s) } { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } → ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } V-Role + s ↝ addUpkeep record s { FFDState = ffds' } VT-Role V-Role? {_} {p} {q} {r} = VT-Role (toWitness p) (toWitness q) (toWitness r) No-V-Role? : - { _ : auto∶ needsUpkeep V-Role } + { _ : auto∶ needsUpkeep VT-Role } { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } → ───────────────────────────────────────────── - s ↝ addUpkeep s V-Role + s ↝ addUpkeep s VT-Role No-V-Role? {p} {q} = No-VT-Role (toWitness p) (toWitness q) {- diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index cea698d..7509987 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -48,7 +48,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) - in .(needsUpkeep V-Role) → + in .(needsUpkeep VT-Role) → .(canProduceV slot sk-V (stake s)) → .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → ValidAction VT-Role-Action s SLOT @@ -64,7 +64,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where ValidAction No-EB-Role-Action s SLOT No-VT-Role : let open LeiosState s - in needsUpkeep V-Role → + in needsUpkeep VT-Role → (¬ canProduceV slot sk-V (stake s)) → ValidAction No-VT-Role-Action s SLOT @@ -113,12 +113,12 @@ private variable EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs votes = map (vote sk-V ∘ hash) EBs' ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) - in addUpkeep record s { FFDState = ffds' } V-Role , EMPTY + in addUpkeep record s { FFDState = ffds' } VT-Role , EMPTY ⟦ No-IB-Role {s} _ _ ⟧ = addUpkeep s IB-Role , EMPTY ⟦ No-EB-Role {s} _ _ ⟧ = addUpkeep s EB-Role , EMPTY -⟦ No-VT-Role {s} _ _ ⟧ = addUpkeep s V-Role , EMPTY +⟦ No-VT-Role {s} _ _ ⟧ = addUpkeep s VT-Role , EMPTY ⟦ Slot {s} _ _ _ ⟧ = - let open LeiosState s renaming (FFDState to ffds; BaseState to bs) + let open LeiosState s renaming (FFDState to ffds) (msgs , (ffds' , _)) = fetch-total {ffds} in (record s @@ -277,10 +277,24 @@ private opaque unfolding List-Model - test : Bool - test = ¿ ValidTrace ((IB-Role-Action , SLOT) ∷ []) ¿ᵇ + test₁ : Bool + test₁ = ¿ ValidTrace ((IB-Role-Action , SLOT) ∷ []) ¿ᵇ + + _ : test₁ ≡ true + _ = refl - _ : test ≡ true + test₂ : Bool + test₂ = + let t = L.reverse $ + (IB-Role-Action , SLOT) + ∷ (EB-Role-Action , SLOT) + ∷ (VT-Role-Action , SLOT) + ∷ (Base₂b-Action , SLOT) + ∷ (Slot-Action , SLOT) + ∷ [] + in ¿ ValidTrace t ¿ᵇ + + _ : test₂ ≡ true _ = refl getLabel : just s -⟦ i / o ⟧⇀ s′ → Action From 302d5033135fd50445b005a6120ed65c9d1564d9 Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Tue, 18 Mar 2025 11:31:21 +0100 Subject: [PATCH 14/22] Add slot to SlotAction --- formal-spec/Leios/Trace/Verifier.agda | 28 +++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 7509987..7e2ff54 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -13,7 +13,8 @@ open GenFFD data Action : Type where IB-Role-Action EB-Role-Action VT-Role-Action : Action No-IB-Role-Action No-EB-Role-Action No-VT-Role-Action : Action - Ftch-Action Slot-Action : Action + Ftch-Action : Action + Slot-Action : ℕ → Action Base₁-Action : Action Base₂a-Action : EndorserBlock → Action Base₂b-Action : Action @@ -73,7 +74,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where in .(Upkeep ≡ᵉ allUpkeep) → .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) → .(ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds') → - ValidAction Slot-Action s SLOT + ValidAction (Slot-Action slot) s SLOT Ftch : ValidAction Ftch-Action s FTCH-LDG @@ -134,6 +135,9 @@ private variable ⟦ Base₂a {s} _ _ _ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY ⟦ Base₂b {s} _ _ _ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY +ValidAction→Eq-Slot : ∀ {s sl} → ValidAction (Slot-Action sl) s SLOT → sl ≡ LeiosState.slot s +ValidAction→Eq-Slot (Slot {s} _ _ _) = refl + instance Dec-ValidAction : ValidAction ⁇³ Dec-ValidAction {IB-Role-Action} {s} {SLOT} .dec @@ -187,15 +191,18 @@ instance Dec-ValidAction {No-VT-Role-Action} {s} {INIT _} .dec = no λ () Dec-ValidAction {No-VT-Role-Action} {s} {SUBMIT _} .dec = no λ () Dec-ValidAction {No-VT-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {Slot-Action} {s} {SLOT} .dec + Dec-ValidAction {Slot-Action sl} {s} {SLOT} .dec + with sl ≟ LeiosState.slot s + ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-Slot x)) + ... | yes p rewrite p with dec | dec | dec ... | yes x | yes y | yes z = yes (Slot x y z) ... | no ¬p | _ | _ = no λ where (Slot p _ _) → ⊥-elim (¬p (recompute dec p)) ... | _ | no ¬p | _ = no λ where (Slot _ p _) → ⊥-elim (¬p (recompute dec p)) ... | _ | _ | no ¬p = no λ where (Slot _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {Slot-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {Slot-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {Slot-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {Slot-Action _} {s} {INIT _} .dec = no λ () + Dec-ValidAction {Slot-Action _} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {Slot-Action _} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {Ftch-Action} {s} {FTCH-LDG} .dec = yes Ftch Dec-ValidAction {Ftch-Action} {s} {SLOT} .dec = no λ () Dec-ValidAction {Ftch-Action} {s} {INIT _} .dec = no λ () @@ -290,7 +297,12 @@ private ∷ (EB-Role-Action , SLOT) ∷ (VT-Role-Action , SLOT) ∷ (Base₂b-Action , SLOT) - ∷ (Slot-Action , SLOT) + ∷ (Slot-Action 0 , SLOT) + ∷ (IB-Role-Action , SLOT) + ∷ (EB-Role-Action , SLOT) + ∷ (VT-Role-Action , SLOT) + ∷ (Base₂b-Action , SLOT) + ∷ (Slot-Action 1 , SLOT) ∷ [] in ¿ ValidTrace t ¿ᵇ @@ -298,7 +310,7 @@ private _ = refl getLabel : just s -⟦ i / o ⟧⇀ s′ → Action -getLabel (Slot _ _ _) = Slot-Action +getLabel (Slot {s} _ _ _) = Slot-Action (LeiosState.slot s) getLabel Ftch = Ftch-Action getLabel Base₁ = Base₁-Action getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb From 80c26a528a35fb4304d4ed7ce4b0ddeb894f1115 Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Tue, 18 Mar 2025 11:46:56 +0100 Subject: [PATCH 15/22] Slot in actions --- formal-spec/Leios/Trace/Verifier.agda | 96 ++++++++++++++++----------- 1 file changed, 57 insertions(+), 39 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 7e2ff54..8ee19a0 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -11,7 +11,7 @@ open import Prelude.Closures _↝_ open GenFFD data Action : Type where - IB-Role-Action EB-Role-Action VT-Role-Action : Action + IB-Role-Action EB-Role-Action VT-Role-Action : ℕ → Action No-IB-Role-Action No-EB-Role-Action No-VT-Role-Action : Action Ftch-Action : Action Slot-Action : ℕ → Action @@ -34,7 +34,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where in .(needsUpkeep IB-Role) → .(canProduceIB slot sk-IB (stake s) tt) → .(ffds FFD.-⟦ FFD.Send (ibHeader h) (just (ibBody b)) / FFD.SendRes ⟧⇀ ffds') → - ValidAction IB-Role-Action s SLOT + ValidAction (IB-Role-Action slot) s SLOT EB-Role : let open LeiosState s renaming (FFDState to ffds) LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs @@ -43,7 +43,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where in .(needsUpkeep EB-Role) → .(canProduceEB slot sk-EB (stake s) tt) → .(ffds FFD.-⟦ FFD.Send (ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds') → - ValidAction EB-Role-Action s SLOT + ValidAction (EB-Role-Action slot) s SLOT VT-Role : let open LeiosState s renaming (FFDState to ffds) EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs @@ -52,7 +52,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where in .(needsUpkeep VT-Role) → .(canProduceV slot sk-V (stake s)) → .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → - ValidAction VT-Role-Action s SLOT + ValidAction (VT-Role-Action slot) s SLOT No-IB-Role : let open LeiosState s in needsUpkeep IB-Role → @@ -136,37 +136,55 @@ private variable ⟦ Base₂b {s} _ _ _ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY ValidAction→Eq-Slot : ∀ {s sl} → ValidAction (Slot-Action sl) s SLOT → sl ≡ LeiosState.slot s -ValidAction→Eq-Slot (Slot {s} _ _ _) = refl +ValidAction→Eq-Slot (Slot _ _ _) = refl + +ValidAction→Eq-IB : ∀ {s sl} → ValidAction (IB-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s +ValidAction→Eq-IB (IB-Role _ _ _) = refl + +ValidAction→Eq-EB : ∀ {s sl} → ValidAction (EB-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s +ValidAction→Eq-EB (EB-Role _ _ _) = refl + +ValidAction→Eq-VT : ∀ {s sl} → ValidAction (VT-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s +ValidAction→Eq-VT (VT-Role _ _ _) = refl instance Dec-ValidAction : ValidAction ⁇³ - Dec-ValidAction {IB-Role-Action} {s} {SLOT} .dec + Dec-ValidAction {IB-Role-Action sl} {s} {SLOT} .dec + with sl ≟ LeiosState.slot s + ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-IB x)) + ... | yes p rewrite p with dec | dec | dec ... | yes x | yes y | yes z = yes (IB-Role x y z) ... | no ¬p | _ | _ = no λ where (IB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) ... | _ | no ¬p | _ = no λ where (IB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) ... | _ | _ | no ¬p = no λ where (IB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {IB-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {IB-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {IB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {EB-Role-Action} {s} {SLOT} .dec + Dec-ValidAction {IB-Role-Action _} {s} {INIT _} .dec = no λ () + Dec-ValidAction {IB-Role-Action _} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {IB-Role-Action _} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {EB-Role-Action sl} {s} {SLOT} .dec + with sl ≟ LeiosState.slot s + ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-EB x)) + ... | yes p rewrite p with dec | dec | dec ... | yes x | yes y | yes z = yes (EB-Role x y z) ... | no ¬p | _ | _ = no λ where (EB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) ... | _ | no ¬p | _ = no λ where (EB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) ... | _ | _ | no ¬p = no λ where (EB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {EB-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {EB-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {EB-Role-Action} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {VT-Role-Action} {s} {SLOT} .dec + Dec-ValidAction {EB-Role-Action _} {s} {INIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action _} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action _} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {VT-Role-Action sl} {s} {SLOT} .dec + with sl ≟ LeiosState.slot s + ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-VT x)) + ... | yes p rewrite p with dec | dec | dec ... | yes x | yes y | yes z = yes (VT-Role x y z) ... | no ¬p | _ | _ = no λ where (VT-Role p _ _) → ⊥-elim (¬p (recompute dec p)) ... | _ | no ¬p | _ = no λ where (VT-Role _ p _) → ⊥-elim (¬p (recompute dec p)) ... | _ | _ | no ¬p = no λ where (VT-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {VT-Role-Action} {s} {INIT _} .dec = no λ () - Dec-ValidAction {VT-Role-Action} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {VT-Role-Action} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {VT-Role-Action _} {s} {INIT _} .dec = no λ () + Dec-ValidAction {VT-Role-Action _} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {VT-Role-Action _} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {No-IB-Role-Action} {s} {SLOT} .dec with dec | dec ... | yes p | yes q = yes (No-IB-Role p q) @@ -285,7 +303,7 @@ private unfolding List-Model test₁ : Bool - test₁ = ¿ ValidTrace ((IB-Role-Action , SLOT) ∷ []) ¿ᵇ + test₁ = ¿ ValidTrace ((IB-Role-Action 0 , SLOT) ∷ []) ¿ᵇ _ : test₁ ≡ true _ = refl @@ -293,16 +311,16 @@ private test₂ : Bool test₂ = let t = L.reverse $ - (IB-Role-Action , SLOT) - ∷ (EB-Role-Action , SLOT) - ∷ (VT-Role-Action , SLOT) - ∷ (Base₂b-Action , SLOT) - ∷ (Slot-Action 0 , SLOT) - ∷ (IB-Role-Action , SLOT) - ∷ (EB-Role-Action , SLOT) - ∷ (VT-Role-Action , SLOT) - ∷ (Base₂b-Action , SLOT) - ∷ (Slot-Action 1 , SLOT) + (IB-Role-Action 0 , SLOT) + ∷ (EB-Role-Action 0 , SLOT) + ∷ (VT-Role-Action 0 , SLOT) + ∷ (Base₂b-Action , SLOT) + ∷ (Slot-Action 0 , SLOT) + ∷ (IB-Role-Action 1 , SLOT) + ∷ (EB-Role-Action 1 , SLOT) + ∷ (VT-Role-Action 1 , SLOT) + ∷ (Base₂b-Action , SLOT) + ∷ (Slot-Action 1 , SLOT) ∷ [] in ¿ ValidTrace t ¿ᵇ @@ -310,17 +328,17 @@ private _ = refl getLabel : just s -⟦ i / o ⟧⇀ s′ → Action -getLabel (Slot {s} _ _ _) = Slot-Action (LeiosState.slot s) -getLabel Ftch = Ftch-Action -getLabel Base₁ = Base₁-Action -getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb -getLabel (Base₂b _ _ _) = Base₂b-Action -getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action -getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action -getLabel (Roles (VT-Role _ _ _)) = VT-Role-Action -getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action -getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action -getLabel (Roles (No-VT-Role _ _)) = No-VT-Role-Action +getLabel (Slot {s} _ _ _) = Slot-Action (LeiosState.slot s) +getLabel Ftch = Ftch-Action +getLabel Base₁ = Base₁-Action +getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb +getLabel (Base₂b _ _ _) = Base₂b-Action +getLabel (Roles (IB-Role {s} _ _ _)) = IB-Role-Action (LeiosState.slot s) +getLabel (Roles (EB-Role {s} _ _ _)) = EB-Role-Action (LeiosState.slot s) +getLabel (Roles (VT-Role {s} _ _ _)) = VT-Role-Action (LeiosState.slot s) +getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action +getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action +getLabel (Roles (No-VT-Role _ _)) = No-VT-Role-Action ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′ ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) From 8e77435f7c9496398a3736909721b41f94598cbb Mon Sep 17 00:00:00 2001 From: Yves Date: Tue, 18 Mar 2025 14:55:57 +0100 Subject: [PATCH 16/22] IBRefs from log --- formal-spec/Leios/Trace/Verifier.agda | 65 ++++++++++++++------------- 1 file changed, 35 insertions(+), 30 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 8ee19a0..208fd1b 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -11,7 +11,9 @@ open import Prelude.Closures _↝_ open GenFFD data Action : Type where - IB-Role-Action EB-Role-Action VT-Role-Action : ℕ → Action + IB-Role-Action : ℕ → Action + EB-Role-Action : ℕ → List String → Action + VT-Role-Action : ℕ → Action No-IB-Role-Action No-EB-Role-Action No-VT-Role-Action : Action Ftch-Action : Action Slot-Action : ℕ → Action @@ -43,16 +45,16 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where in .(needsUpkeep EB-Role) → .(canProduceEB slot sk-EB (stake s) tt) → .(ffds FFD.-⟦ FFD.Send (ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds') → - ValidAction (EB-Role-Action slot) s SLOT + ValidAction (EB-Role-Action slot LI) s SLOT - VT-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) - in .(needsUpkeep VT-Role) → - .(canProduceV slot sk-V (stake s)) → - .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → - ValidAction (VT-Role-Action slot) s SLOT + VT-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing}) + in .(needsUpkeep VT-Role) → + .(canProduceV slot sk-V (stake s)) → + .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') → + ValidAction (VT-Role-Action slot) s SLOT No-IB-Role : let open LeiosState s in needsUpkeep IB-Role → @@ -141,8 +143,10 @@ ValidAction→Eq-Slot (Slot _ _ _) = refl ValidAction→Eq-IB : ∀ {s sl} → ValidAction (IB-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s ValidAction→Eq-IB (IB-Role _ _ _) = refl -ValidAction→Eq-EB : ∀ {s sl} → ValidAction (EB-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s -ValidAction→Eq-EB (EB-Role _ _ _) = refl +ValidAction→Eq-EB : ∀ {s sl ibs} → + let open LeiosState s + in ValidAction (EB-Role-Action sl ibs) s SLOT → sl ≡ slot × ibs ≡ (map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs) +ValidAction→Eq-EB (EB-Role _ _ _) = refl , refl ValidAction→Eq-VT : ∀ {s sl} → ValidAction (VT-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s ValidAction→Eq-VT (VT-Role _ _ _) = refl @@ -161,18 +165,19 @@ instance Dec-ValidAction {IB-Role-Action _} {s} {INIT _} .dec = no λ () Dec-ValidAction {IB-Role-Action _} {s} {SUBMIT _} .dec = no λ () Dec-ValidAction {IB-Role-Action _} {s} {FTCH-LDG} .dec = no λ () - Dec-ValidAction {EB-Role-Action sl} {s} {SLOT} .dec - with sl ≟ LeiosState.slot s - ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-EB x)) - ... | yes p rewrite p + Dec-ValidAction {EB-Role-Action sl ibs} {s} {SLOT} .dec + with sl ≟ LeiosState.slot s | ibs ≟ (map getIBRef $ filter (_∈ᴮ slice L (LeiosState.slot s) 3) (LeiosState.IBs s)) + ... | no ¬p | _ = no λ x → ⊥-elim (¬p (proj₁ $ ValidAction→Eq-EB x)) + ... | _ | no ¬q = no λ x → ⊥-elim (¬q (proj₂ $ ValidAction→Eq-EB x)) + ... | yes p | yes q rewrite p rewrite q with dec | dec | dec ... | yes x | yes y | yes z = yes (EB-Role x y z) ... | no ¬p | _ | _ = no λ where (EB-Role p _ _) → ⊥-elim (¬p (recompute dec p)) ... | _ | no ¬p | _ = no λ where (EB-Role _ p _) → ⊥-elim (¬p (recompute dec p)) ... | _ | _ | no ¬p = no λ where (EB-Role _ _ p) → ⊥-elim (¬p (recompute dec p)) - Dec-ValidAction {EB-Role-Action _} {s} {INIT _} .dec = no λ () - Dec-ValidAction {EB-Role-Action _} {s} {SUBMIT _} .dec = no λ () - Dec-ValidAction {EB-Role-Action _} {s} {FTCH-LDG} .dec = no λ () + Dec-ValidAction {EB-Role-Action _ _} {s} {INIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action _ _} {s} {SUBMIT _} .dec = no λ () + Dec-ValidAction {EB-Role-Action _ _} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {VT-Role-Action sl} {s} {SLOT} .dec with sl ≟ LeiosState.slot s ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-VT x)) @@ -311,16 +316,16 @@ private test₂ : Bool test₂ = let t = L.reverse $ - (IB-Role-Action 0 , SLOT) - ∷ (EB-Role-Action 0 , SLOT) - ∷ (VT-Role-Action 0 , SLOT) - ∷ (Base₂b-Action , SLOT) - ∷ (Slot-Action 0 , SLOT) - ∷ (IB-Role-Action 1 , SLOT) - ∷ (EB-Role-Action 1 , SLOT) - ∷ (VT-Role-Action 1 , SLOT) - ∷ (Base₂b-Action , SLOT) - ∷ (Slot-Action 1 , SLOT) + (IB-Role-Action 0 , SLOT) + ∷ (EB-Role-Action 0 [] , SLOT) + ∷ (VT-Role-Action 0 , SLOT) + ∷ (Base₂b-Action , SLOT) + ∷ (Slot-Action 0 , SLOT) + ∷ (IB-Role-Action 1 , SLOT) + ∷ (EB-Role-Action 1 [] , SLOT) + ∷ (VT-Role-Action 1 , SLOT) + ∷ (Base₂b-Action , SLOT) + ∷ (Slot-Action 1 , SLOT) ∷ [] in ¿ ValidTrace t ¿ᵇ @@ -334,7 +339,7 @@ getLabel Base₁ = Base₁-Action getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb getLabel (Base₂b _ _ _) = Base₂b-Action getLabel (Roles (IB-Role {s} _ _ _)) = IB-Role-Action (LeiosState.slot s) -getLabel (Roles (EB-Role {s} _ _ _)) = EB-Role-Action (LeiosState.slot s) +getLabel (Roles (EB-Role {s} _ _ _)) = let open LeiosState s in EB-Role-Action slot (map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs) getLabel (Roles (VT-Role {s} _ _ _)) = VT-Role-Action (LeiosState.slot s) getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action From d6c480a6cf189a4386482b4fe9581b73fd8484be Mon Sep 17 00:00:00 2001 From: Yves Date: Wed, 19 Mar 2025 18:59:23 +0100 Subject: [PATCH 17/22] Updating FFD buffers --- formal-spec/Leios/Trace/Verifier.agda | 88 ++++++++++++++++++++++----- 1 file changed, 73 insertions(+), 15 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 208fd1b..83c8373 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -10,6 +10,9 @@ open import Leios.Short st hiding (LeiosState; initLeiosState) open import Prelude.Closures _↝_ open GenFFD +data FFDUpdate : Type where + IB-Recv-Update : InputBlock → FFDUpdate + data Action : Type where IB-Role-Action : ℕ → Action EB-Role-Action : ℕ → List String → Action @@ -27,6 +30,13 @@ private variable s s′ : LeiosState α : Action + +data ValidUpdate : FFDUpdate → LeiosState → Type where + + IB-Recv : ∀ {ib} → + let open LeiosState s renaming (FFDState to ffds) + in ValidUpdate (IB-Recv-Update ib) s + data ValidAction : Action → LeiosState → LeiosInput → Type where IB-Role : let open LeiosState s renaming (FFDState to ffds) @@ -254,8 +264,12 @@ instance Dec-ValidAction {Base₂b-Action} {s} {FTCH-LDG} .dec = no λ () Dec-ValidAction {Base₂b-Action} {s} {INIT _} .dec = no λ () +instance + Dec-ValidUpdate : ValidUpdate ⁇² + Dec-ValidUpdate {IB-Recv-Update _} .dec = yes IB-Recv + mutual - data ValidTrace : Actions → Type where + data ValidTrace : List ((Action × LeiosInput) ⊎ FFDUpdate) → Type where [] : ───────────── ValidTrace [] @@ -264,11 +278,21 @@ mutual ∀ (tr : ValidTrace αs) → ∙ ValidAction α (proj₁ ⟦ tr ⟧∗) i ─────────────────── - ValidTrace ((α , i) ∷ αs) + ValidTrace (inj₁ (α , i) ∷ αs) + + _∷_ : ∀ {f αs} → + ∀ (tr : ValidTrace αs) → + (vu : ValidUpdate f (proj₁ ⟦ tr ⟧∗)) → + ─────────────────── + ValidTrace (inj₂ f ∷ αs) + - ⟦_⟧∗ : ∀ {αs : Actions} → ValidTrace αs → LeiosState × LeiosOutput + ⟦_⟧∗ : ∀ {αs : List ((Action × LeiosInput) ⊎ FFDUpdate)} → ValidTrace αs → LeiosState × LeiosOutput ⟦_⟧∗ [] = initLeiosState tt sd tt , EMPTY ⟦_⟧∗ (_ / _ ∷ _ ⊣ vα) = ⟦ vα ⟧ + ⟦ _∷_ {IB-Recv-Update ib} tr vu ⟧∗ = + let (s , o) = ⟦ tr ⟧∗ + in record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ FFDState.inIBs (LeiosState.FFDState s)}} , o Irr-ValidAction : Irrelevant (ValidAction α s i) Irr-ValidAction (IB-Role _ _ _) (IB-Role _ _ _) = refl @@ -283,17 +307,23 @@ Irr-ValidAction Base₁ Base₁ = refl Irr-ValidAction (Base₂a _ _ _) (Base₂a _ _ _) = refl Irr-ValidAction (Base₂b _ _ _) (Base₂b _ _ _) = refl +Irr-ValidUpdate : ∀ {f} → Irrelevant (ValidUpdate f s) +Irr-ValidUpdate IB-Recv IB-Recv = refl + Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs) Irr-ValidTrace [] [] = refl Irr-ValidTrace (α / i ∷ vαs ⊣ vα) (.α / .i ∷ vαs′ ⊣ vα′) rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidAction vα vα′ = refl +Irr-ValidTrace (vαs ∷ u) (vαs′ ∷ u′) + rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidUpdate u u′ + = refl instance Dec-ValidTrace : ValidTrace ⁇¹ Dec-ValidTrace {tr} .dec with tr ... | [] = yes [] - ... | (α , i) ∷ αs + ... | inj₁ (α , i) ∷ αs with ¿ ValidTrace αs ¿ ... | no ¬vαs = no λ where (_ / _ ∷ vαs ⊣ _) → ¬vαs vαs ... | yes vαs @@ -303,12 +333,21 @@ instance $ subst (λ x → ValidAction α x i) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vα ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα + Dec-ValidTrace {tr} .dec | inj₂ u ∷ αs + with ¿ ValidTrace αs ¿ + ... | no ¬vαs = no λ where (vαs ∷ _) → ¬vαs vαs + ... | yes vαs + with ¿ ValidUpdate u (proj₁ ⟦ vαs ⟧∗) ¿ + ... | yes vu = yes (vαs ∷ vu) + ... | no ¬vu = no λ where + (tr ∷ vu) → ¬vu $ subst (λ x → ValidUpdate u x) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vu + private opaque unfolding List-Model test₁ : Bool - test₁ = ¿ ValidTrace ((IB-Role-Action 0 , SLOT) ∷ []) ¿ᵇ + test₁ = ¿ ValidTrace (inj₁ (IB-Role-Action 0 , SLOT) ∷ []) ¿ᵇ _ : test₁ ≡ true _ = refl @@ -316,22 +355,41 @@ private test₂ : Bool test₂ = let t = L.reverse $ - (IB-Role-Action 0 , SLOT) - ∷ (EB-Role-Action 0 [] , SLOT) - ∷ (VT-Role-Action 0 , SLOT) - ∷ (Base₂b-Action , SLOT) - ∷ (Slot-Action 0 , SLOT) - ∷ (IB-Role-Action 1 , SLOT) - ∷ (EB-Role-Action 1 [] , SLOT) - ∷ (VT-Role-Action 1 , SLOT) - ∷ (Base₂b-Action , SLOT) - ∷ (Slot-Action 1 , SLOT) + inj₁ (IB-Role-Action 0 , SLOT) + ∷ inj₁ (EB-Role-Action 0 [] , SLOT) + ∷ inj₁ (VT-Role-Action 0 , SLOT) + ∷ inj₁ (Base₂b-Action , SLOT) + ∷ inj₁ (Slot-Action 0 , SLOT) + ∷ inj₁ (IB-Role-Action 1 , SLOT) + ∷ inj₁ (EB-Role-Action 1 [] , SLOT) + ∷ inj₁ (VT-Role-Action 1 , SLOT) + ∷ inj₁ (Base₂b-Action , SLOT) + ∷ inj₁ (Slot-Action 1 , SLOT) + ∷ inj₂ (IB-Recv-Update + (record { header = + record { slotNumber = 1 + ; producerID = fsuc fzero + ; lotteryPf = tt + ; bodyHash = "0,1,2" + ; signature = tt + } + ; body = record { txs = 0 ∷ 1 ∷ 2 ∷ [] }})) ∷ [] in ¿ ValidTrace t ¿ᵇ _ : test₂ ≡ true _ = refl +data LocalStep : LeiosState → LeiosState → Type where + + StateStep : ∀ {s i o s′} → + just s -⟦ i / o ⟧⇀ s′ → + LocalStep s s′ + + UpdateIB : ∀ {s ib} → + LocalStep s (record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ (FFDState.inIBs (LeiosState.FFDState s)) } }) + + getLabel : just s -⟦ i / o ⟧⇀ s′ → Action getLabel (Slot {s} _ _ _) = Slot-Action (LeiosState.slot s) getLabel Ftch = Ftch-Action From 1ded9c1c141b34f6631b7ed2b34c963b84262542 Mon Sep 17 00:00:00 2001 From: Yves Date: Wed, 19 Mar 2025 19:08:11 +0100 Subject: [PATCH 18/22] Updating FFD buffers --- formal-spec/Leios/Trace/Verifier.agda | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 83c8373..a92ca49 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -12,6 +12,8 @@ open GenFFD data FFDUpdate : Type where IB-Recv-Update : InputBlock → FFDUpdate + EB-Recv-Update : EndorserBlock → FFDUpdate + VT-Recv-Update : List Vote → FFDUpdate data Action : Type where IB-Role-Action : ℕ → Action @@ -30,12 +32,16 @@ private variable s s′ : LeiosState α : Action - data ValidUpdate : FFDUpdate → LeiosState → Type where IB-Recv : ∀ {ib} → - let open LeiosState s renaming (FFDState to ffds) - in ValidUpdate (IB-Recv-Update ib) s + ValidUpdate (IB-Recv-Update ib) s + + EB-Recv : ∀ {eb} → + ValidUpdate (EB-Recv-Update eb) s + + VT-Recv : ∀ {vt} → + ValidUpdate (VT-Recv-Update vt) s data ValidAction : Action → LeiosState → LeiosInput → Type where @@ -267,6 +273,8 @@ instance instance Dec-ValidUpdate : ValidUpdate ⁇² Dec-ValidUpdate {IB-Recv-Update _} .dec = yes IB-Recv + Dec-ValidUpdate {EB-Recv-Update _} .dec = yes EB-Recv + Dec-ValidUpdate {VT-Recv-Update _} .dec = yes VT-Recv mutual data ValidTrace : List ((Action × LeiosInput) ⊎ FFDUpdate) → Type where @@ -293,6 +301,13 @@ mutual ⟦ _∷_ {IB-Recv-Update ib} tr vu ⟧∗ = let (s , o) = ⟦ tr ⟧∗ in record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ FFDState.inIBs (LeiosState.FFDState s)}} , o + ⟦ _∷_ {EB-Recv-Update eb} tr vu ⟧∗ = + let (s , o) = ⟦ tr ⟧∗ + in record s { FFDState = record (LeiosState.FFDState s) { inEBs = eb ∷ FFDState.inEBs (LeiosState.FFDState s)}} , o + ⟦ _∷_ {VT-Recv-Update vt} tr vu ⟧∗ = + let (s , o) = ⟦ tr ⟧∗ + in record s { FFDState = record (LeiosState.FFDState s) { inVTs = vt ∷ FFDState.inVTs (LeiosState.FFDState s)}} , o + Irr-ValidAction : Irrelevant (ValidAction α s i) Irr-ValidAction (IB-Role _ _ _) (IB-Role _ _ _) = refl @@ -309,6 +324,8 @@ Irr-ValidAction (Base₂b _ _ _) (Base₂b _ _ _) = refl Irr-ValidUpdate : ∀ {f} → Irrelevant (ValidUpdate f s) Irr-ValidUpdate IB-Recv IB-Recv = refl +Irr-ValidUpdate EB-Recv EB-Recv = refl +Irr-ValidUpdate VT-Recv VT-Recv = refl Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs) Irr-ValidTrace [] [] = refl From 9b2db8ed5afd368bc75f7642462be61f0d613db8 Mon Sep 17 00:00:00 2001 From: Yves Date: Wed, 19 Mar 2025 19:13:13 +0100 Subject: [PATCH 19/22] LocalStep relation --- formal-spec/Leios/Trace/Verifier.agda | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index a92ca49..98d021e 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -397,15 +397,26 @@ private _ : test₂ ≡ true _ = refl +data _⇑_ : LeiosState → LeiosState → Type where + + UpdateIB : ∀ {s ib} → + s ⇑ record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ (FFDState.inIBs (LeiosState.FFDState s)) } } + + UpdateEB : ∀ {s eb} → + s ⇑ record s { FFDState = record (LeiosState.FFDState s) { inEBs = eb ∷ (FFDState.inEBs (LeiosState.FFDState s)) } } + + UpdateVT : ∀ {s vt} → + s ⇑ record s { FFDState = record (LeiosState.FFDState s) { inVTs = vt ∷ (FFDState.inVTs (LeiosState.FFDState s)) } } + data LocalStep : LeiosState → LeiosState → Type where StateStep : ∀ {s i o s′} → just s -⟦ i / o ⟧⇀ s′ → LocalStep s s′ - UpdateIB : ∀ {s ib} → - LocalStep s (record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ (FFDState.inIBs (LeiosState.FFDState s)) } }) - + UpdateState : ∀ {s s′} → + s ⇑ s′ → + LocalStep s s′ getLabel : just s -⟦ i / o ⟧⇀ s′ → Action getLabel (Slot {s} _ _ _) = Slot-Action (LeiosState.slot s) From 960b32100313695cd73bf42437e48a153d09a494 Mon Sep 17 00:00:00 2001 From: Yves Date: Wed, 19 Mar 2025 19:27:37 +0100 Subject: [PATCH 20/22] More concise --- formal-spec/Leios/Trace/Verifier.agda | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 98d021e..0d2e817 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -399,24 +399,28 @@ private data _⇑_ : LeiosState → LeiosState → Type where - UpdateIB : ∀ {s ib} → - s ⇑ record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ (FFDState.inIBs (LeiosState.FFDState s)) } } + UpdateIB : ∀ {s ib} → let open LeiosState s renaming (FFDState to ffds) in + s ⇑ record s { FFDState = record ffds { inIBs = ib ∷ FFDState.inIBs ffds } } - UpdateEB : ∀ {s eb} → - s ⇑ record s { FFDState = record (LeiosState.FFDState s) { inEBs = eb ∷ (FFDState.inEBs (LeiosState.FFDState s)) } } + UpdateEB : ∀ {s eb} → let open LeiosState s renaming (FFDState to ffds) in + s ⇑ record s { FFDState = record ffds { inEBs = eb ∷ FFDState.inEBs ffds } } - UpdateVT : ∀ {s vt} → - s ⇑ record s { FFDState = record (LeiosState.FFDState s) { inVTs = vt ∷ (FFDState.inVTs (LeiosState.FFDState s)) } } + UpdateVT : ∀ {s vt} → let open LeiosState s renaming (FFDState to ffds) in + s ⇑ record s { FFDState = record ffds { inVTs = vt ∷ FFDState.inVTs ffds } } data LocalStep : LeiosState → LeiosState → Type where StateStep : ∀ {s i o s′} → - just s -⟦ i / o ⟧⇀ s′ → - LocalStep s s′ + ∙ just s -⟦ i / o ⟧⇀ s′ + ─────────────────── + LocalStep s s′ UpdateState : ∀ {s s′} → - s ⇑ s′ → - LocalStep s s′ + ∙ s ⇑ s′ + ─────────────────── + LocalStep s s′ + + -- TODO: add base layer update getLabel : just s -⟦ i / o ⟧⇀ s′ → Action getLabel (Slot {s} _ _ _) = Slot-Action (LeiosState.slot s) From 5886fcd1cb6eeebac146dc67d052a58e1304327d Mon Sep 17 00:00:00 2001 From: Yves Date: Thu, 20 Mar 2025 13:27:58 +0100 Subject: [PATCH 21/22] Parameterized Verifier --- formal-spec/Everything.agda | 1 + formal-spec/Leios/Trace/Verifier.agda | 42 +-------------------- formal-spec/Leios/Trace/Verifier/Test.agda | 44 ++++++++++++++++++++++ 3 files changed, 47 insertions(+), 40 deletions(-) create mode 100644 formal-spec/Leios/Trace/Verifier/Test.agda diff --git a/formal-spec/Everything.agda b/formal-spec/Everything.agda index 4420ba6..bf4d9fc 100644 --- a/formal-spec/Everything.agda +++ b/formal-spec/Everything.agda @@ -24,6 +24,7 @@ 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.UniformShort open import Leios.Voting open import Leios.VRF diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 0d2e817..87f839b 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -1,9 +1,9 @@ open import Leios.Prelude hiding (id) -module Leios.Trace.Verifier where +module Leios.Trace.Verifier (numberOfParties : ℕ) (SUT-id : Fin numberOfParties) where open import Leios.SpecStructure using (SpecStructure) -open import Leios.Defaults 2 fzero using (st; sd; LeiosState; initLeiosState; isb; hpe; hhs; htx; SendIB; FFDState; Dec-SimpleFFD; send-total; fetch-total) +open import Leios.Defaults numberOfParties SUT-id using (st; sd; LeiosState; initLeiosState; isb; hpe; hhs; htx; SendIB; FFDState; Dec-SimpleFFD; send-total; fetch-total) open SpecStructure st hiding (Hashable-IBHeader; Hashable-EndorserBlock; isVoteCertified) open import Leios.Short st hiding (LeiosState; initLeiosState) @@ -359,44 +359,6 @@ instance ... | no ¬vu = no λ where (tr ∷ vu) → ¬vu $ subst (λ x → ValidUpdate u x) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vu -private - opaque - unfolding List-Model - - test₁ : Bool - test₁ = ¿ ValidTrace (inj₁ (IB-Role-Action 0 , SLOT) ∷ []) ¿ᵇ - - _ : test₁ ≡ true - _ = refl - - test₂ : Bool - test₂ = - let t = L.reverse $ - inj₁ (IB-Role-Action 0 , SLOT) - ∷ inj₁ (EB-Role-Action 0 [] , SLOT) - ∷ inj₁ (VT-Role-Action 0 , SLOT) - ∷ inj₁ (Base₂b-Action , SLOT) - ∷ inj₁ (Slot-Action 0 , SLOT) - ∷ inj₁ (IB-Role-Action 1 , SLOT) - ∷ inj₁ (EB-Role-Action 1 [] , SLOT) - ∷ inj₁ (VT-Role-Action 1 , SLOT) - ∷ inj₁ (Base₂b-Action , SLOT) - ∷ inj₁ (Slot-Action 1 , SLOT) - ∷ inj₂ (IB-Recv-Update - (record { header = - record { slotNumber = 1 - ; producerID = fsuc fzero - ; lotteryPf = tt - ; bodyHash = "0,1,2" - ; signature = tt - } - ; body = record { txs = 0 ∷ 1 ∷ 2 ∷ [] }})) - ∷ [] - in ¿ ValidTrace t ¿ᵇ - - _ : test₂ ≡ true - _ = refl - data _⇑_ : LeiosState → LeiosState → Type where UpdateIB : ∀ {s ib} → let open LeiosState s renaming (FFDState to ffds) in diff --git a/formal-spec/Leios/Trace/Verifier/Test.agda b/formal-spec/Leios/Trace/Verifier/Test.agda new file mode 100644 index 0000000..9ba2423 --- /dev/null +++ b/formal-spec/Leios/Trace/Verifier/Test.agda @@ -0,0 +1,44 @@ +open import Leios.Prelude hiding (id) + +module Leios.Trace.Verifier.Test where + +open import Leios.Trace.Verifier 2 fzero +open import Leios.Defaults 2 fzero + +private + opaque + unfolding List-Model + + test₁ : Bool + test₁ = ¿ ValidTrace (inj₁ (IB-Role-Action 0 , SLOT) ∷ []) ¿ᵇ + + _ : test₁ ≡ true + _ = refl + + test₂ : Bool + test₂ = + let t = L.reverse $ + inj₁ (IB-Role-Action 0 , SLOT) + ∷ inj₁ (EB-Role-Action 0 [] , SLOT) + ∷ inj₁ (VT-Role-Action 0 , SLOT) + ∷ inj₁ (Base₂b-Action , SLOT) + ∷ inj₁ (Slot-Action 0 , SLOT) + ∷ inj₁ (IB-Role-Action 1 , SLOT) + ∷ inj₁ (EB-Role-Action 1 [] , SLOT) + ∷ inj₁ (VT-Role-Action 1 , SLOT) + ∷ inj₁ (Base₂b-Action , SLOT) + ∷ inj₁ (Slot-Action 1 , SLOT) + ∷ inj₂ (IB-Recv-Update + (record { header = + record { slotNumber = 1 + ; producerID = fsuc fzero + ; lotteryPf = tt + ; bodyHash = "0,1,2" + ; signature = tt + } + ; body = record { txs = 0 ∷ 1 ∷ 2 ∷ [] }})) + ∷ [] + in ¿ ValidTrace t ¿ᵇ + + _ : test₂ ≡ true + _ = refl From 82b6660bdcd96a2a95ce02f85305baac4011e74e Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Mon, 24 Mar 2025 09:22:25 +0100 Subject: [PATCH 22/22] Improved notation --- formal-spec/Leios/Trace/Verifier.agda | 57 +++++++++++++-------------- 1 file changed, 27 insertions(+), 30 deletions(-) diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda index 87f839b..8a315e8 100644 --- a/formal-spec/Leios/Trace/Verifier.agda +++ b/formal-spec/Leios/Trace/Verifier.agda @@ -288,7 +288,7 @@ mutual ─────────────────── ValidTrace (inj₁ (α , i) ∷ αs) - _∷_ : ∀ {f αs} → + _↥_ : ∀ {f αs} → ∀ (tr : ValidTrace αs) → (vu : ValidUpdate f (proj₁ ⟦ tr ⟧∗)) → ─────────────────── @@ -298,13 +298,13 @@ mutual ⟦_⟧∗ : ∀ {αs : List ((Action × LeiosInput) ⊎ FFDUpdate)} → ValidTrace αs → LeiosState × LeiosOutput ⟦_⟧∗ [] = initLeiosState tt sd tt , EMPTY ⟦_⟧∗ (_ / _ ∷ _ ⊣ vα) = ⟦ vα ⟧ - ⟦ _∷_ {IB-Recv-Update ib} tr vu ⟧∗ = + ⟦ _↥_ {IB-Recv-Update ib} tr vu ⟧∗ = let (s , o) = ⟦ tr ⟧∗ in record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ FFDState.inIBs (LeiosState.FFDState s)}} , o - ⟦ _∷_ {EB-Recv-Update eb} tr vu ⟧∗ = + ⟦ _↥_ {EB-Recv-Update eb} tr vu ⟧∗ = let (s , o) = ⟦ tr ⟧∗ in record s { FFDState = record (LeiosState.FFDState s) { inEBs = eb ∷ FFDState.inEBs (LeiosState.FFDState s)}} , o - ⟦ _∷_ {VT-Recv-Update vt} tr vu ⟧∗ = + ⟦ _↥_ {VT-Recv-Update vt} tr vu ⟧∗ = let (s , o) = ⟦ tr ⟧∗ in record s { FFDState = record (LeiosState.FFDState s) { inVTs = vt ∷ FFDState.inVTs (LeiosState.FFDState s)}} , o @@ -332,7 +332,7 @@ Irr-ValidTrace [] [] = refl Irr-ValidTrace (α / i ∷ vαs ⊣ vα) (.α / .i ∷ vαs′ ⊣ vα′) rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidAction vα vα′ = refl -Irr-ValidTrace (vαs ∷ u) (vαs′ ∷ u′) +Irr-ValidTrace (vαs ↥ u) (vαs′ ↥ u′) rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidUpdate u u′ = refl @@ -352,12 +352,12 @@ instance Dec-ValidTrace {tr} .dec | inj₂ u ∷ αs with ¿ ValidTrace αs ¿ - ... | no ¬vαs = no λ where (vαs ∷ _) → ¬vαs vαs + ... | no ¬vαs = no λ where (vαs ↥ _) → ¬vαs vαs ... | yes vαs with ¿ ValidUpdate u (proj₁ ⟦ vαs ⟧∗) ¿ - ... | yes vu = yes (vαs ∷ vu) + ... | yes vu = yes (vαs ↥ vu) ... | no ¬vu = no λ where - (tr ∷ vu) → ¬vu $ subst (λ x → ValidUpdate u x) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vu + (tr ↥ vu) → ¬vu $ subst (λ x → ValidUpdate u x) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vu data _⇑_ : LeiosState → LeiosState → Type where @@ -398,17 +398,17 @@ getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action getLabel (Roles (No-VT-Role _ _)) = No-VT-Role-Action ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′ -ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) -ValidAction-sound Ftch = Ftch -ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs} -ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) -ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂) -ValidAction-sound (IB-Role {s} x x₁ x₂) = Roles (IB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) -ValidAction-sound (EB-Role {s} x x₁ x₂) = Roles (EB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) -ValidAction-sound (VT-Role {s} x x₁ x₂) = Roles (VT-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)) -ValidAction-sound (No-IB-Role {s} x x₁) = Roles (No-IB-Role {s} x x₁) -ValidAction-sound (No-EB-Role {s} x x₁) = Roles (No-EB-Role {s} x x₁) -ValidAction-sound (No-VT-Role {s} x x₁) = Roles (No-VT-Role {s} x x₁) +ValidAction-sound (Slot x x₁ x₂) = Slot {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound Ftch = Ftch +ValidAction-sound Base₁ = Base₁ +ValidAction-sound (Base₂a x x₁ x₂) = Base₂a (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (Base₂b x x₁ x₂) = Base₂b (recompute dec x) (recompute dec x₁) (recompute dec x₂) +ValidAction-sound (IB-Role x x₁ x₂) = Roles (IB-Role (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (EB-Role x x₁ x₂) = Roles (EB-Role (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (VT-Role x x₁ x₂) = Roles (VT-Role (recompute dec x) (recompute dec x₁) (recompute dec x₂)) +ValidAction-sound (No-IB-Role x x₁) = Roles (No-IB-Role x x₁) +ValidAction-sound (No-EB-Role x x₁) = Roles (No-EB-Role x x₁) +ValidAction-sound (No-VT-Role x x₁) = Roles (No-VT-Role x x₁) ValidAction-complete : (st : just s -⟦ i / o ⟧⇀ s′) → ValidAction (getLabel st) s i ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ _)) = @@ -429,14 +429,11 @@ ValidAction-complete {s} (Roles (VT-Role x x₁ _)) = votes = map (vote sk-V ∘ hash) EBs' pr = proj₂ (send-total {ffds} {vHeader votes} {nothing}) in VT-Role {s} x x₁ pr -ValidAction-complete {s} (Roles (No-IB-Role x x₁)) = No-IB-Role {s} x x₁ -ValidAction-complete {s} (Roles (No-EB-Role x x₁)) = No-EB-Role {s} x x₁ -ValidAction-complete {s} (Roles (No-VT-Role x x₁)) = No-VT-Role {s} x x₁ -ValidAction-complete {s} Ftch = Ftch {s} -ValidAction-complete {s} Base₁ = Base₁ {s} -ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂ -ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂ -ValidAction-complete {s} (Slot {s} x x₁ _) = - let open LeiosState s renaming (FFDState to ffds) - (_ , (_ , pr)) = fetch-total {ffds} - in Slot {s} x x₁ pr +ValidAction-complete (Roles (No-IB-Role x x₁)) = No-IB-Role x x₁ +ValidAction-complete (Roles (No-EB-Role x x₁)) = No-EB-Role x x₁ +ValidAction-complete (Roles (No-VT-Role x x₁)) = No-VT-Role x x₁ +ValidAction-complete Ftch = Ftch +ValidAction-complete Base₁ = Base₁ +ValidAction-complete (Base₂a x x₁ x₂) = Base₂a x x₁ x₂ +ValidAction-complete (Base₂b x x₁ x₂) = Base₂b x x₁ x₂ +ValidAction-complete {s} (Slot x x₁ _) = Slot x x₁ (proj₂ (proj₂ (fetch-total {LeiosState.FFDState s})))