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.Environment.V7.
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 vdf_setup : Set := Vdf.discriminant × Vdf.challenge.

Definition vdf_solution : Set := Vdf.result × Vdf.proof.

Definition seed_to_bytes (x_value : seed) : bytes :=
  let seed_to_state_hash (function_parameter : seed) : State_hash.t :=
    let 'B b_value := function_parameter in
    b_value in
  State_hash.to_bytes (seed_to_state_hash x_value).

Definition vdf_setup_encoding
  : Data_encoding.encoding (Vdf.discriminant × Vdf.challenge) :=
  let vdf_discriminant_encoding :=
    Data_encoding.conv_with_guard Vdf.discriminant_to_bytes
      (fun (b_value : bytes) ⇒
        Option.to_result "VDF discriminant could not be deserialised"
          (Vdf.discriminant_of_bytes_opt b_value)) None
      (Data_encoding.Fixed.bytes_value Vdf.discriminant_size_bytes) in
  let vdf_challenge_encoding :=
    Data_encoding.conv_with_guard Vdf.challenge_to_bytes
      (fun (b_value : bytes) ⇒
        Option.to_result "VDF challenge could not be deserialised"
          (Vdf.challenge_of_bytes_opt b_value)) None
      (Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
  Data_encoding.tup2 vdf_discriminant_encoding vdf_challenge_encoding.

Definition vdf_solution_encoding
  : Data_encoding.encoding (Vdf.result × Vdf.proof) :=
  let vdf_result_encoding :=
    Data_encoding.conv_with_guard Vdf.result_to_bytes
      (fun (b_value : bytes) ⇒
        Option.to_result "VDF result could not be deserialised"
          (Vdf.result_of_bytes_opt b_value)) None
      (Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
  let vdf_proof_encoding :=
    Data_encoding.conv_with_guard Vdf.proof_to_bytes
      (fun (b_value : bytes) ⇒
        Option.to_result "VDF proof could not be deserialised"
          (Vdf.proof_of_bytes_opt b_value)) None
      (Data_encoding.Fixed.bytes_value Vdf.form_size_bytes) in
  Data_encoding.tup2 vdf_result_encoding vdf_proof_encoding.

Definition pp_solution
  (ppf : Format.formatter) (solution : Vdf.result × Vdf.proof) : unit :=
  let '(result_value, proof_value) := solution in
  let '_ :=
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<v 2>"
                CamlinternalFormatBasics.End_of_format) "<v 2>"))
          (CamlinternalFormatBasics.String_literal "VDF result: "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format))) "@[<v 2>VDF result: %a")
      Hex.pp (Hex.of_bytes None (Vdf.result_to_bytes result_value)) in
  let '_ :=
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_lit
          (CamlinternalFormatBasics.Break "@," 0 0)
          (CamlinternalFormatBasics.String_literal "VDF proof: "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format))) "@,VDF proof: %a")
      Hex.pp (Hex.of_bytes None (Vdf.proof_to_bytes proof_value)) in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_lit
        CamlinternalFormatBasics.Close_box
        CamlinternalFormatBasics.End_of_format) "@]").

Definition nonce_encoding : Data_encoding.encoding bytes :=
  Data_encoding.Fixed.bytes_value Constants_repr.nonce_length.

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

Definition nonce_discriminant : bytes :=
  Bytes.of_string "Tezos_generating_vdf_discriminant".

Definition nonce_challenge : bytes :=
  Bytes.of_string "Tezos_generating_vdf_challenge".

Definition generate_vdf_setup (seed_discriminant : seed) (seed_challenge : seed)
  : Vdf.discriminant × Vdf.challenge :=
  let size_value := Vdf.discriminant_size_bytes in
  let seed_value :=
    seed_to_bytes (update_seed_aux seed_discriminant nonce_discriminant) in
  let discriminant := Vdf.generate_discriminant (Some seed_value) size_value in
  let input := seed_to_bytes (update_seed_aux seed_challenge nonce_challenge) in
  let challenge := Vdf.generate_challenge discriminant input in
  (discriminant, challenge).

Definition verify (function_parameter : Vdf.discriminant × Vdf.challenge)
  : Vdf.difficulty Vdf.result × Vdf.proof option bool :=
  let '(discriminant, challenge) := function_parameter in
  fun (vdf_difficulty : Vdf.difficulty) ⇒
    fun (solution : Vdf.result × Vdf.proof) ⇒
      let '(result_value, proof_value) := solution in
      Option.catch None
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Vdf.verify discriminant challenge vdf_difficulty result_value
            proof_value).

Definition vdf_to_seed {A : Set}
  (seed_challenge : seed) (solution : Vdf.result × A) : seed :=
  let '(result_value, _) := solution in
  update_seed_aux seed_challenge (Vdf.result_to_bytes result_value).

Inductive seed_status : Set :=
| RANDAO_seed : seed_status
| VDF_seed : seed_status.

Definition seed_status_encoding : Data_encoding.encoding seed_status :=
  let to_bool (function_parameter : seed_status) : bool :=
    match function_parameter with
    | RANDAO_seedfalse
    | VDF_seedtrue
    end in
  let of_bool (t_value : bool) : seed_status :=
    if t_value then
      VDF_seed
    else
      RANDAO_seed in
  Data_encoding.conv to_bool of_bool None Data_encoding.bool_value.

Definition compare_vdf_solution {A B : Set}
  (solution : Vdf.result × A) (solution' : Vdf.result × B) : int :=
  let '(result_value, _) := solution in
  let '(result', _) := solution' in
  Compare.Bytes.(Compare.S.compare) (Vdf.result_to_bytes result_value)
    (Vdf.result_to_bytes result').