Add a BitVec model type

[coord-e]

Adds thrust_models::model::BitVec<WIDTH, SIGNED>, a model type for SMT-LIB bit-vectors. The integer backend is unchanged: Rust integers are still modeled by Int.

A type can declare BitVec as its Model::Ty and specify its operations with #[thrust::trusted] functions. Examples are a u64-backed bit set (in the spirit of DenseBitSet) and an integer wrapper.

impl thrust_models::Model for BitSet64 {
    type Ty = BitVec<64, false>;
}

#[thrust::trusted]
#[thrust_macros::requires(i < 64)]
#[thrust_macros::ensures(!self == *self | (BitVec::from_int(1) << BitVec::from_int(i)))]
fn insert(&mut self, i: usize) { ... }

Changes

• std.rs: adds model::BitVec<WIDTH, SIGNED>. In annotations, its operations translate to SMT-LIB functions:

  Annotation	SMT-LIB
  +, -, *	bvadd, bvsub, bvmul
  unary -	bvneg
  &, |, ^, !	bvand, bvor, bvxor, bvnot
  <<	bvshl
  >>	bvashr / bvlshr
  <, <=, >, >=	bvslt, ... / bvult, ...
  BitVec::from_int	int_to_bv
  BitVec::to_int	sbv_to_int / ubv_to_int

  Where a row lists two functions, SIGNED selects the first (signed) or the second (unsigned).

• chc:

  • adds Sort::BitVec { width };
  • adds Term::IntToBitVec { width, term };
  • adds the bit-vector functions.

• rty: adds Type::BitVec(BitVecType { width, signed }). Only the type builder reads BitVec's generic arguments; the annotation translator inspects the built type.

Both Z3 5.0.0 and the pinned PCSat accept int_to_bv, ubv_to_int and sbv_to_int.

Tests

Each test has a pass/fail pair:

• bit_vec_set: a u64-backed bit set.
• bit_vec_wrapping: an i32 wrapper, checking that i32::MAX + 1 compares below i32::MAX.

cargo test passes in full (390 UI tests), and cargo clippy -- -D warnings and cargo fmt --check are clean.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AeM1mapvfoQGY5U2G2YLVP

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-03T02:13:21.267209Z	97bd477	New commits

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.