Leios.Linear.Trace.Verifier.Test

Trace verification with sample trace

12
module Leios.Linear.Trace.Verifier.Test where
private

Params

A test setup requires parameters, which are bundled in the Params record. There are the network parameters, the identifier for the system under test (SUT) and there are the schedules for block production and voting in the field winning-slots. Note, in Linear Leios EBs are produced optionally together with an RB.

12345678910111213141516171819202122232425
  params : Params
  params =
    record
      { networkParams =
          record
            { numberOfParties = 2
            ; stakeDistribution =
                let open FunTot (completeFin 2) (maximalFin 2)
                in Fun⇒TotalMap (const 100000000)
            }
      }
 
  testParams : TestParams params
  testParams =
    record
      { sutId = fzero
      ; winning-slots = fromList $
                     (VT , 100) ∷
                     (VT , 104) ∷
                     (VT , 105) ∷
                     (VT , 106) ∷
                     (VT , 107) ∷
        (EB , 108) ∷ (VT , 108) ∷
        []
      }

Additional Linear Leios parameters

Linear Leios has the following three protocol parameters

123
  Lhdr  = 1
  Lvote = 2
  Ldiff = 2

SpecStructure

In order to build a test trace, an implementation for the SpecStructure needs to be specified. For the test trace, we rely on the implementation provided in Test.Defaults.

123
  -- TODO: why does Hashable-EndorserBlock not work instead of hpe...?
  open import Test.Defaults params testParams using (d-SpecStructure; hpe)
  open SpecStructure d-SpecStructure hiding (Hashable-EndorserBlock)

TraceVerifier

1234567
  splitTxs : List Tx → List Tx × List Tx
  splitTxs l = [] , l
 
  validityCheckTime : EndorserBlock → ℕ
  validityCheckTime eb = 4
 
  open import Leios.Linear.Trace.Verifier d-SpecStructure params Lhdr Lvote Ldiff splitTxs validityCheckTime

EndorserBlocks that will be used in the test trace

12345
    EB₁ : EndorserBlock
    EB₁ = mkEB 100 (fsuc fzero) tt (EB , tt) (1 ∷ 2 ∷ 3 ∷ [])
 
    EB₂ : EndorserBlock
    EB₂ = mkEB 108 fzero tt (EB , tt) (3 ∷ 4 ∷ 5 ∷ [])

Checking hash of EndorserBlocks

12
    verify-EB₁-hash : hash EB₁ ≡ 1 ∷ 2 ∷ 3 ∷ []
    verify-EB₁-hash = refl

RankingBlocks that will be used in the test trace

123
    RB₀ RB₁ : RankingBlock
    RB₀ = record { txs = 0 ∷ [] ; announcedEB = nothing ; ebCert = nothing }
    RB₁ = record { txs = [] ; announcedEB = just (hash EB₁) ; ebCert = nothing }

Votes

12
    VT₁ : List Vote
    VT₁ = tt ∷ []

Starting at slot 100

123456789
    s₁₀₀ : LeiosState
    s₁₀₀ = record s₀
             { slot = 100
             ; ToPropose = 0 ∷ 1 ∷ 2 ∷ []
             ; PubKeys = (fzero , tt) ∷ (fsuc fzero , tt) ∷ []
             }
      where
        s₀ : LeiosState
        s₀ = initLeiosState tt stakeDistribution ((fzero , tt) ∷ (fsuc fzero , tt) ∷ [])

Build a test trace

12
    test-trace : TestTrace
    test-trace =

slot: 100 101 102 103 104 105 106 107 108 109

            3* Lhdr    Lvote   Ldiff
          <---------> <-----> <------>
  ___|___|___|___|___|___|___|___|___|___|___

                     +---+
                     |VT₀|
                     +---+
     +---+             |             +---+
  <--|RB₁| <-----------+-------------|RB₂|<--
     |EB₁| <-----------+---+---------|CRT|
     +---+                 |         +---+
                           |
                         +---+
                         |VT₁|
                         +---+

Slot 100

Submitting transactions, Receiving RB₀

123456
                   (No-EB-Role-Action 100 , inj₁ SLOT)
                 ∷ (Base₁-Action      100 , inj₂ (inj₂ (SubmitTxs (3 ∷ 4 ∷ 5 ∷ []))))
                 ∷ (Base₂-Action      100 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 100 , inj₁ SLOT)
                 ∷ (Slot₂-Action      100 , inj₂ (inj₁ (BASE-LDG [ RB₀ ])))
                 ∷ (Slot₁-Action      100 , inj₁ (FFD-OUT []))

Slot 101

Receiving RB₁/EB₁ generated by party 1 in slot 100

12345
                 ∷ (Base₂-Action      101 , inj₁ SLOT)
                 ∷ (No-EB-Role-Action 101 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 101 , inj₁ SLOT)
                 ∷ (Slot₂-Action      101 , inj₂ (inj₁ (BASE-LDG [ RB₁ ])))
                 ∷ (Slot₁-Action      101 , inj₁ (FFD-OUT (inj₁ (ebHeader EB₁) ∷ [])))

Slot 102

1234
                 ∷ (Base₂-Action      102 , inj₁ SLOT)
                 ∷ (No-EB-Role-Action 102 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 102 , inj₁ SLOT)
                 ∷ (Slot₁-Action      102 , inj₁ (FFD-OUT []))

Slot 103

1234
                 ∷ (Base₂-Action      103 , inj₁ SLOT)
                 ∷ (No-EB-Role-Action 103 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 103 , inj₁ SLOT)
                 ∷ (Slot₁-Action      103 , inj₁ (FFD-OUT []))

Slot 104

The SUT is voting for EB₁ in this slot

1234
                 ∷ (Base₂-Action      104 , inj₁ SLOT)
                 ∷ (No-EB-Role-Action 104 , inj₁ SLOT)
                 ∷ (VT-Role-Action 104 EB₁ 101 , inj₁ SLOT)
                 ∷ (Slot₁-Action      104 , inj₁ (FFD-OUT []))

Slot 105

Another vote is received

1234
                 ∷ (Base₂-Action      105 , inj₁ SLOT)
                 ∷ (No-EB-Role-Action 105 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 105 , inj₁ SLOT)
                 ∷ (Slot₁-Action      105 , inj₁ (FFD-OUT (inj₁ (vtHeader VT₁) ∷ [])))

Slot 106

1234
                 ∷ (Base₂-Action      106 , inj₁ SLOT)
                 ∷ (No-EB-Role-Action 106 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 106 , inj₁ SLOT)
                 ∷ (Slot₁-Action      106 , inj₁ (FFD-OUT []))

Slot 107

1234
                 ∷ (Base₂-Action      107 , inj₁ SLOT)
                 ∷ (No-EB-Role-Action 107 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 107 , inj₁ SLOT)
                 ∷ (Slot₁-Action      107 , inj₁ (FFD-OUT []))

Slot 108

SUT is slot leader: create an EB and RB (implicit in Base₂-Action)

1234
                 ∷ (EB-Role-Action    108 EB₂ , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 108 , inj₁ SLOT)
                 ∷ (Base₂-Action      108 , inj₁ SLOT)
                 ∷ (Slot₁-Action      108 , inj₁ (FFD-OUT []))

Slot 109

12
                 ∷ (Base₂-Action      109 , inj₁ SLOT)
                 ∷ []

Verify the test-trace

12
    test₁ : IsOk (verifyTrace (L.reverse test-trace) s₁₀₀)
    test₁ = _

Test error handling

12345678
    retValue : String
    retValue =
      case verifyTrace (L.reverse test-trace) s₁₀₀ of λ where
        (Ok _) → "ok"
        (Err e) → errorMsg e
 
    test₂ : retValue ≡ "ok"
    test₂ = refl