Rename/move testing lang about cbc-casper HOT 10 CLOSED

Hi! check out casper/testing_language.py. You can see where the letters are registered against different functions.

Note that this issue is a discussion on overhauling the testing language to make it more generic across protocols and extensible in the case that you want to add things beyond the basis of a Make/Send. So keep that in mind when groking the existing test lang.

from cbc-casper.

agreed in general! Would love to chat it through.

from cbc-casper.

WIP spec for the protocol state language. In the base language, there are 4 "commands:" M, S, E, and I.

M: make a block. M1-A says: "validator 1 make a block named A."
S: send a block. S2-A says: "send validator 2 the block named A."
E: equivocate. E1-A\(A, B, C) says: "validator 1 make a block named A, where you pretend you haven't seen A, B, and C."
I: make an invalid block. I1-A says: "validator 1 make an invalid block named A."

Some validity rules:

1. A message can only be sent after it is created (by M, E, or I).
2. Two messages cannot be created with the same name.

Other notes:

1. I wonder if we can combine all block generation into a single command. I don't think having I is necessary (b/c in many cases, it could be making an invalid block rather than an equivocation).
2. Is it worth moving specifying the initial validator set into the language?
3. How can we specify validator set changes in the language?

There's absolutely a more rigorous way of defining this - with a CFG or something. Will work on this + get some feedback. Interestingly, it's not a regular language! Also, strangely, I think I can come up with a CFG that specifies the production rules for a CFG that specifies this language. This is b/c the production rules are likely infinite... shot in the dark here though.

from cbc-casper.

A few notes:

• Syntax for E looks reasonable. I would just use one deliminator -- white space or comma, not both.
• I for DOSing the network?
• Would your E example be invalid? Even if the validator is pretending he hasn't seen A, we should probably not allow for a block name collision in the testing language.

from cbc-casper.

You're right that E would be invalid in the above. I think we can simplify the language to just M and S and I.

M: make a block. M1-A says: "validator 1 make a block named A." M1-B\(A) says: "validator 1 make a block B without A in view." M1-C\(A,B) says: "validator 1 make block C without A and B in view." This allows you to equivocate and make invalid blocks as you want.
S: send a block. S2-A says: "send validator 2 the block named A."
I: make an invalid block. I1-A says: "validator 1 make an invalid block named A." This is invalid in a very specific way - we can make it so it is missing some field or something.

This allows us to specify that vast majority of protocols states, excluding certain cases where messages were invalid for other reasons (e.g. their estimate is not justified). As all invalid messages are "caught at the door" and all are treated the same (at least this is the case now), this isn't really a concern IMO.

The validity rules are pretty similar:

1. A message can only be sent after it is created (by M or I).
2. Two messages cannot be created with the same name.

from cbc-casper.

LGTM.

Just want to point out that I doesn't even really change the protocol state at least from the perspective of views, justifications, estimates, etc. It really only is an annoyance (unless a protocol chooses to punish these I message for whatever reason) given that clients have the tools to assess whether it is invalid.

That said, it might be useful in testing certain things (dos), etc

from cbc-casper.

@djrtwo sounds good. I could change state, as it means a validator who receives this invalid message would slash the validator who made this message...

Going to get a core PR up in the next couple of days for this.

from cbc-casper.

right right. If the generation of I is incorporated into the headers of any other message for punishments or otherwise, then agreed. And if that is a potential in designing a cbc casper protocol, then it should be a part of the language

from cbc-casper.

This looks really cool! Scanning over the code and sort of understanding what is going on. What is the best way to start playing with it? Would love to add a guide to the README for test lang. I see test_test_lang.py but still a little unsure.

from cbc-casper.

Addressed in the test lang PR. Closing.

from cbc-casper.