Skip to main content

🥊 Round_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.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.

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 roundPervasives.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_valueSome 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 roundsPervasives.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).

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.

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);
          |}.

Complexity: O(|round_durations|).
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|).
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.