rust-fiat-crypto missing source

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

Jack Hill <jackhill@jackhill.us> writes:

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