feat: rules_verus Bazel integration + verify_contracts target#70
Merged
feat: rules_verus Bazel integration + verify_contracts target#70
Conversation
Formal specification contracts for synth's critical subsystems, designed for future Verus integration via rules_verus + verus_strip. contracts.rs — 4 specification modules: - regalloc: reserved register exclusion (R9/R10/R11), allocation validation, index bounds checking - encoding: Thumb-16/32 byte count, MOVW/MOVT imm16 range, register bit-field range - memory: access size validation (1/2/4/8), bounds check with size - division: trap guard sequence length (CMP+BNE+UDF+xDIV >= 4) Runtime checks inserted at 13 critical sites: - alloc_reg: pre/post allocation validation - index_to_reg: allocatable register check - generate_*_with_bounds_check: access_size precondition (4 sites) - I32Div*/I32Rem* trap guard: sequence length check (4 sites) - encode_thumb32_movw/movt: register + immediate range - SDIV/UDIV encoding: register range + output size 9 unit tests including #[should_panic] for contract violations. VG-001 and VG-006 status updated to in-progress. 895 tests (was 885), clippy clean, fmt clean. Implements: VG-001 Implements: VG-006 Trace: skip Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The contracts module now contains real Verus spec functions inside
verus! {} blocks. Three compilation modes:
1. Plain cargo: #[cfg(not(verus_keep_ghost))] no-op macro strips specs
2. Verus verification: verus! {} enables machine checking
3. verus_strip (rules_verus @ 24d5ddb5): removes blocks entirely
debug_assert! runtime checks remain alongside the formal specs.
Added #![allow(unexpected_cfgs)] for verus_keep_ghost.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Added rules_verus @ a49f72ef (latest, includes verus_strip + bundled sysroot) to MODULE.bazel. Bazel targets: - //crates:verify_contracts — verus_test for contracts.rs (SMT/Z3) - //crates:contracts_plain — verus_strip output for plain Rust rules_verus provides: - Pre-built Verus binaries with bundled Rust nightly sysroot - No rules_rust version conflicts (PR #8 fix) - verus_strip for annotation removal Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
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
1 participant
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
//crates:verify_contracts— Verus SMT verification of contracts.rs//crates:contracts_plain— verus_strip output for plain Rust toolingverus! {}blocks + no-op fallback macroTest plan
cargo test --workspace— 895 tests, 0 failurescargo clippy— cleanbazel test //crates:verify_contracts— Verus verification (CI)🤖 Generated with Claude Code