karpal_verify/
session.rs

1// Copyright (C) 2026 Industrial Algebra
2// SPDX-License-Identifier: Apache-2.0
3
4use crate::{
5    ArtifactLayout, DryRunner, LeanConfig, LeanManifestReportFiles, LocalProcessRunner,
6    ObligationBundle, SmtConfig, VerificationReport, VerifierRunner, dry_run_bundle_artifacts,
7    dry_run_report, execute_report, write_bundle_artifacts,
8};
9#[cfg(feature = "amari")]
10use crate::{StatisticalVerification, ThreeTierVerificationReport, three_tier_report};
11use std::{fs, io, path::Path, string::String};
12
13/// Schema version for CI-oriented verification sidecar/report-file metadata.
14pub const VERIFICATION_SIDECAR_SCHEMA_VERSION: &str = "1";
15
16/// Default file stem used for CI-oriented verification summaries.
17pub const DEFAULT_REPORT_STEM: &str = "verification-report";
18
19/// Paths written for CI-oriented report summaries.
20#[derive(Debug, Clone, PartialEq, Eq)]
21pub struct ReportFiles {
22    pub json_path: String,
23    pub markdown_path: String,
24    pub lean_diagnostics_json_path: Option<String>,
25    pub lean_manifest_path: Option<String>,
26    pub three_tier_json_path: Option<String>,
27    pub three_tier_markdown_path: Option<String>,
28}
29
30/// End-to-end verification session configuration for a bundle.
31#[derive(Debug, Clone)]
32pub struct VerificationSession {
33    bundle: ObligationBundle,
34    layout: ArtifactLayout,
35    lean_module_name: String,
36    smt: SmtConfig,
37    lean: LeanConfig,
38    report_stem: String,
39    #[cfg(feature = "amari")]
40    statistical_verifications: Vec<StatisticalVerification>,
41}
42
43impl VerificationSession {
44    pub fn new(
45        bundle: ObligationBundle,
46        layout: ArtifactLayout,
47        lean_module_name: impl Into<String>,
48    ) -> Self {
49        Self {
50            bundle,
51            layout,
52            lean_module_name: lean_module_name.into(),
53            smt: SmtConfig::default(),
54            lean: LeanConfig::default(),
55            report_stem: DEFAULT_REPORT_STEM.into(),
56            #[cfg(feature = "amari")]
57            statistical_verifications: Vec::new(),
58        }
59    }
60
61    pub fn with_smt_config(mut self, smt: SmtConfig) -> Self {
62        self.smt = smt;
63        self
64    }
65
66    pub fn with_lean_config(mut self, lean: LeanConfig) -> Self {
67        self.lean = lean;
68        self
69    }
70
71    pub fn with_report_stem(mut self, report_stem: impl Into<String>) -> Self {
72        self.report_stem = report_stem.into();
73        self
74    }
75
76    #[cfg(feature = "amari")]
77    pub fn with_statistical_verification(mut self, verification: StatisticalVerification) -> Self {
78        self.statistical_verifications.push(verification);
79        self
80    }
81
82    #[cfg(feature = "amari")]
83    pub fn with_statistical_verifications(
84        mut self,
85        verifications: impl IntoIterator<Item = StatisticalVerification>,
86    ) -> Self {
87        self.statistical_verifications.extend(verifications);
88        self
89    }
90
91    pub fn bundle(&self) -> &ObligationBundle {
92        &self.bundle
93    }
94
95    pub fn layout(&self) -> &ArtifactLayout {
96        &self.layout
97    }
98
99    pub fn lean_module_name(&self) -> &str {
100        &self.lean_module_name
101    }
102
103    pub fn report_stem(&self) -> &str {
104        &self.report_stem
105    }
106
107    /// Build dry-run artifacts and return the attached verification report.
108    pub fn dry_run_report(&self) -> VerificationReport {
109        let artifacts = dry_run_bundle_artifacts(
110            &self.bundle,
111            &self.layout,
112            &self.lean_module_name,
113            &self.smt,
114            &self.lean,
115        );
116        dry_run_report(&self.bundle, &artifacts)
117    }
118
119    /// Build artifacts, execute plans, and return the resulting verification report.
120    pub fn verify_report(&self, runner: &impl VerifierRunner) -> io::Result<VerificationReport> {
121        let artifacts = write_bundle_artifacts(
122            &self.bundle,
123            &self.layout,
124            &self.lean_module_name,
125            &self.smt,
126            &self.lean,
127        )?;
128        Ok(execute_report(&self.bundle, &artifacts, runner))
129    }
130
131    /// Build artifacts, execute plans locally, and return the resulting verification report.
132    pub fn verify_local_report(&self) -> io::Result<VerificationReport> {
133        self.verify_report(&LocalProcessRunner)
134    }
135
136    /// Build artifacts, execute plans, and write JSON / Markdown summaries beside them.
137    pub fn verify_with_ci_outputs(
138        &self,
139        runner: &impl VerifierRunner,
140    ) -> io::Result<VerificationOutput> {
141        let artifacts = write_bundle_artifacts(
142            &self.bundle,
143            &self.layout,
144            &self.lean_module_name,
145            &self.smt,
146            &self.lean,
147        )?;
148        let report = execute_report(&self.bundle, &artifacts, runner);
149        let report_files = write_report_files(
150            &self.layout.root,
151            &self.report_stem,
152            &self.bundle,
153            &report,
154            artifacts.lean_manifest.as_ref(),
155            #[cfg(feature = "amari")]
156            &self.statistical_verifications,
157        )?;
158        Ok(VerificationOutput {
159            report,
160            report_files,
161        })
162    }
163
164    /// Build artifacts, execute plans locally, and write CI-oriented summaries.
165    pub fn verify_local_with_ci_outputs(&self) -> io::Result<VerificationOutput> {
166        self.verify_with_ci_outputs(&LocalProcessRunner)
167    }
168
169    /// Build artifacts via the real writer, then execute a dry-run runner.
170    pub fn verify_with_dry_runner(&self) -> io::Result<VerificationReport> {
171        self.verify_report(&DryRunner)
172    }
173}
174
175/// Report plus the CI-oriented files written beside generated artifacts.
176#[derive(Debug, Clone, PartialEq, Eq)]
177pub struct VerificationOutput {
178    pub report: VerificationReport,
179    pub report_files: ReportFiles,
180}
181
182/// One-shot orchestration helper.
183pub fn verify_bundle(
184    bundle: &ObligationBundle,
185    layout: &ArtifactLayout,
186    lean_module_name: &str,
187    smt: &SmtConfig,
188    lean: &LeanConfig,
189    runner: &impl VerifierRunner,
190) -> io::Result<VerificationReport> {
191    VerificationSession::new(bundle.clone(), layout.clone(), lean_module_name)
192        .with_smt_config(smt.clone())
193        .with_lean_config(lean.clone())
194        .verify_report(runner)
195}
196
197/// One-shot orchestration helper that also writes CI-oriented report files.
198pub fn verify_bundle_with_ci_outputs(
199    bundle: &ObligationBundle,
200    layout: &ArtifactLayout,
201    lean_module_name: &str,
202    smt: &SmtConfig,
203    lean: &LeanConfig,
204    runner: &impl VerifierRunner,
205) -> io::Result<VerificationOutput> {
206    VerificationSession::new(bundle.clone(), layout.clone(), lean_module_name)
207        .with_smt_config(smt.clone())
208        .with_lean_config(lean.clone())
209        .verify_with_ci_outputs(runner)
210}
211
212fn write_report_files(
213    root: impl AsRef<Path>,
214    report_stem: &str,
215    bundle: &ObligationBundle,
216    report: &VerificationReport,
217    lean_manifest: Option<&crate::artifact::LeanManifest>,
218    #[cfg(feature = "amari")] statistical_verifications: &[StatisticalVerification],
219) -> io::Result<ReportFiles> {
220    #[cfg(not(feature = "amari"))]
221    let _ = bundle;
222    let root = root.as_ref();
223    fs::create_dir_all(root)?;
224
225    let lean_manifest_path = report.lean_module.as_ref().map(|module| {
226        path_to_string(
227            &root
228                .join("lean")
229                .join(format!("{}.manifest.json", module.module_name)),
230        )
231    });
232
233    let lean_diagnostics_json_path = report
234        .lean_module
235        .as_ref()
236        .map(|_| -> io::Result<String> {
237            let path = root.join(format!("{report_stem}.lean-diagnostics.json"));
238            fs::write(&path, render_lean_diagnostics_json(report))?;
239            Ok(path_to_string(&path))
240        })
241        .transpose()?;
242
243    #[cfg(feature = "amari")]
244    let three_tier = (!statistical_verifications.is_empty())
245        .then(|| three_tier_report(bundle, statistical_verifications, Some(report)));
246    #[cfg(feature = "amari")]
247    let three_tier_json_path = if let Some(three_tier) = &three_tier {
248        let path = root.join(format!("{report_stem}.three-tier.json"));
249        fs::write(
250            &path,
251            render_three_tier_json_with_links(three_tier, report_stem, root),
252        )?;
253        Some(path_to_string(&path))
254    } else {
255        None
256    };
257    #[cfg(feature = "amari")]
258    let three_tier_markdown_path = if let Some(three_tier) = &three_tier {
259        let path = root.join(format!("{report_stem}.three-tier.md"));
260        fs::write(
261            &path,
262            render_three_tier_markdown_with_links(three_tier, report_stem, root),
263        )?;
264        Some(path_to_string(&path))
265    } else {
266        None
267    };
268    #[cfg(not(feature = "amari"))]
269    let three_tier_json_path = None;
270    #[cfg(not(feature = "amari"))]
271    let three_tier_markdown_path = None;
272
273    let json_path = root.join(format!("{report_stem}.json"));
274    let markdown_path = root.join(format!("{report_stem}.md"));
275    let report_files = ReportFiles {
276        json_path: path_to_string(&json_path),
277        markdown_path: path_to_string(&markdown_path),
278        lean_diagnostics_json_path,
279        lean_manifest_path,
280        three_tier_json_path,
281        three_tier_markdown_path,
282    };
283    fs::write(
284        &json_path,
285        render_report_json_with_links(report, &report_files),
286    )?;
287    fs::write(
288        &markdown_path,
289        render_report_markdown_with_links(report, &report_files),
290    )?;
291    if let (Some(path), Some(manifest)) = (&report_files.lean_manifest_path, lean_manifest) {
292        write_lean_manifest_with_report_links(path, manifest, &report_files)?;
293    }
294
295    Ok(report_files)
296}
297
298fn render_report_json_with_links(report: &VerificationReport, files: &ReportFiles) -> String {
299    let mut json = report.to_json();
300    if json.ends_with('}') {
301        json.pop();
302        json.push_str(",\"report_files\":{");
303        json.push_str(&format!(
304            "\"schema_version\":\"{}\",\"json_path\":\"{}\",\"markdown_path\":\"{}\"",
305            VERIFICATION_SIDECAR_SCHEMA_VERSION,
306            escape_json(&files.json_path),
307            escape_json(&files.markdown_path)
308        ));
309        if let Some(path) = &files.lean_diagnostics_json_path {
310            json.push_str(&format!(
311                ",\"lean_diagnostics_json_path\":\"{}\"",
312                escape_json(path)
313            ));
314        }
315        if let Some(path) = &files.lean_manifest_path {
316            json.push_str(&format!(
317                ",\"lean_manifest_path\":\"{}\"",
318                escape_json(path)
319            ));
320        }
321        if let Some(path) = &files.three_tier_json_path {
322            json.push_str(&format!(
323                ",\"three_tier_json_path\":\"{}\"",
324                escape_json(path)
325            ));
326        }
327        if let Some(path) = &files.three_tier_markdown_path {
328            json.push_str(&format!(
329                ",\"three_tier_markdown_path\":\"{}\"",
330                escape_json(path)
331            ));
332        }
333        json.push_str("}}");
334    }
335    json
336}
337
338fn render_report_markdown_with_links(report: &VerificationReport, files: &ReportFiles) -> String {
339    let mut markdown = report.to_markdown();
340    markdown.push_str("\nReport files:\n");
341    markdown.push_str(&format!(
342        "- Schema version: `{}`\n",
343        VERIFICATION_SIDECAR_SCHEMA_VERSION
344    ));
345    markdown.push_str(&format!("- JSON: `{}`\n", files.json_path));
346    markdown.push_str(&format!("- Markdown: `{}`\n", files.markdown_path));
347    if let Some(path) = &files.lean_diagnostics_json_path {
348        markdown.push_str(&format!("- Lean diagnostics JSON: `{}`\n", path));
349    }
350    if let Some(path) = &files.lean_manifest_path {
351        markdown.push_str(&format!("- Lean manifest: `{}`\n", path));
352    }
353    if let Some(path) = &files.three_tier_json_path {
354        markdown.push_str(&format!("- Three-tier JSON: `{}`\n", path));
355    }
356    if let Some(path) = &files.three_tier_markdown_path {
357        markdown.push_str(&format!("- Three-tier Markdown: `{}`\n", path));
358    }
359    markdown
360}
361
362#[cfg(feature = "amari")]
363fn render_three_tier_json_with_links(
364    report: &ThreeTierVerificationReport,
365    report_stem: &str,
366    root: &Path,
367) -> String {
368    let mut json = report.to_json();
369    if json.ends_with('}') {
370        json.pop();
371        json.push_str(",\"report_files\":{");
372        json.push_str(&format!(
373            "\"schema_version\":\"{}\",\"json_path\":\"{}\",\"markdown_path\":\"{}\"",
374            VERIFICATION_SIDECAR_SCHEMA_VERSION,
375            escape_json(&path_to_string(
376                &root.join(format!("{report_stem}.three-tier.json"))
377            )),
378            escape_json(&path_to_string(
379                &root.join(format!("{report_stem}.three-tier.md"))
380            ))
381        ));
382        json.push_str("}}");
383    }
384    json
385}
386
387#[cfg(feature = "amari")]
388fn render_three_tier_markdown_with_links(
389    report: &ThreeTierVerificationReport,
390    report_stem: &str,
391    root: &Path,
392) -> String {
393    let mut markdown = report.to_markdown();
394    markdown.push_str("\nReport files:\n");
395    markdown.push_str(&format!(
396        "- Schema version: `{}`\n",
397        VERIFICATION_SIDECAR_SCHEMA_VERSION
398    ));
399    markdown.push_str(&format!(
400        "- JSON: `{}`\n",
401        path_to_string(&root.join(format!("{report_stem}.three-tier.json")))
402    ));
403    markdown.push_str(&format!(
404        "- Markdown: `{}`\n",
405        path_to_string(&root.join(format!("{report_stem}.three-tier.md")))
406    ));
407    markdown
408}
409
410fn escape_json(s: &str) -> String {
411    s.replace('\\', "\\\\")
412        .replace('"', "\\\"")
413        .replace('\n', "\\n")
414}
415
416fn write_lean_manifest_with_report_links(
417    manifest_path: &str,
418    manifest: &crate::artifact::LeanManifest,
419    files: &ReportFiles,
420) -> io::Result<()> {
421    let manifest = manifest.clone().with_report_files({
422        let report_files =
423            LeanManifestReportFiles::new(files.json_path.clone(), files.markdown_path.clone());
424        match &files.lean_diagnostics_json_path {
425            Some(path) => report_files.with_lean_diagnostics_json_path(path.clone()),
426            None => report_files,
427        }
428    });
429    fs::write(manifest_path, manifest.to_json())
430}
431
432fn render_lean_diagnostics_json(report: &VerificationReport) -> String {
433    fn esc(s: &str) -> String {
434        s.replace('\\', "\\\\")
435            .replace('"', "\\\"")
436            .replace('\n', "\\n")
437    }
438
439    let module = match &report.lean_module {
440        Some(module) => module,
441        None => return "null".into(),
442    };
443
444    let obligation_entries = report
445        .obligations
446        .iter()
447        .filter(|obligation| {
448            obligation.lean_theorem_ref.is_some() || !obligation.lean_diagnostics.is_empty()
449        })
450        .map(|obligation| {
451            let diagnostics = obligation
452                .lean_diagnostics
453                .iter()
454                .map(|diagnostic| format!("\"{}\"", esc(diagnostic)))
455                .collect::<Vec<_>>()
456                .join(",");
457            format!(
458                "{{\"obligation_name\":\"{}\",\"theorem_ref\":{},\"diagnostics\":[{}]}}",
459                esc(&obligation.obligation_name),
460                obligation
461                    .lean_theorem_ref
462                    .as_ref()
463                    .map(|theorem_ref| format!("\"{}\"", esc(theorem_ref)))
464                    .unwrap_or_else(|| "null".into()),
465                diagnostics
466            )
467        })
468        .collect::<Vec<_>>()
469        .join(",");
470
471    let module_diagnostics = module
472        .diagnostics
473        .iter()
474        .map(|diagnostic| format!("\"{}\"", esc(diagnostic)))
475        .collect::<Vec<_>>()
476        .join(",");
477    let theorem_failures = module
478        .theorem_failures
479        .iter()
480        .map(|failure| format!("\"{}\"", esc(failure)))
481        .collect::<Vec<_>>()
482        .join(",");
483
484    format!(
485        "{{\"schema_version\":\"{}\",\"module_name\":\"{}\",\"module_diagnostics\":[{}],\"theorem_failures\":[{}],\"obligations\":[{}]}}",
486        VERIFICATION_SIDECAR_SCHEMA_VERSION,
487        esc(&module.module_name),
488        module_diagnostics,
489        theorem_failures,
490        obligation_entries
491    )
492}
493
494fn path_to_string(path: &Path) -> String {
495    path.to_string_lossy().into_owned()
496}
497
498#[cfg(test)]
499mod tests {
500    use super::*;
501    use crate::{
502        AlgebraicSignature, ExecutionResult, ExecutionStatus, LeanDiagnostic, LeanOutput, Origin,
503        SmtOutput, Sort,
504    };
505    #[cfg(feature = "amari")]
506    use crate::{StatisticalBound, verify_rare_event};
507
508    fn sample_session(root: &Path) -> VerificationSession {
509        let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
510        let bundle = ObligationBundle::monoid(
511            "sum_monoid",
512            Origin::new("karpal-core", "Monoid for Sum<i32>"),
513            &sig,
514        );
515
516        VerificationSession::new(bundle, ArtifactLayout::new(root), "KarpalVerify")
517    }
518
519    struct SuccessRunner;
520
521    impl VerifierRunner for SuccessRunner {
522        fn run(&self, plan: &crate::InvocationPlan) -> ExecutionResult {
523            ExecutionResult {
524                plan: plan.clone(),
525                status: match plan.kind {
526                    crate::CommandKind::Smt => ExecutionStatus::Unsat,
527                    crate::CommandKind::Lean | crate::CommandKind::Kani => ExecutionStatus::Success,
528                },
529                stdout: String::new(),
530                stderr: String::new(),
531                exit_code: Some(0),
532                backend_version: Some("tool 1.0".into()),
533                smt_output: Some(SmtOutput {
534                    status: Some(ExecutionStatus::Unsat),
535                    model: None,
536                    reason_unknown: None,
537                }),
538                lean_output: (plan.kind == crate::CommandKind::Lean).then(|| LeanOutput {
539                    diagnostics: vec![LeanDiagnostic {
540                        file: Some("lean/KarpalVerify.lean".into()),
541                        line: Some(4),
542                        column: Some(2),
543                        severity: "warning".into(),
544                        message: "declaration uses sorry: associativity".into(),
545                        theorem_hits: vec!["associativity".into()],
546                    }],
547                    theorem_hits: vec!["associativity".into()],
548                }),
549            }
550        }
551    }
552
553    #[test]
554    fn dry_run_report_orchestrates_artifacts_and_report() {
555        let session = sample_session(Path::new("target/karpal-verify-session-dry-run"));
556        let report = session.dry_run_report();
557
558        assert_eq!(report.obligation_count(), 3);
559        assert_eq!(report.root, "target/karpal-verify-session-dry-run");
560        assert!(
561            report
562                .obligations
563                .iter()
564                .all(|entry| entry.status() == Some(ExecutionStatus::DryRun))
565        );
566    }
567
568    #[test]
569    fn verify_report_builds_artifacts_runs_plans_and_returns_report() {
570        let temp = std::env::temp_dir().join("karpal_verify_session_report_test");
571        if temp.exists() {
572            let _ = fs::remove_dir_all(&temp);
573        }
574
575        let session = sample_session(&temp);
576        let report = session
577            .verify_report(&SuccessRunner)
578            .expect("session verification should succeed");
579        assert!(report.is_success());
580        assert!(temp.join("smt").exists());
581        assert!(temp.join("lean").exists());
582        assert_eq!(
583            report
584                .lean_module
585                .as_ref()
586                .map(|module| module.theorem_failures.clone()),
587            Some(vec!["KarpalVerify.associativity".into()])
588        );
589
590        let _ = fs::remove_dir_all(&temp);
591    }
592
593    #[test]
594    fn verify_with_ci_outputs_writes_reports_beside_artifacts() {
595        let temp = std::env::temp_dir().join("karpal_verify_session_ci_output_test");
596        if temp.exists() {
597            let _ = fs::remove_dir_all(&temp);
598        }
599
600        let output = sample_session(&temp)
601            .with_report_stem("summary")
602            .verify_with_ci_outputs(&SuccessRunner)
603            .expect("ci outputs should be written");
604
605        assert!(output.report.is_success());
606        assert!(Path::new(&output.report_files.json_path).exists());
607        assert!(Path::new(&output.report_files.markdown_path).exists());
608        assert!(
609            Path::new(
610                output
611                    .report_files
612                    .lean_diagnostics_json_path
613                    .as_deref()
614                    .expect("lean diagnostics sidecar should be written")
615            )
616            .exists()
617        );
618        assert!(
619            Path::new(
620                output
621                    .report_files
622                    .lean_manifest_path
623                    .as_deref()
624                    .expect("lean manifest path should be recorded")
625            )
626            .exists()
627        );
628        assert!(output.report_files.json_path.ends_with("summary.json"));
629        assert!(output.report_files.markdown_path.ends_with("summary.md"));
630        #[cfg(not(feature = "amari"))]
631        {
632            assert!(output.report_files.three_tier_json_path.is_none());
633            assert!(output.report_files.three_tier_markdown_path.is_none());
634        }
635        assert!(
636            output
637                .report_files
638                .lean_diagnostics_json_path
639                .as_deref()
640                .unwrap()
641                .ends_with("summary.lean-diagnostics.json")
642        );
643        assert!(
644            output
645                .report_files
646                .lean_manifest_path
647                .as_deref()
648                .unwrap()
649                .ends_with("lean/KarpalVerify.manifest.json")
650        );
651
652        let json = fs::read_to_string(&output.report_files.json_path)
653            .expect("summary json should be readable");
654        let markdown = fs::read_to_string(&output.report_files.markdown_path)
655            .expect("summary markdown should be readable");
656        let sidecar = fs::read_to_string(
657            output
658                .report_files
659                .lean_diagnostics_json_path
660                .as_deref()
661                .expect("lean diagnostics sidecar path should be present"),
662        )
663        .expect("lean diagnostics sidecar should be readable");
664        let manifest = fs::read_to_string(
665            output
666                .report_files
667                .lean_manifest_path
668                .as_deref()
669                .expect("lean manifest path should be present"),
670        )
671        .expect("lean manifest should be readable");
672        assert!(json.contains("\"schema_version\":\"1\""));
673        assert!(json.contains("\"report_files\""));
674        assert!(json.contains("\"lean_manifest_path\""));
675        assert!(json.contains("\"lean_diagnostics_json_path\""));
676        assert!(json.contains("\"schema_version\":\"1\",\"json_path\""));
677        assert!(markdown.contains("Report files:"));
678        assert!(markdown.contains("Schema version: `1`"));
679        assert!(markdown.contains("Lean diagnostics JSON"));
680        assert!(markdown.contains("Lean manifest"));
681        assert!(sidecar.contains("\"schema_version\":\"1\""));
682        assert!(manifest.contains("\"schema_version\":\"1\""));
683        assert!(manifest.contains("\"report_files\""));
684        assert!(manifest.contains("\"json_path\""));
685        assert!(manifest.contains("\"markdown_path\""));
686        assert!(manifest.contains("\"lean_diagnostics_json_path\""));
687
688        let _ = fs::remove_dir_all(&temp);
689    }
690
691    #[cfg(feature = "amari")]
692    #[test]
693    fn verify_with_ci_outputs_writes_three_tier_sidecars_when_statistical_evidence_exists() {
694        let temp = std::env::temp_dir().join("karpal_verify_session_three_tier_test");
695        if temp.exists() {
696            let _ = fs::remove_dir_all(&temp);
697        }
698
699        let bundle = sample_session(&temp).bundle().clone();
700        let statistical = verify_rare_event(
701            &bundle.obligations()[0],
702            &StatisticalBound::new(0.05).with_samples(128),
703            || false,
704        );
705
706        let output = sample_session(&temp)
707            .with_report_stem("summary")
708            .with_statistical_verification(statistical)
709            .verify_with_ci_outputs(&DryRunner)
710            .expect("ci outputs should be written");
711
712        let three_tier_json_path = output
713            .report_files
714            .three_tier_json_path
715            .as_deref()
716            .expect("three-tier json should be written");
717        let three_tier_markdown_path = output
718            .report_files
719            .three_tier_markdown_path
720            .as_deref()
721            .expect("three-tier markdown should be written");
722        assert!(Path::new(three_tier_json_path).exists());
723        assert!(Path::new(three_tier_markdown_path).exists());
724        assert!(three_tier_json_path.ends_with("summary.three-tier.json"));
725        assert!(three_tier_markdown_path.ends_with("summary.three-tier.md"));
726
727        let json = fs::read_to_string(three_tier_json_path).expect("three-tier json readable");
728        let markdown =
729            fs::read_to_string(three_tier_markdown_path).expect("three-tier markdown readable");
730        let main_json =
731            fs::read_to_string(&output.report_files.json_path).expect("main report json readable");
732        let main_markdown = fs::read_to_string(&output.report_files.markdown_path)
733            .expect("main report markdown readable");
734
735        assert!(json.contains("\"impossible_count\":1"));
736        assert!(json.contains("\"external_count\":2"));
737        assert!(json.contains("\"report_files\""));
738        assert!(markdown.contains("Three-Tier Verification Report"));
739        assert!(markdown.contains("Schema version: `1`"));
740        assert!(main_json.contains("\"three_tier_json_path\""));
741        assert!(main_json.contains("\"three_tier_markdown_path\""));
742        assert!(main_markdown.contains("Three-tier JSON"));
743        assert!(main_markdown.contains("Three-tier Markdown"));
744
745        let _ = fs::remove_dir_all(&temp);
746    }
747}
karpal_verify/session.rs

karpal_verify/
session.rs
