Fixes #64186, fixes #45880, fixes #64121, fixes #64125, fixes #64177.
Seven sma…ll, independent bug fixes in rounding, integer arithmetic and digit extraction, found while formalizing Base in Lean. Each is a separate commit with its own test, so they can be reviewed or dropped one at a time.
### 1. `floor` with `sigdigits` returns zero just below a power of ten
```julia
julia> floor(prevfloat(1000.0); sigdigits=1)
0.0 # should be 900.0
julia> trunc(prevfloat(1000.0); sigdigits=1)
0.0 # should be 900.0
julia> floor(prevfloat(100.0); sigdigits=1)
0.0 # should be 90.0
julia> floor(Float16(99.94); sigdigits=1)
Float16(0.0) # should be Float16(90.0)
julia> floor(999.9999f0; sigdigits=1)
0.0f0 # should be 900.0f0
```
`base/floatfuncs.jl:133` estimates the leading decimal position with `log10`, which can round up to an integer and select a rounding step ten times too large. The fix corrects estimates near an integer with an exact comparison to the power of ten, using directed rounding at the input precision for `BigFloat`. This complements #63105, which makes the rounding to that position exact: with both, `floor(prevfloat(0.1); sigdigits=1)` is `0.09` and `round(prevfloat(1000.0); sigdigits=16)` is `999.9999999999999`.
[Bug report](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/floatfuncs-sigdigits-hidigit.yaml), [Lean proof](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/FloatFuncs/Refuted.lean#L44)
### 2. `nextpow` returns wrapped results when the next power does not fit
```julia
julia> nextpow(2, Int8(65))
-128 # should be OverflowError
julia> nextpow(2, typemax(UInt8))
0x00 # should be OverflowError
julia> nextpow(Int8(7), Int8(50))
87 # should be OverflowError
julia> nextpow(Int8(7), Int8(88))
97 # should be OverflowError
```
`base/intfuncs.jl:650` returns the power-of-two fast-path result without checking overflow, and its general path can accept a wrapped integer power that happens to increase. The fix checks the fast-path result against the input and uses `checked_pow` for integer bases in the general path.
[Bug report](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/intarith-powers-nextpow-overflow.yaml), [Lean proof](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/Proofs/base/intfuncs.lean#L1285)
### 3. `checked_pow` treats the largest unsigned integer as `-1`
```julia
julia> Base.Checked.checked_pow(UInt8(255), Int8(-1))
0xff # should be DomainError
julia> Base.Checked.checked_pow(UInt8(255), -2)
0x01 # should be DomainError
```
`base/intfuncs.jl:421` recognizes the `-1` unit with `isone(-x)`, which also succeeds when unsigned negation wraps the largest value to one. The fix excludes unsigned values and complex values with unsigned components from that unit check in the shared `power_by_squaring` implementation.
[Bug report](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/intarith-checked-negative-pow.yaml), [Lean proof](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/Proofs/base/checked.lean#L1459)
### 4. `digits` rejects a valid `typemin` negative base
```julia
julia> digits(5; base=typemin(Int))
ERROR: DomainError with -9223372036854775808: # should be [5]
base must be ≥ 2 or ≤ -2
```
`base/intfuncs.jl:1250` validates the base with `abs(base)`, which wraps for `typemin`, and the negative-base digit loops and unsigned digit-count path also negate that base in its original type. The fix uses the existing overflow-safe `uabs` helper for validation and negative-base division in both `digits!` and `ndigits0znb`.
[Bug report](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/parseprint-digits-typemin-base.yaml), [Lean proof](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/Proofs/base/intfuncs.lean#L1316)
### 5. `digits` wraps negative `BigInt` digits into unsigned values
```julia
julia> digits(UInt8, big(-7))
1-element Vector{UInt8}:
0xf9 # should be InexactError
julia> digits(Integer, big(-7))
1-element Vector{Integer}:
0xf9 # should be -7
```
`base/gmp.jl:787` writes positive digit magnitudes through its fast paths and then negates the stored values, so unsigned digits wrap and abstract integer arrays can retain unsigned elements. The fix sends negative inputs through the generic implementation unless the destination element type is signed.
[Bug report](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/bignums-digits-unsigned-negative.yaml), [Lean proof](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/BigNums/Int.lean#L321)
### 6. `digits!` into a short view throws for a `BigInt` and a power-of-two base
```julia
julia> digits!(view(zeros(Int, 10), 1:3), big(2)^62 + 5; base=128)
ERROR: MethodError: no method matching resize!(::SubArray{Int64, 1, Vector{Int64}, Tuple{UnitRange{Int64}}, true}, ::Int64) # should be [5, 0, 0]
```
`base/gmp.jl:803` accepts unit-stride views in the `mpz_export` fast path, whose destination may need resizing even though views do not support `resize!`. The fix restricts that fast path to `Vector` and lets other destinations use the existing generic digit loop.
[Bug report](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/bignums-digits-view-pow2-base.yaml), [Lean proof](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/BigNums/Int.lean#L334)
### 7. Scoped `setprecision` accepts invalid precision and base values
```julia
julia> setprecision(() -> 7, BigFloat, 0)
7 # should be DomainError
julia> setprecision(() -> 7, BigFloat, 10; base=1)
7 # should be DomainError
```
`base/mpfr.jl:1221` installs the converted precision in a scoped value without the validation performed by the global setter. The fix checks that the base is at least two and the precision is positive before running the callback.
[Bug report](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/bignumscov-scoped-setprecision-validation.yaml), [Lean proof](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/BigNumsCov/Mpfr.lean#L533)
