In July, we merged 33 PRs! 🎉
On the side of the frontend, Nadrieril
and I worked at making hax handling of binders (e.g. 'a in for<'a> &'a T: PartialEq<i32>) and traits better. This is not finished yet,
but we made great progress. Our goal is to make the frontend work on
every valid Rust code.
In the engine, thanks to paulmure, we
now are able to process unsafe blocks. Thanks to
maximebuyse, the engine can now
rewrite more return expressions: we are now planning on supporting
return inside loops, along with break and continue.
We’ve been improving F* support and F* libraries. Importantly,
cmester0 is working on a model of
core, in Rust: we aim at replacing our hand-crafted F* model of core
by an hax extraction of this new core model implemented in Rust. We
will also be able to extract this model of core in every of our
backends, enabling a uniform and pain-free core multi-backend
library.
Merged Pull Requests
- #934: chore: assign an issue id for every error in the engine
- #932: chore: assign an issue for every error in
import_thir - #919: fix #422
- #918: chore: remove stale
Hax.Lib.fst - #917: doc: disambiguate_local_idents
- #916: update Cargo.lock
- #909: Revert “fix(engine/fstar): fix super typeclasses attributes”
- #908: fix(engine/deps): stop re-computing over and over the set of assoc items
- #907: Add RewriteControlFlow phase.
- #906: Cleanup trait resolution
- #902: fix(engine/fstar): fix super typeclasses attributes
- #901: Determine emuerate value by index
- #898: Fix some binder-related crashes
- #895: Don’t eval constants eagerly
- #894: Detangle trait solving from
SInto - #892: Support other variants of MIR
- #891: fix: fstar: default trait
- #887: Initial cleanup of binders-related code
- #885: docs(book): depend on
hax-libonly when using hax - #884: Fix incorrect line numbers in error messages
- #883: Fix step boundaries in fold_range_step_by
- #882: fix(fstar-core): add support for
Option::map - #880: Support float literals
- #877: Avoid recursing twice on the arguments.
- #876: Translate additional unsafe MIR operations
- #873: Small PR to fix circularity in Core.Fmt.fsti
- #872: Pre post impl blocks
- #870: count-ones post-condition
- #868: engine: kill a few
exnto get useful errors - #867: Backend: Import unsafe code as a gated feature
- #860: fix(engine): make dep. analysis sensible to UID assoc. items
- #827: Add infos impl
- #819: Add Rust Core Fstar Definitions.