Add hash_collision condition to specs

NethermindEth · Dec 2, 2024 · a8140a1 · a8140a1
1 parent 015a295
commit a8140a1
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean b/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean
@@ -40,7 +40,7 @@ def A_fun__transfer  (var_from var_to var_value : Literal) (s₀ s₉ : State) :
     ∨
     -- Case: _transfer fails
     (
-      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧
+      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧ s₉.evm.hash_collision = false ∧
       (from_addr = 0 ∨ to_addr = 0)
     )
     -- Case: Hash collision

diff --git a/Generated/erc20shim/ERC20Shim/fun_spendAllowance_user.lean b/Generated/erc20shim/ERC20Shim/fun_spendAllowance_user.lean
@@ -35,7 +35,7 @@ def A_fun_spendAllowance  (var_owner var_spender var_value : Literal) (s₀ s₉
     ∨
     -- Case: spendAllowance fails
     (
-      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧
+      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧ s₉.evm.hash_collision = false ∧
       currentAllowance < transfer_value
     )
     -- Case: Hash collision

diff --git a/Generated/erc20shim/ERC20Shim/fun_transferFrom_user.lean b/Generated/erc20shim/ERC20Shim/fun_transferFrom_user.lean
@@ -47,7 +47,7 @@ def A_fun_transferFrom (var : Identifier) (var_from var_to var_value : Literal)
     ∨
     -- Case: transferFrom fails
     (
-      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧
+      IsERC20 erc20 s₉ ∧ preservesEvm s₀ s₉ ∧ s₉.evm.hash_collision = false ∧
       s₉[var]!! = 0
     )
     -- Case: Hash collision