Freezing a verifier at an index

Blueprint rem:compression-abstract, item 2: the recursion of the compressibility criterion goes n → 2n + 1, while gap-preserving compression relates the game at index 2 ^ n to the output at index n; the two are reconciled by freezing the described verifier at index 2n + 1 before compressing it. The frozen verifier answers at every index as the original does at the frozen index, so its game at index 2 ^ n is the original's game at level 2n + 1.

• Cost.Prog.freezeProg k p: on input cons N d, run p on cons (encode k) d. Its cost is that of p plus the cost of copying the input, which is what the reading of the time bounds a polynomial in the size of the input (Decider.TimeBoundAt) allows.
• CL.Sampler.freeze, Decider.freeze, Verifier.freeze: the frozen sampler, decider and verifier, with the transfer of the query clauses, of acceptance (Decider.freeze_accepts), of the values and perfect PCC strategies (Verifier.freeze_valStar, Verifier.freeze_hasPerfectPCC), of the time bounds, and of λ-boundedness (Verifier.freeze_isBounded): the frozen verifier is λ-bounded as soon as the original's dimension, running times and size at the frozen index fit under 2 ^ λ and λ.

def MIPRE.Cost.Prog.freezeProg (k : ℕ) (p : Prog) : Prog

Freeze the index: on input cons N d, run p on cons (encode k) d.

Equations

• MIPRE.Cost.Prog.freezeProg k p = (MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil ((MIPRE.Cost.Prog.const (MIPRE.Cost.encode k)).cons (MIPRE.Cost.Prog.var 1))).let_ p

theorem MIPRE.Cost.Prog.freezeProg_wellScoped {p : Prog} (hp : WellScoped 1 p) (k : ℕ) : WellScoped 1 (freezeProg k p)

theorem MIPRE.Cost.Prog.freezeProg_prefix_eval (k : ℕ) (N d : Data) : Eval [N.cons d] (elim 0 nil ((const (encode k)).cons (var 1))) ((encode k).cons d) ((encode k).size + (d.size + 1) + 1 + 1)

The run of the index-replacing prefix of freezeProg.

theorem MIPRE.Cost.Prog.freezeProg_runs {p : Prog} (hp : WellScoped 1 p) {k : ℕ} {N d r : Data} {t : ℕ} (h : p.Runs ((encode k).cons d) r t) : (freezeProg k p).Runs (N.cons d) r (t + esize k + d.size + 4)

Forward transfer: a run of p at the frozen index gives a run of freezeProg k p at any index, at the additional cost of copying the input.

theorem MIPRE.Cost.Prog.freezeProg_runs_rev {p : Prog} (hp : WellScoped 1 p) {k : ℕ} {N d r : Data} {t : ℕ} (h : (freezeProg k p).Runs (N.cons d) r t) : ∃ t' ≤ t, p.Runs ((encode k).cons d) r t'

Backward transfer: a run of freezeProg k p is a run of p at the frozen index.

theorem MIPRE.Cost.Prog.freezeProg_runs_iff {p : Prog} (hp : WellScoped 1 p) (k : ℕ) (N d r : Data) : (∃ (t : ℕ), (freezeProg k p).Runs (N.cons d) r t) ↔ ∃ (t : ℕ), p.Runs ((encode k).cons d) r t

The frozen program halts on cons N d exactly when p halts on cons (encode k) d, with the same result.

theorem MIPRE.Cost.Prog.esize_freezeProg (k : ℕ) (p : Prog) : esize (freezeProg k p) = esize p + esize k + 53

The description of the frozen program: that of p, plus the index, plus 53 nodes.

theorem MIPRE.freeze_cost_le {T j e t s : ℕ} (ht : t ≤ T * (s + 1) ^ j) : t + e + s + 4 ≤ (T + e + 4) * (s + 1) ^ max j 1

The arithmetic shared by the two freezing time bounds: the frozen program's cost fits under the same polynomial with the coefficient shifted by the cost of copying, once the degree is at least one.

The frozen sampler

def MIPRE.CL.Sampler.freeze {ℓ : ℕ} (S : Sampler ℓ) (k : ℕ) : Sampler ℓ

The sampler frozen at index k: at every index it presents the CL functions of S at index k, its program being freezeProg k S.prog.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.CL.Sampler.freeze_prog {ℓ : ℕ} (S : Sampler ℓ) (k : ℕ) : (S.freeze k).prog = Cost.Prog.freezeProg k S.prog

@[simp]

theorem MIPRE.CL.Sampler.freeze_dim {ℓ : ℕ} (S : Sampler ℓ) (k n : ℕ) : (S.freeze k).dim n = S.dim k

@[simp]

theorem MIPRE.CL.Sampler.freeze_cl {ℓ : ℕ} (S : Sampler ℓ) (k n : ℕ) (w : Player) : (S.freeze k).cl n w = S.cl k w

theorem MIPRE.CL.Sampler.freeze_size {ℓ : ℕ} (S : Sampler ℓ) (k : ℕ) : (S.freeze k).size = S.size + Cost.esize k + 53

theorem MIPRE.CL.Sampler.freeze_timeBoundAt {ℓ : ℕ} (S : Sampler ℓ) {k T j : ℕ} (h : S.TimeBoundAt k T j) (n : ℕ) : (S.freeze k).TimeBoundAt n (T + Cost.esize k + 4) (max j 1)

The frozen sampler's running time at any index is that of S at the frozen index, up to the cost of copying the input.

The frozen decider

def MIPRE.Decider.freeze (D : Decider) (k : ℕ) : Decider

The decider frozen at index k: at every index it decides as D does at index k.

Equations

• D.freeze k = { prog := MIPRE.Cost.Prog.freezeProg k D.prog, closed := ⋯ }

@[simp]

theorem MIPRE.Decider.freeze_prog (D : Decider) (k : ℕ) : (D.freeze k).prog = Cost.Prog.freezeProg k D.prog

theorem MIPRE.Decider.freeze_accepts (D : Decider) (k n : ℕ) (x y a b : Cost.BitStr) : (D.freeze k).Accepts n x y a b ↔ D.Accepts k x y a b

theorem MIPRE.Decider.freeze_size (D : Decider) (k : ℕ) : (D.freeze k).size = D.size + Cost.esize k + 53

theorem MIPRE.Decider.freeze_timeBoundAt (D : Decider) {k T j : ℕ} (h : D.TimeBoundAt k T j) (n : ℕ) : (D.freeze k).TimeBoundAt n (T + Cost.esize k + 4) (max j 1)

The frozen verifier

def MIPRE.Verifier.freeze {ℓ : ℕ} (V : Verifier ℓ) (k : ℕ) : Verifier ℓ

The verifier frozen at index k: its game at every index is the game of V at index k.

Equations

• V.freeze k = { sampler := V.sampler.freeze k, decider := V.decider.freeze k, accepts_length := ⋯ }

@[simp]

theorem MIPRE.Verifier.freeze_sampler {ℓ : ℕ} (V : Verifier ℓ) (k : ℕ) : (V.freeze k).sampler = V.sampler.freeze k

@[simp]

theorem MIPRE.Verifier.freeze_decider {ℓ : ℕ} (V : Verifier ℓ) (k : ℕ) : (V.freeze k).decider = V.decider.freeze k

theorem MIPRE.Verifier.freeze_size {ℓ : ℕ} (V : Verifier ℓ) (k : ℕ) : (V.freeze k).size = V.size + Cost.esize k + 53

theorem MIPRE.Verifier.freeze_rejectsLong {ℓ : ℕ} (V : Verifier ℓ) (k n T : ℕ) : (V.freeze k).RejectsLong n T ↔ V.RejectsLong k T

The frozen verifier rejects long answers at any index exactly when V does at the frozen index.

theorem MIPRE.Verifier.freeze_val {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) (k n T : ℕ) : (V.freeze k).val ω n T = V.val ω k T

The value of the frozen verifier at any index is the value of V at the frozen index, in every value model.

theorem MIPRE.Verifier.freeze_valStar {ℓ : ℕ} (V : Verifier ℓ) (k n T : ℕ) : (V.freeze k).valStar n T = V.valStar k T

The value of the frozen verifier at any index is the value of V at the frozen index.

theorem MIPRE.Verifier.freeze_hasPerfectPCC {ℓ : ℕ} (V : Verifier ℓ) (k n T : ℕ) : (V.freeze k).HasPerfectPCC n T ↔ V.HasPerfectPCC k T

The frozen verifier has a perfect PCC strategy at any index exactly when V has one at the frozen index.

theorem MIPRE.Verifier.freeze_isBounded {ℓ : ℕ} (V : Verifier ℓ) (k lam TS TD jS jD : ℕ) (hS : V.sampler.TimeBoundAt k TS jS) (hD : V.decider.TimeBoundAt k TD jD) (hdim : V.sampler.dim k ≤ 2 ^ lam) (hTS : TS + Cost.esize k + 4 ≤ 2 ^ lam) (hTD : TD + Cost.esize k + 4 ≤ 2 ^ lam) (hjS : max jS 1 ≤ lam) (hjD : max jD 1 ≤ lam) (hsize : V.size + Cost.esize k + 53 ≤ lam) : (V.freeze k).IsBounded lam

λ-boundedness of the frozen verifier. The frozen verifier is λ-bounded when the dimension and the running times of V at the frozen index, shifted by the cost of freezing, fit under 2 ^ λ, and its size, shifted by the size of the index, fits under λ.