Support logical implication (`==>`) in annotations by coord-e · Pull Request #115 · coord-e/thrust

coord-e · 2026-06-09T08:24:02Z

Closes #106.

What

Adds a logical implication operator a ==> b to the annotation formula
language (requires, ensures, the param/ret/sig refinement types, and
invariant!). It is right-associative with the lowest precedence, so
a ==> b ==> c ≡ a ==> (b ==> c) and a || b ==> c ≡ (a || b) ==> c.

Implication is represented explicitly as a first-class chc::Formula::Implies
and emitted to the solver as SMT-LIB (=> lhs rhs), rather than being desugared
away to !lhs || rhs.

(Predicate bodies are out of scope: the plugin consumes them as raw SMT-LIB
string literals, not formula expressions, so they don't go through formula!.)

How

Surface syntax (thrust-macros). Every annotation routes its formula body
through a single preprocessing proc-macro, thrust_macros::formula!:

a contiguous ==> is rewritten to = (assignment — the lowest-precedence,
right-associative Rust operator) so syn reproduces implication's
precedence/associativity for free, including inside closure bodies;
each resulting Expr::Assign is rewritten to a thrust_models::implies(lhs, rhs)
marker call, so the generated #[thrust::formula_fn] body is valid boolean Rust;
a bare = is rejected up front with a clear diagnostic — once desugared it would
be indistinguishable from an implication. (A lone Punct('=') with Alone
spacing not preceded by a joint punct, so ==/!=/<=/>=/==> are
unaffected.)

The invariant |args| ... form is wrapped at the token level, isolating the
closure body (and preserving an explicit -> Ty { .. } return type) since its
input is parsed by syn early.

Explicit representation (plugin).

thrust_models::implies is a #[thrust::def::implies] marker (std.rs);
the analyzer recognizes it (did_cache, analyze/annot.rs) and lowers it to a
new chc::Formula::Implies(lhs, rhs) variant (analyze/annot_fn.rs);
Formula::Implies is threaded through chc.rs (constructor, pretty-print as
==>, is_top/is_bottom, simplify, subst_var/map_var/fv/iter_atoms)
and emitted as (=> ..) in chc/smtlib2.rs. Clause guards now build
guard.implies(formula) directly.

Also enables syn's extra-traits feature explicitly so thrust-macros builds and
unit-tests standalone (it compares/derives over syn AST types).

Tests

tests/ui/{pass,fail}/annot_implication.rs cover basic implication, right-
associativity of an unparenthesized chain, precedence against &&/||/==, and
implication nested inside a quantifier's closure. thrust-macros unit tests cover
the ==> lowering, comparison passthrough, bare-= rejection, and that both
closure forms (bare and -> Ty { .. }) stay parseable after wrapping.

Add a single formula-token preprocessing layer, the `thrust_macros::formula!` proc-macro, that every annotation wraps its formula body in. Its first pass desugars the implication operator `a ==> b` into `!a || b`: - `==>` is rewritten to assignment (the lowest-precedence, right-associative Rust operator) so `syn` reproduces implication's precedence/associativity for free, including inside closure bodies; - each resulting assignment node is rewritten to `(!(lhs)) || (rhs)` so the generated `#[thrust::formula_fn]` body is valid boolean Rust. `requires`/`ensures`, `predicate`, the `param`/`ret`/`sig` refinement types, and `invariant!` all route their formula through `formula!`. Closes #106. Reject bare `=` in formula! to avoid ambiguity with implication `==>` is desugared to assignment, so once parsed an `Expr::Assign` from a genuinely-written `=` is indistinguishable from an implication. Reject a bare `=` (a lone `Punct('=')` with Alone spacing, not preceded by a joint punct, so `==`/`!=`/`<=`/`>=`/`==>` are unaffected) up front with a clear diagnostic. Also enable syn's `extra-traits` feature explicitly (the crate compares `syn::Path` values), so the crate builds and its unit tests run standalone. https://claude.ai/code/session_017DdTwmnyZefiWR7zfcKsEL Document why formula wrapping isolates the body/tail expression https://claude.ai/code/session_017DdTwmnyZefiWR7zfcKsEL Address review: trim comments, dedupe self-rewrite, test expand() - shorten and de-duplicate doc/inline comments - call crate::formula::wrap_formula directly instead of importing it - rename rewrite_self_in_macro_tokens to rewrite_self_in_tokens and reuse it from rty, dropping rty's duplicate copy - unit-test the public formula::expand, not only reject_bare_assignment https://claude.ai/code/session_017DdTwmnyZefiWR7zfcKsEL cargo fmt https://claude.ai/code/session_017DdTwmnyZefiWR7zfcKsEL style fix

style fix

Copilot

Pull request overview

This PR adds first-class logical implication syntax (a ==> b) to Thrust’s annotation/formula language and preserves the operator’s intended precedence/associativity end-to-end (macro preprocessing → analyzer lowering → CHC representation → SMT-LIB emission).

Changes:

Introduces thrust_macros::formula! preprocessing to accept ==> in annotation contexts and lower it to a marker call (thrust_models::implies(lhs, rhs)).
Adds chc::Formula::Implies as an explicit formula variant and emits it to SMT-LIB as (=> lhs rhs).
Adds UI tests covering implication parsing/precedence/associativity and updates syn features to support standalone macro crate testing.

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
thrust-macros/src/spec.rs	Routes predicate bodies and requires/ensures attributes through formula preprocessing; updates `self` rewriting to handle macro token streams.
thrust-macros/src/rty.rs	Wraps refinement-type formulas in `formula!(...)` and centralizes `self` token rewriting.
thrust-macros/src/lib.rs	Exposes the new `formula!` proc-macro entrypoint.
thrust-macros/src/invariant.rs	Wraps invariant closure bodies in `formula!(...)` before parsing to allow `==>` in closures.
thrust-macros/src/formula.rs	Implements the `formula!` preprocessing pipeline (`==>` lowering + bare `=` rejection) and unit tests.
thrust-macros/Cargo.toml	Enables `syn`’s `extra-traits` feature.
tests/ui/pass/annot_implication.rs	Adds passing UI coverage for implication semantics and parsing properties.
tests/ui/fail/annot_implication.rs	Adds failing UI coverage to ensure implication is enforced (unsat).
std.rs	Introduces `thrust_models::implies` marker function annotated for the analyzer.
src/rty.rs	Threads `Formula::Implies` through type-parameter substitution in formulas.
src/chc/unbox.rs	Handles unboxing for the new `Implies` formula variant.
src/chc/smtlib2.rs	Emits implication as SMT-LIB `(=> lhs rhs)`.
src/chc.rs	Adds `Formula::Implies`, pretty-printing, simplification, FV/atom iteration, and guard construction via `implies`.
src/analyze/did_cache.rs	Caches the `implies` marker DefId.
src/analyze/annot.rs	Adds the attribute path for `thrust::def::implies`.
src/analyze/annot_fn.rs	Lowers `thrust_models::implies(lhs, rhs)` calls into the new formula representation.

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

coord-e · 2026-06-13T07:17:27Z

+fn wrap_closure_body(input: TokenStream2) -> TokenStream2 {
+    let tokens: Vec<TokenTree2> = input.into_iter().collect();
+    let bars: Vec<usize> = tokens
+        .iter()
+        .enumerate()
+        .filter(|(_, tt)| matches!(tt, TokenTree2::Punct(p) if p.as_char() == '|'))
+        .map(|(i, _)| i)
+        .collect();
+    let [_open, close, ..] = bars[..] else {
+        return tokens.into_iter().collect();
+    };
+    let header: TokenStream2 = tokens[..=close].iter().cloned().collect();
+    let body = crate::formula::wrap_formula(tokens[close + 1..].iter().cloned().collect());
+    quote!(#header #body)
+}


Fixed in b63a9ff. wrap_closure_body now detects an explicit return type: for |args| -> Ty { .. } it keeps the -> Ty {/} and wraps only the block's tail expression, so the closure stays a parseable ExprClosure. Added a unit test covering both the bare-expression and -> Ty { .. } forms.

Generated by Claude Code

coord-e · 2026-06-13T07:17:24Z

+            TokenTree::Punct(p) if p.as_char() == '=' => {
+                // Look for `=` `=` `>`. `p` is the first `=`.
+                if let Some(TokenTree::Punct(p2)) = iter.peek() {
+                    if p2.as_char() == '=' {
+                        let mut lookahead = iter.clone();
+                        lookahead.next(); // consume the second `=`
+                        if let Some(TokenTree::Punct(p3)) = lookahead.peek() {
+                            if p3.as_char() == '>' {
+                                // Matched `==>`; consume `=` and `>`, emit `=`.
+                                iter.next(); // second `=`
+                                iter.next(); // `>`
+                                out.extend([TokenTree::Punct(Punct::new('=', Spacing::Alone))]);
+                                continue;
+                            }
+                        }
+                    }
+                }
+                out.extend([TokenTree::Punct(p)]);
+            }


Fixed in b63a9ff. desugar_arrows now only matches a contiguous ==> (first = joint, second = joint, then >), so a spaced-out = = > / == > is left as-is, and the synthesized = carries the original ==> span.

Generated by Claude Code

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3151df90e0

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-06-13T07:03:41Z

+    // The predicate body is a boolean formula; route it through `formula!` so it
+    // may use formula syntax (e.g. `==>`). The body is the function's trailing
+    // brace group, wrapped here at the token level before `syn` parses it.
+    let item = wrap_trailing_block(item.into());


Don't route predicate implication through item bodies

For a predicate written as #[thrust_macros::predicate] fn p(x: i64) -> bool { (x > 0) ==> (x >= 0) }, rustc parses the function body before this attribute macro runs, so the ==> tokens are rejected and wrap_trailing_block is never invoked. Even when the tail is valid Rust, the expanded #[thrust::predicate] body is still consumed by analyze/local_def.rs as a raw-SMT string literal, so this does not actually add formula/implication support to predicate bodies.

Useful? React with 👍 / 👎.

Agreed — define_as_predicate consumes predicate bodies as a raw SMT-LIB string literal, not as formula expressions, so wrapping them in formula! was ineffective and misleading. Removed in b63a9ff (dropped wrap_trailing_block and reverted expand_predicate); predicates are no longer claimed to support ==>.

Generated by Claude Code

chatgpt-codex-connector · 2026-06-13T07:03:41Z

+        return tokens.into_iter().collect();
+    };
+    let header: TokenStream2 = tokens[..=close].iter().cloned().collect();
+    let body = crate::formula::wrap_formula(tokens[close + 1..].iter().cloned().collect());


Preserve explicit invariant return types

When an invariant closure includes an explicit return type, e.g. invariant!(|x: i64| -> bool { x >= 1 }), everything after the second | includes -> bool, so this wraps the tokens into |x: i64| formula!(-> bool { ... }) and syn rejects the closure. The previous direct ExprClosure parse accepted this valid closure form, so existing invariants with explicit return types now fail before verification.

Useful? React with 👍 / 👎.

Fixed in b63a9ff — wrap_closure_body preserves an explicit return type by wrapping only the block's tail expression in |args| -> Ty { .. }, with a unit test for both closure forms.

Generated by Claude Code

- desugar_arrows: only rewrite a contiguous `==>` (joint `=`s) and preserve the span on the synthesized `=`, so a spaced-out `= = >` is left alone - invariant: preserve an explicit closure return type by wrapping only the block's tail expression in `|x| -> Ty { .. }` - predicate: drop the `formula!` wrapping; predicate bodies are consumed as raw SMT-LIB string literals, not formula expressions - add unit tests for the closure-form wrapping https://claude.ai/code/session_017DdTwmnyZefiWR7zfcKsEL

coord-e force-pushed the claude/zealous-lamport-7nSnV branch from 76e6ab3 to 2bffc83 Compare June 13, 2026 06:42

claude and others added 2 commits June 13, 2026 15:45

Represent formula implication explicitly

3151df9

style fix

coord-e force-pushed the claude/zealous-lamport-7nSnV branch from 2bffc83 to 3151df9 Compare June 13, 2026 06:46

coord-e marked this pull request as ready for review June 13, 2026 06:56

coord-e requested a review from Copilot June 13, 2026 06:56

Copilot started reviewing on behalf of coord-e June 13, 2026 06:56 View session

Copilot AI reviewed Jun 13, 2026

View reviewed changes

chatgpt-codex-connector Bot reviewed Jun 13, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support logical implication (`==>`) in annotations#115

Support logical implication (`==>`) in annotations#115
coord-e wants to merge 3 commits into
mainfrom
claude/zealous-lamport-7nSnV

coord-e commented Jun 9, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

coord-e Jun 13, 2026

Uh oh!

coord-e Jun 13, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Jun 13, 2026

Uh oh!

coord-e Jun 13, 2026

Uh oh!

chatgpt-codex-connector Bot Jun 13, 2026

Uh oh!

coord-e Jun 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

coord-e commented Jun 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What

How

Tests

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

coord-e Jun 13, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Jun 13, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Jun 13, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Jun 13, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Jun 13, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Jun 13, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

coord-e commented Jun 9, 2026 •

edited

Loading