diff --git a/LeanPool.lean b/LeanPool.lean index 194c50053d..fea8848260 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -2744,6 +2744,18 @@ import LeanPool.LanguageGeneration.FiniteWitness.Width.TwoCore import LeanPool.LanguageGeneration.FiniteWitness.Width.Value import LeanPool.LatticeTriangle import LeanPool.LatticeTriangle.Solution +import LeanPool.Lean4EVM +import LeanPool.Lean4EVM.Primitives.FixedBytes +import LeanPool.Lean4EVM.Primitives.FixedBytes.Address +import LeanPool.Lean4EVM.Primitives.FixedBytes.Bytes32 +import LeanPool.Lean4EVM.Primitives.FixedBytes.Core +import LeanPool.Lean4EVM.Primitives.FixedBytes.H160 +import LeanPool.Lean4EVM.Primitives.FixedBytes.H256 +import LeanPool.Lean4EVM.Primitives.UInt +import LeanPool.Lean4EVM.Primitives.UInt.Core +import LeanPool.Lean4EVM.Primitives.UInt.U128 +import LeanPool.Lean4EVM.Primitives.UInt.U256 +import LeanPool.Lean4EVM.Primitives.UInt.U64 import LeanPool.Lean4GlCoalgebras import LeanPool.Lean4GlCoalgebras.General.Completeness import LeanPool.Lean4GlCoalgebras.General.Game diff --git a/LeanPool/Lean4EVM.lean b/LeanPool/Lean4EVM.lean new file mode 100644 index 0000000000..fa6aec86f0 --- /dev/null +++ b/LeanPool/Lean4EVM.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ + +import LeanPool.Lean4EVM.Primitives.UInt +import LeanPool.Lean4EVM.Primitives.FixedBytes + +/-! +# Verified Ethereum Virtual Machine primitives + +Source: url:https://github.com/mrLSD/Lean4EVM +Authors: mrLSD +Status: verified +Main declarations: `Lean4EVM.U256.toNat_addmod`, `Lean4EVM.U256.toNat_mulmod` +Tags: verified-algorithms, ethereum, fixed-width-arithmetic, byte-representations +MSC: 68Q60, 68V20 +-/ + +/-! +# Lean4EVM + +Fixed-width integer and byte primitives for Ethereum, with proofs of their arithmetic and +conversion operations. The imported library does not define an EVM interpreter, machine state, +gas accounting, or transaction semantics. + +`Primitives.UInt` and `Primitives.FixedBytes` are family façades. Their `Core` modules own shared +representations and proofs; modules named after public types own width- or meaning-specific APIs. +Optional conversions use the suffix `Opt` so the repository declaration audit resolves their full +names distinctly from the wrapping conversions. +-/ + +/- +Upstream MIT notice retained from mrLSD/Lean4EVM at commit +0109646545bc1f29c719c1268bad7c561d2035f8. + +MIT License + +Copyright (c) 2026 Evgeny Ukhanov + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. +-/ diff --git a/LeanPool/Lean4EVM/Primitives/FixedBytes.lean b/LeanPool/Lean4EVM/Primitives/FixedBytes.lean new file mode 100644 index 0000000000..bb07e7ba81 --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/FixedBytes.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.FixedBytes.H160 +import LeanPool.Lean4EVM.Primitives.FixedBytes.H256 +import LeanPool.Lean4EVM.Primitives.FixedBytes.Bytes32 +import LeanPool.Lean4EVM.Primitives.FixedBytes.Address + +/-! +# Fixed-size Ethereum byte values + +Public entry point for exact-size byte primitives. `Core` owns `FixedBytes size`, big-endian +serialization, and the shared proofs. `H160`, `H256`, `Bytes32`, and `Address` are separate nominal +types whose operations, conversions, and laws remain in their respective modules. + +The family is named `FixedBytes` because exact byte width is its defining invariant; equal widths do +not imply semantic interchangeability. +-/ diff --git a/LeanPool/Lean4EVM/Primitives/FixedBytes/Address.lean b/LeanPool/Lean4EVM/Primitives/FixedBytes/Address.lean new file mode 100644 index 0000000000..1ce2d1eaf9 --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/FixedBytes/Address.lean @@ -0,0 +1,269 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.FixedBytes.H160 +import LeanPool.Lean4EVM.Primitives.UInt.U256 + +/-! +# `Address` + +Nominal 20-byte Ethereum addresses, exact serialization, and explicit EVM-word conversions. +-/ + +namespace Lean4EVM + +/-! ## `Address` -/ + +/-- A nominal 20-byte Ethereum account or contract address. -/ +@[ext] +structure Address where + /-- The exact 20-byte address payload. -/ + bytes : FixedBytes 20 + deriving Repr, Hashable + +namespace Address + +/-- Constructs an address from its exact generic representation. -/ +def ofFixedBytes (value : FixedBytes 20) : Address := + ⟨value⟩ + +/-- Returns the exact generic representation. -/ +def toFixedBytes (value : Address) : FixedBytes 20 := + value.bytes + +/-- Constructs an address by retaining the low 160 bits. -/ +def ofNat (n : ℕ) : Address := + ofFixedBytes (FixedBytes.ofNat 20 n) + +/-- Constructs an address only when `n` fits in 160 bits. -/ +def ofNatOpt (n : ℕ) : Option Address := + (FixedBytes.ofNatOpt 20 n).map ofFixedBytes + +/-- Returns the unsigned 160-bit address value. -/ +def toNat (value : Address) : ℕ := + value.toFixedBytes.toNat + +/-- Returns the exact lowercase 20-byte hexadecimal payload. -/ +def toHex (value : Address) : String := + value.toFixedBytes.toHex + +/-- Returns the address byte at `index` in big-endian order, or zero out of bounds. -/ +def getByte (value : Address) (index : ℕ) : UInt8 := + value.toFixedBytes.getByte index + +/-- Returns address bit `index`, counting from the least-significant bit. -/ +def testBit (value : Address) (index : ℕ) : Bool := + value.toFixedBytes.testBit index + +/-- Parses an exact 20-byte big-endian address payload. -/ +def ofByteArrayOpt (bytes : ByteArray) : Option Address := + (FixedBytes.ofByteArrayOpt 20 bytes).map ofFixedBytes + +/-- Serializes the address as exactly 20 big-endian bytes. -/ +def toByteArray (value : Address) : ByteArray := + value.toFixedBytes.toByteArray + +/-- Returns the greatest 160-bit address payload. -/ +def max : Address := + ofFixedBytes (FixedBytes.max 20) + +/-- Converts a 160-bit hash payload to a nominal address. -/ +def ofH160 (value : H160) : Address := + ofFixedBytes value.toFixedBytes + +/-- Converts an address payload to a nominal 160-bit hash. -/ +def toH160 (value : Address) : H160 := + H160.ofFixedBytes value.toFixedBytes + +/-- Extracts the low 160 bits of an EVM word as an address. -/ +def ofU256 (value : U256) : Address := + ofNat value.toNat + +/-- Converts an EVM word to an address only when its high 96 bits are zero. -/ +def ofU256Opt (value : U256) : Option Address := + ofNatOpt value.toNat + +/-- Zero-extends an address to an EVM word. -/ +def toU256 (value : Address) : U256 := + U256.ofNat value.toNat + +/-- Equality of generic representations identifies equal addresses. -/ +theorem toFixedBytes_injective : Function.Injective toFixedBytes := by + intro ⟨a⟩ ⟨b⟩ h + cases h + rfl + +/-- Addresses use unsigned big-endian numeric order. -/ +instance : LinearOrder Address := + LinearOrder.lift' toFixedBytes toFixedBytes_injective + +/-- Zero is the all-zero address. -/ +instance : Zero Address where + zero := ofNat 0 + +/-- One has only the least-significant address bit set. -/ +instance : One Address where + one := ofNat 1 + +/-- Natural casts retain the low 160 bits. -/ +instance : NatCast Address where + natCast := ofNat + +/-- The default address is zero. -/ +instance : Inhabited Address := + ⟨0⟩ + +/-- String conversion emits the raw exact-width hexadecimal payload. -/ +instance : ToString Address where + toString := toHex + +/-- Converting from generic bytes and back is lossless. -/ +@[simp] +theorem toFixedBytes_ofFixedBytes (value : FixedBytes 20) : + (ofFixedBytes value).toFixedBytes = value := + rfl + +/-- Converting to generic bytes and back is lossless. -/ +@[simp] +theorem ofFixedBytes_toFixedBytes (value : Address) : + ofFixedBytes value.toFixedBytes = value := by + cases value + rfl + +/-- Equal unsigned values identify equal addresses. -/ +theorem toNat_injective : Function.Injective toNat := by + intro a b h + apply toFixedBytes_injective + exact FixedBytes.toNat_injective h + +/-- Equality agrees with equality of unsigned address values. -/ +@[simp] +theorem toNat_inj {a b : Address} : a.toNat = b.toNat ↔ a = b := + toNat_injective.eq_iff + +/-- Bit testing agrees with the unsigned address value. -/ +@[simp] +theorem testBit_eq (value : Address) (index : ℕ) : + value.testBit index = value.toNat.testBit index := + FixedBytes.testBit_eq value.toFixedBytes index + +/-- Address bits at indices 160 and above are false. -/ +theorem testBit_of_ge (value : Address) (index : ℕ) (h : 160 ≤ index) : + value.testBit index = false := by + exact FixedBytes.testBit_of_bitWidth_le value.toFixedBytes index (by simpa [FixedBytes.bitWidth]) + +/-- Natural construction retains the low 160 bits. -/ +@[simp] +theorem toNat_ofNat (n : ℕ) : (ofNat n).toNat = n % 2 ^ 160 := by + simp [toNat, ofNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Converting through a natural number is lossless. -/ +@[simp] +theorem ofNat_toNat (value : Address) : ofNat value.toNat = value := by + apply toFixedBytes_injective + simp [ofNat, toNat] + +/-- Every address lies below the 160-bit modulus. -/ +theorem toNat_lt (value : Address) : value.toNat < 2 ^ 160 := by + simpa [toNat, FixedBytes.modulus, FixedBytes.bitWidth] using + FixedBytes.toNat_lt_modulus value.toFixedBytes + +/-- The greatest address payload is `2 ^ 160 - 1`. -/ +@[simp] +theorem toNat_max : max.toNat = 2 ^ 160 - 1 := by + simp [max, toNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Checked construction fails exactly outside the 160-bit range. -/ +@[simp] +theorem ofNatOpt_eq_none_iff (n : ℕ) : ofNatOpt n = none ↔ 2 ^ 160 ≤ n := by + simp [ofNatOpt, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Checked construction succeeds exactly for representable address values. -/ +theorem ofNatOpt_eq_some_iff {n : ℕ} {value : Address} : + ofNatOpt n = some value ↔ n < 2 ^ 160 ∧ ofNat n = value := by + simp [ofNatOpt, ofNat, FixedBytes.ofNatOpt_eq_some_iff, FixedBytes.modulus, + FixedBytes.bitWidth] + +/-- Unsigned order agrees with order on natural-number values. -/ +@[simp] +theorem le_iff_toNat_le (a b : Address) : a ≤ b ↔ a.toNat ≤ b.toNat := + Iff.rfl + +/-- Strict order agrees with order on natural-number values. -/ +@[simp] +theorem lt_iff_toNat_lt (a b : Address) : a < b ↔ a.toNat < b.toNat := + Iff.rfl + +/-- Serialization always emits 20 bytes. -/ +@[simp] +theorem toByteArray_size (value : Address) : value.toByteArray.size = 20 := by + simp [toByteArray] + +/-- Parsing succeeds exactly for 20-byte arrays. -/ +@[simp] +theorem ofByteArrayOpt_isSome (bytes : ByteArray) : + (ofByteArrayOpt bytes).isSome = decide (bytes.size = 20) := by + simp [ofByteArrayOpt] + +/-- Parsing a serialized address is lossless. -/ +@[simp] +theorem ofByteArrayOpt_toByteArray (value : Address) : + ofByteArrayOpt value.toByteArray = some value := by + simp [ofByteArrayOpt, toByteArray] + +/-- Serializing any successfully parsed address reproduces that input. -/ +theorem toByteArray_ofByteArrayOpt_eq_some {bytes : ByteArray} {value : Address} + (h : ofByteArrayOpt bytes = some value) : value.toByteArray = bytes := by + simp only [ofByteArrayOpt, Option.map_eq_some_iff] at h + rcases h with ⟨raw, hraw, rfl⟩ + exact FixedBytes.toByteArray_ofByteArrayOpt_eq_some hraw + +/-- Converting an address to `H160` and back is lossless. -/ +@[simp] +theorem ofH160_toH160 (value : Address) : ofH160 value.toH160 = value := by + cases value + rfl + +/-- Converting `H160` to an address and back is lossless. -/ +@[simp] +theorem toH160_ofH160 (value : H160) : (ofH160 value).toH160 = value := by + cases value + rfl + +/-- Extracting an address from a word retains exactly its low 160 bits. -/ +@[simp] +theorem toNat_ofU256 (value : U256) : (ofU256 value).toNat = value.toNat % 2 ^ 160 := by + simp [ofU256] + +/-- Checked word conversion succeeds exactly when the word fits in 160 bits. -/ +theorem ofU256Opt_eq_some_iff {word : U256} {value : Address} : + ofU256Opt word = some value ↔ word.toNat < 2 ^ 160 ∧ ofU256 word = value := by + exact ofNatOpt_eq_some_iff + +/-- Zero-extension preserves the unsigned address value. -/ +@[simp] +theorem toNat_toU256 (value : Address) : value.toU256.toNat = value.toNat := by + change FixedUInt.toNat (FixedUInt.ofNat value.toNat : U256) = value.toNat + rw [FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + exact lt_trans value.toNat_lt (by decide) + +/-- Zero-extending an address and taking its low 160 bits is lossless. -/ +@[simp] +theorem ofU256_toU256 (value : Address) : ofU256 value.toU256 = value := by + apply toFixedBytes_injective + apply FixedBytes.toNat_injective + change (ofU256 value.toU256).toNat = value.toNat + rw [toNat_ofU256, toNat_toU256, Nat.mod_eq_of_lt value.toNat_lt] + +/-- Checked conversion accepts every zero-extended address word. -/ +@[simp] +theorem ofU256Opt_toU256 (value : Address) : ofU256Opt value.toU256 = some value := by + apply ofU256Opt_eq_some_iff.mpr + rw [toNat_toU256] + exact ⟨value.toNat_lt, ofU256_toU256 value⟩ + +end Address + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/FixedBytes/Bytes32.lean b/LeanPool/Lean4EVM/Primitives/FixedBytes/Bytes32.lean new file mode 100644 index 0000000000..a8bec78daf --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/FixedBytes/Bytes32.lean @@ -0,0 +1,303 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.FixedBytes.H256 + +/-! +# `Bytes32` + +Nominal raw 32-byte values and explicit reinterpretations of hashes and EVM words. +-/ + +namespace Lean4EVM + +/-! ## `Bytes32` -/ + +/-- A nominal raw 32-byte value used by Ethereum encodings and ABI data. -/ +@[ext] +structure Bytes32 where + /-- The exact 32-byte representation. -/ + bytes : FixedBytes 32 + deriving Repr, Hashable + +namespace Bytes32 + +/-- Constructs `Bytes32` from its exact generic representation. -/ +def ofFixedBytes (value : FixedBytes 32) : Bytes32 := + ⟨value⟩ + +/-- Returns the exact generic representation. -/ +def toFixedBytes (value : Bytes32) : FixedBytes 32 := + value.bytes + +/-- Constructs `Bytes32` by retaining the low 256 bits. -/ +def ofNat (n : ℕ) : Bytes32 := + ofFixedBytes (FixedBytes.ofNat 32 n) + +/-- Constructs `Bytes32` only when `n` fits in 256 bits. -/ +def ofNatOpt (n : ℕ) : Option Bytes32 := + (FixedBytes.ofNatOpt 32 n).map ofFixedBytes + +/-- Returns the unsigned natural-number value. -/ +def toNat (value : Bytes32) : ℕ := + value.toFixedBytes.toNat + +/-- Returns the exact 32-byte hexadecimal representation. -/ +def toHex (value : Bytes32) : String := + value.toFixedBytes.toHex + +/-- Returns the byte at `index` in big-endian order, or zero out of bounds. -/ +def getByte (value : Bytes32) (index : ℕ) : UInt8 := + value.toFixedBytes.getByte index + +/-- Returns bit `index`, counting from the least-significant bit. -/ +def testBit (value : Bytes32) (index : ℕ) : Bool := + value.toFixedBytes.testBit index + +/-- Parses an exact 32-byte big-endian array. -/ +def ofByteArrayOpt (bytes : ByteArray) : Option Bytes32 := + (FixedBytes.ofByteArrayOpt 32 bytes).map ofFixedBytes + +/-- Serializes `value` as exactly 32 big-endian bytes. -/ +def toByteArray (value : Bytes32) : ByteArray := + value.toFixedBytes.toByteArray + +/-- Returns the greatest raw 32-byte value. -/ +def max : Bytes32 := + ofFixedBytes (FixedBytes.max 32) + +/-- Reinterprets an EVM word as raw 32-byte data. -/ +def ofU256 (value : U256) : Bytes32 := + ofFixedBytes ⟨value.val⟩ + +/-- Reinterprets raw 32-byte data as an EVM word. -/ +def toU256 (value : Bytes32) : U256 := + ⟨value.toFixedBytes.val⟩ + +/-- Reinterprets a 256-bit hash as raw 32-byte data. -/ +def ofH256 (value : H256) : Bytes32 := + ofFixedBytes value.toFixedBytes + +/-- Reinterprets raw 32-byte data as a 256-bit hash. -/ +def toH256 (value : Bytes32) : H256 := + H256.ofFixedBytes value.toFixedBytes + +/-- Equality of generic representations identifies equal `Bytes32` values. -/ +theorem toFixedBytes_injective : Function.Injective toFixedBytes := by + intro ⟨a⟩ ⟨b⟩ h + cases h + rfl + +/-- `Bytes32` uses unsigned big-endian numeric order. -/ +instance : LinearOrder Bytes32 := + LinearOrder.lift' toFixedBytes toFixedBytes_injective + +/-- Zero is the all-zero 32-byte value. -/ +instance : Zero Bytes32 where + zero := ofNat 0 + +/-- One has only the least-significant bit set. -/ +instance : One Bytes32 where + one := ofNat 1 + +/-- Natural casts retain the low 256 bits. -/ +instance : NatCast Bytes32 where + natCast := ofNat + +/-- The default `Bytes32` is zero. -/ +instance : Inhabited Bytes32 := + ⟨0⟩ + +/-- String conversion emits exact-width hexadecimal notation. -/ +instance : ToString Bytes32 where + toString := toHex + +/-- Complement flips every bit of raw 32-byte data. -/ +instance : Complement Bytes32 where + complement value := ofFixedBytes (~~~value.toFixedBytes) + +/-- Conjunction combines equal-position data bits. -/ +instance : AndOp Bytes32 where + and a b := ofFixedBytes (a.toFixedBytes &&& b.toFixedBytes) + +/-- Disjunction combines equal-position data bits. -/ +instance : OrOp Bytes32 where + or a b := ofFixedBytes (a.toFixedBytes ||| b.toFixedBytes) + +/-- Exclusive-or compares equal-position data bits. -/ +instance : XorOp Bytes32 where + xor a b := ofFixedBytes (a.toFixedBytes ^^^ b.toFixedBytes) + +/-- Converting from generic bytes and back is lossless. -/ +@[simp] +theorem toFixedBytes_ofFixedBytes (value : FixedBytes 32) : + (ofFixedBytes value).toFixedBytes = value := + rfl + +/-- Converting to generic bytes and back is lossless. -/ +@[simp] +theorem ofFixedBytes_toFixedBytes (value : Bytes32) : + ofFixedBytes value.toFixedBytes = value := by + cases value + rfl + +/-- Equal unsigned values identify equal `Bytes32` values. -/ +theorem toNat_injective : Function.Injective toNat := by + intro a b h + apply toFixedBytes_injective + exact FixedBytes.toNat_injective h + +/-- Equality agrees with equality of unsigned values. -/ +@[simp] +theorem toNat_inj {a b : Bytes32} : a.toNat = b.toNat ↔ a = b := + toNat_injective.eq_iff + +/-- Complement is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_complement (value : Bytes32) : + (~~~value).toFixedBytes = ~~~value.toFixedBytes := + rfl + +/-- Conjunction is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_and (a b : Bytes32) : + (a &&& b).toFixedBytes = a.toFixedBytes &&& b.toFixedBytes := + rfl + +/-- Disjunction is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_or (a b : Bytes32) : + (a ||| b).toFixedBytes = a.toFixedBytes ||| b.toFixedBytes := + rfl + +/-- Exclusive-or is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_xor (a b : Bytes32) : + (a ^^^ b).toFixedBytes = a.toFixedBytes ^^^ b.toFixedBytes := + rfl + +/-- Bit testing agrees with the unsigned value. -/ +@[simp] +theorem testBit_eq (value : Bytes32) (index : ℕ) : + value.testBit index = value.toNat.testBit index := + FixedBytes.testBit_eq value.toFixedBytes index + +/-- Bits at indices 256 and above are false. -/ +theorem testBit_of_ge (value : Bytes32) (index : ℕ) (h : 256 ≤ index) : + value.testBit index = false := by + exact FixedBytes.testBit_of_bitWidth_le value.toFixedBytes index (by simpa [FixedBytes.bitWidth]) + +/-- Natural construction retains the low 256 bits. -/ +@[simp] +theorem toNat_ofNat (n : ℕ) : (ofNat n).toNat = n % 2 ^ 256 := by + simp [toNat, ofNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Converting through a natural number is lossless. -/ +@[simp] +theorem ofNat_toNat (value : Bytes32) : ofNat value.toNat = value := by + apply toFixedBytes_injective + simp [ofNat, toNat] + +/-- Every `Bytes32` value is smaller than `2 ^ 256`. -/ +theorem toNat_lt (value : Bytes32) : value.toNat < 2 ^ 256 := by + simpa [toNat, FixedBytes.modulus, FixedBytes.bitWidth] using + FixedBytes.toNat_lt_modulus value.toFixedBytes + +/-- The greatest `Bytes32` value is `2 ^ 256 - 1`. -/ +@[simp] +theorem toNat_max : max.toNat = 2 ^ 256 - 1 := by + simp [max, toNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Unsigned order agrees with order on natural-number values. -/ +@[simp] +theorem le_iff_toNat_le (a b : Bytes32) : a ≤ b ↔ a.toNat ≤ b.toNat := + Iff.rfl + +/-- Strict order agrees with order on natural-number values. -/ +@[simp] +theorem lt_iff_toNat_lt (a b : Bytes32) : a < b ↔ a.toNat < b.toNat := + Iff.rfl + +/-- Checked construction fails exactly outside the 256-bit range. -/ +@[simp] +theorem ofNatOpt_eq_none_iff (n : ℕ) : ofNatOpt n = none ↔ 2 ^ 256 ≤ n := by + simp [ofNatOpt, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Checked construction succeeds exactly for representable 256-bit values. -/ +theorem ofNatOpt_eq_some_iff {n : ℕ} {value : Bytes32} : + ofNatOpt n = some value ↔ n < 2 ^ 256 ∧ ofNat n = value := by + simp [ofNatOpt, ofNat, FixedBytes.ofNatOpt_eq_some_iff, FixedBytes.modulus, + FixedBytes.bitWidth] + +/-- Serialization always emits 32 bytes. -/ +@[simp] +theorem toByteArray_size (value : Bytes32) : value.toByteArray.size = 32 := by + simp [toByteArray] + +/-- Parsing succeeds exactly for 32-byte arrays. -/ +@[simp] +theorem ofByteArrayOpt_isSome (bytes : ByteArray) : + (ofByteArrayOpt bytes).isSome = decide (bytes.size = 32) := by + simp [ofByteArrayOpt] + +/-- Parsing a serialized `Bytes32` value is lossless. -/ +@[simp] +theorem ofByteArrayOpt_toByteArray (value : Bytes32) : + ofByteArrayOpt value.toByteArray = some value := by + simp [ofByteArrayOpt, toByteArray] + +/-- Serializing any successfully parsed `Bytes32` input reproduces that input. -/ +theorem toByteArray_ofByteArrayOpt_eq_some {bytes : ByteArray} {value : Bytes32} + (h : ofByteArrayOpt bytes = some value) : value.toByteArray = bytes := by + simp only [ofByteArrayOpt, Option.map_eq_some_iff] at h + rcases h with ⟨raw, hraw, rfl⟩ + exact FixedBytes.toByteArray_ofByteArrayOpt_eq_some hraw + +/-- Reinterpreting bytes as a word and back is lossless. -/ +@[simp] +theorem ofU256_toU256 (value : Bytes32) : ofU256 value.toU256 = value := by + cases value + rfl + +/-- Reinterpreting a word as bytes and back is lossless. -/ +@[simp] +theorem toU256_ofU256 (value : U256) : (ofU256 value).toU256 = value := + rfl + +/-- Word conversion preserves the unsigned value. -/ +@[simp] +theorem toNat_toU256 (value : Bytes32) : value.toU256.toNat = value.toNat := + rfl + +/-- Byte construction from a word preserves the unsigned value. -/ +@[simp] +theorem toNat_ofU256 (value : U256) : (ofU256 value).toNat = value.toNat := + rfl + +/-- Reinterpreting bytes as a hash and back is lossless. -/ +@[simp] +theorem ofH256_toH256 (value : Bytes32) : ofH256 value.toH256 = value := by + cases value + rfl + +/-- Reinterpreting a hash as bytes and back is lossless. -/ +@[simp] +theorem toH256_ofH256 (value : H256) : (ofH256 value).toH256 = value := by + cases value + rfl + +/-- Hash conversion preserves the unsigned value. -/ +@[simp] +theorem toNat_toH256 (value : Bytes32) : value.toH256.toNat = value.toNat := + rfl + +/-- Byte conversion from a hash preserves the unsigned value. -/ +@[simp] +theorem toNat_ofH256 (value : H256) : (ofH256 value).toNat = value.toNat := + rfl + +end Bytes32 + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/FixedBytes/Core.lean b/LeanPool/Lean4EVM/Primitives/FixedBytes/Core.lean new file mode 100644 index 0000000000..cc1faf6851 --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/FixedBytes/Core.lean @@ -0,0 +1,397 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import Mathlib.Data.BitVec +import Mathlib.Data.Nat.Digits.Defs + +/-! +# Fixed-size byte core + +This module owns the generic `FixedBytes size` representation, exact-length big-endian codec, and +their shared laws. Nominal Ethereum meanings are introduced only by the `H160`, `H256`, `Bytes32`, +and `Address` modules, preventing equal-width values from becoming interchangeable. +-/ + +namespace Lean4EVM + +/-! ## Generic fixed-size bytes -/ + +/-- A byte string containing exactly `size` bytes. -/ +@[ext] +structure FixedBytes (size : ℕ) where + /-- The underlying `8 * size` bits. -/ + val : BitVec (8 * size) + deriving Repr, Hashable + +namespace FixedBytes + +variable {size : ℕ} + +/-- Returns the number of bits in `size` bytes. -/ +def bitWidth (size : ℕ) : ℕ := + 8 * size + +/-- Returns the cardinality `2 ^ (8 * size)` of a fixed-byte domain. -/ +def modulus (size : ℕ) : ℕ := + 2 ^ bitWidth size + +/-- Constructs fixed bytes by retaining the low `8 * size` bits of `n`. -/ +def ofNat (size : ℕ) (n : ℕ) : FixedBytes size := + ⟨BitVec.ofNat (bitWidth size) n⟩ + +/-- Constructs fixed bytes only when `n` fits in `size` bytes. -/ +def ofNatOpt (size : ℕ) (n : ℕ) : Option (FixedBytes size) := + if n < modulus size then some (ofNat size n) else none + +/-- Returns the big-endian byte string interpreted as an unsigned natural number. -/ +def toNat (value : FixedBytes size) : ℕ := + value.val.toNat + +/-- Returns the exact-width hexadecimal representation. -/ +def toHex (value : FixedBytes size) : String := + if size = 0 then "0x" else "0x" ++ value.val.toHex + +/-- Returns the greatest `size`-byte value. -/ +def max (size : ℕ) : FixedBytes size := + ⟨BitVec.allOnes (bitWidth size)⟩ + +/-- Returns the byte at `index` in big-endian order, or zero when out of bounds. -/ +def getByte (value : FixedBytes size) (index : ℕ) : UInt8 := + if index < size then + UInt8.ofNat ((value.toNat / 2 ^ (8 * (size - 1 - index))) % 256) + else + 0 + +/-- Returns bit `index`, counting from the least-significant bit. -/ +def testBit (value : FixedBytes size) (index : ℕ) : Bool := + value.val.getLsbD index + +/-- Interprets a byte list as a big-endian natural number. -/ +def byteListToNat (bytes : List UInt8) : ℕ := + bytes.foldl (fun acc byte => acc * 256 + byte.toNat) 0 + +/-- Interprets a byte array as a big-endian natural number. -/ +def byteArrayToNat (bytes : ByteArray) : ℕ := + byteListToNat bytes.data.toList + +/-- Big-endian decoding is little-endian digit evaluation after reversing the bytes. -/ +theorem byteListToNat_eq_ofDigits (bytes : List UInt8) : + byteListToNat bytes = Nat.ofDigits 256 (bytes.reverse.map UInt8.toNat) := by + unfold byteListToNat + rw [List.foldl_eq_foldr_reverse, Nat.ofDigits_eq_foldr] + simp only [List.foldr_map] + congr 1 + funext byte acc + simp [Nat.add_comm, Nat.mul_comm] + +/-- A byte list decodes below the cardinality determined by its length. -/ +theorem byteListToNat_lt (bytes : List UInt8) : + byteListToNat bytes < 256 ^ bytes.length := by + rw [byteListToNat_eq_ofDigits] + have h := Nat.ofDigits_lt_base_pow_length (b := 256) (l := bytes.reverse.map UInt8.toNat) + (by decide) (by + intro digit hdigit + rcases List.mem_map.mp hdigit with ⟨byte, _, rfl⟩ + exact UInt8.toNat_lt byte) + simpa using h + +/-- Equal-length byte lists with equal big-endian values are equal. -/ +theorem byteListToNat_injective_of_length_eq {a b : List UInt8} + (hlength : a.length = b.length) (hvalue : byteListToNat a = byteListToNat b) : a = b := by + have hdigits : Nat.ofDigits 256 (a.reverse.map UInt8.toNat) = + Nat.ofDigits 256 (b.reverse.map UInt8.toNat) := by + simpa [byteListToNat_eq_ofDigits] using hvalue + have hmapped : a.reverse.map UInt8.toNat = b.reverse.map UInt8.toNat := by + apply Nat.ofDigits_inj_of_len_eq (b := 256) (by decide) + · simpa using hlength + · intro digit hdigit + rcases List.mem_map.mp hdigit with ⟨byte, _, rfl⟩ + exact UInt8.toNat_lt byte + · intro digit hdigit + rcases List.mem_map.mp hdigit with ⟨byte, _, rfl⟩ + exact UInt8.toNat_lt byte + · exact hdigits + have hreversed : a.reverse = b.reverse := + (List.map_inj_right fun x y h => UInt8.toNat_inj.mp h).mp hmapped + simpa using congrArg List.reverse hreversed + +/-- A byte array decodes below the cardinality determined by its length. -/ +theorem byteArrayToNat_lt (bytes : ByteArray) : + byteArrayToNat bytes < 256 ^ bytes.size := by + simpa [byteArrayToNat, ByteArray.size_data] using byteListToNat_lt bytes.data.toList + +/-- Equal-length byte arrays with equal big-endian values are equal. -/ +theorem byteArrayToNat_injective_of_size_eq {a b : ByteArray} + (hsize : a.size = b.size) (hvalue : byteArrayToNat a = byteArrayToNat b) : a = b := by + apply ByteArray.ext + apply Array.toList_inj.mp + apply byteListToNat_injective_of_length_eq + · simpa [ByteArray.size_data] using hsize + · exact hvalue + +/-- Encodes the low `size` bytes of `n` in big-endian order. -/ +def natToByteList : (size : ℕ) → ℕ → List UInt8 + | 0, _ => [] + | size + 1, n => + UInt8.ofNat (n / 256 ^ size) :: natToByteList size (n % 256 ^ size) + +/-- Parses a big-endian byte array when its length is exactly `size`. -/ +def ofByteArrayOpt (size : ℕ) (bytes : ByteArray) : Option (FixedBytes size) := + if bytes.size = size then some (ofNat size (byteArrayToNat bytes)) else none + +/-- Serializes `value` as exactly `size` bytes in big-endian order. -/ +def toByteArray (value : FixedBytes size) : ByteArray := + (natToByteList size value.toNat).toByteArray + +/-- Zero is the all-zero byte string. -/ +instance : Zero (FixedBytes size) where + zero := ofNat size 0 + +/-- One has only the least-significant bit set, when the size is nonzero. -/ +instance : One (FixedBytes size) where + one := ofNat size 1 + +/-- Natural casts retain the low `8 * size` bits. -/ +instance : NatCast (FixedBytes size) where + natCast := ofNat size + +/-- The default fixed byte string is zero. -/ +instance : Inhabited (FixedBytes size) := + ⟨0⟩ + +/-- String conversion uses exact-width hexadecimal notation. -/ +instance : ToString (FixedBytes size) where + toString := toHex + +/-- Complement flips every stored bit. -/ +instance : Complement (FixedBytes size) where + complement value := ⟨~~~value.val⟩ + +/-- Conjunction combines equal-position bits. -/ +instance : AndOp (FixedBytes size) where + and a b := ⟨a.val &&& b.val⟩ + +/-- Disjunction combines equal-position bits. -/ +instance : OrOp (FixedBytes size) where + or a b := ⟨a.val ||| b.val⟩ + +/-- Exclusive-or compares equal-position bits. -/ +instance : XorOp (FixedBytes size) where + xor a b := ⟨a.val ^^^ b.val⟩ + +/-- Equal unsigned values identify equal fixed byte strings. -/ +theorem toNat_injective : Function.Injective (toNat : FixedBytes size → ℕ) := by + intro ⟨a⟩ ⟨b⟩ h + congr + exact BitVec.eq_of_toNat_eq h + +/-- Fixed byte strings use unsigned big-endian numeric order. -/ +instance : LinearOrder (FixedBytes size) := + LinearOrder.lift' toNat toNat_injective + +/-- Extracting the value of constructed fixed bytes performs width reduction. -/ +@[simp] +theorem toNat_ofNat (size n : ℕ) : + (ofNat size n).toNat = n % modulus size := by + simp [ofNat, toNat, modulus, bitWidth] + +/-- Natural casts into fixed bytes perform width reduction. -/ +@[simp] +theorem toNat_natCast (n : ℕ) : + ((n : FixedBytes size)).toNat = n % modulus size := by + exact toNat_ofNat size n + +/-- Converting fixed bytes to a natural number and back is lossless. -/ +@[simp] +theorem ofNat_toNat (value : FixedBytes size) : ofNat size value.toNat = value := by + apply toNat_injective + rw [toNat_ofNat, Nat.mod_eq_of_lt] + exact value.val.isLt + +/-- Every `size`-byte value lies below its domain cardinality. -/ +theorem toNat_lt_modulus (value : FixedBytes size) : value.toNat < modulus size := by + exact value.val.isLt + +/-- Checked construction succeeds exactly for representable values. -/ +theorem ofNatOpt_eq_some_iff {n : ℕ} {value : FixedBytes size} : + ofNatOpt size n = some value ↔ n < modulus size ∧ ofNat size n = value := by + simp only [ofNatOpt] + split <;> simp_all + +/-- Checked construction rejects exactly the out-of-range natural numbers. -/ +@[simp] +theorem ofNatOpt_eq_none_iff (size n : ℕ) : + ofNatOpt size n = none ↔ modulus size ≤ n := by + simp [ofNatOpt] + +/-- The greatest fixed byte value is one below the domain cardinality. -/ +@[simp] +theorem toNat_max (size : ℕ) : (max size).toNat = modulus size - 1 := by + simp [max, toNat, modulus, bitWidth] + +/-- Unsigned order agrees with order on natural-number values. -/ +@[simp] +theorem le_iff_toNat_le (a b : FixedBytes size) : a ≤ b ↔ a.toNat ≤ b.toNat := + Iff.rfl + +/-- Strict order agrees with order on natural-number values. -/ +@[simp] +theorem lt_iff_toNat_lt (a b : FixedBytes size) : a < b ↔ a.toNat < b.toNat := + Iff.rfl + +/-- Equality agrees with equality of natural-number values. -/ +@[simp] +theorem toNat_inj {a b : FixedBytes size} : a.toNat = b.toNat ↔ a = b := + toNat_injective.eq_iff + +/-- Complement has the expected unsigned numeric value. -/ +@[simp] +theorem toNat_complement (value : FixedBytes size) : + (~~~value).toNat = modulus size - 1 - value.toNat := by + change (~~~value.val).toNat = modulus size - 1 - value.val.toNat + simp [modulus, bitWidth] + +/-- Bitwise conjunction agrees with conjunction of unsigned values. -/ +@[simp] +theorem toNat_and (a b : FixedBytes size) : (a &&& b).toNat = a.toNat &&& b.toNat := by + change (a.val &&& b.val).toNat = a.val.toNat &&& b.val.toNat + simp + +/-- Bitwise disjunction agrees with disjunction of unsigned values. -/ +@[simp] +theorem toNat_or (a b : FixedBytes size) : (a ||| b).toNat = a.toNat ||| b.toNat := by + change (a.val ||| b.val).toNat = a.val.toNat ||| b.val.toNat + simp + +/-- Bitwise exclusive-or agrees with exclusive-or of unsigned values. -/ +@[simp] +theorem toNat_xor (a b : FixedBytes size) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by + change (a.val ^^^ b.val).toNat = a.val.toNat ^^^ b.val.toNat + simp + +/-- Testing a fixed byte value agrees with testing its unsigned value. -/ +@[simp] +theorem testBit_eq (value : FixedBytes size) (index : ℕ) : + value.testBit index = value.toNat.testBit index := by + exact (BitVec.testBit_toNat value.val).symm + +/-- Bits beyond the fixed byte width are false. -/ +theorem testBit_of_bitWidth_le (value : FixedBytes size) (index : ℕ) + (h : bitWidth size ≤ index) : value.testBit index = false := by + exact BitVec.getLsbD_of_ge value.val index h + +/-- Reading an in-range byte uses Ethereum's most-significant-byte-first indexing. -/ +@[simp] +theorem getByte_of_index_lt (value : FixedBytes size) (index : ℕ) (h : index < size) : + value.getByte index = + UInt8.ofNat ((value.toNat / 2 ^ (8 * (size - 1 - index))) % 256) := by + simp [getByte, h] + +/-- Reading beyond the fixed byte width returns zero. -/ +@[simp] +theorem getByte_of_index_ge (value : FixedBytes size) (index : ℕ) (h : size ≤ index) : + value.getByte index = 0 := by + simp [getByte, Nat.not_lt.mpr h] + +/-- The big-endian encoder emits exactly its requested number of bytes. -/ +@[simp] +theorem natToByteList_length (size n : ℕ) : (natToByteList size n).length = size := by + induction size generalizing n with + | zero => rfl + | succ size ih => simp [natToByteList, ih] + +/-- The modulus of `size` bytes is `256 ^ size`. -/ +theorem byteBase_pow_eq_modulus (size : ℕ) : 256 ^ size = modulus size := by + simp [modulus, bitWidth, pow_mul] + +private theorem byteListToNat_natToByteList (size n acc : ℕ) (h : n < 256 ^ size) : + (natToByteList size n).foldl (fun acc byte => acc * 256 + byte.toNat) acc = + acc * 256 ^ size + n := by + induction size generalizing n acc with + | zero => + have hn : n = 0 := by simpa using h + simp [natToByteList, hn] + | succ size ih => + have hp : 0 < 256 ^ size := Nat.pow_pos (by decide) + have hq : n / 256 ^ size < 256 := by + rw [Nat.div_lt_iff_lt_mul hp] + simpa [Nat.pow_succ, Nat.mul_comm] using h + have hr : n % 256 ^ size < 256 ^ size := Nat.mod_lt _ hp + simp only [natToByteList, List.foldl_cons] + rw [ih _ _ hr, UInt8.toNat_ofNat', Nat.mod_eq_of_lt hq] + simp only [Nat.add_mul, Nat.pow_succ] + rw [Nat.mul_assoc acc 256 (256 ^ size), Nat.mul_comm 256 (256 ^ size), + ← Nat.mul_assoc acc (256 ^ size) 256, Nat.mul_comm (n / 256 ^ size) (256 ^ size), + Nat.add_assoc, Nat.div_add_mod] + +/-- Decoding a bounded value's fixed-size big-endian encoding is lossless. -/ +@[simp] +theorem byteArrayToNat_toByteArray (value : FixedBytes size) : + byteArrayToNat value.toByteArray = value.toNat := by + unfold byteArrayToNat byteListToNat toByteArray + simp only [List.toList_data_toByteArray] + have h := value.toNat_lt_modulus + rw [← byteBase_pow_eq_modulus] at h + simpa using byteListToNat_natToByteList size value.toNat 0 h + +/-- Serialization always emits exactly the declared number of bytes. -/ +@[simp] +theorem toByteArray_size (value : FixedBytes size) : value.toByteArray.size = size := by + simp [toByteArray] + +/-- Exact-size parsing has a result precisely when the input length matches. -/ +@[simp] +theorem ofByteArrayOpt_isSome (size : ℕ) (bytes : ByteArray) : + (ofByteArrayOpt size bytes).isSome = decide (bytes.size = size) := by + unfold ofByteArrayOpt + split <;> simp_all + +/-- Exact-size parsing fails precisely when the input length differs. -/ +@[simp] +theorem ofByteArrayOpt_eq_none_iff (size : ℕ) (bytes : ByteArray) : + ofByteArrayOpt size bytes = none ↔ bytes.size ≠ size := by + simp [ofByteArrayOpt] + +/-- Parsing returns a value exactly when the size and big-endian value agree. -/ +theorem ofByteArrayOpt_eq_some_iff {bytes : ByteArray} {value : FixedBytes size} : + ofByteArrayOpt size bytes = some value ↔ + bytes.size = size ∧ ofNat size (byteArrayToNat bytes) = value := by + unfold ofByteArrayOpt + split <;> simp_all + +/-- A length-valid array parses to its big-endian numeric value. -/ +theorem ofByteArrayOpt_eq_some_of_size (bytes : ByteArray) (h : bytes.size = size) : + ofByteArrayOpt size bytes = some (ofNat size (byteArrayToNat bytes)) := by + simp [ofByteArrayOpt, h] + +/-- Parsing a serialized fixed byte value is lossless. -/ +@[simp] +theorem ofByteArrayOpt_toByteArray (value : FixedBytes size) : + ofByteArrayOpt size value.toByteArray = some value := by + rw [ofByteArrayOpt_eq_some_of_size value.toByteArray value.toByteArray_size, + byteArrayToNat_toByteArray, ofNat_toNat] + +/-- Serializing any successfully parsed exact-size input reproduces that input. -/ +theorem toByteArray_ofByteArrayOpt_eq_some {bytes : ByteArray} {value : FixedBytes size} + (h : ofByteArrayOpt size bytes = some value) : value.toByteArray = bytes := by + rcases ofByteArrayOpt_eq_some_iff.mp h with ⟨hsize, hvalue⟩ + rw [← hvalue] + apply byteArrayToNat_injective_of_size_eq + · simpa using hsize.symm + · rw [byteArrayToNat_toByteArray, toNat_ofNat, Nat.mod_eq_of_lt] + rw [← byteBase_pow_eq_modulus] + simpa [hsize] using byteArrayToNat_lt bytes + +end FixedBytes + +/-! ## Generic ABI widths -/ + +/-- A generic four-byte ABI value, commonly used for function selectors. -/ +abbrev Bytes4 := FixedBytes 4 + +/-- A generic eight-byte ABI value. -/ +abbrev Bytes8 := FixedBytes 8 + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/FixedBytes/H160.lean b/LeanPool/Lean4EVM/Primitives/FixedBytes/H160.lean new file mode 100644 index 0000000000..1d20cd84a6 --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/FixedBytes/H160.lean @@ -0,0 +1,244 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.FixedBytes.Core + +/-! +# `H160` + +Nominal 160-bit hash values with exact-size serialization and type-owned laws. +-/ + +namespace Lean4EVM + +/-! ## `H160` -/ + +/-- A nominal 160-bit hash value. It is not definitionally an address. -/ +@[ext] +structure H160 where + /-- The exact 20-byte representation. -/ + bytes : FixedBytes 20 + deriving Repr, Hashable + +namespace H160 + +/-- Constructs `H160` from its exact generic representation. -/ +def ofFixedBytes (value : FixedBytes 20) : H160 := + ⟨value⟩ + +/-- Returns the exact generic representation. -/ +def toFixedBytes (value : H160) : FixedBytes 20 := + value.bytes + +/-- Constructs `H160` by retaining the low 160 bits. -/ +def ofNat (n : ℕ) : H160 := + ofFixedBytes (FixedBytes.ofNat 20 n) + +/-- Constructs `H160` only when `n` fits in 160 bits. -/ +def ofNatOpt (n : ℕ) : Option H160 := + (FixedBytes.ofNatOpt 20 n).map ofFixedBytes + +/-- Returns the unsigned natural-number value. -/ +def toNat (value : H160) : ℕ := + value.toFixedBytes.toNat + +/-- Returns the exact 20-byte hexadecimal representation. -/ +def toHex (value : H160) : String := + value.toFixedBytes.toHex + +/-- Returns the byte at `index` in big-endian order, or zero out of bounds. -/ +def getByte (value : H160) (index : ℕ) : UInt8 := + value.toFixedBytes.getByte index + +/-- Returns bit `index`, counting from the least-significant bit. -/ +def testBit (value : H160) (index : ℕ) : Bool := + value.toFixedBytes.testBit index + +/-- Parses an exact 20-byte big-endian array. -/ +def ofByteArrayOpt (bytes : ByteArray) : Option H160 := + (FixedBytes.ofByteArrayOpt 20 bytes).map ofFixedBytes + +/-- Serializes `value` as exactly 20 big-endian bytes. -/ +def toByteArray (value : H160) : ByteArray := + value.toFixedBytes.toByteArray + +/-- Returns the greatest 160-bit hash value. -/ +def max : H160 := + ofFixedBytes (FixedBytes.max 20) + +/-- Equality of generic representations identifies equal `H160` values. -/ +theorem toFixedBytes_injective : Function.Injective toFixedBytes := by + intro ⟨a⟩ ⟨b⟩ h + cases h + rfl + +/-- `H160` uses unsigned big-endian numeric order. -/ +instance : LinearOrder H160 := + LinearOrder.lift' toFixedBytes toFixedBytes_injective + +/-- Zero is the all-zero 160-bit hash. -/ +instance : Zero H160 where + zero := ofNat 0 + +/-- One has only the least-significant bit set. -/ +instance : One H160 where + one := ofNat 1 + +/-- Natural casts retain the low 160 bits. -/ +instance : NatCast H160 where + natCast := ofNat + +/-- The default `H160` is zero. -/ +instance : Inhabited H160 := + ⟨0⟩ + +/-- String conversion emits exact-width hexadecimal notation. -/ +instance : ToString H160 where + toString := toHex + +/-- Complement flips every bit of a 160-bit hash. -/ +instance : Complement H160 where + complement value := ofFixedBytes (~~~value.toFixedBytes) + +/-- Conjunction combines equal-position hash bits. -/ +instance : AndOp H160 where + and a b := ofFixedBytes (a.toFixedBytes &&& b.toFixedBytes) + +/-- Disjunction combines equal-position hash bits. -/ +instance : OrOp H160 where + or a b := ofFixedBytes (a.toFixedBytes ||| b.toFixedBytes) + +/-- Exclusive-or compares equal-position hash bits. -/ +instance : XorOp H160 where + xor a b := ofFixedBytes (a.toFixedBytes ^^^ b.toFixedBytes) + +/-- Converting from generic bytes and back is lossless. -/ +@[simp] +theorem toFixedBytes_ofFixedBytes (value : FixedBytes 20) : + (ofFixedBytes value).toFixedBytes = value := + rfl + +/-- Converting to generic bytes and back is lossless. -/ +@[simp] +theorem ofFixedBytes_toFixedBytes (value : H160) : + ofFixedBytes value.toFixedBytes = value := by + cases value + rfl + +/-- Equal unsigned values identify equal `H160` values. -/ +theorem toNat_injective : Function.Injective toNat := by + intro a b h + apply toFixedBytes_injective + exact FixedBytes.toNat_injective h + +/-- Equality agrees with equality of unsigned values. -/ +@[simp] +theorem toNat_inj {a b : H160} : a.toNat = b.toNat ↔ a = b := + toNat_injective.eq_iff + +/-- Complement is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_complement (value : H160) : + (~~~value).toFixedBytes = ~~~value.toFixedBytes := + rfl + +/-- Conjunction is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_and (a b : H160) : + (a &&& b).toFixedBytes = a.toFixedBytes &&& b.toFixedBytes := + rfl + +/-- Disjunction is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_or (a b : H160) : + (a ||| b).toFixedBytes = a.toFixedBytes ||| b.toFixedBytes := + rfl + +/-- Exclusive-or is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_xor (a b : H160) : + (a ^^^ b).toFixedBytes = a.toFixedBytes ^^^ b.toFixedBytes := + rfl + +/-- Bit testing agrees with the unsigned value. -/ +@[simp] +theorem testBit_eq (value : H160) (index : ℕ) : + value.testBit index = value.toNat.testBit index := + FixedBytes.testBit_eq value.toFixedBytes index + +/-- Bits at indices 160 and above are false. -/ +theorem testBit_of_ge (value : H160) (index : ℕ) (h : 160 ≤ index) : + value.testBit index = false := by + exact FixedBytes.testBit_of_bitWidth_le value.toFixedBytes index (by simpa [FixedBytes.bitWidth]) + +/-- Natural construction retains the low 160 bits. -/ +@[simp] +theorem toNat_ofNat (n : ℕ) : (ofNat n).toNat = n % 2 ^ 160 := by + simp [toNat, ofNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Converting through a natural number is lossless. -/ +@[simp] +theorem ofNat_toNat (value : H160) : ofNat value.toNat = value := by + apply toFixedBytes_injective + simp [ofNat, toNat] + +/-- Every `H160` value is smaller than `2 ^ 160`. -/ +theorem toNat_lt (value : H160) : value.toNat < 2 ^ 160 := by + simpa [toNat, FixedBytes.modulus, FixedBytes.bitWidth] using + FixedBytes.toNat_lt_modulus value.toFixedBytes + +/-- The greatest `H160` value is `2 ^ 160 - 1`. -/ +@[simp] +theorem toNat_max : max.toNat = 2 ^ 160 - 1 := by + simp [max, toNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Unsigned order agrees with order on natural-number values. -/ +@[simp] +theorem le_iff_toNat_le (a b : H160) : a ≤ b ↔ a.toNat ≤ b.toNat := + Iff.rfl + +/-- Strict order agrees with order on natural-number values. -/ +@[simp] +theorem lt_iff_toNat_lt (a b : H160) : a < b ↔ a.toNat < b.toNat := + Iff.rfl + +/-- Checked construction fails exactly outside the 160-bit range. -/ +@[simp] +theorem ofNatOpt_eq_none_iff (n : ℕ) : ofNatOpt n = none ↔ 2 ^ 160 ≤ n := by + simp [ofNatOpt, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Checked construction succeeds exactly for representable 160-bit values. -/ +theorem ofNatOpt_eq_some_iff {n : ℕ} {value : H160} : + ofNatOpt n = some value ↔ n < 2 ^ 160 ∧ ofNat n = value := by + simp [ofNatOpt, ofNat, FixedBytes.ofNatOpt_eq_some_iff, FixedBytes.modulus, + FixedBytes.bitWidth] + +/-- Serialization always emits 20 bytes. -/ +@[simp] +theorem toByteArray_size (value : H160) : value.toByteArray.size = 20 := by + simp [toByteArray] + +/-- Parsing succeeds exactly for 20-byte arrays. -/ +@[simp] +theorem ofByteArrayOpt_isSome (bytes : ByteArray) : + (ofByteArrayOpt bytes).isSome = decide (bytes.size = 20) := by + simp [ofByteArrayOpt] + +/-- Parsing a serialized `H160` value is lossless. -/ +@[simp] +theorem ofByteArrayOpt_toByteArray (value : H160) : + ofByteArrayOpt value.toByteArray = some value := by + simp [ofByteArrayOpt, toByteArray] + +/-- Serializing any successfully parsed `H160` input reproduces that input. -/ +theorem toByteArray_ofByteArrayOpt_eq_some {bytes : ByteArray} {value : H160} + (h : ofByteArrayOpt bytes = some value) : value.toByteArray = bytes := by + simp only [ofByteArrayOpt, Option.map_eq_some_iff] at h + rcases h with ⟨raw, hraw, rfl⟩ + exact FixedBytes.toByteArray_ofByteArrayOpt_eq_some hraw + +end H160 + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/FixedBytes/H256.lean b/LeanPool/Lean4EVM/Primitives/FixedBytes/H256.lean new file mode 100644 index 0000000000..9c4ca9bf8d --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/FixedBytes/H256.lean @@ -0,0 +1,386 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.FixedBytes.Core +import LeanPool.Lean4EVM.Primitives.FixedBytes.H160 +import LeanPool.Lean4EVM.Primitives.UInt.U256 + +/-! +# `H256` + +Nominal 256-bit hash values and explicit, lossless reinterpretation of EVM words. +-/ + +namespace Lean4EVM + +/-! ## `H256` -/ + +/-- A nominal 256-bit hash value. It is distinct from an EVM word and raw `Bytes32`. -/ +@[ext] +structure H256 where + /-- The exact 32-byte representation. -/ + bytes : FixedBytes 32 + deriving Repr, Hashable + +namespace H256 + +/-- Constructs `H256` from its exact generic representation. -/ +def ofFixedBytes (value : FixedBytes 32) : H256 := + ⟨value⟩ + +/-- Returns the exact generic representation. -/ +def toFixedBytes (value : H256) : FixedBytes 32 := + value.bytes + +/-- Constructs `H256` by retaining the low 256 bits. -/ +def ofNat (n : ℕ) : H256 := + ofFixedBytes (FixedBytes.ofNat 32 n) + +/-- Constructs `H256` only when `n` fits in 256 bits. -/ +def ofNatOpt (n : ℕ) : Option H256 := + (FixedBytes.ofNatOpt 32 n).map ofFixedBytes + +/-- Returns the unsigned natural-number value. -/ +def toNat (value : H256) : ℕ := + value.toFixedBytes.toNat + +/-- Returns the exact 32-byte hexadecimal representation. -/ +def toHex (value : H256) : String := + value.toFixedBytes.toHex + +/-- Returns the byte at `index` in big-endian order, or zero out of bounds. -/ +def getByte (value : H256) (index : ℕ) : UInt8 := + value.toFixedBytes.getByte index + +/-- Returns bit `index`, counting from the least-significant bit. -/ +def testBit (value : H256) (index : ℕ) : Bool := + value.toFixedBytes.testBit index + +/-- Parses an exact 32-byte big-endian array. -/ +def ofByteArrayOpt (bytes : ByteArray) : Option H256 := + (FixedBytes.ofByteArrayOpt 32 bytes).map ofFixedBytes + +/-- Serializes `value` as exactly 32 big-endian bytes. -/ +def toByteArray (value : H256) : ByteArray := + value.toFixedBytes.toByteArray + +/-- Returns the greatest 256-bit hash value. -/ +def max : H256 := + ofFixedBytes (FixedBytes.max 32) + +/-- Reinterprets an EVM word as a 256-bit hash. -/ +def ofU256 (value : U256) : H256 := + ofFixedBytes ⟨value.val⟩ + +/-- Reinterprets a 256-bit hash as an EVM word. -/ +def toU256 (value : H256) : U256 := + ⟨value.toFixedBytes.val⟩ + +/-- Reinterprets the last twenty bytes of a hash as `H160`, which is how Ethereum derives an +account identifier from a digest. The leading twelve bytes are discarded. -/ +def toH160 (value : H256) : H160 := + H160.ofNat value.toNat + +/-- Places a 160-bit hash in the last twenty bytes of an `H256`, leaving the leading twelve zero. -/ +def ofH160 (value : H160) : H256 := + ofNat value.toNat + +/-- Equality of generic representations identifies equal `H256` values. -/ +theorem toFixedBytes_injective : Function.Injective toFixedBytes := by + intro ⟨a⟩ ⟨b⟩ h + cases h + rfl + +/-- `H256` uses unsigned big-endian numeric order. -/ +instance : LinearOrder H256 := + LinearOrder.lift' toFixedBytes toFixedBytes_injective + +/-- Zero is the all-zero 256-bit hash. -/ +instance : Zero H256 where + zero := ofNat 0 + +/-- One has only the least-significant bit set. -/ +instance : One H256 where + one := ofNat 1 + +/-- Natural casts retain the low 256 bits. -/ +instance : NatCast H256 where + natCast := ofNat + +/-- The default `H256` is zero. -/ +instance : Inhabited H256 := + ⟨0⟩ + +/-- String conversion emits exact-width hexadecimal notation. -/ +instance : ToString H256 where + toString := toHex + +/-- Complement flips every bit of a 256-bit hash. -/ +instance : Complement H256 where + complement value := ofFixedBytes (~~~value.toFixedBytes) + +/-- Conjunction combines equal-position hash bits. -/ +instance : AndOp H256 where + and a b := ofFixedBytes (a.toFixedBytes &&& b.toFixedBytes) + +/-- Disjunction combines equal-position hash bits. -/ +instance : OrOp H256 where + or a b := ofFixedBytes (a.toFixedBytes ||| b.toFixedBytes) + +/-- Exclusive-or compares equal-position hash bits. -/ +instance : XorOp H256 where + xor a b := ofFixedBytes (a.toFixedBytes ^^^ b.toFixedBytes) + +/-- Converting from generic bytes and back is lossless. -/ +@[simp] +theorem toFixedBytes_ofFixedBytes (value : FixedBytes 32) : + (ofFixedBytes value).toFixedBytes = value := + rfl + +/-- Converting to generic bytes and back is lossless. -/ +@[simp] +theorem ofFixedBytes_toFixedBytes (value : H256) : + ofFixedBytes value.toFixedBytes = value := by + cases value + rfl + +/-- Equal unsigned values identify equal `H256` values. -/ +theorem toNat_injective : Function.Injective toNat := by + intro a b h + apply toFixedBytes_injective + exact FixedBytes.toNat_injective h + +/-- Equality agrees with equality of unsigned values. -/ +@[simp] +theorem toNat_inj {a b : H256} : a.toNat = b.toNat ↔ a = b := + toNat_injective.eq_iff + +/-- Complement is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_complement (value : H256) : + (~~~value).toFixedBytes = ~~~value.toFixedBytes := + rfl + +/-- Conjunction is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_and (a b : H256) : + (a &&& b).toFixedBytes = a.toFixedBytes &&& b.toFixedBytes := + rfl + +/-- Disjunction is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_or (a b : H256) : + (a ||| b).toFixedBytes = a.toFixedBytes ||| b.toFixedBytes := + rfl + +/-- Exclusive-or is preserved by the generic representation. -/ +@[simp] +theorem toFixedBytes_xor (a b : H256) : + (a ^^^ b).toFixedBytes = a.toFixedBytes ^^^ b.toFixedBytes := + rfl + +/-- Bit testing agrees with the unsigned value. -/ +@[simp] +theorem testBit_eq (value : H256) (index : ℕ) : + value.testBit index = value.toNat.testBit index := + FixedBytes.testBit_eq value.toFixedBytes index + +/-- Bits at indices 256 and above are false. -/ +theorem testBit_of_ge (value : H256) (index : ℕ) (h : 256 ≤ index) : + value.testBit index = false := by + exact FixedBytes.testBit_of_bitWidth_le value.toFixedBytes index (by simpa [FixedBytes.bitWidth]) + +/-- Natural construction retains the low 256 bits. -/ +@[simp] +theorem toNat_ofNat (n : ℕ) : (ofNat n).toNat = n % 2 ^ 256 := by + simp [toNat, ofNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Converting through a natural number is lossless. -/ +@[simp] +theorem ofNat_toNat (value : H256) : ofNat value.toNat = value := by + apply toFixedBytes_injective + simp [ofNat, toNat] + +/-- Every `H256` value is smaller than `2 ^ 256`. -/ +theorem toNat_lt (value : H256) : value.toNat < 2 ^ 256 := by + simpa [toNat, FixedBytes.modulus, FixedBytes.bitWidth] using + FixedBytes.toNat_lt_modulus value.toFixedBytes + +/-- The greatest `H256` value is `2 ^ 256 - 1`. -/ +@[simp] +theorem toNat_max : max.toNat = 2 ^ 256 - 1 := by + simp [max, toNat, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Unsigned order agrees with order on natural-number values. -/ +@[simp] +theorem le_iff_toNat_le (a b : H256) : a ≤ b ↔ a.toNat ≤ b.toNat := + Iff.rfl + +/-- Strict order agrees with order on natural-number values. -/ +@[simp] +theorem lt_iff_toNat_lt (a b : H256) : a < b ↔ a.toNat < b.toNat := + Iff.rfl + +/-- Checked construction fails exactly outside the 256-bit range. -/ +@[simp] +theorem ofNatOpt_eq_none_iff (n : ℕ) : ofNatOpt n = none ↔ 2 ^ 256 ≤ n := by + simp [ofNatOpt, FixedBytes.modulus, FixedBytes.bitWidth] + +/-- Checked construction succeeds exactly for representable 256-bit values. -/ +theorem ofNatOpt_eq_some_iff {n : ℕ} {value : H256} : + ofNatOpt n = some value ↔ n < 2 ^ 256 ∧ ofNat n = value := by + simp [ofNatOpt, ofNat, FixedBytes.ofNatOpt_eq_some_iff, FixedBytes.modulus, + FixedBytes.bitWidth] + +/-- Serialization always emits 32 bytes. -/ +@[simp] +theorem toByteArray_size (value : H256) : value.toByteArray.size = 32 := by + simp [toByteArray] + +/-- Parsing succeeds exactly for 32-byte arrays. -/ +@[simp] +theorem ofByteArrayOpt_isSome (bytes : ByteArray) : + (ofByteArrayOpt bytes).isSome = decide (bytes.size = 32) := by + simp [ofByteArrayOpt] + +/-- Parsing a serialized `H256` value is lossless. -/ +@[simp] +theorem ofByteArrayOpt_toByteArray (value : H256) : + ofByteArrayOpt value.toByteArray = some value := by + simp [ofByteArrayOpt, toByteArray] + +/-- Serializing any successfully parsed `H256` input reproduces that input. -/ +theorem toByteArray_ofByteArrayOpt_eq_some {bytes : ByteArray} {value : H256} + (h : ofByteArrayOpt bytes = some value) : value.toByteArray = bytes := by + simp only [ofByteArrayOpt, Option.map_eq_some_iff] at h + rcases h with ⟨raw, hraw, rfl⟩ + exact FixedBytes.toByteArray_ofByteArrayOpt_eq_some hraw + +/-- Reinterpreting a hash as a word and back is lossless. -/ +@[simp] +theorem ofU256_toU256 (value : H256) : ofU256 value.toU256 = value := by + cases value + rfl + +/-- Reinterpreting a word as a hash and back is lossless. -/ +@[simp] +theorem toU256_ofU256 (value : U256) : (ofU256 value).toU256 = value := + rfl + +/-- Word conversion preserves the unsigned value. -/ +@[simp] +theorem toNat_toU256 (value : H256) : value.toU256.toNat = value.toNat := + rfl + +/-- Hash construction from a word preserves the unsigned value. -/ +@[simp] +theorem toNat_ofU256 (value : U256) : (ofU256 value).toNat = value.toNat := + rfl + +/-- Narrowing to `H160` keeps exactly the low 160 bits. -/ +@[simp] +theorem toNat_toH160 (value : H256) : value.toH160.toNat = value.toNat % 2 ^ 160 := by + simp [toH160] + +/-- Widening a 160-bit hash preserves its unsigned value. -/ +@[simp] +theorem toNat_ofH160 (value : H160) : (ofH160 value).toNat = value.toNat := by + rw [ofH160, toNat_ofNat, Nat.mod_eq_of_lt] + exact lt_trans value.toNat_lt (by decide) + +/-- Widening a 160-bit hash and narrowing it back is lossless. -/ +@[simp] +theorem toH160_ofH160 (value : H160) : (ofH160 value).toH160 = value := by + apply H160.toNat_injective + rw [toNat_toH160, toNat_ofH160, Nat.mod_eq_of_lt value.toNat_lt] + +/-- Narrowing is a left inverse of widening, which is the source of the two facts below. -/ +theorem leftInverse_toH160_ofH160 : Function.LeftInverse toH160 ofH160 := + toH160_ofH160 + +/-- Distinct 160-bit hashes widen to distinct 256-bit hashes. -/ +theorem ofH160_injective : Function.Injective ofH160 := + leftInverse_toH160_ofH160.injective + +/-- Every 160-bit hash is the narrowing of some 256-bit hash. -/ +theorem toH160_surjective : Function.Surjective toH160 := + leftInverse_toH160_ofH160.surjective + +/-- Narrowing then widening recovers the hash exactly when its leading twelve bytes are zero. -/ +theorem ofH160_toH160_iff {value : H256} : + ofH160 value.toH160 = value ↔ value.toNat < 2 ^ 160 := by + constructor + · intro h + have hvalue := congrArg H256.toNat h + rw [toNat_ofH160, toNat_toH160] at hvalue + exact hvalue ▸ Nat.mod_lt _ (by decide) + · intro h + apply toNat_injective + rw [toNat_ofH160, toNat_toH160, Nat.mod_eq_of_lt h] + +/-- Widening changes no bit: every bit at 160 and above was already false. The simp set already +proves this from the value lemmas, so it is stated for readability rather than marked `@[simp]`. -/ +theorem testBit_ofH160 (value : H160) (index : ℕ) : + (ofH160 value).testBit index = value.testBit index := by + rw [testBit_eq, H160.testBit_eq, toNat_ofH160] + +/-- Narrowing preserves every bit below 160 and drops exactly the rest. -/ +theorem testBit_toH160 (value : H256) (index : ℕ) (h : index < 160) : + value.toH160.testBit index = value.testBit index := by + rw [H160.testBit_eq, testBit_eq, toNat_toH160, Nat.testBit_mod_two_pow] + simp [h] + +/-- Reducing modulo `2 ^ 160` leaves every byte that lies below that boundary unchanged. -/ +private theorem mod_pow_div_mod (n k : ℕ) (h : k + 8 ≤ 160) : + n % 2 ^ 160 / 2 ^ k % 256 = n / 2 ^ k % 256 := by + have hsplit : (2 : ℕ) ^ 160 = 2 ^ k * 2 ^ (160 - k) := by + rw [← pow_add]; congr 1; omega + rw [hsplit, Nat.mod_mul_right_div_self] + refine Nat.mod_mod_of_dvd _ ?_ + have h256 : (256 : ℕ) = 2 ^ 8 := by decide + rw [h256] + exact pow_dvd_pow 2 (by omega) + +/-- Byte `index` of the narrowed hash is byte `index + 12` of the original: the Ethereum rule that +an account identifier is the last twenty bytes of a digest. -/ +theorem getByte_toH160 (value : H256) (index : ℕ) (h : index < 20) : + value.toH160.getByte index = value.getByte (index + 12) := by + rw [H160.getByte, H256.getByte, FixedBytes.getByte_of_index_lt _ _ h, + FixedBytes.getByte_of_index_lt _ _ (by omega : index + 12 < 32)] + congr 1 + change value.toH160.toNat / 2 ^ (8 * (20 - 1 - index)) % 256 = + value.toNat / 2 ^ (8 * (32 - 1 - (index + 12))) % 256 + rw [toNat_toH160] + have hindex : 8 * (20 - 1 - index) = 8 * (32 - 1 - (index + 12)) := by omega + rw [hindex] + exact mod_pow_div_mod _ _ (by omega) + +/-- Widening places source byte `index` at byte `index + 12` of the result. -/ +theorem getByte_ofH160 (value : H160) (index : ℕ) (h : index < 20) : + (ofH160 value).getByte (index + 12) = value.getByte index := by + rw [H256.getByte, H160.getByte, FixedBytes.getByte_of_index_lt _ _ (by omega : index + 12 < 32), + FixedBytes.getByte_of_index_lt _ _ h] + congr 1 + change (ofH160 value).toNat / 2 ^ (8 * (32 - 1 - (index + 12))) % 256 = + value.toNat / 2 ^ (8 * (20 - 1 - index)) % 256 + rw [toNat_ofH160] + have hindex : 8 * (32 - 1 - (index + 12)) = 8 * (20 - 1 - index) := by omega + rw [hindex] + +/-- The leading twelve bytes of a widened hash are zero. -/ +theorem getByte_ofH160_of_lt (value : H160) (index : ℕ) (h : index < 12) : + (ofH160 value).getByte index = 0 := by + rw [H256.getByte, FixedBytes.getByte_of_index_lt _ _ (by omega : index < 32)] + have hzero : (ofH160 value).toNat / 2 ^ (8 * (32 - 1 - index)) = 0 := by + apply Nat.div_eq_of_lt + refine lt_of_lt_of_le (toNat_ofH160 value ▸ value.toNat_lt) ?_ + exact Nat.pow_le_pow_right (by decide) (by omega) + change UInt8.ofNat ((ofH160 value).toNat / 2 ^ (8 * (32 - 1 - index)) % 256) = 0 + rw [hzero] + rfl + +end H256 + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/UInt.lean b/LeanPool/Lean4EVM/Primitives/UInt.lean new file mode 100644 index 0000000000..6d6d686633 --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/UInt.lean @@ -0,0 +1,15 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.UInt.U256 + +/-! +# Fixed-width unsigned integers + +Public entry point for the fixed-width integer family. `Core` contains the shared representation, +executable arithmetic, and generic laws. `U64`, `U128`, and `U256` keep width-specific operations, +conversions, and theorems beside their owning type. The import order is intentionally widening: +`Core → U64 → U128 → U256`, which keeps cross-width conversions acyclic. +-/ diff --git a/LeanPool/Lean4EVM/Primitives/UInt/Core.lean b/LeanPool/Lean4EVM/Primitives/UInt/Core.lean new file mode 100644 index 0000000000..4d450f3d75 --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/UInt/Core.lean @@ -0,0 +1,957 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import Mathlib.Data.BitVec + +/-! +# Fixed-width unsigned integer core + +This module owns `FixedUInt`, its executable modular arithmetic, the shared proof API, and the +nominal structures `U64`, `U128`, and `U256`. The concrete structures live here so width-specific +modules can depend on one acyclic representation layer. Type-owned operations and conversions are +defined in `U64`, `U128`, and `U256` modules. +-/ + +namespace Lean4EVM + +/-- Representation interface shared by nominal fixed-width unsigned integer types. -/ +class FixedUInt (α : Type) (width : outParam ℕ) where + /-- Returns the fixed-width representation. -/ + toBitVec : α → BitVec width + /-- Constructs a value from its exact-width representation. -/ + ofBitVec : BitVec width → α + /-- Reconstructing a value from its representation is lossless. -/ + of_to : ∀ value, ofBitVec (toBitVec value) = value + /-- Extracting the representation of a constructed value is lossless. -/ + to_of : ∀ bits, toBitVec (ofBitVec bits) = bits + +namespace FixedUInt + +variable {α : Type} {width : ℕ} [FixedUInt α width] + +/-- Returns the modulus `2 ^ width` of a fixed-width arithmetic. -/ +def modulus (width : ℕ) : ℕ := + 2 ^ width + +/-- Constructs a value by retaining the low `width` bits of `n`. -/ +def ofNat (n : ℕ) : α := + FixedUInt.ofBitVec (BitVec.ofNat width n) + +/-- Constructs a value when `n` fits in `width` bits. -/ +def ofNatOpt (n : ℕ) : Option α := + if n < modulus width then some (ofNat n) else none + +/-- Constructs a value from an integer using two's-complement wrapping. -/ +def ofInt (n : ℤ) : α := + FixedUInt.ofBitVec (BitVec.ofInt width n) + +/-- Constructs a value when `n` is nonnegative and fits in `width` bits. -/ +def ofIntOpt (n : ℤ) : Option α := + if 0 ≤ n ∧ n < (modulus width : ℤ) then some (ofNat n.toNat) else none + +/-- Returns the unsigned natural-number value. -/ +def toNat (value : α) : ℕ := + (FixedUInt.toBitVec value).toNat + +/-- Reinterprets the bit pattern as a signed two's-complement integer. -/ +def toSignedInt (value : α) : ℤ := + (FixedUInt.toBitVec value).toInt + +/-- Returns the exact-width hexadecimal representation. -/ +def toHex (value : α) : String := + "0x" ++ (FixedUInt.toBitVec value).toHex + +/-- Returns the greatest representable value. -/ +def max : α := + FixedUInt.ofBitVec (BitVec.allOnes width) + +/-- Returns `true` exactly when unsigned addition overflows. -/ +def addOverflow (a b : α) : Bool := + decide (modulus width ≤ toNat a + toNat b) + +/-- Returns `true` exactly when unsigned subtraction underflows. -/ +def subOverflow (a b : α) : Bool := + decide (toNat a < toNat b) + +/-- Returns `true` exactly when unsigned multiplication overflows. -/ +def mulOverflow (a b : α) : Bool := + decide (modulus width ≤ toNat a * toNat b) + +private def powStep (base : α) (bit : Bool) (result : α) : α := + let squared := FixedUInt.ofBitVec + (FixedUInt.toBitVec result * FixedUInt.toBitVec result) + if bit then + FixedUInt.ofBitVec (FixedUInt.toBitVec squared * FixedUInt.toBitVec base) + else + squared + +/-- Raises `base` to `exponent` by structural binary exponentiation. -/ +def pow (base : α) (exponent : ℕ) : α := + Nat.binaryRec (ofNat 1) (fun bit _ result => powStep base bit result) exponent + +/-- Adds two values modulo `2 ^ width`. -/ +def wrappingAdd (a b : α) : α := + FixedUInt.ofBitVec (FixedUInt.toBitVec a + FixedUInt.toBitVec b) + +/-- Subtracts two values modulo `2 ^ width`. -/ +def wrappingSub (a b : α) : α := + FixedUInt.ofBitVec (FixedUInt.toBitVec a - FixedUInt.toBitVec b) + +/-- Multiplies two values modulo `2 ^ width`. -/ +def wrappingMul (a b : α) : α := + FixedUInt.ofBitVec (FixedUInt.toBitVec a * FixedUInt.toBitVec b) + +/-- Negates a value modulo `2 ^ width`. -/ +def wrappingNeg (value : α) : α := + FixedUInt.ofBitVec (-FixedUInt.toBitVec value) + +/-- Raises a value to a natural exponent modulo `2 ^ width`. -/ +def wrappingPow (base : α) (exponent : ℕ) : α := + pow base exponent + +/-- Returns a wrapping sum together with its overflow flag. -/ +def overflowingAdd (a b : α) : α × Bool := + (wrappingAdd a b, addOverflow a b) + +/-- Returns a wrapping difference together with its underflow flag. -/ +def overflowingSub (a b : α) : α × Bool := + (wrappingSub a b, subOverflow a b) + +/-- Returns a wrapping product together with its overflow flag. -/ +def overflowingMul (a b : α) : α × Bool := + (wrappingMul a b, mulOverflow a b) + +/-- Adds two values when the exact sum fits. -/ +def checkedAdd (a b : α) : Option α := + if addOverflow a b then none else some (wrappingAdd a b) + +/-- Subtracts two values when the exact difference is nonnegative. -/ +def checkedSub (a b : α) : Option α := + if subOverflow a b then none else some (wrappingSub a b) + +/-- Multiplies two values when the exact product fits. -/ +def checkedMul (a b : α) : Option α := + if mulOverflow a b then none else some (wrappingMul a b) + +/-- Divides two values when the divisor is nonzero. -/ +def checkedDiv (a b : α) : Option α := + if toNat b = 0 then none + else some (ofNat (toNat a / toNat b)) + +/-- Computes a remainder when the divisor is nonzero. -/ +def checkedMod (a b : α) : Option α := + if toNat b = 0 then none + else some (ofNat (toNat a % toNat b)) + +/-- Returns quotient and remainder when the divisor is nonzero. -/ +def checkedDivMod (a b : α) : Option (α × α) := + match checkedDiv a b, checkedMod a b with + | some quotient, some remainder => some (quotient, remainder) + | _, _ => none + +/-- Adds two values and clamps overflow to the greatest value. -/ +def saturatingAdd (a b : α) : α := + if addOverflow a b then max else wrappingAdd a b + +/-- Subtracts two values and clamps underflow to zero. -/ +def saturatingSub (a b : α) : α := + if subOverflow a b then ofNat 0 else wrappingSub a b + +/-- Multiplies two values and clamps overflow to the greatest value. -/ +def saturatingMul (a b : α) : α := + if mulOverflow a b then max else wrappingMul a b + +/-- Returns the number of leading zero bits. -/ +def leadingZeros (value : α) : ℕ := + (FixedUInt.toBitVec value).clz.toNat + +/-- Returns the number of trailing zero bits. -/ +def trailingZeros (value : α) : ℕ := + (FixedUInt.toBitVec value).ctz.toNat + +/-- Returns the number of set bits. -/ +def countOnes (value : α) : ℕ := + (FixedUInt.toBitVec value).cpop.toNat + +/-- Returns bit `index`, counting from the least-significant bit. -/ +def testBit (value : α) (index : ℕ) : Bool := + (FixedUInt.toBitVec value).getLsbD index + +/-- Rotates the bit pattern left by `amount` modulo the word width. -/ +def rotateLeft (value : α) (amount : ℕ) : α := + FixedUInt.ofBitVec ((FixedUInt.toBitVec value).rotateLeft amount) + +/-- Rotates the bit pattern right by `amount` modulo the word width. -/ +def rotateRight (value : α) (amount : ℕ) : α := + FixedUInt.ofBitVec ((FixedUInt.toBitVec value).rotateRight amount) + +/-- Zero is the all-zero word. -/ +instance : Zero α where + zero := ofNat 0 + +/-- One is the word with only its least-significant bit set. -/ +instance : One α where + one := ofNat 1 + +/-- Natural casts wrap modulo the word modulus. -/ +instance : NatCast α where + natCast := ofNat + +/-- Integer casts use two's-complement wrapping. -/ +instance : IntCast α where + intCast := ofInt + +/-- Natural scalar multiplication is computed modulo the word modulus. -/ +instance : SMul ℕ α where + smul n value := + FixedUInt.ofBitVec (n • FixedUInt.toBitVec value) + +/-- Integer scalar multiplication is computed modulo the word modulus. -/ +instance : SMul ℤ α where + smul n value := + FixedUInt.ofBitVec (n • FixedUInt.toBitVec value) + +/-- The default fixed-width value is zero. -/ +instance : Inhabited α := + ⟨ofNat 0⟩ + +/-- String conversion uses exact-width hexadecimal notation. -/ +instance : ToString α where + toString := toHex + +/-- Addition wraps at the word width. -/ +instance : Add α where + add := wrappingAdd + +/-- Subtraction wraps at the word width. -/ +instance : Sub α where + sub := wrappingSub + +/-- Multiplication wraps at the word width. -/ +instance : Mul α where + mul := wrappingMul + +/-- Negation wraps at the word width. -/ +instance : Neg α where + neg := wrappingNeg + +/-- Natural powers use wrapping multiplication. -/ +instance : Pow α ℕ where + pow := wrappingPow + +/-- Complement flips every bit in the word. -/ +instance : Complement α where + complement value := FixedUInt.ofBitVec (~~~FixedUInt.toBitVec value) + +/-- Conjunction combines equal-position bits. -/ +instance : AndOp α where + and a b := FixedUInt.ofBitVec (FixedUInt.toBitVec a &&& FixedUInt.toBitVec b) + +/-- Disjunction combines equal-position bits. -/ +instance : OrOp α where + or a b := FixedUInt.ofBitVec (FixedUInt.toBitVec a ||| FixedUInt.toBitVec b) + +/-- Exclusive-or compares equal-position bits. -/ +instance : XorOp α where + xor a b := FixedUInt.ofBitVec (FixedUInt.toBitVec a ^^^ FixedUInt.toBitVec b) + +/-- Left shift returns zero before evaluating an amount at least the word width. -/ +instance : HShiftLeft α ℕ α where + hShiftLeft value amount := + if amount < width then + FixedUInt.ofBitVec (FixedUInt.toBitVec value <<< amount) + else + ofNat 0 + +/-- Logical right shift fills vacated bits with zero. -/ +instance : HShiftRight α ℕ α where + hShiftRight value amount := FixedUInt.ofBitVec (FixedUInt.toBitVec value >>> amount) + +@[simp] +theorem toBitVec_ofBitVec (bits : BitVec width) : + FixedUInt.toBitVec (FixedUInt.ofBitVec bits : α) = bits := + FixedUInt.to_of bits + +@[simp] +theorem ofBitVec_toBitVec (value : α) : + FixedUInt.ofBitVec (FixedUInt.toBitVec value) = value := + FixedUInt.of_to value + +/-- Equality follows from equality of exact-width representations. -/ +theorem toBitVec_injective : Function.Injective (FixedUInt.toBitVec : α → BitVec width) := by + intro a b h + rw [← ofBitVec_toBitVec a, ← ofBitVec_toBitVec b, h] + +/-- Binary exponentiation agrees with exponentiation of the underlying bit vector. -/ +theorem toBitVec_pow (base : α) (exponent : ℕ) : + FixedUInt.toBitVec (pow base exponent) = FixedUInt.toBitVec base ^ exponent := by + induction exponent using Nat.binaryRec with + | zero => simp [pow, ofNat] + | bit bit n ih => + rw [pow, Nat.binaryRec_eq] + · change FixedUInt.toBitVec (powStep base bit (pow base n)) = _ + cases bit + · simp only [powStep, Bool.false_eq_true, ↓reduceIte, toBitVec_ofBitVec, ih] + rw [← pow_add] + congr 1 + simp [Nat.bit] + omega + · simp only [powStep, ↓reduceIte, toBitVec_ofBitVec, ih] + rw [← pow_add, ← pow_succ] + congr 1 + simp [Nat.bit] + omega + · left + apply toBitVec_injective + simp [powStep, ofNat] + +/-- Equality follows from equality of unsigned values. -/ +theorem toNat_injective : Function.Injective (toNat : α → ℕ) := by + intro a b h + have hbits : FixedUInt.toBitVec a = FixedUInt.toBitVec b := + BitVec.eq_of_toNat_eq h + calc + a = FixedUInt.ofBitVec (FixedUInt.toBitVec a) := (ofBitVec_toBitVec a).symm + _ = FixedUInt.ofBitVec (FixedUInt.toBitVec b) := congrArg FixedUInt.ofBitVec hbits + _ = b := ofBitVec_toBitVec b + +/-- Wrapped natural construction is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_ofNat (n : ℕ) : + FixedUInt.toBitVec (ofNat n : α) = BitVec.ofNat width n := by + simp [ofNat] + +/-- Zero is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_zero : FixedUInt.toBitVec (0 : α) = 0 := by + change FixedUInt.toBitVec (ofNat 0 : α) = 0 + simp + +/-- One is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_one : FixedUInt.toBitVec (1 : α) = 1 := by + change FixedUInt.toBitVec (ofNat 1 : α) = 1 + simp + +/-- Natural casts are preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_natCast (n : ℕ) : + FixedUInt.toBitVec (n : α) = (n : BitVec width) := by + change FixedUInt.toBitVec (ofNat n : α) = BitVec.ofNat width n + simp + +/-- Integer casts are preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_intCast (n : ℤ) : + FixedUInt.toBitVec (n : α) = (n : BitVec width) := by + change FixedUInt.toBitVec (ofInt n : α) = BitVec.ofInt width n + simp [ofInt] + +/-- Fixed-width values inherit the unsigned linear order of natural numbers. -/ +instance : LinearOrder α := + LinearOrder.lift' toNat toNat_injective + +/-- Two fixed-width values are equal exactly when their unsigned values are equal. -/ +@[simp] +theorem toNat_inj {a b : α} : toNat a = toNat b ↔ a = b := + toNat_injective.eq_iff + +/-- Converting `n` with wrapping retains its residue modulo `2 ^ width`. -/ +@[simp] +theorem toNat_ofNat (n : ℕ) : + toNat (ofNat n : α) = n % modulus width := by + simp [toNat, ofNat, modulus] + +/-- Natural casts reduce modulo the word modulus. -/ +theorem toNat_natCast (n : ℕ) : + toNat (n : α) = n % modulus width := by + change toNat (ofNat n : α) = _ + exact toNat_ofNat n + +/-- Numeric literals at least two reduce modulo the word modulus. -/ +theorem toNat_ofNat_lit (n : ℕ) [n.AtLeastTwo] : + toNat (ofNat(n) : α) = n % modulus width := by + exact toNat_natCast n + +/-- Binary exponentiation computes natural exponentiation modulo the word modulus. -/ +@[simp] +theorem toNat_pow (base : α) (exponent : ℕ) : + toNat (pow base exponent) = toNat base ^ exponent % modulus width := by + unfold toNat + rw [toBitVec_pow] + induction exponent with + | zero => simp [modulus] + | succ exponent ih => + rw [pow_succ, BitVec.toNat_mul, ih, Nat.pow_succ] + simp [modulus, Nat.mul_mod] + +/-- Wrapped integer construction agrees with reduction modulo the word modulus. -/ +@[simp] +theorem toNat_ofInt (n : ℤ) : + toNat (ofInt n : α) = (n % (modulus width : ℤ)).toNat := by + simp [toNat, ofInt, modulus] + +/-- Signed reinterpretation of an integer is its balanced residue at the word modulus. -/ +@[simp] +theorem toSignedInt_ofInt (n : ℤ) : + toSignedInt (ofInt n : α) = n.bmod (modulus width) := by + simp [toSignedInt, ofInt, modulus] + +/-- The unsigned value of zero is zero. -/ +@[simp] +theorem toNat_zero : toNat (0 : α) = 0 := by + simp [toNat] + +/-- The unsigned value of one is one for every nonempty word. -/ +@[simp] +theorem toNat_one (h : 0 < width := by omega) : toNat (1 : α) = 1 := by + change toNat (ofNat 1 : α) = 1 + rw [toNat_ofNat, Nat.mod_eq_of_lt] + simpa [modulus] using Nat.one_lt_two_pow (Nat.ne_of_gt h) + +/-- Signed reinterpretation maps the zero word to zero. -/ +@[simp] +theorem toSignedInt_zero : toSignedInt (0 : α) = 0 := by + simp [toSignedInt] + +/-- Converting a fixed-width value to a natural and back is lossless. -/ +@[simp] +theorem ofNat_toNat (value : α) : ofNat (toNat value) = value := by + apply toNat_injective + rw [toNat_ofNat, Nat.mod_eq_of_lt] + exact (FixedUInt.toBitVec value).isLt + +/-- Every unsigned value is smaller than its word modulus. -/ +theorem toNat_lt_modulus (value : α) : toNat value < modulus width := + (FixedUInt.toBitVec value).isLt + +/-- Reduction modulo a nonzero word yields a residue representable at the same width. -/ +theorem toNat_ofNat_mod (n : ℕ) {value : α} (hvalue : value ≠ 0) : + toNat (ofNat (n % toNat value) : α) = n % toNat value := by + have hpositive : 0 < toNat value := Nat.pos_of_ne_zero fun h => + hvalue (toNat_injective (h.trans toNat_zero.symm)) + rw [toNat_ofNat, Nat.mod_eq_of_lt ((Nat.mod_lt n hpositive).trans (toNat_lt_modulus value))] + +/-- Checked natural construction succeeds exactly for representable values. -/ +theorem ofNatOpt_eq_some_iff {n : ℕ} {value : α} : + ofNatOpt n = some value ↔ n < modulus width ∧ ofNat n = value := by + simp only [ofNatOpt] + split <;> simp_all + +/-- Checked natural construction rejects exactly the out-of-range values. -/ +@[simp] +theorem ofNatOpt_eq_none_iff (n : ℕ) : + (ofNatOpt n : Option α) = none ↔ modulus width ≤ n := by + simp [ofNatOpt] + +/-- Checked integer construction succeeds exactly for nonnegative representable values. -/ +theorem ofIntOpt_eq_some_iff {n : ℤ} {value : α} : + ofIntOpt n = some value ↔ + 0 ≤ n ∧ n < (modulus width : ℤ) ∧ ofNat n.toNat = value := by + simp only [ofIntOpt] + split <;> simp_all + +/-- Checked integer construction rejects negative and out-of-range values. -/ +@[simp] +theorem ofIntOpt_eq_none_iff (n : ℤ) : + (ofIntOpt n : Option α) = none ↔ + n < 0 ∨ (modulus width : ℤ) ≤ n := by + simp only [ofIntOpt] + split_ifs with h + · simp only [false_iff] + exact not_or_intro (not_lt.mpr h.1) (not_le.mpr h.2) + · simp only [true_iff] + rcases not_and_or.mp h with hnegative | hlarge + · exact Or.inl (lt_of_not_ge hnegative) + · exact Or.inr (le_of_not_gt hlarge) + +/-- The greatest fixed-width value is `2 ^ width - 1`. -/ +@[simp] +theorem toNat_max : toNat (max : α) = modulus width - 1 := by + simp [toNat, max, modulus] + +/-- Addition is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_add (a b : α) : + FixedUInt.toBitVec (a + b) = FixedUInt.toBitVec a + FixedUInt.toBitVec b := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (FixedUInt.toBitVec a + FixedUInt.toBitVec b)) = _ + simp + +/-- Subtraction is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_sub (a b : α) : + FixedUInt.toBitVec (a - b) = FixedUInt.toBitVec a - FixedUInt.toBitVec b := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (FixedUInt.toBitVec a - FixedUInt.toBitVec b)) = _ + simp + +/-- Multiplication is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_mul (a b : α) : + FixedUInt.toBitVec (a * b) = FixedUInt.toBitVec a * FixedUInt.toBitVec b := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (FixedUInt.toBitVec a * FixedUInt.toBitVec b)) = _ + simp + +/-- Negation is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_neg (value : α) : + FixedUInt.toBitVec (-value) = -FixedUInt.toBitVec value := by + change FixedUInt.toBitVec (FixedUInt.ofBitVec (-FixedUInt.toBitVec value)) = _ + simp + +/-- Natural scalar multiplication is preserved by the exact-width representation. -/ +theorem toBitVec_nsmul (n : ℕ) (value : α) : + FixedUInt.toBitVec (n • value) = n • FixedUInt.toBitVec value := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (n • FixedUInt.toBitVec value)) = _ + simp + +/-- Integer scalar multiplication is preserved by the exact-width representation. -/ +theorem toBitVec_zsmul (n : ℤ) (value : α) : + FixedUInt.toBitVec (n • value) = n • FixedUInt.toBitVec value := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (n • FixedUInt.toBitVec value)) = _ + simp + +/-- Wrapping arithmetic forms a commutative ring modulo `2 ^ width`. -/ +instance : CommRing α := + Function.Injective.commRing FixedUInt.toBitVec toBitVec_injective + toBitVec_zero toBitVec_one toBitVec_add toBitVec_mul toBitVec_neg toBitVec_sub + toBitVec_nsmul toBitVec_zsmul toBitVec_pow toBitVec_natCast toBitVec_intCast + +/-- Addition wraps modulo the word modulus. -/ +@[simp] +theorem toNat_add (a b : α) : + toNat (a + b) = (toNat a + toNat b) % modulus width := + by + change toNat (wrappingAdd a b) = (toNat a + toNat b) % modulus width + unfold toNat wrappingAdd modulus + rw [toBitVec_ofBitVec] + rfl + +/-- Subtraction wraps modulo the word modulus. -/ +@[simp] +theorem toNat_sub (a b : α) : + toNat (a - b) = ((modulus width - toNat b) + toNat a) % modulus width := + by + change toNat (wrappingSub a b) = + ((modulus width - toNat b) + toNat a) % modulus width + unfold toNat wrappingSub modulus + rw [toBitVec_ofBitVec] + rfl + +/-- Multiplication wraps modulo the word modulus. -/ +@[simp] +theorem toNat_mul (a b : α) : + toNat (a * b) = (toNat a * toNat b) % modulus width := + by + change toNat (wrappingMul a b) = (toNat a * toNat b) % modulus width + unfold toNat wrappingMul modulus + rw [toBitVec_ofBitVec] + rfl + +/-- Negation wraps modulo the word modulus. -/ +@[simp] +theorem toNat_neg (value : α) : + toNat (-value) = (modulus width - toNat value) % modulus width := by + change toNat (wrappingNeg value) = + (modulus width - toNat value) % modulus width + unfold toNat wrappingNeg modulus + rw [toBitVec_ofBitVec] + exact BitVec.toNat_neg _ + +/-- Bitwise complement is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_complement (value : α) : + FixedUInt.toBitVec (~~~value) = ~~~FixedUInt.toBitVec value := by + change FixedUInt.toBitVec (FixedUInt.ofBitVec (~~~FixedUInt.toBitVec value)) = _ + simp + +/-- Bitwise conjunction is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_and (a b : α) : + FixedUInt.toBitVec (a &&& b) = FixedUInt.toBitVec a &&& FixedUInt.toBitVec b := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (FixedUInt.toBitVec a &&& FixedUInt.toBitVec b)) = _ + simp + +/-- Bitwise disjunction is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_or (a b : α) : + FixedUInt.toBitVec (a ||| b) = FixedUInt.toBitVec a ||| FixedUInt.toBitVec b := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (FixedUInt.toBitVec a ||| FixedUInt.toBitVec b)) = _ + simp + +/-- Bitwise exclusive-or is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_xor (a b : α) : + FixedUInt.toBitVec (a ^^^ b) = FixedUInt.toBitVec a ^^^ FixedUInt.toBitVec b := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (FixedUInt.toBitVec a ^^^ FixedUInt.toBitVec b)) = _ + simp + +/-- Left shift is preserved below the width and is zero for every larger amount. -/ +@[simp] +theorem toBitVec_shiftLeft (value : α) (amount : ℕ) : + FixedUInt.toBitVec (value <<< amount) = + if amount < width then FixedUInt.toBitVec value <<< amount else 0 := by + simp only [HShiftLeft.hShiftLeft] + split <;> simp_all [ofNat] + +/-- Logical right shift is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_shiftRight (value : α) (amount : ℕ) : + FixedUInt.toBitVec (value >>> amount) = FixedUInt.toBitVec value >>> amount := by + change FixedUInt.toBitVec + (FixedUInt.ofBitVec (FixedUInt.toBitVec value >>> amount)) = _ + simp + +/-- A left shift by at least the word width is zero without evaluating a huge shift. -/ +@[simp] +theorem shiftLeft_eq_zero_of_width_le (value : α) (amount : ℕ) (h : width ≤ amount) : + value <<< amount = 0 := by + change value <<< amount = ofNat 0 + apply toBitVec_injective + simp [Nat.not_lt.mpr h] + +/-- A logical right shift by at least the word width is zero. -/ +@[simp] +theorem shiftRight_eq_zero_of_width_le (value : α) (amount : ℕ) (h : width ≤ amount) : + value >>> amount = 0 := by + change value >>> amount = ofNat 0 + apply toBitVec_injective + simp [BitVec.ushiftRight_eq_zero h] + +/-- Bitwise complement has the expected unsigned value. -/ +@[simp] +theorem toNat_complement (value : α) : + toNat (~~~value) = modulus width - 1 - toNat value := by + simp [toNat, modulus] + +/-- Bitwise conjunction agrees with natural-number conjunction. -/ +@[simp] +theorem toNat_and (a b : α) : toNat (a &&& b) = toNat a &&& toNat b := by + simp [toNat] + +/-- Bitwise disjunction agrees with natural-number disjunction. -/ +@[simp] +theorem toNat_or (a b : α) : toNat (a ||| b) = toNat a ||| toNat b := by + simp [toNat] + +/-- Bitwise exclusive-or agrees with natural-number exclusive-or. -/ +@[simp] +theorem toNat_xor (a b : α) : toNat (a ^^^ b) = toNat a ^^^ toNat b := by + simp [toNat] + +/-- Testing a conjunction tests both operands at the same bit. -/ +@[simp] +theorem testBit_and (a b : α) (index : ℕ) : + testBit (a &&& b) index = (testBit a index && testBit b index) := by + simp [testBit] + +/-- Testing a disjunction tests either operand at the same bit. -/ +@[simp] +theorem testBit_or (a b : α) (index : ℕ) : + testBit (a ||| b) index = (testBit a index || testBit b index) := by + simp [testBit] + +/-- Testing an exclusive-or compares the operand bits. -/ +@[simp] +theorem testBit_xor (a b : α) (index : ℕ) : + testBit (a ^^^ b) index = xor (testBit a index) (testBit b index) := by + simp [testBit] + +/-- Complement negates in-range bits and leaves out-of-range bits false. -/ +@[simp] +theorem testBit_complement (value : α) (index : ℕ) : + testBit (~~~value) index = + (decide (index < width) && !testBit value index) := by + simp [testBit] + +/-- A bounded left shift agrees with natural-number shifting modulo the word modulus. -/ +theorem toNat_shiftLeft_of_lt (value : α) (amount : ℕ) (h : amount < width) : + toNat (value <<< amount) = (toNat value <<< amount) % modulus width := by + simp [toNat, h, modulus] + +/-- Logical right shift agrees with natural-number shifting. -/ +@[simp] +theorem toNat_shiftRight (value : α) (amount : ℕ) : + toNat (value >>> amount) = toNat value >>> amount := by + simp [toNat] + +/-- Left rotation is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_rotateLeft (value : α) (amount : ℕ) : + FixedUInt.toBitVec (rotateLeft value amount) = + (FixedUInt.toBitVec value).rotateLeft amount := by + simp [rotateLeft] + +/-- Right rotation is preserved by the exact-width representation. -/ +@[simp] +theorem toBitVec_rotateRight (value : α) (amount : ℕ) : + FixedUInt.toBitVec (rotateRight value amount) = + (FixedUInt.toBitVec value).rotateRight amount := by + simp [rotateRight] + +/-- Left rotation depends only on the amount modulo the word width. -/ +theorem rotateLeft_mod (value : α) (amount : ℕ) : + rotateLeft value (amount % width) = rotateLeft value amount := by + apply toBitVec_injective + simp [BitVec.rotateLeft_mod_eq_rotateLeft] + +/-- Right rotation depends only on the amount modulo the word width. -/ +theorem rotateRight_mod (value : α) (amount : ℕ) : + rotateRight value (amount % width) = rotateRight value amount := by + apply toBitVec_injective + simp [BitVec.rotateRight_mod_eq_rotateRight] + +/-- The overflow flag for addition has its stated arithmetic meaning. -/ +@[simp] +theorem addOverflow_eq_true (a b : α) : + addOverflow a b = true ↔ modulus width ≤ toNat a + toNat b := by + simp [addOverflow] + +/-- The underflow flag for subtraction has its stated arithmetic meaning. -/ +@[simp] +theorem subOverflow_eq_true (a b : α) : + subOverflow a b = true ↔ toNat a < toNat b := by + simp [subOverflow] + +/-- The overflow flag for multiplication has its stated arithmetic meaning. -/ +@[simp] +theorem mulOverflow_eq_true (a b : α) : + mulOverflow a b = true ↔ modulus width ≤ toNat a * toNat b := by + simp [mulOverflow] + +/-- The value component of overflowing addition is the wrapping sum. -/ +@[simp] +theorem overflowingAdd_fst (a b : α) : (overflowingAdd a b).1 = a + b := + rfl + +/-- The flag component of overflowing addition records exact overflow. -/ +@[simp] +theorem overflowingAdd_snd (a b : α) : + (overflowingAdd a b).2 = decide (modulus width ≤ toNat a + toNat b) := + rfl + +/-- The value component of overflowing subtraction is the wrapping difference. -/ +@[simp] +theorem overflowingSub_fst (a b : α) : (overflowingSub a b).1 = a - b := + rfl + +/-- The flag component of overflowing subtraction records exact underflow. -/ +@[simp] +theorem overflowingSub_snd (a b : α) : + (overflowingSub a b).2 = decide (toNat a < toNat b) := + rfl + +/-- The value component of overflowing multiplication is the wrapping product. -/ +@[simp] +theorem overflowingMul_fst (a b : α) : (overflowingMul a b).1 = a * b := + rfl + +/-- The flag component of overflowing multiplication records exact overflow. -/ +@[simp] +theorem overflowingMul_snd (a b : α) : + (overflowingMul a b).2 = decide (modulus width ≤ toNat a * toNat b) := + rfl + +/-- Checked addition succeeds when the exact sum fits. -/ +theorem checkedAdd_eq_some_of_lt (a b : α) + (h : toNat a + toNat b < modulus width) : + checkedAdd a b = some (a + b) := by + change checkedAdd a b = some (wrappingAdd a b) + simp [checkedAdd, addOverflow, Nat.not_le.mpr h] + +/-- Checked addition fails exactly on overflow. -/ +@[simp] +theorem checkedAdd_eq_none_iff (a b : α) : + checkedAdd a b = none ↔ modulus width ≤ toNat a + toNat b := by + simp [checkedAdd, addOverflow] + +/-- Checked subtraction succeeds when the result is nonnegative. -/ +theorem checkedSub_eq_some_of_le (a b : α) (h : toNat b ≤ toNat a) : + checkedSub a b = some (a - b) := by + change checkedSub a b = some (wrappingSub a b) + simp [checkedSub, subOverflow, Nat.not_lt.mpr h] + +/-- Checked subtraction fails exactly on underflow. -/ +@[simp] +theorem checkedSub_eq_none_iff (a b : α) : + checkedSub a b = none ↔ toNat a < toNat b := by + simp [checkedSub, subOverflow] + +/-- Checked multiplication succeeds when the exact product fits. -/ +theorem checkedMul_eq_some_of_lt (a b : α) + (h : toNat a * toNat b < modulus width) : + checkedMul a b = some (a * b) := by + change checkedMul a b = some (wrappingMul a b) + simp [checkedMul, mulOverflow, Nat.not_le.mpr h] + +/-- Checked multiplication fails exactly on overflow. -/ +@[simp] +theorem checkedMul_eq_none_iff (a b : α) : + checkedMul a b = none ↔ modulus width ≤ toNat a * toNat b := by + simp [checkedMul, mulOverflow] + +/-- Checked division fails exactly for a zero divisor. -/ +@[simp] +theorem checkedDiv_eq_none_iff (a b : α) : checkedDiv a b = none ↔ toNat b = 0 := by + simp [checkedDiv] + +/-- Checked remainder fails exactly for a zero divisor. -/ +@[simp] +theorem checkedMod_eq_none_iff (a b : α) : checkedMod a b = none ↔ toNat b = 0 := by + simp [checkedMod] + +/-- Checked division returns the natural-number quotient for a nonzero divisor. -/ +theorem checkedDiv_eq_some_of_ne_zero (a b : α) (h : toNat b ≠ 0) : + checkedDiv a b = some (ofNat (toNat a / toNat b)) := by + simp [checkedDiv, h] + +/-- Checked remainder returns the natural-number remainder for a nonzero divisor. -/ +theorem checkedMod_eq_some_of_ne_zero (a b : α) (h : toNat b ≠ 0) : + checkedMod a b = some (ofNat (toNat a % toNat b)) := by + simp [checkedMod, h] + +/-- Checked quotient and remainder fail exactly for a zero divisor. -/ +@[simp] +theorem checkedDivMod_eq_none_iff (a b : α) : + checkedDivMod a b = none ↔ toNat b = 0 := by + by_cases h : toNat b = 0 + · simp [checkedDivMod, checkedDiv, checkedMod, h] + · simp [checkedDivMod, checkedDiv, checkedMod, h] + +/-- Checked quotient and remainder expose the Euclidean decomposition. -/ +theorem checkedDivMod_eq_some_of_ne_zero (a b : α) (h : toNat b ≠ 0) : + checkedDivMod a b = + some (ofNat (toNat a / toNat b), ofNat (toNat a % toNat b)) := by + simp [checkedDivMod, checkedDiv, checkedMod, h] + +/-- Saturating addition returns the maximum value on overflow. -/ +theorem saturatingAdd_eq_max_of_overflow (a b : α) + (h : modulus width ≤ toNat a + toNat b) : + saturatingAdd a b = max := by + simp [saturatingAdd, addOverflow, h] + +/-- Saturating addition agrees with wrapping addition when the exact sum fits. -/ +theorem saturatingAdd_eq_add_of_lt (a b : α) + (h : toNat a + toNat b < modulus width) : + saturatingAdd a b = a + b := by + change saturatingAdd a b = wrappingAdd a b + simp [saturatingAdd, addOverflow, Nat.not_le.mpr h] + +/-- Saturating subtraction returns zero on underflow. -/ +theorem saturatingSub_eq_zero_of_lt (a b : α) (h : toNat a < toNat b) : + saturatingSub a b = 0 := by + change saturatingSub a b = ofNat 0 + simp [saturatingSub, subOverflow, h] + +/-- Saturating subtraction agrees with wrapping subtraction without underflow. -/ +theorem saturatingSub_eq_sub_of_le (a b : α) (h : toNat b ≤ toNat a) : + saturatingSub a b = a - b := by + change saturatingSub a b = wrappingSub a b + simp [saturatingSub, subOverflow, Nat.not_lt.mpr h] + +/-- Saturating multiplication returns the maximum value on overflow. -/ +theorem saturatingMul_eq_max_of_overflow (a b : α) + (h : modulus width ≤ toNat a * toNat b) : + saturatingMul a b = max := by + simp [saturatingMul, mulOverflow, h] + +/-- Saturating multiplication agrees with wrapping multiplication when the product fits. -/ +theorem saturatingMul_eq_mul_of_lt (a b : α) + (h : toNat a * toNat b < modulus width) : + saturatingMul a b = a * b := by + change saturatingMul a b = wrappingMul a b + simp [saturatingMul, mulOverflow, Nat.not_le.mpr h] + +/-- The population count never exceeds the bit width. -/ +theorem countOnes_le_width (value : α) : countOnes value ≤ width := + BitVec.toNat_cpop_le _ + +/-- The leading-zero count never exceeds the bit width. -/ +theorem leadingZeros_le_width (value : α) : leadingZeros value ≤ width := by + simpa [leadingZeros, BitVec.le_def] using + (BitVec.clz_le (x := FixedUInt.toBitVec value)) + +/-- The trailing-zero count never exceeds the bit width. -/ +theorem trailingZeros_le_width (value : α) : trailingZeros value ≤ width := by + simpa [trailingZeros, BitVec.ctz_eq_reverse_clz, BitVec.le_def] using + (BitVec.clz_le (x := (FixedUInt.toBitVec value).reverse)) + +/-- Unsigned order agrees with natural-number order. -/ +@[simp] +theorem lt_iff_toNat_lt (a b : α) : a < b ↔ toNat a < toNat b := + Iff.rfl + +/-- Unsigned non-strict order agrees with natural-number order. -/ +@[simp] +theorem le_iff_toNat_le (a b : α) : a ≤ b ↔ toNat a ≤ toNat b := + Iff.rfl + +end FixedUInt + +/-- A nominal 64-bit unsigned integer for bounded Ethereum counters and gas quantities. -/ +@[ext] +structure U64 where + /-- The exact 64-bit representation. -/ + val : BitVec 64 + deriving Repr, Hashable + +/-- A nominal 128-bit unsigned integer for Rust and host-runtime quantities. -/ +@[ext] +structure U128 where + /-- The exact 128-bit representation. -/ + val : BitVec 128 + deriving Repr, Hashable + +/-- A nominal 256-bit unsigned integer used for EVM words and Ethereum quantities. -/ +@[ext] +structure U256 where + /-- The exact 256-bit representation. -/ + val : BitVec 256 + deriving Repr, Hashable + +/-- Exact-width representation for `U64`. -/ +instance : FixedUInt U64 64 where + toBitVec := U64.val + ofBitVec := U64.mk + of_to := by intro; rfl + to_of := by intro; rfl + +/-- Exact-width representation for `U128`. -/ +instance : FixedUInt U128 128 where + toBitVec := U128.val + ofBitVec := U128.mk + of_to := by intro; rfl + to_of := by intro; rfl + +/-- Exact-width representation for `U256`. -/ +instance : FixedUInt U256 256 where + toBitVec := U256.val + ofBitVec := U256.mk + of_to := by intro; rfl + to_of := by intro; rfl + +/-- The generic representation of a `U64` is its stored bit vector. -/ +@[simp] +theorem U64.toBitVec_eq_val (value : U64) : FixedUInt.toBitVec value = value.val := + rfl + +/-- The generic representation of a `U128` is its stored bit vector. -/ +@[simp] +theorem U128.toBitVec_eq_val (value : U128) : FixedUInt.toBitVec value = value.val := + rfl + +/-- The generic representation of a `U256` is its stored bit vector. -/ +@[simp] +theorem U256.toBitVec_eq_val (value : U256) : FixedUInt.toBitVec value = value.val := + rfl + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/UInt/U128.lean b/LeanPool/Lean4EVM/Primitives/UInt/U128.lean new file mode 100644 index 0000000000..60eb2d948e --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/UInt/U128.lean @@ -0,0 +1,189 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.UInt.U64 + +/-! +# `U128` + +Type-owned construction, narrowing, widening multiplication, and proof API for 128-bit values. +-/ + +namespace Lean4EVM +namespace U128 + +/-- Constructs a `U128` by retaining the low 128 bits. -/ +abbrev ofNat (n : ℕ) : U128 := FixedUInt.ofNat n +/-- Constructs a `U128` only when `n` fits in 128 bits. -/ +abbrev ofNatOpt (n : ℕ) : Option U128 := FixedUInt.ofNatOpt n +/-- Constructs a `U128` with two's-complement wrapping. -/ +abbrev ofInt (n : ℤ) : U128 := FixedUInt.ofInt n +/-- Constructs a `U128` only from a representable nonnegative integer. -/ +abbrev ofIntOpt (n : ℤ) : Option U128 := FixedUInt.ofIntOpt n +/-- Returns the unsigned value. -/ +abbrev toNat (value : U128) : ℕ := FixedUInt.toNat value +/-- Reinterprets the bits as a signed two's-complement integer. -/ +abbrev toSignedInt (value : U128) : ℤ := FixedUInt.toSignedInt value +/-- Returns the maximum `U128`. -/ +abbrev max : U128 := FixedUInt.max +/-- Returns the modulus `2 ^ 128`. -/ +abbrev modulus : ℕ := FixedUInt.modulus 128 + +/-! ### Overflow policies + +Ordinary `U128` arithmetic wraps. These re-exports give the checked, overflowing and saturating +policies the same `value.operation` spelling, so a caller states its policy without reaching into +the generic `FixedUInt` namespace. +-/ + +/-- Adds two values, or reports `none` when the exact sum does not fit in 128 bits. -/ +abbrev checkedAdd (a b : U128) : Option U128 := FixedUInt.checkedAdd a b +/-- Subtracts two values, or reports `none` when the exact difference is negative. -/ +abbrev checkedSub (a b : U128) : Option U128 := FixedUInt.checkedSub a b +/-- Multiplies two values, or reports `none` when the exact product does not fit in 128 bits. -/ +abbrev checkedMul (a b : U128) : Option U128 := FixedUInt.checkedMul a b +/-- Divides two values, or reports `none` for a zero divisor. -/ +abbrev checkedDiv (a b : U128) : Option U128 := FixedUInt.checkedDiv a b +/-- Computes a remainder, or reports `none` for a zero divisor. -/ +abbrev checkedMod (a b : U128) : Option U128 := FixedUInt.checkedMod a b +/-- Returns quotient and remainder together, or `none` for a zero divisor. -/ +abbrev checkedDivMod (a b : U128) : Option (U128 × U128) := FixedUInt.checkedDivMod a b + +/-- Returns the wrapped sum together with the flag that reports the lost carry. -/ +abbrev overflowingAdd (a b : U128) : U128 × Bool := FixedUInt.overflowingAdd a b +/-- Returns the wrapped difference together with the flag that reports the borrow. -/ +abbrev overflowingSub (a b : U128) : U128 × Bool := FixedUInt.overflowingSub a b +/-- Returns the wrapped product together with the flag that reports the lost high bits. -/ +abbrev overflowingMul (a b : U128) : U128 × Bool := FixedUInt.overflowingMul a b + +/-- Adds two values, clamping an overflowing sum to the greatest U128. -/ +abbrev saturatingAdd (a b : U128) : U128 := FixedUInt.saturatingAdd a b +/-- Subtracts two values, clamping an underflowing difference to zero. -/ +abbrev saturatingSub (a b : U128) : U128 := FixedUInt.saturatingSub a b +/-- Multiplies two values, clamping an overflowing product to the greatest U128. -/ +abbrev saturatingMul (a b : U128) : U128 := FixedUInt.saturatingMul a b + +/-- Reports whether the exact sum leaves the 128-bit range. -/ +abbrev addOverflow (a b : U128) : Bool := FixedUInt.addOverflow a b +/-- Reports whether the exact difference is negative. -/ +abbrev subOverflow (a b : U128) : Bool := FixedUInt.subOverflow a b +/-- Reports whether the exact product leaves the 128-bit range. -/ +abbrev mulOverflow (a b : U128) : Bool := FixedUInt.mulOverflow a b + +/-! ### Bit inspection, rotation and rendering -/ + +/-- Returns bit `index` counting from the least-significant bit; bits at 128 and above are false. -/ +abbrev testBit (value : U128) (index : ℕ) : Bool := FixedUInt.testBit value index +/-- Counts the zero bits above the most-significant set bit. -/ +abbrev leadingZeros (value : U128) : ℕ := FixedUInt.leadingZeros value +/-- Counts the zero bits below the least-significant set bit. -/ +abbrev trailingZeros (value : U128) : ℕ := FixedUInt.trailingZeros value +/-- Counts the set bits. -/ +abbrev countOnes (value : U128) : ℕ := FixedUInt.countOnes value +/-- Rotates the bit pattern left, carrying the bits that leave the top back into the bottom; the +amount is taken modulo 128. -/ +abbrev rotateLeft (value : U128) (amount : ℕ) : U128 := FixedUInt.rotateLeft value amount +/-- Rotates the bit pattern right, carrying the bits that leave the bottom back into the top; the +amount is taken modulo 128. -/ +abbrev rotateRight (value : U128) (amount : ℕ) : U128 := FixedUInt.rotateRight value amount +/-- Renders the value as `0x` followed by exactly 32 hexadecimal digits. -/ +abbrev toHex (value : U128) : String := FixedUInt.toHex value + +/-- The `U128` modulus has the canonical power-of-two form. -/ +@[simp] +theorem modulus_eq : U128.modulus = 2 ^ 128 := + rfl + +/-- Natural casts into `U128` reduce modulo `2 ^ 128`. -/ +@[simp] +theorem toNat_natCast (n : ℕ) : (n : U128).toNat = n % 2 ^ 128 := by + exact FixedUInt.toNat_natCast (α := U128) (width := 128) n + +/-- Numeric `U128` literals reduce modulo `2 ^ 128`. -/ +@[simp] +theorem toNat_ofNat_lit (n : ℕ) [n.AtLeastTwo] : + (ofNat(n) : U128).toNat = n % 2 ^ 128 := by + exact FixedUInt.toNat_ofNat_lit (α := U128) (width := 128) n + +/-- Narrows a `U128` when its value fits in 64 bits. -/ +def toU64Opt (value : U128) : Option U64 := + U64.ofNatOpt value.toNat + +/-- Returns the low 64 bits of a `U128`. -/ +def lowU64 (value : U128) : U64 := + U64.ofNat value.toNat + +/-- Widens a `U128` to `U256` without changing its value. -/ +def toU256 (value : U128) : U256 := + FixedUInt.ofNat value.toNat + +/-- Multiplies two `U128` values exactly into a `U256`. -/ +def wideningMul (a b : U128) : U256 := + FixedUInt.ofNat (a.toNat * b.toNat) + +/-- Widening to `U256` preserves the unsigned value. -/ +@[simp] +theorem toNat_toU256 (value : U128) : FixedUInt.toNat value.toU256 = value.toNat := by + rw [toU256, FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + exact lt_trans (FixedUInt.toNat_lt_modulus value) (by decide) + +/-- Widening from `U128` to `U256` is injective. -/ +theorem toU256_injective : Function.Injective toU256 := by + intro a b h + apply FixedUInt.toNat_injective + have h' := congrArg FixedUInt.toNat h + simpa using h' + +/-- Low-64-bit narrowing agrees with reduction modulo `2 ^ 64`. -/ +@[simp] +theorem toNat_lowU64 (value : U128) : value.lowU64.toNat = value.toNat % U64.modulus := by + exact FixedUInt.toNat_ofNat _ + +/-- Checked narrowing to `U64` fails exactly for out-of-range values. -/ +@[simp] +theorem toU64Opt_eq_none_iff (value : U128) : + value.toU64Opt = none ↔ U64.modulus ≤ value.toNat := by + exact FixedUInt.ofNatOpt_eq_none_iff _ + +/-- Checked narrowing to `U64` returns the low word when the value fits. -/ +theorem toU64Opt_eq_some_of_lt (value : U128) (h : value.toNat < U64.modulus) : + value.toU64Opt = some value.lowU64 := by + simp only [toU64Opt, lowU64, U64.ofNatOpt, FixedUInt.ofNatOpt] + rw [ite_eq_left h] + +/-- Widening a `U64` and narrowing it again is lossless. -/ +@[simp] +theorem toU64Opt_toU128 (value : U64) : value.toU128.toU64Opt = some value := by + have h : value.toU128.toNat < U64.modulus := by + simp only [U64.toNat_toU128] + exact FixedUInt.toNat_lt_modulus value + rw [toU64Opt_eq_some_of_lt _ h] + apply congrArg some + apply FixedUInt.toNat_injective + simp only [toNat_lowU64, U64.toNat_toU128] + exact Nat.mod_eq_of_lt (FixedUInt.toNat_lt_modulus value) + +/-- A `U64` recovered by checked narrowing widens back to the value it came from. With +`toU64Opt_toU128` this makes widening and checked narrowing mutually inverse. -/ +theorem toU128_toU64Opt_eq_some {value : U128} {narrowed : U64} + (h : value.toU64Opt = some narrowed) : narrowed.toU128 = value := by + rw [toU64Opt, U64.ofNatOpt] at h + rcases FixedUInt.ofNatOpt_eq_some_iff.mp h with ⟨hlt, hval⟩ + apply FixedUInt.toNat_injective + simp only [U64.toNat_toU128, ← hval, FixedUInt.toNat_ofNat] + exact Nat.mod_eq_of_lt hlt + +/-- Exact widening multiplication has the natural-number product as its value. -/ +@[simp] +theorem toNat_wideningMul (a b : U128) : + FixedUInt.toNat (wideningMul a b) = a.toNat * b.toNat := by + rw [wideningMul, FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + have h := Nat.mul_lt_mul_of_lt_of_lt + (FixedUInt.toNat_lt_modulus a) (FixedUInt.toNat_lt_modulus b) + simpa [U128.modulus, FixedUInt.modulus, pow_add] using h + +end U128 + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/UInt/U256.lean b/LeanPool/Lean4EVM/Primitives/UInt/U256.lean new file mode 100644 index 0000000000..19accea81f --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/UInt/U256.lean @@ -0,0 +1,605 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.UInt.U128 + +/-! +# `U256` + +The EVM word API: width conversions, signed interpretation, opcode arithmetic, and their laws. +-/ + +namespace Lean4EVM +namespace U256 + +/-- Constructs a `U256` by retaining the low 256 bits. -/ +abbrev ofNat (n : ℕ) : U256 := FixedUInt.ofNat n +/-- Constructs a `U256` only when `n` fits in 256 bits. -/ +abbrev ofNatOpt (n : ℕ) : Option U256 := FixedUInt.ofNatOpt n +/-- Constructs a `U256` with two's-complement wrapping. -/ +abbrev ofInt (n : ℤ) : U256 := FixedUInt.ofInt n +/-- Constructs a `U256` only from a representable nonnegative integer. -/ +abbrev ofIntOpt (n : ℤ) : Option U256 := FixedUInt.ofIntOpt n +/-- Returns the unsigned value. -/ +abbrev toNat (value : U256) : ℕ := FixedUInt.toNat value +/-- Reinterprets the bits as a signed two's-complement integer. -/ +abbrev toSignedInt (value : U256) : ℤ := FixedUInt.toSignedInt value +/-- Compatibility name for signed two's-complement reinterpretation. -/ +abbrev toInt (value : U256) : ℤ := toSignedInt value +/-- Returns the maximum `U256`. -/ +abbrev max : U256 := FixedUInt.max +/-- Returns the modulus `2 ^ 256`. -/ +abbrev modulus : ℕ := FixedUInt.modulus 256 + +/-! ### Overflow policies + +Ordinary `U256` arithmetic wraps. These re-exports give the checked, overflowing and saturating +policies the same `value.operation` spelling, so a caller states its policy without reaching into +the generic `FixedUInt` namespace. +-/ + +/-- Adds two values, or reports `none` when the exact sum does not fit in 256 bits. -/ +abbrev checkedAdd (a b : U256) : Option U256 := FixedUInt.checkedAdd a b +/-- Subtracts two values, or reports `none` when the exact difference is negative. -/ +abbrev checkedSub (a b : U256) : Option U256 := FixedUInt.checkedSub a b +/-- Multiplies two values, or reports `none` when the exact product does not fit in 256 bits. -/ +abbrev checkedMul (a b : U256) : Option U256 := FixedUInt.checkedMul a b +/-- Divides two values, or reports `none` for a zero divisor. -/ +abbrev checkedDiv (a b : U256) : Option U256 := FixedUInt.checkedDiv a b +/-- Computes a remainder, or reports `none` for a zero divisor. -/ +abbrev checkedMod (a b : U256) : Option U256 := FixedUInt.checkedMod a b +/-- Returns quotient and remainder together, or `none` for a zero divisor. -/ +abbrev checkedDivMod (a b : U256) : Option (U256 × U256) := FixedUInt.checkedDivMod a b + +/-- Returns the wrapped sum together with the flag that reports the lost carry. -/ +abbrev overflowingAdd (a b : U256) : U256 × Bool := FixedUInt.overflowingAdd a b +/-- Returns the wrapped difference together with the flag that reports the borrow. -/ +abbrev overflowingSub (a b : U256) : U256 × Bool := FixedUInt.overflowingSub a b +/-- Returns the wrapped product together with the flag that reports the lost high bits. -/ +abbrev overflowingMul (a b : U256) : U256 × Bool := FixedUInt.overflowingMul a b + +/-- Adds two values, clamping an overflowing sum to the greatest U256. -/ +abbrev saturatingAdd (a b : U256) : U256 := FixedUInt.saturatingAdd a b +/-- Subtracts two values, clamping an underflowing difference to zero. -/ +abbrev saturatingSub (a b : U256) : U256 := FixedUInt.saturatingSub a b +/-- Multiplies two values, clamping an overflowing product to the greatest U256. -/ +abbrev saturatingMul (a b : U256) : U256 := FixedUInt.saturatingMul a b + +/-- Reports whether the exact sum leaves the 256-bit range. -/ +abbrev addOverflow (a b : U256) : Bool := FixedUInt.addOverflow a b +/-- Reports whether the exact difference is negative. -/ +abbrev subOverflow (a b : U256) : Bool := FixedUInt.subOverflow a b +/-- Reports whether the exact product leaves the 256-bit range. -/ +abbrev mulOverflow (a b : U256) : Bool := FixedUInt.mulOverflow a b + +/-! ### Bit inspection, rotation and rendering -/ + +/-- Returns bit `index` counting from the least-significant bit; bits at 256 and above are false. -/ +abbrev testBit (value : U256) (index : ℕ) : Bool := FixedUInt.testBit value index +/-- Counts the zero bits above the most-significant set bit. -/ +abbrev leadingZeros (value : U256) : ℕ := FixedUInt.leadingZeros value +/-- Counts the zero bits below the least-significant set bit. -/ +abbrev trailingZeros (value : U256) : ℕ := FixedUInt.trailingZeros value +/-- Counts the set bits. -/ +abbrev countOnes (value : U256) : ℕ := FixedUInt.countOnes value +/-- Rotates the bit pattern left, carrying the bits that leave the top back into the bottom; the +amount is taken modulo 256. -/ +abbrev rotateLeft (value : U256) (amount : ℕ) : U256 := FixedUInt.rotateLeft value amount +/-- Rotates the bit pattern right, carrying the bits that leave the bottom back into the top; the +amount is taken modulo 256. -/ +abbrev rotateRight (value : U256) (amount : ℕ) : U256 := FixedUInt.rotateRight value amount +/-- Renders the value as `0x` followed by exactly 64 hexadecimal digits. -/ +abbrev toHex (value : U256) : String := FixedUInt.toHex value + +/-- The `U256` modulus has the canonical power-of-two form. -/ +@[simp] +theorem modulus_eq : U256.modulus = 2 ^ 256 := + rfl + +/-- Natural casts into `U256` reduce modulo `2 ^ 256`. -/ +@[simp] +theorem toNat_natCast (n : ℕ) : (n : U256).toNat = n % 2 ^ 256 := by + exact FixedUInt.toNat_natCast (α := U256) (width := 256) n + +/-- Numeric `U256` literals reduce modulo `2 ^ 256`. -/ +@[simp] +theorem toNat_ofNat_lit (n : ℕ) [n.AtLeastTwo] : + (ofNat(n) : U256).toNat = n % 2 ^ 256 := by + exact FixedUInt.toNat_ofNat_lit (α := U256) (width := 256) n + +/-- Narrows a `U256` when its value fits in 64 bits. -/ +def toU64Opt (value : U256) : Option U64 := + U64.ofNatOpt value.toNat + +/-- Returns the low 64 bits of a `U256`. -/ +def lowU64 (value : U256) : U64 := + U64.ofNat value.toNat + +/-- Narrows a `U256` when its value fits in 128 bits. -/ +def toU128Opt (value : U256) : Option U128 := + U128.ofNatOpt value.toNat + +/-- Returns the low 128 bits of a `U256`. -/ +def lowU128 (value : U256) : U128 := + U128.ofNat value.toNat + +/-- Returns the high 128 bits of a `U256`. -/ +def highU128 (value : U256) : U128 := + U128.ofNat (value.toNat / U128.modulus) + +/-- Constructs a `U256` from its high and low 128-bit halves. -/ +def fromU128s (high low : U128) : U256 := + ofNat (high.toNat * U128.modulus + low.toNat) + +/-- Converts a Boolean to the EVM word zero or one. -/ +def ofBool (value : Bool) : U256 := + if value then 1 else 0 + +/-- Tests whether an EVM word is nonzero. -/ +def toBool (value : U256) : Bool := + decide (value ≠ 0) + +/-- Tests whether an EVM word is zero. -/ +def isZero (value : U256) : Bool := + decide (value = 0) + +/-- Compares two EVM words as unsigned integers. -/ +def ult (a b : U256) : Bool := + decide (a < b) + +/-- Compares two EVM words in descending unsigned order. -/ +def ugt (a b : U256) : Bool := + decide (a > b) + +/-- Compares two EVM words as signed two's-complement integers. -/ +def slt (a b : U256) : Bool := + decide (a.toSignedInt < b.toSignedInt) + +/-- Compares two EVM words in descending signed two's-complement order. -/ +def sgt (a b : U256) : Bool := + decide (a.toSignedInt > b.toSignedInt) + +/-- Divides EVM words, returning zero for a zero divisor. -/ +def div (a b : U256) : U256 := + if b = 0 then 0 else U256.mk (a.val / b.val) + +/-- Computes EVM remainder, returning zero for a zero divisor. -/ +def mod (a b : U256) : U256 := + if b = 0 then 0 else U256.mk (a.val % b.val) + +/-- EVM unsigned division, including its zero-divisor rule. -/ +instance : Div U256 where + div := div + +/-- EVM unsigned remainder, including its zero-divisor rule. -/ +instance : Mod U256 where + mod := mod + +/-- Divides signed two's-complement EVM words, truncating toward zero. -/ +def sdiv (a b : U256) : U256 := + U256.mk (a.val.sdiv b.val) + +/-- Computes EVM signed remainder, whose sign follows the dividend. -/ +def smod (a b : U256) : U256 := + if b = 0 then 0 else U256.mk (a.val.srem b.val) + +/-- Computes `(a + b) % modulus` with an exact intermediate sum. -/ +def addmod (a b modulus : U256) : U256 := + if modulus = 0 then 0 else ofNat ((a.toNat + b.toNat) % modulus.toNat) + +/-- Computes `(a * b) % modulus` with an exact intermediate product. -/ +def mulmod (a b modulus : U256) : U256 := + if modulus = 0 then 0 else ofNat ((a.toNat * b.toNat) % modulus.toNat) + +/-- Raises `base` to the exponent encoded by `exponent`, modulo `2 ^ 256`. -/ +def exp (base exponent : U256) : U256 := + FixedUInt.pow base exponent.toNat + +/-- Returns the indexed byte, counting from the most-significant byte. -/ +def byteAt (index value : U256) : U256 := + if index.toNat < 32 then + ofNat ((value.toNat / 2 ^ (8 * (31 - index.toNat))) % 256) + else + 0 + +/-- Sign-extends `value` from `byteIndex`; indices at least 32 leave it unchanged. -/ +def signExtend (byteIndex value : U256) : U256 := + if byteIndex.toNat < 32 then + U256.mk <| BitVec.signExtend 256 <| + BitVec.extractLsb' 0 (8 * (byteIndex.toNat + 1)) value.val + else + value + +/-- Shifts `value` left by the EVM word encoded in `shift`. -/ +def shl (shift value : U256) : U256 := + value <<< shift.toNat + +/-- Logically shifts `value` right by the EVM word encoded in `shift`. -/ +def shr (shift value : U256) : U256 := + value >>> shift.toNat + +/-- Arithmetically shifts `value` right by the EVM word encoded in `shift`. -/ +def sar (shift value : U256) : U256 := + U256.mk (value.val.sshiftRight shift.toNat) + +/-- Counts leading zero bits as an EVM word, as specified by `CLZ`. -/ +def clz (value : U256) : U256 := + ofNat (FixedUInt.leadingZeros value) + +/-- `EXP` agrees with natural exponentiation modulo `2 ^ 256`. -/ +@[simp] +theorem toNat_exp (base exponent : U256) : + (exp base exponent).toNat = base.toNat ^ exponent.toNat % 2 ^ 256 := by + exact FixedUInt.toNat_pow base exponent.toNat + +/-- `SHL` returns zero when the EVM shift amount is at least 256. -/ +@[simp] +theorem shl_of_ge_256 (shift value : U256) (h : 256 ≤ shift.toNat) : + shl shift value = 0 := by + exact FixedUInt.shiftLeft_eq_zero_of_width_le value shift.toNat h + +/-- In-range `SHL` agrees with natural left shift modulo `2 ^ 256`. -/ +theorem toNat_shl_of_lt (shift value : U256) (h : shift.toNat < 256) : + (shl shift value).toNat = + (value.toNat <<< shift.toNat) % U256.modulus := by + exact FixedUInt.toNat_shiftLeft_of_lt value shift.toNat h + +/-- `SHR` returns zero when the EVM shift amount is at least 256. -/ +@[simp] +theorem shr_of_ge_256 (shift value : U256) (h : 256 ≤ shift.toNat) : + shr shift value = 0 := by + exact FixedUInt.shiftRight_eq_zero_of_width_le value shift.toNat h + +/-- `SHR` agrees with natural logical right shift. -/ +@[simp] +theorem toNat_shr (shift value : U256) : + (shr shift value).toNat = value.toNat >>> shift.toNat := by + exact FixedUInt.toNat_shiftRight value shift.toNat + +/-- `SAR` fills an oversized shift with the sign bit. -/ +theorem sar_of_ge_256 (shift value : U256) (h : 256 ≤ shift.toNat) : + sar shift value = if value.val.msb then U256.max else 0 := by + cases hsign : value.val.msb + · simp only [Bool.false_eq_true, ↓reduceIte] + apply U256.ext + change value.val.sshiftRight shift.toNat = 0 + rw [BitVec.sshiftRight_eq_of_msb_false hsign, + BitVec.ushiftRight_eq_zero h] + exact (FixedUInt.toBitVec_zero (α := U256) (width := 256)).symm + · simp only [↓reduceIte] + apply U256.ext + change value.val.sshiftRight shift.toNat = BitVec.allOnes 256 + rw [BitVec.sshiftRight_eq_of_msb_true hsign, + BitVec.ushiftRight_eq_zero h] + simp + +/-- Arithmetic right shift exposes the underlying two's-complement operation. -/ +@[simp] +theorem val_sar (shift value : U256) : + (sar shift value).val = value.val.sshiftRight shift.toNat := + rfl + +/-- In-range `SIGNEXTEND` exposes its exact bit-vector result. -/ +theorem val_signExtend_of_lt (byteIndex value : U256) (h : byteIndex.toNat < 32) : + (signExtend byteIndex value).val = + BitVec.signExtend 256 (BitVec.extractLsb' 0 (8 * (byteIndex.toNat + 1)) value.val) := by + simp [signExtend, h] + +/-- In-range `BYTE` has the exact EVM big-endian indexing formula. -/ +theorem toNat_byteAt_of_lt (index value : U256) (h : index.toNat < 32) : + (byteAt index value).toNat = + (value.toNat / 2 ^ (8 * (31 - index.toNat))) % 256 := by + simp only [byteAt, h, ↓reduceIte] + change FixedUInt.toNat (FixedUInt.ofNat _ : U256) = _ + rw [FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + exact lt_trans (Nat.mod_lt _ (by decide)) (by decide) + +/-- The word returned by `CLZ` is the exact leading-zero count. -/ +@[simp] +theorem toNat_clz (value : U256) : + (clz value).toNat = FixedUInt.leadingZeros value := by + change FixedUInt.toNat + (FixedUInt.ofNat (FixedUInt.leadingZeros value) : U256) = _ + rw [FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + exact lt_of_le_of_lt (FixedUInt.leadingZeros_le_width value) (by decide) + +/-- `CLZ` always returns a value at most 256. -/ +theorem clz_toNat_le_256 (value : U256) : (clz value).toNat ≤ 256 := by + rw [toNat_clz] + exact FixedUInt.leadingZeros_le_width value + +/-- Low-128-bit narrowing agrees with reduction modulo `2 ^ 128`. -/ +@[simp] +theorem toNat_lowU128 (value : U256) : + FixedUInt.toNat value.lowU128 = FixedUInt.toNat value % U128.modulus := by + exact FixedUInt.toNat_ofNat _ + +/-- Low-64-bit narrowing agrees with reduction modulo `2 ^ 64`. -/ +@[simp] +theorem toNat_lowU64 (value : U256) : value.lowU64.toNat = value.toNat % U64.modulus := by + exact FixedUInt.toNat_ofNat _ + +/-- The high half is unsigned division by `2 ^ 128`. -/ +@[simp] +theorem toNat_highU128 (value : U256) : + FixedUInt.toNat value.highU128 = FixedUInt.toNat value / U128.modulus := by + change FixedUInt.toNat (FixedUInt.ofNat (value.toNat / U128.modulus) : U128) = _ + rw [FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + apply (Nat.div_lt_iff_lt_mul (by decide : 0 < U128.modulus)).2 + simpa [U128.modulus, U256.modulus, FixedUInt.modulus, pow_add] using + FixedUInt.toNat_lt_modulus value + +/-- Combining two 128-bit halves preserves their exact unsigned value. -/ +@[simp] +theorem toNat_fromU128s (high low : U128) : + FixedUInt.toNat (fromU128s high low) = + FixedUInt.toNat high * U128.modulus + FixedUInt.toNat low := by + change FixedUInt.toNat + (FixedUInt.ofNat (high.toNat * U128.modulus + low.toNat) : U256) = _ + rw [FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + have hhigh := FixedUInt.toNat_lt_modulus high + have hlow := FixedUInt.toNat_lt_modulus low + have hfit : high.toNat * U128.modulus + low.toNat < U128.modulus * U128.modulus := by + have h₁ := Nat.add_lt_add_left hlow (high.toNat * U128.modulus) + rw [show high.toNat * U128.modulus + U128.modulus = + (high.toNat + 1) * U128.modulus by simp [Nat.add_mul]] at h₁ + exact lt_of_lt_of_le h₁ (Nat.mul_le_mul_right U128.modulus (Nat.succ_le_of_lt hhigh)) + simpa [U128.modulus, U256.modulus, FixedUInt.modulus, pow_add] using hfit + +/-- Splitting a combined word recovers its low half. -/ +@[simp] +theorem lowU128_fromU128s (high low : U128) : + lowU128 (fromU128s high low) = low := by + apply FixedUInt.toNat_injective + rw [toNat_lowU128, toNat_fromU128s, Nat.mul_comm (FixedUInt.toNat high) U128.modulus, + Nat.mul_add_mod] + exact Nat.mod_eq_of_lt (FixedUInt.toNat_lt_modulus low) + +/-- Splitting a combined word recovers its high half. -/ +@[simp] +theorem highU128_fromU128s (high low : U128) : + highU128 (fromU128s high low) = high := by + apply FixedUInt.toNat_injective + rw [toNat_highU128, toNat_fromU128s] + rw [Nat.mul_comm (FixedUInt.toNat high) U128.modulus] + rw [Nat.mul_add_div (by decide : 0 < U128.modulus), + Nat.div_eq_of_lt (FixedUInt.toNat_lt_modulus low), Nat.add_zero] + +/-- Splitting and recombining a `U256` is lossless. -/ +@[simp] +theorem fromU128s_highU128_lowU128 (value : U256) : + fromU128s value.highU128 value.lowU128 = value := by + apply FixedUInt.toNat_injective + rw [toNat_fromU128s, toNat_highU128, toNat_lowU128] + exact Nat.div_add_mod' value.toNat U128.modulus + +/-- Checked narrowing succeeds exactly when the value fits in 128 bits. -/ +@[simp] +theorem toU128Opt_eq_none_iff (value : U256) : + value.toU128Opt = none ↔ U128.modulus ≤ value.toNat := by + exact FixedUInt.ofNatOpt_eq_none_iff _ + +/-- Checked narrowing succeeds with the low half when the value fits. -/ +theorem toU128Opt_eq_some_of_lt (value : U256) (h : value.toNat < U128.modulus) : + value.toU128Opt = some value.lowU128 := by + simp only [toU128Opt, lowU128, U128.ofNatOpt, FixedUInt.ofNatOpt] + rw [ite_eq_left h] + +/-- Checked narrowing to `U64` fails exactly for out-of-range values. -/ +@[simp] +theorem toU64Opt_eq_none_iff (value : U256) : + value.toU64Opt = none ↔ U64.modulus ≤ value.toNat := by + exact FixedUInt.ofNatOpt_eq_none_iff _ + +/-- Checked narrowing to `U64` returns the low word when the value fits. -/ +theorem toU64Opt_eq_some_of_lt (value : U256) (h : value.toNat < U64.modulus) : + value.toU64Opt = some value.lowU64 := by + simp only [toU64Opt, lowU64, U64.ofNatOpt, FixedUInt.ofNatOpt] + rw [ite_eq_left h] + +/-- Widening a `U64` to `U256` and narrowing it again is lossless. -/ +@[simp] +theorem toU64Opt_toU256 (value : U64) : value.toU256.toU64Opt = some value := by + have h : FixedUInt.toNat value.toU256 < U64.modulus := by + rw [U64.toNat_toU256] + exact FixedUInt.toNat_lt_modulus value + rw [toU64Opt_eq_some_of_lt _ h] + apply congrArg some + apply FixedUInt.toNat_injective + simp only [toNat_lowU64, U64.toNat_toU256] + exact Nat.mod_eq_of_lt (FixedUInt.toNat_lt_modulus value) + +/-- Widening a `U128` to `U256` and narrowing it again is lossless. -/ +@[simp] +theorem toU128Opt_toU256 (value : U128) : value.toU256.toU128Opt = some value := by + have h : FixedUInt.toNat value.toU256 < U128.modulus := by + rw [U128.toNat_toU256] + exact FixedUInt.toNat_lt_modulus value + rw [toU128Opt_eq_some_of_lt _ h] + apply congrArg some + apply FixedUInt.toNat_injective + simp only [U256.toNat_lowU128, U128.toNat_toU256] + exact Nat.mod_eq_of_lt (FixedUInt.toNat_lt_modulus value) + +/-- A `U64` recovered by checked narrowing widens back to the word it came from. With +`toU64Opt_toU256` this makes widening and checked narrowing mutually inverse. -/ +theorem toU256_toU64Opt_eq_some {value : U256} {narrowed : U64} + (h : value.toU64Opt = some narrowed) : narrowed.toU256 = value := by + rw [toU64Opt, U64.ofNatOpt] at h + rcases FixedUInt.ofNatOpt_eq_some_iff.mp h with ⟨hlt, hval⟩ + apply FixedUInt.toNat_injective + simp only [U64.toNat_toU256, ← hval, FixedUInt.toNat_ofNat] + exact Nat.mod_eq_of_lt hlt + +/-- A `U128` recovered by checked narrowing widens back to the word it came from. With +`toU128Opt_toU256` this makes widening and checked narrowing mutually inverse. -/ +theorem toU256_toU128Opt_eq_some {value : U256} {narrowed : U128} + (h : value.toU128Opt = some narrowed) : narrowed.toU256 = value := by + rw [toU128Opt, U128.ofNatOpt] at h + rcases FixedUInt.ofNatOpt_eq_some_iff.mp h with ⟨hlt, hval⟩ + apply FixedUInt.toNat_injective + simp only [U128.toNat_toU256, ← hval, FixedUInt.toNat_ofNat] + exact Nat.mod_eq_of_lt hlt + +/-- `ISZERO` is true exactly for the zero word. -/ +@[simp] +theorem isZero_eq_true_iff (value : U256) : isZero value = true ↔ value = 0 := by + simp [isZero] + +/-- Boolean interpretation is false exactly for the zero word. -/ +@[simp] +theorem toBool_eq_false_iff (value : U256) : toBool value = false ↔ value = 0 := by + simp [toBool] + +/-- Unsigned less-than agrees with comparison of unsigned natural values. -/ +@[simp] +theorem ult_eq_true_iff (a b : U256) : ult a b = true ↔ a.toNat < b.toNat := by + simp [ult] + +/-- Unsigned greater-than agrees with comparison of unsigned natural values. -/ +@[simp] +theorem ugt_eq_true_iff (a b : U256) : ugt a b = true ↔ b.toNat < a.toNat := by + simp [ugt] + +/-- Signed less-than agrees with two's-complement integer comparison. -/ +@[simp] +theorem slt_eq_true_iff (a b : U256) : + slt a b = true ↔ a.toSignedInt < b.toSignedInt := by + simp [slt] + +/-- Signed greater-than agrees with two's-complement integer comparison. -/ +@[simp] +theorem sgt_eq_true_iff (a b : U256) : + sgt a b = true ↔ b.toSignedInt < a.toSignedInt := by + simp [sgt] + +/-- EVM unsigned division agrees with natural-number division. -/ +@[simp] +theorem toNat_div (a b : U256) : (a / b).toNat = a.toNat / b.toNat := by + by_cases h : b = 0 + · subst b + change (div a 0).toNat = a.toNat / (0 : U256).toNat + simp [div] + · simp only [HDiv.hDiv, Div.div, div, h, ↓reduceIte, toNat, FixedUInt.toNat] + exact BitVec.toNat_udiv + +/-- EVM unsigned division by zero returns zero. -/ +@[simp] +theorem div_zero (a : U256) : a / 0 = 0 := by + simp [HDiv.hDiv, Div.div, div] + +/-- EVM unsigned remainder agrees with natural remainder away from zero. -/ +theorem toNat_mod (a b : U256) : + (a % b).toNat = if b = 0 then 0 else a.toNat % b.toNat := by + by_cases h : b = 0 + · simp [HMod.hMod, Mod.mod, mod, h] + · simp only [HMod.hMod, Mod.mod, mod, h, ↓reduceIte, toNat, FixedUInt.toNat] + exact BitVec.toNat_umod + +/-- EVM remainder by zero returns zero. -/ +@[simp] +theorem mod_zero (a : U256) : a % 0 = 0 := by + simp [HMod.hMod, Mod.mod, mod] + +/-- Signed EVM division by zero returns zero. -/ +@[simp] +theorem sdiv_zero (a : U256) : sdiv a 0 = 0 := by + cases a with + | mk value => + change U256.mk (value.sdiv 0) = U256.mk 0 + congr + exact BitVec.sdiv_zero + +/-- Signed EVM division agrees with truncating integer division, wrapped to 256 bits. -/ +@[simp] +theorem toSignedInt_sdiv (a b : U256) : + (sdiv a b).toSignedInt = + (a.toSignedInt.tdiv b.toSignedInt).bmod U256.modulus := by + change (a.val.sdiv b.val).toInt = (a.val.toInt.tdiv b.val.toInt).bmod (2 ^ 256) + exact BitVec.toInt_sdiv _ _ + +/-- Signed EVM remainder by zero returns zero. -/ +@[simp] +theorem smod_zero (a : U256) : smod a 0 = 0 := by + simp [smod] + +/-- Signed EVM remainder agrees with truncating integer remainder away from zero. -/ +theorem toSignedInt_smod (a b : U256) : + (smod a b).toSignedInt = + if b = 0 then 0 else a.toSignedInt.tmod b.toSignedInt := by + by_cases h : b = 0 + · simp [smod, h] + · change (if b = 0 then 0 else U256.mk (a.val.srem b.val)).toSignedInt = _ + simp only [h, ↓reduceIte] + exact BitVec.toInt_srem _ _ + +/-- Modular addition with modulus zero returns zero. -/ +@[simp] +theorem addmod_zero (a b : U256) : addmod a b 0 = 0 := by + simp [addmod] + +/-- `ADDMOD` uses an exact, non-wrapping intermediate sum. -/ +theorem toNat_addmod (a b modulus : U256) : + (addmod a b modulus).toNat = + if modulus = 0 then 0 else (a.toNat + b.toNat) % modulus.toNat := by + by_cases h : modulus = 0 + · simp [addmod, h] + · simp only [addmod, h, ↓reduceIte] + exact FixedUInt.toNat_ofNat_mod _ h + +/-- Modular multiplication with modulus zero returns zero. -/ +@[simp] +theorem mulmod_zero (a b : U256) : mulmod a b 0 = 0 := by + simp [mulmod] + +/-- `MULMOD` uses an exact, non-wrapping intermediate product. -/ +theorem toNat_mulmod (a b modulus : U256) : + (mulmod a b modulus).toNat = + if modulus = 0 then 0 else (a.toNat * b.toNat) % modulus.toNat := by + by_cases h : modulus = 0 + · simp [mulmod, h] + · simp only [mulmod, h, ↓reduceIte] + exact FixedUInt.toNat_ofNat_mod _ h + +/-- `BYTE` returns zero for an index outside the 32-byte EVM word. -/ +@[simp] +theorem byteAt_of_index_ge (index value : U256) (h : 32 ≤ index.toNat) : + byteAt index value = 0 := by + simp [byteAt, Nat.not_lt.mpr h] + +/-- `BYTE` always returns a single-byte value. -/ +theorem byteAt_toNat_lt (index value : U256) : (byteAt index value).toNat < 256 := by + by_cases h : index.toNat < 32 + · simp only [byteAt, h, ↓reduceIte, FixedUInt.toNat_ofNat] + rw [Nat.mod_eq_of_lt] + · exact Nat.mod_lt _ (by decide) + · exact Nat.lt_trans (Nat.mod_lt _ (by decide)) + (by decide) + · simp [byteAt, h] + +/-- `SIGNEXTEND` leaves a word unchanged for an out-of-range byte index. -/ +@[simp] +theorem signExtend_of_index_ge (byteIndex value : U256) (h : 32 ≤ byteIndex.toNat) : + signExtend byteIndex value = value := by + simp [signExtend, Nat.not_lt.mpr h] + +/-- `CLZ` returns 256 for the zero word. -/ +@[simp] +theorem clz_zero : clz 0 = (256 : U256) := by + apply FixedUInt.toNat_injective + change (clz 0).toNat = (256 : U256).toNat + rw [toNat_clz] + simp only [FixedUInt.leadingZeros] + have hzero : FixedUInt.toBitVec (0 : U256) = 0 := by simp + rw [hzero] + change ((0#256).clz).toNat = FixedUInt.toNat (256 : U256) + have hclz : (0#256).clz = (256 : BitVec 256) := + BitVec.clz_eq_iff_eq_zero.mpr rfl + rw [hclz] + decide + +end U256 + +end Lean4EVM diff --git a/LeanPool/Lean4EVM/Primitives/UInt/U64.lean b/LeanPool/Lean4EVM/Primitives/UInt/U64.lean new file mode 100644 index 0000000000..7901524aec --- /dev/null +++ b/LeanPool/Lean4EVM/Primitives/UInt/U64.lean @@ -0,0 +1,146 @@ +/- +Copyright (c) 2026 mrLSD. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: mrLSD +-/ +import LeanPool.Lean4EVM.Primitives.UInt.Core + +/-! +# `U64` + +Type-owned construction, widening, and proof API for bounded 64-bit Ethereum quantities. +-/ + +namespace Lean4EVM +namespace U64 + +/-- Constructs a `U64` by retaining the low 64 bits. -/ +abbrev ofNat (n : ℕ) : U64 := FixedUInt.ofNat n +/-- Constructs a `U64` only when `n` fits in 64 bits. -/ +abbrev ofNatOpt (n : ℕ) : Option U64 := FixedUInt.ofNatOpt n +/-- Constructs a `U64` with two's-complement wrapping. -/ +abbrev ofInt (n : ℤ) : U64 := FixedUInt.ofInt n +/-- Constructs a `U64` only from a representable nonnegative integer. -/ +abbrev ofIntOpt (n : ℤ) : Option U64 := FixedUInt.ofIntOpt n +/-- Returns the unsigned value. -/ +abbrev toNat (value : U64) : ℕ := FixedUInt.toNat value +/-- Reinterprets the bits as a signed two's-complement integer. -/ +abbrev toSignedInt (value : U64) : ℤ := FixedUInt.toSignedInt value +/-- Returns the maximum `U64`. -/ +abbrev max : U64 := FixedUInt.max +/-- Returns the modulus `2 ^ 64`. -/ +abbrev modulus : ℕ := FixedUInt.modulus 64 + +/-! ### Overflow policies + +Ordinary `U64` arithmetic wraps. These re-exports give the checked, overflowing and saturating +policies the same `value.operation` spelling, so a caller states its policy without reaching into +the generic `FixedUInt` namespace. +-/ + +/-- Adds two values, or reports `none` when the exact sum does not fit in 64 bits. -/ +abbrev checkedAdd (a b : U64) : Option U64 := FixedUInt.checkedAdd a b +/-- Subtracts two values, or reports `none` when the exact difference is negative. -/ +abbrev checkedSub (a b : U64) : Option U64 := FixedUInt.checkedSub a b +/-- Multiplies two values, or reports `none` when the exact product does not fit in 64 bits. -/ +abbrev checkedMul (a b : U64) : Option U64 := FixedUInt.checkedMul a b +/-- Divides two values, or reports `none` for a zero divisor. -/ +abbrev checkedDiv (a b : U64) : Option U64 := FixedUInt.checkedDiv a b +/-- Computes a remainder, or reports `none` for a zero divisor. -/ +abbrev checkedMod (a b : U64) : Option U64 := FixedUInt.checkedMod a b +/-- Returns quotient and remainder together, or `none` for a zero divisor. -/ +abbrev checkedDivMod (a b : U64) : Option (U64 × U64) := FixedUInt.checkedDivMod a b + +/-- Returns the wrapped sum together with the flag that reports the lost carry. -/ +abbrev overflowingAdd (a b : U64) : U64 × Bool := FixedUInt.overflowingAdd a b +/-- Returns the wrapped difference together with the flag that reports the borrow. -/ +abbrev overflowingSub (a b : U64) : U64 × Bool := FixedUInt.overflowingSub a b +/-- Returns the wrapped product together with the flag that reports the lost high bits. -/ +abbrev overflowingMul (a b : U64) : U64 × Bool := FixedUInt.overflowingMul a b + +/-- Adds two values, clamping an overflowing sum to the greatest U64. -/ +abbrev saturatingAdd (a b : U64) : U64 := FixedUInt.saturatingAdd a b +/-- Subtracts two values, clamping an underflowing difference to zero. -/ +abbrev saturatingSub (a b : U64) : U64 := FixedUInt.saturatingSub a b +/-- Multiplies two values, clamping an overflowing product to the greatest U64. -/ +abbrev saturatingMul (a b : U64) : U64 := FixedUInt.saturatingMul a b + +/-- Reports whether the exact sum leaves the 64-bit range. -/ +abbrev addOverflow (a b : U64) : Bool := FixedUInt.addOverflow a b +/-- Reports whether the exact difference is negative. -/ +abbrev subOverflow (a b : U64) : Bool := FixedUInt.subOverflow a b +/-- Reports whether the exact product leaves the 64-bit range. -/ +abbrev mulOverflow (a b : U64) : Bool := FixedUInt.mulOverflow a b + +/-! ### Bit inspection, rotation and rendering -/ + +/-- Returns bit `index` counting from the least-significant bit; bits at 64 and above are false. -/ +abbrev testBit (value : U64) (index : ℕ) : Bool := FixedUInt.testBit value index +/-- Counts the zero bits above the most-significant set bit. -/ +abbrev leadingZeros (value : U64) : ℕ := FixedUInt.leadingZeros value +/-- Counts the zero bits below the least-significant set bit. -/ +abbrev trailingZeros (value : U64) : ℕ := FixedUInt.trailingZeros value +/-- Counts the set bits. -/ +abbrev countOnes (value : U64) : ℕ := FixedUInt.countOnes value +/-- Rotates the bit pattern left, carrying the bits that leave the top back into the bottom; the +amount is taken modulo 64. -/ +abbrev rotateLeft (value : U64) (amount : ℕ) : U64 := FixedUInt.rotateLeft value amount +/-- Rotates the bit pattern right, carrying the bits that leave the bottom back into the top; the +amount is taken modulo 64. -/ +abbrev rotateRight (value : U64) (amount : ℕ) : U64 := FixedUInt.rotateRight value amount +/-- Renders the value as `0x` followed by exactly 16 hexadecimal digits. -/ +abbrev toHex (value : U64) : String := FixedUInt.toHex value + +/-- The `U64` modulus has the canonical power-of-two form. -/ +@[simp] +theorem modulus_eq : U64.modulus = 2 ^ 64 := + rfl + +/-- Natural casts into `U64` reduce modulo `2 ^ 64`. -/ +@[simp] +theorem toNat_natCast (n : ℕ) : (n : U64).toNat = n % 2 ^ 64 := by + exact FixedUInt.toNat_natCast (α := U64) (width := 64) n + +/-- Numeric `U64` literals reduce modulo `2 ^ 64`. -/ +@[simp] +theorem toNat_ofNat_lit (n : ℕ) [n.AtLeastTwo] : + (ofNat(n) : U64).toNat = n % 2 ^ 64 := by + exact FixedUInt.toNat_ofNat_lit (α := U64) (width := 64) n + +/-- Widens a `U64` to `U128` without changing its value. -/ +def toU128 (value : U64) : U128 := + FixedUInt.ofNat value.toNat + +/-- Widens a `U64` to `U256` without changing its value. -/ +def toU256 (value : U64) : U256 := + FixedUInt.ofNat value.toNat + +/-- Widening to `U128` preserves the unsigned value. -/ +@[simp] +theorem toNat_toU128 (value : U64) : + FixedUInt.toNat value.toU128 = value.toNat := by + rw [toU128, FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + exact lt_trans (FixedUInt.toNat_lt_modulus value) (by decide) + +/-- Widening to `U256` preserves the unsigned value. -/ +@[simp] +theorem toNat_toU256 (value : U64) : + FixedUInt.toNat value.toU256 = value.toNat := by + rw [toU256, FixedUInt.toNat_ofNat, Nat.mod_eq_of_lt] + exact lt_trans (FixedUInt.toNat_lt_modulus value) (by decide) + +/-- Widening from `U64` to `U128` is injective. -/ +theorem toU128_injective : Function.Injective toU128 := by + intro a b h + apply FixedUInt.toNat_injective + simpa using congrArg FixedUInt.toNat h + +/-- Widening from `U64` to `U256` is injective. -/ +theorem toU256_injective : Function.Injective toU256 := by + intro a b h + apply FixedUInt.toNat_injective + simpa using congrArg FixedUInt.toNat h + +end U64 + +end Lean4EVM diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 15ae128455..99f2c30dce 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -9284,3 +9284,55 @@ projects: - cycle-decompositions msc: - "05C45" + - slug: lean4evm + title: Verified Ethereum Virtual Machine primitives + summary: >- + Formalizes reusable fixed-width unsigned integers and fixed-size byte values for the + Ethereum Virtual Machine, including wrapping arithmetic, shifts, signed operations, + modular arithmetic, byte extraction, sign extension, and checked width conversions. + branch: fixed-width arithmetic and byte representations + entry_module: LeanPool.Lean4EVM + authors: + - mrLSD + source: + title: Lean4EVM + authors: + - mrLSD + url: https://github.com/mrLSD/Lean4EVM + github_repo: mrLSD/Lean4EVM + commit: 0109646545bc1f29c719c1268bad7c561d2035f8 + license: MIT + status: verified + provenance: human + main_declarations: + - Lean4EVM.U256.toNat_addmod + - Lean4EVM.U256.toNat_mulmod + main_results: + - declaration: Lean4EVM.FixedUInt.toNat_add + informal: >- + The natural value of fixed-width wrapping addition is the sum of the operand values + reduced modulo the width's power-of-two modulus. + - declaration: Lean4EVM.FixedUInt.toNat_mul + informal: >- + The natural value of fixed-width wrapping multiplication is the product of the operand + values reduced modulo the width's power-of-two modulus. + - declaration: Lean4EVM.U256.toNat_addmod + informal: >- + EVM ADDMOD returns zero for modulus zero and otherwise the exact sum of two 256-bit + words reduced modulo the supplied modulus. + - declaration: Lean4EVM.U256.toNat_mulmod + informal: >- + EVM MULMOD returns zero for modulus zero and otherwise the exact product of two 256-bit + words reduced modulo the supplied modulus. + - declaration: Lean4EVM.U256.toNat_byteAt_of_lt + informal: >- + For a byte index below 32, EVM BYTE returns the word's natural value divided by + 2^(8*(31-index)), reduced modulo 256 (big-endian byte extraction). + tags: + - verified-algorithms + - ethereum + - fixed-width-arithmetic + - byte-representations + msc: + - "68Q60" + - "68V20"