Error-correcting codes

Stream: Is there code for X?

[Rado Kirov]

Looks like the theory of error-correcting codes is not in mathlib. Is anyone working on that? If I work on formalizing the basic definitions of linear codes and classical bounds would that be a good addition to mathlib?

I could only find one paper mentioning lean formalization - https://ieeexplore.ieee.org/document/7840479 but I can't get the full text or can't find the actual repo. There seems to be a Coq formalization - https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4335-Affeldt%20et%20al%20(2020)%20-%20A%20Library%20for%20Formalization%20of%20Linear%20Error-Correcting%20Codes.pdf

[Yaël Dillies]

@Wrenna Robson is the canonical person to ask

[Wrenna Robson]

There is a good deal of work happening in https://github.com/Verified-zkEVM/ArkLib along these lines, I believe. I've not been involved myself (yet!) but I'm aware of the work. There's also some groundwork that I laid down a few years ago but nothing more than that.

[Wrenna Robson]

@Bolton Bailey is a good person to ask too

[Wrenna Robson]

I found the main annoyance was deciding how much generality one wants to do things in. Do you want to focus on linear ECCs? ECCs in general?

[Wrenna Robson]

But I think ArkLib have broadly done a good job with this! I don't know if they have plans to move their work into MathLib but it would clearly be desirable (and I'm keen to help out with that when I can).

[Rado Kirov]

Oh neat, https://github.com/Verified-zkEVM/ArkLib/blob/main/ArkLib/Data/CodingTheory/Basic.lean has a lot of what I was looking for. Linear block ECCs is what I want to focus on.

[Wrenna Robson]

Grand

[Wrenna Robson]

As I think they say there they don't use infsep/einfsep (which I developed for this purpose) and I think if the work went into MathLib that would be desirable. But the groundwork is very much there.

[Wrenna Robson]

One thing that would be good in Mathlib that has a somewhat wider application than coding theory is the theory of integer-valued metrics.

[Wrenna Robson]

Which do come up quite a bit in some bits if computer science in natural ways. They aren't topologically interesting particularly but they are metrically interesting.

[Rado Kirov]

Adding https://en.wikipedia.org/wiki/Enumerator_polynomial#MacWilliams_identity would be the next on my list judging by what is there in Arclib.

[Rado Kirov]

theory of integer-valued metrics.

I am not familiar with that.

[Rado Kirov]

does the Arclib project have a separate zulip?

[Wrenna Robson]

Oh well it's no more interesting than to say "some metrics take values in the integers, the Hamming distance being the archetypal example". In this case, as they show there, you have this nice thing that the general noncomputable definition of the minimum distance can be written in terms of a computable function into the (extended) naturals which embeds into R

[Wrenna Robson]

But some arguments that come up naturally in coding theory do rely on this embedding - like, if you know two distances happen to have a difference of less than 1, they must be equal, that kind of thing.

[Wrenna Robson]

The general theory of this would be about sphere packing and packing distances and the like. I don't think we have a description of that either.

[Rado Kirov]

oh neat, I haven't seen a general framework to share between ECC (which are discrete packing problems of sorts) and continuous ones, but what you are saying makes sense. Is there an informal text for this?

[Wrenna Robson]

I'm not aware of a canonical one! I'm sure there is though.

[Wrenna Robson]

My interest was specifically in if I could make some progress in formalising Classic McEliece (which honestly I didn't get very far in - starting very general like this has pitfalls). I'm not really a coding theorist myself, just a dabbler. But it's definitely an area of interest to me.

[Wrenna Robson]

The border between continuous and discrete problems is IMO where cryptography often lies...

[Chris Henson]

If there's a question of the right place to upstream any of this line work, please also consider CSLib!

[Wrenna Robson]

Yes! Honestly that may be the better place for it though I'm still not sure what the boundary is.

[Wrenna Robson]

Another advantage of having a general theory of integer valued metrics would be that in some more niche places one wants to do coding theory but not using the Hamming code.

[Wrenna Robson]

I know there's cryptographic application for that.

[Alexander Hicks]

Hello! Just chiming in on behalf of ArkLib, I'm currently travelling so will keep it brief for now.

does the Arclib project have a separate zulip?

We currently have a private channel on this zulip. Happy to add you if you like!

don't know if they have plans to move their work into MathLib but it would clearly be desirable (and I'm keen to help out with that when I can).

If there's a question of the right place to upstream any of this line work, please also consider CSLib!

We would like to upstream this into mathlib (or cslib) as this could make it more easily accessible to others and also make maintenance easier but it's currently not a priority given that (i) it's not ready to be upstreamed (many sorrys remaining, some things may be stated less generally than desired for mathlib, ...), (ii) even when ready I imagine doing so will take up a decent amount of time.

I would also note that whilst ArkLib is focused on SNARKs, PRs related to coding theory beyond what we currently cover (and plan to cover) would broadly be welcome.

[Rado Kirov]

We currently have a private channel on this zulip. Happy to add you if you like!

Sounds good, though I should probably learn what SNARKs means :)

[Bolton Bailey]

Rado Kirov said:

We currently have a private channel on this zulip. Happy to add you if you like!

Sounds good, though I should probably learn what SNARKs means :)

I'm sure there are many places on the internet where you could read about them, but I answered a few questions about them in this thread, and I am always happy to answer more!