Formalize fork-choice algorithm and state transition function in Lean4

[MegaRedHand]

We want to formalize the core consensus logic in Lean4 to prove its properties.

This issue is mainly a placeholder. More details will be added later.