`LockstepCrossValidator` Function Summaries

[tothtamas28]

Call Graph

---
title: LockstepCrossValidator Call Graph
---
graph LR
    Backend.CheckAccessList --> ValidateAccessEntry
    ValidateAccessEntry --> getMinIngestedTimestamp
    ValidateAccessEntry --> CrossValidatedTimestamp
    ValidateAccessEntry --> validateMessageTiming
    ValidateAccessEntry --> ChainIngester.Contains
    validateExecutingMessage --> validateMessageTiming
    validateExecutingMessage --> ChainIngester.Contains
    runValidationLoop --> advanceValidation
    advanceValidation --> getMinIngestedTimestamp
    advanceValidation --> validateTimestamp
    advanceValidation --> ChainIngester.Error
    advanceValidation --> ChainIngester.Ready
    validateTimestamp --> ChainIngester.GetExecMsgsAtTimestamp
    validateTimestamp --> validateExecutingMessage
    getMinIngestedTimestamp --> ChainIngester.Ready
    getMinIngestedTimestamp --> ChainIngester.LatestTimestamp
    Backend.Start --> Start
    Start --> runValidationLoop

Loading

Function Summaries

The following section is a simplified summary of function postconditions for LockstepCrossValidator.
We apply the following simplifying assumptions:

• We assume each function to evaluate in an instant, in particular, we do not consider race conditions arising from asynchronous ChainIngester behavior.
• Since we're not reasoning about concurrency, we treat crossValidatedTs as uint64.

validateMessageTiming

func validateMessageTiming(
    initTimestamp       uint64,
    inclusionTimestamp  uint64,
    messageExpiryWindow uint64,
    timeout             uint64,
    execTimestamp       uint64,
) (err error)

Summary

• If timeout == 0, then err == nil iff
  • initTimestamp < inclusionTimestamp <= initTimestamp + messageExpiryWindow
• If timeout > 0, then err == nil iff
  • initTimestamp < inclusionTimestamp <= initTimestamp + messageExpiryWindow
  • execTimestamp < execTimestamp + timeout <= initTimestamp + messageExpiryWindow

getMinIngestedTimestamp

func (v *LockstepCrossValidator) getMinIngestedTimestamp() (ts uint64, ok bool)

Summary

• ok iff
  • len(v.chains) > 0
  • forall (ingester : v.chains)
    • ingester.Ready()
    • ingester.LatestTimestamp().ok
• If ok then ts == min (ingester : v.chains) ingester.LatestTimestamp().ts
• If !ok then ts == 0

CrossValidatedTimestamp

func (v *LockstepCrossValidator) CrossValidatedTimestamp() (ts uint64, init bool)

Summary

• ts == v.crossValidatedTs
• init iff ts != 0

ValidateAccessEntry

func (v *LockstepCrossValidator) ValidateAccessEntry(
	access types.Access,
	minSafety types.SafetyLevel,
	execDescriptor types.ExecutingDescriptor,
) (err error)

Summary

• err == nil iff
  • v.getMinIngestedTimestamp().ok
  • v.getMinIngestedTimestamp().ts >= access.Timestamp
  • if minSafety == types.CrossUnsafe then v.CrossValidatedTimestamp().init
  • if minSafety == types.CrossUnsafe then v.CrossValidatedTimestamp().ts >= access.Timestamp

  • validateMessageTiming(
        access.Timestamp,          // initTimestamp
         execDescriptor.Timestamp,  // inclusionTimestamp
         v.messageExpiryWindow,     // messageExpiryWindow
         execDescriptor.Timeout,    // timeout
         execDescriptor.Timestamp,  // execTimestamp
    ).err == nil

  • v.chains[access.ChainID].ok

  • ingester.Contains(types.ContainsQuery{
        Timestamp: access.Timestamp,
        BlockNum:  access.BlockNumber,
        LogIdx:    access.LogIndex,
        Checksum:  access.Checksum,
    }).err == nil

    where ingester == v.chains[access.ChainID].value

After substitutions:

• err == nil iff
  • len(v.chains) > 0
  • forall (ingester : v.chains)
    • ingester.Ready()
    • ingester.LatestTimestamp().ok
  • min (ingester : v.chains) ingester.LatestTimestamp().ts >= access.Timestamp
  • if minSafety == types.CrossUnsafe then
    • v.crossValidatedTs != 0
    • v.crossValidatedTs >= access.Timestamp

  •    access.Timestamp
    <  execDescriptor.Timestamp
    <= execDescriptor.Timestamp + execDescriptor.Timeout
    <= access.Timestamp + v.messageExpiryWindow
    

  • v.chains[access.ChainID].ok

  • i.Contains(types.ContainsQuery{
        Timestamp: access.Timestamp,
        BlockNum:  access.BlockNumber,
        LogIdx:    access.LogIndex,
        Checksum:  access.Checksum,
    }).err == nil

    where i == v.chains[access.ChainID].value

validateExecutingMessage

func (v *LockstepCrossValidator) validateExecutingMessage(
	execMsg *types.ExecutingMessage,
	inclusionTimestamp uint64,
) (err error)

Summary

• err == nil iff
  • v.chains[execMsg.ChainID].ok

  • validateMessageTiming(
        execMsg.Timestamp,      // initTimestamp
        inclusionTimestamp,     // inclusionTimestamp
        v.messageExpiryWindow,  // messageExpiryWindow
        0,                      // timeout
        0,                      // execTimestamp
    ).err == nil

  • ingester.Contains(types.ContainsQuery{
        Timestamp: execMsg.Timestamp,
        BlockNum:  execMsg.BlockNum,
        LogIdx:    execMsg.LogIdx,
        Checksum:  execMsg.Checksum,
    }).err == nil

    where ingester == v.chains[execMsg.ChainID].value

After substitutions:

• err == nil iff
  • v.chains[execMsg.ChainID].ok
  • execMsg.Timestamp < inclusionTimestamp <= execMsg.Timestamp + v.messageExpiryWindow

  • ingester.Contains(types.ContainsQuery{
        Timestamp: execMsg.Timestamp,
        BlockNum:  execMsg.BlockNum,
        LogIdx:    execMsg.LogIdx,
        Checksum:  execMsg.Checksum,
    }).err == nil

    where ingester == v.chains[execMsg.ChainID].value

validateTimestamp

func (v *LockstepCrossValidator) validateTimestamp(ts uint64) (err error)

Summary

• err == nil iff

  forall (ingester : v.chains)
  

  • ingester.GetExecMsgsAtTimestamp(ts).err == nil
    

  • forall (msg : ingester.GetExecMsgsAtTimestamp(ts).msgs) v.validateExecutingMessage(msg.ExecutingMessage, msg.InclusionTimestamp).err == nil
    

After substitutions:

• err == nil iff

  forall (ingester : v.chains)
  

  • ingester.GetExecMsgsAtTimestamp(ts).err == nil
    

  • forall (msg : ingester.GetExecMsgsAtTimestamp(ts).msgs)
    

    • v.chains[msg.ExecutingMessage.ChainID].ok
      

    • msg.ExecutingMessage.Timestamp < msg.InclusionTimestamp <= msg.ExecutingMessage.Timestamp + v.messageExpiryWindow
      

    • i.Contains(types.ContainsQuery{
          Timestamp: msg.ExecutingMessage.Timestamp,
          BlockNum:  msg.ExecutingMessage.BlockNum,
          LogIdx:    msg.ExecutingMessage.LogIdx,
          Checksum:  msg.ExecutingMessage.Checksum,
      }).err == nil

      where i == v.chains[msg.ExecutingMessage.ChainID].value

advanceValidation

func (v *LockstepCrossValidator) advanceValidation()

Summary

• If either

  • v.Error() != nil
  • exists (ingester : v.chains) where either
    • ingester.Error() != nil
    • !ingester.Ready()
  • !v.getMinIngestedTimestamp().ok
  • v.crossValidatedTs == 0 and v.startTimestamp == 0 (see LockstepCrossValidator never advances if startTimestamp is 0 #28)
  • v.crossValidatedTs >= v.getMinIngestedTimestamp().ts

  then

  next(v) == v
  

• Otherwise, if v.crossValidatedTs == 0 and v.startTimestamp != 0, then

  next(v) == { ...v, crossValidatedTs: v.startTimestamp }
  

• Otherwise, if

  forall (ts : [v.crossValidatedTs + 1 .. v.getMinIngestedTimestamp().ts]) v.validateTimestamp(ts) == nil
  

  then

  next(v) == { ...v, crossValidatedTs: v.getMinIngestedTimestamp().ts }
  

• Otherwise, let minimal

  ts : [v.crossValidatedTs + 1 .. v.getMinIngestedTimestamp().ts]
  

  such that v.validateTimestamp(ts) != nil. Then

  next(v) == { ...v, crossValidatedTs: ts - 1, err: e }
  

  for some e != nil

After substitutions:

• If either

  • v.Error() != nil
  • len(v.chains) == 0
  • exists (ingester : v.chains) where either
    • ingester.Error() != nil
    • !ingester.Ready()
    • !ingester.LatestTimestamp().ok
  • v.crossValidatedTs == 0 and v.startTimestamp == 0
  • v.crossValidatedTs >= min (ingester : v.chains) ingester.LatestTimestamp().ts

  then

  next(v) == v
  

• Otherwise, if v.crossValidatedTs == 0 and v.startTimestamp != 0, then

  next(v) == { ...v, crossValidatedTs: v.startTimestamp }
  

• Otherwise, if

  forall (ts : [v.crossValidatedTs + 1 .. min (ingester : v.chains) ingester.LatestTimestamp().ts]) (ingester : v.chains)
  

  • ingester.GetExecMsgsAtTimestamp(ts).err == nil
    

  • forall (msg : ingester.GetExecMsgsAtTimestamp(ts).msgs)
    

    • v.chains[msg.ExecutingMessage.ChainID].ok
      

    • msg.ExecutingMessage.Timestamp < msg.InclusionTimestamp <= msg.ExecutingMessage.Timestamp + v.messageExpiryWindow
      

    • i.Contains(types.ContainsQuery{
          Timestamp: msg.ExecutingMessage.Timestamp,
          BlockNum:  msg.ExecutingMessage.BlockNum,
          LogIdx:    msg.ExecutingMessage.LogIdx,
          Checksum:  msg.ExecutingMessage.Checksum,
      }).err == nil

      where i == v.chains[msg.ExecutingMessage.ChainID].value

  then

  next(v) == { ...v, crossValidatedTs: min (ingester : v.chains) ingester.LatestTimestamp().ts }
  

• Otherwise, let minimal

  ts : [v.crossValidatedTs + 1 .. min (ingester : v.chains) ingester.LatestTimestamp().ts]
  

  such that

  exists (ingester : v.chains)
  

  where either

  • ingester.GetExecMsgsAtTimestamp(ts).err != nil
    

  • exists (msg : ingester.GetExecMsgsAtTimestamp(ts).msgs)
    

    where either

    • !v.chains[msg.ExecutingMessage.ChainID].ok
      

    • msg.ExecutingMessage.Timestamp >= msg.InclusionTimestamp
      

    • msg.InclusionTimestamp > msg.ExecutingMessage.Timestamp + v.messageExpiryWindow
      

    • i.Contains(types.ContainsQuery{
          Timestamp: msg.ExecutingMessage.Timestamp,
          BlockNum:  msg.ExecutingMessage.BlockNum,
          LogIdx:    msg.ExecutingMessage.LogIdx,
          Checksum:  msg.ExecutingMessage.Checksum,
      }).err != nil

      where i == v.chains[msg.ExecutingMessage.ChainID].value

  Then

  next(v) == { ...v, crossValidatedTs: ts - 1, err: e }
  

  for some e != nil.