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.

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

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

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

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?

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

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

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?

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

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.

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

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

Wasn't coqeal basically a library for CCA?

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

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

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

@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?

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

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.

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)

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

Why is this PR tagged as draft?

I cannot find a todo list, is there one?

The todo is doc and headers

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

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?

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