123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124open import Leios.Prelude hiding (id)open import Leios.Config module Leios.Short.Trace.Verifier.Test where params : Paramsparams = record { numberOfParties = 2 ; sutId = fzero ; stakeDistribution = let open FunTot (completeFin 2) (maximalFin 2) in Fun⇒TotalMap (const 100000000) ; stageLength = 2 ; winning-slots = fromList $ (IB , 1) ∷ (EB , 1) ∷ (VT , 1) ∷ (IB , 2) ∷ (EB , 2) ∷ (VT , 2) ∷ (IB , 3) ∷ (EB , 3) ∷ (VT , 3) ∷ (IB , 4) ∷ (EB , 4) ∷ (VT , 4) ∷ (IB , 5) ∷ (EB , 5) ∷ (VT , 5) ∷ (VT , 6) ∷ (IB , 7) ∷ (EB , 7) ∷ (VT , 7) ∷ (IB , 8) ∷ (EB , 8) ∷ (VT , 8) ∷ [] } open Params paramsopen import Leios.Short.Trace.Verifier params private opaque unfolding List-Model s₀ : LeiosState s₀ = initLeiosState tt stakeDistribution tt ((fzero , tt) ∷ (fsuc fzero , tt) ∷ []) test₁ : IsOk (verifyTrace (inj₁ (Slot-Action 0 , SLOT) ∷ inj₁ (Base₂b-Action 0 , SLOT) ∷ []) s₀) test₁ = _ test-valid-ib : Bool test-valid-ib = let h = record { slotNumber = 1 ; producerID = fsuc fzero ; lotteryPf = tt ; bodyHash = 0 ∷ 1 ∷ 2 ∷ [] ; signature = tt } b = record { txs = 0 ∷ 1 ∷ 2 ∷ [] } ib = record { header = h ; body = b } pks = L.zip (completeFinL numberOfParties) (L.replicate numberOfParties tt) s = initLeiosState tt stakeDistribution tt pks in isYes (ibValid? s ib) _ : test-valid-ib ≡ true _ = refl test₂ : IsOk (verifyTrace (L.reverse $ -- slot 0 inj₁ (Base₂b-Action 0 , SLOT) ∷ inj₁ (Slot-Action 0 , SLOT) -- slot 1 ∷ inj₁ (IB-Role-Action 1 , SLOT) ∷ inj₁ (VT-Role-Action 1 , SLOT) ∷ inj₁ (Base₂b-Action 1 , SLOT) ∷ inj₁ (Slot-Action 1 , SLOT) -- slot 2 ∷ 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 ∷ [] }})) ∷ inj₁ (IB-Role-Action 2 , SLOT) ∷ inj₁ (EB-Role-Action 2 [] , SLOT) ∷ inj₁ (VT-Role-Action 2 , SLOT) ∷ inj₁ (Base₂b-Action 2 , SLOT) ∷ inj₁ (Slot-Action 2 , SLOT) -- slot 3 ∷ inj₂ (IB-Recv-Update (record { header = record { slotNumber = 2 ; producerID = fsuc fzero ; lotteryPf = tt ; bodyHash = 3 ∷ 4 ∷ 5 ∷ [] ; signature = tt } ; body = record { txs = 3 ∷ 4 ∷ 5 ∷ [] }})) ∷ inj₁ (IB-Role-Action 3 , SLOT) ∷ inj₁ (VT-Role-Action 3 , SLOT) ∷ inj₁ (Base₂b-Action 3 , SLOT) ∷ inj₁ (Slot-Action 3 , SLOT) -- slot 4 ∷ inj₁ (IB-Role-Action 4 , SLOT) ∷ inj₁ (EB-Role-Action 4 [] , SLOT) ∷ inj₁ (VT-Role-Action 4 , SLOT) ∷ inj₁ (Base₂b-Action 4 , SLOT) ∷ inj₁ (Slot-Action 4 , SLOT) -- slot 5 ∷ inj₁ (IB-Role-Action 5 , SLOT) ∷ inj₁ (VT-Role-Action 5 , SLOT) ∷ inj₁ (Base₂b-Action 5 , SLOT) ∷ inj₁ (Slot-Action 5 , SLOT) -- slot 6 ∷ inj₁ (No-IB-Role-Action 6 , SLOT) ∷ inj₁ (No-EB-Role-Action 6 , SLOT) ∷ inj₁ (VT-Role-Action 6 , SLOT) ∷ inj₁ (Base₂b-Action 6 , SLOT) ∷ inj₁ (Slot-Action 6 , SLOT) -- slot 7 ∷ inj₁ (IB-Role-Action 7 , SLOT) ∷ inj₁ (VT-Role-Action 7 , SLOT) ∷ inj₁ (Base₂b-Action 7 , SLOT) ∷ inj₁ (Slot-Action 7 , SLOT) -- slot 8 ∷ inj₁ (IB-Role-Action 8 , SLOT) ∷ inj₁ (EB-Role-Action 8 ((3 ∷ 4 ∷ 5 ∷ []) ∷ []) , SLOT) ∷ inj₁ (VT-Role-Action 8 , SLOT) ∷ inj₁ (Base₂b-Action 8 , SLOT) ∷ inj₁ (Slot-Action 8 , SLOT) ∷ []) s₀) test₂ = _