A Rocq formalization of information theory and linear error correcting codes

Infotheo is a Rocq library for reasoning about discrete probabilities, information theory, and linear error-correcting codes.

Meta

• Author(s):
  • Reynald Affeldt, AIST (initial)
  • Manabu Hagiwara, Chiba U. (previously AIST) (initial)
  • Jonas Senizergues, ENS Cachan (internship at AIST) (initial)
  • Jacques Garrigue, Nagoya U.
  • Kazuhiko Sakaguchi, Tsukuba U.
  • Taku Asai, Nagoya U. (M2)
  • Takafumi Saikawa, Nagoya U.
  • Naruomi Obata, Titech (M2)
  • Alessandro Bruni, IT-University of Copenhagen
• License: LGPL-2.1-or-later
• Additional dependencies:
  • MathComp ssreflect
  • MathComp fingroup
  • MathComp algebra
  • MathComp solvable
  • MathComp field
  • MathComp analysis
  • MathComp analysis reals standard library
  • Hierarchy Builder
  • Hierarchy Builder
  • MathComp algebra tactics
  • CoqInterval
• Rocq/Coq namespace: infotheo
• Related publication(s):
  • An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols doi:10.1007/978-3-031-95497-9_11
  • Robust Mean Estimation by All Means (short paper) doi:10.4230/LIPIcs.ITP.2024.39
  • Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation doi:10.1145/3479394.3479412
  • Formal Adventures in Convex and Conical Spaces doi:10.1007/978-3-030-53518-6_2
  • A Library for Formalization of Linear Error-Correcting Codes doi:10.1007/s10817-019-09538-8
  • Reasoning with Conditional Probabilities and Joint Distributions in Coq doi:10.11309/jssst.37.3_79
  • Examples of formal proofs about data compression doi:10.23919/ISITA.2018.8664276
  • Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes
  • Formalization of error-correcting codes---from Hamming to modern coding theory doi:10.1007/978-3-319-22102-1_2
  • Formalization of Shannon’s Theorems doi:10.1007/s10817-013-9298-1

Building and installation instructions

The easiest way to install the latest released version of A Rocq formalization of information theory and linear error correcting codes is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-infotheo

To instead build and install manually, do (using GNU make):

git clone https://github.com/affeldt-aist/infotheo.git
cd infotheo
make   # or make -j <number-of-cores-on-your-machine>
make -C extraction tests
make install

Acknowledgments

Many thanks to several contributors.

The principle of inclusion-exclusion is a contribution by Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory) (main theorem: Pr_bigcup_incl_excl; commit 956096859ed89325b2bb74033690ac882bbcd64e)

The variable-length source coding theorems are a contribution by Ryosuke Obi (Chiba U.) (commit a67da5e24eaaabb345d225a5bd0f5e86d35413a8) (with Manabu Hagiwara and Mitsuharu Yamamoto)

Commit 64814f529c1819684c4b8060d0779c24c6339041 was originally by Karl Palmskog.

The formalization of modern coding theory is a collaboration with Y. Takahashi collaborated to the formalization of linear error-correcting codes.

This work was partially supported by a JSPS Grant-in-Aid for Scientific Research (Project Number: 25289118), a JSPS Grand-in-Aid for Scientific Research (Project Number: 18H03204).

Each file is documented in its header. Changes are (lightly) documented in changelog.txt.

Installation with Windows 10 & 11

Installation of infotheo on Windows is less simple. See this page for instructions to install MathComp on Windows 10 & 11 (or this page for instructions in Japanese). Once MathComp is installed (with opam), do opam install coq-infotheo or git clone git@github.com:affeldt-aist/infotheo.git; opam install .