Verify bounded LSH index invariants (7.2.8)

[leynos]

Summary

This branch adds the pre-implementation ExecPlan for roadmap task (7.2.8), which will use Kani to verify bounded LshIndex invariants for no self-pairs, canonical pair ordering, repeated-band deduplication, and insertion-order independence.

The pull request is intentionally draft-only planning work. It does not implement the Kani harnesses or mark the roadmap item complete; future implementation work should begin only after the ExecPlan is approved.

Roadmap task: (7.2.8)
ExecPlan: docs/execplans/7-2-8-kani-verification-of-bounded-lsh-index-invariants.md

Review walkthrough

• Start with docs/execplans/7-2-8-kani-verification-of-bounded-lsh-index-invariants.md to review the proposed scope, approval gate, Kani harness strategy, validation commands, and documentation obligations.

Validation

• markdownlint docs/execplans/7-2-8-kani-verification-of-bounded-lsh-index-invariants.md: passed
• make markdownlint: passed
• make nixie: passed
• make check-fmt: passed
• make lint: passed
• make test: passed, 1429 tests passed and 2 skipped
• coderabbit review --agent: completed with 0 findings

Notes

make fmt was attempted for the documentation change, but mdformat-all modified existing unrelated Markdown files before failing. Those formatter side effects were reverted; the plan file itself passes direct Markdown linting and the repo-wide Markdown and diagram gates pass.

References

• Lody session: https://lody.ai/leynos/sessions/f726e04f-c7e3-4930-9737-459a534bbe74

Summary by Sourcery

Documentation:

• Add a pre-implementation ExecPlan outlining scope, constraints, risks, and acceptance criteria for Kani verification of bounded LshIndex candidate-pair invariants.

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 4b06806b-125e-4e15-acde-7af37c3947ab

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch 7-2-8-kani-verification-of-bounded-lsh-index-invariants

---

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[sourcery-ai]

Reviewer's Guide

Adds a new pre-implementation ExecPlan document defining scope, constraints, risks, and step-by-step plan for using Kani to verify bounded LshIndex invariants, without modifying any production code.

File-Level Changes

Change	Details	Files
Add a detailed ExecPlan for roadmap item 7.2.8 to guide future Kani verification work on bounded LshIndex invariants.	Introduce a living ExecPlan document describing purpose, context, and acceptance criteria for Kani-based verification of LshIndex invariants (no self-pairs, canonical ordering, deduplication, insertion-order independence). Define explicit constraints, tolerances, risks, and decision log to bound the future implementation scope and preserve existing public APIs and domain boundaries. Lay out staged implementation plan, concrete validation commands, and documentation updates required before marking roadmap item 7.2.8 complete.	docs/execplans/7-2-8-kani-verification-of-bounded-lsh-index-invariants.md

---

Tips and commands

Interacting with Sourcery

• Trigger a new review: Comment @sourcery-ai review on the pull request.
• Continue discussions: Reply directly to Sourcery's review comments.
• Generate a GitHub issue from a review comment: Ask Sourcery to create an
  issue from a review comment by replying to it. You can also reply to a
  review comment with @sourcery-ai issue to create an issue from it.
• Generate a pull request title: Write @sourcery-ai anywhere in the pull
  request title to generate a title at any time. You can also comment
  @sourcery-ai title on the pull request to (re-)generate the title at any time.
• Generate a pull request summary: Write @sourcery-ai summary anywhere in
  the pull request body to generate a PR summary at any time exactly where you
  want it. You can also comment @sourcery-ai summary on the pull request to
  (re-)generate the summary at any time.
• Generate reviewer's guide: Comment @sourcery-ai guide on the pull
  request to (re-)generate the reviewer's guide at any time.
• Resolve all Sourcery comments: Comment @sourcery-ai resolve on the
  pull request to resolve all Sourcery comments. Useful if you've already
  addressed all the comments and don't want to see them anymore.
• Dismiss all Sourcery reviews: Comment @sourcery-ai dismiss on the pull
  request to dismiss all existing Sourcery reviews. Especially useful if you
  want to start fresh with a new review - don't forget to comment
  @sourcery-ai review to trigger a new review!

Customizing Your Experience

Access your dashboard to:

• Enable or disable review features such as the Sourcery-generated pull request
  summary, the reviewer's guide, and others.
• Change the review language.
• Add, remove or edit custom review instructions.
• Adjust other review settings.

Getting Help

• Contact our support team for questions or feedback.
• Visit our documentation for detailed guides and information.
• Keep in touch with the Sourcery team by following us on X/Twitter, LinkedIn or GitHub.