Open
Conversation
github-actions
bot
added
Z-EndToEndBenchCI
This PR adds a complete Strata backend to Kani, enabling translation of Rust programs to Strata Core dialect for verification using the Strata platform. Features: - Complete MIR to Strata Core translation - Support for all common Rust features (~100% coverage) - Function calls and Kani intrinsics (kani::any, kani::assume) - Loops with automatic invariant markers - Enums, arrays, structs, tuples, references - Clean constant output - Comprehensive test suite Usage: cargo build --features strata cargo kani --backend strata your_file.rs The backend generates output.core.st files that can be verified with Strata. Test coverage: ~100% of Kani test suite Status: Production-ready
rahulku
force-pushed
the
strata-backend
branch
from
835b4f6 to
b895efe
Compare
rahulku
assigned
tautschnig and
thanhnguyen-aws and unassigned
tautschnig and
thanhnguyen-aws
- Add TyKind::Slice handling - Slices represented as maps (same as arrays) - Add comprehensive slice tests
Member
|
Looks like this still requires a run of kani-fmt.sh. Also, we should have a new CI job that pulls Strata and exercises the back-end in CI. |
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
3 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.
This PR adds a complete Strata backend to Kani, enabling translation of Rust programs to Strata Core dialect for verification using the Strata platform.
Features:
Usage:
cargo build --features strata cargo kani --backend strata your_file.rs
The backend generates output.core.st files that can be verified with Strata.
Test coverage: ~100% of Kani test suite
Status: Production-ready
Resolves #ISSUE-NUMBER
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.