Release 2025.03

What's Changed

Tactics

• Extend clear tactic to allow clearing all unused items in the context recursively by @oskgo in #713
• Improvements to module tweaks by @Cameron-Low in #728
• Reworked outline tactic by @Cameron-Low in #727
• New vernacular command: theory aliases by @strub in #685

Standard library

• Disambiguate precedence in negbLR and negbRL and add new lemmas for left and right distributivity by @oskgo in #737
• Multisets by @oskgo in #722
• reduce number of axioms in Logic by @oskgo in #751
• Add list lemmas and shorten some other proofs using them by @MM45 in #721
• stdlib: in Field, do not erase the unit predicate by @strub in #757

Bug fixes

• Pretty printer: print terminator after module types by @ruipedro16 in #723
• Fix return of properties with provided bit in KEM/PKE libraries by @MM45 in #738
• Fix HC collisions. by @strub in #739
• Minor fixes for sim by @Cameron-Low in #743
• Hi-level error message when subst fails by @strub in #734
• Hi-level error message in clone (axiom <-) by @strub in #748
• fix tactic ehoare-if by @bgregoir in #754

Internals

• [internal] introduce general code position ranges for selecting code blocks. by @Cameron-Low in #709
• remove duplicated code from EcAst by @strub in #731

Chores

• CI: update image from ubuntu-20.04 to ubuntu-24.04 by @strub in #736

New Contributors

• @ruipedro16 made their first contribution in #723

Full Changelog: r2025.02...r2025.03

Release 2025.02

Release 2025.02

What's Changed

• internal: stable ordering of globals components by @strub in #612
• internals: user-defined rules can be headed by a projection by @strub in #616
• cloning: do not allow realizing a non-axiomatic lemma by @strub in #618
• runtest: lint code + fix warnings by @strub in #619
• user reduction: fix some incompleteness issues by @strub in #623
• ci: compile with warning as errors by @strub in #627
• runtest: properly restore the terminal on (exceptional) exit by @strub in #620
• pretty-printer/parser: improve reparsability of the pretty-printer output by @strub in #622
• make runtest fail reasonably on bad config filename by @fdupress in #643
• split SmtMap into SMT Array and finite map by @fdupress in #605
• Fix set_set_swap statement and proof. by @MM45 in #651
• proc rewrite now supports the /= rule by @strub in #648
• Propagate extended code positions to more tactics by @strub in #649
• The tactic swap now takes generalized code position. by @strub in #650
• no user defined rule in op comparison by @strub in #653
• New tactic to alias a subexpression of an instruction by @strub in #647
• lexer: do not lex decimal numbers when the parser won't accept them by @strub in #655
• unroll for: constant-propagate the counter by @strub in #656
• fix "unroll for" failure (InvalidCPos) by @strub in #657
• Fix deep code positions parsing by @strub in #658
• Improve code positions (match + extended assignments) by @Cameron-Low in #654
• Fix include-path management regarding duplicate paths by @strub in #663
• add alt-ergo 2.6 to the docker image by @fdupress in #662
• Track more precisely tuple to tuple assignments in sim by @cassiersg in #667
• Fixing code blocks display in readme by @aubertc in #673
• Merge typing of expressions and formulas by @strub in #671
• Some basic facts on polynomials + fix theory cloning by @strub in #679
• Tactic split with break position by @lyonel2017 in #675
• get rid of axiomatized by in favor of [opaque] with trivial lemma by @oskgo in #681
• Better operators overloading inference by @strub in #665
• PP: various fixes by @strub in #664
• Fine Grained Module Definitions by @Cameron-Low in #661
• Exposed the tp_nothing typolicy of EcTyping by @alleystoughton in #684
• More results on floor/ceil (isint) by @strub in #678
• Service commit (docker / nix / dune) by @strub in #686
• Service commit (expain flag for menhir) by @strub in #687
• runtest: ignore Emacs lock files (.#XXX) by @strub in #688
• Better printing of hint DBs by @strub in #689
• Rigid unification option for hint solve/exact by @strub in #680
• FMap: add lemmas on range after update by @fdupress in #690
• Add PKE libraries (both standard model and ROM) by @MM45 in #677
• KEM libraries (non-ROM and ROM) by @MM45 in #672
• Upgrade to why3 1.8 by @strub in #674
• [external CI] use dev branch for XSalsa checks by @fdupress in #693
• Improve transitivity* and replace* by @Cameron-Low in #692
• Apply cloning substitution to datatype ctor types by @strub in #695
• nix: add a dependency to git so that dune-site works correctly by @strub in #706
• In matching, forbid the capture of all variables by @strub in #708
• New code-position variants: ^()<-, and ^(x)<- to match tuples. by @Cameron-Low in #707
• revert subtype theory + syntactic sugar for cloning it by @strub in #691

New Contributors

• @cassiersg made their first contribution in #667
• @aubertc made their first contribution in #673

Full Changelog: r2024.09...r2025.02

Release 2024.09

Release 2024.09

Release 2024.01

r2024.01

Release 2024.01

Release 2023.09

r2023.09

Release 2023.09

Release 2022.04

First EasyCrypt stable release.