rucc_verify/
lib.rs

1//! SMT verification of the rule set.
2//!
3//! Design: `spec/15-testing.md` section 15.5. Outside the layer stack: this runs in CI, not
4//! in the compiler.
5//!
6//! Every rewrite rule and every lowering rule carries a specification, and this crate
7//! discharges it. An unverified rule does not enter the rule set. Rules that the solver
8//! cannot discharge, usually wide bitvector multiplication, get a bounded proof over
9//! restricted widths plus a reviewed justification, and the count of those is a reported
10//! metric that going up is a signal about.
11//!
12//! The approach follows Crocus (ASPLOS 2024), cited in `spec/01-research-2026.md`.
13//!
14//! # Status
15//!
16//! Not implemented. Built alongside `rucc-rules` in `M3`.
17
18#![doc(html_root_url = "https://docs.rs/rucc-verify/0.1.0")]
19
20/// The milestone in `spec/17-milestones.md` that fills this crate in.
21pub const MILESTONE: &str = "M3";
22
23#[cfg(test)]
24mod tests {
25    #[test]
26    fn milestone_is_recorded() {
27        assert_eq!(super::MILESTONE, "M3");
28    }
29}
rucc_verify/lib.rs

rucc_verify/
lib.rs
