Coding theory and code-based crypography

Stream: Is there code for X?

[Wrenna Robson]

For a little while now I've been looking at the implementation of the mathematics necessary to implement the constructions of code-based cryptography (and so necessarily coding theory and specifically linear codes). I wanted to check what specific to this we already had in mathlib. As far as I can tell, not lots?

[Wrenna Robson]

(It feels like it would be substantially easier to focus on linear codes or at the least fixed-length codes rather than general coding theory.)

[Wrenna Robson]

I'm interested in getting to the point where some of the bleeding-edge innovations that exist in code-based cryptography are relatively easy to formalise.

[Johan Commelin]

As you know, there is loads of linear algebra, but besides that, I don't think we have much in the direction of coding theory.

[Wrenna Robson]

Aye, the extensive linear algebra support is what makes this even a viable proposition.

[Wrenna Robson]

I've been thinking again about this. The standard definition of a linear code of length n and dimension k is a k-dimensional subspace over n-tuples of a finite field. But I'm not quite sure of the best way to define that as a type.

[Wrenna Robson]

Specifically I'm unsure about how to bundle in the information about the dimension.

[Wrenna Robson]

You can also define it as the image of a matrix of rank k from k-tuples to n-tuples, and I guess this is also true over rings instead of a field which comes up in some applications.

[Wrenna Robson]

But that matrix isn't unique.

[Wrenna Robson]

Would appreciate some thoughts from people with experience of what kinds of definitions work well in Lean/mathlib.

[Kevin Buzzard]

If you only care about the subspace and not the basis then why not just encode it as a pair consisting of a term of type submodule F (fin n -> F) and a proof that the term has dimension k? Are you sure you want k to be part of the data?

[Wrenna Robson]

Well that's actually exactly what I had (though I mean, I guess that implicitly has k as a parameter?)

[Wrenna Robson]

But there's a number of ways I can think of having "proof that the dimension is k" some of which seem easier to work with than others

[Wrenna Robson]

Like do I want to state it in terms of finrank? Or doi want to say the there exists some non-singular linear map from ^k to ^n of which it is the image?

[Kevin Buzzard]

Because I'm not clear on your applications I don't know if you want code F or code F n or code F n k. If you have C : code F then you can have C.length : nat and C.dimension : nat. If you have C : code F n k then different things become easier/harder. Mathematically it's "all the same", so perhaps the definition should be informed by what you want to do with these things. For example would it be convenient if two codes with different dimensions have the same type, for some reason, or does this buy you nothing? It all depends on what you're doing I guess.

[Wrenna Robson]

Essentially "coding theory", specifically linear error-correcting codes.

[Kevin Buzzard]

So what are the key definitions and theorems which you envisage formalising? Perhaps that informs the answer.

[Wrenna Robson]

Conceptually two codes with different dimensions should probably be of different type

[Wrenna Robson]

Yeah so this is a good question - in general "all of coding theory" is too much for one person but I'd like to get to the point when I can state and prove standard results about Goppa codes, for instance.

[Wrenna Robson]

There's a number of constructions you can do to combine codes which might be illustratative

[Kevin Buzzard]

The alg geom Goppa codes which use curves over finite fields, or the easier ones?

[Wrenna Robson]

4247d89a-3cdb-4f6a-b331-7f6c6c0d42de.jpg

[Wrenna Robson]

The easier ones aye though I don't purely want to develop a theory of binary codes

[Wrenna Robson]

d1a90021-d238-44f8-8a57-96c86ae9b49a.jpg

[Wrenna Robson]

This is the book I'm referring to: https://link.springer.com/book/10.1007/3-540-31703-1

[Kevin Buzzard]

That construction of a "diagonal concatenation" has notation (C_0, C_1) but depends essentially on a choice of basis for the codes in question.

[Wrenna Robson]

Yes. I think the claim implicitly is that the choice of basis doesn't matter, it generates the same code?

[Kevin Buzzard]

I think that's easily seen to be false?

[Wrenna Robson]

Possibly the same code up to linear isometry - sometimes people can be slightly vague about this.

[Wrenna Robson]

Sometimes a code isn't dependent on a choice of basis, sometimes it's defined with its generator matrix, sometimes it's defined as the kernel of a parity check matrix

[Kevin Buzzard]

I'm not an expert, but my reading of your screenshot is "choose a basis (b1,...,bk) and (c1,...,ck) for your two codes, and then the space spanned by basis (b1,c1),...,(bk,ck) is the diagonal concatenation", and this will clearly change if you change your basis.

[Kevin Buzzard]

Possibly the same code up to linear isometry

OK so now you have introduced what look like three distinct concepts to me: (1) a subspace of F^n of dimension k (2) a subspace of F^n of dimension k equipped with a basis (3) a subspace of F^n of dimension k except that two subspaces are thought of as equal if they are equivalent in the sense of some kind of linear isometry. Only one of these can be a code I guess. Do you want a based_code as well?

[Wrenna Robson]

Hmm - I thought about this but probably not? You want to be able to form propositions like "this matrix G is a generator for code C" though

[Wrenna Robson]

There's a notion of a code having a systematic form - "every code C is linearly isometric to a code C' such that C' has a generator matrix of the form (Identity_n-k | A), for A a k by k matrix".

[Kevin Buzzard]

A generator matrix is just another way of thinking about a basis; you can't make that diagonal concatenation construction without having one though. So why not let code n k be a k-dimensional subspace of fin n -> F, and then mimic the basis API in mathlib to do generator matrices?

[Wrenna Robson]

Generator matrices are probably better thought of as linear maps because we also care about their kernels.

[Kevin Buzzard]

Wrenna Robson said:

There's a notion of a code having a systematic form - "every code C is linearly isometric to a code C' such that C' has a generator matrix of the form (Identity_n-k | A), for A a k by k matrix".

Right -- that's just code language for some statement in linear algebra which we'll have already (basis of a subspace extends to basis of the whole space).

[Wrenna Robson]

Because there's a concept of the dual code (which is just the orthogonal space), and every generator matrix for C is a parity check matrix for its dual.

[Kevin Buzzard]

Let me again stress that I'm no expert but we have vector spaces and we have bases, and it sounds to me like you can mimic what this looks like to make codes and based codes (or a basis for a code or a generator matrix for a code or whatever you want to call it).

[Wrenna Robson]

Yes I think so - really it's just linear algebra! - but there's a number of specific theorems which are either existing results with different names or more exotic things that only work in this specific context.

[Wrenna Robson]

How would you define "k-dimensional subspace"?

[Kevin Buzzard]

Remark; if I've understood the material correctly, then the dual code will change when you make a linear isometry.

[Wrenna Robson]

possibly. A linear isometry between two codes C C' here btw is defined as a linear isometry on fin n -> k which maps C into C' (so it preserves all distances).

[Wrenna Robson]

This is all under the Hamming metric usually although in some contexts more abstract metrics are involved - I'm ignoring that though.

[Kevin Buzzard]

aah then I withdraw my claim :-)

[Wrenna Robson]

yes - in a sense I think that's part of why the definition is like that...

[Kevin Buzzard]

I am a fool -- of course "isometry" will preserve distances. I would just make some random design decision and then get going. Start with code n k being a structure with two fields, the submodule and the proof it's got dimension k, and then try making examples and proving lemmas about them; you'll soon find out whether you've made the right decision.

[Kevin Buzzard]

I think that this might reflect my formalisation technique, and I'm well aware that there are others that do things very differently. For example I had no idea about the "best" way to formalise schemes, but rather than spend any time trying to figure it out I just tried a random way with a couple of undergrads and we learnt from my mistakes. It took three goes to get it right. The same is happening with group cohomology right now, with a debate still running (search for recent posts by Amelia Livingston) about what the correct definition is, but I already supervised not one but two projects (one bachelors, one masters) both of which claimed to define group cohomology! I firmly believe in a "try something and see" approach.

[Wrenna Robson]

Yeah I just - I did do this, I did start, I ran into some issues so I'm asking! As I say it's "proof that it has dimension k" that I'm really asking about.

[Wrenna Robson]

I don't know the best (= best supported by the API) approach to that. Whenever I deal with finrank it seems oddly hard to work with.

[Wrenna Robson]

I've been playing around defining and proving stuff in this area for a little while but every time I try and just make this basic definitions I seem to run aground into things. I suspect it would be easier with someone who also worked in this stuff to bounce ideas off but I don't have that luxury.

[Wrenna Robson]

if "finrank F C = k" is the "right" choice I can work with that but my experience is definitely that there's a lot of pitfalls one can make, and I can think of several other definitions that might also work fine

[Kevin Buzzard]

I think it's definitely morally the right choice, because you know a priori that the subspace is finite-dimensional. However there's a world of difference between that assertion and "I have all the API I need" :-) If you're missing API then you could try and farm it out, or just sorry it.

[Wrenna Robson]

Morally the right choice is good enough for me!

[Peter Nelson]

Fwiw, there is a close connection to matroid theory here (codes are ‘represented matroids’, where the represented matroid is the one whose independent sets are the lin. Ind. sets of columns in the parity check matrix) and the matroid probably wants to have the dimension after the colon.

But it’s you doing the work, not me!

[Wrenna Robson]

@Peter Nelson can you say more about this?

[Wrenna Robson]

(I don't know anything about metroids.)

[Wrenna Robson]

FWIW there is some debate whether or not a particular representation should be attached to a code or not, or whether it should be "matrix-agnostic".

[Stuart Presnell]

@Alena Gusakov gave a talk on formalising matroid theory in the London Learning Lean seminar series.

[Peter Nelson]

I certainly like the matrix-agnostic approach.

A matroid is an abstract system of ‘independent sets’ in a type, and when linearly represented, matroids are essentially linear codes. See Alena’s talk or mine on the same topic from Lean Together last year (on mobile - don’t have the link handy).

My view on the colon makes sense even for codes though - because of the finite dimensionality, there is a canonical correspondence between a code and the dual of its dual. It is easy to set this correspondence up as equality if a code is a ‘subspace of F^(fin n), but if it is a ‘k-dimensional subspace of F^(fin n)’ then the dual code is an ‘n-(n-k)-dimensional subspace of F^(fin n)’, which is not equal because n-(n-k) is not defeq to k. This an an annoyance, but maybe there are advantages that make it worth it.

[Stuart Presnell]

@Peter Nelson: Formalising matroids at Lean Together 2021
https://www.youtube.com/watch?v=FzJuoXy5cG0

[Wrenna Robson]

Peter Nelson said:

I certainly like the matrix-agnostic approach.

A matroid is an abstract system of ‘independent sets’ in a type, and when linearly represented, matroids are essentially linear codes. See Alena’s talk or mine on the same topic from Lean Together last year (on mobile - don’t have the link handy).

My view on the colon makes sense even for codes though - because of the finite dimensionality, there is a canonical correspondence between a code and the dual of its dual. It is easy to set this correspondence up as equality if a code is a ‘subspace of F^(fin n), but if it is a ‘k-dimensional subspace of F^(fin n)’ then the dual code is an ‘n-(n-k)-dimensional subspace of F^(fin n)’, which is not equal because n-(n-k) is not defeq to k. This an an annoyance, but maybe there are advantages that make it worth it.

Interesting. I wasn't sure how essential the finite-dimensionality truly was to the essential definitions (the trick is finding the right level of generality).

What did you mean by "my view on the colon"?

[Peter Nelson]

I meant that I much prefer linear_code (n : nat) := (...), where the dimension d is either a field of the definition or a function of the code defined externally, to linear_code (n d : nat) where the dimension d is tied up before the colon. This is because a linear_code 6 2 isn't propeq to the dual dual code, a linear_code 6 (6-(6-2)), where they really are 'the same' mathematically. (Obviously we make sacrifices like that all the time with things like order duality, but here it might not be necessary at all)

[Wrenna Robson]

I like this. The reason I wasn't necessarily going to do it is that a) I thought it might make associating it with a generator/parity-check matrix harder (but I take your point re: types), b) there are operations on codes which seem to only work for codes of the same dimension.

[Wrenna Robson]

One option would be to have two (three?) different types: linear_code n, which is the type of linear codes of length n, and linear_code_generated by n k, which has a field G (where G is an k by n matrix) and a proof that G has full rank, or whatever and we understand that to mean the linear code generated by a given generator matrix (and I suppose you could have a similar thing for parity matrices).

[Wrenna Robson]

This corresponds to the notion that you can define a linear code abstractly as a subspace, or concretely as the image of a generating matrix or as the kernel of a parity matrix.

[Wrenna Robson]

By the way, do you think the Hamming metric should be pre-associated to the overall space? Does it only make sense to talk about codes with respect to a specific metric?

[Peter Nelson]

Yeah, I don’t know much about the operations that care about the dimension - maybe that’s where the tradeoffs lie.

It seems natural to me to have the generator matrix -> code construction be a function, rather than having the matrix as a field, since that way, you can meaningfully state that code_generated_by A = code_generated_by B for distinct matrices A and B, rather than having that statement fail to typecheck.

Does the matrix need to have full row rank? I know it’s conventional, but taking the row space of an arbitrary matrix as the code it generates works fine enough. If you want to talk about full-rank generators, you can always use that later.

I don’t know enough about the design goals to say anything sensible about metrics.

[Wrenna Robson]

No, maybe it doesn't need full row rank.

[Wrenna Robson]

Essentially the final design goal that I have is: I would like to be able to describe the constructions used in code-based cryptography with (relative) ease.

[Wrenna Robson]

But because I would want to use the Hamming metric at least some of the time, I might want the vector space which is "n-tuples with the Hamming metric", because it isn't going to be correct to define the Hamming metric for all n-tuples (sometimes you want other metrics!)

[Wrenna Robson]

But there are other metrics you use sometimes in a cryptography context, at the very least.