refactor: redefine unsigned fixed width integers in terms of BitVec (#5323)
I made a few choices so far that can probably be discussed: - got rid of `modn` on `UInt`, nobody seems to use it apart from the definition of `shift` which can use normal `mod` - removed the previous defeq optimized definition of `USize.size` in favor for a normal one. The motivation was to allow `OfNat` to work which doesn't seem to be necessary anymore afaict. - Minimized uses of `.val`, should we maybe mark it deprecated? - Mostly got rid of `.val` in basically all theorems as the proper next level of API would now be `.toBitVec`. We could probably re-prove them but it would be more annoying given the change of definition. - Did not yet redefine `log2` in terms of `BitVec` as this would require a `log2` in `BitVec` as well, do we want this? - I added a couple of theorems around the relation of `<` on `UInt` and `Nat`. These were previously not needed because defeq was used all over the place to save us. I did not yet generalize these to all types as I wasn't sure if they are the appropriate lemma that we want to have.
This commit is contained in:
Henrik Böving
GitHub
parent
a04b476431
commit
19e06acc65
28 changed files with 553 additions and 422 deletions
|
|
@ -1385,6 +1385,7 @@ gen_injective_theorems% Except
|
|||
gen_injective_theorems% EStateM.Result
|
||||
gen_injective_theorems% Lean.Name
|
||||
gen_injective_theorems% Lean.Syntax
|
||||
gen_injective_theorems% BitVec
|
||||
|
||||
theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
|
||||
fun x => Nat.noConfusion x id
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ prelude
|
|||
import Init.WFTactics
|
||||
import Init.Data.Nat.Basic
|
||||
import Init.Data.Fin.Basic
|
||||
import Init.Data.UInt.Basic
|
||||
import Init.Data.UInt.BasicAux
|
||||
import Init.Data.Repr
|
||||
import Init.Data.ToString.Basic
|
||||
import Init.GetElem
|
||||
|
|
|
|||
|
|
@ -8,12 +8,13 @@ import Init.Data.Fin.Basic
|
|||
import Init.Data.Nat.Bitwise.Lemmas
|
||||
import Init.Data.Nat.Power2
|
||||
import Init.Data.Int.Bitwise
|
||||
import Init.Data.BitVec.BasicAux
|
||||
|
||||
/-!
|
||||
We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
|
||||
(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
|
||||
with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
|
||||
representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
|
||||
We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
|
||||
others for its relative efficiency (Lean has special support for `Nat`), and the fact that bitwise
|
||||
operations on `Fin` are already defined. Some other possible representations are `List Bool`,
|
||||
`{ l : List Bool // l.length = w }`, `Fin w → Bool`.
|
||||
|
||||
We define many of the bitvector operations from the
|
||||
[`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
|
||||
|
|
@ -22,60 +23,12 @@ of SMT-LIBv2.
|
|||
|
||||
set_option linter.missingDocs true
|
||||
|
||||
/--
|
||||
A bitvector of the specified width.
|
||||
|
||||
This is represented as the underlying `Nat` number in both the runtime
|
||||
and the kernel, inheriting all the special support for `Nat`.
|
||||
-/
|
||||
structure BitVec (w : Nat) where
|
||||
/-- Construct a `BitVec w` from a number less than `2^w`.
|
||||
O(1), because we use `Fin` as the internal representation of a bitvector. -/
|
||||
ofFin ::
|
||||
/-- Interpret a bitvector as a number less than `2^w`.
|
||||
O(1), because we use `Fin` as the internal representation of a bitvector. -/
|
||||
toFin : Fin (2^w)
|
||||
|
||||
/--
|
||||
Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
|
||||
-/
|
||||
-- We manually derive the `DecidableEq` instances for `BitVec` because
|
||||
-- we want to have builtin support for bit-vector literals, and we
|
||||
-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
|
||||
def BitVec.decEq (x y : BitVec n) : Decidable (x = y) :=
|
||||
match x, y with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
if h : n = m then
|
||||
isTrue (h ▸ rfl)
|
||||
else
|
||||
isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
instance : DecidableEq (BitVec n) := BitVec.decEq
|
||||
|
||||
namespace BitVec
|
||||
|
||||
section Nat
|
||||
|
||||
/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
|
||||
@[match_pattern]
|
||||
protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
|
||||
toFin := ⟨i, p⟩
|
||||
|
||||
/-- The `BitVec` with value `i mod 2^n`. -/
|
||||
@[match_pattern]
|
||||
protected def ofNat (n : Nat) (i : Nat) : BitVec n where
|
||||
toFin := Fin.ofNat' (2^n) i
|
||||
|
||||
instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
|
||||
instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
|
||||
|
||||
/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
|
||||
(zero-cost) wrapper around a `Nat`. -/
|
||||
protected def toNat (x : BitVec n) : Nat := x.toFin.val
|
||||
|
||||
/-- Return the bound in terms of toNat. -/
|
||||
theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
|
||||
|
||||
@[deprecated isLt (since := "2024-03-12")]
|
||||
theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
|
||||
|
||||
|
|
@ -238,22 +191,6 @@ end repr_toString
|
|||
|
||||
section arithmetic
|
||||
|
||||
/--
|
||||
Addition for bit vectors. This can be interpreted as either signed or unsigned addition
|
||||
modulo `2^n`.
|
||||
|
||||
SMT-Lib name: `bvadd`.
|
||||
-/
|
||||
protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
|
||||
instance : Add (BitVec n) := ⟨BitVec.add⟩
|
||||
|
||||
/--
|
||||
Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
|
||||
modulo `2^n`.
|
||||
-/
|
||||
protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
|
||||
instance : Sub (BitVec n) := ⟨BitVec.sub⟩
|
||||
|
||||
/--
|
||||
Negation for bit vectors. This can be interpreted as either signed or unsigned negation
|
||||
modulo `2^n`.
|
||||
|
|
@ -387,10 +324,6 @@ SMT-Lib name: `bvult`.
|
|||
-/
|
||||
protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
|
||||
|
||||
instance : LT (BitVec n) where lt := (·.toNat < ·.toNat)
|
||||
instance (x y : BitVec n) : Decidable (x < y) :=
|
||||
inferInstanceAs (Decidable (x.toNat < y.toNat))
|
||||
|
||||
/--
|
||||
Unsigned less-than-or-equal-to for bit vectors.
|
||||
|
||||
|
|
@ -398,10 +331,6 @@ SMT-Lib name: `bvule`.
|
|||
-/
|
||||
protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat
|
||||
|
||||
instance : LE (BitVec n) where le := (·.toNat ≤ ·.toNat)
|
||||
instance (x y : BitVec n) : Decidable (x ≤ y) :=
|
||||
inferInstanceAs (Decidable (x.toNat ≤ y.toNat))
|
||||
|
||||
/--
|
||||
Signed less-than for bit vectors.
|
||||
|
||||
|
|
|
|||
52
src/Init/Data/BitVec/BasicAux.lean
Normal file
52
src/Init/Data/BitVec/BasicAux.lean
Normal file
|
|
@ -0,0 +1,52 @@
|
|||
/-
|
||||
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Fin.Basic
|
||||
|
||||
set_option linter.missingDocs true
|
||||
|
||||
/-!
|
||||
This module exists to provide the very basic `BitVec` definitions required for
|
||||
`Init.Data.UInt.BasicAux`.
|
||||
-/
|
||||
|
||||
namespace BitVec
|
||||
|
||||
section Nat
|
||||
|
||||
/-- The `BitVec` with value `i mod 2^n`. -/
|
||||
@[match_pattern]
|
||||
protected def ofNat (n : Nat) (i : Nat) : BitVec n where
|
||||
toFin := Fin.ofNat' (2^n) i
|
||||
|
||||
instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
|
||||
|
||||
/-- Return the bound in terms of toNat. -/
|
||||
theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
|
||||
|
||||
end Nat
|
||||
|
||||
section arithmetic
|
||||
|
||||
/--
|
||||
Addition for bit vectors. This can be interpreted as either signed or unsigned addition
|
||||
modulo `2^n`.
|
||||
|
||||
SMT-Lib name: `bvadd`.
|
||||
-/
|
||||
protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
|
||||
instance : Add (BitVec n) := ⟨BitVec.add⟩
|
||||
|
||||
/--
|
||||
Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
|
||||
modulo `2^n`.
|
||||
-/
|
||||
protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
|
||||
instance : Sub (BitVec n) := ⟨BitVec.sub⟩
|
||||
|
||||
end arithmetic
|
||||
|
||||
end BitVec
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.UInt.Basic
|
||||
import Init.Data.UInt.BasicAux
|
||||
|
||||
/-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).
|
||||
|
||||
|
|
@ -42,8 +42,10 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
|
|||
|
||||
theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
|
||||
match h with
|
||||
| Or.inl h => Or.inl h
|
||||
| Or.inr ⟨h₁, h₂⟩ => Or.inr ⟨h₁, h₂⟩
|
||||
| Or.inl h =>
|
||||
Or.inl (UInt32.ofNat'_lt_of_lt _ (by decide) h)
|
||||
| Or.inr ⟨h₁, h₂⟩ =>
|
||||
Or.inr ⟨UInt32.lt_ofNat'_of_lt _ (by decide) h₁, UInt32.ofNat'_lt_of_lt _ (by decide) h₂⟩
|
||||
|
||||
theorem isValidChar_zero : isValidChar 0 :=
|
||||
Or.inl (by decide)
|
||||
|
|
@ -57,7 +59,7 @@ theorem isValidChar_zero : isValidChar 0 :=
|
|||
c.val.toUInt8
|
||||
|
||||
/-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other. -/
|
||||
def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.1.2 (by decide))⟩
|
||||
def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.toBitVec.isLt (by decide))⟩
|
||||
|
||||
instance : Inhabited Char where
|
||||
default := 'A'
|
||||
|
|
|
|||
|
|
@ -796,6 +796,8 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
|
|||
| zero => cases h
|
||||
| succ n => simp [Nat.pow_succ]
|
||||
|
||||
protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
|
||||
|
||||
instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
|
||||
⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -8,8 +8,6 @@ import Init.Data.Nat.Linear
|
|||
|
||||
namespace Nat
|
||||
|
||||
protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
|
||||
|
||||
theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
|
||||
have : power * 2 = power + power := by simp_arith
|
||||
rw [this, Nat.sub_add_eq]
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ prelude
|
|||
import Init.Data.Format.Basic
|
||||
import Init.Data.Int.Basic
|
||||
import Init.Data.Nat.Div
|
||||
import Init.Data.UInt.Basic
|
||||
import Init.Data.UInt.BasicAux
|
||||
import Init.Control.Id
|
||||
open Sum Subtype Nat
|
||||
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Author: Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import Init.Data.ByteArray
|
||||
import Init.Data.UInt.Lemmas
|
||||
|
||||
namespace String
|
||||
|
||||
|
|
@ -20,14 +21,14 @@ def toNat! (s : String) : Nat :=
|
|||
def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
|
||||
let c ← a[i]?
|
||||
if c &&& 0x80 == 0 then
|
||||
some ⟨c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))⟩
|
||||
some ⟨c.toUInt32, .inl (Nat.lt_trans c.toBitVec.isLt (by decide))⟩
|
||||
else if c &&& 0xe0 == 0xc0 then
|
||||
let c1 ← a[i+1]?
|
||||
guard (c1 &&& 0xc0 == 0x80)
|
||||
let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32
|
||||
guard (0x80 ≤ r)
|
||||
-- TODO: Prove h from the definition of r once we have the necessary lemmas
|
||||
if h : r < 0xd800 then some ⟨r, .inl h⟩ else none
|
||||
if h : r < 0xd800 then some ⟨r, .inl (UInt32.toNat_lt_of_lt (by decide) h)⟩ else none
|
||||
else if c &&& 0xf0 == 0xe0 then
|
||||
let c1 ← a[i+1]?
|
||||
let c2 ← a[i+2]?
|
||||
|
|
@ -38,7 +39,14 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
|
|||
(c2 &&& 0x3f).toUInt32
|
||||
guard (0x800 ≤ r)
|
||||
-- TODO: Prove `r < 0x110000` from the definition of r once we have the necessary lemmas
|
||||
if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then some ⟨r, h⟩ else none
|
||||
if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then
|
||||
have :=
|
||||
match h with
|
||||
| .inl h => Or.inl (UInt32.toNat_lt_of_lt (by decide) h)
|
||||
| .inr h => Or.inr ⟨UInt32.lt_toNat_of_lt (by decide) h.left, UInt32.toNat_lt_of_lt (by decide) h.right⟩
|
||||
some ⟨r, this⟩
|
||||
else
|
||||
none
|
||||
else if c &&& 0xf8 == 0xf0 then
|
||||
let c1 ← a[i+1]?
|
||||
let c2 ← a[i+2]?
|
||||
|
|
@ -50,7 +58,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
|
|||
((c2 &&& 0x3f).toUInt32 <<< 6) |||
|
||||
(c3 &&& 0x3f).toUInt32
|
||||
if h : 0x10000 ≤ r ∧ r < 0x110000 then
|
||||
some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) h.1, h.2⟩⟩
|
||||
some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) (UInt32.le_toNat_of_le (by decide) h.left), UInt32.toNat_lt_of_lt (by decide) h.right⟩⟩
|
||||
else none
|
||||
else
|
||||
none
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Author: Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import Init.Data.String.Basic
|
||||
import Init.Data.UInt.Basic
|
||||
import Init.Data.UInt.BasicAux
|
||||
import Init.Data.Nat.Div
|
||||
import Init.Data.Repr
|
||||
import Init.Data.Int.Basic
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Henrik Böving
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.UInt.BasicAux
|
||||
import Init.Data.UInt.Basic
|
||||
import Init.Data.UInt.Log2
|
||||
import Init.Data.UInt.Lemmas
|
||||
|
|
|
|||
|
|
@ -4,52 +4,50 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Fin.Basic
|
||||
import Init.Data.UInt.BasicAux
|
||||
import Init.Data.BitVec.Basic
|
||||
|
||||
open Nat
|
||||
|
||||
@[extern "lean_uint8_of_nat"]
|
||||
def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
|
||||
abbrev Nat.toUInt8 := UInt8.ofNat
|
||||
@[extern "lean_uint8_to_nat"]
|
||||
def UInt8.toNat (n : UInt8) : Nat := n.val.val
|
||||
@[extern "lean_uint8_add"]
|
||||
def UInt8.add (a b : UInt8) : UInt8 := ⟨a.val + b.val⟩
|
||||
def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
|
||||
@[extern "lean_uint8_sub"]
|
||||
def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.val - b.val⟩
|
||||
def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩
|
||||
@[extern "lean_uint8_mul"]
|
||||
def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.val * b.val⟩
|
||||
def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
|
||||
@[extern "lean_uint8_div"]
|
||||
def UInt8.div (a b : UInt8) : UInt8 := ⟨a.val / b.val⟩
|
||||
def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint8_mod"]
|
||||
def UInt8.mod (a b : UInt8) : UInt8 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint8_modn"]
|
||||
def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
|
||||
def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨Fin.modn a.val n⟩
|
||||
@[extern "lean_uint8_land"]
|
||||
def UInt8.land (a b : UInt8) : UInt8 := ⟨Fin.land a.val b.val⟩
|
||||
def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint8_lor"]
|
||||
def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
|
||||
def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩
|
||||
@[extern "lean_uint8_xor"]
|
||||
def UInt8.xor (a b : UInt8) : UInt8 := ⟨Fin.xor a.val b.val⟩
|
||||
def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩
|
||||
@[extern "lean_uint8_shift_left"]
|
||||
def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.val <<< (modn b 8).val⟩
|
||||
def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (mod b 8).toBitVec⟩
|
||||
@[extern "lean_uint8_shift_right"]
|
||||
def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
|
||||
def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
|
||||
def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
|
||||
def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (mod b 8).toBitVec⟩
|
||||
def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
|
||||
def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
|
||||
|
||||
instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
|
||||
instance : Add UInt8 := ⟨UInt8.add⟩
|
||||
instance : Sub UInt8 := ⟨UInt8.sub⟩
|
||||
instance : Mul UInt8 := ⟨UInt8.mul⟩
|
||||
instance : Mod UInt8 := ⟨UInt8.mod⟩
|
||||
|
||||
set_option linter.deprecated false in
|
||||
instance : HMod UInt8 Nat UInt8 := ⟨UInt8.modn⟩
|
||||
|
||||
instance : Div UInt8 := ⟨UInt8.div⟩
|
||||
instance : LT UInt8 := ⟨UInt8.lt⟩
|
||||
instance : LE UInt8 := ⟨UInt8.le⟩
|
||||
|
||||
@[extern "lean_uint8_complement"]
|
||||
def UInt8.complement (a:UInt8) : UInt8 := 0-(a+1)
|
||||
def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩
|
||||
|
||||
instance : Complement UInt8 := ⟨UInt8.complement⟩
|
||||
instance : AndOp UInt8 := ⟨UInt8.land⟩
|
||||
|
|
@ -58,69 +56,58 @@ instance : Xor UInt8 := ⟨UInt8.xor⟩
|
|||
instance : ShiftLeft UInt8 := ⟨UInt8.shiftLeft⟩
|
||||
instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_uint8_dec_lt"]
|
||||
def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_uint8_dec_le"]
|
||||
def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
|
||||
|
||||
instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
|
||||
instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
|
||||
instance : Max UInt8 := maxOfLe
|
||||
instance : Min UInt8 := minOfLe
|
||||
|
||||
@[extern "lean_uint16_of_nat"]
|
||||
def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
|
||||
abbrev Nat.toUInt16 := UInt16.ofNat
|
||||
@[extern "lean_uint16_to_nat"]
|
||||
def UInt16.toNat (n : UInt16) : Nat := n.val.val
|
||||
@[extern "lean_uint16_add"]
|
||||
def UInt16.add (a b : UInt16) : UInt16 := ⟨a.val + b.val⟩
|
||||
def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
|
||||
@[extern "lean_uint16_sub"]
|
||||
def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.val - b.val⟩
|
||||
def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩
|
||||
@[extern "lean_uint16_mul"]
|
||||
def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.val * b.val⟩
|
||||
def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
|
||||
@[extern "lean_uint16_div"]
|
||||
def UInt16.div (a b : UInt16) : UInt16 := ⟨a.val / b.val⟩
|
||||
def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint16_mod"]
|
||||
def UInt16.mod (a b : UInt16) : UInt16 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint16_modn"]
|
||||
def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
|
||||
def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨Fin.modn a.val n⟩
|
||||
@[extern "lean_uint16_land"]
|
||||
def UInt16.land (a b : UInt16) : UInt16 := ⟨Fin.land a.val b.val⟩
|
||||
def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint16_lor"]
|
||||
def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩
|
||||
def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
|
||||
@[extern "lean_uint16_xor"]
|
||||
def UInt16.xor (a b : UInt16) : UInt16 := ⟨Fin.xor a.val b.val⟩
|
||||
def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩
|
||||
@[extern "lean_uint16_shift_left"]
|
||||
def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.val <<< (modn b 16).val⟩
|
||||
@[extern "lean_uint16_to_uint8"]
|
||||
def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
|
||||
@[extern "lean_uint8_to_uint16"]
|
||||
def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
|
||||
def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (mod b 16).toBitVec⟩
|
||||
@[extern "lean_uint16_shift_right"]
|
||||
def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
|
||||
def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
|
||||
def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
|
||||
def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (mod b 16).toBitVec⟩
|
||||
def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
|
||||
def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
|
||||
|
||||
instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
|
||||
instance : Add UInt16 := ⟨UInt16.add⟩
|
||||
instance : Sub UInt16 := ⟨UInt16.sub⟩
|
||||
instance : Mul UInt16 := ⟨UInt16.mul⟩
|
||||
instance : Mod UInt16 := ⟨UInt16.mod⟩
|
||||
|
||||
set_option linter.deprecated false in
|
||||
instance : HMod UInt16 Nat UInt16 := ⟨UInt16.modn⟩
|
||||
|
||||
instance : Div UInt16 := ⟨UInt16.div⟩
|
||||
instance : LT UInt16 := ⟨UInt16.lt⟩
|
||||
instance : LE UInt16 := ⟨UInt16.le⟩
|
||||
|
||||
@[extern "lean_uint16_complement"]
|
||||
def UInt16.complement (a:UInt16) : UInt16 := 0-(a+1)
|
||||
def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩
|
||||
|
||||
instance : Complement UInt16 := ⟨UInt16.complement⟩
|
||||
instance : AndOp UInt16 := ⟨UInt16.land⟩
|
||||
|
|
@ -132,74 +119,53 @@ instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
|
|||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_uint16_dec_lt"]
|
||||
def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_uint16_dec_le"]
|
||||
def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
|
||||
|
||||
instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
|
||||
instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
|
||||
instance : Max UInt16 := maxOfLe
|
||||
instance : Min UInt16 := minOfLe
|
||||
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
|
||||
/--
|
||||
Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
|
||||
-/
|
||||
def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
|
||||
if h : n < UInt32.size then
|
||||
UInt32.ofNat' n h
|
||||
else
|
||||
UInt32.ofNat' (UInt32.size - 1) (by decide)
|
||||
abbrev Nat.toUInt32 := UInt32.ofNat
|
||||
@[extern "lean_uint32_add"]
|
||||
def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
|
||||
def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
|
||||
@[extern "lean_uint32_sub"]
|
||||
def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.val - b.val⟩
|
||||
def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩
|
||||
@[extern "lean_uint32_mul"]
|
||||
def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.val * b.val⟩
|
||||
def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
|
||||
@[extern "lean_uint32_div"]
|
||||
def UInt32.div (a b : UInt32) : UInt32 := ⟨a.val / b.val⟩
|
||||
def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint32_mod"]
|
||||
def UInt32.mod (a b : UInt32) : UInt32 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint32_modn"]
|
||||
def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
|
||||
def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨Fin.modn a.val n⟩
|
||||
@[extern "lean_uint32_land"]
|
||||
def UInt32.land (a b : UInt32) : UInt32 := ⟨Fin.land a.val b.val⟩
|
||||
def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint32_lor"]
|
||||
def UInt32.lor (a b : UInt32) : UInt32 := ⟨Fin.lor a.val b.val⟩
|
||||
def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩
|
||||
@[extern "lean_uint32_xor"]
|
||||
def UInt32.xor (a b : UInt32) : UInt32 := ⟨Fin.xor a.val b.val⟩
|
||||
def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
|
||||
@[extern "lean_uint32_shift_left"]
|
||||
def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.val <<< (modn b 32).val⟩
|
||||
def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
|
||||
@[extern "lean_uint32_shift_right"]
|
||||
def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.val >>> (modn b 32).val⟩
|
||||
@[extern "lean_uint32_to_uint8"]
|
||||
def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
|
||||
@[extern "lean_uint32_to_uint16"]
|
||||
def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
|
||||
@[extern "lean_uint8_to_uint32"]
|
||||
def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
|
||||
@[extern "lean_uint16_to_uint32"]
|
||||
def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
|
||||
def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
|
||||
|
||||
instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
|
||||
instance : Add UInt32 := ⟨UInt32.add⟩
|
||||
instance : Sub UInt32 := ⟨UInt32.sub⟩
|
||||
instance : Mul UInt32 := ⟨UInt32.mul⟩
|
||||
instance : Mod UInt32 := ⟨UInt32.mod⟩
|
||||
|
||||
set_option linter.deprecated false in
|
||||
instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
|
||||
|
||||
instance : Div UInt32 := ⟨UInt32.div⟩
|
||||
|
||||
@[extern "lean_uint32_complement"]
|
||||
def UInt32.complement (a:UInt32) : UInt32 := 0-(a+1)
|
||||
def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩
|
||||
|
||||
instance : Complement UInt32 := ⟨UInt32.complement⟩
|
||||
instance : AndOp UInt32 := ⟨UInt32.land⟩
|
||||
|
|
@ -208,60 +174,45 @@ instance : Xor UInt32 := ⟨UInt32.xor⟩
|
|||
instance : ShiftLeft UInt32 := ⟨UInt32.shiftLeft⟩
|
||||
instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
|
||||
|
||||
@[extern "lean_uint64_of_nat"]
|
||||
def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
|
||||
abbrev Nat.toUInt64 := UInt64.ofNat
|
||||
@[extern "lean_uint64_to_nat"]
|
||||
def UInt64.toNat (n : UInt64) : Nat := n.val.val
|
||||
@[extern "lean_uint64_add"]
|
||||
def UInt64.add (a b : UInt64) : UInt64 := ⟨a.val + b.val⟩
|
||||
def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
|
||||
@[extern "lean_uint64_sub"]
|
||||
def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.val - b.val⟩
|
||||
def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩
|
||||
@[extern "lean_uint64_mul"]
|
||||
def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.val * b.val⟩
|
||||
def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
|
||||
@[extern "lean_uint64_div"]
|
||||
def UInt64.div (a b : UInt64) : UInt64 := ⟨a.val / b.val⟩
|
||||
def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint64_mod"]
|
||||
def UInt64.mod (a b : UInt64) : UInt64 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint64_modn"]
|
||||
def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
|
||||
@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
|
||||
def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨Fin.modn a.val n⟩
|
||||
@[extern "lean_uint64_land"]
|
||||
def UInt64.land (a b : UInt64) : UInt64 := ⟨Fin.land a.val b.val⟩
|
||||
def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_uint64_lor"]
|
||||
def UInt64.lor (a b : UInt64) : UInt64 := ⟨Fin.lor a.val b.val⟩
|
||||
def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩
|
||||
@[extern "lean_uint64_xor"]
|
||||
def UInt64.xor (a b : UInt64) : UInt64 := ⟨Fin.xor a.val b.val⟩
|
||||
def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩
|
||||
@[extern "lean_uint64_shift_left"]
|
||||
def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.val <<< (modn b 64).val⟩
|
||||
def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (mod b 64).toBitVec⟩
|
||||
@[extern "lean_uint64_shift_right"]
|
||||
def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.val >>> (modn b 64).val⟩
|
||||
def UInt64.lt (a b : UInt64) : Prop := a.val < b.val
|
||||
def UInt64.le (a b : UInt64) : Prop := a.val ≤ b.val
|
||||
@[extern "lean_uint64_to_uint8"]
|
||||
def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
|
||||
@[extern "lean_uint64_to_uint16"]
|
||||
def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
|
||||
@[extern "lean_uint64_to_uint32"]
|
||||
def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
|
||||
@[extern "lean_uint8_to_uint64"]
|
||||
def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
|
||||
@[extern "lean_uint16_to_uint64"]
|
||||
def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
|
||||
@[extern "lean_uint32_to_uint64"]
|
||||
def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
|
||||
def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (mod b 64).toBitVec⟩
|
||||
def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
|
||||
def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
|
||||
|
||||
instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
|
||||
instance : Add UInt64 := ⟨UInt64.add⟩
|
||||
instance : Sub UInt64 := ⟨UInt64.sub⟩
|
||||
instance : Mul UInt64 := ⟨UInt64.mul⟩
|
||||
instance : Mod UInt64 := ⟨UInt64.mod⟩
|
||||
|
||||
set_option linter.deprecated false in
|
||||
instance : HMod UInt64 Nat UInt64 := ⟨UInt64.modn⟩
|
||||
|
||||
instance : Div UInt64 := ⟨UInt64.div⟩
|
||||
instance : LT UInt64 := ⟨UInt64.lt⟩
|
||||
instance : LE UInt64 := ⟨UInt64.le⟩
|
||||
|
||||
@[extern "lean_uint64_complement"]
|
||||
def UInt64.complement (a:UInt64) : UInt64 := 0-(a+1)
|
||||
def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
|
||||
|
||||
instance : Complement UInt64 := ⟨UInt64.complement⟩
|
||||
instance : AndOp UInt64 := ⟨UInt64.land⟩
|
||||
|
|
@ -273,79 +224,52 @@ instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
|
|||
@[extern "lean_bool_to_uint64"]
|
||||
def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_uint64_dec_lt"]
|
||||
def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_uint64_dec_le"]
|
||||
def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
|
||||
|
||||
instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
|
||||
instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
|
||||
instance : Max UInt64 := maxOfLe
|
||||
instance : Min UInt64 := minOfLe
|
||||
|
||||
-- This instance would interfere with the global instance `NeZero (n + 1)`,
|
||||
-- so we only enable it locally.
|
||||
@[local instance]
|
||||
private def instNeZeroUSizeSize : NeZero USize.size := ⟨add_one_ne_zero _⟩
|
||||
|
||||
@[deprecated (since := "2024-09-16")]
|
||||
theorem usize_size_gt_zero : USize.size > 0 :=
|
||||
Nat.zero_lt_succ ..
|
||||
|
||||
@[extern "lean_usize_of_nat"]
|
||||
def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat' _ n⟩
|
||||
abbrev Nat.toUSize := USize.ofNat
|
||||
@[extern "lean_usize_to_nat"]
|
||||
def USize.toNat (n : USize) : Nat := n.val.val
|
||||
@[extern "lean_usize_add"]
|
||||
def USize.add (a b : USize) : USize := ⟨a.val + b.val⟩
|
||||
@[extern "lean_usize_sub"]
|
||||
def USize.sub (a b : USize) : USize := ⟨a.val - b.val⟩
|
||||
@[extern "lean_usize_mul"]
|
||||
def USize.mul (a b : USize) : USize := ⟨a.val * b.val⟩
|
||||
def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
|
||||
@[extern "lean_usize_div"]
|
||||
def USize.div (a b : USize) : USize := ⟨a.val / b.val⟩
|
||||
def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
|
||||
@[extern "lean_usize_mod"]
|
||||
def USize.mod (a b : USize) : USize := ⟨a.val % b.val⟩
|
||||
@[extern "lean_usize_modn"]
|
||||
def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
|
||||
@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
|
||||
def USize.modn (a : USize) (n : @& Nat) : USize := ⟨Fin.modn a.val n⟩
|
||||
@[extern "lean_usize_land"]
|
||||
def USize.land (a b : USize) : USize := ⟨Fin.land a.val b.val⟩
|
||||
def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
|
||||
@[extern "lean_usize_lor"]
|
||||
def USize.lor (a b : USize) : USize := ⟨Fin.lor a.val b.val⟩
|
||||
def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
|
||||
@[extern "lean_usize_xor"]
|
||||
def USize.xor (a b : USize) : USize := ⟨Fin.xor a.val b.val⟩
|
||||
def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
|
||||
@[extern "lean_usize_shift_left"]
|
||||
def USize.shiftLeft (a b : USize) : USize := ⟨a.val <<< (modn b System.Platform.numBits).val⟩
|
||||
def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
|
||||
@[extern "lean_usize_shift_right"]
|
||||
def USize.shiftRight (a b : USize) : USize := ⟨a.val >>> (modn b System.Platform.numBits).val⟩
|
||||
def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
|
||||
@[extern "lean_uint32_to_usize"]
|
||||
def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.val a.1.2
|
||||
def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
|
||||
@[extern "lean_usize_to_uint32"]
|
||||
def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
|
||||
|
||||
def USize.lt (a b : USize) : Prop := a.val < b.val
|
||||
def USize.le (a b : USize) : Prop := a.val ≤ b.val
|
||||
|
||||
instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
|
||||
instance : Add USize := ⟨USize.add⟩
|
||||
instance : Sub USize := ⟨USize.sub⟩
|
||||
instance : Mul USize := ⟨USize.mul⟩
|
||||
instance : Mod USize := ⟨USize.mod⟩
|
||||
|
||||
set_option linter.deprecated false in
|
||||
instance : HMod USize Nat USize := ⟨USize.modn⟩
|
||||
|
||||
instance : Div USize := ⟨USize.div⟩
|
||||
instance : LT USize := ⟨USize.lt⟩
|
||||
instance : LE USize := ⟨USize.le⟩
|
||||
|
||||
@[extern "lean_usize_complement"]
|
||||
def USize.complement (a:USize) : USize := 0-(a+1)
|
||||
def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩
|
||||
|
||||
instance : Complement USize := ⟨USize.complement⟩
|
||||
instance : AndOp USize := ⟨USize.land⟩
|
||||
|
|
@ -354,19 +278,5 @@ instance : Xor USize := ⟨USize.xor⟩
|
|||
instance : ShiftLeft USize := ⟨USize.shiftLeft⟩
|
||||
instance : ShiftRight USize := ⟨USize.shiftRight⟩
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_usize_dec_lt"]
|
||||
def USize.decLt (a b : USize) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern "lean_usize_dec_le"]
|
||||
def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
||||
instance (a b : USize) : Decidable (a < b) := USize.decLt a b
|
||||
instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
|
||||
instance : Max USize := maxOfLe
|
||||
instance : Min USize := minOfLe
|
||||
|
|
|
|||
132
src/Init/Data/UInt/BasicAux.lean
Normal file
132
src/Init/Data/UInt/BasicAux.lean
Normal file
|
|
@ -0,0 +1,132 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Fin.Basic
|
||||
import Init.Data.BitVec.BasicAux
|
||||
|
||||
/-!
|
||||
This module exists to provide the very basic `UInt8` etc. definitions required for
|
||||
`Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
|
||||
meta code that is then (transitively) used in `Init.Data.UInt.Basic` and `Init.Data.BitVec.Basic`.
|
||||
This file thus breaks the import cycle that would be created by this dependency.
|
||||
-/
|
||||
|
||||
open Nat
|
||||
|
||||
def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
|
||||
@[extern "lean_uint8_of_nat"]
|
||||
def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
|
||||
abbrev Nat.toUInt8 := UInt8.ofNat
|
||||
@[extern "lean_uint8_to_nat"]
|
||||
def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
|
||||
|
||||
instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
|
||||
|
||||
def UInt16.val (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
|
||||
@[extern "lean_uint16_of_nat"]
|
||||
def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩
|
||||
abbrev Nat.toUInt16 := UInt16.ofNat
|
||||
@[extern "lean_uint16_to_nat"]
|
||||
def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
|
||||
@[extern "lean_uint16_to_uint8"]
|
||||
def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
|
||||
@[extern "lean_uint8_to_uint16"]
|
||||
def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
|
||||
|
||||
instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
|
||||
|
||||
def UInt32.val (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨BitVec.ofNatLt n h⟩
|
||||
/--
|
||||
Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
|
||||
-/
|
||||
def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
|
||||
if h : n < UInt32.size then
|
||||
UInt32.ofNat' n h
|
||||
else
|
||||
UInt32.ofNat' (UInt32.size - 1) (by decide)
|
||||
abbrev Nat.toUInt32 := UInt32.ofNat
|
||||
@[extern "lean_uint32_to_uint8"]
|
||||
def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
|
||||
@[extern "lean_uint32_to_uint16"]
|
||||
def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
|
||||
@[extern "lean_uint8_to_uint32"]
|
||||
def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
|
||||
@[extern "lean_uint16_to_uint32"]
|
||||
def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
|
||||
|
||||
instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
|
||||
|
||||
theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
|
||||
n < m → UInt32.ofNat' n h1 < UInt32.ofNat m := by
|
||||
simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
|
||||
Nat.mod_eq_of_lt h2, imp_self]
|
||||
|
||||
theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
|
||||
m < n → UInt32.ofNat m < UInt32.ofNat' n h1 := by
|
||||
simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
|
||||
Nat.mod_eq_of_lt h2, imp_self]
|
||||
|
||||
def UInt64.val (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
|
||||
@[extern "lean_uint64_of_nat"]
|
||||
def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩
|
||||
abbrev Nat.toUInt64 := UInt64.ofNat
|
||||
@[extern "lean_uint64_to_nat"]
|
||||
def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat
|
||||
@[extern "lean_uint64_to_uint8"]
|
||||
def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
|
||||
@[extern "lean_uint64_to_uint16"]
|
||||
def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
|
||||
@[extern "lean_uint64_to_uint32"]
|
||||
def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
|
||||
@[extern "lean_uint8_to_uint64"]
|
||||
def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
|
||||
@[extern "lean_uint16_to_uint64"]
|
||||
def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
|
||||
@[extern "lean_uint32_to_uint64"]
|
||||
def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
|
||||
|
||||
instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
|
||||
|
||||
theorem usize_size_gt_zero : USize.size > 0 := by
|
||||
cases usize_size_eq with
|
||||
| inl h => rw [h]; decide
|
||||
| inr h => rw [h]; decide
|
||||
|
||||
def USize.val (x : USize) : Fin USize.size := x.toBitVec.toFin
|
||||
@[extern "lean_usize_of_nat"]
|
||||
def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩
|
||||
abbrev Nat.toUSize := USize.ofNat
|
||||
@[extern "lean_usize_to_nat"]
|
||||
def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
|
||||
@[extern "lean_usize_add"]
|
||||
def USize.add (a b : USize) : USize := ⟨a.toBitVec + b.toBitVec⟩
|
||||
@[extern "lean_usize_sub"]
|
||||
def USize.sub (a b : USize) : USize := ⟨a.toBitVec - b.toBitVec⟩
|
||||
|
||||
def USize.lt (a b : USize) : Prop := a.toBitVec < b.toBitVec
|
||||
def USize.le (a b : USize) : Prop := a.toBitVec ≤ b.toBitVec
|
||||
|
||||
instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
|
||||
|
||||
instance : Add USize := ⟨USize.add⟩
|
||||
instance : Sub USize := ⟨USize.sub⟩
|
||||
instance : LT USize := ⟨USize.lt⟩
|
||||
instance : LE USize := ⟨USize.le⟩
|
||||
|
||||
@[extern "lean_usize_dec_lt"]
|
||||
def USize.decLt (a b : USize) : Decidable (a < b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
|
||||
|
||||
@[extern "lean_usize_dec_le"]
|
||||
def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
|
||||
inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
|
||||
|
||||
instance (a b : USize) : Decidable (a < b) := USize.decLt a b
|
||||
instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
|
||||
|
|
@ -6,13 +6,14 @@ Authors: Markus Himmel
|
|||
prelude
|
||||
import Init.Data.UInt.Basic
|
||||
import Init.Data.Fin.Bitwise
|
||||
import Init.Data.BitVec.Lemmas
|
||||
|
||||
set_option hygiene false in
|
||||
macro "declare_bitwise_uint_theorems" typeName:ident : command =>
|
||||
`(
|
||||
namespace $typeName
|
||||
|
||||
@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
|
||||
@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
|
||||
|
||||
end $typeName
|
||||
)
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Leonardo de Moura
|
|||
prelude
|
||||
import Init.Data.UInt.Basic
|
||||
import Init.Data.Fin.Lemmas
|
||||
import Init.Data.BitVec.Lemmas
|
||||
import Init.Data.BitVec.Bitblast
|
||||
|
||||
set_option hygiene false in
|
||||
macro "declare_uint_theorems" typeName:ident : command =>
|
||||
|
|
@ -17,48 +19,100 @@ instance : Inhabited $typeName where
|
|||
|
||||
theorem zero_def : (0 : $typeName) = ⟨0⟩ := rfl
|
||||
theorem one_def : (1 : $typeName) = ⟨1⟩ := rfl
|
||||
theorem sub_def (a b : $typeName) : a - b = ⟨a.val - b.val⟩ := rfl
|
||||
theorem mul_def (a b : $typeName) : a * b = ⟨a.val * b.val⟩ := rfl
|
||||
theorem mod_def (a b : $typeName) : a % b = ⟨a.val % b.val⟩ := rfl
|
||||
theorem add_def (a b : $typeName) : a + b = ⟨a.val + b.val⟩ := rfl
|
||||
theorem sub_def (a b : $typeName) : a - b = ⟨a.toBitVec - b.toBitVec⟩ := rfl
|
||||
theorem mul_def (a b : $typeName) : a * b = ⟨a.toBitVec * b.toBitVec⟩ := rfl
|
||||
theorem mod_def (a b : $typeName) : a % b = ⟨a.toBitVec % b.toBitVec⟩ := rfl
|
||||
theorem add_def (a b : $typeName) : a + b = ⟨a.toBitVec + b.toBitVec⟩ := rfl
|
||||
|
||||
@[simp] theorem mk_val_eq : ∀ (a : $typeName), mk a.val = a
|
||||
@[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
|
||||
| ⟨_, _⟩ => rfl
|
||||
theorem val_eq_of_lt {a : Nat} : a < size → ((ofNat a).val : Nat) = a :=
|
||||
Nat.mod_eq_of_lt
|
||||
theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
|
||||
rw [toNat, val_eq_of_lt h]
|
||||
|
||||
theorem le_def {a b : $typeName} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
|
||||
theorem lt_def {a b : $typeName} : a < b ↔ a.1 < b.1 := .rfl
|
||||
theorem lt_iff_val_lt_val {a b : $typeName} : a < b ↔ a.val < b.val := .rfl
|
||||
@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := Fin.not_le
|
||||
@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := Fin.not_lt
|
||||
theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
|
||||
Nat.mod_eq_of_lt
|
||||
|
||||
theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
|
||||
rw [toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
|
||||
|
||||
theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
|
||||
|
||||
@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := by simp [le_def, lt_def]
|
||||
|
||||
@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := by simp [le_def, lt_def]
|
||||
|
||||
@[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
|
||||
|
||||
@[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
|
||||
protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := Fin.le_trans
|
||||
protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := Fin.lt_trans
|
||||
protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := Fin.le_total a.1 b.1
|
||||
protected theorem lt_asymm {a b : $typeName} (h : a < b) : ¬ b < a := Fin.lt_asymm h
|
||||
protected theorem val_eq_of_eq {a b : $typeName} (h : a = b) : a.val = b.val := h ▸ rfl
|
||||
protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by cases a; cases b; simp at h; simp [h]
|
||||
open $typeName (val_eq_of_eq) in
|
||||
protected theorem ne_of_val_ne {a b : $typeName} (h : a.val ≠ b.val) : a ≠ b := fun h' => absurd (val_eq_of_eq h') h
|
||||
open $typeName (ne_of_val_ne) in
|
||||
protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_ne (Fin.ne_of_lt h)
|
||||
|
||||
protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
|
||||
|
||||
protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
|
||||
|
||||
protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
|
||||
|
||||
protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
|
||||
|
||||
protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
|
||||
|
||||
protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
|
||||
cases a; cases b; simp_all
|
||||
|
||||
open $typeName (eq_of_toBitVec_eq) in
|
||||
protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
|
||||
rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
|
||||
|
||||
open $typeName (toBitVec_eq_of_eq) in
|
||||
protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
|
||||
fun h' => absurd (toBitVec_eq_of_eq h') h
|
||||
|
||||
open $typeName (ne_of_toBitVec_ne) in
|
||||
protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
|
||||
apply ne_of_toBitVec_ne
|
||||
apply BitVec.ne_of_lt
|
||||
simpa [lt_def] using h
|
||||
|
||||
@[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
|
||||
@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
|
||||
@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
|
||||
@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
|
||||
@[simp] protected theorem toNat_modn (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
|
||||
protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m
|
||||
| ⟨u⟩, h => Fin.modn_lt u h
|
||||
open $typeName (modn_lt) in
|
||||
protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
|
||||
|
||||
@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
|
||||
|
||||
@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv ..
|
||||
|
||||
@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := BitVec.toNat_sub_of_le
|
||||
|
||||
protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
|
||||
|
||||
open $typeName (toNat_mod toNat_lt_size) in
|
||||
protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % ofNat m) < m := by
|
||||
intro u h1
|
||||
by_cases h2 : m < size
|
||||
· rw [toNat_mod, toNat_ofNat_of_lt h2]
|
||||
apply Nat.mod_lt _ h1
|
||||
· apply Nat.lt_of_lt_of_le
|
||||
· apply toNat_lt_size
|
||||
· simpa using h2
|
||||
|
||||
open $typeName (toNat_mod_lt) in
|
||||
set_option linter.deprecated false in
|
||||
@[deprecated toNat_mod_lt (since := "2024-09-24")]
|
||||
protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
|
||||
intro u
|
||||
simp only [(· % ·)]
|
||||
simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
|
||||
Nat.reducePow]
|
||||
rw [Nat.mod_eq_of_lt]
|
||||
· apply Nat.mod_lt
|
||||
· apply Nat.lt_of_le_of_lt
|
||||
· apply Nat.mod_le
|
||||
· apply Fin.is_lt
|
||||
|
||||
protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
|
||||
simp only [lt_def, mod_def]
|
||||
apply BitVec.umod_lt
|
||||
|
||||
protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
|
||||
| ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
|
||||
protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.1.2
|
||||
|
||||
@[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
|
||||
|
||||
end $typeName
|
||||
|
|
@ -70,27 +124,34 @@ declare_uint_theorems UInt32
|
|||
declare_uint_theorems UInt64
|
||||
declare_uint_theorems USize
|
||||
|
||||
theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
|
||||
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
|
||||
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
|
||||
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
|
||||
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
|
||||
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt8.modn_toNat := @UInt8.toNat_modn
|
||||
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt16.modn_toNat := @UInt16.toNat_modn
|
||||
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt32.modn_toNat := @UInt32.toNat_modn
|
||||
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev UInt64.modn_toNat := @UInt64.toNat_modn
|
||||
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod
|
||||
@[deprecated (since := "2024-06-23")] protected abbrev USize.modn_toNat := @USize.toNat_modn
|
||||
|
|
|
|||
|
|
@ -7,16 +7,16 @@ prelude
|
|||
import Init.Data.Fin.Log2
|
||||
|
||||
@[extern "lean_uint8_log2"]
|
||||
def UInt8.log2 (a : UInt8) : UInt8 := ⟨Fin.log2 a.val⟩
|
||||
def UInt8.log2 (a : UInt8) : UInt8 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
|
||||
@[extern "lean_uint16_log2"]
|
||||
def UInt16.log2 (a : UInt16) : UInt16 := ⟨Fin.log2 a.val⟩
|
||||
def UInt16.log2 (a : UInt16) : UInt16 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
|
||||
@[extern "lean_uint32_log2"]
|
||||
def UInt32.log2 (a : UInt32) : UInt32 := ⟨Fin.log2 a.val⟩
|
||||
def UInt32.log2 (a : UInt32) : UInt32 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
|
||||
@[extern "lean_uint64_log2"]
|
||||
def UInt64.log2 (a : UInt64) : UInt64 := ⟨Fin.log2 a.val⟩
|
||||
def UInt64.log2 (a : UInt64) : UInt64 := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
|
||||
@[extern "lean_usize_log2"]
|
||||
def USize.log2 (a : USize) : USize := ⟨Fin.log2 a.val⟩
|
||||
def USize.log2 (a : USize) : USize := ⟨⟨Fin.log2 a.val⟩⟩
|
||||
|
|
|
|||
|
|
@ -1866,6 +1866,52 @@ instance {n} : LE (Fin n) where
|
|||
instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b) := Nat.decLt ..
|
||||
instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..
|
||||
|
||||
/--
|
||||
A bitvector of the specified width.
|
||||
|
||||
This is represented as the underlying `Nat` number in both the runtime
|
||||
and the kernel, inheriting all the special support for `Nat`.
|
||||
-/
|
||||
structure BitVec (w : Nat) where
|
||||
/-- Construct a `BitVec w` from a number less than `2^w`.
|
||||
O(1), because we use `Fin` as the internal representation of a bitvector. -/
|
||||
ofFin ::
|
||||
/-- Interpret a bitvector as a number less than `2^w`.
|
||||
O(1), because we use `Fin` as the internal representation of a bitvector. -/
|
||||
toFin : Fin (hPow 2 w)
|
||||
|
||||
/--
|
||||
Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
|
||||
-/
|
||||
-- We manually derive the `DecidableEq` instances for `BitVec` because
|
||||
-- we want to have builtin support for bit-vector literals, and we
|
||||
-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
|
||||
def BitVec.decEq (x y : BitVec n) : Decidable (Eq x y) :=
|
||||
match x, y with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
dite (Eq n m)
|
||||
(fun h => isTrue (h ▸ rfl))
|
||||
(fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))
|
||||
|
||||
instance : DecidableEq (BitVec n) := BitVec.decEq
|
||||
|
||||
/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
|
||||
@[match_pattern]
|
||||
protected def BitVec.ofNatLt {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
|
||||
toFin := ⟨i, p⟩
|
||||
|
||||
/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
|
||||
(zero-cost) wrapper around a `Nat`. -/
|
||||
protected def BitVec.toNat (x : BitVec n) : Nat := x.toFin.val
|
||||
|
||||
instance : LT (BitVec n) where lt := (LT.lt ·.toNat ·.toNat)
|
||||
instance (x y : BitVec n) : Decidable (LT.lt x y) :=
|
||||
inferInstanceAs (Decidable (LT.lt x.toNat y.toNat))
|
||||
|
||||
instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)
|
||||
instance (x y : BitVec n) : Decidable (LE.le x y) :=
|
||||
inferInstanceAs (Decidable (LE.le x.toNat y.toNat))
|
||||
|
||||
/-- The size of type `UInt8`, that is, `2^8 = 256`. -/
|
||||
abbrev UInt8.size : Nat := 256
|
||||
|
||||
|
|
@ -1874,12 +1920,12 @@ The type of unsigned 8-bit integers. This type has special support in the
|
|||
compiler to make it actually 8 bits rather than wrapping a `Nat`.
|
||||
-/
|
||||
structure UInt8 where
|
||||
/-- Unpack a `UInt8` as a `Nat` less than `2^8`.
|
||||
/-- Unpack a `UInt8` as a `BitVec 8`.
|
||||
This function is overridden with a native implementation. -/
|
||||
val : Fin UInt8.size
|
||||
toBitVec : BitVec 8
|
||||
|
||||
attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
|
||||
attribute [extern "lean_uint8_to_nat"] UInt8.val
|
||||
attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
|
||||
|
||||
/--
|
||||
Pack a `Nat` less than `2^8` into a `UInt8`.
|
||||
|
|
@ -1887,7 +1933,7 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_uint8_of_nat"]
|
||||
def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
|
||||
val := { val := n, isLt := h }
|
||||
toBitVec := BitVec.ofNatLt n h
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
|
|
@ -1898,7 +1944,9 @@ This function is overridden with a native implementation.
|
|||
def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
|
||||
dite (Eq n m)
|
||||
(fun h => isTrue (h ▸ rfl))
|
||||
(fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
|
||||
|
||||
instance : DecidableEq UInt8 := UInt8.decEq
|
||||
|
||||
|
|
@ -1913,12 +1961,12 @@ The type of unsigned 16-bit integers. This type has special support in the
|
|||
compiler to make it actually 16 bits rather than wrapping a `Nat`.
|
||||
-/
|
||||
structure UInt16 where
|
||||
/-- Unpack a `UInt16` as a `Nat` less than `2^16`.
|
||||
/-- Unpack a `UInt16` as a `BitVec 16`.
|
||||
This function is overridden with a native implementation. -/
|
||||
val : Fin UInt16.size
|
||||
toBitVec : BitVec 16
|
||||
|
||||
attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
|
||||
attribute [extern "lean_uint16_to_nat"] UInt16.val
|
||||
attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
|
||||
|
||||
/--
|
||||
Pack a `Nat` less than `2^16` into a `UInt16`.
|
||||
|
|
@ -1926,7 +1974,7 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_uint16_of_nat"]
|
||||
def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
|
||||
val := { val := n, isLt := h }
|
||||
toBitVec := BitVec.ofNatLt n h
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
|
|
@ -1937,7 +1985,9 @@ This function is overridden with a native implementation.
|
|||
def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
|
||||
dite (Eq n m)
|
||||
(fun h => isTrue (h ▸ rfl))
|
||||
(fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
|
||||
|
||||
instance : DecidableEq UInt16 := UInt16.decEq
|
||||
|
||||
|
|
@ -1952,12 +2002,12 @@ The type of unsigned 32-bit integers. This type has special support in the
|
|||
compiler to make it actually 32 bits rather than wrapping a `Nat`.
|
||||
-/
|
||||
structure UInt32 where
|
||||
/-- Unpack a `UInt32` as a `Nat` less than `2^32`.
|
||||
/-- Unpack a `UInt32` as a `BitVec 32.
|
||||
This function is overridden with a native implementation. -/
|
||||
val : Fin UInt32.size
|
||||
toBitVec : BitVec 32
|
||||
|
||||
attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
|
||||
attribute [extern "lean_uint32_to_nat"] UInt32.val
|
||||
attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
|
||||
|
||||
/--
|
||||
Pack a `Nat` less than `2^32` into a `UInt32`.
|
||||
|
|
@ -1965,14 +2015,14 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
|
||||
val := { val := n, isLt := h }
|
||||
toBitVec := BitVec.ofNatLt n h
|
||||
|
||||
/--
|
||||
Unpack a `UInt32` as a `Nat`.
|
||||
This function is overridden with a native implementation.
|
||||
-/
|
||||
@[extern "lean_uint32_to_nat"]
|
||||
def UInt32.toNat (n : UInt32) : Nat := n.val.val
|
||||
def UInt32.toNat (n : UInt32) : Nat := n.toBitVec.toNat
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
|
|
@ -1991,30 +2041,26 @@ instance : Inhabited UInt32 where
|
|||
default := UInt32.ofNatCore 0 (by decide)
|
||||
|
||||
instance : LT UInt32 where
|
||||
lt a b := LT.lt a.val b.val
|
||||
lt a b := LT.lt a.toBitVec b.toBitVec
|
||||
|
||||
instance : LE UInt32 where
|
||||
le a b := LE.le a.val b.val
|
||||
le a b := LE.le a.toBitVec b.toBitVec
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
Decides less-equal on `UInt32`.
|
||||
This function is overridden with a native implementation.
|
||||
-/
|
||||
@[extern "lean_uint32_dec_lt"]
|
||||
def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LT.lt n m))
|
||||
inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
Decides less-than on `UInt32`.
|
||||
This function is overridden with a native implementation.
|
||||
-/
|
||||
@[extern "lean_uint32_dec_le"]
|
||||
def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LE.le n m))
|
||||
inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
|
||||
|
||||
instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
|
||||
instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
|
||||
|
|
@ -2028,12 +2074,12 @@ The type of unsigned 64-bit integers. This type has special support in the
|
|||
compiler to make it actually 64 bits rather than wrapping a `Nat`.
|
||||
-/
|
||||
structure UInt64 where
|
||||
/-- Unpack a `UInt64` as a `Nat` less than `2^64`.
|
||||
/-- Unpack a `UInt64` as a `BitVec 64`.
|
||||
This function is overridden with a native implementation. -/
|
||||
val : Fin UInt64.size
|
||||
toBitVec: BitVec 64
|
||||
|
||||
attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
|
||||
attribute [extern "lean_uint64_to_nat"] UInt64.val
|
||||
attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
|
||||
|
||||
/--
|
||||
Pack a `Nat` less than `2^64` into a `UInt64`.
|
||||
|
|
@ -2041,7 +2087,7 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_uint64_of_nat"]
|
||||
def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
|
||||
val := { val := n, isLt := h }
|
||||
toBitVec := BitVec.ofNatLt n h
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
|
|
@ -2052,36 +2098,20 @@ This function is overridden with a native implementation.
|
|||
def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
|
||||
dite (Eq n m)
|
||||
(fun h => isTrue (h ▸ rfl))
|
||||
(fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
|
||||
|
||||
instance : DecidableEq UInt64 := UInt64.decEq
|
||||
|
||||
instance : Inhabited UInt64 where
|
||||
default := UInt64.ofNatCore 0 (by decide)
|
||||
|
||||
/--
|
||||
The size of type `USize`, that is, `2^System.Platform.numBits`, which may
|
||||
be either `2^32` or `2^64` depending on the platform's architecture.
|
||||
|
||||
Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
|
||||
Lean unifier can solve constraints such as `?m + 1 = USize.size`. Recall that
|
||||
`numBits` does not reduce to a numeral in the Lean kernel since it is platform
|
||||
specific. Without this trick, the following definition would be rejected by the
|
||||
Lean type checker.
|
||||
```
|
||||
def one: Fin USize.size := 1
|
||||
```
|
||||
Because Lean would fail to synthesize instance `OfNat (Fin USize.size) 1`.
|
||||
Recall that the `OfNat` instance for `Fin` is
|
||||
```
|
||||
instance : OfNat (Fin (n+1)) i where
|
||||
ofNat := Fin.ofNat i
|
||||
```
|
||||
-/
|
||||
abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
|
||||
/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
|
||||
abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
|
||||
|
||||
theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
|
||||
show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from
|
||||
show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
|
||||
match System.Platform.numBits, System.Platform.numBits_eq with
|
||||
| _, Or.inl rfl => Or.inl (by decide)
|
||||
| _, Or.inr rfl => Or.inr (by decide)
|
||||
|
|
@ -2094,21 +2124,20 @@ For example, if running on a 32-bit machine, USize is equivalent to UInt32.
|
|||
Or on a 64-bit machine, UInt64.
|
||||
-/
|
||||
structure USize where
|
||||
/-- Unpack a `USize` as a `Nat` less than `USize.size`.
|
||||
/-- Unpack a `USize` as a `BitVec System.Platform.numBits`.
|
||||
This function is overridden with a native implementation. -/
|
||||
val : Fin USize.size
|
||||
toBitVec : BitVec System.Platform.numBits
|
||||
|
||||
attribute [extern "lean_usize_of_nat_mk"] USize.mk
|
||||
attribute [extern "lean_usize_to_nat"] USize.val
|
||||
attribute [extern "lean_usize_to_nat"] USize.toBitVec
|
||||
|
||||
/--
|
||||
Pack a `Nat` less than `USize.size` into a `USize`.
|
||||
This function is overridden with a native implementation.
|
||||
-/
|
||||
@[extern "lean_usize_of_nat"]
|
||||
def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
|
||||
val := { val := n, isLt := h }
|
||||
}
|
||||
def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize where
|
||||
toBitVec := BitVec.ofNatLt n h
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
/--
|
||||
|
|
@ -2119,7 +2148,9 @@ This function is overridden with a native implementation.
|
|||
def USize.decEq (a b : USize) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
dite (Eq n m) (fun h =>isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
|
||||
dite (Eq n m)
|
||||
(fun h => isTrue (h ▸ rfl))
|
||||
(fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
|
||||
|
||||
instance : DecidableEq USize := USize.decEq
|
||||
|
||||
|
|
@ -2135,12 +2166,12 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_usize_of_nat"]
|
||||
def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
|
||||
val := {
|
||||
val := n
|
||||
isLt := match USize.size, usize_size_eq with
|
||||
toBitVec :=
|
||||
BitVec.ofNatLt n (
|
||||
match System.Platform.numBits, System.Platform.numBits_eq with
|
||||
| _, Or.inl rfl => h
|
||||
| _, Or.inr rfl => Nat.lt_trans h (by decide)
|
||||
}
|
||||
)
|
||||
|
||||
/--
|
||||
A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
|
||||
|
|
@ -2175,7 +2206,7 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
|
||||
{ val := ⟨{ val := n, isLt := isValidChar_UInt32 h }⟩, valid := h }
|
||||
{ val := ⟨BitVec.ofNatLt n (isValidChar_UInt32 h)⟩, valid := h }
|
||||
|
||||
/--
|
||||
Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scalar value,
|
||||
|
|
@ -2185,7 +2216,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
|
|||
def Char.ofNat (n : Nat) : Char :=
|
||||
dite (n.isValidChar)
|
||||
(fun h => Char.ofNatAux n h)
|
||||
(fun _ => { val := ⟨{ val := 0, isLt := by decide }⟩, valid := Or.inl (by decide) })
|
||||
(fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) })
|
||||
|
||||
theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
|
||||
| ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
|
||||
|
|
@ -3445,15 +3476,13 @@ This function is overridden with a native implementation.
|
|||
-/
|
||||
@[extern "lean_usize_to_uint64"]
|
||||
def USize.toUInt64 (u : USize) : UInt64 where
|
||||
val := {
|
||||
val := u.val.val
|
||||
isLt :=
|
||||
let ⟨n, h⟩ := u
|
||||
show LT.lt n _ from
|
||||
match USize.size, usize_size_eq, h with
|
||||
| _, Or.inl rfl, h => Nat.lt_trans h (by decide)
|
||||
| _, Or.inr rfl, h => h
|
||||
}
|
||||
toBitVec := BitVec.ofNatLt u.toBitVec.toNat (
|
||||
let ⟨⟨n, h⟩⟩ := u
|
||||
show LT.lt n _ from
|
||||
match System.Platform.numBits, System.Platform.numBits_eq, h with
|
||||
| _, Or.inl rfl, h => Nat.lt_trans h (by decide)
|
||||
| _, Or.inr rfl, h => h
|
||||
)
|
||||
|
||||
/-- An opaque hash mixing operation, used to implement hashing for tuples. -/
|
||||
@[extern "lean_uint64_mix_hash"]
|
||||
|
|
|
|||
|
|
@ -67,6 +67,7 @@ deriving instance SizeOf for PLift
|
|||
deriving instance SizeOf for ULift
|
||||
deriving instance SizeOf for Decidable
|
||||
deriving instance SizeOf for Fin
|
||||
deriving instance SizeOf for BitVec
|
||||
deriving instance SizeOf for UInt8
|
||||
deriving instance SizeOf for UInt16
|
||||
deriving instance SizeOf for UInt32
|
||||
|
|
|
|||
|
|
@ -11,22 +11,25 @@ import Init.Data.Nat.Linear
|
|||
@[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
|
||||
cases a; simp_arith
|
||||
|
||||
@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
|
||||
cases a; simp_arith [UInt8.toNat]
|
||||
@[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
|
||||
cases a; simp_arith
|
||||
|
||||
@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
|
||||
cases a; simp_arith [UInt16.toNat]
|
||||
@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
|
||||
cases a; simp_arith [UInt8.toNat, BitVec.toNat]
|
||||
|
||||
@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
|
||||
cases a; simp_arith [UInt32.toNat]
|
||||
@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
|
||||
cases a; simp_arith [UInt16.toNat, BitVec.toNat]
|
||||
|
||||
@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
|
||||
cases a; simp_arith [UInt64.toNat]
|
||||
@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
|
||||
cases a; simp_arith [UInt32.toNat, BitVec.toNat]
|
||||
|
||||
@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
|
||||
cases a; simp_arith [USize.toNat]
|
||||
@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
|
||||
cases a; simp_arith [UInt64.toNat, BitVec.toNat]
|
||||
|
||||
@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
|
||||
@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
|
||||
cases a; simp_arith [USize.toNat, BitVec.toNat]
|
||||
|
||||
@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
|
||||
cases a; simp_arith [Char.toNat]
|
||||
|
||||
@[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ prelude
|
|||
import Init.Data.Array.Basic
|
||||
import Init.NotationExtra
|
||||
import Init.Data.ToString.Macro
|
||||
import Init.Data.UInt.Basic
|
||||
|
||||
universe u v w
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Leonardo de Moura
|
|||
prelude
|
||||
import Init.Data.Array.BasicAux
|
||||
import Init.Data.ToString.Macro
|
||||
import Init.Data.UInt.Basic
|
||||
|
||||
namespace Lean
|
||||
universe u v w w'
|
||||
|
|
|
|||
|
|
@ -59,35 +59,35 @@ instance : ToExpr (BitVec n) where
|
|||
instance : ToExpr UInt8 where
|
||||
toTypeExpr := mkConst ``UInt8
|
||||
toExpr a :=
|
||||
let r := mkRawNatLit a.val
|
||||
let r := mkRawNatLit a.toNat
|
||||
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt8) r
|
||||
(.app (.const ``UInt8.instOfNat []) r)
|
||||
|
||||
instance : ToExpr UInt16 where
|
||||
toTypeExpr := mkConst ``UInt16
|
||||
toExpr a :=
|
||||
let r := mkRawNatLit a.val
|
||||
let r := mkRawNatLit a.toNat
|
||||
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt16) r
|
||||
(.app (.const ``UInt16.instOfNat []) r)
|
||||
|
||||
instance : ToExpr UInt32 where
|
||||
toTypeExpr := mkConst ``UInt32
|
||||
toExpr a :=
|
||||
let r := mkRawNatLit a.val
|
||||
let r := mkRawNatLit a.toNat
|
||||
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt32) r
|
||||
(.app (.const ``UInt32.instOfNat []) r)
|
||||
|
||||
instance : ToExpr UInt64 where
|
||||
toTypeExpr := mkConst ``UInt64
|
||||
toExpr a :=
|
||||
let r := mkRawNatLit a.val
|
||||
let r := mkRawNatLit a.toNat
|
||||
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt64) r
|
||||
(.app (.const ``UInt64.instOfNat []) r)
|
||||
|
||||
instance : ToExpr USize where
|
||||
toTypeExpr := mkConst ``USize
|
||||
toExpr a :=
|
||||
let r := mkRawNatLit a.val
|
||||
let r := mkRawNatLit a.toNat
|
||||
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``USize) r
|
||||
(.app (.const ``USize.instOfNat []) r)
|
||||
|
||||
|
|
|
|||
|
|
@ -54,9 +54,9 @@ cf. https://github.com/leanprover/lean4/issues/4157
|
|||
· exact Nat.one_pos
|
||||
· exact Nat.lt_of_le_of_lt h h'
|
||||
· exact h'
|
||||
· rw [USize.le_def, Fin.le_def]
|
||||
· rw [USize.le_def, BitVec.le_def]
|
||||
change _ ≤ (_ % _)
|
||||
rw [Nat.mod_eq_of_lt h', USize.ofNat, Fin.val_ofNat', Nat.mod_eq_of_lt]
|
||||
rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
|
||||
· exact h
|
||||
· exact Nat.lt_of_le_of_lt h h'
|
||||
· exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩
|
||||
|
|
|
|||
|
|
@ -81,8 +81,7 @@ attribute [bv_normalize] BitVec.testBit_toNat
|
|||
@[bv_normalize]
|
||||
theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true) := by
|
||||
rw [BitVec.ult]
|
||||
rw [LT.lt]
|
||||
rw [BitVec.instLT]
|
||||
simp only [(· < ·)]
|
||||
simp
|
||||
|
||||
attribute [bv_normalize] BitVec.natCast_eq_ofNat
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ instance : LawfulCmpEq Nat compare where
|
|||
|
||||
instance : LawfulCmpEq UInt64 compare where
|
||||
eq_of_cmp h := eq_of_compareOfLessAndEq h
|
||||
cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
|
||||
cmp_rfl := compareOfLessAndEq_rfl <| UInt64.lt_irrefl _
|
||||
|
||||
instance : LawfulCmpEq String compare where
|
||||
eq_of_cmp := eq_of_compareOfLessAndEq
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
/-- info: { val := { val := ⟨0, ⋯⟩ }, valid := ⋯ } -/
|
||||
/-- info: { val := { toBitVec := { toFin := ⟨0, ⋯⟩ } }, valid := ⋯ } -/
|
||||
#guard_msgs in
|
||||
#reduce Char.ofNat (nat_lit 0)
|
||||
|
||||
/--
|
||||
info: { val := { val := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ },
|
||||
info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } },
|
||||
valid := Or.inl (Nat.le_of_ble_eq_true rfl) }
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
|
|||
|
|
@ -1,10 +1,10 @@
|
|||
10
|
||||
6
|
||||
7
|
||||
12
|
||||
100
|
||||
553
|
||||
308
|
||||
310
|
||||
13
|
||||
101
|
||||
558
|
||||
311
|
||||
313
|
||||
11
|
||||
InfTree.node.sizeOf_spec.{u} {α : Type u} [SizeOf α] (children : Nat → InfTree α) : sizeOf (InfTree.node children) = 1
|
||||
|
|
|
|||
|
|
@ -1,34 +1,34 @@
|
|||
def UInt32.ofNatCore' (n : Nat) (h : n < UInt32.size) : UInt32 := {
|
||||
val := { val := n, isLt := h }
|
||||
toBitVec := ⟨{ val := n, isLt := h }⟩
|
||||
}
|
||||
|
||||
#eval UInt32.ofNatCore' 10 (by decide)
|
||||
|
||||
def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
|
||||
val := { val := n, isLt := h }
|
||||
toBitVec := ⟨{ val := n, isLt := h }⟩
|
||||
}
|
||||
|
||||
#eval UInt64.ofNatCore' 3 (by decide)
|
||||
|
||||
#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt8 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt8 }
|
||||
#eval (3 : UInt8).val
|
||||
#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt16 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt16 }
|
||||
#eval (3 : UInt16).val
|
||||
#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt32 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt32 }
|
||||
#eval (3 : UInt32).val
|
||||
#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt64 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt64 }
|
||||
#eval (3 : UInt64).val
|
||||
#eval toString $ { val := { val := 3, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (match System.Platform.numBits, System.Platform.numBits_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) }⟩ : USize }
|
||||
#eval (3 : USize).val
|
||||
|
||||
|
||||
#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt8 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt8 }
|
||||
#eval (4 : UInt8).val
|
||||
#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt16 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt16 }
|
||||
#eval (4 : UInt16).val
|
||||
#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt32 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt32 }
|
||||
#eval (4 : UInt32).val
|
||||
#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt64 }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt64 }
|
||||
#eval (4 : UInt64).val
|
||||
#eval toString $ { val := { val := 4, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
|
||||
#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (match System.Platform.numBits, System.Platform.numBits_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) }⟩ : USize }
|
||||
#eval (4 : USize).val
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue