[move-prover] Adding behavioral predicates to the parser (#18428)

* [ai] Basic setup for Cursor/Claude agents.md

This adds autogenerated configuration files for Claude code and for Cursor.

- `CLAUDE.md` which links to `agents.md`
- `agents.md` is generarted via Cursor AND Claude
- Moreover, for safety and privacy, an autogenerated `.cursorignore`.

The process how `agents.md` has been created was as follows:

- Use claude command `/init` to created `CLAUDE.md`
- Ask cursor 'generate `agents.md` by extending `CLAUDE.md`'
- Remove original CLAUDE.md and symlink to agents

This little trick was recommended by Gemini. Moving forward, we can ask Claude or Cursor to further extend this file with specific instructions.

* Separating files.

* [move-prover] Adding behavioral predicates to the parser

This adds parsing support for behavioral predicates for function values
in specifications. These predicates allow reasoning about the behavior
of function-typed parameters:

- `requires_of<f>(args)` - precondition of function `f`
- `aborts_of<f>(args)` - aborts condition of function `f`
- `ensures_of<f>(args)` - postcondition of function `f`
- `modifies_of<f>(args)` - modify clauses of function `f`

State labels can be used to bind pre/post states:
- `S@ensures_of<f>(args)` - with pre-state label
- `ensures_of<f>(args)@R` - with post-state label
- `S@ensures_of<f>(args)@R` - with both labels

The syntax is parsed and passed through to the expansion AST. The model
builder currently produces an error indicating the feature is not yet
fully supported. Tests are added for:
- Valid syntax with model builder error
- Parser error for invalid syntax
- Spec-context-only restriction

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

Author: wrwg

third_party/move/move-compiler-v2/legacy-move-compiler/src/expansion/ast.rs

@@ -5,9 +5,9 @@
 use crate::{
     expansion::translate::is_valid_struct_constant_or_schema_name,
     parser::ast::{
-        self as P, Ability, Ability_, BinOp, CallKind, ConstantName, Field, FunctionName, Label,
-        LambdaCaptureKind, ModuleName, QuantKind, SpecApplyPattern, StructName, UnaryOp, UseDecl,
-        Var, VariantName, ENTRY_MODIFIER,
+        self as P, Ability, Ability_, BehaviorKind, BinOp, CallKind, ConstantName, Field,
+        FunctionName, Label, LambdaCaptureKind, ModuleName, QuantKind, SpecApplyPattern,
+        StructName, UnaryOp, UseDecl, Var, VariantName, ENTRY_MODIFIER,
     },
     shared::{
         ast_debug::*,
@@ -542,6 +542,19 @@ pub enum Exp_ {
         Option<Box<Exp>>,
         Box<Exp>,
     ), // spec only
+    // Behavior predicate for function values in specifications:
+    // [pre_label@]requires_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    // [pre_label@]aborts_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    // [pre_label@]ensures_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    // [pre_label@]modifies_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    Behavior(
+        BehaviorKind,
+        Option<Label>,     // pre-state label
+        ModuleAccess,      // function name
+        Option<Vec<Type>>, // optional type instantiation
+        Spanned<Vec<Exp>>, // arguments
+        Option<Label>,     // post-state label
+    ), // spec only
 
     Assign(LValueList, Box<Exp>),
     FieldMutate(Box<ExpDotted>, Box<Exp>),
@@ -1863,6 +1876,31 @@ impl AstDebug for Exp_ {
                     w.write("]");
                 }
             },
+            E::Behavior(kind, pre_label, fn_name, type_args, sp!(_, args), post_label) => {
+                if let Some(label) = pre_label {
+                    w.write(format!("{}@", label.value().as_str()));
+                }
+                let kind_str = match kind {
+                    BehaviorKind::RequiresOf => "requires_of",
+                    BehaviorKind::AbortsOf => "aborts_of",
+                    BehaviorKind::EnsuresOf => "ensures_of",
+                    BehaviorKind::ModifiesOf => "modifies_of",
+                };
+                w.write(kind_str);
+                w.write("<");
+                fn_name.ast_debug(w);
+                if let Some(tys) = type_args {
+                    w.write("<");
+                    w.comma(tys, |w, ty| ty.ast_debug(w));
+                    w.write(">");
+                }
+                w.write(">(");
+                w.comma(args, |w, e| e.ast_debug(w));
+                w.write(")");
+                if let Some(label) = post_label {
+                    w.write(format!("@{}", label.value().as_str()));
+                }
+            },
             E::UnresolvedError => w.write("_|_"),
         }
     }

third_party/move/move-compiler-v2/legacy-move-compiler/src/expansion/dependency_ordering.rs

@@ -591,6 +591,11 @@ fn exp(context: &mut Context, sp!(_loc, e_): &E::Exp) {
             eopt.iter().for_each(|e| exp(context, e));
             exp(context, e)
         },
+        E::Behavior(_, _, fn_name, type_args, sp!(_, args), _) => {
+            module_access(context, fn_name);
+            types_opt(context, type_args);
+            args.iter().for_each(|e| exp(context, e))
+        },
     }
 }
 

third_party/move/move-compiler-v2/legacy-move-compiler/src/expansion/translate.rs

@@ -2806,6 +2806,32 @@ fn exp_(context: &mut Context, sp!(loc, pe_): P::Exp) -> E::Exp {
             } = unbound_names;
             EE::Spec(spec_id, unbound_vars, unbound_func_ptrs)
         },
+        PE::Behavior(kind, pre_label, fn_name, type_args, sp!(args_loc, args), post_label) => {
+            if !context.in_spec_context {
+                context.env.add_diag(diag!(
+                    Syntax::SpecContextRestricted,
+                    (
+                        loc,
+                        "behavior predicate expression only allowed in specifications"
+                    )
+                ));
+                EE::UnresolvedError
+            } else {
+                let e_fn_name = name_access_chain(
+                    context,
+                    Access::Term,
+                    fn_name,
+                    Some(DeprecatedItem::Function),
+                );
+                let e_type_args = optional_types(context, type_args);
+                let e_args = sp(args_loc, exps(context, args));
+                if let Some(fn_access) = e_fn_name {
+                    EE::Behavior(kind, pre_label, fn_access, e_type_args, e_args, post_label)
+                } else {
+                    EE::UnresolvedError
+                }
+            }
+        },
         PE::UnresolvedError => panic!("ICE error should have been thrown"),
     };
     sp(loc, e_)
@@ -3419,6 +3445,15 @@ fn unbound_names_exp(unbound: &mut UnboundNames, sp!(_, e_): &E::Exp) {
             unbound.vars.extend(unbound_vars);
             unbound.func_ptrs.extend(unbound_func_ptrs);
         },
+        EE::Behavior(_, _, fn_name, _type_args, sp!(_, args), _) => {
+            match &fn_name.value {
+                E::ModuleAccess_::Name(n) => {
+                    unbound.func_ptrs.insert(*n);
+                },
+                E::ModuleAccess_::ModuleAccess(..) => (),
+            }
+            unbound_names_exps(unbound, args);
+        },
     }
 }
 

third_party/move/move-compiler-v2/legacy-move-compiler/src/parser/ast.rs

@@ -639,6 +639,20 @@ pub enum QuantKind_ {
 }
 pub type QuantKind = Spanned<QuantKind_>;
 
+/// The kind of behavior predicate for function values in specifications.
+/// These predicates allow reasoning about the behavior of function-typed parameters.
+#[derive(Debug, PartialEq, Eq, Copy, Clone)]
+pub enum BehaviorKind {
+    /// `requires_of<f>(x)` - the precondition of function `f`
+    RequiresOf,
+    /// `aborts_of<f>(x)` - the aborts condition of function `f`
+    AbortsOf,
+    /// `ensures_of<f>(x, y)` - the postcondition of function `f`
+    EnsuresOf,
+    /// `modifies_of<f>(x)` - the modify clauses of function `f`
+    ModifiesOf,
+}
+
 #[derive(Debug, PartialEq, Eq, Copy, Clone)]
 pub enum CallKind {
     /// Regular function call.
@@ -729,6 +743,20 @@ pub enum Exp_ {
         Vec<Vec<Exp>>,
         Option<Box<Exp>>,
         Box<Exp>,
+    ),
+    // spec only
+    // Behavior predicate for function values in specifications:
+    // [pre_label@]requires_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    // [pre_label@]aborts_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    // [pre_label@]ensures_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    // [pre_label@]modifies_of<f[<T1, ..., Tn>]>(args)[@post_label]
+    Behavior(
+        BehaviorKind,
+        Option<Label>,     // pre-state label
+        NameAccessChain,   // function name
+        Option<Vec<Type>>, // optional type instantiation
+        Spanned<Vec<Exp>>, // arguments
+        Option<Label>,     // post-state label
     ), // spec only
     // (e1, ..., en)
     ExpList(Vec<Exp>),
@@ -2068,6 +2096,31 @@ impl AstDebug for Exp_ {
                 s.ast_debug(w);
                 w.write("}");
             },
+            E::Behavior(kind, pre_label, fn_name, type_args, sp!(_, args), post_label) => {
+                if let Some(label) = pre_label {
+                    w.write(format!("{}@", label.value().as_str()));
+                }
+                let kind_str = match kind {
+                    BehaviorKind::RequiresOf => "requires_of",
+                    BehaviorKind::AbortsOf => "aborts_of",
+                    BehaviorKind::EnsuresOf => "ensures_of",
+                    BehaviorKind::ModifiesOf => "modifies_of",
+                };
+                w.write(kind_str);
+                w.write("<");
+                fn_name.ast_debug(w);
+                if let Some(tys) = type_args {
+                    w.write("<");
+                    w.comma(tys, |w, ty| ty.ast_debug(w));
+                    w.write(">");
+                }
+                w.write(">(");
+                w.comma(args, |w, e| e.ast_debug(w));
+                w.write(")");
+                if let Some(label) = post_label {
+                    w.write(format!("@{}", label.value().as_str()));
+                }
+            },
             E::UnresolvedError => w.write("_|_"),
         }
     }

third_party/move/move-compiler-v2/legacy-move-compiler/src/parser/syntax.rs

@@ -2010,6 +2010,7 @@ fn parse_exp(context: &mut Context) -> Result<Exp, Box<Diagnostic>> {
             parse_lambda(context, start_loc, LambdaCaptureKind::default(), token)?
         },
         Tok::Identifier if is_quant(context) => parse_quant(context)?,
+        Tok::Identifier if is_behavior_predicate(context) => parse_behavior(context)?,
         _ => {
             // This could be either an assignment, operator assignment (e.g., +=), or a binary operator
             // expression, or a cast or test
@@ -2386,6 +2387,106 @@ fn is_quant(context: &mut Context) -> bool {
     }
 }
 
+// Returns the BehaviorKind if the given identifier is a behavior predicate keyword.
+fn behavior_kind_from_str(s: &str) -> Option<BehaviorKind> {
+    match s {
+        "requires_of" => Some(BehaviorKind::RequiresOf),
+        "aborts_of" => Some(BehaviorKind::AbortsOf),
+        "ensures_of" => Some(BehaviorKind::EnsuresOf),
+        "modifies_of" => Some(BehaviorKind::ModifiesOf),
+        _ => None,
+    }
+}
+
+// Check if we're looking at a behavior predicate expression.
+// This can be either:
+//   - `identifier @ behavior_keyword < ...`  (with pre-state label)
+//   - `behavior_keyword < ...`               (without pre-state label)
+fn is_behavior_predicate(context: &mut Context) -> bool {
+    // Behavior predicates are only available in V2_4 and later
+    if context.env.flags().language_version() < LanguageVersion::V2_4 {
+        return false;
+    }
+    if context.tokens.peek() != Tok::Identifier {
+        return false;
+    }
+
+    let content = context.tokens.content();
+
+    // Check for direct behavior keyword followed by `<`
+    if behavior_kind_from_str(content).is_some() {
+        return matches!(context.tokens.lookahead(), Ok(Tok::Less));
+    }
+
+    // Check for `label @ behavior_keyword < ...` pattern
+    match context.tokens.lookahead2() {
+        Ok((Tok::AtSign, Tok::Identifier)) => {
+            // Need to check the third token - it should be a behavior keyword
+            // We can't easily lookahead 3, so we accept this pattern and validate during parse
+            true
+        },
+        _ => false,
+    }
+}
+
+// Parses a behavior predicate expression:
+//   [pre_label@]behavior_kind<fn_exp>(args)[@post_label]
+fn parse_behavior(context: &mut Context) -> Result<Exp_, Box<Diagnostic>> {
+    // Parse optional pre-state label
+    let pre_label = if context.tokens.peek() == Tok::Identifier
+        && matches!(context.tokens.lookahead(), Ok(Tok::AtSign))
+    {
+        let label_name = parse_identifier(context)?;
+        let label = Label(label_name);
+        consume_token(context.tokens, Tok::AtSign)?;
+        Some(label)
+    } else {
+        None
+    };
+
+    // Parse behavior kind
+    let kind_content = context.tokens.content();
+    let kind = behavior_kind_from_str(kind_content).ok_or_else(|| {
+        Box::new(
+            diag!(
+                Syntax::UnexpectedToken,
+                (
+                    current_token_loc(context.tokens),
+                    format!(
+                        "expected a behavior predicate keyword (requires_of, aborts_of, ensures_of, modifies_of), found '{}'",
+                        kind_content
+                    )
+                )
+            )
+        )
+    })?;
+    context.tokens.advance()?;
+
+    // Parse `<` fn_name [type_args] `>`
+    // We parse a name access chain (not a full expression) to avoid ambiguity with `>`
+    consume_token(context.tokens, Tok::Less)?;
+    let fn_name = parse_name_access_chain(context, false, || "a function name")?;
+    // Parse optional type arguments for the function
+    let type_args = parse_optional_type_args(context)?;
+    consume_token(context.tokens, Tok::Greater)?;
+
+    // Parse `(` args `)`
+    let args = parse_call_args(context)?;
+
+    // Parse optional post-state label
+    let post_label = if context.tokens.peek() == Tok::AtSign {
+        context.tokens.advance()?;
+        let label_name = parse_identifier(context)?;
+        Some(Label(label_name))
+    } else {
+        None
+    };
+
+    Ok(Exp_::Behavior(
+        kind, pre_label, fn_name, type_args, args, post_label,
+    ))
+}
+
 // Parses a quantifier expressions, assuming is_quant(context) is true.
 //
 //   <Quantifier> =

third_party/move/move-compiler-v2/tests/checking-lang-v2.4/specs/behavior_predicates_err.exp

@@ -0,0 +1,49 @@
+
+Diagnostics:
+error: behavior predicates for function values (requires_of, aborts_of, ensures_of, modifies_of) are not yet supported in the model
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:14:17
+   │
+14 │         ensures requires_of<f>(x, y);
+   │                 ^^^^^^^^^^^^^^^^^^^^
+
+error: behavior predicates for function values (requires_of, aborts_of, ensures_of, modifies_of) are not yet supported in the model
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:17:17
+   │
+17 │         ensures ensures_of<f>(x, y, result);
+   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: behavior predicates for function values (requires_of, aborts_of, ensures_of, modifies_of) are not yet supported in the model
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:20:19
+   │
+20 │         aborts_if aborts_of<f>(x, y);
+   │                   ^^^^^^^^^^^^^^^^^^
+
+error: behavior predicates for function values (requires_of, aborts_of, ensures_of, modifies_of) are not yet supported in the model
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:23:18
+   │
+23 │         modifies modifies_of<f>(x);
+   │                  ^^^^^^^^^^^^^^^^^
+
+error: global resource access expected
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:23:18
+   │
+23 │         modifies modifies_of<f>(x);
+   │                  ^^^^^^^^^^^^^^^^^
+
+error: behavior predicates for function values (requires_of, aborts_of, ensures_of, modifies_of) are not yet supported in the model
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:33:17
+   │
+33 │         ensures old@ensures_of<f>(x, result);
+   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: behavior predicates for function values (requires_of, aborts_of, ensures_of, modifies_of) are not yet supported in the model
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:36:17
+   │
+36 │         ensures ensures_of<f>(x, result)@post;
+   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: behavior predicates for function values (requires_of, aborts_of, ensures_of, modifies_of) are not yet supported in the model
+   ┌─ tests/checking-lang-v2.4/specs/behavior_predicates_err.move:39:17
+   │
+39 │         ensures pre@ensures_of<f>(x, result)@post;
+   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^