Replace assert with custom require method

[hwwhww]

Replace #2045
Fix #1797

Starting with phase0/beacon-chain.md

Proposed solution

• Replace assert <condition> with custom require(condition: bool, message: str=None) function to signal that the execution is INVALID. Implementers can define their custom error handling method.
• Move some comments to the message field.
• Note that it should be no substantive change.

/cc @ericsson49

[hwwhww]

Strictly speaking, it should be Optional[str] in Python:

Suggested change

	def require(condition: bool, message: str=None) -> None:
	from typing import Optional
	def require(condition: bool, message: Optional[str]=None) -> None:

• Python Optional might be confusing for the readers. Although Optional has been used in validator.md and das-core.md anyway...
• mypy may raise an error if we use a stricter config

I'm fine either way for now.

[CarlBeek]

We could force implicit optionals (https://mypy.readthedocs.io/en/stable/config_file.html#none-and-optional-handling) in the linter.ini

[hwwhww]

@djrtwo

I started with phase0/beacon-chain.md. I'd love to get a green light before working on other spec files. 🙏

[hwwhww]

All asserts under specs folder are replaced with requires.
I updated each file per commit, but please squash them when merging it.

[samlaf]

Curious what's the latest on this? Why do the specs still contain asserts instead of requires?
And how is the dafny team going around this: #1797 ?
Are they just using their own versions of the specs for formal verification?

[ericsson49]

And how is the dafny team going around this: #1797 ? Are they just using their own versions of the specs for formal verification?

Can't say I'm a member of the Dafny team, but I'm working on a transpiler from a subset of Python to Dafny.
I believe "using their own versions of the specs for formal verification" is the correct state of affairs.
My goal is to change this so that specs versions used for formal verification are obtained via a thoroughly tested mechanized translation (i.e. the transpiler from a subset of Python to Dafny).
I personally translate assert to pyassert method in Dafny, which is similar to the requires, with the "exception" that there is only one kind of Exception in Dafny world right now, which doesn't take any argument. Such restriction may seem artificial, but I don't think we really need more expressive exceptions right now.
However, it's more complicated in practice. For "functional pure" translation, assert is more like "abort transaction", i.e. any heap object update that happened before raising an exception is lost.
It may seem strange, but the idea is that "imperative impure" translation should stay as close as possible to Python code - which is interpreted as a reference implementation, while the "functional pure" version should be as close as possible to the intended specification.
The proof obligations should ensure that both variants agree:

• on whether an exception should be raised or not
• if no exception is raised, on respective outcomes (i.e. returned values plus heap object updates)

See also the discussion in #1409 . It includes @franck44 's comment on how they deal with assert in their Dafny code.

Hope that helps.