RAM sparse-entry decoder

This module exposes the exact framed semantics of the concrete two-word sparse address/value decoder.

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeTM_reachesIn_frame {n : ℕ} (tapes : EntryDecodeTapes n) (entry : Entry) (rest : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ tapes.source).HasBinarySuffix (entry.encode ++ rest)) (haddress : (work₀ tapes.address).HasBinaryPrefix []) (hvalue : (work₀ tapes.value).HasBinaryPrefix []) (haddressStart : (work₀ tapes.address).cells 0 = Γ.start) (hvalueStart : (work₀ tapes.value).cells 0 = Γ.start) (haddressCounter : (work₀ tapes.addressCounter).HasBinaryNat 0) (haddressWidth : (work₀ tapes.addressWidth).HasBinaryNat 0) (hvalueCounter : (work₀ tapes.valueCounter).HasBinaryNat 0) (hvalueWidth : (work₀ tapes.valueWidth).HasBinaryNat 0) (hinput : inp₀.read ≠ Γ.start) (hreads : ∀ (i : Fin n), (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (entryDecodeTM tapes).Q), (entryDecodeTM tapes).reachesIn (entryDecodeTime entry.1 entry.2) { state := (entryDecodeTM tapes).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (entryDecodeTM tapes).halted c' ∧ c'.input = inp₀ ∧ (c'.work tapes.source).HasBinarySuffix rest ∧ (c'.work tapes.address).HasBinaryPrefix entry.1.bits ∧ (c'.work tapes.address).cells 0 = Γ.start ∧ (c'.work tapes.value).HasBinaryPrefix entry.2.bits ∧ (c'.work tapes.value).cells 0 = Γ.start ∧ (c'.work tapes.addressCounter).HasBinaryNat (bitlen entry.1) ∧ (c'.work tapes.addressWidth).HasBinaryNat (bitlen entry.1) ∧ (c'.work tapes.valueCounter).HasBinaryNat (bitlen entry.2) ∧ (c'.work tapes.valueWidth).HasBinaryNat (bitlen entry.2) ∧ (∀ (i : Fin n), i ≠ tapes.source → i ≠ tapes.address → i ≠ tapes.value → i ≠ tapes.addressCounter → i ≠ tapes.addressWidth → i ≠ tapes.valueCounter → i ≠ tapes.valueWidth → c'.work i = work₀ i) ∧ c'.output = out₀

Decode one canonical sparse address/value entry exactly, leaving the next encoded entry under the source head and preserving every unrelated tape.

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryDecodeTapes n) (address value inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryDecodeTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryDecodeTM tapes).reachesIn time start current) (htime : time ≤ entryDecodeTime address value) : current.WithinAuxSpace inputLength (initialSpace + entryDecodeTime address value)

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

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeTM_isTransducer {n : ℕ} (tapes : EntryDecodeTapes n) : (entryDecodeTM tapes).IsTransducer

Entry decoding preserves one-way output safety.

Linear unary-marker decoder

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeLinearTM_reachesIn_frame {n : ℕ} (tapes : EntryDecodeTapes n) (entry : Entry) (rest : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ tapes.source).HasBinarySuffix (entry.encode ++ rest)) (haddress : (work₀ tapes.address).HasBinaryPrefix []) (hvalue : (work₀ tapes.value).HasBinaryPrefix []) (haddressStart : (work₀ tapes.address).cells 0 = Γ.start) (hvalueStart : (work₀ tapes.value).cells 0 = Γ.start) (haddressMarker : (work₀ tapes.addressCounter).HasBinaryPrefix []) (haddressMarkerStart : (work₀ tapes.addressCounter).cells 0 = Γ.start) (hvalueMarker : (work₀ tapes.valueCounter).HasBinaryPrefix []) (hvalueMarkerStart : (work₀ tapes.valueCounter).cells 0 = Γ.start) (hinput : inp₀.read ≠ Γ.start) (hreads : ∀ (i : Fin n), (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (entryDecodeLinearTM tapes).Q), (entryDecodeLinearTM tapes).reachesIn (entryDecodeLinearTime entry.1 entry.2) { state := (entryDecodeLinearTM tapes).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (entryDecodeLinearTM tapes).halted c' ∧ c'.input = inp₀ ∧ (c'.work tapes.source).HasBinarySuffix rest ∧ (c'.work tapes.address).HasBinaryPrefix entry.1.bits ∧ (c'.work tapes.address).cells 0 = Γ.start ∧ (c'.work tapes.value).HasBinaryPrefix entry.2.bits ∧ (c'.work tapes.value).cells 0 = Γ.start ∧ (c'.work tapes.addressCounter).HasBinaryPrefix (List.replicate (bitlen entry.1) true) ∧ (c'.work tapes.valueCounter).HasBinaryPrefix (List.replicate (bitlen entry.2) true) ∧ (∀ (i : Fin n), i ≠ tapes.source → i ≠ tapes.address → i ≠ tapes.value → i ≠ tapes.addressCounter → i ≠ tapes.valueCounter → c'.work i = work₀ i) ∧ c'.output = out₀

Decode one canonical sparse entry using unary markers, leaving the next entry under the source head and preserving the two unused width tapes.

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeLinearTime_eq (address value : ℕ) : entryDecodeLinearTime address value = 3 * (bitlen address + bitlen value) + 7

The exact optimized entry-decoding time is linear in the two word widths.

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeLinearTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryDecodeTapes n) (address value inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryDecodeLinearTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryDecodeLinearTM tapes).reachesIn time start current) (htime : time ≤ entryDecodeLinearTime address value) : current.WithinAuxSpace inputLength (initialSpace + entryDecodeLinearTime address value)

Coarse all-prefix auxiliary-space envelope for optimized entry decoding.

theorem Complexity.RAM.RegisterStore.Machine.entryDecodeLinearTM_isTransducer {n : ℕ} (tapes : EntryDecodeTapes n) : (entryDecodeLinearTM tapes).IsTransducer

Optimized entry decoding preserves one-way output safety.