The compressor's decider: the program #

Obligation O4 of blueprint rem:compression-abstract, the program half. The compressor of the halting reduction takes a succinct description (c, n) of a string x and returns a string denoting the compressed verifier of the verifier of x frozen at index 2n + 1: its parameter is λ(n), and its decider — the datum a string carries — is the program haltProg below with (c, n, λ(n)) hardcoded. This module is that program and its acceptance agreement, CompressorSpec.accepts_compr; the accounting is separate.

The decider is the paper's machine 𝓕 (recursive.tex, fig:halt_f) with the recursion removed: the paper's 𝓕 hardcodes its own description and compresses the verifier it is the decider of, while here the string to compress is read from the description c by bit queries — the reading is what the compressibility criterion's succinct descriptions make possible — and the verifier compressed is the string's own, frozen. The paper's Step 2, running 𝓜 for n steps, is the criterion's business and does not appear.

The program prepProg G U does everything but the last step, and always halts on a succinct description:

readProg U.univ: read x from c by bit queries 0, 1, 2, … through the universal machine, stopping at the out-of-range marker of bitQueryAnswer;
parseProg, then the two projections and normBinProg: the parameter encode (descLam x) and the decider datum descDecD x;
G.samplerProg.code: the encoded sampler program sampData G x;
wrapBuildProg U.univ: the encoded wrapped decider decProgData G U x, which is encode (Vof G U x).decider.prog;
freezeBuildProg twice at index 2n + 1: the encoded programs of the frozen verifier;
G.compress.code on ((frozen sampler, frozen decider), λ(n)): the encoded compressed decider.

Then haltProg G U runs it through the universal machine on the decider's own input, and returns what the universal machine does. Forward runs of each stage compose to a forward run of haltProg; the inversion (haltProg_runs_inv) is three cases and determinism, the preparation being a single closed program with an unconditional run, and gives the acceptance agreement haltProg_accepts_iff.

Every stage carries an explicit cost, in the sizes of what it is handed, so that the accounting can be done from these lemmas alone.

Reading a string from its succinct description #

readProg univ on encode c: loop over i = 0, 1, 2, …, running univ on cons (encode c) (encode i), until the answer is the out-of-range marker ofNat 2; the bits answered are accumulated in reverse and reversed at the end. On a succinct description of x the answers are bitQueryAnswer x i, so the result is encode x.

The loop state is cons cD (cons iD acc): the description, the index in binary, and the bits read so far, most recent first.

The compressor's decider: the program #

Reading a string from its succinct description #

Building descriptions of programs #

Small pieces #

The preparation: from (c, n, λ) to the compressed decider's description #

The decider #

The compressor's output, as a string #

The preparation: from `(c, n, λ)` to the compressed decider's description #