feat: halmos symbolic tests

packages/contracts-bedrock/foundry.toml

@@ -101,3 +101,8 @@ script = 'test/kontrol/proofs'
 src = 'test/properties/medusa/'
 test = 'test/properties/medusa/'
 script = 'test/properties/medusa/'
+
+[profile.halmos]
+src = 'test/properties/halmos/'
+test = 'test/properties/halmos/'
+script = 'test/properties/halmos/'

packages/contracts-bedrock/halmos.toml

@@ -0,0 +1,15 @@
+# Halmos configuration file
+
+## The version needed is `halmos 0.1.15.dev2+gc3f45dd`
+## Just running `halmos` will run the tests with the default configuration
+
+[global]
+# Contract to test
+match-contract = "SymTest_"
+
+# Path to the Forge artifacts directory
+forge_build_out = "./forge-artifacts"
+
+
+# Storage layout
+storage_layout = "generic"

packages/contracts-bedrock/justfile

@@ -25,6 +25,13 @@ test-kontrol:
 test-medusa:
   FOUNDRY_PROFILE=medusa medusa fuzz
 
+
+test-halmos-all VERBOSE="-v":
+  FOUNDRY_PROFILE=halmos halmos {{VERBOSE}}
+
+test-halmos TEST VERBOSE="-v":
+  FOUNDRY_PROFILE=halmos halmos --function {{TEST}} {{VERBOSE}}
+
 test-rerun: build-go-ffi
   forge test --rerun -vvv
 

packages/contracts-bedrock/medusa.json

@@ -3,11 +3,13 @@
 		"workers": 10,
 		"workerResetLimit": 50,
 		"timeout": 0,
-		"testLimit": 500000,
+		"testLimit": 0,
+		"shrinkLimit": 5000,
 		"callSequenceLength": 100,
-		"corpusDirectory": "test/properties/medusa/corpus/",
+		"corpusDirectory": "",
 		"coverageEnabled": true,
-		"targetContracts": ["ProtocolAtomicFuzz"],
+		"targetContracts": [],
+		"predeployedContracts": {},
 		"targetContractsBalances": [],
 		"constructorArgs": {},
 		"deployerAddress": "0x30000",
@@ -18,14 +20,14 @@
 		],
 		"blockNumberDelayMax": 60480,
 		"blockTimestampDelayMax": 604800,
-		"blockGasLimit": 30000000,
+		"blockGasLimit": 125000000,
 		"transactionGasLimit": 12500000,
 		"testing": {
 			"stopOnFailedTest": true,
 			"stopOnFailedContractMatching": false,
 			"stopOnNoTests": true,
 			"testAllContracts": false,
-			"traceAll": true,
+			"traceAll": false,
 			"assertionTesting": {
 				"enabled": true,
 				"testViewMethods": false,
@@ -43,13 +45,13 @@
 				}
 			},
 			"propertyTesting": {
-				"enabled": false,
+				"enabled": true,
 				"testPrefixes": [
 					"property_"
 				]
 			},
 			"optimizationTesting": {
-				"enabled": false,
+				"enabled": true,
 				"testPrefixes": [
 					"optimize_"
 				]
@@ -71,12 +73,12 @@
 			"target": ".",
 			"solcVersion": "",
 			"exportDirectory": "",
-			"args": ["--foundry-out-directory", "artifacts","--foundry-compile-all"]
+			"args": []
 		}
 	},
 	"logging": {
 		"level": "info",
 		"logDirectory": "",
 		"noColor": false
 	}
-}
+}

packages/contracts-bedrock/test/invariants/PROPERTIES.md

@@ -0,0 +1,73 @@
+# supertoken properties
+
+legend:
+
+- `[ ]`: property not yet tested
+- `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it
+- `[X]`: tested/proven property
+- `[~]`: partially tested/proven property
+- `:(`: property won't be tested due to some limitation
+
+## Unit test
+
+| id  | description                                                                        | halmos | medusa |
+| --- | ---------------------------------------------------------------------------------- | ------ | ------ |
+| 0   | supertoken token address does not depend on the executing chain’s chainID          | [ ]    | [ ]    |
+| 1   | supertoken token address depends on name, remote token, address and decimals       | [ ]    | [ ]    |
+| 2   | convert() should only allow converting legacy tokens to supertoken and viceversa   | [ ]    | [ ]    |
+| 3   | convert() only allows migrations between tokens representing the same remote asset | [ ]    | [ ]    |
+| 4   | convert() only allows migrations from tokens with the same decimals                | [ ]    | [ ]    |
+| 5   | convert() burns the same amount of one token that it mints of the other            | [ ]    | [ ]    |
+
+## Valid state
+
+| id  | description                                                                                | halmos  | medusa |
+| --- | ------------------------------------------------------------------------------------------ | ------- | ------ |
+| 6   | calls to sendERC20 succeed as long as caller has enough balance                            | [x]     | [ ]    |
+| 7   | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ]    |
+
+## Variable transition
+
+| id  | description                                                                                       | halmos | medusa |
+| --- | ------------------------------------------------------------------------------------------------- | ------ | ------ |
+| 8   | sendERC20 with a value of zero does not modify accounting                                         | [x]    | [ ]    |
+| 9   | relayERC20 with a value of zero does not modify accounting                                        | [x]    | [ ]    |
+| 10  | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount       | [x]    | [ ]    |
+| 11  | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x]    | [ ]    |
+| 12  | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge             | [x]    | [ ]    |
+| 13  | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge             | [x]    | [ ]    |
+| 14  | supertoken total supply starts at zero                                                            | [x]    | [ ]    |
+| 15  | deploying a supertoken registers its remote token in the factory                                  | [ ]    | [ ]    |
+| 16  | deploying an OptimismMintableERC20 registers its remote token in the factory                      | [ ]    | [ ]    |
+
+## High level
+
+| id  | description                                                                                                                                                           | halmos | medusa |
+| --- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ |
+| 17  | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains                                                                           | [ ]    | [ ]    |
+| 18  | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains                                                                           | [ ]    | [ ]    |
+| 19  | sum of total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy)                                                                  | [ ]    | [ ]    |
+| 20  | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ]    | [ ]    |
+| 21  | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed                   | [ ]    | [ ]    |
+
+## Atomic bridging pseudo-properties
+
+As another layer of defense, the following properties are defined which assume bridging operations to be atomic (that is, the sequencer and L2Inbox and CrossDomainMessenger contracts are fully abstracted away, `sendERC20` triggering the `relayERC20` call on the same transaction)
+It’s worth noting that these properties will not hold for a live system
+
+| id  | description                                                                                                                        | halmos | medusa |
+| --- | ---------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ |
+| 22  | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ]    | [x]    |
+| 23  | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount                 | [ ]    | [x]    |
+| 24  | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy)                 | [ ]    | [~]    |
+
+# Expected external interactions
+
+- regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
+
+# Invariant-breaking candidates (brain dump)
+
+here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants
+
+- [ ] changing the decimals of tokens after deployment
+- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols