🐆 Tx_rollup_l2_address.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.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Indexable.

Inclusion of the module [Bls.Public_key_hash]

Definition t := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t).

Definition pp := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp).

Definition pp_short :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short).

Definition op_eq := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_eq).

Definition op_ltgt := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_ltgt).

Definition op_lt := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lt).

Definition op_lteq := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lteq).

Definition op_gteq := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gteq).

Definition op_gt := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gt).

Definition compare := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare).

Definition equal := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal).

Definition max := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.max).

Definition min := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.min).

Definition to_bytes :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes).

Definition of_bytes_opt :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt).

Definition of_bytes_exn :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_exn).

Definition to_b58check :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check).

Definition to_short_b58check :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_short_b58check).

Definition of_b58check_exn :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_exn).

Definition of_b58check_opt :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt).

Definition b58check_encoding :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.b58check_encoding).

Definition encoding :=
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding).

Definition rpc_arg := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg).

Definition zero := Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero).

Definition address : Set := t.

Definition in_memory_size (function_parameter : t)
  : Cache_memory_helpers.sint :=
  let '_ := function_parameter in
  Cache_memory_helpers.op_plusexclamation
    (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
      Cache_memory_helpers.word_size)
    (Cache_memory_helpers.string_size_gen
      Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value)).

Definition size_value {A : Set} (function_parameter : A) : int :=
  let '_ := function_parameter in
  Bls.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value).

Module Indexable.
  Definition Indexable_Make_include :=
    Indexable.Make
      (let t : Set := t in
      {|
        Indexable.VALUE.encoding := encoding;
        Indexable.VALUE.compare := compare;
        Indexable.VALUE.pp := pp
      |}).

Inclusion of the module [Indexable_Make_include]

  Definition t := Indexable_Make_include.(Indexable.INDEXABLE.t).

  Definition index := Indexable_Make_include.(Indexable.INDEXABLE.index).

  Definition value := Indexable_Make_include.(Indexable.INDEXABLE.value).

  Definition either := Indexable_Make_include.(Indexable.INDEXABLE.either).

  Definition value_value :=
    Indexable_Make_include.(Indexable.INDEXABLE.value_value).

  Definition index_value :=
    Indexable_Make_include.(Indexable.INDEXABLE.index_value).

  Definition index_exn :=
    Indexable_Make_include.(Indexable.INDEXABLE.index_exn).

  Definition compact := Indexable_Make_include.(Indexable.INDEXABLE.compact).

  Definition encoding := Indexable_Make_include.(Indexable.INDEXABLE.encoding).

  Definition index_encoding :=
    Indexable_Make_include.(Indexable.INDEXABLE.index_encoding).

  Definition value_encoding :=
    Indexable_Make_include.(Indexable.INDEXABLE.value_encoding).

  Definition compare :=
    Indexable_Make_include.(Indexable.INDEXABLE.compare)
      .

  Definition compare_values :=
    Indexable_Make_include.(Indexable.INDEXABLE.compare_values).

  Definition compare_indexes :=
    Indexable_Make_include.(Indexable.INDEXABLE.compare_indexes).

  Definition pp :=
    Indexable_Make_include.(Indexable.INDEXABLE.pp) .

  Definition in_memory_size (x_value : Indexable.t)
    : Cache_memory_helpers.sint :=
    Indexable.in_memory_size in_memory_size x_value.

  Definition size_value (x_value : Indexable.t) : int :=
    Indexable.size_value size_value x_value.
End Indexable.