Add CSE verification script with KCFG minimization and K module generation #668
Conversation
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
- Add 5 tests with varying function call counts (1, 10, 100, 1000, 10000) - Tests evaluate composable symbolic execution with repeated function calls - All tests use loop-based implementation for scalability - Set depth limit to 50 for controlled symbolic execution 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
- Added pytest-timeout dependency to dev requirements - Set default 300s timeout for test-integration target in Makefile - Allows overriding timeout via TEST_ARGS parameter 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
This script demonstrates how to: - Use KMIR to verify Rust functions with arbitrary entry points - Generate and save APRProof objects - Create proof show output for visualization - Support both add1 and main function verification The script correctly handles both passing (main with assertions) and failing/stuck (add1 with potential overflow) verification cases. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
Added new features to the verification script: - KCFG minimization using apr_proof.minimize_kcfg() to reduce redundant nodes - K module generation from minimized KCFG using to_module() - Save both original and minimized proof show outputs - Track minimization statistics in summary file Results show: - add1 function: reduced from 7 nodes/3 edges to 6 nodes/2 edges - main function: already optimal at 3 nodes/1 edge (no reduction) - Generated K modules saved as .k files for reuse This enhancement enables more efficient proof representation and provides reusable K modules for future verification work. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
Changed from Python object string representation to proper K syntax: - Use kmir.pretty_print() to format KFlatModule as valid K code - Reduced file sizes significantly (80KB→19KB, 53KB→13KB) - Generated modules now follow K language syntax with proper formatting - Modules can be directly imported/used in other K specifications The generated .k files now contain valid K module definitions with: - Proper module/endmodule structure - Correctly formatted rules with labels and priorities - K cell structure with proper XML-like notation - Valid K term syntax instead of Python repr strings 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
Contributor
Author
|
run with main summary. !!!!!! |
Contributor
Author
|
run without main summary: |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 adds a Python script for verifying Rust functions using KMIR, with support for KCFG minimization and K module generation.
Features
mainTest Results
Tested with
cse_call_add1_1time.rs:add1function:mainfunction:Usage
Output Files
The script generates the following in
add1_proof/:.show- Original proof show output.minimized.show- Minimized proof show output.k- K module for reuse.summary- Verification statisticsImplementation Details
APRProof.minimize_kcfg()to reduce proof complexityKCFG.to_module()with proper defunctionalization🤖 Generated with Claude Code