claimroutineinferred_dep

Callback compiles virtual padded input reads

Callback answers virtual padded-input reads using four

O(B_n)

-bit words

avoids storing the exponentially long padded input

Claim·§13.4 Compiling the virtual input operations·inside thmEffective compiler from randomized to deterministic logspace

Statement (paper)

The generated machine

D

simulates the library

A

on the padded input, answering each virtual input read by a callback that uses only the four auxiliary words (the length count

n+1

N_{\mathrm{pad}}+1

J

I

), each of at most

PB_n+2

bits. The callback returns the correct endmarker when

J=0

J=N_{\mathrm{pad}}+1

, regenerates the prefix symbol at address

J

from the real input, and returns zero for a padding address, leaving the library's work tapes untouched. Every auxiliary routine terminates,

D

is total, and the generation of

D

is a finite effective process that does not test the source's promises.

In plain English

The deterministic machine

D

simulates the library

A

on the padded input without writing it out, answering each virtual input read with a callback that keeps only four auxiliary words (

n+1

N_{\mathrm{pad}}+1

J

I

) of at most

PB_n+2

bits each. The callback returns the endmarker at addresses

J=0

and

J=N_{\mathrm{pad}}+1

, recomputes the prefix symbol at address

J

from the real input, and returns zero on padding addresses, all without disturbing the library's work tapes; every routine terminates, so

D

is total and its generation is effective without checking the source's promises.

Why it's here

This makes the padded input

y_x

(whose acceptance behaviour matches

M(x)

by the padding claim) available to the library

A

using only a few logarithmic-size words, so no exponentially long input is ever stored. It supplies the callback data whose space is bounded alongside the library's tapes in the next claim, and ensures

D

is a total, effectively generated machine independent of whether

M

meets its promises.

Classified routine:

Standard virtual-input (composition of logspace computations by recomputing input symbols on demand) technique, as in the textbook proof that logspace reductions compose (e.g., Arora–Barak), applied to the padded input from the earlier padding claim.

Uses

claimFixed deterministic library decides interpreter promiseclaimPadding preserves acceptance probability exactly

Used by

claimSimultaneous work-space bound on all tapes

Sources

PaperOpen

Section: §13.4 Compiling the virtual input operations
Page: —
Label: —
Line: sections/compiler.tex:353

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Callback compiles virtual padded input reads" rests on claim-thm-effective-simulation-1
info
inferred_dep
outline: "Callback compiles virtual padded input reads" rests on claim-thm-effective-simulation-2