Prototype of BFT abstractions and Streamlet; add static type checking

[daira]

fixes #6
fixes #23

[daira]

Suggested change

	self.assertTrue(proposal.is_valid())
	proposal.assert_valid()
	self.assertTrue(proposal.is_valid())

[nathan-at-least]

Why are both lines necessary? Is this "verification-in-depth" which redundantly checks the same condition through different code paths, or are those checks intentionally distinct?

[daira]

We call proposal.assert_valid() first because if the proposal is (incorrectly) not valid, that will tell us why — whereas is_valid() will catch the exception and lose error information. Then we test that is_valid() is implemented correctly for the True case.

[nathan-at-least]

I still don't understand the second statement.

Aren't the two lines entirely equivalent, so long as assert_valid is defined as follows?

def assert_valid(self):
  assert self.is_valid()

I just looked it up, and it seems equivalent, though the dependency is inverted so we have:

    def is_valid(self) -> bool:
        """Is this proposal valid?"""
        try:
            self.assert_valid()
            return True
        except AssertionError:
            return False

My question is "is there ever a case where assert_valid and is_valid will not be entirely equivalent modulo boolean return vs raising AssertionError?

That could be the case if a subclass of PermissionedBFTProposal overrides both methods and makes them logically non-equivalent. So I would refine my question to these two clauses:

• Is it possible / useful for subclasses to override these two methods in a manner in which they aren't logically equivalent (modulo raise-vs-return)?
• If not, is the purpose of these two lines to ensure all subclasses have implemented those two methods as logically equivalent (module raise-vs-return)?

If the answer to the first clause is 'no', then we could add a doc string or maybe a type signature to def is_valid to prohibit overriding that method as a maintenance improvement / clarification.

[nathan-at-least]

UtACK, with one (repeated) clarification question.

Type annotations are super helpful for me! Thanks.

[nathan-at-least]

Why are both lines necessary? Is this "verification-in-depth" which redundantly checks the same condition through different code paths, or are those checks intentionally distinct?