All pull requests

Pull requests

• Dev 2026 10 07 rebased

  #84·abentkamp opened Oct 12, 2026·

  ·

• Cross testing with hax (aeneas side)

  #83·clementblaudeau opened Oct 10, 2026·6/6·

  ·

• fix: check for clashes with pre/post/specs

  #82·clementblaudeau opened Oct 7, 2026·5/6·

  ·

• ci: Check that the latest changes will work with hax

  #81·abentkamp opened Oct 6, 2026·

  ·

• fix: keep supertrait parameters in specs

  #80·clementblaudeau opened Sep 30, 2026·4/6·

  ·

• fix: keep unit argument for specs instead of dropping them

  #79·clementblaudeau opened Sep 30, 2026·3/6·

  ·

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

  #77·clementblaudeau opened Sep 30, 2026·2/6·

  ·

• refactor: remove the step backend for proof-obligations generation

  #76·clementblaudeau opened Sep 23, 2026·1/6·

  ·

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

  #73·karthikbhargavan opened Sep 7, 2026·

  ·

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

  #72·karthikbhargavan opened Sep 7, 2026·

  ·

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

  #71·karthikbhargavan opened Sep 7, 2026·

  ·

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

  #70·karthikbhargavan opened Sep 6, 2026·

  ·

• Translate dynamic-trait types in signatures (upstream)

  #69·karthikbhargavan opened Sep 5, 2026·

  ·

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

  #68·karthikbhargavan opened Sep 5, 2026·

  ·

• Represent enum discriminants as big integers (upstream)

  #67·karthikbhargavan opened Sep 4, 2026·

  ·

• Merge upstream/main into dev (sync through f9a8e3381)

  #66·karthikbhargavan opened Sep 4, 2026·

  ·

• Add a fuzzer for hax/aeneas

  #41·karthikbhargavan opened Aug 9, 2026·

  ·

• Vcgen

  #39·abentkamp opened Aug 6, 2026·

  ·

• Update Lean to v4.33.0-rc2

  #34·abentkamp opened Aug 4, 2026·

  ·
  11

• interp: fix inverted can_end guard in eliminate_shared_loans

  #27·karthikbhargavan opened Jul 25, 2026·

  ·
  1

  1

• pure: harden simplify_let_branching against hoisting branch-local variables

  #26·karthikbhargavan opened Jul 25, 2026·

  ·
  1

• pure/loops: skip output reordering when the ok-tuple is not a permutation of the loop outputs

  #25·karthikbhargavan opened Jul 25, 2026·

  ·
  1

• feat(specs): add a [-proof-manifest] flag, emit a .json

  #8·clementblaudeau opened Jun 16, 2026·

  ·