🐆 Tx_rollup_hash_builder.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_list_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_repr.

Definition message (ctxt : Raw_context.t) (input : Tx_rollup_message_repr.t)
  : M? (Raw_context.t × Tx_rollup_message_hash_repr.t) :=
  Tx_rollup_gas.hash_value
    (let arg := Tx_rollup_message_hash_repr.hash_bytes in
    fun (eta : list bytes) ⇒ arg None eta) ctxt Tx_rollup_message_repr.encoding
    input.

Definition message_result
  (ctxt : Raw_context.t) (input : Tx_rollup_message_result_repr.t)
  : M? (Raw_context.t × Tx_rollup_message_result_hash_repr.t) :=
  Tx_rollup_gas.hash_value
    (let arg := Tx_rollup_message_result_hash_repr.hash_bytes in
    fun (eta : list bytes) ⇒ arg None eta) ctxt
    Tx_rollup_message_result_repr.encoding input.

Definition compact_commitment
  (ctxt : Raw_context.t) (input : Tx_rollup_commitment_repr.Compact.t)
  : M? (Raw_context.t × Tx_rollup_commitment_repr.Hash.t) :=
  Tx_rollup_gas.hash_value
    (let arg := Tx_rollup_commitment_repr.Hash.hash_bytes in
    fun (eta : list bytes) ⇒ arg None eta) ctxt
    Tx_rollup_commitment_repr.Compact.encoding input.

Definition withdraw_list
  (ctxt : Raw_context.t) (input : list Tx_rollup_withdraw_repr.t)
  : M? (Raw_context.t × Tx_rollup_withdraw_list_hash_repr.t) :=
  Tx_rollup_gas.hash_value
    (let arg := Tx_rollup_withdraw_list_hash_repr.hash_bytes in
    fun (eta : list bytes) ⇒ arg None eta) ctxt
    (Data_encoding.list_value None Tx_rollup_withdraw_repr.encoding) input.