scilla_version 0

import ListUtils IntUtils PairUtils

library SSNList

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

type SsnStakeRewardShare = 
| SsnStakeRewardShare of ByStr20 Uint128 Uint128


type SSNCycleInfo =
| SSNCycleInfo of Uint128 Uint128


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

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

let is_ssn_cycle_map_empty =
  fun(m : Map ByStr20 Uint32) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

let is_ssn_deposit_map_empty =
  fun(m : Map ByStr20 Uint128) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

let is_block_deposit_map_empty =
  fun(m : Map BNum Uint128) =>
    let map_size = builtin size m in
    builtin eq map_size uint32_zero

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

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"

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 }

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
    
contract SSNList(
  init_admin: ByStr20,
  init_proxy_address: ByStr20,
  init_gzil_address: ByStr20
)

field ssnlist: Map ByStr20 Ssn = Emp ByStr20 Ssn

field comm_for_ssn: Map ByStr20 (Map Uint32 Uint128) = Emp ByStr20 (Map Uint32 Uint128)

field deposit_amt_deleg: Map ByStr20 (Map ByStr20 Uint128) = Emp ByStr20 (Map ByStr20 Uint128)

field ssn_deleg_amt: Map ByStr20 (Map ByStr20 Uint128) = Emp ByStr20 (Map ByStr20 Uint128)

field buff_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128)) = Emp ByStr20 (Map ByStr20 (Map Uint32 Uint128))

field direct_deposit_deleg: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128)) = Emp ByStr20 (Map ByStr20 (Map Uint32 Uint128))

field last_withdraw_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32) = Emp ByStr20 (Map ByStr20 Uint32)

field last_buf_deposit_cycle_deleg: Map ByStr20 (Map ByStr20 Uint32) = Emp ByStr20 (Map ByStr20 Uint32)

field stake_ssn_per_cycle: Map ByStr20 (Map Uint32 SSNCycleInfo) = Emp ByStr20 (Map Uint32 SSNCycleInfo)

field deleg_stake_per_cycle: Map ByStr20 (Map ByStr20 (Map Uint32 Uint128)) = Emp ByStr20 (Map ByStr20 (Map Uint32 Uint128))

field withdrawal_pending: Map ByStr20 (Map BNum Uint128) = Emp ByStr20 (Map BNum Uint128)

field deleg_swap_request: Map ByStr20 ByStr20 = Emp ByStr20 ByStr20

field bnum_req: Uint128 = Uint128 35000

field cycle_rewards_deleg: Uint128 = uint128_zero

field verifier_reward: Uint128 = uint128_zero

field available_withdrawal: Uint128 = uint128_zero

field current_deleg: Option ByStr20 = None {ByStr20}

field current_ssn: Option ByStr20 = None {ByStr20}

field new_deleg: Option ByStr20 = None {ByStr20}

field verifier: Option ByStr20 = None {ByStr20}

field verifier_receiving_addr: Option ByStr20 = None {ByStr20}

field minstake: Uint128 = Uint128 10000000000000000000

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

field maxcommchangerate: Uint128 = uint128_one

field maxcommrate: Uint128 = Uint128 1000000000
field totalstakeamount: Uint128 = uint128_zero


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

procedure IsProxy()
  is_proxy = builtin eq _sender init_proxy_address;
  match is_proxy with
  | True  =>
  | False =>
    e = ProxyValidationFailed;
    ThrowError e
  end
end

procedure IsNotPaused()
  paused_tmp <- paused;
  match paused_tmp with
  | False =>
  | True  =>
    e = ContractFrozenFailure;
    ThrowError e
  end
end

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

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

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

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

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 Pause(initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  paused := bool_active
end

transition UnPause(initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  paused := bool_inactive
end

transition UpdateAdmin(admin: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  staging_admin = Some {ByStr20} admin;
  stagingcontractadmin := staging_admin
end

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

transition UpdateVerifier(verif: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  newverifier = Some {ByStr20} verif;
  verifier := newverifier
end

transition UpdateVerifierRewardAddr(addr: ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  newAddr = Some {ByStr20} addr;
  verifier_receiving_addr := newAddr
end

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

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

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

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

transition CleanDepositAmt(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanDepositAmtDelegAddr
end

transition CleanPendingWithdrawal(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanPendingWithdrawalDelegAddr
end

transition CleanLastWithdrawCycle(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanLastWithdrawCycleDelegAddr
end

transition CleanLastBuffDepositCycle(deleg_addr_list: List ByStr20, initiator: ByStr20)
  IsProxy;
  IsAdmin initiator;
  forall deleg_addr_list CleanLastBuffDepositCycleDelegAddr
end


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

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

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


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

transition WithdrawStakeRewards(ssnaddr: ByStr20, initiator: ByStr20)
  IsNotPaused;
  IsProxy;
  DelegExists ssnaddr initiator;
  WithdrawalStakeRewards initiator ssnaddr
end

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

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

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



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


transition AddFunds(initiator: ByStr20)
  IsProxy;
  accept;
  e = { _eventname : "Funds deposit "; funder : initiator };
  event e
end




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

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

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

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

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

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

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

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

procedure SwapCleanUp()
  r = Some {ByStr20} reset_addr;
  current_deleg := r;
  current_ssn := r;
  new_deleg := r
end

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

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

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

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

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

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

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

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

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