feat: medusa tests

test/invariants/FuzzTest.t.sol

@@ -30,12 +30,19 @@ contract FuzzTest is PropertyParent {
             otherRequestResponseIdx < _ghost_activeResponses[otherRequestId].length;
             otherRequestResponseIdx++
           ) {
-            // check that it is not pointing to the same request
-            assertTrue(
+            // check that it is not pointing to the same request. If it does, check it wasn't
+            // finalized without answer
+
+            if (
               _ghost_activeResponses[currentRequestId][currentRequestResponseIdx]
-                != _ghost_activeResponses[otherRequestId][otherRequestResponseIdx],
-              'prop 13: different response id for same request'
-            );
+                == _ghost_activeResponses[otherRequestId][otherRequestResponseIdx]
+                && (
+                  (oracle.finalizedAt(currentRequestId) == 0 && oracle.finalizedResponseId(currentRequestId) != 0)
+                    || (oracle.finalizedAt(otherRequestId) == 0 && oracle.finalizedResponseId(otherRequestId) != 0)
+                )
+            ) {
+              assertTrue(false, 'prop 13: same response id for different requests');
+            }
           }
         }
       }
@@ -62,12 +69,19 @@ contract FuzzTest is PropertyParent {
             otherRequestDisputeIdx < _ghost_disputes[otherRequestId].length;
             otherRequestDisputeIdx++
           ) {
-            // check that it is not pointing to the same request
-            assertTrue(
-              _ghost_disputes[currentRequestId][currentRequestDisputeIdx]
-                != _ghost_disputes[otherRequestId][otherRequestDisputeIdx],
-              'prop 13: different dispute id for same request'
-            );
+            // check that it is not pointing to the same request. If it does, check it wasn't
+            // finalized without answer
+
+            if (
+              _ghost_activeResponses[currentRequestId][currentRequestDisputeIdx]
+                == _ghost_activeResponses[otherRequestId][otherRequestDisputeIdx]
+                && (
+                  (oracle.finalizedAt(currentRequestId) == 0 && oracle.finalizedResponseId(currentRequestId) != 0)
+                    || (oracle.finalizedAt(otherRequestId) == 0 && oracle.finalizedResponseId(otherRequestId) != 0)
+                )
+            ) {
+              assertTrue(false, 'prop 13: same response id for different requests');
+            }
           }
         }
       }

test/invariants/Reproducers.t.sol

@@ -5,32 +5,108 @@ import {FuzzTest} from './FuzzTest.t.sol';
 import {IEBORequestModule, IOracle} from './Setup.t.sol';
 
 contract Reproducers is FuzzTest {
-  function test_debug() public {
-    vm.roll(55_341);
-    vm.warp(292_791);
-    vm.prank(0x0000000000000000000000000000000000080000);
+  // forge test --match-test test_prop_singleRequestIdForSingleDisputeOrResponseId_0 -vv
+
+  function test_prop_singleRequestIdForSingleDisputeOrResponseId_0() public {
+    vm.roll(3);
+    vm.warp(107_622);
+    vm.prank(0x0000000000000000000000000000000000030000);
     this.property_requesterCanAlwaysCreateRequest(
-      0, 91_936_153_333_790_985_814_765_645_281_331_945_670_085_017_288_440_355_350_976_283_151_607_122_591_831
+      10, 37_029_423_570_101_568_114_192_451_652_059_639_489_459_691_769_081_285_614_258_977_732_585_787
+    );
+
+    vm.roll(29_920);
+    vm.warp(191_126);
+    vm.prank(0x0000000000000000000000000000000000020000);
+    this.property_proposerProposeBeforeDeadlineAndNoAnswer(
+      3_533_694_129_556_768_659_166_594_920_800_430_618_073_929_656_453_786_986_859_439_806_182_558_244, ''
     );
 
-    vm.roll(114_433);
-    vm.warp(791_132);
-    vm.prank(0x0000000000000000000000000000000000080000);
+    vm.roll(41_973);
+    vm.warp(293_378);
+    vm.prank(0x0000000000000000000000000000000000070000);
+    this.property_disputerCanAlwaysCreateDispute(
+      44_601_490_397_061_246_283_071_436_695_194_755_937_831_813,
+      24_519_928_653_539_120_916_142_750_395_984_862_678_837_009_021_121_402_119
+    );
+
+    vm.roll(72_668);
+    vm.warp(701_817);
+    vm.prank(0x0000000000000000000000000000000000090000);
     this.property_finalizeAfterDeadline(
-      13_479_973_333_575_319_897_333_507_543_509_815_336_818_572_211_270_290_147_286_325_345_251,
-      107_839_786_668_602_559_178_668_057_886_353_385_264_177_471_300_505_974_851_760_065_510_272
+      441_711_766_194_596_082_395_824_375_183_268_584_384_174_444_443_096_125_085_881_927_426_324_089,
+      55_213_970_774_324_510_299_478_046_897_908_487_977_573_366_651_192_816_587_142_984_978_084_060
+    );
+
+    vm.roll(130_241);
+    vm.warp(1_239_575);
+    vm.prank(0x0000000000000000000000000000000000060000);
+    this.property_disputerEscalateFirstDisputedResponse(
+      441_711_766_194_596_082_395_824_375_183_267_903_819_727_185_636_638_495_186_960_857_860_556_558,
+      601_007_113_947_101_039_560_436_606_908_369_912_464
+    );
+
+    vm.roll(133_321);
+    vm.warp(1_272_520);
+    vm.prank(0x0000000000000000000000000000000000030000);
+    this.handleArbitrateDispute(
+      98_079_714_617_799_838_069_981_031_751_129_814_657_974_628_780_861_328_198,
+      10_543_876_310_748_807_825_434_603_100_744_632_307_071_557,
+      7_369_614_386_207_023_510_276_552_037
+    );
+
+    vm.roll(133_321);
+    vm.warp(1_272_520);
+    vm.prank(0x0000000000000000000000000000000000030000);
+    this.property_requesterCanAlwaysCreateRequest(
+      10, 1_184_941_554_243_250_179_654_158_452_865_908_463_662_710_136_610_601_139_976_392_267_926_618_806
     );
 
-    vm.roll(164_579);
-    vm.warp(1_050_332);
-    vm.prank(0x00000000000000000000000000000000000a0000);
-    this.property_requesterCanAlwaysCreateRequest(0, 300_000_000_001_847_143);
+    vm.roll(133_469);
+    vm.warp(1_272_796);
+    vm.prank(0x0000000000000000000000000000000000060000);
+    this.prop_singleRequestIdForSingleDisputeOrResponseId();
+  }
+
+  // forge test --match-test test_property_pledgerCanPledgeFor_1 -vv
 
-    vm.roll(225_050);
-    vm.warp(1_491_370);
-    vm.prank(0x00000000000000000000000000000000000a0000);
+  function test_property_pledgerCanPledgeFor_1() public {
+    vm.roll(56_765);
+    vm.warp(310_068);
+    vm.prank(0x0000000000000000000000000000000000030000);
     this.property_requesterCanAlwaysCreateRequest(
-      0, 115_792_089_237_316_195_423_570_985_008_687_907_853_269_984_665_640_564_039_456_584_007_913_130_122_499
+      23_945_252_909_255_375_823_092_408_840_274_513_180_624_399_837_945_186, 2_086_162_298_782_925_019_460
+    );
+
+    vm.roll(86_763);
+    vm.warp(575_158);
+    vm.prank(0x0000000000000000000000000000000000030000);
+    this.property_proposerProposeBeforeDeadlineAndNoAnswer(
+      631_432_499_075_532_304_456_395_701_379_901_335_158_300_516, ''
+    );
+
+    vm.roll(108_137);
+    vm.warp(650_339);
+    vm.prank(0x0000000000000000000000000000000000030000);
+    this.property_disputerCanAlwaysCreateDispute(
+      862_718_293_348_820_473_429_987_288_449_076_456_476_499_045_871_166_767_810_196_422_572_057,
+      1_239_938_753_245_600_703_949_804_873_417_738_265_153_932
+    );
+
+    vm.roll(143_071);
+    vm.warp(748_820);
+    vm.prank(0x0000000000000000000000000000000000070000);
+    this.property_disputerEscalateFirstDisputedResponse(
+      1_645_504_557_321_206_042_785_170_517_226_798_052_215_695_477_109_921_052_145_574_832,
+      3_213_876_088_517_980_570_777_725_284_107_382_648_403_960_509_936_676_257_779_973
+    );
+
+    vm.roll(150_070);
+    vm.warp(774_026);
+    vm.prank(0x0000000000000000000000000000000000070000);
+    this.property_pledgerCanPledgeFor(
+      6_901_746_346_790_563_787_434_755_862_238_646_067_770_489_658_248_914_019_106_131_779_923_731,
+      6_129_982_162_203_152_163_068_464_937_047_330_911_145_056_599_837_097_252
     );
   }
 }

test/invariants/handlers/BaseHandler.t.sol

@@ -35,6 +35,33 @@ contract BaseHandler is Setup, Actors {
   mapping(address _pledger => mapping(bytes32 _disputeId => uint256 _pledgedAmount)) internal _ghost_pledgesFor;
   mapping(address _pledger => mapping(bytes32 _disputeId => uint256 _pledgedAmount)) internal _ghost_pledgesAgainst;
 
+  // Aggregators
+
+  function _totalPledgesFor(bytes32 _disputeId) internal view returns (uint256) {
+    return _aggregateSum(_ghost_pledgesFor, _disputeId);
+  }
+
+  function _totalPledgesAgainst(bytes32 _disputeId) internal view returns (uint256) {
+    return _aggregateSum(_ghost_pledgesAgainst, _disputeId);
+  }
+
+  function _aggregateSum(
+    mapping(address => mapping(bytes32 => uint256)) storage _data,
+    bytes32 _id
+  ) internal view returns (uint256) {
+    uint256 sum;
+    for (uint256 i; i < _ghost_actors.length; i++) {
+      sum += _data[_ghost_actors[i]][_id];
+    }
+    return sum;
+  }
+
+  function _forEach(bytes32[] storage _arr, function (bytes32) _fn) internal {
+    for (uint256 i; i < _arr.length; i++) {
+      _fn(_arr[i]);
+    }
+  }
+
   // Helper functions
   function _getRandomChain(uint256 _seed) internal view returns (string memory) {
     bytes32[] memory chainIds = eboRequestCreator.getAllowedChainIds();

test/invariants/properties/PropertyDisputer.t.sol

@@ -112,12 +112,18 @@ contract PropertyDisputer is HandlerParent {
 
     vm.prank(msg.sender);
     try bondEscalationModule.pledgeForDispute(_requestData, _disputeData) {
-      assertTrue(_ghost_escalatedDisputes[_disputeId], 'property 8a: pledging for a dispute not escalated');
+      assertTrue(
+        _totalPledgesFor(_disputeId) <= _totalPledgesAgainst(_disputeId), 'property 8a: pledging for the wrong side'
+      );
     } catch {
-      // !_ghost_escalatedDisputes or
-      // past deadline/tying buffer or
-      // already pledged this turn or
-      //
+      // add tying buffer to deadline
+
+      assertTrue(
+        !_ghost_escalatedDisputes[_disputeId]
+          || block.timestamp > oracle.disputeCreatedAt(_disputeId) + DISPUTE_DEADLINE
+          || _totalPledgesFor(_disputeId) > _totalPledgesAgainst(_disputeId),
+        'property 8a: fails on pledging for the correct side'
+      );
     }
   }