//! The list of rules nobody has proved at the width the compiler runs them at.
//!
//! Design: `spec/optimizer/41-correctness.md` section 41.8. The count of rules that needed a
//! bounded proof has been printed since this crate existed, and a number in a build log is a
//! thing nobody reads twice. What that section asks for instead is a file: every such rule listed
//! by name with the reason it was let in, checked in beside the rules, so that adding one is a
//! line in a diff somebody has to approve. The list is the artefact and the count going up is the
//! alarm.
//!
//! Nothing else is on the list, because there is nothing else to put on it. A rule the solver
//! refutes and a rule it gives up on without a written reason do not enter the rule set at all,
//! so the only case there is to record is the middle one: a claim no solver settles at sixty four
//! bits, settled at [`crate::BOUNDED_WIDTHS`] instead, with somebody's reason for taking that as
//! enough.
//!
//! # Naming a rule
//!
//! Rules have no names, so the name here is the pattern printed back, with the guard after it
//! when there is one. That is what a reader recognises the rule by and it is stable under the
//! edits that are not about this rule, which a line number would not be: a rule added at the top
//! of a file would otherwise rewrite every entry below it and the diff would stop meaning
//! anything.
use std::fmt::Write as _;
use rucc_rules::Rule;
use crate::verify::{Report, Verdict};
/// One rule that was let in on a proof at narrower widths than it runs at.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Unverified {
/// The rule file it is in, as it was named on the command line.
pub file: String,
/// The pattern it matches, printed back.
pub pattern: String,
/// The condition on the match, printed back, when the rule has one.
pub guard: Option<String>,
/// The widths it was proved at, narrowest first.
pub widths: Vec<u32>,
/// The reason the rule's `bounded` clause gives, which is what a reviewer signed for.
pub why: String,
}
/// Every rule in one file that was let in on a bounded proof, in the order they are written.
#[must_use]
pub fn listed(file: &str, rules: &[Rule], report: &Report) -> Vec<Unverified> {
let mut out = Vec::new();
for (rule, verdict) in rules.iter().zip(&report.verdicts) {
let Verdict::Bounded { widths, why } = verdict else { continue };
out.push(Unverified {
file: file.to_owned(),
pattern: rule.pattern.to_string(),
guard: rule.guard.as_ref().map(ToString::to_string),
widths: widths.clone(),
why: why.clone(),
});
}
out
}
/// The whole file, as text.
///
/// The entries arrive already in the order the files were verified in, which is sorted, so the
/// grouping below is a run over neighbours rather than a sort of its own. A file that produced no
/// entries gets no heading, because a heading with nothing under it reads as a claim that
/// something is wrong there.
#[must_use]
pub fn render(entries: &[Unverified]) -> String {
let mut out = String::from("# Unverified rules\n\n");
out.push_str(
"Generated by `cargo run -q -p rucc-verify -- crates/rucc-codegen/rules crates/rucc-opt/rules --report docs/UNVERIFIED.md`. Do not edit this file, edit the rules.\n\n",
);
out.push_str(
"Every rule in the rule set carries a bitvector claim and `rucc-verify` discharges it before the rule is allowed in. Almost all of them are settled at the width the compiler runs them at, and there is nothing to say about those. This file is the rest: a rule no solver settles at its own width, proved instead at four and eight bits because somebody wrote down a reason for taking that as enough. `spec/optimizer/41-correctness.md` section 41.8 asks for that set to be a list rather than a number in a build log, because the list is the thing a reviewer can argue with.\n\n",
);
out.push_str(
"A rule the solver refutes is not here, and neither is a rule it gives up on that carries no reason. Neither of those enters the rule set at all, so there is no list for them to be on.\n\n",
);
out.push_str(&format!("{}\n\n", counted(entries.len())));
let mut file = "";
for entry in entries {
if entry.file != file {
file = &entry.file;
let _ = writeln!(out, "## `{file}`\n");
}
out.push_str(&bullet(entry));
}
out
}
/// How many rules are on the list, said as a sentence, which is the number the alarm is about.
fn counted(count: usize) -> String {
match count {
0 => "No rule is on this list, which is the state to keep it in.".to_owned(),
1 => "One rule is on this list.".to_owned(),
many => format!("{many} rules are on this list."),
}
}
/// One entry, as the line it occupies in the file.
fn bullet(entry: &Unverified) -> String {
let mut out = format!("- `{}`", entry.pattern);
if let Some(guard) = &entry.guard {
let _ = write!(out, " when `{guard}`");
}
let _ = writeln!(out, ", proved at {}: {}", widths(&entry.widths), entry.why);
out
}
/// The widths a bounded proof was taken over, said the way a person would say them.
fn widths(over: &[u32]) -> String {
let mut out = String::new();
for (at, width) in over.iter().enumerate() {
if at > 0 {
out.push_str(if at + 1 == over.len() { " and " } else { ", " });
}
let _ = write!(out, "{width}");
}
out.push_str(" bits");
out
}
/// How the list on disk differs from the list the solver just produced.
///
/// The two halves are what was added and what was removed, and both are wanted rather than a
/// count: a rule leaving the list is a rule somebody managed to prove properly and is worth
/// seeing, and a rule joining it is the thing this whole file exists to make visible. Comparing
/// the entry lines rather than the whole text is what makes that possible, since the surrounding
/// prose changing is a different event and gets a different sentence out of the caller.
#[must_use]
pub fn difference(found: &str, wanted: &str) -> (Vec<String>, Vec<String>) {
let entries = |text: &str| -> Vec<String> {
text.lines().filter(|line| line.starts_with("- `")).map(ToOwned::to_owned).collect()
};
let (before, after) = (entries(found), entries(wanted));
let added = after.iter().filter(|line| !before.contains(line)).cloned().collect();
let removed = before.iter().filter(|line| !after.contains(line)).cloned().collect();
(added, removed)
}
#[cfg(test)]
mod tests {
use super::*;
fn entry(file: &str, pattern: &str) -> Unverified {
Unverified {
file: file.to_owned(),
pattern: pattern.to_owned(),
guard: None,
widths: vec![4, 8],
why: "the solver does not settle a multiply of two unknowns at this width".to_owned(),
}
}
#[test]
fn an_empty_list_says_so_rather_than_trailing_off() {
let text = render(&[]);
assert!(text.contains("No rule is on this list"), "{text}");
assert!(!text.contains("- `"), "{text}");
assert!(!text.contains("## `"), "{text}");
}
#[test]
fn an_entry_carries_the_rule_the_widths_and_the_reason() {
let text = render(&[entry("rules/x86-64.rules", "(mul.i64 (value.i64 x) (iconst.i64 k))")]);
assert!(text.contains("One rule is on this list."), "{text}");
assert!(text.contains("## `rules/x86-64.rules`"), "{text}");
assert!(
text.contains(
"- `(mul.i64 (value.i64 x) (iconst.i64 k))`, proved at 4 and 8 bits: the solver"
),
"{text}"
);
}
#[test]
fn a_guard_is_part_of_what_names_the_rule() {
let mut one = entry("rules/x86-64.rules", "(mul.i64 (value.i64 x) (iconst.i64 k))");
one.guard = Some("(= k 1)".to_owned());
let text = render(&[one]);
assert!(text.contains("(iconst.i64 k))` when `(= k 1)`, proved at"), "{text}");
}
#[test]
fn each_file_gets_one_heading_and_the_rules_under_it() {
let text = render(&[
entry("rules/a.rules", "(mul.i8 x y)"),
entry("rules/a.rules", "(mul.i16 x y)"),
entry("rules/b.rules", "(mul.i32 x y)"),
]);
assert_eq!(text.matches("## `rules/a.rules`").count(), 1, "{text}");
assert_eq!(text.matches("## `rules/b.rules`").count(), 1, "{text}");
assert!(text.contains("3 rules are on this list."), "{text}");
}
#[test]
fn one_width_is_not_said_as_a_pair() {
assert_eq!(widths(&[4]), "4 bits");
assert_eq!(widths(&[4, 8]), "4 and 8 bits");
assert_eq!(widths(&[4, 8, 16]), "4, 8 and 16 bits");
}
#[test]
fn the_difference_is_the_rules_that_moved_and_not_the_prose_around_them() {
let before = render(&[entry("rules/a.rules", "(mul.i8 x y)")]);
let after = render(&[entry("rules/a.rules", "(mul.i16 x y)")]);
let (added, removed) = difference(&before, &after);
assert_eq!(added.len(), 1, "{added:?}");
assert_eq!(removed.len(), 1, "{removed:?}");
assert!(added[0].contains("(mul.i16 x y)"), "{added:?}");
assert!(removed[0].contains("(mul.i8 x y)"), "{removed:?}");
// The same list twice is no difference at all, which is the case the gate passes on.
let (added, removed) = difference(&before, &before);
assert!(added.is_empty() && removed.is_empty(), "{added:?} {removed:?}");
}
}