Cryptographic Primitive Code Generation by Fiat

Overview

Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives

Building

CI (Coq) CI (Coq, Windows) CI (Coq, MacOS)

Zulip Rust Crate Go Reference

This repository requires Coq 8.11 or later. Note that if you install Coq from Ubuntu aptitude packages, you need libcoq-ocaml-dev in addition to coq. Note that in some cases (such as installing Coq via homebrew on Mac), you may also need to install ocaml-findlib (for ocamlfind). If you want to build the bedrock2 code, you need Coq 8.13 or later (otherwise you can pass SKIP_BEDROCK2=1 to make). We suggest downloading the latest version of Coq. Generation of JSON code via the Makefile also requires jq.

Alternatively, choose your package-manager to install dependencies:

Package Manager Command Line Invocation
Aptitude (Ubuntu / Debian) apt install coq ocaml-findlib libcoq-ocaml-dev jq
Homebrew (OS X) brew install coq ocaml-findlib coreutils jq
Pacman (Archlinux) pacman -S coq ocaml-findlib ocaml-zarith jq

You can clone this repository with

git clone --recursive https://github.com/mit-plv/fiat-crypto.git

Git submodules are used for some dependencies. If you did not clone with --recursive, run

git submodule update --init --recursive

from inside the repository. Then run:

make

You can check out our CI to see how long the build should take; as of the last update to this line in the README, it takes about 1h10m to run make -j2 on Coq 8.11.1.

If you want to build only the command-line binaries used for generating code, you can save a bit of time by making only the standalone-ocaml target with

make standalone-ocaml

Usage (Generating C Files)

The Coq development builds binary compilers that generate code using some implementation strategy. The parameters (modulus, hardware multiplication input bitwidth, etc.) are specified on the command line of the compiler. The generated C code is written to standard output.

A collection of C files for popular curves can be made with

make c-files

The C files will appear in fiat-c/src/.

Just the compilers generating these C files can be made with

make standalone-ocaml

or make standalone-haskell for compiler binaries generated with Haskell, or make standalone for both the Haskell and OCaml compiler binaries. The binaries are located in src/ExtractionOcaml/ and src/ExtractionHaskell/ respectively.

There is a separate compiler binary for each implementation strategy:

  • saturated_solinas
  • unsaturated_solinas
  • word_by_word_montgomery

Passing no arguments, or passing -h or --help (or any other invalid arguments) will result in a usage message being printed. These binaries output C code on stdout.

Here are some examples of ways to invoke the binaries (from the directories that they live in):

# Generate code for 2^255-19
./unsaturated_solinas '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c
./unsaturated_solinas '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c

# Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1)
./word_by_word_montgomery 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c
./word_by_word_montgomery 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c

You can find more examples in the Makefile.

Note that for large primes, you may need to increase the stack size to avoid stack overflows. For example:

ulimit -S -s 1048576; ./word_by_word_montgomery --static gost_512_paramSetB 32 '2^511 + 111'

This sets the stack size to 1 GB (= 1024 MB = 1024 * 1024 KB = 1048576 KB) before running the command. As of the last edit of this line, this command takes about an hour to run, but does in fact complete successfully. Without a sufficiently large stack-size, it instead stack overflows.

Usage (Generating Bedrock2 Files)

Output is supported to the research language bedrock2. The Coq development builds binary compilers that generate code using some implementation strategy. The parameters (modulus, hardware multiplication input bitwidth, etc.) are specified on the command line of the compiler. The generated bedrock2 code is then written to standard output using the bedrock2 C backend.

A collection of bedrock2/C files for popular curves can be made with

make bedrock2-files

The bedrock2/C files will appear in fiat-bedrock2/src/.

Just the compilers generating these bedrock2/C files can be made with

make standalone-ocaml

or make standalone-haskell for binaries generated with Haskell, or make standalone for both the Haskell and OCaml binaries. The binaries are located in src/ExtractionOcaml/ and src/ExtractionHaskell respectively.

There is a separate compiler binary for each implementation strategy:

  • bedrock2_saturated_solinas
  • bedrock2_unsaturated_solinas
  • bedrock2_word_by_word_montgomery

Passing no arguments, or passing -h or --help (or any other invalid arguments) will result in a usage message being printed. These binaries output bedrock2/C code on stdout.

Here are some examples of ways to invoke the binaries (from the directories that they live in):

# Generate code for 2^255-19
./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c
./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c

# Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1)
./bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c
./bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c

# Generate code for 2^130 - 5
./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '64' '3' '2^130 - 5' > poly1305_64.c
./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '32' '5' '2^130 - 5' > poly1305_32.c

You can find more examples in the Makefile.

License

Fiat-Crypto is distributed under the terms of the MIT License, the Apache License (Version 2.0), and the BSD 1-Clause License; users may pick which license to apply.

See COPYRIGHT, LICENSE-MIT, LICENSE-APACHE, and LICENSE-BSD-1 for details.

Extended Build Instructions

If your COQPATH variable is not empty, you can build with:

export COQPATH="$(pwd)/rewriter/src:$(pwd)/coqprime/src:$(pwd)/bedrock2/bedrock2/src:$(pwd)/bedrock2/deps/coqutil/src${COQPATH:+:}$COQPATH"
make

Reading About The Code

Status of Backends

Fiat Cryptography contains a number of backends; the final step of the pipeline is transforming from straight-line C-like code to expressions in whatever language is being targeted. The Bedrock2 backend comes with proofs that the Bedrock2 AST matches the semantics of our internal AST, but none of the other backends have any proofs about them. While the transformations are not particularly involved, and our proofs ensure that we have picked integer sizes large enough to store values at each operation, there is no verification that the particular integer size casts that we emit are sufficient to ensure that gcc, clang, or whatever compiler is used on the code correctly selects integer sizes for expressions correctly. Note that even the C code printed by the Bedrock2 backend does not have proofs that the conversion to strings is correct.

Hence we provide here a table of the extent to which the various backends are maintained, tested, and proven. A ✔️ in "maintainer" means that the Fiat Cryptography maintainers are fully maintaining and testing the backend; means maintenance by external contributors. We do not provide any quality guarantees for code generated by the backends.

Backend Maintainer / Person of Contact Build Checked by CI Generated Code Tested Internal AST Proven Correct
C ✔️ @JasonGross / entire team ✔️ ✔️ (BoringSSL test-suite)
Bedrock2/C ✔️ @andres-erbsen / entire team ✔️ ✔️ (BoringSSL test-suite) ✔️
Go @mdempsky ✔️
Java Unmaintained ✔️ Known Buggy #707
JSON Experimental (only syntax)
Rust ✔️ ✔️ (Dalek Cryptography test-suite)
Zig @jedisct1 ✔️ (Zig standard library (generated file here) (main CI here))

Contributing a new backend

We weclome new backends (as long as you're willing to maintain them). We hope that the process of contributing a new backend is not too painful, and welcome feedback on how the process could be streamlined. To contribute a new backend, follow the following steps (perhaps using, for example, #936, #660, #638, or #570 as examples):

  • Add a new file to src/Stringification/ for your language, modeled after the existing file of your choice
  • Run git add on your new file and then make update-_CoqProject to have the build system track your file
  • Update src/CLI.v to Require Import your file and add your language to the list default_supported_languages so that it can be passed to the binaries as an argument to --lang
  • Update the Makefile in the following ways:
    • Consider adding a variable near CARGO_BUILD for the build invocation
    • Add targets to .PHONY analogous to c-files, lite-c-files, test-c-files, only-test-c-files
    • Add a variables analogous to C_DIR, ALL_C_FILES, and LITE_C_FILES for your language's generated files
    • Add targets analogous to c-files and lite-c-files and make generated-files and lite-generated-files depend on those targets respectively
    • Add build rules for ALL_<YOUR-LANGUAGE>-FILES
    • Add targets for test-<your-language>-files and only-test-<your-language>-files; both targets should have the same build rule, but test-<your-language>-files should depend on all the generated files of your language, while only-test-<your-language>-files should not have any build rule dependencies.
    • If you are developing a package, you can look for uses of COPY_TO_FIAT_RUST or COPY_TO_FIAT_GO to see how license files are copied
  • Run make to generate all the relevant files of your language, and add the generated files to git
  • Update .gitignore to ignore any compiled files generated by the compiler of your language (analogous to .o and .a for C)
  • Create a file in .github/workflows/ like c.yml, go.yml, rust.yml, etc, to test at least that the generated code compiles.
    • Optionally, also test the built code against some external project's crypto unit tests
  • Update .gitattributes to mark your language's generated files as text and to mark the paths of the generated files as linguist-generated so that diffs don't clog up PR displays.
  • Add your language to the table in preceeding section of the README indicating the status of your backend and marking your GitHub username as the maintainer.

Reading The Code

Demo of Synthesis

The idea of the synthesis process is demoed in src/Demo.v. We strongly recommend reading this before studying the full-scale system.

Proofs About Elliptic Curves

We have some about elliptic curves, for example:

Actual Synthesis Pipeline

The entry point for clients of the PHOAS expressions we use is Language/API.v. Refer to comments in that file for an explanation of the interface; the following text describes how the expressions are generated, not how to interact with them.

The ordering of files (eliding *Proofs.v files) is:

Language/*.v
    ↑
    ├────────────────────────────────┬───────────────────────┬───────────────────────┐
AbstractInterpretation/*.v     MiscCompilerPasses.v    Rewriter/*.v     PushButtonSynthesis/ReificationCache.v      Arithmetic.v
    ↑                                ↑                       ↑                       ↑                                   ↑
Stringification/*.v                  │                       │                       │                        COperationSpecifications.v
    ↑                                │                       │                       │                                   ↑
    └────────────┬───────────────────┴───────────────────────┴────────┬──────────────┘                                   │
           BoundsPipeline.v                                  CompilersTestCases.v                                        │
                 ↑                                                                                                       │
                 └────────────┬──────────────────────────────────────────────────────────────────────────────────────────┘
                     PushButtonSynthesis/*.v
                              ↑
                   ┌──────────┴────────────────┐
                  CLI.v                SlowPrimeSynthesisExamples.v
                   ↑
        ┌──────────┴────────────────┐
StandaloneHaskellMain.v   StandaloneOCamlMain.v
        ↑                           ↑
ExtractionHaskell.v          ExtractionOCaml.v

Within each directory, the dependency graphs (again eliding *Proofs.v and related files) are:

Within Language/:

  Pre.v ←──────────────────────────────────────────────────────────────────────── IdentifierParameters.v
    ↑                                                                                        ↑
Language.v ←── IdentifiersBasicLibrary.v ←──── IdentifiersBasicGenerate.v ←── IdentifiersBasicGENERATED.v ←───────────────────────────── API.v
    ↑                        ↑                                                               ↑
    ├────────────────┐       └────────────────────────────┐                                  │
UnderLets.v    IdentifiersLibrary.v ←──────────── IdentifiersGenerate.v ←─────── IdentifiersGENERATED.v
                     ↑                                       ↑                               ↑
              IdentifiersLibraryProofs.v ←─── IdentifiersGenerateProofs.v ←─ IdentifersGENERATEDProofs.v

Within Stringification/:

Language.v
    ↑
   IR.v
    ↑
 ┌──┴───────┐
C.v       Rust.v

We will come back to the Rewriter/* files shortly.

The files contain:

  • Arithmetic.v: All of the high-level field arithmetic stuff

  • COperationSpecifications.v: The specifications for the various operations to be synthesized. TODO: This file should probably be renamed.

  • AbstractInterpretation/*.v: type-code-based ZRange definitions, abstract interpretation of identifiers (which does let-lifting, for historical reasons, and the dependency on UnderLets should probably be removed), defines the passes:

    • PartialEvaluateWithBounds
    • PartialEvaluateWithListInfoFromBounds
    • CheckPartialEvaluateWithBounds
  • MiscCompilerPasses.v: Defines the passes:

    • EliminateDead (dead code elimination)
    • Subst01 (substitute let-binders used 0 or 1 times)
  • Rewriter/*.v: rewrite rules, rewriting. See below for actual structure of files. Defines the passes:

    • RewriteNBE
    • RewriteArith
    • RewriteArithWithCasts
    • RewriteStripLiteralCasts
    • RewriteToFancy
    • RewriteToFancyWithCasts
    • PartialEvaluate (which is just a synonym for RewriteNBE)
  • Inside Language/:

    • Pre.v: A few definitions which are used in writing out rewrite rules and the interpretations of PHOAS identifiers, e.g., ident.cast, ident.eagerly, Thunked.list_rect, etc

    • Language.v: Defines parts of the PHOAS basic infrastructure parameterized over base types and identifiers including: . PHOAS . reification . denotation/intepretation . utilities for inverting PHOAS exprs . default/dummy values of PHOAS exprs . default instantiation of generic PHOAS types . Gallina reification of ground terms . Flat/indexed syntax trees, and conversions to and from PHOAS

      Defines the passes: . ToFlat . FromFlat . GeneralizeVar

    • API.v: Specializes the type of PHOAS expressions to the particular identifiers we're using, and defines convenience notations, tactics, and definitions for some of the specialized versions.

    • IdentifierParameters.v: Defines a couple of definitions determining the identifiers and types used by the language. These are used as input for the generation of identifier definitions.

    • IdentifiersBasicLibrary.v: Defines the package type holding basic identifier definitions.

    • IdentifiersBasicGenerate.v: Defines the tactics that generate all of the identifier-list-specific definitions used by the PHOAS machinery, in addition to defining the tactics that do reification based on the generated package.

    • IdentifiersBasicGENERATED.v: Basically autogenerated file that defines the inductives of base type codes and identifier codes (the first hand-written because it's short; the latter copy-pasted from a tactic that prints out the inductive), and calls the package-generation-tactic from IdentifiersBasicGenerate.v.

    • UnderLets.v: the UnderLets monad, a pass that does substitution of var-like things, a pass that inserts let-binders in the next-to-last line of code, substituting away var-like things (this is used to ensure that when we output C code, aliasing the input and the output arrays doesn't cause issues). Defines the passes: . SubstVar . SubstVarLike . SubstVarOrIdent

    The following files in Language/ are used only by the rewriter:

    • IdentifiersLibrary.v: Some definitions about identifiers and pattern identifiers and raw identifiers. Some of these definitions take generated definitions as arguments. Also defines a package record to hold all of the generated definitions.

    • IdentifiersGenerate.v: Tactics to generate definitions about untyped and pattern versions of identifiers for the rewriter. Culminates in a tactic which inhabits the package type defined in IdentifiersLibrary.v

    • IdentifiersLibraryProofs.v: proofs about definitions in IdentifiersLibrary. Also defines a package to hold generated proofs that require destructing inductives not yet defined in this file.

    • IdentifiersGenerateProofs.v: tactics to prove lemmas to inhabit the package defined in IdentifiersLibraryProofs.v

    • IdentifiersGENERATE.v: identifiers / inductives and definitions generated by IdentifiersGenerate.

    • IdentifiersGENERATEProofs.v: proofs generated by IdentifiersGenerateProofs, about definitions in IdentifiersGENERATE

  • Inside Stringification/:

    • Language.v: defines a printer (Show instance) for the PHOAS language, defines some common language-independent utilities for conversion to output code, and defines the spec/API of conversion from PHOAS to code in a language as strings. (Depends on AbstractInterpretation.v for ZRange utilities.) Defines the passes: . ToString.LinesToString . ToString.ToFunctionLines

    • IR.v: Defines a common IR for C and Rust (and maybe eventually other languages), and builds most of the infrastructure necessary for instantiating the LanguageSpecification API for a language with pointers and function calls

    • C.v: conversion to C code as strings. Instantiates the API defined in Stringification.Language.

    • Rust.v: conversion to Rust code as strings. Instantiates the API defined in Stringification.Language.

  • CompilersTestCases.v: Various test cases to ensure everything is working

  • BoundsPipeline.v: Assemble the various compiler passes together into a composed pipeline. It is the final interface for the compiler. Also contains some tactics for applying the BoundsPipeline correctness lemma.

  • PushButtonSynthesis/ReificationCache.v: Defines the cache that holds reified versions of operations, as well as the tactics that reify and apply things from the cache.

  • PushButtonSynthesis/*: Reifies the various operations from Arithmetic.v, defines the compositions of the BoundsPipeline with these operations, proves that their interpretations satisfies the specs from COperationSpecifications.v, assembles the reified post-bounds operations into synthesis targets. These are the files that CLI.v depends on:

    • ReificationCache.v: Defines the cache of pre-reified terms. Splitting up reification from uses of the pipeline allows us to not have to re-reify big terms every time we change the pipeline or intermediate stages thereof.
    • InvertHighLow.v: Defines some common definitions, around splitting apart high and low bits of things, for Barrett and FancyMontgomeryReduction.
    • Primitives.v: Specializes the pipeline to basic "primitive" operations such as cmovznz, addcarryx, subborrowx, etc.
    • SmallExamples.v: Some small examples of using the pipeline. Nothing depends on this file; it is for demonstration purposes only.
    • *ReificationCache.v: Holds the reified versions of the definitions used in the corresponding file.
    • BarrettReduction.v, FancyMontgomeryReduction.v, SaturatedSolinas.v, UnsaturatedSolinas.v, WordByWordMontgomery.v: Holds the instantiation of the pipeline to the corresponding implementation choice, as well as any relevant correctness proofs (such as that things assemble into a ring).
  • SlowPrimeSynthesisExamples.v: Additional uses of the pipeline for primes that are kind-of slow, which I don't want extraction blocking on. Also contains some debugging examples.

  • CLI.v: Setting up all of the language-independent parts of extraction; relies on having a list of strings-or-error-messages for each pipeline, and on the arguments to that pipeline, and builds a parser for command line arguments for that.

  • StandaloneHaskellMain.v, StandaloneOCamlMain.v, ExtractionHaskell.v, ExtractionOCaml.v: Extraction of pipeline to various languages

The files defined in Rewriter/ are split up into the following dependency graph (including some files from Language/ at the top):

IdentifiersLibrary.v ←───────────────────────── IdentifiersGenerate.v ←──────────────────── IdentifiersGENERATED.v
    ↑ ↑                                                   ↑                                        ↑
    │ └──────────────── IdentifiersLibraryProofs.v ←──────┴─ IdentifiersGenerateProofs.v ←─ IdentifersGENERATEDProofs.v
    │                                     ↑                                                        ↑
    │                                     │                                                        │
    │                                     │                                                        │
    │                                     │                                                        │
    │                                     │                                                        │
Rewriter.v ←────────────────────── ProofsCommon.v ←──────────────────── ProofsCommonTactics.v      │
    ↑                                 ↗        ↖                                ↑                  │
Reify.v ←──────────────┐           Wf.v   InterpProofs.v                        │                  │
                       │              ↖        ↗                                │                  │
Rules.v                └──────────── AllTactics.v ──────────────────────────────┘                  │
    ↑                                      ↑       ┌───────────────────────────────────────────────┘
RulesProofs.v                         AllTacticsExtra.v
    ↑                                      ↑
    ├────────┬─────────────┬───────────────┴────────┬─────────────────────────────┐
    │   Passes/NBE.v    Passes/Arith.v    Passes/ArithWithCasts.v    Passes/StripLiteralCasts.v
    │        ↑             ↑                        ↑                             ↑
    │        └─────────────┴────────────────────────┴─────────────────────────────┴─────────────┐
    │                                                                                           │
    └────────┬──────────────────────────┐                                                       │
      Passes/ToFancy.v      Passes/ToFancyWithCasts.v                                           │
             ↑                          ↑                                                       │
             └───────┬──────────────────┴───────────────────────────────────────────────────────┘
                     │
                   All.v
  • Rules.v: Defines the list of types of the rewrite rules that will be reified. Largely independent of the expression language.

  • RulesProofs.v: Proves all of the Gallina versions of the rewrite rules correct.

  • Rewriter.v: Defines the rewriter machinery. In particular, all of the rewriter definitions that have non-rewrite-rule-specific proofs about them are found in this file.

  • RewrierReify.v: Defines reification of rewrite rules, continuing on from Rewriter.v, and culminates in the tactic RewriteRules.Tactic.Build_RewriterT and the tactic notation make_Rewriter which define a package of type RewriteRules.GoalType.RewriterT. The Build_* tactic returns a constr, while the make_* tactic notation refines that constr in the goal. Both tactics take two arguments: first a boolean include_interp which specifies whether (true) or not (false) to prefix the list of rewrite rules with the reduction-to-literal rewrite rules; and second a list of bool * Prop which is the list of rewrite rule types to reify, each paired with a boolean saying whether or not to try rewriting again in the output of the replacement for that rule.

  • ProofsCommon.v: Defines the notion of interp-goodness and wf-goodness for rewrite rules, defines tactics to prove these notions, and contains a semi-arbitrary collection of proofs and definitions that are mostly shared between the wf proofs and the interp proofs. Importantly, this file defines everything needed to state and prove that specific rewrite rules are correct. Additionally defines a package RewriteRules.GoalType.VerifiedRewriter which describes the type of the overall specialized rewriter together with its Wf and Interp proofs. (This package should perhaps move to another file?)

  • ProofsCommonTactics.v: Defines the actual tactics used to prove that specific rewrite rules are correct, and to inhabit the packages defined in ProofsCommon.v.

  • Wf.v: Proves wf-preservation of the generic rewriter, taking in wf-goodness of rewrite rules as a hypothesis.

  • InterpProofs.v: Proves interp-correctness of the generic rewriter, taking in interp-goodness of rewrite rules as a hypothesis.

  • AllTactics.v: Defines the tactic RewriteRules.Tactic.make_rewriter (and a similar tactic notation) which build the entire VerifiedRewriter. They take in the include_interp as in Rewriter.v tactics, as well as an hlist of proofs of rewrite rules indexed over a list (bool * Prop) of rewrite rule types. This is the primary interface for defining a rewriter from a list of rewrite rules.

  • AllTacticsExtra.v: Specializes AllTactics.v to what's defined in Identifier.v

  • {NBE, Arith, ArithWithCasts, StripLiteralCasts, ToFancy, ToFancyWithCasts}.v: Use the tactic from AllTactics.v together with the proven list of rewrite rules from RulesProofs.v to reify and reduce the corresponding pass and generate a rewriter.

  • All.v: Definitionless file that Exports the rewriters defined in Rewriter/*.v

Proofs files: For Language.v, there is a semi-arbitrary split between two files Language.Inversion and Language.Wf.

  • Inversion.v:

    • classifies equality of type codes and exprs
    • type codes have decidable equality
    • correctness of the various type-transport definitions
    • correctness lemmas for the various expr.invert_* definitions
    • correctness lemmas for the various reify_* definitions in Language.v
    • inversion_type, which inverts equality of type codes
    • type_beq_to_eq, which converts boolean equality of types to Leibniz equality
    • rewrite_type_transport_correct, which rewrites with the correctness lemmas of the various type-transport definitions
    • type.invert_one e which does case analysis on any inductive type indexed over type codes, in a way that preserves information about the type of e, and generally works even when the goal is dependently typed over e and/or its type
    • ident.invert, which does case-analysis on idents whose type has structure (i.e., is not a var)
    • ident.invert_match, which does case-analysis on idents appearing as the discriminee of a match in the goal or in any hypothesis
    • expr.invert, which does case-analysis on exprs whose type has structure (i.e., is not a var)
    • expr.invert_match, which does case-analysis on exprs appearing as the discriminee of a match in the goal or in any hypothesis
    • expr.invert_subst, which does case-analysis on exprs which show up in hypotheses of the form expr.invert_* _ = Some _
    • expr.inversion_expr, which inverts equalities of exprs
  • Wf.v: Depends on Inversion.v Defines:

    • expr.wf, expr.Wf, expr.wf3, expr.Wf3
    • GeneralizeVar.Flat.wf
    • expr.inversion_wf (and variants), which invert wf hypotheses
    • expr.wf_t (and variants wf_unsafe_t and wf_safe_t) which make progress on wf goals; wf_safe_t should never turn a provable goal into an unprovable one, while wf_unsafe_t might.
    • expr.interp_t (and variants), which should make progress on equivalence-of-interp hypotheses and goals, but is not used much (mainly because I forgot I had defined it)
    • prove_Wf, which proves wf goals on concrete syntax trees in a more optimized way than repeat constructor Proves:
    • funext → (type.eqv Logic.eq) (eqv_iff_eq_of_funext)
    • type.related and type.eqv are PERs
    • Proper instances for type.app_curried, type.and_for_each_lhs_of_arrow
    • type.is_not_higher_order → Reflexive (type.and_for_each_lhs_of_arrow type.eqv)
    • iff between type.related{,_hetero} and related of type.app_curried
    • various properties of type.and{,b_bool}for_each_lhs_of_arrow
    • various properties of type.eqv and ident.{gen_,}interp
    • various properties of ident.cast
    • various properties of expr.wf (particularly of things defined in Language.v)
    • interp and wf proofs for the passes to/from Flat
  • UnderLetsProofs.v: wf and interp lemmas for the various passes defined in UnderLets.v

  • MiscCompilerPassesProofs.v: wf and interp lemmas for the various passes defined in MiscCompilerPasses.v

  • AbstractInterpretation/ZRangeProofs.v: Proves correctness lemmas of the per-operation zrange-bounds-analysis functions

  • AbstractInterpretation/Wf.v: wf lemmas for the AbstractInterpretation pass

  • AbstractInterpretation/Proofs.v: interp lemmas for the AbstractInterpretation pass, and also correctness lemmas that combine Wf and interp

Comments
  • Word-by-Word Montgomery Reduction

    Word-by-Word Montgomery Reduction

    https://eprint.iacr.org/2011/239.pdf Lemma 1 https://eprint.iacr.org/2013/816.pdf Algorithm 1

    High-level behavior: divides T by R modulo N (with not necessarily minimal output). Makes use of the fact that R = w i for some i by repeatedly dividing by the bounds of each digit up to i. Each such division is implemented by first adjusting T such that it is 0 mod (bound i) and discarding its lowest limb. The adjustment is T += N * ((((T mod (bound i)) * ((-N^-1) mod (bound i))) mod (bound i)), which obviously preserves the value mod N. Looking mod (bound i) this does T += -T, so the result must be divisible by bound i and if the last limb has divmod relationship with the remaining limbs, discarding it executes the division. I believe the proof in https://github.com/mit-plv/fiat-crypto/blob/master/src/Arithmetic/MontgomeryReduction/Proofs.v covers each single step here, but operating on multiple limbs needs to be argued by canonical saturated basesystem logic. Yet another reason to have nice support for reasoning about canonicity properties of compact output.

    enhancement 
    opened by andres-erbsen 66
  • Mem extention

    Mem extention

    this is the PR split from #1123. I do get an Error in Parse.v

    File "./src/Assembly/Parse.v", line 190, characters 129-130: Error: Syntax error: [term level 70] expected after ';;R' (in [term]).

    which I don't understand. Generally, I think I need some feedback on what I am trying to do. I just can't get the syntax right with (Z * REG)

    Edit: I skipped the Bedrock files for now, because I want to get the others compile correct first.

    opened by dderjoel 61
  • adding `shl shlx` to mul * imm

    adding `shl shlx` to mul * imm

    This adds two example files using different instructions to multiply by constants using lea / shl / shlx. Also it enables the parser to parse those new instructions, but it is still unable to unify. I think this is because it does not know that a + a == 2*a == 2<<1 and a * 19 == a + 2 * (8a + a), a * 2 * 2 == a * 4 ... Also I'd need some pointers to parse MEM with scaled index, i.e. [ reg + N * reg ]; N being 2, 4, 8.

    opened by dderjoel 44
  • Curves from JSON

    Curves from JSON

    The X25519 curves are now generated from .json files. This code only works in >= 8.7, because it makes use of the recently-merged-from-fiat transparent_abstract tactic to allow defining things in tactics without massive slowdown. The structure is as follows: 0. The module types and tactic definitions that set up the infrastructure live in src/Specific/Framework/

    1. There are .json files in src/Specific/CurveParameters/ that specify curve characteristics. These configuration files don't yet handle Montgomery/P256, nor Karatsuba. @andres-erbsen @jadephilipoom do you have thoughts on unifying the synthesis in all these different cases?

    A simple example is x2555_130.json, which is:

    {
        "modulus"          : "2^255-5",
        "base"             : "130",
        "a24"              : "121665 (* XXX TODO(andreser) FIXME?  Is this right for this curve? *)",
        "sz"               : "3",
        "bitwidth"         : "128",
        "carry_chain1"     : "default",
        "carry_chain2"     : ["0", "1"],
        "coef_div_modulus" : "2",
        "operations"       : ["ladderstep"]
    }
    

    A more complicated example is x25519_c64.json:

    {
        "modulus"          : "2^255-19",
        "base"             : "51",
        "a24"              : "121665",
        "sz"               : "5",
        "bitwidth"         : "64",
        "carry_chain1"     : "default",
        "carry_chain2"     : ["0", "1"],
        "coef_div_modulus" : "2",
        "operations"       : ["femul", "fesquare", "freeze", "ladderstep"],
        "extra_files"      : ["X25519_C64/scalarmult.c"],
        "compiler"         : "gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes",
        "mul_header"       : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
        "mul_code"
        :
        "
      uint128_t t[5];
      limb r0,r1,r2,r3,r4,s0,s1,s2,s3,s4,c;
    
      r0 = in[0];
      r1 = in[1];
      r2 = in[2];
      r3 = in[3];
      r4 = in[4];
    
      s0 = in2[0];
      s1 = in2[1];
      s2 = in2[2];
      s3 = in2[3];
      s4 = in2[4];
    
      t[0]  =  ((uint128_t) r0) * s0;
      t[1]  =  ((uint128_t) r0) * s1 + ((uint128_t) r1) * s0;
      t[2]  =  ((uint128_t) r0) * s2 + ((uint128_t) r2) * s0 + ((uint128_t) r1) * s1;
      t[3]  =  ((uint128_t) r0) * s3 + ((uint128_t) r3) * s0 + ((uint128_t) r1) * s2 + ((uint128_t) r2) * s1;
      t[4]  =  ((uint128_t) r0) * s4 + ((uint128_t) r4) * s0 + ((uint128_t) r3) * s1 + ((uint128_t) r1) * s3 + ((uint128_t) r2) * s2;
    
      r4 *= 19;
      r1 *= 19;
      r2 *= 19;
      r3 *= 19;
    
      t[0] += ((uint128_t) r4) * s1 + ((uint128_t) r1) * s4 + ((uint128_t) r2) * s3 + ((uint128_t) r3) * s2;
      t[1] += ((uint128_t) r4) * s2 + ((uint128_t) r2) * s4 + ((uint128_t) r3) * s3;
      t[2] += ((uint128_t) r4) * s3 + ((uint128_t) r3) * s4;
      t[3] += ((uint128_t) r4) * s4;
    ",
        "square_header"    : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
        "square_code"
        :
        "
      uint128_t t[5];
      limb r0,r1,r2,r3,r4,c;
      limb d0,d1,d2,d4,d419;
    
      r0 = in[0];
      r1 = in[1];
      r2 = in[2];
      r3 = in[3];
      r4 = in[4];
    
      do {
        d0 = r0 * 2;
        d1 = r1 * 2;
        d2 = r2 * 2 * 19;
        d419 = r4 * 19;
        d4 = d419 * 2;
    
        t[0] = ((uint128_t) r0) * r0 + ((uint128_t) d4) * r1 + (((uint128_t) d2) * (r3     ));
        t[1] = ((uint128_t) d0) * r1 + ((uint128_t) d4) * r2 + (((uint128_t) r3) * (r3 * 19));
        t[2] = ((uint128_t) d0) * r2 + ((uint128_t) r1) * r1 + (((uint128_t) d4) * (r3     ));
        t[3] = ((uint128_t) d0) * r3 + ((uint128_t) d1) * r2 + (((uint128_t) r4) * (d419   ));
        t[4] = ((uint128_t) d0) * r4 + ((uint128_t) d1) * r3 + (((uint128_t) r2) * (r2     ));
    "
    }
    
    1. The src/Specific/CurveParameters/remake_curves.sh script holds a list of curves to be made, what directories they should end up living in, and it invokes src/Specific/Framework/make_curve.py to transform these files into outputs. The Python script fills in a few defaults (such as computing s and c from the modulus, if you don't pass them explicitly), and does a lot of processing on the C code that is pasted verbatim from donna to get it to be in the right format for Coq.

    This Python script creates the files:

    • CurveParameters.v (the Coq-ified version of the json file, which instantiates an appropriate module type);
    • Synthesis.v, which instantiates a MakeSynthesisTactics with the curve parameter modules, invokes a tactic from the applied module functor to synthesize all of the relevant non-reflective bits (basically, what used to live in @jadephilipoom 's ArithmeticSynthesisTest.v), and then instantiates another module functor PackageSynthesis which defines notations via tactics in terms to access the names of the various fields defined by the synthesis tactic;
    • any other files you ask it for, such as compiler.sh, femul.v, femulDisplay.v. All of the *Display.v files are simple, and all the the operation synthesis files have a single Definition (with the appropriate type), and solve the definition by invoking a single tactic defined in PackageSynthesis, e.g., synthesize_mul or synthesize_ladderstep.
    Coq 8.7 
    opened by JasonGross 34
  • ArithmeticSynthesisTest for Montgomery multiplication

    ArithmeticSynthesisTest for Montgomery multiplication

    How far away are we from having something like ArithmeticSynthesisTest that uses montgomery multiplication (leaving in admits)? If we can get that, then I can start looking into adding loops to the reflective machinery.

    opened by JasonGross 27
  • bedrock2 extraction tracker issue

    bedrock2 extraction tracker issue

    It would be cool to generate bedrock2 code from fiat-crypto. I think it might go roughly as follows:

    • [x] generate fiat-crypto low-level AST with only word sizes 32 and 64
    • [x] break each 64-bit word into two 32-bit words (e.g., using mul_split)
    • [x] translate that AST to bedrock2.Syntax.cmd
    opened by andres-erbsen 26
  • Use native_compute rather than vm_compute

    Use native_compute rather than vm_compute

    This should hopefully speed things up. See also https://github.com/coq/coq/pull/8055.

    Except it doesn't speed things up (maybe because we are frequently computing enormous PHOAS syntax trees?), so we probably shouldn't merge this. cc @ppedrot

    After     | File Name                                          | Before    || Change    | % Change
    --------------------------------------------------------------------------------------------------
    15m44.56s | Total                                              | 10m54.17s || +4m50.38s | +44.39%
    --------------------------------------------------------------------------------------------------
    11m49.08s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m50.36s  || +4m58.72s | +72.79%
    2m14.24s  | Experiments/NewPipeline/Toplevel2                  | 2m23.03s  || -0m08.78s | -6.14%
    1m37.61s  | Experiments/NewPipeline/Toplevel1                  | 1m37.18s  || +0m00.42s | +0.44%
    0m01.31s  | Experiments/NewPipeline/CLI                        | 0m01.30s  || +0m00.01s | +0.76%
    0m01.20s  | Experiments/NewPipeline/StandaloneOCamlMain        | 0m01.20s  || +0m00.00s | +0.00%
    0m01.12s  | Experiments/NewPipeline/StandaloneHaskellMain      | 0m01.10s  || +0m00.02s | +1.81%
    
    work in progress 
    opened by JasonGross 21
  • Karatsuba test case for bounds analysis

    Karatsuba test case for bounds analysis

    To work on the bounds analysis procedure we discussed, I'd like the following:

    • A file, say, src/Specific/IntegrationTestKaratsuba.v, like src/Specific/IntegrationTestMul.v, which uses the karatsuba algorithm in something-or-other, and compiles up to the (* jgross start here *) comment
    • The code that shows up at (* jgross start here *) should use an identifier like id_with_alt_bounds_and_proof defined as
    Definition id_with_alt_bounds {A} (value : A) (value_for_alt_bounds : A) : A
      := value.
    Definition id_with_alt_bounds_and_proof {A} (value : A) (value_for_alt_bounds : A)
           {pf : value = value_for_alt_bounds}
    := id_with_alt_bounds value value_for_alt_bounds.
    
    • If you unfold id_with_alt_bounds_and_proof, id_with_alt_bounds, then the rest of the file should go through, and should produce reified code that uses Z or TWord 256 or whatever.

    I'll then work on making bounds analysis handle either id_with_alt_bounds or id_with_alt_bounds_and_proof (not sure which, yet, so I figured I'd stick on the safe side and ask for the one with the proof), using value_for_alt_bounds rather than value for computing bounds. Does this sound good to you @jadephilipoom?

    opened by JasonGross 21
  • Define the spec of Weierstrass curves

    Define the spec of Weierstrass curves

    This is the start of work on P256.

    N.B. I've just copy/pasted the equations, and haven't actually yet checked that addition is associative, that it forms a group, etc.

    Questions that should be resolved before this is merged:

    1. [x] Is there a better place for the various tactics I added than src/CompleteWeierstrassCurve/Pre.v (are we trying to minimize dependencies? if not, we can define Util/Tactics.v and put them in there...) 2
    2. [ ] What assumptions do we need to make about a, b, characteristic, etc, for these curves.
    3. [x] Should this be "Weierstrass", "ShortWeierstrass", or something else?
    4. [x] Does my NOT_ON_CURVE kludge need more commenting?
    5. [ ] Is my notation involving reasonable? (Should it be exported somewhere?)
    6. [x] Is the match semantics for onCurve readable for non-Coq-experts, or should we use a different syntax.
    7. [x] Is the boilerplate around add okay, or should I try to get ProgramDefinition` working?
    opened by JasonGross 21
  • Saturated Solinas Reduction

    Saturated Solinas Reduction

    Saturated implementation of Solinas reduction that currently only supports machine_wordsize=64.

    There were multiple places in the template where I had to extract bounds information for proofs. This is accomplished by the if-statement below:

    Definition reduce1 base s c n m (p : list Z) :=
          let p_a := Positional.to_associational weight n p in
          let r_a := sat_reduce base s c n p_a in
          let r_rows := Saturated.Rows.from_associational weight m r_a in
          let r_flat := Saturated.Rows.flatten weight m r_rows in
          let bound := (0, 2^machine_wordsize - 1) in
          if (is_bounded_by (repeat bound n) p) then
            fst r_flat
          else
            add_to_nth 0 (weight (m) * snd r_flat) (fst r_flat).
    

    This change made reification fail when calling reduce1 (and other functions that used a similar trick) inside another if-statement without inlining. Inlining all of these functions causes the code length to dramatically increase, leading to long local build times (~1hr 40m for the reification cache).

    opened by samuel-tian 19
  • Need rewrite rules for new base conversion

    Need rewrite rules for new base conversion

    As discussed in a couple of recent fiat-crypto meetings and #813 (also related to #809), I've been trying to clean up Core.v by removing the enormous nth_default proofs about carry functions. As it stands, the only one being used is nth_default_chained_carries_no_reduce, which is used in base conversion to prove that convert_bases is equivalent to evaluating the input in the source base system and then evenly partitioning it in the destination base system (convert_bases_partitions). Therefore, removing the need for nth_default in that one proof will remove some of the largest and nastiest proofs from the core arithmetic library.

    To that end, in the columns-base-conversion branch, I've written a definition of convert_bases that uses the saturated arithmetic library (Columns.from_associational and Columns.flatten) to convert between bases. It seems to work in my preliminary tests and the proofs pass. However, because the Columns definitions use Z.add_get_carry_full, the output ends up having add-get-carry statements that split at invalid bit indices, e.g.:

    (uint40, uint8) (Z.add_get_carry (2^40) ((uint47) x) ((uint47) y))
    

    Instead, we want an add and then a bitwise div/mod, e.g.:

    dlet xy := (uint48 (Z.add (uint47 x) (uint47 y)) in
    (uint40 (Z.shiftr (uint48 xy) (literal 8)), uint8 (Z.land (uint48 xy) (2^8-1))
    

    I think existing rewrite rules will take care of translating a Z div/mod into a shiftr/land, but I don't know how to write a rule that will do the div/mod translation in the with-casts rules. Especially problematic is figuring out what the range of x + y should be, because it doesn't appear in the initial expression and I think (correct me if I'm wrong) the rewriter won't allow me to write a range in the new expression as an expression (e.g. ZRange.four_corners rx ry).

    I see two main solutions:

    1. Write a rewrite rule that recognizes such add-get-carry statements and changes them into div/mod
    2. Change Columns definitions to use something other than Z.add_get_carry_full when some boolean is set, or parameterize Columns over your desired implementation of div/mod (which we can then plug in as Z.add_get_carry_full for saturated arithmetic and div/mod for base conversion)

    I think 1 is preferable if it's possible. @JasonGross , can you write this rewrite rule? If 1 is not possible, I think I know how to do 2, but would like some feedback on whether introducing this extra abstraction to Columns is reasonable (@andres-erbsen ?). I think the answer kind of hinges on how we want to view Z.add_get_carry_full. Is it a definition that serves as a marker for places where we definitely want to use the carry flag? Or is it a shorthand for "div/mod, figure out if this should use carries based on bounds"?

    opened by jadephilipoom 18
  • Bump rewriter from `5bb7d13` to `de56173`

    Bump rewriter from `5bb7d13` to `de56173`

    Bumps rewriter from 5bb7d13 to de56173.

    Commits
    • de56173 Bump etc/coq-scripts from 153ac32 to efae533 (#89)
    • 3a02179 Merge pull request #88 from JasonGross/test-perf
    • ddb0dc0 Fix step naming on CI
    • 84df3fa Only test perf-Sanity, not perf-SuperFast
    • 58ee840 Make stack overflow less likely
    • 214b0bb Fix thunking
    • 3ad6fc5 Fix de Bruijn index bug in preprocess
    • 26db829 Test perf-SuperFast on CI
    • d9caa32 Bump etc/coq-scripts from 3711598 to 153ac32 (#87)
    • See full diff in compare view

    Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

    Dependabot will merge this PR once CI passes on it, as requested by @JasonGross.


    Dependabot commands and options

    You can trigger Dependabot actions by commenting on this PR:

    • @dependabot rebase will rebase this PR
    • @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
    • @dependabot merge will merge this PR after your CI passes on it
    • @dependabot squash and merge will squash and merge this PR after your CI passes on it
    • @dependabot cancel merge will cancel a previously requested merge and block automerging
    • @dependabot reopen will reopen this PR if it is closed
    • @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
    • @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
    submodules 
    opened by dependabot[bot] 1
  • Bump etc/coq-scripts from `3711598` to `efae533`

    Bump etc/coq-scripts from `3711598` to `efae533`

    Bumps etc/coq-scripts from 3711598 to efae533.

    Commits

    Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

    Dependabot will merge this PR once CI passes on it, as requested by @JasonGross.


    Dependabot commands and options

    You can trigger Dependabot actions by commenting on this PR:

    • @dependabot rebase will rebase this PR
    • @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
    • @dependabot merge will merge this PR after your CI passes on it
    • @dependabot squash and merge will squash and merge this PR after your CI passes on it
    • @dependabot cancel merge will cancel a previously requested merge and block automerging
    • @dependabot reopen will reopen this PR if it is closed
    • @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
    • @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
    submodules 
    opened by dependabot[bot] 1
  • Bedrock/End2End/RupicolaCrypto/Derive.v is too-memory heavy

    Bedrock/End2End/RupicolaCrypto/Derive.v is too-memory heavy

    This is preventing us from being tested on Coq's CI, see https://github.com/coq/coq/pull/16801. Last I checked, it takes about a minute to compile and about 4 GB of RAM (4384020 ko, as of 70f832b7df754b4a41f286a969493a5a9438bdcf). This is up from 20s and about 1GB of RAM (1169688 ko as of 42cace10dde6471b6422ca282c585894dd16978b)

    @andres-erbsen @DIJamner can one of you take care of this?

    opened by JasonGross 4
  • Added dettman multiplication algorithm, made changes to equivalence checker

    Added dettman multiplication algorithm, made changes to equivalence checker

    Two main things that I did here:

    1. Adding the coq implementation of the "dettman multiplication" algorithm.
    2. Changes to the assembly equivalence checker: a. A canonicalization of sums of addcarries, which effectively makes the equivalence checker aware that double-wide (e.g., 128-bit) addition is associative. This is analogous to the preexisting canonicalization of commutative operations, which just sorted the operands. b. A (new, in-some-ways better) implementation of bounds on integer values corresponding to nodes in the dag. Instead of just revealing a few layers of the dag, and using that to bound an expression, I changed the data type of the dag, so that as nodes are inserted into the dag, their bounds are inserted along with the node and its description. The bound on each node can be calculated in terms of the bounds on its operands. So now, the bounds can "look to arbitrary depth", using this dynamic-programming type of strategy.
      c. A new rewriting rule, which replaces or operations with add operations in some cases. When we have a node of the form (orZ, [x; y]), for example, and x is a multiple of 16, and y is upper-bounded by 15, we can rewrite this as (addZ, [x; y]). This uses the bounds that I implemented. d. A new cli optional argument, "--extra-rewrite-rule", which allows optional rewrite rules (which are off by default) to be "turned on" when the equivalence checker is invoked. Currently, the only available optional rewrite rule is the or-to-add rule I mentioned in part (c), which can be turned on by writing "--extra-rewrite-rule or-to-add". It would be easy to add more optional rewrites. I found it necessary to add this option because the or-to-add rule was necessary for some dettman verification, but it was breaking some solinas verification.
    opened by OwenConoly 35
Releases(v0.0.17)
  • v0.0.17(Oct 16, 2022)

    Compatible with Coq 8.15 and 8.16, requires OCaml >= 4.08

    What's Changed

    • Update ensure_stack_limit.sh to be POSIX-compliant and not always unconditionally invoke ulimit by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1438
    • Add some rewrite rules about Z bool comparisons by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1436
    • Use Hint Cut rather than Hint Immediate by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1439

    New Contributors

    • @github-actions made their first contribution in https://github.com/mit-plv/fiat-crypto/pull/1435

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.16...v0.0.17

    Source code(tar.gz)
    Source code(zip)
  • v0.0.16(Oct 14, 2022)

    Compatible with Coq 8.15 and 8.16, requires OCaml >= 4.08

    What's Changed

    • Bump rewriter for more reification performance, including caching reified lemmas via LetIn
      • Bump rewriter to regain Ltac2 reification performance on par with Ltac1 by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1389
      • More Ltac2 Reification performance experiments by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1403
      • Bump rewriter: Don't duplicate reification typechecking time in Qed by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1409
      • More selective correctness proof tactics for PushButtonSynthesis by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1416
      • Bump rewriter for Cache reified lemmas with LetIn by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1413
    • Automatically increase stack size to avoid stack overflows in OCaml compilation of extracted binaries by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1430
      • Add stacksize warnings to avoid confusion by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1407
    • Split out makefiles to allow binary testing without Coq files by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1423
    • Performance improvements in GarageDoor
      • use vm_compute instead of Ltac to check instruction bounds by @samuelgruetter in https://github.com/mit-plv/fiat-crypto/pull/1429
      • More Blind Optmimizations for GarageDoor by @andres-erbsen in https://github.com/mit-plv/fiat-crypto/pull/1431

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.15...v0.0.16

    Source code(tar.gz)
    Source code(zip)
  • v0.0.15(Oct 2, 2022)

    The biggest change of this release is Ltac2 reification and (hopefully) compatibility with Coq 8.15 and 8.16 on Windows. Minimum required versions: Coq 8.15, OCaml 4.08

    What's Changed

    • Port reification to Ltac2 by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1361
    • Garagedoor opens by @andres-erbsen in https://github.com/mit-plv/fiat-crypto/pull/1369
    • Zig backend: bump the comptime branch quota up for cast() calls by @jedisct1 in https://github.com/mit-plv/fiat-crypto/pull/1360
    • Use $$ rather than $ for var so as to not conflict with Ltac2 antiquotations by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1359
    • Makefile fixups by @andres-erbsen in https://github.com/mit-plv/fiat-crypto/pull/1393

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.14...v0.0.15

    Source code(tar.gz)
    Source code(zip)
  • v0.0.14(Aug 27, 2022)

    Likely the last release compatible with Coq 8.11 -- 8.14. Supports Coq 8.11 -- Coq 8.15 (and possibly 8.16)

    What's Changed

    Bedrock2 and Rupicola Pipelines

    • Fe25519 inv merge by @andres-erbsen in https://github.com/mit-plv/fiat-crypto/pull/1154
    • Word-by-word Montgomery with new Bedrock2 Synthesis Pipeline by @RasmusHoldsbjergCSAU in https://github.com/mit-plv/fiat-crypto/pull/1113
    • minor fixes to chacha20 and buf_append by @ashley-lin in https://github.com/mit-plv/fiat-crypto/pull/1255
    • Fix issues in buf_append lemma and its usage, as well as memcpy lemma. by @DIJamner in https://github.com/mit-plv/fiat-crypto/pull/1257
    • rupicola: felem<->bytes conversions by @andres-erbsen in https://github.com/mit-plv/fiat-crypto/pull/1263
    • Add 1-level broadcasting-style array operation compilation and use for poly1305 by @DIJamner in https://github.com/mit-plv/fiat-crypto/pull/1262
    • Add memcpy Rupicola lemma by @DIJamner in https://github.com/mit-plv/fiat-crypto/pull/1224
    • Add with_bedrock2 binaries by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1252

    Code Generators

    • Zig inversion code: compute f and precomp at compile-time by @jedisct1 in https://github.com/mit-plv/fiat-crypto/pull/1275
    • Generate Java files with the expected file names on all platforms by @jedisct1 in https://github.com/mit-plv/fiat-crypto/pull/1260
    • Generate code for the scalar field of standard curves by @jedisct1 in https://github.com/mit-plv/fiat-crypto/pull/1259

    User Messages

    • Display errors messages when synthesis fails by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1286
    • Show casts in comparisons by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1318
    • Display dummy unit arguemnts as ()_... rather than x... by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1317
    • Fix printing of casts in PHOAS output by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1319

    Assembly Equivalence Checker

    • Finish assembly equivalence checker proof by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1178
    • Add more operations to parsing in the equivalence checker: call, cmovb, cmp, db, dd, dq, dw, je, jmp, mul, pop, push, rcr, and shrx, and prefixes like rep ret, repz ret, repnz ret, and labels and align and default rel by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1197
    • Support duplicate functions in multiple --hints-files by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1199
    • Better equivalence-checker error messages by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1193
    • Minor asm improvements by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1209
    • Add support for parsing polynomials by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1213
    • Use poly parsing to support more labels by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1214
    • Error if there are assembly files with no globals by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1216
    • Add some operations to equivalence checker by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1191
    • Fold carry identity dropping into the general identity dropping by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1217
    • fixed annotations on assembly output for assembly-checker by @OwenConoly in https://github.com/mit-plv/fiat-crypto/pull/1357
    • Add pretty-printer for asm error messages by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1219

    Misc Utility Lemmas

    • Add a lemma about filter and Forall by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1177
    • Add some util lemmas and definitions by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1192
    • Add a bunch of iso-based FMap and MSet stuff by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1222
    • Add more structures (towards tries) by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1226
    • Add some more ordered types by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1230
    • Add specialize_all_ways_under_binders_by by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1231
    • Add in_hyp_under_binders_do by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1232
    • Add support for is_true relations in setoid_subst_rel by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1233
    • Add InA_map', the reverse direction of InA_map by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1235
    • Organize and fill out structures and orders by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1234
    • Add FMapSect by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1236
    • Add NoDupA_map_inv' by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1241
    • Rename WIsoSfun to IsoWSfun for slightly more consistency by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1242
    • Add some basic FMap structures by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1239
    • Fix some structures arguments by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1243
    • Add some subrelation instances by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1245
    • Add FMap{Option,Sum} by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1246
    • Add some flat-map lemmas by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1248
    • Add some fold_left lemmas by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1253
    • Use setoid_rewrite in setoid_subst_rel too by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1254
    • Add {NoDupA,SortA}_flat_map by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1256
    • Add FMapProd by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1258
    • Add eq_flat_map_fold_{left,right} by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1261
    • Add some lemmas about fold andb by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1269
    • First stab at FMapTrie by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1266
    • Add some fold higher-order/rev lemmas by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1270
    • Add SortA_rev by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1271
    • Split FMapTrie proofs and definitions for positivity checker by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1273
    • Add Usual{,W}S maps by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1276
    • Fix some structures (missing Orig/Both) by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1264
    • Add some lifts for iso lt types by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1277
    • Remove stupid hints from core db by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1278
    • Fix ListUsualMap by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1279
    • Add FMap{Flip,N,Z} by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1272
    • Rename equal_iff so that we can directly include FMapFacts by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1281
    • Add FMapFacts and make use of common facts by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1282
    • Add examples of Tries for positive, N, Z by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1274
    • Add cardinal_add by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1285
    • Do the heavy-lifting of title-case in GNU Make by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1287
    • [TEMP] Disable FMapTrie functor instantiation by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1288
    • Factor FMapTrie proofs out of the module functor by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1290
    • Remove some pesky FMap hints by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1291
    • Build (but don't yet use) more efficient datastructures for asm dag by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1294
    • Work around coq/coq#7954 by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1297
    • Hide dag behind a (not very strong) interface by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1295
    • Use records in FMap structures by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1307
    • Disable equality schemes for symbolic_state by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1306

    Misc Infrastructure

    • Enable vm_compute on validate with bedrock2 by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1183
    • Adapt w.r.t. coq/coq#15434. by @ppedrot in https://github.com/mit-plv/fiat-crypto/pull/1185
    • Work around new security feature of git by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1194
    • Add support for TIMED=1 in make test-amd64-files by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1196
    • Add support for WITH_PERF=1 to use ocamloptp by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1200
    • Add more parallelism on windows CI by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1204
    • Add PERF_TESTS=1 to call perf record on outputs by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1202
    • Revert commits that don't build on master. by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1221
    • Rename some jobs for clarity by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1223
    • Automatically skip bedrock2 on older versions of Coq by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1238
    • Name the jobs in coq.yml by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1240
    • Suppress masking-absolute-name, make unsupported-attributes a warning by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1247
    • Add Everything.v that requires all files by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1251
    • Only generate files on master PRs by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1267
    • Friendlier GH Actions Queue by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1280
    • Make rupicola depend on bedrock2-compiler as an order-only dependency by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1283
    • Generate .mli files: { => Recursive} Extraction by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1292
    • Adjust warnings in _CoqProject by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1312
    • Adjust more warnings in _CoqProject by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1311
    • Work around COQBUG(https://github.com/coq/coq/issues/16288) by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1316
    • More efficient datastructures for asm dag by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1293
    • Do not compute elements of set as a list in MiscCompilerPasses.subst0n. by @ppedrot in https://github.com/mit-plv/fiat-crypto/pull/1344
    • Adapt w.r.t. coq/coq#16004. by @ppedrot in https://github.com/mit-plv/fiat-crypto/pull/1343
    • Don't leave over a useless let-in in cache_term by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1346
    • Clear unused deps in cache_term for transparent_abstract by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1348

    Submodule Bumping

    • update rupicola/bedrock2/coqutil by @samuelgruetter in https://github.com/mit-plv/fiat-crypto/pull/1228
    • Bump rupicola from 94afa11 to 0b67e4f by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1180
    • Bump coqprime from de0c48a to 12ad864 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1182
    • Bump actions/setup-java from 3.0.0 to 3.1.0 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1184
    • Bump actions/setup-java from 3.1.0 to 3.1.1 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1186
    • Bump haskell/actions from 1 to 2 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1206
    • Bump actions/setup-java from 3.1.1 to 3.2.0 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1218
    • Bump actions/setup-java from 3.2.0 to 3.3.0 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1229
    • Bump etc/coq-scripts from 0ca86bb to 3ad4791 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1268
    • Bump actions/setup-python from 3 to 4 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1289
    • Bump rewriter from f18f187 to 3915f16 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1308
    • Bump etc/coq-scripts from 3ad4791 to d85c149 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1298
    • bump rupicola and adapt to bedrock2 compiler changes by @samuelgruetter in https://github.com/mit-plv/fiat-crypto/pull/1301
    • Bump rewriter from 2c2d78e to f18f187 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1302
    • Bump coqprime from 12ad864 to dc19734 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1303
    • Bump rupicola from 90de960 to 191bc0e by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1304
    • Bump actions/setup-java from 3.3.0 to 3.4.0 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1305
    • Bump etc/coq-scripts from d85c149 to 5116cc9 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1313
    • Bump rewriter from 3915f16 to f3f6bc1 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1314
    • Bump rupicola from 191bc0e to e455547 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1315
    • Bump rupicola from e455547 to e504468 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1320
    • Bump rupicola from e504468 to 34b7686 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1323
    • Bump actions/setup-java from 3.4.0 to 3.4.1 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1324
    • Bump coqprime from dc19734 to f8efa9c by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1327
    • Bump coqprime from f8efa9c to ef3e2f5 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1332
    • Bump rewriter from f3f6bc1 to 474c44b by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1334
    • Bump coqprime from ef3e2f5 to 0f03e44 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1340
    • Bump rupicola from 34b7686 to 3e63c5d by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1345
    • Bump rewriter to split off Reify file by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1349
    • Bump rupicola from 3e63c5d to 7add959 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1352
    • Bump rewriter from 6c69287 to a7e88a2 by @dependabot in https://github.com/mit-plv/fiat-crypto/pull/1356

    New Contributors

    • @RasmusHoldsbjergCSAU made their first contribution in https://github.com/mit-plv/fiat-crypto/pull/1113
    • @ashley-lin made their first contribution in https://github.com/mit-plv/fiat-crypto/pull/1255
    • @OwenConoly made their first contribution in https://github.com/mit-plv/fiat-crypto/pull/1357

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.13...v0.0.14

    Source code(tar.gz)
    Source code(zip)
  • v0.0.13(Mar 29, 2022)

    What's Changed

    • General
      • Add support for SKIP_COQSCRIPTS_INCLUDE=1
    • Experimental Assembly Equivalence Checker:
      • Add reveal_at_least, a more clever form of reveal by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1167
      • Mem extention by @dderjoel in https://github.com/mit-plv/fiat-crypto/pull/1134
      • Rework equivalence checker proofs to be based on remove by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1173

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.12...v0.0.13

    Source code(tar.gz)
    Source code(zip)
  • v0.0.12(Mar 22, 2022)

    What's Changed

    • General:
      • Compatibility with Haskell 9.2.1 by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1048
      • [CLI] Give precedence to the final argument on the command-line by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1097
      • Add encode_word and copy to PushButtonSynthesis by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1103
      • Fixed some performance issues with List.rev l -> List.rev_append l [] by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1106
      • Felem cswap by @DIJamner in https://github.com/mit-plv/fiat-crypto/pull/1128
    • JSON:
      • Add option --emit-all-casts and use it in JSON by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1107
    • C:
      • Inline all functions in C, even in clang by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1165
    • Experimental Assembly Equivalence Checker:
      • Add a pass for turning unary operations into truncations by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1098
      • Add support for checking callee-saved registers by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1096
      • Enable const folding for mul asm by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1127
      • Better explanation of unification error messages by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1136
      • adding shl shlx to mul * imm by @dderjoel in https://github.com/mit-plv/fiat-crypto/pull/1123
      • Parameterize over dereference_scalar in more places by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1161
      • Better equivalence checking errors in the face of bad loads by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1163
      • Mem extension (part 1) by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1166

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.11...v0.0.12

    Source code(tar.gz)
    Source code(zip)
  • v0.0.11(Dec 28, 2021)

    What's Changed

    • concretize and implement sctestbit + partial proof by @andres-erbsen in https://github.com/mit-plv/fiat-crypto/pull/1078
    • Autogenerate fiat-rust/src/lib.rs and expose poly1305 in Rust by @JasonGross in https://github.com/mit-plv/fiat-crypto/pull/1091

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.10...v0.0.11

    Source code(tar.gz)
    Source code(zip)
  • v0.0.10(Dec 13, 2021)

    What's Changed

    • Zig:
      • use @import("builtin") instead of the deprecated reexport
    • Rust:
      • Add conditional no_std to Cargo.toml
      • allow(non_camel_case_types) is now an inner attribute
    • JSON:
      • Fix bitwidths by avoiding rounding
    • Coq:
      • Bump minimum Coq dependency to 8.11
      • Edwards-Montgomery isomorphism proof
    • experimental x86 assembly symbolic equivalence checker

    New Contributors

    • @DIJamner made their first contribution in https://github.com/mit-plv/fiat-crypto/pull/1028
    • @talkon made their first contribution in https://github.com/mit-plv/fiat-crypto/pull/1050
    • @brycx made their first contribution in https://github.com/mit-plv/fiat-crypto/pull/1073

    Full Changelog: https://github.com/mit-plv/fiat-crypto/compare/v0.0.9...v0.0.10

    Source code(tar.gz)
    Source code(zip)
  • v0.0.9(Oct 4, 2021)

    Last tagged release compatible with Coq 8.9, 8.10

    • Adds named typedefs for loose, tight, Montgomery, and non-Montgomery field elements in generated code, as well as a relax method
    • Emits __inline__ via #define only ifdef __GNUC__
    • carry_{add,sub,opp} methods are now included in generated Go code
    • Various adjustments to generated Zig code, including changing of casting and more standard casing
    • Java now uses a slightly different method of casting (#995)
    • Added flags --inline, --inline-internal, --no-field-element-typedefs, --relax-primitive-carry-to-bitwidth, --shiftr-avoid-uint1, --doc-text-before-type-name, --doc-newline-in-typedef-bounds; adjusted default of --asm-stack-size
    Source code(tar.gz)
    Source code(zip)
  • v0.0.8(May 18, 2021)

  • v0.0.7(Apr 28, 2021)

    Last (pre-)release before moving the inversion-c files to a new folder.

    Contains the following changes, among others:

    • Fix a bug in parsing 0x<num1>e<num2>
    • Fix a timing issue in the BY inversion template
    • C Stringification: prepend __extension__ before the typedef with __int128; This allows the generated C code to compile with gcc and -Wpedantic.
    • Adjust style of generated Go code to be more in line with standard Go
    • New Zig backend
    Source code(tar.gz)
    Source code(zip)
  • v0.0.4(May 21, 2020)

  • v0.0.3-beta4(May 13, 2020)

  • v0.0.3-beta3(May 13, 2020)

  • v0.0.3-beta2(May 13, 2020)

  • v0.0.3-beta(May 11, 2020)

  • v0.0.3-alpha(May 11, 2020)

  • v0.0.2-beta(May 2, 2020)

  • v0.0.2-alpha(Apr 29, 2020)

  • v0.0.1-alpha(Feb 4, 2020)

Owner
Programming Languages and Verification Group at MIT CSAIL
Programming Languages and Verification Group at MIT CSAIL
Easy Fiat-Shamirization using Meow

Magikitten A system for making public-coin protocols non-interactive, using Meow. This library is also heavily inspired by Merlin, and provides a simi

Lúcás Meier 11 Nov 10, 2022
Yi Token by Crate Protocol: the primitive for auto-compounding single token staking pools.

yi Yi Token by Crate Protocol: the primitive for auto-compounding single token staking pools. About Yi is a Solana primitive for building single-sided

Crate Protocol 12 Apr 7, 2022
Easy to use cryptographic framework for data protection: secure messaging with forward secrecy and secure data storage. Has unified APIs across 14 platforms.

Themis provides strong, usable cryptography for busy people General purpose cryptographic library for storage and messaging for iOS (Swift, Obj-C), An

Cossack Labs 1.6k Nov 29, 2022
A (mostly) pure-Rust implementation of various cryptographic algorithms.

Rust-Crypto A (mostly) pure-Rust implementation of various common cryptographic algorithms. Rust-Crypto seeks to create practical, auditable, pure-Rus

null 1.2k Nov 24, 2022
Sodium Oxide: Fast cryptographic library for Rust (bindings to libsodium)

sodiumoxide |Crate|Documentation|Gitter| |:---:|:-----------:|:--------:|:-----:|:------:|:----:| |||| NaCl (pronounced "salt") is a new easy-to-use h

sodiumoxide 642 Nov 12, 2022
Collection of cryptographic hash functions written in pure Rust

RustCrypto: hashes Collection of cryptographic hash functions written in pure Rust. All algorithms reside in the separate crates and implemented using

Rust Crypto 1.1k Nov 25, 2022
Modern Cryptographic Firmware

Trussed® Modern Cryptographic Firmware Status Very much WIP. Actively developed. Unstable APIs.

Trussed® 298 Dec 1, 2022
The underlying cryptographic primitives for Manta Ecosystem

manta crypto The underlying cryptography that manta ecosystem relies on. It comes with the following traits: checksum: definitions for message digest.

Manta Network 10 Nov 10, 2021
Secure storage for cryptographic secrets in Rust

secrets secrets is a library to help Rust programmers safely held cryptographic secrets in memory. It is mostly an ergonomic wrapper around the memory

Stephen Touset 163 Oct 31, 2022
Pure Rust implementation of the RNCryptor cryptographic format by Rob Napier

rncryptor Rust Implementation of the RNCryptor spec This library implements the specification for the RNCryptor encrypted file format by Rob Napier. d

null 7 Jun 29, 2022
Pure-Rust traits and utilities for constant-time cryptographic implementations.

subtle Pure-Rust traits and utilities for constant-time cryptographic implementations. It consists of a Choice type, and a collection of traits using

dalek cryptography 193 Oct 27, 2022
Cryptographic signature algorithms: ECDSA, Ed25519

RustCrypto: signatures Support for digital signatures, which provide authentication of data using public-key cryptography. All algorithms reside in th

Rust Crypto 289 Nov 21, 2022
the official Rust and C implementations of the BLAKE3 cryptographic hash function

BLAKE3 is a cryptographic hash function that is: Much faster than MD5, SHA-1, SHA-2, SHA-3, and BLAKE2. Secure, unlike MD5 and SHA-1. And secure again

BLAKE3 team 3.7k Nov 25, 2022
Fastmurmur3 - Fast non-cryptographic hash, with the benchmarks to prove it.

Fastmurmur3 Murmur3 is a fast, non-cryptographic hash function. fastmurmur3 is, in my testing, the fastest implementation of Murmur3. Usage let bytes:

Kurt Wolf 14 Sep 22, 2022
Fuel cryptographic primitives

Fuel Crypto Fuel cryptographic primitives. Compile features std: Unless set, the crate will link to the core-crate instead of the std-crate. More info

Fuel Labs 19 Sep 8, 2022
Dexios-Core is a library used for managing cryptographic functions and headers that adhere to the Dexios format.

What is it? Dexios-Core is a library used for managing cryptographic functions and headers that adhere to the Dexios format. Security Dexios-Core uses

brxken 3 Jul 4, 2022
Common cryptographic library used in software at Mysten Labs.

[fastcrypto] fastcrypto is a common cryptography library used in software at Mysten Labs. It is published as an independent crate to encourage reusabi

Mysten Labs 76 Nov 26, 2022
Next-generation implementation of Ethereum protocol ("client") written in Rust, based on Erigon architecture.

?? Martinez ?? Next-generation implementation of Ethereum protocol ("client") written in Rust, based on Erigon architecture. Why run Martinez? Look at

Arthur·Thomas 23 Jul 3, 2022
Validity is a next-generation, deduction-based language for formally verified, context-aware, autonomous & reactive smart contracts.

Validity Language Validity is a next-generation, deduction-based language for formally verified, context-aware, autonomous & reactive smart contracts.

Tempest Labs 4 Nov 11, 2022