rickub
nandi/rustnimpublic⑂ Fork 0
⑂ 12c0a01b02392b18af24b583ba4ff65ad040e86a
Branches
main View all branches → View all tags →
Commits
⬇ Clone ▾
git clone https://git.rickub.com/nandi/rustnim.git
git clone ssh://git@rickub.com/nandi/rustnim.git

Host key fingerprint (ed25519): SHA256:iycHnxEyq0Q7uyVpB7JlznP0G7JrTPXLYRcAU5CSLhc — verify it before your first connect.

proof.rs · 177 lines · 5.6 KBRust Blame HistoryRaw
Prove byte-identity for base16ct by enumerating whole input domains 99b8376 nandithebull 18h ago1//! The exhaustive differential check described in `PROOF.md`.
2//!
3//! This is separate from `tests/differential.rs` because it is a different
4//! kind of claim. That runner asks whether a handful of hand-written cases
5//! agree; this one enumerates *entire input domains* — every two-byte input
6//! to the decoder, every two-byte input to the encoder, every single byte
7//! through `encode_str` and `HexDisplay` — and compares the complete output
8//! of both programs byte for byte.
9//!
10//! The driver in `proof/main.rs` references base16ct's own module files in
11//! place, so this cannot drift from what `tests/cases/026-base16ct-crate/`
12//! transpiles.
13
14use std::fs;
15use std::io::Write as _;
16use std::path::{Path, PathBuf};
17use std::process::{Command, Stdio};
18
19const RUSTNIM: &str = env!("CARGO_BIN_EXE_rustnim");
20
21fn find_nim() -> PathBuf {
22 if let Ok(p) = std::env::var("RUSTNIM_NIM") {
23 return PathBuf::from(p);
24 }
25 let mut dir: Option<&Path> = Some(Path::new(env!("CARGO_MANIFEST_DIR")));
26 while let Some(d) = dir {
27 let c = d.join(".nim-toolchain/bin/nim");
28 if c.is_file() {
29 return c;
30 }
31 dir = d.parent();
32 }
33 panic!("no .nim-toolchain/bin/nim found; set RUSTNIM_NIM");
34}
35
36fn sh(cmd: &mut Command, what: &str) -> Vec<u8> {
37 let out = cmd
38 .stdout(Stdio::piped())
39 .stderr(Stdio::piped())
40 .output()
41 .unwrap_or_else(|e| panic!("{what}: spawn: {e}"));
42 if !out.status.success() {
43 let mut msg = String::from_utf8_lossy(&out.stderr).into_owned();
44 if msg.trim().is_empty() {
45 msg = String::from_utf8_lossy(&out.stdout).into_owned();
46 }
47 panic!("{what} failed ({:?}):\n{}", out.status.code(), tail(&msg));
48 }
49 out.stdout
50}
51
52fn tail(s: &str) -> String {
53 let v: Vec<&str> = s.trim_end().lines().collect();
54 v[v.len().saturating_sub(25)..].join("\n")
55}
56
57/// Report the first differing line, and how many lines differ in total.
58fn first_difference(a: &[u8], b: &[u8]) -> String {
59 let (sa, sb) = (String::from_utf8_lossy(a), String::from_utf8_lossy(b));
60 let (la, lb): (Vec<_>, Vec<_>) = (sa.lines().collect(), sb.lines().collect());
61 let mut first = None;
62 let mut count = 0usize;
63 for i in 0..la.len().max(lb.len()) {
64 if la.get(i) != lb.get(i) {
65 count += 1;
66 if first.is_none() {
67 first = Some(i);
68 }
69 }
70 }
71 match first {
72 None => format!("{} vs {} bytes, but every line matches", a.len(), b.len()),
73 Some(i) => format!(
74 "{count} line(s) differ; first at line {}:\n rustc: {:?}\n nim : {:?}",
75 i + 1,
76 la.get(i),
77 lb.get(i)
78 ),
79 }
80}
81
82#[test]
83fn base16ct_is_byte_identical_over_the_enumerated_domains() {
84 let root = Path::new(env!("CARGO_MANIFEST_DIR"));
85 let work = root.join("tests/.work/proof");
86 let _ = fs::remove_dir_all(&work);
87 fs::create_dir_all(&work).unwrap();
88
89 let driver = root.join("proof/main.rs");
90 let crate_dir = root.join("tests/cases/026-base16ct-crate");
91 let mut modules: Vec<PathBuf> = fs::read_dir(&crate_dir)
92 .unwrap()
93 .filter_map(|e| e.ok().map(|e| e.path()))
94 .filter(|p| {
95 p.extension().is_some_and(|x| x == "rs")
96 && p.file_name().is_some_and(|f| f != "main.rs")
97 })
98 .collect();
99 modules.sort();
100 assert!(
101 modules.len() == 5,
102 "expected base16ct's five module files, found {:?}",
103 modules
104 );
105
106 // -- rustc: the oracle.
107 let rs_bin = work.join("rs");
108 sh(
109 Command::new("rustc")
110 .arg("--edition=2021")
111 .arg("--cfg")
112 .arg("feature=\"alloc\"")
113 .arg("-A")
114 .arg("warnings")
115 .arg(&driver)
116 .arg("-o")
117 .arg(&rs_bin)
118 .env("TMPDIR", &work),
119 "rustc",
120 );
121 let expected = sh(&mut Command::new(&rs_bin).env("TMPDIR", &work), "the Rust binary");
122
123 // -- rustnim, then Nim.
124 let nim_src = work.join("proof.nim");
125 let mut t = Command::new(RUSTNIM);
126 t.arg(&driver);
127 for m in &modules {
128 t.arg(m);
129 }
130 t.arg("--cfg")
131 .arg("feature=alloc")
132 .arg("-o")
133 .arg(&nim_src)
134 .env("TMPDIR", &work);
135 sh(&mut t, "rustnim");
136
137 let meta = fs::metadata(&nim_src).expect("rustnim wrote no output file");
138 assert!(meta.len() > 0, "rustnim wrote an empty output file");
139
140 let nim_bin = work.join("nim");
141 sh(
142 Command::new(find_nim())
143 .arg("c")
144 .arg("--hints:off")
145 .arg("--warnings:off")
146 .arg("--colors:off")
147 .arg(format!("--nimcache:{}", work.join("cache").display()))
148 .arg(format!("-o:{}", nim_bin.display()))
149 .arg(&nim_src)
150 .env("TMPDIR", &work),
151 "nim c",
152 );
153 let actual = sh(&mut Command::new(&nim_bin).env("TMPDIR", &work), "the Nim binary");
154
155 // The output must be substantial: an empty or truncated run agreeing with
156 // an empty or truncated run would otherwise read as success, which is the
157 // exact failure this project exists to avoid.
158 let lines = expected.iter().filter(|b| **b == b'\n').count();
159 assert!(
160 lines > 150_000 && expected.ends_with(b"done\n"),
161 "the oracle did not run to completion: {lines} lines, {} bytes",
162 expected.len()
163 );
164
165 assert!(
166 expected == actual,
167 "outputs differ.\n{}",
168 first_difference(&expected, &actual)
169 );
170
171 let _ = writeln!(
172 std::io::stderr(),
173 "proof: {} cases, {} bytes of output, byte-identical",
174 lines,
175 expected.len()
176 );
177}