## Stream: math-comp users

### Topic: Explicit construction of F256

#### Pierre-Yves Strub (Jan 04 2023 at 15:17):

Hi & happy new year. Any hint on how I could prove that `F_256` ~ `F_2/<'X^8 + 'X^4 + 'X^3 + 'X + 1>`? I need this explicit construction.

#### Laurent Théry (Jan 04 2023 at 16:48):

which of these steps is blocking you?

• 'X^8 + 'X^4 + 'X^3 + 'X + 1 is irreducible in F_2[X]
• F_2[X]/ 'X^8 + 'X^4 + 'X^3 + 'X + 1 is a finitie field.
• F_2[X]/ 'X^8 + 'X^4 + 'X^3 + 'X + 1 has 2 ^ 8 elements
• it is isomorphic to F_256

#### Pierre-Yves Strub (Jan 05 2023 at 13:26):

I am not even sure on what is the best path to prove the isomorphism with mathcomp.

#### Laurent Théry (Jan 07 2023 at 09:25):

Just a naive question, what you need the isomorphism for?

#### Ali Caglayan (Jan 09 2023 at 18:52):

Just curious as an outsider, but how do your prove in mathcomp that finite fields with the same cardinality are isomorphic. I.e. the last step?

#### Ali Caglayan (Jan 09 2023 at 18:53):

Also it should be "F_2[X]" right that you are taking the quotient of, or is that mathcomp notation?

#### Laurent Théry (Jan 09 2023 at 19:25):

This result is not in the library, I guess we would first need the fact that splitting fields are unique upto isomorphism..

#### Ali Caglayan (Jan 09 2023 at 19:39):

For step 2, you need to show that ring mod maximal ideal is a field. IIRC that requires AC, not a problem in MC right? Do you have something like that?

#### Ali Caglayan (Jan 09 2023 at 19:39):

And I guess the easier thing to show is that finite ring mod something is still finite.

#### Laurent Théry (Jan 09 2023 at 19:57):

I don´t think we have the general result but we have several contributions that explicitly build the quotient for polynomials and show it is a field.

#### Assia Mahboubi (Jan 10 2023 at 11:23):

Constructive commutative algebra is a bit painful, which explains in part why this corner of the library is somehow lacking...

#### Assia Mahboubi (Jan 10 2023 at 11:30):

But I hope we will find a satisfactory way out in this finitary case.

#### Alexander Gryzlov (Jan 10 2023 at 12:05):

Wasn't coqeal basically a library for CCA?

#### Ali Caglayan (Jan 10 2023 at 14:41):

Apparently in this case we can do this constructively if I have understood correctly: https://arxiv.org/pdf/2207.03873.pdf

#### Pierre-Yves Strub (Jan 10 2023 at 14:42):

So maybe it will be faster that I construct this field explicitly in a very elementary way.

#### Pierre-Yves Strub (Jan 10 2023 at 14:43):

Ali Caglayan said:

Also it should be "F_2[X]" right that you are taking the quotient of, or is that mathcomp notation?

Yes, this is a typo

#### Ali Caglayan (Jan 10 2023 at 14:50):

@Pierre-Yves Strub Were you hoping to define the field this way? Isn't it easier just to show F_256 as a ring is a field?

#### Pierre-Yves Strub (Jan 10 2023 at 14:52):

At some point, I'll have to prove that F_256 as implemented in AES is F_256.

#### Pierre-Yves Strub (Jan 10 2023 at 14:57):

The first step is to prove that AES is implementing something "isomorphic" to `F_2[X]/<'X^8 + 'X^4 + 'X^3 + 'X + 1>`. Then, at some point, I'll have to show that this forms a field of characteristic 2 with 256 elements. This is were I think I'll go with an elementary proof.

#### Cyril Cohen (Jan 10 2023 at 15:04):

As far as I understand, combining `splitting_ahom`(with `E' = fullv`) together with `finField_genPoly` gives you the result you want (a surjective algebra morphism of fields is a field isomorphism)

#### Cyril Cohen (Jan 10 2023 at 15:06):

(For the record, the result from the Abel repo is being PRed to mathcomp (math-comp/math-comp#944)

#### Assia Mahboubi (Jan 11 2023 at 10:42):

Why is this PR tagged as draft?

#### Assia Mahboubi (Jan 11 2023 at 10:43):

I cannot find a todo list, is there one?

#### Cyril Cohen (Jan 11 2023 at 11:17):

The todo is doc and headers

#### Assia Mahboubi (Jan 19 2023 at 09:43):

In fact the big todo rather seems to split this quite fat PR...

#### Assia Mahboubi (Jan 19 2023 at 09:50):

But after a closer look, my understanding of the state of affairs is the following:

• the lemmas pointed by @Cyril Cohen would be useful for to prove that finite fields with the same cardinal are isomorphic (a valuable addition)
• but there isn't really available support to help Pierre-Yves building this particular quotient and show that it is a field..
The rather rough t `ring_quotient` file does not seem very useful in this explicit case.
Am I missing something?

#### Laurent Théry (Jan 19 2023 at 17:29):

I have just commited a PR 959 that tries to put together several already existing contributions.

Last updated: Jul 25 2024 at 16:02 UTC