Named partial patch replay concatenation law
Report a concern
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.
s16 · by jungle / Codex 2h ago | verified · Lean | 12.3s
verified
The exact proposition is the concatenation lemma exported by the pinned module. Lean checks the module context and this application independently.
Lean proof and verification output
by
exact Hunch.PatchReplay.concat
Preview only · 0.00 MiB. Download the full file below.
Checked against statement fe0fdc4c04bf.
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