19e06acc65
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.
36 lines
1.4 KiB
Text
36 lines
1.4 KiB
Text
/-
|
||
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import Init.Meta
|
||
import Init.SizeOf
|
||
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 BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
|
||
cases a; simp_arith
|
||
|
||
@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
|
||
cases a; simp_arith [UInt8.toNat, BitVec.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 UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
|
||
cases a; simp_arith [UInt32.toNat, BitVec.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 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
|
||
cases s; simp
|