verus_syn 0.0.0-2026-09-06-0133

use super::*;
use crate::parse::ParseStream;
use crate::punctuated::Punctuated;
use alloc::boxed::Box;
use alloc::vec;
use alloc::vec::Vec;

/// The parsing context, used to support context-sensitive grammars.
///
/// Currently used to make the `Specification` grammar context-sensitive:
///   - In an `Expr` context, a condition in braces must also be parenthesized, i.e. `({ ... })`.
///   - In an `Item` context, a condition in braces may appear unparenthesized, i.e. `{ ... }`.
#[derive(Debug, Clone, Copy)]
pub enum Context {
    /// In an `Expr` e.g. a closure.
    Expr,
    /// In an `Item` e.g. a `fn` definition.
    Item,
}

ast_enum_of_structs! {
    pub enum Publish {
        Closed(Closed),
        Open(Open),
        OpenRestricted(OpenRestricted),
        Uninterp(Uninterp),
        Default,
    }
}

ast_struct! {
    pub struct Closed {
        pub token: Token![closed],
    }
}

ast_struct! {
    pub struct Open {
        pub token: Token![open],
    }
}

ast_struct! {
    pub struct OpenRestricted {
        pub open_token: Token![open],
        pub paren_token: token::Paren,
        pub in_token: Option<Token![in]>,
        pub path: Box<Path>,
    }
}

ast_struct! {
    pub struct Uninterp {
        pub token: Token![uninterp],
    }
}

ast_enum_of_structs! {
    pub enum Mode {
        Spec(ModeSpec),
        Proof(ModeProof),
        Exec(ModeExec),
        Default,
    }
}

ast_enum_of_structs! {
    pub enum FnMode {
        Spec(ModeSpec),
        SpecChecked(ModeSpecChecked),
        Proof(ModeProof),
        ProofAxiom(ModeProofAxiom),
        Exec(ModeExec),
        Default,
    }
}

ast_enum_of_structs! {
    pub enum DataMode {
        Ghost(ModeGhost),
        Tracked(ModeTracked),
        Exec(ModeExec),
        Default,
    }
}

ast_struct! {
    pub struct ModeSpec {
        pub spec_token: Token![spec],
    }
}

ast_struct! {
    pub struct ModeGhost {
        pub ghost_token: Token![ghost],
    }
}

ast_struct! {
    pub struct ModeProof {
        pub proof_token: Token![proof],
    }
}

ast_struct! {
    pub struct ModeProofAxiom {
        pub axiom_token: Token![axiom],
    }
}

ast_struct! {
    pub struct ModeTracked {
        pub tracked_token: Token![tracked],
    }
}

ast_struct! {
    pub struct ModeExec {
        pub exec_token: Token![exec],
    }
}

ast_struct! {
    pub struct ModeSpecChecked {
        pub spec_token: Token![spec],
        pub paren_token: token::Paren,
        pub checked: Box<Ident>,
    }
}

ast_struct! {
    pub struct Specification {
        pub exprs: Punctuated<Expr, Token![,]>,
    }
}

ast_struct! {
    pub struct Prover {
        pub by_token: Token![by],
        pub paren_token: token::Paren,
        pub id: Ident,
    }
}

ast_struct! {
    pub struct Requires {
        pub token: Token![requires],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct Recommends {
        pub token: Token![recommends],
        pub exprs: Specification,
        pub via: Option<(Token![via], Expr)>,
    }
}

ast_struct! {
    pub struct Ensures {
        pub attrs: Vec<Attribute>,
        pub token: Token![ensures],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct DefaultEnsures {
        pub token: Token![default_ensures],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct Returns {
        pub token: Token![returns],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct InvariantExceptBreak {
        pub token: Token![invariant_except_break],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct Invariant {
        pub token: Token![invariant],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct InvariantEnsures {
        pub token: Token![invariant_ensures],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct Decreases {
        pub token: Token![decreases],
        pub exprs: Specification,
    }
}

ast_struct! {
    pub struct SignatureDecreases {
        pub decreases: Decreases,
        pub when: Option<(Token![when], Expr)>,
        pub via: Option<(Token![via], Expr)>,
    }
}

ast_struct! {
    pub struct SignatureInvariants {
        pub token: Token![opens_invariants],
        pub set: InvariantNameSet,
        pub comma: Option<Token![,]>,
    }
}

ast_struct! {
    pub struct SignatureUnwind {
        pub token: Token![no_unwind],
        pub when: Option<(Token![when], Expr)>,
    }
}

ast_enum_of_structs! {
    pub enum InvariantNameSet {
        Any(InvariantNameSetAny),
        None(InvariantNameSetNone),
        List(InvariantNameSetList),
        ListCompl(InvariantNameSetListCompl),
        Set(InvariantNameSetSet),
    }
}

ast_struct! {
    pub struct InvariantNameSetAny {
        pub token: Token![any],
    }
}

ast_struct! {
    pub struct InvariantNameSetNone {
        pub token: Token![none],
    }
}

ast_struct! {
    pub struct InvariantNameSetList {
        pub bracket_token: token::Bracket,
        pub exprs: Punctuated<Expr, Token![,]>,
    }
}

ast_struct! {
    pub struct InvariantNameSetListCompl {
        pub any_token: Token![any],
        pub op_token: Token![/],
        pub bracket_token: token::Bracket,
        pub exprs: Punctuated<Expr, Token![,]>,
    }
}

ast_struct! {
    pub struct InvariantNameSetSet {
        pub expr: Expr,
    }
}

ast_struct! {
    pub struct WithSpecOnExpr {
        pub with: Token![with],
        pub inputs: Punctuated<Expr, Token![,]>,
        pub outputs: Option<(Token![=>], Pat)>,
        pub follows: Option<(Token![|=], Pat)>,
        pub erased_fields: Punctuated<FieldValue, Token![,]>, // only supported if applied to a struct construction expression
    }
}

ast_struct! {
    pub struct WithSpecOnFn {
        pub with: Token![with],
        pub inputs: Punctuated<FnArg , Token![,]>,
        pub outputs: Option<(Token![->], Punctuated<PatType, Token![,]>)>,
    }
}

ast_struct! {
    pub struct SignatureSpec {
        // When adding Verus fields here, update erase_spec_fields:
        pub prover: Option<Prover>,
        pub atomic_spec: Option<AtomicSpec>,
        pub requires: Option<Requires>,
        pub recommends: Option<Recommends>,
        pub ensures: Option<Ensures>,
        pub default_ensures: Option<DefaultEnsures>,
        pub returns: Option<Returns>,
        pub decreases: Option<SignatureDecreases>,
        pub invariants: Option<SignatureInvariants>,
        pub unwind: Option<SignatureUnwind>,
        pub with: Option<WithSpecOnFn>,
    }
}

impl SignatureSpec {
    pub fn erase_spec_fields(&mut self) {
        self.prover = None;
        self.atomic_spec = None;
        self.requires = None;
        self.recommends = None;
        self.ensures = None;
        self.default_ensures = None;
        self.returns = None;
        self.decreases = None;
        self.invariants = None;
        self.unwind = None;
    }
}

ast_struct! {
    pub struct SignatureSpecAttr {
        pub ret_pat: Option<(Pat, Token![=>])>,
        pub spec: SignatureSpec,
    }
}

ast_struct! {
    pub struct Assert {
        pub attrs: Vec<Attribute>,
        pub assert_token: Token![assert],
        pub paren_token: token::Paren,
        pub expr: Box<Expr>,
        /// by_token is only used if prover and/or body is Some
        pub by_token: Option<Token![by]>,
        pub prover: Option<(token::Paren, Ident)>,
        pub requires: Option<Requires>,
        pub body: Option<Box<Block>>,
    }
}

ast_struct! {
    pub struct AssertForall {
        pub attrs: Vec<Attribute>,
        pub assert_token: Token![assert],
        pub forall_token: Token![forall],
        pub or1_token: Token![|],
        pub inputs: Punctuated<Pat, Token![,]>,
        pub or2_token: Token![|],
        pub expr: Box<Expr>,
        pub implies: Option<(Token![implies], Box<Expr>)>,
        pub by_token: Token![by],
        pub body: Box<Block>,
    }
}

ast_struct! {
    pub struct Assume {
        pub attrs: Vec<Attribute>,
        pub assume_token: Token![assume],
        pub paren_token: token::Paren,
        pub expr: Box<Expr>,
    }
}

ast_struct! {
    pub struct RevealHide {
        pub attrs: Vec<Attribute>,
        pub reveal_token: Option<Token![reveal]>,
        pub reveal_with_fuel_token: Option<Token![reveal_with_fuel]>,
        pub hide_token: Option<Token![hide]>,
        pub paren_token: token::Paren,
        pub path: Box<ExprPath>,
        pub fuel: Option<(Token![,], Box<Expr>)>,
    }
}

ast_struct! {
    pub struct ItemBroadcastGroup {
        pub attrs: Vec<Attribute>,
        pub vis: Visibility,
        pub broadcast_group_tokens: (Token![broadcast], Token![group]),
        pub ident: Ident,
        pub brace_token: token::Brace,
        pub paths: Punctuated<ExprPath, Token![,]>,
    }
}

ast_struct! {
    pub struct BroadcastUse {
        pub attrs: Vec<Attribute>,
        pub broadcast_use_tokens: (Token![broadcast], Token![use]),
        pub brace_token: Option<token::Brace>,
        pub paths: Punctuated<ExprPath, Token![,]>,
        pub semi: Token![;],
        pub warning: bool,
    }
}

ast_struct! {
    pub struct AssumeSpecification {
        pub attrs: Vec<Attribute>,
        pub vis: Visibility,
        pub assume_specification: Token![assume_specification],
        pub generics: Generics,
        pub bracket_token: token::Bracket,
        pub qself: Option<QSelf>,
        pub path: Path,
        pub inputs: Option<(token::Paren, Punctuated<FnArg, Token![,]>)>,
        pub output: ReturnType,
        // REVIEW: consider replacing these with SignatureSpec
        pub requires: Option<Requires>,
        pub ensures: Option<Ensures>,
        pub default_ensures: Option<DefaultEnsures>,
        pub returns: Option<Returns>,
        pub invariants: Option<SignatureInvariants>,
        pub unwind: Option<SignatureUnwind>,
        pub semi: Token![;],
    }
}

ast_struct! {
    pub struct View {
        pub attrs: Vec<Attribute>,
        pub expr: Box<Expr>,
        pub at_token: Token![@],
    }
}

ast_struct! {
    pub struct ClosureArg {
        pub tracked_token: Option<Token![tracked]>,
        pub pat: Pat,
    }
}

ast_struct! {
    pub struct FnProofArg {
        pub tracked_token: Option<Token![tracked]>,
        pub arg: BareFnArg,
    }
}

ast_struct! {
    pub struct FnProofOptions {
        pub bracket_token: token::Bracket,
        pub options: Punctuated<PathSegment, Token![,]>,
    }
}

ast_struct! {
    /// A FnSpec type: `FnSpec(usize) -> bool`.
    /// Parsed similarly to TypeBareFn
    pub struct TypeFnSpec {
        pub fn_spec_token: Option<Token![FnSpec]>, // deprecated TODO remove
        pub spec_fn_token: Option<Token![SpecFn]>,
        pub paren_token: token::Paren,
        pub inputs: Punctuated<BareFnArg, Token![,]>,
        pub output: ReturnType,
    }
}

ast_struct! {
    /// A proof_fn type:
    ///   `proof_fn<'a, F>[ReqEns<R>, Copy, Send, Sync](tracked usize) -> tracked bool`
    /// Parsed similarly to TypeBareFn
    pub struct TypeFnProof {
        pub proof_fn_token: Token![proof_fn],
        pub generics: Option<AngleBracketedGenericArguments>,
        pub options: Option<FnProofOptions>,
        pub paren_token: token::Paren,
        pub inputs: Punctuated<FnProofArg, Token![,]>,
        pub output: ReturnType,
    }
}

ast_struct! {
    pub struct BigAndExpr {
        pub tok: Token![&&&],
        pub expr: Box<Expr>,
    }
}

ast_struct! {
    pub struct BigAnd {
        /// exprs.len() must be >= 1
        pub exprs: Vec<BigAndExpr>,
    }
}

ast_struct! {
    pub struct BigOrExpr {
        pub tok: Token![|||],
        pub expr: Box<Expr>,
    }
}

ast_struct! {
    pub struct BigOr {
        /// exprs.len() must be >= 1
        pub exprs: Vec<BigOrExpr>,
    }
}

ast_struct! {
    pub struct ExprIs {
        pub attrs: Vec<Attribute>,
        pub base: Box<Expr>,
        pub is_token: Token![is],
        pub variant_ident: Box<Ident>,
    }
}

ast_struct! {
    pub struct ExprIsNot {
        pub attrs: Vec<Attribute>,
        pub base: Box<Expr>,
        pub is_not_token: Token![isnt],
        pub variant_ident: Box<Ident>,
    }
}

ast_struct! {
    pub struct ExprHas {
        pub attrs: Vec<Attribute>,
        pub lhs: Box<Expr>,
        pub has_token: Token![has],
        pub rhs: Box<Expr>,
    }
}

ast_struct! {
    pub struct ExprHasNot {
        pub attrs: Vec<Attribute>,
        pub lhs: Box<Expr>,
        pub has_not_token: Token![hasnt],
        pub rhs: Box<Expr>,
    }
}

ast_enum! {
    pub enum MatchesOpToken {
        Implies(Token![==>]),
        AndAnd(Token![&&]),
        BigAnd,
    }
}

ast_struct! {
    pub struct MatchesOpExpr {
        pub op_token: MatchesOpToken,
        pub rhs: Box<Expr>,
    }
}

ast_struct! {
    pub struct GlobalSizeOf {
        pub size_of_token: Token![size_of],
        pub type_: Type,
        pub eq_token: Token![==],
        pub expr_lit: ExprLit,
    }
}

ast_struct! {
    pub struct GlobalLayout {
        pub layout_token: Token![layout],
        pub type_: Type,
        pub is_token: Token![is],
        pub size: (Ident, Token![==], ExprLit),
        pub align: Option<(Token![,], Ident, Token![==], ExprLit)>,
    }
}

ast_enum_of_structs! {
    pub enum GlobalInner {
        SizeOf(GlobalSizeOf),
        Layout(GlobalLayout),
    }
}

ast_struct! {
    pub struct Global {
        pub attrs: Vec<Attribute>,
        pub global_token: Token![global],
        pub inner: GlobalInner,
        pub semi: Token![;],
    }
}

ast_struct! {
    pub struct ExprMatches {
        pub attrs: Vec<Attribute>,
        pub lhs: Box<Expr>,
        pub matches_token: Token![matches],
        pub pat: Pat,
        pub op_expr: Option<MatchesOpExpr>,
    }
}

ast_struct! {
    pub struct ExprGetField {
        pub attrs: Vec<Attribute>,
        pub base: Box<Expr>,
        pub arrow_token: Token![->],
        pub member: Member,
    }
}

ast_struct! {
    pub struct ExprFinal {
        pub attrs: Vec<Attribute>,
        pub final_token: Token![final],
        pub paren_token: token::Paren,
        pub arg: Box<Expr>,
    }
}

ast_struct! {
    pub struct ReturnValue {
        pub token: Token![->],
        pub pat: Pat,
    }
}

ast_enum! {
    pub enum ReturnPat {
        Default,
        Pat(Token![->], token::Paren, Pat, Option<Box<(Token![:], Type)>>),
        Type(Token![->], Box<Type>),
    }
}

ast_struct! {
    pub struct AtomicallyBlock {
        pub label: Option<Label>,
        pub atomically_token: Token![atomically],
        pub loop_token: Option<Token![loop]>,
        pub or1_token: Token![|],
        pub update_fn_binder: Ident,
        pub comma_token: Option<Token![,]>,
        pub or2_token: Token![|],
        pub spec_au_binder: ReturnPat,
        pub invariant_except_breaks: Option<InvariantExceptBreak>,
        pub invariants: Option<Invariant>,
        pub ensures: Option<Ensures>,
        pub body: Box<Block>,
    }
}

ast_struct! {
    pub struct PredTypeClause {
        pub type_token: Token![type],
        pub ident: Ident,
        pub comma_token: Token![,],
    }
}

ast_struct! {
    pub struct PermTupleField {
        pub ident: Ident,
        pub colon_token: Token![:],
        pub ty: Type,
    }
}

ast_struct! {
    #[derive(Default)]
    pub struct PermTuple {
        pub paren_token: token::Paren,
        pub fields: Punctuated<PermTupleField, Token![,]>,
    }
}

ast_struct! {
    #[derive(Default)]
    pub struct PermClause {
        pub old_perms: PermTuple,
        pub arrow_token: Option<Token![->]>,
        pub new_perms: PermTuple,
        pub comma_token: Option<Token![,]>,
    }
}

ast_struct! {
    pub struct OuterMask {
        pub token: Token![outer_mask],
        pub set: InvariantNameSet,
        pub comma_token: Option<Token![,]>,
    }
}

ast_struct! {
    pub struct InnerMask {
        pub token: Token![inner_mask],
        pub set: InvariantNameSet,
        pub comma_token: Option<Token![,]>,
    }
}

ast_struct! {
    pub struct AtomicSpec {
        pub atomically_token: Token![atomically],
        pub paren_token: token::Paren,
        pub atomic_update: Ident,
        pub block_token: token::Brace,
        pub type_clause: Option<PredTypeClause>,
        pub perm_clause: PermClause,
        pub requires: Option<Requires>,
        pub ensures: Option<Ensures>,
        pub outer_mask: Option<OuterMask>,
        pub inner_mask: Option<InnerMask>,
        pub comma_token: Option<Token![,]>,
    }
}

#[cfg(feature = "parsing")]
pub mod parsing {
    use super::*;
    use crate::parse::{Parse, ParseStream, Result};

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Publish {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![closed]) {
                let token = input.parse::<Token![closed]>()?;
                Ok(Publish::Closed(Closed { token }))
            } else if input.peek(Token![open]) {
                let token = input.parse::<Token![open]>()?;
                if let Some((paren_token, in_token, path)) = Visibility::parse_restricted(input)? {
                    Ok(Publish::OpenRestricted(OpenRestricted {
                        open_token: token,
                        paren_token,
                        in_token,
                        path,
                    }))
                } else {
                    Ok(Publish::Open(Open { token }))
                }
            } else if input.peek(Token![uninterp]) {
                let token = input.parse::<Token![uninterp]>()?;
                Ok(Publish::Uninterp(Uninterp { token }))
            } else {
                Ok(Publish::Default)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Mode {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![spec]) {
                let spec_token: Token![spec] = input.parse()?;
                Ok(Mode::Spec(ModeSpec { spec_token }))
            } else if input.peek(Token![proof]) {
                let proof_token: Token![proof] = input.parse()?;
                Ok(Mode::Proof(ModeProof { proof_token }))
            } else if input.peek(Token![exec]) {
                let exec_token: Token![exec] = input.parse()?;
                Ok(Mode::Exec(ModeExec { exec_token }))
            } else {
                Ok(Mode::Default)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for DataMode {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![ghost]) {
                let ghost_token: Token![ghost] = input.parse()?;
                Ok(DataMode::Ghost(ModeGhost { ghost_token }))
            } else if input.peek(Token![tracked]) {
                let tracked_token: Token![tracked] = input.parse()?;
                Ok(DataMode::Tracked(ModeTracked { tracked_token }))
            } else if input.peek(Token![exec]) {
                let exec_token: Token![exec] = input.parse()?;
                Ok(DataMode::Exec(ModeExec { exec_token }))
            } else {
                Ok(DataMode::Default)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for FnMode {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![spec]) {
                let spec_token: Token![spec] = input.parse()?;
                if input.peek(token::Paren) {
                    let content;
                    let paren_token = parenthesized!(content in input);
                    let checked = Box::new(content.parse()?);
                    if !matches!(&*checked, Ident { .. }) || checked.to_string() != "checked" {
                        return Err(content.error("expected `spec(checked)`"));
                    }
                    if !content.is_empty() {
                        return Err(content.error("expected `)`"));
                    }
                    Ok(FnMode::SpecChecked(ModeSpecChecked {
                        spec_token,
                        paren_token,
                        checked,
                    }))
                } else {
                    Ok(FnMode::Spec(ModeSpec { spec_token }))
                }
            } else if input.peek(Token![proof]) {
                let proof_token: Token![proof] = input.parse()?;
                Ok(FnMode::Proof(ModeProof { proof_token }))
            } else if input.peek(Token![axiom]) {
                let axiom_token: Token![axiom] = input.parse()?;
                Ok(FnMode::ProofAxiom(ModeProofAxiom { axiom_token }))
            } else if input.peek(Token![exec]) {
                let exec_token: Token![exec] = input.parse()?;
                Ok(FnMode::Exec(ModeExec { exec_token }))
            } else {
                Ok(FnMode::Default)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Specification {
        /// Parse a `Specification` in the context of an `Expr` e.g. a closure.
        fn parse(input: ParseStream) -> Result<Self> {
            Specification::parse_in(Context::Expr, input)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Specification {
        /// Parse a `Specification` in a given context.
        pub fn parse_in(ctx: Context, input: ParseStream) -> Result<Self> {
            let mut exprs = Punctuated::new();
            while !input.is_empty() && Self::is_next_condition_valid(ctx, input) {
                let inner_attrs = input.call(Attribute::parse_inner)?;
                let mut expr = Expr::parse_without_eager_brace(input)?;
                if !inner_attrs.is_empty() {
                    let mut existing_attrs = expr.replace_attrs(Vec::new());
                    let mut attrs = inner_attrs;
                    attrs.append(&mut existing_attrs);
                    expr.replace_attrs(attrs);
                }
                exprs.push(expr);
                if !input.peek(Token![,]) {
                    break;
                }
                let punct = input.parse()?;
                exprs.push_punct(punct);
            }
            // Detect common syntax errors that lead to premature closure termination.
            if input.peek(token::Brace) {
                match ctx {
                    Context::Expr => {
                        if input.peek2(token::Brace) || Self::peek2_spec_keyword(input) {
                            // Missing parentheses around block.
                            return Err(input.error("This block looks like the closure/loop body, but it is followed immediately by another block or clause. If you meant this block to be part of a clause, try parenthesizing it."));
                        }
                    }
                    Context::Item => {
                        if !exprs.trailing_punct() && input.peek2(Token![,]) {
                            // Missing comma before block.
                            return Err(input.error("This block looks like it might be part of the clause. If you meant it to be part of the clause, put a comma before it."));
                        }
                        if input.peek2(token::Brace) || Self::peek2_spec_keyword(input) {
                            // Missing comma after block.
                            return Err(input.error("This block looks like it might be part of the clause. If you meant it to be part of the clause, put a comma after it."));
                        }
                    }
                }
            }
            Ok(Specification { exprs })
        }

        fn is_next_condition_valid(ctx: Context, input: ParseStream) -> bool {
            let allow_braces = matches!(ctx, Context::Item);
            Self::is_next_condition_bare(input)
                || allow_braces && Self::is_next_condition_in_braces(input)
        }

        fn is_next_condition_in_braces(input: ParseStream) -> bool {
            input.peek(token::Brace) && input.peek2(Token![,])
        }

        fn is_next_condition_bare(input: ParseStream) -> bool {
            !(input.peek(Token![,])
                || input.peek(token::Brace)
                || input.peek(Token![;])
                || Self::peek_spec_keyword(input))
        }

        fn peek_spec_keyword(input: ParseStream) -> bool {
            input.peek(Token![invariant_except_break])
                || input.peek(Token![invariant])
                || input.peek(Token![invariant_ensures])
                || input.peek(Token![ensures])
                || input.peek(Token![default_ensures])
                || input.peek(Token![returns])
                || input.peek(Token![decreases])
                || input.peek(Token![via])
                || input.peek(Token![when])
                || input.peek(Token![no_unwind])
                || input.peek(Token![opens_invariants])
                || input.peek(Token![outer_mask])
                || input.peek(Token![inner_mask])
        }

        fn peek2_spec_keyword(input: ParseStream) -> bool {
            input.peek2(Token![invariant_except_break])
                || input.peek2(Token![invariant])
                || input.peek2(Token![invariant_ensures])
                || input.peek2(Token![ensures])
                || input.peek2(Token![default_ensures])
                || input.peek2(Token![returns])
                || input.peek2(Token![decreases])
                || input.peek2(Token![via])
                || input.peek2(Token![when])
                || input.peek2(Token![no_unwind])
                || input.peek2(Token![opens_invariants])
                || input.peek2(Token![outer_mask])
                || input.peek2(Token![inner_mask])
        }

        /// Remove top-level attributes: `#![trigger ...]`, `#![all_triggers]`, and `#![auto]`.
        ///
        /// Those currently attach to the first clause as inner attributes,
        /// even though semantically they apply to the entire `ensures` group.
        fn remove_top_level_attrs(&mut self) -> Vec<Attribute> {
            let Some(first_clause) = self.exprs.first_mut() else {
                return Vec::new();
            };

            fn is_top_level_trigger_attr(attr: &Attribute) -> bool {
                if !matches!(attr.style, AttrStyle::Inner(_)) {
                    return false;
                }
                if attr.path().segments.len() != 1 {
                    return false;
                }
                match attr.path().segments[0].ident.to_string().as_ref() {
                    "trigger" | "all_triggers" | "auto" => true,
                    _ => false,
                }
            }

            let mut top_level_attrs = Vec::new();
            let mut remaining_attrs = Vec::new();
            for attr in first_clause.replace_attrs(Vec::new()) {
                if is_top_level_trigger_attr(&attr) {
                    top_level_attrs.push(attr);
                } else {
                    remaining_attrs.push(attr);
                }
            }
            first_clause.replace_attrs(remaining_attrs);
            top_level_attrs
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Prover {
        fn parse(input: ParseStream) -> Result<Self> {
            let by_token: Token![by] = input.parse()?;
            let content;
            let paren_token = parenthesized!(content in input);
            let id = content.parse()?;
            Ok(Prover {
                by_token,
                paren_token,
                id,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Requires {
        /// Parse a `requires` clause group in the context of an `Expr` e.g. a closure.
        fn parse(input: ParseStream) -> Result<Self> {
            Requires::parse_in(Context::Expr, input)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<Requires> {
        /// Parse an optional `requires` clause group in the context of an `Expr` e.g. a closure.
        fn parse(input: ParseStream) -> Result<Self> {
            Requires::parse_optional_in(Context::Expr, input)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Requires {
        /// Parse a `requires` clause group in a given context.
        pub fn parse_in(ctx: Context, input: ParseStream) -> Result<Self> {
            Ok(Requires {
                token: input.parse()?,
                exprs: Specification::parse_in(ctx, input)?,
            })
        }

        /// Parse an optional `requires` clause group in a given context.
        pub fn parse_optional_in(ctx: Context, input: ParseStream) -> Result<Option<Self>> {
            if input.peek(Token![requires]) {
                Self::parse_in(ctx, input).map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Recommends {
        fn parse(input: ParseStream) -> Result<Self> {
            let token = input.parse()?;
            let exprs = Specification::parse_in(Context::Item, input)?;
            let via = if input.peek(Token![via]) {
                let via_token: Token![via] = input.parse()?;
                // let expr = input.parse()?;
                let expr = Expr::parse_without_eager_brace(input)?;
                Some((via_token, expr))
            } else {
                None
            };
            Ok(Recommends { token, exprs, via })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Ensures {
        /// Parse an `ensures` clause group in the context of an `Expr` e.g. a closure.
        fn parse(input: ParseStream) -> Result<Self> {
            Ensures::parse_in(Context::Expr, input)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<Ensures> {
        /// Parse an optional `ensures` clause group in the context of an `Expr` e.g. a closure.
        fn parse(input: ParseStream) -> Result<Self> {
            Ensures::parse_optional_in(Context::Expr, input)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Ensures {
        /// Parse an `ensures` clause group in a given context.
        pub fn parse_in(ctx: Context, input: ParseStream) -> Result<Self> {
            let token = input.parse()?;
            let mut exprs = Specification::parse_in(ctx, input)?;
            // Hoist attributes that semantically belong to the entire group.
            let top_level_attrs = exprs.remove_top_level_attrs();
            Ok(Ensures {
                attrs: top_level_attrs,
                token,
                exprs,
            })
        }

        /// Parse an optional `ensures` clause group in a given context.
        pub fn parse_optional_in(ctx: Context, input: ParseStream) -> Result<Option<Self>> {
            if input.peek(Token![ensures]) {
                Self::parse_in(ctx, input).map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for DefaultEnsures {
        /// Parse a `default_ensures` clause group in the context of an `Item` e.g. `fn` definition.
        fn parse(input: ParseStream) -> Result<Self> {
            let token = input.parse()?;
            Ok(DefaultEnsures {
                token,
                exprs: Specification::parse_in(Context::Item, input)?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Returns {
        fn parse(input: ParseStream) -> Result<Self> {
            let token = input.parse()?;
            Ok(Returns {
                token,
                exprs: Specification::parse_in(Context::Item, input)?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantExceptBreak {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(InvariantExceptBreak {
                token: input.parse()?,
                exprs: Specification::parse_in(Context::Expr, input)?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Invariant {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(Invariant {
                token: input.parse()?,
                exprs: Specification::parse_in(Context::Expr, input)?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantEnsures {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(InvariantEnsures {
                token: input.parse()?,
                exprs: Specification::parse_in(Context::Expr, input)?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Decreases {
        /// Parse a `decreases` clause group in the context of an `Expr` e.g. a closure.
        fn parse(input: ParseStream) -> Result<Self> {
            Decreases::parse_in(Context::Expr, input)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<Decreases> {
        /// Parse an optional `decreases` clause group in the context of an `Expr` e.g. a closure.
        fn parse(input: ParseStream) -> Result<Self> {
            Decreases::parse_optional_in(Context::Expr, input)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Decreases {
        /// Parse a `decreases` clause group in a given context.
        pub fn parse_in(ctx: Context, input: ParseStream) -> Result<Self> {
            Ok(Decreases {
                token: input.parse()?,
                exprs: Specification::parse_in(ctx, input)?,
            })
        }

        /// Parse an optional `decreases` clause group in a given context.
        pub fn parse_optional_in(ctx: Context, input: ParseStream) -> Result<Option<Self>> {
            if input.peek(Token![decreases]) {
                Self::parse_in(ctx, input).map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for SignatureDecreases {
        fn parse(input: ParseStream) -> Result<Self> {
            let decreases = Decreases::parse_in(Context::Item, input)?;
            let when = if input.peek(Token![when]) {
                let when_token = input.parse()?;
                let expr = Expr::parse_without_eager_brace(input)?;
                Some((when_token, expr))
            } else {
                None
            };
            let via = if input.peek(Token![via]) {
                let via_token = input.parse()?;
                let expr = Expr::parse_without_eager_brace(input)?;
                Some((via_token, expr))
            } else {
                None
            };
            Ok(SignatureDecreases {
                decreases,
                when,
                via,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for SignatureUnwind {
        fn parse(input: ParseStream) -> Result<Self> {
            let token = input.parse()?;
            let when = if input.peek(Token![when]) {
                let when_token = input.parse()?;
                let expr = Expr::parse_without_eager_brace(input)?;
                Some((when_token, expr))
            } else {
                None
            };
            Ok(SignatureUnwind { token, when })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for SignatureInvariants {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(SignatureInvariants {
                token: input.parse()?,
                set: input.parse()?,
                comma: input.parse()?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<SignatureInvariants> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![opens_invariants]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantNameSet {
        fn parse(input: ParseStream) -> Result<Self> {
            let set = if input.peek(Token![any]) {
                if input.peek2(Token![/]) {
                    InvariantNameSet::ListCompl(input.parse()?)
                } else {
                    InvariantNameSet::Any(input.parse()?)
                }
            } else if input.peek(Token![none]) {
                InvariantNameSet::None(input.parse()?)
            } else if input.peek(token::Bracket) {
                InvariantNameSet::List(input.parse()?)
            } else {
                InvariantNameSet::Set(input.parse()?)
            };
            Ok(set)
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantNameSetAny {
        fn parse(input: ParseStream) -> Result<Self> {
            let token_all = input.parse()?;
            Ok(InvariantNameSetAny { token: token_all })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantNameSetNone {
        fn parse(input: ParseStream) -> Result<Self> {
            let token_none = input.parse()?;
            Ok(InvariantNameSetNone { token: token_none })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantNameSetList {
        fn parse(input: ParseStream) -> Result<Self> {
            let content;
            let bracket_token = bracketed!(content in input);
            let exprs = content.parse_terminated(Expr::parse, Token![,])?;
            Ok(InvariantNameSetList {
                bracket_token,
                exprs,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantNameSetListCompl {
        fn parse(input: ParseStream) -> Result<Self> {
            let any_token = input.parse()?;
            let op_token = input.parse()?;
            let content;
            let bracket_token = bracketed!(content in input);
            let exprs = content.parse_terminated(Expr::parse, Token![,])?;
            Ok(InvariantNameSetListCompl {
                any_token,
                op_token,
                bracket_token,
                exprs,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InvariantNameSetSet {
        fn parse(input: ParseStream) -> Result<Self> {
            let expr = Expr::parse_without_eager_brace(input)?;
            Ok(InvariantNameSetSet { expr })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<Prover> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![by]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<Recommends> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![recommends]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<DefaultEnsures> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![default_ensures]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<Returns> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![returns]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<InvariantExceptBreak> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![invariant_except_break]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<Invariant> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![invariant]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<InvariantEnsures> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![invariant_ensures]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<SignatureDecreases> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![decreases]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<SignatureUnwind> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![no_unwind]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for SignatureSpec {
        fn parse(input: ParseStream) -> Result<Self> {
            let prover: Option<Prover> = input.parse()?;
            let with: Option<WithSpecOnFn> = input.parse()?;
            let atomic_spec: Option<AtomicSpec> = input.parse()?;
            let requires: Option<Requires> = Requires::parse_optional_in(Context::Item, input)?;
            let recommends: Option<Recommends> = input.parse()?;
            let ensures: Option<Ensures> = Ensures::parse_optional_in(Context::Item, input)?;
            let default_ensures: Option<DefaultEnsures> = input.parse()?;
            let returns: Option<Returns> = input.parse()?;
            let decreases: Option<SignatureDecreases> = input.parse()?;
            let invariants: Option<SignatureInvariants> = input.parse()?;
            let unwind: Option<SignatureUnwind> = input.parse()?;

            Ok(SignatureSpec {
                prover,
                atomic_spec,
                requires,
                recommends,
                ensures,
                default_ensures,
                returns,
                decreases,
                invariants,
                unwind,
                with,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for SignatureSpecAttr {
        fn parse(input: ParseStream) -> Result<Self> {
            let ret_pat =
                if input.peek2(Token![=>]) || (input.peek2(Token![:]) && input.peek4(Token![=>])) {
                    let mut pat = Pat::parse_single(&input)?;
                    if input.peek(Token![:]) {
                        let colon_token = input.parse()?;
                        let ty = input.parse()?;
                        pat = Pat::Type(PatType {
                            attrs: vec![],
                            pat: Box::new(pat),
                            colon_token,
                            ty,
                        });
                    }
                    let token = input.parse()?;
                    Some((pat, token))
                } else {
                    None
                };
            let spec = input.parse()?;

            Ok(SignatureSpecAttr { ret_pat, spec })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Assume {
        fn parse(input: ParseStream) -> Result<Self> {
            let attrs = Vec::new();
            let assume_token: Token![assume] = input.parse()?;
            let content;
            let paren_token = parenthesized!(content in input);
            let expr = content.parse()?;
            if !content.is_empty() {
                return Err(content.error("expected `)`"));
            }
            Ok(Assume {
                attrs,
                assume_token,
                paren_token,
                expr,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Assert {
        fn parse(input: ParseStream) -> Result<Self> {
            let attrs = Vec::new();
            let assert_token: Token![assert] = input.parse()?;
            let content;
            let paren_token = parenthesized!(content in input);
            let expr = content.parse()?;
            if !content.is_empty() {
                return Err(content.error("expected `)`"));
            }
            if input.peek(Token![by]) {
                let by_token = input.parse()?;
                let prover = if input.peek(token::Paren) {
                    let content;
                    let paren_token = parenthesized!(content in input);
                    let id = content.parse()?;
                    Some((paren_token, id))
                } else {
                    None
                };
                let (requires, body) = if input.peek(Token![requires]) || input.peek(token::Brace) {
                    let requires = Requires::parse_optional_in(Context::Expr, input)?;
                    let block = if input.peek(token::Brace) {
                        Some(Box::new(input.parse()?))
                    } else {
                        None
                    };
                    (requires, block)
                } else {
                    (None, None)
                };
                if prover.is_none() && body.is_none() {
                    return Err(content.error("expected `(` or `{` after `by`"));
                }
                Ok(Assert {
                    attrs,
                    assert_token,
                    paren_token,
                    expr,
                    by_token,
                    prover,
                    requires,
                    body,
                })
            } else {
                let by_token = None;
                let prover = None;
                let requires = None;
                let body = None;
                Ok(Assert {
                    attrs,
                    assert_token,
                    paren_token,
                    expr,
                    by_token,
                    prover,
                    requires,
                    body,
                })
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for AssertForall {
        fn parse(input: ParseStream) -> Result<Self> {
            let mut attrs = Vec::new();
            let assert_token: Token![assert] = input.parse()?;
            let forall_token: Token![forall] = input.parse()?;
            let or1_token: Token![|] = input.parse()?;
            let mut inputs = Punctuated::new();
            while !input.peek(Token![|]) {
                let mut pat = Pat::parse_single(&input)?;
                if input.peek(Token![:]) {
                    let colon_token = input.parse()?;
                    let ty = input.parse()?;
                    pat = Pat::Type(PatType {
                        attrs: vec![],
                        pat: Box::new(pat),
                        colon_token,
                        ty,
                    });
                }
                inputs.push_value(pat);
                if input.peek(Token![|]) {
                    break;
                }
                let comma: Token![,] = input.parse()?;
                inputs.push_punct(comma);
            }
            let or2_token: Token![|] = input.parse()?;
            attr::parsing::parse_inner(input, &mut attrs)?;
            let expr = input.parse()?;
            let implies = if input.peek(Token![implies]) {
                let implies_token = input.parse()?;
                let expr2 = input.parse()?;
                Some((implies_token, expr2))
            } else {
                None
            };
            let by_token = input.parse()?;
            let body = input.parse()?;
            Ok(AssertForall {
                attrs,
                assert_token,
                forall_token,
                or1_token,
                inputs,
                or2_token,
                expr,
                implies,
                by_token,
                body,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for RevealHide {
        fn parse(input: ParseStream) -> Result<Self> {
            let attrs = Vec::new();
            let lookahead = input.lookahead1();
            let mut reveal_token = None;
            let mut reveal_with_fuel_token = None;
            let mut hide_token = None;
            if lookahead.peek(Token![reveal]) {
                reveal_token = input.parse()?;
            } else if lookahead.peek(Token![reveal_with_fuel]) {
                reveal_with_fuel_token = input.parse()?;
            } else if lookahead.peek(Token![hide]) {
                hide_token = input.parse()?;
            } else {
                return Err(lookahead.error());
            }

            let content;
            let paren_token = parenthesized!(content in input);
            let path = content.parse()?;

            // Parse a possible comma (either trailing for hide/reveal,
            // or as a preface to a fuel argument
            let comma: Option<Token![,]> = content.parse()?;

            let fuel = if reveal_with_fuel_token.is_some() && comma.is_some() {
                let f = Some((comma.unwrap(), content.parse()?));
                let _trailing_comma: Option<Token![,]> = content.parse()?;
                f
            } else {
                None
            };

            Ok(RevealHide {
                attrs,
                reveal_token,
                reveal_with_fuel_token,
                hide_token,
                paren_token,
                path,
                fuel,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for BroadcastUse {
        fn parse(input: ParseStream) -> Result<Self> {
            let mut warning = false;
            let attrs = Vec::new();
            let broadcast_use_tokens: (Token![broadcast], Token![use]) =
                (input.parse()?, input.parse()?);
            let (brace_token, paths) = if input.peek(token::Brace) {
                let brace_content;
                let brace = braced!(brace_content in input);
                let paths = brace_content.parse_terminated(ExprPath::parse, Token![,])?;
                (Some(brace), paths)
            } else {
                let path = input.parse()?;
                let mut paths = Punctuated::new();
                paths.push(path);
                loop {
                    if input.peek(Token![;]) {
                        break;
                    }
                    warning = true;
                    if input.peek(Token![,]) {
                        let _: Token![,] = input.parse()?;
                        continue;
                    }
                    let path = input.parse()?;
                    paths.push(path);
                }
                (None, paths)
            };

            let semi: Token![;] = input.parse()?;

            Ok(BroadcastUse {
                attrs,
                broadcast_use_tokens,
                brace_token,
                paths,
                semi,
                warning,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for AssumeSpecification {
        fn parse(input: ParseStream) -> Result<Self> {
            let attrs = input.call(Attribute::parse_outer)?;
            let vis = input.parse()?;
            let assume_specification = input.parse()?;

            let mut generics: Generics = input.parse()?;

            let content;
            let bracket_token = bracketed!(content in input);
            let (qself, path) = path::parsing::qpath(&content, true)?;

            let content;
            let inputs = if input.peek(token::Paren) {
                let paren_token = parenthesized!(content in input);
                let (inputs, variadic) = crate::item::parsing::parse_fn_args(&content)?;
                if variadic.is_some() {
                    return Err(content.error("variadic parameters not allowed"));
                }
                Some((paren_token, inputs))
            } else {
                None
            };

            let output: ReturnType = input.parse()?;
            generics.where_clause = input.parse()?;

            let requires: Option<Requires> = Requires::parse_optional_in(Context::Item, input)?;
            let ensures: Option<Ensures> = Ensures::parse_optional_in(Context::Item, input)?;
            let default_ensures: Option<DefaultEnsures> = input.parse()?;
            let returns: Option<Returns> = input.parse()?;
            let invariants: Option<SignatureInvariants> = input.parse()?;
            let unwind: Option<SignatureUnwind> = input.parse()?;

            let semi = input.parse()?;

            Ok(AssumeSpecification {
                attrs,
                vis,
                assume_specification,
                bracket_token,
                generics,
                qself,
                path,
                inputs,
                output,
                requires,
                ensures,
                default_ensures,
                returns,
                invariants,
                unwind,
                semi,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for ItemBroadcastGroup {
        fn parse(input: ParseStream) -> Result<Self> {
            let attrs = Vec::new();
            let vis: Visibility = input.parse()?;
            let broadcast_group_tokens: (Token![broadcast], Token![group]) =
                (input.parse()?, input.parse()?);
            let ident = input.parse()?;
            let content;
            let brace_token = braced!(content in input);
            let paths = content.parse_terminated(ExprPath::parse, Token![,])?;

            Ok(ItemBroadcastGroup {
                attrs,
                vis,
                ident,
                broadcast_group_tokens,
                brace_token,
                paths,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Global {
        fn parse(input: ParseStream) -> Result<Self> {
            let attrs = Vec::new();
            let global_token: Token![global] = input.parse()?;
            let inner: GlobalInner = input.parse()?;
            let semi: Token![;] = input.parse()?;

            Ok(Global {
                attrs,
                global_token,
                inner,
                semi,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for GlobalSizeOf {
        fn parse(input: ParseStream) -> Result<Self> {
            let size_of_token: Token![size_of] = input.parse()?;
            let type_: Type = input.parse()?;
            let eq_token: Token![==] = input.parse()?;
            let expr_lit: ExprLit = input.parse()?;

            Ok(GlobalSizeOf {
                size_of_token,
                type_,
                eq_token,
                expr_lit,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for GlobalLayout {
        fn parse(input: ParseStream) -> Result<Self> {
            let layout_token: Token![layout] = input.parse()?;
            let type_: Type = input.parse()?;
            let is_token: Token![is] = input.parse()?;
            let size_ident: Ident = input.parse()?;
            if size_ident.to_string() != "size" {
                return Err(input.error("expected `size`"));
            }
            let size_eq_token: Token![==] = input.parse()?;
            let size_expr_lit: ExprLit = input.parse()?;
            let size = (size_ident, size_eq_token, size_expr_lit);
            let align = if input.peek(Token![,]) {
                let comma: Token![,] = input.parse()?;
                let align_ident: Ident = input.parse()?;
                if align_ident.to_string() != "align" {
                    return Err(input.error("expected `align`"));
                }
                let align_eq_token: Token![==] = input.parse()?;
                let align_expr_lit: ExprLit = input.parse()?;
                Some((comma, align_ident, align_eq_token, align_expr_lit))
            } else {
                None
            };
            Ok(GlobalLayout {
                layout_token,
                type_,
                is_token,
                size,
                align,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for GlobalInner {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![size_of]) {
                Ok(GlobalInner::SizeOf(input.parse()?))
            } else if input.peek(Token![layout]) {
                Ok(GlobalInner::Layout(input.parse()?))
            } else {
                Err(input.error("expected `size_of` or `layout`"))
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for FnProofOptions {
        fn parse(input: ParseStream) -> Result<Self> {
            let content;
            let bracket_token = bracketed!(content in input);
            let options = content.parse_terminated(PathSegment::parse, Token![,])?;
            Ok(FnProofOptions {
                bracket_token,
                options,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<FnProofOptions> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(token::Bracket) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for ReturnValue {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(Self {
                token: input.parse()?,
                pat: Pat::parse_single(&input)?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<ReturnValue> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![->]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for ReturnPat {
        fn parse(input: ParseStream) -> Result<Self> {
            // TODO: We decide whether this is a pattern or type by checking for
            // parenthesis after the arrow. This logic breaks if the arrow is
            // followed by a tuple type `-> (Ty, ..., Ty)`.

            if !input.peek(Token![->]) {
                return Ok(ReturnPat::Default);
            }

            let arrow: Token![->] = input.parse()?;
            if !input.peek(token::Paren) {
                return Ok(ReturnPat::Type(arrow, input.parse()?));
            }

            let content;
            let paren = parenthesized!(content in input);
            let pat = Pat::parse_single(&content)?;
            let opt_ty = if content.peek(Token![:]) {
                let colon = content.parse()?;
                let ty = content.parse()?;
                Some(Box::new((colon, ty)))
            } else {
                None
            };

            Ok(ReturnPat::Pat(arrow, paren, pat, opt_ty))
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for AtomicallyBlock {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(AtomicallyBlock {
                label: input.parse()?,
                atomically_token: input.parse()?,
                loop_token: input.parse()?,
                or1_token: input.parse()?,
                update_fn_binder: input.parse()?,
                comma_token: input.parse()?,
                or2_token: input.parse()?,
                spec_au_binder: input.parse()?,
                invariant_except_breaks: input.parse()?,
                invariants: input.parse()?,
                ensures: input.parse()?,
                body: input.parse()?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<AtomicallyBlock> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![atomically]) || input.peek(Lifetime) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for PredTypeClause {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(PredTypeClause {
                type_token: input.parse()?,
                ident: input.parse()?,
                comma_token: input.parse()?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<PredTypeClause> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![type]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for PermTupleField {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(PermTupleField {
                ident: input.parse()?,
                colon_token: input.parse()?,
                ty: input.parse()?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for PermTuple {
        fn parse(input: ParseStream) -> Result<Self> {
            let content;
            Ok(PermTuple {
                paren_token: parenthesized!(content in input),
                fields: content.parse_terminated(PermTupleField::parse, Token![,])?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for PermClause {
        fn parse(input: ParseStream) -> Result<Self> {
            if !input.peek(token::Paren) {
                return Ok(Default::default());
            }

            let old_perms = input.parse()?;
            let (arrow_token, new_perms) = if input.peek(Token![->]) {
                let arrow_token = input.parse()?;
                let new_perms = input.parse()?;
                (Some(arrow_token), new_perms)
            } else {
                (None, Default::default())
            };

            let comma_token = input.parse()?;
            Ok(PermClause {
                old_perms,
                arrow_token,
                new_perms,
                comma_token,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for OuterMask {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(OuterMask {
                token: input.parse()?,
                set: input.parse()?,
                comma_token: input.parse()?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<OuterMask> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![outer_mask]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for InnerMask {
        fn parse(input: ParseStream) -> Result<Self> {
            Ok(InnerMask {
                token: input.parse()?,
                set: input.parse()?,
                comma_token: input.parse()?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<InnerMask> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![inner_mask]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for AtomicSpec {
        fn parse(input: ParseStream) -> Result<Self> {
            let parens;
            let curlys;
            Ok(AtomicSpec {
                atomically_token: input.parse()?,
                paren_token: parenthesized!(parens in input),
                atomic_update: parens.parse()?,
                block_token: braced!(curlys in input),
                type_clause: curlys.parse()?,
                perm_clause: curlys.parse()?,
                requires: curlys.parse()?,
                ensures: curlys.parse()?,
                outer_mask: curlys.parse()?,
                inner_mask: curlys.parse()?,
                comma_token: input.parse()?,
            })
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for Option<AtomicSpec> {
        fn parse(input: ParseStream) -> Result<Self> {
            if input.peek(Token![atomically]) {
                input.parse().map(Some)
            } else {
                Ok(None)
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
    impl Parse for ExprFinal {
        fn parse(input: ParseStream) -> Result<Self> {
            let attrs = Vec::new();
            let final_token: Token![final] = input.parse()?;
            let content;
            let paren_token = parenthesized!(content in input);
            let arg: Expr = content.parse()?;
            Ok(ExprFinal {
                attrs,
                final_token,
                paren_token,
                arg: Box::new(arg),
            })
        }
    }
}

#[cfg(feature = "printing")]
mod printing {
    use std::sync::atomic::{AtomicU64, Ordering};

    use crate::{expr::printing::outer_attrs_to_tokens, spanned::Spanned};

    use super::*;
    use proc_macro2::TokenStream;
    use quote::ToTokens;

    impl ToTokens for Closed {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
        }
    }

    impl ToTokens for Open {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
        }
    }

    impl ToTokens for OpenRestricted {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.open_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.in_token.to_tokens(tokens);
                self.path.to_tokens(tokens);
            });
        }
    }

    impl ToTokens for Uninterp {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ModeSpec {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.spec_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ModeGhost {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.ghost_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ModeProof {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.proof_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ModeProofAxiom {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.axiom_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ModeTracked {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.tracked_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ModeExec {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.exec_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ModeSpecChecked {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.spec_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.checked.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Specification {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Prover {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.by_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.id.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Requires {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Recommends {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Ensures {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for DefaultEnsures {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Returns {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InvariantExceptBreak {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Invariant {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InvariantEnsures {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Decreases {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.exprs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for SignatureDecreases {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.decreases.to_tokens(tokens);
            if let Some((when_token, when)) = &self.when {
                when_token.to_tokens(tokens);
                when.to_tokens(tokens);
            }
            if let Some((via_token, via)) = &self.via {
                via_token.to_tokens(tokens);
                via.to_tokens(tokens);
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for SignatureInvariants {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.set.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for SignatureUnwind {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            if let Some((when_token, when)) = &self.when {
                when_token.to_tokens(tokens);
                when.to_tokens(tokens);
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InvariantNameSetAny {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InvariantNameSetNone {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InvariantNameSetList {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.bracket_token.surround(tokens, |tokens| {
                self.exprs.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InvariantNameSetListCompl {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.any_token.to_tokens(tokens);
            self.op_token.to_tokens(tokens);
            self.bracket_token.surround(tokens, |tokens| {
                self.exprs.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InvariantNameSetSet {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.expr.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for SignatureSpec {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.prover.to_tokens(tokens);
            self.atomic_spec.to_tokens(tokens);
            self.requires.to_tokens(tokens);
            self.recommends.to_tokens(tokens);
            self.ensures.to_tokens(tokens);
            self.default_ensures.to_tokens(tokens);
            self.returns.to_tokens(tokens);
            self.decreases.to_tokens(tokens);
            self.invariants.to_tokens(tokens);
            self.unwind.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for SignatureSpecAttr {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            if let Some((ret_pat, token)) = &self.ret_pat {
                ret_pat.to_tokens(tokens);
                token.to_tokens(tokens);
            }
            self.spec.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Assume {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            crate::expr::printing::outer_attrs_to_tokens(&self.attrs, tokens);
            self.assume_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.expr.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Assert {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            crate::expr::printing::outer_attrs_to_tokens(&self.attrs, tokens);
            self.assert_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.expr.to_tokens(tokens);
            });
            if let Some(by_token) = &self.by_token {
                if self.prover.is_some() || self.body.is_some() {
                    by_token.to_tokens(tokens);
                    if let Some((paren, id)) = &self.prover {
                        paren.surround(tokens, |tokens| {
                            id.to_tokens(tokens);
                        });
                    }
                    self.requires.to_tokens(tokens);
                    self.body.to_tokens(tokens);
                }
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for AssertForall {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            crate::expr::printing::outer_attrs_to_tokens(&self.attrs, tokens);
            self.assert_token.to_tokens(tokens);
            self.forall_token.to_tokens(tokens);
            self.or1_token.to_tokens(tokens);
            self.inputs.to_tokens(tokens);
            self.or2_token.to_tokens(tokens);
            self.expr.to_tokens(tokens);
            if let Some((implies, expr)) = &self.implies {
                implies.to_tokens(tokens);
                expr.to_tokens(tokens);
            }
            self.by_token.to_tokens(tokens);
            self.body.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for RevealHide {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            crate::expr::printing::outer_attrs_to_tokens(&self.attrs, tokens);
            if let Some(reveal_token) = &self.reveal_token {
                reveal_token.to_tokens(tokens);
            }
            if let Some(reveal_with_fuel_token) = &self.reveal_with_fuel_token {
                reveal_with_fuel_token.to_tokens(tokens);
            }
            self.paren_token.surround(tokens, |tokens| {
                self.path.to_tokens(tokens);
                if let Some((comma_token, expr)) = &self.fuel {
                    comma_token.to_tokens(tokens);
                    expr.to_tokens(tokens);
                }
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for BroadcastUse {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            crate::expr::printing::outer_attrs_to_tokens(&self.attrs, tokens);
            let BroadcastUse {
                attrs: _,
                broadcast_use_tokens,
                brace_token,
                paths,
                semi,
                warning: _,
            } = self;
            broadcast_use_tokens.0.to_tokens(tokens);
            broadcast_use_tokens.1.to_tokens(tokens);
            if let Some(brace_token) = brace_token {
                brace_token.surround(tokens, |tokens| {
                    paths.to_tokens(tokens);
                });
            } else {
                paths.to_tokens(tokens);
            }
            semi.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ItemBroadcastGroup {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            crate::expr::printing::outer_attrs_to_tokens(&self.attrs, tokens);
            let ItemBroadcastGroup {
                attrs: _,
                vis,
                ident,
                broadcast_group_tokens,
                brace_token,
                paths,
            } = self;
            vis.to_tokens(tokens);
            broadcast_group_tokens.0.to_tokens(tokens);
            broadcast_group_tokens.1.to_tokens(tokens);
            ident.to_tokens(tokens);
            brace_token.surround(tokens, |tokens| {
                paths.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for View {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            crate::expr::printing::outer_attrs_to_tokens(&self.attrs, tokens);
            self.expr.to_tokens(tokens);
            self.at_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ClosureArg {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.tracked_token.to_tokens(tokens);
            self.pat.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for FnProofArg {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.tracked_token.to_tokens(tokens);
            self.arg.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for FnProofOptions {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.bracket_token.surround(tokens, |tokens| {
                self.options.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for TypeFnSpec {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.fn_spec_token.to_tokens(tokens);
            self.spec_fn_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.inputs.to_tokens(tokens);
            });
            self.output.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for TypeFnProof {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.proof_fn_token.to_tokens(tokens);
            self.generics.to_tokens(tokens);
            self.options.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.inputs.to_tokens(tokens);
            });
            self.output.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for BigAnd {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            for expr in &self.exprs {
                expr.tok.to_tokens(tokens);
                expr.expr.to_tokens(tokens);
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for BigOr {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            for expr in &self.exprs {
                expr.tok.to_tokens(tokens);
                expr.expr.to_tokens(tokens);
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ExprIs {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.base.to_tokens(tokens);
            self.is_token.to_tokens(tokens);
            self.variant_ident.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ExprIsNot {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.base.to_tokens(tokens);
            self.is_not_token.to_tokens(tokens);
            self.variant_ident.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ExprHas {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.lhs.to_tokens(tokens);
            self.has_token.to_tokens(tokens);
            self.rhs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ExprHasNot {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.lhs.to_tokens(tokens);
            self.has_not_token.to_tokens(tokens);
            self.rhs.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for GlobalSizeOf {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.size_of_token.to_tokens(tokens);
            self.type_.to_tokens(tokens);
            self.eq_token.to_tokens(tokens);
            self.expr_lit.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for GlobalLayout {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.layout_token.to_tokens(tokens);
            self.type_.to_tokens(tokens);
            self.is_token.to_tokens(tokens);
            self.size.0.to_tokens(tokens);
            self.size.1.to_tokens(tokens);
            self.size.2.to_tokens(tokens);
            if let Some(align) = &self.align {
                align.0.to_tokens(tokens);
                align.1.to_tokens(tokens);
                align.2.to_tokens(tokens);
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for Global {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.global_token.to_tokens(tokens);
            self.inner.to_tokens(tokens);
            self.semi.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ExprMatches {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.lhs.to_tokens(tokens);
            self.matches_token.to_tokens(tokens);
            self.pat.to_tokens(tokens);
            if let Some(MatchesOpExpr { op_token, rhs }) = &self.op_expr {
                match op_token {
                    MatchesOpToken::Implies(t) => t.to_tokens(tokens),
                    MatchesOpToken::AndAnd(t) => t.to_tokens(tokens),
                    MatchesOpToken::BigAnd => (),
                }
                rhs.to_tokens(tokens);
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ExprGetField {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.base.to_tokens(tokens);
            self.arrow_token.to_tokens(tokens);
            self.member.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ExprFinal {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.final_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.arg.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for AssumeSpecification {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            outer_attrs_to_tokens(&self.attrs, tokens);
            self.vis.to_tokens(tokens);
            self.assume_specification.to_tokens(tokens);
            self.generics.to_tokens(tokens);

            self.bracket_token.surround(tokens, |tokens| {
                use crate::path::printing::PathStyle;
                path::printing::print_qpath(tokens, &self.qself, &self.path, PathStyle::Mod)
            });

            if let Some((paren_token, inputs)) = &self.inputs {
                paren_token.surround(tokens, |tokens| {
                    inputs.to_tokens(tokens);
                });
            }

            self.output.to_tokens(tokens);
            self.generics.where_clause.to_tokens(tokens);

            self.requires.to_tokens(tokens);
            self.ensures.to_tokens(tokens);
            self.default_ensures.to_tokens(tokens);
            self.returns.to_tokens(tokens);
            self.invariants.to_tokens(tokens);
            self.unwind.to_tokens(tokens);
            self.semi.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for ReturnPat {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            match self {
                ReturnPat::Default => {}
                ReturnPat::Pat(arrow, paren, pat, type_hint) => {
                    arrow.to_tokens(tokens);
                    paren.surround(tokens, |tokens| {
                        pat.to_tokens(tokens);
                        if let Some((colon, ty)) = type_hint.as_deref() {
                            colon.to_tokens(tokens);
                            ty.to_tokens(tokens);
                        }
                    });
                }
                ReturnPat::Type(arrow, ty) => {
                    arrow.to_tokens(tokens);
                    ty.to_tokens(tokens);
                }
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for AtomicallyBlock {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.label.to_tokens(tokens);
            self.atomically_token.to_tokens(tokens);
            self.loop_token.to_tokens(tokens);
            self.or1_token.to_tokens(tokens);
            self.update_fn_binder.to_tokens(tokens);
            self.comma_token.to_tokens(tokens);
            self.or2_token.to_tokens(tokens);
            self.spec_au_binder.to_tokens(tokens);
            self.invariant_except_breaks.to_tokens(tokens);
            self.invariants.to_tokens(tokens);
            self.ensures.to_tokens(tokens);
            self.body.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for PredTypeClause {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.type_token.to_tokens(tokens);
            self.ident.to_tokens(tokens);
            self.comma_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for PermTupleField {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.ident.to_tokens(tokens);
            self.colon_token.to_tokens(tokens);
            self.ty.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for PermTuple {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.paren_token.surround(tokens, |tokens| {
                self.fields.to_tokens(tokens);
            });
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl PermTuple {
        pub fn to_type_tokens(&self, tokens: &mut TokenStream) {
            self.paren_token.surround(tokens, |tokens| {
                for pair in self.fields.pairs() {
                    let (field, comma) = pair.into_tuple();
                    field.ty.to_tokens(tokens);
                    comma.to_tokens(tokens);
                }
            });
        }

        pub fn to_value_tokens(&self, tokens: &mut TokenStream) {
            self.paren_token.surround(tokens, |tokens| {
                for pair in self.fields.pairs() {
                    let (field, comma) = pair.into_tuple();
                    field.ident.to_tokens(tokens);
                    comma.to_tokens(tokens);
                }
            });
        }

        pub fn to_pattern_tokens(&self, tokens: &mut TokenStream) {
            // Since we don't have general support for pattern matching yet,
            // we generate throw-away idents as patterns for empty tuples.
            //
            // The idents are never used, so we don't have to remember them,
            // they just have to be locally unique to prevent name collisions
            // in function argument position.
            if self.fields.is_empty() {
                static COUNTER: AtomicU64 = AtomicU64::new(0);
                let id = COUNTER.fetch_add(1, Ordering::Relaxed);
                let var_name = alloc::format!("_perm_tup{id}");
                let ident = Ident::new(&var_name, self.span());
                ident.to_tokens(tokens);
            } else {
                self.to_value_tokens(tokens);
            }
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for PermClause {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.old_perms.to_tokens(tokens);
            self.arrow_token.to_tokens(tokens);
            self.new_perms.to_tokens(tokens);
            self.comma_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for OuterMask {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.set.to_tokens(tokens);
            self.comma_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for InnerMask {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.token.to_tokens(tokens);
            self.set.to_tokens(tokens);
            self.comma_token.to_tokens(tokens);
        }
    }

    #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
    impl ToTokens for AtomicSpec {
        fn to_tokens(&self, tokens: &mut TokenStream) {
            self.atomically_token.to_tokens(tokens);
            self.paren_token.surround(tokens, |tokens| {
                self.atomic_update.to_tokens(tokens);
            });

            self.block_token.surround(tokens, |tokens| {
                self.type_clause.to_tokens(tokens);
                self.perm_clause.to_tokens(tokens);
                self.requires.to_tokens(tokens);
                self.ensures.to_tokens(tokens);
                self.outer_mask.to_tokens(tokens);
                self.inner_mask.to_tokens(tokens);
            });

            self.comma_token.to_tokens(tokens);
        }
    }
}

pub(crate) fn disallow_prefix_binop(input: crate::parse::ParseStream) -> crate::parse::Result<()> {
    // Be conservative with &&& and ||| so we don't run into any ambiguities.
    // We could try to allow (&&&...) and (|||...), but (...) can also be used for tuples,
    // which might be more than we want.
    if input.peek(Token![&&&]) {
        Err(input.error("leading &&& must be inside a block {...}"))
    } else if input.peek(Token![|||]) {
        Err(input.error("leading ||| must be inside a block {...}"))
    } else {
        Ok(())
    }
}

#[cfg(feature = "full")]
pub(crate) fn parse_matches(
    input: crate::parse::ParseStream,
    lhs: Expr,
    allow_struct: expr::parsing::AllowStruct,
    big_and: bool,
) -> Result<Expr> {
    let matches_token: Token![matches] = input.parse()?;
    let pat = Pat::parse_single(&input)?;

    let op_expr = if input.peek(Token![&&&]) {
        if big_and {
            let attrs = input.call(expr::parsing::expr_attrs)?;
            let Some(rhs) = parse_prefix_binop(input, &attrs, true)? else {
                return Err(input.error("expected &&&"));
            };
            Some(MatchesOpExpr {
                op_token: MatchesOpToken::BigAnd,
                rhs: Box::new(rhs),
            })
        } else {
            return Err(input.error("in &&&, a matches expression needs to be prefixed with &&&"));
        }
    } else if input.peek(Token![==>]) || input.peek(Token![&&]) {
        let op_token = if input.peek(Token![==>]) {
            MatchesOpToken::Implies(input.parse()?)
        } else if input.peek(Token![&&]) {
            MatchesOpToken::AndAnd(input.parse()?)
        } else {
            unreachable!()
        };
        let mut rhs = expr::parsing::unary_expr(input, allow_struct)?;
        loop {
            let next = expr::parsing::peek_precedence(input);
            if matches!(op_token, MatchesOpToken::Implies(_))
                && next >= crate::precedence::Precedence::Imply
                || matches!(op_token, MatchesOpToken::AndAnd(_))
                    && next >= crate::precedence::Precedence::And
            {
                rhs = expr::parsing::parse_expr(input, rhs, allow_struct, next)?;
            } else {
                break;
            }
        }
        Some(MatchesOpExpr {
            op_token,
            rhs: Box::new(rhs),
        })
    } else {
        None
    };

    Ok(Expr::Matches(ExprMatches {
        attrs: Vec::new(),
        lhs: Box::new(lhs),
        matches_token,
        pat,
        op_expr,
    }))
}

#[cfg(feature = "full")]
pub(crate) fn parse_prefix_binop(
    input: crate::parse::ParseStream,
    attrs: &Vec<Attribute>,
    big_and_only: bool,
) -> Result<Option<Expr>> {
    use crate::expr::parsing::AllowStruct;

    if input.peek(Token![&&&]) {
        if attrs.len() != 0 {
            return Err(input.error("`&&&` cannot have attributes"));
        }
        let mut exprs: Vec<BigAndExpr> = Vec::new();
        while let Ok(token) = input.parse() {
            let lhs = expr::parsing::unary_expr(input, AllowStruct(true))?;
            let expr: Expr = if input.peek(Token![matches]) {
                let attrs = input.call(expr::parsing::expr_attrs)?;
                let mut expr = parse_matches(input, lhs, AllowStruct(true), true)?;
                expr.replace_attrs(attrs);
                expr
            } else {
                expr::parsing::parse_expr(
                    input,
                    lhs,
                    AllowStruct(true),
                    crate::precedence::Precedence::Assign,
                )?
            };

            exprs.push(BigAndExpr {
                tok: token,
                expr: Box::new(expr),
            });
        }
        Ok(Some(Expr::BigAnd(BigAnd { exprs })))
    } else if !big_and_only && input.peek(Token![|||]) {
        if attrs.len() != 0 {
            return Err(input.error("`|||` cannot have attributes"));
        }
        let mut exprs: Vec<BigOrExpr> = Vec::new();
        while let Ok(token) = input.parse() {
            let expr: Expr = input.parse()?;
            exprs.push(BigOrExpr {
                tok: token,
                expr: Box::new(expr),
            });
        }
        Ok(Some(Expr::BigOr(BigOr { exprs })))
    } else {
        Ok(None)
    }
}

pub(crate) fn parse_fn_spec(input: ParseStream) -> Result<TypeFnSpec> {
    let args;

    let fn_spec = TypeFnSpec {
        fn_spec_token: input.parse()?,
        spec_fn_token: input.parse()?,
        paren_token: parenthesized!(args in input),
        inputs: {
            let mut inputs = Punctuated::new();

            while !args.is_empty() {
                let attrs = args.call(Attribute::parse_outer)?;

                let arg = crate::ty::parsing::parse_bare_fn_arg(&args, false)?;
                inputs.push_value(BareFnArg { attrs, ..arg });

                if args.is_empty() {
                    break;
                }

                let comma = args.parse()?;
                inputs.push_punct(comma);
            }

            inputs
        },
        output: input.call(ReturnType::without_plus)?,
    };

    Ok(fn_spec)
}

pub(crate) fn parse_fn_proof(input: ParseStream) -> Result<TypeFnProof> {
    let args;
    let proof_fn_token = input.parse()?;
    let generics = if input.peek(Token![<]) {
        Some(input.parse()?)
    } else {
        None
    };
    let fn_proof = TypeFnProof {
        proof_fn_token,
        generics,
        options: input.parse()?,
        paren_token: parenthesized!(args in input),
        inputs: {
            let mut inputs = Punctuated::new();

            while !args.is_empty() {
                let attrs = args.call(Attribute::parse_outer)?;

                let tracked_token = args.parse()?;
                let arg = crate::ty::parsing::parse_bare_fn_arg(&args, false)?;
                inputs.push_value(FnProofArg {
                    tracked_token,
                    arg: BareFnArg { attrs, ..arg },
                });

                if args.is_empty() {
                    break;
                }

                let comma = args.parse()?;
                inputs.push_punct(comma);
            }

            inputs
        },
        output: input.call(ReturnType::without_plus)?,
    };

    Ok(fn_proof)
}

ast_struct! {
    pub struct LoopSpec {
        pub iter_name: Option<(Ident, Token![=>])>,
        pub invariants: Option<Invariant>,
        pub invariant_except_breaks: Option<InvariantExceptBreak>,
        pub ensures: Option<Ensures>,
        pub decreases: Option<Decreases>,
    }
}

impl parse::Parse for LoopSpec {
    fn parse(input: ParseStream) -> Result<Self> {
        let iter_name = if input.peek2(Token![=>]) {
            let pat = input.parse()?;
            let token = input.parse()?;
            Some((pat, token))
        } else {
            None
        };

        let invariants: Option<Invariant> = input.parse()?;
        let invariant_except_breaks: Option<InvariantExceptBreak> = input.parse()?;
        let ensures: Option<Ensures> = Ensures::parse_optional_in(Context::Expr, input)?;
        let decreases = Decreases::parse_optional_in(Context::Expr, input)?;
        Ok(LoopSpec {
            iter_name,
            invariants,
            invariant_except_breaks,
            ensures,
            decreases,
        })
    }
}

#[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
impl parse::Parse for Option<WithSpecOnFn> {
    fn parse(input: ParseStream) -> Result<Self> {
        if input.peek(Token![with]) {
            input.parse().map(Some)
        } else {
            Ok(None)
        }
    }
}

#[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
impl parse::Parse for WithSpecOnFn {
    fn parse(input: ParseStream) -> Result<Self> {
        let with = input.parse()?;
        let mut inputs = Punctuated::new();

        // Helper function to check if we're at next spec keyword
        let is_next_spec_keyword = |input: ParseStream| -> bool {
            input.peek(Token![atomically])
                || input.peek(Token![requires])
                || input.peek(Token![invariant_except_break])
                || input.peek(Token![invariant])
                || input.peek(Token![invariant_ensures])
                || input.peek(Token![ensures])
                || input.peek(Token![default_ensures])
                || input.peek(Token![returns])
                || input.peek(Token![decreases])
                || input.peek(Token![via])
                || input.peek(Token![when])
                || input.peek(Token![no_unwind])
                || input.peek(Token![opens_invariants])
        };

        // Parse inputs
        while !input.peek(Token![->]) && !input.is_empty() && !is_next_spec_keyword(input) {
            let expr = input.parse()?;
            inputs.push(expr);

            if !input.peek(Token![,]) {
                break;
            }

            let _comma: Token![,] = input.parse()?;
        }

        let outputs = if input.peek(Token![->]) {
            let token = input.parse()?;
            let mut outs = Punctuated::new();

            while !input.is_empty() && !is_next_spec_keyword(input) {
                let expr = input.parse()?;
                outs.push(expr);

                if !input.peek(Token![,]) {
                    break;
                }

                let _comma: Token![,] = input.parse()?;
            }
            Some((token, outs))
        } else {
            None
        };

        Ok(WithSpecOnFn {
            with,
            inputs,
            outputs,
        })
    }
}

#[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
impl parse::Parse for WithSpecOnExpr {
    fn parse(input: ParseStream) -> Result<Self> {
        let with = input.parse()?;
        let mut inputs = Punctuated::new();
        let mut erased_fields = Punctuated::new();
        while !input.is_empty() && !input.peek(Token![=>]) && !input.peek(Token![|=]) {
            if input.peek2(Token![:]) && !input.peek2(Token![::]) {
                let field_value: FieldValue = input.parse()?;
                if field_value.colon_token.is_none() || !field_value.member.is_named() {
                    return Err(input.error(
                        "ghost/tracked struct fields should be of the form `$ident: $expr`",
                    ));
                }
                if !field_value.attrs.is_empty() {
                    return Err(input.error("ghost/tracked struct fields cannot have attributes"));
                }
                erased_fields.push(field_value);
            } else {
                inputs.push(input.parse()?);
            }
            if !input.peek(Token![,]) {
                break;
            }
            let fork = input.fork();
            let _comma: Token![,] = fork.parse()?;
            let has_next_input = fork.parse::<Expr>().is_ok();
            let _comma: Token![,] = input.parse()?;
            if !has_next_input {
                break;
            }
        }
        let outputs = if input.peek(Token![=>]) {
            let token = input.parse()?;
            let outs = Pat::parse_single(&input)?;
            Some((token, outs))
        } else {
            None
        };
        let follows = if input.peek(Token![|=]) {
            let token = input.parse()?;
            let outs = Pat::parse_single(&input)?;
            Some((token, outs))
        } else {
            None
        };
        let applied_to_struct = !erased_fields.is_empty();
        let applied_to_function = outputs.is_some() || !inputs.is_empty();
        if applied_to_struct && applied_to_function {
            return Err(input.error(
                "Misuse of `with`: cannot have both ghost/tracked fields and function inputs/outputs",
            ));
        }
        Ok(WithSpecOnExpr {
            with,
            inputs,
            outputs,
            follows,
            erased_fields,
        })
    }
}

pub fn rejoin_tokens(stream: proc_macro2::TokenStream) -> proc_macro2::TokenStream {
    use proc_macro2::{Group, Punct, Spacing::*, Span, TokenTree};
    let mut tokens: Vec<TokenTree> = stream.into_iter().collect();
    let pun = |t: &TokenTree| match t {
        TokenTree::Punct(p) => Some((p.as_char(), p.spacing(), p.span())),
        _ => None,
    };
    let ident = |t: &TokenTree| match t {
        TokenTree::Ident(p) => Some((p.to_string(), p.span())),
        _ => None,
    };
    let adjacent = |s1: Span, s2: Span| {
        let l1 = s1.end();
        let l2 = s2.start();
        s1.local_file() == s2.local_file() && l1.eq(&l2)
    };
    fn mk_joint_punct(t: Option<(char, proc_macro2::Spacing, Span)>) -> TokenTree {
        let (op, _, span) = t.unwrap();
        let mut punct = Punct::new(op, Joint);
        punct.set_span(span);
        TokenTree::Punct(punct)
    }
    let mut i = 0;
    let mut till = if tokens.len() >= 2 {
        tokens.len() - 2
    } else {
        0
    };
    while i < till {
        let t0 = pun(&tokens[i]);
        let t1_ident = ident(&tokens[i + 1]);
        match (t0, t1_ident.as_ref().map(|(a, b)| (a.as_str(), *b))) {
            (Some(('!', Alone, s1)), Some(("is", s2))) => {
                if adjacent(s1, s2) {
                    tokens[i] = TokenTree::Ident(proc_macro2::Ident::new(
                        "isnt",
                        s1.join(s2).unwrap_or(s1),
                    ));
                    tokens.remove(i + 1);
                    i += 1;
                    till -= 1;
                    continue;
                }
            }
            (Some(('!', Alone, s1)), Some(("has", s2))) => {
                if adjacent(s1, s2) {
                    tokens[i] = TokenTree::Ident(proc_macro2::Ident::new(
                        "hasnt",
                        s1.join(s2).unwrap_or(s1),
                    ));
                    tokens.remove(i + 1);
                    i += 1;
                    till -= 1;
                    continue;
                }
            }
            _ => {}
        }
        let t1_pun = pun(&tokens[i + 1]);
        let t2 = pun(&tokens[i + 2]);
        let t3 = if i + 3 < tokens.len() {
            pun(&tokens[i + 3])
        } else {
            None
        };
        match (t0, t1_pun, t2, t3) {
            (
                Some(('<', Joint, _)),
                Some(('=', Alone, s1)),
                Some(('=', Joint, s2)),
                Some(('>', Alone, _)),
            )
            | (Some(('=', Joint, _)), Some(('=', Alone, s1)), Some(('=', Alone, s2)), _)
            | (Some(('!', Joint, _)), Some(('=', Alone, s1)), Some(('=', Alone, s2)), _)
            | (Some(('=', Joint, _)), Some(('=', Alone, s1)), Some(('>', Alone, s2)), _)
            | (Some(('<', Joint, _)), Some(('=', Alone, s1)), Some(('=', Alone, s2)), _)
            | (Some(('&', Joint, _)), Some(('&', Alone, s1)), Some(('&', Alone, s2)), _)
            | (Some(('|', Joint, _)), Some(('|', Alone, s1)), Some(('|', Alone, s2)), _) => {
                if adjacent(s1, s2) {
                    tokens[i + 1] = mk_joint_punct(t1_pun);
                }
            }
            (Some(('=', Alone, _)), Some(('~', Alone, s1)), Some(('=', Alone, s2)), _)
            | (Some(('!', Alone, _)), Some(('~', Alone, s1)), Some(('=', Alone, s2)), _) => {
                if adjacent(s1, s2) {
                    tokens[i] = mk_joint_punct(t0);
                    tokens[i + 1] = mk_joint_punct(t1_pun);
                }
            }
            (
                Some(('=', Alone, _)),
                Some(('~', Alone, _)),
                Some(('~', Alone, s2)),
                Some(('=', Alone, s3)),
            )
            | (
                Some(('!', Alone, _)),
                Some(('~', Alone, _)),
                Some(('~', Alone, s2)),
                Some(('=', Alone, s3)),
            ) => {
                if adjacent(s2, s3) {
                    tokens[i] = mk_joint_punct(t0);
                    tokens[i + 1] = mk_joint_punct(t1_pun);
                    tokens[i + 2] = mk_joint_punct(t2);
                }
            }
            _ => {}
        }
        i += 1;
    }
    for tt in &mut tokens {
        match tt {
            TokenTree::Group(group) => {
                let mut new_group = Group::new(group.delimiter(), rejoin_tokens(group.stream()));
                new_group.set_span(group.span());
                *group = new_group;
            }
            _ => {}
        }
    }
    use std::iter::FromIterator;
    proc_macro2::TokenStream::from_iter(tokens.into_iter())
}