feat(stealth-registry): add Kani formal verification for top 3 invariants (#108) - #146
Merged
truthixify merged 19 commits intoAug 4, 2026
Conversation
|
@Michvista 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! 🚀 |
Contributor
|
Two specific failures to fix:
|
Contributor
Author
|
Hiii ive made the fix @truthixify |
Contributor
Author
- Remove RegistryError from mock_sdk import in lib.rs (it is defined in lib.rs itself, not in mock_sdk; importing it caused unresolved import under Kani) - Fix InstanceStorage and Events struct field name mismatch: both declare the field as _env but Storage::instance() and Env::events() were constructing them with env; updated constructors to use _env - Rewrite mock_sdk.rs with consistent LF line endings and clean rustfmt-compliant formatting (no std:: usage; uses core:: and alloc:: only, matching the #![no_std] crate requirement) - Reformat proofs/mod.rs to consistent LF line endings eliminating the mixed CRLF/LF drift that caused cargo fmt --all --check to fail
… conflict Under kani, lib.rs was defining its own crate::DataKey while mock_sdk also defines mock_sdk::DataKey. PersistentStorage methods take &mock_sdk::DataKey, so register_keys creating crate::DataKey caused a type mismatch at compile time. Fix: - Add DataKey to the #[cfg(kani)] import from mock_sdk so the storage layer and the contract logic share one type - Gate the #[cfg(not(kani))] + #[contracttype] DataKey definition so it only exists in the soroban build, not under Kani - Normalize lib.rs to LF line endings throughout to resolve the cargo fmt --all --check failure (CRLF in the pre-existing body was causing rustfmt --check to flag the whole file)
…ustfmt - Under cfg(kani), import into_val (IntoVal trait), symbol_short macro, emit_metric, contract_ids, metric_names, and dimension_names into lib.rs scope so that stealth-registry compiles clean under Kani. - Format remove_keys signature and PersistentStorage::get iterator chain to match canonical rustfmt guidelines. - Standardize LF line endings across lib.rs, mock_sdk.rs, and proofs/mod.rs.
When cargo kani runs on stealth-registry, cargo was compiling the real soroban-sdk and wraith-metrics dependency crates because they were listed under un-gated [dependencies]. soroban-sdk on host target pulls in std and host dependencies, causing Kani verification failures. Fix: Move dependencies and dev-dependencies to target.'cfg(not(kani))' blocks so cargo kani compiles stealth-registry in pure no_std mode using only core/alloc and the embedded mock_sdk.
…re Cargo.toml - Add #[cfg(kani)] extern crate std; to lib.rs to resolve 'unresolved module std' when Kani harness generates std-based proof execution code for no_std crate. - Restore standard [dependencies] and [dev-dependencies] in Cargo.toml so standard cargo test / cargo build in workspace succeed.
…ct rustfmt layout - Optimize Kani proofs in proofs/mod.rs by using direct kani::any() 64-byte array generation instead of 64-iteration loops, and adding #[kani::unwind(10)] attributes. - Match single-line rustfmt layout for remove_keys in lib.rs and get in mock_sdk.rs.
…rs under cfg(kani)
- Convert 52 files in stellar/ from CRLF to LF to fix cargo fmt --all --check failures on the Linux CI runner caused by Windows git autocrlf converting line endings on checkout. - Add .gitattributes at repo root enforcing eol=lf for all text files (.rs, .toml, .yml, .md, .json, .ts, .js) to permanently prevent CRLF re-introduction from Windows developer machines.
…not(kani)) in Cargo.toml
…nnotation fmt fixes (lib.rs): - Merge mock_sdk use import to single line (fits within 100-char limit) - Collapse remove_keys signature to single line (fits within 100-char limit) fmt fixes (mock_sdk.rs): - Expand PersistentStorage and InstanceStorage struct expressions to multi-line - Expand state.storage.iter().find().map() chain to multi-line kani fix (proofs/mod.rs): - Add explicit type Vec<StorageEntry> to storage variable to resolve E0282
…fs to prevent timeout explosion
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR sets up Kani formal verification in
stealth-registry/src/proofs/to prove correctness-critical invariants.Proved Invariants
proof_register_then_resolve): Proves that registering a 64-byte stealth meta-address payload and resolving it immediately returns the exact registered payload.proof_no_duplicate_keys): Proves that active storage entries maintain key uniqueness across mutations.proof_expiry_monotonicity): Proves that TTL extensions during registration and lookup operations result in monotonically non-decreasing expiry ledgers (new_expiry >= old_expiry).CI & Documentation
stellar-kanijob in.github/workflows/ci.ymlusingmodel-checking/kani-github-action@v1.stellar/stealth-registry/README.md.Closes #108