🍬 Script_repr.v
Translated 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.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Definition location : Set := Micheline.canonical_location.
Definition location_encoding
: Data_encoding.encoding Micheline.canonical_location :=
Micheline.canonical_location_encoding.
Definition annot : Set := Micheline.annot.
Definition expr : Set := Micheline.canonical Michelson_v1_primitives.prim.
Definition lazy_expr : Set := Data_encoding.lazy_t expr.
Definition michelson_node (location : Set) : Set :=
Micheline.node location Michelson_v1_primitives.prim.
Definition node : Set := michelson_node location.
Definition expr_encoding
: Data_encoding.encoding (Micheline.canonical Michelson_v1_primitives.prim) :=
Micheline.canonical_encoding "michelson_v1"
Michelson_v1_primitives.prim_encoding.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Definition location : Set := Micheline.canonical_location.
Definition location_encoding
: Data_encoding.encoding Micheline.canonical_location :=
Micheline.canonical_location_encoding.
Definition annot : Set := Micheline.annot.
Definition expr : Set := Micheline.canonical Michelson_v1_primitives.prim.
Definition lazy_expr : Set := Data_encoding.lazy_t expr.
Definition michelson_node (location : Set) : Set :=
Micheline.node location Michelson_v1_primitives.prim.
Definition node : Set := michelson_node location.
Definition expr_encoding
: Data_encoding.encoding (Micheline.canonical Michelson_v1_primitives.prim) :=
Micheline.canonical_encoding "michelson_v1"
Michelson_v1_primitives.prim_encoding.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent "invalid_binary_format"
"Invalid binary format"
"Could not deserialize some piece of data from its binary representation"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Lazy_script_decode" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Lazy_script_decode" unit tt).
Definition lazy_expr_encoding
: Data_encoding.encoding
(Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim)) :=
Data_encoding.lazy_encoding expr_encoding.
Definition lazy_expr_value
(expr : Micheline.canonical Michelson_v1_primitives.prim)
: Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim) :=
Data_encoding.make_lazy expr_encoding expr.
Module t.
Record record : Set := Build {
code : lazy_expr;
storage : lazy_expr;
}.
Definition with_code code (r : record) :=
Build code r.(storage).
Definition with_storage storage (r : record) :=
Build r.(code) storage.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
(let arg := Data_encoding.def "scripted.contracts" in
fun (eta : Data_encoding.encoding t) ⇒ arg None None eta)
(Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.code := code; t.storage := storage_value |} :=
function_parameter in
(code, storage_value))
(fun (function_parameter : lazy_expr × lazy_expr) ⇒
let '(code, storage_value) := function_parameter in
{| t.code := code; t.storage := storage_value; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "code" lazy_expr_encoding)
(Data_encoding.req None None "storage" lazy_expr_encoding))).
Module S := Saturation_repr.
Module Micheline_size.
Module t.
Record record : Set := Build {
nodes : S.t;
string_bytes : S.t;
z_bytes : S.t;
}.
Definition with_nodes nodes (r : record) :=
Build nodes r.(string_bytes) r.(z_bytes).
Definition with_string_bytes string_bytes (r : record) :=
Build r.(nodes) string_bytes r.(z_bytes).
Definition with_z_bytes z_bytes (r : record) :=
Build r.(nodes) r.(string_bytes) z_bytes.
End t.
Definition t := t.record.
Definition make (nodes : S.t) (string_bytes : S.t) (z_bytes : S.t) : t :=
{| t.nodes := nodes; t.string_bytes := string_bytes; t.z_bytes := z_bytes;
|}.
Definition zero : t :=
{| t.nodes := S.zero; t.string_bytes := S.zero; t.z_bytes := S.zero; |}.
Definition add_int (acc_value : t) (n_value : Z.t) : t :=
let numbits := Z.numbits n_value in
let z_bytes := S.safe_int ((numbits +i 7) /i 8) in
{| t.nodes := S.succ acc_value.(t.nodes);
t.string_bytes := acc_value.(t.string_bytes);
t.z_bytes := S.add acc_value.(t.z_bytes) z_bytes; |}.
Definition add_string (acc_value : t) (n_value : string) : t :=
let string_bytes := S.safe_int (String.length n_value) in
{| t.nodes := S.succ acc_value.(t.nodes);
t.string_bytes := S.add acc_value.(t.string_bytes) string_bytes;
t.z_bytes := acc_value.(t.z_bytes); |}.
Definition add_bytes (acc_value : t) (n_value : bytes) : t :=
let string_bytes := S.safe_int (Bytes.length n_value) in
{| t.nodes := S.succ acc_value.(t.nodes);
t.string_bytes := S.add acc_value.(t.string_bytes) string_bytes;
t.z_bytes := acc_value.(t.z_bytes); |}.
Definition add_node (s_value : t) : t :=
t.with_nodes (S.succ s_value.(t.nodes)) s_value.
Definition of_annots (acc_value : t) (annots : list string) : t :=
List.fold_left
(fun (acc_value : t) ⇒
fun (s_value : string) ⇒ add_string acc_value s_value) acc_value annots.
#[bypass_check(guard)]
Fixpoint of_nodes {A B : Set}
(acc_value : t) (nodes : list (Micheline.node A B))
(more_nodes : list (list (Micheline.node A B))) {struct nodes} : t :=
match nodes with
| [] ⇒
match more_nodes with
| [] ⇒ acc_value
| cons nodes more_nodes ⇒ of_nodes acc_value nodes more_nodes
end
| cons (Micheline.Int _ n_value) nodes ⇒
let acc_value := add_int acc_value n_value in
of_nodes acc_value nodes more_nodes
| cons (Micheline.String _ s_value) nodes ⇒
let acc_value := add_string acc_value s_value in
of_nodes acc_value nodes more_nodes
| cons (Micheline.Bytes _ s_value) nodes ⇒
let acc_value := add_bytes acc_value s_value in
of_nodes acc_value nodes more_nodes
| cons (Micheline.Prim _ _ args annots) nodes ⇒
let acc_value := add_node acc_value in
let acc_value := of_annots acc_value annots in
of_nodes acc_value args (cons nodes more_nodes)
| cons (Micheline.Seq _ args) nodes ⇒
let acc_value := add_node acc_value in
of_nodes acc_value args (cons nodes more_nodes)
end.
Definition of_node {A B : Set} (node_value : Micheline.node A B) : t :=
of_nodes zero [ node_value ] nil.
Definition dot_product (s1 : t) (s2 : t) : S.t :=
S.add (S.mul s1.(t.nodes) s2.(t.nodes))
(S.add (S.mul s1.(t.string_bytes) s2.(t.string_bytes))
(S.mul s1.(t.z_bytes) s2.(t.z_bytes))).
End Micheline_size.
Module Micheline_decoding.
Definition micheline_size_dependent_cost : Micheline_size.t :=
let traversal_cost := S.safe_int 60 in
let string_per_byte_cost := S.safe_int 10 in
let z_per_byte_cost := S.safe_int 10 in
Micheline_size.make traversal_cost string_per_byte_cost z_per_byte_cost.
Definition bytes_dependent_cost : S.t := S.safe_int 20.
End Micheline_decoding.
Module Micheline_encoding.
Definition micheline_size_dependent_cost : Micheline_size.t :=
let traversal_cost := S.safe_int 100 in
let string_per_byte_cost := S.safe_int 10 in
let z_per_byte_cost := S.safe_int 25 in
Micheline_size.make traversal_cost string_per_byte_cost z_per_byte_cost.
Definition bytes_dependent_cost : S.t := S.safe_int 33.
End Micheline_encoding.
Definition expr_size {A : Set} (expr : Micheline.canonical A)
: Micheline_size.t := Micheline_size.of_node (Micheline.root_value expr).
Definition serialization_cost (size_value : Micheline_size.t)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(Micheline_size.dot_product size_value
Micheline_encoding.micheline_size_dependent_cost).
Definition deserialization_cost (size_value : Micheline_size.t)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(Micheline_size.dot_product size_value
Micheline_decoding.micheline_size_dependent_cost).
Definition deserialization_cost_estimated_from_bytes (bytes_len : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul Micheline_decoding.bytes_dependent_cost (S.safe_int bytes_len)).
Definition serialization_cost_estimated_from_bytes (bytes_len : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul Micheline_encoding.bytes_dependent_cost (S.safe_int bytes_len)).
Definition cost_micheline_strip_locations (size_value : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul (S.safe_int size_value) (S.safe_int 51)).
Definition cost_micheline_strip_annotations (size_value : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul (S.safe_int size_value) (S.safe_int 51)).
Definition bytes_node_cost (s_value : bytes) : Gas_limit_repr.cost :=
serialization_cost_estimated_from_bytes (Bytes.length s_value).
Definition deserialized_cost {A : Set} (expr : Micheline.canonical A)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost (deserialization_cost (expr_size expr)).
Definition serialized_cost (bytes_value : bytes) : Gas_limit_repr.cost :=
let cost :=
let size_value := Bytes.length bytes_value in
S.add (serialization_cost_estimated_from_bytes size_value)
(S.add (S.safe_int 65) (S.shift_right (S.safe_int size_value) 4)) in
Gas_limit_repr.atomic_step_cost cost.
Definition force_decode_cost {A : Set} (lexpr : Data_encoding.lazy_t A)
: Gas_limit_repr.cost :=
Data_encoding.apply_lazy
(fun (function_parameter : A) ⇒
let '_ := function_parameter in
Gas_limit_repr.free)
(fun (b_value : bytes) ⇒
deserialization_cost_estimated_from_bytes (Bytes.length b_value))
(fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
Gas_limit_repr.free) lexpr.
Inductive bytes_or_value (a : Set) : Set :=
| Only_value : a → bytes_or_value a
| Has_bytes : bytes → bytes_or_value a.
Arguments Only_value {_}.
Arguments Has_bytes {_}.
Definition stable_force_decode_cost
(lexpr :
Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim))
: Gas_limit_repr.cost :=
let has_bytes :=
Data_encoding.apply_lazy
(fun (v_value : Micheline.canonical Michelson_v1_primitives.prim) ⇒
Only_value v_value) (fun (b_value : bytes) ⇒ Has_bytes b_value)
(fun (_v :
bytes_or_value (Micheline.canonical Michelson_v1_primitives.prim)) ⇒
fun (b_value :
bytes_or_value (Micheline.canonical Michelson_v1_primitives.prim)) ⇒
b_value) lexpr in
match has_bytes with
| Has_bytes b_value ⇒
deserialization_cost_estimated_from_bytes (Bytes.length b_value)
| Only_value v_value ⇒
deserialization_cost_estimated_from_bytes
(Data_encoding.Binary.length expr_encoding v_value)
end.
Definition force_decode {A : Set} (lexpr : Data_encoding.lazy_t A) : M? A :=
match Data_encoding.force_decode lexpr with
| Some v_value ⇒ return? v_value
| None ⇒
Error_monad.error_value (Build_extensible "Lazy_script_decode" unit tt)
end.
Definition force_bytes_cost {A : Set}
(expr : Data_encoding.lazy_t (Micheline.canonical A)) : Gas_limit_repr.cost :=
Data_encoding.apply_lazy
(fun (v_value : Micheline.canonical A) ⇒
serialization_cost (expr_size v_value))
(fun (function_parameter : bytes) ⇒
let '_ := function_parameter in
Gas_limit_repr.free)
(fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
Gas_limit_repr.free) expr.
Definition force_bytes {A : Set} (expr : Data_encoding.lazy_t A) : M? bytes :=
Error_monad.catch_f None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Data_encoding.force_bytes expr)
(fun (function_parameter : extensible_type) ⇒
let '_ := function_parameter in
Build_extensible "Lazy_script_decode" unit tt).
Definition unit_value : Micheline.canonical Michelson_v1_primitives.prim :=
Micheline.strip_locations
(Micheline.Prim 0 Michelson_v1_primitives.D_Unit nil nil).
Definition unit_parameter
: Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim) :=
lazy_expr_value unit_value.
Definition is_unit_parameter
: Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim) →
bool :=
let unit_bytes := Data_encoding.force_bytes unit_parameter in
Data_encoding.apply_lazy
(fun (v_value : Micheline.canonical Michelson_v1_primitives.prim) ⇒
match Micheline.root_value v_value with
| Micheline.Prim _ Michelson_v1_primitives.D_Unit [] [] ⇒ true
| _ ⇒ false
end)
(fun (b_value : Compare.Bytes.(Compare.S.t)) ⇒
Compare.Bytes.(Compare.S.equal) b_value unit_bytes)
(fun (res : bool) ⇒
fun (function_parameter : bool) ⇒
let '_ := function_parameter in
res).
#[bypass_check(guard)]
Fixpoint strip_annotations {A B : Set} (node_value : Micheline.node A B)
{struct node_value} : Micheline.node A B :=
match node_value with
| (Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _) as leaf ⇒
leaf
| Micheline.Prim loc_value name args _ ⇒
Micheline.Prim loc_value name (List.map strip_annotations args) nil
| Micheline.Seq loc_value args ⇒
Micheline.Seq loc_value (List.map strip_annotations args)
end.
Reserved Notation "'micheline_fold_nodes".
#[bypass_check(guard)]
Fixpoint micheline_fold_aux {A B C : Set}
(node_value : michelson_node A) (f_value : B → michelson_node A → B)
(acc_value : B) (k_value : B → C) : C :=
let micheline_fold_nodes {A B C} := 'micheline_fold_nodes A B C in
match node_value with
| Micheline.Int _ _ ⇒ k_value (f_value acc_value node_value)
| Micheline.String _ _ ⇒ k_value (f_value acc_value node_value)
| Micheline.Bytes _ _ ⇒ k_value (f_value acc_value node_value)
| Micheline.Prim _ _ subterms _ ⇒
micheline_fold_nodes subterms f_value (f_value acc_value node_value) k_value
| Micheline.Seq _ subterms ⇒
micheline_fold_nodes subterms f_value (f_value acc_value node_value) k_value
end
where "'micheline_fold_nodes" :=
(fun (A B C : Set) ⇒ fix micheline_fold_nodes
(subterms : list (Micheline.node A Michelson_v1_primitives.prim))
(f_value : B → michelson_node A → B) (acc_value : B) (k_value : B → C)
{struct subterms} : C :=
match subterms with
| [] ⇒ k_value acc_value
| cons node_value nodes ⇒
micheline_fold_nodes nodes f_value acc_value
(fun (acc_value : B) ⇒
micheline_fold_aux node_value f_value acc_value k_value)
end).
Definition micheline_fold_nodes {A B C : Set} := 'micheline_fold_nodes A B C.
Definition fold {A B : Set}
(node_value : michelson_node A) (init_value : B)
(f_value : B → michelson_node A → B) : B :=
micheline_fold_aux node_value f_value init_value
(fun (x_value : B) ⇒ x_value).
Definition micheline_nodes {A : Set} (node_value : michelson_node A) : int :=
fold node_value 0
(fun (n_value : int) ⇒
fun (function_parameter : michelson_node A) ⇒
let '_ := function_parameter in
n_value +i 1).
Definition strip_locations_cost {A : Set} (node_value : michelson_node A)
: Gas_limit_repr.cost :=
let nodes := micheline_nodes node_value in
cost_micheline_strip_locations nodes.
Definition strip_annotations_cost {A : Set} (node_value : michelson_node A)
: Gas_limit_repr.cost :=
let nodes := micheline_nodes node_value in
cost_micheline_strip_annotations nodes.
Error_monad.register_error_kind Error_monad.Permanent "invalid_binary_format"
"Invalid binary format"
"Could not deserialize some piece of data from its binary representation"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Lazy_script_decode" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Lazy_script_decode" unit tt).
Definition lazy_expr_encoding
: Data_encoding.encoding
(Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim)) :=
Data_encoding.lazy_encoding expr_encoding.
Definition lazy_expr_value
(expr : Micheline.canonical Michelson_v1_primitives.prim)
: Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim) :=
Data_encoding.make_lazy expr_encoding expr.
Module t.
Record record : Set := Build {
code : lazy_expr;
storage : lazy_expr;
}.
Definition with_code code (r : record) :=
Build code r.(storage).
Definition with_storage storage (r : record) :=
Build r.(code) storage.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
(let arg := Data_encoding.def "scripted.contracts" in
fun (eta : Data_encoding.encoding t) ⇒ arg None None eta)
(Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{| t.code := code; t.storage := storage_value |} :=
function_parameter in
(code, storage_value))
(fun (function_parameter : lazy_expr × lazy_expr) ⇒
let '(code, storage_value) := function_parameter in
{| t.code := code; t.storage := storage_value; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "code" lazy_expr_encoding)
(Data_encoding.req None None "storage" lazy_expr_encoding))).
Module S := Saturation_repr.
Module Micheline_size.
Module t.
Record record : Set := Build {
nodes : S.t;
string_bytes : S.t;
z_bytes : S.t;
}.
Definition with_nodes nodes (r : record) :=
Build nodes r.(string_bytes) r.(z_bytes).
Definition with_string_bytes string_bytes (r : record) :=
Build r.(nodes) string_bytes r.(z_bytes).
Definition with_z_bytes z_bytes (r : record) :=
Build r.(nodes) r.(string_bytes) z_bytes.
End t.
Definition t := t.record.
Definition make (nodes : S.t) (string_bytes : S.t) (z_bytes : S.t) : t :=
{| t.nodes := nodes; t.string_bytes := string_bytes; t.z_bytes := z_bytes;
|}.
Definition zero : t :=
{| t.nodes := S.zero; t.string_bytes := S.zero; t.z_bytes := S.zero; |}.
Definition add_int (acc_value : t) (n_value : Z.t) : t :=
let numbits := Z.numbits n_value in
let z_bytes := S.safe_int ((numbits +i 7) /i 8) in
{| t.nodes := S.succ acc_value.(t.nodes);
t.string_bytes := acc_value.(t.string_bytes);
t.z_bytes := S.add acc_value.(t.z_bytes) z_bytes; |}.
Definition add_string (acc_value : t) (n_value : string) : t :=
let string_bytes := S.safe_int (String.length n_value) in
{| t.nodes := S.succ acc_value.(t.nodes);
t.string_bytes := S.add acc_value.(t.string_bytes) string_bytes;
t.z_bytes := acc_value.(t.z_bytes); |}.
Definition add_bytes (acc_value : t) (n_value : bytes) : t :=
let string_bytes := S.safe_int (Bytes.length n_value) in
{| t.nodes := S.succ acc_value.(t.nodes);
t.string_bytes := S.add acc_value.(t.string_bytes) string_bytes;
t.z_bytes := acc_value.(t.z_bytes); |}.
Definition add_node (s_value : t) : t :=
t.with_nodes (S.succ s_value.(t.nodes)) s_value.
Definition of_annots (acc_value : t) (annots : list string) : t :=
List.fold_left
(fun (acc_value : t) ⇒
fun (s_value : string) ⇒ add_string acc_value s_value) acc_value annots.
#[bypass_check(guard)]
Fixpoint of_nodes {A B : Set}
(acc_value : t) (nodes : list (Micheline.node A B))
(more_nodes : list (list (Micheline.node A B))) {struct nodes} : t :=
match nodes with
| [] ⇒
match more_nodes with
| [] ⇒ acc_value
| cons nodes more_nodes ⇒ of_nodes acc_value nodes more_nodes
end
| cons (Micheline.Int _ n_value) nodes ⇒
let acc_value := add_int acc_value n_value in
of_nodes acc_value nodes more_nodes
| cons (Micheline.String _ s_value) nodes ⇒
let acc_value := add_string acc_value s_value in
of_nodes acc_value nodes more_nodes
| cons (Micheline.Bytes _ s_value) nodes ⇒
let acc_value := add_bytes acc_value s_value in
of_nodes acc_value nodes more_nodes
| cons (Micheline.Prim _ _ args annots) nodes ⇒
let acc_value := add_node acc_value in
let acc_value := of_annots acc_value annots in
of_nodes acc_value args (cons nodes more_nodes)
| cons (Micheline.Seq _ args) nodes ⇒
let acc_value := add_node acc_value in
of_nodes acc_value args (cons nodes more_nodes)
end.
Definition of_node {A B : Set} (node_value : Micheline.node A B) : t :=
of_nodes zero [ node_value ] nil.
Definition dot_product (s1 : t) (s2 : t) : S.t :=
S.add (S.mul s1.(t.nodes) s2.(t.nodes))
(S.add (S.mul s1.(t.string_bytes) s2.(t.string_bytes))
(S.mul s1.(t.z_bytes) s2.(t.z_bytes))).
End Micheline_size.
Module Micheline_decoding.
Definition micheline_size_dependent_cost : Micheline_size.t :=
let traversal_cost := S.safe_int 60 in
let string_per_byte_cost := S.safe_int 10 in
let z_per_byte_cost := S.safe_int 10 in
Micheline_size.make traversal_cost string_per_byte_cost z_per_byte_cost.
Definition bytes_dependent_cost : S.t := S.safe_int 20.
End Micheline_decoding.
Module Micheline_encoding.
Definition micheline_size_dependent_cost : Micheline_size.t :=
let traversal_cost := S.safe_int 100 in
let string_per_byte_cost := S.safe_int 10 in
let z_per_byte_cost := S.safe_int 25 in
Micheline_size.make traversal_cost string_per_byte_cost z_per_byte_cost.
Definition bytes_dependent_cost : S.t := S.safe_int 33.
End Micheline_encoding.
Definition expr_size {A : Set} (expr : Micheline.canonical A)
: Micheline_size.t := Micheline_size.of_node (Micheline.root_value expr).
Definition serialization_cost (size_value : Micheline_size.t)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(Micheline_size.dot_product size_value
Micheline_encoding.micheline_size_dependent_cost).
Definition deserialization_cost (size_value : Micheline_size.t)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(Micheline_size.dot_product size_value
Micheline_decoding.micheline_size_dependent_cost).
Definition deserialization_cost_estimated_from_bytes (bytes_len : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul Micheline_decoding.bytes_dependent_cost (S.safe_int bytes_len)).
Definition serialization_cost_estimated_from_bytes (bytes_len : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul Micheline_encoding.bytes_dependent_cost (S.safe_int bytes_len)).
Definition cost_micheline_strip_locations (size_value : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul (S.safe_int size_value) (S.safe_int 51)).
Definition cost_micheline_strip_annotations (size_value : int)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost
(S.mul (S.safe_int size_value) (S.safe_int 51)).
Definition bytes_node_cost (s_value : bytes) : Gas_limit_repr.cost :=
serialization_cost_estimated_from_bytes (Bytes.length s_value).
Definition deserialized_cost {A : Set} (expr : Micheline.canonical A)
: Gas_limit_repr.cost :=
Gas_limit_repr.atomic_step_cost (deserialization_cost (expr_size expr)).
Definition serialized_cost (bytes_value : bytes) : Gas_limit_repr.cost :=
let cost :=
let size_value := Bytes.length bytes_value in
S.add (serialization_cost_estimated_from_bytes size_value)
(S.add (S.safe_int 65) (S.shift_right (S.safe_int size_value) 4)) in
Gas_limit_repr.atomic_step_cost cost.
Definition force_decode_cost {A : Set} (lexpr : Data_encoding.lazy_t A)
: Gas_limit_repr.cost :=
Data_encoding.apply_lazy
(fun (function_parameter : A) ⇒
let '_ := function_parameter in
Gas_limit_repr.free)
(fun (b_value : bytes) ⇒
deserialization_cost_estimated_from_bytes (Bytes.length b_value))
(fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
Gas_limit_repr.free) lexpr.
Inductive bytes_or_value (a : Set) : Set :=
| Only_value : a → bytes_or_value a
| Has_bytes : bytes → bytes_or_value a.
Arguments Only_value {_}.
Arguments Has_bytes {_}.
Definition stable_force_decode_cost
(lexpr :
Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim))
: Gas_limit_repr.cost :=
let has_bytes :=
Data_encoding.apply_lazy
(fun (v_value : Micheline.canonical Michelson_v1_primitives.prim) ⇒
Only_value v_value) (fun (b_value : bytes) ⇒ Has_bytes b_value)
(fun (_v :
bytes_or_value (Micheline.canonical Michelson_v1_primitives.prim)) ⇒
fun (b_value :
bytes_or_value (Micheline.canonical Michelson_v1_primitives.prim)) ⇒
b_value) lexpr in
match has_bytes with
| Has_bytes b_value ⇒
deserialization_cost_estimated_from_bytes (Bytes.length b_value)
| Only_value v_value ⇒
deserialization_cost_estimated_from_bytes
(Data_encoding.Binary.length expr_encoding v_value)
end.
Definition force_decode {A : Set} (lexpr : Data_encoding.lazy_t A) : M? A :=
match Data_encoding.force_decode lexpr with
| Some v_value ⇒ return? v_value
| None ⇒
Error_monad.error_value (Build_extensible "Lazy_script_decode" unit tt)
end.
Definition force_bytes_cost {A : Set}
(expr : Data_encoding.lazy_t (Micheline.canonical A)) : Gas_limit_repr.cost :=
Data_encoding.apply_lazy
(fun (v_value : Micheline.canonical A) ⇒
serialization_cost (expr_size v_value))
(fun (function_parameter : bytes) ⇒
let '_ := function_parameter in
Gas_limit_repr.free)
(fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
fun (function_parameter : Gas_limit_repr.cost) ⇒
let '_ := function_parameter in
Gas_limit_repr.free) expr.
Definition force_bytes {A : Set} (expr : Data_encoding.lazy_t A) : M? bytes :=
Error_monad.catch_f None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Data_encoding.force_bytes expr)
(fun (function_parameter : extensible_type) ⇒
let '_ := function_parameter in
Build_extensible "Lazy_script_decode" unit tt).
Definition unit_value : Micheline.canonical Michelson_v1_primitives.prim :=
Micheline.strip_locations
(Micheline.Prim 0 Michelson_v1_primitives.D_Unit nil nil).
Definition unit_parameter
: Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim) :=
lazy_expr_value unit_value.
Definition is_unit_parameter
: Data_encoding.lazy_t (Micheline.canonical Michelson_v1_primitives.prim) →
bool :=
let unit_bytes := Data_encoding.force_bytes unit_parameter in
Data_encoding.apply_lazy
(fun (v_value : Micheline.canonical Michelson_v1_primitives.prim) ⇒
match Micheline.root_value v_value with
| Micheline.Prim _ Michelson_v1_primitives.D_Unit [] [] ⇒ true
| _ ⇒ false
end)
(fun (b_value : Compare.Bytes.(Compare.S.t)) ⇒
Compare.Bytes.(Compare.S.equal) b_value unit_bytes)
(fun (res : bool) ⇒
fun (function_parameter : bool) ⇒
let '_ := function_parameter in
res).
#[bypass_check(guard)]
Fixpoint strip_annotations {A B : Set} (node_value : Micheline.node A B)
{struct node_value} : Micheline.node A B :=
match node_value with
| (Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _) as leaf ⇒
leaf
| Micheline.Prim loc_value name args _ ⇒
Micheline.Prim loc_value name (List.map strip_annotations args) nil
| Micheline.Seq loc_value args ⇒
Micheline.Seq loc_value (List.map strip_annotations args)
end.
Reserved Notation "'micheline_fold_nodes".
#[bypass_check(guard)]
Fixpoint micheline_fold_aux {A B C : Set}
(node_value : michelson_node A) (f_value : B → michelson_node A → B)
(acc_value : B) (k_value : B → C) : C :=
let micheline_fold_nodes {A B C} := 'micheline_fold_nodes A B C in
match node_value with
| Micheline.Int _ _ ⇒ k_value (f_value acc_value node_value)
| Micheline.String _ _ ⇒ k_value (f_value acc_value node_value)
| Micheline.Bytes _ _ ⇒ k_value (f_value acc_value node_value)
| Micheline.Prim _ _ subterms _ ⇒
micheline_fold_nodes subterms f_value (f_value acc_value node_value) k_value
| Micheline.Seq _ subterms ⇒
micheline_fold_nodes subterms f_value (f_value acc_value node_value) k_value
end
where "'micheline_fold_nodes" :=
(fun (A B C : Set) ⇒ fix micheline_fold_nodes
(subterms : list (Micheline.node A Michelson_v1_primitives.prim))
(f_value : B → michelson_node A → B) (acc_value : B) (k_value : B → C)
{struct subterms} : C :=
match subterms with
| [] ⇒ k_value acc_value
| cons node_value nodes ⇒
micheline_fold_nodes nodes f_value acc_value
(fun (acc_value : B) ⇒
micheline_fold_aux node_value f_value acc_value k_value)
end).
Definition micheline_fold_nodes {A B C : Set} := 'micheline_fold_nodes A B C.
Definition fold {A B : Set}
(node_value : michelson_node A) (init_value : B)
(f_value : B → michelson_node A → B) : B :=
micheline_fold_aux node_value f_value init_value
(fun (x_value : B) ⇒ x_value).
Definition micheline_nodes {A : Set} (node_value : michelson_node A) : int :=
fold node_value 0
(fun (n_value : int) ⇒
fun (function_parameter : michelson_node A) ⇒
let '_ := function_parameter in
n_value +i 1).
Definition strip_locations_cost {A : Set} (node_value : michelson_node A)
: Gas_limit_repr.cost :=
let nodes := micheline_nodes node_value in
cost_micheline_strip_locations nodes.
Definition strip_annotations_cost {A : Set} (node_value : michelson_node A)
: Gas_limit_repr.cost :=
let nodes := micheline_nodes node_value in
cost_micheline_strip_annotations nodes.