Implement Structural for tuples and fixed-size arrays

Same gap as Result<T,E>/Option<T> (issue #178): both are pervasive
core types with compiler-derived fieldwise/elementwise PartialEq, but
had no Structural impl, so a `T: Structural` generic bound couldn't be
instantiated with them.

- Tuples: mirrors core's own tuple_impls! (library/core/src/tuple.rs),
  which provides PartialEq up to arity 12.
- Arrays: [T; N] is represented differently in VIR (an SMT function,
  not a datatype) from tuples/structs, but Structural's soundness
  argument doesn't depend on that representation - Verus compiles
  exec == directly to the identical spec-level == for any type where
  rustc's own is_structural_eq_shallow query holds (see
  rust_to_vir_base.rs::is_smt_equality), which already covers arrays
  of Structural elements (the same query that allows array literals in
  match patterns). Confirmed via a real generic-bound regression test
  requiring no group_array_axioms broadcast.

Verified:
- vstd still verifies fully (2043/0) after the change
- New regression tests in rust_verify_test/tests/structural.rs
  (test_tuple_is_structural, test_array_is_structural)
- structural.rs, eq_cmp.rs, partial_eq.rs, operators.rs, option.rs,
  results.rs, adts.rs, impl.rs, marker_traits.rs, generics.rs,
  external_type_specification.rs, traits.rs, arrays.rs,
  mut_refs_slices_arrays.rs test suites all pass with no regressions

Assisted-by: Claude Code:claude-sonnet-5

Author: Marti2203

source/builtin/src/lib.rs

@@ -858,6 +858,28 @@ unsafe impl<T: Structural> Structural for Option<T> {}
 
 unsafe impl<T: Structural, E: Structural> Structural for core::result::Result<T, E> {}
 
+unsafe impl<T: Structural, const N: usize> Structural for [T; N] {}
+
+// Mirrors core's own tuple_impls! (library/core/src/tuple.rs), which provides
+// PartialEq for tuples up to arity 12.
+macro_rules! impl_structural_tuple {
+    ($($T:ident)*) => {
+        unsafe impl<$($T: Structural),*> Structural for ($($T,)*) {}
+    }
+}
+
+macro_rules! impl_structural_tuples {
+    () => {
+        impl_structural_tuple!();
+    };
+    ($T:ident $($U:ident)*) => {
+        impl_structural_tuple!($T $($U)*);
+        impl_structural_tuples!($($U)*);
+    };
+}
+
+impl_structural_tuples!(A B C D E F G H I J K L);
+
 pub struct NoCopy {}
 #[cfg(verus_keep_ghost)]
 impl !Copy for NoCopy {}

source/rust_verify_test/tests/structural.rs

@@ -98,6 +98,42 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    // https://github.com/verus-lang/verus/issues/178
+    #[test] test_tuple_is_structural verus_code! {
+        use vstd::prelude::*;
+
+        fn eq_generic<T: PartialEq + Structural>(a: &T, b: &T) -> (r: bool)
+            ensures r == (a == b),
+        {
+            a == b
+        }
+
+        fn test_tuple(a: (u32, bool), b: (u32, bool)) {
+            let r = eq_generic(&a, &b);
+            assert(r == (a == b));
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    // https://github.com/verus-lang/verus/issues/178
+    #[test] test_array_is_structural verus_code! {
+        use vstd::prelude::*;
+
+        fn eq_generic<T: PartialEq + Structural>(a: &T, b: &T) -> (r: bool)
+            ensures r == (a == b),
+        {
+            a == b
+        }
+
+        fn test_array(a: [u32; 3], b: [u32; 3]) {
+            let r = eq_generic(&a, &b);
+            assert(r == (a == b));
+        }
+    } => Ok(())
+}
+
 test_verify_one_file_with_options! {
     #[test] test_structural_trait_bound ["exec_allows_no_decreases_clause"] => verus_code! {
         use vstd::prelude::*;