bugfix: interaction between triggers, let, and nested quantifiers, fixes

 #1347 (#1362)

triggers aren't allowed to have 'let' variables that are declared within a trigger.
However, the logic was wrong for the following corner case:

```
forall |x|
  let y ...;
  forall |z|
    #[trigger] foo(y, z)
```

The problem with this code is that while the trigger *does* contain a let-variable (y),
the trigger is not *for* the outer quantifier, but for the inner one
(where it's allowed because the 'let' is outside)

source/rust_verify_test/tests/triggers.rs

@@ -390,3 +390,58 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_self_in_trigger_in_clone_issue1347 verus_code! {
+        use vstd::*;
+        use vstd::prelude::*;
+
+        struct Node {
+            child: Option<Box<Node>>,
+        }
+
+        impl Node {
+            pub spec fn map(self) -> Map<int, int>;
+        }
+
+        impl Clone for Node {
+            fn clone(&self) -> (res: Self)
+                ensures forall |key: int| #[trigger] self.map().dom().contains(key) ==> key == 3
+            {
+                return Node { child: None }; // FAILS
+            }
+        }
+
+        fn test(n: Node) {
+            let t = n.clone();
+            assert(forall |key: int| n.map().dom().contains(key) ==> key == 3);
+        }
+
+        fn test2(n: Node) {
+            let c = Node::clone;
+            let t = c(&n);
+            assert(forall |key: int| n.map().dom().contains(key) ==> key == 3);
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file! {
+    #[test] test_lets_and_nested_quantifiers_issue1347 verus_code! {
+        spec fn llama(x: int) -> int;
+        spec fn foo(x: int, y: int) -> bool;
+        spec fn bar(x: int) -> bool;
+
+        proof fn test() {
+            let b =
+              forall |x: int| #[trigger] bar(x) ==> ({
+                let y = llama(x);
+                forall |z: int| #[trigger] foo(y, z)
+              });
+
+            assume(b);
+            assume(bar(7));
+            assert(foo(llama(7), 20));
+            assert(foo(llama(7), 21));
+        }
+    } => Ok(())
+}

source/vir/src/sst_visitor.rs

@@ -2,6 +2,7 @@ use crate::ast::{
     BinaryOpr, GenericBound, GenericBoundX, NullaryOpr, SpannedTyped, Typ, UnaryOpr, VarBinder,
     VarIdent, VirErr,
 };
+use crate::ast_visitor::TypVisitor;
 use crate::def::Spanned;
 use crate::inv_masks::{MaskSetE, MaskSingleton};
 use crate::sst::{
@@ -1043,3 +1044,99 @@ where
     let mut visitor = MapStmPrevVisitor { fs };
     visitor.visit_stm(stm)
 }
+
+struct ExpTypVisitorDfs<'a, Env, FE, FT> {
+    map: &'a mut VisitorScopeMap,
+    env: &'a mut Env,
+    fe: &'a mut FE,
+    ft: &'a mut FT,
+}
+
+impl<'a, T, Env, FE, FT> Visitor<Walk, T, VisitorScopeMap> for ExpTypVisitorDfs<'a, Env, FE, FT>
+where
+    FE: FnMut(&Exp, &mut Env, &mut VisitorScopeMap) -> VisitorControlFlow<T>,
+    FT: FnMut(&Typ, &mut Env, &mut VisitorScopeMap) -> VisitorControlFlow<T>,
+{
+    fn visit_exp(&mut self, exp: &Exp) -> Result<(), T> {
+        match (self.fe)(exp, &mut self.env, &mut self.map) {
+            VisitorControlFlow::Stop(val) => Err(val),
+            VisitorControlFlow::Return => Ok(()),
+            VisitorControlFlow::Recurse => self.visit_exp_rec(exp),
+        }
+    }
+
+    fn visit_typ(&mut self, typ: &Typ) -> Result<(), T> {
+        match (self.ft)(typ, &mut self.env, &mut self.map) {
+            VisitorControlFlow::Stop(val) => Err(val),
+            VisitorControlFlow::Return => Ok(()),
+            VisitorControlFlow::Recurse => self.visit_typ_rec(typ),
+        }
+    }
+
+    fn scoper(&mut self) -> Option<&mut VisitorScopeMap> {
+        Some(&mut self.map)
+    }
+}
+
+impl<'a, T, Env, FE, FT> crate::ast_visitor::TypVisitor<Walk, T>
+    for ExpTypVisitorDfs<'a, Env, FE, FT>
+where
+    FE: FnMut(&Exp, &mut Env, &mut VisitorScopeMap) -> VisitorControlFlow<T>,
+    FT: FnMut(&Typ, &mut Env, &mut VisitorScopeMap) -> VisitorControlFlow<T>,
+{
+    fn visit_typ(&mut self, typ: &Typ) -> Result<(), T> {
+        match (self.ft)(typ, &mut self.env, &mut self.map) {
+            VisitorControlFlow::Stop(val) => Err(val),
+            VisitorControlFlow::Return => Ok(()),
+            VisitorControlFlow::Recurse => self.visit_typ_rec(typ),
+        }
+    }
+}
+
+pub(crate) fn exp_typ_visitor_dfs<T, Env, FE, FT>(
+    exp: &Exp,
+    map: &mut VisitorScopeMap,
+    env: &mut Env,
+    fe: &mut FE,
+    ft: &mut FT,
+) -> VisitorControlFlow<T>
+where
+    FE: FnMut(&Exp, &mut Env, &mut VisitorScopeMap) -> VisitorControlFlow<T>,
+    FT: FnMut(&Typ, &mut Env, &mut VisitorScopeMap) -> VisitorControlFlow<T>,
+{
+    let mut visitor = ExpTypVisitorDfs { map, env, fe, ft };
+    match visitor.visit_exp(exp) {
+        Ok(()) => VisitorControlFlow::Recurse,
+        Err(val) => VisitorControlFlow::Stop(val),
+    }
+}
+
+pub(crate) fn exp_typ_visitor_check<E, Env, FE, FT>(
+    exp: &Exp,
+    map: &mut VisitorScopeMap,
+    env: &mut Env,
+    fe: &mut FE,
+    ft: &mut FT,
+) -> Result<(), E>
+where
+    FE: FnMut(&Exp, &mut Env, &mut VisitorScopeMap) -> Result<(), E>,
+    FT: FnMut(&Typ, &mut Env, &mut VisitorScopeMap) -> Result<(), E>,
+{
+    match exp_typ_visitor_dfs(
+        exp,
+        map,
+        env,
+        &mut |exp, env, map| match fe(exp, env, map) {
+            Ok(()) => VisitorControlFlow::Recurse,
+            Err(e) => VisitorControlFlow::Stop(e),
+        },
+        &mut |exp, env, map| match ft(exp, env, map) {
+            Ok(()) => VisitorControlFlow::Recurse,
+            Err(e) => VisitorControlFlow::Stop(e),
+        },
+    ) {
+        VisitorControlFlow::Recurse => Ok(()),
+        VisitorControlFlow::Return => unreachable!(),
+        VisitorControlFlow::Stop(e) => Err(e),
+    }
+}

source/vir/src/triggers.rs

@@ -136,10 +136,37 @@ fn check_trigger_expr_args(state: &mut State, expect_boxed: bool, args: &Exps) {
     }
 }
 
+fn get_free_vars(exp: &Exp) -> Result<HashSet<VarIdent>, VirErr> {
+    let mut scope_map = ScopeMap::new();
+    let mut free_vars = HashSet::<VarIdent>::new();
+    crate::sst_visitor::exp_typ_visitor_check(
+        exp,
+        &mut scope_map,
+        &mut free_vars,
+        &mut |exp: &Exp, free_vars: &mut HashSet<VarIdent>, _scope_map| match &exp.x {
+            ExpX::Var(x) => {
+                free_vars.insert(x.clone());
+                Ok(())
+            }
+            ExpX::Bind(_, _) => {
+                Err(error(&exp.span, "triggers cannot contain let/forall/exists/lambda/choose"))
+            }
+            _ => Ok(()),
+        },
+        &mut |typ: &Typ, free_vars: &mut HashSet<VarIdent>, _scope_map| match &**typ {
+            TypX::TypParam(x) => {
+                free_vars.insert(crate::def::suffix_typ_param_id(x));
+                Ok(())
+            }
+            _ => Ok(()),
+        },
+    )?;
+    Ok(free_vars)
+}
+
 fn check_trigger_expr(
     state: &mut State,
     exp: &Exp,
-    free_vars: &mut HashSet<VarIdent>,
     lets: &HashSet<VarIdent>,
 ) -> Result<(), VirErr> {
     match &exp.x {
@@ -161,13 +188,6 @@ fn check_trigger_expr(
     }
 
     let mut scope_map = ScopeMap::new();
-    let ft = |free_vars: &mut HashSet<VarIdent>, t: &Typ| match &**t {
-        TypX::TypParam(x) => {
-            free_vars.insert(crate::def::suffix_typ_param_id(x));
-            Ok(t.clone())
-        }
-        _ => Ok(t.clone()),
-    };
     crate::sst_visitor::exp_visitor_check(
         exp,
         &mut scope_map,
@@ -189,10 +209,7 @@ fn check_trigger_expr(
             }
             ExpX::Loc(..) | ExpX::VarLoc(..) => Ok(()),
             ExpX::ExecFnByName(..) => Ok(()),
-            ExpX::Call(_, typs, args) => {
-                for typ in typs.iter() {
-                    crate::ast_visitor::map_typ_visitor_env(typ, free_vars, &ft).unwrap();
-                }
+            ExpX::Call(_, _typs, args) => {
                 check_trigger_expr_args(state, true, args);
                 Ok(())
             }
@@ -203,15 +220,11 @@ fn check_trigger_expr(
                         "let variables in triggers not supported, use #![trigger ...] instead",
                     ));
                 }
-                free_vars.insert(x.clone());
                 Ok(())
             }
             ExpX::VarAt(_, VarAt::Pre) => Ok(()),
             ExpX::Old(_, _) => panic!("internal error: Old"),
-            ExpX::NullaryOpr(crate::ast::NullaryOpr::ConstGeneric(typ)) => {
-                crate::ast_visitor::map_typ_visitor_env(typ, free_vars, &ft).unwrap();
-                Ok(())
-            }
+            ExpX::NullaryOpr(crate::ast::NullaryOpr::ConstGeneric(_typ)) => Ok(()),
             ExpX::NullaryOpr(crate::ast::NullaryOpr::TraitBound(..)) => {
                 Err(error(&exp.span, "triggers cannot contain trait bounds"))
             }
@@ -274,7 +287,6 @@ fn check_trigger_expr(
                         Ok(())
                     }
                     ArrayIndex => {
-                        crate::ast_visitor::map_typ_visitor_env(&arg1.typ, free_vars, &ft).unwrap();
                         check_trigger_expr_arg(state, true, arg1);
                         check_trigger_expr_arg(state, true, arg2);
                         Ok(())
@@ -286,8 +298,7 @@ fn check_trigger_expr(
                     }
                 }
             }
-            ExpX::BinaryOpr(crate::ast::BinaryOpr::ExtEq(_, typ), arg1, arg2) => {
-                crate::ast_visitor::map_typ_visitor_env(typ, free_vars, &ft).unwrap();
+            ExpX::BinaryOpr(crate::ast::BinaryOpr::ExtEq(_, _typ), arg1, arg2) => {
                 check_trigger_expr_arg(state, true, arg1);
                 check_trigger_expr_arg(state, true, arg2);
                 Ok(())
@@ -311,6 +322,8 @@ fn check_trigger_expr(
 
 fn get_manual_triggers(state: &mut State, exp: &Exp) -> Result<(), VirErr> {
     let mut map: ScopeMap<VarIdent, bool> = ScopeMap::new();
+    // REVIEW: 'lets' is an over-approximation because nothing ever gets removed
+    // while you traverse?
     let mut lets: HashSet<VarIdent> = HashSet::new();
     map.push_scope(false);
     for x in state.trigger_vars.iter() {
@@ -332,16 +345,21 @@ fn get_manual_triggers(state: &mut State, exp: &Exp) -> Result<(), VirErr> {
                 Ok(())
             }
             ExpX::Unary(UnaryOp::Trigger(TriggerAnnotation::Trigger(group)), e1) => {
-                let mut free_vars: HashSet<VarIdent> = HashSet::new();
+                let free_vars: HashSet<VarIdent> = get_free_vars(e1)?;
                 let e1 = preprocess_exp(&e1);
-                check_trigger_expr(state, &e1, &mut free_vars, &lets)?;
                 for x in &free_vars {
-                    if map.get(x) == Some(&true) && !state.trigger_vars.contains(x) {
+                    if map.get(x) == Some(&true)
+                        && !state.trigger_vars.contains(x)
+                        && !lets.contains(x)
+                    {
                         // If the trigger contains variables declared by a nested quantifier,
                         // it must be the nested quantifier's trigger, not ours.
                         return Ok(());
                     }
                 }
+                check_trigger_expr(state, &e1, &lets)?;
+                // If the trigger doesn't contain *any* of our trigger vars, then it must
+                // be for a more outer quantifier
                 if !state.trigger_vars.iter().any(|trigger_var| free_vars.contains(trigger_var)) {
                     return Ok(());
                 }
@@ -364,8 +382,8 @@ fn get_manual_triggers(state: &mut State, exp: &Exp) -> Result<(), VirErr> {
                         let mut coverage: HashSet<VarIdent> = HashSet::new();
                         let es: Vec<Exp> = trigger.iter().map(preprocess_exp).collect();
                         for e in &es {
-                            let mut free_vars: HashSet<VarIdent> = HashSet::new();
-                            check_trigger_expr(state, e, &mut free_vars, &lets)?;
+                            let free_vars: HashSet<VarIdent> = get_free_vars(e)?;
+                            check_trigger_expr(state, e, &lets)?;
                             for x in free_vars {
                                 if state.trigger_vars.contains(&x) {
                                     coverage.insert(x);