[High] Prove the pure arithmetic and parsing helpers with Kani

[james2177]

Description:
Use the Kani model checker to prove properties of the pure (non-Env) helpers: compute_slash_amount (never exceeds the bond, never negative), tier_fill_window (monotonic, no overflow), fee math (fee ≤ amount, rounding direction), Dutch-decay math, tier lookup monotonicity, and the proof registry's payload byte decoding.

Problem Statement & Context:
Proptests sample the input space, while Kani proves the property for all inputs. Arithmetic helpers are small enough to verify fully, and their bugs directly move funds.

Scope & Acceptance Criteria:

• Pull the helpers into Env-free functions (a pure math module) if they aren't already.
• At least 10 Kani harnesses with #[kani::proof], each with a documented property.
• A make kani target, and harnesses that finish in under 10 minutes in total.
• Out of scope: proving Env-dependent code.

Implementation Guidelines:

1. Key Files/Modules: intent_settlement/src/math.rs, solver_registry/src/lib.rs (score_of, tier), proof_registry/src/lib.rs (the decode helpers), Makefile.
2. Design/Architecture: Keep soroban-sdk types out of the proven functions and use primitive types.
3. Edge Cases/Constraints: i128 multiplication overflow, where Kani needs unwind bounds for the loops.
4. Testing: The Kani harnesses themselves, plus unit tests.

Definition of "Done":

• Kani passes locally with the output in the PR, and the Makefile target is added.
• Reviewed and approved.

Resources:

• Kani: https://model-checking.github.io/kani/

Complexity: High (200 points)

[Olufamous]

@Olufamous has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

I would like to work on this issue because i fully understand the implementation and i can assure you of a perfect outcome, kindly assign me

ℹ️ Repo Maintainers: To accept this application, review their application or assign @Olufamous to this issue.

[Joeljosef7]

@Joeljosef7 has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

I can take this on. I’ll isolate the arithmetic and decoding logic into Env-free helpers where needed, then add Kani harnesses covering the required bounds, monotonicity, overflow, rounding, and parsing properties. I’ll also add the "make kani" target and keep the proofs within the required runtime.

ℹ️ Repo Maintainers: To accept this application, review their application or assign @Joeljosef7 to this issue.

[Chulexino]

@Chulexino has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

Hey team stellar-vortex-protocol, I've reviewed the issue and traced through the related code paths to understand the root cause. I'm ready to implement a fix and would appreciate being assigned to this.

ℹ️ Repo Maintainers: To accept this application, review their application or assign @Chulexino to this issue.

[shemaiahdelia03-cmd]

@shemaiahdelia03-cmd has applied to work on this issue as part of the Stellar Wave Program's 9th wave.

i would love to work on this issue please

ℹ️ Repo Maintainers: To accept this application, review their application or assign @shemaiahdelia03-cmd to this issue.

[drips-wave]

Congratulations, @shemaiahdelia03-cmd! 🎉 Your application was accepted by the repo's maintainers, and the issue is due on September 30, 2026.

🧑‍💻 @shemaiahdelia03-cmd: Please resolve the issue such that the repo's maintainers have enough time to review your contribution before the due date. You'll earn Points for completing the issue on-time, which will make you eligible for a share of the Stellar Wave Program's reward pool.

Warning

When opening a PR, please link it to this issue to ensure it gets tracked accurately. Points are awarded when this issue is marked as completed by the maintainer.

🤠 Repo maintainers: Please keep an eye on the contributor's progress and review their work before the due date. You can manage this issue, including adjusting its complexity and points, here.

🌊 Happy Wave 🌊