{"version":2,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"8a86b4d6476261560d43f6ea3df9394ba847eb65bf27eb0728f61c014858789d","problem":{"id":31,"title":"Diff and patch correctness: a minimum-cost edit script reconstructs its target","description":"Porting target for existing verified edit-script results. Isabelle AFP Min_Ed_Dist0 proves min_eds_correct (the generated script reconstructs the target), min_eds_minimal (no successfully applied script is cheaper), and min_ed_min_eds (distance equals script cost). The existing source proof is supplied; a Lean proof of this exact target remains requested.\n\nThe entire executable model is included. Edit = Sum (Option Nat) (Option Nat): inl none copies the next symbol, inl (some x) replaces it with x, inr none deletes it, and inr (some x) inserts x. Copy costs zero; other edits cost one. Apply rejects copy/replace/delete on empty input. Finishing the script leaves the unconsumed suffix unchanged. The generator compares replace/delete/insert candidates by complete script cost and copies when the heads agree. Empty-input cases insert or delete the remaining symbols. Fuel at least sourceLength+targetLength prevents truncation.\n\nThe conclusions are successful reconstruction and minimum cost against EVERY competing successfully applied script. Neither is a premise. This is unit-cost Levenshtein editing, distinct from insertion/deletion-only LCS distance, encoded bytes or runtime. The Isabelle edit function is total with different out-of-range behavior; this model validates those operations, so the external proof is a guide rather than a directly reusable term. No universal port-equivalence, memoization, Myers correctness or native implementation refinement is claimed. Known-result formalization request prepared with Codex.","statement":"(fun (cost : List (Sum (Option Nat) (Option Nat)) → Nat) =>\n(fun (apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat)) =>\n(fun (best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat))) =>\n(fun (diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))) =>\n∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →\n apply (diff fuel xs ys) xs = some ys ∧\n ∀ script : List (Sum (Option Nat) (Option Nat)), apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script\n) (fun fuel => Nat.rec (fun _ _ : List Nat => [])\n (fun _ recur xs ys => match xs, ys with\n | [], _ => ys.map (fun y => Sum.inr (some y))\n | _, [] => List.replicate xs.length (Sum.inr none)\n | x :: xt, y :: yt => if x = y then Sum.inl none :: recur xt yt\n   else best (Sum.inl (some y) :: recur xt yt)\n             (Sum.inr none :: recur xt ys)\n             (Sum.inr (some y) :: recur xs yt)) fuel)\n) (fun a b c => if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c)\n) (fun script => List.rec (fun xs : List Nat => some xs)\n (fun edit _ rest xs => match edit, xs with\n | .inl none, x :: xt => (rest xt).map (fun ys => x :: ys)\n | .inl (some y), _ :: xt => (rest xt).map (fun ys => y :: ys)\n | .inr none, _ :: xt => rest xt\n | .inr (some y), _ => (rest xs).map (fun ys => y :: ys)\n | _, [] => none) script)\n) (fun script => script.foldr (fun edit n => match edit with | .inl none => n | _ => n + 1) 0)","profile":"core","module_pins":[],"module_context":[],"scope":{"obligations":["round_trip","optimality"],"assumptions":["Fuel is at least the sum of input lengths.","Copy costs zero; replace, delete and insert each cost one."],"cost_metric":"edit_count","model_scope":"Partial unit-cost Levenshtein script application and recursive minimum-cost candidate selection.","implementation":"","correspondence":"algorithm_model","limitations":["Lean proof remains open; source-consuming operations reject empty input.","No equivalence to the total Isabelle interpreter, byte-size optimality or native implementation refinement."]}},"source":null,"proof":null,"proof_url":"/api/v1/submissions/29/proof","source_url":"/api/v1/submissions/29/source","source_hash":"8d853266a9a713fe059b5fdab1ee34a619c63cd7f1bd63493053b2a12c380f70","proof_bytes":16607,"proof_format":"term-trimmed-v1"}