🪜 Level_storage.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_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.

Definition from_raw (c_value : Raw_context.t) (l_value : Raw_level_repr.t)
  : Level_repr.level :=
  let cycle_eras := Raw_context.cycle_eras c_value in
  Level_repr.level_from_raw cycle_eras l_value.

Definition from_raw_with_offset
  (c_value : Raw_context.t) (offset : int32) (l_value : Raw_level_repr.t)
  : M? Level_repr.t :=
  let cycle_eras := Raw_context.cycle_eras c_value in
  Level_repr.level_from_raw_with_offset cycle_eras offset l_value.

Definition root_value (c_value : Raw_context.t) : Level_repr.level :=
  Level_repr.root_level (Raw_context.cycle_eras c_value).

Definition succ (c_value : Raw_context.t) (l_value : Level_repr.t)
  : Level_repr.level :=
  from_raw c_value (Raw_level_repr.succ l_value.(Level_repr.t.level)).

Definition pred (c_value : Raw_context.t) (l_value : Level_repr.t)
  : option Level_repr.level :=
  match Raw_level_repr.pred l_value.(Level_repr.t.level) with
  | None ⇒ None
  | Some l_value ⇒ Some (from_raw c_value l_value)
  end.

Definition add
  (c_value : Raw_context.t) (l_value : Level_repr.t) (n_value : int)
  : Level_repr.level :=
  from_raw c_value (Raw_level_repr.add l_value.(Level_repr.t.level) n_value).

Definition sub
  (c_value : Raw_context.t) (l_value : Level_repr.t) (n_value : int)
  : option Level_repr.level :=
  match Raw_level_repr.sub l_value.(Level_repr.t.level) n_value with
  | None ⇒ None
  | Some raw_level ⇒
    let cycle_eras := Raw_context.cycle_eras c_value in
    let root_level := Level_repr.root_level cycle_eras in
    if Raw_level_repr.op_gteq raw_level root_level.(Level_repr.t.level) then
      Some (from_raw c_value raw_level)
    else
      None
  end.

Definition current (ctxt : Raw_context.t) : Level_repr.t :=
  Raw_context.current_level ctxt.

Definition previous (ctxt : Raw_context.t) : Level_repr.level :=
  let l_value := current ctxt in
  match pred ctxt l_value with
  | None ⇒
    (* ❌ Assert instruction is not handled. *)
    assert Level_repr.level false
  | Some p_value ⇒ p_value
  end.

Definition first_level_in_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
  : Level_repr.level :=
  let cycle_eras := Raw_context.cycle_eras ctxt in
  Level_repr.first_level_in_cycle_from_eras cycle_eras cycle.

Definition last_level_in_cycle
  (ctxt : Raw_context.t) (c_value : Cycle_repr.cycle) : Level_repr.level :=
  match pred ctxt (first_level_in_cycle ctxt (Cycle_repr.succ c_value)) with
  | None ⇒
    (* ❌ Assert instruction is not handled. *)
    assert Level_repr.level false
  | Some x_value ⇒ x_value
  end.

#[bypass_check(guard)]
Definition levels_in_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
  : list Level_repr.t :=
  let first := first_level_in_cycle ctxt cycle in
  let fix loop (n_value : Level_repr.t) (acc_value : list Level_repr.t)
    {struct n_value} : list Level_repr.t :=
    if
      Cycle_repr.op_eq n_value.(Level_repr.t.cycle) first.(Level_repr.t.cycle)
    then
      loop (succ ctxt n_value) (cons n_value acc_value)
    else
      acc_value in
  loop first nil.

Definition levels_in_current_cycle
  (ctxt : Raw_context.t) (op_staroptstar : option int32)
  : unit → list Level_repr.t :=
  let offset :=
    match op_staroptstar with
    | Some op_starsthstar ⇒ op_starsthstar
    | None ⇒ 0
    end in
  fun (function_parameter : unit) ⇒
    let '_ := function_parameter in
    let current_cycle := Cycle_repr.to_int32 (current ctxt).(Level_repr.t.cycle)
      in
    let cycle := current_cycle +i32 offset in
    if cycle <i32 0 then
      nil
    else
      let cycle := Cycle_repr.of_int32_exn cycle in
      levels_in_cycle ctxt cycle.

#[bypass_check(guard)]
Definition levels_with_commitments_in_cycle
  (ctxt : Raw_context.t) (c_value : Cycle_repr.t) : list Level_repr.t :=
  let first := first_level_in_cycle ctxt c_value in
  let fix loop (n_value : Level_repr.t) (acc_value : list Level_repr.t)
    {struct n_value} : list Level_repr.t :=
    if
      Cycle_repr.op_eq n_value.(Level_repr.t.cycle) first.(Level_repr.t.cycle)
    then
      if n_value.(Level_repr.t.expected_commitment) then
        loop (succ ctxt n_value) (cons n_value acc_value)
      else
        loop (succ ctxt n_value) acc_value
    else
      acc_value in
  loop first nil.

Definition last_allowed_fork_level (c_value : Raw_context.t)
  : Raw_level_repr.raw_level :=
  let level := Raw_context.current_level c_value in
  let preserved_cycles := Constants_storage.preserved_cycles c_value in
  match Cycle_repr.sub level.(Level_repr.t.cycle) preserved_cycles with
  | None ⇒ Raw_level_repr.root_value
  | Some cycle ⇒ (first_level_in_cycle c_value cycle).(Level_repr.t.level)
  end.

Definition last_of_a_cycle (ctxt : Raw_context.t) (level : Level_repr.level)
  : bool :=
  let cycle_eras := Raw_context.cycle_eras ctxt in
  Level_repr.last_of_cycle cycle_eras level.

Definition dawn_of_a_new_cycle (ctxt : Raw_context.t) : option Cycle_repr.t :=
  let level := current ctxt in
  if last_of_a_cycle ctxt level then
    Some level.(Level_repr.t.cycle)
  else
    None.

Definition may_snapshot_rolls (ctxt : Raw_context.t) : bool :=
  let level := current ctxt in
  let blocks_per_stake_snapshot :=
    Constants_storage.blocks_per_stake_snapshot ctxt in
  Compare.Int32.(Compare.S.equal)
    (Int32.rem level.(Level_repr.t.cycle_position) blocks_per_stake_snapshot)
    (Int32.pred blocks_per_stake_snapshot).