Bas Spitters

@gmalecha the goals of ext-lib and stdlibpp seem similar. I know you are using both. Would it make sense to try to merge some common parts? There also seems to...

bedrock1 CPS semantics vs bedrock2 postcondition semantics

1

It looks the semantics style has changed between bedrock1 and bedrock2. Is there an overview of which properties we can expect to continue to hold? Of course, one could read...

Reverse dependency?

1

As you know, we have a project depending on fiat-crypto/bedrock https://github.com/AU-COBRA/AUCurves What would be the best way to set up CI? Would it be possible to run this as part...

Platform

2

Inclusion in platform will aid easy installation on all OSes: https://github.com/coq/platform

Jasmin and alternate Montgomery strategies

16

Bedrock2 seems to share a lot of common goals with Jasmin. Jasmin also has an [RISC-V branch](https://github.com/jasmin-lang/jasmin/tree/risc5) Have you considered how they could interact?

Here's a mention of using fiat-crypto to support native crypto in wasm: https://github.com/WebAssembly/wasi-crypto/issues/18

Add an option to clean up the pages

1

Tools like http://scantailor.org/ or http://code.google.com/p/ocrfeeder/ can clean up separate pages. Maybe this can be integrated in the process?

Thanks for the nice program. On a large PDF the collected ppm files can become huge. When not using the -k option, I think i.ppm can be removed once i-new.pdf...

HACSpec

2

Thanks for the nice project! There are some overlaps in goals with the [hacspec](https://github.com/hacspec/hacspec/) project. Cryptographic primitives have been specified there, and some work on ZK proofs is underway. There...

Hoogle like search

2

## Meta-issue ## @peterlefanulumsdaine wants to have hoogle like search for Coq. The coq-community database could be a good target for this. One could start from Search and SearchAbout, but...