def EvmYul.writeBytes (source : ByteArray) (sourceAddr : ℕ) (self : MachineState) (destAddr len : ℕ) : MachineState

Equations

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

def EvmYul.MachineState.M (s f l : ℕ) : ℕ

Equations

• EvmYul.MachineState.M s f 0 = s
• EvmYul.MachineState.M s f l = s ⊔ (f + l + 31) / 32

def EvmYul.MachineState.x : ByteArray

Equations

• EvmYul.MachineState.x = "hello".toUTF8

def EvmYul.MachineState.y : ByteArray

Equations

• EvmYul.MachineState.y = "kokusho".toUTF8

def EvmYul.MachineState.writeWord (self : MachineState) (addr val : UInt256) : MachineState

Equations

• self.writeWord addr val = EvmYul.writeBytes val.toByteArray 0 self addr.toNat 32

def EvmYul.MachineState.lookupMemory (self : MachineState) (addr : UInt256) : UInt256

Equations

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

def EvmYul.MachineState.msize (self : MachineState) : UInt256

Equations

• self.msize = self.activeWords * { val := 32 }

def EvmYul.MachineState.mload (self : MachineState) (spos : UInt256) : UInt256 × MachineState

Equations

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

def EvmYul.MachineState.mstore (self : MachineState) (spos sval : UInt256) : MachineState

Equations

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

def EvmYul.MachineState.mstore8 (self : MachineState) (spos sval : UInt256) : MachineState

Equations

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

def EvmYul.MachineState.mcopy (self : MachineState) (writeStart readStart s : UInt256) : MachineState

Equations

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

def EvmYul.MachineState.gas (self : MachineState) : UInt256

Equations

• self.gas = self.gasAvailable

def EvmYul.MachineState.setReturnData (self : MachineState) (r : ByteArray) : MachineState

Equations

• self.setReturnData r = { gasAvailable := self.gasAvailable, activeWords := self.activeWords, memory := self.memory, returnData := r, H_return := self.H_return }

def EvmYul.MachineState.setHReturn (self : MachineState) (r : ByteArray) : MachineState

Equations

• self.setHReturn r = { gasAvailable := self.gasAvailable, activeWords := self.activeWords, memory := self.memory, returnData := self.returnData, H_return := r }

def EvmYul.MachineState.returndatasize (self : MachineState) : UInt256

Equations

• self.returndatasize = EvmYul.UInt256.ofNat self.returnData.size

def EvmYul.MachineState.returndataat (self : MachineState) (pos : UInt256) : UInt8

Equations

• self.returndataat pos = self.returnData.data.getD pos.toNat 0

def EvmYul.MachineState.returndatacopy (self : MachineState) (mstart rstart size : UInt256) : MachineState

Equations

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

def EvmYul.MachineState.evmReturn (self : MachineState) (mstart s : UInt256) : MachineState

Equations

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

def EvmYul.MachineState.evmRevert (self : MachineState) (mstart s : UInt256) : MachineState

Equations

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

def EvmYul.MachineState.keccak256 (self : MachineState) (mstart s : UInt256) : UInt256 × MachineState

Equations

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

def EvmYul.MachineState.mkNewWithGas (gas : ℕ) : MachineState

Equations

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