Support for unicode str, specs for std::str fns, specs for UTF-8 (#2238)

zero-to-nat · web-flow · commit b9c1b09f6de5 · 2026-03-20T16:47:19.000-04:00
diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs
@@ -1849,13 +1849,6 @@ pub fn f64_to_bits(_f: f64) -> u64 {
     unimplemented!()
 }
 
-#[cfg(verus_keep_ghost)]
-#[rustc_diagnostic_item = "verus::verus_builtin::strslice_is_ascii"]
-#[verifier::spec]
-pub fn strslice_is_ascii<A>(_a: A) -> bool {
-    unimplemented!()
-}
-
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::verus_builtin::strslice_len"]
 #[verifier::spec]
diff --git a/source/rust_verify/src/fn_call_to_vir.rs b/source/rust_verify/src/fn_call_to_vir.rs
@@ -933,21 +933,6 @@ fn verus_item_to_vir<'tcx, 'a>(
                     ),
                 }
             }
-            ExprItem::StrSliceIsAscii => {
-                record_spec_fn(bctx, expr);
-                match &expr.kind {
-                    ExprKind::Call(_, args) => {
-                        assert!(args.len() == 1);
-                        let arg0 = args.first().unwrap();
-                        let arg0 = expr_to_vir_consume(bctx, arg0, ExprModifier::REGULAR)
-                            .expect("internal compiler error");
-                        mk_expr(ExprX::Unary(UnaryOp::StrIsAscii, arg0))
-                    }
-                    _ => panic!(
-                        "Expected a call for verus_builtin::strslice_is_ascii with one argument but did not receive it"
-                    ),
-                }
-            }
             ExprItem::ArchWordBits => {
                 record_spec_fn(bctx, expr);
                 assert!(args.len() == 0);
diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs
@@ -138,7 +138,6 @@ pub(crate) enum ExprItem {
     F64ToBits,
     StrSliceLen,
     StrSliceGetChar,
-    StrSliceIsAscii,
     ArchWordBits,
     ClosureToFnSpec,
     ClosureToFnProof,
@@ -498,7 +497,6 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> {
         ("verus::verus_builtin::f64_to_bits",             VerusItem::Expr(ExprItem::F64ToBits)),
         ("verus::verus_builtin::strslice_len",            VerusItem::Expr(ExprItem::StrSliceLen)),
         ("verus::verus_builtin::strslice_get_char",       VerusItem::Expr(ExprItem::StrSliceGetChar)),
-        ("verus::verus_builtin::strslice_is_ascii",       VerusItem::Expr(ExprItem::StrSliceIsAscii)),
         ("verus::verus_builtin::arch_word_bits",          VerusItem::Expr(ExprItem::ArchWordBits)),
         ("verus::verus_builtin::closure_to_fn_spec",      VerusItem::Expr(ExprItem::ClosureToFnSpec)),
         ("verus::verus_builtin::closure_to_fn_proof",     VerusItem::Expr(ExprItem::ClosureToFnProof)),
diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs
@@ -447,8 +447,6 @@ pub enum UnaryOp {
     HeightTrigger,
     /// Used only for handling verus_builtin::strslice_len
     StrLen,
-    /// Used only for handling verus_builtin::strslice_is_ascii
-    StrIsAscii,
     /// Given an exec/proof expression used to construct a loop iterator,
     /// try to infer a pure specification for the loop iterator.
     /// Evaluate to Some(spec) if successful, None otherwise.
diff --git a/source/vir/src/bitvector_to_air.rs b/source/vir/src/bitvector_to_air.rs
@@ -430,7 +430,7 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<BvExpr, Vir
             UnaryOp::MustBeFinalized | UnaryOp::MustBeElaborated => {
                 panic!("internal error: Exp not finalized: {:?}", arg)
             }
-            UnaryOp::StrLen | UnaryOp::StrIsAscii => panic!(
+            UnaryOp::StrLen => panic!(
                 "internal error: matching for bit vector ops on this match should be impossible"
             ),
             UnaryOp::InferSpecForLoopIter { .. } => {
diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs
@@ -244,7 +244,6 @@ pub const QID_OPAQUE_TYPE_BOUND: &str = "opaque_type_bound";
 
 pub const VERUS_SPEC: &str = "VERUS_SPEC__";
 
-pub const STRSLICE_IS_ASCII: &str = "str%strslice_is_ascii";
 pub const STRSLICE_LEN: &str = "str%strslice_len";
 pub const STRSLICE_GET_CHAR: &str = "str%strslice_get_char";
 pub const STRSLICE_NEW_STRLIT: &str = "str%new_strlit";
diff --git a/source/vir/src/heuristics.rs b/source/vir/src/heuristics.rs
@@ -57,7 +57,7 @@ fn insert_auto_ext_equal(ctx: &Ctx, exp: &Exp) -> Exp {
             UnaryOp::RealToInt => exp.clone(),
             UnaryOp::FloatToBits => exp.clone(),
             UnaryOp::IeeeFloat(_) => exp.clone(),
-            UnaryOp::StrLen | UnaryOp::StrIsAscii | UnaryOp::Length(_) => exp.clone(),
+            UnaryOp::StrLen | UnaryOp::Length(_) => exp.clone(),
             UnaryOp::InferSpecForLoopIter { .. } => exp.clone(),
             UnaryOp::Trigger(_)
             | UnaryOp::CoerceMode { .. }
diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs
@@ -1179,7 +1179,6 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                         | CoerceMode { .. }
                         | StrLen
                         | Length(..)
-                        | StrIsAscii
                         | MutRefCurrent
                         | MutRefFuture(_)
                         | MutRefFinal(_)
@@ -1300,7 +1299,6 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                         | CoerceMode { .. }
                         | StrLen
                         | Length(..)
-                        | StrIsAscii
                         | MutRefCurrent
                         | MutRefFuture(_)
                         | MutRefFinal(_)
diff --git a/source/vir/src/poly.rs b/source/vir/src/poly.rs
@@ -569,8 +569,7 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp {
                 | UnaryOp::FloatToBits
                 | UnaryOp::IeeeFloat(..)
                 | UnaryOp::BitNot(_)
-                | UnaryOp::StrLen
-                | UnaryOp::StrIsAscii => {
+                | UnaryOp::StrLen => {
                     let e1 = coerce_exp_to_native(ctx, &e1);
                     mk_exp(ExpX::Unary(*op, e1))
                 }
diff --git a/source/vir/src/prelude.rs b/source/vir/src/prelude.rs
@@ -1119,14 +1119,12 @@ pub(crate) fn array_functions(box_array: &str) -> Vec<Node> {
 
 pub(crate) fn strslice_functions(strslice_name: &str) -> Vec<Node> {
     let strslice = str_to_node(strslice_name);
-    let strslice_is_ascii = str_to_node(STRSLICE_IS_ASCII);
     let strslice_len = str_to_node(STRSLICE_LEN);
     let strslice_get_char = str_to_node(STRSLICE_GET_CHAR);
     let new_strlit = str_to_node(STRSLICE_NEW_STRLIT);
     let from_strlit = str_to_node(STRSLICE_FROM_STRLIT);
     nodes_vec!(
         // Strings
-        (declare-fun [strslice_is_ascii] ([strslice]) Bool)
         (declare-fun [strslice_len] ([strslice]) Int)
         (declare-fun [strslice_get_char] ([strslice] Int) Int)
         (declare-fun [new_strlit] (Int) [strslice])
diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs
@@ -13,14 +13,13 @@ use crate::context::Ctx;
 use crate::def::{
     ARCH_SIZE, CommandsWithContext, CommandsWithContextX, FUEL_BOOL, FUEL_BOOL_DEFAULT,
     FUEL_DEFAULTS, FUEL_ID, FUEL_PARAM, FUEL_TYPE, I_HI, I_LO, POLY, ProverChoice, SNAPSHOT_CALL,
-    SNAPSHOT_LOOP, SNAPSHOT_PRE, STRSLICE_GET_CHAR, STRSLICE_IS_ASCII, STRSLICE_LEN,
-    STRSLICE_NEW_STRLIT, SUCC, SUFFIX_SNAP_JOIN, SUFFIX_SNAP_MUT, SUFFIX_SNAP_WHILE_BEGIN,
-    SUFFIX_SNAP_WHILE_END, SnapPos, SpanKind, Spanned, U_HI, encode_dt_as_path, fun_to_string,
-    is_variant_ident, new_internal_qid, new_user_qid_name, path_to_string, prefix_box,
-    prefix_ensures, prefix_fuel_id, prefix_no_unwind_when, prefix_open_inv, prefix_pre_var,
-    prefix_requires, prefix_spec_fn_type, prefix_unbox, snapshot_ident, static_name,
-    suffix_global_id, suffix_local_unique_id, suffix_typ_param_ids, variant_field_ident,
-    variant_field_ident_internal, variant_ident,
+    SNAPSHOT_LOOP, SNAPSHOT_PRE, STRSLICE_GET_CHAR, STRSLICE_LEN, STRSLICE_NEW_STRLIT, SUCC,
+    SUFFIX_SNAP_JOIN, SUFFIX_SNAP_MUT, SUFFIX_SNAP_WHILE_BEGIN, SUFFIX_SNAP_WHILE_END, SnapPos,
+    SpanKind, Spanned, U_HI, encode_dt_as_path, fun_to_string, is_variant_ident, new_internal_qid,
+    new_user_qid_name, path_to_string, prefix_box, prefix_ensures, prefix_fuel_id,
+    prefix_no_unwind_when, prefix_open_inv, prefix_pre_var, prefix_requires, prefix_spec_fn_type,
+    prefix_unbox, snapshot_ident, static_name, suffix_global_id, suffix_local_unique_id,
+    suffix_typ_param_ids, variant_field_ident, variant_field_ident_internal, variant_ident,
 };
 use crate::messages::{Span, error, error_with_label};
 use crate::poly::{MonoTyp, MonoTypX, MonoTyps, typ_as_mono, typ_is_poly};
@@ -1021,10 +1020,6 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result<
                 str_ident(STRSLICE_LEN),
                 Arc::new(vec![exp_to_expr(ctx, e, expr_ctxt)?]),
             )),
-            UnaryOp::StrIsAscii => Arc::new(ExprX::Apply(
-                str_ident(STRSLICE_IS_ASCII),
-                Arc::new(vec![exp_to_expr(ctx, e, expr_ctxt)?]),
-            )),
             UnaryOp::Not => mk_not(&exp_to_expr(ctx, e, expr_ctxt)?),
             UnaryOp::BitNot(width_opt) => {
                 let expr = exp_to_expr(ctx, e, expr_ctxt)?;
@@ -2939,11 +2934,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result<Vec<Stmt>, Vi
         }
         StmX::RevealString(lit) => {
             let exprs = Arc::new({
-                vec![
-                    string_is_ascii_to_air(ctx, lit.clone()),
-                    string_len_to_air(ctx, lit.clone()),
-                    string_indices_to_air(ctx, lit.clone()),
-                ]
+                vec![string_len_to_air(ctx, lit.clone()), string_indices_to_air(ctx, lit.clone())]
             });
             let exprx = Arc::new(ExprX::Multi(MultiOp::And, exprs));
             let stmt = Arc::new(StmtX::Assume(exprx));
@@ -3010,14 +3001,6 @@ fn string_indices_to_air(ctx: &Ctx, lit: Arc<String>) -> Expr {
     exprx
 }
 
-fn string_is_ascii_to_air(ctx: &Ctx, lit: Arc<String>) -> Expr {
-    let is_ascii = lit.is_ascii();
-    let cnst = str_to_const_str(ctx, lit);
-    let lhs = str_apply(&str_ident(STRSLICE_IS_ASCII), &vec![cnst]);
-    let is_ascii = Arc::new(ExprX::Const(Constant::Bool(is_ascii)));
-    Arc::new(ExprX::Binary(air::ast::BinaryOp::Eq, lhs, is_ascii))
-}
-
 fn set_fuel(ctx: &Ctx, local: &mut Vec<Decl>, hidden: &Vec<Fun>) {
     let fuel_expr = if hidden.len() == 0 {
         str_var(&FUEL_DEFAULTS)
diff --git a/source/vir/src/sst_util.rs b/source/vir/src/sst_util.rs
@@ -463,9 +463,6 @@ impl ExpX {
                     (format!("height_trigger({})", exp.x.to_user_string(global)), 99)
                 }
                 UnaryOp::StrLen => (format!("{}.len()", exp.x.to_string_prec(global, 99)), 90),
-                UnaryOp::StrIsAscii => {
-                    (format!("{}.is_ascii()", exp.x.to_string_prec(global, 99)), 90)
-                }
                 UnaryOp::Trigger(..)
                 | UnaryOp::CoerceMode { .. }
                 | UnaryOp::MustBeFinalized
diff --git a/source/vir/src/triggers.rs b/source/vir/src/triggers.rs
@@ -127,7 +127,6 @@ fn check_trigger_expr_arg(state: &mut State, arg: &Exp) {
             | UnaryOp::IeeeFloat(_)
             | UnaryOp::BitNot(_)
             | UnaryOp::StrLen
-            | UnaryOp::StrIsAscii
             | UnaryOp::CastToInteger
             | UnaryOp::MutRefCurrent
             | UnaryOp::MutRefFuture(_)
@@ -262,7 +261,6 @@ fn check_trigger_expr(
             }
             ExpX::Unary(op, arg) => match op {
                 UnaryOp::StrLen
-                | UnaryOp::StrIsAscii
                 | UnaryOp::BitNot(_)
                 | UnaryOp::MutRefCurrent
                 | UnaryOp::MutRefFuture(_)
diff --git a/source/vir/src/triggers_auto.rs b/source/vir/src/triggers_auto.rs
@@ -416,7 +416,7 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter
                 UnaryOp::FloatToBits => 1,
                 UnaryOp::IeeeFloat(_) => 1,
                 UnaryOp::InferSpecForLoopIter { .. } => 1,
-                UnaryOp::StrIsAscii | UnaryOp::StrLen => fail_on_strop(),
+                UnaryOp::StrLen => fail_on_strop(),
                 UnaryOp::MutRefFinal(_) => 1,
                 UnaryOp::MutRefCurrent | UnaryOp::MutRefFuture(_) => unreachable!(),
             };
diff --git a/source/vstd/endian.rs b/source/vstd/endian.rs
@@ -909,8 +909,12 @@ impl<B: Base> EndianNat<B> {
                     EndianNat::<BIG>::to_nat_append_least(big_rest, big_least);
                 }
                 assert(big_least.to_nat() == least.to_nat()) by {
-                    assert(big_least.least() == least.to_nat());
-                    reveal_with_fuel(EndianNat::to_nat, 2);
+                    assert(big_least.drop_least().to_nat() * BIG::base() + big_least.least()
+                        == least.to_nat()) by (nonlinear_arith)
+                        requires
+                            big_least.least() == least.to_nat(),
+                            big_least.drop_least().to_nat() == 0,
+                    ;
                 }
                 assert(n.to_nat() == (rest.to_nat() * base_upper_bound_excl::<B>(Self::exp()))
                     + least.to_nat()) by {
diff --git a/source/vstd/prelude.rs b/source/vstd/prelude.rs
@@ -65,10 +65,11 @@ pub use super::std_specs::maybe_uninit::MaybeUninitAdditionalSpecFns;
 #[cfg(feature = "alloc")]
 pub use super::pervasive::VecAdditionalExecFns;
 
+#[cfg(not(verus_verify_core))]
 pub use super::string::StrSliceExecFns;
-#[cfg(feature = "alloc")]
+#[cfg(all(feature = "alloc", not(verus_verify_core)))]
 pub use super::string::StringExecFns;
-#[cfg(feature = "alloc")]
+#[cfg(all(feature = "alloc", not(verus_verify_core)))]
 pub use super::string::StringExecFnsIsAscii;
 
 #[cfg(verus_keep_ghost)]
diff --git a/source/vstd/string.rs b/source/vstd/string.rs
diff --git a/source/vstd/utf8.rs b/source/vstd/utf8.rs
diff --git a/source/vstd/vstd.rs b/source/vstd/vstd.rs

Original file line number	Diff line number	Diff line change
`@@ -430,7 +430,7 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<BvExpr, Vir`
`430`	`430`	`UnaryOp::MustBeFinalized \| UnaryOp::MustBeElaborated => {`
`431`	`431`	`panic!("internal error: Exp not finalized: {:?}", arg)`
`432`	`432`	`}`
`433`		`- UnaryOp::StrLen \| UnaryOp::StrIsAscii => panic!(`
	`433`	`+ UnaryOp::StrLen => panic!(`
`434`	`434`	`"internal error: matching for bit vector ops on this match should be impossible"`
`435`	`435`	`),`
`436`	`436`	`UnaryOp::InferSpecForLoopIter { .. } => {`