Implement Structural for Result<T, E>

Option<T> was already marked Structural (added incidentally in #1695),
but Result<T, E>, the other pervasive std type raised in #178, was not.
This meant generic code with a `T: Structural` bound (needed to connect
exec-mode == to spec-mode ==) could not be instantiated with Result,
even though Result's PartialEq is already fieldwise/structural.

Fix: add `unsafe impl<T: Structural, E: Structural> Structural for
core::result::Result<T, E> {}` in builtin/src/lib.rs, mirroring the
existing Option impl. Result is a core (not alloc/std) type, so this
needs no extra dependency and sidesteps the no_std/orphan-rule concern
raised in the issue for alloc-backed types like Vec/String.

Verified:
- vstd still verifies fully (2044/0) after the change
- New regression test in rust_verify_test/tests/structural.rs fails
  without the fix (E0277: Result<u32,u32> does not implement
  Structural) and passes with it
- 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 test suites all pass with no
  regressions

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

Author: Marti2203

source/builtin/src/lib.rs

@@ -856,6 +856,8 @@ impl_structural! {
 
 unsafe impl<T: Structural> Structural for Option<T> {}
 
+unsafe impl<T: Structural, E: Structural> Structural for core::result::Result<T, E> {}
+
 pub struct NoCopy {}
 #[cfg(verus_keep_ghost)]
 impl !Copy for NoCopy {}

source/rust_verify_test/tests/structural.rs

@@ -80,6 +80,24 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    // https://github.com/verus-lang/verus/issues/178
+    #[test] test_result_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_result(a: Result<u32, u32>, b: Result<u32, u32>) {
+            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::*;