Skip to main content

🦏 Sc_rollup_dissection_chunk_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.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.

Module t.
  Record record : Set := Build {
    state_hash : option Sc_rollup_repr.State_hash.t;
    tick : Sc_rollup_tick_repr.t;
  }.
  Definition with_state_hash state_hash (r : record) :=
    Build state_hash r.(tick).
  Definition with_tick tick (r : record) :=
    Build r.(state_hash) tick.
End t.
Definition t := t.record.

Definition equal (function_parameter : t) : t bool :=
  let '{| t.state_hash := state_hash; t.tick := tick |} := function_parameter in
  fun (chunk2 : t) ⇒
    (Option.equal Sc_rollup_repr.State_hash.equal state_hash
      chunk2.(t.state_hash)) && (Sc_rollup_tick_repr.equal tick chunk2.(t.tick)).

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{| t.state_hash := state_hash; t.tick := tick |} :=
        function_parameter in
      (state_hash, tick))
    (fun (function_parameter :
      option Sc_rollup_repr.State_hash.t × Sc_rollup_tick_repr.t) ⇒
      let '(state_hash, tick) := function_parameter in
      {| t.state_hash := state_hash; t.tick := tick; |}) None
    (Data_encoding.obj2
      (Data_encoding.opt None None "state" Sc_rollup_repr.State_hash.encoding)
      (Data_encoding.req None None "tick" Sc_rollup_tick_repr.encoding)).

Module Dissection_number_of_sections_mismatch.
  Record record : Set := Build {
    expected : Z.t;
    given : Z.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(given).
  Definition with_given given (r : record) :=
    Build r.(expected) given.
End Dissection_number_of_sections_mismatch.
Definition Dissection_number_of_sections_mismatch :=
  Dissection_number_of_sections_mismatch.record.

Module Dissection_start_hash_mismatch.
  Record record : Set := Build {
    expected : option Sc_rollup_repr.State_hash.t;
    given : option Sc_rollup_repr.State_hash.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(given).
  Definition with_given given (r : record) :=
    Build r.(expected) given.
End Dissection_start_hash_mismatch.
Definition Dissection_start_hash_mismatch :=
  Dissection_start_hash_mismatch.record.

Module Dissection_edge_ticks_mismatch.
  Record record : Set := Build {
    dissection_start_tick : Sc_rollup_tick_repr.t;
    dissection_stop_tick : Sc_rollup_tick_repr.t;
    chunk_start_tick : Sc_rollup_tick_repr.t;
    chunk_stop_tick : Sc_rollup_tick_repr.t;
  }.
  Definition with_dissection_start_tick dissection_start_tick (r : record) :=
    Build dissection_start_tick r.(dissection_stop_tick) r.(chunk_start_tick)
      r.(chunk_stop_tick).
  Definition with_dissection_stop_tick dissection_stop_tick (r : record) :=
    Build r.(dissection_start_tick) dissection_stop_tick r.(chunk_start_tick)
      r.(chunk_stop_tick).
  Definition with_chunk_start_tick chunk_start_tick (r : record) :=
    Build r.(dissection_start_tick) r.(dissection_stop_tick) chunk_start_tick
      r.(chunk_stop_tick).
  Definition with_chunk_stop_tick chunk_stop_tick (r : record) :=
    Build r.(dissection_start_tick) r.(dissection_stop_tick)
      r.(chunk_start_tick) chunk_stop_tick.
End Dissection_edge_ticks_mismatch.
Definition Dissection_edge_ticks_mismatch :=
  Dissection_edge_ticks_mismatch.record.

Definition pp_state_hash
  : Format.formatter option Sc_rollup_repr.State_hash.t unit :=
  Format.pp_print_option
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "None"
                CamlinternalFormatBasics.End_of_format) "None")))
    Sc_rollup_repr.State_hash.pp.

Definition pp_hash_opt
  (fmt : Format.formatter)
  (function_parameter : option Sc_rollup_repr.State_hash.t) : unit :=
  match function_parameter with
  | None
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "None"
          CamlinternalFormatBasics.End_of_format) "None")
  | Some x_valueSc_rollup_repr.State_hash.pp fmt x_value
  end.

Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  let '{| t.state_hash := state_hash; t.tick := tick |} := function_parameter in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal "State hash:"
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.Formatting_lit
            (CamlinternalFormatBasics.Break "@ " 1 0)
            (CamlinternalFormatBasics.String_literal "Tick: "
              (CamlinternalFormatBasics.Alpha
                CamlinternalFormatBasics.End_of_format)))))
      "State hash:%a@ Tick: %a") pp_state_hash state_hash Sc_rollup_tick_repr.pp
    tick.

Axiom default_check : int t t list t M? unit.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let description := "Mismatch in the number of sections in the dissection" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Dissection_number_of_sections_mismatch" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Z.t × Z.t) ⇒
            let '(expected, given) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The number of sections must be equal to "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " instead of "
                      (CamlinternalFormatBasics.Alpha
                        CamlinternalFormatBasics.End_of_format))))
                "The number of sections must be equal to %a instead of %a")
              Z.pp_print expected Z.pp_print given))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Data_encoding.n_value)
        (Data_encoding.req None None "given" Data_encoding.n_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_number_of_sections_mismatch" then
            let '{|
              Dissection_number_of_sections_mismatch.expected := expected;
                Dissection_number_of_sections_mismatch.given := given
                |} := cast Dissection_number_of_sections_mismatch payload in
            Some (expected, given)
          else None
        end)
      (fun (function_parameter : Z.t × Z.t) ⇒
        let '(expected, given) := function_parameter in
        Build_extensible "Dissection_number_of_sections_mismatch"
          Dissection_number_of_sections_mismatch
          {| Dissection_number_of_sections_mismatch.expected := expected;
            Dissection_number_of_sections_mismatch.given := given; |}) in
  let description := "Invalid number of sections in the dissection" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Dissection_invalid_number_of_sections" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (n_value : Z.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "A dissection with "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " sections can never be valid"
                      CamlinternalFormatBasics.End_of_format)))
                "A dissection with %a sections can never be valid") Z.pp_print
              n_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "value" Data_encoding.n_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_invalid_number_of_sections" then
            let n_value := cast Z.t payload in
            Some n_value
          else None
        end)
      (fun (n_value : Z.t) ⇒
        Build_extensible "Dissection_invalid_number_of_sections" Z.t n_value) in
  let description := "Mismatch in the start hash of the dissection" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Dissection_start_hash_mismatch" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            option Sc_rollup_repr.State_hash.t ×
              option Sc_rollup_repr.State_hash.t) ⇒
            let '(given, expected) := function_parameter in
            match given with
            | None
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal
                    "The start hash must not be None"
                    CamlinternalFormatBasics.End_of_format)
                  "The start hash must not be None")
            | Some _
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal
                    "The start hash should be equal to "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal
                        ", but the provided hash is "
                        (CamlinternalFormatBasics.Alpha
                          CamlinternalFormatBasics.End_of_format))))
                  "The start hash should be equal to %a, but the provided hash is %a")
                pp_hash_opt expected pp_hash_opt given
            end))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
        (Data_encoding.req None None "given"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_start_hash_mismatch" then
            let '{|
              Dissection_start_hash_mismatch.expected := expected;
                Dissection_start_hash_mismatch.given := given
                |} := cast Dissection_start_hash_mismatch payload in
            Some (expected, given)
          else None
        end)
      (fun (function_parameter :
        option Sc_rollup_repr.State_hash.t × option Sc_rollup_repr.State_hash.t)
        ⇒
        let '(expected, given) := function_parameter in
        Build_extensible "Dissection_start_hash_mismatch"
          Dissection_start_hash_mismatch
          {| Dissection_start_hash_mismatch.expected := expected;
            Dissection_start_hash_mismatch.given := given; |}) in
  let description := "Mismatch in the stop hash of the dissection" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Dissection_stop_hash_mismatch" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (h_value : option Sc_rollup_repr.State_hash.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The stop hash should not be equal to "
                  (CamlinternalFormatBasics.Alpha
                    CamlinternalFormatBasics.End_of_format))
                "The stop hash should not be equal to %a") pp_hash_opt h_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "hash"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_stop_hash_mismatch" then
            let hopt := cast (option Sc_rollup_repr.State_hash.t) payload in
            Some hopt
          else None
        end)
      (fun (hopt : option Sc_rollup_repr.State_hash.t) ⇒
        Build_extensible "Dissection_stop_hash_mismatch"
          (option Sc_rollup_repr.State_hash.t) hopt) in
  let description := "Mismatch in the edge ticks of the dissection" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Dissection_edge_ticks_mismatch" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Sc_rollup_tick_repr.t × Sc_rollup_tick_repr.t ×
              Sc_rollup_tick_repr.t × Sc_rollup_tick_repr.t) ⇒
            let
              '(dissection_start_tick, dissection_stop_tick, chunk_start_tick,
                chunk_stop_tick) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "We should have dissection_start_tick("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ") = "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal
                          " and dissection_stop_tick("
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.String_literal ") = "
                              (CamlinternalFormatBasics.Alpha
                                CamlinternalFormatBasics.End_of_format))))))))
                "We should have dissection_start_tick(%a) = %a and dissection_stop_tick(%a) = %a")
              Sc_rollup_tick_repr.pp dissection_start_tick
              Sc_rollup_tick_repr.pp chunk_start_tick Sc_rollup_tick_repr.pp
              dissection_stop_tick Sc_rollup_tick_repr.pp chunk_stop_tick))
      (Data_encoding.obj4
        (Data_encoding.req None None "dissection_start_tick"
          Sc_rollup_tick_repr.encoding)
        (Data_encoding.req None None "dissection_stop_tick"
          Sc_rollup_tick_repr.encoding)
        (Data_encoding.req None None "chunk_start_tick"
          Sc_rollup_tick_repr.encoding)
        (Data_encoding.req None None "chunk_stop_tick"
          Sc_rollup_tick_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_edge_ticks_mismatch" then
            let e_value := cast Dissection_edge_ticks_mismatch payload in
            Some
              (e_value.(Dissection_edge_ticks_mismatch.dissection_start_tick),
                e_value.(Dissection_edge_ticks_mismatch.dissection_stop_tick),
                e_value.(Dissection_edge_ticks_mismatch.chunk_start_tick),
                e_value.(Dissection_edge_ticks_mismatch.chunk_stop_tick))
          else None
        end)
      (fun (function_parameter :
        Sc_rollup_tick_repr.t × Sc_rollup_tick_repr.t × Sc_rollup_tick_repr.t ×
          Sc_rollup_tick_repr.t) ⇒
        let
          '(dissection_start_tick, dissection_stop_tick, chunk_start_tick,
            chunk_stop_tick) := function_parameter in
        Build_extensible "Dissection_edge_ticks_mismatch"
          Dissection_edge_ticks_mismatch
          {|
            Dissection_edge_ticks_mismatch.dissection_start_tick :=
              dissection_start_tick;
            Dissection_edge_ticks_mismatch.dissection_stop_tick :=
              dissection_stop_tick;
            Dissection_edge_ticks_mismatch.chunk_start_tick := chunk_start_tick;
            Dissection_edge_ticks_mismatch.chunk_stop_tick := chunk_stop_tick;
            |}) in
  let description := "Ticks should only increase in dissection" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Dissection_ticks_not_increasing" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf description)) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_ticks_not_increasing" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Dissection_ticks_not_increasing" unit tt) in
  let description :=
    "Maximum tick increment in a section cannot be more than half total dissection length"
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Dissection_invalid_distribution" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf description)) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_invalid_distribution" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Dissection_invalid_distribution" unit tt) in
  let description := "Cannot recover from a blocked state in a dissection" in
  Error_monad.register_error_kind Error_monad.Permanent
    "Dissection_invalid_successive_states_shape" description description
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.pp_print_string ppf description)) Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Dissection_invalid_successive_states_shape" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Dissection_invalid_successive_states_shape" unit tt).