When using lambda, we're seeing green checkmarks on timeout

[cos]

@claude, inspect

[claude]

Claude finished @cos's task in 17m 32s —— View job • claude/issue-546-20260306-1843 • Create PR ➔

---

Inspecting Issue: Green checkmarks on timeout with lambda

• Gather context
• Understand the request
• Inspect relevant code
• Identify root cause
• Implement fix
• Commit and push

Root Cause

Bug: When multiple Lambda invocations fail concurrently (timeout, connection error, etc.), all produce the exact same diagnostic: message: "cloud verification out of resources/timeout" with loc: Loc::default().

The duplicate diagnostic prevention in GlobalEnv::add_diag uses has_diag which checked ALL diagnostics in the diags Vec — including ones already marked as reported. This caused a subtle interleaving bug:

1. Task A (timeout) → adds { msg: "cloud verification...", loc: Loc::default() } → reported = false
2. Task A → has_errors() → true → report_diag() → marks reported = true
3. Task B (timeout) → tries to add the same diagnostic → has_diag() finds it (already in Vec, reported=true) → does NOT add it
4. Task B → has_errors() → false → shows ✅ green checkmark ← BUG

This is specific to lambda because:

• All Lambda-level HTTP failures use Loc::default() (no source location) → all produce identical diagnostics
• --cloud enables concurrent verification via buffer_unordered, making this interleaving likely

Fix (crates/move-model/src/model.rs)

Changed has_diag to only check unreported diagnostics:

// Before (buggy):
pub fn has_diag(&self, diag: &Diagnostic<FileId>) -> bool {
    self.diags.borrow().iter().any(|(d, _)| d == diag)
}

// After (fixed):
pub fn has_diag(&self, diag: &Diagnostic<FileId>) -> bool {
    self.diags
        .borrow()
        .iter()
        .any(|(d, reported)| !reported && d == diag)
}

Once a diagnostic is reported, it no longer blocks identical errors from subsequent verification tasks. The duplicate suppression still works within a single task's execution.