[codex] Carry nonnegative invariant for unsigned integers

[coord-e]

Summary

• add 0 <= x as an intrinsic refinement for unsigned integer parameters and return values
• aggregate unsigned parameter refinements into the function/basic-block precondition
• preserve intrinsic refinements when installing inferred or explicit basic-block preconditions
• add a regression test for carrying x >= 0 as a u32 loop invariant

Motivation

Thrust models signed and unsigned Rust integers with the same unbounded integer sort. As a result, an unconstrained u32 was not known to be nonnegative, so a loop invariant such as x >= 0 could not be established from the Rust type.

This change keeps the unbounded-integer model while adding the selected unsigned type invariant 0 <= x. It does not model unsigned upper bounds or wrapping arithmetic.

Validation

• cargo fmt --check
• cargo test --lib
• cargo test --test ui loop_invariant_unsigned with the repository solver wrapper
• full UI suite reviewed by the repository owner