Skip to main content

🍲 Dal_errors_repr.v

Translated OCaml

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.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.

Module Dal_subscribe_rollup_invalid_slot_index.
  Record record : Set := Build {
    given : Dal_slot_repr.Index.t;
    maximum : Dal_slot_repr.Index.t;
  }.
  Definition with_given given (r : record) :=
    Build given r.(maximum).
  Definition with_maximum maximum (r : record) :=
    Build r.(given) maximum.
End Dal_subscribe_rollup_invalid_slot_index.
Definition Dal_subscribe_rollup_invalid_slot_index :=
  Dal_subscribe_rollup_invalid_slot_index.record.

Module Dal_endorsement_unexpected_size.
  Record record : Set := Build {
    expected : int;
    got : int;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(got).
  Definition with_got got (r : record) :=
    Build r.(expected) got.
End Dal_endorsement_unexpected_size.
Definition Dal_endorsement_unexpected_size :=
  Dal_endorsement_unexpected_size.record.

Module Dal_publish_slot_header_invalid_index.
  Record record : Set := Build {
    given : Dal_slot_repr.Index.t;
    maximum : Dal_slot_repr.Index.t;
  }.
  Definition with_given given (r : record) :=
    Build given r.(maximum).
  Definition with_maximum maximum (r : record) :=
    Build r.(given) maximum.
End Dal_publish_slot_header_invalid_index.
Definition Dal_publish_slot_header_invalid_index :=
  Dal_publish_slot_header_invalid_index.record.

Module Dal_publish_slot_header_candidate_with_low_fees.
  Record record : Set := Build {
    proposed_fees : Tez_repr.t;
  }.
  Definition with_proposed_fees proposed_fees (r : record) :=
    Build proposed_fees.
End Dal_publish_slot_header_candidate_with_low_fees.
Definition Dal_publish_slot_header_candidate_with_low_fees :=
  Dal_publish_slot_header_candidate_with_low_fees.record.

Module Dal_endorsement_size_limit_exceeded.
  Record record : Set := Build {
    maximum_size : int;
    got : int;
  }.
  Definition with_maximum_size maximum_size (r : record) :=
    Build maximum_size r.(got).
  Definition with_got got (r : record) :=
    Build r.(maximum_size) got.
End Dal_endorsement_size_limit_exceeded.
Definition Dal_endorsement_size_limit_exceeded :=
  Dal_endorsement_size_limit_exceeded.record.

Module Dal_publish_slot_header_duplicate.
  Record record : Set := Build {
    slot : Dal_slot_repr.t;
  }.
  Definition with_slot slot (r : record) :=
    Build slot.
End Dal_publish_slot_header_duplicate.
Definition Dal_publish_slot_header_duplicate :=
  Dal_publish_slot_header_duplicate.record.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let description := "Bad index for slot" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "dal_subscribe_rollup_invalid_slot_index"
      "DAL slot invalid index for subscribing sc rollup" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Dal_slot_repr.Index.t × Dal_slot_repr.Index.t) ⇒
            let '(given, maximum) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal ": Given "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal ". Maximum "
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.Char_literal "." % char
                            CamlinternalFormatBasics.End_of_format))))))
                "%s: Given %a. Maximum %a.") description Dal_slot_repr.Index.pp
              given Dal_slot_repr.Index.pp maximum))
      (Data_encoding.obj2
        (Data_encoding.req None None "given" Dal_slot_repr.Index.encoding)
        (Data_encoding.req None None "got" Dal_slot_repr.Index.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_subscribe_rollup_invalid_slot_index" then
            let '{|
              Dal_subscribe_rollup_invalid_slot_index.given := given;
                Dal_subscribe_rollup_invalid_slot_index.maximum := maximum
                |} := cast Dal_subscribe_rollup_invalid_slot_index payload in
            Some (given, maximum)
          else None
        end)
      (fun (function_parameter : Dal_slot_repr.Index.t × Dal_slot_repr.Index.t)
        ⇒
        let '(given, maximum) := function_parameter in
        Build_extensible "Dal_subscribe_rollup_invalid_slot_index"
          Dal_subscribe_rollup_invalid_slot_index
          {| Dal_subscribe_rollup_invalid_slot_index.given := given;
            Dal_subscribe_rollup_invalid_slot_index.maximum := maximum; |}) in
  let description :=
    "Data-availability layer will be enabled in a future proposal." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.dal_disabled" "DAL is disabled" description
      (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") description))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_feature_disabled" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Dal_feature_disabled" unit tt) in
  let description :=
    "The endorsement for data availability has a different size" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "dal_endorsement_unexpected_size" "DAL endorsement unexpected size"
      description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : int × int) ⇒
            let '(expected, got) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal ": Expected "
                    (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.String_literal ". Got "
                        (CamlinternalFormatBasics.Int
                          CamlinternalFormatBasics.Int_d
                          CamlinternalFormatBasics.No_padding
                          CamlinternalFormatBasics.No_precision
                          (CamlinternalFormatBasics.Char_literal "." % char
                            CamlinternalFormatBasics.End_of_format))))))
                "%s: Expected %d. Got %d.") description expected got))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected_size" Data_encoding.int31)
        (Data_encoding.req None None "got" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_endorsement_unexpected_size" then
            let '{|
              Dal_endorsement_unexpected_size.expected := expected;
                Dal_endorsement_unexpected_size.got := got
                |} := cast Dal_endorsement_unexpected_size payload in
            Some (expected, got)
          else None
        end)
      (fun (function_parameter : int × int) ⇒
        let '(expected, got) := function_parameter in
        Build_extensible "Dal_endorsement_unexpected_size"
          Dal_endorsement_unexpected_size
          {| Dal_endorsement_unexpected_size.expected := expected;
            Dal_endorsement_unexpected_size.got := got; |}) in
  let description := "Slot index above hard limit" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "dal_slot_index_negative_orabove_hard_limit"
      "DAL slot index negative or above hard limit" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal ": Maximum allowed "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Char_literal "." % char
                        CamlinternalFormatBasics.End_of_format))))
                "%s: Maximum allowed %a.") description Dal_slot_repr.Index.pp
              Dal_slot_repr.Index.max_value)) Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_slot_index_above_hard_limit" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Dal_slot_index_above_hard_limit" unit tt) in
  let description := "Bad index for slot header" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "dal_publish_slot_header_invalid_index" "DAL slot header invalid index"
      description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Dal_slot_repr.Index.t × Dal_slot_repr.Index.t) ⇒
            let '(given, maximum) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal ": Given "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal ". Maximum "
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.Char_literal "." % char
                            CamlinternalFormatBasics.End_of_format))))))
                "%s: Given %a. Maximum %a.") description Dal_slot_repr.Index.pp
              given Dal_slot_repr.Index.pp maximum))
      (Data_encoding.obj2
        (Data_encoding.req None None "given" Dal_slot_repr.Index.encoding)
        (Data_encoding.req None None "got" Dal_slot_repr.Index.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_publish_slot_header_invalid_index" then
            let '{|
              Dal_publish_slot_header_invalid_index.given := given;
                Dal_publish_slot_header_invalid_index.maximum := maximum
                |} := cast Dal_publish_slot_header_invalid_index payload in
            Some (given, maximum)
          else None
        end)
      (fun (function_parameter : Dal_slot_repr.Index.t × Dal_slot_repr.Index.t)
        ⇒
        let '(given, maximum) := function_parameter in
        Build_extensible "Dal_publish_slot_header_invalid_index"
          Dal_publish_slot_header_invalid_index
          {| Dal_publish_slot_header_invalid_index.given := given;
            Dal_publish_slot_header_invalid_index.maximum := maximum; |}) in
  let description := "Slot header with too low fees" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "dal_publish_slot_header_with_low_fees" "DAL slot header with low fees"
      description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (proposed : Tez_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal ": Proposed fees "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Char_literal "." % char
                        CamlinternalFormatBasics.End_of_format))))
                "%s: Proposed fees %a.") description Tez_repr.pp proposed))
      (Data_encoding.obj1
        (Data_encoding.req None None "proposed" Tez_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_publish_slot_header_candidate_with_low_fees"
            then
            let '{|
              Dal_publish_slot_header_candidate_with_low_fees.proposed_fees := proposed_fees
                |} :=
              cast Dal_publish_slot_header_candidate_with_low_fees payload in
            Some proposed_fees
          else None
        end)
      (fun (proposed_fees : Tez_repr.t) ⇒
        Build_extensible "Dal_publish_slot_header_candidate_with_low_fees"
          Dal_publish_slot_header_candidate_with_low_fees
          {|
            Dal_publish_slot_header_candidate_with_low_fees.proposed_fees :=
              proposed_fees; |}) in
  let description := "The endorsement for data availability is a too big" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "dal_endorsement_size_limit_exceeded" "DAL endorsement exceeded the limit"
      description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : int × int) ⇒
            let '(maximum_size, got) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal ": Maximum is "
                    (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.String_literal ". Got "
                        (CamlinternalFormatBasics.Int
                          CamlinternalFormatBasics.Int_d
                          CamlinternalFormatBasics.No_padding
                          CamlinternalFormatBasics.No_precision
                          (CamlinternalFormatBasics.Char_literal "." % char
                            CamlinternalFormatBasics.End_of_format))))))
                "%s: Maximum is %d. Got %d.") description maximum_size got))
      (Data_encoding.obj2
        (Data_encoding.req None None "maximum_size" Data_encoding.int31)
        (Data_encoding.req None None "got" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_endorsement_size_limit_exceeded" then
            let '{|
              Dal_endorsement_size_limit_exceeded.maximum_size := maximum_size;
                Dal_endorsement_size_limit_exceeded.got := got
                |} := cast Dal_endorsement_size_limit_exceeded payload in
            Some (maximum_size, got)
          else None
        end)
      (fun (function_parameter : int × int) ⇒
        let '(maximum_size, got) := function_parameter in
        Build_extensible "Dal_endorsement_size_limit_exceeded"
          Dal_endorsement_size_limit_exceeded
          {| Dal_endorsement_size_limit_exceeded.maximum_size := maximum_size;
            Dal_endorsement_size_limit_exceeded.got := got; |}) in
  let description := "A slot header for this slot was already proposed" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "dal_publish_slot_heade_duplicate" "DAL publish slot header duplicate"
      description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (_proposed : Dal_slot_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      (Data_encoding.obj1
        (Data_encoding.req None None "proposed" Dal_slot_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_publish_slot_header_duplicate" then
            let '{| Dal_publish_slot_header_duplicate.slot := slot |} :=
              cast Dal_publish_slot_header_duplicate payload in
            Some slot
          else None
        end)
      (fun (slot : Dal_slot_repr.t) ⇒
        Build_extensible "Dal_publish_slot_header_duplicate"
          Dal_publish_slot_header_duplicate
          {| Dal_publish_slot_header_duplicate.slot := slot; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Dal_rollup_already_subscribed_to_slot"
      "DAL rollup already subscribed to slot" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Sc_rollup_repr.t × Dal_slot_repr.Index.t) ⇒
            let '(rollup, slot_index) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Rollup "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " is already subscribed to data availability slot "
                      (CamlinternalFormatBasics.Alpha
                        CamlinternalFormatBasics.End_of_format))))
                "Rollup %a is already subscribed to data availability slot %a")
              Sc_rollup_repr.pp rollup Dal_slot_repr.Index.pp slot_index))
      (Data_encoding.obj2
        (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
        (Data_encoding.req None None "slot_index" Dal_slot_repr.Index.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dal_rollup_already_registered_to_slot" then
            let '(rollup, slot_index) :=
              cast (Sc_rollup_repr.t × Dal_slot_repr.Index.t) payload in
            Some (rollup, slot_index)
          else None
        end)
      (fun (function_parameter : Sc_rollup_repr.t × Dal_slot_repr.Index.t) ⇒
        let '(rollup, slot_index) := function_parameter in
        Build_extensible "Dal_rollup_already_registered_to_slot"
          (Sc_rollup_repr.t × Dal_slot_repr.Index.t) (rollup, slot_index)) in
  let description :=
    "Requested List of subscribed rollups to slot at a future level" in
  Error_monad.register_error_kind Error_monad.Temporary
    "Dal_requested_subscriptions_at_future_level"
    "Requested list of subscribed dal slots at a future level" description
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter :
          Raw_level_repr.raw_level × Raw_level_repr.raw_level) ⇒
          let '(current_level, future_level) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "The list of subscribed dal slot indices has been requested for level "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    ", but the current level is "
                    (CamlinternalFormatBasics.Alpha
                      CamlinternalFormatBasics.End_of_format))))
              "The list of subscribed dal slot indices has been requested for level %a, but the current level is %a")
            Raw_level_repr.pp future_level Raw_level_repr.pp current_level))
    (Data_encoding.obj2
      (Data_encoding.req None None "current_level" Raw_level_repr.encoding)
      (Data_encoding.req None None "future_level" Raw_level_repr.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Dal_requested_subscriptions_at_future_level" then
          let '(current_level, future_level) :=
            cast (Raw_level_repr.t × Raw_level_repr.t) payload in
          Some (current_level, future_level)
        else None
      end)
    (fun (function_parameter :
      Raw_level_repr.raw_level × Raw_level_repr.raw_level) ⇒
      let '(current_level, future_level) := function_parameter in
      Build_extensible "Dal_requested_subscriptions_at_future_level"
        (Raw_level_repr.t × Raw_level_repr.t) (current_level, future_level)).