Primitive decoder replay and source addresses
Abstract
Unread suffix replay preserves primitive traces and identifies safe live source addresses.
The types C, I and O range independently over arbitrary universes, without finiteness or inhabitedness assumptions. Run means that some finite Trace joins the given Frames. Initialization is the Frame with state initial, acquired count zero and empty output. Safety(action,initial,Record) means that for every source a and input r satisfying Record(a,r), every finite Run from initialization on full(r), and every natural position p below its output length, the emitted symbol at p equals a(p). Liveness(action,initial,Record,InD) means that for every such Record with InD(a) and every natural position p, some finite Run from initialization on full(r) emits more than p symbols. In the address formula, s and otherCut denote arbitrary reachable Frames: the phrase equal cut states refers to their equal readable states, and neither Ready nor Cut is required. Only a must satisfy InD; the acquired counts need not coincide.
Theorem 1.1 (Unread suffix replay with independent old output).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/DecoderReplay.trace_replay (✓ std3). ∎
Source. Repository-derived.
Commentary.
Op has internal(next,batch), acquire(input to Option(next,batch)), and stopped. Step has only the two original internal and successful available acquisition rules. Frame consists of the original readable state and external acquired count and output word. action reads only the state. Trace retains its entire state vertex list and every finite edge batch. full(r)(q)=some(r(q)). Replay preserves that vertex list exactly, accumulates the actual acquisition and output increments, and changes neither state identity nor batches. Offset and old-output changes are external bookkeeping. Partial acquisition and unreachable loops remain allowed.
Theorem 1.2 (Live actual addresses agree after equal-state replay).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/DecoderReplay.actual_address_eq (✓ std3). ∎
Source. Repository-derived.
Commentary.
Safety means that on every Record every emitted position in every finite primitive run equals its source address. Liveness is positionwise and restricted to InD. Equal cut states, equal cumulative words and one equal unread suffix imply address equality: choose a liveness witness beyond both the requested position and old output, compare actual paths, replay the continuation, and apply safety on both records. No replay or joint injection is a premise.