rust-fiat-crypto missing source

  • Open
  • quality assurance status badge
Details
2 participants
  • Dr. Arne Babenhauserheide
  • Jack Hill
Owner
unassigned
Submitted by
Jack Hill
Severity
normal
J
J
Jack Hill wrote on 3 Feb 2022 05:31
(address . bug-guix@gnu.org)
alpine.DEB.2.21.2202022323571.9433@marsh.hcoop.net
Hi Guix,

It looks like our rust-fiat-crypto package is not built from source, but
from autogenerated files. All the code retuned by `guix build -S
rust-fiat-crypto` contains headers like

"""
// AUTOGENERATED FILE: DO NOT EDIT
"""

or

"""
//! Autogenerated: 'src/ExtractionOCaml/word_by_word_montgomery' --lang Rust --inline secp256k1 64 '2^256 - 2^32 - 977' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp
//! curve description: secp256k1
//! machine_wordsize = 64 (from "64")
//! requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp
//! m = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f (from "2^256 - 2^32 - 977")
//!
//! NOTE: In addition to the bounds specified above each function, all
//! functions synthesized for this Montgomery arithmetic require the
//! input to be strictly less than the prime modulus (m), and also
//! require the input to be in the unique saturated representation.
//! All functions also ensure that these two properties are true of
//! return values.
//!
//! Computed values:
//! eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192)
//! bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248)
//! twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) in
//! if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256
"""

These files are autogenerated from the Coq source. I think that we should
build from that source as part of our package definition.

What do you think?
Jack
D
D
Dr. Arne Babenhauserheide wrote on 3 Feb 2022 08:30
(name . Jack Hill)(address . jackhill@jackhill.us)
87k0ec2ypf.fsf@web.de
Jack Hill <jackhill@jackhill.us> writes:
Toggle quote (5 lines)
> These files are autogenerated from the Coq source. I think that we
> should build from that source as part of our package definition.
>
> What do you think?

I think that sounds sensible. Can you try whether it works?

Best wishes,
Arne
--
Unpolitisch sein
heißt politisch sein,
ohne es zu merken.
draketo.de
-----BEGIN PGP SIGNATURE-----

iQJEBAEBCAAuFiEE801qEjXQSQPNItXAE++NRSQDw+sFAmH7hM0QHGFybmVfYmFi
QHdlYi5kZQAKCRAT741FJAPD61D8D/9NF01T3Ftuz+c9BihKWpKdTyAFpWreNKUl
bak3vlcFTC+XiPLqGoGlaLMMu+enzxHqmjhfqTLFEcfhXWcx6icvHojU7ge5NIjs
9Vr+gtkFn2/NeViMj/n+Wk7e+84bc8+RM7c/sz4Q920TrQK8SAOAoxgNF/MINsQn
16lRJknIkW4+M0nx70eVQsaXPoynvkIjSwz4FLi0h7L0WrT0maKfOqfc+0ySVCND
SmkVEuVeHoF47tLl6oQ/4v9kEfLH80p364gXwQOhsuB0ng0Q2KVNFcCHrCA2liXv
SPvdxxKnROh489kzVqct0Gjt8wwwR7AglHsKCYfAyEEyMcG75ahg0NkM0lP3t66o
pmTMnIy50Db6O5P1vDlH9aC9zbvh4RDDl1t/OgXsCr7O3Rdbu9uiIbkkAdoHMp52
HUjTc2YWkDQ7ScEWggOS9NXmACXa0vZm735lg9tjOoE/7uPoHDRoGo3VcmGiAU0J
qj2Xj9Syb6mjmJeHAStt/iqhRTrGPncW48TKZ4GUm31F4G566vKC2d2owHRog0hE
HuvNjeZ8HWomlwCT5Eb8JlbK38X8xBqd0VK8XxO7tWgrPX0g1ZPsHFPdCSf4DuoP
8KXTSKIPKaIHSYO/3LMv8gebUndEio7NYJR/LuWLFwqicMYIhEmW4Jfm7iLs18M4
c8YSvvF6YYjEBAEBCAAuFiEE3Si95tmHXKvOSosd3M8NswvBBUgFAmH7hM0QHGFy
bmVfYmFiQHdlYi5kZQAKCRDczw2zC8EFSPLoA/wPRbF08CMBLjXamX0U0sJ5AE35
Uhh1gFtZ4WAKEbB94HGV60R9GtfAfKxZJdg/cnVWGtsbWbRCkF+bHJWR+ZihWfhV
VxTGKbybVM6RZtryIcHQxUR9NLHoWuitOWr3GCmLrlpz1QcnOeQpZNQawr/4MsKi
YxAYL4+K/2p250ab+g==
=b75W
-----END PGP SIGNATURE-----

?