Replace thrust:: with thrust_macros:: for requires/ensures in UI tests

[coord-e]

#70

[Copilot]

Pull request overview

Updates Thrust UI tests to use the newer thrust_macros-based annotation flow (and corresponding formula syntax), in line with the work to retire the old annotation parser (#70).

Changes:

• Switched UI tests from #[thrust::requires/ensures] to #[thrust_macros::requires/ensures].
• Updated annotation syntax in tests to the newer model conventions (e.g., ^x → !x, <v> → thrust_models::model::Box::new(v)), and added missing thrust_models::Model impls for some ADTs.
• Refactored the injected std.rs model for integer types via an int_model! macro and added additional operator/compare impls to ease mixing primitives with model::Int.

Reviewed changes

Copilot reviewed 52 out of 52 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
thrust-macros/src/lib.rs	Adjusts turbofish generation for expanded helpers (but currently introduces a syntax issue for lifetime-only generics).
std.rs	Introduces int_model! to consolidate integer model impls and adds ops/compare impls with model::Int.
tests/ui/pass/take_max.rs	Uses thrust_macros::requires/ensures for UI pass coverage.
tests/ui/pass/take_max_annot.rs	Updates requires/ensures path and post-state syntax (^ → !).
tests/ui/pass/split.rs	Uses thrust_macros::requires/ensures for UI pass coverage.
tests/ui/pass/recursive.rs	Uses thrust_macros::requires/ensures for UI pass coverage.
tests/ui/pass/mut_recursive.rs	Uses thrust_macros::requires/ensures for UI pass coverage.
tests/ui/pass/loop.rs	Uses thrust_macros::requires/ensures for UI pass coverage.
tests/ui/pass/just_rec.rs	Uses thrust_macros::requires/ensures for UI pass coverage (multiple functions).
tests/ui/pass/fn_ptr.rs	Uses thrust_macros::requires/ensures for UI pass coverage.
tests/ui/pass/fn_poly_annot.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI coverage.
tests/ui/pass/fn_poly_annot_stronger.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI coverage.
tests/ui/pass/fn_poly_annot_ref.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI coverage.
tests/ui/pass/fn_poly_annot_recursive.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI coverage.
tests/ui/pass/fn_poly_annot_nested.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI coverage.
tests/ui/pass/fn_poly_annot_multi_inst.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI coverage.
tests/ui/pass/fn_poly_annot_complex.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI coverage.
tests/ui/pass/extern_spec_take.rs	Switches to thrust_macros and updates post-state syntax in ensures.
tests/ui/pass/enum_ref_drop.rs	Uses thrust_macros::requires/ensures for UI pass coverage.
tests/ui/pass/annot.rs	Uses thrust_macros::requires/ensures for basic annotation UI coverage.
tests/ui/pass/annot_raw_command.rs	Uses thrust_macros::requires/ensures in raw SMT command scenario.
tests/ui/pass/annot_raw_command_multi.rs	Uses thrust_macros::requires/ensures in multi-command raw SMT scenario.
tests/ui/pass/annot_box_term.rs	Updates box-term syntax to thrust_models::model::Box::new(...).
tests/ui/pass/adt.rs	Adds Model impl for enum and switches to thrust_macros::requires/ensures.
tests/ui/pass/adt_poly_fn_poly.rs	Adds Model impl for generic enum and switches to thrust_macros::requires/ensures.
tests/ui/pass/adt_poly_fn_mono.rs	Adds Model impl for generic enum and switches to thrust_macros::requires/ensures.
tests/ui/pass/adt_mut.rs	Switches to thrust_macros::requires/ensures.
tests/ui/pass/annot_preds_raw_command.rs	Removes UI test that used thrust::raw_command + predicate-style ensures.
tests/ui/pass/annot_preds_raw_command_multi.rs	Removes UI test that used multiple thrust::raw_command + predicate-style ensures.
tests/ui/fail/take_max.rs	Uses thrust_macros::requires/ensures for UI fail coverage.
tests/ui/fail/take_max_annot.rs	Updates requires/ensures path and post-state syntax (^ → !).
tests/ui/fail/split.rs	Uses thrust_macros::requires/ensures for UI fail coverage.
tests/ui/fail/recursive.rs	Uses thrust_macros::requires/ensures for UI fail coverage.
tests/ui/fail/mut_recursive.rs	Uses thrust_macros::requires/ensures for UI fail coverage.
tests/ui/fail/loop.rs	Uses thrust_macros::requires/ensures for UI fail coverage.
tests/ui/fail/just_rec.rs	Uses thrust_macros::requires/ensures for UI fail coverage (multiple functions).
tests/ui/fail/fn_ptr.rs	Uses thrust_macros::requires/ensures for UI fail coverage.
tests/ui/fail/fn_poly_annot.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI fail coverage.
tests/ui/fail/fn_poly_annot_stronger.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI fail coverage.
tests/ui/fail/fn_poly_annot_ref.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI fail coverage.
tests/ui/fail/fn_poly_annot_recursive.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI fail coverage.
tests/ui/fail/fn_poly_annot_nested.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI fail coverage.
tests/ui/fail/fn_poly_annot_multi_inst.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI fail coverage.
tests/ui/fail/fn_poly_annot_complex.rs	Uses thrust_macros::requires/ensures for polymorphic annotation UI fail coverage.
tests/ui/fail/extern_spec_take.rs	Switches to thrust_macros and updates post-state syntax in ensures.
tests/ui/fail/enum_ref_drop.rs	Uses thrust_macros::requires/ensures for UI fail coverage.
tests/ui/fail/annot.rs	Uses thrust_macros::requires/ensures for basic annotation UI fail coverage.
tests/ui/fail/annot_box_term.rs	Updates box-term syntax to thrust_models::model::Box::new(...).
tests/ui/fail/adt.rs	Adds Model impl for enum and switches to thrust_macros::requires/ensures.
tests/ui/fail/adt_poly_fn_poly.rs	Adds Model impl for generic enum and switches to thrust_macros::requires/ensures.
tests/ui/fail/adt_poly_fn_mono.rs	Adds Model impl for generic enum and switches to thrust_macros::requires/ensures.
tests/ui/fail/adt_mut.rs	Switches to thrust_macros::requires/ensures.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.