Converse of Liu–Pass: Average-Case Hardness of $K^t$ Implies One-Way Functions

This module formalizes the Section 4 converse construction of Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity (Theorem 4.1, §4, p. 10 and Theorem 3.1 (b) $\Rightarrow$ (a), §3, p. 9 of arXiv:2009.11514v1): if $t$-time-bounded Kolmogorov complexity $K^t$ is mildly hard on average against uniform strict PPT heuristics for some polynomial-time computable time bound $t(n) \ge n + 1$, then there exists a weak one-way function (Cslib.Crypto.WeakOneWay), and therefore by Yao's hardness amplification (Cslib.Crypto.WeakOneWay.exists_oneWay) there exists a strong one-way function (Cslib.Crypto.OneWay).

Model note ($t(n) \ge n + 1$ sufficient clock hypothesis vs. $t(n) > 0$): In Liu and Pass, Fact 2.1, §2.2, p. 8; Theorem 3.1 (b), §3, p. 9; Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1, the time bound is stated as $t(n) > 0$ under a machine model in which outputting an $n$-bit string takes at least $1$ step. Under complexitylib's multi-tape Turing machine output convention (DescriptionMethod.universalTM), the literal/copy program bound supplies a program that prints each $n$-bit string within $n + 1$ steps (Kolmogorov.timeBoundedNat_le_length_add). This module assumes ∀ n, n + 1 ≤ t n so that bound ensures finite $K^t$ for every input; this is a sufficient clock hypothesis in the native model, rather than a lower bound on every program or an equivalence with the source's $t(n) > 0$ convention.

Construction Overview (Liu and Pass, Proof of Theorem 4.1, §4, p. 10)

1. Parameter-indexed candidate function (LiuPassConverse.liuPassCore): At parameter $n \in \mathbb{N}$, every string $y \in \{0, 1\}^n$ has time-bounded Kolmogorov complexity $K^t(y) \le n + \mathrm{copyOverhead} =: \mathrm{maxComplexity}(n)$ whenever $t(n) \ge n + 1$ (Kolmogorov.timeBoundedNat_le_length_add). Set $\mathrm{lenWidth}(n) := \lfloor \log_2(\mathrm{maxComplexity}(n)) \rfloor + 1$ and $\mathrm{inputSchedule}(n) := \mathrm{lenWidth}(n) + \mathrm{maxComplexity}(n)$. On an input $x \in \{0, 1\}^{\mathrm{inputSchedule}(n)}$, liuPassCore t n x decodes the $\mathrm{lenWidth}(n)$-bit prefix in binary (capped at $\mathrm{maxComplexity}(n)$ via BitString.boundedBinaryValue) to a length $i \le \mathrm{maxComplexity}(n)$, extracts the $i$-bit program prefix $\Pi$ from the remaining $\mathrm{maxComplexity}(n)$ bits, and outputs the framed pair (i, universalTMRunFor Π (t n)).
2. Preimage soundness and shared-coin PPT heuristic reduction: Any preimage of targetImage i y = (i, some y) under liuPassCore t n yields a program of length at most $i$ that outputs $y$ within $t(n)$ steps, certifying $K^t(y) \le i$ (timeBoundedNat_le_of_liuPassCore_eq_targetImage). Whereas Liu and Pass (§4, p. 10) fix a "good" random tape by an averaging argument and union bound (obtaining weak-OWF polynomial $q(n) = 2^{2c+3} n p(n)^2$), our proof shares a single polynomial coin tape across all $\mathrm{maxComplexity}(n) + 1$ queries via IsPPTOn.exists_total_seeded_evaluator and searches over $i \in \{0, \dots, \mathrm{maxComplexity}(n)\}$ to define a uniform strict PPT heuristic $\mathcal{H}$ for timeBoundedNat t. Whenever the inverter $\mathcal{A}$ succeeds on the planted challenge targetImage (timeBoundedNat t y) y, no smaller $i < K^t(y)$ can have any valid preimage, so $\mathcal{H}(y)$ deterministically recovers $K^t(y)$, yielding the tighter linear-in-$p$ weak-OWF polynomial $q(n) = 2^{\mathrm{copyOverhead} + 1}(n + \mathrm{copyOverhead} + 1) p(n)$.
3. Measure lower bound via canonical planting (plant): Mapping each $y \in \{0, 1\}^n$ to the canonical $\mathrm{inputSchedule}(n)$-bit input encoding its shortest $t(n)$-time program $\Pi^*_y$ (exists_length_eq_timeBoundedNat) padded with zeros (exists_liuPassCore_eq_targetImage_timeBoundedNat) is injective on BitString n → BitString (inputSchedule n) and scales uniform probability mass by exact factor $2^{-(\mathrm{lenWidth}(n) + \mathrm{copyOverhead})} \ge \frac{1}{2^{\mathrm{copyOverhead} + 1}(n + \mathrm{copyOverhead} + 1)}$. Consequently, the failure probability of $\mathcal{A}$ in familyInversionGame is at least $\frac{1}{q(n)}$ whenever $\mathcal{H}$ fails with probability at least $\frac{1}{p(n)}$.
4. Schedule reindexing and Yao amplification: Applying OneWayReindex.weakOneWay extends liuPassCore t to a weak one-way function on all input lengths (weakOneWay_reindex_liuPassCore, exists_weakOneWay_of_mildlyHardOnAverage_timeBoundedNat), and WeakOneWay.exists_oneWay yields a strong one-way function (exists_oneWay_of_mildlyHardOnAverage_timeBoundedNat).

Main definitions

• Cslib.Crypto.LiuPassConverse.maxComplexity, Cslib.Crypto.LiuPassConverse.lenWidth, Cslib.Crypto.LiuPassConverse.inputSchedule: complexity bound $n + \mathrm{copyOverhead}$, binary length-prefix width, and total input length at parameter $n$.
• Cslib.Crypto.LiuPassConverse.liuPassCore: the Section 4 parameter-indexed candidate one-way function family $(i, \Pi') \mapsto (i, U(\Pi.\mathrm{take}\ i, 1^{t(n)}))$.

Main results

• Cslib.Crypto.LiuPassConverse.timeBoundedNat_le_of_liuPassCore_eq_targetImage, Cslib.Crypto.LiuPassConverse.exists_liuPassCore_eq_targetImage_timeBoundedNat: preimage soundness and canonical preimage existence for liuPassCore.
• Cslib.Crypto.weakOneWay_reindex_liuPassCore, Cslib.Crypto.exists_weakOneWay_of_mildlyHardOnAverage_timeBoundedNat, Cslib.Crypto.exists_weakOneWay_of_mildlyHardOnAverageENat_timeBounded: Liu and Pass, Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1.
• Cslib.Crypto.exists_oneWay_of_mildlyHardOnAverage_timeBoundedNat, Cslib.Crypto.exists_oneWay_of_mildlyHardOnAverageENat_timeBounded, Cslib.Crypto.exists_oneWay_of_exists_mildlyHardOnAverage_timeBoundedNat, Cslib.Crypto.exists_oneWay_of_exists_mildlyHardOnAverageENat_timeBounded: Liu and Pass, Theorem 3.1 (b) $\Rightarrow$ (a), §3, p. 9 of arXiv:2009.11514v1.

References

• Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity, full version arXiv:2009.11514v1 (Sections 3 and 4).

Section 4 schedule and core function (liuPassCore)

noncomputable def Cslib.Crypto.LiuPassConverse.maxComplexity (n : ℕ) : ℕ

Upper bound $n + \mathrm{copyOverhead}$ on timeBoundedNat t y for all $y \in \{0, 1\}^n$ when $t(n) \ge n + 1$.

noncomputable def Cslib.Crypto.LiuPassConverse.lenWidth (n : ℕ) : ℕ

Bit width $\lfloor \log_2(\mathrm{maxComplexity}(n)) \rfloor + 1$ for binary encoding of program lengths $i \in \{0, \dots, \mathrm{maxComplexity}(n)\}$.

noncomputable def Cslib.Crypto.LiuPassConverse.inputSchedule (n : ℕ) : ℕ

Input length schedule $m(n) = \mathrm{lenWidth}(n) + \mathrm{maxComplexity}(n)$ at parameter $n$.

theorem Cslib.Crypto.LiuPassConverse.le_inputSchedule (n : ℕ) : n + 1 ≤ inputSchedule n

noncomputable def Cslib.Crypto.LiuPassConverse.decodeLen (n : ℕ) (x : List Bool) : ℕ

Decode the program-length prefix $i \in \{0, \dots, \mathrm{maxComplexity}(n)\}$ from the first lenWidth n bits of x.

theorem Cslib.Crypto.LiuPassConverse.decodeLen_le (n : ℕ) (x : List Bool) : decodeLen n x ≤ maxComplexity n

noncomputable def Cslib.Crypto.LiuPassConverse.decodeProg (n : ℕ) (x : List Bool) : List Bool

Extract the candidate program of length at most decodeLen n x after the lenWidth n-bit prefix of x.

theorem Cslib.Crypto.LiuPassConverse.length_decodeProg_le (n : ℕ) (x : List Bool) : (decodeProg n x).length ≤ decodeLen n x

noncomputable def Cslib.Crypto.LiuPassConverse.liuPassCore (t : ℕ → ℕ) (n : ℕ) (x : List Bool) : List Bool

Section 4 parameter-indexed candidate one-way function family (Liu and Pass, §4, p. 10 of arXiv:2009.11514v1): parse $x$ into a length $i := \mathrm{decodeLen}\ n\ x \le n + \mathrm{copyOverhead}$ and a program $\Pi := \mathrm{decodeProg}\ n\ x$ of length at most $i$, run the universal multi-tape Turing machine on $\Pi$ for $t(n)$ steps, and output the framed pair (i, universalTMRunFor Π (t n)).

def Cslib.Crypto.LiuPassConverse.targetImage (i : ℕ) (y : List Bool) : List Bool

Framed target output corresponding to program length i and halting output some y.

@[simp]

theorem Cslib.Crypto.LiuPassConverse.targetImage_inj {i₁ i₂ : ℕ} {y₁ y₂ : List Bool} : targetImage i₁ y₁ = targetImage i₂ y₂ ↔ i₁ = i₂ ∧ y₁ = y₂

theorem Cslib.Crypto.LiuPassConverse.liuPassCore_eq_targetImage_iff {t : ℕ → ℕ} {n i : ℕ} {x y : List Bool} : liuPassCore t n x = targetImage i y ↔ decodeLen n x = i ∧ Kolmogorov.DescriptionMethod.universalTMRunFor (decodeProg n x) (t n) = some y

Polynomial-time computability of schedule and core

theorem Cslib.Crypto.LiuPassConverse.computableInPolyTime_inputSchedule : Turing.MultiTapeTM.ComputableInPolyTime inputSchedule Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

theorem Cslib.Crypto.LiuPassConverse.computableInPolyTime_liuPassCore {t : ℕ → ℕ} (ht : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => liuPassCore t p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

Preimage soundness and canonical planting

theorem Cslib.Crypto.LiuPassConverse.timeBoundedNat_le_of_liuPassCore_eq_targetImage {t : ℕ → ℕ} {n i : ℕ} {x y : List Bool} (hy : y.length = n) (ht : n + 1 ≤ t n) (h : liuPassCore t n x = targetImage i y) : Kolmogorov.timeBoundedNat t y ≤ i

Any preimage of targetImage i y under liuPassCore t n certifies timeBoundedNat t y ≤ i.

theorem Cslib.Crypto.LiuPassConverse.exists_liuPassCore_eq_targetImage_timeBoundedNat {t : ℕ → ℕ} (ht : ∀ (n : ℕ), n + 1 ≤ t n) {n : ℕ} {y : List Bool} (hy : y.length = n) : ∃ (x : List Bool), x.length = inputSchedule n ∧ liuPassCore t n x = targetImage (Kolmogorov.timeBoundedNat t y) y

Every $n$-bit string $y$ has a canonical inputSchedule n-bit preimage under liuPassCore t n for the framed output targetImage (timeBoundedNat t y) y whenever $t(n) \ge n + 1$.

Deterministic heuristic search and PPT reduction

Uniform distribution and failure probability bounds

Theorem 4.1: Mild average-case hardness of $K^t$ implies weak one-way functions

theorem Cslib.Crypto.weakOneWay_reindex_liuPassCore {t : ℕ → ℕ} (ht_comp : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (ht : ∀ (n : ℕ), n + 1 ≤ t n) (hK : Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat t)) : WeakOneWay (OneWayReindex.reindex LiuPassConverse.inputSchedule (LiuPassConverse.liuPassCore t))

Liu and Pass, Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1 (explicit candidate function): If $t : \mathbb{N} \to \mathbb{N}$ is computable in unary polynomial time with $t(n) \ge n + 1$ for all $n$ (a sufficient clock hypothesis in the native model ensuring finite $K^t$ via timeBoundedNat_le_length_add, where the source writes $t(n) > 0$), and $t$-time-bounded Kolmogorov complexity timeBoundedNat t is mildly hard on average against uniform strict PPT heuristics (MildlyHardOnAverage (timeBoundedNat t)), then the schedule-reindexed Section 4 candidate function OneWayReindex.reindex inputSchedule (liuPassCore t) is a weak one-way function (WeakOneWay).

theorem Cslib.Crypto.exists_weakOneWay_of_mildlyHardOnAverage_timeBoundedNat {t : ℕ → ℕ} (ht_comp : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (ht : ∀ (n : ℕ), n + 1 ≤ t n) (hK : Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat t)) : ∃ (f : List Bool → List Bool), WeakOneWay f

Liu and Pass, Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1 (existential form): If $t : \mathbb{N} \to \mathbb{N}$ is computable in unary polynomial time with $t(n) \ge n + 1$ for all $n$ (a sufficient clock hypothesis in the native model ensuring finite $K^t$ via timeBoundedNat_le_length_add, where the source writes $t(n) > 0$), and $t$-time-bounded Kolmogorov complexity timeBoundedNat t is mildly hard on average against uniform strict PPT heuristics (MildlyHardOnAverage (timeBoundedNat t)), then there exists a weak one-way function (WeakOneWay).

theorem Cslib.Crypto.exists_weakOneWay_of_mildlyHardOnAverageENat_timeBounded {t : ℕ → ℕ} (ht_comp : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (ht : ∀ (n : ℕ), n + 1 ≤ t n) (hK : Complexity.MildlyHardOnAverageENat (Kolmogorov.timeBounded t)) : ∃ (f : List Bool → List Bool), WeakOneWay f

ℕ∞-valued Kolmogorov.timeBounded corollary of Theorem 4.1: if timeBounded t is mildly hard on average against uniform strict PPT heuristics (MildlyHardOnAverageENat (timeBounded t)) for a polynomial-time computable $t(n) \ge n + 1$, then there exists a weak one-way function.

Theorem 3.1 (b) $\Rightarrow$ (a): Mild average-case hardness of $K^t$ implies strong

one-way functions

theorem Cslib.Crypto.exists_oneWay_of_mildlyHardOnAverage_timeBoundedNat {t : ℕ → ℕ} (ht_comp : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (ht : ∀ (n : ℕ), n + 1 ≤ t n) (hK : Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat t)) : ∃ (F : List Bool → List Bool), OneWay F

Liu and Pass, Theorem 3.1 (b) $\Rightarrow$ (a), §3, p. 9 and Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1: If $t : \mathbb{N} \to \mathbb{N}$ is computable in unary polynomial time with $t(n) \ge n + 1$ for all $n$ (a sufficient clock hypothesis in the native model ensuring finite $K^t$ via timeBoundedNat_le_length_add, where the source writes $t(n) > 0$), and $t$-time-bounded Kolmogorov complexity timeBoundedNat t is mildly hard on average against uniform strict PPT heuristics (MildlyHardOnAverage (timeBoundedNat t)), then there exists a strong one-way function (OneWay).

theorem Cslib.Crypto.exists_oneWay_of_mildlyHardOnAverageENat_timeBounded {t : ℕ → ℕ} (ht_comp : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (ht : ∀ (n : ℕ), n + 1 ≤ t n) (hK : Complexity.MildlyHardOnAverageENat (Kolmogorov.timeBounded t)) : ∃ (F : List Bool → List Bool), OneWay F

ℕ∞-valued Kolmogorov.timeBounded version of Theorem 3.1 (b) $\Rightarrow$ (a).

theorem Cslib.Crypto.exists_oneWay_of_exists_mildlyHardOnAverage_timeBoundedNat (h : ∃ (t : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n t) ∧ Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat fun (n : ℕ) => Polynomial.eval n t)) : ∃ (F : List Bool → List Bool), OneWay F

Liu and Pass, Theorem 3.1 (b) $\Rightarrow$ (a), §3, p. 9 of arXiv:2009.11514v1 (existential polynomial time-bound form): If there exists a polynomial $t \in \mathbb{N}[X]$ with $t(n) \ge n + 1$ for all $n$ (a sufficient clock hypothesis in the native model ensuring finite $K^t$ via timeBoundedNat_le_length_add, where the source writes $t(n) > 0$) such that timeBoundedNat (fun n => t.eval n) is mildly hard on average against uniform strict PPT heuristics, then there exists a strong one-way function (OneWay).

theorem Cslib.Crypto.exists_oneWay_of_exists_mildlyHardOnAverageENat_timeBounded (h : ∃ (t : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n t) ∧ Complexity.MildlyHardOnAverageENat (Kolmogorov.timeBounded fun (n : ℕ) => Polynomial.eval n t)) : ∃ (F : List Bool → List Bool), OneWay F

ℕ∞-valued Kolmogorov.timeBounded existential form of Theorem 3.1 (b) $\Rightarrow$ (a).