Skip to main content

👥 Delegate_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.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_delegate_storage.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Misc.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
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.
Require TezosOfOCaml.Proto_alpha.Token.

Module Cannot_find_active_stake.
  Record record : Set := Build {
    cycle : Cycle_repr.t;
    delegate : Signature.public_key_hash;
  }.
  Definition with_cycle cycle (r : record) :=
    Build cycle r.(delegate).
  Definition with_delegate delegate (r : record) :=
    Build r.(cycle) delegate.
End Cannot_find_active_stake.
Definition Cannot_find_active_stake := Cannot_find_active_stake.record.

Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "delegate.no_deletion"
      "Forbidden delegate deletion" "Tried to unregister a delegate"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (delegate : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Delegate deletion is forbidden ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format)))
                "Delegate deletion is forbidden (%a)")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
              delegate))
      (Data_encoding.obj1
        (Data_encoding.req None None "delegate"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "No_deletion" then
            let c_value := cast Signature.public_key_hash payload in
            Some c_value
          else None
        end)
      (fun (c_value : Signature.public_key_hash) ⇒
        Build_extensible "No_deletion" Signature.public_key_hash c_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "delegate.already_active" "Delegate already active"
      "Useless delegate reactivation"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The delegate is still active, no need to refresh it"
                  CamlinternalFormatBasics.End_of_format)
                "The delegate is still active, no need to refresh it")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Active_delegate" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Active_delegate" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "delegate.unchanged"
      "Unchanged delegated" "Contract already delegated to the given delegate"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The contract is already delegated to the same delegate"
                  CamlinternalFormatBasics.End_of_format)
                "The contract is already delegated to the same delegate")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Current_delegate" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Current_delegate" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "delegate.empty_delegate_account" "Empty delegate account"
      "Cannot register a delegate when its implicit account is empty"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (delegate : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Delegate registration is forbidden when the delegate\n implicit account is empty ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format)))
                "Delegate registration is forbidden when the delegate\n implicit account is empty (%a)")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
              delegate))
      (Data_encoding.obj1
        (Data_encoding.req None None "delegate"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Empty_delegate_account" then
            let c_value := cast Signature.public_key_hash payload in
            Some c_value
          else None
        end)
      (fun (c_value : Signature.public_key_hash) ⇒
        Build_extensible "Empty_delegate_account" Signature.public_key_hash
          c_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "contract.manager.unregistered_delegate" "Unregistered delegate"
      "A contract cannot be delegated to an unregistered delegate"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (k_value : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The provided public key (with hash "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      ") is not registered as valid delegate key."
                      CamlinternalFormatBasics.End_of_format)))
                "The provided public key (with hash %a) is not registered as valid delegate key.")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) k_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "hash"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unregistered_delegate" then
            let k_value := cast Signature.public_key_hash payload in
            Some k_value
          else None
        end)
      (fun (k_value : Signature.public_key_hash) ⇒
        Build_extensible "Unregistered_delegate" Signature.public_key_hash
          k_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "delegate.unassigned_validation_slot_for_level"
      "Unassigned validation slot for level"
      "The validation slot for the given level is not assigned. Nobody payed for that slot, or the level is either in the past or too far in the future (further than the validatiors_selection_offset constant)"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Level_repr.level × int) ⇒
            let '(l_value, slot) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "The validation slot "
                  (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.String_literal " for the level "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal
                          " is not assigned. Nobody payed for that slot, or the level is either in the past or too far in the future (further than the validatiors_selection_offset constant)"
                          CamlinternalFormatBasics.End_of_format)))))
                "The validation slot %i for the level %a is not assigned. Nobody payed for that slot, or the level is either in the past or too far in the future (further than the validatiors_selection_offset constant)")
              slot Level_repr.pp l_value))
      (Data_encoding.obj2
        (Data_encoding.req None None "level" Level_repr.encoding)
        (Data_encoding.req None None "slot" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unassigned_validation_slot_for_level" then
            let '(l_value, s_value) := cast (Level_repr.t × int) payload in
            Some (l_value, s_value)
          else None
        end)
      (fun (function_parameter : Level_repr.level × int) ⇒
        let '(l_value, s_value) := function_parameter in
        Build_extensible "Unassigned_validation_slot_for_level"
          (Level_repr.level × int) (l_value, s_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "delegate.cannot_find_active_stake" "Cannot find active stake"
      "The active stake of a delegate cannot be found for the given cycle."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Cycle_repr.cycle × Signature.public_key_hash) ⇒
            let '(cycle, delegate) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The active stake of the delegate "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " cannot be found for the cycle "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Char_literal "." % char
                          CamlinternalFormatBasics.End_of_format)))))
                "The active stake of the delegate %a cannot be found for the cycle %a.")
              Cycle_repr.pp cycle
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
              delegate))
      (Data_encoding.obj2
        (Data_encoding.req None None "cycle" Cycle_repr.encoding)
        (Data_encoding.req None None "delegate"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Cannot_find_active_stake" then
            let '{|
              Cannot_find_active_stake.cycle := cycle;
                Cannot_find_active_stake.delegate := delegate
                |} := cast Cannot_find_active_stake payload in
            Some (cycle, delegate)
          else None
        end)
      (fun (function_parameter : Cycle_repr.cycle × Signature.public_key_hash)
        ⇒
        let '(cycle, delegate) := function_parameter in
        Build_extensible "Cannot_find_active_stake" Cannot_find_active_stake
          {| Cannot_find_active_stake.cycle := cycle;
            Cannot_find_active_stake.delegate := delegate; |}) in
  Error_monad.register_error_kind Error_monad.Temporary
    "delegate.not_registered" "Not a registered delegate"
    "The provided public key hash is not the address of a registered delegate."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "The provided public key hash ("
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    ") is not the address of a registered delegate. If you own this account and want to register it as a delegate, use a delegation operation to delegate the account to itself."
                    CamlinternalFormatBasics.End_of_format)))
              "The provided public key hash (%a) is not the address of a registered delegate. If you own this account and want to register it as a delegate, use a delegation operation to delegate the account to itself.")
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
    (Data_encoding.obj1
      (Data_encoding.req None None "pkh"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Not_registered" then
          let pkh := cast Signature.public_key_hash payload in
          Some pkh
        else None
      end)
    (fun (pkh : Signature.public_key_hash) ⇒
      Build_extensible "Not_registered" Signature.public_key_hash pkh).

Definition set_inactive {A : Set}
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : Pervasives.result Raw_context.t A :=
  let ctxt := Delegate_activation_storage.set_inactive ctxt delegate in
  Error_monad.op_gtpipeeq
    (Stake_storage.deactivate_only_call_from_delegate_storage ctxt delegate)
    Error_monad.ok.

Definition set_active
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Raw_context.t :=
  let? '(ctxt, inactive) := Delegate_activation_storage.set_active ctxt delegate
    in
  if Pervasives.not inactive then
    return? ctxt
  else
    Stake_storage.activate_only_call_from_delegate_storage ctxt delegate.

Definition staking_balance
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Tez_repr.t :=
  let? is_registered := Contract_delegate_storage.registered ctxt delegate in
  if is_registered then
    Stake_storage.get_staking_balance ctxt delegate
  else
    return? Tez_repr.zero.

Definition pubkey (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Signature.public_key :=
  Contract_manager_storage.get_manager_key
    (Some
      (Build_extensible "Unregistered_delegate" Signature.public_key_hash
        delegate)) ctxt delegate.

Definition init_value
  (ctxt : Raw_context.t) (contract : Contract_repr.t)
  (delegate : Signature.public_key_hash) : M? Raw_context.t :=
  let? known_delegate :=
    Contract_manager_storage.is_manager_key_revealed ctxt delegate in
  let? '_ :=
    Error_monad.error_unless known_delegate
      (Build_extensible "Unregistered_delegate" Signature.public_key_hash
        delegate) in
  let? is_registered := Contract_delegate_storage.registered ctxt delegate in
  let? '_ :=
    Error_monad.error_unless is_registered
      (Build_extensible "Unregistered_delegate" Signature.public_key_hash
        delegate) in
  let? ctxt := Contract_delegate_storage.init_value ctxt contract delegate in
  let? balance_and_frozen_bonds :=
    Contract_storage.get_balance_and_frozen_bonds ctxt contract in
  Stake_storage.add_stake ctxt delegate balance_and_frozen_bonds.

Definition set
  (c_value : Raw_context.t) (contract : Contract_repr.contract)
  (delegate : option Signature.public_key_hash) : M? Raw_context.t :=
  match delegate with
  | None
    let? '_ :=
      match Contract_repr.is_implicit contract with
      | Some pkh
        let? is_registered := Contract_delegate_storage.registered c_value pkh
          in
        Error_monad.fail_when is_registered
          (Build_extensible "No_deletion" Signature.public_key_hash pkh)
      | NoneError_monad.return_unit
      end in
    let? function_parameter := Contract_delegate_storage.find c_value contract
      in
    match function_parameter with
    | Nonereturn? c_value
    | Some delegate
      let? balance_and_frozen_bonds :=
        Contract_storage.get_balance_and_frozen_bonds c_value contract in
      let? c_value :=
        Stake_storage.remove_stake c_value delegate balance_and_frozen_bonds in
      Contract_delegate_storage.delete c_value contract
    end
  | Some delegate
    let? known_delegate :=
      Contract_manager_storage.is_manager_key_revealed c_value delegate in
    let? registered_delegate :=
      Contract_delegate_storage.registered c_value delegate in
    let self_delegation :=
      match Contract_repr.is_implicit contract with
      | Some pkh
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) pkh
          delegate
      | Nonefalse
      end in
    if
      (Pervasives.not known_delegate) ||
      (Pervasives.not (registered_delegate || self_delegation))
    then
      Error_monad.fail
        (Build_extensible "Unregistered_delegate" Signature.public_key_hash
          delegate)
    else
      let? current_delegate := Contract_delegate_storage.find c_value contract
        in
      let? '_ :=
        match
          (current_delegate,
            match current_delegate with
            | Some current_delegate
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
                delegate current_delegate
            | _false
            end) with
        | (Some current_delegate, true)
          if self_delegation then
            let? function_parameter :=
              Delegate_activation_storage.is_inactive c_value delegate in
            match function_parameter with
            | trueError_monad.return_unit
            | false
              Error_monad.fail (Build_extensible "Active_delegate" unit tt)
            end
          else
            Error_monad.fail (Build_extensible "Current_delegate" unit tt)
        | ((None | Some _), _)Error_monad.return_unit
        end in
      let? '_ :=
        match Contract_repr.is_implicit contract with
        | Some pkh
          let? is_registered := Contract_delegate_storage.registered c_value pkh
            in
          if (Pervasives.not self_delegation) && is_registered then
            Error_monad.fail
              (Build_extensible "No_deletion" Signature.public_key_hash pkh)
          else
            Error_monad.return_unit
        | NoneError_monad.return_unit
        end in
      let _exists :=
        Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.mem)
          c_value contract in
      let? '_ :=
        Error_monad.error_when (self_delegation && (Pervasives.not _exists))
          (Build_extensible "Empty_delegate_account" Signature.public_key_hash
            delegate) in
      let? balance_and_frozen_bonds :=
        Contract_storage.get_balance_and_frozen_bonds c_value contract in
      let? c_value :=
        Stake_storage.remove_contract_stake c_value contract
          balance_and_frozen_bonds in
      let? c_value := Contract_delegate_storage.set c_value contract delegate in
      let? c_value :=
        Stake_storage.add_stake c_value delegate balance_and_frozen_bonds in
      if self_delegation then
        let c_value :=
          Storage.Delegates.(Storage_sigs.Data_set_storage.add) c_value delegate
          in
        set_active c_value delegate
      else
        return? c_value
  end.

Definition frozen_deposits_limit
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? (option Tez_repr.t) :=
  Storage.Contract.Frozen_deposits_limit.(Storage_sigs.Indexed_data_storage.find)
    ctxt (Contract_repr.implicit_contract delegate).

Definition set_frozen_deposits_limit
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (limit : option Tez_repr.t) : Raw_context.t :=
  Storage.Contract.Frozen_deposits_limit.(Storage_sigs.Indexed_data_storage.add_or_remove)
    ctxt (Contract_repr.implicit_contract delegate) limit.

Definition update_activity
  (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
  : M? (Raw_context.t × list Signature.public_key_hash) :=
  let preserved := Constants_storage.preserved_cycles ctxt in
  match Cycle_repr.sub last_cycle preserved with
  | Nonereturn? (ctxt, nil)
  | Some _unfrozen_cycle
    let? '(ctxt, deactivated) :=
      Stake_storage.fold_on_active_delegates_with_rolls ctxt
        (Variant.Build "Sorted" unit tt) (Pervasives.Ok (ctxt, nil))
        (fun (delegate : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (acc_value :
              M? (Raw_context.t × list Signature.public_key_hash)) ⇒
              let? '(ctxt, deactivated) := acc_value in
              let? cycle :=
                Delegate_activation_storage.last_cycle_before_deactivation ctxt
                  delegate in
              if Cycle_repr.op_lteq cycle last_cycle then
                let? ctxt := set_inactive ctxt delegate in
                return? (ctxt, (cons delegate deactivated))
              else
                return? (ctxt, deactivated)) in
    return? (ctxt, deactivated)
  end.

Definition expected_slots_for_given_active_stake {A : Set}
  (ctxt : Raw_context.t) (total_active_stake : Tez_repr.t)
  (active_stake : Tez_repr.t) : Pervasives.result int A :=
  let blocks_per_cycle := Int32.to_int (Constants_storage.blocks_per_cycle ctxt)
    in
  let consensus_committee_size :=
    Constants_storage.consensus_committee_size ctxt in
  let number_of_endorsements_per_cycle :=
    blocks_per_cycle ×i consensus_committee_size in
  Result._return
    (Z.to_int
      (((Z.of_int64 (Tez_repr.to_mutez active_stake)) ×Z
      (Z.of_int number_of_endorsements_per_cycle)) /Z
      (Z.of_int64 (Tez_repr.to_mutez total_active_stake)))).

Definition delegate_participated_enough
  (ctxt : Raw_context.t) (delegate : Contract_repr.t) : M? bool :=
  let? function_parameter :=
    Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
      ctxt delegate in
  match function_parameter with
  | NoneError_monad.return_true
  | Some missed_endorsements
    return?
      (missed_endorsements.(Storage.missed_endorsements_info.remaining_slots)
      i 0)
  end.

Definition delegate_has_revealed_nonces
  (delegate : Signature.public_key_hash)
  (unrevelead_nonces_set :
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
  : bool :=
  Pervasives.not
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.mem)
      delegate unrevelead_nonces_set).

Definition distribute_endorsing_rewards
  (ctxt : Raw_context.t) (last_cycle : Cycle_repr.t)
  (unrevealed_nonces : list Storage.Seed.unrevealed_nonce)
  : M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let endorsing_reward_per_slot :=
    Constants_storage.endorsing_reward_per_slot ctxt in
  let unrevealed_nonces_set :=
    List.fold_left
      (fun (set :
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
        ⇒
        fun (function_parameter : Storage.Seed.unrevealed_nonce) ⇒
          let '{|
            Storage.Cycle.unrevealed_nonce.nonce_hash := _;
              Storage.Cycle.unrevealed_nonce.delegate := delegate
              |} := function_parameter in
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.add)
            delegate set)
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
      unrevealed_nonces in
  let? total_active_stake :=
    Stake_storage.get_total_active_stake ctxt last_cycle in
  let? delegates := Stake_storage.get_selected_distribution ctxt last_cycle in
  List.fold_left_es
    (fun (function_parameter :
      Raw_context.t ×
        list
          (Receipt_repr.balance × Receipt_repr.balance_update ×
            Receipt_repr.update_origin)) ⇒
      let '(ctxt, balance_updates) := function_parameter in
      fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
        let '(delegate, active_stake) := function_parameter in
        let delegate_contract := Contract_repr.implicit_contract delegate in
        let? sufficient_participation :=
          delegate_participated_enough ctxt delegate_contract in
        let has_revealed_nonces :=
          delegate_has_revealed_nonces delegate unrevealed_nonces_set in
        let? expected_slots :=
          expected_slots_for_given_active_stake ctxt total_active_stake
            active_stake in
        let rewards := Tez_repr.mul_exn endorsing_reward_per_slot expected_slots
          in
        let? '(ctxt, balance_updates) :=
          if sufficient_participation && has_revealed_nonces then
            let? '(ctxt, payed_rewards_receipts) :=
              Token.transfer None ctxt
                (Token.Source_infinite Token.Endorsing_rewards)
                (Token.Sink_container (Token.Contract delegate_contract))
                rewards in
            return?
              (ctxt, (Pervasives.op_at payed_rewards_receipts balance_updates))
          else
            let? '(ctxt, payed_rewards_receipts) :=
              Token.transfer None ctxt
                (Token.Source_infinite Token.Endorsing_rewards)
                (Token.Sink_infinite
                  (Token.Lost_endorsing_rewards delegate
                    (Pervasives.not sufficient_participation)
                    (Pervasives.not has_revealed_nonces))) rewards in
            return?
              (ctxt, (Pervasives.op_at payed_rewards_receipts balance_updates))
          in
        let ctxt :=
          Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.remove)
            ctxt delegate_contract in
        return? (ctxt, balance_updates)) (ctxt, nil) delegates.

Definition clear_outdated_slashed_deposits
  (ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : Raw_context.t :=
  let max_slashable_period := Constants_storage.max_slashing_period ctxt in
  match Cycle_repr.sub new_cycle max_slashable_period with
  | Nonectxt
  | Some outdated_cycle
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.clear)
      (ctxt, outdated_cycle)
  end.

Definition max_frozen_deposits_and_delegates_to_remove
  (ctxt : Raw_context.t) (from_cycle : Cycle_repr.cycle)
  (to_cycle : Cycle_repr.cycle)
  : M?
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
      Tez_repr.t ×
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t)) :=
  let frozen_deposits_percentage :=
    Constants_storage.frozen_deposits_percentage ctxt in
  let cycles := Cycle_repr.op_minusminusminusgt from_cycle to_cycle in
  let? cleared_cycle_delegates :=
    match Cycle_repr.pred from_cycle with
    | None
      return?
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
    | Some cleared_cycle
      let? cleared_cycle_delegates :=
        Stake_storage.find_selected_distribution ctxt cleared_cycle in
      match cleared_cycle_delegates with
      | None
        return?
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
      | Some delegates
        return?
          (List.fold_left
            (fun (set :
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
              ⇒
              fun (function_parameter : Signature.public_key_hash × Tez_repr.t)
                ⇒
                let '(d_value, _) := function_parameter in
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.add)
                  d_value set)
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
            delegates)
      end
    end in
  List.fold_left_es
    (fun (function_parameter :
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
        Tez_repr.t ×
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
      ⇒
      let '(maxima, delegates_to_remove) := function_parameter in
      fun (cycle : Cycle_repr.t) ⇒
        let? active_stakes := Stake_storage.get_selected_distribution ctxt cycle
          in
        return?
          (List.fold_left
            (fun (function_parameter :
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
                Tez_repr.t ×
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
              ⇒
              let '(maxima, delegates_to_remove) := function_parameter in
              fun (function_parameter : Signature.public_key_hash × Tez_repr.t)
                ⇒
                let '(delegate, stake) := function_parameter in
                let stake_to_be_deposited :=
                  Tez_repr.div_exn
                    (Tez_repr.mul_exn stake frozen_deposits_percentage) 100 in
                let maxima :=
                  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.update)
                    delegate
                    (fun (function_parameter : option Tez_repr.t) ⇒
                      match function_parameter with
                      | NoneSome stake_to_be_deposited
                      | Some maximum
                        Some (Tez_repr.max maximum stake_to_be_deposited)
                      end) maxima in
                let delegates_to_remove :=
                  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.remove)
                    delegate delegates_to_remove in
                (maxima, delegates_to_remove)) (maxima, delegates_to_remove)
            active_stakes))
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty),
      cleared_cycle_delegates) cycles.

Definition freeze_deposits (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t Cycle_repr.cycle
  list
    (Receipt_repr.balance × Receipt_repr.balance_update ×
      Receipt_repr.update_origin)
  M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (ctxt : Raw_context.t) ⇒
    fun (new_cycle : Cycle_repr.cycle) ⇒
      fun (balance_updates :
        list
          (Receipt_repr.balance × Receipt_repr.balance_update ×
            Receipt_repr.update_origin)) ⇒
        let max_slashable_period := Constants_storage.max_slashing_period ctxt
          in
        let? from_cycle :=
          match Cycle_repr.sub new_cycle (max_slashable_period -i 1) with
          | None
            let? first_level_of_protocol :=
              Storage.Tenderbake.First_level_of_protocol.(Storage_sigs.Single_data_storage.get)
                ctxt in
            let cycle_eras := Raw_context.cycle_eras ctxt in
            let level :=
              Level_repr.level_from_raw cycle_eras first_level_of_protocol in
            return? level.(Level_repr.t.cycle)
          | Some cyclereturn? cycle
          end in
        let preserved_cycles := Constants_storage.preserved_cycles ctxt in
        let to_cycle := Cycle_repr.add new_cycle preserved_cycles in
        let? '(maxima, delegates_to_remove) :=
          max_frozen_deposits_and_delegates_to_remove ctxt from_cycle to_cycle
          in
        let? '(ctxt, balance_updates) :=
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.fold_es)
            (fun (delegate : Signature.public_key_hash) ⇒
              fun (maximum_stake_to_be_deposited : Tez_repr.t) ⇒
                fun (function_parameter :
                  Raw_context.t ×
                    list
                      (Receipt_repr.balance × Receipt_repr.balance_update ×
                        Receipt_repr.update_origin)) ⇒
                  let '(ctxt, balance_updates) := function_parameter in
                  let delegate_contract :=
                    Contract_repr.implicit_contract delegate in
                  let? ctxt :=
                    Frozen_deposits_storage.update_initial_amount ctxt
                      delegate_contract maximum_stake_to_be_deposited in
                  let? deposits :=
                    Frozen_deposits_storage.get ctxt delegate_contract in
                  let current_amount :=
                    deposits.(Storage.deposits.current_amount) in
                  if
                    Tez_repr.op_gt current_amount maximum_stake_to_be_deposited
                  then
                    let? to_reimburse :=
                      Tez_repr.op_minusquestion current_amount
                        maximum_stake_to_be_deposited in
                    let? '(ctxt, bupds) :=
                      Token.transfer (Some origin) ctxt
                        (Token.Source_container (Token.Frozen_deposits delegate))
                        (Token.Sink_container (Token.Delegate_balance delegate))
                        to_reimburse in
                    return? (ctxt, (Pervasives.op_at bupds balance_updates))
                  else
                    if
                      Tez_repr.op_lt current_amount
                        maximum_stake_to_be_deposited
                    then
                      let? desired_to_freeze :=
                        Tez_repr.op_minusquestion maximum_stake_to_be_deposited
                          current_amount in
                      let? balance :=
                        Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.get)
                          ctxt delegate_contract in
                      let to_freeze := Tez_repr.min balance desired_to_freeze in
                      let? '(ctxt, bupds) :=
                        Token.transfer (Some origin) ctxt
                          (Token.Source_container
                            (Token.Delegate_balance delegate))
                          (Token.Sink_container (Token.Frozen_deposits delegate))
                          to_freeze in
                      return? (ctxt, (Pervasives.op_at bupds balance_updates))
                    else
                      return? (ctxt, balance_updates)) maxima
            (ctxt, balance_updates) in
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.fold_es)
          (fun (delegate : Signature.public_key_hash) ⇒
            fun (function_parameter :
              Raw_context.t ×
                list
                  (Receipt_repr.balance × Receipt_repr.balance_update ×
                    Receipt_repr.update_origin)) ⇒
              let '(ctxt, balance_updates) := function_parameter in
              let delegate_contract := Contract_repr.implicit_contract delegate
                in
              let? ctxt :=
                Frozen_deposits_storage.update_initial_amount ctxt
                  delegate_contract Tez_repr.zero in
              let? frozen_deposits :=
                Frozen_deposits_storage.get ctxt delegate_contract in
              if
                Tez_repr.op_gt frozen_deposits.(Storage.deposits.current_amount)
                  Tez_repr.zero
              then
                let? '(ctxt, bupds) :=
                  Token.transfer (Some origin) ctxt
                    (Token.Source_container (Token.Frozen_deposits delegate))
                    (Token.Sink_container (Token.Delegate_balance delegate))
                    frozen_deposits.(Storage.deposits.current_amount) in
                return? (ctxt, (Pervasives.op_at bupds balance_updates))
              else
                return? (ctxt, balance_updates)) delegates_to_remove
          (ctxt, balance_updates).

Definition freeze_deposits_do_not_call_except_for_migration
  : Raw_context.t Cycle_repr.cycle
  list
    (Receipt_repr.balance × Receipt_repr.balance_update ×
      Receipt_repr.update_origin)
  M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  freeze_deposits (Some Receipt_repr.Protocol_migration).

Module Delegate_sampler_state.
  Module Cache_client.
    Definition cached_value : Set :=
      Sampler.t (Signature.public_key × Signature.public_key_hash).

    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.

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_contract delegate in
        let? frozen_deposits_limit :=
          Storage.Contract.Frozen_deposits_limit.(Storage_sigs.Indexed_data_storage.find)
            ctxt delegate_contract 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 frozen_deposits_percentage :=
          Constants_storage.frozen_deposits_percentage ctxt in
        let stake_to_consider :=
          match frozen_deposits_limit with
          | Some frozen_deposits_limit
            (* ❌ Try-with are not handled *)
            try_with
              (fun _
                let max_mutez := Tez_repr.of_mutez_exn Int64.max_int in
                if
                  Tez_repr.op_gt frozen_deposits_limit
                    (Tez_repr.div_exn max_mutez 100)
                then
                  let frozen_deposits_limit_by_10 :=
                    Tez_repr.mul_exn frozen_deposits_limit 10 in
                  if
                    Tez_repr.op_lt frozen_deposits_limit_by_10 staking_balance
                  then
                    frozen_deposits_limit_by_10
                  else
                    staking_balance
                else
                  Tez_repr.min staking_balance
                    (Tez_repr.div_exn
                      (Tez_repr.mul_exn frozen_deposits_limit 100)
                      frozen_deposits_percentage)) (fun _staking_balance)
          | Nonestaking_balance
          end in
        let? expanded_balance := Tez_repr.op_starquestion total_balance 100 in
        let? max_staking_capacity :=
          Tez_repr.op_divquestion expanded_balance
            (Int64.of_int frozen_deposits_percentage) in
        let stake_for_cycle :=
          Tez_repr.min stake_to_consider max_staking_capacity 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 := Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) 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 := Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) 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 ((Signature.public_key × Signature.public_key_hash) × Sampler.mass))
        ⇒
        fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
          let '(pkh, stake) := function_parameter in
          let? pk := pubkey ctxt pkh in
          return? (cons ((pk, pkh), (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
  match Cycle_repr.sub new_cycle max_slashing_period with
  | Nonereturn? ctxt
  | Some outdated_cycle
    let? ctxt := Delegate_sampler_state.remove_existing ctxt outdated_cycle in
    Storage.Seed.For_cycle.(Storage.FOR_CYCLE.remove_existing) ctxt
      outdated_cycle
  end.

Definition cycle_end
  (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
  (unrevealed_nonces : list Storage.Seed.unrevealed_nonce)
  : M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin) × list Signature.public_key_hash) :=
  let new_cycle := Cycle_repr.add last_cycle 1 in
  let? ctxt := select_new_distribution_at_cycle_end ctxt new_cycle in
  let ctxt := clear_outdated_slashed_deposits ctxt new_cycle in
  let? '(ctxt, balance_updates) :=
    distribute_endorsing_rewards ctxt last_cycle unrevealed_nonces in
  let? '(ctxt, balance_updates) :=
    freeze_deposits None ctxt new_cycle balance_updates in
  let? ctxt := Stake_storage.clear_at_cycle_end ctxt new_cycle in
  let? ctxt := clear_outdated_sampling_data ctxt new_cycle in
  let? '(ctxt, deactivated_delagates) := update_activity ctxt last_cycle in
  return? (ctxt, balance_updates, deactivated_delagates).

Definition balance (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Tez_repr.t :=
  let contract := Contract_repr.implicit_contract delegate in
  Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.get)
    ctxt contract.

Definition frozen_deposits
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Storage.deposits :=
  Frozen_deposits_storage.get ctxt (Contract_repr.implicit_contract delegate).

Definition full_balance
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Tez_repr.t :=
  let? frozen_deposits := frozen_deposits ctxt delegate in
  let delegate_contract := Contract_repr.implicit_contract delegate in
  let? balance_and_frozen_bonds :=
    Contract_storage.get_balance_and_frozen_bonds ctxt delegate_contract in
  Tez_repr.op_plusquestion frozen_deposits.(Storage.deposits.current_amount)
    balance_and_frozen_bonds.

Definition deactivated
  : Raw_context.t Signature.public_key_hash M? bool :=
  Delegate_activation_storage.is_inactive.

Definition delegated_balance
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Tez_repr.t :=
  let? staking_balance := staking_balance ctxt delegate in
  let? balance := balance ctxt delegate in
  let? frozen_deposits := frozen_deposits ctxt delegate in
  let? self_staking_balance :=
    Tez_repr.op_plusquestion balance
      frozen_deposits.(Storage.deposits.current_amount) in
  Tez_repr.op_minusquestion staking_balance self_staking_balance.

Definition fold {A : Set}
  : Raw_context.t Variant.t A (Signature.public_key_hash A A)
  A := Storage.Delegates.(Storage_sigs.Data_set_storage.fold).

Definition list_value : Raw_context.t list Signature.public_key_hash :=
  Storage.Delegates.(Storage_sigs.Data_set_storage.elements).

Definition check_delegate
  (ctxt : Raw_context.t) (pkh : Signature.public_key_hash) : M? unit :=
  let function_parameter :=
    Storage.Delegates.(Storage_sigs.Data_set_storage.mem) ctxt pkh in
  match function_parameter with
  | trueError_monad.return_unit
  | false
    Error_monad.fail
      (Build_extensible "Not_registered" Signature.public_key_hash pkh)
  end.

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 (Signature.public_key × Signature.public_key_hash)) :=
    let read (ctxt : Raw_context.t)
      : M?
        (Seed_repr.seed ×
          Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value)) :=
      let? seed_value :=
        Storage.Seed.For_cycle.(Storage.FOR_CYCLE.get) 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 × (Signature.public_key × Signature.public_key_hash)) :=
    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, pkh) := Sampler.sample state_value sample in
    return? (c_value, (pk, pkh)).
End Random.

Definition slot_owner
  (c_value : Raw_context.t) (level : Level_repr.t) (slot : Slot_repr.t)
  : M? (Raw_context.t × (Signature.public_key × Signature.public_key_hash)) :=
  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 ×
      (Signature.public_key × Signature.public_key_hash)) :=
  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 already_slashed_for_double_endorsing
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t) : M? bool :=
  let? function_parameter :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  match function_parameter with
  | NoneError_monad.return_false
  | Some slashedreturn? slashed.(Storage.slashed_level.for_double_endorsing)
  end.

Definition already_slashed_for_double_baking
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t) : M? bool :=
  let? function_parameter :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  match function_parameter with
  | NoneError_monad.return_false
  | Some slashedreturn? slashed.(Storage.slashed_level.for_double_baking)
  end.

Definition punish_double_endorsing
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t)
  : M? (Raw_context.t × Tez_repr.t × Receipt_repr.balance_updates) :=
  let delegate_contract := Contract_repr.implicit_contract delegate in
  let? frozen_deposits := Frozen_deposits_storage.get ctxt delegate_contract in
  let slashing_ratio :=
    Constants_storage.ratio_of_frozen_deposits_slashed_per_double_endorsement
      ctxt in
  let punish_value :=
    Tez_repr.div_exn
      (Tez_repr.mul_exn frozen_deposits.(Storage.deposits.initial_amount)
        slashing_ratio.(Constants_repr.ratio.numerator))
      slashing_ratio.(Constants_repr.ratio.denominator) in
  let amount_to_burn :=
    Tez_repr.min frozen_deposits.(Storage.deposits.current_amount) punish_value
    in
  let? '(ctxt, balance_updates) :=
    Token.transfer None ctxt
      (Token.Source_container (Token.Frozen_deposits delegate))
      (Token.Sink_infinite Token.Double_signing_punishments) amount_to_burn in
  let? ctxt := Stake_storage.remove_stake ctxt delegate amount_to_burn in
  let? slashed :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  let slashed :=
    match slashed with
    | None
      {| Storage.slashed_level.for_double_endorsing := true;
        Storage.slashed_level.for_double_baking := false; |}
    | Some slashed
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit
          (Compare.Bool.(Compare.S.op_eq)
            slashed.(Storage.slashed_level.for_double_endorsing) false) in
      Storage.slashed_level.with_for_double_endorsing true slashed
    end in
  let ctxt :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.add)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
      slashed in
  return? (ctxt, amount_to_burn, balance_updates).

Definition punish_double_baking
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t)
  : M? (Raw_context.t × Tez_repr.t × Receipt_repr.balance_updates) :=
  let delegate_contract := Contract_repr.implicit_contract delegate in
  let? frozen_deposits := Frozen_deposits_storage.get ctxt delegate_contract in
  let slashing_for_one_block := Constants_storage.double_baking_punishment ctxt
    in
  let amount_to_burn :=
    Tez_repr.min frozen_deposits.(Storage.deposits.current_amount)
      slashing_for_one_block in
  let? '(ctxt, balance_updates) :=
    Token.transfer None ctxt
      (Token.Source_container (Token.Frozen_deposits delegate))
      (Token.Sink_infinite Token.Double_signing_punishments) amount_to_burn in
  let? ctxt := Stake_storage.remove_stake ctxt delegate amount_to_burn in
  let? slashed :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  let slashed :=
    match slashed with
    | None
      {| Storage.slashed_level.for_double_endorsing := false;
        Storage.slashed_level.for_double_baking := true; |}
    | Some slashed
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit
          (Compare.Bool.(Compare.S.op_eq)
            slashed.(Storage.slashed_level.for_double_baking) false) in
      Storage.slashed_level.with_for_double_baking true slashed
    end in
  let ctxt :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.add)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
      slashed in
  return? (ctxt, amount_to_burn, balance_updates).

Inductive level_participation : Set :=
| Participated : level_participation
| Didn't_participate : level_participation.

Definition record_endorsing_participation
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (participation : level_participation) (endorsing_power : int)
  : M? Raw_context.t :=
  match participation with
  | Participatedset_active ctxt delegate
  | Didn't_participate
    let contract := Contract_repr.implicit_contract delegate in
    let? function_parameter :=
      Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
        ctxt contract in
    match function_parameter with
    |
      Some {|
        Storage.missed_endorsements_info.remaining_slots := remaining_slots;
          Storage.missed_endorsements_info.missed_levels := missed_levels
          |} ⇒
      let remaining_slots := remaining_slots -i endorsing_power in
      Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.update)
        ctxt contract
        {| Storage.missed_endorsements_info.remaining_slots := remaining_slots;
          Storage.missed_endorsements_info.missed_levels := missed_levels +i 1;
          |}
    | None
      let level := Level_storage.current ctxt in
      let? stake_distribution :=
        Raw_context.stake_distribution_for_current_cycle ctxt in
      match
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find)
          delegate stake_distribution with
      | None
        let '_ :=
          (* ❌ Assert instruction is not handled. *)
          assert unit (level.(Level_repr.t.cycle_position) =i32 0) in
        return? ctxt
      | Some active_stake
        let? total_active_stake :=
          Stake_storage.get_total_active_stake ctxt level.(Level_repr.t.cycle)
          in
        let? expected_slots :=
          expected_slots_for_given_active_stake ctxt total_active_stake
            active_stake in
        let '{|
          Constants_repr.ratio.numerator := numerator;
            Constants_repr.ratio.denominator := denominator
            |} := Constants_storage.minimal_participation_ratio ctxt in
        let minimal_activity := (expected_slots ×i numerator) /i denominator in
        let maximal_inactivity := expected_slots -i minimal_activity in
        let remaining_slots := maximal_inactivity -i endorsing_power in
        Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.init_value)
          ctxt contract
          {|
            Storage.missed_endorsements_info.remaining_slots := remaining_slots;
            Storage.missed_endorsements_info.missed_levels := 1; |}
      end
    end
  end.

Definition record_baking_activity_and_pay_rewards_and_fees
  (ctxt : Raw_context.t) (payload_producer : Signature.public_key_hash)
  (block_producer : Signature.public_key_hash) (baking_reward : Tez_repr.t)
  (reward_bonus : option Tez_repr.t)
  : M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let? ctxt := set_active ctxt payload_producer in
  let? ctxt :=
    if
      Pervasives.not
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
          payload_producer block_producer)
    then
      set_active ctxt block_producer
    else
      return? ctxt in
  let pay_payload_producer
    (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
    : M? (Raw_context.t × Receipt_repr.balance_updates) :=
    let contract := Contract_repr.implicit_contract delegate in
    let? '(ctxt, block_fees) := Token.balance ctxt Token.Block_fees in
    Token.transfer_n None ctxt
      [
        ((Token.Source_container Token.Block_fees), block_fees);
        ((Token.Source_infinite Token.Baking_rewards), baking_reward)
      ] (Token.Sink_container (Token.Contract contract)) in
  let pay_block_producer
    (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
    (bonus : Tez_repr.t) : M? (Raw_context.t × Receipt_repr.balance_updates) :=
    let contract := Contract_repr.implicit_contract delegate in
    Token.transfer None ctxt (Token.Source_infinite Token.Baking_bonuses)
      (Token.Sink_container (Token.Contract contract)) bonus in
  let? '(ctxt, balance_updates_payload_producer) :=
    pay_payload_producer ctxt payload_producer in
  let? '(ctxt, balance_updates_block_producer) :=
    match reward_bonus with
    | Some bonuspay_block_producer ctxt block_producer bonus
    | Nonereturn? (ctxt, nil)
    end in
  return?
    (ctxt,
      (Pervasives.op_at balance_updates_payload_producer
        balance_updates_block_producer)).

Module participation_info.
  Record record : Set := Build {
    expected_cycle_activity : int;
    minimal_cycle_activity : int;
    missed_slots : int;
    missed_levels : int;
    remaining_allowed_missed_slots : int;
    expected_endorsing_rewards : Tez_repr.t;
  }.
  Definition with_expected_cycle_activity expected_cycle_activity
    (r : record) :=
    Build expected_cycle_activity r.(minimal_cycle_activity) r.(missed_slots)
      r.(missed_levels) r.(remaining_allowed_missed_slots)
      r.(expected_endorsing_rewards).
  Definition with_minimal_cycle_activity minimal_cycle_activity (r : record) :=
    Build r.(expected_cycle_activity) minimal_cycle_activity r.(missed_slots)
      r.(missed_levels) r.(remaining_allowed_missed_slots)
      r.(expected_endorsing_rewards).
  Definition with_missed_slots missed_slots (r : record) :=
    Build r.(expected_cycle_activity) r.(minimal_cycle_activity) missed_slots
      r.(missed_levels) r.(remaining_allowed_missed_slots)
      r.(expected_endorsing_rewards).
  Definition with_missed_levels missed_levels (r : record) :=
    Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
      r.(missed_slots) missed_levels r.(remaining_allowed_missed_slots)
      r.(expected_endorsing_rewards).
  Definition with_remaining_allowed_missed_slots remaining_allowed_missed_slots
    (r : record) :=
    Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
      r.(missed_slots) r.(missed_levels) remaining_allowed_missed_slots
      r.(expected_endorsing_rewards).
  Definition with_expected_endorsing_rewards expected_endorsing_rewards
    (r : record) :=
    Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
      r.(missed_slots) r.(missed_levels) r.(remaining_allowed_missed_slots)
      expected_endorsing_rewards.
End participation_info.
Definition participation_info := participation_info.record.

Definition delegate_participation_info
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? participation_info :=
  let level := Level_storage.current ctxt in
  let? stake_distribution :=
    Stake_storage.get_selected_distribution ctxt level.(Level_repr.t.cycle) in
  match
    List.assoc_opt Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
      delegate stake_distribution with
  | None
    return?
      {| participation_info.expected_cycle_activity := 0;
        participation_info.minimal_cycle_activity := 0;
        participation_info.missed_slots := 0;
        participation_info.missed_levels := 0;
        participation_info.remaining_allowed_missed_slots := 0;
        participation_info.expected_endorsing_rewards := Tez_repr.zero; |}
  | Some active_stake
    let? total_active_stake :=
      Stake_storage.get_total_active_stake ctxt level.(Level_repr.t.cycle) in
    let? expected_cycle_activity :=
      expected_slots_for_given_active_stake ctxt total_active_stake active_stake
      in
    let '{|
      Constants_repr.ratio.numerator := numerator;
        Constants_repr.ratio.denominator := denominator
        |} := Constants_storage.minimal_participation_ratio ctxt in
    let endorsing_reward_per_slot :=
      Constants_storage.endorsing_reward_per_slot ctxt in
    let minimal_cycle_activity :=
      (expected_cycle_activity ×i numerator) /i denominator in
    let maximal_cycle_inactivity :=
      expected_cycle_activity -i minimal_cycle_activity in
    let expected_endorsing_rewards :=
      Tez_repr.mul_exn endorsing_reward_per_slot expected_cycle_activity in
    let contract := Contract_repr.implicit_contract delegate in
    let? missed_endorsements :=
      Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
        ctxt contract in
    let '(missed_slots, missed_levels, remaining_allowed_missed_slots) :=
      match missed_endorsements with
      | None(0, 0, maximal_cycle_inactivity)
      |
        Some {|
          Storage.missed_endorsements_info.remaining_slots := remaining_slots;
            Storage.missed_endorsements_info.missed_levels := missed_levels
            |} ⇒
        ((maximal_cycle_inactivity -i remaining_slots), missed_levels,
          (Compare.Int.max 0 remaining_slots))
      end in
    let expected_endorsing_rewards :=
      match
        (missed_endorsements,
          match missed_endorsements with
          | Some r_value
            r_value.(Storage.missed_endorsements_info.remaining_slots) <i 0
          | _false
          end) with
      | (Some r_value, true)Tez_repr.zero
      | (_, _)expected_endorsing_rewards
      end in
    return?
      {| participation_info.expected_cycle_activity := expected_cycle_activity;
        participation_info.minimal_cycle_activity := minimal_cycle_activity;
        participation_info.missed_slots := missed_slots;
        participation_info.missed_levels := missed_levels;
        participation_info.remaining_allowed_missed_slots :=
          remaining_allowed_missed_slots;
        participation_info.expected_endorsing_rewards :=
          expected_endorsing_rewards; |}
  end.

Definition init_first_cycles (ctxt : Raw_context.t) : M? Raw_context.t :=
  let preserved := Constants_storage.preserved_cycles ctxt in
  List.fold_left_es
    (fun (ctxt : Raw_context.t) ⇒
      fun (c_value : int) ⇒
        let cycle := Cycle_repr.of_int32_exn (Int32.of_int c_value) in
        let? ctxt := Stake_storage.snapshot_value ctxt in
        select_distribution_for_cycle ctxt cycle) ctxt
    (Misc.op_minusminusgt 0 preserved).