🪜 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.Environment.V8.
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)
  : M? 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) : M? 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)
  : M? 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)
  : M? (option Level_repr.level) :=
  match Raw_level_repr.pred l_value.(Level_repr.t.level) with
  | None ⇒ Error_monad.Result_syntax.return_none
  | Some l_value ⇒
    let? x_value := from_raw c_value l_value in
    Error_monad.Result_syntax.return_some x_value
  end.

Definition add
  (c_value : Raw_context.t) (l_value : Level_repr.t) (n_value : int)
  : M? Level_repr.level :=
  let? res := Raw_level_repr.add l_value.(Level_repr.t.level) n_value in
  from_raw c_value res.

Definition sub
  (c_value : Raw_context.t) (l_value : Level_repr.t) (n_value : int)
  : M? (option Level_repr.level) :=
  let? res := Raw_level_repr.sub l_value.(Level_repr.t.level) n_value in
  match res with
  | None ⇒ return? 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
      let? fr := from_raw c_value raw_level in
      Error_monad.Result_syntax.return_some fr
    else
      Error_monad.Result_syntax.return_none
  end.

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

Definition previous (ctxt : Raw_context.t) : M? Level_repr.level :=
  let l_value := current ctxt in
  let? p_value := pred ctxt l_value in
  match p_value with
  | None ⇒
    Error_monad.Result_syntax.tzfail (Build_extensible "Asserted" unit tt)
  | Some p_value ⇒ return? p_value
  end.

Definition first_level_in_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
  : M? 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) : M? Level_repr.level :=
  let? level := first_level_in_cycle ctxt (Cycle_repr.succ c_value) in
  let? p_value := pred ctxt level in
  match p_value with
  | None ⇒
    Error_monad.Result_syntax.tzfail (Build_extensible "Asserted" unit tt)
  | Some x_value ⇒ return? x_value
  end.

#[bypass_check(guard)]
Definition levels_in_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
  : M? (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} : M? (list Level_repr.t) :=
    let? sn := succ ctxt n_value in
    if
      Cycle_repr.op_eq n_value.(Level_repr.t.cycle) first.(Level_repr.t.cycle)
    then
      loop sn (cons n_value acc_value)
    else
      return? acc_value in
  loop first nil.

Definition levels_in_current_cycle
  (ctxt : Raw_context.t) (op_staroptstar : option int32)
  : unit → M? (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
      return? 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) : M? (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} : M? (list Level_repr.t) :=
    if
      Cycle_repr.op_eq n_value.(Level_repr.t.cycle) first.(Level_repr.t.cycle)
    then
      let? sn := succ ctxt n_value in
      if n_value.(Level_repr.t.expected_commitment) then
        loop sn (cons n_value acc_value)
      else
        loop sn acc_value
    else
      return? acc_value in
  loop first nil.

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

Definition last_of_a_cycle (ctxt : Raw_context.t) (level : Level_repr.level)
  : M? 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)
  : M? (option Cycle_repr.t) :=
  let level := current ctxt in
  let? loac := last_of_a_cycle ctxt level in
  if loac then
    return? (Some level.(Level_repr.t.cycle))
  else
    return? None.

Definition may_snapshot_stake_distribution (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).

Definition may_compute_randao (ctxt : Raw_context.t) : bool :=
  let level := current ctxt in
  let nonce_reveal_cutoff := Constants_storage.nonce_revelation_threshold ctxt
    in
  Compare.Int32.(Compare.S.equal) level.(Level_repr.t.cycle_position)
    nonce_reveal_cutoff.