Skip to content

Support Self and generic variables in loop invariants#99

Draft
coord-e wants to merge 2 commits into
mainfrom
claude/loop-invariant-context-self-generics
Draft

Support Self and generic variables in loop invariants#99
coord-e wants to merge 2 commits into
mainfrom
claude/loop-invariant-context-self-generics

Conversation

@coord-e
Copy link
Copy Markdown
Owner

@coord-e coord-e commented May 30, 2026

Summary

Extends thrust_macros::invariant! to invariants over generic- and Self-typed variables, by extending #[thrust_macros::context] to thread the enclosing context into each invariant!.

#[thrust_macros::context]
fn f<T: PartialEq>(v: T) {
    while cond {
        thrust_macros::invariant!(|x: T, v: T| x == v);
        ...
    }
}

Frontend (thrust-macros)

  • #[thrust_macros::context] (which already stamps the enclosing impl/trait header onto methods so method-level requires/ensures recover the outer generics) now also accepts free functions and modules and threads the in-scope generics, where-predicates, and (in methods) Self into every invariant! it encounters.
  • invariant! accepts a threaded [self] [params] [wheres] <closure> input. The generated formula function re-declares the threaded generics (shadowing the enclosing ones) and is instantiated via turbofish; in methods, Self is re-declared the same way as a synthetic type parameter and instantiated with the real Self (legal in expression position).
  • The concrete, non-generic form from Implement loop invariant annotation #95 keeps working without context.
  • The macro crate is reorganized into context, invariant, and spec modules; the root keeps only the proc-macro entry points and a few shared private helpers.

Test plan

  • Pass/fail UI test pairs for the generic and Self cases (loop_invariant_generic, loop_invariant_self).
  • cargo test --test ui (203 passed), cargo clippy --all-targets, cargo fmt --check all clean.

Notes

  • A struct used as an invariant variable must model structurally: its Model::Ty must mirror its fields (e.g. a one-field tuple struct models as a one-tuple). A mismatching model trips an existing subtyping panic unrelated to this PR.

https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt

@coord-e coord-e mentioned this pull request May 30, 2026
2 tasks
@coord-e coord-e force-pushed the claude/reduce-pvar-allocation-XFxwT branch from 6e84fab to c4e64ef Compare May 30, 2026 03:30
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from f8dae72 to 5903aba Compare May 30, 2026 03:31
@coord-e coord-e force-pushed the claude/reduce-pvar-allocation-XFxwT branch from c4e64ef to f6f063e Compare May 30, 2026 03:33
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from 5903aba to 4da71aa Compare May 30, 2026 03:34
@coord-e coord-e force-pushed the claude/reduce-pvar-allocation-XFxwT branch from f6f063e to 61e2146 Compare May 30, 2026 03:37
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from 4da71aa to abd3602 Compare May 30, 2026 03:38
@coord-e coord-e force-pushed the claude/reduce-pvar-allocation-XFxwT branch from 61e2146 to 3d93645 Compare May 30, 2026 03:39
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from abd3602 to 0605e6b Compare May 30, 2026 03:40
@coord-e coord-e force-pushed the claude/reduce-pvar-allocation-XFxwT branch from 3d93645 to faaaa7c Compare May 30, 2026 05:07
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from 0605e6b to 995ff18 Compare May 30, 2026 05:10
@coord-e coord-e force-pushed the claude/reduce-pvar-allocation-XFxwT branch from faaaa7c to ca7f820 Compare May 30, 2026 05:13
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from 995ff18 to 35176d6 Compare May 30, 2026 05:14
Base automatically changed from claude/reduce-pvar-allocation-XFxwT to main May 30, 2026 05:30
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from 35176d6 to b4844c6 Compare May 30, 2026 05:35
claude added 2 commits May 30, 2026 06:16
Pure refactor: move the existing `context` impl into `context.rs`, and the
`predicate`/`requires`/`ensures`/`_requires_ensures` machinery (plus
`FnItemWithSignature`, `ExpandedTokens`, and their helpers) into `spec.rs`.

The crate root now holds only the proc-macro entry points (thin delegations)
and the two helpers shared across modules (`FnOuterItem`,
`fn_params_with_model_ty`). The shared helpers stay private: a private root
item is visible to every descendant module, so no `pub(crate)` is required.

No behavior change.

https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt
Extend `thrust_macros::invariant!` to invariants over generic- and
`Self`-typed variables, by extending `#[thrust_macros::context]` to thread the
surrounding context into each `invariant!` it encounters.

`context` now also accepts free functions and modules (in addition to
`impl`/`trait`) and threads the in-scope generics, where-predicates, and
(in methods) `Self` into every `invariant!`.

`invariant!` accepts a threaded `[self] [params] [wheres] <closure>` input.
The generated formula function re-declares the threaded generics (shadowing
the enclosing ones) and is instantiated via turbofish; in methods, `Self` is
re-declared the same way as a synthetic type parameter and instantiated with
the real `Self` (legal in expression position).

Adds pass/fail UI test pairs for the generic and `Self` cases. Note that a
struct used as an invariant variable must model structurally (its `Model::Ty`
must mirror its fields, e.g. a one-field tuple struct models as a one-tuple);
a mismatching model trips an existing subtyping panic unrelated to this
change.

https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt
@coord-e coord-e force-pushed the claude/loop-invariant-context-self-generics branch from b4844c6 to 4d56d1c Compare May 30, 2026 06:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants