🌍 Global_constants_storage.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Global_constants_costs.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
#[bypass_check(guard)]
Fixpoint traverse_node {A B C D : Set}
(accu_value : A) (node_value : Micheline.node B C)
(f_value : A → Micheline.node B C → (A → Micheline.node B C → D) → D)
(k_value : A → Micheline.node B C → D) {struct node_value} : D :=
f_value accu_value node_value
(fun (accu_value : A) ⇒
fun (node_value : Micheline.node B C) ⇒
match node_value with
| (Micheline.String _ _ | Micheline.Int _ _ | Micheline.Bytes _ _) ⇒
k_value accu_value node_value
| Micheline.Prim loc_value prim args annot ⇒
traverse_nodes accu_value args f_value
(fun (accu_value : A) ⇒
fun (args : list (Micheline.node B C)) ⇒
f_value accu_value (Micheline.Prim loc_value prim args annot)
k_value)
| Micheline.Seq loc_value elts ⇒
traverse_nodes accu_value elts f_value
(fun (accu_value : A) ⇒
fun (elts : list (Micheline.node B C)) ⇒
f_value accu_value (Micheline.Seq loc_value elts) k_value)
end)
with traverse_nodes {A B C D : Set}
(accu_value : A) (nodes : list (Micheline.node B C))
(f_value : A → Micheline.node B C → (A → Micheline.node B C → D) → D)
(k_value : A → list (Micheline.node B C) → D) {struct nodes} : D :=
match nodes with
| [] ⇒ k_value accu_value nil
| cons node_value nodes ⇒
traverse_node accu_value node_value f_value
(fun (accu_value : A) ⇒
fun (node_value : Micheline.node B C) ⇒
traverse_nodes accu_value nodes f_value
(fun (accu_value : A) ⇒
fun (nodes : list (Micheline.node B C)) ⇒
k_value accu_value (cons node_value nodes)))
end.
Definition bottom_up_fold_cps {A B C D : Set}
(initial_accumulator : A) (node_value : Micheline.node B C)
(initial_k : A → Micheline.node B C → D)
(f_value : A → Micheline.node B C → (A → Micheline.node B C → D) → D)
: D := traverse_node initial_accumulator node_value f_value initial_k.
Module Gas_costs := Global_constants_costs.
Definition Expr_hash_map :=
Map.Make
{|
Compare.COMPARABLE.compare := Script_expr_hash.compare
|}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Global_constants_costs.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
#[bypass_check(guard)]
Fixpoint traverse_node {A B C D : Set}
(accu_value : A) (node_value : Micheline.node B C)
(f_value : A → Micheline.node B C → (A → Micheline.node B C → D) → D)
(k_value : A → Micheline.node B C → D) {struct node_value} : D :=
f_value accu_value node_value
(fun (accu_value : A) ⇒
fun (node_value : Micheline.node B C) ⇒
match node_value with
| (Micheline.String _ _ | Micheline.Int _ _ | Micheline.Bytes _ _) ⇒
k_value accu_value node_value
| Micheline.Prim loc_value prim args annot ⇒
traverse_nodes accu_value args f_value
(fun (accu_value : A) ⇒
fun (args : list (Micheline.node B C)) ⇒
f_value accu_value (Micheline.Prim loc_value prim args annot)
k_value)
| Micheline.Seq loc_value elts ⇒
traverse_nodes accu_value elts f_value
(fun (accu_value : A) ⇒
fun (elts : list (Micheline.node B C)) ⇒
f_value accu_value (Micheline.Seq loc_value elts) k_value)
end)
with traverse_nodes {A B C D : Set}
(accu_value : A) (nodes : list (Micheline.node B C))
(f_value : A → Micheline.node B C → (A → Micheline.node B C → D) → D)
(k_value : A → list (Micheline.node B C) → D) {struct nodes} : D :=
match nodes with
| [] ⇒ k_value accu_value nil
| cons node_value nodes ⇒
traverse_node accu_value node_value f_value
(fun (accu_value : A) ⇒
fun (node_value : Micheline.node B C) ⇒
traverse_nodes accu_value nodes f_value
(fun (accu_value : A) ⇒
fun (nodes : list (Micheline.node B C)) ⇒
k_value accu_value (cons node_value nodes)))
end.
Definition bottom_up_fold_cps {A B C D : Set}
(initial_accumulator : A) (node_value : Micheline.node B C)
(initial_k : A → Micheline.node B C → D)
(f_value : A → Micheline.node B C → (A → Micheline.node B C → D) → D)
: D := traverse_node initial_accumulator node_value f_value initial_k.
Module Gas_costs := Global_constants_costs.
Definition Expr_hash_map :=
Map.Make
{|
Compare.COMPARABLE.compare := Script_expr_hash.compare
|}.
Init function; without side-effects in Coq
Definition init_module : unit :=
let description :=
"Attempted to register an expression that, after fully expanding all referenced global constants, would result in too many levels of nesting."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "Expression_too_deep"
"Expression too deep" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Expression_too_deep" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Expression_too_deep" unit tt) in
let description :=
"Attempted to register an expression as global constant that has already been registered."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"Expression_already_registered" "Expression already registered"
description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Expression_already_registered" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Expression_already_registered" unit tt) in
let description :=
"Found a badly formed constant expression. The 'constant' primitive must always be followed by a string of the hash of the expression it points to."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"Badly_formed_constant_expression" "Badly formed constant expression"
description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Badly_formed_constant_expression" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Badly_formed_constant_expression" unit tt) in
let description :=
"No registered global was found at the given hash in storage." in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "Nonexistent_global"
"Tried to look up nonexistent global" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Nonexistent_global" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Nonexistent_global" unit tt) in
let description :=
"Encountered an expression that, after expanding all constants, is larger than the expression size limit."
in
Error_monad.register_error_kind Error_monad.Branch "Expression_too_large"
"Expression too large" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Expression_too_large" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Expression_too_large" unit tt).
Definition get (context_value : Raw_context.t) (hash_value : Script_expr_hash.t)
: M? (Raw_context.t × Script_repr.expr) :=
let? '(context_value, value_value) :=
Storage.Global_constants.Map.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
context_value hash_value in
match value_value with
| None ⇒ Error_monad.tzfail (Build_extensible "Nonexistent_global" unit tt)
| Some value_value ⇒ return? (context_value, value_value)
end.
Definition expr_to_address_in_context
(context_value : Raw_context.t) (expr : Script_repr.expr)
: M? (Raw_context.t × Script_expr_hash.t) :=
let lexpr := Script_repr.lazy_expr_value expr in
let? context_value :=
Raw_context.consume_gas context_value (Script_repr.force_bytes_cost lexpr)
in
let? b_value := Script_repr.force_bytes lexpr in
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expr_to_address_in_context_cost b_value) in
return? (context_value, (Script_expr_hash.hash_bytes None [ b_value ])).
Definition node_too_large (node_value : Script_repr.node) : bool :=
let node_size := Script_repr.Micheline_size.of_node node_value in
let nodes :=
Saturation_repr.to_int node_size.(Script_repr.Micheline_size.t.nodes) in
let string_bytes :=
Saturation_repr.to_int node_size.(Script_repr.Micheline_size.t.string_bytes)
in
let z_bytes :=
Saturation_repr.to_int node_size.(Script_repr.Micheline_size.t.z_bytes) in
(nodes >i Constants_repr.max_micheline_node_count) ||
((string_bytes +i z_bytes) >i Constants_repr.max_micheline_bytes_limit).
Definition expand_node
(context_value : Raw_context.t) (node_value : Script_repr.node)
: M?
(Raw_context.t ×
Micheline.node Script_repr.location Michelson_v1_primitives.prim) :=
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expand_no_constants_branch_cost node_value) in
let? '(context_value, node_value, did_expansion) :=
bottom_up_fold_cps (context_value, Expr_hash_map.(Map.S.empty), false)
node_value
(fun (function_parameter :
Raw_context.t × Expr_hash_map.(Map.S.t) Script_repr.node × bool) ⇒
let '(context_value, _, did_expansion) := function_parameter in
fun (node_value :
Micheline.node Script_repr.location Michelson_v1_primitives.prim) ⇒
return? (context_value, node_value, did_expansion))
(fun (function_parameter :
Raw_context.t × Expr_hash_map.(Map.S.t) Script_repr.node × bool) ⇒
let '(context_value, map, did_expansion) := function_parameter in
fun (node_value :
Micheline.node Script_repr.location Michelson_v1_primitives.prim) ⇒
fun (k_value :
Raw_context.t × Expr_hash_map.(Map.S.t) Script_repr.node × bool →
Micheline.node Script_repr.location Michelson_v1_primitives.prim →
M?
(Raw_context.t ×
Micheline.node Script_repr.location Michelson_v1_primitives.prim
× bool)) ⇒
match node_value with
| Micheline.Prim _ Michelson_v1_primitives.H_constant args annot ⇒
let? context_value :=
Raw_context.consume_gas context_value
Gas_costs.expand_constants_branch_cost in
match (args, annot) with
| (cons (Micheline.String _ address) [], []) ⇒
match Script_expr_hash.of_b58check_opt address with
| None ⇒
Error_monad.tzfail
(Build_extensible "Badly_formed_constant_expression" unit tt)
| Some hash_value ⇒
match Expr_hash_map.(Map.S.find) hash_value map with
| Some node_value ⇒
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expand_no_constants_branch_cost node_value)
in
k_value (context_value, map, true) node_value
| None ⇒
let? '(context_value, expr) := get context_value hash_value
in
let node_value := Micheline.root_value expr in
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expand_no_constants_branch_cost node_value)
in
k_value
(context_value,
(Expr_hash_map.(Map.S.add) hash_value node_value map),
true) node_value
end
end
| _ ⇒
Error_monad.tzfail
(Build_extensible "Badly_formed_constant_expression" unit tt)
end
|
(Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _ |
Micheline.Prim _ _ _ _ | Micheline.Seq _ _) ⇒
k_value (context_value, map, did_expansion) node_value
end) in
if did_expansion then
if node_too_large node_value then
Error_monad.tzfail (Build_extensible "Expression_too_large" unit tt)
else
return? (context_value, node_value)
else
return? (context_value, node_value).
Definition expand
(context_value : Raw_context.t)
(expr : Micheline.canonical Michelson_v1_primitives.prim)
: M? (Raw_context.t × Micheline.canonical Michelson_v1_primitives.prim) :=
let? '(context_value, node_value) :=
expand_node context_value (Micheline.root_value expr) in
return? (context_value, (Micheline.strip_locations node_value)).
let description :=
"Attempted to register an expression that, after fully expanding all referenced global constants, would result in too many levels of nesting."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "Expression_too_deep"
"Expression too deep" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Expression_too_deep" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Expression_too_deep" unit tt) in
let description :=
"Attempted to register an expression as global constant that has already been registered."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"Expression_already_registered" "Expression already registered"
description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Expression_already_registered" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Expression_already_registered" unit tt) in
let description :=
"Found a badly formed constant expression. The 'constant' primitive must always be followed by a string of the hash of the expression it points to."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"Badly_formed_constant_expression" "Badly formed constant expression"
description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Badly_formed_constant_expression" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Badly_formed_constant_expression" unit tt) in
let description :=
"No registered global was found at the given hash in storage." in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch "Nonexistent_global"
"Tried to look up nonexistent global" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Nonexistent_global" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Nonexistent_global" unit tt) in
let description :=
"Encountered an expression that, after expanding all constants, is larger than the expression size limit."
in
Error_monad.register_error_kind Error_monad.Branch "Expression_too_large"
"Expression too large" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Expression_too_large" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Expression_too_large" unit tt).
Definition get (context_value : Raw_context.t) (hash_value : Script_expr_hash.t)
: M? (Raw_context.t × Script_repr.expr) :=
let? '(context_value, value_value) :=
Storage.Global_constants.Map.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
context_value hash_value in
match value_value with
| None ⇒ Error_monad.tzfail (Build_extensible "Nonexistent_global" unit tt)
| Some value_value ⇒ return? (context_value, value_value)
end.
Definition expr_to_address_in_context
(context_value : Raw_context.t) (expr : Script_repr.expr)
: M? (Raw_context.t × Script_expr_hash.t) :=
let lexpr := Script_repr.lazy_expr_value expr in
let? context_value :=
Raw_context.consume_gas context_value (Script_repr.force_bytes_cost lexpr)
in
let? b_value := Script_repr.force_bytes lexpr in
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expr_to_address_in_context_cost b_value) in
return? (context_value, (Script_expr_hash.hash_bytes None [ b_value ])).
Definition node_too_large (node_value : Script_repr.node) : bool :=
let node_size := Script_repr.Micheline_size.of_node node_value in
let nodes :=
Saturation_repr.to_int node_size.(Script_repr.Micheline_size.t.nodes) in
let string_bytes :=
Saturation_repr.to_int node_size.(Script_repr.Micheline_size.t.string_bytes)
in
let z_bytes :=
Saturation_repr.to_int node_size.(Script_repr.Micheline_size.t.z_bytes) in
(nodes >i Constants_repr.max_micheline_node_count) ||
((string_bytes +i z_bytes) >i Constants_repr.max_micheline_bytes_limit).
Definition expand_node
(context_value : Raw_context.t) (node_value : Script_repr.node)
: M?
(Raw_context.t ×
Micheline.node Script_repr.location Michelson_v1_primitives.prim) :=
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expand_no_constants_branch_cost node_value) in
let? '(context_value, node_value, did_expansion) :=
bottom_up_fold_cps (context_value, Expr_hash_map.(Map.S.empty), false)
node_value
(fun (function_parameter :
Raw_context.t × Expr_hash_map.(Map.S.t) Script_repr.node × bool) ⇒
let '(context_value, _, did_expansion) := function_parameter in
fun (node_value :
Micheline.node Script_repr.location Michelson_v1_primitives.prim) ⇒
return? (context_value, node_value, did_expansion))
(fun (function_parameter :
Raw_context.t × Expr_hash_map.(Map.S.t) Script_repr.node × bool) ⇒
let '(context_value, map, did_expansion) := function_parameter in
fun (node_value :
Micheline.node Script_repr.location Michelson_v1_primitives.prim) ⇒
fun (k_value :
Raw_context.t × Expr_hash_map.(Map.S.t) Script_repr.node × bool →
Micheline.node Script_repr.location Michelson_v1_primitives.prim →
M?
(Raw_context.t ×
Micheline.node Script_repr.location Michelson_v1_primitives.prim
× bool)) ⇒
match node_value with
| Micheline.Prim _ Michelson_v1_primitives.H_constant args annot ⇒
let? context_value :=
Raw_context.consume_gas context_value
Gas_costs.expand_constants_branch_cost in
match (args, annot) with
| (cons (Micheline.String _ address) [], []) ⇒
match Script_expr_hash.of_b58check_opt address with
| None ⇒
Error_monad.tzfail
(Build_extensible "Badly_formed_constant_expression" unit tt)
| Some hash_value ⇒
match Expr_hash_map.(Map.S.find) hash_value map with
| Some node_value ⇒
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expand_no_constants_branch_cost node_value)
in
k_value (context_value, map, true) node_value
| None ⇒
let? '(context_value, expr) := get context_value hash_value
in
let node_value := Micheline.root_value expr in
let? context_value :=
Raw_context.consume_gas context_value
(Gas_costs.expand_no_constants_branch_cost node_value)
in
k_value
(context_value,
(Expr_hash_map.(Map.S.add) hash_value node_value map),
true) node_value
end
end
| _ ⇒
Error_monad.tzfail
(Build_extensible "Badly_formed_constant_expression" unit tt)
end
|
(Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _ |
Micheline.Prim _ _ _ _ | Micheline.Seq _ _) ⇒
k_value (context_value, map, did_expansion) node_value
end) in
if did_expansion then
if node_too_large node_value then
Error_monad.tzfail (Build_extensible "Expression_too_large" unit tt)
else
return? (context_value, node_value)
else
return? (context_value, node_value).
Definition expand
(context_value : Raw_context.t)
(expr : Micheline.canonical Michelson_v1_primitives.prim)
: M? (Raw_context.t × Micheline.canonical Michelson_v1_primitives.prim) :=
let? '(context_value, node_value) :=
expand_node context_value (Micheline.root_value expr) in
return? (context_value, (Micheline.strip_locations node_value)).
Computes the maximum depth of a Micheline node. Fails
with [Expression_too_deep] if greater than
[max_allowed_global_constant_depth].
#[bypass_check(guard)]
Definition check_depth {A B : Set} (node_value : Micheline.node A B) : M? int :=
let fix advance {C D E : Set}
(node_value : Micheline.node C D) (depth : int) (k_value : int → M? E)
{struct node_value} : M? E :=
if depth >i Constants_repr.max_allowed_global_constant_depth then
Error_monad.error_value (Build_extensible "Expression_too_deep" unit tt)
else
match node_value with
|
(Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _ |
Micheline.Prim _ _ [] _ | Micheline.Seq _ []) ⇒ k_value (depth +i 1)
|
(Micheline.Prim loc_value _ (cons hd tl) _ |
Micheline.Seq loc_value (cons hd tl)) ⇒
advance hd (depth +i 1)
(fun (dhd : int) ⇒
advance (Micheline.Seq loc_value tl) depth
(fun (dtl : int) ⇒ k_value (Compare.Int.max dhd dtl)))
end in
advance node_value 0 (fun (x_value : int) ⇒ Pervasives.Ok x_value).
Definition register
(context_value : Raw_context.t)
(value_value : Micheline.canonical Michelson_v1_primitives.prim)
: M? (Raw_context.t × Script_expr_hash.t × Z.t) :=
let? '(context_value, node_value) :=
expand_node context_value (Micheline.root_value value_value) in
let? _depth := check_depth node_value in
let? '(context_value, key_value) :=
expr_to_address_in_context context_value value_value in
let? '(context_value, size_value) :=
Error_monad.trace_value
(Build_extensible "Expression_already_registered" unit tt)
(Storage.Global_constants.Map.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
context_value key_value value_value) in
return? (context_value, key_value, (Z.of_int size_value)).
Definition check_depth {A B : Set} (node_value : Micheline.node A B) : M? int :=
let fix advance {C D E : Set}
(node_value : Micheline.node C D) (depth : int) (k_value : int → M? E)
{struct node_value} : M? E :=
if depth >i Constants_repr.max_allowed_global_constant_depth then
Error_monad.error_value (Build_extensible "Expression_too_deep" unit tt)
else
match node_value with
|
(Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _ |
Micheline.Prim _ _ [] _ | Micheline.Seq _ []) ⇒ k_value (depth +i 1)
|
(Micheline.Prim loc_value _ (cons hd tl) _ |
Micheline.Seq loc_value (cons hd tl)) ⇒
advance hd (depth +i 1)
(fun (dhd : int) ⇒
advance (Micheline.Seq loc_value tl) depth
(fun (dtl : int) ⇒ k_value (Compare.Int.max dhd dtl)))
end in
advance node_value 0 (fun (x_value : int) ⇒ Pervasives.Ok x_value).
Definition register
(context_value : Raw_context.t)
(value_value : Micheline.canonical Michelson_v1_primitives.prim)
: M? (Raw_context.t × Script_expr_hash.t × Z.t) :=
let? '(context_value, node_value) :=
expand_node context_value (Micheline.root_value value_value) in
let? _depth := check_depth node_value in
let? '(context_value, key_value) :=
expr_to_address_in_context context_value value_value in
let? '(context_value, size_value) :=
Error_monad.trace_value
(Build_extensible "Expression_already_registered" unit tt)
(Storage.Global_constants.Map.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
context_value key_value value_value) in
return? (context_value, key_value, (Z.of_int size_value)).