v2024.10.23

What's Changed

• Moving FStar.Getopt -> FStarC.Getopt by @mtzguido in #148
• Update ASN1.Spec.Interpreter.fst with converters in ASN1.Base.fst by @Black-Kamous in #147
• ASN1* : Provably Correct Non-Malleable Parsing for ASN.1 DER by @FVRobbin in #66
• 3D: optimize total compile-time constant-size pairs without actions by @tahina-pro in #152
• also simplify compile-time constant-sized lists in pairs by @tahina-pro in #153
• Optimize validation of arrays by @nikswamy in #151
• A few miscellaneous fixes to 3D by @nikswamy in #154

New Contributors

• @Black-Kamous made their first contribution in #147
• @FVRobbin made their first contribution in #66

Full Changelog: v2024.08.23...v2024.10.23

v2024.08.23

What's Changed

• Generate 3d probe-and-validate wrapper functions by @tahina-pro in #129
• Adding offsetof checks as static assertions when refining a C type by @nikswamy in #144

Full Changelog: v2024.08.09...v2024.08.23

v2024.08.09

What's Changed

• LowParse.Low.Int32le: add assert by @mtzguido in #119
• Produce and upload a Windows binary package by @tahina-pro in #120
• GenMakefile: copy EverParse.h by @tahina-pro in #121
• Avoid local variable shadowing in generated C code by @tahina-pro in #122
• Fix warnings and documentation for "at-most" constructs by @tahina-pro in #128
• Assorted build fixes. by @gebner in #123
• Total Length is the length of the datagram, measured in octets, including internet header and data. by @lemmy in #131
• PayloadLength = 0 => NextHeader \in {0, 59} by @lemmy in #132
• Add constraint for UDP's length field by @lemmy in #134
• LowParse.Low.Sum: bump rlimit by @mtzguido in #139
• Allow external functions returning values by @tahina-pro in #140
• Z3TestGen fixes: negative test cases, handle outparameters in test executables by @tahina-pro in #141
• 3d: weaken allow_reading for entrypoints by @tahina-pro in #142

New Contributors

• @gebner made their first contribution in #123

Full Changelog: v2023.12.08...v2024.08.09

v2023.12.08

What's Changed

• lowparse: rlimit tweaks for new F* by @mtzguido in #99
• Improving a proof in InputStream.Extern by @aseemr in #100
• Test case generation for 3d by @tahina-pro in #101
• Define KRML_HOST_IGNORE to mark unused arguments by @tahina-pro in #102
• KRML_HOST_IGNORE -> KRML_MAYBE_UNUSED_VAR in EverParseEndianness*.h by @tahina-pro in #104
• Two bug fixes by @nikswamy in #109
• Generate test checker executable by @tahina-pro in #106
• EverParse3d.InputStream.Extern.fst: fix proof regression by @mtzguido in #114
• fix the Extern.peep proof once and for all by @tahina-pro in #115
• Fixes #103 by @lemmy in #113
• VxLAN packets are two octets short. by @lemmy in #112
• 3d: allow fields that consume all input by @tahina-pro in #116
• EverParse3d.InputStream.Base: do not use typeclasses for extra_t by @mtzguido in #117
• Add branch exploration for Z3 test case generation by @tahina-pro in #111
• Support for validating pointer-rich formats given a probe to check for pointer validity by @nikswamy in #118

New Contributors

• @lemmy made their first contribution in #113

Full Changelog: v2023.05.03...v2023.12.08

v2023.05.03

What's Changed

• Output types: ExternalAPI, ExternalTypes, and Makefile generation by @tahina-pro in #90
• F*+dune: new F* library layout, improved handling of FSTAR_HOME by @tahina-pro in #92
• Remove effect-based writers by @tahina-pro in #93
• EverParse3d.InputStream.Extern.fst: proof maintenance by @mtzguido in #94
• Update usage of --split_queries by @mtzguido in #96
• getopt: remove use of FStar.BaseTypes by @mtzguido in #97
• EverParse3d: Prelude: update for FStarLang/FStar#2892 by @mtzguido in #98
• Clarify bitfields in LowParse and 3d; BE bitfields now MSB-first by @tahina-pro in #95

Full Changelog: v2023.02.08...v2023.05.03

v2023.02.08

Full Changelog: v2023.01.23...v2023.02.08

v2023.01.23

Full Changelog: v2023.01.14...v2023.01.23

v2023.01.14

What's Changed

• Some changes related to the F* core typechecker by @aseemr in #88
• Adapting lowparse writers effect for F* PR 2760 by @aseemr in #89

Full Changelog: v2022.11.09...v2023.01.14

v2022.11.09

Release v2022.11.09

v2022.06.13

Release v2022.06.13