Potentially Fix Pipeline (Kani issues)

[wallstop]

Description

Type of Change

• 🐛 Bug fix (non-breaking change that fixes an issue)
• ✨ New feature (non-breaking change that adds functionality)
• 💥 Breaking change (fix or feature that would cause existing functionality to change)
• 📚 Documentation (changes to documentation only)
• ♻️ Refactor (code change that neither fixes a bug nor adds a feature)
• 🧪 Test (adding or updating tests)
• 🔧 CI/Build (changes to CI configuration or build process)

Checklist

Required

• I have read the CONTRIBUTING guide
• I have followed the zero-panic policy:
  • No unwrap() in production code
  • No expect() in production code
  • No panic!() or todo!()
  • All fallible operations return Result
• I have added tests that prove my fix is effective or my feature works
• I have run cargo fmt && cargo clippy --all-targets with no warnings
• I have run cargo nextest run and all tests pass

If Applicable

• I have updated the documentation accordingly
• I have added an entry to CHANGELOG.md for user-facing changes
• I have updated relevant examples in the examples/ directory
• My changes generate no new compiler warnings

Testing

Tests added/modified:

• (None)

Manual testing performed:

• (None)

Related Issues

---

[github-actions]

📝 Changelog Reminder

This PR does not appear to update CHANGELOG.md.

If this PR includes user-facing changes, please consider adding an entry to the changelog under the appropriate section:

• Added - New features
• Changed - Changes in existing functionality
• Deprecated - Soon-to-be removed features
• Removed - Removed features
• Fixed - Bug fixes
• Security - Vulnerability fixes

You can skip this reminder by adding one of these labels: skip-changelog, dependencies, chore, ci, internal

When is a changelog entry needed?

A changelog entry is typically needed for:

• New public API methods or types
• Bug fixes that affect users
• Performance improvements
• Breaking changes
• New features or configuration options

A changelog entry is typically NOT needed for:

• Internal refactoring with no API changes
• CI/tooling improvements
• Documentation fixes (unless significant)
• Test additions/fixes

---

This is an automated reminder. The PR will not be blocked by this check.

[Copilot]

Pull request overview

This PR aims to make the Kani verification pipeline more reliable in CI by reducing proof state-space, adding explicit unwind bounds, and improving Kani tooling feedback so timeouts/unwind-related failures are easier to diagnose.

Changes:

• Tighten/adjust several Kani proofs (smaller symbolic ranges, smaller constructed structures) and add explicit #[kani::unwind(N)] in a few places.
• Add per-proof timeout handling and extra “quick mode default unwind” guidance to verify-kani.sh.
• Add an advisory scan for proofs missing #[kani::unwind(N)] in both the shell and Python Kani coverage checkers; update Kani guidance docs accordingly.

Reviewed changes

Copilot reviewed 12 out of 13 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
src/time_sync.rs	Narrows proof input ranges and adds explicit unwind bounds to improve Kani tractability/CI stability.
src/sync_layer/mod.rs	Reduces proof construction complexity (1 player/window) and lowers unwind to target the invariant being proven.
src/input_queue/mod.rs	Makes non-sequential proof deterministic (concrete skip) and increases unwind to match proof operations.
scripts/verify-kani.sh	Wraps Kani invocations with a timeout and prints clearer guidance for quick-mode unwind failures.
scripts/check-kani-coverage.sh	Adds an advisory check for missing #[kani::unwind(N)] attributes in proofs.
scripts/check-kani-coverage.py	Adds cross-platform advisory detection for proofs missing #[kani::unwind(N)] (with optional verbosity).
loom-tests/tests/loom_saved_states.rs	Cleans up imports (no behavior change).
CLAUDE.md	Replaces long instructions with concise reminders pointing to .llm/context.md.
AGENTS.md	Same as above: slimmed instructions, points to .llm/context.md.
.llm/skills/kani-verification.md	Documents CI --quick / default unwind behavior and adds guidance/allowlist marker.
.llm/context.md	Clarifies CI failure conditions and reiterates Kani unwind implications in quick mode.
.github/copilot-instructions.md	Slimmed instructions to defer to .llm/context.md.

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Fortress Rollback Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.50.

Benchmark suite	Current: 60bd197	Previous: 55d1aef	Ratio
Frame arithmetic/add/1	1 ns/iter (± 0)	0 ns/iter (± 0)	+∞
Frame arithmetic/add/10	1 ns/iter (± 0)	0 ns/iter (± 0)	+∞
Frame arithmetic/add/100	1 ns/iter (± 0)	0 ns/iter (± 0)	+∞
Frame arithmetic/add/1000	1 ns/iter (± 0)	0 ns/iter (± 0)	+∞

This comment was automatically generated by workflow using github-action-benchmark.

[Copilot]

Pull request overview

Copilot reviewed 40 out of 126 changed files in this pull request and generated 6 comments.

---

You can also share your feedback on Copilot code review. Take the survey.

[Copilot]

Pull request overview

Copilot reviewed 41 out of 129 changed files in this pull request and generated 3 comments.

---

You can also share your feedback on Copilot code review. Take the survey.

[Copilot]

Pull request overview

Copilot reviewed 42 out of 132 changed files in this pull request and generated 4 comments.

---

You can also share your feedback on Copilot code review. Take the survey.

[Copilot]

Pull request overview

Copilot reviewed 42 out of 132 changed files in this pull request and generated 1 comment.

---

You can also share your feedback on Copilot code review. Take the survey.