Model unsigned integers as non-negative

[coord-e]

usize, u32 and u64 now have thrust_models::model::UInt as their model, and a value whose model is UInt is refined with v >= 0. The fact is an assumption where such a value is read and an obligation where one is produced, so unsigned subtraction that may underflow is rejected.

Analyzer

TypeBuilder::build yields a rty::RefinedType. The refinement describes the value as a whole: a refinement nested in a type has no counterpart on the value side, where the analyzer keeps the facts about the parts of a value in the formula of a PlaceType, so nested positions are left unrefined. Enum variant fields are the exception, as they are related against the field's own value, and EnumVariantDef records them as refinement types.

An annotated refinement is conjoined onto what the model already says about the value rather than replacing it. truncate_outer_fn_params asserted that every parameter but the last is unrefined; it now asserts that they carry no predicate variable.

Models

In annotations Int and UInt mix through model::Integer, and an Array of either integer model is indexed by both through model::IndexModel. Seq is indexed and measured by UInt, so Seq::len() returns one; the ghost_const pair used it as a source of an Int and now works over Seq<UInt>.

Tests

unsigned_sub pins the obligation direction (x - y without requires(x >= y) is Unsat) and unsigned_loop the assumption direction (while n > 0 { n -= 1 } ends at 0, which does not hold for i32). The UI suite passes: 346 tests.

Known gap

The refinement only reaches a value's root, so an unsigned value read out of a nested position has no fact to offer, and one flowing into an unsigned position raises an obligation that cannot be discharged:

position	fact available
parameter, return value, local	yes
enum variant field	yes
struct or tuple field	no
pointee of &u32 / &mut u32	no
element of Vec<u32>, Seq's length	no

This costs verification of programs that used to pass: #[thrust::callable] fn get(x: &u32) -> u32 { *x } is now Unsat, as is returning s.n from a struct S { n: u32 }. No test in the suite has such a flow, which is why it is green. Closing the gap needs the unsignedness where a type is rebuilt from a PlaceType, i.e. in rty::Type rather than in a refinement.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RiJqqjcQaJoLMyZ5PJZ1dM

---

Generated by Claude Code