🏋️ Fitness_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.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Module t.
Record record : Set := Build {
level : Raw_level_repr.t;
locked_round : option Round_repr.t;
predecessor_round : Round_repr.t;
round : Round_repr.t;
}.
Definition with_level level (r : record) :=
Build level r.(locked_round) r.(predecessor_round) r.(round).
Definition with_locked_round locked_round (r : record) :=
Build r.(level) locked_round r.(predecessor_round) r.(round).
Definition with_predecessor_round predecessor_round (r : record) :=
Build r.(level) r.(locked_round) predecessor_round r.(round).
Definition with_round round (r : record) :=
Build r.(level) r.(locked_round) r.(predecessor_round) round.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.def "fitness" None None
(Data_encoding.conv_with_guard
(fun (function_parameter : t) ⇒
let '{|
t.level := level;
t.locked_round := locked_round;
t.predecessor_round := predecessor_round;
t.round := round
|} := function_parameter in
(level, locked_round, predecessor_round, round))
(fun (function_parameter :
Raw_level_repr.t × option Round_repr.t × Round_repr.t × Round_repr.t) ⇒
let '(level, locked_round, predecessor_round, round) :=
function_parameter in
match locked_round with
| None ⇒
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
| Some locked_round_val ⇒
if Round_repr.op_lteq round locked_round_val then
Pervasives.Error "Locked round must be smaller than round."
else
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
end) None
(Data_encoding.obj4
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "locked_round"
(Data_encoding.option_value Round_repr.encoding))
(Data_encoding.req None None "predecessor_round" Round_repr.encoding)
(Data_encoding.req None None "round" Round_repr.encoding))).
Definition pp (ppf : Format.formatter) (f_value : t) : unit :=
let minus_sign :=
if Round_repr.op_eq f_value.(t.predecessor_round) Round_repr.zero then
""
else
"-" in
let locked_round (ppf : Format.formatter) (locked_round : option Round_repr.t)
: unit :=
match locked_round with
| None ⇒ Format.pp_print_string ppf "unlocked"
| Some round ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "locked: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "locked: %a")
Round_repr.pp round
end in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "(" % char
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))))))))))
"(%a, %a, %s%a, %a)") Raw_level_repr.pp f_value.(t.level) locked_round
f_value.(t.locked_round) minus_sign Round_repr.pp
f_value.(t.predecessor_round) Round_repr.pp f_value.(t.round).
Module Locked_round_not_less_than_round.
Record record : Set := Build {
round : Round_repr.t;
locked_round : Round_repr.t;
}.
Definition with_round round (r : record) :=
Build round r.(locked_round).
Definition with_locked_round locked_round (r : record) :=
Build r.(round) locked_round.
End Locked_round_not_less_than_round.
Definition Locked_round_not_less_than_round :=
Locked_round_not_less_than_round.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Module t.
Record record : Set := Build {
level : Raw_level_repr.t;
locked_round : option Round_repr.t;
predecessor_round : Round_repr.t;
round : Round_repr.t;
}.
Definition with_level level (r : record) :=
Build level r.(locked_round) r.(predecessor_round) r.(round).
Definition with_locked_round locked_round (r : record) :=
Build r.(level) locked_round r.(predecessor_round) r.(round).
Definition with_predecessor_round predecessor_round (r : record) :=
Build r.(level) r.(locked_round) predecessor_round r.(round).
Definition with_round round (r : record) :=
Build r.(level) r.(locked_round) r.(predecessor_round) round.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.def "fitness" None None
(Data_encoding.conv_with_guard
(fun (function_parameter : t) ⇒
let '{|
t.level := level;
t.locked_round := locked_round;
t.predecessor_round := predecessor_round;
t.round := round
|} := function_parameter in
(level, locked_round, predecessor_round, round))
(fun (function_parameter :
Raw_level_repr.t × option Round_repr.t × Round_repr.t × Round_repr.t) ⇒
let '(level, locked_round, predecessor_round, round) :=
function_parameter in
match locked_round with
| None ⇒
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
| Some locked_round_val ⇒
if Round_repr.op_lteq round locked_round_val then
Pervasives.Error "Locked round must be smaller than round."
else
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
end) None
(Data_encoding.obj4
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "locked_round"
(Data_encoding.option_value Round_repr.encoding))
(Data_encoding.req None None "predecessor_round" Round_repr.encoding)
(Data_encoding.req None None "round" Round_repr.encoding))).
Definition pp (ppf : Format.formatter) (f_value : t) : unit :=
let minus_sign :=
if Round_repr.op_eq f_value.(t.predecessor_round) Round_repr.zero then
""
else
"-" in
let locked_round (ppf : Format.formatter) (locked_round : option Round_repr.t)
: unit :=
match locked_round with
| None ⇒ Format.pp_print_string ppf "unlocked"
| Some round ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "locked: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "locked: %a")
Round_repr.pp round
end in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "(" % char
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))))))))))
"(%a, %a, %s%a, %a)") Raw_level_repr.pp f_value.(t.level) locked_round
f_value.(t.locked_round) minus_sign Round_repr.pp
f_value.(t.predecessor_round) Round_repr.pp f_value.(t.round).
Module Locked_round_not_less_than_round.
Record record : Set := Build {
round : Round_repr.t;
locked_round : Round_repr.t;
}.
Definition with_round round (r : record) :=
Build round r.(locked_round).
Definition with_locked_round locked_round (r : record) :=
Build r.(round) locked_round.
End Locked_round_not_less_than_round.
Definition Locked_round_not_less_than_round :=
Locked_round_not_less_than_round.record.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "invalid_fitness"
"Invalid fitness"
"Fitness representation should be exactly 4 times 4 bytes long."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Invalid fitness"
CamlinternalFormatBasics.End_of_format) "Invalid fitness")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_fitness" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_fitness" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "wrong_fitness"
"Wrong fitness" "Wrong fitness."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Wrong fitness."
CamlinternalFormatBasics.End_of_format) "Wrong fitness.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_fitness" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Wrong_fitness" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "outdated_fitness"
"Outdated fitness" "Outdated fitness: referring to a previous version"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Outdated fitness: referring to a previous version."
CamlinternalFormatBasics.End_of_format)
"Outdated fitness: referring to a previous version.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Outdated_fitness" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Outdated_fitness" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"locked_round_not_less_than_round" "Locked round not smaller than round"
"The round is smaller than or equal to the locked round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
let '(round, locked_round) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Incorrect fitness: round "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is less than or equal to locked round "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Incorrect fitness: round %a is less than or equal to locked round %a.")
Round_repr.pp round Round_repr.pp locked_round))
(Data_encoding.obj2
(Data_encoding.req None None "round" Round_repr.encoding)
(Data_encoding.req None None "locked_round" Round_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Locked_round_not_less_than_round" then
let '{|
Locked_round_not_less_than_round.round := round;
Locked_round_not_less_than_round.locked_round := locked_round
|} := cast Locked_round_not_less_than_round payload in
Some (round, locked_round)
else None
end)
(fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
let '(round, locked_round) := function_parameter in
Build_extensible "Locked_round_not_less_than_round"
Locked_round_not_less_than_round
{| Locked_round_not_less_than_round.round := round;
Locked_round_not_less_than_round.locked_round := locked_round; |}).
Definition create_without_locked_round
(level : Raw_level_repr.t) (predecessor_round : Round_repr.t)
(round : Round_repr.t) : t :=
{| t.level := level; t.locked_round := None;
t.predecessor_round := predecessor_round; t.round := round; |}.
Definition create
(level : Raw_level_repr.t) (locked_round : option Round_repr.t)
(predecessor_round : Round_repr.t) (round : Round_repr.t) : M? t :=
match locked_round with
| None ⇒
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
| Some locked_round_val ⇒
let? '_ :=
Error_monad.error_when (Round_repr.op_lteq round locked_round_val)
(Build_extensible "Locked_round_not_less_than_round"
Locked_round_not_less_than_round
{| Locked_round_not_less_than_round.round := round;
Locked_round_not_less_than_round.locked_round := locked_round_val;
|}) in
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
end.
Definition int32_to_bytes (i_value : int32) : bytes :=
let b_value := Bytes.make 4 "000" % char in
let '_ := TzEndian.set_int32 b_value 0 i_value in
b_value.
Definition int32_of_bytes (b_value : bytes) : M? int32 :=
if (Bytes.length b_value) ≠i 4 then
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
else
return? (TzEndian.get_int32 b_value 0).
Definition locked_round_to_bytes (function_parameter : option Round_repr.t)
: bytes :=
match function_parameter with
| None ⇒ Bytes.empty
| Some locked_round ⇒ int32_to_bytes (Round_repr.to_int32 locked_round)
end.
Definition locked_round_of_bytes (b_value : bytes) : M? (option Round_repr.t) :=
if (Bytes.length b_value) =i 0 then
return? None
else
if (Bytes.length b_value) =i 4 then
let? r_value := Round_repr.of_int32 (TzEndian.get_int32 b_value 0) in
return? (Some r_value)
else
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt).
Definition predecessor_round_of_bytes (neg_predecessor_round : bytes)
: M? Round_repr.t :=
let? neg_predecessor_round := int32_of_bytes neg_predecessor_round in
Round_repr.of_int32 (Int32.pred (Int32.neg neg_predecessor_round)).
Definition round_of_bytes (round : bytes) : M? Round_repr.t :=
Error_monad.op_gtgtquestion (int32_of_bytes round) Round_repr.of_int32.
Definition to_raw (function_parameter : t) : list bytes :=
let '{|
t.level := level;
t.locked_round := locked_round;
t.predecessor_round := predecessor_round;
t.round := round
|} := function_parameter in
[
Bytes.of_string Constants_repr.fitness_version_number;
int32_to_bytes (Raw_level_repr.to_int32 level);
locked_round_to_bytes locked_round;
int32_to_bytes
(Int32.pred (Int32.neg (Round_repr.to_int32 predecessor_round)));
int32_to_bytes (Round_repr.to_int32 round)
].
Definition from_raw (function_parameter : list bytes) : M? t :=
match
(function_parameter,
match function_parameter with
|
cons version
(cons level
(cons locked_round (cons neg_predecessor_round (cons round [])))) ⇒
Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end,
match function_parameter with
| cons version (cons _ []) ⇒
Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end) with
|
(cons version
(cons level
(cons locked_round (cons neg_predecessor_round (cons round [])))), true,
_) ⇒
let? level :=
Error_monad.op_gtgtquestion (int32_of_bytes level) Raw_level_repr.of_int32
in
let? locked_round := locked_round_of_bytes locked_round in
let? predecessor_round := predecessor_round_of_bytes neg_predecessor_round
in
let? round := round_of_bytes round in
create level locked_round predecessor_round round
| (cons version (cons _ []), _, true) ⇒
Error_monad.error_value (Build_extensible "Outdated_fitness" unit tt)
| ([], _, _) ⇒
Error_monad.error_value (Build_extensible "Outdated_fitness" unit tt)
| (_, _, _) ⇒
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
end.
Definition round_from_raw (function_parameter : list bytes) : M? Round_repr.t :=
match
(function_parameter,
match function_parameter with
|
cons version
(cons _level
(cons _locked_round (cons _neg_predecessor_round (cons round []))))
⇒
Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end,
match function_parameter with
| cons version (cons _ []) ⇒
Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end) with
|
(cons version
(cons _level
(cons _locked_round (cons _neg_predecessor_round (cons round [])))),
true, _) ⇒ round_of_bytes round
| (cons version (cons _ []), _, true) ⇒ return? Round_repr.zero
| ([], _, _) ⇒ return? Round_repr.zero
| (_, _, _) ⇒
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
end.
Definition predecessor_round_from_raw (function_parameter : list bytes)
: M? Round_repr.t :=
match
(function_parameter,
match function_parameter with
|
cons version
(cons _level
(cons _locked_round (cons neg_predecessor_round (cons _round []))))
⇒
Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end,
match function_parameter with
| cons version (cons _ []) ⇒
Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end) with
|
(cons version
(cons _level
(cons _locked_round (cons neg_predecessor_round (cons _round [])))),
true, _) ⇒ predecessor_round_of_bytes neg_predecessor_round
| (cons version (cons _ []), _, true) ⇒ return? Round_repr.zero
| ([], _, _) ⇒ return? Round_repr.zero
| (_, _, _) ⇒
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
end.
Definition check_except_locked_round
(fitness : t) (level : Raw_level_repr.raw_level)
(predecessor_round : Round_repr.t) : M? unit :=
let '{|
t.level := expected_level;
t.locked_round := _;
t.predecessor_round := expected_predecessor_round;
t.round := _
|} := fitness in
let correct :=
(Raw_level_repr.op_eq level expected_level) &&
(Round_repr.op_eq predecessor_round expected_predecessor_round) in
Error_monad.error_unless correct (Build_extensible "Wrong_fitness" unit tt).
Definition check_locked_round (fitness : t) (locked_round : option Round_repr.t)
: M? unit :=
let '{|
t.level := _;
t.locked_round := expected_locked_round;
t.predecessor_round := _;
t.round := _
|} := fitness in
let correct :=
match (locked_round, expected_locked_round) with
| (None, None) ⇒ true
| ((Some _, None) | (None, Some _)) ⇒ false
| (Some v_value, Some v') ⇒ Round_repr.op_eq v_value v'
end in
Error_monad.error_unless correct (Build_extensible "Wrong_fitness" unit tt).
Definition level (fitness : t) : Raw_level_repr.t := fitness.(t.level).
Definition round (fitness : t) : Round_repr.t := fitness.(t.round).
Definition locked_round (fitness : t) : option Round_repr.t :=
fitness.(t.locked_round).
Definition predecessor_round (fitness : t) : Round_repr.t :=
fitness.(t.predecessor_round).
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "invalid_fitness"
"Invalid fitness"
"Fitness representation should be exactly 4 times 4 bytes long."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Invalid fitness"
CamlinternalFormatBasics.End_of_format) "Invalid fitness")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_fitness" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Invalid_fitness" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "wrong_fitness"
"Wrong fitness" "Wrong fitness."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Wrong fitness."
CamlinternalFormatBasics.End_of_format) "Wrong fitness.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_fitness" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Wrong_fitness" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent "outdated_fitness"
"Outdated fitness" "Outdated fitness: referring to a previous version"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Outdated fitness: referring to a previous version."
CamlinternalFormatBasics.End_of_format)
"Outdated fitness: referring to a previous version.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Outdated_fitness" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Outdated_fitness" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent
"locked_round_not_less_than_round" "Locked round not smaller than round"
"The round is smaller than or equal to the locked round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
let '(round, locked_round) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Incorrect fitness: round "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is less than or equal to locked round "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Incorrect fitness: round %a is less than or equal to locked round %a.")
Round_repr.pp round Round_repr.pp locked_round))
(Data_encoding.obj2
(Data_encoding.req None None "round" Round_repr.encoding)
(Data_encoding.req None None "locked_round" Round_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Locked_round_not_less_than_round" then
let '{|
Locked_round_not_less_than_round.round := round;
Locked_round_not_less_than_round.locked_round := locked_round
|} := cast Locked_round_not_less_than_round payload in
Some (round, locked_round)
else None
end)
(fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
let '(round, locked_round) := function_parameter in
Build_extensible "Locked_round_not_less_than_round"
Locked_round_not_less_than_round
{| Locked_round_not_less_than_round.round := round;
Locked_round_not_less_than_round.locked_round := locked_round; |}).
Definition create_without_locked_round
(level : Raw_level_repr.t) (predecessor_round : Round_repr.t)
(round : Round_repr.t) : t :=
{| t.level := level; t.locked_round := None;
t.predecessor_round := predecessor_round; t.round := round; |}.
Definition create
(level : Raw_level_repr.t) (locked_round : option Round_repr.t)
(predecessor_round : Round_repr.t) (round : Round_repr.t) : M? t :=
match locked_round with
| None ⇒
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
| Some locked_round_val ⇒
let? '_ :=
Error_monad.error_when (Round_repr.op_lteq round locked_round_val)
(Build_extensible "Locked_round_not_less_than_round"
Locked_round_not_less_than_round
{| Locked_round_not_less_than_round.round := round;
Locked_round_not_less_than_round.locked_round := locked_round_val;
|}) in
return?
{| t.level := level; t.locked_round := locked_round;
t.predecessor_round := predecessor_round; t.round := round; |}
end.
Definition int32_to_bytes (i_value : int32) : bytes :=
let b_value := Bytes.make 4 "000" % char in
let '_ := TzEndian.set_int32 b_value 0 i_value in
b_value.
Definition int32_of_bytes (b_value : bytes) : M? int32 :=
if (Bytes.length b_value) ≠i 4 then
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
else
return? (TzEndian.get_int32 b_value 0).
Definition locked_round_to_bytes (function_parameter : option Round_repr.t)
: bytes :=
match function_parameter with
| None ⇒ Bytes.empty
| Some locked_round ⇒ int32_to_bytes (Round_repr.to_int32 locked_round)
end.
Definition locked_round_of_bytes (b_value : bytes) : M? (option Round_repr.t) :=
if (Bytes.length b_value) =i 0 then
return? None
else
if (Bytes.length b_value) =i 4 then
let? r_value := Round_repr.of_int32 (TzEndian.get_int32 b_value 0) in
return? (Some r_value)
else
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt).
Definition predecessor_round_of_bytes (neg_predecessor_round : bytes)
: M? Round_repr.t :=
let? neg_predecessor_round := int32_of_bytes neg_predecessor_round in
Round_repr.of_int32 (Int32.pred (Int32.neg neg_predecessor_round)).
Definition round_of_bytes (round : bytes) : M? Round_repr.t :=
Error_monad.op_gtgtquestion (int32_of_bytes round) Round_repr.of_int32.
Definition to_raw (function_parameter : t) : list bytes :=
let '{|
t.level := level;
t.locked_round := locked_round;
t.predecessor_round := predecessor_round;
t.round := round
|} := function_parameter in
[
Bytes.of_string Constants_repr.fitness_version_number;
int32_to_bytes (Raw_level_repr.to_int32 level);
locked_round_to_bytes locked_round;
int32_to_bytes
(Int32.pred (Int32.neg (Round_repr.to_int32 predecessor_round)));
int32_to_bytes (Round_repr.to_int32 round)
].
Definition from_raw (function_parameter : list bytes) : M? t :=
match
(function_parameter,
match function_parameter with
|
cons version
(cons level
(cons locked_round (cons neg_predecessor_round (cons round [])))) ⇒
Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end,
match function_parameter with
| cons version (cons _ []) ⇒
Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end) with
|
(cons version
(cons level
(cons locked_round (cons neg_predecessor_round (cons round [])))), true,
_) ⇒
let? level :=
Error_monad.op_gtgtquestion (int32_of_bytes level) Raw_level_repr.of_int32
in
let? locked_round := locked_round_of_bytes locked_round in
let? predecessor_round := predecessor_round_of_bytes neg_predecessor_round
in
let? round := round_of_bytes round in
create level locked_round predecessor_round round
| (cons version (cons _ []), _, true) ⇒
Error_monad.error_value (Build_extensible "Outdated_fitness" unit tt)
| ([], _, _) ⇒
Error_monad.error_value (Build_extensible "Outdated_fitness" unit tt)
| (_, _, _) ⇒
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
end.
Definition round_from_raw (function_parameter : list bytes) : M? Round_repr.t :=
match
(function_parameter,
match function_parameter with
|
cons version
(cons _level
(cons _locked_round (cons _neg_predecessor_round (cons round []))))
⇒
Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end,
match function_parameter with
| cons version (cons _ []) ⇒
Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end) with
|
(cons version
(cons _level
(cons _locked_round (cons _neg_predecessor_round (cons round [])))),
true, _) ⇒ round_of_bytes round
| (cons version (cons _ []), _, true) ⇒ return? Round_repr.zero
| ([], _, _) ⇒ return? Round_repr.zero
| (_, _, _) ⇒
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
end.
Definition predecessor_round_from_raw (function_parameter : list bytes)
: M? Round_repr.t :=
match
(function_parameter,
match function_parameter with
|
cons version
(cons _level
(cons _locked_round (cons neg_predecessor_round (cons _round []))))
⇒
Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end,
match function_parameter with
| cons version (cons _ []) ⇒
Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
Constants_repr.fitness_version_number
| _ ⇒ false
end) with
|
(cons version
(cons _level
(cons _locked_round (cons neg_predecessor_round (cons _round [])))),
true, _) ⇒ predecessor_round_of_bytes neg_predecessor_round
| (cons version (cons _ []), _, true) ⇒ return? Round_repr.zero
| ([], _, _) ⇒ return? Round_repr.zero
| (_, _, _) ⇒
Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
end.
Definition check_except_locked_round
(fitness : t) (level : Raw_level_repr.raw_level)
(predecessor_round : Round_repr.t) : M? unit :=
let '{|
t.level := expected_level;
t.locked_round := _;
t.predecessor_round := expected_predecessor_round;
t.round := _
|} := fitness in
let correct :=
(Raw_level_repr.op_eq level expected_level) &&
(Round_repr.op_eq predecessor_round expected_predecessor_round) in
Error_monad.error_unless correct (Build_extensible "Wrong_fitness" unit tt).
Definition check_locked_round (fitness : t) (locked_round : option Round_repr.t)
: M? unit :=
let '{|
t.level := _;
t.locked_round := expected_locked_round;
t.predecessor_round := _;
t.round := _
|} := fitness in
let correct :=
match (locked_round, expected_locked_round) with
| (None, None) ⇒ true
| ((Some _, None) | (None, Some _)) ⇒ false
| (Some v_value, Some v') ⇒ Round_repr.op_eq v_value v'
end in
Error_monad.error_unless correct (Build_extensible "Wrong_fitness" unit tt).
Definition level (fitness : t) : Raw_level_repr.t := fitness.(t.level).
Definition round (fitness : t) : Round_repr.t := fitness.(t.round).
Definition locked_round (fitness : t) : option Round_repr.t :=
fitness.(t.locked_round).
Definition predecessor_round (fitness : t) : Round_repr.t :=
fitness.(t.predecessor_round).