Skip to content

Fold invariant_context into context - #231

Draft
coord-e wants to merge 1 commit into
mainfrom
claude/unify-context-attribute-8ak4yh
Draft

Fold invariant_context into context#231
coord-e wants to merge 1 commit into
mainfrom
claude/unify-context-attribute-8ak4yh

Conversation

@coord-e

@coord-e coord-e commented Aug 16, 2026

Copy link
Copy Markdown
Owner

#[thrust_macros::context] stamped each method of an impl/trait with the enclosing header, while #[thrust_macros::invariant_context] threaded the same header — plus the host signature — into the invariant! calls in a function body. Two attributes for one question: what does the code inside this item see?

They become one. #[thrust_macros::context] now takes a function as well, and an impl/trait hands each of its methods the enclosing header along with the attribute itself, so a method carrying a loop invariant no longer needs one of its own:

#[thrust_macros::context]
impl Counter {
    fn run(&mut self) -> i64 {
        let init = *self;
        while rand() {
            thrust_macros::invariant!(|init: Self, self: &mut Self| init.value <= (*self).value);
            self.value += 1;
        }
        init.value
    }
}

A free function still opts in explicitly, with #[thrust_macros::context] in place of the old name.

Who does what

The impl/trait expansion stays a distributor: it knows which items are methods and what header they sit under, and nothing about what a body holds. It stamps two attributes per method —

#[thrust::_outer_context(impl Counter)]
#[::thrust_macros::context]
fn run(&mut self) -> i64 { .. }

— and each method's body is then threaded by its own expansion of the attribute, the same one a free function gets, which reads the header back from #[thrust::_outer_context(..)]: the path requires/ensures already take. That expansion accepts a free function, an impl method, or a trait method through the existing FnItemWithSignature, so a trait method with no body needs no special case.

Not extending a where clause nothing asked for

Threading a body that names no spec macro now leaves it alone. invariant_context extended the host's where clause with the Model predicates unconditionally, which was fine while it was opt-in per function; with every method of a #[context] item threaded, those bounds would otherwise land on methods that have no formula to justify them.

Changes

context.rs dispatches on the item: a function is threaded, an impl/trait hands its methods the header and this attribute. ContextInjector moves here from invariant_context.rs, which is deleted
spec.rs FnItemWithSignature::sig_mut, to extend the threaded function's where clause
tests/ui 17 files: free functions take #[thrust_macros::context], methods drop the attribute entirely

No behaviour change for the analyzer; the macro expansion each test produces is the same as before.

`#[thrust_macros::context]` stamped each method of an `impl`/`trait` with the
enclosing header, while `#[thrust_macros::invariant_context]` threaded the same
header -- plus the host signature -- into the `invariant!` calls in a function body.
Two attributes for one question: what does the code inside this item see?

They become one. `#[thrust_macros::context]` now takes a function as well, and an
`impl`/`trait` hands each of its methods the enclosing header along with the attribute
itself, so a method carrying a loop invariant no longer needs one of its own:

    #[thrust_macros::context]
    impl Counter {
        fn run(&mut self) -> i64 {
            while rand() {
                thrust_macros::invariant!(|init: Self, self: &mut Self| ..);
            }
        }
    }

The `impl`/`trait` expansion stays a distributor: it knows which items are methods and
what header they sit under, and nothing about what a body holds. Each method's body is
threaded by its own expansion of the attribute, the same one a free function gets,
which reads the header back from `#[thrust::_outer_context(..)]` -- the path
`requires`/`ensures` already take.

Threading a body that names no spec macro leaves it alone, rather than extending its
where clause with `Model` predicates nothing asked for: with every method of a
`#[context]` item threaded, those bounds would otherwise land on methods that have no
formula to justify them.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PJ6XNNsSBdPkAzrWHftvqV
@coord-e
coord-e force-pushed the claude/unify-context-attribute-8ak4yh branch from f0652ce to e1aa185 Compare August 20, 2026 06:33
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