From 4641192ea7b1e0a44d445c062890e79aa92a29a9 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Wed, 15 Jan 2025 20:00:49 +0200 Subject: [PATCH] Specs --- .gitignore | 1 + certora/conf/EntryPoint.conf | 28 ++ certora/conf/EntryPoint_sanity.conf | 28 ++ certora/conf/alwaysRevert.conf | 28 ++ certora/conf/nonHandleOps.conf | 24 + certora/conf/residual.conf | 25 + certora/patch/prover_optimization.patch | 40 ++ certora/report/all.sh | 94 ++++ certora/report/all_sanity.sh | 93 ++++ .../report/certora_final_results_regular.csv | 50 ++ .../report/certora_final_results_sanity.csv | 85 ++++ certora/report/certora_results_regular.md | 56 +++ certora/report/certora_results_sanity.md | 90 ++++ certora/report/markdown.sh | 31 ++ certora/report/table_generator.py | 63 +++ certora/specs/alwaysRevert.spec | 13 + certora/specs/entryPoint.spec | 472 ++++++++++++++++++ certora/specs/entryPointSanity.spec | 437 ++++++++++++++++ certora/specs/entryPointShared.spec | 125 +++++ certora/specs/residual.spec | 49 ++ 20 files changed, 1832 insertions(+) create mode 100644 certora/conf/EntryPoint.conf create mode 100644 certora/conf/EntryPoint_sanity.conf create mode 100644 certora/conf/alwaysRevert.conf create mode 100644 certora/conf/nonHandleOps.conf create mode 100644 certora/conf/residual.conf create mode 100644 certora/patch/prover_optimization.patch create mode 100755 certora/report/all.sh create mode 100755 certora/report/all_sanity.sh create mode 100644 certora/report/certora_final_results_regular.csv create mode 100644 certora/report/certora_final_results_sanity.csv create mode 100644 certora/report/certora_results_regular.md create mode 100644 certora/report/certora_results_sanity.md create mode 100755 certora/report/markdown.sh create mode 100644 certora/report/table_generator.py create mode 100644 certora/specs/alwaysRevert.spec create mode 100644 certora/specs/entryPoint.spec create mode 100644 certora/specs/entryPointSanity.spec create mode 100644 certora/specs/entryPointShared.spec create mode 100644 certora/specs/residual.spec diff --git a/.gitignore b/.gitignore index f6a4ff528..c7e919973 100644 --- a/.gitignore +++ b/.gitignore @@ -18,3 +18,4 @@ artifacts .DS_Store /contracts/dist/ /contracts/types/ +.certora_internal diff --git a/certora/conf/EntryPoint.conf b/certora/conf/EntryPoint.conf new file mode 100644 index 000000000..cb8608c8a --- /dev/null +++ b/certora/conf/EntryPoint.conf @@ -0,0 +1,28 @@ +{ + "files": [ + "contracts/core/EntryPoint.sol" + ], + "hashing_length_bound": "96", + "loop_iter": "4", + "optimistic_fallback": true, + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin=node_modules/@openzeppelin", + "@uniswap=node_modules/@uniswap" + ], + "process": "emv", + "prover_args": [ + "-canonicalizeTAC false", + "-assumeFPStrictlyMonotonic false", + "-enableSolidityBasedInlining true", + "-adaptiveSolverConfig false", + "-destructiveOptimizations enable", + "-enableFlowSensitivePartitioning true", + "-enableABIAnalysis true", + "-optimisticBufferContents true", + "-enableAggressiveABIOptimization true" + ], + "smt_timeout": "1800", + "verify": "EntryPoint:certora/specs/entryPoint.spec", +} \ No newline at end of file diff --git a/certora/conf/EntryPoint_sanity.conf b/certora/conf/EntryPoint_sanity.conf new file mode 100644 index 000000000..2b9e18856 --- /dev/null +++ b/certora/conf/EntryPoint_sanity.conf @@ -0,0 +1,28 @@ +{ + "files": [ + "contracts/core/EntryPoint.sol" + ], + "hashing_length_bound": "96", + "loop_iter": "4", + "optimistic_fallback": true, + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin=node_modules/@openzeppelin", + "@uniswap=node_modules/@uniswap" + ], + "process": "emv", + "prover_args": [ + "-canonicalizeTAC false", + "-assumeFPStrictlyMonotonic false", + "-enableSolidityBasedInlining true", + "-adaptiveSolverConfig false", + "-destructiveOptimizations enable", + "-enableFlowSensitivePartitioning true", + "-enableABIAnalysis true", + "-optimisticBufferContents true", + "-enableAggressiveABIOptimization true" + ], + "smt_timeout": "1800", + "verify": "EntryPoint:certora/specs/entryPointSanity.spec", +} \ No newline at end of file diff --git a/certora/conf/alwaysRevert.conf b/certora/conf/alwaysRevert.conf new file mode 100644 index 000000000..41fe59d65 --- /dev/null +++ b/certora/conf/alwaysRevert.conf @@ -0,0 +1,28 @@ +{ + "files": [ + "contracts/core/EntryPoint.sol" + ], + "hashing_length_bound": "96", + "loop_iter": "3", + "optimistic_fallback": true, + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin=node_modules/@openzeppelin", + "@uniswap=node_modules/@uniswap" + ], + "process": "emv", + "prover_args": [ + "-canonicalizeTAC false", + "-assumeFPStrictlyMonotonic false", + "-enableSolidityBasedInlining true", + "-adaptiveSolverConfig false", + "-destructiveOptimizations enable", + "-enableFlowSensitivePartitioning true", + "-enableABIAnalysis true", + "-optimisticBufferContents true", + "-enableAggressiveABIOptimization true" + ], + "smt_timeout": "1800", + "verify": "EntryPoint:certora/specs/alwaysRevert.spec", +} \ No newline at end of file diff --git a/certora/conf/nonHandleOps.conf b/certora/conf/nonHandleOps.conf new file mode 100644 index 000000000..b342555f5 --- /dev/null +++ b/certora/conf/nonHandleOps.conf @@ -0,0 +1,24 @@ +{ + "files": [ + "contracts/core/EntryPoint.sol" + ], + "hashing_length_bound": "96", + "loop_iter": "3", + "optimistic_fallback": true, + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin=node_modules/@openzeppelin", + "@uniswap=node_modules/@uniswap" + ], + "process": "emv", + "prover_args": [ + "-canonicalizeTAC false", + "-assumeFPStrictlyMonotonic false", + "-enableSolidityBasedInlining true", + "-destructiveOptimizations enable" + ], + "rule_sanity": "basic", + "smt_timeout": "1800", + "verify": "EntryPoint:certora/specs/entryPoint.spec", +} \ No newline at end of file diff --git a/certora/conf/residual.conf b/certora/conf/residual.conf new file mode 100644 index 000000000..7c61bbec6 --- /dev/null +++ b/certora/conf/residual.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "contracts/core/EntryPoint.sol" + ], + "hashing_length_bound": "96", + "independent_satisfy": true, + "loop_iter": "3", + "optimistic_fallback": true, + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin=node_modules/@openzeppelin", + "@uniswap=node_modules/@uniswap" + ], + "process": "emv", + "prover_args": [ + "-canonicalizeTAC false", + "-assumeFPStrictlyMonotonic false", + "-enableSolidityBasedInlining true" + ], + "rule_sanity": "basic", + "rule": ["checkInnerHandleOp"], + "smt_timeout": "1800", + "verify": "EntryPoint:certora/specs/residual.spec", +} \ No newline at end of file diff --git a/certora/patch/prover_optimization.patch b/certora/patch/prover_optimization.patch new file mode 100644 index 000000000..b3416921a --- /dev/null +++ b/certora/patch/prover_optimization.patch @@ -0,0 +1,40 @@ +diff --git a/contracts/core/EntryPoint.sol b/contracts/core/EntryPoint.sol +index 058d8eb..8953da2 100644 +--- a/contracts/core/EntryPoint.sol ++++ b/contracts/core/EntryPoint.sol +@@ -108,7 +108,7 @@ contract EntryPoint is IEntryPoint, StakeManager, NonceManager, ReentrancyGuardT + assembly ("memory-safe") { + success := call(gas(), address(), 0, add(innerCall, 0x20), mload(innerCall), 0, 32) + collected := mload(0) +- mstore(0x40, saveFreePtr) ++ // mstore(0x40, saveFreePtr) // make analysis succeed, no-op + } + } + if (!success) { +@@ -299,7 +299,7 @@ contract EntryPoint is IEntryPoint, StakeManager, NonceManager, ReentrancyGuardT + MemoryUserOp mUserOp; + bytes32 userOpHash; + uint256 prefund; +- uint256 contextOffset; ++ bytes contextOffset; // make analysis succeed, no-op + uint256 preOpGas; + } + +@@ -780,7 +780,7 @@ contract EntryPoint is IEntryPoint, StakeManager, NonceManager, ReentrancyGuardT + */ + function getOffsetOfMemoryBytes( + bytes memory data +- ) internal pure returns (uint256 offset) { ++ ) internal pure returns (bytes memory offset /* make analysis succeed, no-op */) { + assembly { + offset := data + } +@@ -791,7 +791,7 @@ contract EntryPoint is IEntryPoint, StakeManager, NonceManager, ReentrancyGuardT + * @param offset - The offset to get the bytes from. + */ + function getMemoryBytesFromOffset( +- uint256 offset ++ bytes memory offset // make analysis succeed, no-op + ) internal pure returns (bytes memory data) { + assembly ("memory-safe") { + data := offset diff --git a/certora/report/all.sh b/certora/report/all.sh new file mode 100755 index 000000000..8677c5628 --- /dev/null +++ b/certora/report/all.sh @@ -0,0 +1,94 @@ +git apply ./certora/patch/prover_optimization.patch + +certoraRun.py certora/conf/nonHandleOps.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_NonHandleOps --rule onlyValidatedCalls_NonHandleOps --parametric_contracts EntryPoint +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleOps --rule onlyValidatedCalls_3HandleOps +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleOps --rule onlyValidatedCalls_2HandleOps +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_1HandleOps --rule onlyValidatedCalls_1HandleOps +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_0HandleOps --rule onlyValidatedCalls_0HandleOps +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps000 --rule onlyValidatedCalls_3HandleAggregatedOps000 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps001 --rule onlyValidatedCalls_3HandleAggregatedOps001 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps002 --rule onlyValidatedCalls_3HandleAggregatedOps002 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps003 --rule onlyValidatedCalls_3HandleAggregatedOps003 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps010 --rule onlyValidatedCalls_3HandleAggregatedOps010 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps011 --rule onlyValidatedCalls_3HandleAggregatedOps011 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps012 --rule onlyValidatedCalls_3HandleAggregatedOps012 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps013 --rule onlyValidatedCalls_3HandleAggregatedOps013 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps020 --rule onlyValidatedCalls_3HandleAggregatedOps020 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps021 --rule onlyValidatedCalls_3HandleAggregatedOps021 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps022 --rule onlyValidatedCalls_3HandleAggregatedOps022 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps023 --rule onlyValidatedCalls_3HandleAggregatedOps023 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps030 --rule onlyValidatedCalls_3HandleAggregatedOps030 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps031 --rule onlyValidatedCalls_3HandleAggregatedOps031 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps032 --rule onlyValidatedCalls_3HandleAggregatedOps032 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps033 --rule onlyValidatedCalls_3HandleAggregatedOps033 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps100 --rule onlyValidatedCalls_3HandleAggregatedOps100 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps101 --rule onlyValidatedCalls_3HandleAggregatedOps101 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps102 --rule onlyValidatedCalls_3HandleAggregatedOps102 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps103 --rule onlyValidatedCalls_3HandleAggregatedOps103 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps110 --rule onlyValidatedCalls_3HandleAggregatedOps110 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps111 --rule onlyValidatedCalls_3HandleAggregatedOps111 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps112 --rule onlyValidatedCalls_3HandleAggregatedOps112 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps113 --rule onlyValidatedCalls_3HandleAggregatedOps113 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps120 --rule onlyValidatedCalls_3HandleAggregatedOps120 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps121 --rule onlyValidatedCalls_3HandleAggregatedOps121 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps122 --rule onlyValidatedCalls_3HandleAggregatedOps122 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps123 --rule onlyValidatedCalls_3HandleAggregatedOps123 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps130 --rule onlyValidatedCalls_3HandleAggregatedOps130 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps131 --rule onlyValidatedCalls_3HandleAggregatedOps131 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps132 --rule onlyValidatedCalls_3HandleAggregatedOps132 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps133 --rule onlyValidatedCalls_3HandleAggregatedOps133 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps200 --rule onlyValidatedCalls_3HandleAggregatedOps200 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps201 --rule onlyValidatedCalls_3HandleAggregatedOps201 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps202 --rule onlyValidatedCalls_3HandleAggregatedOps202 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps203 --rule onlyValidatedCalls_3HandleAggregatedOps203 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps210 --rule onlyValidatedCalls_3HandleAggregatedOps210 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps211 --rule onlyValidatedCalls_3HandleAggregatedOps211 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps212 --rule onlyValidatedCalls_3HandleAggregatedOps212 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps213 --rule onlyValidatedCalls_3HandleAggregatedOps213 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps220 --rule onlyValidatedCalls_3HandleAggregatedOps220 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps221 --rule onlyValidatedCalls_3HandleAggregatedOps221 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps222 --rule onlyValidatedCalls_3HandleAggregatedOps222 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps223 --rule onlyValidatedCalls_3HandleAggregatedOps223 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps230 --rule onlyValidatedCalls_3HandleAggregatedOps230 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps231 --rule onlyValidatedCalls_3HandleAggregatedOps231 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps232 --rule onlyValidatedCalls_3HandleAggregatedOps232 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps233 --rule onlyValidatedCalls_3HandleAggregatedOps233 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps300 --rule onlyValidatedCalls_3HandleAggregatedOps300 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps301 --rule onlyValidatedCalls_3HandleAggregatedOps301 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps302 --rule onlyValidatedCalls_3HandleAggregatedOps302 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps303 --rule onlyValidatedCalls_3HandleAggregatedOps303 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps310 --rule onlyValidatedCalls_3HandleAggregatedOps310 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps311 --rule onlyValidatedCalls_3HandleAggregatedOps311 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps312 --rule onlyValidatedCalls_3HandleAggregatedOps312 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps313 --rule onlyValidatedCalls_3HandleAggregatedOps313 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps320 --rule onlyValidatedCalls_3HandleAggregatedOps320 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps321 --rule onlyValidatedCalls_3HandleAggregatedOps321 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps322 --rule onlyValidatedCalls_3HandleAggregatedOps322 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps323 --rule onlyValidatedCalls_3HandleAggregatedOps323 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps330 --rule onlyValidatedCalls_3HandleAggregatedOps330 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps331 --rule onlyValidatedCalls_3HandleAggregatedOps331 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps332 --rule onlyValidatedCalls_3HandleAggregatedOps332 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_3HandleAggregatedOps333 --rule onlyValidatedCalls_3HandleAggregatedOps333 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps00 --rule onlyValidatedCalls_2HandleAggregatedOps00 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps01 --rule onlyValidatedCalls_2HandleAggregatedOps01 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps02 --rule onlyValidatedCalls_2HandleAggregatedOps02 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps03 --rule onlyValidatedCalls_2HandleAggregatedOps03 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps10 --rule onlyValidatedCalls_2HandleAggregatedOps10 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps11 --rule onlyValidatedCalls_2HandleAggregatedOps11 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps12 --rule onlyValidatedCalls_2HandleAggregatedOps12 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps13 --rule onlyValidatedCalls_2HandleAggregatedOps13 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps20 --rule onlyValidatedCalls_2HandleAggregatedOps20 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps21 --rule onlyValidatedCalls_2HandleAggregatedOps21 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps22 --rule onlyValidatedCalls_2HandleAggregatedOps22 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps23 --rule onlyValidatedCalls_2HandleAggregatedOps23 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps30 --rule onlyValidatedCalls_2HandleAggregatedOps30 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps31 --rule onlyValidatedCalls_2HandleAggregatedOps31 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps32 --rule onlyValidatedCalls_2HandleAggregatedOps32 +# certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_2HandleAggregatedOps33 --rule onlyValidatedCalls_2HandleAggregatedOps33 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_1HandleAggregatedOps0 --rule onlyValidatedCalls_1HandleAggregatedOps0 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_1HandleAggregatedOps1 --rule onlyValidatedCalls_1HandleAggregatedOps1 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_1HandleAggregatedOps2 --rule onlyValidatedCalls_1HandleAggregatedOps2 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_1HandleAggregatedOps3 --rule onlyValidatedCalls_1HandleAggregatedOps3 +certoraRun.py certora/conf/EntryPoint.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg onlyValidatedCalls_0HandleAggregatedOps --rule onlyValidatedCalls_0HandleAggregatedOps + +git apply -R ./certora/patch/prover_optimization.patch \ No newline at end of file diff --git a/certora/report/all_sanity.sh b/certora/report/all_sanity.sh new file mode 100755 index 000000000..964d58cd5 --- /dev/null +++ b/certora/report/all_sanity.sh @@ -0,0 +1,93 @@ +git apply ./certora/patch/prover_optimization.patch + +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleOps --rule sanity_onlyValidatedCalls_3HandleOps --parametric_contracts EntryPoint +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleOps --rule sanity_onlyValidatedCalls_2HandleOps +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_1HandleOps --rule sanity_onlyValidatedCalls_1HandleOps +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_0HandleOps --rule sanity_onlyValidatedCalls_0HandleOps +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps000 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps000 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps001 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps001 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps002 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps002 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps003 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps003 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps010 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps010 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps011 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps011 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps012 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps012 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps013 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps013 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps020 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps020 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps021 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps021 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps022 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps022 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps023 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps023 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps030 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps030 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps031 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps031 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps032 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps032 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps033 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps033 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps100 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps100 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps101 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps101 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps102 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps102 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps103 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps103 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps110 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps110 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps111 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps111 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps112 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps112 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps113 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps113 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps120 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps120 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps121 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps121 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps122 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps122 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps123 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps123 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps130 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps130 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps131 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps131 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps132 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps132 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps133 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps133 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps200 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps200 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps201 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps201 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps202 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps202 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps203 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps203 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps210 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps210 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps211 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps211 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps212 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps212 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps213 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps213 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps220 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps220 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps221 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps221 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps222 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps222 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps223 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps223 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps230 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps230 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps231 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps231 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps232 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps232 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps233 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps233 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps300 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps300 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps301 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps301 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps302 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps302 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps303 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps303 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps310 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps310 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps311 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps311 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps312 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps312 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps313 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps313 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps320 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps320 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps321 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps321 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps322 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps322 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps323 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps323 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps330 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps330 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps331 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps331 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps332 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps332 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_3HandleAggregatedOps333 --rule sanity_onlyValidatedCalls_3HandleAggregatedOps333 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps00 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps00 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps01 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps01 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps02 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps02 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps03 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps03 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps10 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps10 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps11 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps11 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps12 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps12 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps13 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps13 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps20 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps20 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps21 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps21 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps22 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps22 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps23 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps23 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps30 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps30 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps31 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps31 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps32 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps32 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_2HandleAggregatedOps33 --rule sanity_onlyValidatedCalls_2HandleAggregatedOps33 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_1HandleAggregatedOps0 --rule sanity_onlyValidatedCalls_1HandleAggregatedOps0 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_1HandleAggregatedOps1 --rule sanity_onlyValidatedCalls_1HandleAggregatedOps1 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_1HandleAggregatedOps2 --rule sanity_onlyValidatedCalls_1HandleAggregatedOps2 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_1HandleAggregatedOps3 --rule sanity_onlyValidatedCalls_1HandleAggregatedOps3 +certoraRun.py certora/conf/EntryPoint_sanity.conf --build_cache --server prover --prover_version jtoman/push-cvl-assumes --msg sanity_onlyValidatedCalls_0HandleAggregatedOps --rule sanity_onlyValidatedCalls_0HandleAggregatedOps + +git apply -R ./certora/patch/prover_optimization.patch \ No newline at end of file diff --git a/certora/report/certora_final_results_regular.csv b/certora/report/certora_final_results_regular.csv new file mode 100644 index 000000000..82cc96f1f --- /dev/null +++ b/certora/report/certora_final_results_regular.csv @@ -0,0 +1,50 @@ +Main String,First Number,Last Number,Original URL,Status +HandleAggregatedOps,3,000,https://prover.certora.com/output/60724/dc61f3406e1b45afa3ec5fc480acad12?anonymousKey=57a630c1ba831ffbda48e641a294f57ffb55f776,PASSED +HandleAggregatedOps,3,001,https://prover.certora.com/output/60724/98838dafaba7443db41fc6a5d038239b?anonymousKey=15c011365c6645b5161d70fe6f6a68c55f114c09,PASSED +HandleAggregatedOps,3,002,https://prover.certora.com/output/60724/a13c20b2742442218d4033b2bbcc1575?anonymousKey=f38dcb73883882d99f492141cadd11d98169dbf1,PASSED +HandleAggregatedOps,3,003,https://prover.certora.com/output/60724/d130cea66d1c44379877cc5506e3f498?anonymousKey=3c1ae5775f8d672926055aae4529b294ce514048,PASSED +HandleAggregatedOps,3,010,https://prover.certora.com/output/60724/e6e7d20e38034acba4b579a135605789?anonymousKey=738136472db3ace0198b45eeb273e3b4ca799410,PASSED +HandleAggregatedOps,3,011,https://prover.certora.com/output/60724/8ec06ba489004e3d825f896154ae4b8e?anonymousKey=4f2a87346b42bdcb0f09123abd2ff866ce8f8635,PASSED +HandleAggregatedOps,3,012,https://prover.certora.com/output/60724/dd2b6b67e7604216b91dd635ea40a3a9?anonymousKey=a8c07557aa3ec4befd7987c824caa748a5559482,PASSED +HandleAggregatedOps,3,013,https://prover.certora.com/output/60724/70da1e37d18e4f43a10946af68f4dbe1?anonymousKey=7380044b45c11baba43a1d6f5c4635e404ec50f4,PASSED +HandleAggregatedOps,3,020,https://prover.certora.com/output/60724/fec7e4a70f2d414ab652863c886375a9?anonymousKey=f40c63a1a8c827febd1636c3bad1e48ca20db81f,PASSED +HandleAggregatedOps,3,021,https://prover.certora.com/output/60724/f24730f769c449368f9af037fe9304c0?anonymousKey=c3b67523341940aa349782e9149487403eb6bf12,PASSED +HandleAggregatedOps,3,022,https://prover.certora.com/output/60724/b0c6a515eb8e4e84aff5329bb82efbc5?anonymousKey=3c30e47af257d7aeb47e2c5a48928a457f355947,PASSED +HandleAggregatedOps,3,030,https://prover.certora.com/output/60724/bc99c47a3eaa4f25b0d3ec47b61c94ba?anonymousKey=4f422b4a21aa40c068821d8adb9be98d49b49eaf,PASSED +HandleAggregatedOps,3,031,https://prover.certora.com/output/60724/726e528e49304dc9aa6e9929316fa22a?anonymousKey=6fc96524153f72b8048e90a5c79d2db99779c4ed,PASSED +HandleAggregatedOps,3,100,https://prover.certora.com/output/60724/c32db3ef9bd347a690652da34e5c97d8?anonymousKey=6b7c6cc3ea5ba801e123a31d37a299695fac2f1a,PASSED +HandleAggregatedOps,3,101,https://prover.certora.com/output/60724/c5a85703d60c4f5eb02c3f94de12a0d1?anonymousKey=2485460100fe1b87064967443763943d57b4391b,PASSED +HandleAggregatedOps,3,102,https://prover.certora.com/output/60724/23cfbc2ec45b4da38e1dad26b624c5c5?anonymousKey=82f7d69f4362c308a2e0ab5f350fb065652c7de8,PASSED +HandleAggregatedOps,3,103,https://prover.certora.com/output/60724/9077432b3a104cb397917be33f1505c4?anonymousKey=35b96455661b58fae5e3ff8f240913a10a3597bf,PASSED +HandleAggregatedOps,3,110,https://prover.certora.com/output/60724/0a8f15cdaed8421e918ab78a7823d176?anonymousKey=74c435c3b0e58331ad6b305a8e551d3e343628e1,PASSED +HandleAggregatedOps,3,111,https://prover.certora.com/output/60724/3f63c12e3dfd4f7d8cbef39094fa578f?anonymousKey=f12ce8b6dd9a155a1d4d2f899e2138b25667df35,PASSED +HandleAggregatedOps,3,112,https://prover.certora.com/output/60724/685f3fa404f54b20ac3f28cf23ce9212?anonymousKey=1a1d209f216b26235197e02950dd26e663a81f70,PASSED +HandleAggregatedOps,3,120,https://prover.certora.com/output/60724/ec8e36615726418cb685df5de12d787b?anonymousKey=2511cccfacd5b5b0ca6fb9837cb57f3a3ac1571a,PASSED +HandleAggregatedOps,3,121,https://prover.certora.com/output/60724/0f3d1cd548d14f23b69d0548b874a350?anonymousKey=791604b2125415e6eca3829d412e89bbbc942304,PASSED +HandleAggregatedOps,3,130,https://prover.certora.com/output/60724/1b6aa5f14eeb4d868d61a6b2902aa287?anonymousKey=885f1d8eba85e8fc141ee563451f0e7397a9f373,PASSED +HandleAggregatedOps,3,200,https://prover.certora.com/output/60724/bed803ee5db94b6697f3fddca43e8828?anonymousKey=945090bff5e2c8cea938b3c018d6ee10e45d64e8,PASSED +HandleAggregatedOps,3,201,https://prover.certora.com/output/60724/9b9aee2c488b40a98c2248d9d0c1c2f0?anonymousKey=97d42a8ddddfb63a507e579ca6f77384ea5e1596,PASSED +HandleAggregatedOps,3,202,https://prover.certora.com/output/60724/a84bf2a03edb47889f71cb75911e2d8c?anonymousKey=cb6a4c0b93d76011804a4ba7e11bbe4818cedea4,PASSED +HandleAggregatedOps,3,210,https://prover.certora.com/output/60724/4260e29222384ff9a16eaf9c3da1b5cf?anonymousKey=5635d2efa7ce5979f13cd08c3e6722dcb9be73da,PASSED +HandleAggregatedOps,3,211,https://prover.certora.com/output/60724/0e4d3b5f0a434018be564f3f7c98838b?anonymousKey=0cf0fd89716146776f2c39a7c377d3698dc3406f,PASSED +HandleAggregatedOps,3,220,https://prover.certora.com/output/60724/d5b0dcb2bedf453ea29a355d6511a2c9?anonymousKey=f43e05484ef3722f0e6a71a1c3b957568fa91bb4,PASSED +HandleAggregatedOps,3,300,https://prover.certora.com/output/60724/00189a407aad421ca9dec41602ca2e8c?anonymousKey=4c650cb9788972b8191bd57ca0df5075bf82fa61,PASSED +HandleAggregatedOps,3,301,https://prover.certora.com/output/60724/2554ebb8cad140ee900e18709b7bd965?anonymousKey=3c2c6534a14373b0cbda6b56bbf95e3492a6029c,PASSED +HandleAggregatedOps,3,310,https://prover.certora.com/output/60724/6a8619cd26a8424b8dacaf1797c97190?anonymousKey=c3fac8b3e641a01649b3c0e8edb5f669c327a6e7,PASSED +HandleAggregatedOps,2,00,https://prover.certora.com/output/60724/12f981f9bd774caab7ceef11e5086e1a?anonymousKey=1135d12af38d676469bea543e23cd731bddfd013,PASSED +HandleAggregatedOps,2,01,https://prover.certora.com/output/60724/aaa689ca5fb14a3490db263f07b0e26b?anonymousKey=e1beba192be5bbec0e2464804a7e5163afb07618,PASSED +HandleAggregatedOps,2,02,https://prover.certora.com/output/60724/27589b72435744fcac6996d50ef5d7a1?anonymousKey=5826ae2266a7b2bda8cd4e97627ced0a99bc6954,PASSED +HandleAggregatedOps,2,03,https://prover.certora.com/output/60724/fc8ac2be53bd4aaca09ae080be7a5a43?anonymousKey=65e1fe6f45795566c12a05e47a2f05a4fc604645,PASSED +HandleAggregatedOps,2,10,https://prover.certora.com/output/60724/6942e750f42e452fb48be67636cc56c6?anonymousKey=33d90a8bef60ead250e6f6d71628fd56e6171dab,PASSED +HandleAggregatedOps,2,11,https://prover.certora.com/output/60724/e06e75b5e46e4f3b924e3643b7f595ba?anonymousKey=c858f1a776922ae600e8f9e2319de144c3ff06e6,PASSED +HandleAggregatedOps,2,12,https://prover.certora.com/output/60724/8b4c5e886d9a46f8a550ba9c6fb7ddc8?anonymousKey=c69d5094374d3394e497f64749720708b602cda5,PASSED +HandleAggregatedOps,2,13,https://prover.certora.com/output/60724/d18a6e6fb8ca4c6bb43f89c4498278f0?anonymousKey=953dde2614073fd4c38341a0cf5a926a7fac25e9,PASSED +HandleAggregatedOps,2,20,https://prover.certora.com/output/60724/87cb36328cca47f098ee74359059f7d6?anonymousKey=1ed7c9dbd6b5d36978c71575ddde3a37d38b3472,PASSED +HandleAggregatedOps,2,21,https://prover.certora.com/output/60724/74dc94e8b8f44c54aef24c0dd0ce13dc?anonymousKey=8574ce9692ad745899eb93d950ba148d47d7738c,PASSED +HandleAggregatedOps,2,22,https://prover.certora.com/output/60724/98225deba57b4cc2b43408ccff7652b7?anonymousKey=da75ddc91837e5fc5b2ce201fb7f714eb6644d61,PASSED +HandleAggregatedOps,2,30,https://prover.certora.com/output/60724/e5056b035edd418ea0b611535f428866?anonymousKey=745f9203802de5319a4a3a418aef2ae7d6ad1438,PASSED +HandleAggregatedOps,2,31,https://prover.certora.com/output/60724/d5c4383aedfc4caf86445f4e78148911?anonymousKey=0fa3141b94a52e00e087ea7eb4afd1f0f148ad7d,PASSED +HandleAggregatedOps,1,0,https://prover.certora.com/output/60724/2b3b7732957c433685d51de207883729?anonymousKey=db948e5b0734824bc3d8c1b1c7880b7c9670d3f2,PASSED +HandleAggregatedOps,1,1,https://prover.certora.com/output/60724/a1162c852b88454dbb18f6219684d91e?anonymousKey=fb2595072ff5549a4c7885f53e9916fa1a925e40,PASSED +HandleAggregatedOps,1,2,https://prover.certora.com/output/60724/d7749024a1a843369974e9b3d6fd0f05?anonymousKey=99721856bb24e0e85b7c26e321e192321d466d96,PASSED +HandleAggregatedOps,1,3,https://prover.certora.com/output/60724/193b3db7a6994f82a842d9bffd6d2466?anonymousKey=20d04d4534c76699f5f37646daa9d2189e8c756d,PASSED diff --git a/certora/report/certora_final_results_sanity.csv b/certora/report/certora_final_results_sanity.csv new file mode 100644 index 000000000..54a181b3d --- /dev/null +++ b/certora/report/certora_final_results_sanity.csv @@ -0,0 +1,85 @@ +Main String,First Number,Last Number,Original URL,Status +HandleAggregatedOps,3,000,https://prover.certora.com/output/60724/e64edd6a913540ac9f368b9e3eef1313?anonymousKey=3634d3f5a292fc3e981505ce70760c5448c26c06,FAILED +HandleAggregatedOps,3,001,https://prover.certora.com/output/60724/094e18dd410140bbb0f44c178438ed71?anonymousKey=98340dfd037b9dbf3adeda2a1610b94457c22604,PASSED +HandleAggregatedOps,3,002,https://prover.certora.com/output/60724/c50271181aeb4b00bf56a92eb4fc89de?anonymousKey=087d7d6fdd2429c36c26b62551b6aaf7c179b532,PASSED +HandleAggregatedOps,3,003,https://prover.certora.com/output/60724/3d892759879846aea18459428b859fcf?anonymousKey=ed43225eb84a604c8d75c63f95f3e6220101ee2e,PASSED +HandleAggregatedOps,3,010,https://prover.certora.com/output/60724/30bd5c648907461d9e96bb54df47ae1a?anonymousKey=f43466f2e4533c08960070458ed5010b445426b1,PASSED +HandleAggregatedOps,3,011,https://prover.certora.com/output/60724/80afb6bc7a394074b612ba02547b780d?anonymousKey=94970bc0ae6cdf8509b373f4ac8aef3614d0c1fb,PASSED +HandleAggregatedOps,3,012,https://prover.certora.com/output/60724/2283f3231cdd415f9ca3f4a7ade96d74?anonymousKey=f5c2e246e2626e63f3d280c4f097b36fc6af8fe2,PASSED +HandleAggregatedOps,3,013,https://prover.certora.com/output/60724/e6d5c6f8620c447bb686669ab92ffdcd?anonymousKey=1afee448867e87233bf3a15865ac0d1a775c3acf,PASSED +HandleAggregatedOps,3,020,https://prover.certora.com/output/60724/af77ca71531f462f8c73e7d995d806b9?anonymousKey=9448bbd7173949be8a29e667cea66a4962637b02,PASSED +HandleAggregatedOps,3,021,https://prover.certora.com/output/60724/a80c41a8c8ec4ec79566473870281559?anonymousKey=c0cf30869111d253c3ac3ef66574860678cf8b19,PASSED +HandleAggregatedOps,3,022,https://prover.certora.com/output/60724/9edebd0948a04d979ba384369d144ae9?anonymousKey=4acfc9f4f348b2064ceb87caef838eb3d65af4c7,PASSED +HandleAggregatedOps,3,023,https://prover.certora.com/output/60724/d8cbcfbe3731411c927447ee5f427275?anonymousKey=e98169ca59fdc612a253661bb1570814c64594be,FAILED +HandleAggregatedOps,3,030,https://prover.certora.com/output/60724/b2fb891f443648cd993c626906a2b854?anonymousKey=8b942daba0ad86535932f8060aff932135f86ca4,PASSED +HandleAggregatedOps,3,031,https://prover.certora.com/output/60724/b2394d5c91514c5692093a9278a9426d?anonymousKey=4a7bf456259faf7bc44ff472d4d103df96b6f09c,PASSED +HandleAggregatedOps,3,032,https://prover.certora.com/output/60724/27c3e793925d44c6bf4f595705cd92d6?anonymousKey=d174075eb65bfd99ff7aebf6a84add5b8199f33a,FAILED +HandleAggregatedOps,3,033,https://prover.certora.com/output/60724/9eaeb7cd7ef246aeab26c70a3a6ee989?anonymousKey=95e281368a3826db782cc212ec92ef0b178ee762,FAILED +HandleAggregatedOps,3,100,https://prover.certora.com/output/60724/3a20e79890394ed99e60eb9d2b666d8f?anonymousKey=4c1767e8c6f8848454f9c6c023f7b9b1cf49ff68,PASSED +HandleAggregatedOps,3,101,https://prover.certora.com/output/60724/4190a164b5654d01a5df4c33ee821f3c?anonymousKey=1cef8db7c6452cd5435d959e34a986f02f1b44e3,PASSED +HandleAggregatedOps,3,102,https://prover.certora.com/output/60724/a3ad50a219ab4ee88040eadbe00c5bc4?anonymousKey=10f6c8eaee247a09d0e1c735799d711b277e05d8,PASSED +HandleAggregatedOps,3,103,https://prover.certora.com/output/60724/def9cdd818984fb186f56dc762090a3e?anonymousKey=56643de82cd8681719ec30a1bedd0e3d59fc924e,PASSED +HandleAggregatedOps,3,110,https://prover.certora.com/output/60724/9f1b9eb00ce241d8acf2ae24f232185b?anonymousKey=6e688917a9cc7136db61f728491a4d23796f730f,PASSED +HandleAggregatedOps,3,111,https://prover.certora.com/output/60724/90192a80b7c4497c9206a1468f0cda92?anonymousKey=bd015de1869fa047a029fa4b3eabdf3b7193feaf,PASSED +HandleAggregatedOps,3,112,https://prover.certora.com/output/60724/58397ae0b88940e2b0ab6a9f1f19cb80?anonymousKey=f8d703d7c66a15056dd86cdbd1555c0726995fa6,PASSED +HandleAggregatedOps,3,113,https://prover.certora.com/output/60724/e94555b81bf44569af76abf73e29c8b9?anonymousKey=2c7ffa5fa74d02f2586fb895014f8dc60f5e70dc,FAILED +HandleAggregatedOps,3,120,https://prover.certora.com/output/60724/93076f28336344488c6fd0e9f6a5a117?anonymousKey=9171a603a9f68298c2f9fb49cc96a53cc6ba0fea,PASSED +HandleAggregatedOps,3,121,https://prover.certora.com/output/60724/18230c011677446f8ed4af3945d35529?anonymousKey=17e6307ea269e109c6e2c846c12d2badcb9544ab,PASSED +HandleAggregatedOps,3,122,https://prover.certora.com/output/60724/bd92b8004d944d26b783d0e591b37236?anonymousKey=328e501e2fdeafe47fdec908ea6d3a4e511aac00,PASSED +HandleAggregatedOps,3,123,https://prover.certora.com/output/60724/c7fc3737b6f04dffbc09bd5a984afb1d?anonymousKey=2c5660b62212d30930bdccfade1e0c5bc7214689,FAILED +HandleAggregatedOps,3,130,https://prover.certora.com/output/60724/a3621b4bd9664b6b8c8405e209696a7f?anonymousKey=12124533304f7fb8453966f55050119de1500537,PASSED +HandleAggregatedOps,3,131,https://prover.certora.com/output/60724/8140b8864a8a49f284b31f00b7e5df3d?anonymousKey=2c61d69ea7dd114f94ebb9c9814306dd5c2a6d29,PASSED +HandleAggregatedOps,3,132,https://prover.certora.com/output/60724/5908ae03bc7040e1b869a5a0cc1332fd?anonymousKey=ac0e07a7aae9364ba43c1f9e3efe148c7924fb97,FAILED +HandleAggregatedOps,3,133,https://prover.certora.com/output/60724/6ea3cfad60ac48f584b4b2f4165511f6?anonymousKey=162487f293de2bd897fb0b1029b5eebc57005a26,FAILED +HandleAggregatedOps,3,200,https://prover.certora.com/output/60724/277a124a99a846dc9b5a316042b6775f?anonymousKey=44d1262929c04f0f1a40d795ba398558f472bd33,PASSED +HandleAggregatedOps,3,201,https://prover.certora.com/output/60724/edba0f4edd664766808ce773acb2bfdd?anonymousKey=5e6f22911362bfece7f0b4a00bbae60ed1dbfaf1,PASSED +HandleAggregatedOps,3,202,https://prover.certora.com/output/60724/e23cb483798a4b0d8f83f52dceca038a?anonymousKey=915e818c8c87467da158385e91e3089a850879f0,PASSED +HandleAggregatedOps,3,203,https://prover.certora.com/output/60724/41ae2007a36748a9b9844c91e98db912?anonymousKey=cf163e16b0ac3dabbb1acc75c7c1880e73d34c9d,FAILED +HandleAggregatedOps,3,210,https://prover.certora.com/output/60724/23affcc77ef543368e03d073c8c288e0?anonymousKey=c2d647445d510d298639b2a4d0d06414cf61cd4b,PASSED +HandleAggregatedOps,3,211,https://prover.certora.com/output/60724/592a3c01e5474bf496a2eafdd8a3dfe1?anonymousKey=70ce93af5d43e6768ae129c370c76f3fe2067d76,PASSED +HandleAggregatedOps,3,212,https://prover.certora.com/output/60724/f432273a2f074339849bbdbfc66d3058?anonymousKey=a4ecf8657b8e97b8618ddb68639dd93991e2aa60,FAILED +HandleAggregatedOps,3,213,https://prover.certora.com/output/60724/c80d2562fd6e4774a0828e6f8686ed01?anonymousKey=4905acd2d528f67d92af20e87db6aacdac1c7980,FAILED +HandleAggregatedOps,3,220,https://prover.certora.com/output/60724/b9d3ba973f6f4416b08dd5bc837ef2e2?anonymousKey=f261fe4470862660f6a63046e1909d59fbe92642,PASSED +HandleAggregatedOps,3,221,https://prover.certora.com/output/60724/9190dce2fe07437bba05bcc37365e555?anonymousKey=95769ad3712b0c283f5904e53a464350eebf7493,FAILED +HandleAggregatedOps,3,222,https://prover.certora.com/output/60724/913877c0b30a423790595d96480052ba?anonymousKey=04fa7fb5fff6489c09045519c99054d4324c2445,FAILED +HandleAggregatedOps,3,223,https://prover.certora.com/output/60724/98925043f2894e2eb0b6ec64fde65c9d?anonymousKey=50991c4542ec245c047b3d6be378a3affacb1f5d,FAILED +HandleAggregatedOps,3,230,https://prover.certora.com/output/60724/5c221a3af3024ccdbdf2349d84447f40?anonymousKey=586a62ded7408ceead073359ddfc18240c8c9690,FAILED +HandleAggregatedOps,3,231,https://prover.certora.com/output/60724/b1b30ff0e9ae4bb7a8e3dea19440f8b8?anonymousKey=daee0867f4fc0d3bc345dbfc616d0f68a958221c,FAILED +HandleAggregatedOps,3,232,https://prover.certora.com/output/60724/4d64751f4c3f4fcdbd05bbb972d2bdf7?anonymousKey=c062add5fef2bd881170b232a1fab2387d83041b,FAILED +HandleAggregatedOps,3,233,https://prover.certora.com/output/60724/6d459a85b06d46eebd99017edd83aff2?anonymousKey=f35db50b53172a9d3b67fcd856802514d75c67df,FAILED +HandleAggregatedOps,3,300,https://prover.certora.com/output/60724/5c50bb8faf894f4cbd85f920d8b5bb72?anonymousKey=7c76afe1db9fab483fb3ef18c38169b1335f2a5e,PASSED +HandleAggregatedOps,3,301,https://prover.certora.com/output/60724/7c865576bc09484bb6a39f7a83916b3e?anonymousKey=c57182e6804567fd5c26f60b5970ec35a4482175,PASSED +HandleAggregatedOps,3,302,https://prover.certora.com/output/60724/d39f9295f34942328e383f72d30a03c5?anonymousKey=2d96d579c5b1dd9bc4bd906ae638f777e0baf7a0,FAILED +HandleAggregatedOps,3,303,https://prover.certora.com/output/60724/d000d5bdee214358867621b5a157d0e1?anonymousKey=65497260c568f4d462a509b4c00691bba3680c3b,FAILED +HandleAggregatedOps,3,310,https://prover.certora.com/output/60724/d98ed98e8122419e81169ea9bdd98e1a?anonymousKey=6c966ef651882da2b90cd2050185284160fe5299,PASSED +HandleAggregatedOps,3,311,https://prover.certora.com/output/60724/643180c3e4874646b753c2d9b760cb7c?anonymousKey=7d07f5e7cd229d69e4b7d05cc616a8f7c63cca11,PASSED +HandleAggregatedOps,3,312,https://prover.certora.com/output/60724/72c2e35e0fac420085d4987d34d2aaae?anonymousKey=64e93434c3bd02326b52d55838d2de39a5b60e28,FAILED +HandleAggregatedOps,3,313,https://prover.certora.com/output/60724/e704badb6a874924844e9965325c42b9?anonymousKey=d898e2a4102c33bcb41da2a22d7e3495595e596b,FAILED +HandleAggregatedOps,3,320,https://prover.certora.com/output/60724/f05a0b8a107a4a6aab6c8999e720676b?anonymousKey=32944ba6db92203788d882ee1b8c8a0b3470e81e,FAILED +HandleAggregatedOps,3,321,https://prover.certora.com/output/60724/08a81a2667f04169b824048925aabbec?anonymousKey=b68dd58e60993a708e4110d9ac59ea9c290b5b0a,FAILED +HandleAggregatedOps,3,322,https://prover.certora.com/output/60724/469f3ba61bae4951a66c6348a5685622?anonymousKey=003d0809bf97b8ee6e2b77604a427006a6eed414,FAILED +HandleAggregatedOps,3,323,https://prover.certora.com/output/60724/200e59f3a0524862bd3a1c09082733df?anonymousKey=f7f57c6d1e7ecc78544b72338adc7da930018680,FAILED +HandleAggregatedOps,3,330,https://prover.certora.com/output/60724/3610184c8a4d447f89840c00882c3097?anonymousKey=1c2168a3faaf0d2a9ade926a8175fb374c093c08,FAILED +HandleAggregatedOps,3,331,https://prover.certora.com/output/60724/e0e04b34121140fcbc22ead7e414871d?anonymousKey=b824404517625fbe8b85eaf58b1d5e67b43a4724,FAILED +HandleAggregatedOps,3,332,https://prover.certora.com/output/60724/947b97acc73c4f6996a24bc6c864116c?anonymousKey=018a193602d7a79cd57e7847d8be0efa4fff52e7,FAILED +HandleAggregatedOps,3,333,https://prover.certora.com/output/60724/ac3de85243984899b7484c2efce08539?anonymousKey=b075c73e6af9bdf6b848f412bdc3511316f7af0b,FAILED +HandleAggregatedOps,2,00,https://prover.certora.com/output/60724/3ceb7a6e50f94553802782cf7dc6b8cc?anonymousKey=ae127caf28bf2dab31effc3a9153b9e177592b79,FAILED +HandleAggregatedOps,2,01,https://prover.certora.com/output/60724/240c20b4a35a4bdeaea3b99dbe3e3781?anonymousKey=ce5e1d6048c9a590e869662bdb3c5392b56417d4,PASSED +HandleAggregatedOps,2,02,https://prover.certora.com/output/60724/36962bc9678741de94f207aff967e881?anonymousKey=c07d25f79ffc121bc949f5c433e07fd8c87585e4,PASSED +HandleAggregatedOps,2,03,https://prover.certora.com/output/60724/9a5f23d4492d4162aaf0572dde02f7a9?anonymousKey=748eb853abe091b6765a2c861a0717d19f7a85a5,PASSED +HandleAggregatedOps,2,10,https://prover.certora.com/output/60724/28a521c2b756454a95c8d329ee94a1a5?anonymousKey=5e3ef941945fbe2e0cd61c57e78405b5a955f2d8,PASSED +HandleAggregatedOps,2,11,https://prover.certora.com/output/60724/b452f9b1ba3b4c359eca93925f0df10a?anonymousKey=bef456b1d3208f81ed6c8c80f16f1962ee992775,PASSED +HandleAggregatedOps,2,12,https://prover.certora.com/output/60724/60e2e0fa318146a088fabf947c5036b5?anonymousKey=73f5039671a946b9ec1a8952cdf8c7e267633fe0,PASSED +HandleAggregatedOps,2,13,https://prover.certora.com/output/60724/777e6b601c3b4a0aafd2a1d447cda84b?anonymousKey=65c0f9dc2f29e2bbd292af8fe856f9e24e6bb325,PASSED +HandleAggregatedOps,2,20,https://prover.certora.com/output/60724/b7198bf9de994947b0ce01b33e49a4f3?anonymousKey=85781becd95e1de72d618057127463ab762db4fe,PASSED +HandleAggregatedOps,2,21,https://prover.certora.com/output/60724/7877b648fa1140a6a1d4d505e524494e?anonymousKey=e573b06f6518b621b0880ffe6d14253d4752caa1,PASSED +HandleAggregatedOps,2,22,https://prover.certora.com/output/60724/6a9c2ddd1a35430da296028668677392?anonymousKey=0c96d419ceda754cd21fbb5d538b93ada2b4c4d2,PASSED +HandleAggregatedOps,2,23,https://prover.certora.com/output/60724/ae0266a699fb42b69020f88285873fc1?anonymousKey=51e7075cfed2ec0a7c5adbd8848a0f05a21fb631,FAILED +HandleAggregatedOps,2,30,https://prover.certora.com/output/60724/5a8fe7205b4949b18135560ad8fc33d8?anonymousKey=b258f487f4e594d9e78be01e517856cc47d7cacb,PASSED +HandleAggregatedOps,2,31,https://prover.certora.com/output/60724/2c68fac884f24812b772e5b2ed636bf4?anonymousKey=8db294fc7cf33164fde71616ba653a4537aee560,PASSED +HandleAggregatedOps,2,32,https://prover.certora.com/output/60724/e95d2a95482a47109edd61a20fa3c757?anonymousKey=a7ead1f1c9e93a2b673706f9a0875bdd7254b98e,FAILED +HandleAggregatedOps,2,33,https://prover.certora.com/output/60724/d9366bd0ba3c43b1a6c5b0d4f85f5407?anonymousKey=c275585623784a04ce4b0914cac71195f0f18e60,FAILED +HandleAggregatedOps,1,0,https://prover.certora.com/output/60724/eae4d2b90573448c8592bfe805dae5e0?anonymousKey=d760becb5921b6cdea7dc1d8634b1904c7c2b926,FAILED +HandleAggregatedOps,1,1,https://prover.certora.com/output/60724/4f9b483c717942bcb1e8dcd8bef187f1?anonymousKey=42388a9fda99b0866a0424d2a07e5a83cc79d830,PASSED +HandleAggregatedOps,1,2,https://prover.certora.com/output/60724/c2da067b5a914e13bd82bca2e3aa1b6f?anonymousKey=f0ef76620530d27045b236ecd955675a58d51aa0,PASSED +HandleAggregatedOps,1,3,https://prover.certora.com/output/60724/424aa54818f0405a9e0d2d40d2ad265c?anonymousKey=5f6b0d50097e16e4e09ad3775e949823bbf3b47e,PASSED diff --git a/certora/report/certora_results_regular.md b/certora/report/certora_results_regular.md new file mode 100644 index 000000000..f7384803f --- /dev/null +++ b/certora/report/certora_results_regular.md @@ -0,0 +1,56 @@ +| Rule | URL | +|------|-----| +| onlyValidatedCalls_NonHandleOps | https://prover.certora.com/output/60724/5a3bc1fbf49d4b7ba2ad809176b14999?anonymousKey=9bf9c24f90efa39a4b70108047f0bcf6d1bc6248 | +| onlyValidatedCalls_3HandleOps | https://prover.certora.com/output/60724/8583146d12a245a68ccfa01699609574?anonymousKey=250b24ec6ac3249e1baed41c5bc7b80b6aa9f5ff | +| onlyValidatedCalls_2HandleOps | https://prover.certora.com/output/60724/dabc1d0b52634ccd8b98a785f9df1dad?anonymousKey=055630d4c0801755673c620e3ca4ac5bb63ec5c9 | +| onlyValidatedCalls_1HandleOps | https://prover.certora.com/output/60724/5297f047034943ed980cf590f006c794?anonymousKey=02bf0b254e6a74903c1c9b66f4307141bcf4426d | +| onlyValidatedCalls_0HandleOps | https://prover.certora.com/output/60724/d7a7af92278f4c35b407f3e25a0c1fdc?anonymousKey=0e1c881e458d0977cee46703999a544e9e48cacd | +| onlyValidatedCalls_3HandleAggregatedOps000 | https://prover.certora.com/output/60724/dc61f3406e1b45afa3ec5fc480acad12?anonymousKey=57a630c1ba831ffbda48e641a294f57ffb55f776 | +| onlyValidatedCalls_3HandleAggregatedOps001 | https://prover.certora.com/output/60724/98838dafaba7443db41fc6a5d038239b?anonymousKey=15c011365c6645b5161d70fe6f6a68c55f114c09 | +| onlyValidatedCalls_3HandleAggregatedOps002 | https://prover.certora.com/output/60724/a13c20b2742442218d4033b2bbcc1575?anonymousKey=f38dcb73883882d99f492141cadd11d98169dbf1 | +| onlyValidatedCalls_3HandleAggregatedOps003 | https://prover.certora.com/output/60724/d130cea66d1c44379877cc5506e3f498?anonymousKey=3c1ae5775f8d672926055aae4529b294ce514048 | +| onlyValidatedCalls_3HandleAggregatedOps010 | https://prover.certora.com/output/60724/e6e7d20e38034acba4b579a135605789?anonymousKey=738136472db3ace0198b45eeb273e3b4ca799410 | +| onlyValidatedCalls_3HandleAggregatedOps011 | https://prover.certora.com/output/60724/8ec06ba489004e3d825f896154ae4b8e?anonymousKey=4f2a87346b42bdcb0f09123abd2ff866ce8f8635 | +| onlyValidatedCalls_3HandleAggregatedOps012 | https://prover.certora.com/output/60724/dd2b6b67e7604216b91dd635ea40a3a9?anonymousKey=a8c07557aa3ec4befd7987c824caa748a5559482 | +| onlyValidatedCalls_3HandleAggregatedOps013 | https://prover.certora.com/output/60724/70da1e37d18e4f43a10946af68f4dbe1?anonymousKey=7380044b45c11baba43a1d6f5c4635e404ec50f4 | +| onlyValidatedCalls_3HandleAggregatedOps020 | https://prover.certora.com/output/60724/fec7e4a70f2d414ab652863c886375a9?anonymousKey=f40c63a1a8c827febd1636c3bad1e48ca20db81f | +| onlyValidatedCalls_3HandleAggregatedOps021 | https://prover.certora.com/output/60724/f24730f769c449368f9af037fe9304c0?anonymousKey=c3b67523341940aa349782e9149487403eb6bf12 | +| onlyValidatedCalls_3HandleAggregatedOps022 | https://prover.certora.com/output/60724/b0c6a515eb8e4e84aff5329bb82efbc5?anonymousKey=3c30e47af257d7aeb47e2c5a48928a457f355947 | +| onlyValidatedCalls_3HandleAggregatedOps030 | https://prover.certora.com/output/60724/bc99c47a3eaa4f25b0d3ec47b61c94ba?anonymousKey=4f422b4a21aa40c068821d8adb9be98d49b49eaf | +| onlyValidatedCalls_3HandleAggregatedOps031 | https://prover.certora.com/output/60724/726e528e49304dc9aa6e9929316fa22a?anonymousKey=6fc96524153f72b8048e90a5c79d2db99779c4ed | +| onlyValidatedCalls_3HandleAggregatedOps100 | https://prover.certora.com/output/60724/c32db3ef9bd347a690652da34e5c97d8?anonymousKey=6b7c6cc3ea5ba801e123a31d37a299695fac2f1a | +| onlyValidatedCalls_3HandleAggregatedOps101 | https://prover.certora.com/output/60724/c5a85703d60c4f5eb02c3f94de12a0d1?anonymousKey=2485460100fe1b87064967443763943d57b4391b | +| onlyValidatedCalls_3HandleAggregatedOps102 | https://prover.certora.com/output/60724/23cfbc2ec45b4da38e1dad26b624c5c5?anonymousKey=82f7d69f4362c308a2e0ab5f350fb065652c7de8 | +| onlyValidatedCalls_3HandleAggregatedOps103 | https://prover.certora.com/output/60724/9077432b3a104cb397917be33f1505c4?anonymousKey=35b96455661b58fae5e3ff8f240913a10a3597bf | +| onlyValidatedCalls_3HandleAggregatedOps110 | https://prover.certora.com/output/60724/0a8f15cdaed8421e918ab78a7823d176?anonymousKey=74c435c3b0e58331ad6b305a8e551d3e343628e1 | +| onlyValidatedCalls_3HandleAggregatedOps111 | https://prover.certora.com/output/60724/3f63c12e3dfd4f7d8cbef39094fa578f?anonymousKey=f12ce8b6dd9a155a1d4d2f899e2138b25667df35 | +| onlyValidatedCalls_3HandleAggregatedOps112 | https://prover.certora.com/output/60724/685f3fa404f54b20ac3f28cf23ce9212?anonymousKey=1a1d209f216b26235197e02950dd26e663a81f70 | +| onlyValidatedCalls_3HandleAggregatedOps120 | https://prover.certora.com/output/60724/ec8e36615726418cb685df5de12d787b?anonymousKey=2511cccfacd5b5b0ca6fb9837cb57f3a3ac1571a | +| onlyValidatedCalls_3HandleAggregatedOps121 | https://prover.certora.com/output/60724/0f3d1cd548d14f23b69d0548b874a350?anonymousKey=791604b2125415e6eca3829d412e89bbbc942304 | +| onlyValidatedCalls_3HandleAggregatedOps130 | https://prover.certora.com/output/60724/1b6aa5f14eeb4d868d61a6b2902aa287?anonymousKey=885f1d8eba85e8fc141ee563451f0e7397a9f373 | +| onlyValidatedCalls_3HandleAggregatedOps200 | https://prover.certora.com/output/60724/bed803ee5db94b6697f3fddca43e8828?anonymousKey=945090bff5e2c8cea938b3c018d6ee10e45d64e8 | +| onlyValidatedCalls_3HandleAggregatedOps201 | https://prover.certora.com/output/60724/9b9aee2c488b40a98c2248d9d0c1c2f0?anonymousKey=97d42a8ddddfb63a507e579ca6f77384ea5e1596 | +| onlyValidatedCalls_3HandleAggregatedOps202 | https://prover.certora.com/output/60724/a84bf2a03edb47889f71cb75911e2d8c?anonymousKey=cb6a4c0b93d76011804a4ba7e11bbe4818cedea4 | +| onlyValidatedCalls_3HandleAggregatedOps210 | https://prover.certora.com/output/60724/4260e29222384ff9a16eaf9c3da1b5cf?anonymousKey=5635d2efa7ce5979f13cd08c3e6722dcb9be73da | +| onlyValidatedCalls_3HandleAggregatedOps211 | https://prover.certora.com/output/60724/0e4d3b5f0a434018be564f3f7c98838b?anonymousKey=0cf0fd89716146776f2c39a7c377d3698dc3406f | +| onlyValidatedCalls_3HandleAggregatedOps220 | https://prover.certora.com/output/60724/d5b0dcb2bedf453ea29a355d6511a2c9?anonymousKey=f43e05484ef3722f0e6a71a1c3b957568fa91bb4 | +| onlyValidatedCalls_3HandleAggregatedOps300 | https://prover.certora.com/output/60724/00189a407aad421ca9dec41602ca2e8c?anonymousKey=4c650cb9788972b8191bd57ca0df5075bf82fa61 | +| onlyValidatedCalls_3HandleAggregatedOps301 | https://prover.certora.com/output/60724/2554ebb8cad140ee900e18709b7bd965?anonymousKey=3c2c6534a14373b0cbda6b56bbf95e3492a6029c | +| onlyValidatedCalls_3HandleAggregatedOps310 | https://prover.certora.com/output/60724/6a8619cd26a8424b8dacaf1797c97190?anonymousKey=c3fac8b3e641a01649b3c0e8edb5f669c327a6e7 | +| onlyValidatedCalls_2HandleAggregatedOps00 | https://prover.certora.com/output/60724/12f981f9bd774caab7ceef11e5086e1a?anonymousKey=1135d12af38d676469bea543e23cd731bddfd013 | +| onlyValidatedCalls_2HandleAggregatedOps01 | https://prover.certora.com/output/60724/aaa689ca5fb14a3490db263f07b0e26b?anonymousKey=e1beba192be5bbec0e2464804a7e5163afb07618 | +| onlyValidatedCalls_2HandleAggregatedOps02 | https://prover.certora.com/output/60724/27589b72435744fcac6996d50ef5d7a1?anonymousKey=5826ae2266a7b2bda8cd4e97627ced0a99bc6954 | +| onlyValidatedCalls_2HandleAggregatedOps03 | https://prover.certora.com/output/60724/fc8ac2be53bd4aaca09ae080be7a5a43?anonymousKey=65e1fe6f45795566c12a05e47a2f05a4fc604645 | +| onlyValidatedCalls_2HandleAggregatedOps10 | https://prover.certora.com/output/60724/6942e750f42e452fb48be67636cc56c6?anonymousKey=33d90a8bef60ead250e6f6d71628fd56e6171dab | +| onlyValidatedCalls_2HandleAggregatedOps11 | https://prover.certora.com/output/60724/e06e75b5e46e4f3b924e3643b7f595ba?anonymousKey=c858f1a776922ae600e8f9e2319de144c3ff06e6 | +| onlyValidatedCalls_2HandleAggregatedOps12 | https://prover.certora.com/output/60724/8b4c5e886d9a46f8a550ba9c6fb7ddc8?anonymousKey=c69d5094374d3394e497f64749720708b602cda5 | +| onlyValidatedCalls_2HandleAggregatedOps13 | https://prover.certora.com/output/60724/d18a6e6fb8ca4c6bb43f89c4498278f0?anonymousKey=953dde2614073fd4c38341a0cf5a926a7fac25e9 | +| onlyValidatedCalls_2HandleAggregatedOps20 | https://prover.certora.com/output/60724/87cb36328cca47f098ee74359059f7d6?anonymousKey=1ed7c9dbd6b5d36978c71575ddde3a37d38b3472 | +| onlyValidatedCalls_2HandleAggregatedOps21 | https://prover.certora.com/output/60724/74dc94e8b8f44c54aef24c0dd0ce13dc?anonymousKey=8574ce9692ad745899eb93d950ba148d47d7738c | +| onlyValidatedCalls_2HandleAggregatedOps22 | https://prover.certora.com/output/60724/98225deba57b4cc2b43408ccff7652b7?anonymousKey=da75ddc91837e5fc5b2ce201fb7f714eb6644d61 | +| onlyValidatedCalls_2HandleAggregatedOps30 | https://prover.certora.com/output/60724/e5056b035edd418ea0b611535f428866?anonymousKey=745f9203802de5319a4a3a418aef2ae7d6ad1438 | +| onlyValidatedCalls_2HandleAggregatedOps31 | https://prover.certora.com/output/60724/d5c4383aedfc4caf86445f4e78148911?anonymousKey=0fa3141b94a52e00e087ea7eb4afd1f0f148ad7d | +| onlyValidatedCalls_1HandleAggregatedOps0 | https://prover.certora.com/output/60724/2b3b7732957c433685d51de207883729?anonymousKey=db948e5b0734824bc3d8c1b1c7880b7c9670d3f2 | +| onlyValidatedCalls_1HandleAggregatedOps1 | https://prover.certora.com/output/60724/a1162c852b88454dbb18f6219684d91e?anonymousKey=fb2595072ff5549a4c7885f53e9916fa1a925e40 | +| onlyValidatedCalls_1HandleAggregatedOps2 | https://prover.certora.com/output/60724/d7749024a1a843369974e9b3d6fd0f05?anonymousKey=99721856bb24e0e85b7c26e321e192321d466d96 | +| onlyValidatedCalls_1HandleAggregatedOps3 | https://prover.certora.com/output/60724/193b3db7a6994f82a842d9bffd6d2466?anonymousKey=20d04d4534c76699f5f37646daa9d2189e8c756d | diff --git a/certora/report/certora_results_sanity.md b/certora/report/certora_results_sanity.md new file mode 100644 index 000000000..7647c370d --- /dev/null +++ b/certora/report/certora_results_sanity.md @@ -0,0 +1,90 @@ +| Rule | URL | +|------|-----| +| sanity_onlyValidatedCalls_3HandleOps | https://prover.certora.com/output/60724/5fff655ef21c4f38a1c3e523fdf77161?anonymousKey=387bbd493e771a2b0d47062f9ba757df1a191870 | +| sanity_onlyValidatedCalls_2HandleOps | https://prover.certora.com/output/60724/2e50c4bd6d1b425d96667d6c8132eb43?anonymousKey=57bcb2801ffd3c0236125b2a629ad13944b54ec0 | +| sanity_onlyValidatedCalls_1HandleOps | https://prover.certora.com/output/60724/519dc2ef505540328e50c1b0f74e7045?anonymousKey=16a8365f6adfec4c087125078b34f7a9d37775ce | +| sanity_onlyValidatedCalls_0HandleOps | https://prover.certora.com/output/60724/b7633e80101e4d40bf3439e615a4c850?anonymousKey=48f8a5826ae1e7ff05ace2605b52796f4ae70d18 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps000 | https://prover.certora.com/output/60724/e64edd6a913540ac9f368b9e3eef1313?anonymousKey=3634d3f5a292fc3e981505ce70760c5448c26c06 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps001 | https://prover.certora.com/output/60724/094e18dd410140bbb0f44c178438ed71?anonymousKey=98340dfd037b9dbf3adeda2a1610b94457c22604 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps002 | https://prover.certora.com/output/60724/c50271181aeb4b00bf56a92eb4fc89de?anonymousKey=087d7d6fdd2429c36c26b62551b6aaf7c179b532 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps003 | https://prover.certora.com/output/60724/3d892759879846aea18459428b859fcf?anonymousKey=ed43225eb84a604c8d75c63f95f3e6220101ee2e | +| sanity_onlyValidatedCalls_3HandleAggregatedOps010 | https://prover.certora.com/output/60724/30bd5c648907461d9e96bb54df47ae1a?anonymousKey=f43466f2e4533c08960070458ed5010b445426b1 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps011 | https://prover.certora.com/output/60724/80afb6bc7a394074b612ba02547b780d?anonymousKey=94970bc0ae6cdf8509b373f4ac8aef3614d0c1fb | +| sanity_onlyValidatedCalls_3HandleAggregatedOps012 | https://prover.certora.com/output/60724/2283f3231cdd415f9ca3f4a7ade96d74?anonymousKey=f5c2e246e2626e63f3d280c4f097b36fc6af8fe2 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps013 | https://prover.certora.com/output/60724/e6d5c6f8620c447bb686669ab92ffdcd?anonymousKey=1afee448867e87233bf3a15865ac0d1a775c3acf | +| sanity_onlyValidatedCalls_3HandleAggregatedOps020 | https://prover.certora.com/output/60724/af77ca71531f462f8c73e7d995d806b9?anonymousKey=9448bbd7173949be8a29e667cea66a4962637b02 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps021 | https://prover.certora.com/output/60724/a80c41a8c8ec4ec79566473870281559?anonymousKey=c0cf30869111d253c3ac3ef66574860678cf8b19 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps022 | https://prover.certora.com/output/60724/9edebd0948a04d979ba384369d144ae9?anonymousKey=4acfc9f4f348b2064ceb87caef838eb3d65af4c7 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps023 | https://prover.certora.com/output/60724/d8cbcfbe3731411c927447ee5f427275?anonymousKey=e98169ca59fdc612a253661bb1570814c64594be | +| sanity_onlyValidatedCalls_3HandleAggregatedOps030 | https://prover.certora.com/output/60724/b2fb891f443648cd993c626906a2b854?anonymousKey=8b942daba0ad86535932f8060aff932135f86ca4 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps031 | https://prover.certora.com/output/60724/b2394d5c91514c5692093a9278a9426d?anonymousKey=4a7bf456259faf7bc44ff472d4d103df96b6f09c | +| sanity_onlyValidatedCalls_3HandleAggregatedOps032 | https://prover.certora.com/output/60724/27c3e793925d44c6bf4f595705cd92d6?anonymousKey=d174075eb65bfd99ff7aebf6a84add5b8199f33a | +| sanity_onlyValidatedCalls_3HandleAggregatedOps033 | https://prover.certora.com/output/60724/9eaeb7cd7ef246aeab26c70a3a6ee989?anonymousKey=95e281368a3826db782cc212ec92ef0b178ee762 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps100 | https://prover.certora.com/output/60724/3a20e79890394ed99e60eb9d2b666d8f?anonymousKey=4c1767e8c6f8848454f9c6c023f7b9b1cf49ff68 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps101 | https://prover.certora.com/output/60724/4190a164b5654d01a5df4c33ee821f3c?anonymousKey=1cef8db7c6452cd5435d959e34a986f02f1b44e3 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps102 | https://prover.certora.com/output/60724/a3ad50a219ab4ee88040eadbe00c5bc4?anonymousKey=10f6c8eaee247a09d0e1c735799d711b277e05d8 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps103 | https://prover.certora.com/output/60724/def9cdd818984fb186f56dc762090a3e?anonymousKey=56643de82cd8681719ec30a1bedd0e3d59fc924e | +| sanity_onlyValidatedCalls_3HandleAggregatedOps110 | https://prover.certora.com/output/60724/9f1b9eb00ce241d8acf2ae24f232185b?anonymousKey=6e688917a9cc7136db61f728491a4d23796f730f | +| sanity_onlyValidatedCalls_3HandleAggregatedOps111 | https://prover.certora.com/output/60724/90192a80b7c4497c9206a1468f0cda92?anonymousKey=bd015de1869fa047a029fa4b3eabdf3b7193feaf | +| sanity_onlyValidatedCalls_3HandleAggregatedOps112 | https://prover.certora.com/output/60724/58397ae0b88940e2b0ab6a9f1f19cb80?anonymousKey=f8d703d7c66a15056dd86cdbd1555c0726995fa6 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps113 | https://prover.certora.com/output/60724/e94555b81bf44569af76abf73e29c8b9?anonymousKey=2c7ffa5fa74d02f2586fb895014f8dc60f5e70dc | +| sanity_onlyValidatedCalls_3HandleAggregatedOps120 | https://prover.certora.com/output/60724/93076f28336344488c6fd0e9f6a5a117?anonymousKey=9171a603a9f68298c2f9fb49cc96a53cc6ba0fea | +| sanity_onlyValidatedCalls_3HandleAggregatedOps121 | https://prover.certora.com/output/60724/18230c011677446f8ed4af3945d35529?anonymousKey=17e6307ea269e109c6e2c846c12d2badcb9544ab | +| sanity_onlyValidatedCalls_3HandleAggregatedOps122 | https://prover.certora.com/output/60724/bd92b8004d944d26b783d0e591b37236?anonymousKey=328e501e2fdeafe47fdec908ea6d3a4e511aac00 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps123 | https://prover.certora.com/output/60724/c7fc3737b6f04dffbc09bd5a984afb1d?anonymousKey=2c5660b62212d30930bdccfade1e0c5bc7214689 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps130 | https://prover.certora.com/output/60724/a3621b4bd9664b6b8c8405e209696a7f?anonymousKey=12124533304f7fb8453966f55050119de1500537 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps131 | https://prover.certora.com/output/60724/8140b8864a8a49f284b31f00b7e5df3d?anonymousKey=2c61d69ea7dd114f94ebb9c9814306dd5c2a6d29 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps132 | https://prover.certora.com/output/60724/5908ae03bc7040e1b869a5a0cc1332fd?anonymousKey=ac0e07a7aae9364ba43c1f9e3efe148c7924fb97 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps133 | https://prover.certora.com/output/60724/6ea3cfad60ac48f584b4b2f4165511f6?anonymousKey=162487f293de2bd897fb0b1029b5eebc57005a26 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps200 | https://prover.certora.com/output/60724/277a124a99a846dc9b5a316042b6775f?anonymousKey=44d1262929c04f0f1a40d795ba398558f472bd33 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps201 | https://prover.certora.com/output/60724/edba0f4edd664766808ce773acb2bfdd?anonymousKey=5e6f22911362bfece7f0b4a00bbae60ed1dbfaf1 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps202 | https://prover.certora.com/output/60724/e23cb483798a4b0d8f83f52dceca038a?anonymousKey=915e818c8c87467da158385e91e3089a850879f0 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps203 | https://prover.certora.com/output/60724/41ae2007a36748a9b9844c91e98db912?anonymousKey=cf163e16b0ac3dabbb1acc75c7c1880e73d34c9d | +| sanity_onlyValidatedCalls_3HandleAggregatedOps210 | https://prover.certora.com/output/60724/23affcc77ef543368e03d073c8c288e0?anonymousKey=c2d647445d510d298639b2a4d0d06414cf61cd4b | +| sanity_onlyValidatedCalls_3HandleAggregatedOps211 | https://prover.certora.com/output/60724/592a3c01e5474bf496a2eafdd8a3dfe1?anonymousKey=70ce93af5d43e6768ae129c370c76f3fe2067d76 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps212 | https://prover.certora.com/output/60724/f432273a2f074339849bbdbfc66d3058?anonymousKey=a4ecf8657b8e97b8618ddb68639dd93991e2aa60 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps213 | https://prover.certora.com/output/60724/c80d2562fd6e4774a0828e6f8686ed01?anonymousKey=4905acd2d528f67d92af20e87db6aacdac1c7980 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps220 | https://prover.certora.com/output/60724/b9d3ba973f6f4416b08dd5bc837ef2e2?anonymousKey=f261fe4470862660f6a63046e1909d59fbe92642 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps221 | https://prover.certora.com/output/60724/9190dce2fe07437bba05bcc37365e555?anonymousKey=95769ad3712b0c283f5904e53a464350eebf7493 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps222 | https://prover.certora.com/output/60724/913877c0b30a423790595d96480052ba?anonymousKey=04fa7fb5fff6489c09045519c99054d4324c2445 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps223 | https://prover.certora.com/output/60724/98925043f2894e2eb0b6ec64fde65c9d?anonymousKey=50991c4542ec245c047b3d6be378a3affacb1f5d | +| sanity_onlyValidatedCalls_3HandleAggregatedOps230 | https://prover.certora.com/output/60724/5c221a3af3024ccdbdf2349d84447f40?anonymousKey=586a62ded7408ceead073359ddfc18240c8c9690 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps231 | https://prover.certora.com/output/60724/b1b30ff0e9ae4bb7a8e3dea19440f8b8?anonymousKey=daee0867f4fc0d3bc345dbfc616d0f68a958221c | +| sanity_onlyValidatedCalls_3HandleAggregatedOps232 | https://prover.certora.com/output/60724/4d64751f4c3f4fcdbd05bbb972d2bdf7?anonymousKey=c062add5fef2bd881170b232a1fab2387d83041b | +| sanity_onlyValidatedCalls_3HandleAggregatedOps233 | https://prover.certora.com/output/60724/6d459a85b06d46eebd99017edd83aff2?anonymousKey=f35db50b53172a9d3b67fcd856802514d75c67df | +| sanity_onlyValidatedCalls_3HandleAggregatedOps300 | https://prover.certora.com/output/60724/5c50bb8faf894f4cbd85f920d8b5bb72?anonymousKey=7c76afe1db9fab483fb3ef18c38169b1335f2a5e | +| sanity_onlyValidatedCalls_3HandleAggregatedOps301 | https://prover.certora.com/output/60724/7c865576bc09484bb6a39f7a83916b3e?anonymousKey=c57182e6804567fd5c26f60b5970ec35a4482175 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps302 | https://prover.certora.com/output/60724/d39f9295f34942328e383f72d30a03c5?anonymousKey=2d96d579c5b1dd9bc4bd906ae638f777e0baf7a0 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps303 | https://prover.certora.com/output/60724/d000d5bdee214358867621b5a157d0e1?anonymousKey=65497260c568f4d462a509b4c00691bba3680c3b | +| sanity_onlyValidatedCalls_3HandleAggregatedOps310 | https://prover.certora.com/output/60724/d98ed98e8122419e81169ea9bdd98e1a?anonymousKey=6c966ef651882da2b90cd2050185284160fe5299 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps311 | https://prover.certora.com/output/60724/643180c3e4874646b753c2d9b760cb7c?anonymousKey=7d07f5e7cd229d69e4b7d05cc616a8f7c63cca11 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps312 | https://prover.certora.com/output/60724/72c2e35e0fac420085d4987d34d2aaae?anonymousKey=64e93434c3bd02326b52d55838d2de39a5b60e28 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps313 | https://prover.certora.com/output/60724/e704badb6a874924844e9965325c42b9?anonymousKey=d898e2a4102c33bcb41da2a22d7e3495595e596b | +| sanity_onlyValidatedCalls_3HandleAggregatedOps320 | https://prover.certora.com/output/60724/f05a0b8a107a4a6aab6c8999e720676b?anonymousKey=32944ba6db92203788d882ee1b8c8a0b3470e81e | +| sanity_onlyValidatedCalls_3HandleAggregatedOps321 | https://prover.certora.com/output/60724/08a81a2667f04169b824048925aabbec?anonymousKey=b68dd58e60993a708e4110d9ac59ea9c290b5b0a | +| sanity_onlyValidatedCalls_3HandleAggregatedOps322 | https://prover.certora.com/output/60724/469f3ba61bae4951a66c6348a5685622?anonymousKey=003d0809bf97b8ee6e2b77604a427006a6eed414 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps323 | https://prover.certora.com/output/60724/200e59f3a0524862bd3a1c09082733df?anonymousKey=f7f57c6d1e7ecc78544b72338adc7da930018680 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps330 | https://prover.certora.com/output/60724/3610184c8a4d447f89840c00882c3097?anonymousKey=1c2168a3faaf0d2a9ade926a8175fb374c093c08 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps331 | https://prover.certora.com/output/60724/e0e04b34121140fcbc22ead7e414871d?anonymousKey=b824404517625fbe8b85eaf58b1d5e67b43a4724 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps332 | https://prover.certora.com/output/60724/947b97acc73c4f6996a24bc6c864116c?anonymousKey=018a193602d7a79cd57e7847d8be0efa4fff52e7 | +| sanity_onlyValidatedCalls_3HandleAggregatedOps333 | https://prover.certora.com/output/60724/ac3de85243984899b7484c2efce08539?anonymousKey=b075c73e6af9bdf6b848f412bdc3511316f7af0b | +| sanity_onlyValidatedCalls_2HandleAggregatedOps00 | https://prover.certora.com/output/60724/3ceb7a6e50f94553802782cf7dc6b8cc?anonymousKey=ae127caf28bf2dab31effc3a9153b9e177592b79 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps01 | https://prover.certora.com/output/60724/240c20b4a35a4bdeaea3b99dbe3e3781?anonymousKey=ce5e1d6048c9a590e869662bdb3c5392b56417d4 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps02 | https://prover.certora.com/output/60724/36962bc9678741de94f207aff967e881?anonymousKey=c07d25f79ffc121bc949f5c433e07fd8c87585e4 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps03 | https://prover.certora.com/output/60724/9a5f23d4492d4162aaf0572dde02f7a9?anonymousKey=748eb853abe091b6765a2c861a0717d19f7a85a5 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps10 | https://prover.certora.com/output/60724/28a521c2b756454a95c8d329ee94a1a5?anonymousKey=5e3ef941945fbe2e0cd61c57e78405b5a955f2d8 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps11 | https://prover.certora.com/output/60724/b452f9b1ba3b4c359eca93925f0df10a?anonymousKey=bef456b1d3208f81ed6c8c80f16f1962ee992775 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps12 | https://prover.certora.com/output/60724/60e2e0fa318146a088fabf947c5036b5?anonymousKey=73f5039671a946b9ec1a8952cdf8c7e267633fe0 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps13 | https://prover.certora.com/output/60724/777e6b601c3b4a0aafd2a1d447cda84b?anonymousKey=65c0f9dc2f29e2bbd292af8fe856f9e24e6bb325 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps20 | https://prover.certora.com/output/60724/b7198bf9de994947b0ce01b33e49a4f3?anonymousKey=85781becd95e1de72d618057127463ab762db4fe | +| sanity_onlyValidatedCalls_2HandleAggregatedOps21 | https://prover.certora.com/output/60724/7877b648fa1140a6a1d4d505e524494e?anonymousKey=e573b06f6518b621b0880ffe6d14253d4752caa1 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps22 | https://prover.certora.com/output/60724/6a9c2ddd1a35430da296028668677392?anonymousKey=0c96d419ceda754cd21fbb5d538b93ada2b4c4d2 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps23 | https://prover.certora.com/output/60724/ae0266a699fb42b69020f88285873fc1?anonymousKey=51e7075cfed2ec0a7c5adbd8848a0f05a21fb631 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps30 | https://prover.certora.com/output/60724/5a8fe7205b4949b18135560ad8fc33d8?anonymousKey=b258f487f4e594d9e78be01e517856cc47d7cacb | +| sanity_onlyValidatedCalls_2HandleAggregatedOps31 | https://prover.certora.com/output/60724/2c68fac884f24812b772e5b2ed636bf4?anonymousKey=8db294fc7cf33164fde71616ba653a4537aee560 | +| sanity_onlyValidatedCalls_2HandleAggregatedOps32 | https://prover.certora.com/output/60724/e95d2a95482a47109edd61a20fa3c757?anonymousKey=a7ead1f1c9e93a2b673706f9a0875bdd7254b98e | +| sanity_onlyValidatedCalls_2HandleAggregatedOps33 | https://prover.certora.com/output/60724/d9366bd0ba3c43b1a6c5b0d4f85f5407?anonymousKey=c275585623784a04ce4b0914cac71195f0f18e60 | +| sanity_onlyValidatedCalls_1HandleAggregatedOps0 | https://prover.certora.com/output/60724/eae4d2b90573448c8592bfe805dae5e0?anonymousKey=d760becb5921b6cdea7dc1d8634b1904c7c2b926 | +| sanity_onlyValidatedCalls_1HandleAggregatedOps1 | https://prover.certora.com/output/60724/4f9b483c717942bcb1e8dcd8bef187f1?anonymousKey=42388a9fda99b0866a0424d2a07e5a83cc79d830 | +| sanity_onlyValidatedCalls_1HandleAggregatedOps2 | https://prover.certora.com/output/60724/c2da067b5a914e13bd82bca2e3aa1b6f?anonymousKey=f0ef76620530d27045b236ecd955675a58d51aa0 | +| sanity_onlyValidatedCalls_1HandleAggregatedOps3 | https://prover.certora.com/output/60724/424aa54818f0405a9e0d2d40d2ad265c?anonymousKey=5f6b0d50097e16e4e09ad3775e949823bbf3b47e | diff --git a/certora/report/markdown.sh b/certora/report/markdown.sh new file mode 100755 index 000000000..8da8ebabc --- /dev/null +++ b/certora/report/markdown.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +# Input shell script file with certoraRun calls +input_file="certora/report/all.sh" + +# Output markdown file +output_file="certora_results.md" + +# Initialize the markdown table +echo "| Rule | URL |" > "$output_file" +echo "|------|-----|" >> "$output_file" + +# Loop through each line in the input file +while IFS= read -r line +do + # Extract the rule name (assuming it follows `--rule`) + rule=$(echo "$line" | sed -n 's/.*--rule \([^ ]*\).*/\1/p') + + # Run the command and capture output + output=$(eval "$line") + + # Extract the URL from the output + url=$(echo "$output" | sed -n 's/.*see verification results at \([^ ]*\).*/\1/p') + + # Append the rule and URL to the markdown table + if [[ -n "$rule" && -n "$url" ]]; then + echo "| $rule | $url |" >> "$output_file" + fi +done < "$input_file" + +echo "Markdown table with results has been saved to $output_file." diff --git a/certora/report/table_generator.py b/certora/report/table_generator.py new file mode 100644 index 000000000..f68000c29 --- /dev/null +++ b/certora/report/table_generator.py @@ -0,0 +1,63 @@ +import re +import requests +import pandas as pd + +# Input markdown file and output CSV file +input_file = "certora_results_sanity.md" +output_file = "certora_final_results_sanity.csv" + +# List to hold table rows +table = [] + +# Read markdown file +with open(input_file, 'r') as file: + # Skip the header + lines = file.readlines()[2:] + + for line in lines: + # Parse each row + parts = line.strip().split("|") + rule = parts[1].strip() + url = parts[2].strip() + + # Use regex to extract components + match = re.match(r'(\D+)(\d+)(\D+)(\d+)', rule) + if match: + main_string, first_number, remaining_string, last_number = match.groups() + + # Modify URL to include 'output.json' + json_url = url.split("?")[0] + "/output.json?" + url.split("?")[1] + + # Fetch and parse the JSON + try: + response = requests.get(json_url) + response.raise_for_status() + json_data = response.json() + + # Check the rules for SUCCESS status + status = "PASSED" + for rule_name, rule_data in json_data.get("rules", {}).items(): + for result, methods in rule_data.items(): + if result == "SUCCESS" and (len(methods) != 1 or not methods[0]): + status = "FAILED" + break + elif result != "SUCCESS" and methods: # Non-empty for non-SUCCESS results + status = "FAILED" + break + if status == "FAILED": + break + + except requests.RequestException as e: + print(f"Error fetching {json_url}: {e}") + status = "FAILED" + except (KeyError, ValueError) as e: + print(f"Error parsing JSON from {json_url}: {e}") + status = "FAILED" + + # Append the parsed data to the table + table.append([remaining_string, first_number, last_number, url, status]) + +# Convert to DataFrame and save as CSV +df = pd.DataFrame(table, columns=["Main String", "First Number", "Last Number", "Original URL", "Status"]) +df.to_csv(output_file, index=False) +print(f"Table saved to {output_file}") diff --git a/certora/specs/alwaysRevert.spec b/certora/specs/alwaysRevert.spec new file mode 100644 index 000000000..515c0a915 --- /dev/null +++ b/certora/specs/alwaysRevert.spec @@ -0,0 +1,13 @@ + +//// # Verifies that certain function always revert as expected */ +rule alwaysRevert(method f) +filtered { f-> + f.selector == sig:getSenderAddress(bytes).selector + || f.selector == sig:delegateAndRevert(address,bytes).selector +} +{ + env e; + calldataarg args; + f@withrevert(e,args); + assert lastReverted; +} \ No newline at end of file diff --git a/certora/specs/entryPoint.spec b/certora/specs/entryPoint.spec new file mode 100644 index 000000000..66541ae80 --- /dev/null +++ b/certora/specs/entryPoint.spec @@ -0,0 +1,472 @@ +import "./entryPointShared.spec"; + +methods { + unresolved external in _._ => DISPATCH [ + EntryPoint.innerHandleOp(bytes,EntryPoint.UserOpInfo,bytes), + ] default ASSERT_FALSE; + + function EntryPoint.getUserOpHash(EntryPoint.PackedUserOperation calldata) internal returns bytes32 => NONDET; +} + +function cvlInnerHandleOp(env e) returns uint256 { + // assert verificationAndCallGasLimit >= require_uint256(opInfo.mUserOp.callGasLimit + opInfo.mUserOp.verificationGasLimit + 5000); // we intentionally do not reason about gas + assert e.msg.sender == currentContract; + // we are not asserting callData.length > 0 even though it is required for actual execution. + // the reason is that requiring it here prohibits some critical performance imporvement. + numExecuted = numExecuted + 1; + uint toRet; + return toRet; +} + +// a rule checking cvlInnerHandleOp summary - separate spec file: `residual.spec` + + +//// # Check that every op that exec-ed on an account has been checked via the validateUserOp function +/** +* Verified by keeping track of opcodes that have been verified and executed opcodes +*/ + + +/* everything but handle*Ops functions*/ +rule onlyValidatedCalls_NonHandleOps(method f) +filtered { f -> !isHandleOps(f) } +{ + // check only entrypoint + require f.contract == entryPoint; + // delegateAndRevert should always revert anyway, filter out + require f.selector != sig:delegateAndRevert(address,bytes).selector; + // innerHandleOp is... inner! + require f.selector != sig:EntryPoint.innerHandleOp(bytes,EntryPoint.UserOpInfo,bytes).selector; + check_onlyValidatedCalls_assert(f, 100, 100, 100, 100); +} + +/* all variants of handleOps */ +rule onlyValidatedCalls_3HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_assert(f, 3, 100, 100, 100); +} + +rule onlyValidatedCalls_2HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_assert(f, 2, 100, 100, 100); +} + +rule onlyValidatedCalls_1HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_assert(f, 1, 100, 100, 100); +} + +rule onlyValidatedCalls_0HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_assert(f, 0, 100, 100, 100); +} + +/* all variants of handleAggregatedOps */ + +// 3 - (0,1,2,3) x (0,1,2,3) x (0,1,2,3) +rule onlyValidatedCalls_3HandleAggregatedOps000(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 0, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps001(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 0, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps002(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 0, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps003(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 0, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps010(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 1, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps011(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 1, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps012(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 1, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps013(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 1, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps020(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 2, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps021(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 2, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps022(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 2, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps023(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 2, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps030(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 3, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps031(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 3, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps032(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 3, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps033(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 0, 3, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps100(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 0, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps101(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 0, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps102(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 0, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps103(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 0, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps110(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 1, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps111(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 1, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps112(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 1, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps113(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 1, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps120(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 2, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps121(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 2, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps122(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 2, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps123(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 2, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps130(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 3, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps131(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 3, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps132(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 3, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps133(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 1, 3, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps200(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 0, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps201(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 0, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps202(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 0, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps203(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 0, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps210(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 1, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps211(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 1, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps212(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 1, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps213(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 1, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps220(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 2, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps221(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 2, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps222(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 2, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps223(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 2, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps230(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 3, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps231(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 3, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps232(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 3, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps233(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 2, 3, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps300(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 0, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps301(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 0, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps302(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 0, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps303(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 0, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps310(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 1, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps311(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 1, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps312(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 1, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps313(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 1, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps320(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 2, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps321(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 2, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps322(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 2, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps323(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 2, 3); } + +rule onlyValidatedCalls_3HandleAggregatedOps330(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 3, 0); } + +rule onlyValidatedCalls_3HandleAggregatedOps331(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 3, 1); } + +rule onlyValidatedCalls_3HandleAggregatedOps332(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 3, 2); } + +rule onlyValidatedCalls_3HandleAggregatedOps333(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 3, 3, 3, 3); } + + +// 2 - (0,1,2,3) x (0,1,2,3) +rule onlyValidatedCalls_2HandleAggregatedOps00(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 0, 0, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps01(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 0, 1, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps02(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 0, 2, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps03(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 0, 3, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps10(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 1, 0, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps11(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 1, 1, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps12(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 1, 2, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps13(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 1, 3, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps20(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 2, 0, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps21(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 2, 1, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps22(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 2, 2, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps23(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 2, 3, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps30(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 3, 0, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps31(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 3, 1, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps32(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 3, 2, 100); } + +rule onlyValidatedCalls_2HandleAggregatedOps33(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 2, 3, 3, 100); } + + +// 1 - 0,1,2,3 +rule onlyValidatedCalls_1HandleAggregatedOps0(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 1, 0, 100, 100); } + +rule onlyValidatedCalls_1HandleAggregatedOps1(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 1, 1, 100, 100); } + +rule onlyValidatedCalls_1HandleAggregatedOps2(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 1, 2, 100, 100); } + +rule onlyValidatedCalls_1HandleAggregatedOps3(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_assert(f, 1, 3, 100, 100); } + +rule onlyValidatedCalls_0HandleAggregatedOps(method f) +filtered { f-> + f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector +} +{ + check_onlyValidatedCalls_assert(f, 0, 100, 100, 100); +} + +function check_onlyValidatedCalls_assert(method f, uint sz, uint subsz0, uint subsz1, uint subsz2) { + env e; + calldataarg args; + numValidated = 0; + numExecuted = 0; + executionValidated = true; + + dispatchHandleOps(f, e, sz, subsz0, subsz1, subsz2); + + assert numValidated == numExecuted; + assert executionValidated; +} + + +rule innerHandleOpProtected() +{ + env e; + bytes callData; + EntryPoint.UserOpInfo opInfo; + bytes context; + require e.msg.sender != currentContract; + + innerHandleOp@withrevert(e, callData, opInfo, context); + assert lastReverted; +} + + +//// # Validity of balance decrease +/** + * Who can decrease balance of (in StakeManager) ? + */ +rule onlySelfReduces(method f, address user) { + env e; + calldataarg args; + uint256 before = balanceOf(user); + f(e, args); + uint256 after = balanceOf(user); + assert after < before => e.msg.sender == user; +} + +rule sanity(method f) { + env e; + calldataarg arg; + f(e, arg); + satisfy true; +} diff --git a/certora/specs/entryPointSanity.spec b/certora/specs/entryPointSanity.spec new file mode 100644 index 000000000..e00002394 --- /dev/null +++ b/certora/specs/entryPointSanity.spec @@ -0,0 +1,437 @@ +import "./entryPointShared.spec"; + +methods { + unresolved external in _._ => DISPATCH [ + EntryPoint.innerHandleOp(bytes,EntryPoint.UserOpInfo,bytes), + ] default HAVOC_ALL; +} + +function cvlInnerHandleOp(env e) returns uint256 { + // no assertions in sanity/satisfy, just requires + // xxx require no value is passed + // assert verificationAndCallGasLimit >= require_uint256(opInfo.mUserOp.callGasLimit + opInfo.mUserOp.verificationGasLimit + 5000); // we intentionally do not reason about gas + require e.msg.sender == currentContract; + numExecuted = numExecuted + 1; + uint toRet; + return toRet; +} + + +function check_onlyValidatedCalls_satisfy(method f, uint sz, uint subsz0, uint subsz1, uint subsz2) { + env e; + calldataarg args; + numValidated = 0; + numExecuted = 0; + executionValidated = true; + + dispatchHandleOps(f, e, sz, subsz0, subsz1, subsz2); + + require numValidated == numExecuted; + require executionValidated; + + if (isHandleOps(f) && sz > 0 + || (f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector && sz > 0 && subsz0+subsz1+subsz2 > 0) + ) { + satisfy numExecuted > 0; + } else { + assert numExecuted == 0; + } +} + +// SATISFY +/* everything but handle*Ops functions*/ +rule sanity_onlyValidatedCalls_NonHandleOps(method f) +filtered { f -> !isHandleOps(f) } +{ + // check only entrypoint + require f.contract == entryPoint; + // delegateAndRevert should always revert anyway, filter out + require f.selector != sig:delegateAndRevert(address,bytes).selector; + // innerHandleOp is... inner! + require f.selector != sig:EntryPoint.innerHandleOp(bytes,EntryPoint.UserOpInfo,bytes).selector; + check_onlyValidatedCalls_satisfy(f, 100, 100, 100, 100); +} + +/* all variants of handleOps */ +rule sanity_onlyValidatedCalls_3HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_satisfy(f, 3, 100, 100, 100); +} + +rule sanity_onlyValidatedCalls_2HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_satisfy(f, 2, 100, 100, 100); +} + +rule sanity_onlyValidatedCalls_1HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_satisfy(f, 1, 100, 100, 100); +} + +rule sanity_onlyValidatedCalls_0HandleOps(method f) +filtered { f-> + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector +} +{ + check_onlyValidatedCalls_satisfy(f, 0, 100, 100, 100); +} + +/* all variants of handleAggregatedOps */ + +// 3 - (0,1,2,3) x (0,1,2,3) x (0,1,2,3) +rule sanity_onlyValidatedCalls_3HandleAggregatedOps000(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 0, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps001(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 0, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps002(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 0, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps003(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 0, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps010(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 1, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps011(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 1, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps012(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 1, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps013(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 1, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps020(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 2, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps021(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 2, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps022(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 2, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps023(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 2, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps030(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 3, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps031(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 3, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps032(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 3, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps033(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 0, 3, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps100(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 0, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps101(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 0, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps102(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 0, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps103(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 0, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps110(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 1, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps111(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 1, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps112(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 1, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps113(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 1, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps120(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 2, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps121(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 2, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps122(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 2, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps123(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 2, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps130(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 3, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps131(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 3, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps132(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 3, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps133(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 1, 3, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps200(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 0, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps201(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 0, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps202(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 0, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps203(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 0, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps210(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 1, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps211(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 1, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps212(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 1, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps213(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 1, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps220(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 2, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps221(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 2, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps222(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 2, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps223(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 2, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps230(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 3, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps231(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 3, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps232(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 3, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps233(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 2, 3, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps300(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 0, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps301(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 0, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps302(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 0, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps303(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 0, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps310(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 1, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps311(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 1, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps312(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 1, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps313(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 1, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps320(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 2, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps321(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 2, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps322(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 2, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps323(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 2, 3); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps330(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 3, 0); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps331(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 3, 1); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps332(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 3, 2); } + +rule sanity_onlyValidatedCalls_3HandleAggregatedOps333(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 3, 3, 3, 3); } + + +// 2 - (0,1,2,3) x (0,1,2,3) +rule sanity_onlyValidatedCalls_2HandleAggregatedOps00(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 0, 0, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps01(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 0, 1, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps02(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 0, 2, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps03(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 0, 3, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps10(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 1, 0, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps11(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 1, 1, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps12(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 1, 2, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps13(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 1, 3, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps20(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 2, 0, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps21(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 2, 1, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps22(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 2, 2, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps23(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 2, 3, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps30(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 3, 0, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps31(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 3, 1, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps32(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 3, 2, 100); } + +rule sanity_onlyValidatedCalls_2HandleAggregatedOps33(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 2, 3, 3, 100); } + + +// 1 - 0,1,2,3 +rule sanity_onlyValidatedCalls_1HandleAggregatedOps0(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 1, 0, 100, 100); } + +rule sanity_onlyValidatedCalls_1HandleAggregatedOps1(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 1, 1, 100, 100); } + +rule sanity_onlyValidatedCalls_1HandleAggregatedOps2(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 1, 2, 100, 100); } + +rule sanity_onlyValidatedCalls_1HandleAggregatedOps3(method f) +filtered { f-> f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector } +{ check_onlyValidatedCalls_satisfy(f, 1, 3, 100, 100); } + +rule sanity_onlyValidatedCalls_0HandleAggregatedOps(method f) +filtered { f-> + f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector +} +{ + check_onlyValidatedCalls_satisfy(f, 0, 100, 100, 100); +} \ No newline at end of file diff --git a/certora/specs/entryPointShared.spec b/certora/specs/entryPointShared.spec new file mode 100644 index 000000000..eaf71ba30 --- /dev/null +++ b/certora/specs/entryPointShared.spec @@ -0,0 +1,125 @@ +using EntryPoint as entryPoint; + +methods { + + function Exec.call( + address to, + uint256 value, + bytes memory data, + uint256 txGas + ) internal returns (bool) => execCallSummary(to, value, data, txGas); + + function _.createSender(bytes initCode) external => NONDET; + + function _.validateUserOp( + EntryPoint.PackedUserOperation userOp, + bytes32 hash, + uint256 missingFunds + ) external => validateUserOpSummary() expect uint256; + function _.validatePaymasterUserOp( + EntryPoint.PackedUserOperation userOp, + bytes32 userOpHash, + uint256 maxCost + ) external => NONDET; + function _.validateSignatures( + EntryPoint.PackedUserOperation[] userOps, + bytes signature + ) external => NONDET; + + function balanceOf(address) external returns (uint256) envfree; + function _compensate(address beneficiary, uint256 amount) internal => NONDET; + function _createSenderIfNeeded( + uint256 opIndex, + EntryPoint.UserOpInfo memory opInfo, + bytes calldata initCode + ) internal => NONDET; + + function _.postOp( + IPaymaster.PostOpMode mode, + bytes context, + uint256 actualGasCost, + uint256 actualUserOpFeePerGas + ) external => NONDET; + + function calldataKeccak(bytes calldata data) internal returns bytes32 => keccak256(data); + + function EntryPoint.innerHandleOp( + bytes, + EntryPoint.UserOpInfo, + bytes + ) external returns uint256 with (env e) => cvlInnerHandleOp(e); + + + + // optimizations + function emitUserOperationEvent(EntryPoint.UserOpInfo memory opInfo, bool success, uint256 actualGasCost, uint256 actualGas) internal => NONDET; + function emitPrefundTooLow(EntryPoint.UserOpInfo memory opInfo) internal => NONDET; + function Exec.getReturnData(uint256) internal returns (bytes memory) => nondetBytes(); + +} + + + +persistent ghost mathint numValidated; +persistent ghost mathint numExecuted; +persistent ghost bool executionValidated; +persistent ghost mapping(mathint => bytes32) validatedUserOpHash; + +function nondetBytes() returns bytes { + bytes b; + return b; +} + +function validateUserOpSummary() returns uint256 { + numValidated = numValidated + 1; + uint256 validationData; + return validationData; +} + +function execCallSummary(address to, uint256 value, bytes data, uint256 txGas) returns bool { + if (numExecuted >= numValidated || + validatedUserOpHash[numExecuted] != keccak256(data)) { + executionValidated = false; // any reason not to assert here? XXX + } + numExecuted = numExecuted + 1; + bool result; + return result; +} + + +function limitPerAggregatorOps(IEntryPoint.UserOpsPerAggregator[] op, uint idx, uint subsz) { + require op[idx].userOps.length == subsz; +} + +function dispatchHandleOps(method f, env e, uint sz, uint subsz0, uint subsz1, uint subsz2) { + if (f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector) { + EntryPoint.PackedUserOperation[] ops; + assert sz <= 3, "We prove up to size 3"; + require ops.length == sz; + address beneficiary; + handleOps(e,ops,beneficiary); + } else if (f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector) { + IEntryPoint.UserOpsPerAggregator[] ops; + assert sz <= 3, "We prove up to size 3"; + require ops.length == sz; + if (ops.length >= 1) { + limitPerAggregatorOps(ops, 0, subsz0); + if (ops.length >= 2) { + limitPerAggregatorOps(ops, 1, subsz1); + if (ops.length >= 3) { + limitPerAggregatorOps(ops, 2, subsz2); + } + } + } + address beneficiary; + handleAggregatedOps(e,ops,beneficiary); + } else { + // xx add handle aggregated ops + calldataarg args; + f(e, args); + } +} + +definition isHandleOps(method f) returns bool = + f.selector == sig:handleOps(EntryPoint.PackedUserOperation[],address).selector + || f.selector == sig:handleAggregatedOps(IEntryPoint.UserOpsPerAggregator[],address).selector; diff --git a/certora/specs/residual.spec b/certora/specs/residual.spec new file mode 100644 index 000000000..ffd7abd20 --- /dev/null +++ b/certora/specs/residual.spec @@ -0,0 +1,49 @@ +import "./entryPointShared.spec"; + +persistent ghost mathint prevNumExecuted; + +persistent ghost mathint minimalGas; + +persistent ghost bool inputCalldataLengthIsZero; + +hook GAS uint g { + if (numExecuted == prevNumExecuted) { + require g < 2^250; // sane bound to avoid overflow + // did not execute yet, assume there was enough gas + require g*63/64 >= minimalGas; + } +} + +hook REVERT(uint offset, uint size) { + // let's require enough gas + assert numExecuted == prevNumExecuted + 1 || inputCalldataLengthIsZero; +} + +function cvlInnerHandleOp(env e) returns uint256 { + // not supposed to be summarized in residual + assert false; + uint toRet; + return toRet; +} + +rule checkInnerHandleOp() { + prevNumExecuted = numExecuted; + + env e; + bytes callData; + inputCalldataLengthIsZero = callData.length == 0; + EntryPoint.UserOpInfo opInfo; + bytes context; + minimalGas = opInfo.mUserOp.callGasLimit + opInfo.mUserOp.paymasterPostOpGasLimit + 10000 /* Inner gas overhead */; + + require e.msg.value == 0; + require e.msg.sender == entryPoint; + + innerHandleOp@withrevert(e, callData, opInfo, context); + bool reverted = lastReverted; + assert reverted || numExecuted == prevNumExecuted + 1 || inputCalldataLengthIsZero; + // use independent satisfies + satisfy reverted; + satisfy numExecuted == prevNumExecuted + 1; + satisfy inputCalldataLengthIsZero; +} \ No newline at end of file