Supported states

When a participant wishes to call forceMove, respondWithMove, respondWithAlternativeMove, or conclude, they need to provide proof to the adjudicator that the channel has arrived at a given state with agreement among all participants. This post gives a formal definition of what this proof should entail.

Define the following type:

interface SignedState {
  state: State,
  sigs: Set<Signature>
}

Consider a state channel with participants participants.
Let support be of type SignedState[].
Define

numParticipants := participants.length
m := numStates := support.length
state := support[m-1]
supporters(i) := {
  addresses a :
  for some sig \in support[i].sigs), a == recoverSigner(support[i].state, sig)
}
mover(k) := k % numParticipants

ie.

  • supporters(i) is the set of addresses which signed the i-th state
  • mover(k) is the index of the participant who’s turn it is at turn k

We say that
support supports state if:

  • (R1) For all i = 0,..,m-1, there exists a j \in i, ..., m such that mover(support[i].state.turnNumber) \in supporters(j)
  • (R2) Union(supporters(i)) = Set(participants)

In this case, we call support a support of state.

Note that this definition only makes sense in the context where the states in support are sequential, ie.
support[i+1].state.turnNumber == support[i].state + 1 for i = 0,...,m-1.
In practice, this is guaranteed by first checking that successive pairs of states form valid transitions.

The implementation here is a sufficient, gas-efficient (but not equivalent) way of satisfying the above definition. The implementation is equivalent to R1+R2 plus the following requirement, which would typically hold in practice.

  • (R2’) supporters(i) partition Set(participants), ie. each participant is in precisely one supporters(i)

Any support of state satisfying R1 & R2 can be trivially modified to satisfy R1 & R2’ by discarding all but the latest signature for a given participant. R1 & R2’ also implies that non-participants cannot support a state.

Providing the whoSignedWhat array allows the adjudicator to verify that R1 & R2 hold in a gas-efficient manner, since the adjudicator can verify R1 without having to loop over j.

The simplest two examples which satisfy this definition are:

    • m == numParticipants; and
    • supporters(i) = {participant[mover(support[i].state.turnNumber)]}
    • This corresponds to a full round of states is provided, and each participant signed precisely the state on their turn.
    • In this case, whoSignedWhat is equal to [0,1,...,numParticipants - 1].
    • m == 1; and
    • supporters(0) = Set(participants)
    • This corresponds to where one state was provided and each participant signed it.
    • In this case, whoSignedWhat is equal to [0,0,..,0].

In practice, one would almost always use either 1 or 2.

We might want to add the condition that the states form a sequence of validTransitions to the definition of “support”. The concept doesn’t seem to be much use without that.

Agreed, though the only thing required for it to make sense is that the turn numbers are sequential.

All makes sense. I think I’m with Tom that each transition needs to be valid for it to really enable support, as you defined it.

I don’t know if it formally needs to go in here, but for completeness, I’d be tempted to add some mechanism to identify the state as belonging to the channel. The turn number is necessary but not sufficient in practice. I enforce this rigorously, and everywhere.