key names updated

data/Template.json

@@ -79,10 +79,10 @@
       },
       "property": "When a user withdraws x amount of ETH, the user's balance should decrease by x. Due to reentrancy, an attacker can call withdraw recursively before balance is updated, draining more than their balance.",
       "property_specification": {
-        "Pre-condition": "User balance = B",
-        "Operation": "withdraw(amount)",
-        "Expected": "User balance = B - amount",
-        "Actual": "Reentrant calls allow user balance = B - (n * amount) where n > 1"
+        "precondition": "User balance = B",
+        "operation": "withdraw(amount)",
+        "postcondition": "User balance = B - amount",
+        "actual": "Reentrant calls allow user balance = B - (n * amount) where n > 1"
       }
     }
   ],
@@ -130,10 +130,10 @@
       "mitigation": "Moved balance update before external call (checks-effects-interactions pattern)",
       "property": "When a user withdraws x amount, the user's balance should decrease by x. Due to reentrancy, an attacker can withdraw multiple times before balance updates, draining more than their balance.",
       "property_specification": {
-        "Pre-condition": "User balance = B",
-        "Operation": "withdraw(amount)",
-        "Expected": "User balance = B - amount",
-        "Actual": "Reentrant calls allow user balance = B - (n * amount) where n > 1"
+        "precondition": "User balance = B",
+        "operation": "withdraw(amount)",
+        "postcondition": "User balance = B - amount",
+        "actual": "Reentrant calls allow user balance = B - (n * amount) where n > 1"
       }
     }
   ],

data/contracts.json

@@ -228,7 +228,7 @@
                     "precondition": "User has AToken balance B",
                     "operation": "burn(user, receiver, amount, index)",
                     "expected_postcondition": "User's AToken balance = B - amount (within rounding tolerance ε)",
-                    "actual_vulnerability": "When amount.rayDiv(index) rounds down to 0, the burn operation transfers amount underlying tokens but burns 0 ATokens, resulting in user AToken balance unchanged = B, violating the expected post-condition where the balance should be B - amount."
+                    "actual": "When amount.rayDiv(index) rounds down to 0, the burn operation transfers amount underlying tokens but burns 0 ATokens, resulting in user AToken balance unchanged = B, violating the postcondition where the balance should be B - amount."
                 }
             },
             {
@@ -672,7 +672,7 @@
                 "status": "Fixed",
                 "mitigation": "Added require(amountScaled != 0, Errors.CT_INVALID_BURN_AMOUNT) to prevent zero-value burns",
                 "property": "When a user burns x amount of ATokens, the user's AToken balance should decrease by x, and the user should receive x amount of underlying tokens. Due to rounding errors in conversion, a user could receive underlying tokens without burning any ATokens, breaking the invariant that burning decreases AToken balance proportionally to the underlying amount transferred.",
-                "property_specification": "precondition: User has AToken balance B. Operation: burn(user, receiver, amount, index). Expected post-condition: User's AToken balance = B - amount (within rounding tolerance ε). Actual vulnerability: When amount.rayDiv(index) rounds down to 0, the burn operation transfers amount underlying tokens but burns 0 ATokens, resulting in user AToken balance unchanged = B, violating the expected post-condition where the balance should be B - amount."
+                "property_specification": "precondition: User has AToken balance B. operation: burn(user, receiver, amount, index). postcondition: User's AToken balance = B - amount (within rounding tolerance ε). actual vulnerability: When amount.rayDiv(index) rounds down to 0, the burn operation transfers amount underlying tokens but burns 0 ATokens, resulting in user AToken balance unchanged = B, violating the postcondition where the balance should be B - amount."
             }
         ],
         "events": [
@@ -935,7 +935,7 @@
                     "precondition": "User has debt balance B",
                     "operation": "mint(user, onBehalfOf, amount, rate)",
                     "expected_postcondition": "User's debt balance = B + amount (within rounding tolerance ε)",
-                    "actual_vulnerability": "When amount conversion rounds down to 0 in intermediate calculations, the mint operation may mint zero debt tokens while still transferring underlying tokens (or vice versa), resulting in user debt balance unchanged = B, violating the expected post-condition where the balance should be B + amount."
+                    "actual": "When amount conversion rounds down to 0 in intermediate calculations, the mint operation may mint zero debt tokens while still transferring underlying tokens (or vice versa), resulting in user debt balance unchanged = B, violating the postcondition where the balance should be B + amount."
                 }
             },
             {
@@ -1255,7 +1255,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed to avoid transfer on mint/burn of zero stable debt tokens",
                 "property": "When a user mints x amount of stable debt tokens, the user's debt balance should increase by x, and the protocol should receive x amount of underlying tokens from the user. Due to rounding errors in conversion, a user could receive debt tokens without transferring underlying tokens, or could transfer underlying tokens without receiving debt tokens, breaking the invariant that minting increases debt balance proportionally to underlying amount transferred.",
-                "property_specification": "precondition: User has debt balance B. Operation: mint(user, onBehalfOf, amount, rate). Expected post-condition: User's debt balance = B + amount (within rounding tolerance ε). Actual vulnerability: When amount conversion rounds down to 0 in intermediate calculations, the mint operation may mint zero debt tokens while still transferring underlying tokens (or vice versa), resulting in user debt balance unchanged = B, violating the expected post-condition where the balance should be B + amount."
+                "property_specification": "precondition: User has debt balance B. operation: mint(user, onBehalfOf, amount, rate). postcondition: User's debt balance = B + amount (within rounding tolerance ε). actual vulnerability: When amount conversion rounds down to 0 in intermediate calculations, the mint operation may mint zero debt tokens while still transferring underlying tokens (or vice versa), resulting in user debt balance unchanged = B, violating the postcondition where the balance should be B + amount."
             }
         ],
         "events": [
@@ -2113,9 +2113,9 @@
                 "property": "MUST return as close to, and no more than, the exact amount of Vault shares that would be minted in a deposit() call in the same transaction",
                 "property_specification": {
                     "precondition": "The vault has a maximum deposit limit L",
-                    "Operation": "A user calls previewDeposit(x) for an amount x > L",
-                    "Expected post-condition": "previewDeposit(x) returns the same number of shares as it would for x = L (since the function should not account for limits)",
-                    "Actual vulnerability": "previewDeposit(x) returns the number of shares for L (due to min(x, L)), which is different from what it would return for an amount x' where x' > L, implying the function accounts for the limit, violating the EIP."
+                    "operation": "A user calls previewDeposit(x) for an amount x > L",
+                    "postcondition": "previewDeposit(x) returns the same number of shares as it would for x = L (since the function should not account for limits)",
+                    "actual": "previewDeposit(x) returns the number of shares for L (due to min(x, L)), which is different from what it would return for an amount x' where x' > L, implying the function accounts for the limit, violating the EIP."
                 }
             },
             {
@@ -2145,9 +2145,9 @@
                 "property": "MUST return as close to, and no more than, the exact amount of Vault shares that would be minted in a deposit() call in the same transaction",
                 "property_specification": {
                     "precondition": "The vault has a maximum deposit limit",
-                    "Operation": "A user calls previewMint(y) for a number of shares y that would require more than L in assets",
-                    "Expected post-condition": "previewMint(y) returns the amount of assets needed to mint y shares without accounting for limits",
-                    "Actual vulnerability": "previewMint(y) returns the assets for y shares but capped at L, implying the function accounts for the deposit limit, violating the EIP."
+                    "operation": "A user calls previewMint(y) for a number of shares y that would require more than L in assets",
+                    "postcondition": "previewMint(y) returns the amount of assets needed to mint y shares without accounting for limits",
+                    "actual": "previewMint(y) returns the assets for y shares but capped at L, implying the function accounts for the deposit limit, violating the EIP."
                 }
             },
             {
@@ -2177,9 +2177,9 @@
                 "property": "previewWithdraw() MUST NOT account for withdrawal limits like those returned from maxWithdraw()",
                 "property_specification": {
                     "precondition": "The vault has available liquidity",
-                    "Operation": "A user calls previewWithdraw(x) for an amount x > L",
-                    "Expected post-condition": "previewWithdraw(x) returns the number of shares needed to withdraw x assets without accounting for limits",
-                    "Actual vulnerability": "previewWithdraw(x) returns the number of shares for L (due to min(x, L)), implying the function accounts for the withdrawal limit, violating the EIP-4626 standard"
+                    "operation": "A user calls previewWithdraw(x) for an amount x > L",
+                    "postcondition": "previewWithdraw(x) returns the number of shares needed to withdraw x assets without accounting for limits",
+                    "actual": "previewWithdraw(x) returns the number of shares for L (due to min(x, L)), implying the function accounts for the withdrawal limit, violating the EIP-4626 standard"
                 }
             },
             {
@@ -2209,9 +2209,9 @@
                 "property": "previewWithdraw() MUST NOT account for withdrawal limits like those returned from maxWithdraw()",
                 "property_specification": {
                     "precondition": "The vault has available liquidity",
-                    "Operation": "A user calls previewRedeem(y) for a number of shares y that would require more than L in assets",
-                    "Expected post-condition": "previewRedeem(y) returns the amount of assets that would be received for y shares without accounting for limits",
-                    "Actual vulnerability": "previewRedeem(y) returns the assets for y shares but capped at L, implying the function accounts for the withdrawal limit, violating the EIP-4626 standard"
+                    "operation": "A user calls previewRedeem(y) for a number of shares y that would require more than L in assets",
+                    "postcondition": "previewRedeem(y) returns the amount of assets that would be received for y shares without accounting for limits",
+                    "actual": "previewRedeem(y) returns the assets for y shares but capped at L, implying the function accounts for the withdrawal limit, violating the EIP-4626 standard"
                 }
             },
             {
@@ -2372,9 +2372,9 @@
                 "property": "totalAssets must never revert",
                 "property_specification": {
                     "precondition": "The vault's state has claimable fees greater than its aToken balance",
-                    "Operation": "A user calls totalAssets()",
-                    "Expected post-condition": "The function returns a value without reverting",
-                    "Actual vulnerability": "The function attempts to compute ATOKEN.balanceOf(address(this)) - getClaimableFees(), which underflows and reverts, violating the EIP-4626 standard"
+                    "operation": "A user calls totalAssets()",
+                    "postcondition": "The function returns a value without reverting",
+                    "actual": "The function attempts to compute ATOKEN.balanceOf(address(this)) - getClaimableFees(), which underflows and reverts, violating the EIP-4626 standard"
                 }
             },
             {
@@ -3026,7 +3026,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#82 merged in commit 385b397.",
                 "property": "When a user deposits an amount of underlying tokens, the vault's internal state variable lastVaultBalance should be updated to match the actual aToken balance. Due to rounding in aToken's balance updates, the lastVaultBalance could become mismatched, leading to a permanent revert state for any function that calls accrueYield().",
-                "property_specification": "precondition: The vault has a current aToken balance B and lastVaultBalance = B. Operation: A user deposits an amount of underlying tokens that, after conversion to aTokens, results in a balance B' that is not exactly represented due to rayMath rounding. Expected post-condition: lastVaultBalance is updated to B'. Actual vulnerability: The deposit function updates lastVaultBalance with the exact deposit amount, while aToken uses rayMath for its balance, causing a mismatch. This mismatch can accumulate over multiple operations, leading to a state where the lastVaultBalance is less than the actual balance, causing the yield calculation to revert."
+                "property_specification": "precondition: The vault has a current aToken balance B and lastVaultBalance = B. operation: A user deposits an amount of underlying tokens that, after conversion to aTokens, results in a balance B' that is not exactly represented due to rayMath rounding. postcondition: lastVaultBalance is updated to B'. actual vulnerability: The deposit function updates lastVaultBalance with the exact deposit amount, while aToken uses rayMath for its balance, causing a mismatch. This mismatch can accumulate over multiple operations, leading to a state where the lastVaultBalance is less than the actual balance, causing the yield calculation to revert."
             },
             {
                 "function": "getClaimableFees",
@@ -3036,7 +3036,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#86 merged in commit 385b397.",
                 "property": "After every fee accrual, the vault's internal lastVaultBalance should equal the actual aToken balance. Due to rounding differences between how the vault updates lastVaultBalance (exact) and how aToken updates its balance (rayMath), a mismatch of up to 1 unit can occur per deposit/withdraw. Over many operations, this mismatch can accumulate, causing the vault to either undercharge fees (losing fee revenue) or overcharge fees (taking more than its fair share).",
-                "property_specification": "precondition: The vault has lastVaultBalance = aToken balance (B) and accumulatedFees = F. Operation: A user deposits or withdraws an amount that, after aToken's rayMath rounding, results in a new aToken balance B' that differs from the vault's update by Δ (where |Δ| ≤ 1). Expected post-condition: lastVaultBalance = B' and fee accrual is based on the correct new yield. Actual vulnerability: The vault updates lastVaultBalance with the exact asset amount, but the aToken balance uses rounded values. This creates a persistent difference that affects future fee calculations, leading to either loss of fees (if lastVaultBalance > actual balance) or overcharging fees (if lastVaultBalance < actual balance)."
+                "property_specification": "precondition: The vault has lastVaultBalance = aToken balance (B) and accumulatedFees = F. operation: A user deposits or withdraws an amount that, after aToken's rayMath rounding, results in a new aToken balance B' that differs from the vault's update by Δ (where |Δ| ≤ 1). postcondition: lastVaultBalance = B' and fee accrual is based on the correct new yield. actual vulnerability: The vault updates lastVaultBalance with the exact asset amount, but the aToken balance uses rounded values. This creates a persistent difference that affects future fee calculations, leading to either loss of fees (if lastVaultBalance > actual balance) or overcharging fees (if lastVaultBalance < actual balance)."
             },
             {
                 "function": "previewRedeem",
@@ -3046,7 +3046,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#82 merged in commit 385b397.",
                 "property": "The previewRedeem function should return the amount of assets that would be received if the redemption were executed immediately. However, because the preview function does not account for the yield accrual that would happen during the actual redemption, it can return a larger amount than what is actually redeemable.",
-                "property_specification": "precondition: The vault has some yield that has not been accrued, and a fee is set. Operation: A user calls previewRedeem(shares) to see how many assets they would get for redeeming a certain number of shares. Expected post-condition: The function returns the exact amount of assets that would be received if redeem(shares) were called immediately. Actual vulnerability: previewRedeem does not simulate the fee deduction that would occur in _accrueYield() during the actual redeem transaction, leading to an overestimation of the assets that would be received."
+                "property_specification": "precondition: The vault has some yield that has not been accrued, and a fee is set. operation: A user calls previewRedeem(shares) to see how many assets they would get for redeeming a certain number of shares. postcondition: The function returns the exact amount of assets that would be received if redeem(shares) were called immediately. actual vulnerability: previewRedeem does not simulate the fee deduction that would occur in _accrueYield() during the actual redeem transaction, leading to an overestimation of the assets that would be received."
             },
             {
                 "function": "withdrawFees",
@@ -3056,7 +3056,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#82 merged in commit 385b397.",
                 "property": "When the owner withdraws fees, they should receive fees on all yield earned up to that point, including any recent gifts to the protocol. However, an attacker can frontrun the fee withdrawal to make the gift after the accrual but before the withdrawal, causing the gift to be excluded from fees.",
-                "property_specification": "precondition: The owner intends to withdraw fees. Operation: An attacker triggers _accrueYield() (by making a small deposit) before the owner calls withdrawFees. After the accrual, the attacker gifts aTokens directly to the vault. Expected post-condition: When the owner calls withdrawFees, the fees on the gifted amount are included. Actual vulnerability: withdrawFees uses the stored accumulatedFees from before the gift, rather than recalculating fees on the new balance, allowing the gifted amount to be withdrawn by the owner without paying fees to the fee collector."
+                "property_specification": "precondition: The owner intends to withdraw fees. operation: An attacker triggers _accrueYield() (by making a small deposit) before the owner calls withdrawFees. After the accrual, the attacker gifts aTokens directly to the vault. postcondition: When the owner calls withdrawFees, the fees on the gifted amount are included. actual vulnerability: withdrawFees uses the stored accumulatedFees from before the gift, rather than recalculating fees on the new balance, allowing the gifted amount to be withdrawn by the owner without paying fees to the fee collector."
             },
             {
                 "function": "previewDeposit",
@@ -3066,7 +3066,7 @@
                 "status": "Acknowledged",
                 "mitigation": "As per EIP4626, all the preview functions may revert due to other conditions that would also cause primary functions to revert. Relying on Aave is acceptable, given that primary functions are impacted by its limitations (e.g. users cannot withdraw if there is no available liquidity in the Aave Pool).",
                 "property": "The previewDeposit function should return the number of shares that would be minted for a given deposit amount, independent of any deposit limits. However, this implementation caps the deposit amount by the maximum deposit limit, which violates the EIP-4626 requirement.",
-                "property_specification": "precondition: The vault has a maximum deposit limit L. Operation: A user calls previewDeposit(x) for an amount x > L. Expected post-condition: previewDeposit(x) returns the same number of shares as it would for x = L (since the function should not account for limits). Actual vulnerability: previewDeposit(x) returns the number of shares for L (due to min(x, L)), which is different from what it would return for an amount x' where x' > L, implying the function accounts for the limit, violating the EIP."
+                "property_specification": "precondition: The vault has a maximum deposit limit L. operation: A user calls previewDeposit(x) for an amount x > L. postcondition: previewDeposit(x) returns the same number of shares as it would for x = L (since the function should not account for limits). actual vulnerability: previewDeposit(x) returns the number of shares for L (due to min(x, L)), which is different from what it would return for an amount x' where x' > L, implying the function accounts for the limit, violating the EIP."
             },
             {
                 "function": "previewMint",
@@ -3076,7 +3076,7 @@
                 "status": "Acknowledged",
                 "mitigation": "As per EIP4626, all the preview functions may revert due to other conditions that would also cause primary functions to revert. Relying on Aave is acceptable, given that primary functions are impacted by its limitations (e.g. users cannot withdraw if there is no available liquidity in the Aave Pool).",
                 "property": "The previewMint function should return the amount of assets needed to mint a given number of shares, independent of any minting limits. However, this implementation caps the result by the maximum deposit limit, which violates the EIP-4626 requirement.",
-                "property_specification": "precondition: The vault has a maximum deposit limit L. Operation: A user calls previewMint(y) for a number of shares y that would require more than L in assets. Expected post-condition: previewMint(y) returns the amount of assets needed to mint y shares without accounting for limits. Actual vulnerability: previewMint(y) returns the assets for y shares but capped at L, implying the function accounts for the deposit limit, violating the EIP."
+                "property_specification": "precondition: The vault has a maximum deposit limit L. operation: A user calls previewMint(y) for a number of shares y that would require more than L in assets. postcondition: previewMint(y) returns the amount of assets needed to mint y shares without accounting for limits. actual vulnerability: previewMint(y) returns the assets for y shares but capped at L, implying the function accounts for the deposit limit, violating the EIP."
             },
             {
                 "function": "previewWithdraw",
@@ -3086,7 +3086,7 @@
                 "status": "Acknowledged",
                 "mitigation": "As per EIP4626, all the preview functions may revert due to other conditions that would also cause primary functions to revert. Relying on Aave is acceptable, given that primary functions are impacted by its limitations (e.g. users cannot withdraw if there is no available liquidity in the Aave Pool).",
                 "property": "The previewWithdraw function should return the number of shares needed to withdraw a given amount of assets, independent of any withdrawal limits. However, this implementation caps the withdrawal amount by the available liquidity, which violates the EIP-4626 requirement.",
-                "property_specification": "precondition: The vault has available liquidity L. Operation: A user calls previewWithdraw(x) for an amount x > L. Expected post-condition: previewWithdraw(x) returns the number of shares needed to withdraw x assets without accounting for limits. Actual vulnerability: previewWithdraw(x) returns the number of shares for L (due to min(x, L)), implying the function accounts for the withdrawal limit, violating the EIP."
+                "property_specification": "precondition: The vault has available liquidity L. operation: A user calls previewWithdraw(x) for an amount x > L. postcondition: previewWithdraw(x) returns the number of shares needed to withdraw x assets without accounting for limits. actual vulnerability: previewWithdraw(x) returns the number of shares for L (due to min(x, L)), implying the function accounts for the withdrawal limit, violating the EIP."
             },
             {
                 "function": "previewRedeem",
@@ -3096,7 +3096,7 @@
                 "status": "Acknowledged",
                 "mitigation": "As per EIP4626, all the preview functions may revert due to other conditions that would also cause primary functions to revert. Relying on Aave is acceptable, given that primary functions are impacted by its limitations (e.g. users cannot withdraw if there is no available liquidity in the Aave Pool).",
                 "property": "The previewRedeem function should return the amount of assets that would be received for redeeming a given number of shares, independent of any redemption limits. However, this implementation caps the result by the available liquidity, which violates the EIP-4626 requirement.",
-                "property_specification": "precondition: The vault has available liquidity L. Operation: A user calls previewRedeem(y) for a number of shares y that would require more than L in assets. Expected post-condition: previewRedeem(y) returns the amount of assets that would be received for y shares without accounting for limits. Actual vulnerability: previewRedeem(y) returns the assets for y shares but capped at L, implying the function accounts for the withdrawal limit, violating the EIP."
+                "property_specification": "precondition: The vault has available liquidity L. operation: A user calls previewRedeem(y) for a number of shares y that would require more than L in assets. postcondition: previewRedeem(y) returns the amount of assets that would be received for y shares without accounting for limits. actual vulnerability: previewRedeem(y) returns the assets for y shares but capped at L, implying the function accounts for the withdrawal limit, violating the EIP."
             },
             {
                 "function": "totalAssets",
@@ -3106,7 +3106,7 @@
                 "status": "Acknowledged",
                 "mitigation": "Although conforming to a standard is important and even essential to a degree, there is likely little to be gained from modifying and altering the core code's functionality to adapt to the minutiae of the standard. As the vault relies inherently on the Aave Protocol, it is acceptable to revert due to Aave-specific calculations.",
                 "property": "The totalAssets function should never revert. However, because it computes aToken balance minus claimable fees, it can revert if the claimable fees exceed the aToken balance due to previous mismatches.",
-                "property_specification": "precondition: The vault's state has claimable fees greater than its aToken balance. Operation: A user calls totalAssets(). Expected post-condition: The function returns a value without reverting. Actual vulnerability: The function attempts to compute ATOKEN.balanceOf(address(this)) - getClaimableFees(), which underflows and reverts, violating the EIP."
+                "property_specification": "precondition: The vault's state has claimable fees greater than its aToken balance. operation: A user calls totalAssets(). postcondition: The function returns a value without reverting. actual vulnerability: The function attempts to compute ATOKEN.balanceOf(address(this)) - getClaimableFees(), which underflows and reverts, violating the EIP."
             }
         ],
         "events": [
@@ -3683,9 +3683,9 @@
                 "property": "Each withdrawal request should receive ETH proportional to its share rate at finalization, independent of other requests in the same batch.",
                 "property_specification": {
                     "precondition": "User A has request with shareRate RA, User B with shareRate RB, RA < RB, both in same batch. Slashing causes final shareRate S where RA < S < RB",
-                    "Operation": "finalize(batch)",
-                    "Expected post-condition": "A receives amount based on RA, B receives amount based on RB",
-                    "Actual vulnerability": "Weighted average calculation causes A to receive less than expected and B to receive more, with A subsidizing B's losses."
+                    "operation": "finalize(batch)",
+                    "postcondition": "A receives amount based on RA, B receives amount based on RB",
+                    "actual": "Weighted average calculation causes A to receive less than expected and B to receive more, with A subsidizing B's losses."
                 }
             },
             {
@@ -4048,7 +4048,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in commit 336b6f3. The withdrawals finalization process was changed to remove the discount factor in favor of share rate batch-wise calculation approach.",
                 "property": "Each withdrawal request should receive ETH proportional to its share rate at finalization, independent of other requests in the same batch.",
-                "property_specification": "precondition: User A has request with shareRate RA, User B with shareRate RB, RA < RB, both in same batch. Slashing causes final shareRate S where RA < S < RB. Operation: finalize(batch). Expected post-condition: A receives amount based on RA, B receives amount based on RB. Actual vulnerability: Weighted average calculation causes A to receive less than expected and B to receive more, with A subsidizing B's losses."
+                "property_specification": "precondition: User A has request with shareRate RA, User B with shareRate RB, RA < RB, both in same batch. Slashing causes final shareRate S where RA < S < RB. operation: finalize(batch). postcondition: A receives amount based on RA, B receives amount based on RB. actual vulnerability: Weighted average calculation causes A to receive less than expected and B to receive more, with A subsidizing B's losses."
             },
             {
                 "function": "finalize",
@@ -4058,7 +4058,7 @@
                 "status": "Acknowledged",
                 "mitigation": "The contract is upgradeable; locked funds can be recovered via DAO vote by upgrading the implementation. Also strict on-chain batch validation was considered too complex.",
                 "property": "The total ETH sent to the withdrawalQueue for finalization must exactly match the sum of claimable amounts for all requests in the batch.",
-                "property_specification": "precondition: Two requests with different share rates are placed in the same batch. Operation: finalize(batch) with ETH amount calculated based on incorrect batching. Expected post-condition: All claimable amounts sum to the ETH sent. Actual vulnerability: More ETH is sent than can be claimed, leaving residual ETH permanently locked in the contract."
+                "property_specification": "precondition: Two requests with different share rates are placed in the same batch. operation: finalize(batch) with ETH amount calculated based on incorrect batching. postcondition: All claimable amounts sum to the ETH sent. actual vulnerability: More ETH is sent than can be claimed, leaving residual ETH permanently locked in the contract."
             },
             {
                 "function": "finalize",
@@ -4068,7 +4068,7 @@
                 "status": "Acknowledged",
                 "mitigation": "Accepted as intended behavior; edge cases are rare and deviations are tiny in real scenarios. Complex iterative approach would introduce more risks.",
                 "property": "Users who entered the queue with higher share rates should fully recover when the protocol's share rate recovers, regardless of batching.",
-                "property_specification": "precondition: User A (shareRate 1.0) and User B (shareRate 2.0) are in same batch. Final shareRate after recovery is 1.5. Operation: finalize(batch). Expected post-condition: User B receives 1.666 ETH (as if finalized separately). Actual vulnerability: User B receives only 1.5 ETH, losing value compared to separate batch finalization."
+                "property_specification": "precondition: User A (shareRate 1.0) and User B (shareRate 2.0) are in same batch. Final shareRate after recovery is 1.5. operation: finalize(batch). postcondition: User B receives 1.666 ETH (as if finalized separately). actual vulnerability: User B receives only 1.5 ETH, losing value compared to separate batch finalization."
             }
         ],
         "events": [
@@ -4306,7 +4306,7 @@
                     "mitigation": "Add a check to ensure that the scaled amount to burn is greater than zero before performing the burn and transfer, or avoid transfer when the burned amount is zero."
                 },
                 "property": "The total assets of a user should decrease exactly by the amount of underlying withdrawn. Rounding should not allow a user to receive underlying without a corresponding decrease in AToken balance.",
-                "property_specification": "Pre-condition: User has AToken balance B, underlying asset balance of AToken contract is sufficient. Operation: burn(user, receiver, amount, index) where amount > 0 but amount.rayDiv(index) == 0 due to rounding. Expected post-condition: User's AToken balance decreases by the scaled amount (which is zero) and underlying amount is transferred, so user's net position decreases by amount of underlying. Actual vulnerability: User's AToken balance does not change (burn of zero), but user receives underlying amount, resulting in a net gain of underlying without any reduction in AToken balance, violating the expected invariant that AToken burn should correspond to underlying transfer."
+                "property_specification": "precondition: User has AToken balance B, underlying asset balance of AToken contract is sufficient. operation: burn(user, receiver, amount, index) where amount > 0 but amount.rayDiv(index) == 0 due to rounding. postcondition: User's AToken balance decreases by the scaled amount (which is zero) and underlying amount is transferred, so user's net position decreases by amount of underlying. actual vulnerability: User's AToken balance does not change (burn of zero), but user receives underlying amount, resulting in a net gain of underlying without any reduction in AToken balance, violating the expected invariant that AToken burn should correspond to underlying transfer."
             },
             {
                 "name": "mint",
@@ -4800,7 +4800,7 @@
                 "status": "Fixed",
                 "mitigation": "Add a check to ensure that the scaled amount to burn is greater than zero before performing the burn and transfer, or avoid transfer when the burned amount is zero.",
                 "property": "The total assets of a user should decrease exactly by the amount of underlying withdrawn. Rounding should not allow a user to receive underlying without a corresponding decrease in AToken balance.",
-                "property_specification": "Pre-condition: User has AToken balance B, underlying asset balance of AToken contract is sufficient. Operation: burn(user, receiver, amount, index) where amount > 0 but amount.rayDiv(index) == 0 due to rounding. Expected post-condition: User's AToken balance decreases by the scaled amount (which is zero) and underlying amount is transferred, so user's net position decreases by amount of underlying. Actual vulnerability: User's AToken balance does not change (burn of zero), but user receives underlying amount, resulting in a net gain of underlying without any reduction in AToken balance, violating the expected invariant that AToken burn should correspond to underlying transfer."
+                "property_specification": "precondition: User has AToken balance B, underlying asset balance of AToken contract is sufficient. operation: burn(user, receiver, amount, index) where amount > 0 but amount.rayDiv(index) == 0 due to rounding. postcondition: User's AToken balance decreases by the scaled amount (which is zero) and underlying amount is transferred, so user's net position decreases by amount of underlying. actual vulnerability: User's AToken balance does not change (burn of zero), but user receives underlying amount, resulting in a net gain of underlying without any reduction in AToken balance, violating the expected invariant that AToken burn should correspond to underlying transfer."
             }
         ],
         "events": [
@@ -5046,7 +5046,7 @@
                     "mitigation": "Add a check to ensure that the amount after conversion to ray is greater than zero before minting, or avoid minting when the minted amount would be zero."
                 },
                 "property": "When a user borrows (mints debt), their debt balance should increase exactly by the borrowed amount (plus accrued interest). Rounding should not allow a user to receive underlying without a corresponding increase in debt.",
-                "property_specification": "Pre-condition: User has debt balance D, total supply S. Operation: mint(user, amount, rate) where amount > 0 but amount.wadToRay() == 0 due to rounding. Expected post-condition: User's debt balance increases by amount (scaled appropriately). Actual vulnerability: User's debt balance does not increase (mint of zero), but the LendingPool would transfer underlying to the user, resulting in a net gain without debt increase, violating the invariant that debt minting should correspond to underlying received."
+                "property_specification": "precondition: User has debt balance D, total supply S. operation: mint(user, amount, rate) where amount > 0 but amount.wadToRay() == 0 due to rounding. postcondition: User's debt balance increases by amount (scaled appropriately). actual vulnerability: User's debt balance does not increase (mint of zero), but the LendingPool would transfer underlying to the user, resulting in a net gain without debt increase, violating the invariant that debt minting should correspond to underlying received."
             },
             {
                 "name": "burn",
@@ -5358,7 +5358,7 @@
                 "status": "Fixed",
                 "mitigation": "Add a check to ensure that the amount after conversion to ray is greater than zero before minting, or avoid minting when the minted amount would be zero.",
                 "property": "When a user borrows (mints debt), their debt balance should increase exactly by the borrowed amount (plus accrued interest). Rounding should not allow a user to receive underlying without a corresponding increase in debt.",
-                "property_specification": "Pre-condition: User has debt balance D, total supply S. Operation: mint(user, amount, rate) where amount > 0 but amount.wadToRay() == 0 due to rounding. Expected post-condition: User's debt balance increases by amount (scaled appropriately). Actual vulnerability: User's debt balance does not increase (mint of zero), but the LendingPool would transfer underlying to the user, resulting in a net gain without debt increase, violating the invariant that debt minting should correspond to underlying received."
+                "property_specification": "precondition: User has debt balance D, total supply S. operation: mint(user, amount, rate) where amount > 0 but amount.wadToRay() == 0 due to rounding. postcondition: User's debt balance increases by amount (scaled appropriately). actual vulnerability: User's debt balance does not increase (mint of zero), but the LendingPool would transfer underlying to the user, resulting in a net gain without debt increase, violating the invariant that debt minting should correspond to underlying received."
             }
         ],
         "events": [
@@ -5519,7 +5519,7 @@
                     "mitigation": "Add require(owner != address(0), 'INVALID_OWNER');"
                 },
                 "property": "The contract must have a non-zero owner to allow administrative functions to be callable.",
-                "property_specification": "Pre-condition: Owner address can be any address. Operation: initialize(owner, ...) where owner == address(0). Expected post-condition: The contract owner is address(0) and administrative functions are permanently locked. Actual vulnerability: The owner becomes zero address, violating the invariant that owner must be a valid address capable of executing privileged functions."
+                "property_specification": "precondition: Owner address can be any address. operation: initialize(owner, ...) where owner == address(0). postcondition: The contract owner is address(0) and administrative functions are permanently locked. actual vulnerability: The owner becomes zero address, violating the invariant that owner must be a valid address capable of executing privileged functions."
             },
             {
                 "name": "deposit",
@@ -5553,7 +5553,7 @@
                     "mitigation": "Fixed in PR#82 merged in commit 385b397."
                 },
                 "property": "After a deposit, the vault should remain in a consistent state where subsequent operations do not revert due to internal accounting mismatches.",
-                "property_specification": "Pre-condition: Vault state is consistent, lastVaultBalance equals ATOKEN.balanceOf(vault). Operation: deposit(assets) where assets is not a multiple of liquidity index. Expected post-condition: Vault remains consistent, lastVaultBalance == ATOKEN.balanceOf(vault) after deposit. Actual vulnerability: lastVaultBalance is incremented by assets, but ATOKEN.balanceOf increases by a different amount due to rounding, leading to inconsistency that causes future accrueYield() calls to revert."
+                "property_specification": "precondition: Vault state is consistent, lastVaultBalance equals ATOKEN.balanceOf(vault). operation: deposit(assets) where assets is not a multiple of liquidity index. postcondition: Vault remains consistent, lastVaultBalance == ATOKEN.balanceOf(vault) after deposit. actual vulnerability: lastVaultBalance is incremented by assets, but ATOKEN.balanceOf increases by a different amount due to rounding, leading to inconsistency that causes future accrueYield() calls to revert."
             },
             {
                 "name": "depositATokens",
@@ -5587,7 +5587,7 @@
                     "mitigation": "Fixed in PR#80, merged in commit 34ad6e3."
                 },
                 "property": "Depositing aTokens (which already represent Aave positions) should not be limited by the Aave pool's supply cap because it does not increase net supply to the pool.",
-                "property_specification": "Pre-condition: Aave pool has a supply cap, and the total supplied is near the cap. The vault holds aTokens whose underlying value would push the cap over if deposited as underlying. Operation: depositATokens(assets) with assets amount that converts to underlying value exceeding remaining cap. Expected post-condition: Deposit should succeed because no new underlying is supplied to Aave. Actual vulnerability: The function reverts due to the supply cap check, preventing legitimate aToken deposits."
+                "property_specification": "precondition: Aave pool has a supply cap, and the total supplied is near the cap. The vault holds aTokens whose underlying value would push the cap over if deposited as underlying. operation: depositATokens(assets) with assets amount that converts to underlying value exceeding remaining cap. postcondition: Deposit should succeed because no new underlying is supplied to Aave. actual vulnerability: The function reverts due to the supply cap check, preventing legitimate aToken deposits."
             },
             {
                 "name": "depositWithSig",
@@ -5870,7 +5870,7 @@
                     "mitigation": "Fixed in PR#86 merged in commit 385b397."
                 },
                 "property": "After any deposit or withdrawal, lastVaultBalance should equal ATOKEN.balanceOf(vault) to ensure accurate fee calculation on future yield.",
-                "property_specification": "Pre-condition: lastVaultBalance = ATOKEN.balanceOf(vault) = B. Operation: withdraw(assets) where assets is not a multiple of the liquidity index. Expected post-condition: lastVaultBalance' = ATOKEN.balanceOf(vault)' = B - assets_actual. Actual vulnerability: lastVaultBalance is decreased by assets (exact), but ATOKEN.balanceOf decreases by a different amount due to rounding, causing a mismatch that leads to fee miscalculation."
+                "property_specification": "precondition: lastVaultBalance = ATOKEN.balanceOf(vault) = B. operation: withdraw(assets) where assets is not a multiple of the liquidity index. postcondition: lastVaultBalance' = ATOKEN.balanceOf(vault)' = B - assets_actual. actual vulnerability: lastVaultBalance is decreased by assets (exact), but ATOKEN.balanceOf decreases by a different amount due to rounding, causing a mismatch that leads to fee miscalculation."
             },
             {
                 "name": "withdrawATokens",
@@ -6422,7 +6422,7 @@
                     "mitigation": "Fixed in PR#82 merged in commit 385b397."
                 },
                 "property": "All yield generated by the vault, including gifts, should be subject to fee accrual before fees are withdrawn.",
-                "property_specification": "Pre-condition: Vault has lastUpdated = T (current block), and some user gifts aTokens to the vault in the same block after a transaction that set lastUpdated. Operation: withdrawFees() called after the gift. Expected post-condition: The gift amount is included in new yield and fees are charged on it. Actual vulnerability: getClaimableFees() returns accumulatedFees from before the gift because block.timestamp == lastUpdated, so no new fees are calculated, allowing the gift to bypass fee charges."
+                "property_specification": "precondition: Vault has lastUpdated = T (current block), and some user gifts aTokens to the vault in the same block after a transaction that set lastUpdated. operation: withdrawFees() called after the gift. postcondition: The gift amount is included in new yield and fees are charged on it. actual vulnerability: getClaimableFees() returns accumulatedFees from before the gift because block.timestamp == lastUpdated, so no new fees are calculated, allowing the gift to bypass fee charges."
             },
             {
                 "name": "claimRewards",
@@ -7158,7 +7158,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#82 merged in commit 385b397.",
                 "property": "After a deposit, the vault's internal lastVaultBalance must exactly match the actual aToken balance to ensure subsequent operations do not revert.",
-                "property_specification": "Pre-condition: lastVaultBalance == ATOKEN.balanceOf(vault). Operation: deposit(assets) where assets is not a multiple of the liquidity index. Expected post-condition: lastVaultBalance' == ATOKEN.balanceOf(vault)'. Actual vulnerability: lastVaultBalance is incremented by assets, but ATOKEN.balanceOf increases by a different rounded amount, causing a permanent mismatch that leads to underflow/overflow in future accruals, causing reverts."
+                "property_specification": "precondition: lastVaultBalance == ATOKEN.balanceOf(vault). operation: deposit(assets) where assets is not a multiple of the liquidity index. postcondition: lastVaultBalance' == ATOKEN.balanceOf(vault)'. actual vulnerability: lastVaultBalance is incremented by assets, but ATOKEN.balanceOf increases by a different rounded amount, causing a permanent mismatch that leads to underflow/overflow in future accruals, causing reverts."
             },
             {
                 "function": "depositATokens, depositATokensWithSig, mintWithATokens, mintWithATokensWithSig, _handleDeposit, _handleMint",
@@ -7168,7 +7168,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#80, merged in commit 34ad6e3.",
                 "property": "Depositing aTokens should always be allowed regardless of Aave supply caps because it does not increase net supply to the pool.",
-                "property_specification": "Pre-condition: Aave pool has a supply cap and the remaining cap is less than the underlying value of the aTokens being deposited. Operation: depositATokens(assets). Expected post-condition: The deposit succeeds and the user receives vault shares. Actual vulnerability: The function reverts due to the supply cap check, preventing legitimate aToken deposits."
+                "property_specification": "precondition: Aave pool has a supply cap and the remaining cap is less than the underlying value of the aTokens being deposited. operation: depositATokens(assets). postcondition: The deposit succeeds and the user receives vault shares. actual vulnerability: The function reverts due to the supply cap check, preventing legitimate aToken deposits."
             },
             {
                 "function": "withdraw, withdrawATokens, withdrawWithSig, withdrawATokensWithSig, redeem, redeemAsATokens, redeemWithSig, redeemWithATokensWithSig, setFee, withdrawFees, getClaimableFees, _accrueYield, _baseDeposit, _baseWithdraw, _handleDeposit, _handleMint, _handleWithdraw, _handleRedeem",
@@ -7178,7 +7178,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#86 merged in commit 385b397.",
                 "property": "At any time, the vault's lastVaultBalance should be exactly equal to ATOKEN.balanceOf(vault) to ensure accurate fee calculation.",
-                "property_specification": "Pre-condition: lastVaultBalance = ATOKEN.balanceOf(vault). Operation: deposit(assets) or withdraw(assets) where assets is not a multiple of the liquidity index. Expected post-condition: lastVaultBalance' = ATOKEN.balanceOf(vault)'. Actual vulnerability: lastVaultBalance changes by exactly assets, but ATOKEN.balanceOf changes by a rounded amount (assets ± rounding error), causing a persistent mismatch that accumulates over time, leading to fee miscalculation."
+                "property_specification": "precondition: lastVaultBalance = ATOKEN.balanceOf(vault). operation: deposit(assets) or withdraw(assets) where assets is not a multiple of the liquidity index. postcondition: lastVaultBalance' = ATOKEN.balanceOf(vault)'. actual vulnerability: lastVaultBalance changes by exactly assets, but ATOKEN.balanceOf changes by a rounded amount (assets ± rounding error), causing a persistent mismatch that accumulates over time, leading to fee miscalculation."
             },
             {
                 "function": "initialize",
@@ -7188,7 +7188,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#71, merged in commit 3927afd.",
                 "property": "The contract owner must be a non-zero address to ensure administrative functions are accessible.",
-                "property_specification": "Pre-condition: None. Operation: initialize(owner = address(0), ...). Expected post-condition: The contract owner is a non-zero address that can execute onlyOwner functions. Actual vulnerability: The owner becomes address(0), and all onlyOwner functions become permanently locked, violating the invariant that administrative functions must be callable by a valid owner."
+                "property_specification": "precondition: None. operation: initialize(owner = address(0), ...). postcondition: The contract owner is a non-zero address that can execute onlyOwner functions. actual vulnerability: The owner becomes address(0), and all onlyOwner functions become permanently locked, violating the invariant that administrative functions must be callable by a valid owner."
             },
             {
                 "function": "withdrawFees",
@@ -7198,7 +7198,7 @@
                 "status": "Fixed",
                 "mitigation": "Fixed in PR#82 merged in commit 385b397.",
                 "property": "All yield generated by the vault, including gifts, should be subject to fee accrual before fees are withdrawn.",
-                "property_specification": "Pre-condition: lastUpdated = current block after a user transaction. A gift of aTokens is sent to the vault in the same block. Operation: withdrawFees() called after the gift. Expected post-condition: The gift amount is included in newYield and fees are charged accordingly. Actual vulnerability: getClaimableFees() returns accumulatedFees from before the gift because block.timestamp == lastUpdated, so no new fees are calculated, allowing the gift to bypass fee charges."
+                "property_specification": "precondition: lastUpdated = current block after a user transaction. A gift of aTokens is sent to the vault in the same block. operation: withdrawFees() called after the gift. postcondition: The gift amount is included in newYield and fees are charged accordingly. actual vulnerability: getClaimableFees() returns accumulatedFees from before the gift because block.timestamp == lastUpdated, so no new fees are calculated, allowing the gift to bypass fee charges."
             }
         ],
         "events": [