bug#53742: rust-fiat-crypto missing source

bug#53742: rust-fiat-crypto missing source

[Jack Hill]

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

bug#53742: rust-fiat-crypto missing source

[Dr. Arne Babenhauserheide]

[-- Attachment #1: Type: text/plain, Size: 371 bytes --]


Jack Hill <jackhill@jackhill.us> writes:
> 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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 1125 bytes --]