{"version":3,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"fe0fdc4c04bfc633ebe9f40a7e2161f487b20e911f015938391e2e5e8b6106a9","problem":{"id":33,"title":"Named partial patch replay concatenation law","description":"The reusable PatchReplay module defines a generic partial replay interpreter and proves the concatenation law once. This target reuses the named lemma. It concerns sequential replay with failure propagation; it establishes no CRDT network delivery, diff minimality or native implementation refinement.","statement":"∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State), Hunch.PatchReplay.replay State Op step (xs ++ ys) s = ys.foldl (fun prior op => prior.bind (step op)) (Hunch.PatchReplay.replay State Op step xs s)","profile":"core","module_pins":[{"id":1,"hash":"527d91c48d760214c5802af0f022008063b177251f485842f8234df651666143"}],"module_context":[{"id":1,"hash":"527d91c48d760214c5802af0f022008063b177251f485842f8234df651666143","namespace":"PatchReplay","source":"namespace Hunch.PatchReplay\ndef replay : ((State Op : Type) → (Op → State → Option State) → List Op → State → Option State) :=\n  fun _ _ step ops s => ops.foldl (fun prior op => prior.bind (step op)) (some s)\n\ntheorem concat : (∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State), replay State Op step (xs ++ ys) s = ys.foldl (fun prior op => prior.bind (step op)) (replay State Op step xs s)) :=\n  by\n    intro State Op step xs ys s\n    exact List.foldl_append\n\nend Hunch.PatchReplay\n"}],"scope":{"obligations":["composition"],"assumptions":["Each operation returns an optional state; failure propagates through replay."],"cost_metric":"none","model_scope":"Generic sequential partial patch interpreter over arbitrary state and operation types.","implementation":"","correspondence":"abstract_model","limitations":["No concurrency, delivery liveness, runtime or implementation refinement guarantee."]}},"source":null,"proof":null,"proof_url":"/api/v1/submissions/16/proof","source_url":"/api/v1/submissions/16/source","source_hash":"6df2fc43900035bc02c15a37a702882f1f219d658d91366ae2d822848f4dfa54","proof_bytes":35,"proof_format":"term-trimmed-v1"}