Strata/Core has no way to cast between bitvectors and integers. We're porting the Verus proofs in dalek-lite to Boole, and even the most basic spec function — u8_32_as_nat, interpreting 32 bytes as a 256-bit little-endian integer — needs a Bv8 → Int cast to even be expressible. Without it, essentially every Curve25519 lemma is blocked. PR #1191 attempts to add support for the operators in Boole and Core's internals (not part of Core's grammar).
Proposal: Add three operators to Core: Bv{n}.ToUInt : Bv{n} → Int (≙ SMT-LIB ubv_to_int, ≙ Lean BitVec.toNat), Bv{n}.ToInt : Bv{n} → Int (≙ sbv_to_int, ≙ BitVec.toInt, two's-complement), and Int.ToBv{n} : Int → Bv{n} (≙ (_ int_to_bv n), ≙ BitVec.ofInt n). Only ToUInt is strictly required for the dalek-lite port; the other two come almost for free on the same plumbing PR #1191 already built, and they make round-trip lemmas much cleaner.
Soundness: All three are total — no preconditions, no Safe variants, no axioms. BitVec.toNat/toInt/ofInt n are total in Lean and the corresponding SMT-LIB 2.7 operators are total in the standard, and they agree pointwise (int_to_bv wraps mod $$2^n$$ on negative inputs, matching BitVec.ofInt).
Strata/Core has no way to cast between bitvectors and integers. We're porting the Verus proofs in dalek-lite to Boole, and even the most basic spec function —
u8_32_as_nat, interpreting 32 bytes as a 256-bit little-endian integer — needs aBv8 → Intcast to even be expressible. Without it, essentially every Curve25519 lemma is blocked. PR #1191 attempts to add support for the operators in Boole and Core's internals (not part of Core's grammar).Proposal: Add three operators to Core:
Bv{n}.ToUInt : Bv{n} → Int(≙ SMT-LIBubv_to_int, ≙ LeanBitVec.toNat),Bv{n}.ToInt : Bv{n} → Int(≙sbv_to_int, ≙BitVec.toInt, two's-complement), andInt.ToBv{n} : Int → Bv{n}(≙(_ int_to_bv n), ≙BitVec.ofInt n). OnlyToUIntis strictly required for the dalek-lite port; the other two come almost for free on the same plumbing PR #1191 already built, and they make round-trip lemmas much cleaner.Soundness: All three are total — no preconditions, no$$2^n$$ on negative inputs, matching
Safevariants, no axioms.BitVec.toNat/toInt/ofInt nare total in Lean and the corresponding SMT-LIB 2.7 operators are total in the standard, and they agree pointwise (int_to_bvwraps modBitVec.ofInt).