Skip to content

Commit

Permalink
🚧 pausing point on invariants redesign
Browse files Browse the repository at this point in the history
  • Loading branch information
@neodaoist
neodaoist committed Nov 30, 2023
1 parent a151cef commit 03b627b
Show file tree
Hide file tree
Showing 3 changed files with 240 additions and 56 deletions.
194 changes: 193 additions & 1 deletion test/invariant/ClarityMarkets.invariant.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ contract ClarityMarketsInvariantTest is Test {
selectors[0] = OptionsHandler.writeNewCall.selector;
selectors[1] = OptionsHandler.writeNewPut.selector;
selectors[2] = OptionsHandler.writeExisting.selector;
// TODO batchWrite
// Transfer
selectors[3] = OptionsHandler.transferLongs.selector;
selectors[4] = OptionsHandler.transferShorts.selector;
Expand All @@ -47,6 +48,8 @@ contract ClarityMarketsInvariantTest is Test {
selectors[6] = OptionsHandler.exerciseOption.selector;
// Redeem
selectors[7] = OptionsHandler.redeemCollateral.selector;
// Skim
// TODO skim

targetSelector(FuzzSelector({addr: address(handler), selectors: selectors}));
targetContract(address(handler));
Expand Down Expand Up @@ -74,7 +77,196 @@ contract ClarityMarketsInvariantTest is Test {
}
}

///////// Debugging
///////// User Balance Invariants

function invariant_B1_totalSupplyForTokenIdEqSumOfAllBalances() public {
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);
uint256 shortTokenId = optionTokenId.longToShort();
uint256 assignedShortTokenId = optionTokenId.longToAssignedShort();

// long token type
IOption.Option memory option = clarity.option(optionTokenId);
if (block.timestamp <= option.expiry) {
assertEq(
clarity.totalSupply(optionTokenId),
handler.ghost_longSumFor(optionTokenId),
"sumOfAllBalancesForTokenIdEqTotalSupply long, before expiry"
);
} else {
assertEq(
clarity.totalSupply(optionTokenId),
0,
"sumOfAllBalancesForTokenIdEqTotalSupply long, after expiry"
);
}

// short token type
assertApproxEqAbs(
clarity.totalSupply(shortTokenId),
handler.ghost_shortSumFor(optionTokenId),
1,
"sumOfAllBalancesForTokenIdEqTotalSupply short"
);

// assigned short token type
assertEq(
clarity.totalSupply(assignedShortTokenId),
handler.ghost_assignedShortSumFor(optionTokenId),
"sumOfAllBalancesForTokenIdEqTotalSupply assignedShort"
);
}
}

///////// Options Supply and State Invariants

// TODO replace ghost state checks with option state checks

function invariant_C1_totalSupplyOfLongsEqTotalSupplyOfShorts() public {
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);
uint256 shortTokenId = optionTokenId.longToShort();

IOption.Option memory option = clarity.option(optionTokenId);
if (block.timestamp <= option.expiry) {
assertEq(
clarity.totalSupply(optionTokenId),
clarity.totalSupply(shortTokenId),
"totalSupplyOfLongsEqTotalSupplyOfShorts, before expiry"
);
} else {
assertEq(
clarity.totalSupply(optionTokenId),
0,
"totalSupplyOfLongsEqTotalSupplyOfShorts, after expiry"
);
}
}
}

function invariant_C2_totalSupplyOfShortsEqWSubNSubXSubRMulProportionUnassigned()
public
{
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);
uint256 shortTokenId = optionTokenId.longToShort();

uint256 writtenSubNetted = handler.ghost_amountWrittenFor(optionTokenId)
- handler.ghost_amountNettedFor(optionTokenId);

assertEq(
clarity.totalSupply(shortTokenId),
writtenSubNetted - handler.ghost_amountExercisedFor(optionTokenId)
- (
(
handler.ghost_amountRedeemedFor(optionTokenId)
* (
writtenSubNetted
- handler.ghost_amountExercisedFor(optionTokenId)
)
) / writtenSubNetted
),
"totalSupplyOfShortsEqWSubNSubXSubRMulProportionUnassigned"
);
}
}

function invariant_C3_totalSupplyOfAssignedShortsEqXSubRMulProportionAssigned()
public
{
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);
uint256 assignedShortTokenId = optionTokenId.longToAssignedShort();

uint256 writtenSubNetted = handler.ghost_amountWrittenFor(optionTokenId)
- handler.ghost_amountNettedFor(optionTokenId);

assertEq(
clarity.totalSupply(assignedShortTokenId),
handler.ghost_amountExercisedFor(optionTokenId)
- (
(
handler.ghost_amountRedeemedFor(optionTokenId)
* handler.ghost_amountExercisedFor(optionTokenId)
) / writtenSubNetted
),
"totalSupplyOfAssignedShortsEqXSubRMulProportionAssigned"
);
}
}

function invariant_C4_amountWrittenGteNAddXAddR() public {
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);

assertGe(
handler.ghost_amountWrittenFor(optionTokenId),
handler.ghost_amountNettedFor(optionTokenId)
+ handler.ghost_amountExercisedFor(optionTokenId)
+ handler.ghost_amountRedeemedFor(optionTokenId),
"amountWrittenGteNAddXAddR"
);
}
}

function invariant_C5_amountNettedLteW() public {
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);

assertLe(
handler.ghost_amountNettedFor(optionTokenId),
handler.ghost_amountWrittenFor(optionTokenId),
"amountNettedLteW"
);
}
}

function invariant_C6_amountExercisedLteWSubN() public {
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);

assertLe(
handler.ghost_amountExercisedFor(optionTokenId),
handler.ghost_amountWrittenFor(optionTokenId)
- handler.ghost_amountNettedFor(optionTokenId),
"amountExercisedLteWSubN"
);
}
}

function invariant_C7_amountRedeemedLteWSubN() public {
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);

assertLe(
handler.ghost_amountRedeemedFor(optionTokenId),
handler.ghost_amountWrittenFor(optionTokenId)
- handler.ghost_amountNettedFor(optionTokenId),
"amountRedeemedLteWSubN"
);
}
}

function invariant_C8_amountWrittenSubNSubREqTotalSupplyOfShortsAddAssignedShorts()
public
{
for (uint256 i = 0; i < handler.optionsCount(); i++) {
uint256 optionTokenId = handler.optionTokenIdAt(i);
uint256 shortTokenId = optionTokenId.longToShort();
uint256 assignedShortTokenId = optionTokenId.longToAssignedShort();

assertEq(
handler.ghost_amountWrittenFor(optionTokenId)
- handler.ghost_amountNettedFor(optionTokenId)
- handler.ghost_amountRedeemedFor(optionTokenId),
clarity.totalSupply(shortTokenId)
+ clarity.totalSupply(assignedShortTokenId),
"amountWrittenSubNSubREqTotalSupplyOfShortsAddAssignedShorts"
);
}
}

///////// Logs

function invariant_util_callSummary() public view {
handler.callSummary();
Expand Down
17 changes: 10 additions & 7 deletions test/specification/Clarity.invariant
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,12 @@

## Core Protocol Invariant
For all ERC20 assets in the domain:
- Invariant: A1 - Clearinghouse asset balance is greater than or equal to total clearing liabilities for that asset
- Invariant: A1 - Clearinghouse asset balance is greater than or equal to total clearing liabilities
for that asset

## User Balance Invariants
## Token Invariants
For all token ids in the domain:
- Invariant: B1 - Sum of all balances is equal to total supply of that token id
- Invariant: B1 - Total supply is equal to sum of all balances for that token id

## Options Supply and State Invariants
For all options in the domain:
Expand All @@ -16,10 +17,12 @@ For all options in the domain:
the product of redeemed and proportion options unassigned
- Invariant: C3 - Total supply of assigned shorts is equal to amount exercised minus the product of
redeemed and proportion of options assigned
- Invariant: C4 - Amount netted is less than or equal to amount written
- Invariant: C5 - Amount exercised is less than or equal to amount written minus amount netted
- Invariant: C6 - Amount redeemed is less than or equal to amount written minus amount netted
- Invariant: C7 - Amount written minus netted minus redeemed is equal to total supply of unassigned
- Invariant: C4 - Amount written is greater than or equal to amount netted plus amount exercised plus
amount redeemed
- Invariant: C5 - Amount netted is less than or equal to amount written
- Invariant: C6 - Amount exercised is less than or equal to amount written minus amount netted
- Invariant: C7 - Amount redeemed is less than or equal to amount written minus amount netted
- Invariant: C8 - Amount written minus netted minus redeemed is equal to total supply of unassigned
shorts plus total supply of assigned shorts

## Futures Supply and State Invariants
Expand Down
Loading

0 comments on commit 03b627b

Please sign in to comment.