Physical-bank query and successor writeback

Abstract

RarePriorLiteralController.LiveProducerWork

The current bank is first copied to the pre tape and then encoded by the literal key carry into the raw unary query. bank_query identifies that query with nativeKey for the bank-encoded Runtime and captured operation. build_key_work preserves the pre, result and old-field work, row slot and offset through the carry phase.

PayloadGood is a proof invariant relating the scanner row and accumulator to a copied unary payload. installed_payload_step reads the installed physical program, establishes the next payload invariant and refines installedGraphStep. The nativeTable appears in this specification; the transition obtains each payload bit from nativeBit on the installed tape.

Writeback alternates a read from the copied result tape and a write to the role-selected bank. writeCheckpoint fixes every already written prefix and retains the remaining bank cells. The write-cycle and write-prefix inductions include the exhausted boundary, and result_drop removes only the optional-result marker before writing the complete successor Runtime.

The displayed endpoint starts at phase nine with bankProbe zero and the complete successful result tape. It reaches phase eleven with exactly the selected successor bank and the opposite bank preserved. Operation, role and outer image context stay fixed, and writeback emits no frame bits. Phase eleven retains work; it does not assert canonical Ready or a complete repeated service cycle.

Theorem 1.1 (Complete bitwise writeback with a quiet trace).

$$\forall (s:\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{State}),\forall (d:\mathrm{Runtime}),(s).\mathrm{phase}=9\to (s).\mathrm{bankProbe}=0\to ((s).\mathrm{result}).\mathrm{tape}=\mathrm{word}(\mathrm{optionalRuntimeCodec}(\mathrm{some}(d)))\to \exists (t:\mathbb{N}),\exists (q:\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{State}),((\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{run}(s,t)=q)\wedge ((((q).\mathrm{phase}=11)\wedge ((((q).\mathrm{actual}=(\mathrm{if}(s).\mathrm{role}\mathrm{then}(s).\mathrm{actual}\mathrm{else}\mathrm{word}(\mathrm{runtimeCodec}(d))))\wedge ((((q).\mathrm{synthetic}=(\mathrm{if}(s).\mathrm{role}\mathrm{then}\mathrm{word}(\mathrm{runtimeCodec}(d))\mathrm{else}(s).\mathrm{synthetic}))\wedge ((((q).\mathrm{operation}=(s).\mathrm{operation})\wedge ((((q).\mathrm{role}=(s).\mathrm{role})\wedge (((((q).\mathrm{addressed}).\mathrm{outer}=((s).\mathrm{addressed}).\mathrm{outer})\wedge (\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{trace}(s,t)=[]))))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/LiveProducerWork.write_complete (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two-instruction per-cell schedule writes every Runtime bit, then the exhausted probe retires. The proof keeps both physical banks in the statement and shows the entire output trace is empty during this phase.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/LiveProducerWork.write_complete
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/LiveProducerExecution