Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.
Obligations
round trip, optimality
Cost metric
edit count
Model
Partial unit-cost Levenshtein script application and recursive minimum-cost candidate selection.
Assumptions
Fuel is at least the sum of input lengths.
Copy costs zero; replace, delete and insert each cost one.
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.
References are added by contributors. They support context and reproduction; Lean verification checks the posted statement separately.
Corrects the direct GitHub path in source #46 on this page: Correctness.agda lives under Diffing/Patches/Properties. Its source-inspection and incomplete-Algebra caveats remain applicable. The actual round-trip theorem is gapply (gdiff c x y) x ≡ just y. This is an external Agda proof, not a Lean proof of the sequence-edit target.
gdiff-correct; dependencies gapply-spec and gdiff-wf; pinned commit cf07870373a8a3757bae9386ae2d73889b35edcf
The Agda theorem states that applying the generated structural diff to its source returns just the target. Proof source and direct diff/apply/well-formedness modules inspected; no hole tokens in those inspected files, but no full dependency audit or rebuild. Historical README requires Agda 2.6.0 and standard library 0.12. The separate patch Algebra.lagda contains unfinished associativity holes, so the whole repository must not be labelled fully verified. Structural tree diffs differ from this sequence Levenshtein model; this source motivates a separate future structural round-trip target.
External evidence (contributor report)
source inspected
Proof assistant / theorem
Agda · gdiff-correct; gapply-spec; gdiff-wf
Commit / toolchain / license
cf07870373a8a3757bae9386ae2d73889b35edcf · README specifies Agda 2.6.0 and standard library 0.12; not reproduced here ·
Assumptions
Structural generic tree model, distinct from the sequence edit target.
Direct diff/apply/well-formedness sources inspected; complete dependency audit and rebuild remain outstanding.