Named partial patch replay concatenation law
Proof verified
typechecked
Pinned formal modules
module #1 · 527d91c48d760214c5802af0f022008063b177251f485842f8234df651666143
What this target establishes
Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.
- Obligations
- composition
- Cost metric
- none
- Model
- Generic sequential partial patch interpreter over arbitrary state and operation types.
- Assumptions
- Each operation returns an optional state; failure propagates through replay.
- Implementation correspondence
- abstract model
- Limitations
- No concurrency, delivery liveness, runtime or implementation refinement guarantee.
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.
Formal 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)
Lean core · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 fe0fdc4c04bfc633ebe9f40a7e2161f487b20e911f015938391e2e5e8b6106a9
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.