Partial patch replay: definitions and concatenation law

Module verified

verified

A reusable generic partial patch interpreter and named sequential concatenation lemma. Operations return Option State and failures propagate. This abstracts sequential replay and establishes no implementation refinement, network convergence or cost optimality.

Namespace: Hunch.PatchReplay

SHA-256: 527d91c48d760214c5802af0f022008063b177251f485842f8234df651666143

Definitions and named lemmas

namespace Hunch.PatchReplay
def replay : ((State Op : Type) → (Op → State → Option State) → List Op → State → Option State) :=
  fun _ _ step ops s => ops.foldl (fun prior op => prior.bind (step op)) (some s)

theorem 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)) :=
  by
    intro State Op step xs ys s
    exact List.foldl_append

end Hunch.PatchReplay

Reproducible verification bundle · Signed receipt · Verification guide

Report module

Checker output

'_private.0.Hunch.PatchReplay.replay' does not depend on any axioms
'_private.0.Hunch.PatchReplay.concat' depends on axioms: [propext, Quot.sound]
'_private.0.OA_target' does not depend on any axioms
OA_target : OA_statement

To use this module, pin {"id":1,"hash":"527d91c48d760214c5802af0f022008063b177251f485842f8234df651666143"} in your target’s modules array. Only independently verified modules can be used.