v0.0.8

Commits: v0.0.7...v0.0.8

v0.0.7

sketch wp_read_RDH

v0.0.5

For Coq platform 8.17 beta.

Bedrock2 v0.0.4

A pre-release tag for use with Fiat Cryptography v0.0.16 and a non-dev opam package.

What's Changed (Partial List)

• use vm_compute instead of Ltac to check instruction bounds
• Pass -native-compiler ondemand for bedrock2 ex by @JasonGross in #283
• trying to merge egraph-less parts from egraphs branch by @samuelgruetter in #284

Full Changelog: v0.0.3...v0.0.4

Bedrock2 v0.0.3

A pre-release tag for use with Fiat Cryptography v0.0.15 and a non-dev opam package.

What's Changed

• make bedrock2_install now installs examples by @JasonGross in #281

Full Changelog: v0.0.2...v0.0.3

Bedrock2 v0.0.2

A pre-release tag for use with Fiat Cryptography v0.0.15 and a non-dev opam package.

What's Changed

• add in-memory uint128 add for 32-bit by @andres-erbsen in #240
• try out SepCalls in lightbulb.v by @andres-erbsen in #244
• Add support for metrics in the FlatToRiscvFunctions and FlattenExpr passes by @pratapsingh1729 in #246
• Adapt w.r.t. coq/coq#16004 by @Alizter in #250
• Name Coq builds so they are more stable across updates by @JasonGross in #258
• Fix probable typo introduced in bcd4bcf by @JasonGross in #265
• Faster ensure_free by @JasonGross in #267
• Memmove by @andres-erbsen in #275
• add memequal, memswap, memconst by @andres-erbsen in #277
• Python instead of sed by @andres-erbsen in #276
• Add CI tests for Windows and Mac by @JasonGross in #272
• speed up WeakestPreconditionProofs by @andres-erbsen in #280

New Contributors

• @pratapsingh1729 made their first contribution in #246
• @Alizter made their first contribution in #250

Full Changelog: v0.0.1...v0.0.2

Bedrock2 v0.0.1

A pre-release tag for use with Fiat Cryptography v0.0.12 and a non-dev opam package.