Replace height intrinsic with is_smaller_than and make height a parti…

…al order (#570)

* Replace height intrinsic with is_smaller_than,
and in the SMT encoding, encode height as a Z3 partial order rather than an int
to allow decreases on infinite maps.

* Update .github/workflows/get-z3.sh to Z3 4.12.2

* Allow decreases on FnSpec fields

* Add is_smaller_than_lexicographic and some comments

* Add decreases_to macro

* Split is_smaller_than handling into separate function

* Restrict usage of decreases through FnSpec and Map,
erring on the side of caution,
inspired by FStarLang/FStar#2954

.github/workflows/get-z3.sh

@@ -1,5 +1,5 @@
 #! /bin/bash
-z3_version="4.10.1"
+z3_version="4.12.2"
 
 filename=z3-$z3_version-x64-glibc-2.31
 wget https://github.com/Z3Prover/z3/releases/download/z3-$z3_version/$filename.zip

source/air/src/ast.rs

@@ -49,6 +49,22 @@ pub enum UnaryOp {
     BitExtract(u32, u32),
 }
 
+/// These are Z3 special relations x <= y that are documented at
+/// https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/
+#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)]
+pub enum Relation {
+    /// reflexive, transitive, antisymmetric
+    PartialOrder,
+    /// reflexive, transitive, antisymmetric, and for all x, y. (x <= y or y <= x)
+    LinearOrder,
+    /// reflexive, transitive, antisymmetric, and for all x, y, z. (y <= x and z <= x) ==> (y <= z or z <= y)
+    TreeOrder,
+    /// reflexive, transitive, antisymmetric, and:
+    /// - for all x, y, z. (x <= y and x <= z) ==> (y <= z or z <= y)
+    /// - for all x, y, z. (y <= x and z <= x) ==> (y <= z or z <= y)
+    PiecewiseLinearOrder,
+}
+
 #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)]
 pub enum BinaryOp {
     Implies,
@@ -59,7 +75,12 @@ pub enum BinaryOp {
     Gt,
     EuclideanDiv,
     EuclideanMod,
-
+    /// Z3 special relations (see Relation above)
+    /// The u64 is the Z3 unique name ("index") for each relation that the user wants
+    /// ("To create a different relation that is also a partial order use a different index,
+    /// such as (_ partial-order 1)", according to
+    /// https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/ .)
+    Relation(Relation, u64),
     BitXor,
     BitAnd,
     BitOr,

source/air/src/closure.rs

@@ -455,7 +455,7 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex
         ExprX::Binary(op, e1, e2) => {
             let (es, ts) = simplify_exprs_ref(ctxt, state, &vec![e1, e2]);
             let typ = match op {
-                BinaryOp::Implies | BinaryOp::Eq => Arc::new(TypX::Bool),
+                BinaryOp::Implies | BinaryOp::Eq | BinaryOp::Relation(..) => Arc::new(TypX::Bool),
                 BinaryOp::Le | BinaryOp::Ge | BinaryOp::Lt | BinaryOp::Gt => Arc::new(TypX::Bool),
                 BinaryOp::EuclideanDiv | BinaryOp::EuclideanMod => Arc::new(TypX::Int),
                 BinaryOp::BitUGt | BinaryOp::BitULt | BinaryOp::BitUGe | BinaryOp::BitULe => {

source/air/src/parser.rs

@@ -1,7 +1,7 @@
 use crate::ast::{
     BinaryOp, BindX, Binder, BinderX, Binders, Command, CommandX, Commands, Constant, Decl, DeclX,
-    Decls, Expr, ExprX, Exprs, MultiOp, Qid, Quant, QueryX, Span, Stmt, StmtX, Stmts, Trigger,
-    Triggers, Typ, TypX, UnaryOp,
+    Decls, Expr, ExprX, Exprs, MultiOp, Qid, Quant, QueryX, Relation, Span, Stmt, StmtX, Stmts,
+    Trigger, Triggers, Typ, TypX, UnaryOp,
 };
 use crate::def::mk_skolem_id;
 use crate::messages::{error_from_labels, error_from_spans, MessageLabel, MessageLabels};
@@ -45,6 +45,27 @@ fn underscore_atom_atom_expr(s1: &str, s2: &str) -> Option<Constant> {
     None
 }
 
+fn relation_binary_op(n1: &Node, n2: &Node) -> Option<BinaryOp> {
+    match (n1, n2) {
+        (Node::Atom(s1), Node::Atom(s2)) => {
+            if let Ok(n) = s2.parse::<u64>() {
+                match s1.as_str() {
+                    "partial-order" => Some(BinaryOp::Relation(Relation::PartialOrder, n)),
+                    "linear-order" => Some(BinaryOp::Relation(Relation::LinearOrder, n)),
+                    "tree-order" => Some(BinaryOp::Relation(Relation::TreeOrder, n)),
+                    "piecewise-linear-order" => {
+                        Some(BinaryOp::Relation(Relation::PiecewiseLinearOrder, n))
+                    }
+                    _ => None,
+                }
+            } else {
+                None
+            }
+        }
+        _ => None,
+    }
+}
+
 fn map_nodes_to_vec<A, F>(nodes: &[Node], f: &F) -> Result<Arc<Vec<A>>, String>
 where
     F: Fn(&Node) -> Result<A, String>,
@@ -229,6 +250,13 @@ impl Parser {
                     Node::Atom(s) if s.to_string() == "bvlshr" => Some(BinaryOp::LShr),
                     Node::Atom(s) if s.to_string() == "bvshl" => Some(BinaryOp::Shl),
                     Node::Atom(s) if s.to_string() == "concat" => Some(BinaryOp::BitConcat),
+                    Node::List(nodes)
+                        if nodes.len() == 3
+                            && nodes[0] == Node::Atom("_".to_string())
+                            && relation_binary_op(&nodes[1], &nodes[2]).is_some() =>
+                    {
+                        relation_binary_op(&nodes[1], &nodes[2])
+                    }
                     _ => None,
                 };
                 let lop = match &nodes[0] {

source/air/src/printer.rs

@@ -158,6 +158,18 @@ impl Printer {
                     _ => Node::List(vec![str_to_node(sop), self.expr_to_node(expr)]),
                 }
             }
+            ExprX::Binary(BinaryOp::Relation(relation, n), lhs, rhs) => {
+                use crate::ast::Relation;
+                let s = match relation {
+                    Relation::PartialOrder => "partial-order",
+                    Relation::LinearOrder => "linear-order",
+                    Relation::TreeOrder => "tree-order",
+                    Relation::PiecewiseLinearOrder => "piecewise-linear-order",
+                };
+                let op =
+                    Node::List(vec![str_to_node("_"), str_to_node(s), Node::Atom(n.to_string())]);
+                Node::List(vec![op, self.expr_to_node(lhs), self.expr_to_node(rhs)])
+            }
             ExprX::Binary(op, lhs, rhs) => {
                 let sop = match op {
                     BinaryOp::Implies => "=>",
@@ -168,7 +180,7 @@ impl Printer {
                     BinaryOp::Gt => ">",
                     BinaryOp::EuclideanDiv => "div",
                     BinaryOp::EuclideanMod => "mod",
-
+                    BinaryOp::Relation(..) => unreachable!(),
                     BinaryOp::BitXor => "bvxor",
                     BinaryOp::BitAnd => "bvand",
                     BinaryOp::BitOr => "bvor",
@@ -440,7 +452,7 @@ impl NodeWriter {
                         {
                             brk = true;
                         }
-                        Node::Atom(a) if a == ":pattern" => {
+                        Node::Atom(a) if a == ":pattern" || a == ":qid" || a == ":skolemid" => {
                             was_pattern = true;
                         }
                         _ => {}

source/air/src/tests.rs

@@ -1600,3 +1600,33 @@ fn no_choose5() {
         )
     )
 }
+
+#[test]
+fn yes_partial_order() {
+    yes!(
+        (declare-sort X 0)
+        (declare-const c1 X)
+        (declare-const c2 X)
+        (declare-const c3 X)
+        (check-valid
+            (axiom ((_ partial-order 77) c1 c2))
+            (axiom ((_ partial-order 77) c2 c3))
+            (assert ((_ partial-order 77) c1 c3))
+        )
+    )
+}
+
+#[test]
+fn no_partial_order() {
+    no!(
+        (declare-sort X 0)
+        (declare-const c1 X)
+        (declare-const c2 X)
+        (declare-const c3 X)
+        (check-valid
+            (axiom ((_ partial-order 77) c1 c2))
+            (axiom ((_ partial-order 76) c2 c3))
+            (assert ((_ partial-order 77) c1 c3))
+        )
+    )
+}

source/air/src/typecheck.rs

@@ -225,14 +225,18 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result<Typ, TypeError> {
         ExprX::Binary(BinaryOp::Implies, e1, e2) => {
             check_exprs(typing, "=>", &[bt(), bt()], &bt(), &[e1.clone(), e2.clone()])
         }
-        ExprX::Binary(BinaryOp::Eq, e1, e2) => {
+        ExprX::Binary(op @ (BinaryOp::Eq | BinaryOp::Relation(..)), e1, e2) => {
             let t1 = check_expr(typing, e1)?;
             let t2 = check_expr(typing, e2)?;
             if typ_eq(&t1, &t2) {
                 Ok(bt())
             } else {
                 Err(format!(
-                    "in equality, left expression has type {} and right expression has different type {}",
+                    "in {}, left expression has type {} and right expression has different type {}",
+                    match op {
+                        BinaryOp::Eq => "equality",
+                        _ => "relation",
+                    },
                     typ_name(&t1),
                     typ_name(&t2)
                 ))

source/builtin/src/lib.rs

@@ -1055,6 +1055,38 @@ pub fn arch_word_bits() -> nat {
     unimplemented!();
 }
 
-pub fn height<A>(_a: A) -> nat {
+pub fn is_smaller_than<A, B>(_: A, _: B) -> bool {
     unimplemented!();
 }
+
+pub fn is_smaller_than_lexicographic<A, B>(_: A, _: B) -> bool {
+    unimplemented!();
+}
+
+pub fn is_smaller_than_recursive_function_field<A, B>(_: A, _: B) -> bool {
+    unimplemented!();
+}
+
+#[macro_export]
+macro_rules! decreases_to_internal {
+    ($($x:expr),* $(,)? => $($y:expr),* $(,)?) => {
+        $crate::is_smaller_than_lexicographic(($($y,)*), ($($x,)*))
+    }
+}
+
+/// decreases_to!(b => a) means that height(a) < height(b), so that b can decrease to a
+/// in decreases clauses.
+/// decreases_to!(b1, ..., bn => a1, ..., am) can compare lexicographically ordered values,
+/// which can be useful when making assertions about decreases clauses.
+/// Notes:
+/// - decreases_to! desugars to a call to is_smaller_than_lexicographic.
+/// - you can write #[trigger](decreases_to!(b => a)) to trigger on height(a).
+///   (in the SMT encoding, height is a function call and is a useful trigger,
+///   while is_smaller_than/is_smaller_than_lexicographic is not a function call
+///   and is not a useful trigger.)
+#[macro_export]
+macro_rules! decreases_to {
+    ($($x:tt)*) => {
+        ::builtin_macros::verus_proof_macro_exprs!($crate::decreases_to_internal!($($x)*))
+    };
+}

source/pervasive/map.rs

@@ -300,6 +300,41 @@ impl<K, V> Map<K, V> {
 
 // Trusted axioms
 
+/* REVIEW: this is simpler than the two separate axioms below -- would this be ok?
+#[verifier(external_body)]
+#[verifier(broadcast_forall)]
+pub proof fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K)
+    requires
+        m.dom().contains(key),
+    ensures
+        #[trigger](decreases_to!(m => m[key])),
+{
+}
+*/
+
+#[verifier(external_body)]
+#[verifier(broadcast_forall)]
+pub proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
+    requires
+        m.dom().finite(),
+        m.dom().contains(key),
+    ensures
+        #[trigger](decreases_to!(m => m[key])),
+{
+}
+
+// REVIEW: this is currently a special case that is hard-wired into the verifier
+// It implements a version of https://github.com/FStarLang/FStar/pull/2954 .
+#[verifier(external_body)]
+#[verifier(broadcast_forall)]
+pub proof fn axiom_map_index_decreases_infinite<K, V>(m: Map<K, V>, key: K)
+    requires
+        m.dom().contains(key),
+    ensures
+        #[trigger] is_smaller_than_recursive_function_field(m[key], m),
+{
+}
+
 #[verifier(external_body)]
 #[verifier(broadcast_forall)]
 pub proof fn axiom_map_empty<K, V>()

source/pervasive/seq.rs

@@ -173,6 +173,16 @@ impl<A> Seq<A> {
 
 // Trusted axioms
 
+#[verifier(external_body)]
+#[verifier(broadcast_forall)]
+pub proof fn axiom_seq_index_decreases<A>(s: Seq<A>, i: int)
+    requires
+        0 <= i < s.len(),
+    ensures
+        #[trigger](decreases_to!(s => s[i])),
+{
+}
+
 #[verifier(external_body)]
 #[verifier(broadcast_forall)]
 pub proof fn axiom_seq_empty<A>()

source/rust_verify/example/summer_school/chapter-1-22.rs

@@ -136,9 +136,8 @@ fn check_is_sorted_tree(tree: &Tree) -> (ret: TreeSortedness)
 
             proof {
                 sorted_tree_means_sorted_sequence(**left);
+                sorted_tree_means_sorted_sequence(**right);
             }
-            // sorted_tree_means_sorted_sequence(**right); // TODO: why is only one of these calls
-            // necessary?
 
             // assert(equal(tree@, [email protected](seq![*value as int]).add(right@)));
             // assert([email protected]() > 0);

source/rust_verify/src/consts.rs

@@ -1 +1 @@
-pub const EXPECTED_SOLVER_VERSION: &str = "4.10.1";
+pub const EXPECTED_SOLVER_VERSION: &str = "4.12.2";

source/rust_verify/src/erase.rs

@@ -6,7 +6,7 @@ use rustc_span::SpanData;
 use vir::ast::{AutospecUsage, Fun, Krate, Mode, Path, Pattern};
 use vir::modes::ErasureModes;
 
-#[derive(Clone, Copy, Debug)]
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
 pub enum CompilableOperator {
     IntIntrinsic,
     Implies,
@@ -25,7 +25,7 @@ pub enum CompilableOperator {
 }
 
 /// Information about each call in the AST (each ExprKind::Call).
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub enum ResolvedCall {
     /// The call is to a spec or proof function, and should be erased
     Spec,

source/rust_verify/src/lifetime_generate.rs

@@ -2004,7 +2004,13 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
         ctxt.ignored_functions.insert(*id);
     }
     for (hir_id, span, call) in &erasure_hints.resolved_calls {
-        ctxt.calls.insert(*hir_id, call.clone()).map(|_| panic!("{:?}", span));
+        if ctxt.calls.contains_key(hir_id) {
+            if &ctxt.calls[hir_id] != call {
+                panic!("inconsistent resolved_calls: {:?}", span);
+            }
+        } else {
+            ctxt.calls.insert(*hir_id, call.clone());
+        }
     }
     for (span, mode) in &erasure_hints.erasure_modes.condition_modes {
         if crate::spans::from_raw_span(&span.raw_span).is_none() {
@@ -2015,7 +2021,13 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
             panic!("missing id_to_hir");
         }
         for hir_id in &id_to_hir[&span.id] {
-            ctxt.condition_modes.insert(*hir_id, *mode).map(|_| panic!("{:?}", span));
+            if ctxt.condition_modes.contains_key(hir_id) {
+                if &ctxt.condition_modes[hir_id] != mode {
+                    panic!("inconsistent condition_modes: {:?}", span);
+                }
+            } else {
+                ctxt.condition_modes.insert(*hir_id, *mode);
+            }
         }
     }
     for (span, mode) in &erasure_hints.erasure_modes.var_modes {
@@ -2027,7 +2039,13 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
             panic!("missing id_to_hir");
         }
         for hir_id in &id_to_hir[&span.id] {
-            ctxt.var_modes.insert(*hir_id, *mode).map(|v| panic!("{:?} {:?}", span, v));
+            if ctxt.var_modes.contains_key(hir_id) {
+                if &ctxt.var_modes[hir_id] != mode {
+                    panic!("inconsistent var_modes: {:?}", span);
+                }
+            } else {
+                ctxt.var_modes.insert(*hir_id, *mode);
+            }
         }
     }
     for (hir_id, mode) in &erasure_hints.direct_var_modes {