use std::borrow::Cow;
use std::collections::HashMap;
use std::path::{Path, PathBuf};
use super::Prover;
use super::quickcheck::{
PreparedQuickCheckBackend, PreparedQuickCheckSuite, QuickCheckError, QuickCheckErrorKind,
QuickCheckProofResult, QuickCheckProperty, load_quickcheck_context,
};
use super::types::{
AssertionSemantics, BoolPropertyResult, EquivParallelism, EquivResult, ProverFn,
QuickCheckAssertionSemantics, QuickCheckOptions,
};
use crate::toolchain_shim::run_prove_quickcheck_main;
use regex::escape;
use xlsynth_pir::prove_equiv_via_toolchain::{self, ToolchainEquivResult};
const MAX_TOOLCHAIN_MESSAGE: usize = 512;
pub enum ExternalProver {
ToolExe(PathBuf),
ToolDir(PathBuf),
Toolchain,
}
fn resolve_tool_path(prover: &ExternalProver, exe_name: &str) -> Result<PathBuf, String> {
let (candidate, label) = match prover {
ExternalProver::ToolExe(path) => (path.clone(), "tool executable".to_string()),
ExternalProver::ToolDir(dir) => (dir.join(exe_name), exe_name.to_string()),
ExternalProver::Toolchain => match std::env::var("XLSYNTH_TOOLS") {
Ok(dir) => (PathBuf::from(dir).join(exe_name), exe_name.to_string()),
Err(_) => {
return Err("XLSYNTH_TOOLS is not set; cannot locate external tool".to_string());
}
},
};
if candidate.exists() {
Ok(candidate)
} else {
Err(format!("{label} not found at {}", candidate.display()))
}
}
impl Prover for ExternalProver {
fn prove_ir_fn_equiv(
self: &Self,
lhs: &xlsynth_pir::ir::Fn,
rhs: &xlsynth_pir::ir::Fn,
) -> EquivResult {
let lhs = ProverFn::new(lhs, None);
let rhs = ProverFn::new(rhs, None);
self.prove_ir_equiv(
&lhs,
&rhs,
EquivParallelism::SingleThreaded,
AssertionSemantics::Ignore,
None,
false,
)
}
fn prove_ir_pkg_text_equiv(
self: &Self,
lhs_pkg_text: &str,
rhs_pkg_text: &str,
top: Option<&str>,
) -> EquivResult {
match self {
ExternalProver::ToolExe(path) => {
prove_equiv_via_toolchain::prove_ir_pkg_equiv_with_tool_exe(
lhs_pkg_text,
rhs_pkg_text,
top,
path,
)
.into()
}
ExternalProver::ToolDir(path) => {
prove_equiv_via_toolchain::prove_ir_pkg_equiv_with_tool_dir(
lhs_pkg_text,
rhs_pkg_text,
top,
path,
)
.into()
}
ExternalProver::Toolchain => match std::env::var("XLSYNTH_TOOLS") {
Ok(dir) => ExternalProver::ToolDir(PathBuf::from(dir)).prove_ir_pkg_text_equiv(
lhs_pkg_text,
rhs_pkg_text,
top,
),
Err(_) => EquivResult::Error(
"XLSYNTH_TOOLS is not set; cannot run toolchain equivalence".to_string(),
),
},
}
}
fn prove_ir_equiv<'a>(
self: &Self,
lhs: &ProverFn<'a>,
rhs: &ProverFn<'a>,
strategy: EquivParallelism,
assertion_semantics: AssertionSemantics,
assert_label_filter: Option<&str>,
allow_flatten: bool,
) -> EquivResult {
if !lhs.uf_map.is_empty() || !rhs.uf_map.is_empty() {
return EquivResult::Error("External provers do not support UFs".to_string());
}
match strategy {
EquivParallelism::SingleThreaded => {
if lhs.fixed_implicit_activation || rhs.fixed_implicit_activation {
return EquivResult::Error(
"External provers do not support fixed implicit activation".to_string(),
);
}
if lhs.has_domains() || rhs.has_domains() {
return EquivResult::Error(
"External provers do not support parameter domains".to_string(),
);
}
if assertion_semantics != AssertionSemantics::Ignore {
return EquivResult::Error(
"External provers require assertion_semantics=ignore".to_string(),
);
}
if assert_label_filter.is_some() {
return EquivResult::Error(
"External provers do not support assertion label filters".to_string(),
);
}
if allow_flatten {
return EquivResult::Error(
"External provers do not support flattening".to_string(),
);
}
let lhs_pkg = match lhs.pkg_ref {
Some(pkg) => pkg.to_string(),
None => format!("package lhs\n\ntop {}\n", lhs.fn_ref.to_string()),
};
let rhs_pkg = match rhs.pkg_ref {
Some(pkg) => pkg.to_string(),
None => format!("package rhs\n\ntop {}\n", rhs.fn_ref.to_string()),
};
let (lhs_unified, rhs_unified, unified_top) =
unify_toolchain_tops(&lhs_pkg, &rhs_pkg, &lhs.fn_ref.name, &rhs.fn_ref.name);
self.prove_ir_pkg_text_equiv(&lhs_unified, &rhs_unified, Some(&unified_top))
}
EquivParallelism::OutputBits => {
if assert_label_filter.is_some() {
return EquivResult::Error(
"External provers do not support assertion label filters".to_string(),
);
}
EquivResult::Error(
"External provers do not support output-bits parallel strategy".to_string(),
)
}
EquivParallelism::InputBitSplit => {
if assert_label_filter.is_some() {
return EquivResult::Error(
"External provers do not support assertion label filters".to_string(),
);
}
EquivResult::Error(
"External provers do not support input-bit split strategy".to_string(),
)
}
}
}
fn prove_ir_quickcheck<'a>(
self: &Self,
_ir_fn: &ProverFn<'a>,
_assertion_semantics: QuickCheckAssertionSemantics,
assert_label_filter: Option<&str>,
) -> BoolPropertyResult {
if assert_label_filter.is_some() {
return BoolPropertyResult::ToolchainDisproved(
"External provers do not support assertion label filters".to_string(),
);
}
BoolPropertyResult::ToolchainDisproved(
"External provers do not support IR-level quickcheck; use prove_dslx_quickcheck"
.to_string(),
)
}
fn prepare_dslx_quickchecks(
&self,
entry_file: &Path,
dslx_stdlib_path: Option<&Path>,
additional_search_paths: &[&Path],
test_filter: Option<&str>,
assertion_semantics: QuickCheckAssertionSemantics,
assert_label_filter: Option<&str>,
uf_map: &HashMap<String, String>,
options: QuickCheckOptions,
) -> Result<PreparedQuickCheckSuite<'_>, QuickCheckError> {
let exe = if assertion_semantics != QuickCheckAssertionSemantics::Never {
Err("External quickcheck requires assertion_semantics=never".to_string())
} else if assert_label_filter.is_some() {
Err("External quickcheck does not support assertion label filters".to_string())
} else if !uf_map.is_empty() {
Err("External quickcheck does not support uninterpreted functions".to_string())
} else if !options.optimize {
Err("The XLS toolchain always optimizes QuickCheck IR; use an in-process solver to disable optimization".to_string())
} else {
resolve_tool_path(self, "prove_quickcheck_main")
}.map_err(|message| QuickCheckError::new(QuickCheckErrorKind::Configuration, message))?;
let context = load_quickcheck_context(
entry_file,
dslx_stdlib_path,
additional_search_paths,
test_filter,
)?;
let backend = ExternalQuickChecks {
exe,
entry_file: entry_file.into(),
source: context.source.clone(),
stdlib: dslx_stdlib_path.map(Path::to_path_buf),
search_paths: additional_search_paths
.iter()
.map(|p| p.to_path_buf())
.collect(),
};
Ok(PreparedQuickCheckSuite::new(context, Box::new(backend)))
}
}
struct ExternalQuickChecks {
exe: PathBuf,
entry_file: PathBuf,
source: String,
stdlib: Option<PathBuf>,
search_paths: Vec<PathBuf>,
}
impl PreparedQuickCheckBackend for ExternalQuickChecks {
fn prove(&self, property: &QuickCheckProperty) -> QuickCheckProofResult {
let result = match std::fs::read_to_string(&self.entry_file) {
Ok(source) if source == self.source => {
let filter = format!("^{}$", escape(&property.name));
let paths: Vec<_> = self.search_paths.iter().map(PathBuf::as_path).collect();
match run_prove_quickcheck_main(
&self.exe,
&self.entry_file,
self.stdlib.as_deref(),
&paths,
&filter,
) {
Ok(_) => BoolPropertyResult::Proved,
Err(message) => BoolPropertyResult::ToolchainDisproved(
message.chars().take(MAX_TOOLCHAIN_MESSAGE).collect(),
),
}
}
Ok(_) => BoolPropertyResult::Error(
"DSLX input changed after QuickCheck preparation; prepare the suite again".into(),
),
Err(error) => {
BoolPropertyResult::Error(format!("Failed to read prepared DSLX input: {error}"))
}
};
QuickCheckProofResult {
implicit_token: false,
result,
}
}
}
impl From<ToolchainEquivResult> for EquivResult {
fn from(result: ToolchainEquivResult) -> Self {
match result {
ToolchainEquivResult::Proved => EquivResult::Proved,
ToolchainEquivResult::Disproved(msg) => EquivResult::ToolchainDisproved(msg),
ToolchainEquivResult::TimedOutOrInterrupted(msg) => EquivResult::Inconclusive(msg),
ToolchainEquivResult::Error(msg) => EquivResult::Error(msg),
}
}
}
fn unify_toolchain_tops<'a>(
lhs_ir: &'a str,
rhs_ir: &'a str,
lhs_top: &str,
rhs_top: &str,
) -> (Cow<'a, str>, Cow<'a, str>, String) {
if lhs_top == rhs_top {
return (
Cow::Borrowed(lhs_ir),
Cow::Borrowed(rhs_ir),
lhs_top.to_string(),
);
}
let unified = lhs_top.to_string();
let rhs_rewritten = rhs_ir.replace(rhs_top, &unified);
(Cow::Borrowed(lhs_ir), Cow::Owned(rhs_rewritten), unified)
}
#[cfg(test)]
mod tests {
use super::*;
use xlsynth_pir::ir_parser::Parser;
#[test]
fn fn_equiv_convenience_uses_supported_assertion_semantics() {
let ir = r#"package test
fn f(x: bits[1] id=1) -> bits[1] {
ret identity.2: bits[1] = identity(x, id=2)
}
"#;
let pkg = Parser::new(ir).parse_and_validate_package().unwrap();
let f = pkg.get_fn("f").unwrap();
let tool_dir = tempfile::tempdir().unwrap();
let prover = ExternalProver::ToolDir(tool_dir.path().to_path_buf());
let result = prover.prove_ir_fn_equiv(f, f);
assert!(matches!(
result,
EquivResult::Error(msg) if msg.contains("check_ir_equivalence_main not found")
));
}
}