From bac425064e4d42ba40f6959d8c379efaa0241853 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Wed, 12 Nov 2025 11:14:22 -0800 Subject: [PATCH 1/2] Add focus tactic for quickcheck so we can convert them to lec --- xlsynth-driver/tests/invoke_test.rs | 121 ++++++++++++ .../src/dslx_tactics/obligations.rs | 15 +- .../src/dslx_tactics/tactics/focus.rs | 173 +++++++++++++++--- 3 files changed, 278 insertions(+), 31 deletions(-) diff --git a/xlsynth-driver/tests/invoke_test.rs b/xlsynth-driver/tests/invoke_test.rs index fd690e4c..edc3a02d 100644 --- a/xlsynth-driver/tests/invoke_test.rs +++ b/xlsynth-driver/tests/invoke_test.rs @@ -3887,6 +3887,127 @@ fn test_prove_quickcheck_script_mode() { ); } +#[cfg_attr(feature="has-boolector", test_case("boolector"; "boolector_success"))] +#[cfg_attr(feature="has-bitwuzla", test_case("bitwuzla"; "bitwuzla_success"))] +#[cfg_attr(feature="with-z3-binary-test", test_case("z3-binary"; "z3_binary_success"))] +#[cfg_attr(feature="with-bitwuzla-binary-test", test_case("bitwuzla-binary"; "bitwuzla_bin_success"))] +#[cfg_attr(feature="with-boolector-binary-test", test_case("boolector-binary"; "boolector_bin_success"))] +fn test_prove_quickcheck_focus_tactic_transforms_to_lec(solver: &str) { + use std::collections::BTreeMap; + use xlsynth_driver::proofs::obligations::{ + FileWithHistory, ObligationPayload, ProverObligation, QcObligation, + }; + use xlsynth_driver::proofs::script::{Command, ScriptStep}; + use xlsynth_driver::proofs::tactics::focus::{FocusPair, FocusTactic}; + use xlsynth_driver::proofs::tactics::IsTactic; + use xlsynth_driver::proofs::tactics::Tactic; + + let _ = env_logger::builder().is_test(true).try_init(); + + const FOCUS_QC_DSLX: &str = r#" +fn lhs(x: u32) -> u32 { x + u32:1 } +fn rhs(x: u32) -> u32 { x + u32:1 } + +#[quickcheck] +fn prop_equiv(x: u32) -> bool { + lhs(x) == rhs(x) +} +"#; + + let temp_dir = tempfile::tempdir().unwrap(); + let dslx_path = temp_dir.path().join("focus_qc.x"); + std::fs::write(&dslx_path, FOCUS_QC_DSLX).unwrap(); + + let focus_tactic = FocusTactic { + pairs: vec![FocusPair { + lhs: "lhs".to_string(), + rhs: "rhs".to_string(), + }], + }; + + // Preview the obligations produced by the focus tactic so we can inspect the + // specialized DSLX prior to invoking the driver. + let preview_base = ProverObligation { + selector_segment: "root".to_string(), + description: None, + payload: ObligationPayload::QuickCheck(QcObligation { + file: FileWithHistory::from_text(FOCUS_QC_DSLX), + tests: vec!["prop_equiv".to_string()], + uf_map: BTreeMap::new(), + }), + }; + let preview_obligations = focus_tactic + .apply(&preview_base) + .expect("preview focus application should succeed"); + for ob in &preview_obligations { + if let ObligationPayload::Lec(lec) = &ob.payload { + println!( + "[preview] obligation {} LHS file:\n{}", + ob.selector_segment, lec.lhs.file.text + ); + println!( + "[preview] obligation {} RHS file:\n{}", + ob.selector_segment, lec.rhs.file.text + ); + } + } + + let steps = vec![ + ScriptStep { + selector: vec!["root".to_string()], + command: Command::Apply(Tactic::Focus(focus_tactic.clone())), + }, + ScriptStep { + selector: vec!["root".to_string(), "pair_1".to_string()], + command: Command::Solve, + }, + ScriptStep { + selector: vec!["root".to_string(), "skeleton".to_string()], + command: Command::Solve, + }, + ]; + let script_json = serde_json::to_string(&steps).unwrap(); + let script_path = temp_dir.path().join("focus_script.json"); + std::fs::write(&script_path, script_json).unwrap(); + + let toolchain_toml = temp_dir.path().join("xlsynth-toolchain.toml"); + let toolchain_contents = add_tool_path_value("[toolchain]\n"); + std::fs::write(&toolchain_toml, toolchain_contents).unwrap(); + + let driver = env!("CARGO_BIN_EXE_xlsynth-driver"); + let output = std::process::Command::new(driver) + .arg("--toolchain") + .arg(toolchain_toml.to_str().unwrap()) + .arg("prove-quickcheck") + .arg("--dslx_input_file") + .arg(dslx_path.to_str().unwrap()) + .arg("--test_filter") + .arg("prop_equiv") + .arg("--solver") + .arg(solver) + .arg("--tactic_json") + .arg(script_path.to_str().unwrap()) + .output() + .expect("prove-quickcheck focus tactic invocation should run"); + + let stdout = String::from_utf8_lossy(&output.stdout); + println!("focus tactic stdout:\n{}", stdout); + println!( + "focus tactic stderr:\n{}", + String::from_utf8_lossy(&output.stderr) + ); + assert!( + output.status.success(), + "prove-quickcheck focus tactic run should succeed. stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + assert!( + stdout.contains("[prove-quickcheck] success: QuickCheck obligations proved"), + "unexpected stdout: {}", + stdout + ); +} + // Parameterized version of the multi-quickcheck test that explicitly invokes // each solver (external or SMT backend) to ensure the fallback to // implicit-token mangled names works with each configured solver backend. Only diff --git a/xlsynth-prover/src/dslx_tactics/obligations.rs b/xlsynth-prover/src/dslx_tactics/obligations.rs index d8649250..5e5ae388 100644 --- a/xlsynth-prover/src/dslx_tactics/obligations.rs +++ b/xlsynth-prover/src/dslx_tactics/obligations.rs @@ -134,6 +134,11 @@ impl LecObligation { self.rhs.uf_map.insert(right.to_string(), uf.to_string()); self } + + pub fn set_next_uf_alias(&mut self, left: &str, right: &str, uf: &str) -> &mut Self { + let next_uf = format!("{uf}_{}", self.lhs.uf_map.len() + 1); + self.set_uf_alias(left, right, &next_uf) + } } impl QcObligation { @@ -156,10 +161,16 @@ impl QcObligation { self } - pub fn set_uf_map(&mut self, map: BTreeMap) -> &mut Self { - self.uf_map = map; + pub fn set_uf_alias(&mut self, left: &str, right: &str, uf: &str) -> &mut Self { + self.uf_map.insert(left.to_string(), uf.to_string()); + self.uf_map.insert(right.to_string(), uf.to_string()); self } + + pub fn set_next_uf_alias(&mut self, left: &str, right: &str, uf: &str) -> &mut Self { + let next_uf = format!("{uf}_{}", self.uf_map.len() + 1); + self.set_uf_alias(left, right, &next_uf) + } } impl ProverObligation { diff --git a/xlsynth-prover/src/dslx_tactics/tactics/focus.rs b/xlsynth-prover/src/dslx_tactics/tactics/focus.rs index ffa3f7e7..831e8cdd 100644 --- a/xlsynth-prover/src/dslx_tactics/tactics/focus.rs +++ b/xlsynth-prover/src/dslx_tactics/tactics/focus.rs @@ -3,7 +3,10 @@ //! Focus tactic: prove a set of function pairs equivalent and a skeleton //! equivalence with those functions abstracted as shared UFs. -use crate::dslx_tactics::obligations::{ObligationPayload, ProverObligation, Side}; +use crate::dslx_tactics::obligations::{ + FileWithHistory, LecObligation, LecSide, ObligationPayload, ProverObligation, QcObligation, + Side, +}; use crate::dslx_tactics::tactics::IsTactic; use crate::dslx_tactics::tactics::utils::is_valid_ident; use serde::{Deserialize, Serialize}; @@ -35,53 +38,97 @@ impl IsTactic for FocusTactic { } } - let base_lec = match &base.payload { - ObligationPayload::Lec(lec) => lec, - _ => return Err("focus tactic requires a Lec obligation".to_string()), - }; + match &base.payload { + ObligationPayload::Lec(lec) => self.apply_to_lec(lec), + ObligationPayload::QuickCheck(qc) => self.apply_to_qc(qc), + } + } +} +impl FocusTactic { + fn apply_to_lec(&self, base: &LecObligation) -> Result, String> { let mut obligations: Vec = Vec::new(); - // 1) Per-pair equivalence checks - for (idx, p) in self.pairs.iter().enumerate() { - let mut ob = ProverObligation { + for (idx, pair) in self.pairs.iter().enumerate() { + let mut lec = base.clone(); + lec.set_top(Side::Lhs, &pair.lhs); + lec.set_top(Side::Rhs, &pair.rhs); + obligations.push(ProverObligation { selector_segment: format!("pair_{}", idx + 1), description: None, - payload: ObligationPayload::Lec(base_lec.clone()), - }; - if let ObligationPayload::Lec(lec) = &mut ob.payload { - lec.set_top(Side::Lhs, &p.lhs); - lec.set_top(Side::Rhs, &p.rhs); - } - obligations.push(ob); + payload: ObligationPayload::Lec(lec), + }); + } + + let mut skeleton = base.clone(); + for pair in self.pairs.iter() { + skeleton.set_next_uf_alias(&pair.lhs, &pair.rhs, "__uf_focus"); + } + obligations.push(ProverObligation { + selector_segment: "skeleton".to_string(), + description: None, + payload: ObligationPayload::Lec(skeleton), + }); + + Ok(obligations) + } + + fn apply_to_qc(&self, base: &QcObligation) -> Result, String> { + if self.pairs.is_empty() { + return Err( + "focus tactic requires at least one pair for QuickCheck obligations".to_string(), + ); } - // 2) Skeleton with shared UFs for focused functions - { - let mut ob = ProverObligation { - selector_segment: "skeleton".to_string(), + let mut obligations: Vec = Vec::new(); + + for (idx, pair) in self.pairs.iter().enumerate() { + obligations.push(ProverObligation { + selector_segment: format!("pair_{}", idx + 1), description: None, - payload: ObligationPayload::Lec(base_lec.clone()), - }; - if let ObligationPayload::Lec(lec) = &mut ob.payload { - for (idx, p) in self.pairs.iter().enumerate() { - let uf = format!("__uf_focus_{}", idx + 1); - lec.set_uf_alias(&p.lhs, &p.rhs, &uf); - } - } - obligations.push(ob); + payload: ObligationPayload::Lec(self.qc_pair_to_lec(base, pair)), + }); } + let mut skeleton = base.clone(); + for pair in self.pairs.iter() { + skeleton.set_next_uf_alias(&pair.lhs, &pair.rhs, "__uf_focus"); + } + obligations.push(ProverObligation { + selector_segment: "skeleton".to_string(), + description: None, + payload: ObligationPayload::QuickCheck(skeleton), + }); + Ok(obligations) } + + fn qc_pair_to_lec(&self, base: &QcObligation, pair: &FocusPair) -> LecObligation { + // let stripped_text = Self::strip_quickcheck_functions(&base.file.text); + let file = FileWithHistory::from_text(&base.file.text); + LecObligation { + lhs: LecSide { + top_func: pair.lhs.clone(), + uf_map: base.uf_map.clone(), + file: file.clone(), + }, + rhs: LecSide { + top_func: pair.rhs.clone(), + uf_map: base.uf_map.clone(), + file, + }, + } + } } #[cfg(test)] mod tests { use super::*; use crate::dslx_tactics::obligations::{ - FileWithHistory, LecObligation, LecSide, ObligationPayload, ProverObligation, SourceFile, + FileWithHistory, LecObligation, LecSide, ObligationPayload, ProverObligation, QcObligation, + SourceFile, }; + use std::collections::BTreeMap; fn base_obligation_with(sel: &str) -> ProverObligation { let lhs = LecSide { @@ -172,4 +219,72 @@ mod tests { Some("__uf_focus_2") ); } + + #[test] + fn transforms_quickcheck_into_lec_and_qc_skeleton() { + let qc = QcObligation { + file: FileWithHistory::from_text( + "pub fn lhs(x: u32) -> u32 { x + u32:1 }\n\ + pub fn rhs(x: u32) -> u32 { x + u32:1 }\n", + ), + tests: vec!["prop_equiv".to_string()], + uf_map: BTreeMap::from([("shared".to_string(), "UF_SHARED".to_string())]), + }; + let base = ProverObligation { + selector_segment: "root".to_string(), + description: None, + payload: ObligationPayload::QuickCheck(qc), + }; + let t = FocusTactic { + pairs: vec![FocusPair { + lhs: "lhs".to_string(), + rhs: "rhs".to_string(), + }], + }; + + let obs = t.apply(&base).expect("quickcheck focus"); + assert_eq!(obs.len(), 2); + + let pair = obs + .iter() + .find(|o| o.selector_segment == "pair_1") + .expect("pair obligation"); + let pair_lec = match &pair.payload { + ObligationPayload::Lec(lec) => lec, + _ => panic!("expected Lec payload"), + }; + assert_eq!(pair_lec.lhs.top_func, "lhs"); + assert_eq!(pair_lec.rhs.top_func, "rhs"); + assert_eq!( + pair_lec.lhs.uf_map.get("shared").map(|s| s.as_str()), + Some("UF_SHARED") + ); + assert_eq!( + pair_lec.rhs.uf_map.get("shared").map(|s| s.as_str()), + Some("UF_SHARED") + ); + + let skeleton = obs + .iter() + .find(|o| o.selector_segment == "skeleton") + .expect("skeleton obligation"); + let skeleton_qc = match &skeleton.payload { + ObligationPayload::QuickCheck(qc) => qc, + _ => panic!("expected QuickCheck payload"), + }; + assert_eq!( + skeleton_qc.uf_map.get("shared").map(|s| s.as_str()), + Some("UF_SHARED") + ); + assert_eq!( + skeleton_qc.uf_map.get("lhs").map(|s| s.as_str()), + Some("__uf_focus_2") + ); + assert_eq!( + skeleton_qc.uf_map.get("rhs").map(|s| s.as_str()), + Some("__uf_focus_2") + ); + assert!(skeleton_qc.file.text.contains("pub fn lhs")); + assert!(skeleton_qc.file.text.contains("pub fn rhs")); + } } From d31da208189eab3757c66799de0170c4a628cfcd Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Wed, 12 Nov 2025 11:17:42 -0800 Subject: [PATCH 2/2] Make at least one pair requirement applied to both lec and qc --- xlsynth-prover/src/dslx_tactics/tactics/focus.rs | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/xlsynth-prover/src/dslx_tactics/tactics/focus.rs b/xlsynth-prover/src/dslx_tactics/tactics/focus.rs index 831e8cdd..4bb835ad 100644 --- a/xlsynth-prover/src/dslx_tactics/tactics/focus.rs +++ b/xlsynth-prover/src/dslx_tactics/tactics/focus.rs @@ -38,6 +38,10 @@ impl IsTactic for FocusTactic { } } + if self.pairs.is_empty() { + return Err("focus tactic requires at least one pair".to_string()); + } + match &base.payload { ObligationPayload::Lec(lec) => self.apply_to_lec(lec), ObligationPayload::QuickCheck(qc) => self.apply_to_qc(qc), @@ -74,12 +78,6 @@ impl FocusTactic { } fn apply_to_qc(&self, base: &QcObligation) -> Result, String> { - if self.pairs.is_empty() { - return Err( - "focus tactic requires at least one pair for QuickCheck obligations".to_string(), - ); - } - let mut obligations: Vec = Vec::new(); for (idx, pair) in self.pairs.iter().enumerate() {