🪜 Level_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.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Module t.
Record record : Set := Build {
level : Raw_level_repr.t;
level_position : int32;
cycle : Cycle_repr.t;
cycle_position : int32;
expected_commitment : bool;
}.
Definition with_level level (r : record) :=
Build level r.(level_position) r.(cycle) r.(cycle_position)
r.(expected_commitment).
Definition with_level_position level_position (r : record) :=
Build r.(level) level_position r.(cycle) r.(cycle_position)
r.(expected_commitment).
Definition with_cycle cycle (r : record) :=
Build r.(level) r.(level_position) cycle r.(cycle_position)
r.(expected_commitment).
Definition with_cycle_position cycle_position (r : record) :=
Build r.(level) r.(level_position) r.(cycle) cycle_position
r.(expected_commitment).
Definition with_expected_commitment expected_commitment (r : record) :=
Build r.(level) r.(level_position) r.(cycle) r.(cycle_position)
expected_commitment.
End t.
Definition t := t.record.
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
let compare (function_parameter : t) : t → int :=
let '{| t.level := l1 |} := function_parameter in
fun (function_parameter : t) ⇒
let '{| t.level := l2 |} := function_parameter in
Raw_level_repr.compare l1 l2 in
{|
Compare.COMPARABLE.compare := compare
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Module t.
Record record : Set := Build {
level : Raw_level_repr.t;
level_position : int32;
cycle : Cycle_repr.t;
cycle_position : int32;
expected_commitment : bool;
}.
Definition with_level level (r : record) :=
Build level r.(level_position) r.(cycle) r.(cycle_position)
r.(expected_commitment).
Definition with_level_position level_position (r : record) :=
Build r.(level) level_position r.(cycle) r.(cycle_position)
r.(expected_commitment).
Definition with_cycle cycle (r : record) :=
Build r.(level) r.(level_position) cycle r.(cycle_position)
r.(expected_commitment).
Definition with_cycle_position cycle_position (r : record) :=
Build r.(level) r.(level_position) r.(cycle) cycle_position
r.(expected_commitment).
Definition with_expected_commitment expected_commitment (r : record) :=
Build r.(level) r.(level_position) r.(cycle) r.(cycle_position)
expected_commitment.
End t.
Definition t := t.record.
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
let compare (function_parameter : t) : t → int :=
let '{| t.level := l1 |} := function_parameter in
fun (function_parameter : t) ⇒
let '{| t.level := l2 |} := function_parameter in
Raw_level_repr.compare l1 l2 in
{|
Compare.COMPARABLE.compare := compare
|}).
Inclusion of the module [Compare_Make_include]
Definition op_eq := Compare_Make_include.(Compare.S.op_eq).
Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).
Definition op_lt := Compare_Make_include.(Compare.S.op_lt).
Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).
Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).
Definition op_gt := Compare_Make_include.(Compare.S.op_gt).
Definition compare := Compare_Make_include.(Compare.S.compare).
Definition equal := Compare_Make_include.(Compare.S.equal).
Definition max := Compare_Make_include.(Compare.S.max).
Definition min := Compare_Make_include.(Compare.S.min).
Definition level : Set := t.
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
let '{| t.level := level |} := function_parameter in
Raw_level_repr.pp ppf level.
Definition pp_full (ppf : Format.formatter) (l_value : t) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " (cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))))))))
"%a.%ld (cycle %a.%ld)") Raw_level_repr.pp l_value.(t.level)
l_value.(t.level_position) Cycle_repr.pp l_value.(t.cycle)
l_value.(t.cycle_position).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.level := level;
t.level_position := level_position;
t.cycle := cycle;
t.cycle_position := cycle_position;
t.expected_commitment := expected_commitment
|} := function_parameter in
(level, level_position, cycle, cycle_position, expected_commitment))
(fun (function_parameter :
Raw_level_repr.t × int32 × Cycle_repr.t × int32 × bool) ⇒
let
'(level, level_position, cycle, cycle_position, expected_commitment) :=
function_parameter in
{| t.level := level; t.level_position := level_position; t.cycle := cycle;
t.cycle_position := cycle_position;
t.expected_commitment := expected_commitment; |}) None
(Data_encoding.obj5
(Data_encoding.req None
(Some
"The level of the block relative to genesis. This is also the Shell's notion of level.")
"level" Raw_level_repr.encoding)
(Data_encoding.req None
(Some
"The level of the block relative to the successor of the genesis block. More precisely, it is the position of the block relative to the block that starts the ""Alpha family"" of protocols, which includes all protocols except Genesis (that is, from 001 onwards).")
"level_position" Data_encoding.int32_value)
(Data_encoding.req None
(Some
"The current cycle's number. Note that cycles are a protocol-specific notion. As a result, the cycle number starts at 0 with the first block of the Alpha family of protocols.")
"cycle" Cycle_repr.encoding)
(Data_encoding.req None
(Some
"The current level of the block relative to the first block of the current cycle.")
"cycle_position" Data_encoding.int32_value)
(Data_encoding.req None
(Some
"Tells whether the baker of this block has to commit a seed nonce hash.")
"expected_commitment" Data_encoding.bool_value)).
Definition diff_value (function_parameter : t) : t → int32 :=
let '{| t.level := l1 |} := function_parameter in
fun (function_parameter : t) ⇒
let '{| t.level := l2 |} := function_parameter in
(Raw_level_repr.to_int32 l1) -i32 (Raw_level_repr.to_int32 l2).
Module cycle_era.
Record record : Set := Build {
first_level : Raw_level_repr.t;
first_cycle : Cycle_repr.t;
blocks_per_cycle : int32;
blocks_per_commitment : int32;
}.
Definition with_first_level first_level (r : record) :=
Build first_level r.(first_cycle) r.(blocks_per_cycle)
r.(blocks_per_commitment).
Definition with_first_cycle first_cycle (r : record) :=
Build r.(first_level) first_cycle r.(blocks_per_cycle)
r.(blocks_per_commitment).
Definition with_blocks_per_cycle blocks_per_cycle (r : record) :=
Build r.(first_level) r.(first_cycle) blocks_per_cycle
r.(blocks_per_commitment).
Definition with_blocks_per_commitment blocks_per_commitment (r : record) :=
Build r.(first_level) r.(first_cycle) r.(blocks_per_cycle)
blocks_per_commitment.
End cycle_era.
Definition cycle_era := cycle_era.record.
Definition cycle_eras : Set := list cycle_era.
Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).
Definition op_lt := Compare_Make_include.(Compare.S.op_lt).
Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).
Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).
Definition op_gt := Compare_Make_include.(Compare.S.op_gt).
Definition compare := Compare_Make_include.(Compare.S.compare).
Definition equal := Compare_Make_include.(Compare.S.equal).
Definition max := Compare_Make_include.(Compare.S.max).
Definition min := Compare_Make_include.(Compare.S.min).
Definition level : Set := t.
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
let '{| t.level := level |} := function_parameter in
Raw_level_repr.pp ppf level.
Definition pp_full (ppf : Format.formatter) (l_value : t) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " (cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))))))))
"%a.%ld (cycle %a.%ld)") Raw_level_repr.pp l_value.(t.level)
l_value.(t.level_position) Cycle_repr.pp l_value.(t.cycle)
l_value.(t.cycle_position).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.level := level;
t.level_position := level_position;
t.cycle := cycle;
t.cycle_position := cycle_position;
t.expected_commitment := expected_commitment
|} := function_parameter in
(level, level_position, cycle, cycle_position, expected_commitment))
(fun (function_parameter :
Raw_level_repr.t × int32 × Cycle_repr.t × int32 × bool) ⇒
let
'(level, level_position, cycle, cycle_position, expected_commitment) :=
function_parameter in
{| t.level := level; t.level_position := level_position; t.cycle := cycle;
t.cycle_position := cycle_position;
t.expected_commitment := expected_commitment; |}) None
(Data_encoding.obj5
(Data_encoding.req None
(Some
"The level of the block relative to genesis. This is also the Shell's notion of level.")
"level" Raw_level_repr.encoding)
(Data_encoding.req None
(Some
"The level of the block relative to the successor of the genesis block. More precisely, it is the position of the block relative to the block that starts the ""Alpha family"" of protocols, which includes all protocols except Genesis (that is, from 001 onwards).")
"level_position" Data_encoding.int32_value)
(Data_encoding.req None
(Some
"The current cycle's number. Note that cycles are a protocol-specific notion. As a result, the cycle number starts at 0 with the first block of the Alpha family of protocols.")
"cycle" Cycle_repr.encoding)
(Data_encoding.req None
(Some
"The current level of the block relative to the first block of the current cycle.")
"cycle_position" Data_encoding.int32_value)
(Data_encoding.req None
(Some
"Tells whether the baker of this block has to commit a seed nonce hash.")
"expected_commitment" Data_encoding.bool_value)).
Definition diff_value (function_parameter : t) : t → int32 :=
let '{| t.level := l1 |} := function_parameter in
fun (function_parameter : t) ⇒
let '{| t.level := l2 |} := function_parameter in
(Raw_level_repr.to_int32 l1) -i32 (Raw_level_repr.to_int32 l2).
Module cycle_era.
Record record : Set := Build {
first_level : Raw_level_repr.t;
first_cycle : Cycle_repr.t;
blocks_per_cycle : int32;
blocks_per_commitment : int32;
}.
Definition with_first_level first_level (r : record) :=
Build first_level r.(first_cycle) r.(blocks_per_cycle)
r.(blocks_per_commitment).
Definition with_first_cycle first_cycle (r : record) :=
Build r.(first_level) first_cycle r.(blocks_per_cycle)
r.(blocks_per_commitment).
Definition with_blocks_per_cycle blocks_per_cycle (r : record) :=
Build r.(first_level) r.(first_cycle) blocks_per_cycle
r.(blocks_per_commitment).
Definition with_blocks_per_commitment blocks_per_commitment (r : record) :=
Build r.(first_level) r.(first_cycle) r.(blocks_per_cycle)
blocks_per_commitment.
End cycle_era.
Definition cycle_era := cycle_era.record.
Definition cycle_eras : Set := list cycle_era.
Init function; without side-effects in Coq
Definition init_module1 : unit :=
Error_monad.register_error_kind Error_monad.Temporary
"level_repr.invalid_cycle_eras" "Invalid cycle eras"
"The cycles eras are not valid: empty list or non-decreasing first levels or first cycles."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The cycles eras are not valid: empty list or non-decreasing first levels or first cycles."
CamlinternalFormatBasics.End_of_format)
"The cycles eras are not valid: empty list or non-decreasing first levels or first cycles.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_cycle_eras" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_cycle_eras" unit tt).
Definition create_cycle_eras (cycle_eras : list cycle_era)
: M? (list cycle_era) :=
match cycle_eras with
| [] ⇒
Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
| cons newest_era older_eras ⇒
let fix aux (era : cycle_era) (older_eras : list cycle_era) : M? unit :=
let '{|
cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle
|} := era in
match older_eras with
|
cons
({|
cycle_era.first_level := first_level_of_previous_era;
cycle_era.first_cycle := first_cycle_of_previous_era
|} as previous_era) even_older_eras ⇒
if
(Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
(Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
then
aux previous_era even_older_eras
else
Error_monad.error_value
(Build_extensible "Invalid_cycle_eras" unit tt)
| [] ⇒ return? tt
end in
let? '_ := aux newest_era older_eras in
return? cycle_eras
end.
Definition add_cycle_era (new_era : cycle_era) (cycle_eras : list cycle_era)
: M? (list cycle_era) := create_cycle_eras (cons new_era cycle_eras).
Definition cycle_era_encoding : Data_encoding.encoding cycle_era :=
Data_encoding.conv
(fun (function_parameter : cycle_era) ⇒
let '{|
cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle;
cycle_era.blocks_per_cycle := blocks_per_cycle;
cycle_era.blocks_per_commitment := blocks_per_commitment
|} := function_parameter in
(first_level, first_cycle, blocks_per_cycle, blocks_per_commitment))
(fun (function_parameter : Raw_level_repr.t × Cycle_repr.t × int32 × int32)
⇒
let
'(first_level, first_cycle, blocks_per_cycle, blocks_per_commitment) :=
function_parameter in
{| cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle;
cycle_era.blocks_per_cycle := blocks_per_cycle;
cycle_era.blocks_per_commitment := blocks_per_commitment; |}) None
(Data_encoding.obj4
(Data_encoding.req None (Some "The first level of a new cycle era.")
"first_level" Raw_level_repr.encoding)
(Data_encoding.req None (Some "The first cycle of a new cycle era.")
"first_cycle" Cycle_repr.encoding)
(Data_encoding.req None
(Some
"The value of the blocks_per_cycle constant used during the cycle era starting with first_level.")
"blocks_per_cycle" Data_encoding.int32_value)
(Data_encoding.req None
(Some
"The value of the blocks_per_commitment constant used during the cycle era starting with first_level.")
"blocks_per_commitment" Data_encoding.int32_value)).
Definition cycle_eras_encoding : Data_encoding.encoding (list cycle_era) :=
Data_encoding.conv_with_guard (fun (eras : list cycle_era) ⇒ eras)
(fun (eras : list cycle_era) ⇒
match create_cycle_eras eras with
| Pervasives.Ok eras ⇒ Pervasives.Ok eras
| Pervasives.Error _ ⇒ Pervasives.Error "Invalid cycle eras"
end) None (Data_encoding.list_value None cycle_era_encoding).
Definition current_era {A : Set} (eras : list A) : M? A :=
match eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons cycle_era _ ⇒ return? cycle_era
end.
Definition root_level (cycle_eras : list cycle_era) : M? t :=
let first_era := List.last_opt cycle_eras in
let? first_era :=
match first_era with
| Some first_era ⇒ return? first_era
| None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end in
return?
{| t.level := first_era.(cycle_era.first_level); t.level_position := 0;
t.cycle := Cycle_repr.root_value; t.cycle_position := 0;
t.expected_commitment := false; |}.
Definition era_of_level
(cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level)
: M? cycle_era :=
let fix aux (function_parameter : list cycle_era) : M? cycle_era :=
match function_parameter with
| cons ({| cycle_era.first_level := first_level |} as era) previous_eras ⇒
if Raw_level_repr.op_gteq level first_level then
return? era
else
aux previous_eras
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end in
aux cycle_eras.
Definition era_of_cycle (cycle_eras : list cycle_era) (cycle : Cycle_repr.t)
: M? cycle_era :=
let fix aux (function_parameter : list cycle_era) : M? cycle_era :=
match function_parameter with
| cons ({| cycle_era.first_cycle := first_cycle |} as era) previous_eras ⇒
if Cycle_repr.op_gteq cycle first_cycle then
return? era
else
aux previous_eras
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end in
aux cycle_eras.
Definition level_from_raw_with_era
(era : cycle_era) (first_level_in_alpha_family : Raw_level_repr.raw_level)
(level : Raw_level_repr.raw_level) : M? t :=
let '{|
cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle;
cycle_era.blocks_per_cycle := blocks_per_cycle;
cycle_era.blocks_per_commitment := blocks_per_commitment
|} := era in
let level_position_in_era := Raw_level_repr.diff_value level first_level in
if level_position_in_era ≥i32 0 then
let cycles_since_era_start := level_position_in_era /i32 blocks_per_cycle in
let? cycle :=
Cycle_repr.add first_cycle (Int32.to_int cycles_since_era_start) in
let cycle_position := Int32.rem level_position_in_era blocks_per_cycle in
let level_position :=
Raw_level_repr.diff_value level first_level_in_alpha_family in
let expected_commitment :=
(Int32.rem cycle_position blocks_per_commitment) =i32
(Int32.pred blocks_per_commitment) in
return?
{| t.level := level; t.level_position := level_position; t.cycle := cycle;
t.cycle_position := cycle_position;
t.expected_commitment := expected_commitment; |}
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition level_from_raw_aux_exn
(cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level) : M? t :=
let? first_level_in_alpha_family :=
match List.rev cycle_eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons {| cycle_era.first_level := first_level |} _ ⇒ return? first_level
end in
let? era := era_of_level cycle_eras level in
level_from_raw_with_era era first_level_in_alpha_family level.
Definition level_from_raw
(cycle_eras : list cycle_era) (l_value : Raw_level_repr.raw_level) : M? t :=
level_from_raw_aux_exn cycle_eras l_value.
Error_monad.register_error_kind Error_monad.Temporary
"level_repr.invalid_cycle_eras" "Invalid cycle eras"
"The cycles eras are not valid: empty list or non-decreasing first levels or first cycles."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The cycles eras are not valid: empty list or non-decreasing first levels or first cycles."
CamlinternalFormatBasics.End_of_format)
"The cycles eras are not valid: empty list or non-decreasing first levels or first cycles.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_cycle_eras" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_cycle_eras" unit tt).
Definition create_cycle_eras (cycle_eras : list cycle_era)
: M? (list cycle_era) :=
match cycle_eras with
| [] ⇒
Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
| cons newest_era older_eras ⇒
let fix aux (era : cycle_era) (older_eras : list cycle_era) : M? unit :=
let '{|
cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle
|} := era in
match older_eras with
|
cons
({|
cycle_era.first_level := first_level_of_previous_era;
cycle_era.first_cycle := first_cycle_of_previous_era
|} as previous_era) even_older_eras ⇒
if
(Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
(Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
then
aux previous_era even_older_eras
else
Error_monad.error_value
(Build_extensible "Invalid_cycle_eras" unit tt)
| [] ⇒ return? tt
end in
let? '_ := aux newest_era older_eras in
return? cycle_eras
end.
Definition add_cycle_era (new_era : cycle_era) (cycle_eras : list cycle_era)
: M? (list cycle_era) := create_cycle_eras (cons new_era cycle_eras).
Definition cycle_era_encoding : Data_encoding.encoding cycle_era :=
Data_encoding.conv
(fun (function_parameter : cycle_era) ⇒
let '{|
cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle;
cycle_era.blocks_per_cycle := blocks_per_cycle;
cycle_era.blocks_per_commitment := blocks_per_commitment
|} := function_parameter in
(first_level, first_cycle, blocks_per_cycle, blocks_per_commitment))
(fun (function_parameter : Raw_level_repr.t × Cycle_repr.t × int32 × int32)
⇒
let
'(first_level, first_cycle, blocks_per_cycle, blocks_per_commitment) :=
function_parameter in
{| cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle;
cycle_era.blocks_per_cycle := blocks_per_cycle;
cycle_era.blocks_per_commitment := blocks_per_commitment; |}) None
(Data_encoding.obj4
(Data_encoding.req None (Some "The first level of a new cycle era.")
"first_level" Raw_level_repr.encoding)
(Data_encoding.req None (Some "The first cycle of a new cycle era.")
"first_cycle" Cycle_repr.encoding)
(Data_encoding.req None
(Some
"The value of the blocks_per_cycle constant used during the cycle era starting with first_level.")
"blocks_per_cycle" Data_encoding.int32_value)
(Data_encoding.req None
(Some
"The value of the blocks_per_commitment constant used during the cycle era starting with first_level.")
"blocks_per_commitment" Data_encoding.int32_value)).
Definition cycle_eras_encoding : Data_encoding.encoding (list cycle_era) :=
Data_encoding.conv_with_guard (fun (eras : list cycle_era) ⇒ eras)
(fun (eras : list cycle_era) ⇒
match create_cycle_eras eras with
| Pervasives.Ok eras ⇒ Pervasives.Ok eras
| Pervasives.Error _ ⇒ Pervasives.Error "Invalid cycle eras"
end) None (Data_encoding.list_value None cycle_era_encoding).
Definition current_era {A : Set} (eras : list A) : M? A :=
match eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons cycle_era _ ⇒ return? cycle_era
end.
Definition root_level (cycle_eras : list cycle_era) : M? t :=
let first_era := List.last_opt cycle_eras in
let? first_era :=
match first_era with
| Some first_era ⇒ return? first_era
| None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end in
return?
{| t.level := first_era.(cycle_era.first_level); t.level_position := 0;
t.cycle := Cycle_repr.root_value; t.cycle_position := 0;
t.expected_commitment := false; |}.
Definition era_of_level
(cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level)
: M? cycle_era :=
let fix aux (function_parameter : list cycle_era) : M? cycle_era :=
match function_parameter with
| cons ({| cycle_era.first_level := first_level |} as era) previous_eras ⇒
if Raw_level_repr.op_gteq level first_level then
return? era
else
aux previous_eras
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end in
aux cycle_eras.
Definition era_of_cycle (cycle_eras : list cycle_era) (cycle : Cycle_repr.t)
: M? cycle_era :=
let fix aux (function_parameter : list cycle_era) : M? cycle_era :=
match function_parameter with
| cons ({| cycle_era.first_cycle := first_cycle |} as era) previous_eras ⇒
if Cycle_repr.op_gteq cycle first_cycle then
return? era
else
aux previous_eras
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end in
aux cycle_eras.
Definition level_from_raw_with_era
(era : cycle_era) (first_level_in_alpha_family : Raw_level_repr.raw_level)
(level : Raw_level_repr.raw_level) : M? t :=
let '{|
cycle_era.first_level := first_level;
cycle_era.first_cycle := first_cycle;
cycle_era.blocks_per_cycle := blocks_per_cycle;
cycle_era.blocks_per_commitment := blocks_per_commitment
|} := era in
let level_position_in_era := Raw_level_repr.diff_value level first_level in
if level_position_in_era ≥i32 0 then
let cycles_since_era_start := level_position_in_era /i32 blocks_per_cycle in
let? cycle :=
Cycle_repr.add first_cycle (Int32.to_int cycles_since_era_start) in
let cycle_position := Int32.rem level_position_in_era blocks_per_cycle in
let level_position :=
Raw_level_repr.diff_value level first_level_in_alpha_family in
let expected_commitment :=
(Int32.rem cycle_position blocks_per_commitment) =i32
(Int32.pred blocks_per_commitment) in
return?
{| t.level := level; t.level_position := level_position; t.cycle := cycle;
t.cycle_position := cycle_position;
t.expected_commitment := expected_commitment; |}
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition level_from_raw_aux_exn
(cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level) : M? t :=
let? first_level_in_alpha_family :=
match List.rev cycle_eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons {| cycle_era.first_level := first_level |} _ ⇒ return? first_level
end in
let? era := era_of_level cycle_eras level in
level_from_raw_with_era era first_level_in_alpha_family level.
Definition level_from_raw
(cycle_eras : list cycle_era) (l_value : Raw_level_repr.raw_level) : M? t :=
level_from_raw_aux_exn cycle_eras l_value.
Init function; without side-effects in Coq
Definition init_module2 : unit :=
Error_monad.register_error_kind Error_monad.Permanent "level_not_in_alpha"
"Level not in Alpha family" "Level not in Alpha family"
(Some
(fun (ppf : Format.formatter) ⇒
fun (level : Raw_level_repr.raw_level) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Level "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is not in the Alpha family of protocols."
CamlinternalFormatBasics.End_of_format)))
"Level %a is not in the Alpha family of protocols.")
Raw_level_repr.pp level))
(Data_encoding.obj1
(Data_encoding.req None None "level" Raw_level_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Level_not_in_alpha" then
let level := cast Raw_level_repr.t payload in
Some level
else None
end)
(fun (level : Raw_level_repr.raw_level) ⇒
Build_extensible "Level_not_in_alpha" Raw_level_repr.raw_level level).
Definition level_from_raw_aux
(cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level) : M? t :=
let? first_level_in_alpha_family :=
match List.rev cycle_eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons {| cycle_era.first_level := first_level |} _ ⇒ return? first_level
end in
let? '_ :=
Error_monad.error_when
(Raw_level_repr.op_lt level first_level_in_alpha_family)
(Build_extensible "Level_not_in_alpha" Raw_level_repr.raw_level level) in
let? era := era_of_level cycle_eras level in
level_from_raw_with_era era first_level_in_alpha_family level.
Error_monad.register_error_kind Error_monad.Permanent "level_not_in_alpha"
"Level not in Alpha family" "Level not in Alpha family"
(Some
(fun (ppf : Format.formatter) ⇒
fun (level : Raw_level_repr.raw_level) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Level "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is not in the Alpha family of protocols."
CamlinternalFormatBasics.End_of_format)))
"Level %a is not in the Alpha family of protocols.")
Raw_level_repr.pp level))
(Data_encoding.obj1
(Data_encoding.req None None "level" Raw_level_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Level_not_in_alpha" then
let level := cast Raw_level_repr.t payload in
Some level
else None
end)
(fun (level : Raw_level_repr.raw_level) ⇒
Build_extensible "Level_not_in_alpha" Raw_level_repr.raw_level level).
Definition level_from_raw_aux
(cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level) : M? t :=
let? first_level_in_alpha_family :=
match List.rev cycle_eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons {| cycle_era.first_level := first_level |} _ ⇒ return? first_level
end in
let? '_ :=
Error_monad.error_when
(Raw_level_repr.op_lt level first_level_in_alpha_family)
(Build_extensible "Level_not_in_alpha" Raw_level_repr.raw_level level) in
let? era := era_of_level cycle_eras level in
level_from_raw_with_era era first_level_in_alpha_family level.
Init function; without side-effects in Coq
Definition init_module3 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"negative_level_and_offset_sum" "Negative sum of level and offset"
"Negative sum of level and offset"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int32 × int32) ⇒
let '(level, offset) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Sum of level ("
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ") and offset ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ") is negative."
CamlinternalFormatBasics.End_of_format)))))
"Sum of level (%ld) and offset (%ld) is negative.") level offset))
(Data_encoding.obj2
(Data_encoding.req None None "level" Data_encoding.int32_value)
(Data_encoding.req None None "offset" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_level_and_offset_sum" then
let '(level, offset) := cast (int32 × int32) payload in
Some (level, offset)
else None
end)
(fun (function_parameter : int32 × int32) ⇒
let '(level, offset) := function_parameter in
Build_extensible "Negative_level_and_offset_sum" (int32 × int32)
(level, offset)).
Definition level_from_raw_with_offset
(cycle_eras : list cycle_era) (offset : int32)
(raw_level : Raw_level_repr.raw_level) : M? t :=
let res :=
Raw_level_repr.of_int32 ((Raw_level_repr.to_int32 raw_level) +i32 offset) in
let? level :=
match res with
| Pervasives.Ok level ⇒ Pervasives.Ok level
| Pervasives.Error _ ⇒
Error_monad.error_value
(Build_extensible "Negative_level_and_offset_sum" (int32 × int32)
((Raw_level_repr.to_int32 raw_level), offset))
end in
level_from_raw_aux cycle_eras level.
Definition first_level_in_cycle_from_eras
(cycle_eras : list cycle_era) (cycle : Cycle_repr.t) : M? t :=
let? first_level_in_alpha_family :=
match List.rev cycle_eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons {| cycle_era.first_level := first_level |} _ ⇒ return? first_level
end in
let? era := era_of_cycle cycle_eras cycle in
let cycle_position := Cycle_repr.diff_value cycle era.(cycle_era.first_cycle)
in
let offset := era.(cycle_era.blocks_per_cycle) ×i32 cycle_position in
let first_level_in_cycle :=
Raw_level_repr.of_int32_exn
((Raw_level_repr.to_int32 era.(cycle_era.first_level)) +i32 offset) in
level_from_raw_with_era era first_level_in_alpha_family first_level_in_cycle.
Definition last_of_cycle (cycle_eras : list cycle_era) (level : t) : M? bool :=
let? era := era_of_level cycle_eras level.(t.level) in
return?
((Int32.succ level.(t.cycle_position)) =i32 era.(cycle_era.blocks_per_cycle)).
Error_monad.register_error_kind Error_monad.Permanent
"negative_level_and_offset_sum" "Negative sum of level and offset"
"Negative sum of level and offset"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int32 × int32) ⇒
let '(level, offset) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Sum of level ("
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ") and offset ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ") is negative."
CamlinternalFormatBasics.End_of_format)))))
"Sum of level (%ld) and offset (%ld) is negative.") level offset))
(Data_encoding.obj2
(Data_encoding.req None None "level" Data_encoding.int32_value)
(Data_encoding.req None None "offset" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_level_and_offset_sum" then
let '(level, offset) := cast (int32 × int32) payload in
Some (level, offset)
else None
end)
(fun (function_parameter : int32 × int32) ⇒
let '(level, offset) := function_parameter in
Build_extensible "Negative_level_and_offset_sum" (int32 × int32)
(level, offset)).
Definition level_from_raw_with_offset
(cycle_eras : list cycle_era) (offset : int32)
(raw_level : Raw_level_repr.raw_level) : M? t :=
let res :=
Raw_level_repr.of_int32 ((Raw_level_repr.to_int32 raw_level) +i32 offset) in
let? level :=
match res with
| Pervasives.Ok level ⇒ Pervasives.Ok level
| Pervasives.Error _ ⇒
Error_monad.error_value
(Build_extensible "Negative_level_and_offset_sum" (int32 × int32)
((Raw_level_repr.to_int32 raw_level), offset))
end in
level_from_raw_aux cycle_eras level.
Definition first_level_in_cycle_from_eras
(cycle_eras : list cycle_era) (cycle : Cycle_repr.t) : M? t :=
let? first_level_in_alpha_family :=
match List.rev cycle_eras with
| [] ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| cons {| cycle_era.first_level := first_level |} _ ⇒ return? first_level
end in
let? era := era_of_cycle cycle_eras cycle in
let cycle_position := Cycle_repr.diff_value cycle era.(cycle_era.first_cycle)
in
let offset := era.(cycle_era.blocks_per_cycle) ×i32 cycle_position in
let first_level_in_cycle :=
Raw_level_repr.of_int32_exn
((Raw_level_repr.to_int32 era.(cycle_era.first_level)) +i32 offset) in
level_from_raw_with_era era first_level_in_alpha_family first_level_in_cycle.
Definition last_of_cycle (cycle_eras : list cycle_era) (level : t) : M? bool :=
let? era := era_of_level cycle_eras level.(t.level) in
return?
((Int32.succ level.(t.cycle_position)) =i32 era.(cycle_era.blocks_per_cycle)).