Add focus tactic for quickcheck so we can convert them to lec

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

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<String, String>) -> &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 {

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,95 @@ impl IsTactic for FocusTactic {
             }
         }
 
-        let base_lec = match &base.payload {
-            ObligationPayload::Lec(lec) => lec,
-            _ => return Err("focus tactic requires a Lec obligation".to_string()),
-        };
+        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),
+        }
+    }
+}
 
+impl FocusTactic {
+    fn apply_to_lec(&self, base: &LecObligation) -> Result<Vec<ProverObligation>, String> {
         let mut obligations: Vec<ProverObligation> = 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)
+    }
 
-        // 2) Skeleton with shared UFs for focused functions
-        {
-            let mut ob = ProverObligation {
-                selector_segment: "skeleton".to_string(),
+    fn apply_to_qc(&self, base: &QcObligation) -> Result<Vec<ProverObligation>, String> {
+        let mut obligations: Vec<ProverObligation> = 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 +217,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"));
+    }
 }