Skip to main content

🪜 Level_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.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.

Module t.
  Record record : Set := Build {
    level : Raw_level_repr.t;
    level_position : int32;
    cycle : Cycle_repr.t;
    cycle_position : int32;
    expected_commitment : bool;
  }.
  Definition with_level level (r : record) :=
    Build level r.(level_position) r.(cycle) r.(cycle_position)
      r.(expected_commitment).
  Definition with_level_position level_position (r : record) :=
    Build r.(level) level_position r.(cycle) r.(cycle_position)
      r.(expected_commitment).
  Definition with_cycle cycle (r : record) :=
    Build r.(level) r.(level_position) cycle r.(cycle_position)
      r.(expected_commitment).
  Definition with_cycle_position cycle_position (r : record) :=
    Build r.(level) r.(level_position) r.(cycle) cycle_position
      r.(expected_commitment).
  Definition with_expected_commitment expected_commitment (r : record) :=
    Build r.(level) r.(level_position) r.(cycle) r.(cycle_position)
      expected_commitment.
End t.
Definition t := t.record.

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    let compare (function_parameter : t) : t int :=
      let '{| t.level := l1 |} := function_parameter in
      fun (function_parameter : t) ⇒
        let '{| t.level := l2 |} := function_parameter in
        Raw_level_repr.compare l1 l2 in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_Make_include]
Definition op_eq := Compare_Make_include.(Compare.S.op_eq).

Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).

Definition op_lt := Compare_Make_include.(Compare.S.op_lt).

Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).

Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).

Definition op_gt := Compare_Make_include.(Compare.S.op_gt).

Definition compare := Compare_Make_include.(Compare.S.compare).

Definition equal := Compare_Make_include.(Compare.S.equal).

Definition max := Compare_Make_include.(Compare.S.max).

Definition min := Compare_Make_include.(Compare.S.min).

Definition level : Set := t.

Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  let '{| t.level := level |} := function_parameter in
  Raw_level_repr.pp ppf level.

Definition pp_full (ppf : Format.formatter) (l_value : t) : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Alpha
        (CamlinternalFormatBasics.Char_literal "." % char
          (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            (CamlinternalFormatBasics.String_literal " (cycle "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Char_literal "." % char
                  (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format))))))))
      "%a.%ld (cycle %a.%ld)") Raw_level_repr.pp l_value.(t.level)
    l_value.(t.level_position) Cycle_repr.pp l_value.(t.cycle)
    l_value.(t.cycle_position).

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{|
        t.level := level;
          t.level_position := level_position;
          t.cycle := cycle;
          t.cycle_position := cycle_position;
          t.expected_commitment := expected_commitment
          |} := function_parameter in
      (level, level_position, cycle, cycle_position, expected_commitment))
    (fun (function_parameter :
      Raw_level_repr.t × int32 × Cycle_repr.t × int32 × bool) ⇒
      let
        '(level, level_position, cycle, cycle_position, expected_commitment) :=
        function_parameter in
      {| t.level := level; t.level_position := level_position; t.cycle := cycle;
        t.cycle_position := cycle_position;
        t.expected_commitment := expected_commitment; |}) None
    (Data_encoding.obj5
      (Data_encoding.req None
        (Some
          "The level of the block relative to genesis. This is also the Shell's notion of level.")
        "level" Raw_level_repr.encoding)
      (Data_encoding.req None
        (Some
          "The level of the block relative to the successor of the genesis block. More precisely, it is the position of the block relative to the block that starts the \""Alpha family\"" of protocols, which includes all protocols except Genesis (that is, from 001 onwards).")
        "level_position" Data_encoding.int32_value)
      (Data_encoding.req None
        (Some
          "The current cycle's number. Note that cycles are a protocol-specific notion. As a result, the cycle number starts at 0 with the first block of the Alpha family of protocols.")
        "cycle" Cycle_repr.encoding)
      (Data_encoding.req None
        (Some
          "The current level of the block relative to the first block of the current cycle.")
        "cycle_position" Data_encoding.int32_value)
      (Data_encoding.req None
        (Some
          "Tells whether the baker of this block has to commit a seed nonce hash.")
        "expected_commitment" Data_encoding.bool_value)).

Definition diff_value (function_parameter : t) : t int32 :=
  let '{| t.level := l1 |} := function_parameter in
  fun (function_parameter : t) ⇒
    let '{| t.level := l2 |} := function_parameter in
    (Raw_level_repr.to_int32 l1) -i32 (Raw_level_repr.to_int32 l2).

Module cycle_era.
  Record record : Set := Build {
    first_level : Raw_level_repr.t;
    first_cycle : Cycle_repr.t;
    blocks_per_cycle : int32;
    blocks_per_commitment : int32;
  }.
  Definition with_first_level first_level (r : record) :=
    Build first_level r.(first_cycle) r.(blocks_per_cycle)
      r.(blocks_per_commitment).
  Definition with_first_cycle first_cycle (r : record) :=
    Build r.(first_level) first_cycle r.(blocks_per_cycle)
      r.(blocks_per_commitment).
  Definition with_blocks_per_cycle blocks_per_cycle (r : record) :=
    Build r.(first_level) r.(first_cycle) blocks_per_cycle
      r.(blocks_per_commitment).
  Definition with_blocks_per_commitment blocks_per_commitment (r : record) :=
    Build r.(first_level) r.(first_cycle) r.(blocks_per_cycle)
      blocks_per_commitment.
End cycle_era.
Definition cycle_era := cycle_era.record.

Definition cycle_eras : Set := list cycle_era.

Init function; without side-effects in Coq
Definition init_module1 : unit :=
  Error_monad.register_error_kind Error_monad.Temporary
    "level_repr.invalid_cycle_eras" "Invalid cycle eras"
    "The cycles eras are not valid: empty list or non-decreasing first levels or first cycles."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "The cycles eras are not valid: empty list or non-decreasing first levels or first cycles."
                CamlinternalFormatBasics.End_of_format)
              "The cycles eras are not valid: empty list or non-decreasing first levels or first cycles.")))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_cycle_eras" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Invalid_cycle_eras" unit tt).

Definition create_cycle_eras (cycle_eras : list cycle_era)
  : M? (list cycle_era) :=
  match cycle_eras with
  | []
    Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
  | cons newest_era older_eras
    let fix aux (era : cycle_era) (older_eras : list cycle_era) : M? unit :=
      let '{|
        cycle_era.first_level := first_level;
          cycle_era.first_cycle := first_cycle
          |} := era in
      match older_eras with
      |
        cons
          ({|
            cycle_era.first_level := first_level_of_previous_era;
              cycle_era.first_cycle := first_cycle_of_previous_era
              |} as previous_era) even_older_eras
        if
          (Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
          (Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
        then
          aux previous_era even_older_eras
        else
          Error_monad.error_value
            (Build_extensible "Invalid_cycle_eras" unit tt)
      | []return? tt
      end in
    let? '_ := aux newest_era older_eras in
    return? cycle_eras
  end.

Definition cycle_era_encoding : Data_encoding.encoding cycle_era :=
  Data_encoding.conv
    (fun (function_parameter : cycle_era) ⇒
      let '{|
        cycle_era.first_level := first_level;
          cycle_era.first_cycle := first_cycle;
          cycle_era.blocks_per_cycle := blocks_per_cycle;
          cycle_era.blocks_per_commitment := blocks_per_commitment
          |} := function_parameter in
      (first_level, first_cycle, blocks_per_cycle, blocks_per_commitment))
    (fun (function_parameter : Raw_level_repr.t × Cycle_repr.t × int32 × int32)
      ⇒
      let
        '(first_level, first_cycle, blocks_per_cycle, blocks_per_commitment) :=
        function_parameter in
      {| cycle_era.first_level := first_level;
        cycle_era.first_cycle := first_cycle;
        cycle_era.blocks_per_cycle := blocks_per_cycle;
        cycle_era.blocks_per_commitment := blocks_per_commitment; |}) None
    (Data_encoding.obj4
      (Data_encoding.req None (Some "The first level of a new cycle era.")
        "first_level" Raw_level_repr.encoding)
      (Data_encoding.req None (Some "The first cycle of a new cycle era.")
        "first_cycle" Cycle_repr.encoding)
      (Data_encoding.req None
        (Some
          "The value of the blocks_per_cycle constant used during the cycle era starting with first_level.")
        "blocks_per_cycle" Data_encoding.int32_value)
      (Data_encoding.req None
        (Some
          "The value of the blocks_per_commitment constant used during the cycle era starting with first_level.")
        "blocks_per_commitment" Data_encoding.int32_value)).

Definition cycle_eras_encoding : Data_encoding.encoding (list cycle_era) :=
  Data_encoding.conv_with_guard (fun (eras : list cycle_era) ⇒ eras)
    (fun (eras : list cycle_era) ⇒
      match create_cycle_eras eras with
      | Pervasives.Ok erasPervasives.Ok eras
      | Pervasives.Error _Pervasives.Error "Invalid cycle eras"
      end) None (Data_encoding.list_value None cycle_era_encoding).

Definition current_era {A : Set} (function_parameter : list A) : A :=
  match function_parameter with
  | []
    (* ❌ Assert instruction is not handled. *)
    assert _ false
  | cons cycle_era _cycle_era
  end.

Definition root_level (cycle_eras : list cycle_era) : t :=
  let first_era := List.last_opt cycle_eras in
  let first_era :=
    match first_era with
    | Some first_erafirst_era
    | None
      (* ❌ Assert instruction is not handled. *)
      assert cycle_era false
    end in
  {| t.level := first_era.(cycle_era.first_level); t.level_position := 0;
    t.cycle := Cycle_repr.root_value; t.cycle_position := 0;
    t.expected_commitment := false; |}.

Definition era_of_level
  (cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level)
  : cycle_era :=
  let fix aux (function_parameter : list cycle_era) : cycle_era :=
    match function_parameter with
    | cons ({| cycle_era.first_level := first_level |} as era) previous_eras
      if Raw_level_repr.op_gteq level first_level then
        era
      else
        aux previous_eras
    | []
      (* ❌ Assert instruction is not handled. *)
      assert cycle_era false
    end in
  aux cycle_eras.

Definition era_of_cycle (cycle_eras : list cycle_era) (cycle : Cycle_repr.t)
  : cycle_era :=
  let fix aux (function_parameter : list cycle_era) : cycle_era :=
    match function_parameter with
    | cons ({| cycle_era.first_cycle := first_cycle |} as era) previous_eras
      if Cycle_repr.op_gteq cycle first_cycle then
        era
      else
        aux previous_eras
    | []
      (* ❌ Assert instruction is not handled. *)
      assert cycle_era false
    end in
  aux cycle_eras.

Definition level_from_raw_with_era
  (era : cycle_era) (first_level_in_alpha_family : Raw_level_repr.raw_level)
  (level : Raw_level_repr.raw_level) : t :=
  let '{|
    cycle_era.first_level := first_level;
      cycle_era.first_cycle := first_cycle;
      cycle_era.blocks_per_cycle := blocks_per_cycle;
      cycle_era.blocks_per_commitment := blocks_per_commitment
      |} := era in
  let level_position_in_era := Raw_level_repr.diff_value level first_level in
  let '_ :=
    (* ❌ Assert instruction is not handled. *)
    assert unit (level_position_in_era i32 0) in
  let cycles_since_era_start := level_position_in_era /i32 blocks_per_cycle in
  let cycle := Cycle_repr.add first_cycle (Int32.to_int cycles_since_era_start)
    in
  let cycle_position := Int32.rem level_position_in_era blocks_per_cycle in
  let level_position :=
    Raw_level_repr.diff_value level first_level_in_alpha_family in
  let expected_commitment :=
    (Int32.rem cycle_position blocks_per_commitment) =i32
    (Int32.pred blocks_per_commitment) in
  {| t.level := level; t.level_position := level_position; t.cycle := cycle;
    t.cycle_position := cycle_position;
    t.expected_commitment := expected_commitment; |}.

Definition level_from_raw_aux_exn
  (cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level) : t :=
  let first_level_in_alpha_family :=
    match List.rev cycle_eras with
    | []
      (* ❌ Assert instruction is not handled. *)
      assert Raw_level_repr.t false
    | cons {| cycle_era.first_level := first_level |} _first_level
    end in
  let era := era_of_level cycle_eras level in
  level_from_raw_with_era era first_level_in_alpha_family level.

Definition level_from_raw
  (cycle_eras : list cycle_era) (l_value : Raw_level_repr.raw_level) : t :=
  level_from_raw_aux_exn cycle_eras l_value.

Init function; without side-effects in Coq
Definition init_module2 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent "level_not_in_alpha"
    "Level not in Alpha family" "Level not in Alpha family"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (level : Raw_level_repr.raw_level) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Level "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    " is not in the Alpha family of protocols."
                    CamlinternalFormatBasics.End_of_format)))
              "Level %a is not in the Alpha family of protocols.")
            Raw_level_repr.pp level))
    (Data_encoding.obj1
      (Data_encoding.req None None "level" Raw_level_repr.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Level_not_in_alpha" then
          let level := cast Raw_level_repr.t payload in
          Some level
        else None
      end)
    (fun (level : Raw_level_repr.raw_level) ⇒
      Build_extensible "Level_not_in_alpha" Raw_level_repr.raw_level level).

Definition level_from_raw_aux
  (cycle_eras : list cycle_era) (level : Raw_level_repr.raw_level) : M? t :=
  let first_level_in_alpha_family :=
    match List.rev cycle_eras with
    | []
      (* ❌ Assert instruction is not handled. *)
      assert Raw_level_repr.t false
    | cons {| cycle_era.first_level := first_level |} _first_level
    end in
  let? '_ :=
    Error_monad.error_when
      (Raw_level_repr.op_lt level first_level_in_alpha_family)
      (Build_extensible "Level_not_in_alpha" Raw_level_repr.raw_level level) in
  let era := era_of_level cycle_eras level in
  return? (level_from_raw_with_era era first_level_in_alpha_family level).

Init function; without side-effects in Coq
Definition init_module3 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "negative_level_and_offset_sum" "Negative sum of level and offset"
    "Negative sum of level and offset"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : int32 × int32) ⇒
          let '(level, offset) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Sum of level ("
                (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  (CamlinternalFormatBasics.String_literal ") and offset ("
                    (CamlinternalFormatBasics.Int32
                      CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.String_literal ") is negative."
                        CamlinternalFormatBasics.End_of_format)))))
              "Sum of level (%ld) and offset (%ld) is negative.") level offset))
    (Data_encoding.obj2
      (Data_encoding.req None None "level" Data_encoding.int32_value)
      (Data_encoding.req None None "offset" Data_encoding.int32_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Negative_level_and_offset_sum" then
          let '(level, offset) := cast (int32 × int32) payload in
          Some (level, offset)
        else None
      end)
    (fun (function_parameter : int32 × int32) ⇒
      let '(level, offset) := function_parameter in
      Build_extensible "Negative_level_and_offset_sum" (int32 × int32)
        (level, offset)).

Definition level_from_raw_with_offset
  (cycle_eras : list cycle_era) (offset : int32)
  (raw_level : Raw_level_repr.raw_level) : M? t :=
  let res :=
    Raw_level_repr.of_int32 ((Raw_level_repr.to_int32 raw_level) +i32 offset) in
  match res with
  | Pervasives.Ok levellevel_from_raw_aux cycle_eras level
  | Pervasives.Error _
    Error_monad.error_value
      (Build_extensible "Negative_level_and_offset_sum" (int32 × int32)
        ((Raw_level_repr.to_int32 raw_level), offset))
  end.

Definition first_level_in_cycle_from_eras
  (cycle_eras : list cycle_era) (cycle : Cycle_repr.t) : t :=
  let first_level_in_alpha_family :=
    match List.rev cycle_eras with
    | []
      (* ❌ Assert instruction is not handled. *)
      assert Raw_level_repr.t false
    | cons {| cycle_era.first_level := first_level |} _first_level
    end in
  let era := era_of_cycle cycle_eras cycle in
  let cycle_position := Cycle_repr.diff_value cycle era.(cycle_era.first_cycle)
    in
  let offset := era.(cycle_era.blocks_per_cycle) ×i32 cycle_position in
  let first_level_in_cycle :=
    Raw_level_repr.of_int32_exn
      ((Raw_level_repr.to_int32 era.(cycle_era.first_level)) +i32 offset) in
  level_from_raw_with_era era first_level_in_alpha_family first_level_in_cycle.

Definition last_of_cycle (cycle_eras : list cycle_era) (level : t) : bool :=
  let era := era_of_level cycle_eras level.(t.level) in
  (Int32.succ level.(t.cycle_position)) =i32 era.(cycle_era.blocks_per_cycle).