Skip to main content

✒️ Contract_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.

Inductive t : Set :=
| Implicit : Signature.public_key_hash t
| Originated : Contract_hash.t t.

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    let compare (l1 : t) (l2 : t) : int :=
      match (l1, l2) with
      | (Implicit pkh1, Implicit pkh2)
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkh1
          pkh2
      | (Originated h1, Originated h2)Contract_hash.compare h1 h2
      | (Implicit _, Originated _) ⇒ (-1)
      | (Originated _, Implicit _) ⇒ 1
      end in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_Make_include]
Definition op_eq := Compare_Make_include.(Compare.S.op_eq).

Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).

Definition op_lt := Compare_Make_include.(Compare.S.op_lt).

Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).

Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).

Definition op_gt := Compare_Make_include.(Compare.S.op_gt).

Definition compare := Compare_Make_include.(Compare.S.compare).

Definition equal := Compare_Make_include.(Compare.S.equal).

Definition max := Compare_Make_include.(Compare.S.max).

Definition min := Compare_Make_include.(Compare.S.min).

Definition contract : Set := t.

Definition blake2b_hash_size : Saturation_repr.t :=
  Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
    (Cache_memory_helpers.string_size_gen 20).

Definition public_key_hash_in_memory_size : Saturation_repr.t :=
  Cache_memory_helpers.op_plusexclamation
    (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
      Cache_memory_helpers.word_size) blake2b_hash_size.

Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
  match function_parameter with
  | Implicit _
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      public_key_hash_in_memory_size
  | Originated _
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      blake2b_hash_size
  end.

Definition to_b58check (function_parameter : t) : string :=
  match function_parameter with
  | Implicit pbk
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) pbk
  | Originated h_valueContract_hash.to_b58check h_value
  end.

Definition of_b58check (s_value : string) : M? t :=
  match Base58.decode s_value with
  | Some data
    match data with
    | Build_extensible tag _ payload
      if String.eqb tag "Data" then
        let h_value :=
          cast Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload
            in
        return? (Implicit (Signature.Ed25519Hash h_value))
      else if String.eqb tag "Data" then
        let h_value :=
          cast Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload
            in
        return? (Implicit (Signature.Secp256k1Hash h_value))
      else if String.eqb tag "Data" then
        let h_value :=
          cast P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) payload in
        return? (Implicit (Signature.P256Hash h_value))
      else if String.eqb tag "Data" then
        let h_value := cast Contract_hash.t payload in
        return? (Originated h_value)
      else
        Error_monad.error_value
          (Build_extensible "Invalid_contract_notation" string s_value)
    end
  | None
    Error_monad.error_value
      (Build_extensible "Invalid_contract_notation" string s_value)
  end.

Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  match function_parameter with
  | Implicit pbk
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) ppf pbk
  | Originated h_valueContract_hash.pp ppf h_value
  end.

Definition pp_short (ppf : Format.formatter) (function_parameter : t) : unit :=
  match function_parameter with
  | Implicit pbk
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short) ppf pbk
  | Originated h_valueContract_hash.pp_short ppf h_value
  end.

Definition cases {A : Set} (is_contract : A option t) (to_contract : t A)
  : list (Data_encoding.case A) :=
  [
    Data_encoding.case_value "Implicit" None (Data_encoding.Tag 0)
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
      (fun (k_value : A) ⇒
        match is_contract k_value with
        | Some (Implicit k_value) ⇒ Some k_value
        | _None
        end)
      (fun (k_value : Signature.public_key_hash) ⇒
        to_contract (Implicit k_value));
    Data_encoding.case_value "Originated" None (Data_encoding.Tag 1)
      (Data_encoding.Fixed.add_padding Contract_hash.encoding 1)
      (fun (k_value : A) ⇒
        match is_contract k_value with
        | Some (Originated k_value) ⇒ Some k_value
        | _None
        end)
      (fun (k_value : Contract_hash.t) ⇒ to_contract (Originated k_value))
  ].

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.def "contract_id" (Some "A contract handle")
    (Some
      "A contract notation as given to an RPC or inside scripts. Can be a base58 implicit contract hash or a base58 originated contract hash.")
    (Data_encoding.splitted
      (Data_encoding.conv to_b58check
        (fun (s_value : string) ⇒
          match of_b58check s_value with
          | Pervasives.Ok s_values_value
          | Pervasives.Error _
            Data_encoding.Json.cannot_destruct
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid contract notation."
                  CamlinternalFormatBasics.End_of_format)
                "Invalid contract notation.")
          end) None Data_encoding.string_value)
      (Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
        (cases (fun (x_value : t) ⇒ Some x_value)
          (fun (x_value : t) ⇒ x_value)))).

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "contract.invalid_contract_notation" "Invalid contract notation"
    "A malformed contract notation was given to an RPC or in a script."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (x_value : string) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Invalid contract notation "
                (CamlinternalFormatBasics.Caml_string
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format))
              "Invalid contract notation %S") x_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "notation" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_contract_notation" then
          let loc_value := cast string payload in
          Some loc_value
        else None
      end)
    (fun (loc_value : string) ⇒
      Build_extensible "Invalid_contract_notation" string loc_value).

Definition implicit_contract (id : Signature.public_key_hash) : t :=
  Implicit id.

Definition is_implicit (function_parameter : t)
  : option Signature.public_key_hash :=
  match function_parameter with
  | Implicit m_valueSome m_value
  | Originated _None
  end.

Definition is_originated (function_parameter : t) : option Contract_hash.t :=
  match function_parameter with
  | Implicit _None
  | Originated h_valueSome h_value
  end.

Definition originated_contract (nonce_value : Origination_nonce.t) : t :=
  let data :=
    Data_encoding.Binary.to_bytes_exn None Origination_nonce.encoding
      nonce_value in
  Originated (Contract_hash.hash_bytes None [ data ]).

#[bypass_check(guard)]
Definition originated_contracts (function_parameter : Origination_nonce.t)
  : Origination_nonce.t list t :=
  let '{|
    Origination_nonce.t.operation_hash := first_hash;
      Origination_nonce.t.origination_index := first
      |} := function_parameter in
  fun (function_parameter : Origination_nonce.t) ⇒
    let
      '{|
        Origination_nonce.t.operation_hash := last_hash;
          Origination_nonce.t.origination_index := last
          |} as origination_nonce := function_parameter in
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (Operation_hash.equal first_hash last_hash) in
    let fix contracts (acc_value : list t) (origination_index : int32)
      {struct origination_index} : list t :=
      if origination_index <i32 first then
        acc_value
      else
        let origination_nonce :=
          Origination_nonce.t.with_origination_index origination_index
            origination_nonce in
        let acc_value := cons (originated_contract origination_nonce) acc_value
          in
        contracts acc_value (Int32.pred origination_index) in
    contracts nil (Int32.pred last).

Definition rpc_arg : RPC_arg.arg t :=
  let construct := to_b58check in
  let destruct (hash_value : string) : Pervasives.result t string :=
    Result.map_error
      (fun (function_parameter : Error_monad.trace Error_monad._error) ⇒
        let '_ := function_parameter in
        "Cannot parse contract id") (of_b58check hash_value) in
  RPC_arg.make (Some "A contract identifier encoded in b58check.") "contract_id"
    destruct construct tt.

Module Index.
  Definition t : Set := contract.

  Definition path_length : int := 1.

  Definition to_path (c_value : t) (l_value : list string) : list string :=
    let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
    let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
    cons key_value l_value.

  Definition of_path (function_parameter : list string) : option t :=
    match function_parameter with
    | cons key_value []
      Option.bind (Hex.to_bytes (Hex.Hex key_value))
        (Data_encoding.Binary.of_bytes_opt encoding)
    | _None
    end.

  Definition rpc_arg : RPC_arg.arg t := rpc_arg.

  Definition encoding : Data_encoding.encoding t := encoding.

  Definition compare : t t int := compare.

  (* Index *)
  Definition module :=
    {|
      Storage_description.INDEX.path_length := path_length;
      Storage_description.INDEX.to_path := to_path;
      Storage_description.INDEX.of_path := of_path;
      Storage_description.INDEX.rpc_arg := rpc_arg;
      Storage_description.INDEX.encoding := encoding;
      Storage_description.INDEX.compare := compare
    |}.
End Index.
Definition Index := Index.module.