From 3b78768f605c0d4cb3f38b5b407799e1c58c4c69 Mon Sep 17 00:00:00 2001 From: Andrei Burdusa Date: Thu, 29 Aug 2024 12:50:14 +0300 Subject: [PATCH 1/2] Erase default values from storage --- Clear/EVMState.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index 96f1092..a5b977d 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -65,7 +65,10 @@ def Account.lookupStorage (act : Account) (k : UInt256) : UInt256 := | _ => 0 def Account.updateStorage (act : Account) (k v : UInt256) : Account := - {act with storage := Finmap.insert k v act.storage} + if v == default then + { act with storage := act.storage.erase k } + else + { act with storage := Finmap.insert k v act.storage} -- definition of the machine state From 178504e776cb01f9b4801b52e65d498ca5b1170f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Mon, 7 Oct 2024 13:15:55 +0200 Subject: [PATCH 2/2] Don't use default for numbers/values --- Clear/EVMState.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Clear/EVMState.lean b/Clear/EVMState.lean index a5b977d..62a403f 100644 --- a/Clear/EVMState.lean +++ b/Clear/EVMState.lean @@ -65,7 +65,7 @@ def Account.lookupStorage (act : Account) (k : UInt256) : UInt256 := | _ => 0 def Account.updateStorage (act : Account) (k v : UInt256) : Account := - if v == default then + if v == 0 then { act with storage := act.storage.erase k } else { act with storage := Finmap.insert k v act.storage}