Skip to main content

🍬 Script_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
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_nodesof_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_valuereturn? 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.