theorem USize.toNat_ofNat_le (n : ℕ) : toNat (OfNat.ofNat n) ≤ n

theorem USize.toNat_ofNat_eq (n : ℕ) (n_small : n < UInt32.size) : toNat (OfNat.ofNat n) = n

@[irreducible]

def toBytes'_ax : ℕ → List UInt8

Equations

• toBytes'_ax 0 = []
• toBytes'_ax n'.succ = { toBitVec := { toFin := ⟨n'.succ.mod UInt8.size, ⋯⟩ } } :: toBytes'_ax (n'.succ / UInt8.size)

theorem toBytes'_le {k n : ℕ} (h : n < 2 ^ (8 * k)) : (toBytes'_ax n).length ≤ k

theorem toBytes'_UInt256_le {n : ℕ} (h : n < EvmYul.UInt256.size) : (toBytes'_ax n).length ≤ 32

axiom Axioms.ffi_zeroes (len : USize) : ffi.ByteArray.zeroes len = { data := (List.replicate len.toNat 0).toArray }

This should either be provable at some point or a reasonable assumption

axiom Axioms.toBytesBigEndian_rw (n : ℕ) : EvmYul.toBytesBigEndian n = (List.reverse ∘ toBytes'_ax) n

Needed to bypass private attribute of toBytes'

theorem ffi_zeroes_size (len : USize) : (ffi.ByteArray.zeroes len).size = len.toNat

theorem toBytesBigEndian_lenght_le (n : ℕ) (n_small : n < EvmYul.UInt256.size) : (EvmYul.toBytesBigEndian n).length ≤ 32

theorem BE_zero : BE 0 = ByteArray.empty

theorem BE_size_le_32 (n : ℕ) (h : n < EvmYul.UInt256.size) : (BE n).size ≤ 32

theorem zeroes_size_eq_sub {n : ℕ} (n_small : n < EvmYul.UInt256.size) : (2 ^ System.Platform.numBits - (BE n).size % 2 ^ System.Platform.numBits + 32) % 2 ^ System.Platform.numBits = 32 - (BE n).size

theorem zeroes_size_eq_32 {n : ℕ} (n_small : n < EvmYul.UInt256.size) : (2 ^ System.Platform.numBits - (BE n).size % 2 ^ System.Platform.numBits + 32) % 2 ^ System.Platform.numBits + (BE n).size = 32

@[simp]

theorem fromByteArrayBigEndian_empty : EvmYul.fromByteArrayBigEndian ByteArray.empty = 0

theorem UInt256.val_eq {n : ℕ} (h : n < EvmYul.UInt256.size) : ↑(EvmYul.UInt256.ofNat n).val = n

theorem UInt256.ofNat_eq {n : ℕ} : EvmYul.UInt256.ofNat n = { val := Fin.ofNat n }

theorem UInt256.ofNat_toNat {n : ℕ} (n_le_size : n < EvmYul.UInt256.size) : (EvmYul.UInt256.ofNat n).toNat = n

theorem UInt256.ofNat_toSigned {n : ℕ} {p : ℤ} (h : ↑n = p) : EvmYul.UInt256.ofNat n = EvmYul.UInt256.toSigned p

theorem UInt256.toByteArray_size (val : EvmYul.UInt256) : val.toByteArray.size = 32

theorem UInt256.toArray_size (n : EvmYul.UInt256) : n.toByteArray.data.size = 32

@[simp]

theorem UInt256.sub_0 {n : EvmYul.UInt256} : n - EvmYul.UInt256.ofNat 0 = n

@[simp]

theorem UInt256.zero_add {n : ℕ} : EvmYul.UInt256.ofNat 0 + EvmYul.UInt256.ofNat n = EvmYul.UInt256.ofNat n

theorem UInt256.add_succ_mod_size {p : ℤ} (pos : 0 ≤ p) (size_ok : p + 1 < ↑EvmYul.UInt256.size) : (p + 1) % ↑EvmYul.UInt256.size = p + 1

theorem UInt256.sub_to_fin (n m : EvmYul.UInt256) : n - m = { val := n.val - m.val }

theorem UInt256.toNat_sub_dist (n m : EvmYul.UInt256) (le_ok : m ≤ n) : (n - m).toNat = n.toNat - m.toNat

theorem UInt256.ofNat_le (n m : EvmYul.UInt256) : (n ≤ m) = (n.toNat ≤ m.toNat)

@[simp]

theorem accountAddressIsSome (n : ℕ) (size : n < EvmYul.AccountAddress.size) : EvmYul.AccountAddress.ofNat n = ⟨n, size⟩

@[simp]

theorem isCreate_false {τ : EvmYul.OperationType} (opcode : EvmYul.Operation τ) (noCreate : opcode ≠ EvmYul.Operation.CREATE) (noCreate2 : opcode ≠ EvmYul.Operation.CREATE2) : opcode.isCreate = false

theorem X_bad_pc {gas : ℕ} {opcode : UInt8} {symValidJumps : Array EvmYul.UInt256} {symState : EvmYul.EVM.State} (gpos : 1 < gas) (pc1 : symState.pc = EvmYul.UInt256.ofNat 1) (opcode_single : symState.executionEnv.code = { data := #[opcode] }) (stack_ok : List.length symState.stack < 1025) : EvmYul.EVM.X gas symValidJumps symState = Except.ok (EvmYul.EVM.ExecutionResult.success { toState := symState.toState, gasAvailable := symState.gasAvailable, activeWords := symState.activeWords, memory := symState.memory, returnData := ByteArray.empty, H_return := symState.H_return, pc := symState.pc, stack := symState.stack, execLength := symState.execLength + 1 } ByteArray.empty)

Execution result of X for a single-opcode program when pc is set to 1