Dense public-input lookup -- proof internals #
theorem
Complexity.RAM.RegisterStore.Machine.denseInputIdleTM_reachesIn_frame_internal
{n : ℕ}
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hinput : TM.Parked inp₀)
(hwork : ∀ (i : Fin n), TM.Parked (work₀ i))
(houtput : TM.Parked out₀)
:
∃ (c' : Complexity.Cfg n denseInputIdleTM.Q),
denseInputIdleTM.reachesIn 1 { state := denseInputIdleTM.qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ denseInputIdleTM.halted c' ∧ c'.input = inp₀ ∧ c'.work = work₀ ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.capturePreviousInputBitTM_reachesIn_frame_internal
{n : ℕ}
(result : Fin n)
(bit : Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hinput : inp₀.StartInvariant)
(hhead : 2 ≤ inp₀.head)
(hbit : inp₀.cells (inp₀.head - 1) = Γ.ofBool bit)
(hresult : work₀ result = TM.resetBinaryBlank)
(hwork : ∀ (i : Fin n), TM.Parked (work₀ i))
(houtput : TM.Parked out₀)
:
∃ (c' : Complexity.Cfg n (capturePreviousInputBitTM result).Q),
(capturePreviousInputBitTM result).reachesIn 2
{ state := (capturePreviousInputBitTM result).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (capturePreviousInputBitTM result).halted c' ∧ c'.input = inp₀ ∧ c'.work = Function.update work₀ result (denseInputBitTape bit) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.denseInputBitTape_hasBinaryNat_internal
(bit : Bool)
:
(denseInputBitTape bit).HasBinaryNat (if bit = true then 1 else 0)
theorem
Complexity.RAM.RegisterStore.Machine.denseInputStepTM_reachesIn_frame_internal
{n : ℕ}
(counter result : Fin n)
(hne : counter ≠ result)
(remaining : ℕ)
(bit : Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hinput : inp₀.StartInvariant)
(hhead : 2 ≤ inp₀.head)
(hbit : inp₀.cells (inp₀.head - 1) = Γ.ofBool bit)
(hcounter : (work₀ counter).HasBinaryNat remaining)
(hresult : remaining = 1 → work₀ result = TM.resetBinaryBlank)
(hwork : ∀ (i : Fin n), TM.Parked (work₀ i))
(houtput : TM.Parked out₀)
:
∃ (c' : Complexity.Cfg n (denseInputStepTM counter result).Q),
(denseInputStepTM counter result).reachesIn (denseInputStepTime remaining)
{ state := (denseInputStepTM counter result).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (denseInputStepTM counter result).halted c' ∧ c'.input = inp₀ ∧ (c'.work counter).HasBinaryNat (remaining - 1) ∧ c'.work result = denseInputStepResult remaining bit (work₀ result) ∧ (∀ (i : Fin n), i ≠ counter → i ≠ result → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.denseInputScanTM_reachesIn_frame_internal
{n : ℕ}
(counter result : Fin n)
(hne : counter ≠ result)
(input : List Bool)
(address : ℕ)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(haddress : address ≠ 0)
(hcounter : (work₀ counter).HasBinaryNat address)
(hresult : work₀ result = TM.resetBinaryBlank)
(hwork : ∀ (i : Fin n), TM.Parked (work₀ i))
(houtput : TM.Parked out₀)
:
∃ (c' : Complexity.Cfg n (denseInputScanTM counter result).Q),
(denseInputScanTM counter result).reachesIn (denseInputScanTime input.length address)
{ state := (denseInputScanTM counter result).qstart,
input := (Tape.init (List.map Γ.ofBool input)).move Dir3.right, work := work₀, output := out₀ }
c' ∧ (denseInputScanTM counter result).halted c' ∧ c'.input.head = input.length + 1 ∧ c'.input.cells = (Tape.init (List.map Γ.ofBool input)).cells ∧ (c'.work counter).HasBinaryNat (address - input.length) ∧ (c'.work result).HasBinaryNat (initRegs input address) ∧ (∀ (i : Fin n), i ≠ counter → i ≠ result → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.denseInputScanTime_le_width_internal
(inputLength address : ℕ)
:
theorem
Complexity.RAM.RegisterStore.Machine.denseInputLookupTM_hoareTime_internal
{n : ℕ}
(query counter result scratch : Fin n)
(hqc : query ≠ counter)
(hqr : query ≠ result)
(hqs : query ≠ scratch)
(hcr : counter ≠ result)
(hcs : counter ≠ scratch)
(hrs : result ≠ scratch)
(input : List Bool)
(address : ℕ)
(initialWork : Fin n → Tape)
(out₀ : Tape)
(haddress : address ≠ 0)
(hready : DenseInputLookupReady query counter result scratch address initialWork)
(houtput : TM.Parked out₀)
:
(denseInputLookupTM query counter result scratch).HoareTime
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInputLookupResult query counter result scratch input address initialWork work ∧ out = out₀)
(denseInputLookupTime input.length address)