Skip to main content

👥 Delegate_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module1 : unit :=
  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).

Definition registered : Raw_context.t Signature.public_key_hash bool :=
  Storage.Delegates.(Storage_sigs.Data_set_storage.mem).

Module Contract.
  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 := 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.

Init function; without side-effects in Coq
  Definition init_module2 : unit :=
    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
    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" ++
                    String.String "010" " implicit account is empty (")
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format)))
                ("Delegate registration is forbidden when the delegate" ++
                  String.String "010"
                    " 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).

  Definition set_self_delegate
    (c_value : Raw_context.t) (delegate : Signature.public_key_hash)
    : M? Raw_context.t :=
    let is_registered := registered c_value delegate in
    if is_registered then
      let? '_ :=
        let? is_inactive :=
          Delegate_activation_storage.is_inactive c_value delegate in
        Error_monad.fail_unless is_inactive
          (Build_extensible "Active_delegate" unit tt) in
      Stake_storage.set_active c_value delegate
    else
      let contract := Contract_repr.Implicit delegate in
      let? pk :=
        Contract_manager_storage.get_manager_key
          (Some
            (Build_extensible "Unregistered_delegate" Signature.public_key_hash
              delegate)) c_value delegate in
      let? '_ :=
        let is_allocated := Contract_storage.allocated c_value contract in
        Error_monad.fail_unless is_allocated
          (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
      let c_value :=
        Storage.Delegates.(Storage_sigs.Data_set_storage.add) c_value delegate
        in
      let? c_value := Delegate_consensus_key.init_value c_value delegate pk in
      let? c_value := Stake_storage.set_active c_value delegate in
      return? c_value.

Init function; without side-effects in Coq
  Definition init_module3 : 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
    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).

  Definition set_delegate
    (c_value : Raw_context.t) (contract : Contract_repr.t)
    (delegate : option Signature.public_key_hash) : M? Raw_context.t :=
    let? '_ :=
      match contract with
      | Contract_repr.Originated _Error_monad.Lwt_result_syntax.return_unit
      | Contract_repr.Implicit pkh
        let is_registered := registered c_value pkh in
        Error_monad.fail_when is_registered
          (Build_extensible "No_deletion" Signature.public_key_hash pkh)
      end in
    let? '_ :=
      let? current_delegate := Contract_delegate_storage.find c_value contract
        in
      match
        ((delegate, current_delegate),
          match (delegate, current_delegate) with
          | (Some delegate, Some current_delegate)
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
              delegate current_delegate
          | _false
          end) with
      | ((None, None), _)Error_monad.Lwt_result_syntax.return_unit
      | ((Some delegate, Some current_delegate), true)
        Error_monad.Lwt_result_syntax.tzfail
          (Build_extensible "Current_delegate" unit tt)
      | (_, _)Error_monad.Lwt_result_syntax.return_unit
      end 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
    match delegate with
    | None
      let? c_value := Contract_delegate_storage.delete c_value contract in
      return? c_value
    | Some delegate
      let? '_ :=
        let is_delegate_registered := registered c_value delegate in
        Error_monad.fail_when (Pervasives.not is_delegate_registered)
          (Build_extensible "Unregistered_delegate" Signature.public_key_hash
            delegate) 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
      return? c_value
    end.

  Definition set
    (c_value : Raw_context.t) (contract : Contract_repr.t)
    (delegate : option Signature.public_key_hash) : M? Raw_context.t :=
    match
      ((delegate, contract),
        match (delegate, contract) with
        | (Some delegate, Contract_repr.Implicit source)
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) source
            delegate
        | _false
        end) with
    | ((Some delegate, Contract_repr.Implicit source), true)
      set_self_delegate c_value delegate
    | (_, _)set_delegate c_value contract delegate
    end.
End Contract.

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

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

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 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 delegate) limit.

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

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

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

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 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 delegated_balance
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Tez_repr.t :=
  let? staking_balance := staking_balance ctxt delegate in
  let? self_staking_balance := full_balance ctxt delegate in
  Tez_repr.op_minusquestion staking_balance self_staking_balance.

Definition drain
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (destination : Signature.public_key_hash)
  : M?
    (Raw_context.t × bool × Tez_repr.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let destination_contract := Contract_repr.Implicit destination in
  let is_destination_allocated :=
    Contract_storage.allocated ctxt destination_contract in
  let delegate_contract := Contract_repr.Implicit delegate in
  let? '(ctxt, _, balance_updates1) :=
    if Pervasives.not is_destination_allocated then
      Fees_storage.burn_origination_fees None ctxt
        (Z.of_int (Constants_storage.origination_size ctxt))
        (Token.Source_container (Token.Contract delegate_contract))
    else
      return? (ctxt, Z.zero, nil) in
  let? manager_balance := spendable_balance ctxt delegate in
  let? one_percent := Tez_repr.op_divquestion manager_balance 100 in
  let fees := Tez_repr.max Tez_repr.one one_percent in
  let? transferred := Tez_repr.op_minusquestion manager_balance fees in
  let? '(ctxt, balance_updates2) :=
    Token.transfer None ctxt
      (Token.Source_container (Token.Contract delegate_contract))
      (Token.Sink_container (Token.Contract destination_contract)) transferred
    in
  return?
    (ctxt, (Pervasives.not is_destination_allocated), fees,
      (Pervasives.op_at balance_updates1 balance_updates2)).