Boole feature request seeds + bitwise operator lowering

[kondylidou]

Summary

Adds a curated set of one-gap Boole feature-request seeds anchored to two real Verus verification repositories — dalek-lite (Curve25519/Ristretto crypto) and VeruSAGE-Bench Vest (binary parser/serializer combinators) — and implements the first of them: bitwise operators on bvN types.

Real-world motivation

dalek-lite (curve25519-dalek/src/specs/): every spec function uses bv8/bv64 bitwise ops for scalar clamping, fixed-size field arithmetic on FieldElement51 (5 × u64 limbs), NAF scalar reconstruction via Seq::skip(1), and .X/.Y/.Z/.T field access on EdwardsPoint.

VeruSAGE-Bench Vest (SecureSpecCombinator, leb128, repetition): parsers return Option<(int, T)>, postconditions use matches destructuring, by (bit_vector) discharges bitvector identities in LEB128, and RepeatN uses Sequence::drop_first() / skip.

Both repositories share the same core gaps: bitvector operators, sequence slicing, struct field access, Option in spec functions, and trait/interface declarations.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[joscoh]

No blocking comments (once previous comments are resolved), just a few questions/suggestions

[shigoel]

Review Summary

Overall: Well-structured PR. The bitwise operator lowering follows existing patterns cleanly, and the mutual recursion fix is a real improvement with good test coverage. The new seed files for future features are useful documentation.

Lean invariant coverage: The two non-trivial modifications (casesIdx/inlineIfConstr propagation and sibling bvar injection) are tested indirectly by the mutual recursion test (even/odd over MyNat) which exercises both paths via solver and gen_smt_vcs + grind. No formal invariant, but indirect test coverage is adequate.

Performance: Minor O(n²) list appends in foldlM — acceptable for small mutual recursion blocks.

See inline comments for specific items (4 total).