Define Maia grammars for messages

[LivInTheLookingGlass]

This is our current definition (as near as I can tell). I chose Maia for this because it allows for limited context sensitivity, rather than needing a semantic analyzer in addition. This should make my grammar Bounded Enumerable.

EncodedMessage = TupleLength SerializedTuple ;
SerializedTuple = TupleItem TupleItem TupleItem TupleItem TupleItem* ;
TupleItem = TupleLength .{TupleLength} ;
TupleLength = UnsignedBigEndianInt{4} ;

forEvery EncodedMessage : length(SerializedTuple) == TupleLength ;
forEvery TupleItem : length(TupleItem) == TupleLength ;

// SerializedTuple item 1 is pathfinding header
// SerializedTuple item 2 is sender ID
// SerializedTuple item 3 is checksum
// SerializedTuple item 4 is timestamp
// SerializedTuple item 5+ are user defined payload

[LivInTheLookingGlass]

The proposal in #113 would come out to be significantly more complicated.

EncodedMessage = TupleLength SerializedTuple ;
SerializedTuple = TupleItem TupleItem TupleItem TupleItem TupleItem* ;
TupleItem = TupleLength TupleType SerializedItem ;
TupleLength = UnsignedBigEndianInt{4} ;
TupleType = UnsignedBigEndianInt{1} ;
SerializedItem = UnsignedBigEndianInt{1} |
                 UnsignedBigEndianInt{2} |
                 UnsignedBigEndianInt{4} |
                 UnsignedBigEndianInt{8} |
                 BigEndianInt{1} |
                 BigEndianInt{2} |
                 BigEndianInt{4} |
                 BigEndianInt{8} |
                 SerializedTuple |
                 BigInt |
                 .* ;
BigInt = ('+' | '-') .+ ;

forEvery EncodedMessage : length(SerializedTuple) == TupleLength ;
forEvery TupleItem : length(SerializedItem) == TupleLength ;

// Typing schemes
forEvery TupleItem : (TupleType == 0x33 or TupleType == 0x34) implies length(SerializedItem) == 1 ;
forEvery TupleItem : (TupleType == 0x35 or TupleType == 0x36) implies length(SerializedItem) == 2 ;
forEvery TupleItem : (TupleType == 0x37 or TupleType == 0x38) implies length(SerializedItem) == 4 ;
forEvery TupleItem : (TupleType == 0x39 or TupleType == 0x3A) implies length(SerializedItem) == 8 ;
forEvery TupleItem : (TupleType == 0x32) implies length(SerializedItem) >= 10 and SerializedItem[0] in < '+', '-' > ;

// SerializedTuple item 1 is pathfinding header
// SerializedTuple item 2 is sender ID
// SerializedTuple item 3 is checksum
// SerializedTuple item 4 is timestamp
// SerializedTuple item 5+ are user defined payload

[LivInTheLookingGlass]

The proposal in #84 would look like:

EncodedMessage = shortLength TupleLength SerializedTuple ;
SerializedTuple = TupleItem TupleItem TupleItem TupleItem TupleItem* ;
TupleItem = shortLength TupleLength SerializedItem ;
shortItem = UnsignedBigEndianInt{1}
TupleLength = UnsignedBigEndianInt{shortLength} ;
SerializedItem = .{TupleLength}

// These rules are redundant for clarity
forEvery EncodedMessage : length(TupleLength) == shortLength ;
forEvery EncodedMessage : length(SerializedTuple) == TupleLength ;
forEvery TupleItem : length(TupleLength) == shotLength ;
forEvery TupleItem : length(SerializedItem) == TupleLength ;

// SerializedTuple item 1 is pathfinding header
// SerializedTuple item 2 is sender ID
// SerializedTuple item 3 is checksum
// SerializedTuple item 4 is timestamp
// SerializedTuple item 5+ are user defined payload

This definition would restrict TupleLengths to being either 1, 2, 4, or 8 bytes long

[LivInTheLookingGlass]

Combining #113 and #84 would look like:

EncodedMessage = shortLength TupleLength SerializedTuple ;
SerializedTuple = TupleItem TupleItem TupleItem TupleItem TupleItem* ;
TupleItem = shortLength TupleLength TupleType SerializedItem ;
shortLength = UnsignedBigEndianInt{1} ;
TupleLength = UnsignedBigEndianInt{shortLength} ;
TupleType = UnsignedBigEndianInt{1} ;
SerializedItem = UnsignedBigEndianInt{1} |
                 UnsignedBigEndianInt{2} |
                 UnsignedBigEndianInt{4} |
                 UnsignedBigEndianInt{8} |
                 BigEndianInt{1} |
                 BigEndianInt{2} |
                 BigEndianInt{4} |
                 BigEndianInt{8} |
                 SerializedTuple |
                 BigInt |
                 .* ;
BigInt = ('+' | '-') .+ ;

forEvery EncodedMessage : length(TupleLength) == shortLength ;
forEvery EncodedMessage : length(SerializedTuple) == TupleLength ;
forEvery TupleItem : length(TupleLength) == shotLength ;
forEvery TupleItem : length(SerializedItem) == TupleLength ;

// Typing schemes
forEvery TupleItem : (TupleType == 0x33 or TupleType == 0x34) implies length(SerializedItem) == 1 ;
forEvery TupleItem : (TupleType == 0x35 or TupleType == 0x36) implies length(SerializedItem) == 2 ;
forEvery TupleItem : (TupleType == 0x37 or TupleType == 0x38) implies length(SerializedItem) == 4 ;
forEvery TupleItem : (TupleType == 0x39 or TupleType == 0x3A) implies length(SerializedItem) == 8 ;
forEvery TupleItem : (TupleType == 0x32) implies length(SerializedItem) >= 10 and SerializedItem[0] in < '+', '-' > ;

// SerializedTuple item 1 is pathfinding header
// SerializedTuple item 2 is sender ID
// SerializedTuple item 3 is checksum
// SerializedTuple item 4 is timestamp
// SerializedTuple item 5+ are user defined payload

This definition would restrict TupleLengths to being either 1, 2, 4, or 8 bytes long

[LivInTheLookingGlass]

This is probably irrelevant if I switch to msgpack