ssnlist.scilla

scilla_version 0

import ListUtils IntUtils PairUtils

library SSNList

(* A non-custodial staking contract with admin privileges *)
(* SSN Data Type *)
(* Each SSN has the following fields: *)

(* ActiveStatus      : Bool *)
(*                     Represents whether the SSN has the minnimum stake amount and therefore ready to participate in staking and receive rewards. *)
(* StakeAmount       : Uint128 *)
(*                     Total stake that can be used for reward calculation. *)
(* StakeRewards      : Uint128 *)
(*                     (Unwithdrawn) Reward accumulated so far across all cycles. It only includes the reward that the SSN can distribute to its delegators. *)
(*                     It does not include SSN's own commission. *)
(* Name              : String *)
(*                     A human-readable name for this SSN. *)
(* URLRaw            : String *)
(*                     Represents "ip:port" of the SSN serving raw API requests. *)
(* URLApi            : String *)
(*                     Representing URL exposed by SSN serving public API requests. *)
(* BufferedDeposit   : Uint128 *)
(*                     Stake deposit that cannot be counted as a part of reward calculation for the ongoing reward cycle. But, to be considered *)
(*                     for the next one. *)
(* Commission        : Uint128 *)
(*                     Percentage of incoming rewards that the SSN takes as commission. If the commission is 10.5%, then it is multiplied by 10^7 and then the resulting integer is set as commission. The assumption is that the percentage is up to 7 decimal places. *)
(* CommissionRewards : Uint128 *)
(*                     Number of ZILs earned as commission by the SSN. *)
(* ReceivingAddress   : ByStr20 *)
(*                     Address that will be used to receive commission. *)
(* Invariant : ActiveStatus = (Minstake < StakeAmount)  *)

type Ssn =
| Ssn of Bool Uint128 Uint128 String String String Uint128 Uint128 Uint128 ByStr20

(*  SSNAddress        : ByStr20 *)
(*                      Address of the SSN. *)
(*  CycleReward       : Uint128 *)
(*                      Integer representation of reward assigned by the verifier to this SSN for this cycle. *)
(*  TotalStakeAmount  : Uint128 *)
(*                      Total stake amount at a specific cycle.                                               *)
type SsnStakeRewardShare = 
| SsnStakeRewardShare of ByStr20 Uint128 Uint128

(* SSNCycleInfo Data Type *)

(*   Each SSNCycleInfo has the following fields: *)
(*    TotalStakeDuringTheCycle            : Uint128 *)
(*                                          Represents the amount staked during this cycle for the given SSN. *)
(*    TotalRewardEarnedDuringTheCycle    : Uint128 *)
(*                                         Represents the total reward earned during this cycle for the given SSN. . *)

type SSNCycleInfo =
| SSNCycleInfo of Uint128 Uint128

(* Used in order to be able to iterate over the procedure CalcStakeRewards *)
(* deleg, ssn_operator, reward_cycle *)

type TmpArg =
| TmpArg of ByStr20 ByStr20 Uint32

let one_msg =
  fun (m : Message) =>
    let e = Nil {Message} in
    Cons {Message} m e

let uint128_one =  Uint128 1
let uint128_zero = Uint128 0
let uint128_10_power_7 = Uint128 10000000
let uint128_10_power_9 = Uint128 1000000000
let uint128_100 = Uint128 100

let uint32_one = Uint32 1
let uint32_zero = Uint32 0

let option_value =
  tfun 'A =>
  fun (default: 'A) =>
  fun (opt_val: Option 'A) =>
    match opt_val with
    | Some v => v
    | None => default
    end

let option_map_uint128_uint128_value =
  let f = @option_value (Map Uint128 Uint128) in
  let emt = Emp Uint128 Uint128 in
  f emt

let option_uint128_value =
  let f = @option_value Uint128 in
  f uint128_zero
  
let option_uint32_value =
  let f = @option_value Uint32 in
  f uint32_zero

let sub_one_to_zero =
  fun (x: Uint32) =>
  let less_than_one = builtin lt x uint32_one in
  match less_than_one with
  | True =>
    uint32_zero
  | False =>
    let res = builtin sub x uint32_one in
    res
  end

let option_add =
  fun (x_opt: Option Uint128) =>
  fun (y_opt: Option Uint128) =>
    match x_opt with
    | Some x =>
      let y = option_uint128_value y_opt in
      let res = builtin add x y in
      Some {Uint128} res
    | None => y_opt
    end

let change_rate =
  fun (old: Uint128) =>
  fun (new: Uint128) =>
    let a = builtin lt old new in
    match a with
    | True =>
      builtin sub new old
    | False =>
      builtin sub old new
    end

let iota : Uint32 -> Uint32 -> List Uint32 =
  fun (m : Uint32) => fun (n : Uint32) =>
    let m_lt_n = builtin lt m n in
    match m_lt_n with
    | True =>
        let delta = builtin sub n m in
        let delta_nat = builtin to_nat delta in
        let nil = Nil {Uint32} in
        let acc_init = Pair {(List Uint32) Uint32} nil n in
        let one = Uint32 1 in
        let step = fun (xs_n : Pair (List Uint32) Uint32) => fun (ignore : Nat) =>
          match xs_n with
          | Pair xs n =>
              let new_n = builtin sub n one in
              let new_xs = Cons {Uint32} new_n xs in
              Pair {(List Uint32) Uint32} new_xs new_n
          end in
        let fold = @nat_fold (Pair (List Uint32) Uint32) in
        let xs_m = fold step acc_init delta_nat in
        match xs_m with
        | Pair xs m => xs
        end
    | False => Nil {Uint32}
    end


let uint128_to_uint256 : Uint128 -> Uint256 =
  fun (x : Uint128) =>
    let ox256 = builtin to_uint256 x in
      match ox256 with
      | None =>
        (* this never happens, hence we throw a division by zero exception just in case *)
        let zero = Uint256 0 in
        builtin div zero zero
      | Some x256 => x256
      end

(* Compute "(x * y) / z" with protection against integer overflows *)
let muldiv : Uint128 -> Uint128 -> Uint128 -> Uint128 =
    fun (x : Uint128) =>
    fun (y : Uint128) =>
    fun (z : Uint128) =>
      let x256 = uint128_to_uint256 x in
      let y256 = uint128_to_uint256 y in
      let z256 = uint128_to_uint256 z in
      let x_mul_y256 = builtin mul x256 y256 in
      let res256 = builtin div x_mul_y256 z256 in
      let ores128 = builtin to_uint128 res256 in
      match ores128 with
      | None =>
        (* this must never happen, hence we throw an integer overflow exception *)
        let max_uint128 = Uint128 340282366920938463463374607431768211455 in
        let fourtytwo128 = Uint128 42 in
        builtin mul max_uint128 fourtytwo128
      | Some res128 =>
        res128
      end

let map_to_stake_rewards = 
  fun (total_stake: Uint128) =>
  fun (element: Pair ByStr20 Uint128) =>
    match element with
    | Pair ssnaddr cycle_reward => SsnStakeRewardShare ssnaddr cycle_reward total_stake 
    end

(* check if last_withdraw_cycle_deleg[deleg] is empty *)
let is_ssn_cycle_map_empty =
  fun(m : Map ByStr20 Uint32) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

(* check if deposit_amt_deleg[deleg] is empty *)
let is_ssn_deposit_map_empty =
  fun(m : Map ByStr20 Uint128) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

(* check if withdrawal_pending[deleg] is empty *)
let is_block_deposit_map_empty =
  fun(m : Map BNum Uint128) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

(* check if nested maps are empty *)
(* buff_deposit_deleg[deleg] *)
(* direct_deposit_deleg[deleg] *)
(* deleg_stake_per_cycle[deleg] *)
let is_ssn_cycle_deposit_map_empty =
  fun(m : Map ByStr20 (Map Uint32 Uint128)) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

(* check if final inner map is empty *)
(* buff_deposit_deleg[deleg][ssn] *)
(* direct_deposit_deleg[deleg][ssn] *)
(* deleg_stake_per_cycle[deleg][ssn] *)
let is_cycle_deposit_map_empty =
  fun(m : Map Uint32 Uint128) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

let bool_active = True
let bool_inactive = False
let addfunds_tag = "AddFunds"

(* for SwapDelegator *)
let reset_addr = 0x0000000000000000000000000000000000000000

type Error =
  | ContractFrozenFailure
  | VerifierValidationFailed
  | AdminValidationFailed
  | StagingAdminNotExist
  | StagingAdminValidationFailed
  | ProxyValidationFailed
  | DelegDoesNotExistAtSSN
  | DelegHasBufferedDeposit
  | ChangeCommError
  | SSNNotExist
  | SSNAlreadyExist
  | DelegHasUnwithdrawRewards
  | DelegHasNoSufficientAmt
  | SSNNoComm
  | DelegStakeNotEnough
  | ExceedMaxChangeRate
  | ExceedMaxCommRate
  | InvalidTotalAmt
  | VerifierNotSet
  | VerifierRecvAddrNotSet
  | ReDelegInvalidSSNAddr
  | AvailableRewardsError
  | InvalidSwapAddr
  | SwapAddrValidationFailed
  | SwapAddrAlreadyExistsAsRequest

let make_error =
  fun (result: Error) =>
    let result_code =
      match result with
      | ContractFrozenFailure => Int32 -1
      | VerifierValidationFailed => Int32 -2
      | AdminValidationFailed => Int32 -3
      | StagingAdminNotExist => Int32 -4
      | StagingAdminValidationFailed => Int32 -5
      | ProxyValidationFailed => Int32 -6
      | DelegDoesNotExistAtSSN => Int32 -7
      | DelegHasBufferedDeposit => Int32 -8
      | ChangeCommError => Int32 -9
      | SSNNotExist => Int32 -10
      | SSNAlreadyExist => Int32 -11
      | DelegHasUnwithdrawRewards => Int32 -12
      | DelegHasNoSufficientAmt => Int32 -13
      | SSNNoComm => Int32 -14
      | DelegStakeNotEnough => Int32 -15
      | ExceedMaxChangeRate => Int32 -16
      | ExceedMaxCommRate => Int32 -17
      | InvalidTotalAmt => Int32 -18
      | VerifierNotSet => Int32 -19
      | VerifierRecvAddrNotSet => Int32 -20
      | ReDelegInvalidSSNAddr => Int32 -21
      | AvailableRewardsError => Int32 -22
      | InvalidSwapAddr => Int32 -23
      | SwapAddrValidationFailed => Int32 -24
      | SwapAddrAlreadyExistsAsRequest => Int32 -25
      end
    in
    { _exception: "Error"; code: result_code }

(* Utility used for migration *)
let list_map_to_pair_with_constant : forall 'A. forall 'B. List 'A -> 'B -> List (Pair 'A 'B) =
  tfun 'A =>
  tfun 'B => 
  fun (list : List 'A) =>
  fun (const : 'B) =>
    let f = fun (key : 'A) => Pair {'A 'B} key const in
    let mapper = @list_map 'A (Pair 'A 'B) in
    mapper f list
    
(***************************************************)
(*             The contract definition             *)
(***************************************************)
contract SSNList(
  init_admin: ByStr20,
  init_proxy_address: ByStr20,
  init_gzil_address: ByStr20
)

(* Keeps track of SSNS *)
(* AddressOfSSN -> SSNInfo *)
field ssnlist: Map ByStr20 Ssn = Emp ByStr20 Ssn

(* Record commission for SSN for each reward cycle *)
(* AddressofSSN -> (RewardCycle -> commission ) *)
field comm_for_ssn: Map ByStr20 (Map Uint32 Uint128) = Emp ByStr20 (Map Uint32 Uint128)

(* Following data structure helps to calculate rewards for delegators *)
(* Keeps track of stakes deposited at SSNs *)
(* Record deposit amount for every deleg for every ssn *)
(* AddressofDeleg -> (AddressofSSN -> StakeAmount) *)
field deposit_amt_deleg: Map ByStr20 (Map ByStr20 Uint128) = Emp ByStr20 (Map ByStr20 Uint128)

(* AddressofSSN -> (AddressofDeleg -> StakeAmount) *)
(* Used by offchain services like wallets *)
field ssn_deleg_amt: Map ByStr20 (Map ByStr20 Uint128) = Emp ByStr20 (Map ByStr20 Uint128)

(* Keeps track of buffered deposit for a delegator *)
(* AddressOfDeleg -> (AddressofSSN -> (RewardCycleNumber -> BufferedStakeAmountDuringTheCycle)) *)
(* The BufferedStakeAmount will only be truely delegated at next cycle *)
field buff_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128)) = Emp ByStr20 (Map ByStr20 (Map Uint32 Uint128))

(* Keeps track of stake deposits for a delegator that can be considered for reward calcuation *)
(* AddressofDeleg -> (AddressofSSN -> (RewardCycleNumber -> StakeAmount)) *)
field direct_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128)) = Emp ByStr20 (Map ByStr20 (Map Uint32 Uint128))

(* Keeps track of the cycle number when a deleg last withdrew its rewards *)
(* AddressOfDeleg -> ( AddressOfSSN -> CycleNumberWhenLastWithdrawn) *)
(* notice here, the last withdraw cycle also indicated the earlist deposit cycle this round *)
(* this will help reduce some calculation for DistributeStakeRewards, also can avoid some corner cases *)
field last_withdraw_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32) = Emp ByStr20 (Map ByStr20 Uint32)

(* Keeps track of the cycle number when a deleg last buffered deposit its delegate *)
(* AddressOfDeleg -> ( AddressOfSSN -> CycleNumberWhenLastDeposit) *)
field last_buf_deposit_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32) = Emp ByStr20 (Map ByStr20 Uint32)

(* AddressOfSSN -> (RewardCycleNumber -> Pair (TotalStakeDuringTheCycleForSSN, TotalRewardEarnedDuringTheCycle) *)
field stake_ssn_per_cycle: Map ByStr20 (Map Uint32 SSNCycleInfo) = Emp ByStr20 (Map Uint32 SSNCycleInfo)

(* AddressOfDeleg -> AddressOfSSN -> EffectCycleNum -> Deposit *)
field deleg_stake_per_cycle: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128)) = Emp ByStr20 (Map ByStr20 (Map Uint32 Uint128))

(* AddressOfDeleg -> BlockNumber -> Deposit *)
field withdrawal_pending: Map ByStr20 (Map BNum Uint128) = Emp ByStr20 (Map BNum Uint128)

(* AddressOfInitialDeleg -> AddressOfNewDeleg *)
(* used to transfer all stakes and pending withdrawal of deleg_A -> deleg_B *)
(* see RequestDelegatorSwap *)
field deleg_swap_request: Map ByStr20 ByStr20 = Emp ByStr20 ByStr20

field bnum_req: Uint128 = Uint128 35000

(* Temporary storage maps *)
field cycle_rewards_deleg: Uint128 = uint128_zero

(* Used during AssignStakeReward *)
(* Record the latest rewards earned by verifier *)
field verifier_reward: Uint128 = uint128_zero

field available_withdrawal: Uint128 = uint128_zero

field current_deleg: Option ByStr20 = None {ByStr20}

(* Used during SwapDelegator *)
(* Keeps tracks of the ssn address to pass to other procedures in forall calls *)
field current_ssn: Option ByStr20 = None {ByStr20}

(* Used during SwapDelegator *)
(* Keeps tracks of the new deleg address to pass to other procedures*)
field new_deleg: Option ByStr20 = None {ByStr20}

field verifier: Option ByStr20 = None {ByStr20}

field verifier_receiving_addr: Option ByStr20 = None {ByStr20}

(* 10 mil ZIL expressed in Qa where 1 ZIL = 10^12 Qa *)
field minstake: Uint128 = Uint128 10000000000000000000

(* 10 ZIL expresssed in Qa where 1 ZIL = 10^12 Qa *)
field mindelegstake: Uint128 = Uint128 10000000000000

field contractadmin: ByStr20  = init_admin
field stagingcontractadmin: Option ByStr20 = None {ByStr20}
field gziladdr: ByStr20 = init_gzil_address
field lastrewardcycle: Uint32 = uint32_one
field paused: Bool = True

(* 1% *)
field maxcommchangerate: Uint128 = uint128_one

(* 100% expressed as an integer multipled by 10^7 *)
field maxcommrate: Uint128 = Uint128 1000000000
field totalstakeamount: Uint128 = uint128_zero

(* Procedures *)
(* Internal functions, used like Solidity modifiers *)

(* to erase buff_deposit_deleg outer keys *)
(* see CleanBuffDeposit *)
procedure CleanBuffDepositDelegAddr(deleg: ByStr20)
  buff_deposit_deleg_map <- buff_deposit_deleg[deleg];
  match buff_deposit_deleg_map with
  | Some buff_deposit_deleg_entry =>
    is_map_empty = is_ssn_cycle_deposit_map_empty buff_deposit_deleg_entry;
    match is_map_empty with
    | True => (* empty map *)
      delete buff_deposit_deleg[deleg]
    | False => (* contains other records *)
    end
  | None => (* nothing to delete *)
  end
end

(* to erase buff_deposit_deleg inner keys *)
(* see CleanBuffDeposit *)
procedure CleanBuffDepositSSNAddr(deleg_ssn_pair: Pair ByStr20 ByStr20)
  match deleg_ssn_pair with
  | Pair deleg ssn =>
    inner_map <- buff_deposit_deleg[deleg][ssn];
    match inner_map with
    | Some inner_entry =>
      is_map_empty = is_cycle_deposit_map_empty inner_entry;
      match is_map_empty with
      | True => (* empty map *)
        delete buff_deposit_deleg[deleg][ssn]
      | False => (* contains other records *)
      end
    | None => (* nothing to delete *)
    end
  end
end

(* to erase direct_deposit_deleg inner keys  *)
procedure CleanDirectDepositSSNAddr(deleg_ssn_pair: Pair ByStr20 ByStr20)
  match deleg_ssn_pair with
  | Pair deleg ssn =>
    inner_map <- direct_deposit_deleg[deleg][ssn];
    match inner_map with
    | Some inner_entry =>
      is_map_empty = is_cycle_deposit_map_empty inner_entry;
      match is_map_empty with
      | True => (* empty map *)
        delete direct_deposit_deleg[deleg][ssn]
      | False => (* contains other records *)
      end
    | None => (* nothing to delete *)
    end
  end
end

(* to erase direct_deposit_deleg outer keys  *)
procedure CleanDirectDepositDelegAddr(deleg: ByStr20)
  direct_deposit_deleg_map <- direct_deposit_deleg[deleg];
  match direct_deposit_deleg_map with
  | Some direct_deposit_deleg_entry =>
    is_map_empty = is_ssn_cycle_deposit_map_empty direct_deposit_deleg_entry;
    match is_map_empty with
    | True => (* empty map *)
      delete direct_deposit_deleg[deleg]
    | False => (* contains other records *)
    end
  | None => (* nothing to delete *)
  end
end

(* to erase deleg_stake_per_cycle inner keys  *)
procedure CleanDelegStakePerCycleSSNAddr(deleg_ssn_pair: Pair ByStr20 ByStr20)
  match deleg_ssn_pair with
  | Pair deleg ssn =>
    inner_map <- deleg_stake_per_cycle[deleg][ssn];
    match inner_map with
    | Some inner_entry =>
      is_map_empty = is_cycle_deposit_map_empty inner_entry;
      match is_map_empty with
      | True => (* empty map *)
        delete deleg_stake_per_cycle[deleg][ssn]
      | False => (* contains other records *)
      end
    | None => (* nothing to delete *)
    end
  end
end

(* to erase deleg_stake_per_cycle outer keys  *)
procedure CleanDelegStakePerCycleDelegAddr(deleg: ByStr20)
  deleg_stake_per_cycle_map <- deleg_stake_per_cycle[deleg];
  match deleg_stake_per_cycle_map with
  | Some deleg_stake_per_cycle_entry =>
    is_map_empty = is_ssn_cycle_deposit_map_empty deleg_stake_per_cycle_entry;
    match is_map_empty with
    | True => (* empty map *)
      delete deleg_stake_per_cycle[deleg]
    | False => (* contains other records *)
    end
  | None => (* nothing to delete *)
  end
end

(* to erase deposit_amt_deleg outer keys  *)
procedure CleanDepositAmtDelegAddr(deleg: ByStr20)
  ssn_deposit_map <- deposit_amt_deleg[deleg];
  match ssn_deposit_map with
  | Some ssn_deposit_entry =>
    is_map_empty = is_ssn_deposit_map_empty ssn_deposit_entry;
    match is_map_empty with
    | True => (* empty map *)
      delete deposit_amt_deleg[deleg]
    | False => (* contains other records *)
    end
  | None => (* nothing to delete *)
  end
end

(* to erase last_withdraw_cycle_deleg outer keys  *)
procedure CleanLastWithdrawCycleDelegAddr(deleg: ByStr20)
  ssn_cycle_map <- last_withdraw_cycle_deleg[deleg];
  match ssn_cycle_map with
  | Some ssn_cycle_entry =>
    is_map_empty = is_ssn_cycle_map_empty ssn_cycle_entry;
    match is_map_empty with
    | True => (* empty map *)
      delete last_withdraw_cycle_deleg[deleg]
    | False => (* contains other records *)
    end
  | None => (* nothing to delete *)
  end
end

(* to erase last_buf_deposit_cycle_deleg outer keys  *)
procedure CleanLastBuffDepositCycleDelegAddr(deleg: ByStr20)
  ssn_cycle_map <- last_buf_deposit_cycle_deleg[deleg];
  match ssn_cycle_map with
  | Some ssn_cycle_entry =>
    is_map_empty = is_ssn_cycle_map_empty ssn_cycle_entry;
    match is_map_empty with
    | True => (* empty map *)
      delete last_buf_deposit_cycle_deleg[deleg]
    | False => (* contains other records *)
    end
  | None => (* nothing to delete *)
  end
end

(* to erase withdrawal_pending outer keys  *)
procedure CleanPendingWithdrawalDelegAddr(deleg: ByStr20)
  block_deposit_map <- withdrawal_pending[deleg];
  match block_deposit_map with
  | Some block_deposit_entry =>
    is_map_empty = is_block_deposit_map_empty block_deposit_entry;
    match is_map_empty with
    | True => (* empty map *)
      delete withdrawal_pending[deleg]
    | False => (* contains other records *)
    end
  | None => (* nothing to delete *)
  end
end

(* delete the cycle key and any other external keys if the inner map is empty *)
(* for use in replace of normal delete operation to erase empty nested maps *)
procedure DeleteBuffDeposit(deleg: ByStr20, ssnaddr: ByStr20, cycle: Uint32)
  delete buff_deposit_deleg[deleg][ssnaddr][cycle];
  deleg_ssn_pair = Pair {ByStr20 ByStr20} deleg ssnaddr;
  CleanBuffDepositSSNAddr deleg_ssn_pair;
  CleanBuffDepositDelegAddr deleg
end

(* delete the cycle key and any other external keys if the inner map is empty *)
(* for use in replace of normal delete operation to erase empty nested maps *)
procedure DeleteDirectDeposit(deleg: ByStr20, ssnaddr: ByStr20, cycle: Uint32)
  delete direct_deposit_deleg[deleg][ssnaddr][cycle];
  deleg_ssn_pair = Pair {ByStr20 ByStr20} deleg ssnaddr;
  CleanDirectDepositSSNAddr deleg_ssn_pair;
  CleanDirectDepositDelegAddr deleg
end

(* delete the blk num and any other external keys if the inner map is empty *)
(* for use in replace of normal delete operation to erase empty nested maps *)
procedure DeletePendingWithdrawal(deleg: ByStr20, withdraw_number: BNum)
  delete withdrawal_pending[deleg][withdraw_number];
  CleanPendingWithdrawalDelegAddr deleg
end

procedure TruncateDeleg(deleg: ByStr20, ssnaddr: ByStr20)
  delete deposit_amt_deleg[deleg][ssnaddr];
  delete ssn_deleg_amt[ssnaddr][deleg];
  delete buff_deposit_deleg[deleg][ssnaddr];
  delete direct_deposit_deleg[deleg][ssnaddr];
  delete last_withdraw_cycle_deleg[deleg][ssnaddr];
  delete deleg_stake_per_cycle[deleg][ssnaddr];
  delete last_buf_deposit_cycle_deleg[deleg][ssnaddr];

  (* ssn_deleg_amt won't have empty maps *)
  CleanDepositAmtDelegAddr deleg;
  CleanBuffDepositDelegAddr deleg;
  CleanDirectDepositDelegAddr deleg;
  CleanDelegStakePerCycleDelegAddr deleg;
  CleanLastWithdrawCycleDelegAddr deleg;
  CleanLastBuffDepositCycleDelegAddr deleg
end

procedure ThrowError(err: Error)
  e = make_error err;
  throw e
end

procedure ValidateRate(rate: Uint128)
  max_rate <- maxcommrate;
  validate = uint128_le rate max_rate;
  match validate with
  | True =>
  | False =>
    e = ExceedMaxCommRate;
    ThrowError e
  end
end

procedure ValidateChangeRate(old: Uint128, new: Uint128)
  maxcommchangerate_l <- maxcommchangerate;
  absolute_change = change_rate old new;
  absolute_change = builtin div absolute_change uint128_10_power_7;
  valid = uint128_le absolute_change maxcommchangerate_l;
  match valid with
  | True =>
  | False =>
    e = ExceedMaxChangeRate;
    ThrowError e
  end
end

procedure IncreaseTotalStakeAmt(amt: Uint128)
  current_amt <- totalstakeamount;
  new_amt = builtin add current_amt amt;
  totalstakeamount := new_amt
end

procedure DecreaseTotalStakeAmt(amt: Uint128)
  current_amt <- totalstakeamount;
  valid = uint128_le amt current_amt;
  match valid with
  | True =>
    new_amt = builtin sub current_amt amt;
    totalstakeamount := new_amt
  | False =>
    e = InvalidTotalAmt;
    ThrowError e
  end
end

procedure IncreaseTotalStakeAmtOnStatus(amt: Uint128, status: Bool)
  match status with
  | True =>
    e = { _eventname: "SSNActive"; increase_amt: amt };
    event e;
    IncreaseTotalStakeAmt amt
  | False =>
  end  
end

procedure DecreaseTotalStakeAmtOnStatus(amt: Uint128, status: Bool)
  match status with
  | True =>
  | False =>
    e = { _eventname: "SSNInactive"; decreased_amt: amt };
    event e;
    DecreaseTotalStakeAmt amt
  end
end

(* Check if the initiator is verifier *)
procedure CallerIsVerifier(initiator: ByStr20)
  verifier_tmp <- verifier;
  match verifier_tmp with
  | Some v =>
    is_verifier = builtin eq initiator v;
    match is_verifier with
    | True =>
    | False =>
      e = VerifierValidationFailed;
      ThrowError e
    end
  | None =>
    e = VerifierNotSet;
    ThrowError e
  end
end

(* Check if the initiator is admin *)
procedure IsAdmin(initiator: ByStr20)
  contractadmin_tmp <- contractadmin;
  is_admin = builtin eq initiator contractadmin_tmp;
  match is_admin with
  | True  =>
  | False =>
    e = AdminValidationFailed;
    ThrowError e
  end
end

(* Check if the caller is the proxy *)
procedure IsProxy()
  is_proxy = builtin eq _sender init_proxy_address;
  match is_proxy with
  | True  =>
  | False =>
    e = ProxyValidationFailed;
    ThrowError e
  end
end

(* Check if the contract is not paused *)
procedure IsNotPaused()
  paused_tmp <- paused;
  match paused_tmp with
  | False =>
  | True  =>
    e = ContractFrozenFailure;
    ThrowError e
  end
end

(* Check if the contract is paused *)
procedure IsPaused()
  paused_tmp <- paused;
  match paused_tmp with
  | False =>
    e = ContractFrozenFailure;
    ThrowError e
  | True => 
  end
end

procedure TransferFunds(tag: String, amt: Uint128, recipient: ByStr20)
    msg = {_tag: tag; _recipient: recipient; _amount: amt};
    msgs = one_msg msg;
    send msgs
end

(* current_block > withdraw_number + bnum_req *)
procedure CalculateTotalWithdrawal(withdraw: Pair BNum Uint128)
  current_deleg_o <- current_deleg;
  match current_deleg_o with
  | Some deleg =>
    match withdraw with
    | Pair withdraw_number amt =>
      current_bnum <- & BLOCKNUMBER;
      current_bnum_req <- bnum_req;
      bnum = builtin badd withdraw_number current_bnum_req;
      can_withdraw = builtin blt bnum current_bnum;
      match can_withdraw with
      | True =>
          DeletePendingWithdrawal deleg withdraw_number;
          current_amt <- available_withdrawal;
          current_amt = builtin add current_amt amt;
          available_withdrawal := current_amt
      | False => 
      end
    end
  | None => (* Won't reach *)
  end
end

procedure AssertCorrectRewards(remaining_rewards: Uint128, ssn_rewards: Uint128)
  validate = uint128_le ssn_rewards remaining_rewards;
  match validate with
  | True =>
  | False =>
    e = AvailableRewardsError;
    ThrowError e
  end
end

procedure UpdateStakeReward(entry: SsnStakeRewardShare)
  lastreward_blk <- lastrewardcycle;
  match entry with
  | SsnStakeRewardShare ssnaddr cycle_reward total_stake =>
    curval <- ssnlist[ssnaddr];
    match curval with
    | None =>
      e = SSNNotExist;
      ThrowError e
    | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
      match active_status with
      | False =>
        e = { _eventname: "SSN inactive"; ssn_addr: ssnaddr};
        event e
      | True  =>
        (* To calculate rewards belong to this ssn operator *)
        new_rewards = muldiv stake_amt cycle_reward total_stake;
        current_verifier_reward <- verifier_reward;

        AssertCorrectRewards current_verifier_reward new_rewards;
        new_current_verifier_reward = builtin sub current_verifier_reward new_rewards;
        verifier_reward := new_current_verifier_reward;

        (* To calculate commission *)
        reward_comm_tmp = muldiv new_rewards comm uint128_10_power_9;
        total_reward_comm = builtin add reward_comm_tmp comm_rewards;

        (* To calculate rewards can be distributed to delegators *)
        delegate_reward = builtin sub new_rewards reward_comm_tmp;

        p = SSNCycleInfo stake_amt delegate_reward;
        stake_ssn_per_cycle[ssnaddr][lastreward_blk] := p;

        (* Update ssn info *)
        new_stake_amt = builtin add stake_amt buffdeposit;
        deleg_reward = builtin add delegate_reward rewards;
        ssn = Ssn active_status new_stake_amt deleg_reward name urlraw urlapi uint128_zero comm total_reward_comm rec_addr;
        ssnlist[ssnaddr] := ssn;
        IncreaseTotalStakeAmt buffdeposit;
        e = { _eventname: "SSN assign reward"; ssnaddr: ssnaddr; cycle_number: lastreward_blk; delegate_rewards: delegate_reward; comm_rewards:  reward_comm_tmp};
        event e
      end
    end
  end
end

(* this procedure is to send rewards to deleg *)
procedure SendDelegRewards(addr: ByStr20, amt: Uint128)
  to_send = builtin eq amt uint128_zero;
  match to_send with
  | True =>
  | False =>
    TransferFunds addfunds_tag amt addr;
    e = { _eventname: "Send deleg rewards"; addr: addr; amt:  amt};
    event e
  end
end

(* Check if a delegs exists for a given SSN *)
procedure DelegExists(ssnaddr: ByStr20, deleg: ByStr20)
  if_exists <- exists deposit_amt_deleg[deleg][ssnaddr];
  match if_exists with
  | True  =>
  | False =>
    e = DelegDoesNotExistAtSSN;
    ThrowError e
    end
end

procedure FillLastWithdrawCycle(ssnaddr: ByStr20, deleg : ByStr20)
  lwcd_o <- last_withdraw_cycle_deleg[deleg][ssnaddr];
  match lwcd_o with
  | Some lwcd =>
  | None =>
    lrc <- lastrewardcycle;
    last_withdraw_cycle_deleg[deleg][ssnaddr] := lrc
  end
end

procedure FillInDepositDelegAmt(ssnaddr: ByStr20, deleg: ByStr20, amount: Uint128)
  deposit_amt <- deposit_amt_deleg[deleg][ssnaddr];
  match deposit_amt with
  | Some amt =>
    new_amt = builtin add amt amount;
    deposit_amt_deleg[deleg][ssnaddr] := new_amt;
    ssn_deleg_amt[ssnaddr][deleg] := new_amt
  | None =>
    deposit_amt_deleg[deleg][ssnaddr] := amount;
    ssn_deleg_amt[ssnaddr][deleg] := amount
  end
end

procedure AssertNoRewards(ssnaddr: ByStr20, deleg: ByStr20, total_rewards: Uint128)
  no_total_rewards = builtin eq total_rewards uint128_zero;
  match no_total_rewards with
  | True =>
  | False =>
    lrcd_tmp <- last_withdraw_cycle_deleg[deleg][ssnaddr];
    lrcd = option_uint32_value lrcd_tmp;
    lrc <- lastrewardcycle;
    has_reward = builtin lt lrcd lrc;
    match has_reward with
    | True =>
      offset = builtin sub lrc lrcd;
      offset_only_one = builtin eq offset uint32_one;
      match offset_only_one with
      | True =>
        (* if there is only one cycle ahead, and if it only has buffered deposit, then the rewards *)
        (* could be zero, we should let him go. to identify this case, we need calculate the exact rewards *)
        last_reward_cycle = builtin sub lrc uint32_one;
        last2_reward_cycle = sub_one_to_zero last_reward_cycle;
        cur_opt <- direct_deposit_deleg[deleg][ssnaddr][last_reward_cycle];
        buf_opt <- buff_deposit_deleg[deleg][ssnaddr][last2_reward_cycle];
        comb_opt = option_add cur_opt buf_opt;
        last_amt_o <- deleg_stake_per_cycle[deleg][ssnaddr][last_reward_cycle];
        last_amt = option_uint128_value last_amt_o;
        staking_of_deleg = match comb_opt with
        | Some stake => builtin add last_amt stake
        | None => last_amt
        end;
        no_rewards = builtin eq staking_of_deleg uint128_zero;
        match no_rewards with
        | True =>
        | False =>
          e = DelegHasUnwithdrawRewards;
          ThrowError e
        end
      | False =>
        e = DelegHasUnwithdrawRewards;
        ThrowError e
      end
    | False =>
    end
  end
end

procedure AsseertNoBufferedDeposit(ssnaddr: ByStr20, deleg: ByStr20)
  ldcd_o <- last_buf_deposit_cycle_deleg[deleg][ssnaddr];
  ldcd = option_uint32_value ldcd_o;
  lrc <- lastrewardcycle;
  (* in fact, lrc will only more than or equal to ldcd, equal means he has delegated this round and withdrawn this round as well *)
  has_buffered = uint32_le lrc ldcd;
  match has_buffered with
  | True =>
    e = DelegHasBufferedDeposit;
    ThrowError e
  | False =>
  end
end

(* corner case check for swap request process in which there is buff_deposit but zero reward after assign rewards *)
procedure AssertNoBufferedDepositLessOneCycle(ssnaddr: ByStr20, deleg: ByStr20)
  lrc <- lastrewardcycle;
  last_reward_cycle = builtin sub lrc uint32_one;
  has_buffered <- buff_deposit_deleg[deleg][ssnaddr][last_reward_cycle];
  match has_buffered with
  | Some buff_deposit =>
    e = DelegHasBufferedDeposit;
    ThrowError e
  | None =>
  end
end

procedure IsDelegstakeSufficient(amount: Uint128)
  mindelegstake_l <- mindelegstake;
  suffi =  uint128_le mindelegstake_l amount;
  match suffi with
  | True =>
  | False =>
    e = DelegStakeNotEnough;
    ThrowError e
  end
end

procedure AdjustDeleg(ssnaddr: ByStr20, deleg: ByStr20, total_amount: Uint128, withdraw_amount: Uint128)
  sufficient = uint128_le withdraw_amount total_amount;
  match sufficient with
  | True =>
    need_truncate =  builtin eq withdraw_amount total_amount;
    match need_truncate with
    | True =>
      (* Remove all info map recorded for this deleg *)
      TruncateDeleg deleg ssnaddr
    | False =>
      (* Readjust all rest deleg to this cycle *)
      lrc <- lastrewardcycle;
      rest_deleg = builtin sub total_amount withdraw_amount;
      (* rest delegate should also meet mindelegstake *)
      IsDelegstakeSufficient rest_deleg;
      TruncateDeleg deleg ssnaddr;
      (* Refer to transition TruncateDeleg, here we don't use Fillin transition because we *)
      (* know they are all empty, and this can reduce some gasfee *)
      deposit_amt_deleg[deleg][ssnaddr] := rest_deleg;
      ssn_deleg_amt[ssnaddr][deleg] := rest_deleg;
      direct_deposit_deleg[deleg][ssnaddr][lrc] := rest_deleg;
      last_withdraw_cycle_deleg[deleg][ssnaddr] := lrc
    end
  | False =>
    e = DelegHasNoSufficientAmt;
    ThrowError e
  end
end

procedure UnDelegateStakeAmt(initiator: ByStr20, ssn: ByStr20, undeleg_amt: Uint128)
  ssn_o <- ssnlist[ssn];
  deleg <- deposit_amt_deleg[initiator][ssn];
  match ssn_o with
  | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    match deleg with
    | Some amt =>
      AssertNoRewards ssn initiator rewards;
      AsseertNoBufferedDeposit ssn initiator;
      AdjustDeleg ssn initiator amt undeleg_amt;
      (* Illegal withdraw amount could be handled in procedure AdjustDeleg *)
      new_amt = builtin sub stake_amt undeleg_amt;
      minstake_tmp <- minstake;
      status = uint128_le minstake_tmp new_amt;
      ssn_option_tmp = Ssn status new_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr;
      ssnlist[ssn] := ssn_option_tmp;
      e = { _eventname: "Remove delegate from SSN"; ssn_addr: ssn; deleg_address: initiator; amt: undeleg_amt };
      event e;
      match active_status with
      | True =>
        (* If the original status is active, we can substract from totalstakeamt, otherwise dont do so *)
        DecreaseTotalStakeAmt undeleg_amt;
        event_decrease = { _eventname: "DecreaseTotalStakeAmt"; decreased_amt: undeleg_amt };
        event event_decrease;
        (* If ssn becomes inactive, we need to decrease the rest ones as well *)
        DecreaseTotalStakeAmtOnStatus new_amt status
      | False =>
        event_decrease = { _eventname: "SSNInactiveBefore" };
        event event_decrease
      end
    | None =>
      e = DelegDoesNotExistAtSSN;
      ThrowError e
    end
  | None =>
    e = SSNNotExist;
    ThrowError e
  end
end

procedure WithdrawalStakeAmt(initiator: ByStr20, ssn: ByStr20, withdraw_amount: Uint128)
  ssn_o <- ssnlist[ssn];
  deleg <- deposit_amt_deleg[initiator][ssn];
  match ssn_o with
  | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    match deleg with
    | Some amt =>
      AssertNoRewards ssn initiator rewards;
      AsseertNoBufferedDeposit ssn initiator;
      AdjustDeleg ssn initiator amt withdraw_amount;
      (* Illegal withdraw amount could be handled in procedure AdjustDeleg *)
      new_amt = builtin sub stake_amt withdraw_amount;
      minstake_tmp <- minstake;
      status = uint128_le minstake_tmp new_amt;
      ssn_option_tmp = Ssn status new_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr;
      ssnlist[ssn] := ssn_option_tmp;
      withdrawal_bnum <- & BLOCKNUMBER;
      withdraw_amt_o <- withdrawal_pending[initiator][withdrawal_bnum];
      withdraw_amt_pending = match withdraw_amt_o with
      | Some v => builtin add v withdraw_amount
      | None => withdraw_amount
      end;
      withdrawal_pending[initiator][withdrawal_bnum] := withdraw_amt_pending;
      e = { _eventname: "Deleg withdraw deposit"; ssn_addr: ssn; deleg_address: initiator; withdraw_amount: withdraw_amount };
      event e;
      match active_status with
      | True =>
        (* If the original status is active, we can substract from totalstakeamt, otherwise dont do so *)
        DecreaseTotalStakeAmt withdraw_amount;
        event_decrease = { _eventname: "DecreaseTotalStakeAmt"; decreased_amt: withdraw_amount };
        event event_decrease;
        (* If ssn becomes inactive, we need to decrease the rest as well *)
        DecreaseTotalStakeAmtOnStatus new_amt status
      | False =>
        event_decrease = { _eventname: "SSNInactiveBefore" };
        event event_decrease
      end
    | None =>
      e = DelegDoesNotExistAtSSN;
      ThrowError e
    end
  | None =>
    e = SSNNotExist;
    ThrowError e
  end
end

procedure IncreaseReward(reward: Uint128)
  exist_reward <- cycle_rewards_deleg;
  new_reward = builtin add exist_reward reward;
  cycle_rewards_deleg := new_reward
end

procedure CalcStakeRewards(tmp_arg: TmpArg)
  match tmp_arg with
  | TmpArg deleg ssn_operator reward_cycle =>
    last_reward_cycle = builtin sub reward_cycle uint32_one;
    last2_reward_cycle = sub_one_to_zero last_reward_cycle;
    cur_opt <- direct_deposit_deleg[deleg][ssn_operator][last_reward_cycle];
    buf_opt <- buff_deposit_deleg[deleg][ssn_operator][last2_reward_cycle];
    comb_opt = option_add cur_opt buf_opt;

    last_amt_o <- deleg_stake_per_cycle[deleg][ssn_operator][last_reward_cycle];
    last_amt = option_uint128_value last_amt_o;
    staking_and_rewards_per_cycle_for_ssn_opt <- stake_ssn_per_cycle[ssn_operator][reward_cycle];

    (* the rewards for this cycle also computed within this procedure, so we no long keep histric data *)
    (* delete empty keys if need to *)
    (* no need to remove deleg_stake_per_cycle empty keys as assigning it with other cycle later *)
    delete deleg_stake_per_cycle[deleg][ssn_operator][last_reward_cycle];
    DeleteDirectDeposit deleg ssn_operator last_reward_cycle;
    DeleteBuffDeposit deleg ssn_operator last2_reward_cycle;

    staking_of_deleg = match comb_opt with
    | Some stake => builtin add last_amt stake
    | None => last_amt
    end;
    deleg_stake_per_cycle[deleg][ssn_operator][reward_cycle] := staking_of_deleg;
    
    match staking_and_rewards_per_cycle_for_ssn_opt with
    | Some (SSNCycleInfo total_staking total_rewards) =>
      reward = muldiv total_rewards staking_of_deleg total_staking;
      IncreaseReward reward
    | None =>
    end

  end
end

procedure MintCall(recipient: ByStr20, amount: Uint128)
  is_zero = builtin eq amount uint128_zero;
  match is_zero with
  | True =>
  | False =>
    addr <- gziladdr;
    msg_to_gzil = {_tag: "Mint"; _recipient: addr; _amount: uint128_zero; 
                  recipient: recipient; amount: amount};
    msgs = one_msg msg_to_gzil;
    send msgs
  end
end

procedure WithdrawalStakeRewards(deleg: ByStr20, ssn_operator: ByStr20)
  last_withdraw_cycle_deleg_m <- last_withdraw_cycle_deleg[deleg][ssn_operator];
  last_withdraw_cycle = option_uint32_value last_withdraw_cycle_deleg_m;
  lrc <- lastrewardcycle;

  m = builtin add last_withdraw_cycle uint32_one;
  n = builtin add lrc uint32_one;
  list_need_compute_rewards = iota m n;
  
  (* Combine deleg and ssn_operator with list_need_compute_rewards *)
  mapper = @list_map Uint32 TmpArg;
  f = fun (cycle: Uint32) => TmpArg deleg ssn_operator cycle;
  combined_args_list = mapper f list_need_compute_rewards;

  (* Calculate rewards *)
  cycle_rewards_deleg := uint128_zero;
  forall combined_args_list CalcStakeRewards;

  (* Send rewards out and mint gzil *)
  reward <- cycle_rewards_deleg;
  SendDelegRewards deleg reward;
  MintCall deleg reward;

  ssn_o <- ssnlist[ssn_operator];
  match ssn_o with
  | Some (Ssn active_status stake_amt total_rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    rest_rewards = builtin sub total_rewards reward;
    ssn = Ssn active_status stake_amt rest_rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr;
    ssnlist[ssn_operator] := ssn
  | None => throw
  end;
  e = { _eventname: "WithdrawalStakeRewards"; rewards: reward};
  event e;
  last_withdraw_cycle_deleg[deleg][ssn_operator] := lrc;
  msg_to_delegator = {_tag : "WithdrawStakeRewardsSuccessCallBack"; _recipient : deleg; _amount : uint128_zero; 
  ssnaddr : ssn_operator; rewards : reward};
  msg = one_msg msg_to_delegator;
  send msg
end

procedure Delegate(ssnaddr: ByStr20, initiator: ByStr20, amount: Uint128)
  curval <- ssnlist[ssnaddr];
  match curval with
  | None =>
    e = SSNNotExist;
    ThrowError e
  | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    IsDelegstakeSufficient amount;
    lrc <- lastrewardcycle;
    (* The delegated stake can be accepted. *) 
    FillInDepositDelegAmt ssnaddr initiator amount;
    (* If it is the first time delegator delegates to a given SSN, then we need to fill last_withdraw_cycle_deleg with lastrewardcycle *)
    (* otherwise, the rewards calculation will start from cycle 1 which is wrong *)
    FillLastWithdrawCycle ssnaddr initiator;
    (* It is buffered if the SSN is active if not it is added to the stake_amount. *)
    match active_status with
    | True  =>
      last_buf_deposit_cycle_deleg[initiator][ssnaddr] := lrc;
      new_buff_amt  = builtin add amount buffdeposit;
      (* The SSN is active so add the delegated stake to the buffer *)
      ssn = Ssn bool_active stake_amt rewards name urlraw urlapi new_buff_amt comm comm_rewards rec_addr;
      ssnlist[ssnaddr] := ssn;
      (* record this to buffer deposit for deleg *)
      stake_amt_for_deleg_option  <- buff_deposit_deleg[initiator][ssnaddr][lrc];
      match stake_amt_for_deleg_option  with
      | Some stake_amt_for_deleg =>
        new_stake_amt_for_deleg = builtin add stake_amt_for_deleg amount;
        buff_deposit_deleg[initiator][ssnaddr][lrc] := new_stake_amt_for_deleg
      | None =>
        buff_deposit_deleg[initiator][ssnaddr][lrc] := amount
      end
    | False =>
      minstake_tmp <- minstake;
      (* The SSN is inactive so add the delegated stake to stake_amount *)
      new_stake_amt  = builtin add amount stake_amt;
      status = uint128_le minstake_tmp new_stake_amt;
      (* The SSN becomes active if the total stake after deposit is greater than the minimum required. *)
      ssn = Ssn status new_stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr;
      ssnlist[ssnaddr] := ssn;
      (* If ssn becomes active, then we need to increase totalstakeamount *)
      IncreaseTotalStakeAmtOnStatus new_stake_amt status;
      (* record this to direct deposit for deleg *)
      stake_amt_for_deleg_option  <- direct_deposit_deleg[initiator][ssnaddr][lrc];
      match stake_amt_for_deleg_option  with
      | Some stake_amt_for_deleg =>
        new_stake_amt_for_deleg = builtin add stake_amt_for_deleg amount;
        direct_deposit_deleg[initiator][ssnaddr][lrc] := new_stake_amt_for_deleg
      | None =>
        direct_deposit_deleg[initiator][ssnaddr][lrc] := amount
      end
    end
  end  
end

(***************************************************)
(*                  Transition                     *)
(***************************************************)

(***************************************************)
(*            House keeping transition             *)
(***************************************************)

(* @dev: pause the contract. Used by admin only. *)
(* @param initiator: The original caller who called the proxy. *)
transition Pause(initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  paused := bool_active
end

(* @dev: unpause/unfreeze the contract. Used by admin only. *)
(* @param initiator: The original caller who called the proxy. *)
transition UnPause(initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  paused := bool_inactive
end

(* @dev: Start a proposal for new contract admin. Used by admin only. *)
(* @param admin: New admin value *)
(* @param initiator: The original caller who called the proxy. *)
transition UpdateAdmin(admin: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  staging_admin = Some {ByStr20} admin;
  stagingcontractadmin := staging_admin
end

(* @dev: Claim to be the new admin of contract. *)
(* @param initiator: The original caller who called the proxy. *)
transition ClaimAdmin(initiator: ByStr20)
  IsProxy;
  staging_admin <- stagingcontractadmin;
  match staging_admin with
  | Some admin =>
    is_valid = builtin eq initiator admin;
    match is_valid with
    | True =>
      contractadmin := admin;
      staging_admin = None {ByStr20};
      stagingcontractadmin := staging_admin;
      e = { _eventname: "ClaimAdmin"; new_admin: admin };
      event e
    | False =>
      e = StagingAdminValidationFailed;
      ThrowError e
    end
  | None =>
    e = StagingAdminNotExist;
    ThrowError e
  end
end

(* @dev: Set the verifier of the contract. Used by admin only. *)
(* @param verif: New verifier value *)
(* @param initiator: The original caller who called the proxy *)
transition UpdateVerifier(verif: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  newverifier = Some {ByStr20} verif;
  verifier := newverifier
end

(* @dev: Set the verifier receiving address of the contract. Used by admin only. *)
(* @param addr: New verifier receiving address *)
(* @param initiator: The original caller who called the proxy *)
transition UpdateVerifierRewardAddr(addr: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  newAddr = Some {ByStr20} addr;
  verifier_receiving_addr := newAddr
end

(* @dev: Set the staking parameters of contract. Used by admin only. *)
(* @param min_stake: New minstake value *)
(* @param min_deleg_stake: New mindelegstake value *)
(* @param initiator: The original caller who called the proxy *)
transition UpdateStakingParameters(min_stake: Uint128, min_deleg_stake: Uint128, max_comm_change_rate: Uint128, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  minstake := min_stake;
  mindelegstake := min_deleg_stake;
  maxcommchangerate := max_comm_change_rate
end

transition ChangeBNumReq(input_bnum_req: Uint128, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  bnum_req := input_bnum_req
end

transition UpdateGzilAddr(gzil_addr: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  gziladdr := gzil_addr
end

transition AddSSN(ssnaddr: ByStr20, name: String, urlraw: String, urlapi: String, comm: Uint128, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  already_exists <- exists ssnlist[ssnaddr];
  match already_exists with
  | True  =>
    e = SSNAlreadyExist;
    ThrowError e
  | False =>
    ValidateRate comm;
    status = bool_inactive;
    stake_amt = Uint128 0;
    rewards = Uint128 0;
    buff_deposit = Uint128 0;
    comm_rewards = Uint128 0;
    s = Ssn status stake_amt rewards name urlraw urlapi buff_deposit comm comm_rewards ssnaddr;
    ssnlist[ssnaddr] := s;
    lrc <- lastrewardcycle;
    comm_for_ssn[ssnaddr][lrc] := comm;
    e = { _eventname: "SSN added"; ssn_addr: ssnaddr };
    event e
  end
end

transition UpdateSSN(ssnaddr: ByStr20, new_name: String, new_urlraw: String, new_urlapi: String, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  ssn_o <- ssnlist[ssnaddr];
  match ssn_o with
  | Some (Ssn active_status staking_amt deleg_reward name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    ssn = Ssn active_status staking_amt deleg_reward new_name new_urlraw new_urlapi buffdeposit comm comm_rewards rec_addr;
    ssnlist[ssnaddr] := ssn;
    e = { _eventname: "UpdateSSN"; ssnaddr: ssnaddr; new_name: new_name; new_urlraw: new_urlraw; new_urlapi: new_urlapi; initiator: initiator };
    event e
  | None =>
    e = SSNNotExist;
    ThrowError e
  end
end

(* @dev: delete empty maps {} for buff_deposit_deleg  *)
(* invoked by staking-tool purge script *)
(* @param deleg_addr_list: the list of deleg address to be deleted (1st layer map); buff_deposit_deleg[deleg] *)
(* @param ssn_addr_list: the list of ssn address to be deleted (2nd layer map); buff_deposit_deleg[deleg][ssn] *)
transition CleanBuffDeposit(deleg_addr_list: List ByStr20, ssn_addr_list: List (Pair ByStr20 ByStr20), initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  (* must clean all the inner maps before cleaning the outer maps *)
  forall ssn_addr_list CleanBuffDepositSSNAddr;
  forall deleg_addr_list CleanBuffDepositDelegAddr
end

(* @dev: delete empty maps {} for direct_deposit_deleg  *)
(* invoked by staking-tool purge script *)
(* @param deleg_addr_list: the list of deleg address to be deleted (1st layer map); direct_deposit_deleg[deleg] *)
(* @param ssn_addr_list: the list of ssn address to be deleted (2nd layer map); direct_deposit_deleg[deleg][ssn] *)
transition CleanDirectDeposit(deleg_addr_list: List ByStr20, ssn_addr_list: List (Pair ByStr20 ByStr20), initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  (* must clean all the inner maps before cleaning the outer maps *)
  forall ssn_addr_list CleanDirectDepositSSNAddr;
  forall deleg_addr_list CleanDirectDepositDelegAddr
end

(* @dev: delete empty maps {} for deleg_stake_per_cycle  *)
(* invoked by staking-tool purge script *)
(* @param deleg_addr_list: the list of deleg address to be deleted (1st layer map); deleg_stake_per_cycle[deleg] *)
(* @param ssn_addr_list: the list of ssn address to be deleted (2nd layer map); deleg_stake_per_cycle[deleg][ssn] *)
transition CleanDelegStakePerCycle(deleg_addr_list: List ByStr20, ssn_addr_list: List (Pair ByStr20 ByStr20), initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  (* must clean all the inner maps before cleaning the outer maps *)
  forall ssn_addr_list CleanDelegStakePerCycleSSNAddr;
  forall deleg_addr_list CleanDelegStakePerCycleDelegAddr
end

(* @dev: delete empty maps {} for deposit_amt_deleg *)
(* invoked by staking-tool purge script *)
(* @param deleg_addr_list: the list of deleg address to be deleted (1st layer map); deposit_amt_deleg[deleg] *)
transition CleanDepositAmt(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanDepositAmtDelegAddr
end

(* @dev: delete empty maps {} for withdrawal_pending *)
(* invoked by staking-tool purge script *)
(* @param deleg_addr_list: the list of deleg address to be deleted (1st layer map); withdrawal_pending[deleg] *)
transition CleanPendingWithdrawal(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanPendingWithdrawalDelegAddr
end

(* @dev: delete empty maps {} for last_withdraw_cycle_deleg *)
(* invoked by staking-tool purge script *)
(* @param deleg_addr_list: the list of deleg address to be deleted (1st layer map); last_withdraw_cycle_deleg[deleg] *)
transition CleanLastWithdrawCycle(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanLastWithdrawCycleDelegAddr
end

(* @dev: delete empty maps {} for last_buf_deposit_cycle_deleg *)
(* invoked by staking-tool purge script *)
(* @param deleg_addr_list: the list of deleg address to be deleted (1st layer map); last_buf_deposit_cycle_deleg[deleg] *)
transition CleanLastBuffDepositCycle(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanLastBuffDepositCycleDelegAddr
end

(***************************************************)
(*             SSN operator transition             *)
(***************************************************)

(* @dev : To update the commision rate for a given SSN *)
(* @param new_rate: The new commision rate *)
(* @param initiator: The original caller who called the proxy *)
(* If the percentage is 5.2%, then, the value of this field will be 5.2 x 10^7 represented as an integer *)
(* The max rate is 100%, so the max new rate will be 100 x 10^7 which is 10^9 *)
transition UpdateComm(new_rate: Uint128, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  curval <- ssnlist[initiator];
  match curval with
  | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    lrc <- lastrewardcycle;
    old_comm_option <- comm_for_ssn[initiator][lrc];
    match old_comm_option with
    | Some old_comm =>
      e = ChangeCommError;
      ThrowError e
    | None =>
      ValidateRate new_rate;
      ValidateChangeRate comm new_rate;
      comm_for_ssn[initiator][lrc] := new_rate;
      ssn =  Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit new_rate comm_rewards rec_addr;
      ssnlist[initiator] := ssn;
      e = { _eventname: "UpdateComm"; ssn_addr: initiator; new_rate: new_rate };
      event e
    end
  | None =>
    e = SSNNotExist;
    ThrowError e
  end
end

(* @dev: Withdraw comm. Can be called by a ssn operator. *)
(* @param initiator: The original caller who called the proxy *)
transition WithdrawComm(initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  curval <- ssnlist[initiator];
  match curval with
  | None =>
    e = SSNNotExist;
    ThrowError e
  | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    has_comm = uint128_gt comm_rewards uint128_zero;
    match has_comm with
    | True =>
      e = { _eventname: "SSN withdraw reward"; ssn_addr: initiator; withdraw_comm: comm_rewards };
      event e;
      ssn = Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm uint128_zero rec_addr;
      ssnlist[initiator] := ssn;
      TransferFunds addfunds_tag comm_rewards rec_addr
    | False =>
      e = SSNNoComm;
      ThrowError e
    end
  end
end

(* @dev : To update the received address for a given SSN *)
(* @param new_addr: The new received address *)
(* @param initiator: The original caller who called the proxy. This is SSN address. *)
transition UpdateReceivingAddr(new_addr: ByStr20, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  curval <- ssnlist[initiator];
  match curval with
  | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    ssn =  Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards new_addr;
    ssnlist[initiator] := ssn;
    e = { _eventname: "UpdateReceivingAddr"; ssn_addr: initiator; new_addr: new_addr };
    event e
  | None =>
    e = SSNNotExist;
    ThrowError e
  end
end

(***************************************************)
(*                Delegator transition             *)
(***************************************************)

(* @dev : To delegate the stake to the contract. *)
(* @param ssnaddr: The address of the SSN to which the deleg wants to stake *)
(* @param initiator: The original caller who called the proxy aka the deleg. *)
transition DelegateStake(ssnaddr: ByStr20, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  (* Accept the deposit from SSN and add to contract balance. *)
  accept; 
  amount = _amount;
  Delegate ssnaddr initiator amount;
  e = { _eventname: "DelegateStake"; ssn_addr: ssnaddr; delegator: initiator; amount: amount };
  event e;
  msg_to_delegator = {_tag : "DelegateStakeSuccessCallBack"; _recipient : initiator; _amount : uint128_zero; 
  ssnaddr : ssnaddr; amount : amount};
  msg = one_msg msg_to_delegator;
  send msg
end

(* @dev: Withdraw stake reward. Can be called by a deleg. *)
(* @param ssnaddr: The address of the SSN to which the deleg wants to stake *)
(* @param initiator: The original caller who called the proxy *)
transition WithdrawStakeRewards(ssnaddr: ByStr20, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  DelegExists ssnaddr initiator;
  WithdrawalStakeRewards initiator ssnaddr
end

(* @dev: Intitiate the process of unbonding of ZIL for withdrawal purpose. Used by delegs. *)
(* @param ssnaddr: Address of the SSN to which stake had been delegated. *)
(* @param amt: The amount which the delegators want to unbond*)
(* @param initiator: The original caller who called the proxy. *)
transition WithdrawStakeAmt(ssnaddr: ByStr20, amt: Uint128, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  WithdrawalStakeAmt initiator ssnaddr amt;
  msg_to_delegator = {_tag : "WithdrawStakeAmtSuccessCallBack"; _recipient : initiator; _amount : uint128_zero; 
  ssnaddr : ssnaddr; amount : amt};
  msg = one_msg msg_to_delegator;
  send msg
end

(* @dev: Withdrawal of all unbonded stake. Used by delegs. *)
(* @param initiator: The original caller who called the proxy. *)
transition CompleteWithdrawal(initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  withdraw_map_o <- withdrawal_pending[initiator];
  match withdraw_map_o with
  | Some withdraw_map =>
    withdraw_list = builtin to_list withdraw_map;
    (* To init tmp fields *)
    withdrawal_zero = uint128_zero;
    available_withdrawal := withdrawal_zero;
    c = Some {ByStr20} initiator;
    current_deleg := c;

    (* Calculate withdrawal that can be transferred *)
    forall withdraw_list CalculateTotalWithdrawal;
    withdraw_amt <- available_withdrawal;
    transfer = builtin eq withdraw_amt uint128_zero;
    match transfer with
    | True =>
      e = { _eventname: "NoUnbondedStake"; ssnaddr: initiator };
      event e;
      msg_to_delegator = {_tag : "CompleteWithdrawalNoUnbondedStakeCallBack"; _recipient : initiator; _amount : uint128_zero; 
      amount : uint128_zero};
      msg = one_msg msg_to_delegator;
      send msg
    | False =>
      e = { _eventname: "CompleteWithdrawal"; ssnaddr: initiator; amount: withdraw_amt };
      event e;
      TransferFunds addfunds_tag withdraw_amt initiator;
      msg_to_delegator = {_tag : "CompleteWithdrawalSuccessCallBack"; _recipient : initiator; _amount : uint128_zero; 
      amount : withdraw_amt};
      msg = one_msg msg_to_delegator;
      send msg
    end
  | None =>
    e = { _eventname: "NoPendingWithdrawal"; ssnaddr: initiator };
    event e
  end
end

(* @dev: Transfer stake deposit from one SSN to another. Used by delegs. *)
(* @param ssnaddr: SSN from where the stake deposit will be withdrawn for transfer purpose. *)
(* @param to_ssn: SSN that will receive the withdrawn stake deposit. *)
(* @param amount: The amount of stake deposit to transfer. *)
(* @param initiator: The original caller who called the proxy. *)
transition ReDelegateStake(ssnaddr: ByStr20, to_ssn: ByStr20, amount: Uint128, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  same_ssn = builtin eq ssnaddr to_ssn;
  match same_ssn with
  | True =>
    e = ReDelegInvalidSSNAddr;
    ThrowError e
  | False =>
    UnDelegateStakeAmt initiator ssnaddr amount;
    Delegate to_ssn initiator amount;
    e = { _eventname: "ReDelegateStakeSuccess"; ssnaddr: ssnaddr; to_ssn: to_ssn; delegator: initiator; delegate_amount: amount };
    event e;
    msg_to_delegator = {_tag : "ReDelegateStakeSuccessCallBack"; _recipient : initiator; _amount : uint128_zero; 
    ssnaddr: ssnaddr; tossn: to_ssn; amount : amount};
    msg = one_msg msg_to_delegator;
    send msg
  end
  
end

(***************************************************)
(*                 Verifier transition             *)
(***************************************************)

(* @dev: Assign stake reward to all ssn from ssnlist. Used by verifier only. *)
(* @param ssnrewardlist: List of SSN address and cycle rewards in Qa *)
(*  CycleReward       : Uint128 *)
(*                      Integer representation of reward assigned by the verifier to this SSN for this cycle. *)
(*                      It's floor(NumberOfDSEpochsInCurrentCycle * 110,000 * VerificationPassed) *)
(* https://github.com/Zilliqa/ZIP/blob/master/zips/zip-11.md#verifier *)

(* @param initiator: The original caller who called the proxy *)
transition AssignStakeReward(ssnreward_list: List (Pair ByStr20 Uint128), initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  CallerIsVerifier initiator;
  lrc <- lastrewardcycle;
  accept;
  newLastRewardCycleNum = builtin add uint32_one lrc;
  lastrewardcycle := newLastRewardCycleNum;
  (* _amount: total rewards for ssn operator, delegators and verifier *)
  verifier_reward := _amount;
  
  total_stake_amt <- totalstakeamount;
  f = map_to_stake_rewards total_stake_amt;

  mapper = @list_map (Pair ByStr20 Uint128) SsnStakeRewardShare;
  ssn_stake_reward_list = mapper f ssnreward_list;
  forall ssn_stake_reward_list UpdateStakeReward;
  verifier_reward_amt <- verifier_reward;
  verifier_o <- verifier_receiving_addr;
  match verifier_o with
  | Some v => 
    is_zero = builtin eq verifier_reward_amt uint128_zero;
    match is_zero with
    | True =>
    | False =>
      TransferFunds addfunds_tag verifier_reward_amt v
    end
  | None =>
    e = VerifierRecvAddrNotSet;
    ThrowError e
  end

end

(***************************************************)
(*                  Generic transition             *)
(***************************************************)

(* @dev: Move funds from initiator to recipient, i.e., contract address. *)
(* @param initiator: The original caller who called the proxy. *)
transition AddFunds(initiator: ByStr20)
  IsProxy;
  accept;
  e = { _eventname : "Funds deposit "; funder : initiator };
  event e
end

(***************************************************)
(*         Contract upgrade transition             *)
(***************************************************)

(* @dev   Adds new ssn to ssnlist. Used by admin only. *)
(* @param ssnaddr: Address of the ssn to be added *)
(* @param stake_amt: Stake amount of ssn *)
(* @param rewards: Rewards of the ssn to be added *)
(* @param name: Human readable name *)
(* @param urlraw: string representing "ip:port" of the ssn serving raw api request *)
(* @param urlapi: string representing url exposed by ssn serving public api request *)
(* @param buffered_deposit: Any buffered stake deposit *)
(* @param comm: Percentage of incoming rewards that the SSN takes *)
(* @param comm_rewards: Number of ZILs earned as comm *)
(* @param min_delegate_amt: Minimum nb. of ZILs required for delegation *)
(* @param rec_addr: Address that will be used to receive comm *)
(* @param initiator: The original caller who called the proxy *)
transition AddSSNAfterUpgrade(ssnaddr: ByStr20, stake_amt: Uint128, rewards: Uint128, name: String, urlraw: String, urlapi: String, buff_deposit: Uint128,  comm: Uint128, comm_rewards: Uint128, rec_addr: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  already_exists <- exists ssnlist[ssnaddr];
  match already_exists with
  | True  =>
    e = { _eventname: "SSN already exists"; ssn_addr: ssnaddr };
    event e
  | False =>
    minstake_tmp <- minstake;
    status = uint128_le minstake_tmp stake_amt;
    s = Ssn status stake_amt rewards name urlraw urlapi buff_deposit comm comm_rewards rec_addr;
    ssnlist[ssnaddr] := s;
    e = { _eventname: "SSN added"; ssn_addr: ssnaddr };
    event e
  end
end

(* @dev: Adds or deletes a new deleg. Used by admin only during contract upgrade. *)
(* @param ssnaddr: Address of the ssn *)
(* @param deleg: Address of the deleg *)
(* @param stake_amt: Stake amount *)
(* @param initiator: The original caller who called the proxy *)
(* Its very crucial that after this operation, we should restore direct and buffered map, as well as *)
(* lastrewardcycle last_withdraw_cycle_deleg last_buf_deposit_cycle_deleg totalstakeamount *)
transition UpdateDeleg(ssnaddr: ByStr20, deleg: ByStr20, stake_amt: Uint128, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  ssn_o <- ssnlist[ssnaddr];
  minstake_tmp <- minstake;
  match ssn_o with
  | Some (Ssn active_status staking_amt deleg_reward name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    is_delete = builtin eq stake_amt uint128_zero;
    match is_delete with
    | True =>
      alr_deleg_amt_o <- deposit_amt_deleg[deleg][ssnaddr];
      match alr_deleg_amt_o with
      | Some alr_deleg =>
        TruncateDeleg deleg ssnaddr;
        new_stake_amt = builtin sub staking_amt alr_deleg;
        status = uint128_le minstake_tmp new_stake_amt;
        ssn = Ssn status new_stake_amt deleg_reward name urlraw urlapi buffdeposit comm comm_rewards rec_addr;
        ssnlist[ssnaddr] := ssn;
        e = { _eventname: "Deleg deleted"; ssn_addr: ssnaddr; deleg_address: deleg };
        event e;
        TransferFunds addfunds_tag alr_deleg deleg 
      | None =>
      end
    | False =>
      FillInDepositDelegAmt ssnaddr deleg stake_amt;
      new_stake_amt = builtin add stake_amt staking_amt;
      status = uint128_le minstake_tmp new_stake_amt;
      ssn = Ssn status new_stake_amt deleg_reward name urlraw urlapi buffdeposit comm comm_rewards rec_addr;
      ssnlist[ssnaddr] := ssn;
      e = { _eventname: "Deleg added"; ssn_addr: ssnaddr; deleg_address: deleg };
      event e
    end
  | None =>
    e = SSNNotExist;
    ThrowError e
  end
end

transition PopulateStakeSSNPerCycle(ssn_addr: ByStr20, cycle: Uint32, totalAmt: Uint128, rewards: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  info = SSNCycleInfo totalAmt rewards;
  stake_ssn_per_cycle[ssn_addr][cycle] := info
end

transition PopulateLastWithdrawCycleForDeleg(deleg_addr: ByStr20, ssn_addr: ByStr20, cycle: Uint32, initiator: ByStr20)
  IsPaused;  
  IsProxy;
  IsAdmin initiator;
  last_withdraw_cycle_deleg[deleg_addr][ssn_addr] := cycle
end

transition PopulateLastBufDepositCycleDeleg(deleg_addr: ByStr20, ssn_addr: ByStr20, cycle: Uint32, initiator: ByStr20)
  IsPaused;  
  IsProxy;
  IsAdmin initiator;
  last_buf_deposit_cycle_deleg[deleg_addr][ssn_addr] := cycle
end

transition PopulateBuffDeposit(deleg_addr: ByStr20, ssn_addr: ByStr20, cycle: Uint32, amt: Uint128, initiator: ByStr20)
  IsPaused;  
  IsProxy;
  IsAdmin initiator;
  buff_deposit_deleg[deleg_addr][ssn_addr][cycle] := amt
end

transition PopulateDirectDeposit(deleg_addr: ByStr20, ssn_addr: ByStr20, cycle: Uint32, amt: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  direct_deposit_deleg[deleg_addr][ssn_addr][cycle] := amt
end

transition PopulateDepositAmtDeleg(deleg_addr: ByStr20, ssn_addr: ByStr20, amt: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  deposit_amt_deleg[deleg_addr][ssn_addr] := amt;
  ssn_deleg_amt[ssn_addr][deleg_addr] := amt
end


transition PopulateDelegStakePerCycle(deleg_addr: ByStr20, ssn_addr: ByStr20, cycle: Uint32, amt: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  deleg_stake_per_cycle[deleg_addr][ssn_addr][cycle] := amt
end

transition PopulateLastRewardCycle(cycle: Uint32, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  lastrewardcycle := cycle
end

transition PopulateCommForSSN(ssn_addr: ByStr20, cycle: Uint32, comm: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  comm_for_ssn[ssn_addr][cycle] := comm
end

transition PopulateTotalStakeAmt(amt: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  totalstakeamount := amt
end

transition PopulatePendingWithdrawal(ssn_addr: ByStr20, block_number: BNum, stake: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  withdrawal_pending[ssn_addr][block_number] := stake
end

transition PopulateDelegSwapRequest(requestor: ByStr20, new_deleg_addr: ByStr20, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  deleg_swap_request[requestor] := new_deleg_addr
end

(* @dev:  Drain the contract's balance. Used by current admin only *)
(*        in event of contract upgrade or emergency. *)
(* @param initiator: The original caller who called the proxy *)
(* @param amt: The amount (Qa) to be drained from the contract back to the admin address *)
transition DrainContractBalance(amt: Uint128, initiator: ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator;
  bal <- _balance;
  less_than = builtin lt bal amt;
  match less_than with
  | True => throw
  | False =>
    TransferFunds addfunds_tag amt initiator
  end
end

(***************************************************)
(*           Contract state migration              *)
(***************************************************)

(* Common validation procedure for all migration transitions *)
procedure ValidateMigration (initiator : ByStr20)
  IsPaused;
  IsProxy;
  IsAdmin initiator
end

(***************************************************)

procedure MigrateCommForSsnByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field comm_for_ssn: Map ByStr20 (Map Uint32 Uint128)
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.comm_for_ssn[key];
    match old_val_opt with
    | Some old_val =>
      comm_for_ssn[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateCommForSsn (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field comm_for_ssn: Map ByStr20 (Map Uint32 Uint128)
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field comm_for_ssn: Map ByStr20 (Map Uint32 Uint128)
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateCommForSsnByKey
end

(***************************************************)

procedure MigrateDepositAmtDelegByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field deposit_amt_deleg: Map ByStr20 (Map ByStr20 Uint128)
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.deposit_amt_deleg[key];
    match old_val_opt with
    | Some old_val =>
      deposit_amt_deleg[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateDepositAmtDeleg (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field deposit_amt_deleg: Map ByStr20 (Map ByStr20 Uint128)
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field deposit_amt_deleg: Map ByStr20 (Map ByStr20 Uint128)
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateDepositAmtDelegByKey
end

(***************************************************)

procedure MigrateSsnDelegAmtByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field ssn_deleg_amt: Map ByStr20 (Map ByStr20 Uint128)
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.ssn_deleg_amt[key];
    match old_val_opt with
    | Some old_val =>
      ssn_deleg_amt[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateSsnDelegAmt (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field ssn_deleg_amt: Map ByStr20 (Map ByStr20 Uint128)
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field ssn_deleg_amt: Map ByStr20 (Map ByStr20 Uint128)
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateSsnDelegAmtByKey
end

(***************************************************)

procedure MigrateBuffDepositDelegByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field buff_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.buff_deposit_deleg[key];
    match old_val_opt with
    | Some old_val =>
      buff_deposit_deleg[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateBuffDepositDeleg (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field buff_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field buff_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateBuffDepositDelegByKey
end

(***************************************************)

procedure MigrateDirectDepositDelegByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field direct_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.direct_deposit_deleg[key];
    match old_val_opt with
    | Some old_val =>
      direct_deposit_deleg[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateDirectDepositDeleg (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field direct_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field direct_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateDirectDepositDelegByKey
end

(***************************************************)

procedure MigrateLastWithdrawCycleDelegByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field last_withdraw_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32)
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.last_withdraw_cycle_deleg[key];
    match old_val_opt with
    | Some old_val =>
      last_withdraw_cycle_deleg[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateLastWithdrawCycleDeleg (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field last_withdraw_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32)
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field last_withdraw_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32)
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateLastWithdrawCycleDelegByKey
end

(***************************************************)

procedure MigrateLastBufDepositCycleDelegByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field last_buf_deposit_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32)
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.last_buf_deposit_cycle_deleg[key];
    match old_val_opt with
    | Some old_val =>
      last_buf_deposit_cycle_deleg[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateLastBufDepositCycleDeleg (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field last_buf_deposit_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32)
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field last_buf_deposit_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32)
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateLastBufDepositCycleDelegByKey
end

(***************************************************)

procedure MigrateDelegStakePerCycleByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field deleg_stake_per_cycle: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.deleg_stake_per_cycle[key];
    match old_val_opt with
    | Some old_val =>
      deleg_stake_per_cycle[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateDelegStakePerCycle (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field deleg_stake_per_cycle: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field deleg_stake_per_cycle: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128))
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateDelegStakePerCycleByKey
end

(***************************************************)

procedure MigrateWithdrawalPendingByKey (
  arg : Pair ByStr20 (ByStr20 with contract
                                     field withdrawal_pending: Map ByStr20 (Map BNum Uint128)
                              end))
  match arg with
  | Pair key old_contract =>                          
    old_val_opt <-& old_contract.withdrawal_pending[key];
    match old_val_opt with
    | Some old_val =>
      withdrawal_pending[key] := old_val
    | None => (* Nothing to migrate *)
    end
  end
end

transition MigrateWithdrawalPending (
  initiator : ByStr20,
  keys : List ByStr20,
  old_contract : ByStr20 with contract
                                field withdrawal_pending: Map ByStr20 (Map BNum Uint128)
                         end)
  ValidateMigration initiator;
  mapper = @list_map_to_pair_with_constant ByStr20 (ByStr20 with contract
                                                                   field withdrawal_pending: Map ByStr20 (Map BNum Uint128)
                                                            end);
  paired_list = mapper keys old_contract;
  forall paired_list MigrateWithdrawalPendingByKey
end

(***************************************************)
(*                  Swap transition                *)
(***************************************************)

procedure ActualSwapDirectDeposit(direct_deposit_cycle: Pair Uint32 Uint128)
  current_ssn_o <- current_ssn;
  current_deleg_o <- current_deleg;
  new_deleg_o <- new_deleg;

  fst = @fst Uint32 Uint128;
  snd = @snd Uint32 Uint128;
  reward_cycle = fst direct_deposit_cycle;
  current_direct_deposit_amt = snd direct_deposit_cycle;

  match new_deleg_o with
  | Some new_deleg_addr =>
    match current_deleg_o with
    | Some initial_deleg =>
      match current_ssn_o with
      | Some ssn =>
        (* new deleg already has existing direct deposit on ssn *)
        new_deleg_direct_deposit_amt <- direct_deposit_deleg[new_deleg_addr][ssn][reward_cycle];
        match new_deleg_direct_deposit_amt with
        | Some new_deleg_direct_deposit =>
          new_amt = builtin add new_deleg_direct_deposit current_direct_deposit_amt;
          direct_deposit_deleg[new_deleg_addr][ssn][reward_cycle] := new_amt;
          e = { _eventname: "SwapDirectDepositExists"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn; existing_amt: current_direct_deposit_amt; transferred_amt: new_deleg_direct_deposit; new_amt: new_amt };
          event e
        | None =>
          (* new deleg has no direct deposit on ssn *)
          (* take amount from current deleg and give to new deleg *)
          direct_deposit_deleg[new_deleg_addr][ssn][reward_cycle] := current_direct_deposit_amt;
          e = { _eventname: "SwapDirectDepositNewEntry"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn; amt: current_direct_deposit_amt };
          event e
        end
      | None =>
        (* no ssn to get info from *)
      end
    | None =>
      (* no current deleg to get info from *)
    end
  | None =>
    (* no new deleg to transfer to *)
  end
end

(* @dev Swap deleg address from current_deleg -> new_deleg in direct_deposit_deleg *)
(* @see ActualSwapDirectDeposit *)
procedure SwapDirectDeposit(ssndeposit: Pair ByStr20 Uint128)
  fst = @fst ByStr20 Uint128;
  ssn_address = fst ssndeposit;
  current_deleg_o <- current_deleg;

  match current_deleg_o with
  | Some deleg =>
    direct_deposit_cycle_map <- direct_deposit_deleg[deleg][ssn_address];
    match direct_deposit_cycle_map with
    | Some direct_deposit_cycle_map_o =>
      direct_deposit_list = builtin to_list direct_deposit_cycle_map_o;
      ssn = Some {ByStr20} ssn_address;
      current_ssn := ssn;
      forall direct_deposit_list ActualSwapDirectDeposit;
      (* delete after add operation *)
      delete direct_deposit_deleg[deleg][ssn_address]
    | None => (* No direct deposit at this ssn *)
    end
  | None => (* not possible to have no existing deleg *)
  end
end

procedure ActualSwapDelegStakePerCycle(deleg_stake_cycle: Pair Uint32 Uint128)
  current_ssn_o <- current_ssn;
  current_deleg_o <- current_deleg;
  new_deleg_o <- new_deleg;

  fst = @fst Uint32 Uint128;
  snd = @snd Uint32 Uint128;
  cycle_no = fst deleg_stake_cycle;
  current_deposit_amt = snd deleg_stake_cycle;

  match new_deleg_o with
  | Some new_deleg_addr =>
    match current_deleg_o with
    | Some initial_deleg =>
      match current_ssn_o with
      | Some ssn =>
        (* new deleg already has existing deleg stake per cycle on ssn *)
        deleg_stake_deposit <- deleg_stake_per_cycle[new_deleg_addr][ssn][cycle_no];
        match deleg_stake_deposit with
        | Some stake_deposit =>
          new_amt = builtin add stake_deposit current_deposit_amt;
          deleg_stake_per_cycle[new_deleg_addr][ssn][cycle_no] := new_amt;
          e = { _eventname: "SwapDelegStakePerCycleExists"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn; existing_amt: current_deposit_amt; transferred_amt: stake_deposit; new_amt: new_amt };
          event e
        | None =>
          (* new deleg has no deleg stake per cycle on ssn *)
          (* take amount from current deleg and give to new deleg *)
          deleg_stake_per_cycle[new_deleg_addr][ssn][cycle_no] := current_deposit_amt;
          e = { _eventname: "SwapDelegStakePerCycleNewEntry"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn; amt: current_deposit_amt };
          event e
        end
      | None =>
        (* no ssn to get info from *)
      end
    | None =>
      (* no current deleg to get info from *)
    end
  | None =>
    (* no new deleg to transfer to *)
  end
end

(* @dev Swap deleg address from current_deleg -> new_deleg in deleg_stake_cycle *)
(* @see ActualSwapDelegStakePerCycle *)
procedure SwapDelegStakePerCycle(ssndeposit: Pair ByStr20 Uint128)
  fst = @fst ByStr20 Uint128;
  ssn_address = fst ssndeposit;
  current_deleg_o <- current_deleg;

  match current_deleg_o with
  | Some deleg =>
    deleg_stake_per_cycle_map <- deleg_stake_per_cycle[deleg][ssn_address];
    match deleg_stake_per_cycle_map with
    | Some deleg_stake_per_cycle_map_o =>
      deleg_stake_per_cycle_list = builtin to_list deleg_stake_per_cycle_map_o;
      ssn = Some {ByStr20} ssn_address;
      current_ssn := ssn;
      forall deleg_stake_per_cycle_list ActualSwapDelegStakePerCycle;
      (* delete after add operation *)
      delete deleg_stake_per_cycle[deleg][ssn_address]
    | None => (* No deposit at this ssn *)
    end
  | None => (* not possible to have no existing deleg *)
  end
end

(* @dev Swap deleg address from current_deleg -> new_deleg in deposit_amt_deleg *)
procedure SwapDepositAmtDeleg(ssndeposit: Pair ByStr20 Uint128)
  fst = @fst ByStr20 Uint128;
  ssn_address = fst ssndeposit;
  current_deleg_o <- current_deleg;
  new_deleg_o <- new_deleg;

  match current_deleg_o with
  | Some initial_deleg =>
    deposit_deleg_amt <- deposit_amt_deleg[initial_deleg][ssn_address];
    match deposit_deleg_amt with
    | Some deposit_amt =>
      match new_deleg_o with
      | Some new_deleg_addr =>
        current_deposit_deleg_amt <- deposit_amt_deleg[new_deleg_addr][ssn_address];
        match current_deposit_deleg_amt with
        | Some existing_deposit_amt =>
          (* new deleg already has an existing deposit_amt_deleg entry *)
          new_amt = builtin add existing_deposit_amt deposit_amt;
          deposit_amt_deleg[new_deleg_addr][ssn_address] := new_amt;
          delete deposit_amt_deleg[initial_deleg][ssn_address];
          e = { _eventname: "SwapDepositAmtDelegExists"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; existing_amt: existing_deposit_amt; transferred_amt: deposit_amt; new_amt: new_amt };
          event e
        | None =>
          (* new deleg has no deposit deleg amt on ssn *)
          (* take amount from current deleg and give to new deleg *)
          deposit_amt_deleg[new_deleg_addr][ssn_address] := deposit_amt;
          delete deposit_amt_deleg[initial_deleg][ssn_address];
          e = { _eventname: "SwapDepositAmtDelegNewEntry"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; amt: deposit_amt };
          event e
        end
      | None => (* no new deleg to transfer to *)
      end
    | None => (* No deposit at this ssn *)
    end
  | None => (* not possible to have no existing deleg *)
  end
end

(* @dev Swap deleg address from current_deleg -> new_deleg in ssn_deleg_amt *)
procedure SwapSSNDelegAmt(ssndeposit: Pair ByStr20 Uint128)
  fst = @fst ByStr20 Uint128;
  ssn_address = fst ssndeposit;
  current_deleg_o <- current_deleg;
  new_deleg_o <- new_deleg;

  match current_deleg_o with
  | Some initial_deleg =>
    ssn_deleg_deposit <- ssn_deleg_amt[ssn_address][initial_deleg];
    match ssn_deleg_deposit with
    | Some ssn_deleg_deposit_amt =>
      match new_deleg_o with
      | Some new_deleg_addr =>
        new_ssn_deleg_amt <- ssn_deleg_amt[ssn_address][new_deleg_addr];
        match new_ssn_deleg_amt with
        | Some existing_deleg_amt =>
          new_amt = builtin add existing_deleg_amt ssn_deleg_deposit_amt;
          ssn_deleg_amt[ssn_address][new_deleg_addr] := new_amt;
          delete ssn_deleg_amt[ssn_address][initial_deleg];
          e = { _eventname: "SwapSSNDelegAmtExists"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; existing_amt: existing_deleg_amt; transferred_amt: ssn_deleg_deposit_amt; new_amt: new_amt };
          event e
        | None =>
          (* new deleg has no deposit deleg amt on ssn *)
          (* take amount from current deleg and give to new deleg *)
          ssn_deleg_amt[ssn_address][new_deleg_addr] := ssn_deleg_deposit_amt;
          delete ssn_deleg_amt[ssn_address][initial_deleg];
          e = { _eventname: "SwapSSNDelegAmtNewEntry"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; amt: ssn_deleg_deposit_amt };
          event e
        end
      | None => (* no new deleg to transfer to *)
      end
    | None => (* No deleg deposit for this ssn *)
    end
  | None => (* not possible to have no existing deleg *)
  end
end

(* @dev Swap deleg address from current_deleg -> new_deleg in last_withdraw_cycle_deleg *)
(* Both parties have been asserted to have no buffered deposits or rewards; lwcd should be identical or one-off lrc *)
(* If current_deleg and new_deleg has same ssn, don't replace new_deleg entry *)
procedure SwapLastWithdrawCycleDeleg(ssndeposit: Pair ByStr20 Uint128)
  fst = @fst ByStr20 Uint128;
  ssn_address = fst ssndeposit;
  current_deleg_o <- current_deleg;
  new_deleg_o <- new_deleg;

  match current_deleg_o with
  | Some initial_deleg =>
    lwcd <- last_withdraw_cycle_deleg[initial_deleg][ssn_address];
    match lwcd with
    | Some requestor_lwcd =>
      match new_deleg_o with
      | Some new_deleg_addr =>
        new_deleg_lwcd <- last_withdraw_cycle_deleg[new_deleg_addr][ssn_address];
        match new_deleg_lwcd with
        | Some existing_lwcd =>
          (* new deleg has delegate same ssn as requestor *)
          (* don't replace; already assert no buffered deposit and rewards for both requestor and new_deleg  *)
          (* requestor lwcd should be similar to new_deleg lwcd *)
          delete last_withdraw_cycle_deleg[initial_deleg][ssn_address];
          e = { _eventname: "SwapLastWithdrawCycleDelegExists"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; existing_lwcd: existing_lwcd };
          event e
        | None =>
          (* new deleg has no last withdraw cycle for this ssn *)
          last_withdraw_cycle_deleg[new_deleg_addr][ssn_address] := requestor_lwcd;
          delete last_withdraw_cycle_deleg[initial_deleg][ssn_address];
          e = { _eventname: "SwapLastWithdrawCycleDelegNewEntry"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; lwcd: requestor_lwcd };
          event e
        end
      | None => (* no new deleg to transfer to *)
      end
    | None => (* No last withdraw cycle for this ssn *)
    end
  | None => (* not possible to have no existing deleg *)
  end
end

(* @dev Swap deleg address from current_deleg -> new_deleg in last_buf_deposit_cycle_deleg *)
(* Both parties have been asserted to have no buffered deposits or rewards; lbdc should be identical or one-off lrc *)
(* If current_deleg and new_deleg has same ssn, don't replace new_deleg entry *)
procedure SwapLastBuffDepositCycleDeleg(ssndeposit: Pair ByStr20 Uint128)
  fst = @fst ByStr20 Uint128;
  ssn_address = fst ssndeposit;
  current_deleg_o <- current_deleg;
  new_deleg_o <- new_deleg;

  match current_deleg_o with
  | Some initial_deleg =>
    lbdc <- last_buf_deposit_cycle_deleg[initial_deleg][ssn_address];
    match lbdc with
    | Some requestor_lbdc =>
      match new_deleg_o with
      | Some new_deleg_addr =>
        new_deleg_lbdc <- last_buf_deposit_cycle_deleg[new_deleg_addr][ssn_address];
        match new_deleg_lbdc with
        | Some existing_lbdc =>
          (* new deleg has delegate same ssn as requestor *)
          (* don't replace; already assert no buffered deposit and rewards for both requestor and new_deleg  *)
          delete last_buf_deposit_cycle_deleg[initial_deleg][ssn_address];
          e = { _eventname: "SwapLastBuffDepositCycleDelegExists"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; existing_lbdc: existing_lbdc };
          event e
        | None =>
          (* new deleg has no last buff deposit for this ssn *)
          last_buf_deposit_cycle_deleg[new_deleg_addr][ssn_address] := requestor_lbdc;
          delete last_buf_deposit_cycle_deleg[initial_deleg][ssn_address];
          e = { _eventname: "SwapLastBuffDepositCycleDelegNewEntry"; initial_deleg: initial_deleg; new_deleg: new_deleg_addr; ssn_addr: ssn_address; lbdc: requestor_lbdc };
          event e
        end
      | None => (* no new deleg to transfer to *)
      end
    | None => (* requestor has no last buff deposit cycle at this ssn *)
    end
  | None => (* not possible to have no existing deleg *)
  end
end

(* @dev Swap deleg address from current_deleg -> new_deleg in withdrawal_pending *)
procedure SwapPendingWithdrawal(blk_deposit_cycle: Pair BNum Uint128)
  current_deleg_o <- current_deleg;
  new_deleg_o <- new_deleg;
  fst = @fst BNum Uint128;
  snd = @snd BNum Uint128;
  blk_num = fst blk_deposit_cycle;
  deposit = snd blk_deposit_cycle;
  
  match new_deleg_o with
  | Some new_deleg_addr =>
    new_deleg_pending_withdrawal <- withdrawal_pending[new_deleg_addr][blk_num];
    match new_deleg_pending_withdrawal with
    | Some existing_deposit =>
      (* new deleg has exisiting blk_num *)
      new_deposit = builtin add existing_deposit deposit;
      withdrawal_pending[new_deleg_addr][blk_num] := new_deposit;
      e = { _eventname: "SwapPendingWithdrawalExists"; initial_deleg: current_deleg_o; new_deleg: new_deleg_addr; existing_deposit: existing_deposit; new_deposit: new_deposit };
      event e
    | None =>
      (* new deleg has no blk_num entry*)
      withdrawal_pending[new_deleg_addr][blk_num] := deposit;
      e = { _eventname: "SwapPendingWithdrawalNewEntry"; initial_deleg: current_deleg_o; new_deleg: new_deleg_addr; deposit: deposit };
      event e
    end
  | None => (* no new deleg to transfer to *)
  end
end

(* @dev Clears the mutable addresses after use *)
procedure SwapCleanUp()
  r = Some {ByStr20} reset_addr;
  current_deleg := r;
  current_ssn := r;
  new_deleg := r
end

(* @dev Change a delegator's stake from initiator -> new_deleg_addr. *)
(* not swapping buff_deposit_deleg because there is pre-assertion that requestor has no buff deposits *)
procedure SwapDelegator(requestor: ByStr20, new_deleg_addr: ByStr20)
  c = Some {ByStr20} requestor;
  current_deleg := c;
  n = Some {ByStr20} new_deleg_addr;
  new_deleg := n;

  (* get the list of requestor's ssn *)
  ssn_deposit_map <- deposit_amt_deleg[requestor];
  match ssn_deposit_map with
   | Some ssn_deposit_entry =>
     ssn_deposit_list = builtin to_list ssn_deposit_entry;
     (* swap *)
     forall ssn_deposit_list SwapDirectDeposit;
     forall ssn_deposit_list SwapDelegStakePerCycle;
     forall ssn_deposit_list SwapDepositAmtDeleg;
     forall ssn_deposit_list SwapSSNDelegAmt;
     forall ssn_deposit_list SwapLastBuffDepositCycleDeleg;
     forall ssn_deposit_list SwapLastWithdrawCycleDeleg
   | None => (* nothing to swap *)
  end;
  
  (* swap pending withdrawal *)
  match c with
  | Some initial_deleg =>
    deleg_blk_map <- withdrawal_pending[initial_deleg];
    match deleg_blk_map with
    | Some deleg_blk_entry =>
      cycle_reward_list = builtin to_list deleg_blk_entry;
      forall cycle_reward_list SwapPendingWithdrawal;
      delete withdrawal_pending[initial_deleg]
    | None => (* no pending withdrawal *)
    end
  | None => (* not possible to have no existing deleg *)
  end
end

(* checks if there exists A -> B to prevent B -> A due to potential cyclic swap issue *)
(* if there is A -> B, and B -> A, then a cyclic swap issue may occur deppending on who accepts first *)
(* A -> (B) -> A, A is final inheritor *)
(* B -> (A) -> B, B is final inheritor *)
(* to prevent this scenario, prevent B -A from happening *)
procedure IsNotCyclicSwap(initiator: ByStr20, new_deleg_addr: ByStr20)
 cyclic_initiator <- deleg_swap_request[new_deleg_addr];
 match cyclic_initiator with
 | Some addr =>
   (* is there a B -> X, where X == A? *)
   is_cyclic_request = builtin eq addr initiator;
   match is_cyclic_request with
   | True =>
     e = SwapAddrAlreadyExistsAsRequest;
     ThrowError e
   | False =>
   end
 | None =>
 end
end

(* check for A -> A request *)
procedure IsNotSelfSwap(initiator: ByStr20, new_deleg_addr: ByStr20)
  is_identical_addr = builtin eq initiator new_deleg_addr;
  match is_identical_addr with
  | True =>
    e = InvalidSwapAddr;
    ThrowError e
  | False =>
  end
end

(* checks if new delegator matches that of stored request *)
procedure IsValidSwapAddr(requestor: ByStr20, new_deleg_addr: ByStr20)
  swap_addr <- deleg_swap_request[requestor];
  match swap_addr with
  | Some requestor_swap_addr =>
    is_new_deleg_valid = builtin eq requestor_swap_addr new_deleg_addr;
    match is_new_deleg_valid with
    | True => (* new_deleg address matches requestor swap address *)
    | False =>
      (* throw error - requestor swap address is different *)
      e = SwapAddrValidationFailed;
      ThrowError e
    end
  | None => (* throw error *)
    e = InvalidSwapAddr;
    ThrowError e
  end
end

procedure AssertSwapNoBufferedAndRewards(ssndeposit: Pair ByStr20 Uint128)
  current_deleg_o <- current_deleg;
  fst = @fst ByStr20 Uint128;
  ssn_address = fst ssndeposit;
  ssn_o <- ssnlist[ssn_address];

  match ssn_o with
  | Some (Ssn active_status stake_amt rewards name urlraw urlapi buffdeposit comm comm_rewards rec_addr) =>
    match current_deleg_o with
    | Some requestor =>
      AssertNoRewards ssn_address requestor rewards;
      AsseertNoBufferedDeposit ssn_address requestor;
      AssertNoBufferedDepositLessOneCycle ssn_address requestor
    | None =>
    end
  | None =>
  end
end

(* checks if the requestor has buffered deposit or rewards *)
procedure AssertNoBufferedAndRewards(requestor : ByStr20)
  c = Some {ByStr20} requestor;
  current_deleg := c;
  (* get the list of requestor's ssn *)
  ssn_deposit_map <- deposit_amt_deleg[requestor];
  match ssn_deposit_map with
   | Some ssn_deposit_entry =>
     ssn_deposit_list = builtin to_list ssn_deposit_entry;
     forall ssn_deposit_list AssertSwapNoBufferedAndRewards
   | None =>
  end
end

(* @dev: Creates a request to another delegator to indicate interest in transferring all stakes, rewards etc to the delegator *)
(* @param new_deleg_addr: Address of the new deleg that will be receiving all the stakes from requestor *)
(* @param initiator: Address of the requestor; the one who call the proxy *)
(* requestor can override the new deleg address by sending a new request *)
transition RequestDelegatorSwap(new_deleg_addr: ByStr20, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  IsNotSelfSwap initiator new_deleg_addr;
  IsNotCyclicSwap initiator new_deleg_addr;
  (* both requestor and new_deleg should not have buffered deposit or rewards, mitigate lbcd and lwcd issues *)
  AssertNoBufferedAndRewards initiator;
  AssertNoBufferedAndRewards new_deleg_addr;
  deleg_swap_request[initiator] := new_deleg_addr;
  e = { _eventname: "RequestDelegatorSwap"; initial_deleg: initiator; new_deleg: new_deleg_addr };
  event e
end

(* @dev: Accepts a swap request from a requestor. *)
(* Once confirmed, everything which was under the requestor would be transferred over to the new deleg *)
(* @param requestor: Address of the one that creates the swap request *)
(* @param initiator: Address of the new_deleg confirming the request *)
(* Transfer cannot be reverted once confirmed *)
transition ConfirmDelegatorSwap(requestor: ByStr20, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  IsValidSwapAddr requestor initiator;
  (* both requestor and new_deleg should not have buffered deposit or rewards, mitigate lbcd and lwcd issues *)
  AssertNoBufferedAndRewards requestor;
  AssertNoBufferedAndRewards initiator;
  SwapDelegator requestor initiator;
  SwapCleanUp;
  (* delete the requestor's deleg key from these maps; requestor's ssnaddr key already deleted in the Swap proc *)
  CleanDirectDepositDelegAddr requestor;
  CleanDelegStakePerCycleDelegAddr requestor;
  CleanDepositAmtDelegAddr requestor;
  CleanLastWithdrawCycleDelegAddr requestor;
  CleanLastBuffDepositCycleDelegAddr requestor;
  delete deleg_swap_request[requestor];
  e = { _eventname: "ConfirmDelegatorSwap"; initial_deleg: requestor; new_deleg: initiator };
  event e
end

(* @dev: Revokes a swap request. *)
(* for requestor use *)
(* @param initiator: Address of requestor who wants to revoke the swap process *)
transition RevokeDelegatorSwap(initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  swap_addr <- deleg_swap_request[initiator];
  match swap_addr with
  | Some requestor_swap_addr =>
    delete deleg_swap_request[initiator];
    e = { _eventname: "RevokeDelegatorSwap"; initial_deleg: initiator; new_deleg: requestor_swap_addr };
    event e
  | None =>
    e = InvalidSwapAddr;
    ThrowError e
  end
end

(* @dev: Rejects a swap request from a requestor. *)
(* for swap recipient use *)
(* Once rejected, requestor must create swap request again *)
(* @param requestor: Address of the one that creates the swap request *)
(* @param initiator: Address of the new_deleg rejecting the request *)
transition RejectDelegatorSwap(requestor: ByStr20, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  IsValidSwapAddr requestor initiator;
  delete deleg_swap_request[requestor];
  e = { _eventname: "RejectDelegatorSwap"; requestor: requestor; new_deleg: initiator };
  event e
end