Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
161 changes: 156 additions & 5 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,19 @@ In order:
- VOLE as an ideal functionality, and VOLE-in-the-head;
- libzk's compositional structure as a composition of these components, without ciphersuites.

### Concurrent and quantum security

- **Concurrent composition:** extend the protocol semantics with environments, scheduling,
session identifiers and concurrent executions; prove a composition theorem with efficient
simulators and explicit setup, corruption and communication assumptions. Then develop
selected adaptive-corruption and non-malleability applications, alongside the static-malicious
OT target.
- **Quantum-secure cryptography:** uniform quantum-efficient distinguishers, computational
indistinguishability with quantum side information, and security reductions for concrete
constructions. Connect the quantum-computation and lattice tracks through these adversary
models; justify each reduction in that model. Later targets include quantum oracle access,
the quantum random-oracle model, and extraction or rewinding under their precise hypotheses.

## Complexity classes and reductions

### Coverage catalogue
Expand Down Expand Up @@ -213,6 +226,17 @@ index links to canonical definitions rather than keeping a second set.
- **Immunity:** immune and bi-immune sets, P-bi-immune sets in EXP (Balcázar and Schöning), and
almost-everywhere hardness.

### Average-case complexity

- Distribution ensembles with computability and samplability certificates; distributional
reductions with explicit domination and resource bounds; DistNP, errorless average-case
classes and heuristic classes, keeping runtime tails and permitted error distinct. Reuse the
specialized Liu–Pass hardness notions through proved bridges.
- **Levin completeness:** a distributional bounded-halting problem complete for the chosen
polynomial-time computable-distribution class, followed by a separately scoped extension to
samplable distributions. Connect the framework to one-way functions, learning and the
metacomplexity track ([#798]), preserving the distribution and reduction conventions.

### Counting and modular classes

- The Another Solution Problem (ASP) framework: certify polynomial-time forward and inverse
Expand Down Expand Up @@ -271,6 +295,14 @@ universe size, not supplied as unverified input tables. In dependency order:
structures and algorithms.
- A witness-carrying reduction structure once a client needs one, for example size bounds for
Cook–Levin.
- **Logical lower-bound methods:** Ehrenfeucht–Fraïssé and pebble games with their logical
equivalence theorems, locality and concrete nondefinability results; then counting and
fixed-point expressiveness, including Cai–Fürer–Immerman-style separations. Reuse upstream
model-theoretic foundations and connect the methods to the ordered capture theorems.
- **Dynamic descriptive complexity:** dynamic programs and update semantics with explicit
initialization, auxiliary relations and domain conventions; invariant-preservation rules and
reachability in DynFO as a target. Relate logical update restrictions to the stateful-algorithm
interfaces through explicit translations.

### Uniform circuit families

Expand All @@ -283,7 +315,8 @@ DLOGTIME-uniform AC⁰ under explicit conventions.

- **TFNP:** CLS, further local search, fixed-point and equilibrium problems.
- **Parameterized:** strongly uniform variants (computable `f`), further explicit polynomial
kernels, the W and A hierarchies, and parameterized lower bounds.
kernels, the W and A hierarchies, and parameterized lower bounds; connect these to
[structural graph algorithms](#structural-graph-algorithms) and their decomposition costs.
- **Exponential-time SAT** ([#894]): amplify Schöning's random walk, with a time bound, then
PPSZ. Further fine-grained reductions and consequences of ETH, SETH and other named hypotheses.

Expand All @@ -305,8 +338,15 @@ DLOGTIME-uniform AC⁰ under explicit conventions.

### Proof complexity

Proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares, and
certified DPLL solver runtimes.
- Proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares, and
certified DPLL solver runtimes.
- **Feasible interpolation:** from a Resolution refutation of `A(x,y) ∧ B(x,z)`, construct a
circuit separating the `x` assignments extendible to `A` from those extendible to `B`, with
proof-size and extraction-time bounds. Prove the monotone variant under its polarity
hypotheses and transfer circuit and communication lower bounds to proof-size lower bounds.
- **Proof search:** automatizability and weak automatizability with explicit encodings and
runtime dependence on the shortest proof; proof-search reductions built on the Cook–Reckhow
and p-simulation APIs; then reflection principles and bounded-arithmetic witnessing theorems.

## Circuits and algebraic complexity

Expand Down Expand Up @@ -377,6 +417,10 @@ each statement against the numbered result. Organize modules by subject, not cha
list-size/agreement guarantees and decoding runtime as separate obligations; concrete
list-decodable codes for Nisan–Wigderson.
- **Boolean analysis:** hypercontractivity beyond `p ≤ 2 ≤ q` and its applications.
- **Resource-bounded measure and dimension:** martingales and gales with explicit computation
budgets, their success sets, and measure and dimension within complexity classes; connect
quantitative randomness to the Kolmogorov-complexity development. State the resource bounds
and uniformity of the betting strategies separately from ordinary measure-theoretic facts.

## Communication, queries, learning and other models

Expand All @@ -390,7 +434,12 @@ each statement against the numbered result. Organize modules by subject, not cha
The first Count-Min milestone is scoped in [#1201](https://github.com/cslib-community/complexitylib/issues/1201).
- **Learning:** machine-certified running times for the LMN and Kushilevitz–Mansour learners;
distributional problems and reductions, samplability, average-to-worst-case connections,
PAC/agnostic/SQ learning, learning lower bounds, compression and refutation.
PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. Give the
computational–statistical gap program concrete clients: an SQ oracle with tolerance and query
costs, statistical-dimension lower bounds for a specified planted problem, and corresponding
sample and runtime upper bounds. Develop low-degree likelihood-ratio and sum-of-squares
comparisons where justified, distinguishing restricted-model bounds from unrestricted
computational hardness. Use the [distributional framework](#average-case-complexity).
- **Property and distribution testing:** access models, one/two-sided and tolerant testing,
query and sample bounds, canonical testers and lower bounds.
- **Kolmogorov complexity and metacomplexity** ([#798], [#884]): the near-linear threshold regime
Expand All @@ -409,13 +458,102 @@ each statement against the numbered result. Organize modules by subject, not cha
circuit, channel and measurement semantics with uniformity and approximation costs, reusing
suitable quantum foundations rather than incompatible models; BQP, QMA and related query,
communication and interactive classes, with amplification, containments and complete
problems.
problems. Supply the [quantum adversary models](#concurrent-and-quantum-security) needed by
cryptographic reductions.

### Differential privacy and adaptive data analysis

- Dataset adjacency and `(ε, δ)`-differential privacy for probabilistic programs, with
postprocessing and adaptive composition. Start with a finite or discrete mechanism proving
both privacy and utility, including sampling cost and finite-precision error.
- The exponential mechanism, private query answering and private learning; privacy–accuracy
and sample-complexity lower bounds; then adaptive data-analysis and generalization guarantees.
Keep the adjacency relation, interaction model, privacy parameters and computational resources
explicit, reusing the probability, oracle-computation and learning APIs.

[#1459]: https://github.com/cslib-community/complexitylib/issues/1459
[#1463]: https://github.com/cslib-community/complexitylib/issues/1463
[#1481]: https://github.com/cslib-community/complexitylib/issues/1481
[#1482]: https://github.com/cslib-community/complexitylib/issues/1482

## Algorithms and optimization

### Optimization and duality

- **Linear programming:** rational input and output encodings, primal and dual certificates,
weak and strong duality, and infeasible or unbounded outcomes. Reuse Mathlib's convexity and
linear-algebra foundations; certify certificate checking and a polynomial-time LP algorithm
with bit complexity and intermediate precision accounted for.
- **Separation and optimization:** a precise oracle interface and a separation–optimization
equivalence with its representation, accuracy and well-boundedness hypotheses. Extend to
convex optimization through explicit oracle and numerical-error contracts.
- **Primal–dual approximation and multiplicative weights:** reusable analyses with vertex cover
and set cover as first primal–dual clients; multiplicative-weights regret and approximation
bounds with finite-precision implementations, then applications to games, learning and
optimization.

### Combinatorial optimization

Coordinate native graph-algorithm work with [CSLib's graph-algorithm directions](https://github.com/leanprover/cslib/blob/main/CONTRIBUTING.md#graph-algorithms-and-graph-foundations),
reusing graph and matroid foundations and the shared data-structure interfaces.

- **Flows and matching:** integral max-flow/min-cut and a native augmenting-path algorithm with
charged runtime; then minimum-cost flow and weighted bipartite matching through common
residual-network and duality machinery.
- **Spanning trees and matroids:** minimum spanning trees with sorting and disjoint-set costs;
weighted matroid greedy optimality with an independence-oracle interface; then matroid
intersection with explicit oracle and implementation costs.
- **Submodular optimization:** the `1 - 1/e` approximation for nonnegative monotone submodular
maximization under a cardinality constraint, charging value-oracle calls separately from their
concrete realizations; then further constraints and approximation bounds.

### Online algorithms and competitive analysis

- Request sequences, online strategies, offline optima and competitive ratios with additive
constants; distinguish deterministic and randomized strategies and oblivious and adaptive
adversaries. Compare algorithms in the same action and cost model, including initialization.
- **Paging:** an LRU competitive bound and a matching deterministic lower bound as the first
clients. Reuse native amortized certificates and make adversarial request generation explicit.
- **Adaptive search trees:** a BST access-and-rotation model, the splay access lemma, static
optimality, working-set and dynamic-finger bounds, and Wilber-style lower bounds. State dynamic
optimality as a conjectural research target with explicit strategy and sequence quantifiers.

### Structural graph algorithms

- Tree decompositions, width and normalization into a suitable decomposition form; a reusable
dynamic-programming evaluator over a supplied decomposition, with state-space, transition,
join and runtime bounds. Start with native independent-set, coloring and SAT/CSP decision and
counting clients, specifying the graph whose width is measured.
- **Algorithmic metatheorems:** MSO-to-automata/evaluator compilation and a Courcelle-style
theorem with computable parameter dependence on width and formula size. Keep the supplied
decomposition and its encoding explicit; certify decomposition finding separately. Connect
the evaluator to descriptive complexity, parameterized reductions and constraint networks.

### Sampling and approximate counting

- **Markov-chain sampling:** finite kernels, stationarity, reversibility and total-variation
mixing; coupling, path coupling, conductance and canonical-path arguments. Implement
Metropolis sampling for encoded rational target weights, charging initialization, arithmetic
and every transition, with support and mixing hypotheses explicit.
- **FPRAS and almost-uniform sampling:** interfaces separating relative error, failure
probability, output-distribution error and runtime, including zero-count instances. Start
with a complete DNF-counting FPRAS; prove sampling/counting reductions for suitably
self-reducible relations, with the sampling and counting oracle costs included.
- Extend to randomized approximate counting for matchings and permanents of nonnegative
rational matrices through explicit mixing and reduction theorems. Reuse the coupling and
expander APIs and connect to the separate Stockmeyer oracle-counting track where their
hypotheses agree.

### Constructive probabilistic methods

- **Moser–Tardos resampling:** an actual resampling program, its correctness and expected
resampling bound, and native sampling and event-detection costs, building on the variable
form of the Local Lemma.
- **Conditional expectations and pessimistic estimators:** certified choice and update rules,
algorithmic alteration, and concrete coloring, satisfiability or combinatorial-construction
clients. Preserve the quantitative guarantee when converting an existence argument into a
deterministic or randomized algorithm.

## Machines, RAM and data structures

- **Native distinct-position frontend** ([#1482]): initialized signed input produces exact
Expand Down Expand Up @@ -593,6 +731,19 @@ each statement against the numbered result. Organize modules by subject, not cha
and a `690n²Dg` charged bound in the source's admissible parameter regime. Prime selection,
solving the prepared instances, product/backend composition and the full #1394 endpoint remain.

### Parallel, external-memory and distributed models

- **Parallel algorithms:** work–span semantics and a processor-scheduling or simulation theorem,
followed by prefix scan, sorting and graph primitives with both work and span bounds. State
processor access, synchronization and scheduling overhead explicitly.
- **Memory hierarchies:** external-memory and ideal-cache models with explicit capacity and
block-size parameters; scanning, B-tree operations, blocked matrix multiplication and
cache-oblivious sorting as clients. Connect arithmetic-step, memory-access and cache-miss
bounds through concrete realizations, including replacement and initialization conventions.
- **Distributed complexity:** LOCAL and CONGEST models with explicit identifiers, round,
message-size and randomness conventions; locality lower bounds and communication-to-round
reductions with corresponding algorithmic examples.

## Coverage and reuse

The long-term bar is to support formalizing every paper in the
Expand Down
Loading