This PR improves the hax proofs by removing some admitted parts. It focuses on the v1 module and chain.rs. The main improvements come from the use of refinement types, and from some hax improvements around loops and more (not released yet which is why this is a draft PR for now).
Co-authored-by: Maxime Buyse <maxime@cryspen.com>
Co-authored-by: maximebuyse <45398004+maximebuyse@users.noreply.github.com>
