GNU bug report logs - #53742
rust-fiat-crypto missing source

Previous Next

To reply to this bug, email your comments to 53742 AT debbugs.gnu.org.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Jack Hill <jackhill <at> jackhill.us>
To: bug-guix <at> gnu.org
Cc: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>,
 Aleksandr Vityazev <avityazev <at> posteo.org>
Subject: rust-fiat-crypto missing source
Date: Wed, 2 Feb 2022 23:31:27 -0500 (EST)

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

Message #8 received at submit <at> debbugs.gnu.org (full text, mbox):

From: "Dr. Arne Babenhauserheide" <arne_bab <at> web.de>
To: Jack Hill <jackhill <at> jackhill.us>
Cc: 53742 <at> debbugs.gnu.org, bug-guix <at> gnu.org,
 Nicolas Goaziou <mail <at> nicolasgoaziou.fr>,
 Aleksandr Vityazev <avityazev <at> posteo.org>
Subject: Re: bug#53742: rust-fiat-crypto missing source
Date: Thu, 03 Feb 2022 08:30:54 +0100

[Message part 1 (text/plain, inline)]

Jack Hill <jackhill <at> 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

[signature.asc (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.