⚡️ Optimise erc1155 NoBackdoor halmos Test

[daejunpark]

🕓 Changelog

This PR uncomments the erc721 and erc1155 NoBackdoor halmos tests and optimises the erc1155 NoBackdoor halmos test. In addition, we remove the test-parallel flag in the halmos configuration, because if both test-parallel and solver-parallel are enabled, the (peak) number of parallel solver processes could be too high, which could affect performance. The erc721 halmos tests take substantial amount of time as part of the CI. Henceforth, we run the halmos CI pipeline each day at 03:30 a.m. (= "nightly" tests) as scheduled cron job instead of integrating it into the normal push and pull_request pipeline.

🐶 Cute Animal Picture

[daejunpark]

performance profile on MacBook M1 Pro with 16GB RAM:

ERC1155TestHalmos:

$ halmos --config test/halmos.toml --contract ERC1155TestHalmos

Running 2 tests for test/tokens/halmos/ERC1155TestHalmos.t.sol:ERC1155TestHalmos
[vm.ffi] ['python', 'lib/utils/compile.py', 'src/snekmate/tokens/mocks/erc1155_mock.vy', '--evm-version', 'shanghai', '--optimize', 'none']
setup: 59.15s (decode: 0.09s, run: 59.06s)

Executing testHalmosAssertNoBackdoor
# of potential paths involving assertion violations: 38 / 71  (--solver-threads 10)
[PASS] testHalmosAssertNoBackdoor(bytes4,address,address) (paths: 71, time: 39.39s (paths: 31.35s, models: 8.04s), bounds: [])

Executing testHalmosSafeTransferFrom
# of potential paths involving assertion violations: 14 / 59  (--solver-threads 10)
[PASS] testHalmosSafeTransferFrom(address,address,address,address) (paths: 59, time: 13.81s (paths: 13.81s, models: 0.00s), bounds: [])

Symbolic test result: 2 passed; 0 failed; time: 112.57s
[time] total: 114.19s (build: 0.86s, load: 0.76s, tests: 112.57s)

ERC721TestHalmos:

$ halmos --config test/halmos.toml --contract ERC721TestHalmos

Running 2 tests for test/tokens/halmos/ERC721TestHalmos.t.sol:ERC721TestHalmos
[vm.ffi] ['python', 'lib/utils/compile.py', 'src/snekmate/tokens/mocks/erc721_mock.vy', '--evm-version', 'shanghai', '--optimize', 'none']
setup: 7.98s (decode: 0.08s, run: 7.90s)

Executing testHalmosAssertNoBackdoor
# of potential paths involving assertion violations: 128 / 234  (--solver-threads 10)
[PASS] testHalmosAssertNoBackdoor(bytes4,address,address) (paths: 234, time: 499.42s (paths: 242.00s, models: 257.42s), bounds: [])

Executing testHalmosSafeTransferFrom
# of potential paths involving assertion violations: 22 / 248  (--solver-threads 10)
[PASS] testHalmosSafeTransferFrom(address,address,address,address,uint256,uint256) (paths: 248, time: 97.95s (paths: 97.95s, models: 0.00s), bounds: [])

Symbolic test result: 2 passed; 0 failed; time: 606.01s
[time] total: 607.46s (build: 0.68s, load: 0.76s, tests: 606.01s)

[pcaversaccio]

Thx a lot for this @daejunpark! I did a small clean-up here: e597e1c and moved the halmos CI to a cron job since erc721 is taking way to long to be integrated into the normal PR pipeline. Any ideas on how to optimise erc721 further?