From 82b3cf179a953123b6aa579598cd75781645a56b Mon Sep 17 00:00:00 2001
From: Pi Lanningham <pi.lanningham@gmail.com>
Date: Thu, 22 Feb 2024 02:31:21 -0500
Subject: [PATCH 1/3] In progress spec annotations

---
 lib/staking_contracts/datums.ak     |  1 +
 lib/staking_contracts/stake_pool.ak | 41 +++++++++++++++++++++++++++--
 lib/staking_contracts/utils.ak      | 20 +++++++++++++-
 validators/stake_pool_mint.ak       | 10 ++++++-
 4 files changed, 68 insertions(+), 4 deletions(-)

diff --git a/lib/staking_contracts/datums.ak b/lib/staking_contracts/datums.ak
index 090f679..6ac1abb 100644
--- a/lib/staking_contracts/datums.ak
+++ b/lib/staking_contracts/datums.ak
@@ -57,6 +57,7 @@ pub type StakePoolDatum {
 
 pub type StakePoolRedeemer {
   //Index of the reward setting to be used ina locking tx.
+  // Spec 1.5.8
   reward_index: Int,
 }
 
diff --git a/lib/staking_contracts/stake_pool.ak b/lib/staking_contracts/stake_pool.ak
index f0fdef7..a6d3a82 100644
--- a/lib/staking_contracts/stake_pool.ak
+++ b/lib/staking_contracts/stake_pool.ak
@@ -21,10 +21,13 @@ use staking_contracts/utils.{
 }
 use sundae/multisig.{Signature, satisfied}
 
+// Spec 1.4
 pub fn update_transaction(datum: StakePoolDatum, ctx: ScriptContext) -> Bool {
   when ctx.purpose is {
     //Ensure the utxo is spent by the owner
+    // Spec 1.4.1
     Spend(_) ->
+      // Spec 1.4.2
       satisfied(
         datum.owner,
         ctx.transaction.extra_signatories,
@@ -35,6 +38,7 @@ pub fn update_transaction(datum: StakePoolDatum, ctx: ScriptContext) -> Bool {
   }
 }
 
+// Spec 1.5
 pub fn lock_transaction(
   datum: StakePoolDatum,
   redeemer: StakePoolRedeemer,
@@ -43,6 +47,7 @@ pub fn lock_transaction(
 ) -> Bool {
   when ctx.purpose is {
     //Ensure the utxo is spent in a valid locking tx
+    // Spec 1.5.1
     Spend(my_output_reference) ->
       is_proper_locking_tx(
         my_output_reference,
@@ -55,6 +60,7 @@ pub fn lock_transaction(
   }
 }
 
+// Spec 1.5
 fn is_proper_locking_tx(
   my_output_reference: OutputReference,
   datum: StakePoolDatum,
@@ -62,10 +68,12 @@ fn is_proper_locking_tx(
   ctx: ScriptContext,
   time_lock_hash: ByteArray,
 ) {
+  // Spec 1.5.2
   expect Finite(lower_bound) =
     ctx.transaction.validity_range.lower_bound.bound_type
   expect lower_bound >= datum.open_time
   //Find the input guarded by this validator
+  // 1.5.3 "which is known by finding the transaction input with the same output reference from the script context purpose"
   expect Some(self) =
     ctx.transaction.inputs
       |> transaction.find_input(my_output_reference)
@@ -73,6 +81,7 @@ fn is_proper_locking_tx(
   let self_input = self.output
 
   //Find amount of inputs with stake pool script, should be exactly 1
+  // Spec 1.5.3 - n.b. checked in the `and` below
   let exactly_one_stake_pool_input =
     length(
       filter_inputs_by_credential(
@@ -82,52 +91,65 @@ fn is_proper_locking_tx(
     ) == 1
 
   //We need to ensure the output of the tx has the same validator attached
+  // Spec 1.5.4 - n.b. existance, but not uniqueness (there is at least one)
   expect ScriptCredential(self_script) = self_input.address.payment_credential
   let self_outputs =
     ctx.transaction.outputs
       |> transaction.find_script_outputs(self_script)
   expect Some(self_output) = self_outputs |> at(0)
 
+  // Spec 1.5.5 - n.b. in particular, The staking address is unchanged
   expect self_input.address == self_output.address
+
   //The output needs to include a utxo with time lock validator
+  // Spec 1.5.6 - n.b. existance, but not uniqueness (there is at least one)
   let time_lock_outputs =
     ctx.transaction.outputs
       |> transaction.find_script_outputs(time_lock_hash)
   expect Some(time_lock) = time_lock_outputs |> at(0)
 
+  // Spec 1.5.7 - inline datum of time TimeLockDatum
   expect InlineDatum(time_lock_data) = time_lock.datum
-
   let time_lock_datum = to_time_lock_datum(time_lock_data)
 
   //We use the reward setting as indicated by the submitter of the transaction
+  // Spec 1.5.9 - n.b. manipulation of reward_index will fail, because either time or reward quantity will be incorrect
   expect Some(reward_setting) =
     datum.reward_settings |> at(redeemer.reward_index)
+  
   //Find out current stake_pool token quantity
+  // Spec 1.5.13.1 "be the quantity of reward token in the stake pool input"
   let stake_pool_size =
     self_input.value
       |> value.quantity_of(datum.policy_id, datum.asset_name)
 
   //Find stake_pool token quantity in output
+  // Spec 1.5.13.1 "the quantity of the same in the stake pool output"
   let new_stake_pool_size =
     self_output.value
       |> value.quantity_of(datum.policy_id, datum.asset_name)
 
   //Difference between old and new quantity is equal to the reward to the staker
+  // Spec 1.5.13.1 - n.b. withdrawn_amount => reward
   let reward = stake_pool_size - new_stake_pool_size
 
   //The locked amount in the time lock output
+  // Spec 1.5.13.2 - n.b. total_locked_output => locked_amount
   let locked_amount =
     time_lock.value
       |> value.quantity_of(datum.policy_id, datum.asset_name)
 
   //The staked amount is deduced from the locked amount and the reward
+  // Spec 1.5.13.3 - n.b. derived_user_locked_output => staked_amount
   let staked_amount = locked_amount - reward
 
   //Ensure the locked amount matches the reward setting
+  // Spec 1.5.13.4 + 1.5.13.5 - n.b. checked in the `and` below
   let correct_locked_amount =
     locked_amount == add_reward(staked_amount, reward_setting.reward_multiplier)
 
   //Make sure no other assets have been altered in the stake pool output compared to the input
+  // Spec 1.5.14.1 - n.b. checked in the `and` below
   let correct_output_value =
     value.without_lovelace(self_input.value) == add(
       value.without_lovelace(self_output.value),
@@ -137,11 +159,16 @@ fn is_proper_locking_tx(
     )
 
   //Allow higher lovelace amount to support increase of minutxo
+  // Spec 1.5.14.2
   expect
     value.lovelace_of(self_input.value) <= value.lovelace_of(self_output.value)
+
   //Make sure settings have not been altered
+  // Spec 1.5.7 - "with the same value as the datum attached to the input"
+  // n.b. checked in the `and` below
   let same_datum = InlineDatum(datum) == self_output.datum
-
+  
+  // Spec 1.5.15 - n.b. included in `and` below
   let one_stake_nft_minted =
     1 == value.quantity_of(
       value.from_minted_value(ctx.transaction.mint),
@@ -149,16 +176,25 @@ fn is_proper_locking_tx(
       bytearray.drop(time_lock_datum.extra.time_lock_nft, 28),
     )
 
+  // Spec 1.5.16
   expect bytearray.take(time_lock_datum.extra.time_lock_nft, 28) == self_script
+
   and {
+    // Spec 1.5.15
     one_stake_nft_minted?,
+    // Spec 1.5.3
     exactly_one_stake_pool_input?,
     //Ensure exactly one stake pool output
+    // Spec 1.5.4 - n.b. uniqueness
     must_have_exactly_one_output(self_outputs)?,
     //Ensure exactly one time lock output
+    // Spec 1.5.6 - n.b. uniqueness
     must_have_exactly_one_output(time_lock_outputs)?,
+    // Spec 1.5.7
     same_datum?,
+    // Spec 1.5.13.4 + 1.5.13.5
     correct_locked_amount?,
+    // Spec 1.5.11 + 1.5.12
     //Ensure that the time lock does not expire too soon
     must_be_locked_until(
       ctx.transaction.validity_range,
@@ -166,6 +202,7 @@ fn is_proper_locking_tx(
       reward_setting.ms_locked,
       hour_millis,
     )?,
+    // Spec 1.5.14.1
     correct_output_value?,
   }
 }
diff --git a/lib/staking_contracts/utils.ak b/lib/staking_contracts/utils.ak
index d0a3e99..e89d1e8 100644
--- a/lib/staking_contracts/utils.ak
+++ b/lib/staking_contracts/utils.ak
@@ -15,10 +15,12 @@ use staking_contracts/datums.{
 }
 use sundae/multisig.{Signature}
 
+// Spec 1.5.3
 pub fn filter_inputs_by_credential(inputs: List<Input>, cred: Credential) {
   inputs |> filter(fn(i) { i.output.address.payment_credential == cred })
 }
 
+// Spec 1.5.3 + 1.5.6 - uniqueness of outputs
 pub fn must_have_exactly_one_output(outputs: List<Output>) {
   length(outputs) == 1
 }
@@ -31,11 +33,17 @@ pub fn must_be_signed_by(transaction: Transaction, vk: VerificationKeyHash) {
   has(transaction.extra_signatories, vk)
 }
 
+// Spec 1.5.13.4
 pub fn add_reward(amount: Int, reward: Rational) -> Int {
+  // Spec 1.5.10
   expect Less != rational.compare(reward, rational.zero())
+  // Spec 1.5.13.4 - "rounded down"
   rational.floor(
+    // Spec 1.5.13.4 - "multiplied by"
     rational.mul(
+      // Spec 1.5.13.4 - "derived_user_locked_output" => amount, which comes from staked_amount
       rational.from_int(amount),
+      // Spec 1.5.13.4 - "1 + reward_multiplier"
       rational.add(rational.from_int(1), reward),
     ),
   )
@@ -50,28 +58,38 @@ pub fn must_contain_asset(outputs: List<Output>, unit: ByteArray) -> Bool {
   )
 }
 
+// Spec 1.5.11
 pub const hour_millis = 3_600_000
 
 //Ensure that the time_lock output is set to expire after a set amount of days, with a certain buffer
 //to allow for a realistic transaction validity range
+// Spec 1.5.11 + 1.5.12
 pub fn must_be_locked_until(
   range: ValidityRange,
   time_lock: Output,
   ms_to_be_locked: Int,
-  buffer: Int,
+  buffer: Int, // n.b. passed buffer
 ) {
+  // Spec 1.5.12 - "the datum attached to the time lock position"
   expect InlineDatum(time_lock_datum) = time_lock.datum
+  // Spec 1.5.12 - "has extra.lock_until"
   let lock_expiration_time =
     to_time_lock_datum(time_lock_datum).extra.lock_until
+  // Spec 1.5.11 - "two finite bounds"
   expect Finite(upper_bound) = range.upper_bound.bound_type
   expect Finite(lower_bound) = range.lower_bound.bound_type
 
+  // Spec 1.5.12 - "upper_bound + reward_setting.ms_locked"
   let correct_lock_time = upper_bound + ms_to_be_locked
 
+  // Spec 1.5.12 - "is equal to"
   let is_locked_until_correct_time = lock_expiration_time == correct_lock_time
+  // Spec 1.5.11 - "that differ by at most"
   let range_less_than_buffer = upper_bound - lower_bound <= buffer
   and {
+    // Spec 1.5.12
     is_locked_until_correct_time?,
+    // Spec 1.5.11
     range_less_than_buffer?,
   }
 }
diff --git a/validators/stake_pool_mint.ak b/validators/stake_pool_mint.ak
index 23d9f8c..e227e64 100644
--- a/validators/stake_pool_mint.ak
+++ b/validators/stake_pool_mint.ak
@@ -5,7 +5,11 @@ use staking_contracts/stake_nft_mint.{
 }
 use staking_contracts/stake_pool.{lock_transaction, update_transaction}
 
-validator(time_lock_hash: ByteArray) {
+// Spec 1
+validator(
+  // Spec 1.1
+  time_lock_hash: ByteArray
+) {
   fn mint(redeemer: StakeNFTMintRedeemer, ctx: ScriptContext) {
     if redeemer.mint {
       mint_transaction(redeemer, ctx, time_lock_hash)?
@@ -14,13 +18,17 @@ validator(time_lock_hash: ByteArray) {
     }
   }
 
+  // Spec 1.2
   fn spend(
     datum: StakePoolDatum,
     redeemer: StakePoolRedeemer,
     ctx: ScriptContext,
   ) -> Bool {
+    // Spec 1.3
     or {
+      // Spec 1.4
       update_transaction(datum, ctx)?,
+      // Spec 1.5
       lock_transaction(datum, redeemer, ctx, time_lock_hash)?,
     }
   }

From 598339b6a87b524349f91d475bf87b2f7339d020 Mon Sep 17 00:00:00 2001
From: Pi Lanningham <pi.lanningham@gmail.com>
Date: Sun, 25 Feb 2024 20:21:10 -0500
Subject: [PATCH 2/3] Finish spec annotations!!

---
 lib/staking_contracts/datums.ak         |   3 +
 lib/staking_contracts/stake_nft_mint.ak | 114 +++++++++++++++++++++++-
 lib/staking_contracts/utils.ak          |  30 +++++--
 validators/stake_pool_mint.ak           |  10 ++-
 validators/stake_proxy.ak               |  56 +++++++++++-
 validators/time_lock.ak                 |  14 ++-
 6 files changed, 207 insertions(+), 20 deletions(-)

diff --git a/lib/staking_contracts/datums.ak b/lib/staking_contracts/datums.ak
index 6ac1abb..1708cce 100644
--- a/lib/staking_contracts/datums.ak
+++ b/lib/staking_contracts/datums.ak
@@ -89,16 +89,19 @@ pub type StakeProxyDatum {
   nft_policy_id: PolicyId,
 }
 
+// Spec 2.5.13
 pub fn to_stake_pool_datum(data: Data) -> StakePoolDatum {
   expect my_datum: StakePoolDatum = data
   my_datum
 }
 
+// UNUSED
 pub fn to_stake_proxy_datum(data: Data) -> StakeProxyDatum {
   expect my_datum: StakeProxyDatum = data
   my_datum
 }
 
+// Spec 2.5.14, 2.6.8.6, 4.3.2.5
 pub fn to_time_lock_datum(data: Data) -> TimeLockDatum {
   expect my_datum: TimeLockDatum = data
   my_datum
diff --git a/lib/staking_contracts/stake_nft_mint.ak b/lib/staking_contracts/stake_nft_mint.ak
index 4b554c7..6b2845f 100644
--- a/lib/staking_contracts/stake_nft_mint.ak
+++ b/lib/staking_contracts/stake_nft_mint.ak
@@ -22,100 +22,155 @@ use staking_contracts/datums.{
 use staking_contracts/utils.{hour_millis, must_start_after, time_to_date_string}
 use sundae/multisig.{Signature}
 
+// Spec 2.4
 pub type StakeNFTMintRedeemer {
+  // Spec 2.4.1
   stake_pool_index: Int,
+  // Spec 2.4.2
   time_lock_index: Int,
+  // Spec 2.4.3
   mint: Bool,
 }
 
+// Spec 2.5
 pub fn mint_transaction(
   redeemer: StakeNFTMintRedeemer,
   ctx: ScriptContext,
   time_lock_hash: ByteArray,
 ) -> Bool {
   when ctx.purpose is {
+    // Spec 2.5.2
     Mint(own_policy) -> {
       //Retrieve all minted assets into an array
       let minted = from_minted_value(ctx.transaction.mint) |> flatten()
 
       //Only 2 assets minted
+      // Spec 2.5.3
       expect 2 == list.length(minted)
+
       //Look for the reference nft (CIP-68)
+      // Spec 2.5.4 - "exactly one token"
       expect [reference_nft] =
+        // Spec 2.5.4 - "being minted"
         minted
+          // Spec 2.5.4 - "with"
           |> filter(
                fn(mt) {
-                 mt.1st == own_policy && take(mt.2nd, 4) == reference_prefix
+                 // Spec 2.5.4 - "a policy ID of Stake NFT"
+                 mt.1st == own_policy &&
+                 // Spec 2.5.4 - "and an asset name prefixed by"
+                 take(mt.2nd, 4) == reference_prefix
                },
              )
 
       //Look for the stake nft (CIP-68)
+      //  Spec 2.5.5 - "exactly one token"
       expect [stake_nft] =
+        // Spec 2.5.5 - "being minted"
         minted
+          // Spec 2.5.5 - "with"
           |> filter(
                fn(mt) {
-                 mt.1st == own_policy && take(mt.2nd, 4) == stake_nft_prefix
+                 // Spec 2.5.5 - "a policy ID of Stake NFT"
+                 mt.1st == own_policy &&
+                 // Spec 2.5.5 - "and an asset name prefixed by"
+                 take(mt.2nd, 4) == stake_nft_prefix
                },
              )
 
       //Asset name without CIP-68 prefix
+      // Spec 2.5.6
       let asset_name = drop(reference_nft.2nd, 4)
 
       //Ensure the stake nft has the same asset name as the reference nft
+      // Spec 2.5.7 - n.b. included in the `and` condition below
       let correct_stake_nft_name = drop(stake_nft.2nd, 4) == asset_name
 
       //only one reference nft minted
+      // Spec 2.5.8
       expect 1 == reference_nft.3rd
       //only one stake nft minted
+      // Spec 2.5.8
       expect 1 == stake_nft.3rd
+
       //The stake pool input
+      // Spec 2.5.9
       expect Some(stake_pool_input) =
         ctx.transaction.inputs |> at(redeemer.stake_pool_index)
+
+      // Spec 2.5.10 - n.b. stake_pool_cred checked below
       expect ScriptCredential(stake_pool_cred) =
         stake_pool_input.output.address.payment_credential
+
       //The time lock output
+      // Spec 2.5.11
       expect Some(time_lock_output) =
         ctx.transaction.outputs |> at(redeemer.time_lock_index)
+
+      // Spec 2.5.12 - n.b. time_lock_cred checked below
       expect ScriptCredential(time_lock_cred) =
         time_lock_output.address.payment_credential
+
       //Fetch inlinedatum from stakepool input and cast to StakePoolDatum
+      // Spec 2.5.13
       expect InlineDatum(stake_pool_input_datum) = stake_pool_input.output.datum
       let stake_pool_datum = to_stake_pool_datum(stake_pool_input_datum)
 
       //Fetch inlinedatum from timelock output and cast to TimeLockDatum
+      // Spec 2.5.14
       expect InlineDatum(time_lock_output_datum) = time_lock_output.datum
       let time_lock_datum = to_time_lock_datum(time_lock_output_datum)
 
       //The amount of tokens to be locked (no decimals taken into account)
+      // Spec 2.5.15
       let raw_amount =
         time_lock_output.value
           |> quantity_of(stake_pool_datum.policy_id, stake_pool_datum.asset_name)
 
+      // Spec 2.5.16 - n.b. actually checked below in the `and` condition
       let reference_nft_in_time_lock =
         1 == quantity_of(time_lock_output.value, own_policy, reference_nft.2nd)
 
       //Construct the proper asset name using the unique components
+      // Spec 2.5.17 - "let proper_asset_name" be
       let proper_asset_name =
-        blake2b_256(serialise(stake_pool_input.output_reference))
-          |> take(28)
+        // Spec 2.5.17 - "the blake2b_256 hash of"
+        blake2b_256(
+          // Spec 2.5.17 - "the serialized"
+          serialise(
+            // Spec 2.5.17 - "stake_pool_input.output_reference"
+            stake_pool_input.output_reference
+          )
+        )
+        // Spec 2.5.17 - The first 28 bytes of
+        |> take(28)
 
       //Construct the proper metadata nft name
+      // Spec 2.5.18 - "let proper_meta_name be"
       let proper_meta_name =
         list.foldl(
           [
+            // Spec 2.5.18 - Stake NFT
             "Stake NFT ",
+            // Spec 2.5.18 - "the reward token asset name"
             stake_pool_datum.asset_name,
+            // Spec 2.5.18 - a dash
             " - ",
+            // Spec 2.5.18 - and some human readable expression of lock_until
+            // n.b. the details of this method are not audited, but the impact is low
             time_to_date_string(time_lock_datum.extra.lock_until),
           ],
           "",
+          // Spec 2.5.18 - "The concatenation of"
           fn(el, sum) { bytearray.concat(sum, el) },
         )
 
       //Validations
       //Make sure the asset name is as expected
+      // Spec 2.5.19 - n.b. included in the `and` condition below
       let correct_reference_name = asset_name == proper_asset_name
 
+      // Spec 2.5.20 - n.b. included in the `and` condition below
       let correct_stake_nft_set =
         time_lock_datum.extra.time_lock_nft == bytearray.concat(
           own_policy,
@@ -123,43 +178,65 @@ pub fn mint_transaction(
         )
 
       //Ensure the metadata token name is as expected
+      // Spec 2.5.21 - n.b. included in the `and` condition below
       let correct_meta_name =
         dict.get(time_lock_datum.metadata, "name") == Some(proper_meta_name)
 
       //Make sure an extra field is present in the metadata showing the tokens locked by the nft
+      // Spec 2.5.22
       let proper_meta_amount =
         list.foldl(
           [
+            // Spec 2.5.22 - `[(`
             "[",
             "(",
+            // Spec 2.5.22 - The reward token policy ID
             bytearray.from_string(bytearray.to_hex(stake_pool_datum.policy_id)),
+            // Spec 2.5.22 - `,`
             ",",
+            // Spec 2.5.22 - The reward token asset name
             bytearray.from_string(bytearray.to_hex(stake_pool_datum.asset_name)),
+            // Spec 2.5.22 - `,`
             ",",
+            // Spec 2.5.22 - `raw_amount`
             bytearray.from_string(string.from_int(raw_amount)),
+            // Spec 2.5.22 - `)]`
             ")",
             "]",
           ],
           "",
+          // Spec 2.5.22 "the concatenation of"
           fn(el, sum) { bytearray.concat(sum, el) },
         )
+      // Spec 2.5.22 - n.b. included in the `and` condition below
       let correct_meta_amount =
+        // Spec 2.5.22 - The CIP-68 metadata at "locked_amount" must be
         dict.get(time_lock_datum.metadata, "locked_assets") == Some(
           proper_meta_amount,
         )
 
       //Verify script hashes
+      // Spec 2.5.10 - n.b. stake_pool_cred comes from stake_pool_input, and this is included in the `and` below
       let correct_stake_pool = own_policy == stake_pool_cred
+      // Spec 2.5.12 - n.b. time_lock_cred comes from time_lock_output, and this is included in the `and` below
       let correct_time_lock = time_lock_hash == time_lock_cred
 
       and {
+        // Spec 2.5.16
         reference_nft_in_time_lock?,
+        // Spec 2.5.20
         correct_stake_nft_set?,
+        // Spec 2.5.7
         correct_stake_nft_name?,
+        // Spec 2.5.19
         correct_reference_name?,
+        // Spec 2.5.21
         correct_meta_name?,
+        // Spec 2.5.22
         correct_meta_amount?,
+        // Spec 2.5.10
         correct_stake_pool?,
+        // Spec 2.5.12
         correct_time_lock?,
       }
     }
@@ -167,12 +244,16 @@ pub fn mint_transaction(
   }
 }
 
+// Spec 2.6
 pub fn burn_transaction(ctx: ScriptContext, time_lock_hash: ByteArray) -> Bool {
   when ctx.purpose is {
+    // Spec 2.6.2
     Mint(own_policy) -> {
       //Retrieve all minted assets into an array
+      // Spec 2.6.3
       let burned = from_minted_value(ctx.transaction.mint) |> flatten()
       //Look for the reference nfts (CIP-68)
+      // Spec 2.6.5
       let reference_nfts =
         burned
           |> filter(
@@ -180,8 +261,10 @@ pub fn burn_transaction(ctx: ScriptContext, time_lock_hash: ByteArray) -> Bool {
                  mt.1st == own_policy && take(mt.2nd, 4) == reference_prefix
                },
              )
+      // Spec 2.6.4
       let burned_count = list.length(burned)
       //Look for the stake nft (CIP-68)
+      // Spec 2.6.6
       let stake_nfts =
         burned
           |> filter(
@@ -190,33 +273,47 @@ pub fn burn_transaction(ctx: ScriptContext, time_lock_hash: ByteArray) -> Bool {
                },
              )
 
+      // Spec 2.6.7
       let nft_count = list.length(reference_nfts) + list.length(stake_nfts)
 
       //Ensure that only CIP-68 nft's are burned
+      // Spec 2.6.7 - n.b. included in the `and` condition below
       let correct_number_burned = burned_count == nft_count
 
+      // Spec 2.6.8
       let correct_burns =
+        // Spec 2.6.8 - "For each asset"
         list.all(
+          // Spec 2.6.8 - "in reference_nfts"
           reference_nfts,
           fn(reference_nft) {
             //Asset name without CIP-68 prefix
+            // Spec 2.6.8.1
             let asset_name = drop(reference_nft.2nd, 4)
 
+            // Spec 2.6.8.2
             expect Some(stake_nft) =
               stake_nfts |> find(fn(sk) { drop(sk.2nd, 4) == asset_name })
 
             when reference_nft.3rd is {
               //Burn scenario (unlock of locked tokens)
+              // Spec 2.6.8.3 - n.b. any other case is immediately False
               -1 -> {
                 //Full asset unit
+                // Used in Spec 2.6.8.7
                 let burned_unit = bytearray.concat(stake_nft.1st, stake_nft.2nd)
                 //The time lock input that contains the reference nft
+                // Spec 2.6.8.5 - "There must be", "Let this input be the time_lock_input"
                 expect Some(time_lock_input) =
+                  // Spec 2.6.8.5 - "input"
                   ctx.transaction.inputs
+                  // Spec 2.6.8.5 - "at least one"
                     |> find(
                          fn(i) {
+                          // Spec 2.6.8.5 - "with the time_lock_hash script credential"
                            i.output.address.payment_credential == ScriptCredential(
                              time_lock_hash,
+                             // Spec 2.6.8.5 - "with the reference NFT in the value"
                            ) && quantity_of(
                              i.output.value,
                              reference_nft.1st,
@@ -226,31 +323,40 @@ pub fn burn_transaction(ctx: ScriptContext, time_lock_hash: ByteArray) -> Bool {
                        )
 
                 //The inline datum belonging to the time lock inptu cast to TimeLockDatum
+                // Spec 2.6.8.6
                 expect InlineDatum(time_lock_input_datum) =
                   time_lock_input.output.datum
                 let time_lock_datum = to_time_lock_datum(time_lock_input_datum)
 
                 //Ensure the tokens burned match the timelock nft
+                // Spec 2.6.8.7 - n.b. included in the `and` condition below
                 let correct_token_burned =
                   time_lock_datum.extra.time_lock_nft == burned_unit
 
                 //Make sure both tokens are burned
+                // Spec 2.6.8.4 - n.b. equivalent to checking that stake_nft.3rd is equal to -1
                 let both_burned = stake_nft.3rd == reference_nft.3rd
                 and {
+                  // Spec 2.6.8.8
                   must_start_after(
                     ctx.transaction.validity_range,
                     time_lock_datum.extra.lock_until,
                   )?,
+                  // Spec 2.6.8.7
                   correct_token_burned?,
+                  // 2.6.8.4
                   both_burned?,
                 }
               }
+              // Spec 2.6.8.3
               _ -> False
             }
           },
         )
       and {
+        // Spec 2.6.7
         correct_number_burned?,
+        // Spec 2.6.8
         correct_burns?,
       }
     }
diff --git a/lib/staking_contracts/utils.ak b/lib/staking_contracts/utils.ak
index e89d1e8..758d33a 100644
--- a/lib/staking_contracts/utils.ak
+++ b/lib/staking_contracts/utils.ak
@@ -15,7 +15,7 @@ use staking_contracts/datums.{
 }
 use sundae/multisig.{Signature}
 
-// Spec 1.5.3
+// Spec 1.5.3, 4.3.3
 pub fn filter_inputs_by_credential(inputs: List<Input>, cred: Credential) {
   inputs |> filter(fn(i) { i.output.address.payment_credential == cred })
 }
@@ -25,36 +25,45 @@ pub fn must_have_exactly_one_output(outputs: List<Output>) {
   length(outputs) == 1
 }
 
+// UNUSED
 pub fn must_have_same_datum(input_datum: Data, output_datum: Data) {
   input_datum == output_datum
 }
 
+// UNUSED
 pub fn must_be_signed_by(transaction: Transaction, vk: VerificationKeyHash) {
   has(transaction.extra_signatories, vk)
 }
 
-// Spec 1.5.13.4
+// Spec 1.5.13.4, 4.3.2.20
 pub fn add_reward(amount: Int, reward: Rational) -> Int {
-  // Spec 1.5.10
+  // Spec 1.5.10, 4.3.2.19
   expect Less != rational.compare(reward, rational.zero())
-  // Spec 1.5.13.4 - "rounded down"
+  // Spec 1.5.13.4, 4.3.2.20 - "rounded down"
   rational.floor(
-    // Spec 1.5.13.4 - "multiplied by"
+    // Spec 1.5.13.4, 4.3.2.20 - "multiplied by"
     rational.mul(
-      // Spec 1.5.13.4 - "derived_user_locked_output" => amount, which comes from staked_amount
+      // Spec 1.5.13.4, 4.3.2.20 - "derived_user_locked_output" => amount, which comes from staked_amount
       rational.from_int(amount),
-      // Spec 1.5.13.4 - "1 + reward_multiplier"
+      // Spec 1.5.13.4, 4.3.2.20 - "1 + reward_multiplier"
       rational.add(rational.from_int(1), reward),
     ),
   )
 }
 
 //Returns true if the list of outputs contains at least 1 of the provided unit
+// Spec 4.3.2.2 - n.b. unit is equal to `batcher_certificate`
 pub fn must_contain_asset(outputs: List<Output>, unit: ByteArray) -> Bool {
+  // Spec 4.3.2.2 - "with a policy ID equal to the first 28 bytes of batcher certificate"
   let policy_id = unit |> take(28)
+  // Spec 4.3.2.2 - "an asset name equal to the remainder of the batcher certificate"
   let asset_id = unit |> drop(28)
+  // Spec 4.3.2.2 - "Must have at least one"
   is_some(
-    outputs |> find(fn(o) { quantity_of(o.value, policy_id, asset_id) > 0 }),
+    // Spec 4.3.2.2 - "one output such that"
+    outputs |> find(fn(o) {
+      // Spec 4.3.2.2 - "the value on that output contains an asset" "and a quantity greater than 0"
+      quantity_of(o.value, policy_id, asset_id) > 0 }),
   )
 }
 
@@ -94,8 +103,12 @@ pub fn must_be_locked_until(
   }
 }
 
+// Spec 2.6.8.8, 3.3.3
 pub fn must_start_after(range: ValidityRange, lock_expiration_time: PosixTime) {
+  // Spec 2.6.8.8 - "the transaction lower bound must be"
   when range.lower_bound.bound_type is {
+    // Spec 2.6.8.8 - Finite, and after or equal to `extra.lock_until`
+    // n.b. lock_expiration_time comes from extra.lock_until
     Finite(tx_earliest_time) -> lock_expiration_time <= tx_earliest_time
     _ -> False
   }?
@@ -103,6 +116,7 @@ pub fn must_start_after(range: ValidityRange, lock_expiration_time: PosixTime) {
 
 //Produces a date string in the format YYYYMMDD
 //Taken from https://stackoverflow.com/questions/7136385/calculate-day-number-from-an-unix-timestamp-in-a-math-way
+// Spec 2.5.18 - n.b. because of the complexity, the details of this code are not covered by the audit
 pub fn time_to_date_string(time: PosixTime) -> ByteArray {
   let s = time / 1000
   let z = s / 86400 + 719468
diff --git a/validators/stake_pool_mint.ak b/validators/stake_pool_mint.ak
index e227e64..cf8a4b0 100644
--- a/validators/stake_pool_mint.ak
+++ b/validators/stake_pool_mint.ak
@@ -5,15 +5,19 @@ use staking_contracts/stake_nft_mint.{
 }
 use staking_contracts/stake_pool.{lock_transaction, update_transaction}
 
-// Spec 1
+// Spec 1, 2, 2.1
 validator(
-  // Spec 1.1
+  // Spec 1.1, 2.2
   time_lock_hash: ByteArray
 ) {
+  // Spec 2.3
   fn mint(redeemer: StakeNFTMintRedeemer, ctx: ScriptContext) {
+    // Spec 2.3, 2.5.1
     if redeemer.mint {
+      // Spec 2.5
       mint_transaction(redeemer, ctx, time_lock_hash)?
-    } else {
+    } else { // Spec 2.6.1
+      // Spec 2.6
       burn_transaction(ctx, time_lock_hash)?
     }
   }
diff --git a/validators/stake_proxy.ak b/validators/stake_proxy.ak
index 31339cb..6e0d986 100644
--- a/validators/stake_proxy.ak
+++ b/validators/stake_proxy.ak
@@ -23,23 +23,31 @@ use staking_contracts/utils.{
 }
 use sundae/multisig.{Signature, satisfied}
 
+// Spec 4, 4.1
 validator(time_lock_hash: ByteArray, batcher_certificate) {
+  // Spec 4.2
   fn stake_proxy(
     datum: StakeProxyDatum,
     _redeemer: Void,
     ctx: ScriptContext,
   ) -> Bool {
+    // Spec 4.3
     or {
+      // Spec 4.3.1
       refund_transaction(datum, ctx)?,
+      // Spec 4.3.2
       lock_transaction(datum, ctx, time_lock_hash, batcher_certificate)?,
     }
   }
 }
 
+// Spec 4.3.1
 fn refund_transaction(datum: StakeProxyDatum, ctx: ScriptContext) -> Bool {
   when ctx.purpose is {
     //The proxy needs to be spent in a manual refund
+    // Spec 4.3.1.1
     Spend(_) ->
+      // Spec 4.3.1.2
       satisfied(
         datum.owner,
         ctx.transaction.extra_signatories,
@@ -50,6 +58,7 @@ fn refund_transaction(datum: StakeProxyDatum, ctx: ScriptContext) -> Bool {
   }
 }
 
+// Spec 4.3.2
 fn lock_transaction(
   datum: StakeProxyDatum,
   ctx: ScriptContext,
@@ -58,8 +67,11 @@ fn lock_transaction(
 ) -> Bool {
   when ctx.purpose is {
     //The proxy needs to be spend in a locking transaction by a certified batcher
+    // Spec 4.3.2.1
     Spend(my_output_reference) -> and {
+        // Spec 4.3.2.3 - 
         is_proper_locking_tx(my_output_reference, datum, ctx, time_lock_hash)?,
+        // Spec 4.3.2.2
         must_contain_asset(ctx.transaction.outputs, batcher_certificate)?,
       }
     _ -> False
@@ -68,6 +80,7 @@ fn lock_transaction(
 
 //Ensures that tokens are locked for the duration the user requests
 //and that the reward is matching the expectation
+// Spec 4.3.2.3
 fn is_proper_locking_tx(
   my_output_reference: OutputReference,
   datum: StakeProxyDatum,
@@ -80,6 +93,7 @@ fn is_proper_locking_tx(
       |> transaction.find_input(my_output_reference)
 
   //Find amount of inputs with stake proxy script, should be exactly 1
+  // Spec 4.3.2.3 - n.b. included in the `and` below
   let exactly_one_stake_proxy_input =
     length(
       filter_inputs_by_credential(
@@ -89,21 +103,27 @@ fn is_proper_locking_tx(
     ) == 1
 
   //Find the output locking the staked tokens + reward and extract its datum
+  // Spec 4.3.2.4 - n.b. existence, uniqueness is checked below
   let time_lock_outputs =
     ctx.transaction.outputs
       |> transaction.find_script_outputs(time_lock_hash)
+  // Spec 4.3.2.4 - n.b. existence, uniqueness is checked below
   expect Some(time_lock_output) = time_lock_outputs |> list.at(0)
+  // Spec 4.3.2.5
   expect InlineDatum(time_lock_output_datum) = time_lock_output.datum
   let time_lock_datum = to_time_lock_datum(time_lock_output_datum)
 
   //Time lock should have lovelace, staked asset + reference nft
+  // Spec 4.3.2.6
   expect list.length(value.flatten(time_lock_output.value)) == 3
-  //Time lock should have at least 2 ADA
+  //Time lock should have at least 2 ADA - n.b. comment incorrect
+  // Spec 4.3.2.7
   expect value.lovelace_of(time_lock_output.value) == datum.lovelace_amount
   //We assume all assets matching the policy_id+asset_name are to be staked
   let staked_tokens = datum.asset_amount
 
   //The amount of tokens locked, should be staked + reward
+  // Spec 4.3.2.8
   let locked_tokens =
     time_lock_output.value
       |> quantity_of(datum.policy_id, datum.asset_name)
@@ -111,72 +131,100 @@ fn is_proper_locking_tx(
   //Find minted stake nft
   let minted = from_minted_value(ctx.transaction.mint)
 
+  // Spec 4.3.2.9
   let minted_policy_id = bytearray.take(time_lock_datum.extra.time_lock_nft, 28)
 
+  // Spec 4.3.2.10
   let minted_asset_name =
     bytearray.drop(time_lock_datum.extra.time_lock_nft, 28)
 
   //Make sure the minted nft is using the expected policy_id
+  // Spec 4.3.2.11 - n.b. included in the `and` below
   let correct_stake_nft_policy_id = minted_policy_id == datum.nft_policy_id
 
   //Make sure only 1 is minted
+  // Spec 4.3.2.12 - n.b. included in the `and` below
   let correct_nft_minted =
     quantity_of(minted, minted_policy_id, minted_asset_name) == 1
 
   //There should be 1 destination output
+  // Spec 4.3.2.13 - "There must be exactly one"
   expect [destination_output] =
+    // Spec 4.3.2.13 - "output"
     ctx.transaction.outputs
+      // Spec 4.3.2.13 - "such that"
       |> list.filter(
            fn(o) {
-             o.address == datum.destination.address && o.datum == datum.destination.datum
+             // Spec 4.3.2.13 - "the address of the output is equal to datum.destination.address"
+             o.address == datum.destination.address
+             // Spec 4.3.2.13 - "And the datum of the output is equal to datum.destination.datum"
+             && o.datum == datum.destination.datum
            },
          )
+  // Spec 4.3.2.13 - n.b. Here, we compute the difference between the input and the two outputs sent to the user
   let lovelace_cost =
     value.lovelace_of(self.output.value) - (
       value.lovelace_of(time_lock_output.value) + value.lovelace_of(
         destination_output.value,
       )
     )
-
+  // Spec 4.3.2.13 - and here we enforce that that difference is exactly 2 ada
   expect lovelace_cost == 2_000_000
+  
   //The value of the proxy input should match the value of time_lock+destination
   //taking the lovelace cost (tx fee + sequencer fee) and reward and minted nft's into account
+  // Spec 4.3.2.15 + 4.3.2.16
   let combined_user_value =
+    // Spec 4.3.2.15.1 - "Let relevant outputs be the sum of the time lock output"
     time_lock_output.value
+    // Spec 4.3.2.15.2 - "The destination output"
       |> value.merge(destination_output.value)
+      // Spec 4.3.2.15.3 - "the 2 million lovelace fee"
       |> value.merge(value.from_lovelace(lovelace_cost))
+      // Spec 4.3.2.16.1 - "Let relevant inputs be the sum of the transaction mint" (n.b. negated because we check for equality with zero, rather than checking for equality)
       |> value.merge(value.negate(value.from_minted_value(ctx.transaction.mint)))
+      // Spec 4.3.2.16.2 - "the total value on the stake proxy input being spent" (n.b. negated because ...)
       |> value.merge(value.negate(self.output.value))
+      // Spec 4.3.2.16.3 - "the reward token from the stake pool"
       |> value.merge(
            value.negate(
              value.from_asset(
                datum.policy_id,
                datum.asset_name,
+               // Spec 4.3.2.16.3 "calculated as the difference between the tokens on the time lock output and the amount declared in the datum"
                locked_tokens - staked_tokens,
              ),
            ),
          )
-
+  // Spec 4.3.2.17 - n.b. we check equal to zero, because we subtracted off `relevant_outputs` above
   expect combined_user_value == value.zero()
+  // Spec 4.3.2.18
   expect
     quantity_of(destination_output.value, minted_policy_id, minted_asset_name) == 1
   //Ensure locked tokens is staked + reward
+  // Spec 4.3.2.20 - n.b. included in the `and` below
   let correct_locked_tokens =
     locked_tokens == add_reward(staked_tokens, datum.reward_multiplier)
 
   and {
+    // Spec 4.3.2.3
     exactly_one_stake_proxy_input?,
     //Ensure only one time lock output to avoid unexpected results
+    // Spec 4.3.2.4 - n.b. uniqueness
     must_have_exactly_one_output(time_lock_outputs)?,
+    // Spec 4.3.2.11
     correct_stake_nft_policy_id?,
     //Make sure the time lock does not lock the assets too long
+    // Spec 4.3.2.21
     must_be_locked_until(
       ctx.transaction.validity_range,
       time_lock_output,
       datum.ms_locked,
       hour_millis,
     )?,
+    // Spec 4.3.2.20
     correct_locked_tokens?,
+    // Spec 4.3.2.12
     correct_nft_minted?,
   }
 }
diff --git a/validators/time_lock.ak b/validators/time_lock.ak
index e889e53..effe5b5 100644
--- a/validators/time_lock.ak
+++ b/validators/time_lock.ak
@@ -4,12 +4,17 @@ use aiken/transaction/value.{MintedValue, from_minted_value, quantity_of}
 use staking_contracts/datums.{TimeLockDatum}
 use staking_contracts/utils.{must_start_after}
 
+// Spec 3, 3.1
 validator {
+  // Spec 3.2
   fn time_lock(datum: TimeLockDatum, _redeemer: Void, ctx: ScriptContext) {
     when ctx.purpose is {
+      // Spec 3.3.1
       //This utxo can only be spend by its owner and after the unlock time has passed
       Spend(_) -> and {
+          // Spec 3.3.2
           nft_is_burned(ctx.transaction.mint, datum.extra.time_lock_nft),
+          // Spec 3.3.3
           must_start_after(
             ctx.transaction.validity_range,
             datum.extra.lock_until,
@@ -20,8 +25,15 @@ validator {
   }
 }
 
+// Spec 3.3.2 - n.b. minted comes from transaction.mint, and nft comes from datum.extra.time_lock_nft
 fn nft_is_burned(minted: MintedValue, nft: ByteArray) {
   let minted_value = from_minted_value(minted)
-  let minted_amount = minted_value |> quantity_of(take(nft, 28), drop(nft, 28))
+  // Spec 3.3.2
+  let minted_amount = minted_value
+    |> quantity_of( // Spec 3.3.2.3
+      take(nft, 28), // Spec 3.3.2.1
+      drop(nft, 28)  // Spec 3.3.2.2
+    )
+  // Spec 3.3.2.4
   minted_amount == -1
 }

From 12127afed6f3b336c954e097226f9759241de96e Mon Sep 17 00:00:00 2001
From: Pi Lanningham <pi.lanningham@gmail.com>
Date: Mon, 26 Feb 2024 13:48:54 -0500
Subject: [PATCH 3/3] Fix typo in spec

---
 validators/stake_proxy.ak | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/validators/stake_proxy.ak b/validators/stake_proxy.ak
index 6e0d986..fad0bd7 100644
--- a/validators/stake_proxy.ak
+++ b/validators/stake_proxy.ak
@@ -80,7 +80,7 @@ fn lock_transaction(
 
 //Ensures that tokens are locked for the duration the user requests
 //and that the reward is matching the expectation
-// Spec 4.3.2.3
+// Spec 4.3.2
 fn is_proper_locking_tx(
   my_output_reference: OutputReference,
   datum: StakeProxyDatum,