diff --git a/test/invariant/ClarityMarkets.invariant.t.sol b/test/invariant/ClarityMarkets.invariant.t.sol index 8a7b049..48bcc97 100644 --- a/test/invariant/ClarityMarkets.invariant.t.sol +++ b/test/invariant/ClarityMarkets.invariant.t.sol @@ -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; @@ -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)); @@ -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(); diff --git a/test/specification/Clarity.invariant b/test/specification/Clarity.invariant index 98d887d..996d0ca 100644 --- a/test/specification/Clarity.invariant +++ b/test/specification/Clarity.invariant @@ -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: @@ -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 diff --git a/test/util/OptionsHandler.sol b/test/util/OptionsHandler.sol index 522f0a8..0a95663 100644 --- a/test/util/OptionsHandler.sol +++ b/test/util/OptionsHandler.sol @@ -102,10 +102,15 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { _; } - modifier requireOpenInterest() { - vm.assume(calls["writeNewCall"] > 0 || calls["writeNewPut"] > 0); - - _; + // Helpers + + function _requireOpenInterest(uint256 optionTokenId) private view { + vm.assume(ghost_amountWrittenFor[optionTokenId] > 0); + vm.assume( + ghost_amountWrittenFor[optionTokenId] + > ghost_amountExercisedFor[optionTokenId] + + ghost_amountNettedFor[optionTokenId] + ); } // Contructor @@ -293,7 +298,6 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { external createActor countCall("writeExisting") - requireOpenInterest { // set option token id uint256 optionTokenId = _options.at(optionIndex % _options.count()); @@ -308,6 +312,9 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { // get option info IOption.Option memory option = clarity.option(optionTokenId); + // check for open interest + _requireOpenInterest(optionTokenId); + // set call vs. put specifics IERC20 writeAsset; uint256 writeAssetAmount; @@ -350,7 +357,6 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { external createActor countCall("transferLongs") - requireOpenInterest { // set option token id uint256 optionTokenId = _options.at(optionIndex % _options.count()); @@ -362,6 +368,9 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { // bind option amount optionAmount = bound(optionAmount, 1, clarity.balanceOf(sender, optionTokenId)); + // check for open interest + _requireOpenInterest(optionTokenId); + // transfer options to current actor vm.prank(sender); clarity.transfer(currentActor, optionTokenId, optionAmount); @@ -378,7 +387,6 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { external createActor countCall("transferShorts") - requireOpenInterest { // set option token id uint256 optionTokenId = _options.at(optionIndex % _options.count()); @@ -394,6 +402,9 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { // bind option amount optionAmount = bound(optionAmount, 1, clarity.balanceOf(sender, shortTokenId)); + // check for open interest + _requireOpenInterest(optionTokenId); + // transfer options to current actor vm.prank(sender); clarity.transfer(currentActor, shortTokenId, optionAmount); @@ -436,6 +447,9 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { ? clarity.option(optionTokenId).baseAsset : clarity.option(optionTokenId).quoteAsset; + // check for open interest + _requireOpenInterest(optionTokenId); + // net off position vm.prank(writer); uint256 writeAssetReturned = @@ -475,7 +489,6 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { function exerciseOption(uint256 optionIndex, uint256 ownerIndex, uint256 optionAmount) external countCall("exerciseOption") - requireOpenInterest { // set option token id uint256 optionTokenId = _options.at(optionIndex % _options.count()); @@ -490,6 +503,9 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { // get option info IOption.Option memory option = clarity.option(optionTokenId); + // check for open interest + _requireOpenInterest(optionTokenId); + // warp into exercise window, if necessary if ( block.timestamp > option.expiry @@ -565,7 +581,6 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { function redeemCollateral(uint256 optionIndex, uint256 ownerIndex) external countCall("redeemCollateral") - requireOpenInterest { // set option token id uint256 optionTokenId = _options.at(optionIndex % _options.count()); @@ -575,7 +590,7 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { ownerIndex = ownerIndex % ghost_shortOwnersOf[optionTokenId].length; address writer = ghost_shortOwnersOf[optionTokenId][ownerIndex]; - // track balances + // track balances, before redeem uint256 shortBalance = clarity.balanceOf(writer, shortTokenId); uint256 assignedBalance = clarity.balanceOf(writer, optionTokenId.longToAssignedShort()); @@ -591,7 +606,6 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { // set call vs. put specifics IERC20 writeAsset; IERC20 exerciseAsset; - if (option.optionType == IOption.OptionType.CALL) { writeAsset = IERC20(option.baseAsset); exerciseAsset = IERC20(option.quoteAsset); @@ -611,8 +625,9 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { ghost_clearingLiabilityFor[address(exerciseAsset)] -= exerciseAssetRedeemed; ghost_shortSumFor[optionTokenId] -= shortBalance; + ghost_assignedShortSumFor[optionTokenId] -= assignedBalance; - // TODO track ghost_amountRedeemedFor + ghost_amountRedeemedFor[optionTokenId] += (shortBalance + assignedBalance); // if a writer has no more shorts, swap and pop from short owners array if (clarity.balanceOf(writer, shortTokenId) == 0) { @@ -623,6 +638,14 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { } } + function sendExtra() external { + // TODO + } + + function skim() external { + // TODO + } + // Util function callSummary() external view { @@ -642,35 +665,12 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { console2.log("exerciseOption", calls["exerciseOption"]); // Redeem console2.log("redeemCollateral", calls["redeemCollateral"]); + // Skim + console2.log("skim", calls["skim"]); } - ///////// Actors - - // TODO WIP - - // function actorsCount() external view returns (uint256) { - // return _actors.actors.length; - // } - - // function actors() external view returns (address[] memory) { - // return _actors.actors; - // } - - // function forEachActor(function(address) external func) public { - // _actors.forEach(func); - // } - - // function reduceActors( - // uint256 acc, - // function(uint256,address) external returns (uint256) func - // ) public returns (uint256) { - // return _actors.reduce(acc, func); - // } - // ///////// Assets - // TODO WIP - function baseAssetsCount() external view returns (uint256) { return baseAssets.assets.length; } @@ -687,17 +687,6 @@ contract OptionsHandler is CommonBase, StdCheats, StdUtils { return quoteAssets.at(index); } - // function forEachAsset(function(IERC20) external func) public { - // _assets.forEach(func); - // } - - // function reduceAssets( - // uint256 acc, - // function(uint256,IERC20) external returns (uint256) func - // ) public returns (uint256) { - // return _assets.reduce(acc, func); - // } - ///////// Options // TODO WIP