213 lines
8.5 KiB
Rust
213 lines
8.5 KiB
Rust
//! Writes the proof corpus as Kani harness crates, one per generated program: every graph of
|
|
//! `codegen::board::corpus::proof_graphs` (the board generator's corpus, the start screen's
|
|
//! microcontroller examples and the e2e firmware fixture) for every board the generator
|
|
//! covers, on both executors, each as the firmware flashed to the board would carry it. The crates form
|
|
//! one cargo workspace, so `cargo kani --workspace` compiles their shared dependencies once.
|
|
//! `tools/kani-programs.sh` runs it, then the proofs, then writes each `proofs.json`.
|
|
//!
|
|
//! ```text
|
|
//! cargo run -p flowrs-core --example program_proofs -- <out dir> <flowRS checkout> [graph...]
|
|
//! cargo run -p flowrs-core --example program_proofs -- --compare <committed> <run's> [--subset]
|
|
//! ```
|
|
//!
|
|
//! With graph names, only those corpus graphs are written; FLOWRS_PROOF_BOARDS (board ids,
|
|
//! comma-separated) keeps only those boards. It writes `<out>/Cargo.toml` (the
|
|
//! workspace), `<out>/<crate>/{Cargo.toml,src/lib.rs,proofs.json}` and `<out>/programs.json`
|
|
//! (one entry per program: its id, crate, graph, board, chip, family, target, harness,
|
|
//! unwinding bound, and the SHA-256 of its flow module and of its harness). A board that
|
|
//! refuses a graph is listed there with the refusal and no crate. `tools/kani_programs.py`
|
|
//! makes flowRS's proof table from it (`codegen::proof_table`).
|
|
|
|
use std::path::{Path, PathBuf};
|
|
|
|
use flowrs_core::codegen::board::{FirmwareOptions, Harness, corpus, family_of, generate};
|
|
use flowrs_core::codegen::mcu::{McuTarget, refusal_message};
|
|
use flowrs_core::codegen::proof::{ProgramMeta, flow_text, program_proof};
|
|
use serde_json::json;
|
|
|
|
fn fail(msg: &str) -> ! {
|
|
eprintln!("program_proofs: {msg}");
|
|
std::process::exit(1);
|
|
}
|
|
|
|
fn write(path: &Path, text: &str) {
|
|
if let Some(dir) = path.parent()
|
|
&& let Err(e) = std::fs::create_dir_all(dir)
|
|
{
|
|
fail(&format!("{}: {e}", dir.display()));
|
|
}
|
|
if let Err(e) = std::fs::write(path, text) {
|
|
fail(&format!("{}: {e}", path.display()));
|
|
}
|
|
}
|
|
|
|
/// `--compare COMMITTED NEW [--subset]`: hold a run's proof table to the committed one
|
|
/// (`codegen::proof_table::compare`); exit 1 on any difference.
|
|
fn compare(args: &[String]) -> ! {
|
|
use flowrs_core::codegen::proof_table;
|
|
let read = |p: &str| {
|
|
let text = std::fs::read_to_string(p).unwrap_or_else(|e| fail(&format!("{p}: {e}")));
|
|
proof_table::parse(&text).unwrap_or_else(|e| fail(&format!("{p}: {e}")))
|
|
};
|
|
let (Some(old), Some(new)) = (args.first(), args.get(1)) else {
|
|
fail("usage: program_proofs --compare <committed table> <run's table> [--subset]");
|
|
};
|
|
let (old, new) = (read(old), read(new));
|
|
let why = proof_table::compare(&old, &new, args.iter().any(|a| a == "--subset"));
|
|
for w in &why {
|
|
eprintln!("kani-programs: {w}");
|
|
}
|
|
if why.is_empty() {
|
|
println!(
|
|
"kani-programs: this run agrees with the proof table ({} programs)",
|
|
new.programs.len()
|
|
);
|
|
std::process::exit(0);
|
|
}
|
|
eprintln!(
|
|
"kani-programs: this run differs from the proof table in {} way(s); a whole-corpus run \
|
|
with KANI_PROGRAMS_WRITE=1 rewrites it ({}), for review",
|
|
why.len(),
|
|
proof_table::PATH
|
|
);
|
|
std::process::exit(1);
|
|
}
|
|
|
|
fn main() {
|
|
let args: Vec<String> = std::env::args().skip(1).collect();
|
|
if args.first().map(String::as_str) == Some("--compare") {
|
|
compare(&args[1..]);
|
|
}
|
|
if args.len() < 2 {
|
|
fail("usage: program_proofs <out dir> <flowRS checkout> [graph...]");
|
|
}
|
|
let out = PathBuf::from(&args[0]);
|
|
let hal = Path::new(&args[1])
|
|
.join("crates/flowrs-hal")
|
|
.canonicalize()
|
|
.unwrap_or_else(|e| fail(&format!("the flowrs-hal source under {}: {e}", args[1])));
|
|
let only: Vec<&str> = args[2..].iter().map(String::as_str).collect();
|
|
|
|
let reg = flowrs_boards::BoardRegistry::with_builtins();
|
|
let wanted: Vec<String> = std::env::var("FLOWRS_PROOF_BOARDS")
|
|
.map(|v| v.split(',').map(|b| b.trim().to_string()).collect())
|
|
.unwrap_or_default();
|
|
let mut boards: Vec<_> = reg
|
|
.boards()
|
|
.iter()
|
|
.filter(|b| family_of(b).is_ok())
|
|
.filter(|b| wanted.is_empty() || wanted.contains(&b.id))
|
|
.collect();
|
|
boards.sort_by(|a, b| a.id.cmp(&b.id));
|
|
|
|
let mut members = Vec::new();
|
|
let mut programs = Vec::new();
|
|
for board in boards {
|
|
let Ok((family, table)) = family_of(board) else {
|
|
continue;
|
|
};
|
|
for target in McuTarget::ALL {
|
|
for (name, graph) in corpus::proof_graphs() {
|
|
if !only.is_empty() && !only.contains(&name) {
|
|
continue;
|
|
}
|
|
let fw = match generate(
|
|
&graph,
|
|
target,
|
|
board,
|
|
&FirmwareOptions {
|
|
harness: Harness::Standalone,
|
|
link: None,
|
|
twin: false,
|
|
},
|
|
) {
|
|
Ok(fw) => fw,
|
|
Err(r) => {
|
|
programs.push(json!({
|
|
"graph": name,
|
|
"board": board.id,
|
|
"target": target.id(),
|
|
"refused": refusal_message(target, &r),
|
|
}));
|
|
continue;
|
|
}
|
|
};
|
|
// The program the harness proves is the one the firmware carries.
|
|
let flow = flow_text(&fw.lowered.source);
|
|
if !fw.main_rs.contains(&format!("mod flow {{\n{flow}}}\n")) {
|
|
fail(&format!(
|
|
"{name} on {} ({}): the firmware's mod flow is not the app's text",
|
|
board.id,
|
|
target.id()
|
|
));
|
|
}
|
|
let p = program_proof(
|
|
&fw.lowered,
|
|
target,
|
|
&ProgramMeta {
|
|
board: board.id.clone(),
|
|
chip: table.regdb.to_string(),
|
|
family: family.name().to_string(),
|
|
graph: Some(name.to_string()),
|
|
},
|
|
);
|
|
if p.flow_sha256 != fw.proof.flow_sha256
|
|
|| p.id != fw.proof.id
|
|
|| p.harness_sha256 != fw.proof.harness_sha256
|
|
{
|
|
fail(&format!(
|
|
"{name}: the firmware's proof names another program or harness"
|
|
));
|
|
}
|
|
let dir = out.join(&p.crate_name);
|
|
if p.harness.is_some() {
|
|
let manifest = p.cargo_toml.replace(
|
|
"\"<your flowRS checkout>/crates/flowrs-hal\"",
|
|
&format!("{:?}", hal.display().to_string()),
|
|
);
|
|
write(&dir.join("Cargo.toml"), &manifest);
|
|
write(&dir.join("src/lib.rs"), &p.lib_rs);
|
|
members.push(p.crate_name.clone());
|
|
}
|
|
write(&dir.join("proofs.json"), &p.manifest);
|
|
programs.push(json!({
|
|
"id": p.id,
|
|
"crate": p.crate_name,
|
|
"dir": p.crate_name,
|
|
"graph": name,
|
|
"board": board.id,
|
|
"chip": table.regdb,
|
|
"family": family.name(),
|
|
"target": target.id(),
|
|
"harness": p.harness,
|
|
"unwind": p.unwind,
|
|
"flow_sha256": p.flow_sha256,
|
|
"harness_sha256": p.harness_sha256,
|
|
"not_provable": p.not_provable,
|
|
}));
|
|
}
|
|
}
|
|
}
|
|
let list = members
|
|
.iter()
|
|
.map(|m| format!(" \"{m}\","))
|
|
.collect::<Vec<_>>()
|
|
.join("\n");
|
|
write(
|
|
&out.join("Cargo.toml"),
|
|
&format!(
|
|
"# The proof corpus as Kani harness crates (flowrs-core's\n\
|
|
# examples/program_proofs.rs); tools/kani-programs.sh proves them.\n\
|
|
[workspace]\nresolver = \"3\"\nmembers = [\n{list}\n]\n"
|
|
),
|
|
);
|
|
let text = serde_json::to_string_pretty(&programs)
|
|
.unwrap_or_else(|e| fail(&format!("programs.json: {e}")));
|
|
write(&out.join("programs.json"), &(text + "\n"));
|
|
println!(
|
|
"program_proofs: {} programs ({} with a harness) in {}",
|
|
programs.len(),
|
|
members.len(),
|
|
out.display()
|
|
);
|
|
}
|