⛽ Gas_comparable_input_size.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.

Definition t : Set := int.

Module micheline_size.
  Record record : Set := Build {
    traversal : t;
    int_bytes : t;
    string_bytes : t;
  }.
  Definition with_traversal traversal (r : record) :=
    Build traversal r.(int_bytes) r.(string_bytes).
  Definition with_int_bytes int_bytes (r : record) :=
    Build r.(traversal) int_bytes r.(string_bytes).
  Definition with_string_bytes string_bytes (r : record) :=
    Build r.(traversal) r.(int_bytes) string_bytes.
End micheline_size.
Definition micheline_size := micheline_size.record.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv (fun (i_value : t) ⇒ Int64.of_int i_value)
    (fun (l_value : int64) ⇒ Int64.to_int l_value) None
    Data_encoding.int64_value.

Definition micheline_size_encoding : Data_encoding.encoding micheline_size :=
  Data_encoding.conv
    (fun (function_parameter : micheline_size) ⇒
      let '{|
        micheline_size.traversal := traversal;
          micheline_size.int_bytes := int_bytes;
          micheline_size.string_bytes := string_bytes
          |} := function_parameter in
      (traversal, int_bytes, string_bytes))
    (fun (function_parameter : t × t × t) ⇒
      let '(traversal, int_bytes, string_bytes) := function_parameter in
      {| micheline_size.traversal := traversal;
        micheline_size.int_bytes := int_bytes;
        micheline_size.string_bytes := string_bytes; |}) None
    (Data_encoding.tup3 encoding encoding encoding).

Definition zero : int := 0.

Definition add : int → int → int := Pervasives.op_plus.

Definition pp : Format.formatter → int → unit := Format.pp_print_int.

Definition pp_micheline_size
  (fmtr : Format.formatter) (function_parameter : micheline_size) : unit :=
  let '{|
    micheline_size.traversal := traversal;
      micheline_size.int_bytes := int_bytes;
      micheline_size.string_bytes := string_bytes
      |} := function_parameter in
  Format.fprintf fmtr
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            CamlinternalFormatBasics.End_of_format ""))
        (CamlinternalFormatBasics.String_literal "{ traversal = "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Char_literal ";" % char
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@;" 1 0)
                (CamlinternalFormatBasics.String_literal " int_bytes = "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal ";" % char
                      (CamlinternalFormatBasics.Formatting_lit
                        (CamlinternalFormatBasics.Break "@;" 1 0)
                        (CamlinternalFormatBasics.String_literal
                          " string_bytes = "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal ";" % char
                              (CamlinternalFormatBasics.Formatting_lit
                                (CamlinternalFormatBasics.Break "@," 0 0)
                                (CamlinternalFormatBasics.Char_literal
                                  "}" % char
                                  (CamlinternalFormatBasics.Formatting_lit
                                    CamlinternalFormatBasics.Close_box
                                    CamlinternalFormatBasics.End_of_format)))))))))))))))
      "@[{ traversal = %a;@; int_bytes = %a;@; string_bytes = %a;@,}@]") pp
    traversal pp int_bytes pp string_bytes.

Definition to_int {A : Set} (x_value : A) : A := x_value.

Definition of_int {A : Set} (x_value : A) : A := x_value.

Definition unit_value : t := 1.

Definition integer (i_value : Alpha_context.Script_int.num) : t :=
  (Z.numbits (Alpha_context.Script_int.to_zint i_value)) /i 8.

Definition string_value : string → int := String.length.

Definition script_string : Alpha_context.Script_string.t → int :=
  Alpha_context.Script_string.length.

Definition bytes_value (b_value : Bytes.t) : t := Bytes.length b_value.

Definition mutez (_tez : Alpha_context.Tez.tez) : t := 8.

Definition bool_value (function_parameter : bool) : t :=
  let '_ := function_parameter in
  1.

Definition signature (_signature : Script_typed_ir.Script_signature.t) : t :=
  Script_typed_ir.Script_signature.size_value.

Definition key_hash (_keyhash : Signature.public_key_hash) : t :=
  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value).

Definition public_key (public_key : Signature.public_key) : t :=
  Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.size_value) public_key.

Definition chain_id (_chain_id : Script_typed_ir.Script_chain_id.t) : t :=
  Script_typed_ir.Script_chain_id.size_value.

Definition address (addr : Script_typed_ir.address) : t :=
  let entrypoint := addr.(Script_typed_ir.address.entrypoint) in
  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) +i
  (String.length (Alpha_context.Entrypoint.to_string entrypoint)).

Definition tx_rollup_l2_address
  (x_value : Indexable.t Tx_rollup_l2_address.address) : int :=
  Tx_rollup_l2_address.Indexable.size_value (Indexable.forget x_value).

Definition timestamp (tstamp : Alpha_context.Script_timestamp.t) : t :=
  (Z.numbits (Alpha_context.Script_timestamp.to_zint tstamp)) /i 8.

Axiom size_of_comparable_value : ∀ {a : Set},
  Script_typed_ir.comparable_ty → a → t.