/ synthesizer / program / src / resources / credits.alpha
credits.alpha
   1  // Copyright (c) 2019-2025 Provable Inc.
   2  // This file is part of the snarkVM library.
   3  
   4  // Licensed under the Apache License, Version 2.0 (the "License");
   5  // you may not use this file except in compliance with the License.
   6  // You may obtain a copy of the License at:
   7  
   8  // http://www.apache.org/licenses/LICENSE-2.0
   9  
  10  // Unless required by applicable law or agreed to in writing, software
  11  // distributed under the License is distributed on an "AS IS" BASIS,
  12  // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  13  // See the License for the specific language governing permissions and
  14  // limitations under the License.
  15  
  16  /********************************************** INVARIANTS ************************************************************/
  17  
  18  // 1. contains committee[r0] =>
  19  //   a. contains delegated[r0]
  20  //      - The set of delegated addresses is superset of active validators.
  21  // 2. delegated[*] >= 10,000
  22  //   a. contain bonded[*].microcredits >= 10,000
  23  //      - Delegators can bond to any address with the 10,000 credit minimum
  24  // 3. delegated[r0] < 10,000,000 =>
  25  //   a. !contain committee[r0]
  26  //      - If the delegated total (which includes the self bond) is less than 10,000,000 credits, it won't be in the committee
  27  // 4. bond[r0].validator == r0 =>
  28  //   a. contains committee[r0]
  29  //     - Self bonded addresses are always active validators. Delegators **can** force validators to unbond by removing sufficient delegation
  30  // 5. committee[r0] =>
  31  //   a. bonded[r0].microcredits >= 100 credits
  32  //      - Self bonded addresses are always active validators with at least 100 credits self bonded
  33  //   b. delegated[r0] >= 10,000,000 credits
  34  //      - The total delegated amount for an active validator is at least 10,000,000 credits
  35  // 6. delegated[r0] == sum bond[*].microcredits by bond[].validator == r0
  36  // 7. bond[r0].microcredits < 10,000 =>
  37  //   a. bond[r0].validator == r0
  38  //   b. contains committee[r0]
  39  //   - A bond value < 10,000 implies self-bonded active validator.
  40  // 8. bond[r0].validator != r0 =>
  41  //   a. bond[r0].microcredits >= 10,000
  42  // 9. count bonded[] - count committee[] == metadata[ax1qgqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqavzal6]
  43  //   - Delegator count consistent with metadata.
  44  // 10. count committee[] == metadata[ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd]
  45  // 11. 100,000 + count committee[] >= count bonded[] >= count delegated[] >= count committee[]
  46  // 12. bond[*].microcredits > 100
  47  
  48  
  49  /**********************************************************************************************************************/
  50  
  51  program credits.alpha;
  52  
  53  /**********************************************************************************************************************/
  54  
  55  /// The `committee` mapping contains the active validator set and their corresponding stake.
  56  mapping committee:
  57      // The key represents the address of the validator.
  58      key as address.public;
  59      // The value represents the committee state of the validator.
  60      value as committee_state.public;
  61  
  62  // The `committee_state` struct tracks the total stake of the validator, and whether they are open to new stakers.
  63  struct committee_state:
  64      // The boolean flag indicating if the validator is open to new stakers.
  65      is_open as boolean;
  66      // The percentage amount (from 0 to 100, inclusive) of rewards that retained by the validator.
  67      commission as u8;
  68  
  69  /**********************************************************************************************************************/
  70  
  71  // The `delegated` mapping tracks the total amount of microcredits that are prebonded and bonded to validator addresses.
  72  // Note: The mapping includes both prebonded and bonded microcredits. However, it does not contain unbonding microcredits.
  73  mapping delegated:
  74      // The key represents the address of the validator.
  75      key as address.public;
  76      // The value represents the amount of microcredits bonded to the validator, by the validator and its delegators.
  77      value as u64.public;
  78  
  79  /**********************************************************************************************************************/
  80  
  81  /// The `metadata` mapping stores:
  82  ///   - The number of members in the committee.
  83  ///   - The number of delegators.
  84  mapping metadata:
  85      // The key represents the index at which the count is stored.
  86      //    - This address (ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd) stores the number of **members** in the committee.
  87      //    - This address (ax1qgqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqavzal6) stores the number of **delegators**.
  88      key as address.public;
  89      // The value represents the count.
  90      value as u32.public;
  91  
  92  /**********************************************************************************************************************/
  93  
  94  // The `bonded` mapping represents the amount of microcredits that are currently bonded.
  95  mapping bonded:
  96      // The key represents the address of the staker, which includes the validators and their delegators.
  97      key as address.public;
  98      // The value represents the bond state.
  99      value as bond_state.public;
 100  
 101  // The `bond_state` struct tracks the amount of microcredits that are currently bonded to the specified validator.
 102  struct bond_state:
 103      // The address of the validator.
 104      validator as address;
 105      // The amount of microcredits that are currently bonded to the specified validator.
 106      microcredits as u64;
 107  
 108  /**********************************************************************************************************************/
 109  
 110  // The `unbonding` mapping contains a set of stakers with their unbonding microcredits and unlock height.
 111  mapping unbonding:
 112      // The key represents the address of the staker, which includes the validators and their delegators.
 113      key as address.public;
 114      // The value represents the unbond state.
 115      value as unbond_state.public;
 116  
 117  // The `unbond_state` struct tracks the microcredits that are currently unbonding, along with the unlock height.
 118  struct unbond_state:
 119      // The amount of microcredits that are currently unbonding.
 120      microcredits as u64;
 121      // The block height at which the unbonding will be complete, and can be claimed.
 122      height as u32;
 123  
 124  /**********************************************************************************************************************/
 125  
 126  // The `account` mapping is used to store credits publicly.
 127  mapping account:
 128      // The key represents the address of the owner.
 129      key as address.public;
 130      // The value represents the amount of public microcredits that belong to the specified owner.
 131      value as u64.public;
 132  
 133  /**********************************************************************************************************************/
 134  
 135  // The `withdraw` mapping contains the staking address and their corresponding withdrawal address.
 136  mapping withdraw:
 137      // The key represents the staking address of the owner.
 138      key as address.public;
 139      // The value represents the withdrawal address of the owner.
 140      value as address.public;
 141  
 142  /**********************************************************************************************************************/
 143  
 144  mapping pool:
 145      // The key represents the index at which the count is stored.
 146      //    - This address (ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd) stores the number of microcredits
 147      //      that have been migrated into the pool for records after the inclusion upgrade.
 148      key as address.public;
 149      // The value represents the amount of microcredits in the pool.
 150      value as u64.public;
 151  
 152  /**********************************************************************************************************************/
 153  
 154  // The `credits` record is used to store credits privately.
 155  record credits:
 156      // The address of the owner.
 157      owner as address.private;
 158      // The amount of private microcredits that belong to the specified owner.
 159      microcredits as u64.private;
 160  
 161  /**********************************************************************************************************************/
 162  
 163  // This function allows a validator to bond their microcredits to themselves and specify a withdrawal address
 164  // and commission percentage.
 165  //
 166  // The commission percentage is the portion of rewards that the validator may claim for itself.
 167  // Note: Setting the commission percentage to 100 results in all rewards being retained for the validator.
 168  //
 169  // The corresponding functions for 'bond_validator' are 'unbond_public' and 'claim_unbond_public'.
 170  function bond_validator:
 171      // Input the withdrawal address.
 172      input r0 as address.public;
 173      // Input the amount of microcredits to bond.
 174      input r1 as u64.public;
 175      // Input the commission percentage.
 176      input r2 as u8.public;
 177  
 178      // Ensure the withdrawal address is not the validator address.
 179      assert.neq self.signer r0;
 180  
 181      // Determine if the amount is at least 1 credit.
 182      gte r1 1_000_000u64 into r3;
 183      // Enforce the amount is at least 1 credit.
 184      assert.eq r3 true;
 185  
 186      // Ensure the commission percentage does not exceed 100%.
 187      gt r2 100u8 into r4;
 188      assert.neq r4 true;
 189  
 190      // Bond the specified amount of microcredits to the specified validator.
 191      async bond_validator self.signer r0 r1 r2 into r5;
 192      // Output the finalize future.
 193      output r5 as credits.alpha/bond_validator.future;
 194  
 195  finalize bond_validator:
 196      // Input the validator's address.
 197      input r0 as address.public;
 198      // Input the withdrawal address.
 199      input r1 as address.public;
 200      // Input the amount of microcredits to bond.
 201      input r2 as u64.public;
 202      // Input the commission percentage.
 203      input r3 as u8.public;
 204  
 205      // Retrieve the withdrawal address for the validator.
 206      get.or_use withdraw[r0] r1 into r4;
 207      // Ensure that the withdrawal address is consistent.
 208      assert.eq r1 r4;
 209  
 210      // Construct the initial committee state.
 211      // Note: We set the initial 'is_open' state to 'true'.
 212      cast true r3 into r5 as committee_state;
 213      // Retrieve the committee state of the specified validator.
 214      get.or_use committee[r0] r5 into r6;
 215  
 216      // Ensure the commission percentage remains unchanged.
 217      // Note: The commission percentage can only be set when the validator bonds for the first time.
 218      assert.eq r3 r6.commission;
 219  
 220      /* Bonded */
 221  
 222      // Construct the initial bond state.
 223      cast r0 0u64 into r7 as bond_state;
 224      // Get the bond state for the signer, or default to the initial bond state.
 225      get.or_use bonded[r0] r7 into r8;
 226      // Enforce the validator matches in the bond state.
 227      assert.eq r8.validator r0;
 228  
 229      // Increment the amount of microcredits for the bond state.
 230      add r8.microcredits r2 into r9;
 231      // Construct the updated bond state.
 232      cast r0 r9 into r10 as bond_state;
 233  
 234      /* Delegated */
 235  
 236      // Include total pre-delegated amount when deciding if validator has enough credits to join committee.
 237      // First get the current delegated amount, or start with 0 if none delegated.
 238      get.or_use delegated[r0] 0u64 into r11;
 239      // Self-bond amount + existing delegated amount = total bond.
 240      add r2 r11 into r12;
 241      // Determine if the amount is at least 10 million credits.
 242      gte r12 10_000_000_000_000u64 into r13;
 243      // Enforce the amount is at least 10 million credits.
 244      assert.eq r13 true;
 245  
 246      /* Account */
 247  
 248      // Get the balance of the signer.
 249      // If the account does not exist, this finalize scope will fail.
 250      get account[r0] into r14;
 251      // Decrement the balance of the signer.
 252      sub r14 r2 into r15;
 253  
 254      /* Writes */
 255  
 256      // if (new_validator)
 257      contains committee[r0] into r16;
 258      branch.eq r16 true to validator_in_committee;
 259      // {
 260          // Set the withdrawal address.
 261          // Note: This operation is only necessary on the first time for a validator entry, in order to initialize the value.
 262          set r4 into withdraw[r0];
 263  
 264          // Check if the initial bond amount is at least 100 credits.
 265          gte r2 100_000_000u64 into r17;
 266          // Ensure that the initial bond is at least 100 credits.
 267          assert.eq r17 true;
 268  
 269          // Get the committee size.
 270          get.or_use metadata[ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd] 0u32 into r18;
 271          // Increment the committee size by one.
 272          add r18 1u32 into r19;
 273          // Set the new committee size.
 274          set r19 into metadata[ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd];
 275  
 276          // Check if the validator exists in the unbonding state.
 277          contains unbonding[r0] into r20;
 278          // Ensure the validator currently is not unbonding.
 279          assert.eq r20 false;
 280      // }
 281  
 282      position validator_in_committee;
 283  
 284      // Update the committee state of the specified validator.
 285      set r6 into committee[r0];
 286      // Update the delegated amount.
 287      set r12 into delegated[r0];
 288      // Update the bond state for the signer.
 289      set r10 into bonded[r0];
 290      // Update the balance of the signer.
 291      set r15 into account[r0];
 292  
 293  /**********************************************************************************************************************/
 294  
 295  // This function allows any delegator to bond their microcredits to a validator and specify a withdrawal address.
 296  //
 297  // The declared validator is **not** required to be in the committee yet, however it may **not** be unbonding.
 298  // This function enforces a minimum of 10,000 credits for each delegator.
 299  // The maximum number of delegators allowed in the committee is 100,000 delegator addresses.
 300  //
 301  // The corresponding functions for 'bond_public' are 'bond_validator', 'unbond_public', and 'claim_unbond_public'.
 302  function bond_public:
 303      // Input the validator's address.
 304      input r0 as address.public;
 305      // Input the withdrawal address.
 306      input r1 as address.public;
 307      // Input the amount of microcredits to bond.
 308      input r2 as u64.public;
 309  
 310      // Determine if the amount is at least one credit.
 311      gte r2 1_000_000u64 into r3;
 312      // Enforce the amount is at least one credit.
 313      assert.eq r3 true;
 314  
 315      // Do not allow self-bonding. Validators start with bond_validator.
 316      assert.neq self.caller r0;
 317  
 318      // Bond the specified amount of microcredits to the specified validator.
 319      async bond_public self.caller r0 r1 r2 into r4;
 320      // Output the finalize future.
 321      output r4 as credits.alpha/bond_public.future;
 322  
 323  finalize bond_public:
 324      // Input the staker's address.
 325      input r0 as address.public;
 326      // Input the validator's address.
 327      input r1 as address.public;
 328      // Input the withdrawal address.
 329      input r2 as address.public;
 330      // Input the amount of microcredits to bond.
 331      input r3 as u64.public;
 332  
 333      // Retrieve the withdrawal address for the staker.
 334      get.or_use withdraw[r0] r2 into r4;
 335      // Ensure that the withdrawal address is consistent.
 336      assert.eq r2 r4;
 337  
 338      // Check if the delegator is already bonded to the validator.
 339      contains bonded[r0] into r5;
 340      branch.eq r5 true to continue_bond_delegator;
 341      // {
 342          // Set the withdrawal address.
 343          // Note: This operation is only necessary on the first time for a staker entry, in order to initialize the value.
 344          set r2 into withdraw[r0];
 345  
 346          // Ensure that the validator is open to new stakers. By default, `is_open` is set to `true`.
 347          cast true 0u8 into r6 as committee_state;
 348          get.or_use committee[r1] r6 into r7;
 349          assert.eq r7.is_open true;
 350  
 351          // Get the number of delegators.
 352          get.or_use metadata[ax1qgqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqavzal6] 0u32 into r8;
 353          // Increment the number of bonded delegators by one.
 354          add r8 1u32 into r9;
 355          // Determine if the number of delegators is less than or equal to 100_000.
 356          lte r9 100_000u32 into r10;
 357          // Enforce that the number of delegators is less than or equal to 100_000.
 358          assert.eq r10 true;
 359          // Set the new number of delegators.
 360          set r9 into metadata[ax1qgqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqavzal6];
 361      // }
 362  
 363      position continue_bond_delegator;
 364  
 365      /* Bonded */
 366  
 367      // Construct the initial bond state.
 368      cast r1 0u64 into r11 as bond_state;
 369      // Get the bond state for the caller, or default to the initial bond state.
 370      get.or_use bonded[r0] r11 into r12;
 371      // Enforce the validator matches in the bond state.
 372      assert.eq r12.validator r1;
 373  
 374      // Increment the microcredits in the bond state.
 375      add r12.microcredits r3 into r13;
 376  
 377      // Determine if the amount is at least 10 thousand credits.
 378      gte r13 10_000_000_000u64 into r14;
 379      // Enforce the amount is at least 10 thousand credits.
 380      assert.eq r14 true;
 381  
 382      // Construct the updated bond state.
 383      cast r1 r13 into r15 as bond_state;
 384  
 385      /* Account */
 386  
 387      // Get the balance of the caller.
 388      // If the account does not exist, this finalize scope will fail.
 389      get account[r0] into r16;
 390      // Decrement the balance of the caller.
 391      sub r16 r3 into r17;
 392  
 393      /* Delegated */
 394  
 395      // Get current total delegated amount.
 396      get.or_use delegated[r1] 0u64 into r18;
 397      // Add new bond amount to current delegation.
 398      add r3 r18 into r19;
 399  
 400      /* Unbonding */
 401  
 402      // Check if the validator exists in the unbonding state.
 403      contains unbonding[r1] into r20;
 404      // Ensure the validator currently is not unbonding.
 405      assert.eq r20 false;
 406  
 407      /* Writes */
 408  
 409      // Update the bond state for the caller.
 410      set r15 into bonded[r0];
 411      // Update the balance of the caller.
 412      set r17 into account[r0];
 413      // Update delegated amount.
 414      set r19 into delegated[r1];
 415  
 416  /**********************************************************************************************************************/
 417  
 418  // This function allows any staker to unbond their microcredits from a validator,
 419  // callable only by using the withdrawal address of the staker or the validator.
 420  //
 421  // **Validators**: It will remove the validator if the self bonded balance falls below 100 credits
 422  // or the total delegated balance falls below 10M credits.
 423  // **Delegators**: It will remove the validator if the total delegated balance falls below 10M credits.
 424  // It will remove the entire bond_state of the delegator if it falls below 10,000 credits.
 425  //
 426  // Validators are permitted to fully unbond any of their delegators. When a validator unbonds a delegator,
 427  // the entire bonded balance is unbonded, regardless of the amount of microcredits and may end up removing the validator
 428  // from the committee if the total delegated balance falls below 10M credits.
 429  //
 430  // The corresponding function for 'unbond_public' is 'claim_unbond_public'.
 431  function unbond_public:
 432      // Input the staker's address.
 433      input r0 as address.public;
 434      // Input the amount of microcredits to unbond.
 435      input r1 as u64.public;
 436  
 437      // Unbond the specified amount of microcredits for the specified validator.
 438      async unbond_public self.caller r0 r1 into r2;
 439      // Output the finalize future.
 440      output r2 as credits.alpha/unbond_public.future;
 441  
 442  finalize unbond_public:
 443      // Input the caller's address.
 444      input r0 as address.public;
 445      // Input the staker's address.
 446      input r1 as address.public;
 447      // Input the amount of microcredits to unbond.
 448      input r2 as u64.public;
 449  
 450      // Set the default unbonding state.
 451      add block.height 360u32 into r3;
 452      // Construct the default unbonding state.
 453      cast 0u64 r3 into r4 as unbond_state;
 454  
 455      // Retrieve the staker's bond state.
 456      // Note: If the bonded state does not exist, reject the transition.
 457      get bonded[r1] into r5;
 458  
 459      /* Check Caller's Permission */
 460  
 461      // Get the staker's withdrawal address.
 462      get withdraw[r1] into r6;
 463      // Check if the caller's address equals the staker's withdrawal address.
 464      is.eq r0 r6 into r7;
 465  
 466      // Check if the validator's withdrawal address has been set.
 467      // Note: This contains check must use `withdraw` and **not** `committee` to ensure the validator
 468      // can unbond delegators even when the validator is not in the committee. Of course, if the validator is
 469      // in the committee, then the validator must be able to unbond its delegators.
 470      contains withdraw[r5.validator] into r8;
 471      // Get the validator's withdrawal address from the bond state, using the zero address as the default.
 472      get.or_use withdraw[r5.validator] ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd into r9;
 473      // Check if the validator's withdrawal address matches the caller.
 474      is.eq r0 r9 into r10;
 475      // AND the withdraw address has been set (to prevent an edge case where a validator uses the zero address as a withdrawal address).
 476      and r8 r10 into r11;
 477  
 478      // Either the caller is the staker's withdrawal address OR the validator's withdrawal address is set to the caller.
 479      or r7 r11 into r12;
 480      // Enforce the permission as `true`.
 481      assert.eq r12 true;
 482  
 483      // Check if bonded to self (validator) or to a different address (delegator).
 484      is.eq r5.validator r1 into r13;
 485      branch.eq r13 true to unbond_validator;
 486  
 487      /* Unbond the Delegator */
 488      // {
 489          // Retrieve or initialize the unbonding state.
 490          get.or_use unbonding[r1] r4 into r14;
 491          // Retrieve the delegated amount in microcredits for the validator.
 492          get delegated[r5.validator] into r15;
 493  
 494          // Calculate new bonded microcredits.
 495          // Note: If the subtraction underflows, reject the transition.
 496          sub r5.microcredits r2 into r16;
 497  
 498          // Check if the delegator will fall below 10,000 bonded credits.
 499          lt r16 10_000_000_000u64 into r17;
 500  
 501          // If the validator is forcing the delegator to unbond OR the delegator will fall below 10,000 bonded credits.
 502          or r11 r17 into r18;
 503  
 504          // Determine the amount to unbond: requested amount if >= 10,000 credits, otherwise the full bonded amount.
 505          ternary r18 r5.microcredits r2 into r19;
 506  
 507          /* Unbonding */
 508  
 509          // Increment existing unbond amount by the new unbond amount.
 510          // Note: If the addition overflows, reject the transition.
 511          add r14.microcredits r19 into r20;
 512          // Construct the updated unbond state.
 513          cast r20 r3 into r21 as unbond_state;
 514          // Store the new unbonding state.
 515          set r21 into unbonding[r1];
 516  
 517          /* Delegated */
 518  
 519          // Calculate the new delegated total for the validator.
 520          // Note: If the subtraction underflows, reject the transition.
 521          sub r15 r19 into r22;
 522          // Store the new delegated total.
 523          set r22 into delegated[r5.validator];
 524  
 525          // Check if the new bonded state is falling below 10,000 credits, or if the validator is forcing an unbond on the delegator.
 526          branch.eq r18 true to remove_delegator;
 527  
 528          /* Decrement the Delegator */
 529          // {
 530              /* Bonded */
 531  
 532              // Construct the new bond state.
 533              cast r5.validator r16 into r23 as bond_state;
 534              // Set the new bond state.
 535              set r23 into bonded[r1];
 536  
 537              // Jump to the end of the unbond delegator process.
 538              branch.eq true true to end_unbond_delegator;
 539          // }
 540  
 541          position remove_delegator;
 542          // {
 543              /* Bonded */
 544  
 545              // Remove the bonded state.
 546              remove bonded[r1];
 547  
 548              /* Metadata */
 549  
 550              // Retrieve the current number of delegators.
 551              get metadata[ax1qgqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqavzal6] into r24;
 552              // Decrement the number of delegators by one.
 553              sub r24 1u32 into r25;
 554              // Store the new number of delegators.
 555              set r25 into metadata[ax1qgqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqavzal6];
 556          // } Intentionally fall through to end_unbond_delegator
 557  
 558          position end_unbond_delegator;
 559          // {
 560              // Check if the new delegated total is at least 10M credits.
 561              gte r22 10_000_000_000_000u64 into r26;
 562              // Jump to end if the delegated total is at least 10M credits.
 563              branch.eq r26 true to end;
 564          // }
 565          // If the delegated total is below 10M credits, continue to unbonding the validator.
 566      //}
 567  
 568      /* Unbond the Validator */
 569      position unbond_validator;
 570      // {
 571          // Check if the committee contains the validator.
 572          contains committee[r5.validator] into r27;
 573          // Determine if the delegator unbonding from a validator is not in the committee.
 574          nor r13 r27 into r28;
 575          // Jump to the end, if the delegator unbonding from a validator is not in the committee.
 576          branch.eq r28 true to end;
 577  
 578          // Retrieve the committee state.
 579          // Note: If the committee state does not exist, reject the transition.
 580          get committee[r5.validator] into r29;
 581          // Retrieve the bond state of the validator.
 582          // Note: If the bonded state does not exist, reject the transition.
 583          get bonded[r5.validator] into r30;
 584          // Retrieve the total delegated balance for the validator.
 585          // Note: If the delegated state does not exist, reject the transition.
 586          get delegated[r5.validator] into r31;
 587  
 588          // Check if the current delegated amount is below 10M credits.
 589          // Note: This will only be `true` if a delegator unbond caused the validator to fall below 10M credits.
 590          lt r31 10_000_000_000_000u64 into r32;
 591          branch.eq r32 true to remove_validator;
 592  
 593          // Calculate the updated delegated total after unbonding.
 594          // Note: If the subtraction underflows, reject the transition.
 595          sub r31 r2 into r33;
 596  
 597          // Calculate the updated amount of microcredits after unbonding.
 598          sub r30.microcredits r2 into r34;
 599  
 600          // Check if the new bond state is below the required minimums.
 601          gte r34 100_000_000u64 into r35; // Minimum self bond requirement: 100 credits.
 602          gte r33 10_000_000_000_000u64 into r36; // Minimum total delegated requirement: 10M credits.
 603  
 604          // If either bond state is below the thresholds, remove the validator from the committee.
 605          and r35 r36 into r37;
 606          branch.eq r37 false to remove_validator;
 607  
 608          /* Unbonding */
 609  
 610          // Retrieve or initialize the unbonding state.
 611          get.or_use unbonding[r5.validator] r4 into r38;
 612          // Increment the unbond amount.
 613          // Note: If the addition overflows, reject the transition.
 614          add r38.microcredits r2 into r39;
 615          // Set the updated unbond state.
 616          cast r39 r3 into r40 as unbond_state;
 617          // Store the new unbonding state.
 618          set r40 into unbonding[r5.validator];
 619  
 620          /* Delegated */
 621  
 622          // Store the new delegated total.
 623          set r33 into delegated[r5.validator];
 624  
 625          /* Bonded */
 626  
 627          // Construct and store the new bond state.
 628          cast r5.validator r34 into r41 as bond_state;
 629          set r41 into bonded[r5.validator];
 630  
 631          // Jump to end.
 632          branch.eq true true to end;
 633      //}
 634  
 635      /* Remove the Validator from the Committee */
 636      position remove_validator;
 637      // {
 638          /* Committee */
 639  
 640          // Remove the validator from the committee.
 641          remove committee[r5.validator];
 642  
 643          /* Metadata */
 644  
 645          // Retrieve the current committee size.
 646          get metadata[ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd] into r42;
 647          // Decrement the committee size by one.
 648          sub r42 1u32 into r43;
 649          // Store the new committee size.
 650          set r43 into metadata[ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd];
 651  
 652          /* Delegated */
 653  
 654          // Decrease the delegated total by the bonded amount.
 655          sub r31 r30.microcredits into r44;
 656          // Store the new delegated total.
 657          set r44 into delegated[r5.validator];
 658  
 659          /* Bonded */
 660  
 661          // Remove the bonded state.
 662          remove bonded[r5.validator];
 663  
 664          /* Unbonding */
 665  
 666          // Retrieve or initialize the unbonding state.
 667          get.or_use unbonding[r5.validator] r4 into r45;
 668          // Increment the unbond amount by the full bonded amount.
 669          // Note: If the addition overflows, reject the transition.
 670          add r30.microcredits r45.microcredits into r46;
 671          // Construct the updated unbond state.
 672          cast r46 r3 into r47 as unbond_state;
 673          // Store the new unbonding state.
 674          set r47 into unbonding[r5.validator];
 675      //}
 676  
 677      position end;
 678  
 679  /**********************************************************************************************************************/
 680  
 681  // The `claim_unbond_public` function allows any staker to claim their microcredits
 682  // to their withdrawal address after the unbonding period.
 683  //
 684  // Note: Please be advised that this function is callable by any user for any staker.
 685  //
 686  // This function also removes the staker's withdrawal address if the staker no longer has any bonded balance.
 687  function claim_unbond_public:
 688      // Input the staker's address.
 689      input r0 as address.public;
 690  
 691      // Claim the unbonded microcredits.
 692      async claim_unbond_public r0 into r1;
 693      // Output the finalize future.
 694      output r1 as credits.alpha/claim_unbond_public.future;
 695  
 696  finalize claim_unbond_public:
 697      // Input the staker's address.
 698      input r0 as address.public;
 699  
 700      // Get the unbond state for the address, or fail if it does not exist.
 701      get unbonding[r0] into r1;
 702      // Determine if unbonding is complete.
 703      gte block.height r1.height into r2;
 704      // Enforce the unbonding is complete.
 705      assert.eq r2 true;
 706  
 707      /* Withdraw */
 708  
 709      // Get the withdrawal address for the address.
 710      get withdraw[r0] into r3;
 711  
 712      /* Account */
 713  
 714      // Add the unbonded amount to the withdrawal address public balance.
 715      // Increments `account[r3]` by `r1.microcredits`.
 716      // If `account[r3]` does not exist, 0u64 is used.
 717      // If `account[r3] + r1.microcredits` overflows, `claim_unbond_public` is reverted.
 718      get.or_use account[r3] 0u64 into r4;
 719      add r1.microcredits r4 into r5;
 720      set r5 into account[r3];
 721  
 722      /* Unbonding */
 723  
 724      // Remove the unbond state for the staker.
 725      remove unbonding[r0];
 726  
 727      // Check if the staker is still bonded.
 728      contains bonded[r0] into r6;
 729      // Ends the `claim_unbond_public` logic.
 730      branch.eq r6 true to end;
 731  
 732      /* Withdraw */
 733  
 734      // If the caller is no longer bonded, remove the withdrawal address.
 735      remove withdraw[r0];
 736  
 737      // The terminus.
 738      position end;
 739  
 740  /**********************************************************************************************************************/
 741  
 742  // This function allows a validator to set their state to be either opened or closed to new stakers.
 743  // When the validator is open to new stakers, any staker (including the validator) can bond or unbond from the validator.
 744  // When the validator is closed to new stakers, existing stakers can still bond or unbond from the validator, but new stakers cannot bond.
 745  //
 746  // This function serves two primary purposes:
 747  // 1. Allow a validator to leave the committee, by closing themselves to stakers and then unbonding all of their stakers.
 748  // 2. Allow a validator to maintain their % of stake, by closing themselves to allowing more stakers to bond to them.
 749  function set_validator_state:
 750      // Input the 'is_open' state.
 751      input r0 as boolean.public;
 752      // Set the validator to be either open or closed to new stakers.
 753      async set_validator_state self.caller r0 into r1;
 754      // Output the finalize future.
 755      output r1 as credits.alpha/set_validator_state.future;
 756  
 757  finalize set_validator_state:
 758      // Input the validator's address.
 759      input r0 as address.public;
 760      // Input the 'is_open' state.
 761      input r1 as boolean.public;
 762  
 763      // Get the committee state for the specified validator.
 764      // If the validator does not exist, this finalize scope will fail.
 765      get committee[r0] into r2;
 766  
 767      // Construct the updated committee state.
 768      cast r1 r2.commission into r3 as committee_state;
 769      // Update the committee state for the specified validator.
 770      set r3 into committee[r0];
 771  
 772  /**********************************************************************************************************************/
 773  
 774  // The `transfer_public` function sends the specified amount
 775  // from the caller's `account` to the receiver's `account`.
 776  function transfer_public:
 777      // Input the receiver.
 778      input r0 as address.public;
 779      // Input the amount.
 780      input r1 as u64.public;
 781      // Transfer the credits publicly.
 782      async transfer_public self.caller r0 r1 into r2;
 783      // Output the finalize future.
 784      output r2 as credits.alpha/transfer_public.future;
 785  
 786  finalize transfer_public:
 787      // Input the caller.
 788      input r0 as address.public;
 789      // Input the receiver.
 790      input r1 as address.public;
 791      // Input the amount.
 792      input r2 as u64.public;
 793      // Decrements `account[r0]` by `r2`.
 794      // If `account[r0] - r2` underflows, `transfer_public` is reverted.
 795      get account[r0] into r3;
 796      sub r3 r2 into r4;
 797      set r4 into account[r0];
 798      // Increments `account[r1]` by `r2`.
 799      // If `account[r1]` does not exist, 0u64 is used.
 800      // If `account[r1] + r2` overflows, `transfer_public` is reverted.
 801      get.or_use account[r1] 0u64 into r5;
 802      add r5 r2 into r6;
 803      set r6 into account[r1];
 804  
 805  /**********************************************************************************************************************/
 806  
 807  // The `transfer_public_as_signer` function sends the specified amount
 808  // from the signer's `account` to the receiver's `account`.
 809  function transfer_public_as_signer:
 810      // Input the receiver.
 811      input r0 as address.public;
 812      // Input the amount.
 813      input r1 as u64.public;
 814      // Transfer the credits publicly.
 815      async transfer_public_as_signer self.signer r0 r1 into r2;
 816      // Output the finalize future.
 817      output r2 as credits.alpha/transfer_public_as_signer.future;
 818  
 819  finalize transfer_public_as_signer:
 820      // Input the signer.
 821      input r0 as address.public;
 822      // Input the receiver.
 823      input r1 as address.public;
 824      // Input the amount.
 825      input r2 as u64.public;
 826      // Decrements `account[r0]` by `r2`.
 827      // If `account[r0] - r2` underflows, `transfer_public_as_signer` is reverted.
 828      get account[r0] into r3;
 829      sub r3 r2 into r4;
 830      set r4 into account[r0];
 831      // Increments `account[r1]` by `r2`.
 832      // If `account[r1]` does not exist, 0u64 is used.
 833      // If `account[r1] + r2` overflows, `transfer_public_as_signer` is reverted.
 834      get.or_use account[r1] 0u64 into r5;
 835      add r5 r2 into r6;
 836      set r6 into account[r1];
 837  
 838  /**********************************************************************************************************************/
 839  
 840  // The `transfer_private` function sends the specified amount
 841  // from the sender's record to the receiver in a record.
 842  function transfer_private:
 843      // Input the sender's record.
 844      input r0 as credits.record;
 845      // Input the receiver.
 846      input r1 as address.private;
 847      // Input the amount.
 848      input r2 as u64.private;
 849      // Checks the given record has a sufficient amount.
 850      // This `sub` operation is safe, and the proof will fail
 851      // if an underflow occurs. The destination register `r3` holds
 852      // the change amount to be returned to the sender.
 853      sub r0.microcredits r2 into r3;
 854      // Construct a record for the specified receiver.
 855      cast r1 r2 into r4 as credits.record;
 856      // Construct a record with the change amount for the sender.
 857      cast r0.owner r3 into r5 as credits.record;
 858      // Output the receiver's record.
 859      output r4 as credits.record;
 860      // Output the sender's change record.
 861      output r5 as credits.record;
 862  
 863  /**********************************************************************************************************************/
 864  
 865  // The `transfer_private_to_public` function turns a specified amount
 866  // from a record into public credits for the specified receiver.
 867  //
 868  // This function preserves privacy for the sender's record, however
 869  // it publicly reveals the receiver and the amount.
 870  function transfer_private_to_public:
 871      // Input the sender's record.
 872      input r0 as credits.record;
 873      // Input the receiver.
 874      input r1 as address.public;
 875      // Input the amount.
 876      input r2 as u64.public;
 877      // Checks the given record has a sufficient amount.
 878      // This `sub` operation is safe, and the proof will fail
 879      // if an underflow occurs. The destination register `r3` holds
 880      // the change amount for the sender.
 881      sub r0.microcredits r2 into r3;
 882      // Construct a record with the change amount for the sender.
 883      cast r0.owner r3 into r4 as credits.record;
 884      // Increment the amount publicly for the receiver.
 885      async transfer_private_to_public r1 r2 into r5;
 886      // Output the sender's change record.
 887      output r4 as credits.record;
 888      // Output the finalize future.
 889      output r5 as credits.alpha/transfer_private_to_public.future;
 890  
 891  finalize transfer_private_to_public:
 892      // Input the receiver.
 893      input r0 as address.public;
 894      // Input the amount.
 895      input r1 as u64.public;
 896      // Retrieve the balance of the receiver.
 897      // If `account[r0]` does not exist, 0u64 is used.
 898      get.or_use account[r0] 0u64 into r2;
 899      // Increments `account[r0]` by `r1`.
 900      // If `r1 + r2` overflows, `transfer_private_to_public` is reverted.
 901      add r1 r2 into r3;
 902      // Updates the balance of the sender.
 903      set r3 into account[r0];
 904  
 905  /**********************************************************************************************************************/
 906  
 907  // The `transfer_public_to_private` function turns a specified amount
 908  // from the mapping `account` into a record for the specified receiver.
 909  //
 910  // This function publicly reveals the sender, the receiver, and the specified amount.
 911  // However, subsequent methods using the receiver's record can preserve the receiver's privacy.
 912  function transfer_public_to_private:
 913      // Input the receiver.
 914      input r0 as address.private;
 915      // Input the amount.
 916      input r1 as u64.public;
 917      // Construct a record for the receiver.
 918      cast r0 r1 into r2 as credits.record;
 919      // Decrement the balance of the sender publicly.
 920      async transfer_public_to_private self.caller r1 into r3;
 921      // Output the record of the receiver.
 922      output r2 as credits.record;
 923      // Output the finalize future.
 924      output r3 as credits.alpha/transfer_public_to_private.future;
 925  
 926  finalize transfer_public_to_private:
 927      // Input the sender.
 928      input r0 as address.public;
 929      // Input the amount.
 930      input r1 as u64.public;
 931      // Retrieve the balance of the sender.
 932      get account[r0] into r2;
 933      // Decrements `account[r0]` by `r1`.
 934      // If `r2 - r1` underflows, `transfer_public_to_private` is reverted.
 935      sub r2 r1 into r3;
 936      // Updates the balance of the sender.
 937      set r3 into account[r0];
 938  
 939  /**********************************************************************************************************************/
 940  
 941  // The `join` function combines two records into one.
 942  function join:
 943      // Input the first record.
 944      input r0 as credits.record;
 945      // Input the second record.
 946      input r1 as credits.record;
 947      // Combines the amount of the first record and the second record.
 948      // This `add` operation is safe, and the proof will fail
 949      // if an overflow occurs.
 950      add r0.microcredits r1.microcredits into r2;
 951      // Construct a record with the combined amount.
 952      cast r0.owner r2 into r3 as credits.record;
 953      // Output the record.
 954      output r3 as credits.record;
 955  
 956  /**********************************************************************************************************************/
 957  
 958  // The `split` function splits a record into two records. The given input amount will be stored in the first record,
 959  // and the remaining amount will be stored in the second record, with the fee deducted from the remaining amount.
 960  // If the caller executes a transaction that contains only a call to this function, then the transaction does not
 961  // require a fee, unless the caller wishes to provide an additional fee. Transactions that contain multiple transitions
 962  // (that include one or more calls to this function) will require a fee as per standard consensus rules.
 963  function split:
 964      // Input the record.
 965      input r0 as credits.record;
 966      // Input the amount to split.
 967      input r1 as u64.private;
 968      // Checks the given record has a sufficient amount to split.
 969      // This `sub` operation is safe, and the proof will fail
 970      // if an underflow occurs.
 971      sub r0.microcredits r1 into r2;
 972      // Checks the given record has a sufficient fee to remove.
 973      // This `sub` operation is safe, and the proof will fail
 974      // if an underflow occurs.
 975      sub r2 10_000u64 into r3;
 976      // Construct the first record.
 977      cast r0.owner r1 into r4 as credits.record;
 978      // Construct the second record.
 979      cast r0.owner r3 into r5 as credits.record;
 980      // Output the first record.
 981      output r4 as credits.record;
 982      // Output the second record.
 983      output r5 as credits.record;
 984  
 985  /**********************************************************************************************************************/
 986  
 987  // The `fee_private` function charges the specified amount from the sender's record.
 988  function fee_private:
 989      // Input the sender's record.
 990      input r0 as credits.record;
 991      // Input the amount.
 992      input r1 as u64.public;
 993      // Input the priority fee amount.
 994      input r2 as u64.public;
 995      // Input the deployment or execution ID.
 996      input r3 as field.public;
 997      // Ensure the amount is nonzero.
 998      assert.neq r1 0u64;
 999      // Ensure the deployment or execution ID is nonzero.
1000      assert.neq r3 0field;
1001      // Add the fee and priority fee amounts.
1002      add r1 r2 into r4;
1003      // Checks the given record has a sufficient amount.
1004      // This `sub` operation is safe, and the proof will fail
1005      // if an underflow occurs. The destination register `r3` holds
1006      // the change amount for the sender.
1007      sub r0.microcredits r4 into r5;
1008      // Construct a record with the change amount for the sender.
1009      cast r0.owner r5 into r6 as credits.record;
1010      // Output the sender's change record.
1011      output r6 as credits.record;
1012  
1013  /**********************************************************************************************************************/
1014  
1015  // The `fee_public` function charges the specified amount from the sender's account.
1016  function fee_public:
1017      // Input the amount.
1018      input r0 as u64.public;
1019      // Input the priority fee amount.
1020      input r1 as u64.public;
1021      // Input the deployment or execution ID.
1022      input r2 as field.public;
1023      // Ensure the amount is nonzero.
1024      assert.neq r0 0u64;
1025      // Ensure the deployment or execution ID is nonzero.
1026      assert.neq r2 0field;
1027      // Add the fee and priority fee amounts.
1028      add r0 r1 into r3;
1029      // Decrement the balance of the sender publicly.
1030      async fee_public self.signer r3 into r4;
1031      // Output the finalize future.
1032      output r4 as credits.alpha/fee_public.future;
1033  
1034  finalize fee_public:
1035      // Input the sender's address.
1036      input r0 as address.public;
1037      // Input the total fee amount.
1038      input r1 as u64.public;
1039      // Retrieve the balance of the sender.
1040      // If `account[r0]` does not exist, `fee_public` is reverted.
1041      get account[r0] into r2;
1042      // Decrements `account[r0]` by `r1`.
1043      // If `r2 - r1` underflows, `fee_public` is reverted.
1044      sub r2 r1 into r3;
1045      // Updates the balance of the sender.
1046      set r3 into account[r0];
1047  
1048  /**********************************************************************************************************************/
1049  
1050  // The `upgrade` function migrates the input record to the pool of records after the inclusion upgrade.
1051  // The original record will be spent and the new record will be created with the same amount of credits.
1052  // If the caller executes a transaction that contains only a call to this function, then the transaction does not
1053  // require a fee, unless the caller wishes to provide an additional fee. Transactions that contain multiple transitions
1054  // (that include one or more calls to this function) will require a fee as per standard consensus rules.
1055  function upgrade:
1056      // Input the record.
1057      input r0 as credits.record;
1058  
1059      // Check if the record amount is at most 500,000 credits.
1060      lte r0.microcredits 1_000_000_000_000u64 into r1;
1061      // Ensure that the record amount is at most 500,000 credits.
1062      assert.eq r1 true;
1063  
1064      // Construct a record for the specified receiver.
1065      cast r0.owner r0.microcredits into r2 as credits.record;
1066  
1067      // Decrement the private pool of records before the inclusion upgrade.
1068      async upgrade r0.microcredits into r3;
1069      // Output the upgraded record.
1070      output r2 as credits.record;
1071      // Output the finalize future.
1072      output r3 as credits.alpha/upgrade.future;
1073  
1074  finalize upgrade:
1075      // Input the record amount.
1076      input r0 as u64.public;
1077  
1078      // Get the remaining `credits.record` pool size.
1079      get.or_use pool[ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd] 0u64 into r1;
1080      // Increment the pool by the record amount.
1081      add r1 r0 into r2;
1082      // Determine if the total number of migrated credits is less than or equal to 4_000_000 credits.
1083      lte r2 4_000_000_000_000u64 into r3;
1084      // Enforce that the total number of migrated credits is less than or equal to 4_000_000 credits.
1085      assert.eq r3 true;
1086  
1087      // Set the new pool size.
1088      set r2 into pool[ax1qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq3qtczd];
1089  
1090  /**********************************************************************************************************************/