fiat cryptography - Githubissues

spitters commented 2 years ago

As requested at https://github.com/coq/platform/issues/28 opening an issue tracking: https://github.com/mit-plv/fiat-crypto/issues/925

MSoegtropIMC commented 2 years ago

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

JasonGross commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

cc @samuelgruetter @andres-erbsen about coqutil vs stdpp

andres-erbsen commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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

MSoegtropIMC commented 2 years ago

@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 commented 2 years ago

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 https://github.com/coq/opam-coq-archive/pull/2115, but am lacking debugging time.

JasonGross commented 2 years ago

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 commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

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

JasonGross commented 2 years ago

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 commented 2 years ago

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

JasonGross commented 2 years ago

I've created https://github.com/coq/platform/issues/178

MSoegtropIMC commented 2 years ago

I guess you mean https://github.com/coq/opam-coq-archive/pull/2137.

JasonGross commented 2 years ago

There is now a non-dev version of Fiat Crypto (and its dependencies) on opam. I'll try to add longer descriptions to what the packages contain today

MSoegtropIMC commented 2 years ago

@JasonGross : thanks! I see if I can still take it into 2022.03, but I can't promise.

JasonGross commented 2 years ago

Thanks, and no worries if you can't. Let me know if you have any issues building. Note, btw, that when we test opam install on our CI, to build on Windows we have to export COQEXTRAFLAGS='-async-proofs-j 1' and pass -j 1 to opam install to not get mem-killed.

MSoegtropIMC commented 2 years ago

Sorry, I need to delay this to the next release, but I plan to do it shortly after the release in the main branch.

MSoegtropIMC commented 2 years ago

@JasonGross : did you test this on Mac?

I get this error:

/Applications/Xcode.app/Contents/Developer/usr/bin/make -f Makefile.coq.ex
sed: illegal option -- z
usage: sed script [-Ealnru] [-i extension] [file ...]
    sed [-Ealnu] [-i extension] [-e script] ... [-f script_file] ... [file ...]

MSoegtropIMC commented 2 years ago

If you don't have a Mac available, I can look into it (I have some experience with sed compatibility ...).

It has btw. been discussed to have a package conf-gsed, which provides gnu sed under name gsed on all platforms. On Linux and cygwin it would be just a symlink in the opam switch bin folder.

JasonGross commented 2 years ago

We have a Mac CI job, which we make sure passes

I don't have a Mac easily available, though, so if you can dig into it (at least to find the command that's having a problem), I'd appreciate that.

MSoegtropIMC commented 2 years ago

@JasonGross : sorry for the delay - I was moving homes ...

The culprit seems to be the sed -z at the end of (coq-bedrock2.0.0.1/etc/bytedump.sh)

I am not sure what this is supposed to do, so I can't suggest a posix/OSX compatible patch.

MSoegtropIMC commented 2 years ago

@JasonGross : can you please recommend one or two "smoke test" files for each involved package? 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).

JasonGross commented 2 years ago

The culprit seems to be the sed -z at the end of (coq-bedrock2.0.0.1/etc/bytedump.sh)

I am not sure what this is supposed to do, so I can't suggest a posix/OSX compatible patch.

       -z, --null-data

              separate lines by NUL characters

@andres-erbsen Can you comment on what sed -z '$ s/\n$//' is supposed to do, and if there's a way to do it without sed -z?

can you please recommend one or two "smoke test" files for each involved package? 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).

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 commented 2 years ago

I meanwhile figured out that the sed -z thing is supposed to remove a \n at the very end of the stream, although this is not entirely safe in case the binary dump actually does contain zeros (in that case it would also remove \n\000 sequences in the middle. One can likely solve this with posix awk (if nobody has a better idea).

MSoegtropIMC commented 1 year ago

I delayed this to 2023.3 - it doesn't seem feasible for the 2022.09 release.

andres-erbsen commented 1 year ago

Just an update: fiat-crypto and dependencies now successfully build on Windows and Mac again in our CI. Overall we replaced the binary notations with an Ltac2 printf, replaced sed with a python script that also does CRLF->LF conversion, and accommodated cygwin path handling in Makefiles.

I think this means that there are no known blockers left for coq-platform inclusion. If targeting the ongoing release seems desirable given the status and timeline, my proposed pick would be the master branch of fiat-crypto along with its pinned dependencies, which currently means just the master of each repo.

MSoegtropIMC commented 1 year ago

@andres-erbsen : very well - I am anyway delayed cause of the issues introduced by using ocamlfind in 8.16.0, so I will add it and see what happens.

Just for my understanding: fiat-crypto requires bedrock2 via rupicola, and this is not optional. The posts by @JasonGross above are a bit ambiguous in this point. Opam says, fiat-crypto required bedrock2:

opam list --recursive --required-by coq-fiat-crypto
# Packages matching: (installed | available) & rec-required-by(coq-fiat-crypto)
# Name                   # Installed       # Synopsis
base-num                 --                Num library distributed with the OCaml compiler
base-threads             base
base-unix                base
camlp5                   --                Preprocessor-pretty-printer of OCaml
conf-findutils           1                 Virtual package relying on findutils
conf-gmp                 4                 Virtual package relying on a GMP lib system installation
conf-jq                  --                Virtual package relying on jq
conf-m4                  --                Virtual package relying on m4
conf-perl                --                Virtual package relying on perl
coq                      8.16.0            pinned to version 8.16.0
coq-bedrock2             --                A work-in-progress language and compiler for verified low-level programming
coq-bignums              8.16.0            Bignums, the Coq library of arbitrary large numbers
coq-coqprime             1.2.0             Certifying prime numbers in Coq
coq-coqutil              0.0.1             Coq library for tactics, basic definitions, sets, maps
coq-fiat-crypto          --                Cryptographic Primitive Code Generation by Fiat
coq-rewriter             --                Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-t
coq-rupicola             --                Gallina to imperative code compilation, currently in design phase
dkml-base-compiler       --                OCaml cross-compiler and libraries from the DKML distribution that works with 
dune                     3.4.1             Fast, portable, and opinionated build system
num                      1.4               The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                    4.13.1            The OCaml compiler (virtual package)
ocaml-base-compiler      --                First alpha release of OCaml 5.0.0
ocaml-config             2                 OCaml Switch Configuration
ocaml-option-nnp         --                Set OCaml to be compiled with --disable-naked-pointers
ocaml-secondary-compiler --                OCaml 4.08.1 Secondary Switch Compiler
ocaml-variants           4.13.1+options    Official release of OCaml 4.13.1
ocamlfind                1.9.5~relocatable pinned to version 1.9.5~relocatable
ocamlfind-secondary      --                Adds support for ocaml-secondary-compiler to ocamlfind
zarith                   1.12              Implements arithmetic and logical operations over arbitrary-precision integers

Not sure what the "dkml-base-compiler" is btw. Is this required at run time?

One more thought: should I include fiat-crypto in installers? The installers don't include ocamlc - would common usage of fiat-crypto require ocamlc at run time? If so, it would make sense to include it only in the opam based "compile from sources" Coq Platform installations (which works on all platforms).

JasonGross commented 1 year ago

@MSoegtropIMC Let me tag a new release of all the relevant packages for the platform

Just for my understanding: fiat-crypto requires bedrock2 via rupicola, and this is not optional.

That's right. The dev package of fiat-crypto requires only coqutil, but the released version requires rupicola and bedrock2.

Not sure what the "dkml-base-compiler" is btw. Is this required at run time?

I'm not sure, what's the dependency path from fiat-crypto to dkml-base-compiler? We only list

depends: [
  "ocaml" {build}
  "ocamlfind" {build}
  "conf-jq" {build}
  "coq" {>= "8.11~"}
  "coq-coqprime" {>= "1.2.0"}
  "coq-rewriter" {= "0.0.2"}
  "coq-rupicola" {= "0.0.4"}
]

One more thought: should I include fiat-crypto in installers? The installers don't include ocamlc - would common usage of fiat-crypto require ocamlc at run time? If so, it would make sense to include it only in the opam based "compile from sources" Coq Platform installations (which works on all platforms).

fiat-crypto requires ocamlc to build but not to use. Common usage of fiat-crypto is either to import the Coq sources (no need for ocamlc here), or to run one of the binaries we install into BINDIR=%{bin}% (the binaries require ocamlc to build, but are standalone and don't require ocaml to run). Does this answer your question?

JasonGross commented 1 year ago

@andres-erbsen How much of bedrock2 does fiat-crypto now depend on? Previously we were only depending on bedrock2_ex, but it seems like now we maybe depend on compiler_noex as well?

JasonGross commented 1 year ago

I've added new tags, and made https://github.com/coq/opam-coq-archive/pull/2337 and https://github.com/coq/opam-coq-archive/pull/2339

I could plausibly make the bedrock2/rupicola dependency optional via depopts, but I don't think its's worth it because that would complicate the opam file, from

build: [
  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "coq" "standalone-ocaml"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "BINDIR=%{bin}%" "install" "install-standalone-ocaml"]
depends: [
  "ocaml" {build & >= "4.08~"}
  "ocamlfind" {build}
  "coq" {>= "8.15~"}
  "coq-coqprime" {>= "1.2.0"}
  "coq-rewriter" {= "0.0.5"}
  "coq-rupicola" {= "0.0.5"}
  "coq-bedrock2-compiler" {= "0.0.2"}
]

to something like

build: [
  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "SKIP_BEDROCK2=1" {!coq-rupicola:installed | !coq-bedrock2-compiler:installed} "coq" "standalone-ocaml"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "SKIP_BEDROCK2=1" {!coq-rupicola:installed | !coq-bedrock2-compiler:installed} "BINDIR=%{bin}%" "install" "install-standalone-ocaml"]
depends: [
  "ocaml" {build & >= "4.08~"}
  "ocamlfind" {build}
  "coq" {>= "8.15~"}
  "coq-coqprime" {>= "1.2.0"}
  "coq-coqutil" {= "0.0.2"}
  "coq-rewriter" {= "0.0.5"}
]
depopts: [
  "coq-rupicola"
  "coq-bedrock2-compiler"
]
conflicts: [
  "coq-rupicola" {!= "0.0.5"}
  "coq-bedrock2-compiler" {!= "0.0.2"}
]

andres-erbsen commented 1 year ago

@andres-erbsen How much of bedrock2 does fiat-crypto now depend on? Previously we were only depending on bedrock2_ex, but it seems like now we maybe depend on compiler_noex as well?

That is correct, End2End demos in fiat-crypto depend on the bedrock2 compiler and on riscv-coq. Nothing in fiat-crypto depends on bedrock2/end2end or bedrock2/processor (or kami), but bedrock2 CI does test them on Windows and Mac.

JasonGross commented 1 year ago

I've made (non-dev) packages for coq-bedrock2-compiler and coq-riscv in https://github.com/coq/opam-coq-archive/pull/2337. I can make packages for the other ones if we want ned2end or processor or kami dependencies.

MSoegtropIMC commented 1 year ago

@JasonGross : thanks for the clarifications and updates! I see if it works.

The dkml-base-compiler seems to be an optional dependency of ocaml - it is listed as recursive dependency of ocaml but not installed.

MSoegtropIMC commented 1 year ago

@JasonGross : the prerequisites now compile on Mac and Linux (didn't test Windows as yet), but for fiat-crypto I get:

File "./src/Bedrock/End2End/X25519/GarageDoor.v", line 20, characters 0-40:
Error: Cannot find a physical path bound to logical path
bedrock2Examples.LAN9250.

I also get:

Fatal error: exception Stack overflow
make: *** [Makefile:596: src/ExtractionOCaml/unsaturated_solinas] Error 2
Fatal error: exception Stack overflow
make: *** [Makefile:596: src/ExtractionOCaml/saturated_solinas] Error 2
Fatal error: exception Stack overflow
make: *** [Makefile:596: src/ExtractionOCaml/base_conversion] Error 2
Fatal error: exception Stack overflow
make: *** [Makefile:596: src/ExtractionOCaml/word_by_word_montgomery] Error 2
Fatal error: exception Stack overflow
make: *** [Makefile:596: src/ExtractionOCaml/bedrock2_unsaturated_solinas] Error 2
Fatal error: exception Stack overflow
make: *** [Makefile:596: src/ExtractionOCaml/bedrock2_saturated_solinas] Error 2

This is one a machine with 128GB RAM. Note that native compute is not enabled in Coq Platform (it would not work in the installers due to the lack of ocamlc).

MSoegtropIMC commented 1 year ago

P.S.: what works (and this is a big step forward) is:

  PACKAGES="${PACKAGES} coq-coqutil.0.0.2"
  PACKAGES="${PACKAGES} coq-rewriter.0.0.6"
  PACKAGES="${PACKAGES} coq-riscv.0.0.2"
  PACKAGES="${PACKAGES} coq-bedrock2.0.0.2"
  PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.2"
  PACKAGES="${PACKAGES} coq-rupicola.0.0.5"

JasonGross commented 1 year ago

@MSoegtropIMC to fix the stack overflow, try ulimit -s 32768 as in https://github.com/coq/coq/blob/ae720ae193c957e1882f7c87b1c85b2f4ecde629/dev/ci/ci-fiat_crypto.sh#L13-L24

@andres-erbsen can you help debug the issue with bedrock2? We are installing with make "EXTERNAL_DEPENDENCIES=1" "install_bedrock2" at https://github.com/coq/opam-coq-archive/blob/6ec231b2c7cf2fe49c74182987e4c5e41c263650/released/packages/coq-bedrock2/coq-bedrock2.0.0.2/opam#L14 Is there a reason this would miss bedrock2Examples.LAN9250?

andres-erbsen commented 1 year ago

https://github.com/mit-plv/bedrock2/blob/master/bedrock2/Makefile#L98 installs without examples, fiat-crypto needs install with examples

MSoegtropIMC commented 1 year ago

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

JasonGross commented 1 year ago

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

MSoegtropIMC commented 1 year ago

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 commented 1 year ago

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

JasonGross commented 1 year ago

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 https://github.com/coq/platform/issues/178#issuecomment-1211112651 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.

coq / platform

fiat cryptography #178