Stream: math-comp users

Topic: Explicit construction of F256


view this post on Zulip 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.

view this post on Zulip Laurent Théry (Jan 04 2023 at 16:48):

which of these steps is blocking you?

view this post on Zulip 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.

view this post on Zulip Laurent Théry (Jan 07 2023 at 09:25):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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..

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Assia Mahboubi (Jan 10 2023 at 11:30):

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

view this post on Zulip Alexander Gryzlov (Jan 10 2023 at 12:05):

Wasn't coqeal basically a library for CCA?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Assia Mahboubi (Jan 11 2023 at 10:42):

Why is this PR tagged as draft?

view this post on Zulip Assia Mahboubi (Jan 11 2023 at 10:43):

I cannot find a todo list, is there one?

view this post on Zulip Cyril Cohen (Jan 11 2023 at 11:17):

The todo is doc and headers

view this post on Zulip Assia Mahboubi (Jan 19 2023 at 09:43):

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

view this post on Zulip Assia Mahboubi (Jan 19 2023 at 09:50):

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

view this post on Zulip 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