⛽ Gas_input_size.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Gas_comparable_input_size.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_set.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Include Gas_comparable_input_size.

Definition list_value {a : Set} (list_value : Script_list.t a) : t :=
  list_value.(Script_list.t.length).

Definition set {a : Set} (set : Script_typed_ir.set a) : M? t :=
  let res := Script_int.to_int (Script_set.size_value set) in
  match res with
  | None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
  | Some x_value ⇒ return? x_value
  end.

Definition map {a b : Set} (map : Script_typed_ir.map a b) : M? t :=
  let res := Script_int.to_int (Script_map.size_value map) in
  match res with
  | None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
  | Some x_value ⇒ return? x_value
  end.

Definition micheline_zero : micheline_size :=
  {| Gas_comparable_input_size.micheline_size.traversal := 0;
    Gas_comparable_input_size.micheline_size.int_bytes := 0;
    Gas_comparable_input_size.micheline_size.string_bytes := 0; |}.

Definition op_plusplus (x_value : micheline_size) (y_value : micheline_size)
  : micheline_size :=
  {|
    Gas_comparable_input_size.micheline_size.traversal :=
      x_value.(Gas_comparable_input_size.micheline_size.traversal) +i
      y_value.(Gas_comparable_input_size.micheline_size.traversal);
    Gas_comparable_input_size.micheline_size.int_bytes :=
      x_value.(Gas_comparable_input_size.micheline_size.int_bytes) +i
      y_value.(Gas_comparable_input_size.micheline_size.int_bytes);
    Gas_comparable_input_size.micheline_size.string_bytes :=
      x_value.(Gas_comparable_input_size.micheline_size.string_bytes) +i
      y_value.(Gas_comparable_input_size.micheline_size.string_bytes); |}.

Definition node_value (leaves : list micheline_size) : micheline_size :=
  let r_value := List.fold_left op_plusplus micheline_zero leaves in
  Gas_comparable_input_size.micheline_size.with_traversal
    (r_value.(Gas_comparable_input_size.micheline_size.traversal) +i 1) r_value.

#[bypass_check(guard)]
Fixpoint of_micheline {a b : Set} (x_value : Micheline.node a b)
  {struct x_value} : micheline_size :=
  match x_value with
  | Micheline.Int _loc z_value ⇒
    let int_bytes := integer (Script_int.of_zint z_value) in
    {| Gas_comparable_input_size.micheline_size.traversal := 1;
      Gas_comparable_input_size.micheline_size.int_bytes := int_bytes;
      Gas_comparable_input_size.micheline_size.string_bytes := 0; |}
  | Micheline.String _loc s_value ⇒
    let string_bytes := String.length s_value in
    {| Gas_comparable_input_size.micheline_size.traversal := 1;
      Gas_comparable_input_size.micheline_size.int_bytes := 0;
      Gas_comparable_input_size.micheline_size.string_bytes := string_bytes; |}
  | Micheline.Bytes _loc b_value ⇒
    let string_bytes := bytes_value b_value in
    {| Gas_comparable_input_size.micheline_size.traversal := 1;
      Gas_comparable_input_size.micheline_size.int_bytes := 0;
      Gas_comparable_input_size.micheline_size.string_bytes := string_bytes; |}
  | Micheline.Prim _loc _prim subterms _annot ⇒
    node_value (List.map of_micheline subterms)
  | Micheline.Seq _loc subterms ⇒ node_value (List.map of_micheline subterms)
  end.

Definition sapling_transaction_inputs (tx : Alpha_context.Sapling.transaction)
  : t := List.length tx.(Sapling.UTXO.transaction.inputs).

Definition sapling_transaction_outputs (tx : Alpha_context.Sapling.transaction)
  : t := List.length tx.(Sapling.UTXO.transaction.outputs).

Definition sapling_transaction_bound_data
  (tx : Alpha_context.Sapling.transaction) : t :=
  String.length tx.(Sapling.UTXO.transaction.bound_data).