add paper example for localize_error, some fixes

crates/ide-assists/src/handlers/proof_action/intro_failing_ensures.rs

@@ -84,7 +84,7 @@ pub(crate) fn vst_rewriter_intro_failing_ensures(
 
 #[cfg(test)]
 mod tests {
-    use crate::tests::{check_assist, check_assist_with_verus_error};
+    use crate::tests::check_assist_with_verus_error;
 
     use super::*;
 

crates/ide-assists/src/handlers/proof_action/localize_error.rs

@@ -121,22 +121,22 @@ fn split_expr(ctx: &AssistContext<'_>, exp: &Expr) -> Option<Vec<Expr>> {
     }
 }
 
-// TODO: remove
-pub(crate) fn _vst_rewriter_localize_error(
-    ctx: &AssistContext<'_>,
-    assertion: AssertExpr,
-) -> Option<String> {
-    let exp = &assertion.expr;
-    let split_exprs = split_expr(ctx, exp)?;
-    let mut stmts: StmtList = StmtList::new();
-    for e in split_exprs {
-        let assert_expr = AssertExpr::new(e);
-        stmts.statements.push(assert_expr.into());
-    }
-    stmts.statements.push(assertion.into());
-    let blk = BlockExpr::new(stmts);
-    return Some(blk.to_string());
-}
+// TODO: make this a separate proof action
+// pub(crate) fn _vst_rewriter_localize_error(
+//     ctx: &AssistContext<'_>,
+//     assertion: AssertExpr,
+// ) -> Option<String> {
+//     let exp = &assertion.expr;
+//     let split_exprs = split_expr(ctx, exp)?;
+//     let mut stmts: StmtList = StmtList::new();
+//     for e in split_exprs {
+//         let assert_expr = AssertExpr::new(e);
+//         stmts.statements.push(assert_expr.into());
+//     }
+//     stmts.statements.push(assertion.into());
+//     let blk = BlockExpr::new(stmts);
+//     return Some(blk.to_string());
+// }
 
 // maybe register another action with minimization
 // TODO: try changing this to use verus
@@ -147,6 +147,9 @@ pub(crate) fn vst_rewriter_localize_error_minimized(
     let this_fn = ctx.vst_find_node_at_offset::<Fn, ast::Fn>()?; 
     let exp = &assertion.expr;
     let split_exprs = split_expr(ctx, exp)?;
+    for e in &split_exprs {
+        dbg!({}, e.to_string());
+    }
     let mut stmts: StmtList = StmtList::new();
     for e in split_exprs {
         dbg!("{}", &e.to_string());
@@ -170,11 +173,12 @@ mod tests {
     use crate::tests::check_assist;
     use super::*;
 
-    // TEST: &&
+    // TEST: && (1)
     #[test]
     fn decompose_conjunct_failure() {
         check_assist(
             localize_error,
+// before
             r#"
 use vstd::prelude::*;
 fn foo()
@@ -201,6 +205,61 @@ fn main() {}
     }
 
 
+    // TEST: && (2)
+    #[test]
+    fn decompose_conjunct_failure2() {
+        check_assist(
+            localize_error,
+// before
+            r#"
+use vstd::prelude::*;
+
+proof fn lemma_mul_inequality(x: int, y: int, z: int) by(nonlinear_arith)
+    requires x <= y && z > 0
+    ensures  x * z <= y * z    
+{}
+
+proof fn lemma_mul_strict_upper_bound(x: int, xbound: int, y: int, ybound: int)
+    requires x < xbound && y < ybound && 0 <= x && 0 <= y
+    ensures x * y <= (xbound - 1) * (ybound - 1)
+{
+    {
+        as$0sert(x <= xbound - 1 && y > 0);
+        lemma_mul_inequality(x, xbound - 1, y);
+    };
+    lemma_mul_inequality(y, ybound-1, xbound-1);
+}
+
+fn main() {}
+"#,
+// after
+            r#"
+use vstd::prelude::*;
+
+proof fn lemma_mul_inequality(x: int, y: int, z: int) by(nonlinear_arith)
+    requires x <= y && z > 0
+    ensures  x * z <= y * z    
+{}
+
+proof fn lemma_mul_strict_upper_bound(x: int, xbound: int, y: int, ybound: int)
+    requires x < xbound && y < ybound && 0 <= x && 0 <= y
+    ensures x * y <= (xbound - 1) * (ybound - 1)
+{
+    {
+        {
+            assert(y > 0);
+            assert(x <= xbound - 1 && y > 0);
+        };
+        lemma_mul_inequality(x, xbound - 1, y);
+    };
+    lemma_mul_inequality(y, ybound-1, xbound-1);
+}
+
+fn main() {}
+"#,
+        );
+    }
+
     // TEST: match
     #[test]
     fn decompose_match_failure() {

crates/ide-assists/src/vst_api/proof_action_context.rs

@@ -89,11 +89,36 @@ impl<'a> AssistContext<'a> {
         let new:vst::Stmt = new.into();
         let stmts = func.body.as_ref()?.stmt_list.statements.clone(); 
         let mut func = func.clone();
-        let replaced_stmts: Vec<vst::Stmt> = stmts.into_iter().map(|s| if s.to_string().trim() == old.to_string().trim() {new.clone()} else {s}).collect();
+        let replaced_stmts = self.replace_statement_rec(&stmts, old, new);
         func.body.as_mut()?.stmt_list.statements = replaced_stmts;  
         Some(func)
     }
 
+    fn replace_statement_rec(&self, stmts: &Vec<vst::Stmt>, old: vst::Stmt, new: vst::Stmt) -> Vec<vst::Stmt>
+    {
+        let replaced_stmts: Vec<vst::Stmt> = stmts.into_iter().map(|s| 
+            if s.to_string().trim() == old.to_string().trim() {
+                new.clone()
+            } 
+            else {
+                if let vst::Stmt::ExprStmt(exprstmt) = s {
+                    if let vst::Expr::BlockExpr(be) = &*exprstmt.expr {
+                        let inner_stmts = &be.stmt_list.statements;
+                        let changed_inner = self.replace_statement_rec(&inner_stmts, old.clone(), new.clone());
+                        let mut changed_stmts =vst::StmtList::new();
+                        changed_stmts.statements = changed_inner;
+                        let changed_exprstmt:vst::Stmt = vst::BlockExpr::new(changed_stmts).into();
+                        changed_exprstmt
+                    } else {
+                        s.clone()
+                    }
+                } else {
+                    s.clone()
+                }                
+            }).collect();  
+        replaced_stmts
+    }
+
     // helper routine to reduce a list of predicate into &&-ed predicate
     pub(crate) fn reduce_exprs(&self, es: Vec<vst::Expr>) -> Option<vst::Expr> {
         es.into_iter().reduce(|acc, e| {

crates/ide-assists/src/vst_api/run_verus.rs

@@ -104,6 +104,8 @@ impl<'a> AssistContext<'a> {
         let output = 
             Command::new(verus_exec_path)
                 .arg(path)
+                .arg("--multiple-errors")
+                .arg("10") // we want many errors as proof-action reads this. By default, Verus gives a couple of errors as a human reads those.
                 .output();
 
         // match std::fs::remove_file(path) {