Invariant structure

.gas-snapshot

@@ -1,14 +1,15 @@
-ModulusFuzz:test_mod_resultIsAlwaysLessThanModDivisor(uint256,uint256) (runs: 256, μ: 38396, ~: 40651)
-GAS_ModulusGas_ModAdmin:test_setModDivisor() (gas: 13812)
+ModulusFuzz:test_mod_resultIsAlwaysLessThanModDivisor(uint256,uint256) (runs: 256, μ: 38497, ~: 40674)
+GAS_ModulusGas_ModAdmin:test_setModDivisor() (gas: 13835)
 GAS_ModulusGas_Owner:test_setModAdmin() (gas: 14155)
 GAS_ModulusGas_Stranger:test_getModDivisor() (gas: 7514)
 GAS_ModulusGas_Stranger:test_getOwner() (gas: 7577)
 GAS_ModulusGas_Stranger:test_getResult() (gas: 7546)
 GAS_ModulusGas_Stranger:test_mod() (gas: 12544)
+ModulusInvariants:invariant_gettersNeverRevert() (runs: 512, calls: 262144, reverts: 0)
 ModulusUnit:test_constructor() (gas: 10608)
-ModulusUnit:test_mod() (gas: 30677)
-ModulusUnit:test_mod_revertsIfModDivisorIsZero() (gas: 13544)
+ModulusUnit:test_mod() (gas: 30655)
 ModulusUnit:test_setModAdmin() (gas: 15159)
-ModulusUnit:test_setModAdmin_onlyOwner_reverts() (gas: 11908)
-ModulusUnit:test_setModDivisor() (gas: 17945)
+ModulusUnit:test_setModAdmin_onlyOwner_reverts() (gas: 11986)
+ModulusUnit:test_setModDivisor() (gas: 17968)
 ModulusUnit:test_setModDivisor_onlyModAdmin_reverts() (gas: 11895)
+ModulusUnit:test_setModDivisor_zeroValue_reverts() (gas: 11166)

foundry.toml

@@ -3,4 +3,14 @@ src = 'src'
 out = 'out'
 libs = ['lib']
 
+[fuzz]
+runs = 256
+max_test_rejects = 120000
+seed = '0xB00B1E5'
+
+[invariant]
+runs = 512
+depth = 512
+fail_on_revert = true
+
 # See more config options https://github.com/foundry-rs/foundry/tree/master/config

src/Modulus.sol

@@ -8,6 +8,7 @@ contract Modulus {
 
     error OnlyOwner(address expected, address actual);
     error OnlyModAdmin(address expected, address actual);
+    error ModDivisorCannotBeZero();
 
     /// @notice Owner of the contract - Can set the modAdmin
     address private s_owner;
@@ -21,6 +22,7 @@ contract Modulus {
     constructor(address modAdmin) {
         s_owner = msg.sender;
         s_modAdmin = modAdmin;
+        s_modDivisor = 1;
     }
 
     function setModAdmin(address modAdmin) external onlyOwner() {
@@ -30,6 +32,7 @@ contract Modulus {
     }
 
     function setModDivisor(uint256 modDivisor) external onlyModAdmin() {
+        if (modDivisor == 0) revert ModDivisorCannotBeZero();
         uint256 previous = s_modDivisor;
         s_modDivisor = modDivisor;
         emit ModDivisorSet(previous, modDivisor);

test/Invariant/Actors/ActorModAdmin.t.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.16;
+
+import {Test} from "forge-std/Test.sol";
+import {Modulus} from "../../../src/Modulus.sol";
+
+contract ActorModAdmin is Test {
+    Modulus internal s_modulus;
+
+    function storeModulus(Modulus modulus) external {
+        s_modulus = modulus;
+    }
+
+    function setModDivisor(uint256 modDivisor) external {
+        if (modDivisor == 0) modDivisor = 1;
+        s_modulus.setModDivisor(modDivisor);
+    }
+}

test/Invariant/Actors/ActorStranger.t.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.16;
+
+import {Test} from "forge-std/Test.sol";
+import {Modulus} from "../../../src/Modulus.sol";
+
+contract ActorStranger is Test {
+    Modulus internal s_modulus;
+
+    function storeModulus(Modulus modulus) external {
+        s_modulus = modulus;
+    }
+
+    function mod(uint256 numerator) external {
+        s_modulus.mod(numerator);
+    }
+}

test/Invariant/InvariantsBase.t.sol

@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.16;
+
+import {Test} from "forge-std/Test.sol";
+
+contract InvariantsBase is Test {
+
+    struct FuzzSelector {
+        address addr;
+        bytes4[] selectors;
+    }
+
+    address[] private s_excludeContracts;
+    address[] private s_targetContracts;
+    FuzzSelector[] private s_targetSelectors;
+    address[] private s_targetSenders;
+
+    constructor() {
+        // https://github.com/foundry-rs/foundry/issues/2963
+        s_targetSenders.push(address(1));
+    }
+
+    function excludeContracts() public view returns (address[] memory) {
+        return s_excludeContracts;
+    }
+
+    function targetContracts() public view returns (address[] memory) {
+        return s_targetContracts;
+    }
+
+    function targetSelectors() public view returns (FuzzSelector[] memory) {
+        return s_targetSelectors;
+    }
+
+    function targetSenders() public view returns (address[] memory) {
+        return s_targetSenders;
+    }
+
+    // To avoid calling auxiliary functions that are inherited but not under test
+    // such as forge-std/Test.sol functions.
+    function addSelectors(
+        address newSelectorAddress,
+        bytes4[] memory newSelectors
+    ) public {
+        s_targetSelectors.push(FuzzSelector(newSelectorAddress, newSelectors));
+    }
+
+    function addSender(address newSenderAddress) public {
+        s_targetSenders.push(newSenderAddress);
+    }
+
+    // Utility function to exclude contracts that shouldn't be called
+    function excludeContract(address excludedContractAddress) public {
+        s_excludeContracts.push(excludedContractAddress);
+    }
+}

test/Invariant/Modulus.t.sol

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.16;
+
+import {Modulus} from "../../src/Modulus.sol";
+import {Test} from "forge-std/Test.sol";
+import {Constants} from "../Constants.t.sol";
+import {InvariantsBase} from "./InvariantsBase.t.sol";
+import {ActorModAdmin} from "./Actors/ActorModAdmin.t.sol";
+import {ActorStranger} from "./Actors/ActorStranger.t.sol";
+
+contract ModulusInvariants is Test, InvariantsBase, Constants {
+    Modulus internal s_modulus;
+
+    function setUp() public virtual {
+        // Deploy actors
+        ActorModAdmin modAdmin = new ActorModAdmin();
+        ActorStranger stranger = new ActorStranger();
+
+        // Deploy Modulus contract
+        changePrank(address(OWNER));
+        s_modulus = new Modulus(address(modAdmin));
+        excludeContract(address(s_modulus));
+
+        // Store the Modulus address on each of the actors
+        modAdmin.storeModulus(s_modulus);
+        stranger.storeModulus(s_modulus);
+
+        // Add mod admin selectors to callable functions
+        bytes4[] memory modAdminSelectors = new bytes4[](1);
+        modAdminSelectors[0] = ActorModAdmin.setModDivisor.selector;
+        addSelectors(address(modAdmin), modAdminSelectors);
+
+        // Add stranger selectors to callable functions
+        bytes4[] memory strangerSelectors = new bytes4[](1);
+        strangerSelectors[0] = ActorStranger.mod.selector;
+        addSelectors(address(stranger), strangerSelectors);
+    }
+
+    function invariant_gettersNeverRevert() public {
+        s_modulus.getResult();
+        s_modulus.getModDivisor();
+        s_modulus.getModAdmin();
+        s_modulus.getOwner();
+    }
+}

test/Unit/Modulus.t.sol

@@ -50,6 +50,12 @@ contract ModulusUnit is Test, Constants {
         s_modulus.setModDivisor(123);
     }
 
+    function test_setModDivisor_zeroValue_reverts() public {
+        changePrank(MOD_ADMIN);
+        vm.expectRevert(Modulus.ModDivisorCannotBeZero.selector);
+        s_modulus.setModDivisor(0);
+    }
+
     function test_setModDivisor() public {
         changePrank(MOD_ADMIN);
         s_modulus.setModDivisor(MOD_DIVISOR_2);
@@ -67,11 +73,4 @@ contract ModulusUnit is Test, Constants {
         s_modulus.mod(numerator);
         assertEq(s_modulus.getResult(), expected);
     }
-
-    function test_mod_revertsIfModDivisorIsZero() public {
-        changePrank(MOD_ADMIN);
-        s_modulus.setModDivisor(0);
-        vm.expectRevert();
-        s_modulus.mod(50);
-    }
 }