Skip to content

Commit 1a0d70c

Browse files
Mikhail Mikheevmmv08
authored andcommitted
fix munged patch
1 parent 930478f commit 1a0d70c

File tree

3 files changed

+25
-22
lines changed

3 files changed

+25
-22
lines changed

.github/workflows/certora.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,8 @@ jobs:
2525
uses: actions/setup-java@v3
2626
with: { java-version: "17", java-package: jre, distribution: semeru }
2727

28-
- name: Install certora cli-beta
29-
run: pip install -Iv certora-cli-beta==4.2.0
28+
- name: Install certora cli
29+
run: pip install -Iv certora-cli
3030

3131
- name: Install solc
3232
run: |

certora/applyHarness.patch

Lines changed: 22 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,32 @@
1-
diff -druN Safe.sol Safe.sol
2-
--- Safe.sol 2023-05-16 15:08:39
3-
+++ Safe.sol 2023-05-25 16:23:56
4-
@@ -76,7 +76,7 @@
5-
* so we create a Safe with 0 owners and threshold 1.
6-
* This is an unusable Safe, perfect for the singleton
7-
*/
8-
- threshold = 1;
9-
+ // threshold = 1; MUNGED: remove and add to constructor of the harness
10-
}
11-
12-
/**
131
diff -druN base/Executor.sol base/Executor.sol
14-
--- base/Executor.sol 2023-05-16 15:08:39
15-
+++ base/Executor.sol 2023-05-25 16:23:31
16-
@@ -25,11 +25,9 @@
17-
Enum.Operation operation,
2+
--- base/Executor.sol 2023-06-22 14:42:39.769357540 +0200
3+
+++ base/Executor.sol 2023-06-22 15:34:09.211725615 +0200
4+
@@ -26,11 +26,13 @@
185
uint256 txGas
196
) internal returns (bool success) {
20-
+ // MUNGED lets just be a bit more optimistic, `execute` does nothing for `DELEGATECALL` and always returns true
217
if (operation == Enum.Operation.DelegateCall) {
22-
- // solhint-disable-next-line no-inline-assembly
8+
+ // MUNGED lets just be a bit more optimistic, `execute` does nothing for `DELEGATECALL` and always returns true
9+
// solhint-disable-next-line no-inline-assembly
10+
/// @solidity memory-safe-assembly
2311
- assembly {
2412
- success := delegatecall(txGas, to, add(data, 0x20), mload(data), 0, 0)
2513
- }
14+
+ // assembly {
15+
+ // success := delegatecall(txGas, to, add(data, 0x20), mload(data), 0, 0)
16+
+ // }
2617
+ return true;
2718
} else {
2819
// solhint-disable-next-line no-inline-assembly
29-
assembly {
20+
/// @solidity memory-safe-assembly
21+
diff -druN Safe.sol Safe.sol
22+
--- Safe.sol 2023-06-22 14:43:53.738861263 +0200
23+
+++ Safe.sol 2023-06-22 15:28:00.436277677 +0200
24+
@@ -76,7 +76,7 @@
25+
* so we create a Safe with 0 owners and threshold 1.
26+
* This is an unusable Safe, perfect for the singleton
27+
*/
28+
- threshold = 1;
29+
+ // threshold = 1; MUNGED: remove and add to constructor of the harness
30+
}
31+
32+
/**

certora/scripts/verifySafe.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ certoraRun certora/harnesses/SafeHarness.sol \
1010
--verify SafeHarness:certora/specs/Safe.spec \
1111
--solc solc7.6 \
1212
--optimistic_loop \
13-
--prover_args "-optimisticFallback true" \
13+
--settings -optimisticFallback=true \
1414
--loop_iter 3 \
1515
--optimistic_hashing \
1616
--hashing_length_bound 352 \

0 commit comments

Comments
 (0)