fiat cryptography

[spitters]

As requested at #28 opening an issue tracking:
mit-plv/fiat-crypto#925

[MSoegtropIMC]

@JasonGross : can you please comment on this request? Would you agree to the inclusion?

[JasonGross]

I think the main bottleneck is that if we include fiat-crypto, we'd also need to include coq-rewriter and coq-coqutil. Neither of these have non-dev packages. I'm willing to make such packages, but I'm not sure that coq-rewriter is sufficiently well-written to be included in the platform (especially under so general a name as "rewriter"), and coqutil at the very least might require a better description than "Coq library for tactics, basic definitions, sets, maps".

[spitters]

I haven't looked at coqutil closely enough, but how big is the overlap with stdpp. Some of the goals seem similar, at least wrt basic definitions, sets, maps.

…

On Mon, Jan 17, 2022 at 8:51 PM Jason Gross ***@***.***> wrote: I think the main bottleneck is that if we include fiat-crypto, we'd also need to include coq-rewriter and coq-coqutil. Neither of these have non-dev packages. I'm willing to make such packages, but I'm not sure that coq-rewriter is sufficiently well-written to be included in the platform (especially under so general a name as "rewriter"), and coqutil at the very least might require a better description than "Coq library for tactics, basic definitions, sets, maps". — Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android. You are receiving this because you authored the thread.Message ID: ***@***.***>

[JasonGross]

cc @samuelgruetter @andres-erbsen about coqutil vs stdpp

[andres-erbsen]

I would expect significant conceptual overlap without any drop-in compatibility between coqutil and stdpp. At the very least, both seem to overlap the coq standard library to a significant extent.

[andres-erbsen]

Another consideration for including coqutil in the coq platform is that I don't use the coq platform or opam, and I don't think @samuelgruetter does either. I see that @JasonGross has volunteered to create packages, but reading the coq platform charter gave me a sense that more active maintenance would be expected, and I don't know how to predict how our choices in coqutil would work out for coq platform users. As far as I'm concerned, you'all are welcome to include coqutil in the coq platform, and reading the list of other packages does not make me feel like there is a clear quality standard that coqutil does not meet, but please judge carefully whether including it would actually do the potential users a favor given the respective development and release models (or lack thereof).

[MSoegtropIMC]

The idea behind Coq Platform is not so much that we guarantee that everything included meets content wise the highest design quality standards. A certain technical quality is guaranteed by using Coq, of course. The things should be useful and one main consideration is that if something is included and users base their work on a package, they should be able to rely on that they don't have to factor it out with the next Coq Release. Also we expect that the API of a package is reasonably stable.

There is an "extended" content level, though, where no such guarantees are given. This is for packages where the authors want to see what resonance they get.

[JasonGross]

I think coqutil and rewriter are fine for the extended content level (fiat-crypto also makes no strong guaranties about its API, or alternatively we consider the fully stable API to be the generated binaries, and I've been at least making an effort to identify changes in more intermediate APIs in releases lately).

Is there a way to tag opam packages as more-or-less experimental / unguaranteed?

[Zimmi48]

given the respective development and release models (or lack thereof)

The main issue for including coqutil (even in the extended level) would be if there is no one committing to make timely releases when new Coq versions are released.

[silene]

The main issue for including coqutil (even in the extended level) would be if there is no one committing to make timely releases when new Coq versions are released.

Can't we take for granted that whoever is volunteering to maintain fiat-crypto is also volunteering to maintain its closely related (almost internal) dependencies such as coqutil? Or am I misunderstanding your remark? (Perhaps you were considering the situation where coqutil would be integrated but not fiat-crypto?)

[Zimmi48]

That does make sense to me. As long as the person that volunteers confirms that this would work.

[MSoegtropIMC]

@JasonGross , @andres-erbsen, @spitters : so how shall we proceed?

If you say that the API of fiat-crypto is not very stable I am not sure if it is useful as a base for other peoples work. Even the packages in "extended" are intended to be useful as base for derived work. Would you consider fiat-crypto as "leaf" in a project derivation tree?

I could btw. not find an opam package for it, so it is hard for me to judge if other work already depends on it.

[JasonGross]

I could btw. not find an opam package for it, so it is hard for me to judge if other work already depends on it.

https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-fiat-crypto/coq-fiat-crypto.dev/opam

That does make sense to me. As long as the person that volunteers confirms that this would work.

I'm happy to make nominal releases of coqutil and rewriter.

If you say that the API of fiat-crypto is not very stable I am not sure if it is useful as a base for other peoples work. Even the packages in "extended" are intended to be useful as base for derived work. Would you consider fiat-crypto as "leaf" in a project derivation tree?

I think this is a question for @spitters , though there's the additional issue that I think the newest work building on fiat-crypto is about the bedrock2/rupicola part, which is currently not even in the dev package because bedrock2 moves too quickly and rupicola too slowly to have good opam packages. I've been trying to make some progress on this at coq/opam#2115, but am lacking debugging time.

[JasonGross]

so how shall we proceed?

I can make non-dev packages of fiat-crypto, coqutil, and the rewriter, though it might take me a couple days. (Someone else should also feel free to make the packages ... should I make releases of each of the projects first?)

[MSoegtropIMC]

@spitters : can you say a few words on the intended usage of fiat-crypto for derived work - essentially your vision about it? From the description of @JasonGross I am not sure if it would be the right move to include fiat-crypto in Coq Platform now.

@JasonGross : how do you see the outlook? Is it so that the APIs of fiat-crypto will stabilize in say a year, or is using fiat-cyrpto more like landing a helicopter on a sheet of paper flying in the air for the next few years?

should I make releases of each of the projects first?

Assuming we decide it is a good idea to include fiat-crypto, yes - Coq Platform has a strict "releases only" policy - we do some minor patching from time to time, but a tag is a must have.

I would also prefer if you would review the meta information in the dev opam package (description ...) and do the first release of the opam packages.

[Zimmi48]

@spitters will get the chance to answer in more detail, but his team is already relying on fiat-crypto for derived work. See an example paper here: https://eprint.iacr.org/2021/549.pdf

[spitters]

We're using fiat with my PhD-students in https://github.com/AU-COBRA/AUCurves, which also depends on bedrock2.

[JasonGross]

The non-bedrock2 API of Fiat Crypto is essentially stable, mostly due to lack of developer time to work on it. The bedrock2/rupicola part is still under more-or-less active development.

I guess if the non-dev packages are tagged, I can just tag a release at the relevant compatible commit each time Coq is released, and so the non-dev / platform version could include rupicola and bedrock2 and all the bells and whistles.

[JasonGross]

I've created tags for all the dependencies, I'll try to create opam packages soon

[JasonGross]

I've created #178

[MSoegtropIMC]

I guess you mean coq/opam#2137.

[MSoegtropIMC]

@andres-erbsen : so one should use $(MAKE) -f Makefile.coq install (wihtout the noex)?

[JasonGross]

I think you need to do $(MAKE) -f bedrock2/Makefile.coq.noex install && $(MAKE) -f bedrock2/Makefile.coq.ex install`. But if mit-plv/bedrock2#281 is merged we can just tag a new release and use that.

[MSoegtropIMC]

Btw.: I need a smoke test file for each of these packages:

coq-rewriter.0.0.6"
coq-riscv.0.0.2"
coq-bedrock2.0.0.2"
coq-bedrock2-compiler.0.0.2"
coq-rupicola.0.0.5"
coq-fiat-crypto.0.0.15

[MSoegtropIMC]

@JasonGross : a new tag would be nice - I can take your change as local patch until it is there.

[JasonGross]

Btw.: I need a smoke test file for each of these packages:

coq-rewriter.0.0.6"
coq-riscv.0.0.2"
coq-bedrock2.0.0.2"
coq-bedrock2-compiler.0.0.2"
coq-rupicola.0.0.5"
coq-fiat-crypto.0.0.15

@MSoegtropIMC What do you mean by smoke test file? Is what I said at #178 (comment) not sufficient for rewriter and fiat-crypto?

Not sure for coqutil, bedrock2, rupicola (maybe @andres-erbsen or @samuelgruetter will have an idea), but for rewriter:

Require Import Rewriter.Util.plugins.RewriterBuild.
Require Import Coq.Arith.Arith.
Make rew0nat := Rewriter For (Nat.add_0_r, Nat.add_0_l).

(should take about 10s) and for fiat-crypto, let's do

Require Import Crypto.Bedrock.Everything Crypto.Everything.
Check Crypto.StandaloneOCamlMain.UnsaturatedSolinas.main.

[MSoegtropIMC]

@JasonGross : I prefer example files which exist in the projects, but I can take these lines. Also I would like to have one file for each project. But for packages in the extended level it is not a strict requirement (there are currently no exceptions, though).

[MSoegtropIMC]

Well actually there are a few exceptions already ... but still I would like to have smoke test files. The smoke test proved useful quite frequently already.

[MSoegtropIMC]

@JasonGross : an editorial note: the bedrock2 opam package says "A verified compiler targeting RISC-V from this language exists but is not yet on opam." As far as I understand this does exist in opam now.

[andres-erbsen]

Here are some fast-ish non-leaf files form the other developments:
coqutil: src/coqutil/Map/SortedListWord.v
riscv: src/riscv/Examples/MulTrapHandler.v
bedrock2: bedrock2/bedrock2Examples/ipow.v
bedrock2 compiler: compiler/src/compiler/Pipeline.v
rupicola: src/Rupicola/Examples/Uppercase.v

[JasonGross]

@andres-erbsen as per

The smoke test files should mostly test that installed .vo files are accessible under the intended log path, that plugins work and they should run as fast as possible (at most total 10s per package).

I think we're supposed to suggest short scripts that are not things that are installed. Are you suggesting just Require Import on each of those files as the smoke test? Or copy-pasting the entire file and making sure it works as intended when you compile it against the installed version? (But will it work when binding the package with -Q instead of -R?)

@MSoegtropIMC coq/opam#2341 should hopefully work. Once merged, the 0.0.15 version of fiat-crypto should automatically require the correct version of bedrock2.

[andres-erbsen]

Hmm, I thought we wanted existing files. \_o_/ For Require Import, it would be neat to test GarageDoor.v if that Requires in less than 10s.

@JasonGross : I prefer example files which exist in the projects, but I can take these lines.

[JasonGross]

Ah, I missed that, thanks!

[JasonGross]

Good smoke test files for rewriter: https://github.com/mit-plv/rewriter/blob/master/src/Rewriter/Demo.v (12s) or https://github.com/mit-plv/rewriter/blob/master/src/Rewriter/Rewriter/Examples.v (54s)
Decent smoke test files for fiat-crypto: https://github.com/mit-plv/fiat-crypto/blob/master/src/Demo.v (46s), https://github.com/mit-plv/fiat-crypto/blob/master/src/CLI.v (4s, but doesn't really test any reduction behavior)

The Requires in these files might have to be adjusted if you want them to work externally.

[MSoegtropIMC]

Thanks! I think the 46s are fine for a large project like fiat-crypto. For rewriter I will take the Demo.v. file. For the others I will test the files suggested by Andres.

I can patch the requires on copy (quite a few projects need this).

[MSoegtropIMC]

The suggested tests are all fine (and don't require patching of Require statements).

I will do tests on Linux and Windows and then merge.

Thanks a lot for the support!

[MSoegtropIMC]

There is one more issue: bedrock2 does not compile in 32 bit Windows - as far as I understand some 128 bit C stuff:

2022-10-04T23:10:23.8937576Z    194	i686-w64-mingw32-gcc.exe -fsyntax-only special/TypecheckExprToCString.c
2022-10-04T23:10:23.8938186Z    195	special/TypecheckExprToCString.c: In function ‘main’:
2022-10-04T23:10:23.8938783Z    196	special/TypecheckExprToCString.c:32:105: error: ‘__uint128_t’ undeclared (first use in this function); did you mean ‘__int128__’?
2022-10-04T23:10:23.8939429Z    197	   32 |   _Generic((uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)((uintptr_t)42ULL)*((uintptr_t)7ULL))>>32 : ((__uint128_t)((uintptr_t)42ULL)*((uintptr_t)7ULL))>>64), uintptr_t: 0);
2022-10-04T23:10:23.8939891Z    198	      |                                                                                                         ^~~~~~~~~~~
2022-10-04T23:10:23.8940233Z    199	      |                                                                                                         __int128__
2022-10-04T23:10:23.8940668Z    200	special/TypecheckExprToCString.c:32:105: note: each undeclared identifier is reported only once for each function it appears in
2022-10-04T23:10:23.8941211Z    201	make[1]: *** [Makefile:83: typecheckExprToCString] Error 1

For the time being I will solve this by excluding fiat-crypto in 32 bit Windows, but it might be worthwhile to fix it. For Coq 32 bit Windows is not completely obsolete, because it needs only about half the amount of memory which also makes it faster (better cache utilization). Since memory is an issue with Coq especially on laptops, even some researchers prefer the 32 bit Windows version.

Otherwise everything is fine except that Coq Platform CI now again touches the 6h limit on Windows. Coq Platform meanwhile has an option to exclude or individually select "large packages" and I will put fiat-crypto and its dependencies in this group. Do you have a good name for fiat-crypto and its dependencies? IMHO it is not adequate to treat bedrock2 as fiat-crypto dependency in package selection. Well, these questions are one pagers anyway, so I will include the list of packages (but make them selectable only as one set), but a better name would be nice. How about MIT-SW since as far as I understand this is the majority of the SW oriented tools of the MIT Coq group(s).

[andres-erbsen]

I created mit-plv/bedrock2@1c9f0ed which I hope will fix the 32-bit issue.

The build-times of these repositories are indeed annoying. I'm sorry about that. Is that timeout a blocker for anything?

I agree that grouping all these packages under the name of any one of them would not be fair, but I'm not sure what a better presentation would be -- riscv-coq isn't even clearly about software on its own. Perhaps the closest existing categorization is that all of these projects started in the MIT PLV ("programming languages and verification") group.

Is the information that would appear in this page somewhere in the repository so that I could pass it by other maintainers of these projects?

[JasonGross]

Please update to coq-fiat-crypto.0.0.17 once coq/opam#2353 is merged

[MSoegtropIMC]

I updated fiat-crypto to version 0.0.17 in the 2022.09.1 prep branch.

[MSoegtropIMC]

FTR: the update of fiat-crypto required these updates of dependencies:

-        PACKAGES="${PACKAGES} coq-riscv.0.0.2"
+        PACKAGES="${PACKAGES} coq-riscv.0.0.3"
-        PACKAGES="${PACKAGES} coq-bedrock2.0.0.3"
+        PACKAGES="${PACKAGES} coq-bedrock2.0.0.4"
-        PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.3"
+        PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.4"
-        PACKAGES="${PACKAGES} coq-rupicola.0.0.5"
+        PACKAGES="${PACKAGES} coq-rupicola.0.0.6"

Since this is all in the extended level I would say a more formal process is not required and I take your request to update fiat-crypto as request to update the dependencies as well.