⛽ 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.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
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 : Script_int.num) : t :=
(Z.numbits (Script_int.to_zint i_value)) /i 8.
Definition string_value : string → int := String.length.
Definition script_string : Script_string.t → int := 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 : Script_timestamp.t) : t :=
(Z.numbits (Script_timestamp.to_zint tstamp)) /i 8.
#[bypass_check(guard)]
Fixpoint size_of_comparable_value {a : Set}
(wit : Script_typed_ir.comparable_ty) (v_value : a) {struct wit} : t :=
match (wit, v_value) with
| (Script_typed_ir.Unit_t, _) ⇒ unit_value
| (Script_typed_ir.Int_t, v_value) ⇒
let v_value := cast Script_int.num v_value in
integer v_value
| (Script_typed_ir.Nat_t, v_value) ⇒
let v_value := cast Script_int.num v_value in
integer v_value
| (Script_typed_ir.String_t, v_value) ⇒
let v_value := cast Script_string.t v_value in
script_string v_value
| (Script_typed_ir.Bytes_t, v_value) ⇒
let v_value := cast bytes v_value in
bytes_value v_value
| (Script_typed_ir.Mutez_t, v_value) ⇒
let v_value := cast Tez_repr.t v_value in
mutez v_value
| (Script_typed_ir.Bool_t, v_value) ⇒
let v_value := cast bool v_value in
bool_value v_value
| (Script_typed_ir.Key_hash_t, v_value) ⇒
let v_value := cast Signature.public_key_hash v_value in
key_hash v_value
| (Script_typed_ir.Timestamp_t, v_value) ⇒
let v_value := cast Script_timestamp.t v_value in
timestamp v_value
| (Script_typed_ir.Address_t, v_value) ⇒
let v_value := cast Script_typed_ir.address v_value in
address v_value
| (Script_typed_ir.Tx_rollup_l2_address_t, v_value) ⇒
let v_value := cast Script_typed_ir.tx_rollup_l2_address v_value in
tx_rollup_l2_address v_value
| (Script_typed_ir.Pair_t leaf node_value _ Dependent_bool.YesYes, v_value) ⇒
let 'existT _ [__0, __1] [v_value, node_value, leaf] :=
cast_exists (Es := [Set ** Set])
(fun '[__0, __1] ⇒
[__0 × __1 ** Script_typed_ir.ty ** Script_typed_ir.ty])
[v_value, node_value, leaf] in
let '(lv, rv) := v_value in
let size_value :=
(size_of_comparable_value leaf lv) +i
(size_of_comparable_value node_value rv) in
size_value +i 1
| (Script_typed_ir.Union_t _left _right _ Dependent_bool.YesYes, v_value) ⇒
let 'existT _ [__2, __3] [v_value, _right, _left] :=
cast_exists (Es := [Set ** Set])
(fun '[__2, __3] ⇒
[Script_typed_ir.union __2 __3 ** Script_typed_ir.ty **
Script_typed_ir.ty]) [v_value, _right, _left] in
let size_value :=
match v_value with
| Script_typed_ir.L v_value ⇒ size_of_comparable_value _left v_value
| Script_typed_ir.R v_value ⇒ size_of_comparable_value _right v_value
end in
size_value +i 1
| (Script_typed_ir.Option_t ty_value _ Dependent_bool.Yes, v_value) ⇒
let 'existT _ __4 [v_value, ty_value] :=
cast_exists (Es := Set) (fun __4 ⇒ [option __4 ** Script_typed_ir.ty])
[v_value, ty_value] in
match v_value with
| None ⇒ 1
| Some x_value ⇒ (size_of_comparable_value ty_value x_value) +i 1
end
| (Script_typed_ir.Signature_t, v_value) ⇒
let v_value := cast Script_typed_ir.signature v_value in
signature v_value
| (Script_typed_ir.Key_t, v_value) ⇒
let v_value := cast Signature.public_key v_value in
public_key v_value
| (Script_typed_ir.Chain_id_t, v_value) ⇒
let v_value := cast Script_typed_ir.Script_chain_id.t v_value in
chain_id v_value
| _ ⇒ unreachable_gadt_branch
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
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 : Script_int.num) : t :=
(Z.numbits (Script_int.to_zint i_value)) /i 8.
Definition string_value : string → int := String.length.
Definition script_string : Script_string.t → int := 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 : Script_timestamp.t) : t :=
(Z.numbits (Script_timestamp.to_zint tstamp)) /i 8.
#[bypass_check(guard)]
Fixpoint size_of_comparable_value {a : Set}
(wit : Script_typed_ir.comparable_ty) (v_value : a) {struct wit} : t :=
match (wit, v_value) with
| (Script_typed_ir.Unit_t, _) ⇒ unit_value
| (Script_typed_ir.Int_t, v_value) ⇒
let v_value := cast Script_int.num v_value in
integer v_value
| (Script_typed_ir.Nat_t, v_value) ⇒
let v_value := cast Script_int.num v_value in
integer v_value
| (Script_typed_ir.String_t, v_value) ⇒
let v_value := cast Script_string.t v_value in
script_string v_value
| (Script_typed_ir.Bytes_t, v_value) ⇒
let v_value := cast bytes v_value in
bytes_value v_value
| (Script_typed_ir.Mutez_t, v_value) ⇒
let v_value := cast Tez_repr.t v_value in
mutez v_value
| (Script_typed_ir.Bool_t, v_value) ⇒
let v_value := cast bool v_value in
bool_value v_value
| (Script_typed_ir.Key_hash_t, v_value) ⇒
let v_value := cast Signature.public_key_hash v_value in
key_hash v_value
| (Script_typed_ir.Timestamp_t, v_value) ⇒
let v_value := cast Script_timestamp.t v_value in
timestamp v_value
| (Script_typed_ir.Address_t, v_value) ⇒
let v_value := cast Script_typed_ir.address v_value in
address v_value
| (Script_typed_ir.Tx_rollup_l2_address_t, v_value) ⇒
let v_value := cast Script_typed_ir.tx_rollup_l2_address v_value in
tx_rollup_l2_address v_value
| (Script_typed_ir.Pair_t leaf node_value _ Dependent_bool.YesYes, v_value) ⇒
let 'existT _ [__0, __1] [v_value, node_value, leaf] :=
cast_exists (Es := [Set ** Set])
(fun '[__0, __1] ⇒
[__0 × __1 ** Script_typed_ir.ty ** Script_typed_ir.ty])
[v_value, node_value, leaf] in
let '(lv, rv) := v_value in
let size_value :=
(size_of_comparable_value leaf lv) +i
(size_of_comparable_value node_value rv) in
size_value +i 1
| (Script_typed_ir.Union_t _left _right _ Dependent_bool.YesYes, v_value) ⇒
let 'existT _ [__2, __3] [v_value, _right, _left] :=
cast_exists (Es := [Set ** Set])
(fun '[__2, __3] ⇒
[Script_typed_ir.union __2 __3 ** Script_typed_ir.ty **
Script_typed_ir.ty]) [v_value, _right, _left] in
let size_value :=
match v_value with
| Script_typed_ir.L v_value ⇒ size_of_comparable_value _left v_value
| Script_typed_ir.R v_value ⇒ size_of_comparable_value _right v_value
end in
size_value +i 1
| (Script_typed_ir.Option_t ty_value _ Dependent_bool.Yes, v_value) ⇒
let 'existT _ __4 [v_value, ty_value] :=
cast_exists (Es := Set) (fun __4 ⇒ [option __4 ** Script_typed_ir.ty])
[v_value, ty_value] in
match v_value with
| None ⇒ 1
| Some x_value ⇒ (size_of_comparable_value ty_value x_value) +i 1
end
| (Script_typed_ir.Signature_t, v_value) ⇒
let v_value := cast Script_typed_ir.signature v_value in
signature v_value
| (Script_typed_ir.Key_t, v_value) ⇒
let v_value := cast Signature.public_key v_value in
public_key v_value
| (Script_typed_ir.Chain_id_t, v_value) ⇒
let v_value := cast Script_typed_ir.Script_chain_id.t v_value in
chain_id v_value
| _ ⇒ unreachable_gadt_branch
end.