Reading a string as a normal form verifier: the wrapper decider

Blueprint rem:compression-abstract, item 1: a string of the compressibility criterion is a pair (λ, 𝒟) of a parameter and a decider program, read as the verifier (S^compr_λ, wrap 𝒟). The wrapper is what makes the pair a normal form verifier: the one structural requirement of def:normal-verifier is Verifier.accepts_length, that the decider accept only questions of the sampler's dimension — the paper's step 1, "compute the dimension s(n) of the sampler and check |x| = |y| = s(n); if not, reject".

Nothing else has to be enforced. Synchronicity at an index and the answer-length bound are conditions on membership in the classes (Verifier.InClassA, InClassB), not on well-formedness, so the wrapper leaves them to the class definition; and the paper's timeout counter is likewise not needed here, since a decider that fails to halt simply fails to be n-bounded, and its string then lies in neither class.

• Prog.wrapCore univ sampProg dec: on input (N, x, y, a, b), run sampProg on (N, dimension) through the universal machine univ, convert the dimension to unary, compare it with the lengths of x and of y, and run dec on the whole input through univ if both match, rejecting otherwise.
• The three forward runs (wrapCore_runs_of_eq, wrapCore_runs_of_ne_left, wrapCore_runs_of_ne_right) and the inversion wrapCore_halts_of, which is what turns them into the characterization of acceptance.
• Decider.wrap, Decider.wrap_accepts, and Verifier.ofSamplerDeciderD, the normal form verifier a pair denotes. The decider component is a datum run by the universal machine, not a program: a string carries data, a datum that is not the encoding of any program still has to name a verifier, and reading it as a program would need a decoder with a fallback (once Cost.progNorm, in a module since removed) that the compressor's decider of obligation O4 would then have to reimplement in the ambient model — its tree-grammar check as a worklist program — only to reproduce a fallback nobody wanted. On the encoding of a program the two readings agree (wrap_accepts_prog, by UniversalMachine.time_le and halts_of), and Verifier.ofSamplerDecider is that special case, which the two distinguished strings use.

The program

def MIPRE.Cost.Prog.wrapCheck (i j : ℕ) (c : Prog) : Prog

One length check, reusable for both questions: read the length of the bit string at index i, compare it with the unary numeral at index j, and continue with c if they agree, rejecting otherwise.

Equations

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

def MIPRE.Cost.Prog.wrapCheckEnv (l : BitStr) (m : ℕ) (env : Env) : Env

The environment wrapCheck hands to its continuation.

Equations

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

def MIPRE.Cost.Prog.wrapTail (univ : Prog) (decD : Data) : Prog

The last step: run the string's decider — the datum decD, which the string carries and which need not be the encoding of any program — on the whole input, through univ. At this point the input sits at index 19.

Equations

• univ.wrapTail decD = ((MIPRE.Cost.Prog.const decD).cons (MIPRE.Cost.Prog.var 19)).let_ (MIPRE.Cost.Prog.callVar 0 univ)

def MIPRE.Cost.Prog.wrapHead (univ sampProg c : Prog) : Prog

The head: compute the sampler's dimension at the input index, in unary.

Equations

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

def MIPRE.Cost.Prog.wrapPre (univ sampProg c : Prog) : Prog

The prefix: the head, then the two questions taken apart.

Equations

• univ.wrapPre sampProg c = univ.wrapHead sampProg (MIPRE.Cost.Prog.elim 4 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.elim 1 MIPRE.Cost.Prog.nil c))

def MIPRE.Cost.Prog.wrapCore (univ sampProg : Prog) (decD : Data) : Prog

The wrapper's program. Input: encode (N, x, y, a, b).

Equations

• univ.wrapCore sampProg decD = univ.wrapPre sampProg (MIPRE.Cost.Prog.wrapCheck 2 4 (MIPRE.Cost.Prog.wrapCheck 5 9 (univ.wrapTail decD)))

theorem MIPRE.Cost.Prog.wrapCheck_wellScoped {i j n : ℕ} (hi : i < n) (hj : j < n) {c : Prog} (hc : WellScoped (n + 5) c) : WellScoped n (wrapCheck i j c)

theorem MIPRE.Cost.Prog.wrapTail_wellScoped {univ : Prog} (hU : WellScoped 1 univ) (decD : Data) : WellScoped 20 (univ.wrapTail decD)

theorem MIPRE.Cost.Prog.wrapHead_wellScoped {univ : Prog} (hU : WellScoped 1 univ) (sampProg : Prog) {c : Prog} (hc : WellScoped 6 c) : WellScoped 1 (univ.wrapHead sampProg c)

theorem MIPRE.Cost.Prog.wrapPre_wellScoped {univ : Prog} (hU : WellScoped 1 univ) (sampProg : Prog) {c : Prog} (hc : WellScoped 10 c) : WellScoped 1 (univ.wrapPre sampProg c)

theorem MIPRE.Cost.Prog.wrapCore_wellScoped {univ : Prog} (hU : WellScoped 1 univ) (sampProg : Prog) (decD : Data) : WellScoped 1 (univ.wrapCore sampProg decD)

The length check

theorem MIPRE.Cost.Prog.len_run (z : BitStr) : ∃ (t : ℕ), lenProg.Runs (encode z) (Data.ofNat (List.length z)) t

theorem MIPRE.Cost.Prog.eq_run (p q : ℕ) : ∃ (t : ℕ), eqBitsProg.Runs ((Data.ofNat p).cons (Data.ofNat q)) (encode (decide (p = q))) t

theorem MIPRE.Cost.Prog.wrapCheck_runs_of_ne {i j : ℕ} {c : Prog} {env : Env} {l : BitStr} {m : ℕ} (hi : env.get i = encode l) (hj : env.get j = Data.ofNat m) (hne : List.length l ≠ m) : ∃ (t : ℕ), Eval env (wrapCheck i j c) Data.nil t

theorem MIPRE.Cost.Prog.wrapCheck_runs_of_eq {i j : ℕ} {c : Prog} {env : Env} {l : BitStr} {m : ℕ} (hi : env.get i = encode l) (hj : env.get j = Data.ofNat m) (heq : List.length l = m) {r : Data} {t : ℕ} (hc : Eval (wrapCheckEnv l m env) c r t) : ∃ (t' : ℕ), Eval env (wrapCheck i j c) r t'

theorem MIPRE.Cost.Prog.wrapCheck_inv {i j : ℕ} {c : Prog} {env : Env} {l : BitStr} {m : ℕ} (hi : env.get i = encode l) (hj : env.get j = Data.ofNat m) {r : Data} {t : ℕ} (h : Eval env (wrapCheck i j c) r t) : List.length l ≠ m ∧ r = Data.nil ∨ List.length l = m ∧ ∃ (t' : ℕ), Eval (wrapCheckEnv l m env) c r t'

Inversion. A run of the check either fails the comparison and returns nil, or passes it and is a run of the continuation.

The whole run

def MIPRE.Cost.Prog.wrapPreEnv {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (x y a b : BitStr) : Env

The environment the prefix hands to the first length check.

Equations

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

theorem MIPRE.Cost.Prog.dim_run {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (n : ℕ) : ∃ (t : ℕ), U.univ.Runs ((encode S.prog).cons ((encode n).cons (encode CL.Sampler.Query.dimension))) (encode (S.dim n)) t

theorem MIPRE.Cost.Prog.toUnary_run (k : ℕ) : ∃ (t : ℕ), toUnaryProg.Runs (encode k) (Data.ofNat k) t

theorem MIPRE.Cost.Prog.input_cons (n : ℕ) (x y a b : BitStr) : encode (n, x, y, a, b) = (encode n).cons ((encode x).cons ((encode y).cons ((encode a).cons (encode b))))

theorem MIPRE.Cost.Prog.wrapPre_runs {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (n : ℕ) (x y a b : BitStr) {c : Prog} {r : Data} {t : ℕ} (hc : Eval (wrapPreEnv S n x y a b) c r t) : ∃ (t' : ℕ), Eval [encode (n, x, y, a, b)] (U.univ.wrapPre S.prog c) r t'

The prefix runs, whatever the continuation does.

theorem MIPRE.Cost.Prog.wrapPre_inv {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (n : ℕ) (x y a b : BitStr) {c : Prog} {r : Data} {t : ℕ} (h : Eval [encode (n, x, y, a, b)] (U.univ.wrapPre S.prog c) r t) : ∃ (t' : ℕ), Eval (wrapPreEnv S n x y a b) c r t'

Inversion of the prefix.

The three outcomes

theorem MIPRE.Cost.Prog.wrapCore_runs_of_ne_left {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (decD : Data) (n : ℕ) (x y a b : BitStr) (hx : List.length x ≠ S.dim n) : ∃ (t : ℕ), (U.univ.wrapCore S.prog decD).Runs (encode (n, x, y, a, b)) Data.nil t

theorem MIPRE.Cost.Prog.wrapCore_runs_of_ne_right {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (decD : Data) (n : ℕ) (x y a b : BitStr) (hx : List.length x = S.dim n) (hy : List.length y ≠ S.dim n) : ∃ (t : ℕ), (U.univ.wrapCore S.prog decD).Runs (encode (n, x, y, a, b)) Data.nil t

theorem MIPRE.Cost.Prog.wrapCore_runs_of_eq {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (decD : Data) (n : ℕ) (x y a b : BitStr) (hx : List.length x = S.dim n) (hy : List.length y = S.dim n) {r : Data} {t₇ : ℕ} (h₇ : U.univ.Runs (decD.cons (encode (n, x, y, a, b))) r t₇) : ∃ (t : ℕ), (U.univ.wrapCore S.prog decD).Runs (encode (n, x, y, a, b)) r t

theorem MIPRE.Cost.Prog.wrapCore_halts_inv {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (decD : Data) (n : ℕ) (x y a b : BitStr) {r : Data} {t : ℕ} (h : (U.univ.wrapCore S.prog decD).Runs (encode (n, x, y, a, b)) r t) : r = Data.nil ∨ ∃ (t' : ℕ), U.univ.Runs (decD.cons (encode (n, x, y, a, b))) r t'

The wrapper halts only if the universal machine does on the string's decider.

The wrapped decider and the verifier a pair denotes

def MIPRE.Decider.wrap {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (decD : Cost.Data) : Decider

The decider a string denotes: the datum decD the string carries, run by the universal machine, wrapped in the question-length check against the sampler S. The datum need not be the encoding of a program; when it is, encode dec, the run is a run of dec (wrap_accepts_prog).

Equations

• MIPRE.Decider.wrap U S decD = { prog := U.univ.wrapCore S.prog decD, closed := ⋯ }

@[simp]

theorem MIPRE.Decider.wrap_prog {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (decD : Cost.Data) : (wrap U S decD).prog = U.univ.wrapCore S.prog decD

theorem MIPRE.Decider.wrap_accepts {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (decD : Cost.Data) (n : ℕ) (x y a b : Cost.BitStr) : (wrap U S decD).Accepts n x y a b ↔ List.length x = S.dim n ∧ List.length y = S.dim n ∧ ∃ (t : ℕ), U.univ.Runs (decD.cons (Cost.encode (n, x, y, a, b))) (Cost.encode true) t

Acceptance of the wrapped decider: the two questions have the sampler's dimension and the universal machine, run on the string's decider and the input, returns true.

theorem MIPRE.Decider.wrap_accepts_prog {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (dec : Cost.Prog) (n : ℕ) (x y a b : Cost.BitStr) : (wrap U S (Cost.encode dec)).Accepts n x y a b ↔ List.length x = S.dim n ∧ List.length y = S.dim n ∧ ∃ (t : ℕ), dec.Runs (Cost.encode (n, x, y, a, b)) (Cost.encode true) t

Acceptance when the datum is the encoding of a program dec: the universal machine's run is a run of dec (UniversalMachine.time_le, halts_of).

theorem MIPRE.Decider.wrap_accepts_length {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (decD : Cost.Data) (n : ℕ) (x y a b : Cost.BitStr) (h : (wrap U S decD).Accepts n x y a b) : List.length x = S.dim n ∧ List.length y = S.dim n

The wrapped decider accepts only questions of the sampler's dimension: the one structural requirement of def:normal-verifier.

def MIPRE.Verifier.ofSamplerDeciderD {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (decD : Cost.Data) : Verifier ℓ

The verifier a pair (S, d) denotes: the sampler S, and the datum d — the string's decider, run by the universal machine — wrapped in the question-length check. Every pair denotes one, well formed or not.

Equations

• MIPRE.Verifier.ofSamplerDeciderD U S decD = { sampler := S, decider := MIPRE.Decider.wrap U S decD, accepts_length := ⋯ }

def MIPRE.Verifier.ofSamplerDecider {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (dec : Cost.Prog) : Verifier ℓ

The verifier a pair (S, 𝒟) of a sampler and a decider program denotes: ofSamplerDeciderD at the program's encoding.

Equations

• MIPRE.Verifier.ofSamplerDecider U S dec = MIPRE.Verifier.ofSamplerDeciderD U S (MIPRE.Cost.encode dec)

@[simp]

theorem MIPRE.Verifier.ofSamplerDeciderD_sampler {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (decD : Cost.Data) : (ofSamplerDeciderD U S decD).sampler = S

@[simp]

theorem MIPRE.Verifier.ofSamplerDecider_sampler {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (dec : Cost.Prog) : (ofSamplerDecider U S dec).sampler = S

theorem MIPRE.Verifier.ofSamplerDeciderD_accepts {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (decD : Cost.Data) (n : ℕ) (x y a b : Cost.BitStr) : (ofSamplerDeciderD U S decD).decider.Accepts n x y a b ↔ List.length x = S.dim n ∧ List.length y = S.dim n ∧ ∃ (t : ℕ), U.univ.Runs (decD.cons (Cost.encode (n, x, y, a, b))) (Cost.encode true) t

theorem MIPRE.Verifier.ofSamplerDecider_accepts {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (dec : Cost.Prog) (n : ℕ) (x y a b : Cost.BitStr) : (ofSamplerDecider U S dec).decider.Accepts n x y a b ↔ List.length x = S.dim n ∧ List.length y = S.dim n ∧ ∃ (t : ℕ), dec.Runs (Cost.encode (n, x, y, a, b)) (Cost.encode true) t

The wrapper at the level of data

Decider.wrap is what Verifier.IsBounded bounds, and it is therefore what a tabulation has to run: the bound says nothing about the inner decider, the datum the string carries, since UniversalMachine.halts_of produces a run with no bound on its cost. So the tabulation needs encode (wrapCore univ sampProg decD) as a primitive recursive function of the encoded sampler program and the datum — which it can be, because wrapCore mentions the sampler program only under Prog.const (encode ·) and the datum only under Prog.const.

ProgD is that mirror: the constructors of Prog at the level of Data, and the wrapper rebuilt from them. Every _eq lemma is rfl, Prog.toData being structural, and dWrapCore_eq is rfl too — nothing here is a second definition to keep in step with the first, it is the same definition seen through the encoding. The existing wrapCheck, wrapHead, wrapTail, wrapCore and everything proved about them are untouched.

def MIPRE.Cost.Prog.ProgD.dV (i : ℕ) : Data

Equations

• MIPRE.Cost.Prog.ProgD.dV i = (MIPRE.Cost.Data.ofNat 0).cons (MIPRE.Cost.Data.ofNat i)

def MIPRE.Cost.Prog.ProgD.dNil : Data

Equations

• MIPRE.Cost.Prog.ProgD.dNil = (MIPRE.Cost.Data.ofNat 1).cons MIPRE.Cost.Data.nil

def MIPRE.Cost.Prog.ProgD.dC (h t : Data) : Data

Equations

• MIPRE.Cost.Prog.ProgD.dC h t = (MIPRE.Cost.Data.ofNat 2).cons (h.cons t)

def MIPRE.Cost.Prog.ProgD.dE (i : ℕ) (n c : Data) : Data

Equations

• MIPRE.Cost.Prog.ProgD.dE i n c = (MIPRE.Cost.Data.ofNat 3).cons ((MIPRE.Cost.Data.ofNat i).cons (n.cons c))

def MIPRE.Cost.Prog.ProgD.dL (e b : Data) : Data

Equations

• MIPRE.Cost.Prog.ProgD.dL e b = (MIPRE.Cost.Data.ofNat 4).cons (e.cons b)

def MIPRE.Cost.Prog.ProgD.dK (d : Data) : Data

Equations

• MIPRE.Cost.Prog.ProgD.dK d = (MIPRE.Cost.Data.ofNat 6).cons d

theorem MIPRE.Cost.Prog.ProgD.primrec_dC : Primrec₂ dC

theorem MIPRE.Cost.Prog.ProgD.primrec_dL : Primrec₂ dL

theorem MIPRE.Cost.Prog.ProgD.primrec_dK : Primrec dK

theorem MIPRE.Cost.Prog.ProgD.primrec_dE (i : ℕ) : Primrec₂ (dE i)

The wrapper, at the level of data.

def MIPRE.Cost.Prog.ProgD.dWrapCheck (i j : ℕ) (c : Data) : Data

Equations

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

def MIPRE.Cost.Prog.ProgD.dWrapTail (univ decD : Data) : Data

Equations

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

def MIPRE.Cost.Prog.ProgD.dWrapHead (univ sampD c : Data) : Data

Equations

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

def MIPRE.Cost.Prog.ProgD.dWrapCore (univ sampD decD : Data) : Data

Equations

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

theorem MIPRE.Cost.Prog.ProgD.dWrapCore_eq (univ sampProg : Prog) (decD : Data) : dWrapCore (encode univ) (encode sampProg) decD = encode (univ.wrapCore sampProg decD)

theorem MIPRE.Cost.Prog.ProgD.primrec_dWrapCheck (i j : ℕ) : Primrec (dWrapCheck i j)

theorem MIPRE.Cost.Prog.ProgD.primrec_dWrapTail (univ : Data) : Primrec (dWrapTail univ)

theorem MIPRE.Cost.Prog.ProgD.primrec_dWrapCore (univ : Data) : Primrec₂ (dWrapCore univ)