🎫 Ticket_hash_builder.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.Gas_limit_repr.
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.Ticket_hash_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
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.Ticket_hash_repr.
Init function; without side-effects in Coq
Definition init_module : unit :=
Error_monad.register_error_kind Error_monad.Branch "Failed_to_hash_node"
"Failed to hash node"
"Failed to hash node for a key in the ticket-balance table"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Failed to hash node for a key in the ticket-balance table"
CamlinternalFormatBasics.End_of_format)
"Failed to hash node for a key in the ticket-balance table")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failed_to_hash_node" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Failed_to_hash_node" unit tt).
Definition hash_bytes_cost (bytes_value : bytes) : Gas_limit_repr.cost :=
let op_plus := Saturation_repr.add in
let v0 := Saturation_repr.safe_int (Bytes.length bytes_value) in
let lsr := Saturation_repr.shift_right in
Gas_limit_repr.atomic_step_cost
(op_plus (Saturation_repr.safe_int 200) (op_plus v0 (lsr v0 2))).
Definition hash_of_node {A : Set}
(ctxt : Raw_context.t) (node_value : Script_repr.michelson_node A)
: M? (Ticket_hash_repr.t × Raw_context.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt (Script_repr.strip_locations_cost node_value)
in
let node_value := Micheline.strip_locations node_value in
let? bytes_value :=
Result.of_option
(Error_monad.trace_of_error
(Build_extensible "Failed_to_hash_node" unit tt))
(Data_encoding.Binary.to_bytes_opt None Script_repr.expr_encoding
node_value) in
let? ctxt := Raw_context.consume_gas ctxt (hash_bytes_cost bytes_value) in
return?
((Ticket_hash_repr.of_script_expr_hash
(Script_expr_hash.hash_bytes None [ bytes_value ])), ctxt).
Definition hash_of_node_uncarbonated {A : Set}
(node_value : Micheline.node A Michelson_v1_primitives.prim)
: M? Ticket_hash_repr.t :=
let node_value := Micheline.strip_locations node_value in
let? bytes_value :=
Result.of_option
(Error_monad.trace_of_error
(Build_extensible "Failed_to_hash_node" unit tt))
(Data_encoding.Binary.to_bytes_opt None Script_repr.expr_encoding
node_value) in
return?
(Ticket_hash_repr.of_script_expr_hash
(Script_expr_hash.hash_bytes None [ bytes_value ])).
Definition make
(ctxt : Raw_context.t)
(ticketer :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(ty_value :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(contents :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(owner :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
: M? (Ticket_hash_repr.t × Raw_context.t) :=
hash_of_node ctxt
(Micheline.Seq Micheline.dummy_location
[ ticketer; ty_value; contents; owner ]).
Definition make_uncarbonated
(ticketer :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(ty_value :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(contents :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(owner :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
: M? Ticket_hash_repr.t :=
hash_of_node_uncarbonated
(Micheline.Seq Micheline.dummy_location
[ ticketer; ty_value; contents; owner ]).
Error_monad.register_error_kind Error_monad.Branch "Failed_to_hash_node"
"Failed to hash node"
"Failed to hash node for a key in the ticket-balance table"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Failed to hash node for a key in the ticket-balance table"
CamlinternalFormatBasics.End_of_format)
"Failed to hash node for a key in the ticket-balance table")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failed_to_hash_node" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Failed_to_hash_node" unit tt).
Definition hash_bytes_cost (bytes_value : bytes) : Gas_limit_repr.cost :=
let op_plus := Saturation_repr.add in
let v0 := Saturation_repr.safe_int (Bytes.length bytes_value) in
let lsr := Saturation_repr.shift_right in
Gas_limit_repr.atomic_step_cost
(op_plus (Saturation_repr.safe_int 200) (op_plus v0 (lsr v0 2))).
Definition hash_of_node {A : Set}
(ctxt : Raw_context.t) (node_value : Script_repr.michelson_node A)
: M? (Ticket_hash_repr.t × Raw_context.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt (Script_repr.strip_locations_cost node_value)
in
let node_value := Micheline.strip_locations node_value in
let? bytes_value :=
Result.of_option
(Error_monad.trace_of_error
(Build_extensible "Failed_to_hash_node" unit tt))
(Data_encoding.Binary.to_bytes_opt None Script_repr.expr_encoding
node_value) in
let? ctxt := Raw_context.consume_gas ctxt (hash_bytes_cost bytes_value) in
return?
((Ticket_hash_repr.of_script_expr_hash
(Script_expr_hash.hash_bytes None [ bytes_value ])), ctxt).
Definition hash_of_node_uncarbonated {A : Set}
(node_value : Micheline.node A Michelson_v1_primitives.prim)
: M? Ticket_hash_repr.t :=
let node_value := Micheline.strip_locations node_value in
let? bytes_value :=
Result.of_option
(Error_monad.trace_of_error
(Build_extensible "Failed_to_hash_node" unit tt))
(Data_encoding.Binary.to_bytes_opt None Script_repr.expr_encoding
node_value) in
return?
(Ticket_hash_repr.of_script_expr_hash
(Script_expr_hash.hash_bytes None [ bytes_value ])).
Definition make
(ctxt : Raw_context.t)
(ticketer :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(ty_value :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(contents :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(owner :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
: M? (Ticket_hash_repr.t × Raw_context.t) :=
hash_of_node ctxt
(Micheline.Seq Micheline.dummy_location
[ ticketer; ty_value; contents; owner ]).
Definition make_uncarbonated
(ticketer :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(ty_value :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(contents :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
(owner :
Micheline.node Micheline.canonical_location Michelson_v1_primitives.prim)
: M? Ticket_hash_repr.t :=
hash_of_node_uncarbonated
(Micheline.Seq Micheline.dummy_location
[ ticketer; ty_value; contents; owner ]).