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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.

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

  Definition encoded_size : int := 37.

  Definition decoded_prefix : string := "\001v\132\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]
Init function; without side-effects in Coq
  Definition init_module2 : unit :=
    let msg := "Error while generating rollup address" in
    Error_monad.register_error_kind Error_monad.Permanent
      "rollup.error_smart_contract_rollup_address_generation" msg msg
      (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") msg))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Error_sc_rollup_address_generation" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Error_sc_rollup_address_generation" unit tt).

  Definition from_nonce (nonce_value : Origination_nonce.t) : M? t :=
    (fun (function_parameter : option bytes) ⇒
      match function_parameter with
      | None
        Error_monad.error_value
          (Build_extensible "Error_sc_rollup_address_generation" unit tt)
      | Some nonce_valuereturn? (hash_bytes None [ nonce_value ])
      end)
      (Data_encoding.Binary.to_bytes_opt None Origination_nonce.encoding
        nonce_value).
End Address.

Definition commitment_hash_prefix : string := "\017\144\021d".

Module Commitment_hash.
  Definition prefix : string := "scc1".

  Definition encoded_size : int := 54.

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "commitment_hash" in
      let title := "The hash of a commitment of a smart contract rollup" in
      let b58check_prefix := commitment_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).
End Commitment_hash.

Definition state_hash_prefix : string := "\017\144z\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).
End State_hash.

Definition t : Set := Address.t.

Definition Staker := Signature.Public_key_hash.

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_module5 : 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.

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

  Definition path_length : int := 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) : option Address.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 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 Commitment_hash_index.
  Include Commitment_hash.

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

Definition Number_of_messages :=
  Bounded.Int32.Make
    (let min_int := 1 in
    let max_int := 4096 in
    {|
      Bounded.Int32.BOUNDS.min_int := min_int;
      Bounded.Int32.BOUNDS.max_int := max_int
    |}).

Definition Number_of_ticks :=
  Bounded.Int32.Make
    (let min_int := 1 in
    let max_int := Int32.max_int in
    {|
      Bounded.Int32.BOUNDS.min_int := min_int;
      Bounded.Int32.BOUNDS.max_int := max_int
    |}).

Module Commitment.
  Module t.
    Record record : Set := Build {
      compressed_state : State_hash.t;
      inbox_level : Raw_level_repr.t;
      predecessor : Commitment_hash.t;
      number_of_messages : Number_of_messages.(Bounded.Int32.S.t);
      number_of_ticks : Number_of_ticks.(Bounded.Int32.S.t);
    }.
    Definition with_compressed_state compressed_state (r : record) :=
      Build compressed_state r.(inbox_level) r.(predecessor)
        r.(number_of_messages) r.(number_of_ticks).
    Definition with_inbox_level inbox_level (r : record) :=
      Build r.(compressed_state) inbox_level r.(predecessor)
        r.(number_of_messages) r.(number_of_ticks).
    Definition with_predecessor predecessor (r : record) :=
      Build r.(compressed_state) r.(inbox_level) predecessor
        r.(number_of_messages) r.(number_of_ticks).
    Definition with_number_of_messages number_of_messages (r : record) :=
      Build r.(compressed_state) r.(inbox_level) r.(predecessor)
        number_of_messages r.(number_of_ticks).
    Definition with_number_of_ticks number_of_ticks (r : record) :=
      Build r.(compressed_state) r.(inbox_level) r.(predecessor)
        r.(number_of_messages) number_of_ticks.
  End t.
  Definition t := t.record.

  Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
    let '{|
      t.compressed_state := compressed_state;
        t.inbox_level := inbox_level;
        t.predecessor := predecessor;
        t.number_of_messages := number_of_messages;
        t.number_of_ticks := number_of_ticks
        |} := function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<v 2>"
                CamlinternalFormatBasics.End_of_format) "<v 2>"))
          (CamlinternalFormatBasics.String_literal "SCORU Commitment:"
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@ " 1 0)
              (CamlinternalFormatBasics.String_literal "compressed_state: "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Formatting_lit
                    (CamlinternalFormatBasics.Break "@ " 1 0)
                    (CamlinternalFormatBasics.String_literal "inbox_level: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Formatting_lit
                          (CamlinternalFormatBasics.Break "@ " 1 0)
                          (CamlinternalFormatBasics.String_literal
                            "predecessor: "
                            (CamlinternalFormatBasics.Alpha
                              (CamlinternalFormatBasics.Formatting_lit
                                (CamlinternalFormatBasics.Break "@ " 1 0)
                                (CamlinternalFormatBasics.String_literal
                                  "number_of_messages: "
                                  (CamlinternalFormatBasics.Int
                                    CamlinternalFormatBasics.Int_d
                                    CamlinternalFormatBasics.No_padding
                                    CamlinternalFormatBasics.No_precision
                                    (CamlinternalFormatBasics.Formatting_lit
                                      (CamlinternalFormatBasics.Break "@ " 1 0)
                                      (CamlinternalFormatBasics.String_literal
                                        "number_of_ticks: "
                                        (CamlinternalFormatBasics.Int
                                          CamlinternalFormatBasics.Int_d
                                          CamlinternalFormatBasics.No_padding
                                          CamlinternalFormatBasics.No_precision
                                          (CamlinternalFormatBasics.Formatting_lit
                                            CamlinternalFormatBasics.Close_box
                                            CamlinternalFormatBasics.End_of_format))))))))))))))))))
        "@[<v 2>SCORU Commitment:@ compressed_state: %a@ inbox_level: %a@ predecessor: %a@ number_of_messages: %d@ number_of_ticks: %d@]")
      State_hash.pp compressed_state Raw_level_repr.pp inbox_level
      Commitment_hash.pp predecessor
      (Int32.to_int
        (Number_of_messages.(Bounded.Int32.S.to_int32) number_of_messages))
      (Int32.to_int (Number_of_ticks.(Bounded.Int32.S.to_int32) number_of_ticks)).

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.compressed_state := compressed_state;
            t.inbox_level := inbox_level;
            t.predecessor := predecessor;
            t.number_of_messages := number_of_messages;
            t.number_of_ticks := number_of_ticks
            |} := function_parameter in
        (compressed_state, inbox_level, predecessor, number_of_messages,
          number_of_ticks))
      (fun (function_parameter :
        State_hash.t × Raw_level_repr.t × Commitment_hash.t ×
          Number_of_messages.(Bounded.Int32.S.t) ×
          Number_of_ticks.(Bounded.Int32.S.t)) ⇒
        let
          '(compressed_state, inbox_level, predecessor, number_of_messages,
            number_of_ticks) := function_parameter in
        {| t.compressed_state := compressed_state; t.inbox_level := inbox_level;
          t.predecessor := predecessor;
          t.number_of_messages := number_of_messages;
          t.number_of_ticks := number_of_ticks; |}) None
      (Data_encoding.obj5
        (Data_encoding.req None None "compressed_state" State_hash.encoding)
        (Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
        (Data_encoding.req None None "predecessor" Commitment_hash.encoding)
        (Data_encoding.req None None "number_of_messages"
          Number_of_messages.(Bounded.Int32.S.encoding))
        (Data_encoding.req None None "number_of_ticks"
          Number_of_ticks.(Bounded.Int32.S.encoding))).

  Definition hash_value (commitment : t) : Commitment_hash.t :=
    let commitment_bytes :=
      Data_encoding.Binary.to_bytes_exn None encoding commitment in
    Commitment_hash.hash_bytes None [ commitment_bytes ].
End Commitment.

Module Kind.
  Inductive t : Set :=
  | Example_arith : t.

  Definition example_arith_case : Data_encoding.case t :=
    Data_encoding.case_value "Example_arith smart contract rollup kind" None
      (Data_encoding.Tag 0) Data_encoding.unit_value
      (fun (function_parameter : t) ⇒
        let 'Example_arith := function_parameter in
        Some tt)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Example_arith).

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.union (Some (Variant.Build "Uint16" unit tt))
      [ example_arith_case ].

  Definition equal (x_value : t) (y_value : t) : bool :=
    let '(Example_arith, Example_arith) := (x_value, y_value) in
    true.

  Definition pp (fmt : Format.formatter) (kind_value : t) : unit :=
    let 'Example_arith := kind_value in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Example_arith"
          CamlinternalFormatBasics.End_of_format) "Example_arith").
End Kind.