🐆 Tx_rollup_hash_builder.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_hash_builder.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_message_result_repr.

The function [withdraw_list] is valid.

Lemma withdraw_list_is_valid ctxt input :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt,_) := Tx_rollup_hash_builder.withdraw_list ctxt input in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [message_result] is valid.

Lemma message_result_is_valid ctxt input :
  Raw_context.Valid.t ctxt →
  letP? '(ctxt,_) :=
    Tx_rollup_hash_builder.message_result ctxt input in
  Raw_context.Valid.t ctxt.
Proof.
  intro Hctxt.
  eapply Tx_rollup_gas.hash_value_is_valid.
  { assumption. }
  { exact Tx_rollup_message_result_repr.encoding_is_valid. }
  { exact I. }
Qed.