feat(cli): give an engine-gap verdict one fresh retry before it's final

crates/flowproof-cli/src/lib.rs

@@ -716,20 +716,121 @@ fn cmd_record(spec_path: &Path, options: RecordOptions) -> Result<u8, String> {
                         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<flowproof_agent::RecordSummary, FreshRetryError> {
+    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<u8, String> {
+    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 {

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
+`<flow>.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
 ```