Skip to main content

🌍 Global_constants_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
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
  | NoneError_monad.fail (Build_extensible "Nonexistent_global" unit tt)
  | Some value_valuereturn? (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.fail
                    (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.fail
                  (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.fail (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)).