Skip to main content

🦏 Sc_rollup_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.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.

Module Address.
  Definition prefix : string := "scr1".

  Definition encoded_size : int := 37.

  Definition decoded_prefix : string :=
    String.String "001" ("v" ++ String.String "132" (String.String "217" "")).

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "Sc_rollup_hash" in
      let title := "A smart contract rollup address" in
      let b58check_prefix := decoded_prefix in
      let size_value := Some 20 in
      {|
        Blake2B.PrefixedName.name := name;
        Blake2B.PrefixedName.title := title;
        Blake2B.PrefixedName.size_value := size_value;
        Blake2B.PrefixedName.b58check_prefix := b58check_prefix
      |}).

Inclusion of the module [H]
  Definition t := H.(S.HASH.t).

  Definition name := H.(S.HASH.name).

  Definition title := H.(S.HASH.title).

  Definition pp := H.(S.HASH.pp).

  Definition pp_short := H.(S.HASH.pp_short).

  Definition op_eq := H.(S.HASH.op_eq).

  Definition op_ltgt := H.(S.HASH.op_ltgt).

  Definition op_lt := H.(S.HASH.op_lt).

  Definition op_lteq := H.(S.HASH.op_lteq).

  Definition op_gteq := H.(S.HASH.op_gteq).

  Definition op_gt := H.(S.HASH.op_gt).

  Definition compare := H.(S.HASH.compare).

  Definition equal := H.(S.HASH.equal).

  Definition max := H.(S.HASH.max).

  Definition min := H.(S.HASH.min).

  Definition hash_bytes := H.(S.HASH.hash_bytes).

  Definition hash_string := H.(S.HASH.hash_string).

  Definition zero := H.(S.HASH.zero).

  Definition size_value := H.(S.HASH.size_value).

  Definition to_bytes := H.(S.HASH.to_bytes).

  Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).

  Definition to_b58check := H.(S.HASH.to_b58check).

  Definition to_short_b58check := H.(S.HASH.to_short_b58check).

  Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).

  Definition b58check_encoding := H.(S.HASH.b58check_encoding).

  Definition encoding := H.(S.HASH.encoding).

  Definition rpc_arg := H.(S.HASH.rpc_arg).

  Definition Map := H.(S.HASH.Map).

Init function; without side-effects in Coq
Inclusion of the module [Path_encoding_Make_hex_include]
  Definition to_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.to_path).

  Definition of_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.of_path).

  Definition path_length :=
    Path_encoding_Make_hex_include.(Path_encoding.S.path_length).

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

Definition state_hash_prefix : string :=
  String.String "017" (String.String "144" ("z" ++ String.String "202" "")).

Module State_hash.
  Definition prefix : string := "scs1".

  Definition encoded_size : int := 54.

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "state_hash" in
      let title := "The hash of the VM state of a smart contract rollup" in
      let b58check_prefix := state_hash_prefix in
      let size_value {A : Set} : option A :=
        None in
      {|
        Blake2B.PrefixedName.name := name;
        Blake2B.PrefixedName.title := title;
        Blake2B.PrefixedName.size_value := size_value;
        Blake2B.PrefixedName.b58check_prefix := b58check_prefix
      |}).

Inclusion of the module [H]
  Definition t := H.(S.HASH.t).

  Definition name := H.(S.HASH.name).

  Definition title := H.(S.HASH.title).

  Definition pp := H.(S.HASH.pp).

  Definition pp_short := H.(S.HASH.pp_short).

  Definition op_eq := H.(S.HASH.op_eq).

  Definition op_ltgt := H.(S.HASH.op_ltgt).

  Definition op_lt := H.(S.HASH.op_lt).

  Definition op_lteq := H.(S.HASH.op_lteq).

  Definition op_gteq := H.(S.HASH.op_gteq).

  Definition op_gt := H.(S.HASH.op_gt).

  Definition compare := H.(S.HASH.compare).

  Definition equal := H.(S.HASH.equal).

  Definition max := H.(S.HASH.max).

  Definition min := H.(S.HASH.min).

  Definition hash_bytes := H.(S.HASH.hash_bytes).

  Definition hash_string := H.(S.HASH.hash_string).

  Definition zero := H.(S.HASH.zero).

  Definition size_value := H.(S.HASH.size_value).

  Definition to_bytes := H.(S.HASH.to_bytes).

  Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).

  Definition to_b58check := H.(S.HASH.to_b58check).

  Definition to_short_b58check := H.(S.HASH.to_short_b58check).

  Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).

  Definition b58check_encoding := H.(S.HASH.b58check_encoding).

  Definition encoding := H.(S.HASH.encoding).

  Definition rpc_arg := H.(S.HASH.rpc_arg).

  Definition Map := H.(S.HASH.Map).

Init function; without side-effects in Coq
Inclusion of the module [Path_encoding_Make_hex_include]
  Definition to_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.to_path).

  Definition of_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.of_path).

  Definition path_length :=
    Path_encoding_Make_hex_include.(Path_encoding.S.path_length).

  Definition context_hash_to_state_hash (h_value : Context_hash.t) : M? t :=
    if Compare.Int.equal size_value Context_hash.size_value then
      return? (of_bytes_exn (Context_hash.to_bytes h_value))
    else
      Error_monad.error_value (Build_extensible "Asserted" unit tt).

  Inductive unreachable : Set :=.

  (* Axiom hash_bytes : forall {A : Set}, unreachable -> A. *)

  (* Axiom hash_string : forall {A : Set}, unreachable -> A. *)
End State_hash.

Definition t : Set := Address.t.

Definition description : string :=
  Pervasives.op_caret
    "A smart contract rollup is identified by a base58 address starting with "
    Address.prefix.

Definition error_description : string :=
  Format.sprintf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal
        "A smart contract rollup address must be a valid hash starting with '"
        (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
          (CamlinternalFormatBasics.String_literal "'."
            CamlinternalFormatBasics.End_of_format)))
      "A smart contract rollup address must be a valid hash starting with '%s'.")
    Address.prefix.

Init function; without side-effects in Coq
Definition init_module3 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "rollup.invalid_smart_contract_rollup_address"
    "Invalid smart contract rollup address" error_description
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (x_value : string) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Invalid smart contract rollup address "
                (CamlinternalFormatBasics.Caml_string
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format))
              "Invalid smart contract rollup address %S") x_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "address" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_sc_rollup_address" then
          let loc_value := cast string payload in
          Some loc_value
        else None
      end)
    (fun (loc_value : string) ⇒
      Build_extensible "Invalid_sc_rollup_address" string loc_value).

Definition of_b58check (s_value : string)
  : Pervasives.result Address.t string :=
  let error_value {A : Set} (function_parameter : unit)
    : Pervasives.result A string :=
    let '_ := function_parameter in
    Pervasives.Error
      (Format.sprintf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Invalid_sc_rollup_address "
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              CamlinternalFormatBasics.End_of_format))
          "Invalid_sc_rollup_address %s") s_value) in
  match Base58.decode s_value with
  | Some data
    match data with
    | Build_extensible tag _ payload
      if String.eqb tag "Data" then
        let hash_value := cast Address.t payload in
        return? hash_value
      else error_value tt
    end
  | _error_value tt
  end.

Definition pp : Format.formatter Address.t unit := Address.pp.

Definition encoding : Data_encoding.encoding Address.t :=
  Data_encoding.def "rollup_address" (Some "A smart contract rollup address")
    (Some description)
    (Data_encoding.conv_with_guard Address.to_b58check of_b58check None
      Data_encoding.string_value).

Definition rpc_arg : RPC_arg.arg Address.t :=
  let construct := Address.to_b58check in
  let destruct (hash_value : string) : Pervasives.result Address.t string :=
    Result.map_error
      (fun (function_parameter : string) ⇒
        let '_ := function_parameter in
        error_description) (of_b58check hash_value) in
  RPC_arg.make (Some "A smart contract rollup address.") "sc_rollup_address"
    destruct construct tt.

Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
  let '_ := function_parameter in
  Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
    (Cache_memory_helpers.string_size_gen Address.size_value).

Definition Staker := Signature.Public_key_hash.

Module Index.
  Definition t : Set := Address.t.

  Definition path_length : M? int := return? 1.

  Definition to_path (c_value : Address.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 Address.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 Address.t := rpc_arg.

  Definition encoding : Data_encoding.encoding Address.t := encoding.

  Definition compare : Address.t Address.t int := Address.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.

Module Number_of_ticks.
  Definition Bounded_Int64_include :=
    Bounded.Int64
      (let min_value := 0 in
      let max_value := Int64.max_int in
      {|
        Bounded.BOUNDS.min_value := min_value;
        Bounded.BOUNDS.max_value := max_value
      |}).

Inclusion of the module [Bounded_Int64_include]
  Definition t := Bounded_Int64_include.(Bounded.S.t).

  Definition min_value := Bounded_Int64_include.(Bounded.S.min_value).

  Definition max_value := Bounded_Int64_include.(Bounded.S.max_value).

  Definition op_eq := Bounded_Int64_include.(Bounded.S.op_eq).

  Definition op_ltgt := Bounded_Int64_include.(Bounded.S.op_ltgt).

  Definition op_lt := Bounded_Int64_include.(Bounded.S.op_lt).

  Definition op_lteq := Bounded_Int64_include.(Bounded.S.op_lteq).

  Definition op_gteq := Bounded_Int64_include.(Bounded.S.op_gteq).

  Definition op_gt := Bounded_Int64_include.(Bounded.S.op_gt).

  Definition compare := Bounded_Int64_include.(Bounded.S.compare).

  Definition equal := Bounded_Int64_include.(Bounded.S.equal).

  Definition max := Bounded_Int64_include.(Bounded.S.max).

  Definition min := Bounded_Int64_include.(Bounded.S.min).

  Definition encoding := Bounded_Int64_include.(Bounded.S.encoding).

  Definition pp := Bounded_Int64_include.(Bounded.S.pp).

  Definition to_value := Bounded_Int64_include.(Bounded.S.to_value).

  Definition of_value := Bounded_Int64_include.(Bounded.S.of_value).

  Definition zero : M? t :=
    match of_value 0 with
    | Some zeroreturn? zero
    | NoneError_monad.error_value (Build_extensible "Asserted" unit tt)
    end.
End Number_of_ticks.