[kani] Use function contracts instead of proofs

[joshlf]

---

This PR is on branch ptr-kani.

• [kani] Prove some PtrInner methods #2444
• [kani] Use function contracts instead of proofs #2449

[codecov-commenter]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 90.43%. Comparing base (d769fb9) to head (f375ace).
Report is 1 commits behind head on main.

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #2449      +/-   ##
==========================================
+ Coverage   90.42%   90.43%   +0.01%     
==========================================
  Files          18       18              
  Lines        7319     7331      +12     
==========================================
+ Hits         6618     6630      +12     
  Misses        701      701              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.