@[reducible, inline]

abbrev EvmYul.Storage : Type

Equations

• EvmYul.Storage = Batteries.RBMap EvmYul.UInt256 EvmYul.UInt256 compare

def EvmYul.Storage.toFinmap (self : Storage) : Finmap fun (x : UInt256) => UInt256

Equations

• One or more equations did not get rendered due to their size.

def EvmYul.Storage.toEvmYulStorage (self : Storage) : Storage

Equations

• self.toEvmYulStorage = Batteries.RBMap.foldl (fun (acc : EvmYul.Storage) (k v : EvmYul.UInt256) => Batteries.RBMap.insert acc (EvmYul.UInt256.ofNat ↑k.val) v) ∅ self

def EvmYul.toBlobs (pair : UInt256 × UInt256) : Option (String × String)

Equations

• EvmYul.toBlobs pair = do let rlp ← RLP (𝕋.𝔹 (BE pair.2.toNat)) pure (EvmYul.toHex (ffi.KEC pair.1.toByteArray), EvmYul.toHex rlp)

def EvmYul.computeTrieRoot (storage : Storage) : Option ByteArray

Equations

• EvmYul.computeTrieRoot storage = match Array.mapM EvmYul.toBlobs (↑storage).toArray with | none => none | some pairs => (ByteArray.ofBlob (blobComputeTrieRoot pairs)).toOption