valeria_rule_audit/
valeria_rule_audit.rs

1//! Read id/width/input/reference TSV; report built-in coverage, never assume it.
2use std::io::{self, BufRead};
3
4use bitwright::engine::{Engine, Strategy};
5use bitwright::{BitVec, Context, FnEnv, ParseOptions, SymbolKey, Width};
6
7fn main() {
8    let strategy = if std::env::args().any(|a| a == "--deobfuscate") {
9        Strategy::deobfuscate()
10    } else {
11        Strategy::standard()
12    };
13    let engine = Engine::builder()
14        .builtin()
15        .strategy(strategy)
16        .build()
17        .unwrap();
18    let mut invalid = false;
19    for line in io::stdin().lock().lines() {
20        let line = line.unwrap();
21        let fields: Vec<_> = line.split('\t').collect();
22        if fields.len() != 4 {
23            panic!("expected id/width/input/reference");
24        }
25        let mut cx = Context::new();
26        let options = ParseOptions::width(Width::new(fields[1].parse().unwrap()).unwrap());
27        let result = (|| -> Result<_, Box<dyn std::error::Error>> {
28            let input = cx.parse(fields[2], &options)?;
29            let reference = cx.parse(fields[3], &options)?;
30            let before = cx.tree_size(input)?;
31            if !agrees(&mut cx, &[input, reference])? {
32                return Ok((
33                    "invalid-reference",
34                    before,
35                    before,
36                    cx.tree_size(reference)?,
37                    cx.display(input).to_string().replace(['\n', '\t'], " "),
38                    cx.display(reference).to_string().replace(['\n', '\t'], " "),
39                ));
40            }
41            let output = engine.simplify(&mut cx, input)?.expr;
42            let want = engine.simplify(&mut cx, reference)?.expr;
43            let after = cx.tree_size(output)?;
44            let target = cx.tree_size(want)?;
45            let status = if !agrees(&mut cx, &[input, reference, output, want])? {
46                "invalid-output"
47            } else if output == want {
48                "covered"
49            } else if after > target {
50                "gap"
51            } else {
52                "different-form"
53            };
54            Ok((
55                status,
56                before,
57                after,
58                target,
59                cx.display(output).to_string().replace(['\n', '\t'], " "),
60                cx.display(want).to_string().replace(['\n', '\t'], " "),
61            ))
62        })();
63        match result {
64            Ok((status, before, after, target, output, want)) => {
65                invalid |= status.starts_with("invalid-");
66                println!(
67                    "{}\t{}\t{status}\t{before}\t{after}\t{target}\t{output}\t{want}",
68                    fields[0], fields[1]
69                );
70            }
71            Err(error) => {
72                invalid = true;
73                println!(
74                    "{}\t{}\terror\t{}",
75                    fields[0],
76                    fields[1],
77                    error.to_string().replace(['\n', '\t'], " ")
78                );
79            }
80        }
81    }
82    if invalid {
83        std::process::exit(1);
84    }
85}
86
87// Refutation only, not a proof: exercise every limb, including bits above 64.
88fn agrees(cx: &mut Context, roots: &[bitwright::Expr]) -> Result<bool, bitwright::Error> {
89    for seed in 0..32_u64 {
90        let env = FnEnv(|key: &SymbolKey, width: Width| {
91            let mut state = format!("{key:?}")
92                .bytes()
93                .fold(seed.wrapping_mul(0x9e3779b97f4a7c15), |state, byte| {
94                    state.wrapping_mul(0x100000001b3) ^ u64::from(byte)
95                });
96            let limbs: Vec<_> = (0..width.bits().div_ceil(64))
97                .map(|_| {
98                    state = state.wrapping_add(0x9e3779b97f4a7c15);
99                    let mut value = state;
100                    value = (value ^ (value >> 30)).wrapping_mul(0xbf58476d1ce4e5b9);
101                    value = (value ^ (value >> 27)).wrapping_mul(0x94d049bb133111eb);
102                    value ^ (value >> 31)
103                })
104                .collect();
105            Some(match seed {
106                0 => BitVec::zero(width),
107                1 => BitVec::ones(width),
108                _ => BitVec::wrapping_from_limbs(width, &limbs),
109            })
110        });
111        let values = cx.eval(roots, &env)?;
112        if values.iter().any(|v| *v != values[0]) {
113            return Ok(false);
114        }
115    }
116    Ok(true)
117}
valeria_rule_audit/valeria_rule_audit.rs

valeria_rule_audit/
valeria_rule_audit.rs
