Skip to main content

🎫 Ticket_hash_builder.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
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 ]).