🥊 Round_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.Period_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Time_repr.
Definition round : Set := int32.
Definition t : Set := round.
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Int32.compare
|}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Time_repr.
Definition round : Set := int32.
Definition t : Set := round.
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Int32.compare
|}.
Inclusion of the module [Compare.Int32]
Definition op_eq := Compare.Int32.(Compare.S.op_eq).
Definition op_ltgt := Compare.Int32.(Compare.S.op_ltgt).
Definition op_lt := Compare.Int32.(Compare.S.op_lt).
Definition op_lteq := Compare.Int32.(Compare.S.op_lteq).
Definition op_gteq := Compare.Int32.(Compare.S.op_gteq).
Definition op_gt := Compare.Int32.(Compare.S.op_gt).
Definition compare := Compare.Int32.(Compare.S.compare).
Definition equal := Compare.Int32.(Compare.S.equal).
Definition max := Compare.Int32.(Compare.S.max).
Definition min := Compare.Int32.(Compare.S.min).
Definition zero : int32 := 0.
Definition succ (n_value : int32) : int32 :=
if Compare.Int32.(Compare.S.equal) n_value Int32.max_int then
Pervasives.invalid_arg
"round_repr.succ: cannot apply succ to maximum round value"
else
Int32.succ n_value.
Definition pp (fmt : Format.formatter) (i_value : int32) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%ld") i_value.
Definition op_ltgt := Compare.Int32.(Compare.S.op_ltgt).
Definition op_lt := Compare.Int32.(Compare.S.op_lt).
Definition op_lteq := Compare.Int32.(Compare.S.op_lteq).
Definition op_gteq := Compare.Int32.(Compare.S.op_gteq).
Definition op_gt := Compare.Int32.(Compare.S.op_gt).
Definition compare := Compare.Int32.(Compare.S.compare).
Definition equal := Compare.Int32.(Compare.S.equal).
Definition max := Compare.Int32.(Compare.S.max).
Definition min := Compare.Int32.(Compare.S.min).
Definition zero : int32 := 0.
Definition succ (n_value : int32) : int32 :=
if Compare.Int32.(Compare.S.equal) n_value Int32.max_int then
Pervasives.invalid_arg
"round_repr.succ: cannot apply succ to maximum round value"
else
Int32.succ n_value.
Definition pp (fmt : Format.formatter) (i_value : int32) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%ld") i_value.
Init function; without side-effects in Coq
Definition init_module1 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "negative_round"
"Negative round" "Round cannot be built out of negative integers."
(Some
(fun (ppf : Format.formatter) ⇒
fun (i_value : int64) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Negative round cannot be built out of negative integers ("
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))
"Negative round cannot be built out of negative integers (%Ld)")
i_value))
(Data_encoding.obj1
(Data_encoding.req None None "Negative_round" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_round" then
let i_value := cast int payload in
Some (Int64.of_int i_value)
else None
end)
(fun (i_value : int64) ⇒
Build_extensible "Negative_round" int (Int64.to_int i_value)) in
Error_monad.register_error_kind Error_monad.Permanent "round_overflow"
"Round overflow"
"Round cannot be built out of integer greater than maximum int32 value."
(Some
(fun (ppf : Format.formatter) ⇒
fun (i_value : int64) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Round cannot be built out of integer greater than maximum int32 value ("
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))
"Round cannot be built out of integer greater than maximum int32 value (%Ld)")
i_value))
(Data_encoding.obj1
(Data_encoding.req None None "Round_overflow" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Round_overflow" then
let i_value := cast int payload in
Some (Int64.of_int i_value)
else None
end)
(fun (i_value : int64) ⇒
Build_extensible "Round_overflow" int (Int64.to_int i_value)).
Definition of_int32 (i_value : t) : M? t :=
if op_gteq i_value 0 then
Pervasives.Ok i_value
else
Error_monad.error_value
(Build_extensible "Negative_round" int (Int32.to_int i_value)).
Definition pred (r_value : int32) : M? t :=
let p_value := Int32.pred r_value in
of_int32 p_value.
Definition of_int (i_value : int) : M? int32 :=
if i_value <i 0 then
Error_monad.error_value (Build_extensible "Negative_round" int i_value)
else
let i32 := Int32.of_int i_value in
if (Int32.to_int i32) =i i_value then
Pervasives.Ok i32
else
Error_monad.error_value (Build_extensible "Round_overflow" int i_value).
Definition to_int (i32 : Int32.t) : M? int :=
let i_value := Int32.to_int i32 in
if Int32.equal (Int32.of_int i_value) i32 then
return? i_value
else
Error_monad.error_value (Build_extensible "Round_overflow" int i_value).
Definition to_int32 {A : Set} (t_value : A) : A := t_value.
Definition to_slot (round : Int32.t) (committee_size : int) : M? Slot_repr.t :=
let? r_value := to_int round in
let slot := Pervasives._mod r_value committee_size in
Slot_repr.of_int slot.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard (fun (i_value : t) ⇒ i_value)
(fun (i_value : t) ⇒
match of_int32 i_value with
| Pervasives.Ok round ⇒ Pervasives.Ok round
| Pervasives.Error _ ⇒
Pervasives.Error "Round_repr.encoding: negative round"
end) None Data_encoding.int32_value.
Module Durations.
Module t.
Record record : Set := Build {
first_round_duration : Period_repr.t;
delay_increment_per_round : Period_repr.t;
}.
Definition with_first_round_duration first_round_duration (r : record) :=
Build first_round_duration r.(delay_increment_per_round).
Definition with_delay_increment_per_round delay_increment_per_round
(r : record) :=
Build r.(first_round_duration) delay_increment_per_round.
End t.
Definition t := t.record.
Module Non_increasing_rounds.
Record record : Set := Build {
increment : Period_repr.t;
}.
Definition with_increment increment (r : record) :=
Build increment.
End Non_increasing_rounds.
Definition Non_increasing_rounds := Non_increasing_rounds.record.
Module Round_durations_must_be_at_least_one_second.
Record record : Set := Build {
round : Period_repr.t;
}.
Definition with_round round (r : record) :=
Build round.
End Round_durations_must_be_at_least_one_second.
Definition Round_durations_must_be_at_least_one_second :=
Round_durations_must_be_at_least_one_second.record.
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "negative_round"
"Negative round" "Round cannot be built out of negative integers."
(Some
(fun (ppf : Format.formatter) ⇒
fun (i_value : int64) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Negative round cannot be built out of negative integers ("
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))
"Negative round cannot be built out of negative integers (%Ld)")
i_value))
(Data_encoding.obj1
(Data_encoding.req None None "Negative_round" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_round" then
let i_value := cast int payload in
Some (Int64.of_int i_value)
else None
end)
(fun (i_value : int64) ⇒
Build_extensible "Negative_round" int (Int64.to_int i_value)) in
Error_monad.register_error_kind Error_monad.Permanent "round_overflow"
"Round overflow"
"Round cannot be built out of integer greater than maximum int32 value."
(Some
(fun (ppf : Format.formatter) ⇒
fun (i_value : int64) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Round cannot be built out of integer greater than maximum int32 value ("
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))
"Round cannot be built out of integer greater than maximum int32 value (%Ld)")
i_value))
(Data_encoding.obj1
(Data_encoding.req None None "Round_overflow" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Round_overflow" then
let i_value := cast int payload in
Some (Int64.of_int i_value)
else None
end)
(fun (i_value : int64) ⇒
Build_extensible "Round_overflow" int (Int64.to_int i_value)).
Definition of_int32 (i_value : t) : M? t :=
if op_gteq i_value 0 then
Pervasives.Ok i_value
else
Error_monad.error_value
(Build_extensible "Negative_round" int (Int32.to_int i_value)).
Definition pred (r_value : int32) : M? t :=
let p_value := Int32.pred r_value in
of_int32 p_value.
Definition of_int (i_value : int) : M? int32 :=
if i_value <i 0 then
Error_monad.error_value (Build_extensible "Negative_round" int i_value)
else
let i32 := Int32.of_int i_value in
if (Int32.to_int i32) =i i_value then
Pervasives.Ok i32
else
Error_monad.error_value (Build_extensible "Round_overflow" int i_value).
Definition to_int (i32 : Int32.t) : M? int :=
let i_value := Int32.to_int i32 in
if Int32.equal (Int32.of_int i_value) i32 then
return? i_value
else
Error_monad.error_value (Build_extensible "Round_overflow" int i_value).
Definition to_int32 {A : Set} (t_value : A) : A := t_value.
Definition to_slot (round : Int32.t) (committee_size : int) : M? Slot_repr.t :=
let? r_value := to_int round in
let slot := Pervasives._mod r_value committee_size in
Slot_repr.of_int slot.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard (fun (i_value : t) ⇒ i_value)
(fun (i_value : t) ⇒
match of_int32 i_value with
| Pervasives.Ok round ⇒ Pervasives.Ok round
| Pervasives.Error _ ⇒
Pervasives.Error "Round_repr.encoding: negative round"
end) None Data_encoding.int32_value.
Module Durations.
Module t.
Record record : Set := Build {
first_round_duration : Period_repr.t;
delay_increment_per_round : Period_repr.t;
}.
Definition with_first_round_duration first_round_duration (r : record) :=
Build first_round_duration r.(delay_increment_per_round).
Definition with_delay_increment_per_round delay_increment_per_round
(r : record) :=
Build r.(first_round_duration) delay_increment_per_round.
End t.
Definition t := t.record.
Module Non_increasing_rounds.
Record record : Set := Build {
increment : Period_repr.t;
}.
Definition with_increment increment (r : record) :=
Build increment.
End Non_increasing_rounds.
Definition Non_increasing_rounds := Non_increasing_rounds.record.
Module Round_durations_must_be_at_least_one_second.
Record record : Set := Build {
round : Period_repr.t;
}.
Definition with_round round (r : record) :=
Build round.
End Round_durations_must_be_at_least_one_second.
Definition Round_durations_must_be_at_least_one_second :=
Round_durations_must_be_at_least_one_second.record.
Init function; without side-effects in Coq
Definition init_module2 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"durations.non_increasing_rounds" "Non increasing round"
"The provided rounds are not increasing."
(Some
(fun (ppf : Format.formatter) ⇒
fun (increment : Period_repr.period) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The provided rounds are not increasing (increment: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))
"The provided rounds are not increasing (increment: %a)")
Period_repr.pp increment))
(Data_encoding.obj1
(Data_encoding.req None None "increment" Period_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Non_increasing_rounds" then
let '{| Non_increasing_rounds.increment := increment |} :=
cast Non_increasing_rounds payload in
Some increment
else None
end)
(fun (increment : Period_repr.period) ⇒
Build_extensible "Non_increasing_rounds" Non_increasing_rounds
{| Non_increasing_rounds.increment := increment; |}).
Definition pp (fmt : Format.formatter) (t_value : t) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.Char_literal "+" % char
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))) "%a,@ +%a")
Period_repr.pp t_value.(t.first_round_duration) Period_repr.pp
t_value.(t.delay_increment_per_round).
Definition create
(first_round_duration : Period_repr.period)
(delay_increment_per_round : Period_repr.period) : M? t :=
let? '_ :=
Error_monad.error_when
((Period_repr.to_seconds first_round_duration) <i64 1)
(Build_extensible "Round_durations_must_be_at_least_one_second"
Round_durations_must_be_at_least_one_second
{|
Round_durations_must_be_at_least_one_second.round :=
first_round_duration; |}) in
let? '_ :=
Error_monad.error_when
((Period_repr.to_seconds delay_increment_per_round) <i64 1)
(Build_extensible "Non_increasing_rounds" Non_increasing_rounds
{| Non_increasing_rounds.increment := delay_increment_per_round; |})
in
return?
{| t.first_round_duration := first_round_duration;
t.delay_increment_per_round := delay_increment_per_round; |}.
Definition create_opt
(first_round_duration : Period_repr.period)
(delay_increment_per_round : Period_repr.period) : option t :=
match create first_round_duration delay_increment_per_round with
| Pervasives.Ok v_value ⇒ Some v_value
| Pervasives.Error _ ⇒ None
end.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard
(fun (function_parameter : t) ⇒
let '{|
t.first_round_duration := first_round_duration;
t.delay_increment_per_round := delay_increment_per_round
|} := function_parameter in
(first_round_duration, delay_increment_per_round))
(fun (function_parameter : Period_repr.t × Period_repr.t) ⇒
let '(first_round_duration, delay_increment_per_round) :=
function_parameter in
match create_opt first_round_duration delay_increment_per_round with
| None ⇒
Pervasives.Error
"Either round durations are non-increasing or minimal block delay < 1"
| Some rounds ⇒ Pervasives.Ok rounds
end) None
(Data_encoding.obj2
(Data_encoding.req None None "first_round_duration" Period_repr.encoding)
(Data_encoding.req None None "delay_increment_per_round"
Period_repr.encoding)).
Definition round_duration (function_parameter : t)
: int32 → Period_repr.period :=
let '{|
t.first_round_duration := first_round_duration;
t.delay_increment_per_round := delay_increment_per_round
|} := function_parameter in
fun (round : int32) ⇒
if round <i32 0 then
Pervasives.invalid_arg "round must be a non-negative integer"
else
let first_round_duration_s : int64 :=
Period_repr.to_seconds first_round_duration
in let delay_increment_per_round_s : int64 :=
Period_repr.to_seconds delay_increment_per_round in
Period_repr.of_seconds_exn
(first_round_duration_s +i64
((Int64.of_int32 round) ×i64 delay_increment_per_round_s)).
End Durations.
Error_monad.register_error_kind Error_monad.Permanent
"durations.non_increasing_rounds" "Non increasing round"
"The provided rounds are not increasing."
(Some
(fun (ppf : Format.formatter) ⇒
fun (increment : Period_repr.period) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The provided rounds are not increasing (increment: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))
"The provided rounds are not increasing (increment: %a)")
Period_repr.pp increment))
(Data_encoding.obj1
(Data_encoding.req None None "increment" Period_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Non_increasing_rounds" then
let '{| Non_increasing_rounds.increment := increment |} :=
cast Non_increasing_rounds payload in
Some increment
else None
end)
(fun (increment : Period_repr.period) ⇒
Build_extensible "Non_increasing_rounds" Non_increasing_rounds
{| Non_increasing_rounds.increment := increment; |}).
Definition pp (fmt : Format.formatter) (t_value : t) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.Char_literal "+" % char
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))) "%a,@ +%a")
Period_repr.pp t_value.(t.first_round_duration) Period_repr.pp
t_value.(t.delay_increment_per_round).
Definition create
(first_round_duration : Period_repr.period)
(delay_increment_per_round : Period_repr.period) : M? t :=
let? '_ :=
Error_monad.error_when
((Period_repr.to_seconds first_round_duration) <i64 1)
(Build_extensible "Round_durations_must_be_at_least_one_second"
Round_durations_must_be_at_least_one_second
{|
Round_durations_must_be_at_least_one_second.round :=
first_round_duration; |}) in
let? '_ :=
Error_monad.error_when
((Period_repr.to_seconds delay_increment_per_round) <i64 1)
(Build_extensible "Non_increasing_rounds" Non_increasing_rounds
{| Non_increasing_rounds.increment := delay_increment_per_round; |})
in
return?
{| t.first_round_duration := first_round_duration;
t.delay_increment_per_round := delay_increment_per_round; |}.
Definition create_opt
(first_round_duration : Period_repr.period)
(delay_increment_per_round : Period_repr.period) : option t :=
match create first_round_duration delay_increment_per_round with
| Pervasives.Ok v_value ⇒ Some v_value
| Pervasives.Error _ ⇒ None
end.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard
(fun (function_parameter : t) ⇒
let '{|
t.first_round_duration := first_round_duration;
t.delay_increment_per_round := delay_increment_per_round
|} := function_parameter in
(first_round_duration, delay_increment_per_round))
(fun (function_parameter : Period_repr.t × Period_repr.t) ⇒
let '(first_round_duration, delay_increment_per_round) :=
function_parameter in
match create_opt first_round_duration delay_increment_per_round with
| None ⇒
Pervasives.Error
"Either round durations are non-increasing or minimal block delay < 1"
| Some rounds ⇒ Pervasives.Ok rounds
end) None
(Data_encoding.obj2
(Data_encoding.req None None "first_round_duration" Period_repr.encoding)
(Data_encoding.req None None "delay_increment_per_round"
Period_repr.encoding)).
Definition round_duration (function_parameter : t)
: int32 → Period_repr.period :=
let '{|
t.first_round_duration := first_round_duration;
t.delay_increment_per_round := delay_increment_per_round
|} := function_parameter in
fun (round : int32) ⇒
if round <i32 0 then
Pervasives.invalid_arg "round must be a non-negative integer"
else
let first_round_duration_s : int64 :=
Period_repr.to_seconds first_round_duration
in let delay_increment_per_round_s : int64 :=
Period_repr.to_seconds delay_increment_per_round in
Period_repr.of_seconds_exn
(first_round_duration_s +i64
((Int64.of_int32 round) ×i64 delay_increment_per_round_s)).
End Durations.
Init function; without side-effects in Coq
Definition init_module3 : unit :=
Error_monad.register_error_kind Error_monad.Permanent "round_too_high"
"round too high" "block round too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (round : int32) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Block round is too high: "
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))
"Block round is too high: %ld") round))
(Data_encoding.obj1
(Data_encoding.req None None "level_offset_too_high"
Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Round_too_high" then
let round := cast int32 payload in
Some round
else None
end)
(fun (round : int32) ⇒ Build_extensible "Round_too_high" int32 round).
Definition raw_level_offset_of_round
(round_durations : Durations.t) (round : int32) : M? int64 :=
if round =i32 zero then
return? Int64.zero
else
let sum_durations :=
let '{|
Durations.t.first_round_duration := first_round_duration;
Durations.t.delay_increment_per_round := delay_increment_per_round
|} := round_durations in
let roundz := Int64.of_int32 round in
let m_value :=
Z.of_int64 ((roundz ×i64 (Int64.pred roundz)) /i64 (Int64.of_int 2)) in
(m_value ×Z
(Z.of_int64 (Period_repr.to_seconds delay_increment_per_round))) +Z
((Z.of_int32 round) ×Z
(Z.of_int64 (Period_repr.to_seconds first_round_duration))) in
if sum_durations >Z (Z.of_int64 Int64.max_int) then
Error_monad.error_value (Build_extensible "Round_too_high" int32 round)
else
return? (Z.to_int64 sum_durations).
Error_monad.register_error_kind Error_monad.Permanent "round_too_high"
"round too high" "block round too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (round : int32) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Block round is too high: "
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))
"Block round is too high: %ld") round))
(Data_encoding.obj1
(Data_encoding.req None None "level_offset_too_high"
Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Round_too_high" then
let round := cast int32 payload in
Some round
else None
end)
(fun (round : int32) ⇒ Build_extensible "Round_too_high" int32 round).
Definition raw_level_offset_of_round
(round_durations : Durations.t) (round : int32) : M? int64 :=
if round =i32 zero then
return? Int64.zero
else
let sum_durations :=
let '{|
Durations.t.first_round_duration := first_round_duration;
Durations.t.delay_increment_per_round := delay_increment_per_round
|} := round_durations in
let roundz := Int64.of_int32 round in
let m_value :=
Z.of_int64 ((roundz ×i64 (Int64.pred roundz)) /i64 (Int64.of_int 2)) in
(m_value ×Z
(Z.of_int64 (Period_repr.to_seconds delay_increment_per_round))) +Z
((Z.of_int32 round) ×Z
(Z.of_int64 (Period_repr.to_seconds first_round_duration))) in
if sum_durations >Z (Z.of_int64 Int64.max_int) then
Error_monad.error_value (Build_extensible "Round_too_high" int32 round)
else
return? (Z.to_int64 sum_durations).
Init function; without side-effects in Coq
Definition init_module4 : unit :=
Error_monad.register_error_kind Error_monad.Permanent "level_offset_too_high"
"level offset too high" "The block's level offset is too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (offset : Period_repr.period) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The block's level offset is too high: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"The block's level offset is too high: %a") Period_repr.pp offset))
(Data_encoding.obj1
(Data_encoding.req None None "level_offset_too_high" Period_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Level_offset_too_high" then
let offset := cast Period_repr.t payload in
Some offset
else None
end)
(fun (offset : Period_repr.period) ⇒
Build_extensible "Level_offset_too_high" Period_repr.period offset).
Module round_and_offset.
Record record : Set := Build {
round : int32;
offset : Period_repr.t;
}.
Definition with_round round (r : record) :=
Build round r.(offset).
Definition with_offset offset (r : record) :=
Build r.(round) offset.
End round_and_offset.
Definition round_and_offset := round_and_offset.record.
Error_monad.register_error_kind Error_monad.Permanent "level_offset_too_high"
"level offset too high" "The block's level offset is too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (offset : Period_repr.period) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The block's level offset is too high: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"The block's level offset is too high: %a") Period_repr.pp offset))
(Data_encoding.obj1
(Data_encoding.req None None "level_offset_too_high" Period_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Level_offset_too_high" then
let offset := cast Period_repr.t payload in
Some offset
else None
end)
(fun (offset : Period_repr.period) ⇒
Build_extensible "Level_offset_too_high" Period_repr.period offset).
Module round_and_offset.
Record record : Set := Build {
round : int32;
offset : Period_repr.t;
}.
Definition with_round round (r : record) :=
Build round r.(offset).
Definition with_offset offset (r : record) :=
Build r.(round) offset.
End round_and_offset.
Definition round_and_offset := round_and_offset.record.
Complexity: O(log level_offset).
Definition round_and_offset_value
(round_durations : Durations.t) (level_offset : Period_repr.period)
: M? round_and_offset :=
let level_offset_in_seconds := Period_repr.to_seconds level_offset in
let overflow_bound := Int64.shift_right Int64.max_int 10 in
if overflow_bound <i64 level_offset_in_seconds then
Error_monad.error_value
(Build_extensible "Level_offset_too_high" Period_repr.period level_offset)
else
let '{|
Durations.t.first_round_duration := first_round_duration;
Durations.t.delay_increment_per_round := delay_increment_per_round
|} := round_durations in
let first_round_duration := Period_repr.to_seconds first_round_duration in
let delay_increment_per_round :=
Period_repr.to_seconds delay_increment_per_round in
if level_offset_in_seconds <i64 first_round_duration then
return?
{| round_and_offset.round := 0; round_and_offset.offset := level_offset;
|}
else
let round :=
if delay_increment_per_round =i64 Int64.zero then
level_offset_in_seconds /i64 first_round_duration
else
let pow_2 (n_value : int64) : int64 :=
n_value ×i64 n_value in
let double (n_value : int64) : int64 :=
Int64.shift_left n_value 1 in
let times_8 (n_value : int64) : int64 :=
Int64.shift_left n_value 3 in
let half (n_value : int64) : int64 :=
Int64.shift_right n_value 1 in
let sqrt (n_value : int64) : int64 :=
let x0 := Pervasives.ref_value (half n_value) in
if (Pervasives.op_exclamation x0) >i64 1 then
let x1 :=
Pervasives.ref_value
(half
((Pervasives.op_exclamation x0) +i64
(n_value /i64 (Pervasives.op_exclamation x0)))) in
let '_ :=
(* ❌ While loops not handled. *)
tt in
Pervasives.op_exclamation x0
else
n_value in
let discr :=
(pow_2
((double first_round_duration) -i64 delay_increment_per_round))
+i64
(times_8 (delay_increment_per_round ×i64 level_offset_in_seconds))
in
((delay_increment_per_round -i64 (double first_round_duration)) +i64
(sqrt discr)) /i64 (double delay_increment_per_round) in
let? current_level_offset :=
raw_level_offset_of_round round_durations (Int64.to_int32 round) in
return?
{| round_and_offset.round := Int64.to_int32 round;
round_and_offset.offset :=
Period_repr.of_seconds_exn
((Period_repr.to_seconds level_offset) -i64 current_level_offset);
|}.
(round_durations : Durations.t) (level_offset : Period_repr.period)
: M? round_and_offset :=
let level_offset_in_seconds := Period_repr.to_seconds level_offset in
let overflow_bound := Int64.shift_right Int64.max_int 10 in
if overflow_bound <i64 level_offset_in_seconds then
Error_monad.error_value
(Build_extensible "Level_offset_too_high" Period_repr.period level_offset)
else
let '{|
Durations.t.first_round_duration := first_round_duration;
Durations.t.delay_increment_per_round := delay_increment_per_round
|} := round_durations in
let first_round_duration := Period_repr.to_seconds first_round_duration in
let delay_increment_per_round :=
Period_repr.to_seconds delay_increment_per_round in
if level_offset_in_seconds <i64 first_round_duration then
return?
{| round_and_offset.round := 0; round_and_offset.offset := level_offset;
|}
else
let round :=
if delay_increment_per_round =i64 Int64.zero then
level_offset_in_seconds /i64 first_round_duration
else
let pow_2 (n_value : int64) : int64 :=
n_value ×i64 n_value in
let double (n_value : int64) : int64 :=
Int64.shift_left n_value 1 in
let times_8 (n_value : int64) : int64 :=
Int64.shift_left n_value 3 in
let half (n_value : int64) : int64 :=
Int64.shift_right n_value 1 in
let sqrt (n_value : int64) : int64 :=
let x0 := Pervasives.ref_value (half n_value) in
if (Pervasives.op_exclamation x0) >i64 1 then
let x1 :=
Pervasives.ref_value
(half
((Pervasives.op_exclamation x0) +i64
(n_value /i64 (Pervasives.op_exclamation x0)))) in
let '_ :=
(* ❌ While loops not handled. *)
tt in
Pervasives.op_exclamation x0
else
n_value in
let discr :=
(pow_2
((double first_round_duration) -i64 delay_increment_per_round))
+i64
(times_8 (delay_increment_per_round ×i64 level_offset_in_seconds))
in
((delay_increment_per_round -i64 (double first_round_duration)) +i64
(sqrt discr)) /i64 (double delay_increment_per_round) in
let? current_level_offset :=
raw_level_offset_of_round round_durations (Int64.to_int32 round) in
return?
{| round_and_offset.round := Int64.to_int32 round;
round_and_offset.offset :=
Period_repr.of_seconds_exn
((Period_repr.to_seconds level_offset) -i64 current_level_offset);
|}.
Complexity: O(|round_durations|).
Definition timestamp_of_round
(round_durations : Durations.t) (predecessor_timestamp : Time_repr.time)
(predecessor_round : int32) (round : int32) : M? Time_repr.time :=
let pred_round_duration :=
Durations.round_duration round_durations predecessor_round in
let? start_of_current_level :=
Time_repr.op_plusquestion predecessor_timestamp pred_round_duration in
let? level_offset := raw_level_offset_of_round round_durations round in
let level_offset := Period_repr.of_seconds_exn level_offset in
Time_repr.op_plusquestion start_of_current_level level_offset.
(round_durations : Durations.t) (predecessor_timestamp : Time_repr.time)
(predecessor_round : int32) (round : int32) : M? Time_repr.time :=
let pred_round_duration :=
Durations.round_duration round_durations predecessor_round in
let? start_of_current_level :=
Time_repr.op_plusquestion predecessor_timestamp pred_round_duration in
let? level_offset := raw_level_offset_of_round round_durations round in
let level_offset := Period_repr.of_seconds_exn level_offset in
Time_repr.op_plusquestion start_of_current_level level_offset.
Unlike [timestamp_of_round], this function gets the starting time
of a given round, given the timestamp and the round of a proposal
at the same level.
We compute the starting time of [considered_round] from a given
[round_durations] description, some [current_round], and its
starting time [current_timestamp].
Complexity: O(|round_durations|).
Definition timestamp_of_another_round_same_level
(round_durations : Durations.t) (current_timestamp : Time_repr.t)
(current_round : int32) (considered_round : int32) : M? Time_repr.t :=
let? target_offset :=
raw_level_offset_of_round round_durations considered_round in
let? current_offset := raw_level_offset_of_round round_durations current_round
in
return?
(Time_repr.of_seconds
(((Time_repr.to_seconds current_timestamp) -i64 current_offset) +i64
target_offset)).
Module Round_of_past_timestamp.
Record record : Set := Build {
provided_timestamp : Time.t;
predecessor_timestamp : Time.t;
predecessor_round : t;
}.
Definition with_provided_timestamp provided_timestamp (r : record) :=
Build provided_timestamp r.(predecessor_timestamp) r.(predecessor_round).
Definition with_predecessor_timestamp predecessor_timestamp (r : record) :=
Build r.(provided_timestamp) predecessor_timestamp r.(predecessor_round).
Definition with_predecessor_round predecessor_round (r : record) :=
Build r.(provided_timestamp) r.(predecessor_timestamp) predecessor_round.
End Round_of_past_timestamp.
Definition Round_of_past_timestamp := Round_of_past_timestamp.record.
(round_durations : Durations.t) (current_timestamp : Time_repr.t)
(current_round : int32) (considered_round : int32) : M? Time_repr.t :=
let? target_offset :=
raw_level_offset_of_round round_durations considered_round in
let? current_offset := raw_level_offset_of_round round_durations current_round
in
return?
(Time_repr.of_seconds
(((Time_repr.to_seconds current_timestamp) -i64 current_offset) +i64
target_offset)).
Module Round_of_past_timestamp.
Record record : Set := Build {
provided_timestamp : Time.t;
predecessor_timestamp : Time.t;
predecessor_round : t;
}.
Definition with_provided_timestamp provided_timestamp (r : record) :=
Build provided_timestamp r.(predecessor_timestamp) r.(predecessor_round).
Definition with_predecessor_timestamp predecessor_timestamp (r : record) :=
Build r.(provided_timestamp) predecessor_timestamp r.(predecessor_round).
Definition with_predecessor_round predecessor_round (r : record) :=
Build r.(provided_timestamp) r.(predecessor_timestamp) predecessor_round.
End Round_of_past_timestamp.
Definition Round_of_past_timestamp := Round_of_past_timestamp.record.
Init function; without side-effects in Coq
Definition init_module5 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"round_of_past_timestamp" "Round_of_timestamp for past timestamp"
"Provided timestamp is before the expected level start."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Time.t × Time.t × t) ⇒
let '(provided_ts, predecessor_ts, round) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Provided timestamp ("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
") is before the expected level start (computed based on predecessor_ts "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " at round "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))))
"Provided timestamp (%a) is before the expected level start (computed based on predecessor_ts %a at round %a).")
Time.pp_hum provided_ts Time.pp_hum predecessor_ts pp round))
(Data_encoding.obj3
(Data_encoding.req None None "provided_timestamp" Time.encoding)
(Data_encoding.req None None "predecessor_timestamp" Time.encoding)
(Data_encoding.req None None "predecessor_round" encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Round_of_past_timestamp" then
let '{|
Round_of_past_timestamp.provided_timestamp := provided_timestamp;
Round_of_past_timestamp.predecessor_timestamp :=
predecessor_timestamp;
Round_of_past_timestamp.predecessor_round := predecessor_round
|} := cast Round_of_past_timestamp payload in
Some (provided_timestamp, predecessor_timestamp, predecessor_round)
else None
end)
(fun (function_parameter : Time.t × Time.t × t) ⇒
let '(provided_timestamp, predecessor_timestamp, predecessor_round) :=
function_parameter in
Build_extensible "Round_of_past_timestamp" Round_of_past_timestamp
{| Round_of_past_timestamp.provided_timestamp := provided_timestamp;
Round_of_past_timestamp.predecessor_timestamp :=
predecessor_timestamp;
Round_of_past_timestamp.predecessor_round := predecessor_round; |}).
Definition round_of_timestamp
(round_durations : Durations.t) (predecessor_timestamp : Time_repr.time)
(predecessor_round : int32) (timestamp : Time.t) : M? int32 :=
let round_duration :=
Durations.round_duration round_durations predecessor_round in
let? start_of_current_level :=
Time_repr.op_plusquestion predecessor_timestamp round_duration in
let? diff_value :=
Error_monad.record_trace
(Build_extensible "Round_of_past_timestamp" Round_of_past_timestamp
{| Round_of_past_timestamp.provided_timestamp := timestamp;
Round_of_past_timestamp.predecessor_timestamp :=
predecessor_timestamp;
Round_of_past_timestamp.predecessor_round := predecessor_round; |})
(Period_repr.of_seconds
(Time_repr.diff_value timestamp start_of_current_level)) in
let? round_and_offset_value :=
round_and_offset_value round_durations diff_value in
return? round_and_offset_value.(round_and_offset.round).
Definition level_offset_of_round (round_durations : Durations.t) (round : int32)
: M? Period_repr.period :=
let? offset := raw_level_offset_of_round round_durations round in
return? (Period_repr.of_seconds_exn offset).
Module Internals_for_test.
Module round_and_offset_raw.
Record record : Set := Build {
round : round;
offset : Period_repr.t;
}.
Definition with_round round (r : record) :=
Build round r.(offset).
Definition with_offset offset (r : record) :=
Build r.(round) offset.
End round_and_offset_raw.
Definition round_and_offset_raw := round_and_offset_raw.record.
Definition round_and_offset_value
(round_durations : Durations.t) (level_offset : Period_repr.period)
: M? round_and_offset_raw :=
let? v_value := round_and_offset_value round_durations level_offset in
return?
{| round_and_offset_raw.round := v_value.(round_and_offset.round);
round_and_offset_raw.offset := v_value.(round_and_offset.offset); |}.
End Internals_for_test.
Error_monad.register_error_kind Error_monad.Permanent
"round_of_past_timestamp" "Round_of_timestamp for past timestamp"
"Provided timestamp is before the expected level start."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Time.t × Time.t × t) ⇒
let '(provided_ts, predecessor_ts, round) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Provided timestamp ("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
") is before the expected level start (computed based on predecessor_ts "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " at round "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))))
"Provided timestamp (%a) is before the expected level start (computed based on predecessor_ts %a at round %a).")
Time.pp_hum provided_ts Time.pp_hum predecessor_ts pp round))
(Data_encoding.obj3
(Data_encoding.req None None "provided_timestamp" Time.encoding)
(Data_encoding.req None None "predecessor_timestamp" Time.encoding)
(Data_encoding.req None None "predecessor_round" encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Round_of_past_timestamp" then
let '{|
Round_of_past_timestamp.provided_timestamp := provided_timestamp;
Round_of_past_timestamp.predecessor_timestamp :=
predecessor_timestamp;
Round_of_past_timestamp.predecessor_round := predecessor_round
|} := cast Round_of_past_timestamp payload in
Some (provided_timestamp, predecessor_timestamp, predecessor_round)
else None
end)
(fun (function_parameter : Time.t × Time.t × t) ⇒
let '(provided_timestamp, predecessor_timestamp, predecessor_round) :=
function_parameter in
Build_extensible "Round_of_past_timestamp" Round_of_past_timestamp
{| Round_of_past_timestamp.provided_timestamp := provided_timestamp;
Round_of_past_timestamp.predecessor_timestamp :=
predecessor_timestamp;
Round_of_past_timestamp.predecessor_round := predecessor_round; |}).
Definition round_of_timestamp
(round_durations : Durations.t) (predecessor_timestamp : Time_repr.time)
(predecessor_round : int32) (timestamp : Time.t) : M? int32 :=
let round_duration :=
Durations.round_duration round_durations predecessor_round in
let? start_of_current_level :=
Time_repr.op_plusquestion predecessor_timestamp round_duration in
let? diff_value :=
Error_monad.record_trace
(Build_extensible "Round_of_past_timestamp" Round_of_past_timestamp
{| Round_of_past_timestamp.provided_timestamp := timestamp;
Round_of_past_timestamp.predecessor_timestamp :=
predecessor_timestamp;
Round_of_past_timestamp.predecessor_round := predecessor_round; |})
(Period_repr.of_seconds
(Time_repr.diff_value timestamp start_of_current_level)) in
let? round_and_offset_value :=
round_and_offset_value round_durations diff_value in
return? round_and_offset_value.(round_and_offset.round).
Definition level_offset_of_round (round_durations : Durations.t) (round : int32)
: M? Period_repr.period :=
let? offset := raw_level_offset_of_round round_durations round in
return? (Period_repr.of_seconds_exn offset).
Module Internals_for_test.
Module round_and_offset_raw.
Record record : Set := Build {
round : round;
offset : Period_repr.t;
}.
Definition with_round round (r : record) :=
Build round r.(offset).
Definition with_offset offset (r : record) :=
Build r.(round) offset.
End round_and_offset_raw.
Definition round_and_offset_raw := round_and_offset_raw.record.
Definition round_and_offset_value
(round_durations : Durations.t) (level_offset : Period_repr.period)
: M? round_and_offset_raw :=
let? v_value := round_and_offset_value round_durations level_offset in
return?
{| round_and_offset_raw.round := v_value.(round_and_offset.round);
round_and_offset_raw.offset := v_value.(round_and_offset.offset); |}.
End Internals_for_test.