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

Previous Next

Package: guix;

Reported by: Jack Hill <jackhill <at> jackhill.us>

Date: Thu, 3 Feb 2022 04:32:02 UTC

Severity: normal

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

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

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to bug-guix <at> gnu.org:
bug#53742; Package guix. (Thu, 03 Feb 2022 04:32:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to Jack Hill <jackhill <at> jackhill.us>:
New bug report received and forwarded. Copy sent to bug-guix <at> gnu.org. (Thu, 03 Feb 2022 04:32:02 GMT) Full text and rfc822 format available.

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




Information forwarded to bug-guix <at> gnu.org:
bug#53742; Package guix. (Thu, 03 Feb 2022 07:32:01 GMT) Full text and rfc822 format available.

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)]

Information forwarded to bug-guix <at> gnu.org:
bug#53742; Package guix. (Thu, 03 Feb 2022 07:32:02 GMT) Full text and rfc822 format available.

This bug report was last modified 2 years and 54 days ago.

Previous Next


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