safrole.asn

-- Safrole STF test vectors schema

SafroleModule DEFINITIONS ::= BEGIN

IMPORTS
    TimeSlot, ValidatorsData, Entropy, EntropyBuffer,
    TicketBody, TicketsAccumulator, TicketsOrKeys, TicketsExtrinsic,
    EpochMark, TicketsMark, Ed25519Public, BandersnatchRingCommitment
        FROM JamTypes;


State ::= SEQUENCE {
    -- [τ] Prior most recent block's timeslot. Mutated to τ'.
    tau TimeSlot,
    -- [η] Prior entropy buffer. Mutated to η'.
    eta EntropyBuffer,
    -- [λ] Prior previous epoch validator keys and metadata. Mutated to λ'.
    lambda ValidatorsData,
    -- [κ] Prior current epoch validator keys and metadata. Mutated to κ'.
    kappa ValidatorsData,
    -- [γ_k] Prior next epoch validator keys and metadata. Mutated to γ'_k.
    gamma-k ValidatorsData,
    -- [ι] Prior scheduled validator keys and metadata. Mutated to ι'.
    iota ValidatorsData,
    -- [γ_a] Prior sealing-key contest ticket accumulator. Mutated to γ'_a.
    gamma-a TicketsAccumulator,
    -- [γ_s] Prior sealing-key series of the current epoch. Mutated to γ'_s.
    gamma-s TicketsOrKeys,
    -- [γ_z] Prior Bandersnatch ring commitment. Mutated to γ'_z.
    gamma-z BandersnatchRingCommitment,
    -- [ψ'_o] Posterior offenders sequence.
    post-offenders SEQUENCE OF Ed25519Public
}

Input ::= SEQUENCE {
    -- [H_t] Current time slot as found within the block header.
    slot TimeSlot,
    -- [Y(H_v)] Per block entropy generated using per block entropy source.
    entropy Entropy,
    -- [E_T] Tickets extrinsic.
    extrinsic TicketsExtrinsic
}

OutputData ::= SEQUENCE {
    -- [H_e] New epoch marker.
    epoch-mark [0] EpochMark OPTIONAL,
    -- [H_w] Winning tickets marker.
    tickets-mark [1] TicketsMark OPTIONAL
}

-- State transition function execution error.
-- Error codes **are not specified** in the the Graypaper.
-- Feel free to ignore the actual value.
ErrorCode ::= ENUMERATED {
    -- Timeslot value must be strictly monotonic.
    bad-slot (0),
    -- Received a ticket while in epoch's tail.
    unexpected-ticket (1),
    -- Tickets must be sorted.
    bad-ticket-order (2),
    -- Invalid ticket ring proof.
    bad-ticket-proof (3),
    -- Invalid ticket attempt value.
    bad-ticket-attempt (4),
    -- Reserved
    reserved (5),
    -- Found a ticket duplicate.
    duplicate-ticket (6)
}

Output ::= CHOICE {
    ok   OutputData,
    err  ErrorCode
}

TestCase ::= SEQUENCE {
    input        Input,
    pre-state    State,
    output       Output,
    post-state   State
}

END