Siddharth
Siddharth
In the course of the development, I grabbed facts about right shifting over integers [from `mathlib4`](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Int/Bitwise.lean). The core proof strategy is to perform a case analysis of the msb: -...
These will be used by LeanSAT for bitblasting rotations by constant distances. We first reduce the case when the rotation amount is larger than the width to the case where...
Adapted from [this zulip thread titled 'reverse FFI: building a "fat" static library'](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/reverse.20FFI.3A.20building.20a.20.22fat.22.20static.20library.3F/near/440460506) --- The motivation is to enable more reverse-FFI use-cases. End users should be able to build a...
This proof needs cleanup, and is stacked over the theory developed over at #4179 . The key idea is to notice that `signExtend` behavior is controlled by the `msb`. When...
### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...
FFI generates boxed accessor for a trivial structure containing a UInt64 inside nontrivial structure
Consider the MWE: ```lean -- bug.lean structure Unboxed where val : UInt64 -- trivial structure, expected FFI layout of UInt64 structure God where unboxed : Unboxed unused : Bool /--...
```lean @[simp] theorem shiftLeftRec_zero (x : BitVec w₁) (y : BitVec w₂) : shiftLeftRec x y 0 = x