def BE : ℕ → ByteArray

Equations

• BE = List.toByteArray ∘ EvmYul.toBytesBigEndian

def EvmYul.chainId : ℕ

Equations

• EvmYul.chainId = 1

def EvmYul.UInt256.toByteArray (val : UInt256) : ByteArray

Equations

• val.toByteArray = ffi.ByteArray.zeroes { toBitVec := 32 - ↑(BE val.toNat).size } ++ BE val.toNat

@[reducible, inline]

abbrev EvmYul.Literal : Type

Equations

• EvmYul.Literal = EvmYul.UInt256

def EvmYul.AccountAddress.size : ℕ

Equations

• EvmYul.AccountAddress.size = 1461501637330902918203684832716283019655932542976

@[reducible, inline]

abbrev EvmYul.AccountAddress : Type

Equations

• EvmYul.AccountAddress = Fin EvmYul.AccountAddress.size

instance EvmYul.instOrdAccountAddress : Ord AccountAddress

Equations

• EvmYul.instOrdAccountAddress = { compare := fun (a₁ a₂ : EvmYul.AccountAddress) => compare ↑a₁ ↑a₂ }

instance EvmYul.instInhabitedAccountAddress : Inhabited AccountAddress

Equations

• EvmYul.instInhabitedAccountAddress = { default := Fin.ofNat 0 }

def EvmYul.AccountAddress.ofNat (n : ℕ) : AccountAddress

Equations

• EvmYul.AccountAddress.ofNat n = Fin.ofNat n

def EvmYul.AccountAddress.ofUInt256 (v : UInt256) : AccountAddress

Equations

• EvmYul.AccountAddress.ofUInt256 v = Fin.ofNat (↑v.val % EvmYul.AccountAddress.size)

instance EvmYul.AccountAddress.instOfNat {n : ℕ} : OfNat AccountAddress n

Equations

• EvmYul.AccountAddress.instOfNat = { ofNat := Fin.ofNat n }

def EvmYul.AccountAddress.toByteArray (a : AccountAddress) : ByteArray

Equations

• a.toByteArray = ffi.ByteArray.zeroes { toBitVec := 20 - ↑(BE ↑a).size } ++ BE ↑a

def EvmYul.hexOfByte (byte : UInt8) : String

Equations

• EvmYul.hexOfByte byte = hexDigitRepr (byte.toNat >>> 4 &&& 15) ++ hexDigitRepr (byte.toNat &&& 15)

def EvmYul.toHex (bytes : ByteArray) : String

Equations

• EvmYul.toHex bytes = ByteArray.foldl (fun (acc : String) (byte : UInt8) => acc ++ EvmYul.hexOfByte byte) "" bytes

instance EvmYul.instReprByteArray_evmYul : Repr ByteArray

Equations

• EvmYul.instReprByteArray_evmYul = { reprPrec := fun (s : ByteArray) (x : ℕ) => Std.Format.text (EvmYul.toHex s) }

def EvmYul.Identifier : Type

Equations

• EvmYul.Identifier = String

instance EvmYul.instToStringIdentifier : ToString Identifier

Equations

• EvmYul.instToStringIdentifier = inferInstanceAs (ToString String)

instance EvmYul.instInhabitedIdentifier : Inhabited Identifier

Equations

• EvmYul.instInhabitedIdentifier = inferInstanceAs (Inhabited String)

instance EvmYul.instDecidableEqIdentifier : DecidableEq Identifier

Equations

• EvmYul.instDecidableEqIdentifier = inferInstanceAs (DecidableEq String)

instance EvmYul.instReprIdentifier : Repr Identifier

Equations

• EvmYul.instReprIdentifier = inferInstanceAs (Repr String)

def EvmYul.NaryNotation.«term!nary[_^_]» : Lean.ParserDescr

Equations

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

def EvmYul.Primop.Nullary : Type

Equations

• EvmYul.Primop.Nullary = EvmYul.UInt256

def EvmYul.Primop.Unary : Type

Equations

• EvmYul.Primop.Unary = (EvmYul.UInt256 → EvmYul.UInt256)

def EvmYul.Primop.Binary : Type

Equations

• EvmYul.Primop.Binary = (EvmYul.UInt256 → EvmYul.UInt256 → EvmYul.UInt256)

def EvmYul.Primop.Ternary : Type

Equations

• EvmYul.Primop.Ternary = (EvmYul.UInt256 → EvmYul.UInt256 → EvmYul.UInt256 → EvmYul.UInt256)

def EvmYul.Primop.Quaternary : Type

Equations

• EvmYul.Primop.Quaternary = (EvmYul.UInt256 → EvmYul.UInt256 → EvmYul.UInt256 → EvmYul.UInt256 → EvmYul.UInt256)

instance instDecidableEqByteArray_evmYul : DecidableEq ByteArray

TODO(rework later to a sane version)

Equations

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

def Option.option {α β : Type} (dflt : β) (f : α → β) : Option α → β

Equations

• Option.option dflt f none = dflt
• Option.option dflt f (some x_1) = f x_1

def Option.toExceptWith {α β : Type} (dflt : β) (x : Option α) : Except β α

Equations

• Option.toExceptWith dflt x = Option.option (Except.error dflt) Except.ok x

def ByteArray.get? (self : ByteArray) (n : ℕ) : Option UInt8

Equations

• self.get? n = if h : n < self.size then some (self.get n h) else none

partial def Nat.toHex (n : ℕ) : String

def hexOfByte (byte : UInt8) : String

Equations

• hexOfByte byte = hexDigitRepr (byte.toNat >>> 4 &&& 15) ++ hexDigitRepr (byte.toNat &&& 15)

def toHex (bytes : ByteArray) : String

Equations

• toHex bytes = ByteArray.foldl (fun (acc : String) (byte : UInt8) => acc ++ hexOfByte byte) "" bytes

def padLeft (n : ℕ) (s : String) : String

Add 0s to make the hex representation valid for ByteArray.ofBlob

Equations

• padLeft n s = if s.length < n then String.replicate (n - s.length) '0' ++ s else s

def ByteArray.extract' (a : ByteArray) (b e : ℕ) : ByteArray

TODO - Well this is ever so slightly unfortunate. It appears to be the case that some (all?) definitions that have C++ implementations use 64bit-width integers to hold numeric arguments.

When this assumption is broken, e.g. n : Nat := 2^64, the Lean (4.9.0) gives inernal out of memory error.

This implementation works around the issue at the price of using a slower implementation in case either of the arguments is too big.

Equations

• a.extract' b e = if (decide (b < 2 ^ 64) && decide (e < 2 ^ 64)) = true then a.extract b e else { data := { toList := List.take (e - b) (List.drop b a.toList) } }

def HexPrefix : String

Equations

• HexPrefix = "0x"

def TargetSchedule : String

Equations

• TargetSchedule = "Cancun"

def isHexDigitChar (c : Char) : Bool

Equations

• isHexDigitChar c = (decide ('0' ≤ c) && decide (c ≤ '9') || decide ('a' ≤ c.toLower) && decide (c.toLower ≤ 'f'))

def cToHex? (c : Char) : Except String ℕ

Equations

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

def ofHex? : List Char → Except String UInt8

Equations

• ofHex? [] = pure 0
• ofHex? [msb, lsb] = do let __do_lift ← cToHex? msb let __do_lift_1 ← cToHex? lsb (pure ∘ UInt8.ofNat) (__do_lift * 16 + __do_lift_1)
• ofHex? x✝ = throw "Need two hex digits for every byte."

def Blob : Type

Equations

• Blob = String

instance instInhabitedBlob : Inhabited Blob

Equations

• instInhabitedBlob = inferInstanceAs (Inhabited String)

def Blob.toString : Blob → String

Equations

• blob.toString = blob

instance instToStringBlob : ToString Blob

Equations

• instToStringBlob = { toString := Blob.toString }

def getBlob? (s : String) : Except String Blob

Equations

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

def getBlob?.isHex (s : String) : Bool

Equations

• getBlob?.isHex s = s.startsWith HexPrefix

def getBlob! (s : String) : Blob

Equations

• getBlob! s = (getBlob? s).toOption.get!

def ByteArray.ofBlob (self : Blob) : Except String ByteArray

Equations

• ByteArray.ofBlob self = do let chunks ← mapM ofHex? (List.toChunks 2 (String.toList self)) pure { data := chunks.toArray }

def ByteArray.readBytes (source : ByteArray) (start size : ℕ) : ByteArray

Equations

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

def ByteArray.readWithoutPadding (source : ByteArray) (addr len : ℕ) : ByteArray

Equations

• source.readWithoutPadding addr len = if addr ≥ source.size then ByteArray.empty else let len := len ⊓ source.size; source.extract addr (addr + len)

def ByteArray.readWithPadding (source : ByteArray) (addr len : ℕ) : ByteArray

Equations

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

inductive 𝕋 : Type

• 𝔹 : ByteArray → 𝕋
• 𝕃 : List 𝕋 → 𝕋

instance instRepr𝕋 : Repr 𝕋

Equations

• instRepr𝕋 = { reprPrec := repr𝕋✝ }

instance instBEq𝕋 : BEq 𝕋

Equations

• instBEq𝕋 = { beq := beq𝕋✝ }

def lengthRLP (rlp : ByteArray) : Option ℕ

Equations

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

partial def separateListRLP (rlp : ByteArray) : Option (List ByteArray)

def oneStepRLP (rlp : ByteArray) : Option (ByteArray ⊕ List ByteArray)

Equations

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

partial def deserializeRLP (rlp : ByteArray) : Option 𝕋

@[irreducible]

def R_l (l : List 𝕋) : Option ByteArray

Equations

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

@[irreducible]

def RLP (t : 𝕋) : Option ByteArray

Equations

• RLP (𝕋.𝔹 a) = R_b✝ a
• RLP (𝕋.𝕃 a) = R_l a

def myByteArray : ByteArray

Equations

• myByteArray = { data := #[1, 2, 3] }

def ByteArray.write (source : ByteArray) (sourceAddr : ℕ) (dest : ByteArray) (destAddr len : ℕ) : ByteArray

Equations

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