Feedback wanted on Hamming implementation

Stream: maths

[Wrenna Robson]

Quite puzzled about

type mismatch at field 'to_distrib_mul_action'
  module.to_distrib_mul_action
has type
  distrib_mul_action ?m_1 (ham ?m_3) : Type (max ? ? ?)
but is expected to have type
  distrib_mul_action α (ham β) : Type (max ? u_2 u_3)

when I try and use the module instance to define a normed space (however doomed that might be).

[Yaël Dillies]

Is the context #14739 still?

[Adam Topaz]

It could be an issue with universes. Try adding universe parameters explicitly?

[Wrenna Robson]

Yaël Dillies said:

Is the context #14739 still?

I'm not sure what else it'd be.

[Wrenna Robson]

Adam Topaz said:

It could be an issue with universes. Try adding universe parameters explicitly?

Hmm - maybe. It gets "fixed" if I make it so that the module instance is only defined coming from add_comm_group rather than add_comm_monoid - so my hypothesis is some kind of nasty non-def-eq thing somewhere.

[Wrenna Robson]

instance [Π i, add_comm_group (β i)] {α : Type*} [normed_field α]
[Π i, module α (β i)] : normed_space α (ham β) :=
{ norm_smul_le := sorry, ..@ham.module _ _ β _ _ _ }

This works.

[Wrenna Robson]

(Instead of

instance [Π i, add_comm_group (β i)] {α : Type*} [normed_field α]
[Π i, module α (β i)] : normed_space α (ham β) :=
{ norm_smul_le := sorry, ..ham.module }

[Adam Topaz]

oh no... there may be a diamond somewhere...

[Adam Topaz]

do you have a #mwe ?

[Wrenna Robson]

Unfortunately it's a bit hard to do because this really uses most things in the file.

[Wrenna Robson]

So the MWE is, well, the file in that PR

[Riccardo Brasca]

I was very busy today, I will have a look at the PR tomorrow.

[Wrenna Robson]

Sure, when you can :)

[Riccardo Brasca]

It looks like a very good start to me!

[Wrenna Robson]

Sweet! What do you think you'd like to see next in the coding theory/Hamming space?

[Wrenna Robson]

Also: I've been trying to decide how to define linear codes or more generally non-linear block codes, and whether they should have the encoding function which constructs them attached.

[Wrenna Robson]

Would be interested to see what you think?

[Wrenna Robson]

(Also: specifically would be useful to know what else you think could go in this PR so that the Hamming stuff, at least, is fully featured. It might be nice to have some way of saying "the minimum distance of a set"...?

[Bolton Bailey]

I can't speak for others, but I personally would be interested to see Reed-Solomon codes in mathlib. RS codes are used in STARK cryptography and it's something I've been working on in Coq for the company I'm working at this summer. It would be interesting to see how easy or hard they are to implement.

[Wrenna Robson]

Oh, interesting - yeah I mean my interests are also cryptographic.

[Wrenna Robson]

What've you been doing in Coq?

[Wrenna Robson]

Have you been building on the existing work in this area?

[Wrenna Robson]

I've been trying my hand at some Goppa code stuff for Classic McEliece but was finding it frustrating.

[Bolton Bailey]

I've been working for RiscZero, which has produced a zk-STARK to verify computations on the RISC-V architecture. I've been working on verifying the soundness of their system. Still in early stages of that project.

[Wrenna Robson]

Cool. This is the area I work in (at least, well, it would be if I could get anything to work, but nominally this is my PhD). I would be very interested in anything that's been publicly released.

[Wrenna Robson]

Well, at least my interest in general is formal methods in cryptography.

[Bolton Bailey]

Nothing publically released yet, since it's still under development. I'll be sure to let you know when we do come out with something though.

[Wrenna Robson]

Sweet.

[Joe Hendrix]

@Bolton Bailey @Wrenna Robson I just saw this thread and was curious if there are specifications of either of these now. I've been off-and-on working on porting the one of the Classic Mceeliece reference implementations to Lean 4, and finally got that today. The repo is here.

The plan is to eventually have reasonable efficient executable specifications of a cryptographic algorithms (that can equivalence checked with other implementations) along with proofs to related the efficient executable specifications with more general definitions in Mathlib 4.

[Bolton Bailey]

@Joe Hendrix good to hear there's another person interested in using Lean for cryptography. My own work on STARKs is not public yet, but the PR #14739 did get merged. Not sure what Wrenna's plans are for more coding theory/cryptography in mathlib, but I imagine there's quite a bit you could build out.

[Wrenna Robson]

Hi, yeah, sorry, I've been on holiday the last couple weeks

[Wrenna Robson]

I've been working on a PR to add "infsep", which you can essentially think of as minimum distance

[Wrenna Robson]

This turned out to need rather a bit of API work to do properly.

[Wrenna Robson]

https://github.com/leanprover-community/mathlib/pull/15689

[Wrenna Robson]

This will allow us to coherently talk about the minimum distance of a set in the language of mathlib.

[Wrenna Robson]

Which obviously we need for coding reasons.

[Wrenna Robson]

I'm considering the best next steps. I would like to settle on a definition of what a code is, but I was going round a bit on the right generality for that.

[Wrenna Robson]

Getting Reed-Solomon codes in would be a good next goal.

[Wrenna Robson]

I'm going to be on an internship from October for a few months so will have less time for mathlib stuff, but I will be keeping an eye on things and thinking about it in my free time.

[Wrenna Robson]

(as you can see, two months ago I was wondering on the right definition for a code - ironically the issue was that it's such a simple definition. But there's a few ways you could do it.)

[Wrenna Robson]

Oh, I'm not sure if I mentioned it above, but I also refactored the Lagrange interpolation file, in part with an eye towards RS-style constructions.

[Wrenna Robson]

@Bolton Bailey what is the definition of RS codes that is used in your context?

[Bolton Bailey]

I agree that it would probably be best to define a structure for codes and then go from there in terms of implementing RS as an instantiation of that structure. Essentially the definition that is used in the papers I work with is that an RS code is parameterized by a field, a code length and a rate, and the code is the subset of vectors of field elements of that length.

[Bolton Bailey]

Maybe we could make a short hierarchy where we define a very general code, and then quickly go on to define block codes so we can prove theorems about code distances and things like that.

[Wrenna Robson]

Right and then have linear codes as an instance of that? Maybe. Or we could just start with block codes.

[Wrenna Robson]

The thing about block codes is that on some level you don't actually care about the encoding function.

[Wrenna Robson]

Just the set of codewords.

[Wrenna Robson]

While that's really not true for general codes I think?

[Wrenna Robson]

You could define block codes of length n over an alphabet C as set (fin n -> C).

[Wrenna Robson]

Or if you want to maintain it as an encoding, you could define a block code with message length k and block length n as an injective map from fin k -> C to fin n -> C.