Sparse entry emission #

theorem Complexity.RAM.RegisterStore.Machine.entryEncodeTM_hoareTime_frame {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : (work₀ tapes.address).HasBinaryNat entry.1) (hvalue : (work₀ tapes.value).HasBinaryNat entry.2) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) :

(entryEncodeTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (work tapes.address).HasBinarySuffix [] ∧ (work tapes.address).cells = (work₀ tapes.address).cells ∧ (work tapes.address).head = entry.1.bits.length + 1 ∧ (work tapes.value).HasBinarySuffix [] ∧ (work tapes.value).cells = (work₀ tapes.value).cells ∧ (work tapes.value).head = entry.2.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ entry.encode)) (entryEncodeTime entry)

Emit exactly Entry.encode entry from distinct canonical address and value work tapes, with a literal frame around those sources.

theorem Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeTM_hoareTime_frame {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (addressHeadBound valueHeadBound : ℕ) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : (work₀ tapes.address).HasBinaryContent entry.1.bits) (haddressStart : (work₀ tapes.address).cells 0 = Γ.start) (haddressHead : 1 ≤ (work₀ tapes.address).head ∧ (work₀ tapes.address).head ≤ addressHeadBound) (hvalue : (work₀ tapes.value).HasBinaryContent entry.2.bits) (hvalueStart : (work₀ tapes.value).cells 0 = Γ.start) (hvalueHead : 1 ≤ (work₀ tapes.value).head ∧ (work₀ tapes.value).head ≤ valueHeadBound) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) :

(rewindEntryEncodeTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (work tapes.address).HasBinarySuffix [] ∧ (work tapes.address).cells = (work₀ tapes.address).cells ∧ (work tapes.address).head = entry.1.bits.length + 1 ∧ (work tapes.value).HasBinarySuffix [] ∧ (work tapes.value).cells = (work₀ tapes.value).cells ∧ (work tapes.value).head = entry.2.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ entry.encode)) (rewindEntryEncodeTime entry addressHeadBound valueHeadBound)

Rewind arbitrary bounded decoded address/value cursors and emit exactly Entry.encode entry, retaining a literal frame around both sources.

theorem Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeRestoreTM_hoareTime_frame {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (haddress : (work₀ tapes.address).HasBinaryNat entry.1) (hvalue : (work₀ tapes.value).HasBinaryNat entry.2) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → TM.Parked (work₀ i)) (houtput : out₀.HasBinaryPrefix emitted) :

(rewindEntryEncodeRestoreTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out.HasBinaryPrefix (emitted ++ entry.encode)) (rewindEntryEncodeRestoreTime entry)

Emit one entry from canonical address/value sources, then restore the entire work family exactly.

theorem Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeRestoreTM_retargetOutput_hoareTime_frame {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (emitted : List Bool) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (haddress : (work₀ tapes.address.castSucc).HasBinaryNat entry.1) (hvalue : (work₀ tapes.value.castSucc).HasBinaryNat entry.2) (hinput : TM.Parked inp₀) (hother : ∀ (i : Fin n), i ≠ tapes.address → i ≠ tapes.value → TM.Parked (work₀ i.castSucc)) (hbuffer : (work₀ (Fin.last n)).HasBinaryPrefix emitted) :

(rewindEntryEncodeRestoreTM tapes).retargetOutput.HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ (∀ (i : Fin (n + 1)), i ≠ Fin.last n → work i = work₀ i) ∧ (work (Fin.last n)).HasBinaryPrefix (emitted ++ entry.encode) ∧ out = (Tape.init []).move Dir3.right) (rewindEntryEncodeRestoreTime entry)

Redirect restored entry emission into the fresh last work tape. All base work tapes are restored exactly and the real output remains standard blank.

Entry emission is append-only on the output tape.

Rewind-and-emit entry encoding is append-only on the output tape.

theorem Complexity.RAM.RegisterStore.Machine.entryEncodeTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryEncodeTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryEncodeTM tapes).reachesIn time start current) (htime : time ≤ entryEncodeTime entry) :

current.WithinAuxSpace inputLength (initialSpace + entryEncodeTime entry)

Coarse all-prefix auxiliary-space envelope for entry emission.

theorem Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryEncodeTapes n) (entry : Entry) (addressHeadBound valueHeadBound inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (rewindEntryEncodeTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (rewindEntryEncodeTM tapes).reachesIn time start current) (htime : time ≤ rewindEntryEncodeTime entry addressHeadBound valueHeadBound) :

current.WithinAuxSpace inputLength (initialSpace + rewindEntryEncodeTime entry addressHeadBound valueHeadBound)

Coarse all-prefix envelope for rewind-and-emit entry encoding.

Documentation