👥 Delegate_storage.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.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.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Fees_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Fees_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_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.
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.
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.
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)).
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)).