feat: Verus-style contracts with runtime debug_assert! checking#69
Merged
feat: Verus-style contracts with runtime debug_assert! checking#69
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>
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
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>
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
Formal specification contracts for critical subsystems, designed for future Verus integration.
contracts.rs (new module)
Runtime checks at 13 critical sites
alloc_reg,index_to_regPath to Verus
These
debug_assert!contracts mirror Verusrequires/ensuresspecs.When
rules_veruswithverus_stripis ready, wrap inverus!{}blocksfor machine-checked verification.
895 tests (was 885), VG-001/VG-006 in-progress.
Test plan
cargo test --workspace— 895 tests, 0 failures#[should_panic]) passcargo clippy— clean🤖 Generated with Claude Code