Skip to main content

👥 Delegate_sampler.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.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.

Module Delegate_sampler_state.
  Module Cache_client.
    Definition cached_value : Set := Sampler.t Delegate_consensus_key.pk.

    Definition namespace_value : Cache_repr.namespace :=
      Cache_repr.create_namespace "sampler_state".

    Definition cache_index : int := 2.

    Definition value_of_identifier (ctxt : Raw_context.t) (identifier : string)
      : M?
        Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value) :=
      let cycle := Cycle_repr.of_string_exn identifier in
      Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.get)
        ctxt cycle.

    (* Cache_client *)
    Definition module :=
      {|
        Cache_repr.CLIENT.namespace_value := namespace_value;
        Cache_repr.CLIENT.cache_index := cache_index;
        Cache_repr.CLIENT.value_of_identifier := value_of_identifier
      |}.
  End Cache_client.
  Definition Cache_client := Cache_client.module.

  Axiom Cache : Cache_repr.INTERFACE (cached_value := Cache_client.cached_value).

  Definition identifier_of_cycle (cycle : Cycle_repr.cycle) : string :=
    Format.asprintf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
        "%a") Cycle_repr.pp cycle.

  Definition init_value
    (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
    (sampler_state :
      Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value))
    : M? Raw_context.t :=
    let id := identifier_of_cycle cycle in
    let? ctxt :=
      Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.init_value)
        ctxt cycle sampler_state in
    let size_value := 1 in
    let? ctxt :=
      Cache.(Cache_repr.INTERFACE.update) ctxt id
        (Some (sampler_state, size_value)) in
    return? ctxt.

  Definition get (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
    : M?
      Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value) :=
    let id := identifier_of_cycle cycle in
    let? function_parameter := Cache.(Cache_repr.INTERFACE.find) ctxt id in
    match function_parameter with
    | None
      Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.get)
        ctxt cycle
    | Some v_valuereturn? v_value
    end.

  Definition remove_existing (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
    : M? Raw_context.t :=
    let id := identifier_of_cycle cycle in
    let? ctxt := Cache.(Cache_repr.INTERFACE.update) ctxt id None in
    Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.remove_existing)
      ctxt cycle.
End Delegate_sampler_state.

Module Random.
  Definition init_random_state
    (seed_value : Seed_repr.seed) (level : Level_repr.t) (index_value : int)
    : bytes × int :=
    ((Raw_hashes.blake2b
      (Data_encoding.Binary.to_bytes_exn None
        (Data_encoding.tup3 Seed_repr.seed_encoding Data_encoding.int32_value
          Data_encoding.int32_value)
        (seed_value, level.(Level_repr.t.cycle_position),
          (Int32.of_int index_value)))), 0).

  #[bypass_check(guard)]
  Definition take_int64 (bound : int64) (state_value : bytes × int)
    : int64 × (bytes × int) :=
    let drop_if_over := Int64.max_int -i64 (Int64.rem Int64.max_int bound) in
    let fix loop (function_parameter : bytes × int) {struct function_parameter}
      : int64 × (bytes × int) :=
      let '(bytes_value, n_value) := function_parameter in
      let consumed_bytes := 8 in
      let state_size := Bytes.length bytes_value in
      if n_value >i (state_size -i consumed_bytes) then
        loop ((Raw_hashes.blake2b bytes_value), 0)
      else
        let r_value := TzEndian.get_int64 bytes_value n_value 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 (bytes_value, (n_value +i consumed_bytes))
        else
          let v_value := Int64.rem r_value bound in
          (v_value, (bytes_value, (n_value +i consumed_bytes))) in
    loop state_value.

[sampler_for_cycle ctxt cycle] reads the sampler for [cycle] from [ctxt] if it has been previously inited. Otherwise it initializes the sampler and caches it in [ctxt] with [Raw_context.set_sampler_for_cycle].
  Definition sampler_for_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
    : M? (Raw_context.t × Seed_repr.seed × Sampler.t Raw_context.consensus_pk) :=
    let read (ctxt : Raw_context.t)
      : M?
        (Seed_repr.seed ×
          Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value)) :=
      let? seed_value := Seed_storage.for_cycle ctxt cycle in
      let? state_value := Delegate_sampler_state.get ctxt cycle in
      return? (seed_value, state_value) in
    Raw_context.sampler_for_cycle read ctxt cycle.

  Definition owner
    (c_value : Raw_context.t) (level : Level_repr.t) (offset : int)
    : M? (Raw_context.t × Raw_context.consensus_pk) :=
    let cycle := level.(Level_repr.t.cycle) in
    let? '(c_value, seed_value, state_value) := sampler_for_cycle c_value cycle
      in
    let sample (int_bound : int) (mass_bound : int64) : int × int64 :=
      let state_value := init_random_state seed_value level offset in
      let '(i_value, state_value) :=
        take_int64 (Int64.of_int int_bound) state_value in
      let '(elt_value, _) := take_int64 mass_bound state_value in
      ((Int64.to_int i_value), elt_value) in
    let? pk := Sampler.sample state_value sample in
    return? (c_value, pk).
End Random.

Definition slot_owner
  (c_value : Raw_context.t) (level : Level_repr.t) (slot : Slot_repr.t)
  : M? (Raw_context.t × Raw_context.consensus_pk) :=
  Random.owner c_value level (Slot_repr.to_int slot).

Definition baking_rights_owner
  (c_value : Raw_context.t) (level : Level_repr.t) (round : Round_repr.t)
  : M? (Raw_context.t × Slot_repr.t × Raw_context.consensus_pk) :=
  let? round := Round_repr.to_int round in
  let consensus_committee_size :=
    Constants_storage.consensus_committee_size c_value in
  let? slot := Slot_repr.of_int (Pervasives._mod round consensus_committee_size)
    in
  let? '(ctxt, pk) := slot_owner c_value level slot in
  return? (ctxt, slot, pk).

Definition get_stakes_for_selected_index
  (ctxt : Raw_context.t) (index_value : int)
  : M? (list (Signature.public_key_hash × Tez_repr.t) × Tez_repr.t) :=
  Stake_storage.fold_snapshot ctxt index_value
    (fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
      let '(delegate, staking_balance) := function_parameter in
      fun (function_parameter :
        list (Signature.public_key_hash × Tez_repr.t) × Tez_repr.t) ⇒
        let '(acc_value, total_stake) := function_parameter in
        let delegate_contract := Contract_repr.Implicit delegate in
        let? frozen_deposits_limit :=
          Delegate_storage.frozen_deposits_limit ctxt delegate in
        let? balance_and_frozen_bonds :=
          Contract_storage.get_balance_and_frozen_bonds ctxt delegate_contract
          in
        let? frozen_deposits :=
          Frozen_deposits_storage.get ctxt delegate_contract in
        let? total_balance :=
          Tez_repr.op_plusquestion balance_and_frozen_bonds
            frozen_deposits.(Storage.deposits.current_amount) in
        let? stake_for_cycle :=
          let frozen_deposits_percentage :=
            Int64.of_int (Constants_storage.frozen_deposits_percentage ctxt) in
          let max_mutez := Tez_repr.of_mutez_exn Int64.max_int in
          let frozen_deposits_limit :=
            match frozen_deposits_limit with
            | Some fdpfdp
            | Nonemax_mutez
            end in
          let aux := Tez_repr.min total_balance frozen_deposits_limit in
          let? overflow_bound := Tez_repr.op_divquestion max_mutez 100 in
          if Tez_repr.op_lteq aux overflow_bound then
            let? aux := Tez_repr.op_starquestion aux 100 in
            let? v_value :=
              Tez_repr.op_divquestion aux frozen_deposits_percentage in
            return? (Tez_repr.min v_value staking_balance)
          else
            let? sbal := Tez_repr.op_divquestion staking_balance 100 in
            let? a_value :=
              Tez_repr.op_divquestion aux frozen_deposits_percentage in
            if Tez_repr.op_lteq sbal a_value then
              return? staking_balance
            else
              let? r_value :=
                Tez_repr.op_divquestion max_mutez frozen_deposits_percentage in
              return? r_value in
        let? total_stake := Tez_repr.op_plusquestion total_stake stake_for_cycle
          in
        return? ((cons (delegate, stake_for_cycle) acc_value), total_stake))
    (nil, Tez_repr.zero).

Definition compute_snapshot_index_for_seed {A : Set}
  (max_snapshot_index : int) (seed_value : Seed_repr.seed)
  : Pervasives.result int A :=
  let rd :=
    Seed_repr.initialize_new seed_value [ Bytes.of_string "stake_snapshot" ] in
  let seq := Seed_repr.sequence_value rd 0 in
  return?
    (Int32.to_int
      (Pervasives.fst
        (Seed_repr.take_int32 seq (Int32.of_int max_snapshot_index)))).

Definition compute_snapshot_index
  (ctxt : Raw_context.t) (cycle : Cycle_repr.t) (max_snapshot_index : int)
  : M? int :=
  let? seed_value := Seed_storage.for_cycle ctxt cycle in
  compute_snapshot_index_for_seed max_snapshot_index seed_value.

Definition select_distribution_for_cycle
  (ctxt : Raw_context.t) (cycle : Cycle_repr.t) : M? Raw_context.t :=
  let? max_snapshot_index := Stake_storage.max_snapshot_index ctxt in
  let? seed_value := Seed_storage.raw_for_cycle ctxt cycle in
  let? selected_index :=
    compute_snapshot_index_for_seed max_snapshot_index seed_value in
  let? '(stakes, total_stake) :=
    get_stakes_for_selected_index ctxt selected_index in
  let? ctxt :=
    Stake_storage.set_selected_distribution_for_cycle ctxt cycle stakes
      total_stake in
  let? stakes_pk :=
    List.fold_left_es
      (fun (acc_value : list (Delegate_consensus_key.pk × Sampler.mass)) ⇒
        fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
          let '(pkh, stake) := function_parameter in
          let? pk :=
            Delegate_consensus_key.active_pubkey_for_cycle ctxt pkh cycle in
          return? (cons (pk, (Tez_repr.to_mutez stake)) acc_value)) nil stakes
    in
  let state_value := Sampler.create stakes_pk in
  let? ctxt := Delegate_sampler_state.init_value ctxt cycle state_value in
  Raw_context.init_sampler_for_cycle ctxt cycle seed_value state_value.

Definition select_new_distribution_at_cycle_end
  (ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : M? Raw_context.t :=
  let preserved := Constants_storage.preserved_cycles ctxt in
  let? for_cycle := Cycle_repr.add new_cycle preserved in
  select_distribution_for_cycle ctxt for_cycle.

Definition clear_outdated_sampling_data
  (ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : M? Raw_context.t :=
  let max_slashing_period := Constants_storage.max_slashing_period ctxt in
  let? res := Cycle_repr.sub new_cycle max_slashing_period in
  match res with
  | Nonereturn? ctxt
  | Some outdated_cycle
    let? ctxt := Delegate_sampler_state.remove_existing ctxt outdated_cycle in
    Seed_storage.remove_for_cycle ctxt outdated_cycle
  end.

Module Migration_from_Kathmandu.
  Definition update_sampler (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
    : M? Raw_context.t :=
    let? stakes := Stake_storage.get_selected_distribution ctxt cycle in
    let? stakes_pk :=
      List.fold_left_es
        (fun (acc_value : list (Delegate_consensus_key.pk × Sampler.mass)) ⇒
          fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
            let '(delegate, stake) := function_parameter in
            let? pk := Delegate_consensus_key.active_pubkey ctxt delegate in
            return? (cons (pk, (Tez_repr.to_mutez stake)) acc_value)) nil stakes
      in
    let state_value := Sampler.create stakes_pk in
    let? ctxt := Delegate_sampler_state.init_value ctxt cycle state_value in
    let? seed_value := Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) ctxt cycle
      in
    Raw_context.init_sampler_for_cycle ctxt cycle seed_value state_value.
End Migration_from_Kathmandu.