From e9f9951485c5588bb17cfe6390407f1bf6079e23 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Thu, 22 Aug 2024 16:18:03 +0200
Subject: [PATCH] Verify helper for accessing dynamic arrays

---
 ...pping_address_uint256_of_address_user.lean | 36 +++++++++++++++++--
 1 file changed, 33 insertions(+), 3 deletions(-)

diff --git a/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean b/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean
index d5574bc..9527d18 100644
--- a/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean
+++ b/Generated/erc20shim/ERC20Shim/mapping_index_access_mapping_address_uint256_of_address_user.lean
@@ -10,13 +10,43 @@ section
 
 open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities 
 
-def A_mapping_index_access_mapping_address_uint256_of_address (dataSlot : Identifier) (slot key : Literal) (s₀ s₉ : State) : Prop := sorry
+def A_mapping_index_access_mapping_address_uint256_of_address (dataSlot : Identifier) (slot key : Literal) (s₀ s₉ : State) : Prop :=
+  let s₁ := s₀ 🇪⟦ s₀.evm.mstore 0x00 (Address.ofUInt256 key) ⟧
+  let s₂ := s₁ 🇪⟦ s₁.evm.mstore 0x20 slot ⟧
+  match s₂.evm.keccak256 0x00 0x40 with
+  | some ⟨addr, evm⟩ => s₉ = s₂ 🇪⟦ evm ⟧⟦ dataSlot ↦ addr ⟧
+  | none => s₉.evm.hash_collision = True
+
+-- Helper reifications
+lemma shift_eq_size : Fin.shiftLeft (n := UInt256.size) 1 160 = Address.size := by
+  constructor
+
+lemma EVMAddrSize' {s : State} : (s, [Fin.shiftLeft 1 160]) = (s, [Address.size.toUInt256]) := by
+  simp
+  exact shift_eq_size
 
 lemma mapping_index_access_mapping_address_uint256_of_address_abs_of_concrete {s₀ s₉ : State} {dataSlot slot key} :
   Spec (mapping_index_access_mapping_address_uint256_of_address_concrete_of_code.1 dataSlot slot key) s₀ s₉ →
   Spec (A_mapping_index_access_mapping_address_uint256_of_address dataSlot slot key) s₀ s₉ := by
-  unfold mapping_index_access_mapping_address_uint256_of_address_concrete_of_code A_mapping_index_access_mapping_address_uint256_of_address
-  sorry
+  unfold mapping_index_access_mapping_address_uint256_of_address_concrete_of_code A_mapping_index_access_mapping_address_uint256_of_address  
+  rcases s₀ with ⟨evm, varstore⟩ | _ | _ <;> [simp only; aesop_spec; aesop_spec]
+  apply spec_eq
+  clr_funargs
+
+  rw [ EVMSub', EVMShl', EVMAddrSize' ]; simp
+  rw [ Address.and_size_eq_ofUInt256 ]
+  rw [ multifill_cons, multifill_nil ]
+  simp
+
+  clr_varstore
+
+  generalize prep_def : (mstore evm 0 ↑↑(Address.ofUInt256 key)).mstore 32 slot = state_prep
+
+  cases state_prep.keccak256 0 64
+  · aesop_spec
+  · simp
+    unfold setEvm State.insert
+    aesop_spec
 
 end