crytic / properties Goto Github PK

Ex: maybe making a lib version?

See https://twitter.com/agfviggiano/status/1732328333105418326

Which would cover everything in https://github.com/crytic/building-secure-contracts/blob/master/development-guidelines/token_integration.md#erc20-tokens, plus other edge cases we are aware of

The idea would be to have helpers to ease the integration of erc20 edge case, like

import "@crytic/properties/contracts/util/erc20/erc20.sol";

Which would include :

• All the different ERC20
• all_erc20_standard() returns ( IERC20[] memory) - returns all standards token deployed, and converted to IERC20 object (or a similar name)
• all_erc20_non_standard() returns ( IERC20[] memory) - returns all non-standard token deployed, and converted to IERC20 object (or a similar name)
• all_erc20() returns ( IERC20[] memory) - returns all tokens deployed, and converted to IERC20 object (or a similar name)

Describe the desired feature or improvement

add invariants like https://twitter.com/CertoraInc/status/1727791536933323201

Describe the desired feature or improvement

I am reviewing a smart contract that contains a very complex logic to mint NFTs with random rarities using Chainlink VRF. Just by reading the code it is hard to understand if it correctly implements the specification. It would be nice to have pre-built echidna properties to test invariants.

In my particular example, the invariants are rather commonplace to other NFT projects, which is why I believe these are generic enough to be applied to other smart contracts:

• max NFTs per wallet: no user can have more NFTs than the max
• max NFTs minted: total supply must not exceed the max
• max NFTs per project owner: the project owner cannot have more than the max
• NFT price (in Ether, but can be extended to ERC-20 too): minting an NFT must cost exactly the NFT price
• NFT rarity: the number of NFTs minted for a given rarity must match their assigned percentages, within an error margin
• whitelist: no user can mint NFTs if they are not on the whitelist
• etc

If you think this is useful I can work on these properties and submit a PR.

Describe the issue:

The PropertiesConstants contracts contain some hardcoded parameters that are related to Echidna's default setup, such as USER1, USER2, and USER3.

The issue is that it also contains INITIAL_BALANCE, which has nothing to do with balanceAddr or balanceContract. This can be confusing to users.

Maybe it is better to migrate this value to another contract and create the related BALANCE_ADDR or BALANCE_CONTRACT variables.

Steps to reproduce the issue:

N/A

If additional code is needed for reproducing, please copy it here, or drop us a link to the repository:

N/A

Echidna version:

N/A

Additional information:

N/A

We need to standardize the properties in this repo, for example:

• properties must be described with natspec
• the english description of the invariant must be present
• The mode must be described (internal /external / isolated / function override / model testing) (https://secure-contracts.com/program-analysis/echidna/basic/common-testing-approaches.html#partial-testing)

We should also agree on a structure to group the properties in the file, and how to document the sections (ex

Once we have defined the rules, we should apply them on the repo, and integrate them in the contribution guidelines

Describe the desired feature or improvement

The formatting of the codebase is inconsistent:

https://github.com/crytic/properties/blob/main/contracts/util/PropertiesHelper.sol#L184

        if ( !(a < b)) {

https://github.com/crytic/properties/blob/main/contracts/util/PropertiesHelper.sol#L197

        if(!(a <= b)) {

Describe the issue:

The state

There's a set of functions in contracts/util/PropertiesHelper.sol named clamp... for making numbers fit in a fixed range by performing modulo. For example using such function to put numbers 0-10 in the range 4-6 will result in:

in:  0 1 2 3 4 5 6 7 8 9 10
out: 6 4 5 6 4 5 6 4 5 6 4

The problem

In the programming nomenclature the term "clamp" usually refers to putting number in a fixed range by assigning it the value of the boundary, if that boundary is exceeded. For example clamping numbers 0-10 in the range 4-6 would result in:

in:  0 1 2 3 4 5 6 7 8 9 10
out: 4 4 4 4 4 5 6 6 6 6 6

I'm writing this based on my experience, I got really confused when I saw PropertyHelper's clamp... functions in use for the first time. I checked my expectations by searching on the internet for "clamp a number", and all the resources were referring to "clamping" as assigning the exceeded boundary, not calculating the modulo. I think that many developers using PropertiesHelper for the first time will be confused or misled.

The solution

I think that the clamp... functions should be renamed to something less confusing. For example the name wrap... could be good, it would reflect how numbers exceeding the limit are returning into the range on the other end.

Steps to reproduce the issue:

Write code using PropertiesHelper.

If additional code is needed for reproducing, please copy it here, or drop us a link to the repository:

No response

Echidna version:

All of them.

Additional information:

No response

Describe the desired feature or improvement

This is a bit subjective, but I find it confusing:

import {PropertiesAsserts} from "@crytic/properties/contracts/util/PropertiesHelper.sol";

I propose a refactor so that the contract name matches the contract filename:

import {PropertiesAsserts} from "@crytic/properties/contracts/util/PropertiesAsserts.sol";

Describe the desired feature or improvement

Since a lot of MultiSigs work in a relatively similar way (e.g., using signatures, some threshold of votes/signatures is required, only approved signers can execute, etc.) we could probably build a set of general properties to test MultiSigs.

For example:

• If votes < threshold, calls can't be executed
• Signatures cannot be reused
• nonce is strictly monotonously increasing
• nonce can only be used once

Similar to https://github.com/crytic/slither/blob/master/trophies.md.

Example: pods-finance/yield-contracts#141

Describe the desired feature or improvement

When integrating https://github.com/crytic/properties with an existing foundry codebase, many assertion helpers collide with forge-std/Test.sol, which makes it harder to use both helpers on the same set of contracts.

For example, this repo's assertWithMsg from this repo serves the same purpose as foundry's assertTrue, so they could have the same name. Also, one uses assertGte while the other uses assertGe, etc.

It would be nice if this repo was fully compatible with foundry for an easier integration.

Describe the issue:

These 2 tests:

contract CryticABDKMath64x64Properties {
    ...
    function add_test_range(int128 x, int128 y) public view {
        int128 result;
        try this.add(x, y) {
            result = this.add(x, y);
            assert(result <= MAX_64x64 && result >= MIN_64x64);
        } catch {
            // If it reverts, just ignore
        }
    }

    function sub_test_range(int128 x, int128 y) public view {
        int128 result;
        try this.sub(x, y) {
            result = this.sub(x, y);
            assert(result <= MAX_64x64 && result >= MIN_64x64);
        } catch {
            // If it reverts, just ignore
        }
    }
}

They are not actually showing failure in case this.add/this.sub overflow or underflow.
It looks like result being int128 makes it always conforming with the assert statement despite the failure in this.add/this.sub.

Steps to reproduce the issue:

• Create a smart contract to contain the test in ``tests/ABDKMath64x64PropertyTests/hardhat/contracts/CryticMathTest.sol`

pragma solidity ^0.8.0;
import "@crytic/properties/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol";

contract CryticABDKMath64x64Harness is CryticABDKMath64x64Properties {
    /* Any additional test can be added here */
}

• Working directory: tests/ABDKMath64x64PropertyTests/hardhat

• Force ABDKMath64x64 to overflow/underflow by commenting out the require statement on the tested methods.

library ABDKMath64x64 {
   ....
  function add (int128 x, int128 y) internal pure returns (int128) {
    unchecked {
      int256 result = int256(x) + y;
      // COMMENTED THIS TO FORCE IT TO FAIL
      //  require (result >= MIN_64x64 && result <= MAX_64x64);
      return int128 (result);
    }
  }
  function sub (int128 x, int128 y) internal pure returns (int128) {
    unchecked {
      int256 result = int256(x) - y;
      // COMMENTED THIS TO FORCE IT TO FAIL
      //  require (result >= MIN_64x64 && result <= MAX_64x64);
      return int128 (result);
    }
  }
}

• Run echidna-test . --contract CryticABDKMath64x64Harness --test-mode assertion

• Output:

sub_test_range(int128,int128):  passed! 🎉
abs(int128):  passed! 🎉
add_test_maximum_value():  passed! 🎉
mulu(int128,uint256):  passed! 🎉
add_test_range(int128,int128):  passed! 🎉

• Some other tests failed due to that change but add_test_range and sub_test_range did not fail as expected.

If additional code is needed for reproducing, please copy it here, or drop us a link to the repository:

No response

Echidna version:

Echidna 2.0.1

Additional information:

No response

Describe the desired feature or improvement

PropertiesHelper.clampBetween do not emit a LogString event with the value is clamped, which makes debugging harder. This is missing in both uint256 and int256 versions.

In the IERC721Internal interface you define the following function usedId:

function usedId(uint256 tokenId) external view returns (bool);

I'm having a hard time to understand what is the reason behind using this as part of the interface. In your ERC721Compliant contract, you declare it but not use it:

If someone adds something like usedId[id] = true to the _customMint function, the following property always fails obviously:

If you want to track the used ids, you should update it after the above test assertion to make sense.

Furthermore, the README section on the ERC721 is outdated. There is no ITokenMock in the ERC721 case for example, but IERC721Internal. I would recommend making it consistent with the ERC20 example tho & updating the docs about the latest status quo.

Describe the desired feature or improvement

We can re-use some of the work done for ABDK to support https://github.com/PaulRBerg/prb-math

Describe the desired feature or improvement

Uniswap v2 might be a good first one

Describe the desired feature or improvement

1. How challenging would it be to create a generic set of merkle trie properties?
2. Do merkle trie library interfaces have enough commonalities for this kind of test suite to be possible?

Describe the desired feature or improvement

https://github.com/d-xo/weird-erc20#tokens provides a good list of non-standard ERC20 tokens, along with nice example contracts. I think we should aim to integrate these tokens as test-cases and be able to detect a good number of these.

For example, we can use a low level call, or try/catch, and verify that it actually reverts

Describe the desired feature or improvement

ERC721 might be a good target

Describe the desired feature or improvement

As discussed here, it'd be nice to port the ABDKMath properties over to PRBMath.

https://github.com/abdk-consulting/abdk-libraries-solidity/releases/tag/v3.2