436 lines
18 KiB
Rust
436 lines
18 KiB
Rust
//! flowRS's proof table (`codegen::proof_table`, `data/program-proofs.json`) is the proof
|
|
//! corpus as the generator writes it today: every program, by its two digests, refused where
|
|
//! the generator refuses, run by the pinned Kani. A generator change that alters any program's
|
|
//! `mod flow` (or its harness, or what a board refuses) fails here until the build host proves
|
|
//! the corpus again (`KANI_PROGRAMS_WRITE=1 tools/kani-programs.sh`), so no stale "proved" can
|
|
//! stand in the table; and an export's record names the program it is about.
|
|
|
|
use flowrs_core::codegen::board::{FirmwareOptions, Harness, corpus, family_of, generate};
|
|
use flowrs_core::codegen::mcu::{McuTarget, refusal_message};
|
|
use flowrs_core::codegen::proof::{self, KANI_PIN, ProgramMeta, Record, program_proof};
|
|
use flowrs_core::codegen::proof_table::{self, Entry};
|
|
use std::collections::BTreeMap;
|
|
|
|
const AGAIN: &str = "the proof table is stale: on the build host, run \
|
|
`KANI_PROGRAMS_WRITE=1 tools/kani-programs.sh` and commit crates/flowrs-core/data/program-proofs.json";
|
|
|
|
/// (graph, board, target).
|
|
type Key = (String, String, String);
|
|
/// (id, flow SHA-256, harness SHA-256).
|
|
type Generated = (String, String, String);
|
|
|
|
/// Every program of the proof corpus, as `examples/program_proofs.rs` generates it for
|
|
/// `tools/kani-programs.sh`: (graph, board, target) -> Ok((id, flow, harness)) or the refusal.
|
|
fn generated() -> BTreeMap<Key, Result<Generated, String>> {
|
|
let reg = flowrs_boards::BoardRegistry::with_builtins();
|
|
let mut out = BTreeMap::new();
|
|
for board in reg.boards() {
|
|
let Ok((family, table)) = family_of(board) else {
|
|
continue;
|
|
};
|
|
for target in McuTarget::ALL {
|
|
for (name, graph) in corpus::proof_graphs() {
|
|
let key = (name.to_string(), board.id.clone(), target.id().to_string());
|
|
let fw = generate(
|
|
&graph,
|
|
target,
|
|
board,
|
|
&FirmwareOptions {
|
|
harness: Harness::Standalone,
|
|
link: None,
|
|
twin: false,
|
|
},
|
|
);
|
|
let v = match fw {
|
|
Err(r) => Err(refusal_message(target, &r)),
|
|
Ok(fw) => {
|
|
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()),
|
|
},
|
|
);
|
|
// What the export ships names the same program and harness.
|
|
assert_eq!(p.flow_sha256, fw.proof.flow_sha256, "{key:?}");
|
|
assert_eq!(p.harness_sha256, fw.proof.harness_sha256, "{key:?}");
|
|
Ok((
|
|
p.id,
|
|
p.flow_sha256,
|
|
p.harness_sha256.expect("a corpus program has a harness"),
|
|
))
|
|
}
|
|
};
|
|
out.insert(key, v);
|
|
}
|
|
}
|
|
}
|
|
out
|
|
}
|
|
|
|
#[test]
|
|
#[ignore = "compares flowRS's proof scripts, which are not in this snapshot"]
|
|
fn the_table_reads_and_was_run_by_the_pinned_kani() {
|
|
let t = proof_table::table().expect("data/program-proofs.json is a proof table");
|
|
assert_eq!(t.schema, proof_table::SCHEMA);
|
|
assert!(proof_table::pinned(t), "{:?}: {AGAIN}", t.kani);
|
|
assert_eq!(t.run.by, "tools/kani-programs.sh");
|
|
assert!(!t.run.at.is_empty() && !t.run.host.is_empty());
|
|
// tools/kani-env.sh pins the same Kani the code holds a result to.
|
|
let env = std::fs::read_to_string(
|
|
std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../tools/kani-env.sh"),
|
|
)
|
|
.unwrap();
|
|
assert!(
|
|
env.lines().any(|l| l == format!("KANI_PIN={KANI_PIN}")),
|
|
"tools/kani-env.sh does not pin Kani {KANI_PIN}"
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn the_table_is_the_proof_corpus_the_generator_writes_today() {
|
|
let t = proof_table::table().expect("a proof table");
|
|
let table: BTreeMap<(String, String, String), &Entry> = t
|
|
.programs
|
|
.iter()
|
|
.map(|e| ((e.graph.clone(), e.board.clone(), e.target.clone()), e))
|
|
.collect();
|
|
assert_eq!(table.len(), t.programs.len(), "a program listed twice");
|
|
let now = generated();
|
|
let mut wrong = Vec::new();
|
|
for (key, want) in &now {
|
|
let Some(e) = table.get(key) else {
|
|
wrong.push(format!("{key:?}: not in the table"));
|
|
continue;
|
|
};
|
|
match want {
|
|
Err(why) => {
|
|
if e.status != "refused" || e.reason.as_deref() != Some(why.as_str()) {
|
|
wrong.push(format!(
|
|
"{key:?}: refused ({why}), the table says {} {:?}",
|
|
e.status, e.reason
|
|
));
|
|
}
|
|
}
|
|
Ok((id, flow, harness)) => {
|
|
if e.status == "refused" {
|
|
wrong.push(format!("{key:?}: generated now, refused in the table"));
|
|
} else if e.id.as_deref() != Some(id.as_str())
|
|
|| e.flow_sha256.as_deref() != Some(flow.as_str())
|
|
|| e.harness_sha256.as_deref() != Some(harness.as_str())
|
|
{
|
|
wrong.push(format!(
|
|
"{key:?}: now {id} (flow {}, harness {}), the table proved {:?} (flow \
|
|
{:?}, harness {:?})",
|
|
&flow[..12],
|
|
&harness[..12],
|
|
e.id,
|
|
e.flow_sha256,
|
|
e.harness_sha256
|
|
));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
for key in table.keys() {
|
|
if !now.contains_key(key) {
|
|
wrong.push(format!("{key:?}: in the table, no longer generated"));
|
|
}
|
|
}
|
|
assert!(wrong.is_empty(), "{AGAIN}:\n {}", wrong.join("\n "));
|
|
// The corpus has programs on every covered board, and the SparkFun Thing Plus's UART
|
|
// programs are generated (its UART is in flowrs-boards, from SparkFun's schematic).
|
|
for board in [
|
|
"nucleo_f401re",
|
|
"nucleo_g071rb",
|
|
"rpi_pico",
|
|
"feather_rp2040",
|
|
"sparkfun_thing_plus_rp2040",
|
|
] {
|
|
for g in [
|
|
"uart.read",
|
|
"uart.write (echo)",
|
|
"spi.transfer",
|
|
"i2c.write",
|
|
"mcuio (all but PWM)",
|
|
] {
|
|
for target in McuTarget::ALL {
|
|
let k = (g.to_string(), board.to_string(), target.id().to_string());
|
|
assert!(matches!(now.get(&k), Some(Ok(_))), "{k:?} is refused");
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn every_program_with_a_harness_has_a_result_and_a_proved_one_has_both_covers() {
|
|
let t = proof_table::table().expect("a proof table");
|
|
for e in &t.programs {
|
|
let n = format!("{} on {} ({})", e.graph, e.board, e.target);
|
|
if e.status == "refused" {
|
|
assert!(e.reason.is_some() && e.flow_sha256.is_none(), "{n}");
|
|
continue;
|
|
}
|
|
assert!(
|
|
["proved", "failed", "not_proved", "budget_exceeded"].contains(&e.status.as_str()),
|
|
"{n}: {}",
|
|
e.status
|
|
);
|
|
if e.status == "proved" {
|
|
let c = e.checks.expect("a proved program's checks");
|
|
let v = e.covers.expect("a proved program's covers");
|
|
assert!(c.failed == 0 && c.undetermined == 0, "{n}: {c:?}");
|
|
assert!(v.total >= 2 && v.satisfied == v.total, "{n}: {v:?}");
|
|
assert!(e.reason.is_none(), "{n}");
|
|
}
|
|
}
|
|
}
|
|
|
|
/// An export ships the table's result for its program, and only for its program: the record a
|
|
/// firmware's `proof/proofs.json` carries is the manifest with the result filled in, and a
|
|
/// manifest of another program (or another harness) is never filled.
|
|
#[test]
|
|
fn a_program_the_table_proved_ships_its_result_and_no_other_program_inherits_it() {
|
|
let reg = flowrs_boards::BoardRegistry::with_builtins();
|
|
let (_, graph) = corpus::proof_graphs()
|
|
.into_iter()
|
|
.find(|(n, _)| *n == "uart.write (echo)")
|
|
.unwrap();
|
|
let opts = FirmwareOptions {
|
|
harness: Harness::Standalone,
|
|
link: None,
|
|
twin: false,
|
|
};
|
|
let fw = generate(&graph, McuTarget::Rtic, reg.get("rpi_pico").unwrap(), &opts).unwrap();
|
|
let shipped = Record::parse(&fw.proof.proofs_json()).unwrap();
|
|
let h = &shipped.harnesses[0];
|
|
assert_eq!(h.status, "proved", "{h:?}");
|
|
assert_eq!(shipped.program.flow_sha256, fw.proof.flow_sha256);
|
|
assert_eq!(h.harness_sha256, fw.proof.harness_sha256);
|
|
assert_eq!(
|
|
shipped.kani.as_ref().unwrap().version.as_deref(),
|
|
Some(KANI_PIN)
|
|
);
|
|
let run = shipped.run.as_ref().unwrap();
|
|
assert_eq!(run["by"], "tools/kani-programs.sh");
|
|
assert_eq!(run["table"], proof_table::PATH);
|
|
assert_eq!(run["as"], "uart.write (echo)");
|
|
// The files the export writes carry exactly that record.
|
|
let files = fw.proof.files();
|
|
assert_eq!(
|
|
files.iter().map(|f| f.0.as_str()).collect::<Vec<_>>(),
|
|
["proof/Cargo.toml", "proof/src/lib.rs", "proof/proofs.json"]
|
|
);
|
|
assert_eq!(files[2].1, fw.proof.proofs_json());
|
|
assert_eq!(
|
|
proof::sha256_hex(&files[1].1),
|
|
h.harness_sha256.clone().unwrap()
|
|
);
|
|
|
|
// The same graph with one more node is another program: nothing is filled in.
|
|
let mut other = graph.clone();
|
|
let n = other.add_node("embedded.gpio.digital_out", 0.0, 0.0);
|
|
other
|
|
.get_node_mut(n)
|
|
.unwrap()
|
|
.properties
|
|
.insert("pin".into(), "21".into());
|
|
let fw2 = generate(&other, McuTarget::Rtic, reg.get("rpi_pico").unwrap(), &opts).unwrap();
|
|
assert_ne!(fw2.proof.flow_sha256, fw.proof.flow_sha256);
|
|
let r2 = Record::parse(&fw2.proof.proofs_json()).unwrap();
|
|
assert_eq!(r2.harnesses[0].status, "not_run");
|
|
assert!(r2.kani.is_none() && r2.run.is_none());
|
|
// A table entry is never filled into a manifest whose digests are not its own.
|
|
let (entry, table) = proof_table::lookup(
|
|
&fw.proof.flow_sha256,
|
|
fw.proof.harness_sha256.as_deref().unwrap(),
|
|
)
|
|
.unwrap();
|
|
assert!(proof_table::fill(&fw2.proof.manifest, entry, table).is_none());
|
|
// Nor is one found by the flow alone: a harness that differs (here, one cover dropped)
|
|
// has another digest.
|
|
let edited = fw
|
|
.proof
|
|
.lib_rs
|
|
.replace("kani::cover!(r.is_err()", "let _ = (r.is_err()");
|
|
assert!(proof_table::lookup(&fw.proof.flow_sha256, &proof::sha256_hex(&edited)).is_none());
|
|
}
|
|
|
|
#[test]
|
|
fn flow_of_finds_the_module_the_firmware_carries() {
|
|
let reg = flowrs_boards::BoardRegistry::with_builtins();
|
|
for (name, graph) in corpus::proof_graphs() {
|
|
for target in McuTarget::ALL {
|
|
let Ok(fw) = generate(
|
|
&graph,
|
|
target,
|
|
reg.get("nucleo_f401re").unwrap(),
|
|
&FirmwareOptions {
|
|
harness: Harness::Standalone,
|
|
link: None,
|
|
twin: false,
|
|
},
|
|
) else {
|
|
continue;
|
|
};
|
|
let flow = proof::flow_text(&fw.lowered.source);
|
|
assert_eq!(proof::flow_of(&fw.main_rs), Some(flow.as_str()), "{name}");
|
|
assert_eq!(
|
|
proof::flow_of(&fw.proof.lib_rs),
|
|
Some(flow.as_str()),
|
|
"{name}"
|
|
);
|
|
assert_eq!(proof::sha256_hex(&flow), fw.proof.flow_sha256, "{name}");
|
|
}
|
|
}
|
|
assert_eq!(proof::flow_of("no module here"), None);
|
|
assert_eq!(proof::flow_of("mod flow {\n fn a() {}\n"), None);
|
|
assert_eq!(
|
|
proof::flow_of("// x\nmod flow {\n fn a() {}\n}\nmod b {\n}\n"),
|
|
Some(" fn a() {}\n")
|
|
);
|
|
}
|
|
|
|
/// The e2e suite's document of the corpus's `digital_in+not` (`e2e/fixtures/firmware/
|
|
/// in_not_out.flowrs`, which `e2e/proofcarry.spec.js` opens in the editor) is that program, as
|
|
/// the table proved it, on every board and executor: the Code view shows it proved.
|
|
#[test]
|
|
fn the_e2e_document_of_a_corpus_graph_is_a_program_the_table_proved() {
|
|
let text = include_str!("../../../e2e/fixtures/firmware/in_not_out.flowrs");
|
|
let graph = flowrs_core::graph::document::load(text).unwrap();
|
|
let reg = flowrs_boards::BoardRegistry::with_builtins();
|
|
for board in ["nucleo_f401re", "rpi_pico"] {
|
|
for target in McuTarget::ALL {
|
|
let fw = generate(
|
|
&graph,
|
|
target,
|
|
reg.get(board).unwrap(),
|
|
&FirmwareOptions {
|
|
harness: Harness::Standalone,
|
|
link: None,
|
|
twin: false,
|
|
},
|
|
)
|
|
.unwrap();
|
|
let r = Record::parse(&fw.proof.proofs_json()).unwrap();
|
|
assert_eq!(r.harnesses[0].status, "proved", "{board} {}", target.id());
|
|
assert_eq!(r.run.unwrap()["as"], "digital_in+not");
|
|
}
|
|
}
|
|
}
|
|
|
|
/// The e2e suite's document of the frame DSP firmware (`e2e/fixtures/firmware/mcu_dsp.flowrs`,
|
|
/// which `e2e/mcu-dsp.spec.js` opens) is the exported fixture `mcu_dsp.fdsl`'s program, as the
|
|
/// table proved it, on the STM32F4 and the STM32G0 boards and the Pico, both executors.
|
|
#[test]
|
|
fn the_e2e_document_of_the_frame_dsp_firmware_is_a_program_the_table_proved() {
|
|
let text = include_str!("../../../e2e/fixtures/firmware/mcu_dsp.flowrs");
|
|
let graph = flowrs_core::graph::document::load(text).unwrap();
|
|
let reg = flowrs_boards::BoardRegistry::with_builtins();
|
|
for board in ["nucleo_f401re", "nucleo_g071rb", "rpi_pico"] {
|
|
for target in McuTarget::ALL {
|
|
let fw = generate(
|
|
&graph,
|
|
target,
|
|
reg.get(board).unwrap(),
|
|
&FirmwareOptions {
|
|
harness: Harness::Standalone,
|
|
link: None,
|
|
twin: false,
|
|
},
|
|
)
|
|
.unwrap_or_else(|r| panic!("{board} {}: {r:?}", target.id()));
|
|
let r = Record::parse(&fw.proof.proofs_json()).unwrap();
|
|
assert_eq!(r.harnesses[0].status, "proved", "{board} {}", target.id());
|
|
assert_eq!(r.run.unwrap()["as"], "e2e: mcu_dsp.fdsl");
|
|
}
|
|
}
|
|
}
|
|
|
|
/// An edit of a table's entry `usize`.
|
|
type Edit = fn(&mut proof_table::Table, usize);
|
|
|
|
/// A run's table is held to the committed one in what a result is (the gate's
|
|
/// `tools/kani-programs.sh`): a status, a check count, a cover, a digest, a program more or
|
|
/// fewer, or another Kani is a difference; time and peak memory are the run's own.
|
|
#[test]
|
|
fn a_run_that_departs_from_the_table_is_told_apart() {
|
|
let t = proof_table::table().unwrap().clone();
|
|
assert!(proof_table::compare(&t, &t, false).is_empty());
|
|
let first_proved = t
|
|
.programs
|
|
.iter()
|
|
.position(|e| e.status == "proved")
|
|
.unwrap();
|
|
let edits: [(&str, Edit); 9] = [
|
|
("status", |t, i| {
|
|
t.programs[i].status = "budget_exceeded".into()
|
|
}),
|
|
("checks", |t, i| {
|
|
t.programs[i].checks.as_mut().unwrap().passed -= 1;
|
|
}),
|
|
("covers", |t, i| {
|
|
t.programs[i].covers.as_mut().unwrap().satisfied -= 1;
|
|
}),
|
|
("flow_sha256", |t, i| {
|
|
t.programs[i].flow_sha256 = Some("0".repeat(64));
|
|
}),
|
|
("harness_sha256", |t, i| {
|
|
t.programs[i].harness_sha256 = Some("0".repeat(64));
|
|
}),
|
|
("reason", |t, i| t.programs[i].reason = Some("x".into())),
|
|
("unwind", |t, i| t.programs[i].unwind = Some(1)),
|
|
("Kani", |t, _| t.kani.version = Some("0.67.0".into())),
|
|
("not in the table", |t, i| {
|
|
let mut e = t.programs[i].clone();
|
|
e.graph.push_str(" (again)");
|
|
t.programs.push(e);
|
|
}),
|
|
];
|
|
for (what, edit) in edits {
|
|
let mut run = t.clone();
|
|
edit(&mut run, first_proved);
|
|
let why = proof_table::compare(&t, &run, false);
|
|
assert!(why.iter().any(|w| w.contains(what)), "{what}: {why:?}");
|
|
}
|
|
// A program missing from a whole run is a difference; from a run of some graphs it is not.
|
|
let mut part = t.clone();
|
|
part.programs.remove(first_proved);
|
|
assert!(!proof_table::compare(&t, &part, false).is_empty());
|
|
assert!(proof_table::compare(&t, &part, true).is_empty());
|
|
// Time and peak memory are the run's own.
|
|
let mut slower = t.clone();
|
|
slower.programs[first_proved].time_s = Some(1e6);
|
|
slower.programs[first_proved].peak_mem_gb = Some(99.0);
|
|
slower.run.wall_s = Some(1e6);
|
|
assert!(proof_table::compare(&t, &slower, false).is_empty());
|
|
}
|
|
|
|
/// The corpus and an export are proved with the same arguments: tools/kani-programs.sh's
|
|
/// `ARGS` (the corpus and the canary) is `codegen::proof::KANI_ARGS`, which `flowrsc prove`
|
|
/// passes too, and the script runs the canary before the corpus.
|
|
#[test]
|
|
#[ignore = "compares flowRS's proof scripts, which are not in this snapshot"]
|
|
fn the_corpus_the_canary_and_flowrsc_prove_run_kani_with_the_same_arguments() {
|
|
let script = std::fs::read_to_string(
|
|
std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../tools/kani-programs.sh"),
|
|
)
|
|
.unwrap();
|
|
let args = script
|
|
.lines()
|
|
.find(|l| l.starts_with("ARGS=("))
|
|
.expect("tools/kani-programs.sh sets ARGS");
|
|
assert_eq!(args, format!("ARGS=({})", proof::KANI_ARGS.join(" ")));
|
|
let canary = script
|
|
.find("cargo kani \"${ARGS[@]}\")")
|
|
.expect("the canary runs with ARGS");
|
|
let corpus = script
|
|
.find("cargo kani --workspace \"${ARGS[@]}\")")
|
|
.expect("the corpus runs with ARGS");
|
|
assert!(canary < corpus, "the canary runs first");
|
|
assert!(proof::KANI_ARGS.contains(&"--no-overflow-checks"));
|
|
assert!(proof::KANI_ARGS.contains(&"restrict-vtable"));
|
|
}
|