🌱 Seed_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.State_hash.
Inductive seed : Set :=
| B : State_hash.t → seed.
Inductive t : Set :=
| T : State_hash.t → t.
Inductive sequence : Set :=
| S : State_hash.t → sequence.
Definition nonce : Set := bytes.
Definition nonce_encoding : Data_encoding.encoding bytes :=
Data_encoding.Fixed.bytes_value Constants_repr.nonce_length.
Definition initial_seed : string := "Laissez-faire les proprietaires.".
Definition zero_bytes : bytes := Bytes.make Nonce_hash.size_value "000" % char.
Definition state_hash_encoding : Data_encoding.encoding State_hash.t :=
Data_encoding.conv State_hash.to_bytes State_hash.of_bytes_exn None
(Data_encoding.Fixed.bytes_value Nonce_hash.size_value).
Definition seed_encoding : Data_encoding.encoding seed :=
Data_encoding.conv
(fun (function_parameter : seed) ⇒
let 'B b_value := function_parameter in
b_value) (fun (b_value : State_hash.t) ⇒ B b_value) None
state_hash_encoding.
Definition empty : seed := B (State_hash.hash_string None [ initial_seed ]).
Definition nonce_value (function_parameter : seed) : bytes → seed :=
let 'B state_value := function_parameter in
fun (nonce_value : bytes) ⇒
B
(State_hash.hash_bytes None
[ State_hash.to_bytes state_value; nonce_value ]).
Definition initialize_new (function_parameter : seed) : list bytes → t :=
let 'B state_value := function_parameter in
fun (append : list bytes) ⇒
T
(State_hash.hash_bytes None
(cons (State_hash.to_bytes state_value) (cons zero_bytes append))).
Definition xor_higher_bits (i_value : int32) (b_value : bytes) : bytes :=
let higher := TzEndian.get_int32 b_value 0 in
let r_value := Int32.logxor higher i_value in
let res := Bytes.copy b_value in
let '_ := TzEndian.set_int32 res 0 r_value in
res.
Definition sequence_value (function_parameter : t) : int32 → sequence :=
let 'T state_value := function_parameter in
fun (n_value : int32) ⇒
(fun (b_value : bytes) ⇒ S (State_hash.hash_bytes None [ b_value ]))
(xor_higher_bits n_value (State_hash.to_bytes state_value)).
Definition take (function_parameter : sequence) : bytes × sequence :=
let 'S state_value := function_parameter in
let b_value := State_hash.to_bytes state_value in
let h_value := State_hash.hash_bytes None [ b_value ] in
((State_hash.to_bytes h_value), (S h_value)).
#[bypass_check(guard)]
Definition take_int32 (s_value : sequence) (bound : int32) : int32 × sequence :=
if bound ≤i32 0 then
Pervasives.invalid_arg "Seed_repr.take_int32"
else
let drop_if_over := Int32.max_int -i32 (Int32.rem Int32.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int32 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int32 bytes_value 0 in
let r_value :=
if r_value =i32 Int32.min_int then
0
else
Int32.abs r_value in
if r_value ≥i32 drop_if_over then
loop s_value
else
let v_value := Int32.rem r_value bound in
(v_value, s_value) in
loop s_value.
#[bypass_check(guard)]
Definition take_int64 (s_value : sequence) (bound : int64) : int64 × sequence :=
if bound ≤i64 0 then
Pervasives.invalid_arg "Seed_repr.take_int64"
else
let drop_if_over := Int64.max_int -i64 (Int64.rem Int64.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int64 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int64 bytes_value 0 in
let r_value :=
if r_value =i64 Int64.min_int then
0
else
Int64.abs r_value in
if r_value ≥i64 drop_if_over then
loop s_value
else
let v_value := Int64.rem r_value bound in
(v_value, s_value) in
loop s_value.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.State_hash.
Inductive seed : Set :=
| B : State_hash.t → seed.
Inductive t : Set :=
| T : State_hash.t → t.
Inductive sequence : Set :=
| S : State_hash.t → sequence.
Definition nonce : Set := bytes.
Definition nonce_encoding : Data_encoding.encoding bytes :=
Data_encoding.Fixed.bytes_value Constants_repr.nonce_length.
Definition initial_seed : string := "Laissez-faire les proprietaires.".
Definition zero_bytes : bytes := Bytes.make Nonce_hash.size_value "000" % char.
Definition state_hash_encoding : Data_encoding.encoding State_hash.t :=
Data_encoding.conv State_hash.to_bytes State_hash.of_bytes_exn None
(Data_encoding.Fixed.bytes_value Nonce_hash.size_value).
Definition seed_encoding : Data_encoding.encoding seed :=
Data_encoding.conv
(fun (function_parameter : seed) ⇒
let 'B b_value := function_parameter in
b_value) (fun (b_value : State_hash.t) ⇒ B b_value) None
state_hash_encoding.
Definition empty : seed := B (State_hash.hash_string None [ initial_seed ]).
Definition nonce_value (function_parameter : seed) : bytes → seed :=
let 'B state_value := function_parameter in
fun (nonce_value : bytes) ⇒
B
(State_hash.hash_bytes None
[ State_hash.to_bytes state_value; nonce_value ]).
Definition initialize_new (function_parameter : seed) : list bytes → t :=
let 'B state_value := function_parameter in
fun (append : list bytes) ⇒
T
(State_hash.hash_bytes None
(cons (State_hash.to_bytes state_value) (cons zero_bytes append))).
Definition xor_higher_bits (i_value : int32) (b_value : bytes) : bytes :=
let higher := TzEndian.get_int32 b_value 0 in
let r_value := Int32.logxor higher i_value in
let res := Bytes.copy b_value in
let '_ := TzEndian.set_int32 res 0 r_value in
res.
Definition sequence_value (function_parameter : t) : int32 → sequence :=
let 'T state_value := function_parameter in
fun (n_value : int32) ⇒
(fun (b_value : bytes) ⇒ S (State_hash.hash_bytes None [ b_value ]))
(xor_higher_bits n_value (State_hash.to_bytes state_value)).
Definition take (function_parameter : sequence) : bytes × sequence :=
let 'S state_value := function_parameter in
let b_value := State_hash.to_bytes state_value in
let h_value := State_hash.hash_bytes None [ b_value ] in
((State_hash.to_bytes h_value), (S h_value)).
#[bypass_check(guard)]
Definition take_int32 (s_value : sequence) (bound : int32) : int32 × sequence :=
if bound ≤i32 0 then
Pervasives.invalid_arg "Seed_repr.take_int32"
else
let drop_if_over := Int32.max_int -i32 (Int32.rem Int32.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int32 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int32 bytes_value 0 in
let r_value :=
if r_value =i32 Int32.min_int then
0
else
Int32.abs r_value in
if r_value ≥i32 drop_if_over then
loop s_value
else
let v_value := Int32.rem r_value bound in
(v_value, s_value) in
loop s_value.
#[bypass_check(guard)]
Definition take_int64 (s_value : sequence) (bound : int64) : int64 × sequence :=
if bound ≤i64 0 then
Pervasives.invalid_arg "Seed_repr.take_int64"
else
let drop_if_over := Int64.max_int -i64 (Int64.rem Int64.max_int bound) in
let fix loop (s_value : sequence) {struct s_value} : int64 × sequence :=
let '(bytes_value, s_value) := take s_value in
let r_value := TzEndian.get_int64 bytes_value 0 in
let r_value :=
if r_value =i64 Int64.min_int then
0
else
Int64.abs r_value in
if r_value ≥i64 drop_if_over then
loop s_value
else
let v_value := Int64.rem r_value bound in
(v_value, s_value) in
loop s_value.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_nonce_length" "Unexpected nonce length"
"Nonce length is incorrect."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Nonce length is not "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" bytes long as it should."
CamlinternalFormatBasics.End_of_format)))
"Nonce length is not %i bytes long as it should.")
Constants_repr.nonce_length)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_nonce_length" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_nonce_length" unit tt).
Definition make_nonce (nonce_value : bytes) : M? bytes :=
if (Bytes.length nonce_value) ≠i Constants_repr.nonce_length then
Error_monad.error_value (Build_extensible "Unexpected_nonce_length" unit tt)
else
return? nonce_value.
Definition hash_value (nonce_value : bytes) : Nonce_hash.t :=
Nonce_hash.hash_bytes None [ nonce_value ].
Definition check_hash (nonce_value : bytes) (hash_value : Nonce_hash.t)
: bool :=
((Bytes.length nonce_value) =i Constants_repr.nonce_length) &&
(Nonce_hash.equal (Nonce_hash.hash_bytes None [ nonce_value ]) hash_value).
Definition nonce_hash_key_part : Nonce_hash.t → list string → list string :=
Nonce_hash.to_path.
Definition initial_nonce_0 : bytes := zero_bytes.
Definition initial_nonce_hash_0 : Nonce_hash.t := hash_value initial_nonce_0.
Definition deterministic_seed (seed_value : seed) : seed :=
nonce_value seed_value zero_bytes.
#[bypass_check(guard)]
Definition initial_seeds (initial_seed : option State_hash.t) (n_value : int)
: list seed :=
let fix loop (acc_value : list seed) (elt_value : seed) (i_value : int)
{struct i_value} : list seed :=
if i_value =i 1 then
List.rev (cons elt_value acc_value)
else
loop (cons elt_value acc_value) (deterministic_seed elt_value)
(i_value -i 1) in
let first_seed :=
match initial_seed with
| Some initial_seed ⇒ nonce_value (B initial_seed) initial_nonce_0
| None ⇒ B (State_hash.hash_bytes None nil)
end in
loop nil first_seed n_value.
Error_monad.register_error_kind Error_monad.Permanent
"unexpected_nonce_length" "Unexpected nonce length"
"Nonce length is incorrect."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Nonce length is not "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" bytes long as it should."
CamlinternalFormatBasics.End_of_format)))
"Nonce length is not %i bytes long as it should.")
Constants_repr.nonce_length)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_nonce_length" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_nonce_length" unit tt).
Definition make_nonce (nonce_value : bytes) : M? bytes :=
if (Bytes.length nonce_value) ≠i Constants_repr.nonce_length then
Error_monad.error_value (Build_extensible "Unexpected_nonce_length" unit tt)
else
return? nonce_value.
Definition hash_value (nonce_value : bytes) : Nonce_hash.t :=
Nonce_hash.hash_bytes None [ nonce_value ].
Definition check_hash (nonce_value : bytes) (hash_value : Nonce_hash.t)
: bool :=
((Bytes.length nonce_value) =i Constants_repr.nonce_length) &&
(Nonce_hash.equal (Nonce_hash.hash_bytes None [ nonce_value ]) hash_value).
Definition nonce_hash_key_part : Nonce_hash.t → list string → list string :=
Nonce_hash.to_path.
Definition initial_nonce_0 : bytes := zero_bytes.
Definition initial_nonce_hash_0 : Nonce_hash.t := hash_value initial_nonce_0.
Definition deterministic_seed (seed_value : seed) : seed :=
nonce_value seed_value zero_bytes.
#[bypass_check(guard)]
Definition initial_seeds (initial_seed : option State_hash.t) (n_value : int)
: list seed :=
let fix loop (acc_value : list seed) (elt_value : seed) (i_value : int)
{struct i_value} : list seed :=
if i_value =i 1 then
List.rev (cons elt_value acc_value)
else
loop (cons elt_value acc_value) (deterministic_seed elt_value)
(i_value -i 1) in
let first_seed :=
match initial_seed with
| Some initial_seed ⇒ nonce_value (B initial_seed) initial_nonce_0
| None ⇒ B (State_hash.hash_bytes None nil)
end in
loop nil first_seed n_value.