Question about SPDX marking on some crypto files

[Derek Fawcus]

Hello,
  having just learnt of this product, I started poking through
the source;  when I got to some of the crypto code I noticed
something curious,  and did a bit more research.

  I'm curious about the SPDX licence marking on the crypto
source files which seem to be autogenerated,  specifically
these:

   src/crypto/curve25519-fiat32.h - GPL-2.0
      machine generated from https://github.com/mit-plv/fiat-crypto
   src/crypto/curve25519-hacl64.h - GPL-2.0
      mahine generated from https://github.com/mitls/hacl-star

The LICENCE file on the former site indicates that its code is
MIT licence, so it seems odd that the output from its execution
should be any more restrictive.

Whereas for the latter site, its README.md explicitly states
'All generated C code is released under MIT', so again it seems
odd to make the tag more restrictive.

So was there simply an error made when the SPDX tags were applied,
or has some additional significant manual addition occured to
justify changing the licence?

Doing any significant manual change to the output would however
seem to defeat the object in using formally verified automatically
generated implementations.

Thanks.

DF