xlsynth_driver/proofs/
script.rs

1// SPDX-License-Identifier: Apache-2.0
2
3//! Script-driven obligation tree execution with selectors and tactics.
4
5use std::collections::HashMap;
6use std::io::Read;
7use std::path::PathBuf;
8
9use crate::proofs::obligations::ProverObligation;
10use crate::proofs::plans::{ObligationPlan, build_plan_from_obligations};
11use crate::proofs::tactics::{IsTactic, Tactic};
12use crate::prover::{ProverReport, ProverReportNode, TaskOutcome, run_prover_plan};
13use serde::{Deserialize, Serialize};
14use xlsynth_prover::prover::SolverChoice;
15
16pub type Selector = Vec<String>;
17
18fn root_selector() -> Selector {
19    vec!["root".to_string()]
20}
21fn join_selector(parent: &Selector, seg: &str) -> Selector {
22    let mut v = parent.clone();
23    v.push(seg.to_string());
24    v
25}
26fn selector_to_path(sel: &Selector) -> String {
27    sel.join("/")
28}
29
30#[derive(Clone, Debug, PartialEq, Eq)]
31pub enum NodeStatus {
32    Open,
33    Pending,
34    Solved,
35    Failed,
36}
37
38#[derive(Debug)]
39pub enum NodeKind {
40    Leaf(ProverObligation),
41    Internal {
42        #[allow(dead_code)]
43        tactic: Tactic,
44        children: Vec<OblNode>,
45        original: ProverObligation,
46    },
47}
48
49#[derive(Debug)]
50pub struct OblNode {
51    #[allow(dead_code)]
52    pub segment: String,
53    pub selector: Selector,
54    pub kind: NodeKind,
55    pub status: NodeStatus,
56    pub solve: bool,
57}
58
59impl OblNode {
60    pub fn leaf(seg: String, parent: &Selector, ob: ProverObligation) -> Self {
61        Self {
62            segment: seg.clone(),
63            selector: join_selector(parent, &seg),
64            kind: NodeKind::Leaf(ob),
65            status: NodeStatus::Open,
66            solve: false,
67        }
68    }
69}
70
71#[derive(Debug)]
72pub struct OblTreeConfig {
73    pub dslx_stdlib_path: Option<PathBuf>,
74    pub dslx_paths: Vec<PathBuf>,
75    pub solver: Option<SolverChoice>,
76    pub timeout_ms: Option<u64>,
77}
78
79#[derive(Debug)]
80pub struct OblTree {
81    pub root: OblNode,
82    pub config: OblTreeConfig,
83}
84
85impl OblTree {
86    pub fn new(mut root_obligation: ProverObligation, config: OblTreeConfig) -> Self {
87        // Ensure root obligation has selector segment = "root"
88        root_obligation.selector_segment = "root".to_string();
89        let root = OblNode {
90            segment: "root".to_string(),
91            selector: root_selector(),
92            kind: NodeKind::Leaf(root_obligation),
93            status: NodeStatus::Open,
94            solve: false,
95        };
96        Self { root, config }
97    }
98
99    fn find_mut<'a>(node: &'a mut OblNode, sel: &Selector) -> Option<&'a mut OblNode> {
100        if &node.selector == sel {
101            return Some(node);
102        }
103        if let NodeKind::Internal { children, .. } = &mut node.kind {
104            for c in children.iter_mut() {
105                if let Some(found) = Self::find_mut(c, sel) {
106                    return Some(found);
107                }
108            }
109        }
110        None
111    }
112
113    // Note: parent lookup is performed by computing the parent selector in the
114    // executor.
115}
116
117#[derive(Clone, Debug, Serialize, Deserialize)]
118pub enum Command {
119    Apply(Tactic),
120    Solve,
121}
122
123#[derive(Clone, Debug, Serialize, Deserialize)]
124pub struct ScriptStep {
125    pub selector: Selector,
126    pub command: Command,
127}
128
129fn apply_tactic(
130    node: &mut OblNode,
131    parent_selector: &Selector,
132    tactic: Tactic,
133) -> Result<(), String> {
134    let base = match &node.kind {
135        NodeKind::Leaf(ob) => ob.clone(),
136        _ => return Err("tactic requires a leaf".to_string()),
137    };
138    let children_obs = tactic.apply(&base)?;
139    let mut children: Vec<OblNode> = Vec::new();
140    for (idx, ob) in children_obs.into_iter().enumerate() {
141        if ob.selector_segment.is_empty() {
142            return Err(format!(
143                "tactic produced child {} with empty selector segment",
144                idx + 1
145            ));
146        }
147        let seg = ob.selector_segment.clone();
148        children.push(OblNode::leaf(seg, parent_selector, ob));
149    }
150    node.kind = NodeKind::Internal {
151        tactic,
152        children,
153        original: base,
154    };
155    Ok(())
156}
157
158fn collect_solve_targets(node: &OblNode, out: &mut Vec<(Selector, ProverObligation)>) {
159    match &node.kind {
160        NodeKind::Leaf(ob) => {
161            if node.solve {
162                out.push((node.selector.clone(), ob.clone()));
163            }
164        }
165        NodeKind::Internal { children, .. } => {
166            for c in children.iter() {
167                collect_solve_targets(c, out);
168            }
169        }
170    }
171}
172
173#[derive(Clone, Debug)]
174enum TaskSimple {
175    Success,
176    Failure,
177    Indefinite,
178}
179
180fn collect_outcomes(report: &ProverReportNode) -> HashMap<String, TaskSimple> {
181    let mut out: HashMap<String, TaskSimple> = HashMap::new();
182    match report {
183        ProverReportNode::Task {
184            task_id, outcome, ..
185        } => {
186            if let (Some(tid), Some(outcome_ref)) = (task_id, outcome) {
187                let simple = match outcome_ref {
188                    TaskOutcome::Normal { success: true } => TaskSimple::Success,
189                    TaskOutcome::Normal { success: false } => TaskSimple::Failure,
190                    TaskOutcome::Indefinite { .. } => TaskSimple::Indefinite,
191                };
192                out.insert(tid.clone(), simple);
193            }
194        }
195        ProverReportNode::Group { tasks, .. } => {
196            for t in tasks {
197                out.extend(collect_outcomes(t));
198            }
199        }
200    }
201    out
202}
203
204fn update_from_outcome(
205    tree: &mut OblTree,
206    report: &ProverReport,
207    sel: Selector,
208    path: &str,
209    status: Option<TaskSimple>,
210    solved: &mut Vec<Selector>,
211    failed_logs: &mut Vec<TaskLogEntry>,
212    indefinite_logs: &mut Vec<TaskLogEntry>,
213    rolled_back: &mut Vec<RollbackEntry>,
214) {
215    match status {
216        Some(TaskSimple::Success) => {
217            if let Some(n) = OblTree::find_mut(&mut tree.root, &sel) {
218                n.status = NodeStatus::Solved;
219            }
220            let _ = report.plan.find_task_node(path);
221            solved.push(sel);
222        }
223        Some(TaskSimple::Failure) => {
224            if let Some(n) = OblTree::find_mut(&mut tree.root, &sel) {
225                n.status = NodeStatus::Failed;
226            }
227            if let Some(task_node) = report.plan.find_task_node(path) {
228                if let ProverReportNode::Task {
229                    task_id,
230                    cmdline,
231                    stdout,
232                    stderr,
233                    ..
234                } = task_node
235                {
236                    println!(
237                        "FAILED TASK id={:?}\ncmd={}\nstdout=\n{}\nstderr=\n{}\n",
238                        task_id,
239                        cmdline.as_deref().unwrap_or(""),
240                        stdout.as_deref().unwrap_or(""),
241                        stderr.as_deref().unwrap_or("")
242                    );
243                    failed_logs.push(TaskLogEntry {
244                        selector: sel.clone(),
245                        stdout: stdout.clone(),
246                        stderr: stderr.clone(),
247                    });
248                }
249            }
250            if sel.len() > 1 {
251                let parent_sel: Selector = sel[..sel.len() - 1].to_vec();
252                if let Some(parent) = OblTree::find_mut(&mut tree.root, &parent_sel) {
253                    if let NodeKind::Internal { original, .. } = &parent.kind {
254                        let original_ob = original.clone();
255                        parent.kind = NodeKind::Leaf(original_ob);
256                        parent.status = NodeStatus::Open;
257                        parent.solve = false;
258                    }
259                    rolled_back.push(RollbackEntry {
260                        selector: parent_sel,
261                        reason_selector: sel,
262                    });
263                }
264            }
265        }
266        Some(TaskSimple::Indefinite) => {
267            if let Some(n) = OblTree::find_mut(&mut tree.root, &sel) {
268                n.status = NodeStatus::Pending;
269            }
270            if let Some(task_node) = report.plan.find_task_node(path) {
271                if let ProverReportNode::Task { stdout, stderr, .. } = task_node {
272                    indefinite_logs.push(TaskLogEntry {
273                        selector: sel,
274                        stdout: stdout.clone(),
275                        stderr: stderr.clone(),
276                    });
277                }
278            }
279        }
280        None => {
281            if let Some(n) = OblTree::find_mut(&mut tree.root, &sel) {
282                n.status = NodeStatus::Pending;
283            }
284        }
285    }
286}
287
288#[derive(Clone, Debug, Serialize, Deserialize)]
289pub struct TaskLogEntry {
290    pub selector: Selector,
291    pub stdout: Option<String>,
292    pub stderr: Option<String>,
293}
294
295#[derive(Clone, Debug, Serialize, Deserialize)]
296pub struct RollbackEntry {
297    pub selector: Selector,
298    pub reason_selector: Selector,
299}
300
301#[derive(Clone, Debug, Serialize, Deserialize)]
302pub struct ScriptReport {
303    pub solved: Vec<Selector>,
304    pub indefinite: Vec<TaskLogEntry>,
305    pub failed: Vec<TaskLogEntry>,
306    pub rolled_back: Vec<RollbackEntry>,
307}
308
309/// Parses a tactic script from a string as a JSON array of ScriptStep objects.
310pub fn parse_script_steps_from_json_str(input: &str) -> Result<Vec<ScriptStep>, String> {
311    serde_json::from_str::<Vec<ScriptStep>>(input)
312        .map_err(|e| format!("tactic script: expected JSON array of ScriptStep: {}", e))
313}
314
315/// Parses a tactic script from a string as JSONL (one ScriptStep JSON object
316/// per non-empty, non-comment line).
317pub fn parse_script_steps_from_jsonl_str(input: &str) -> Result<Vec<ScriptStep>, String> {
318    let mut steps: Vec<ScriptStep> = Vec::new();
319    for (lineno, line) in input.lines().enumerate() {
320        let line = line.trim();
321        if line.is_empty() {
322            continue;
323        }
324        if line.starts_with('#') {
325            continue;
326        }
327        match serde_json::from_str::<ScriptStep>(line) {
328            Ok(step) => steps.push(step),
329            Err(e) => {
330                return Err(format!(
331                    "tactic script (jsonl) parse error on line {}: {}",
332                    lineno + 1,
333                    e
334                ));
335            }
336        }
337    }
338    Ok(steps)
339}
340
341/// Reads the raw script text from a path ("-" for stdin) with contextualized
342/// errors.
343fn read_script_text_from_path(path: &str, kind: &str) -> Result<String, String> {
344    if path == "-" {
345        let mut buf = String::new();
346        std::io::stdin()
347            .read_to_string(&mut buf)
348            .map_err(|e| format!("failed to read tactic script ({} ) from stdin: {}", kind, e))?;
349        Ok(buf)
350    } else {
351        std::fs::read_to_string(path)
352            .map_err(|e| format!("failed to read tactic script ({}) {}: {}", kind, path, e))
353    }
354}
355
356/// Reads and parses a tactic script from a path ("-" for stdin) as JSON array.
357pub fn read_script_steps_from_json_path(path: &str) -> Result<Vec<ScriptStep>, String> {
358    let text = read_script_text_from_path(path, "json")?;
359    parse_script_steps_from_json_str(&text)
360}
361
362/// Reads and parses a tactic script from a path ("-" for stdin) as JSONL.
363pub fn read_script_steps_from_jsonl_path(path: &str) -> Result<Vec<ScriptStep>, String> {
364    let text = read_script_text_from_path(path, "jsonl")?;
365    parse_script_steps_from_jsonl_str(&text)
366}
367
368pub fn execute_script(tree: &mut OblTree, steps: &[ScriptStep]) -> Result<ScriptReport, String> {
369    // 1) Apply all tactics except Solve; mark Solve flags only.
370    for step in steps {
371        match &step.command {
372            Command::Solve => {
373                let node = OblTree::find_mut(&mut tree.root, &step.selector).ok_or_else(|| {
374                    format!("selector not found: {}", selector_to_path(&step.selector))
375                })?;
376                if !matches!(node.kind, NodeKind::Leaf(_)) {
377                    return Err("solve requires a leaf".to_string());
378                }
379                node.solve = true;
380            }
381            Command::Apply(tactic) => {
382                let node = OblTree::find_mut(&mut tree.root, &step.selector).ok_or_else(|| {
383                    format!("selector not found: {}", selector_to_path(&step.selector))
384                })?;
385                apply_tactic(node, &step.selector, tactic.clone())?;
386            }
387        }
388    }
389
390    // 2) Gather solve leaves and build obligations with selector paths.
391    let mut targets: Vec<(Selector, ProverObligation)> = Vec::new();
392    collect_solve_targets(&tree.root, &mut targets);
393    let mut obligations_with_ids: Vec<(String, ProverObligation)> = Vec::new();
394    for (sel, ob) in targets.iter() {
395        let path = selector_to_path(sel);
396        obligations_with_ids.push((path, ob.clone()));
397    }
398
399    log::debug!("obligations_to_solve={}", obligations_with_ids.len());
400
401    if obligations_with_ids.is_empty() {
402        return Ok(ScriptReport {
403            solved: vec![],
404            indefinite: vec![],
405            failed: vec![],
406            rolled_back: vec![],
407        });
408    }
409
410    // No special-case for skeleton-only; always execute the plan.
411
412    // 3) Build plan and run.
413    let stdlib = tree.config.dslx_stdlib_path.as_deref();
414    let paths: Vec<&std::path::Path> = tree.config.dslx_paths.iter().map(|p| p.as_path()).collect();
415    let plan_bundle: ObligationPlan = build_plan_from_obligations(
416        &obligations_with_ids,
417        stdlib,
418        &paths,
419        tree.config.solver.clone(),
420        tree.config.timeout_ms,
421    )?;
422    let (plan, tempdir) = plan_bundle.into_parts();
423    let _keep_tempdir = tempdir;
424    let cores = std::thread::available_parallelism()
425        .map(|n| n.get())
426        .unwrap_or(1);
427    let report: ProverReport = run_prover_plan(plan, cores).map_err(|e| e.to_string())?;
428
429    // 4) Map outcomes by task_id path.
430    let outcomes: HashMap<String, TaskSimple> = collect_outcomes(&report.plan);
431
432    // 5) Update node statuses and perform rollbacks.
433    let mut solved: Vec<Selector> = Vec::new();
434    let mut failed_logs: Vec<TaskLogEntry> = Vec::new();
435    let mut indefinite_logs: Vec<TaskLogEntry> = Vec::new();
436    let mut rolled_back: Vec<RollbackEntry> = Vec::new();
437
438    for (sel, _) in targets.into_iter() {
439        let path = selector_to_path(&sel);
440        let status = outcomes.get(&path).cloned();
441        update_from_outcome(
442            tree,
443            &report,
444            sel,
445            &path,
446            status,
447            &mut solved,
448            &mut failed_logs,
449            &mut indefinite_logs,
450            &mut rolled_back,
451        );
452    }
453
454    Ok(ScriptReport {
455        solved,
456        indefinite: indefinite_logs,
457        failed: failed_logs,
458        rolled_back,
459    })
460}
461
462#[cfg(test)]
463#[cfg(feature = "has-bitwuzla")]
464mod tests {
465    use super::*;
466    use crate::proofs::obligations::{
467        FileWithHistory, LecObligation, ObligationPayload, ProverObligation, SourceFile,
468    };
469    use crate::proofs::tactics::cosliced::{CoslicedTactic, NamedSlice};
470
471    fn sel(parts: &[&str]) -> Selector {
472        parts.iter().map(|s| s.to_string()).collect()
473    }
474
475    fn base_obligation() -> ProverObligation {
476        use crate::proofs::obligations::LecSide;
477        let dslx = "pub fn f(x: u8) -> u8 { x + u8:3 }".to_string();
478        let lhs = LecSide {
479            top_func: "f".to_string(),
480            uf_map: std::collections::BTreeMap::new(),
481            file: FileWithHistory {
482                base_source: SourceFile::Text(dslx.clone()),
483                edits: Vec::new(),
484                text: dslx.clone(),
485            },
486        };
487        let rhs = LecSide {
488            top_func: "f".to_string(),
489            uf_map: std::collections::BTreeMap::new(),
490            file: FileWithHistory {
491                base_source: SourceFile::Text(dslx.clone()),
492                edits: Vec::new(),
493                text: dslx,
494            },
495        };
496        ProverObligation {
497            selector_segment: "root".to_string(),
498            description: None,
499            payload: ObligationPayload::Lec(LecObligation { lhs, rhs }),
500        }
501    }
502
503    fn base_config() -> OblTreeConfig {
504        let mut cfg = OblTreeConfig {
505            dslx_stdlib_path: None,
506            dslx_paths: vec![],
507            solver: None,
508            timeout_ms: None,
509        };
510        cfg.solver = Some(SolverChoice::Bitwuzla);
511        cfg
512    }
513
514    #[test]
515    fn cosliced_then_solve_all_succeeds() {
516        let mut tree = OblTree::new(base_obligation(), base_config());
517        let s1 = vec![
518            NamedSlice {
519                func_name: "f_slice_1".to_string(),
520                code: SourceFile::Text("pub fn f_slice_1(x: u8) -> u8 { x + u8:1 }".to_string()),
521            },
522            NamedSlice {
523                func_name: "f_slice_2".to_string(),
524                code: SourceFile::Text("pub fn f_slice_2(x: u8) -> u8 { x + u8:2 }".to_string()),
525            },
526        ];
527        let s2 = vec![
528            NamedSlice {
529                func_name: "f_slice_1".to_string(),
530                code: SourceFile::Text("pub fn f_slice_1(x: u8) -> u8 { x + u8:1 }".to_string()),
531            },
532            NamedSlice {
533                func_name: "f_slice_2".to_string(),
534                code: SourceFile::Text("pub fn f_slice_2(x: u8) -> u8 { x + u8:2 }".to_string()),
535            },
536        ];
537        let c1 = NamedSlice {
538            func_name: "f_composed".to_string(),
539            code: SourceFile::Text(
540                "pub fn f_composed(x: u8) -> u8 { f_slice_2(f_slice_1(x)) }".to_string(),
541            ),
542        };
543        let c2 = NamedSlice {
544            func_name: "f_composed".to_string(),
545            code: SourceFile::Text(
546                "pub fn f_composed(x: u8) -> u8 { f_slice_2(f_slice_1(x)) }".to_string(),
547            ),
548        };
549        let mut steps = Vec::new();
550        steps.push(ScriptStep {
551            selector: root_selector(),
552            command: Command::Apply(Tactic::Cosliced(CoslicedTactic {
553                lhs_slices: s1,
554                rhs_slices: s2,
555                lhs_composed: c1,
556                rhs_composed: c2,
557            })),
558        });
559        // Solve all leaves produced by cosliced (including skeleton)
560        for seg in ["lhs_self", "rhs_self", "slice_1", "slice_2", "skeleton"] {
561            steps.push(ScriptStep {
562                selector: sel(&["root", seg]).clone(),
563                command: Command::Solve,
564            });
565        }
566
567        execute_script(&mut tree, &steps).expect("execute_script");
568        // Gather statuses from the tree
569        fn walk(
570            n: &OblNode,
571            solved: &mut Vec<Selector>,
572            failed: &mut Vec<Selector>,
573            pending: &mut Vec<Selector>,
574        ) {
575            match n.status {
576                NodeStatus::Solved => solved.push(n.selector.clone()),
577                NodeStatus::Failed => failed.push(n.selector.clone()),
578                NodeStatus::Pending => pending.push(n.selector.clone()),
579                _ => {}
580            }
581            if let NodeKind::Internal { children, .. } = &n.kind {
582                for c in children {
583                    walk(c, solved, failed, pending);
584                }
585            }
586        }
587        let mut solved = Vec::new();
588        let mut failed = Vec::new();
589        let mut pending = Vec::new();
590        walk(&tree.root, &mut solved, &mut failed, &mut pending);
591        assert!(failed.is_empty(), "some tasks failed: {:?}", failed);
592        assert!(pending.is_empty(), "some tasks pending: {:?}", pending);
593        let solved_paths: std::collections::HashSet<String> =
594            solved.iter().map(|s| selector_to_path(s)).collect();
595        for seg in ["lhs_self", "rhs_self", "slice_1", "slice_2", "skeleton"] {
596            if !solved_paths.contains(&format!("root/{}", seg)) {
597                println!("missing solved {}", seg);
598            }
599            assert!(
600                solved_paths.contains(&format!("root/{}", seg)),
601                "missing solved {}",
602                seg
603            );
604        }
605    }
606}
xlsynth_driver/proofs/script.rs

xlsynth_driver/proofs/
script.rs
