🦏 Sc_rollup_dissection_chunk_repr.v
Translated 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_value ⇒ Sc_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.
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_value ⇒ Sc_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).
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).