rucc-verify 0.1.0

SMT verification of the rucc rewrite and lowering rule set.

Coverage
100%
2 out of 2 items documented0 out of 0 items with examples
Size
Source code size: 3.22 kB This is the summed size of all the files inside the crates.io package for this release.
Documentation size: 111.12 kB This is the summed size of all files generated by rustdoc for all configured targets
Ø build duration
this release: 2s Average build duration of successful builds.
all releases: 2s Average build duration of successful builds in releases after 2024-10-23.
Links
Homepage
tamnd/rucc
0 0 31
crates.io
Dependencies
Versions
Owners

SMT verification of the rule set.

Design: spec/15-testing.md section 15.5. Outside the layer stack: this runs in CI, not in the compiler.

Every rewrite rule and every lowering rule carries a specification, and this crate discharges it. An unverified rule does not enter the rule set. Rules that the solver cannot discharge, usually wide bitvector multiplication, get a bounded proof over restricted widths plus a reviewed justification, and the count of those is a reported metric that going up is a signal about.

The approach follows Crocus (ASPLOS 2024), cited in spec/01-research-2026.md.

Status

Not implemented. Built alongside rucc-rules in M3.