def Ξ_ECREC (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_SHA256 (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_RIP160 (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_ID (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def nat_of_slice (B : ByteArray) (start width : ℕ) : ℕ

Equations

• nat_of_slice B start width = EvmYul.fromByteArrayBigEndian (B.readWithoutPadding start width) <<< (8 * (width - (B.readWithoutPadding start width).size))

@[irreducible]

def expModAux (m a c : ℕ) : ℕ → ℕ

Equations

• expModAux m a c 0 = a % m
• expModAux m a c k.succ = if (k.succ % 2 == 1) = true then expModAux m (a * c % m) (c * c % m) (k.succ / 2) else expModAux m (a % m) (c * c % m) (k.succ / 2)

def expMod (m : ℕ) (b : EvmYul.UInt256) (n : ℕ) : ℕ

Equations

• expMod m b n = expModAux m 1 b.toNat n

def Ξ_EXPMOD (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_BN_ADD (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_BN_MUL (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_SNARKV (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_BLAKE2_F (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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

def Ξ_PointEval (σ : EvmYul.AccountMap) (g : EvmYul.UInt256) (A : EvmYul.Substate) (I : EvmYul.ExecutionEnv) : Bool × EvmYul.AccountMap × EvmYul.UInt256 × EvmYul.Substate × ByteArray

Equations

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