From 8a817b081ae162cbabf3a9044e609da0291466b5 Mon Sep 17 00:00:00 2001
From: Ziqiao Zhou <ziqiaozhou@microsoft.com>
Date: Mon, 27 Jan 2025 18:11:16 -0800
Subject: [PATCH 1/2] Support slice::get && Ignore trait predicates when not
 visible to local.

* Why: trait SliceIndex<T: ?Sized>: private_slice_index::Sealed
* Add spec for slice::get
---
 source/rust_verify/src/rust_to_vir_func.rs | 17 ++++++++++++-
 source/vstd/slice.rs                       | 28 ++++++++++++++++++++++
 2 files changed, 44 insertions(+), 1 deletion(-)

diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs
index ec41f13259..727f0b5a4f 100644
--- a/source/rust_verify/src/rust_to_vir_func.rs
+++ b/source/rust_verify/src/rust_to_vir_func.rs
@@ -1389,7 +1389,22 @@ pub(crate) fn remove_ignored_trait_bounds_from_predicates<'tcx>(
     use rustc_middle::ty::{ConstKind, ScalarInt, ValTree};
     preds.retain(|p: &Clause<'tcx>| match p.kind().skip_binder() {
         rustc_middle::ty::ClauseKind::<'tcx>::Trait(tp) => {
-            if in_trait && trait_ids.contains(&tp.trait_ref.def_id) && tp.trait_ref.args.len() >= 1
+            let td = tcx.trait_def(tp.trait_ref.def_id);
+            // Recursively check parent path visibility
+            let mut visible = tcx.visibility(td.def_id).is_visible_locally();
+            let mut def_id = td.def_id;
+            while let Some(parent_def_id) = tcx.opt_parent(def_id) {
+                if !tcx.visibility(parent_def_id).is_visible_locally() {
+                    visible = false;
+                    break;
+                }
+                def_id = parent_def_id;
+            }
+            if !visible {
+                false
+            } else if in_trait
+                && trait_ids.contains(&tp.trait_ref.def_id)
+                && tp.trait_ref.args.len() >= 1
             {
                 if let GenericArgKind::Type(ty) = tp.trait_ref.args[0].unpack() {
                     match ty.kind() {
diff --git a/source/vstd/slice.rs b/source/vstd/slice.rs
index 15384444b9..2955c710ed 100644
--- a/source/vstd/slice.rs
+++ b/source/vstd/slice.rs
@@ -103,8 +103,36 @@ pub exec fn slice_subrange<T, 'a>(slice: &'a [T], i: usize, j: usize) -> (out: &
     &slice[i..j]
 }
 
+#[verifier::external_trait_specification]
+pub trait ExSliceIndex<T> where T: ?Sized {
+    type ExternalTraitSpecificationFor: core::slice::SliceIndex<T>;
+
+    type Output: ?Sized;
+}
+
+pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
+    &<I as core::slice::SliceIndex<[T]>>::Output,
+>) where I: core::slice::SliceIndex<[T]>
+    returns
+        spec_slice_get(slice, i),
+;
+
+pub open spec fn spec_slice_get<T: ?Sized, I: core::slice::SliceIndex<T>>(
+    val: &T,
+    idx: I,
+) -> Option<&<I as core::slice::SliceIndex<T>>::Output>;
+
+pub broadcast proof fn axiom_slice_get_usize<T>(v: &[T], i: usize)
+    ensures
+        i < v.len() ==> #[trigger] spec_slice_get(v, i) === Some(&v[i as int]),
+        i >= v.len() ==> spec_slice_get(v, i).is_none(),
+{
+    admit();
+}
+
 pub broadcast group group_slice_axioms {
     axiom_spec_len,
+    axiom_slice_get_usize,
 }
 
 } // verus!

From fe6ae59c6bbb646d4230f0dd4cb3439927400e6d Mon Sep 17 00:00:00 2001
From: Ziqiao Zhou <ziqiaozhou@microsoft.com>
Date: Thu, 6 Feb 2025 17:05:27 -0800
Subject: [PATCH 2/2] skip trait bound check if path ==
 core::slice::index::private_slice_index::Sealed

---
 source/rust_verify/src/rust_to_vir_func.rs | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs
index 727f0b5a4f..c23f5dc677 100644
--- a/source/rust_verify/src/rust_to_vir_func.rs
+++ b/source/rust_verify/src/rust_to_vir_func.rs
@@ -1389,18 +1389,9 @@ pub(crate) fn remove_ignored_trait_bounds_from_predicates<'tcx>(
     use rustc_middle::ty::{ConstKind, ScalarInt, ValTree};
     preds.retain(|p: &Clause<'tcx>| match p.kind().skip_binder() {
         rustc_middle::ty::ClauseKind::<'tcx>::Trait(tp) => {
-            let td = tcx.trait_def(tp.trait_ref.def_id);
-            // Recursively check parent path visibility
-            let mut visible = tcx.visibility(td.def_id).is_visible_locally();
-            let mut def_id = td.def_id;
-            while let Some(parent_def_id) = tcx.opt_parent(def_id) {
-                if !tcx.visibility(parent_def_id).is_visible_locally() {
-                    visible = false;
-                    break;
-                }
-                def_id = parent_def_id;
-            }
-            if !visible {
+            // Skip private trait bounds
+            let path = tcx.def_path_str(tp.trait_ref.def_id);
+            if path == "core::slice::index::private_slice_index::Sealed" {
                 false
             } else if in_trait
                 && trait_ids.contains(&tp.trait_ref.def_id)