Replace height intrinsic with is_smaller_than and make height a partial order

.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,14 @@ pub enum UnaryOp {
     BitExtract(u32, u32),
 }
 
+#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)]
+pub enum Relation {
+    PartialOrder,
+    LinearOrder,
+    TreeOrder,
+    PiecewiseLinearOrder,
+}
+
 #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)]
 pub enum BinaryOp {
     Implies,
@@ -59,7 +67,7 @@ pub enum BinaryOp {
     Gt,
     EuclideanDiv,
     EuclideanMod,
-
+    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

@@ -1045,6 +1045,14 @@ pub fn arch_word_bits() -> nat {
     unimplemented!();
 }
 
-pub fn height<A>(_a: A) -> nat {
+// is_smaller_than(a, b) means that height(a) < height(b), so that b can decrease to a
+// in decreases clauses.
+// Notes:
+// - you can use is_smaller_than((a1, ..., an), (b1, ..., bn)) to compare lexicographically
+//   ordered values, which can be useful when making assertions about decreases clauses
+// - when is_smaller_than(a, b) is used as a trigger, it actually triggers on height(a)
+//   (in the SMT encoding, height is a function call and is a useful trigger,
+//   while is_smaller_than is not a function call and is not a useful trigger.)
+pub fn is_smaller_than<A, B>(_: A, _: B) -> bool {
     unimplemented!();
 }

source/pervasive/map.rs

@@ -297,6 +297,16 @@ impl<K, V> Map<K, V> {
 
 // Trusted axioms
 
+#[verifier(external_body)]
+#[verifier(broadcast_forall)]
+pub proof fn axiom_map_index_height<K, V>(m: Map<K, V>, key: K)
+    requires
+        m.dom().contains(key),
+    ensures
+        #[trigger] is_smaller_than(m[key], m),
+{
+}
+
 #[verifier(external_body)]
 #[verifier(broadcast_forall)]
 pub proof fn axiom_map_empty<K, V>()

source/pervasive/seq.rs

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

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

@@ -137,9 +137,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::{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

@@ -1827,7 +1827,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() {
@@ -1838,7 +1844,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 {
@@ -1850,7 +1862,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 {

source/rust_verify/src/rust_to_vir_expr.rs

@@ -568,7 +568,7 @@ fn fn_call_to_vir<'tcx>(
     let is_signed_max = f_name == "builtin::signed_max";
     let is_unsigned_max = f_name == "builtin::unsigned_max";
     let is_arch_word_bits = f_name == "builtin::arch_word_bits";
-    let is_height = f_name == "builtin::height";
+    let is_smaller_than = f_name == "builtin::is_smaller_than";
 
     let is_reveal_strlit = tcx.is_diagnostic_item(Symbol::intern("builtin::reveal_strlit"), f);
     let is_strslice_len = tcx.is_diagnostic_item(Symbol::intern("builtin::strslice_len"), f);
@@ -702,7 +702,7 @@ fn fn_call_to_vir<'tcx>(
         || is_strslice_is_ascii
         || is_closure_to_fn_spec
         || is_arch_word_bits
-        || is_height;
+        || is_smaller_than;
     let is_spec_allow_proof_args_pre = is_spec_op
         || is_builtin_add
         || is_builtin_sub
@@ -1110,10 +1110,60 @@ fn fn_call_to_vir<'tcx>(
         return mk_expr(ExprX::UnaryOpr(UnaryOpr::IntegerTypeBound(kind, Mode::Spec), arg));
     }
 
-    if is_height {
-        assert!(args.len() == 1);
-        let arg = expr_to_vir(bctx, &args[0], ExprModifier::REGULAR)?;
-        return mk_expr(ExprX::UnaryOpr(UnaryOpr::Height, arg));
+    if is_smaller_than {
+        assert!(args.len() == 2);
+        let args0 = extract_tuple(args[0]);
+        let args1 = extract_tuple(args[1]);
+        // convert is_smaller_than((x0, y0, z0), (x1, y1, z1)) into
+        // x0 < x1 || (x0 == x1 && (y0 < y1 || (y0 == y1 && z0 < z1)))
+        // see also check_decrease in recursion.rs
+        let tbool = Arc::new(TypX::Bool);
+        let tint = Arc::new(TypX::Int(IntRange::Int));
+        let when_equalx = ExprX::Const(Constant::Bool(args1.len() < args0.len()));
+        let when_equal = bctx.spanned_typed_new(expr.span, &tbool, when_equalx);
+        let mut dec_exp: vir::ast::Expr = when_equal;
+        for (i, (exp0, exp1)) in args0.iter().zip(args1.iter()).rev().enumerate() {
+            let mk_bop = |op: BinaryOp, e1: vir::ast::Expr, e2: vir::ast::Expr| {
+                bctx.spanned_typed_new(expr.span, &tbool, ExprX::Binary(op, e1, e2))
+            };
+            let mk_cmp = |lt: bool| -> Result<vir::ast::Expr, VirErr> {
+                let e0 = expr_to_vir(bctx, exp0, ExprModifier::REGULAR)?;
+                let e1 = expr_to_vir(bctx, exp1, ExprModifier::REGULAR)?;
+                if vir::recursion::height_is_int(&e0.typ) {
+                    if lt {
+                        // 0 <= x < y
+                        let zerox = ExprX::Const(vir::ast_util::const_int_from_u128(0));
+                        let zero = bctx.spanned_typed_new(expr.span, &tint, zerox);
+                        let op0 = BinaryOp::Inequality(InequalityOp::Le);
+                        let cmp0 = mk_bop(op0, zero, e0);
+                        let op1 = BinaryOp::Inequality(InequalityOp::Lt);
+                        let e0 = expr_to_vir(bctx, exp0, ExprModifier::REGULAR)?;
+                        let cmp1 = mk_bop(op1, e0, e1);
+                        Ok(mk_bop(BinaryOp::And, cmp0, cmp1))
+                    } else {
+                        Ok(mk_bop(BinaryOp::Eq(Mode::Spec), e0, e1))
+                    }
+                } else {
+                    Ok(mk_bop(BinaryOp::HeightCompare(lt), e0, e1))
+                }
+            };
+            if i == 0 {
+                // i == 0 means last shared exp0/exp1, which we visit first
+                if args1.len() < args0.len() {
+                    // if z0 == z1, we can ignore the extra args0:
+                    // z0 < z1 || z0 == z1
+                    dec_exp = mk_bop(BinaryOp::Or, mk_cmp(true)?, mk_cmp(false)?);
+                } else {
+                    // z0 < z1
+                    dec_exp = mk_cmp(true)?;
+                }
+            } else {
+                // x0 < x1 || (x0 == x1 && dec_exp)
+                let and = mk_bop(BinaryOp::And, mk_cmp(false)?, dec_exp);
+                dec_exp = mk_bop(BinaryOp::Or, mk_cmp(true)?, and);
+            }
+        }
+        return Ok(dec_exp);
     }
 
     if is_smartptr_new {