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

@@ -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() {

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!