Repository navigation

All pull requests

Labels (17)Milestones (0)New pull request

Open

(27)

Closed

(46)

Dev 2026 11 02 rebased
#96clementblaudeau opened Nov 3, 2026Collaborator
ci: check that every commit belongs to a documented fork patch
#95clementblaudeau opened Nov 2, 2026Collaborator
fix: only skip the crates CoreModels provides under -core-models-lib
#93r-near opened Oct 28, 2026
1
fix: treat the region of Formatter as immutable under -core-models-lib
#90maximebuyse opened Oct 22, 2026
feat: trait-level specs
#85clementblaudeau opened Oct 14, 2026Collaborator
test: cross testing with hax (aeneas side)
#83clementblaudeau opened Oct 10, 2026Collaborator
fix: check for clashes with pre/post/specs
#82clementblaudeau opened Oct 7, 2026Collaborator
ci: Check that the latest changes will work with hax
#81abentkamp opened Oct 6, 2026
fix: keep supertrait parameters in specs
#80clementblaudeau opened Sep 30, 2026Collaborator
fix: keep unit argument for specs instead of dropping them
#79clementblaudeau opened Sep 30, 2026Collaborator
fix: [core-models-lib] keep type parameters that are not Allocator
#77clementblaudeau opened Sep 30, 2026Collaborator
refactor: remove the step backend for proof-obligations generation
#76clementblaudeau opened Sep 23, 2026Collaborator
3
extract: emit opaque trait-impl instances as axioms instead of { sorry }
#73karthikbhargavan opened Sep 7, 2026
symbolic: erase untranslatable type sub-terms to an opaque placeholder
#72karthikbhargavan opened Sep 7, 2026
translate: emit an opaque stub when a function body fails to translate
#71karthikbhargavan opened Sep 7, 2026
interp: don't stash a dummy for a borrow-free overwritten place (cryspen/aeneas)
#70karthikbhargavan opened Sep 6, 2026
Translate dynamic-trait types in signatures (upstream)
#69karthikbhargavan opened Sep 5, 2026
Contain whole-crate aborts: route lookups through catchable errors (cryspen/aeneas)
#68karthikbhargavan opened Sep 5, 2026
Represent enum discriminants as big integers (upstream)
#67karthikbhargavan opened Sep 4, 2026
Merge upstream/main into dev (sync through f9a8e3381)
#66karthikbhargavan opened Sep 4, 2026
Add a fuzzer for hax/aeneas
#41karthikbhargavan opened Aug 9, 2026
Vcgen
#39abentkamp opened Aug 6, 2026
Update Lean to v4.33.0-rc2
#34abentkamp opened Aug 4, 2026
11
interp: fix inverted can_end guard in eliminate_shared_loans
#27karthikbhargavan opened Jul 25, 2026
1
pure: harden simplify_let_branching against hoisting branch-local variables
#26karthikbhargavan opened Jul 25, 2026

Navigation Menu

Repository navigation

All pull requests

Dev 2026 11 02 rebased

ci: check that every commit belongs to a documented fork patch

fix: only skip the crates CoreModels provides under -core-models-lib

fix: treat the region of `Formatter` as immutable under `-core-models-lib`

feat: trait-level specs

test: cross testing with hax (aeneas side)

fix: check for clashes with pre/post/specs

ci: Check that the latest changes will work with hax

fix: keep supertrait parameters in specs

fix: keep unit argument for specs instead of dropping them

fix: [core-models-lib] keep type parameters that are not Allocator

refactor: remove the step backend for proof-obligations generation

extract: emit opaque trait-impl instances as axioms instead of { sorry }

symbolic: erase untranslatable type sub-terms to an opaque placeholder

translate: emit an opaque stub when a function body fails to translate

interp: don't stash a dummy for a borrow-free overwritten place (cryspen/aeneas)

Translate dynamic-trait types in signatures (upstream)

Contain whole-crate aborts: route lookups through catchable errors (cryspen/aeneas)

Represent enum discriminants as big integers (upstream)

Merge upstream/main into dev (sync through f9a8e3381)

Add a fuzzer for hax/aeneas

Vcgen

Update Lean to v4.33.0-rc2

interp: fix inverted can_end guard in eliminate_shared_loans

pure: harden simplify_let_branching against hoisting branch-local variables

Pull requests