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.

1234567891011121314151617181920212223
  params : Params
  params =
    record
      { networkParams =
          record
            { numberOfParties = 2
            ; stakeDistribution =
                let open FunTot (completeFin 2) (maximalFin 2)
                in Fun⇒TotalMap (const 100000000)
            }
      ; Lhdr = 1
      ; Lvote = 2
      ; Ldiff = 2
      ; σc-num = 99
      ; σc-den = 100
      }
 
  testParams : TestParams params
  testParams =
    record
      { sutId = fzero
      ; winning-slots = fromList $ 108 ∷ []
      }

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

1
  open import Leios.Linear.Trace.Verifier d-SpecStructure params

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 { txsOrEbCert = inj₁ (0 ∷ []) ; announcedEB = nothing }
    RB₁ = record { txsOrEbCert = inj₁ [] ; announcedEB = just (hash EB₁) }

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. The base layer hands over the chain oldest first, so the tip is RB₁ and not RB₀; this is the step that pins the ordering, since the vote in slot 104 is for the EB that RB₁ announces.

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

Slot 102

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

Slot 103

1234
                 ∷ (No-EB-Role-Action 103 , inj₁ SLOT)
                 ∷ (Base₂-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
                 ∷ (No-EB-Role-Action 104 , inj₁ SLOT)
                 ∷ (Base₂-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
                 ∷ (No-EB-Role-Action 105 , inj₁ SLOT)
                 ∷ (Base₂-Action      105 , inj₁ SLOT)
                 ∷ (No-VT-Role-Action 105 , inj₁ SLOT)
                 ∷ (Slot₁-Action      105 , inj₁ (FFD-OUT (inj₁ (vtHeader VT₁) ∷ [])))

Slot 106

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

Slot 107

1234
                 ∷ (No-EB-Role-Action 107 , inj₁ SLOT)
                 ∷ (Base₂-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

123
                 ∷ (No-EB-Role-Action 109 , inj₁ SLOT)
                 ∷ (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