Fiat Cryptography v0.0.14

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 ...

Fiat Cryptography v0.0.13

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 #1167
  • Mem extention by @dderjoel in #1134
  • Rework equivalence checker proofs to be based on remove by @JasonGross in #1173

Full Changelog: v0.0.12...v0.0.13

Fiat Cryptography v0.0.12

What's Changed

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

Full Changelog: v0.0.11...v0.0.12

Fiat Cryptography v0.0.11

What's Changed

• concretize and implement sctestbit + partial proof by @andres-erbsen in #1078
• Autogenerate fiat-rust/src/lib.rs and expose poly1305 in Rust by @JasonGross in #1091

Full Changelog: v0.0.10...v0.0.11

Fiat Cryptography v0.0.10

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 #1028
• @talkon made their first contribution in #1050
• @brycx made their first contribution in #1073

Full Changelog: v0.0.9...v0.0.10

Fiat Cryptography v0.0.9

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

Fiat Cryptography v0.0.8

Minor improvements in generated comments.
Moved inversion files to a new folder.

Fiat Cryptography v0.0.7

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

Fiat Cryptography v0.0.6

Regenerate bedrock2 files

Fiat Cryptography v0.0.5

Regenerate bedrock2 files