def EvmYul.UInt256.size : ℕ

The size of type UInt256, that is, 2^256.

Equations

• EvmYul.UInt256.size = 115792089237316195423570985008687907853269984665640564039457584007913129639936

structure EvmYul.UInt256 : Type

• val : Fin size

instance EvmYul.instBEqUInt256 : BEq UInt256

Equations

• EvmYul.instBEqUInt256 = { beq := EvmYul.beqUInt256✝ }

instance EvmYul.instOrdUInt256 : Ord UInt256

Equations

• EvmYul.instOrdUInt256 = { compare := EvmYul.ordUInt256✝ }

instance EvmYul.instToStringUInt256 : ToString UInt256

Equations

• EvmYul.instToStringUInt256 = { toString := fun (a : EvmYul.UInt256) => toString a.val }

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

Equations

• EvmYul.UInt256.ofNat n = Id.run { val := Fin.ofNat n }

def EvmYul.UInt256.toNat (u : UInt256) : ℕ

Equations

• u.toNat = ↑u.val

instance EvmYul.UInt256.instRepr : Repr UInt256

Equations

• EvmYul.UInt256.instRepr = { reprPrec := fun (n : EvmYul.UInt256) (x : ℕ) => repr n.toNat }

instance EvmYul.UInt256.instOfNatFinSize {n : ℕ} : OfNat (Fin size) n

Equations

• EvmYul.UInt256.instOfNatFinSize = { ofNat := Fin.ofNat n }

instance EvmYul.UInt256.instInhabited : Inhabited UInt256

Equations

• EvmYul.UInt256.instInhabited = { default := EvmYul.UInt256.ofNat 0 }

@[reducible, inline]

abbrev Nat.toUInt256 : ℕ → EvmYul.UInt256

Equations

• Nat.toUInt256 = EvmYul.UInt256.ofNat

@[reducible, inline]

abbrev UInt8.toUInt256 (a : UInt8) : EvmYul.UInt256

Equations

• a.toUInt256 = { val := ⟨a.toNat, ⋯⟩ }

def Bool.toUInt256 (b : Bool) : EvmYul.UInt256

Equations

• b.toUInt256 = if b = true then EvmYul.UInt256.ofNat 1 else EvmYul.UInt256.ofNat 0

@[simp]

theorem Bool.toUInt256_true : true.toUInt256 = EvmYul.UInt256.ofNat 1

@[simp]

theorem Bool.toUInt256_false : false.toUInt256 = EvmYul.UInt256.ofNat 0

def EvmYul.UInt256.add (a b : UInt256) : UInt256

Equations

• a.add b = { val := a.val + b.val }

def EvmYul.UInt256.sub (a b : UInt256) : UInt256

Equations

• a.sub b = { val := a.val - b.val }

def EvmYul.UInt256.mul (a b : UInt256) : UInt256

Equations

• a.mul b = { val := a.val * b.val }

def EvmYul.UInt256.div (a b : UInt256) : UInt256

Equations

• a.div b = { val := a.val / b.val }

def EvmYul.UInt256.mod (a b : UInt256) : UInt256

Equations

• a.mod b = if (b.val == 0) = true then { val := 0 } else { val := a.val % b.val }

def EvmYul.UInt256.modn (a : UInt256) (n : ℕ) : UInt256

Equations

• a.modn n = { val := a.val.modn n }

def EvmYul.UInt256.land (a b : UInt256) : UInt256

Equations

• a.land b = { val := a.val.land b.val }

def EvmYul.UInt256.lor (a b : UInt256) : UInt256

Equations

• a.lor b = { val := a.val.lor b.val }

def EvmYul.UInt256.xor (a b : UInt256) : UInt256

Equations

• a.xor b = { val := a.val.xor b.val }

def EvmYul.UInt256.shiftLeft (a b : UInt256) : UInt256

Equations

• a.shiftLeft b = if b.val ≥ 256 then { val := 0 } else { val := a.val <<< b.val }

def EvmYul.UInt256.shiftRight (a b : UInt256) : UInt256

Equations

• a.shiftRight b = if b.val ≥ 256 then { val := 0 } else { val := a.val >>> b.val }

def EvmYul.UInt256.log2 (a : UInt256) : UInt256

Equations

• a.log2 = { val := a.val.log2 }

instance EvmYul.UInt256.instAdd : Add UInt256

Equations

• EvmYul.UInt256.instAdd = { add := EvmYul.UInt256.add }

instance EvmYul.UInt256.instSub : Sub UInt256

Equations

• EvmYul.UInt256.instSub = { sub := EvmYul.UInt256.sub }

instance EvmYul.UInt256.instMul : Mul UInt256

Equations

• EvmYul.UInt256.instMul = { mul := EvmYul.UInt256.mul }

instance EvmYul.UInt256.instDiv : Div UInt256

Equations

• EvmYul.UInt256.instDiv = { div := EvmYul.UInt256.div }

instance EvmYul.UInt256.instMod : Mod UInt256

Equations

• EvmYul.UInt256.instMod = { mod := EvmYul.UInt256.mod }

instance EvmYul.UInt256.instHModNat : HMod UInt256 ℕ UInt256

Equations

• EvmYul.UInt256.instHModNat = { hMod := EvmYul.UInt256.modn }

instance EvmYul.UInt256.instLT : LT UInt256

Equations

• EvmYul.UInt256.instLT = { lt := fun (a b : EvmYul.UInt256) => a.val < b.val }

instance EvmYul.UInt256.instLE : LE UInt256

Equations

• EvmYul.UInt256.instLE = { le := fun (a b : EvmYul.UInt256) => a.val ≤ b.val }

instance EvmYul.UInt256.instPreorder : Preorder UInt256

Equations

• EvmYul.UInt256.instPreorder = Preorder.mk EvmYul.UInt256.instPreorder.proof_1 EvmYul.UInt256.instPreorder.proof_2 EvmYul.UInt256.instPreorder.proof_3

def EvmYul.UInt256.complement (a : UInt256) : UInt256

Equations

• a.complement = { val := 0 - (a.val + 1) }

def EvmYul.UInt256.lnot (a : UInt256) : UInt256

Equations

• a.lnot = EvmYul.UInt256.ofNat (EvmYul.UInt256.size - 1) - a

def EvmYul.UInt256.abs (a : UInt256) : UInt256

Equations

• a.abs = if 2 ^ 255 ≤ a.toNat then { val := a.val * -1 } else a

def EvmYul.UInt256.fromSigned (a : UInt256) : ℤ

Equations

• a.fromSigned = if a.toNat < 2 ^ 255 then ↑↑a.val else -↑((EvmYul.UInt256.size - 1).xor ↑a.val) - 1

def EvmYul.UInt256.toSigned (i : ℤ) : UInt256

Equations

• EvmYul.UInt256.toSigned (Int.ofNat n) = EvmYul.UInt256.ofNat n
• EvmYul.UInt256.toSigned (Int.negSucc n) = EvmYul.UInt256.ofNat (EvmYul.UInt256.size - 1 - n)

instance EvmYul.UInt256.instComplement : Complement UInt256

Equations

• EvmYul.UInt256.instComplement = { complement := EvmYul.UInt256.complement }

def EvmYul.UInt256.pow (b n : UInt256) : UInt256

Equations

• b.pow n = EvmYul.UInt256.powAux✝ { val := 1 } b ↑n.val

instance EvmYul.UInt256.instHPow : HPow UInt256 UInt256 UInt256

Equations

• EvmYul.UInt256.instHPow = { hPow := EvmYul.UInt256.pow }

instance EvmYul.UInt256.instAndOp : AndOp UInt256

Equations

• EvmYul.UInt256.instAndOp = { and := EvmYul.UInt256.land }

instance EvmYul.UInt256.instOrOp : OrOp UInt256

Equations

• EvmYul.UInt256.instOrOp = { or := EvmYul.UInt256.lor }

instance EvmYul.UInt256.instXor : Xor UInt256

Equations

• EvmYul.UInt256.instXor = { xor := EvmYul.UInt256.xor }

instance EvmYul.UInt256.instShiftLeft : ShiftLeft UInt256

Equations

• EvmYul.UInt256.instShiftLeft = { shiftLeft := EvmYul.UInt256.shiftLeft }

instance EvmYul.UInt256.instShiftRight : ShiftRight UInt256

Equations

• EvmYul.UInt256.instShiftRight = { shiftRight := EvmYul.UInt256.shiftRight }

instance EvmYul.UInt256.instDecidableEq : DecidableEq UInt256

Equations

• a.instDecidableEq b = match decEq a.val b.val with | isTrue h => isTrue ⋯ | isFalse h => let_fun neq := ⋯; isFalse neq

def EvmYul.UInt256.decLt (a b : UInt256) : Decidable (a < b)

Equations

• a.decLt b = inferInstanceAs (Decidable (a < b))

def EvmYul.UInt256.decLe (a b : UInt256) : Decidable (a ≤ b)

Equations

• a.decLe b = inferInstanceAs (Decidable (a ≤ b))

instance EvmYul.UInt256.instDecidableLt (a b : UInt256) : Decidable (a < b)

Equations

• a.instDecidableLt b = a.decLt b

instance EvmYul.UInt256.instDecidableLe (a b : UInt256) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = a.decLe b

instance EvmYul.UInt256.instMax : Max UInt256

Equations

• EvmYul.UInt256.instMax = maxOfLe

instance EvmYul.UInt256.instMin : Min UInt256

Equations

• EvmYul.UInt256.instMin = minOfLe

def EvmYul.UInt256.eq0 (a : UInt256) : Bool

Equations

• a.eq0 = (a == { val := 0 })

def EvmYul.UInt256.byteAt (a b : UInt256) : UInt256

Equations

• a.byteAt b = if a > { val := 31 } then { val := 0 } else b >>> EvmYul.UInt256.ofNat ((31 - a.toNat) * 8) &&& { val := 255 }

def EvmYul.UInt256.sgn (a : UInt256) : ℤ

Equations

• a.sgn = if 2 ^ 255 ≤ a.toNat then -1 else if a.eq0 = true then 0 else 1

def EvmYul.UInt256.bigUInt : UInt256

Equations

• EvmYul.UInt256.bigUInt = EvmYul.UInt256.ofNat 115792089237316195423570985008687907853269984665640564039457584007913129639935

def EvmYul.UInt256.sdiv (a b : UInt256) : UInt256

Equations

• a.sdiv b = if 2 ^ 255 ≤ a.toNat then if 2 ^ 255 ≤ b.toNat then a.abs / b.abs else { val := (a.abs / b).val * -1 } else if 2 ^ 255 ≤ b.toNat then { val := (a / b.abs).val * -1 } else a / b

def EvmYul.UInt256.smod (a b : UInt256) : UInt256

Equations

• a.smod b = if (b.toNat == 0) = true then { val := 0 } else EvmYul.UInt256.toSigned (a.sgn * ↑(a.abs % b.abs).toNat)

def EvmYul.UInt256.sltBool (a b : UInt256) : Bool

Equations

• a.sltBool b = if a.toNat ≥ 2 ^ 255 then if b.toNat ≥ 2 ^ 255 then decide (a < b) else true else if b.toNat ≥ 2 ^ 255 then false else decide (a < b)

def EvmYul.UInt256.sgtBool (a b : UInt256) : Bool

Equations

• a.sgtBool b = if a.toNat ≥ 2 ^ 255 then if b.toNat ≥ 2 ^ 255 then decide (a > b) else false else if b.toNat ≥ 2 ^ 255 then true else decide (a > b)

@[reducible, inline]

abbrev EvmYul.UInt256.fromBool (b : Bool) : UInt256

Equations

• EvmYul.UInt256.fromBool = Bool.toUInt256

def EvmYul.UInt256.slt (a b : UInt256) : UInt256

Equations

• a.slt b = EvmYul.UInt256.fromBool (a.sltBool b)

def EvmYul.UInt256.sgt (a b : UInt256) : UInt256

Equations

• a.sgt b = EvmYul.UInt256.fromBool (a.sgtBool b)

def EvmYul.UInt256.sar (a b : UInt256) : UInt256

Equations

• a.sar b = if b.sltBool { val := 0 } = true then (b.complement >>> a).complement else b >>> a

def EvmYul.UInt256.signextend (a b : UInt256) : UInt256

Equations

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

def EvmYul.UInt256.addMod (a b c : UInt256) : UInt256

Equations

• a.addMod b c = if c.eq0 = true then { val := 0 } else EvmYul.UInt256.ofNat ((↑a.val + ↑b.val).mod c.toNat)

def EvmYul.UInt256.mulMod (a b c : UInt256) : UInt256

Equations

• a.mulMod b c = if c.eq0 = true then { val := 0 } else EvmYul.UInt256.ofNat ((↑a.val * ↑b.val).mod c.toNat)

def EvmYul.UInt256.exp (a b : UInt256) : UInt256

Equations

• a.exp b = a.pow b

def EvmYul.UInt256.lt (a b : UInt256) : UInt256

Equations

• a.lt b = EvmYul.UInt256.fromBool (decide (a < b))

def EvmYul.UInt256.gt (a b : UInt256) : UInt256

Equations

• a.gt b = EvmYul.UInt256.fromBool (decide (a > b))

def EvmYul.UInt256.eq (a b : UInt256) : UInt256

Equations

• a.eq b = EvmYul.UInt256.fromBool (decide (a = b))

def EvmYul.UInt256.isZero (a : UInt256) : UInt256

Equations

• a.isZero = EvmYul.UInt256.fromBool a.eq0

def EvmYul.fromBytes' : List UInt8 → ℕ

Equations

• EvmYul.fromBytes' [] = 0
• EvmYul.fromBytes' (b :: bs) = ↑b.toFin + 2 ^ 8 * EvmYul.fromBytes' bs

def EvmYul.fromBytesBigEndian : List UInt8 → ℕ

Equations

• EvmYul.fromBytesBigEndian = EvmYul.fromBytes' ∘ List.reverse

def EvmYul.fromByteArrayBigEndian (b : ByteArray) : ℕ

Equations

• EvmYul.fromByteArrayBigEndian b = EvmYul.fromBytesBigEndian b.toList

def EvmYul.toBytesBigEndian : ℕ → List UInt8

Equations

• EvmYul.toBytesBigEndian = List.reverse ∘ EvmYul.toBytes'✝

theorem EvmYul.zeroPadBytes_len {bs : List UInt8} {n : ℕ} (h : bs.length ≤ n) : (EvmYul.zeroPadBytes✝ n bs).length = n

def EvmYul.fromBytes! (bs : List UInt8) : ℕ

Equations

• EvmYul.fromBytes! bs = EvmYul.fromBytes' (List.take 32 bs)

@[simp]

theorem EvmYul.fromBytes_wasnt_naughty {bs : List UInt8} : fromBytes! bs < 2 ^ 256

def EvmYul.fromBytes_if_you_really_must? (bs : List UInt8) : UInt256

Equations

• EvmYul.fromBytes_if_you_really_must? bs = { val := ⟨EvmYul.fromBytes! bs, ⋯⟩ }

def EvmYul.toBytes! (n : UInt256) : List UInt8

Equations

• EvmYul.toBytes! n = EvmYul.zeroPadBytes✝ 32 (EvmYul.toBytes'✝ ↑n.val)

def EvmYul.uInt256OfByteArray (arr : ByteArray) : UInt256

Equations

• EvmYul.uInt256OfByteArray arr = EvmYul.UInt256.ofNat (EvmYul.fromBytes' arr.data.toList.reverse)

def ByteArray.copySlice' (src : ByteArray) (srcOff : ℕ) (dest : ByteArray) (destOff len : ℕ) (exact : Bool := true) : ByteArray

Equations

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