diff --git a/crates/flowproof-cli/src/lib.rs b/crates/flowproof-cli/src/lib.rs index bb55f41..1ee1cab 100644 --- a/crates/flowproof-cli/src/lib.rs +++ b/crates/flowproof-cli/src/lib.rs @@ -716,20 +716,121 @@ fn cmd_record(spec_path: &Path, options: RecordOptions) -> Result { return record_failure_result(&err, json); } RepairLoopOutcome::GaveUp(err, report) => { - write_repair_report(&out, &report)?; - if json { - let mut payload = record_failure_json(&err) - .unwrap_or_else(|| serde_json::json!({ "error": err.to_string() })); - payload["repair"] = - serde_json::to_value(&report).map_err(|e| e.to_string())?; - println!( - "{}", - serde_json::to_string_pretty(&payload).map_err(|e| e.to_string())? + // An engine_gap verdict is a judgment call on + // whatever the live app happened to show that + // instant — not a proven, reproducible fact. Give + // the whole flow one independent, fresh attempt + // before treating that verdict as final; a + // budget-exhausted verdict already tried several + // real fixes, so it does not get a freebie retry. + let is_engine_gap = matches!( + report.outcome, + flowproof_agent::RepairOutcome::EngineGap { .. } + ); + if !is_engine_gap { + write_repair_report(&out, &report)?; + return emit_repair_failure(&err, &report, &report, json); + } + if !json { + eprintln!( + "Repair called this an engine gap; giving the flow one fresh, \ + independent attempt before reporting a final failure..." ); - return Ok(EXIT_ERROR); } - print_repair_report(&report); - return Err(err.to_string()); + match fresh_record_attempt(spec_path, &values, &out, author, recording) { + Ok(summary) => { + let combined = RepairReportWithFreshRetry { + first_attempt: &report, + fresh_retry: FreshRetryOutcome::Passed, + }; + write_json_report(&out, &combined)?; + if !json { + println!( + "Fresh retry passed without needing repair — the first \ + failure was a one-off, not a real problem." + ); + } + summary + } + Err(FreshRetryError::Setup(setup_err)) => { + let combined = RepairReportWithFreshRetry { + first_attempt: &report, + fresh_retry: FreshRetryOutcome::FailedAgain { + report: flowproof_agent::RepairReport { + attempts: Vec::new(), + outcome: + flowproof_agent::RepairOutcome::NotApplicable { + reason: setup_err.clone(), + }, + }, + }, + }; + write_json_report(&out, &combined)?; + return Err(setup_err); + } + Err(FreshRetryError::Record(retry_err)) => { + match run_repair_loop( + spec_path, &values, &out, author, recording, retry_err, + ) { + RepairLoopOutcome::Passed { + summary, + report: retry_report, + } => { + let combined = RepairReportWithFreshRetry { + first_attempt: &report, + fresh_retry: FreshRetryOutcome::Repaired { + report: retry_report.clone(), + }, + }; + write_json_report(&out, &combined)?; + if !json { + print_repair_report(&retry_report); + } + summary + } + RepairLoopOutcome::NotRepaired(final_err) => { + let combined = RepairReportWithFreshRetry { + first_attempt: &report, + fresh_retry: FreshRetryOutcome::FailedAgain { + report: flowproof_agent::RepairReport { + attempts: Vec::new(), + outcome: + flowproof_agent::RepairOutcome::NotApplicable { + reason: final_err.to_string(), + }, + }, + }, + }; + write_json_report(&out, &combined)?; + return emit_repair_failure( + &final_err, &combined, &report, json, + ); + } + RepairLoopOutcome::GaveUp(final_err, final_report) => { + let combined = RepairReportWithFreshRetry { + first_attempt: &report, + fresh_retry: FreshRetryOutcome::FailedAgain { + report: final_report.clone(), + }, + }; + write_json_report(&out, &combined)?; + if !json { + eprintln!( + "Fresh retry did not recover either — two \ + independent failures agree, this looks like a \ + real problem, not a flake." + ); + } + return emit_repair_failure( + &final_err, + &combined, + &final_report, + json, + ); + } + } + } + } } } } else { @@ -794,6 +895,66 @@ fn record_failure_result(err: &flowproof_agent::RecordError, json: bool) -> Resu Err(err.to_string()) } +/// Either half of what [`fresh_record_attempt`] can fail with: a setup +/// problem (can't even load the spec or open a driver — not something a +/// second repair loop pass could address) or a genuine [`RecordError`] from +/// actually running the flow, which the caller can feed back into +/// [`run_repair_loop`] as it would any other failure. +enum FreshRetryError { + Setup(String), + Record(flowproof_agent::RecordError), +} + +/// One completely fresh `record` attempt: reload the spec, rebuild the +/// driver from scratch (new browser session, new login), and run once. Used +/// to give an `engine_gap` verdict a second, independent roll of the dice — +/// see [`cmd_record`]'s handling of [`RepairLoopOutcome::GaveUp`] for why +/// that verdict is treated as provisional rather than final. +fn fresh_record_attempt( + spec_path: &Path, + values: &ValuesArgs, + out: &Path, + author: AuthorArg, + recording: flowproof_driver::RecordingOptions, +) -> Result { + let (spec, _env_overlay) = + load_prepared_spec(spec_path, values).map_err(FreshRetryError::Setup)?; + let mut driver = record_driver(&spec).map_err(FreshRetryError::Setup)?; + flowproof_agent::record_with_author_and_options( + &spec, + &mut driver, + out, + author.into(), + recording, + ) + .map_err(FreshRetryError::Record) +} + +/// Report a final repair failure, in whichever shape the caller has: +/// `repair_payload` is whatever gets embedded in the `--json` output's +/// `repair` field (a plain [`flowproof_agent::RepairReport`] or, after a +/// fresh retry, a [`RepairReportWithFreshRetry`]); `human_report` is the +/// most relevant single report for the human-readable printout. +fn emit_repair_failure( + err: &flowproof_agent::RecordError, + repair_payload: &impl serde::Serialize, + human_report: &flowproof_agent::RepairReport, + json: bool, +) -> Result { + if json { + let mut payload = record_failure_json(err) + .unwrap_or_else(|| serde_json::json!({ "error": err.to_string() })); + payload["repair"] = serde_json::to_value(repair_payload).map_err(|e| e.to_string())?; + println!( + "{}", + serde_json::to_string_pretty(&payload).map_err(|e| e.to_string())? + ); + return Ok(EXIT_ERROR); + } + print_repair_report(human_report); + Err(err.to_string()) +} + enum RepairLoopOutcome { Passed { summary: flowproof_agent::RecordSummary, @@ -1114,11 +1275,45 @@ fn repair_report_path(out: &Path) -> PathBuf { } fn write_repair_report(out: &Path, report: &flowproof_agent::RepairReport) -> Result<(), String> { + write_json_report(out, report) +} + +fn write_json_report(out: &Path, report: &impl serde::Serialize) -> Result<(), String> { let path = repair_report_path(out); let json = serde_json::to_string_pretty(report).map_err(|e| e.to_string())?; std::fs::write(&path, json).map_err(|e| format!("cannot write {}: {e}", path.display())) } +/// What happened when an `engine_gap` verdict got one fresh, independent +/// attempt before being treated as final — see [`cmd_record`]'s handling of +/// [`RepairLoopOutcome::GaveUp`] for why that verdict is provisional rather +/// than immediate. +#[derive(Debug, serde::Serialize)] +#[serde(tag = "retry_outcome", rename_all = "kebab-case")] +enum FreshRetryOutcome { + /// The fresh attempt just worked — no repair needed at all the second + /// time, meaning the first failure really was a one-off flake. + Passed, + /// The fresh attempt failed too, but this time the repair loop found a + /// real fix. + Repaired { + report: flowproof_agent::RepairReport, + }, + /// The fresh attempt failed again and repair gave up again — two + /// independent failures agreeing is real evidence, not a flake. + FailedAgain { + report: flowproof_agent::RepairReport, + }, +} + +/// The full record of an `engine_gap` verdict plus what its fresh retry did. +#[derive(Debug, serde::Serialize)] +struct RepairReportWithFreshRetry<'a> { + #[serde(flatten)] + first_attempt: &'a flowproof_agent::RepairReport, + fresh_retry: FreshRetryOutcome, +} + fn print_repair_report(report: &flowproof_agent::RepairReport) { for attempt in &report.attempts { let status = if attempt.applied { diff --git a/docs/getting-started.md b/docs/getting-started.md index 6f26215..1b06270 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -257,6 +257,19 @@ something more patching can solve). The only file this ever touches is the changed, and why. Pass `--no-repair` to disable this and get the original behavior: stop and report the first failure immediately. +When the model concludes a failure is a Flowproof limitation rather than a +fixable flow (an "engine gap"), that verdict is treated as provisional, not +final: live evidence at the moment of failure can be ambiguous (a target +that briefly reads as empty text, for example), so `record` gives the whole +flow one independent, fresh attempt — a new driver session, from the top — +before reporting a hard failure. If the fresh attempt passes outright, the +first failure was a one-off; if it fails again and repair finds a real fix, +that's used; if it fails the same way again, both failures are recorded in +`.repair.json` as agreeing evidence of a genuine problem. A +budget-exhausted verdict (repair genuinely tried several real fixes) does +not get this free retry — only a verdict that never really tried a fix at +all. + ```bash flowproof record shop.flow.yaml --no-repair ```