mit-plv/fiat-crypto v0.0.14

Fiat Cryptography v0.0.14

on GitHub

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 #1154
• Word-by-word Montgomery with new Bedrock2 Synthesis Pipeline by @RasmusHoldsbjergCSAU in #1113
• minor fixes to chacha20 and buf_append by @ashley-lin in #1255
• Fix issues in buf_append lemma and its usage, as well as memcpy lemma. by @DIJamner in #1257
• rupicola: felem<->bytes conversions by @andres-erbsen in #1263
• Add 1-level broadcasting-style array operation compilation and use for poly1305 by @DIJamner in #1262
• Add memcpy Rupicola lemma by @DIJamner in #1224
• Add with_bedrock2 binaries by @JasonGross in #1252

Code Generators

• Zig inversion code: compute f and precomp at compile-time by @jedisct1 in #1275
• Generate Java files with the expected file names on all platforms by @jedisct1 in #1260
• Generate code for the scalar field of standard curves by @jedisct1 in #1259

User Messages

• Display errors messages when synthesis fails by @JasonGross in #1286
• Show casts in comparisons by @JasonGross in #1318
• Display dummy unit arguemnts as ()_... rather than x... by @JasonGross in #1317
• Fix printing of casts in PHOAS output by @JasonGross in #1319

Assembly Equivalence Checker

• Finish assembly equivalence checker proof by @JasonGross in #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 #1197
• Support duplicate functions in multiple --hints-files by @JasonGross in #1199
• Better equivalence-checker error messages by @JasonGross in #1193
• Minor asm improvements by @JasonGross in #1209
• Add support for parsing polynomials by @JasonGross in #1213
• Use poly parsing to support more labels by @JasonGross in #1214
• Error if there are assembly files with no globals by @JasonGross in #1216
• Add some operations to equivalence checker by @JasonGross in #1191
• Fold carry identity dropping into the general identity dropping by @JasonGross in #1217
• fixed annotations on assembly output for assembly-checker by @OwenConoly in #1357
• Add pretty-printer for asm error messages by @JasonGross in #1219

Misc Utility Lemmas

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

Misc Infrastructure

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

Submodule Bumping

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

New Contributors

• @RasmusHoldsbjergCSAU made their first contribution in #1113
• @ashley-lin made their first contribution in #1255
• @OwenConoly made their first contribution in #1357

Full Changelog: v0.0.13...v0.0.14