Skip to main content

🐆 Tx_rollup_message_hash_repr.v

Proofs

See code, Gitlab , OCaml

[compare] function is valid
Lemma compare_is_valid :
  Compare.Valid.t (fun _True) id Tx_rollup_message_hash_repr.compare.
Proof.
  apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.