Skip analysis of extern_spec target only when trusted or ignored

Stopping the extern_spec_fn target from re-registering its own key (by
removing it from the refine set) also dropped its `refine_fn_def`, which
is where a trusted/ignored target is added to `skip_analysis`. Inserting
every local target into `skip_analysis` instead sent the extern spec down
the NoAnalyze branch of `refine_fn_def` for all targets, so a non-trusted
target's body was never checked against the spec: a `#[context]` trait
method's `ensures` (e.g. tests/ui/fail/trait_assoc_type_spec.rs) became a
trusted assumption and the program verified even though the body cannot
establish it.

Only insert the target into `skip_analysis` when it is itself trusted or
ignored (e.g. a `#[thrust::trusted]` `rand` whose `unimplemented!()` body
must not be analyzed). Non-trusted targets stay out of `skip_analysis`, so
the extern spec is registered in Analyze mode and their bodies are checked
against the spec.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VowL2RdawM4Xch4tsdbSf3

Author: claude

src/analyze/crate_.rs

@@ -70,7 +70,26 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             if analyzer.is_annotated_as_extern_spec_fn() {
                 let target_def_id = analyzer.extern_spec_fn_target_def_id();
                 if let Some(local_target_def_id) = target_def_id.as_local() {
-                    self.skip_analysis.insert(local_target_def_id);
+                    // Drop the plain target from the refine loop so it does not re-register the
+                    // key this extern spec owns. The target's own `refine_fn_def` would have
+                    // added it to `skip_analysis` only when it is trusted/ignored; replicate that
+                    // decision here. Otherwise the extern spec is registered in NoAnalyze mode for
+                    // every local target, and a non-trusted target's body (e.g. a `#[context]`
+                    // trait method) would never be checked against the spec.
+                    let target = local_target_def_id.to_def_id();
+                    let is_trusted_or_ignored = self
+                        .tcx
+                        .get_attrs_by_path(target, &analyze::annot::trusted_path())
+                        .next()
+                        .is_some()
+                        || self
+                            .tcx
+                            .get_attrs_by_path(target, &analyze::annot::ignored_path())
+                            .next()
+                            .is_some();
+                    if is_trusted_or_ignored {
+                        self.skip_analysis.insert(local_target_def_id);
+                    }
                     keys.swap_remove(&local_target_def_id);
                 }
                 if matches!(