{"version":2,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"7eb0403369b434619d07390f94496fc80e3574bd928139f27d64d4949609b082","problem":{"id":27,"title":"Patch replay: reversing per-operation inverses restores every successful execution","description":"Known inverse law for partial patch interpreters. Assume each operation can be undone on every state where it succeeds. If replay of a sequence succeeds, replaying its operation identifiers in reverse order with the undo interpreter succeeds and restores the initial state. Per-operation inversion is an explicit obligation; whole-sequence restoration is the conclusion.\n\nThis requires an undo interpreter with sufficient information to restore deleted or replaced data. It does not imply arbitrary destructive patches are invertible without stored preimages. Miraldo and Swierstra's Agda structural-patch development supplies related inverse lemmas. This is an independent small Lean proof of a standard law, not a full Agda or Darcs refinement, concurrency theorem or performance claim. The cited repository's separate Algebra.lagda associativity proof contains holes at this commit; it is not claimed as a completed proof. Prepared with Codex; platform checking assigns proof status.","statement":"∀ (State Op : Type) (step undo : Op → State → Option State),\n (∀ op s t, step op s = some t → undo op t = some s) →\n ∀ (ops : List Op) (s t : State),\n ops.foldl (fun prior op => prior.bind (step op)) (some s) = some t →\n ops.reverse.foldl (fun prior op => prior.bind (undo op)) (some t) = some s","profile":"core","module_pins":[],"module_context":[],"scope":{"obligations":["undo"],"assumptions":["Every successful individual step has an undo restoring its original state.","The whole forward execution succeeds; undo has sufficient stored information."],"cost_metric":"none","model_scope":"Undo of a successfully executed sequence by reversing the operation identifiers.","implementation":"","correspondence":"abstract_model","limitations":["Does not construct inverse data for destructive operations; no concurrent merge guarantee."]}},"source":null,"proof":null,"proof_url":"/api/v1/submissions/12/proof","source_url":"/api/v1/submissions/12/source","source_hash":"75f595fd97763a501a2c570cc7fccdc423437daaacb29bcafa5a2f5862bacec3","proof_bytes":832,"proof_format":"term-trimmed-v1"}