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.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Internal_errors.
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 in_memory_size (function_parameter : t) : Saturation_repr.t :=
  match function_parameter with
  | Implicit _
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      Cache_memory_helpers.public_key_hash_in_memory_size
  | Originated _
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      Cache_memory_helpers.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 implicit_of_b58data (function_parameter : Base58.data)
  : option Signature.public_key_hash :=
  match function_parameter 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
      Some (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
      Some (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
      Some (Signature.P256Hash h_value)
    else None
  end.

Definition originated_of_b58data (function_parameter : Base58.data)
  : option Contract_hash.t :=
  match function_parameter with
  | Build_extensible tag _ payload
    if String.eqb tag "Data" then
      let h_value := cast Contract_hash.t payload in
      Some h_value
    else None
  end.

Definition contract_of_b58data (data : Base58.data) : option t :=
  match implicit_of_b58data data with
  | Some pkhSome (Implicit pkh)
  | None
    match originated_of_b58data data with
    | Some contract_hashSome (Originated contract_hash)
    | NoneNone
    end
  end.

Definition of_b58check_gen {A : Set}
  (of_b58data : Base58.data option A) (s_value : string) : M? A :=
  match Base58.decode s_value with
  | Some data
    match of_b58data data with
    | Some c_valuereturn? c_value
    | None
      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 of_b58check : string M? t := of_b58check_gen contract_of_b58data.

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 implicit_case {A : Set}
  (proj : A option Signature.public_key_hash)
  (inj : Signature.public_key_hash A) : Data_encoding.case A :=
  Data_encoding.case_value "Implicit" None (Data_encoding.Tag 0)
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding) proj inj.

Definition originated_case {A : Set}
  (proj : A option Contract_hash.t) (inj : Contract_hash.t A)
  : Data_encoding.case A :=
  Data_encoding.case_value "Originated" None (Data_encoding.Tag 1)
    (Data_encoding.Fixed.add_padding Contract_hash.encoding 1) proj inj.

Definition cases {A : Set} (is_contract : A option t) (to_contract : t A)
  : list (Data_encoding.case A) :=
  [
    implicit_case
      (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));
    originated_case
      (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_gen {A B C : Set}
  (id_extra : string) (title_extra : string) (can_be : string)
  (cases : (A option A) (B B) list (Data_encoding.case C))
  (to_b58check : C string) (of_b58data : Base58.data option C)
  : Data_encoding.encoding C :=
  Data_encoding.def (Pervasives.op_caret "contract_id" id_extra)
    (Some (Pervasives.op_caret "A contract handle" title_extra))
    (Some
      (Pervasives.op_caret
        "A contract notation as given to an RPC or inside scripts. Can be a base58 "
        can_be))
    (Data_encoding.splitted
      (Data_encoding.conv to_b58check
        (fun (s_value : string) ⇒
          match of_b58check_gen of_b58data 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 : A) ⇒ Some x_value)
          (fun (x_value : B) ⇒ x_value)))).

Definition encoding : Data_encoding.encoding t :=
  encoding_gen "" ""
    "implicit contract hash or a base58 originated contract hash." cases
    to_b58check contract_of_b58data.

Definition implicit_encoding
  : Data_encoding.encoding Signature.public_key_hash :=
  encoding_gen ".implicit" " -- implicit account" "implicit contract hash."
    (fun (proj : Signature.public_key_hash option Signature.public_key_hash)
      ⇒
      fun (inj : Signature.public_key_hash Signature.public_key_hash) ⇒
        [ implicit_case proj inj ])
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check)
    implicit_of_b58data.

Definition originated_encoding : Data_encoding.encoding Contract_hash.t :=
  encoding_gen ".originated" " -- originated account"
    "originated contract hash."
    (fun (proj : Contract_hash.t option Contract_hash.t) ⇒
      fun (inj : Contract_hash.t Contract_hash.t) ⇒
        [ originated_case proj inj ]) Contract_hash.to_b58check
    originated_of_b58data.

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 originated_contract (nonce_value : Origination_nonce.t) : t :=
  Originated (Contract_hash.of_nonce nonce_value).

#[bypass_check(guard)]
Definition originated_contracts (function_parameter : Origination_nonce.t)
  : Origination_nonce.t M? (list Contract_hash.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? '_ :=
      Internal_errors.do_assert (Operation_hash.equal first_hash last_hash) in
    let fix contracts
      (acc_value : list Contract_hash.t) (origination_index : int32)
      {struct origination_index} : list Contract_hash.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 (Contract_hash.of_nonce origination_nonce) acc_value in
        contracts acc_value (Int32.pred origination_index) in
    return? (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 := t.

  Definition path_length : M? int := return? 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) : M? (option t) :=
    match function_parameter with
    | cons key_value []
      return?
        (Option.bind (Hex.to_bytes (Hex.Hex key_value))
          (Data_encoding.Binary.of_bytes_opt encoding))
    | _return? 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.

Definition of_b58data : Base58.data option t := contract_of_b58data.