Encoded-head finite ROM execution

Abstract

RarePriorLiteralController.EncodedHead

The head is an encoded finite tape. Its literal scan, carry, read, write and emit instructions implement the ROM copy checkpoints, including paused cuts and permanent halt at the exhausted width.

Theorem 1.1 (Encoded head at every paused instruction).

$$\forall (w:\mathbb{N}),\forall (\mathrm{rom}:\mathrm{Fin}(w)\to \mathrm{Bool}),((\forall (m:\mathbb{N}),\forall (\mathrm{hm}:m\le w),\forall (r:\mathbb{N}),((\mathrm{motorRun}(\mathrm{rom},\mathrm{motorEntry}(w),\mathrm{motorTime}(m)+r)=\mathrm{motorRun}(\mathrm{rom},\mathrm{motorCheckpoint}(\mathrm{rom},m,\mathrm{hm}),r))\wedge (\mathrm{motorTrace}(\mathrm{rom},\mathrm{motorEntry}(w),\mathrm{motorTime}(m)+r)=\mathrm{copyTrace}(\mathrm{rom},\mathrm{copyEntry}(w),4\ast m)++\mathrm{motorTrace}(\mathrm{rom},\mathrm{motorCheckpoint}(\mathrm{rom},m,\mathrm{hm}),r))))\wedge ((((\mathrm{motorRun}(\mathrm{rom},\mathrm{motorEntry}(w),\mathrm{motorTime}(w))).\mathrm{tape}=\mathrm{rom})\wedge (((\mathrm{motorTrace}(\mathrm{rom},\mathrm{motorEntry}(w),\mathrm{motorTime}(w))=\mathrm{List}.\mathrm{ofFn}((\mathrm{fun}i:\mathrm{Fin}(w)\mapsto \mathrm{rom}(i))))\wedge (\forall (n:\mathbb{N}),\mathrm{motorRun}(\mathrm{rom},\mathrm{motorEntry}(w),\mathrm{motorTime}(w)+2\ast w+2+n)=\{\{\mathrm{motorCheckpoint}(\mathrm{rom},w,{\mathrm{le}}_{\mathrm{rfl}})\mathrm{with}\mathrm{probe}:=\mathrm{Fin}.\mathrm{last}(w)\}\mathrm{with}\mathrm{pc}:=\mathrm{MotorPC}.\mathrm{halt}\}))))))$$

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

Source. Repository-derived.

Commentary.

For every finite ROM, the actual head-bit scan and carry execution reaches the exact macro checkpoint tape and trace, preserves all residual instruction cuts, copies the complete tape and reaches a permanent halt.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EncodedHead.encoded_head_copy_refinement
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeFullResidual
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/EventFrames
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorResidentCode
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorSerialExecution