Skip to content

Fix exact Rust trace proof identity #7

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MauScheff merged 1 commit into from
Oct 20, 2026
Merged

Fix exact Rust trace proof identity #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
299 changes: 205 additions & 94 deletions tooling/rust/rms/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22032,6 +22032,11 @@ fn rust_trace_proof(
runner_symbol: &str,
target: Option<&str>,
) -> (bool, bool) {
// Source facts and #[path] resolution must use the same root identity.
let Ok(base) = fs::canonicalize(base) else {
return (false, false);
};
let base = base.as_path();
let mut functions = BTreeMap::<(PathBuf, String), RustTraceFunctionFacts>::new();
let mut paths_by_name = BTreeMap::<String, Vec<PathBuf>>::new();
let mut sources = BTreeMap::new();
Expand Down Expand Up @@ -22068,7 +22073,8 @@ fn rust_trace_proof(
.and_then(TomlValue::as_str)
.unwrap_or("src/lib.rs"),
);
let index = rust_proof_calls::Index::new(&sources, library.clone(), crate_name);
let index = rust_proof_calls::Index::new(&sources, library.clone(), crate_name)
.for_test_proof(&base.join(runner_path));
let target = target.and_then(|target| {
if let Some((path, symbol)) = binding_reference_parts(target) {
let resolved = index.resolve(&base.join(path), &[symbol.to_string()])?;
Expand Down Expand Up @@ -103885,142 +103891,247 @@ fn produce_transition_trace() {
}

#[test]
fn rust_trace_proof_resolves_exact_facade_and_path_aliased_serializer() {
let root = unique_test_dir("trace-proof-exact-rust-identity");
fn rust_trace_proof_tracks_declared_library_test_modules() {
let root = unique_test_dir("trace-library-test-modules");
fs::create_dir_all(root.join("src")).unwrap();
fs::create_dir_all(root.join("tests")).unwrap();
fs::write(
root.join("Cargo.toml"),
"[package]\nname = 'proof-owner'\nversion = '0.1.0'\n",
)
.unwrap();
fs::write(
root.join("src/lib.rs"),
"mod transition; pub use crate::transition::transition_record;",
"[package]\nname='proof-owner'\nversion='0.1.0'\nautotests=false\n",
)
.unwrap();
let library = "mod transition; #[cfg(test)] #[path=\"../tests/trace.rs\"] mod trace; #[cfg(test)] #[path=\"../tests/probe.rs\"] mod probe;";
fs::write(root.join("src/lib.rs"), library).unwrap();
fs::write(
root.join("src/transition.rs"),
"pub fn transition_record() -> Record { todo!() }",
)
.unwrap();
fs::write(
root.join("tests/machine_probe.rs"),
r#"
pub fn record_json(record: &Record) -> serde_json::Value {
serde_json::json!({"state_before":record.state_before,"state_after":record.state_after,
"input":record.input,"output":record.output,"source":record.source})
}"#,
)
.unwrap();
let source = r#"
use proof_owner::*;
#[path = "machine_probe.rs"] mod probe;
fn emit(records: &[Record]) {
let document = serde_json::json!({"records":records.iter().map(probe::record_json).collect::<Vec<_>>()});
std::fs::write("trace.json", serde_json::to_vec(&document).unwrap()).unwrap();
}
#[test]
fn produce() {
let mut records = vec![];
let record = proof_owner::transition_record();
records.push(record);
emit(&records);
}"#;
let runner = root.join("tests/trace_producer.rs");
fs::write(root.join("tests/probe.rs"), "pub fn record_json(record: &Record) -> Value { serde_json::json!({\"state_before\":record.state_before,\"state_after\":record.state_after,\"output\":record.output,\"source\":record.source}) }").unwrap();
let producer = "use crate::transition::transition_record; #[test] fn produce() { let records = vec![transition_record()]; let rows = records.iter().map(crate::probe::record_json).collect::<Vec<_>>(); std::fs::write(\"trace\",serde_json::to_vec(&rows).unwrap()); }";
fs::write(root.join("tests/trace.rs"), producer).unwrap();
let check = || {
rust_trace_proof(
&root,
"tests/trace_producer.rs",
"tests/trace.rs",
"produce",
Some("src/transition.rs#transition_record"),
)
};
fs::write(&runner, source).unwrap();
assert_eq!(check(), (true, true));
let sources = rust_source_files(&root)
.into_iter()
.map(|path| {
let source = fs::read_to_string(&path).unwrap();
(path, source)
})
.collect();
let production = rust_proof_calls::Index::new(
&sources,
root.join("src/lib.rs"),
Some("proof_owner".into()),
);
assert!(production
.resolve(
&root.join("src/lib.rs"),
&["trace".into(), "produce".into()]
)
.is_none());
assert!(production
.for_test_proof(&root.join("tests/trace.rs"))
.resolve(
&root.join("src/lib.rs"),
&["trace".into(), "produce".into()]
)
.is_some());
for invalid_library in [
"mod transition;", // Not attached to this library.
"mod transition; #[cfg(feature=\"optional\")] #[path=\"../tests/trace.rs\"] mod trace;",
"mod transition; #[cfg_attr(test, path=\"../tests/trace.rs\")] mod trace;",
"mod transition; #[path=\"../tests/trace.rs\"] mod first; #[path=\"../tests/trace.rs\"] mod second;",
] {
fs::write(root.join("src/lib.rs"), invalid_library).unwrap();
assert!(!check().0, "{invalid_library}");
}
fs::write(root.join("src/lib.rs"), library).unwrap();
fs::write(
&runner,
source.replace("proof_owner::transition_record()", "transition_record()"),
root.join("tests/probe.rs"),
"pub fn record_json(record: &Record) -> Value { serde_json::json!({}) }",
)
.unwrap();
assert_eq!(check(), (true, true));

// A same-name local function is not the canonical transition recorder.
assert_eq!(check(), (true, false));
fs::write(
&runner,
format!(
"{}\nfn transition_record() -> Record {{ todo!() }}",
source.replace("proof_owner::transition_record()", "transition_record()")
root.join("tests/trace.rs"),
producer.replace(
"use crate::transition::transition_record;",
"fn transition_record() -> Record { todo!() }",
),
)
.unwrap();
assert!(!check().0);
fs::write(
root.join("tests/impostor.rs"),
"pub fn transition_record() -> Record { todo!() }",
)
.unwrap();
fs::write(
&runner,
format!("#[path = \"impostor.rs\"] mod proof_owner;\n{source}"),
)
.unwrap();
assert!(!check().0);
fs::write(&runner, source).unwrap();
fs::write(
root.join("src/lib.rs"),
"mod wrong; pub use crate::wrong::transition_record;",
root.join("tests/trace.rs"),
producer.replace("use crate::transition::transition_record;", "use super::*;"),
)
.unwrap();
fs::write(root.join("src/lib.rs"), "mod transition;").unwrap();
fs::write(root.join("src/transition.rs"), "pub fn transition_record() -> Record { todo!() } #[cfg(test)] #[path=\"../tests/trace.rs\"] mod trace;").unwrap();
assert!(check().0);
fs::write(
root.join("src/wrong.rs"),
root.join("src/transition.rs"),
"pub fn transition_record() -> Record { todo!() }",
)
.unwrap();
fs::write(root.join("src/lib.rs"), "mod transition; mod wrong;").unwrap();
fs::write(root.join("src/wrong.rs"), "fn transition_record() -> Record { todo!() } #[cfg(test)] #[path=\"../tests/trace.rs\"] mod trace;").unwrap();
assert!(!check().0);
fs::write(
root.join("src/lib.rs"),
"mod transition; pub use crate::transition::transition_record;",
)
.unwrap();
fs::write(&runner, source.replace("machine_probe.rs", "missing.rs")).unwrap();
assert_eq!(check(), (true, false));
fs::write(
root.join("tests/wrong.rs"),
"pub fn record_json(record: &Record) -> Value { serde_json::json!({}) }",
)
.unwrap();
fs::write(&runner, source.replace("machine_probe.rs", "wrong.rs")).unwrap();
assert_eq!(check(), (true, false));
fs::remove_dir_all(root).unwrap();
}
#[test]
fn rust_trace_proof_resolves_exact_facade_and_path_aliased_serializer() {
let unique = unique_test_dir("trace-proof-exact-rust-identity");
let relative = PathBuf::from(unique.file_name().unwrap());
// Do not change process cwd: native tests run concurrently.
for root in [
std::env::current_dir().unwrap().join(&relative),
relative.clone(),
Path::new(".").join(&relative),
] {
fs::create_dir_all(root.join("src")).unwrap();
fs::create_dir_all(root.join("tests")).unwrap();
fs::write(
root.join("Cargo.toml"),
"[package]\nname = 'proof-owner'\nversion = '0.1.0'\n",
)
.unwrap();
fs::write(
root.join("src/lib.rs"),
"mod transition; pub use crate::transition::transition_record;",
)
.unwrap();
fs::write(
root.join("src/transition.rs"),
"pub fn transition_record() -> Record { todo!() }",
)
.unwrap();
fs::write(
root.join("tests/machine_probe.rs"),
r#"
pub fn record_json(record: &Record) -> serde_json::Value {
serde_json::json!({"state_before":record.state_before,"state_after":record.state_after,
"input":record.input,"output":record.output,"source":record.source})
}"#,
)
.unwrap();
let source = r#"
use proof_owner::*;
#[path = "machine_probe.rs"] mod probe;
fn emit(records: &[Record]) {
let document = serde_json::json!({"records":records.iter().map(probe::record_json).collect::<Vec<_>>()});
std::fs::write("trace.json", serde_json::to_vec(&document).unwrap()).unwrap();
}
#[test]
fn produce() {
let mut records = vec![];
let record = proof_owner::transition_record();
records.push(record);
emit(&records);
}"#;
let runner = root.join("tests/trace_producer.rs");
let check = || {
rust_trace_proof(
&root,
"tests/trace_producer.rs",
"produce",
Some("src/transition.rs#transition_record"),
)
};
fs::write(&runner, source).unwrap();
assert_eq!(check(), (true, true));
fs::write(
&runner,
source.replace("proof_owner::transition_record()", "transition_record()"),
)
.unwrap();
assert_eq!(check(), (true, true));

// Two inspectable imports cannot select a serializer by its leaf name.
fs::write(
root.join("tests/other.rs"),
fs::read_to_string(root.join("tests/machine_probe.rs")).unwrap(),
)
.unwrap();
fs::write(&runner, source.replace("#[path = \"machine_probe.rs\"] mod probe;", "#[path = \"machine_probe.rs\"] mod probe; mod other; use probe::*; use other::*;")
// A same-name local function is not the canonical transition recorder.
fs::write(
&runner,
format!(
"{}\nfn transition_record() -> Record {{ todo!() }}",
source.replace("proof_owner::transition_record()", "transition_record()")
),
)
.unwrap();
assert!(!check().0);
fs::write(
root.join("tests/impostor.rs"),
"pub fn transition_record() -> Record { todo!() }",
)
.unwrap();
fs::write(
&runner,
format!("#[path = \"impostor.rs\"] mod proof_owner;\n{source}"),
)
.unwrap();
assert!(!check().0);
fs::write(&runner, source).unwrap();
fs::write(
root.join("src/lib.rs"),
"mod wrong; pub use crate::wrong::transition_record;",
)
.unwrap();
fs::write(
root.join("src/wrong.rs"),
"pub fn transition_record() -> Record { todo!() }",
)
.unwrap();
assert!(!check().0);
fs::write(
root.join("src/lib.rs"),
"mod transition; pub use crate::transition::transition_record;",
)
.unwrap();
fs::write(&runner, source.replace("machine_probe.rs", "missing.rs")).unwrap();
assert_eq!(check(), (true, false));
fs::write(
root.join("tests/wrong.rs"),
"pub fn record_json(record: &Record) -> Value { serde_json::json!({}) }",
)
.unwrap();
fs::write(&runner, source.replace("machine_probe.rs", "wrong.rs")).unwrap();
assert_eq!(check(), (true, false));

// Two inspectable imports cannot select a serializer by its leaf name.
fs::write(
root.join("tests/other.rs"),
fs::read_to_string(root.join("tests/machine_probe.rs")).unwrap(),
)
.unwrap();
fs::write(&runner, source.replace("#[path = \"machine_probe.rs\"] mod probe;", "#[path = \"machine_probe.rs\"] mod probe; mod other; use probe::*; use other::*;")
.replace(".map(probe::record_json)", ".map(record_json)")).unwrap();
assert_eq!(check(), (true, false));
assert_eq!(check(), (true, false));

// Calling the recorder does not make a copied JSON document derived evidence.
fs::write(&runner, r#"use proof_owner::*;
// Calling the recorder does not make a copied JSON document derived evidence.
fs::write(&runner, r#"use proof_owner::*;
fn produce() {
let _record = proof_owner::transition_record();
let document = serde_json::json!({"records":[], "decoy":"record.state_before record.state_after record.output record.source"});
std::fs::write("trace.json", serde_json::to_vec(&document).unwrap()).unwrap();
}"#).unwrap();
assert_eq!(check(), (true, false));
fs::write(
&runner,
source.replace(
"let record = proof_owner::transition_record();",
"let proof_owner = fake; let record = proof_owner::transition_record();",
),
)
.unwrap();
assert!(!check().0);
fs::remove_dir_all(&root).unwrap();
assert_eq!(check(), (true, false));
fs::write(
&runner,
source.replace(
"let record = proof_owner::transition_record();",
"let proof_owner = fake; let record = proof_owner::transition_record();",
),
)
.unwrap();
assert!(!check().0);
fs::remove_dir_all(&root).unwrap();
}
}

#[test]
Expand Down
Loading
Loading