Skip to main content

🌱 Seed_repr.v

Translated OCaml

See proofs, Gitlab , 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.

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_seednonce_value (B initial_seed) initial_nonce_0
    | NoneB (State_hash.hash_bytes None nil)
    end in
  loop nil first_seed n_value.