formal-verification scoping placeholder

[nayt9]

This PR introduces a formal verification scoping document for commitment_core and resolves pre-existing contract/test inconsistencies to ensure the codebase builds and tests cleanly.

---

Formal Verification Scope

• Added: COMMITMENT_CORE_FORMAL_VERIFICATION_SCOPE.md

This document defines:

• Proof boundary

  • Clearly scoped contract surface for verification

• Trusted assumptions

  • External conditions and invariants assumed to hold

• First-pass safety goals

  • Core correctness and safety properties to be proven

• Prioritized lemma set, covering:

  • Authorization correctness
  • Reentrancy safety
  • Arithmetic safety (overflow/underflow)
  • Lifecycle correctness
  • Conservation properties (value/fee integrity)

• Targeted functions:

  • create_commitment
  • settle
  • early_exit
  • allocate
  • withdraw_fees

---

Integration

• Linked the formal verification scope from lib.rs
• Extended SECURITY_CHECKLIST.md:
  • Ensures the verification scope remains tied to ongoing contract review
  • Provides visibility for auditors and contributors

---

Fixes & Cleanup

While validating the scope against the live code, this PR also:

• Fixed contract/test drift across:

  • lib.rs
  • fee_tests.rs
  • tests.rs
  • test_zero_address.rs

• Resolved shared_utils re-export conflict in lib.rs

• Restored successful build and test execution

closes #293

[drips-wave]

@nayt9 Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits