def EvmYul.Substate.storageKeysCmp (sk₁ sk₂ : AccountAddress × UInt256) : Ordering

Not important for reasoning about Substate, this is currently done to get some nice performance properties of the Batteries.RBMap.

TODO - to reason about the model, we will be better off with Finset or some such - without the requirement of ordering.

The current goal is to make sure that the model is executable and conformance-testable before we make it easy to reason about.

Equations

• EvmYul.Substate.storageKeysCmp sk₁ sk₂ = compare sk₁ sk₂

structure EvmYul.LogEntry : Type

• address : AccountAddress
• topics : Array UInt256
• data : ByteArray

instance EvmYul.instBEqLogEntry : BEq LogEntry

Equations

• EvmYul.instBEqLogEntry = { beq := EvmYul.beqLogEntry✝ }

instance EvmYul.instInhabitedLogEntry : Inhabited LogEntry

Equations

• EvmYul.instInhabitedLogEntry = { default := { address := default, topics := default, data := default } }

instance EvmYul.instReprLogEntry : Repr LogEntry

Equations

• EvmYul.instReprLogEntry = { reprPrec := EvmYul.reprLogEntry✝ }

def EvmYul.LogEntry.to𝕋 : LogEntry → 𝕋

Equations

• { address := address, topics := topics, data := data }.to𝕋 = 𝕋.𝕃 [𝕋.𝔹 address.toByteArray, 𝕋.𝕃 (List.map (𝕋.𝔹 ∘ EvmYul.UInt256.toByteArray) topics.toList), 𝕋.𝔹 data]

@[reducible, inline]

abbrev EvmYul.LogSeries : Type

Equations

• EvmYul.LogSeries = Array EvmYul.LogEntry

def EvmYul.LogSeries.to𝕋 (logSeries : LogSeries) : 𝕋

Equations

• logSeries.to𝕋 = 𝕋.𝕃 (List.map EvmYul.LogEntry.to𝕋 logSeries.toList)

structure EvmYul.Substate : Type

The Substate A. Section 6.1.

• selfDestructSet Aₛ
• touchedAccounts Aₜ
• refundBalance Aᵣ
• accessedAccounts Aₐ
• accessedStorageKey Aₖ
• logSeries Aₗ

• selfDestructSet : Batteries.RBSet AccountAddress compare
• touchedAccounts : Batteries.RBSet AccountAddress compare
• refundBalance : UInt256
• accessedAccounts : Batteries.RBSet AccountAddress compare
• accessedStorageKeys : Batteries.RBSet (AccountAddress × UInt256) storageKeysCmp
• logSeries : LogSeries

instance EvmYul.instBEqSubstate : BEq Substate

Equations

• EvmYul.instBEqSubstate = { beq := EvmYul.beqSubstate✝ }

instance EvmYul.instInhabitedSubstate : Inhabited Substate

Equations

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

instance EvmYul.instReprSubstate : Repr Substate

Equations

• EvmYul.instReprSubstate = { reprPrec := EvmYul.reprSubstate✝ }

def EvmYul.A0 : Substate

(63) A0 ≡ (∅, (), ∅, 0, π, ∅)

Equations

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

def EvmYul.bloomFilter (a : Array ByteArray) : ByteArray

Equations

• EvmYul.bloomFilter a = Array.foldl EvmYul.bloomFilter.set3Bits (ffi.ByteArray.zeroes 256) a

def EvmYul.bloomFilter.setBit (bytes256 : ByteArray) (bitIndex : ℕ) : ByteArray

Equations

• EvmYul.bloomFilter.setBit bytes256 bitIndex = bytes256.set! (255 - bitIndex / 8) (bytes256[255 - bitIndex / 8]! ||| UInt8.ofNat (1 <<< (bitIndex % 8)))

def EvmYul.bloomFilter.bitIndices (x : ByteArray) : List ℕ

Equations

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

def EvmYul.bloomFilter.set3Bits (acc b : ByteArray) : ByteArray

Equations

• EvmYul.bloomFilter.set3Bits acc b = List.foldl EvmYul.bloomFilter.setBit acc (EvmYul.bloomFilter.bitIndices b)

def EvmYul.Substate.joinLogs (substate : Substate) : Array ByteArray

Equations

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