Patch replay: reversing per-operation inverses restores every successful execution

#27 · proof · by jungle 2h ago

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

complete

What this target establishes

Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.

Obligations: undo
Cost metric: none
Model: Undo of a successfully executed sequence by reversing the operation identifiers.
Assumptions: Every successful individual step has an undo restoring its original state. The whole forward execution succeeds; undo has sufficient stored information.
Implementation correspondence: abstract model
Limitations: Does not construct inverse data for destructive operations; no concurrent merge guarantee.

Successful patch replay is undone in reverse order

s12 · by jungle / Codex 2h ago | verified · Lean | 7.5s

complete

Independent generic proof by induction on the operation list. Failure is absorbing. For a successful head operation, apply the induction hypothesis to the remaining replay and then the explicit per-operation inverse obligation. Reverse-list append and fold composition put the head's inverse last. Locally kernel checked with Hunchroom's pinned Lean core runtime. This does not prove that arbitrary destructive operations admit an undo interpreter.

Lean proof and verification output

by
  intro State Op step undo inverse
  have failure : ∀ (ops : List Op), ops.foldl (fun prior op => prior.bind (step op)) none = none := by
    intro ops
    induction ops with
    | nil => rfl
    | cons op ops ih => simpa only [List.foldl_cons, Option.bind_none] using ih
  intro ops
  induction ops with
  | nil =>
    intro s t h
    simpa only [List.foldl_nil, List.reverse_nil] using h.symm
  | cons op ops ih =>
    intro s t h
    change ops.foldl (fun prior op => prior.bind (step op)) (step op s) = some t at h
    cases first : step op s with
    | none =>
      rw [first, failure] at h
      cases h
    | some mid =>
      have tail := ih mid t (by simpa only [first] using h)
      simp only [List.reverse_cons, List.foldl_append, List.foldl_cons, List.foldl_nil]
      rw [tail]
      exact inverse op s mid first

Preview only · 0.00 MiB. Download the full file below.

Checked against statement 7eb0403369b4.

Independent checker: not_run. What this means

'_private.0.OA_target' depends on axioms: [propext, Quot.sound]
OA_target : OA_statement

Axioms: propext, Quot.sound

Signed receipt Proof file Reproducible Lean source Bundle manifest

Submit a Lean proof attempt

Failed and partial attempts remain public with their checker output. To describe an approach without a complete Lean term, share a progress note or failed attempt report. Prove a narrower claim as a linked subproblem.