9 Pull requests merged by 5 people

• Add invariants for while loops.

  #1375 merged Apr 24, 2025

• Add arg_count to MIR bodies

  #1417 merged Apr 23, 2025

• Fix dependencies bounded integers

  #808 merged Apr 23, 2025

• Use ConstantExprKind::Todo more

  #1414 merged Apr 23, 2025

• fix(proof-libs): give a computable definition to >>

  #1415 merged Apr 23, 2025

• fix(engine) Fix name clashes for functions defined in impl methods.

  #1416 merged Apr 23, 2025

• feat(fstar/proof-libs): add a lemma for simplifying double casts

  #1408 merged Apr 23, 2025

• Typeclass forBitAnd; Instantiations for Prims.bool

  #1410 merged Apr 23, 2025

• feat(justfile): just expand: always use nightly

  #1413 merged Apr 22, 2025

1 Pull request opened by 1 person

• Add a fake `DefId` for promoted constants

  #1420 opened Apr 25, 2025

5 Issues closed by 2 people

• Replace implementations for auto. derived impl `Clone`, `Debug` (& more?)

  #108 closed Apr 24, 2025

• Monomorphize `unsize`

  #566 closed Apr 24, 2025

• Engine: refactor the module `ast_utils`

  #599 closed Apr 24, 2025

• Error with `hax_lib::fstar::before` on impl method

  #1315 closed Apr 24, 2025

• Name clash with `panic`s in two implementations of the same trait.

  #1411 closed Apr 23, 2025

2 Issues opened by 1 person

• Add hash-consing for `DefId`s

  #1419 opened Apr 24, 2025

• Add example phase and example backend

  #1418 opened Apr 24, 2025

10 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Generate axioms for items with `Erased` attribute in the coq backend

  #1185 commented on Apr 24, 2025 • 0 new comments

• [ProVerif] Translate generic types

  #1314 commented on Apr 24, 2025 • 0 new comments

• Support impl Trait in attribute name interpolation

  #1313 commented on Apr 24, 2025 • 0 new comments

• Trait resolution crash on coinductive goal

  #1310 commented on Apr 24, 2025 • 0 new comments

• Engine: F*: stop relying on F* builtin equality

  #1160 commented on Apr 24, 2025 • 0 new comments

• Organise Helper/Macro libraries

  #408 commented on Apr 24, 2025 • 0 new comments

• Attributes: introduce them in engine's AST

  #49 commented on Apr 24, 2025 • 0 new comments

• Coq small fixes

  #1108 commented on Apr 23, 2025 • 0 new comments

• Start transitioning annotated core numbers

  #1143 commented on Apr 24, 2025 • 0 new comments

• feat(lib) New sandwich core changes

  #1192 commented on Apr 24, 2025 • 0 new comments