ENG-162 add Kani invariant coverage#477
Conversation
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (2)
📝 WalkthroughSummary
Notable review areas
WalkthroughAdds Kani workflow wiring and proof harnesses for vault kernel and universal-account code, expands related tests, and updates Soroban vault CLI documentation with new governance and NAV prerequisites. ChangesKani Proofs, Vault Kernel Refactoring, and Test Coverage
Soroban Vault CLI Documentation Updates
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Suggested reviewers
🚥 Pre-merge checks | ✅ 2✅ Passed checks (2 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Warning Review ran into problems🔥 ProblemsErrors were encountered while retrieving linked issues. Errors (1)
Comment |
| } | ||
|
|
||
| #[test] | ||
| #[ignore = "ENG-162: enable after PayloadExecutionParameters stores and verifies immutable domain_id"] |
38ee973 to
2e257b9
Compare
|
@coderabbitai review |
✅ Action performedReview finished.
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Warning
CodeRabbit couldn't request changes on this pull request because it doesn't have sufficient GitHub permissions.
Please grant CodeRabbit Pull requests: Read and write permission and re-run the review.
Actionable comments posted: 4
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
tools/soroban-vault-cli/README.md (1)
161-179: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winAdd acceptance steps to make the setup sequence executable in timelocked governance.
At Line 161–Line 179, the flow submits proposals but never accepts them, so the “active supply route” setup can remain pending and non-operative. Add
governance accept-readysteps (or explicitly scope this block to zero-timelock environments).Suggested doc patch
tmplr-soroban-vault governance submit-set-allowed-adapters \ --admin GCURATOR_OR_MULTISIG... \ --adapters CBLENDADAPTER...,CCUSTODIALADAPTER... +tmplr-soroban-vault governance accept-ready --admin GCURATOR_OR_MULTISIG... --kind allowed-adapters tmplr-soroban-vault governance submit-set-cap \ --admin GCURATOR_OR_MULTISIG... \ --market-id 0 \ --cap 1000000000 tmplr-soroban-vault governance submit-set-cap \ --admin GCURATOR_OR_MULTISIG... \ --market-id 1 \ --cap 1000000000 +tmplr-soroban-vault governance accept-ready --admin GCURATOR_OR_MULTISIG... --kind cap tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR_OR_MULTISIG... \ --entry 0:CBLENDADAPTER... \ --entry 1:CCUSTODIALADAPTER... +tmplr-soroban-vault governance accept-ready --admin GCURATOR_OR_MULTISIG... --kind supply-queue🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tools/soroban-vault-cli/README.md` around lines 161 - 179, The governance setup flow in the README submits proposals for allowed adapters, caps, and the supply queue, but it never includes the acceptance step needed for timelocked governance. Update the sequence around the governance commands to add the corresponding governance accept-ready step after each submit, or clearly state that this block only applies when timelock is zero. Make sure the instructions reference the governance CLI flow shown in the README so the setup becomes executable end-to-end.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In @.github/workflows/kani.yml:
- Line 45: The Kani workflow still references the mutable
model-checking/kani-github-action@v1 tag in multiple jobs, so update every use
of that action to an immutable 40-character commit SHA. Replace the `@v1`
reference in the workflow steps that invoke the Kani action so each job is
pinned consistently, using the action identifier
model-checking/kani-github-action to locate all occurrences.
In `@contract/vault/kernel/src/actions/mod.rs`:
- Around line 112-128: `PayoutSettlement` and `EmergencyResetOutcome` currently
expose contradictory crate-visible state that `apply_payout_settlement` and
`handle_emergency_reset` must trust implicitly. Replace them with stronger
enums/variants so payout success vs failure are distinct and the refund data is
represented as a single optional payload, then update the consumers and any
Kani/test paths that inspect these results to match the new shape. Keep the
existing symbols easy to locate by refactoring around `PayoutSettlement` and
`EmergencyResetOutcome` in `actions::mod`.
In `@contract/vault/kernel/src/lib.rs`:
- Around line 211-216: The refund-owner proof check is only comparing the first
byte of the Address, so mutations in the remaining bytes can slip through.
Update assert_refund_owner_is_owner in kernel::lib to reuse assert_address_eq
for the Some(owner) case, matching the existing full-address proof pattern used
elsewhere. Also review the other affected proof assertions noted in the diff and
align them to full Address equality so the harness validates the entire
owner/receiver/refund address.
In `@contract/vault/kernel/tests/property_tests.rs`:
- Around line 1647-1712: The property test for AtomicRedeem only checks the
success path, so add an explicit reject-path assertion in
prop_atomic_redeem_respects_idle_cap. Use preview_withdraw_assets and the
existing apply_action call to branch on previewed_assets >
old_state.idle_assets, and assert result.is_err() in that case before validating
BurnShares and TransferAssets effects on the success branch. Mirror the
structure of prop_atomic_withdraw_respects_idle_cap so the test covers both the
failure and success behavior of KernelAction::AtomicRedeem.
---
Outside diff comments:
In `@tools/soroban-vault-cli/README.md`:
- Around line 161-179: The governance setup flow in the README submits proposals
for allowed adapters, caps, and the supply queue, but it never includes the
acceptance step needed for timelocked governance. Update the sequence around the
governance commands to add the corresponding governance accept-ready step after
each submit, or clearly state that this block only applies when timelock is
zero. Make sure the instructions reference the governance CLI flow shown in the
README so the setup becomes executable end-to-end.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: f490281c-7ed9-4afa-97aa-0160d0ae1d60
📒 Files selected for processing (15)
.github/workflows/kani.ymlCargo.tomlREADME.mdcontract/universal-account/tests/universal_account.rscontract/vault/kernel/Cargo.tomlcontract/vault/kernel/src/actions/mod.rscontract/vault/kernel/src/lib.rscontract/vault/kernel/src/math/number.rscontract/vault/kernel/tests/property_tests.rsfuzz/fuzz_targets/fuzz_fee_math.rstest-utils/src/controller/universal_account.rstools/soroban-vault-cli/README.mduniversal-account/src/authentication/mod.rsuniversal-account/src/execute_args.rsuniversal-account/src/state/migration.rs
|
@coderabbitai stop jerking off and review my PR! |
|
✅ Action performedFull review finished. |
|
✅ Action performedFull review finished. |
|
✅ Action performedFull review finished. |
There was a problem hiding this comment.
Warning
CodeRabbit couldn't request changes on this pull request because it doesn't have sufficient GitHub permissions.
Please grant CodeRabbit Pull requests: Read and write permission and re-run the review.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
tools/soroban-vault-cli/README.md (1)
161-179: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAdd explicit proposal acceptance steps in this setup flow.
Line 161-179 shows
governance submit-*commands only; in timelocked setups this sequence is incomplete withoutgovernance accept-ready, so readers can follow commands that won’t activate routes. Add matching acceptance commands (or a one-line note that these submits require acceptance before allocation works).Suggested doc patch
tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR_OR_MULTISIG... \ --entry 0:CBLENDADAPTER... \ --entry 1:CCUSTODIALADAPTER... +tmplr-soroban-vault governance accept-ready --admin GCURATOR_OR_MULTISIG... --kind allowed-adapters +tmplr-soroban-vault governance accept-ready --admin GCURATOR_OR_MULTISIG... --kind cap +tmplr-soroban-vault governance accept-ready --admin GCURATOR_OR_MULTISIG... --kind supply-queue🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tools/soroban-vault-cli/README.md` around lines 161 - 179, The governance setup flow in README is incomplete because the `submit-*` commands in the `governance` section do not show the required acceptance step for timelocked proposals. Update the documentation around the `governance submit-set-allowed-adapters`, `governance submit-set-cap`, and `governance submit-set-supply-queue` examples to include the matching `governance accept-ready` command(s) or a clear note that these submissions must be accepted before the routes become active.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@contract/vault/kernel/src/actions/mod.rs`:
- Around line 1811-1823: The emergency-reset path in plan_emergency_reset should
not blindly dequeue the withdraw_queue after refunding from OpState::Withdrawing
or OpState::Payout. First validate that the active queue head exists and matches
the current op-state/owner (and expected shares/amount) before calling
withdraw_queue.dequeue(); if the head is missing or mismatched, abort the reset
instead of reporting success. Use the existing refund_owner, refund_shares,
restore_to_idle, and withdraw_queue logic in plan_emergency_reset to enforce
this invariant.
---
Outside diff comments:
In `@tools/soroban-vault-cli/README.md`:
- Around line 161-179: The governance setup flow in README is incomplete because
the `submit-*` commands in the `governance` section do not show the required
acceptance step for timelocked proposals. Update the documentation around the
`governance submit-set-allowed-adapters`, `governance submit-set-cap`, and
`governance submit-set-supply-queue` examples to include the matching
`governance accept-ready` command(s) or a clear note that these submissions must
be accepted before the routes become active.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 97e66cb1-99db-492e-a969-2095571313d6
📒 Files selected for processing (15)
.github/workflows/kani.ymlCargo.tomlREADME.mdcontract/universal-account/tests/universal_account.rscontract/vault/kernel/Cargo.tomlcontract/vault/kernel/src/actions/mod.rscontract/vault/kernel/src/lib.rscontract/vault/kernel/src/math/number.rscontract/vault/kernel/tests/property_tests.rsfuzz/fuzz_targets/fuzz_fee_math.rstest-utils/src/controller/universal_account.rstools/soroban-vault-cli/README.mduniversal-account/src/authentication/mod.rsuniversal-account/src/execute_args.rsuniversal-account/src/state/migration.rs
There was a problem hiding this comment.
Warning
CodeRabbit couldn't request changes on this pull request because it doesn't have sufficient GitHub permissions.
Please grant CodeRabbit Pull requests: Read and write permission and re-run the review.
Actionable comments posted: 4
♻️ Duplicate comments (3)
contract/vault/kernel/src/lib.rs (1)
211-216: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAssert full
Addressequality in these proofs.These checks still only compare
.0[0], so mutations in the other 31 bytes can slip through the harness. Reuseassert_address_eqanywhere the proof is meant to pin owner/receiver identity.As per coding guidelines, “Write comprehensive unit tests for new, non-trivial logic.”
Also applies to: 1427-1435
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@contract/vault/kernel/src/lib.rs` around lines 211 - 216, The proof helper in assert_refund_owner_is_owner is only comparing owner.0[0], so it can miss mutations in the rest of the Address bytes. Update this check to use assert_address_eq (as used elsewhere for identity checks) so the full Address is validated, and apply the same fix to the related owner/receiver proof assertions referenced in the comment.Source: Coding guidelines
contract/vault/kernel/tests/property_tests.rs (1)
1647-1712: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAssert the atomic-redeem reject path explicitly.
This property still only validates successful redeems. When
previewed_assets > old_state.idle_assets, a buggy implementation that succeeds or clamps would still pass the test.As per coding guidelines, “Write comprehensive unit tests for new, non-trivial logic.”
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@contract/vault/kernel/tests/property_tests.rs` around lines 1647 - 1712, The property test for `prop_atomic_redeem_respects_idle_cap` only checks the success case, so add an explicit reject-path assertion when `previewed_assets > old_state.idle_assets` by verifying `apply_action` returns an error for `KernelAction::AtomicRedeem`. Keep the existing success assertions for the `Ok` branch, but make the test fail if the redeem incorrectly succeeds or clamps the transfer amount, using the same `preview_withdraw_assets`, `apply_action`, and `KernelEffect` checks to locate the logic.Source: Coding guidelines
contract/vault/kernel/src/actions/mod.rs (1)
1811-1823: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick winValidate the queue head before emergency reset dequeues it.
plan_emergency_resetstill refunds the owner fromOpState::Withdrawing/OpState::Payoutand then blindly dequeues whatever head is present. If op-state andwithdraw_queuedrift, reset can refund one request while removing another, or succeed with no matching queue entry at all.As per coding guidelines, “Check invariants around refunds, withdrawals, account deletion, authorization, and replay or double-execution risks.”
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@contract/vault/kernel/src/actions/mod.rs` around lines 1811 - 1823, The emergency reset path in plan_emergency_reset should not blindly dequeue after refunding from OpState::Withdrawing or OpState::Payout. Before calling state.withdraw_queue.dequeue(), validate that the queue head matches the active op-state being refunded (owner and escrow/amount should align), and fail or skip the reset if the invariant is broken. Use the OpState variants and the withdraw_queue access in this function to locate the logic and add the head check right before the dequeue.Source: Coding guidelines
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@contract/vault/kernel/src/lib.rs`:
- Around line 1176-1265: The emergency-reset Kani proofs are using an invalid
starting state by constructing OpState::Withdrawing and OpState::Payout while
the withdraw queue is empty, which masks queue-head mismatch issues. Update
these proofs so the initial VaultState includes a queue/op-state combination
that satisfies the real invariant for the active operation, using the existing
helpers around plan_emergency_reset, withdraw_queue, and the OpState variants to
build a valid withdrawal/payout in-progress state. Keep the assertions focused
on the reset outcome, but ensure the setup no longer depends on drift-tolerant
invalid state handling.
In `@tools/soroban-vault-cli/README.md`:
- Around line 159-174: The “active route” example in the README currently shows
only submit commands, but the setup is not effective until the relevant
proposals are accepted. Update the example around the governance
submit-set-allowed-adapters and submit-set-cap flow to either include the
matching accept-ready commands for those proposal kinds or clearly note that
acceptance is still required before the route becomes active.
In `@universal-account/src/authentication/mod.rs`:
- Around line 232-243: The `valid_raw_message` helper in `authentication::mod`
builds a `raw::Message` from `WithRawString` using an empty `raw` string paired
with a separate parsed `Payload`, which makes the signed/raw state inconsistent.
Update it to construct the message through the same serializer-backed path
production uses, such as `WithRawString::from_parsed(...)`, so the raw and
parsed forms are derived from one another before wrapping it in
`MessageWithValidSignature`. This keeps the proof harness aligned with
`verify_execution` and makes invalid states unrepresentable.
In `@universal-account/src/state/migration.rs`:
- Around line 211-260: The migration proofs in V0, V1, and UnbrickV1 only cover
empty key maps, so they miss regressions that break populated key storage.
Update the Kani proofs or add a conventional regression test around state::V0,
state::V1, V1.transform, and UnbrickV1.transform that initializes IterableMap
with at least one KeyId/KeyParameters entry and asserts the keys survive the
migration unchanged, alongside the existing scalar checks.
---
Duplicate comments:
In `@contract/vault/kernel/src/actions/mod.rs`:
- Around line 1811-1823: The emergency reset path in plan_emergency_reset should
not blindly dequeue after refunding from OpState::Withdrawing or
OpState::Payout. Before calling state.withdraw_queue.dequeue(), validate that
the queue head matches the active op-state being refunded (owner and
escrow/amount should align), and fail or skip the reset if the invariant is
broken. Use the OpState variants and the withdraw_queue access in this function
to locate the logic and add the head check right before the dequeue.
In `@contract/vault/kernel/src/lib.rs`:
- Around line 211-216: The proof helper in assert_refund_owner_is_owner is only
comparing owner.0[0], so it can miss mutations in the rest of the Address bytes.
Update this check to use assert_address_eq (as used elsewhere for identity
checks) so the full Address is validated, and apply the same fix to the related
owner/receiver proof assertions referenced in the comment.
In `@contract/vault/kernel/tests/property_tests.rs`:
- Around line 1647-1712: The property test for
`prop_atomic_redeem_respects_idle_cap` only checks the success case, so add an
explicit reject-path assertion when `previewed_assets > old_state.idle_assets`
by verifying `apply_action` returns an error for `KernelAction::AtomicRedeem`.
Keep the existing success assertions for the `Ok` branch, but make the test fail
if the redeem incorrectly succeeds or clamps the transfer amount, using the same
`preview_withdraw_assets`, `apply_action`, and `KernelEffect` checks to locate
the logic.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 38a9239c-b5bb-46fa-bb0a-f922d7a577e6
📒 Files selected for processing (15)
.github/workflows/kani.ymlCargo.tomlREADME.mdcontract/universal-account/tests/universal_account.rscontract/vault/kernel/Cargo.tomlcontract/vault/kernel/src/actions/mod.rscontract/vault/kernel/src/lib.rscontract/vault/kernel/src/math/number.rscontract/vault/kernel/tests/property_tests.rsfuzz/fuzz_targets/fuzz_fee_math.rstest-utils/src/controller/universal_account.rstools/soroban-vault-cli/README.mduniversal-account/src/authentication/mod.rsuniversal-account/src/execute_args.rsuniversal-account/src/state/migration.rs
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
tools/soroban-vault-cli/README.md (1)
162-187: 🎯 Functional Correctness | 🔵 TrivialHuman-check priority: verify CLI command/flag names remain exact (
--kind allowed-adapters|cap|supply-queue,--entry,--market-id) against the current parser before release.As per path instructions, “point out the critical aspects of the pull request that a human would be useful to inspect.”
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tools/soroban-vault-cli/README.md` around lines 162 - 187, The CLI usage examples for governance commands should be double-checked against the current parser before release, with special attention to the exact flag and kind names used in the README snippets. Verify that `submit-set-allowed-adapters`, `submit-set-cap`, `submit-set-supply-queue`, and `accept-ready` still accept the documented `--kind allowed-adapters|cap|supply-queue`, `--entry`, and `--market-id` values exactly as shown, and update the examples if any parser names or accepted values have changed.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@tools/soroban-vault-cli/README.md`:
- Around line 162-187: The CLI usage examples for governance commands should be
double-checked against the current parser before release, with special attention
to the exact flag and kind names used in the README snippets. Verify that
`submit-set-allowed-adapters`, `submit-set-cap`, `submit-set-supply-queue`, and
`accept-ready` still accept the documented `--kind
allowed-adapters|cap|supply-queue`, `--entry`, and `--market-id` values exactly
as shown, and update the examples if any parser names or accepted values have
changed.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: b17897ad-a62c-4638-b979-f254161013ac
📒 Files selected for processing (4)
.github/workflows/kani.ymlcontract/vault/kernel/src/lib.rscontract/vault/kernel/tests/property_tests.rstools/soroban-vault-cli/README.md
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 919c814d64
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| tmplr-soroban-vault governance accept-ready \ | ||
| --admin GCURATOR_OR_MULTISIG... \ | ||
| --kind cap |
There was a problem hiding this comment.
When a governance queue also has a ready cap-group proposal, this documented accept-ready --kind cap can accept more than the market-cap proposals submitted above: the CLI filters by checking whether the action/raw proposal text contains the lowercased kind string (tools/soroban-vault-cli/src/commands.rs:2998-3008), so CapGroup/cap_group_id also matches cap, and run_governance_accept_ready accepts every ready match. The setup instructions should direct operators to accept the specific proposal IDs or otherwise disambiguate the cap proposal, rather than using this broad filter.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a39c949659
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| - "Cargo.lock" | ||
| - "common/**" | ||
| - "contract/universal-account/**" | ||
| - "contract/vault/kernel/**" |
There was a problem hiding this comment.
When a PR changes only contract/vault/macros/**, this workflow is skipped because the pull_request.paths list matches contract/vault/kernel/** but not the proc-macro crate. I checked contract/vault/kernel/Cargo.toml: templar-vault-kernel depends on templar-vault-macros, so macro changes can alter generated kernel code or break Kani compilation while avoiding PR Kani until the nightly run. Please include contract/vault/macros/** or remove the filter so these Kani jobs run for that dependency.
Useful? React with 👍 / 👎.
1 participant
Summary
Adds targeted Kani harnesses and cheaper regression/property coverage for high-risk Universal Account and Vault invariants, plus a dedicated GitHub Actions workflow to run those proofs nightly, manually, and on PRs that touch the relevant UA/Vault verification surfaces.
Universal Account coverage:
domain_idreplay-isolation requirement.Vault coverage:
Deposit -> RequestWithdrawsequence remains too expensive for Kani.Workflow coverage:
.github/workflows/kani.ymlwith nightly, manual, and path-filtered PR triggers.Soroban vault CLI docs:
submit-set-cap --market-id ... --cap ...proposal before governance accepts them in the supply queue.curator allocate-withdrawdoes not refresh route NAV; operators should runcurator refresh-marketsafter adapter NAV changes before relying on share-rate/accounting views.devwith the cap and NAV semantics above.Note: exact Kani proof of Vault deposit/redeem preview parity over the current production
Number/U256 math path is intentionally not included. The real path currently stalls Kani, so this PR keeps that coverage as property tests rather than adding a simplified formal model that would not prove production behavior.Validation
cargo fmt --all --checkgit diff --checkcargo check -p templar-vault-kernel --all-featurescargo test -p templar-universal-account state::migration --lib -- --nocapturecargo test -p templar-universal-account verify_rejects_signed_payload_mutation_for_each_format -- --nocaptureTEST_CONTRACTS_PREBUILT=1 cargo test -p templar-universal-account-contract replayed_nonce_fails_without_reexecuting_payload --test universal_account -- --nocaptureTEST_CONTRACTS_PREBUILT=1 cargo test -p templar-universal-account-contract removed_key_cannot_execute_transaction --test universal_account -- --nocaptureTEST_CONTRACTS_PREBUILT=1 cargo test -p templar-universal-account-contract failed_execute_does_not_consume_nonce_and_success_consumes_once --test universal_account -- --nocapturecargo test -p templar-vault-kernel --test property_tests -- --nocapturetimeout 300s cargo kani -p templar-universal-accounttimeout 300s cargo kani -p templar-vault-kerneltimeout 360s cargo kani -p templar-vault-kernel --features action-sync-externalcargo kani -p templar-vault-kernel --features action-refresh-fees --harness refresh_fees_zero_fee_rates_only_update_anchor --harness refresh_fees_active_rates_only_mint_fee_shares_and_update_anchorVault Kernel / Refresh Fees,Vault Kernel / Withdraw Escrow, and the broadVault Kerneljob.origin/devat50918bfe; local post-rebase checks passed:cargo fmt --all --check,git diff --check.129255 bytes.This change is