From a8140a146b00f6ad0fd9487dd2814aabd3f13240 Mon Sep 17 00:00:00 2001 From: Daniel Britten Date: Mon, 2 Dec 2024 05:47:52 +0000 Subject: [PATCH] Add `hash_collision` condition to specs --- Generated/erc20shim/ERC20Shim/fun__transfer_user.lean | 2 +- Generated/erc20shim/ERC20Shim/fun_spendAllowance_user.lean | 2 +- Generated/erc20shim/ERC20Shim/fun_transferFrom_user.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean b/Generated/erc20shim/ERC20Shim/fun__transfer_user.lean index d0b2252..83a942e 100644 --- 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 index 5b059dc..55a44ee 100644 --- 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 index b684a73..bdee7b9 100644 --- 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