Release 2026.02

What's Changed

• Fix a regression in ecall from #789 by @oskgo in #833
• Emit type check error when argument to sided rnd is present but unused by @oskgo in #832
• fix outline error printing by @oskgo in #839
• Inlined documentation by @strub in #783
• fix handling of bounds in conseq equiv phoare by @oskgo in #837
• Manually handle some cases where t_mytrivial is too weak by @oskgo in #848
• reduce when needed in proc and call rules by @bgregoir in #849
• Make casts from existing single sided formulas to two sided ones use a more robust pattern by @oskgo in #851
• Remove dead-code in theory cloning code. by @strub in #853
• Kill warnings + unify flags for ci/dev dune environments by @strub in #852
• Also swap memory types when swapping memories by @oskgo in #856
• In matching, do not unify a memory with itself by @strub in #857
• Improve error message in top-assumption rewrite by @strub in #858
• When doing section-analysis, recurse in operators body by @strub in #860
• When doing section-analysis, recurse in types body by @strub in #866
• Fix dependency analysis by @strub in #862
• Build: unify release/dev warnings flags by @strub in #867
• [docker] update dockerfiles, add formosa docker by @fdupress in #840
• [eco]: add a compilation trace (messages + goals) by @strub in #559
• Fixing the free memory of the second goal of byehoare by @namasikanam in #869
• New lazy/eager logic. by @loutr in #787
• Refman skeleton. by @strub in #868
• CI (doc): not cancellable by @strub in #874
• Positivity check in type constructors by @loutr in #811
• fix alpha-conversion problems in ehoare by @bgregoir in #872
• Revert typeclass additions by @Gustavo2622 in #876
• Allow substitutions of locals using the same memory as that used by a Pr by @oskgo in #870
• [documentation]: document if by @strub in #875
• [seq]: remove bck/fwd option + cleanup by @strub in #878
• proofnav: improve EasyCrypt error handling in Sphinx extension by @strub in #882
• ecproofs: add caching and script export for proof directives by @strub in #883
• [documentation]: document the splitwhile tactic by @strub in #881
• documentation: Sphinx: change default role to code:easycrypt by @strub in #886
• [Internal] Make |- and -| compose in different orders by @oskgo in #885
• Build docker images in CI by @fdupress in #842
• [documentation]: tactic swap by @strub in #889

Full Changelog: r2025.11...r2026.02

Release 2025.11

What's Changed

• Making program logic formulas memory-agnostic by @oskgo in #789
• Expose memory binding(s) in program logic statements by @oskgo in #816
• address TODOs from memory softcoding PR by @oskgo in #817
• Fix some regressions from PR #789 by @oskgo in #820
• Removing spurious print statements in theories by @loutr in #822
• Feature: Adding statement level proc change by @Gustavo2622 in #823
• Add lemmas for list count and perm_eq by @cassiersg in #824
• Fix comparison of fixpoints by @strub in #826
• Ident printing fixes by @Gustavo2622 in #828
• Proc change multiline to range + deep code position by @Gustavo2622 in #831
• Library for keyed-hash functions by @MM45 in #809
• Library for tweakable hash functions by @MM45 in #810
• recover UC example by @mbbarbosa in #821

New Contributors

• @mbbarbosa made their first contribution in #821

Full Changelog: r2025.10...r2025.11

Release 2025.10

What's Changed

• add Reflection theory by @oskgo in #794
• List: new lemmas: nth0, nth1, map1, head_drop by @namasikanam in #796
• [tactic] Single sided match should work for arbitrary pre-conditions by @Cameron-Low in #795
• [tactic] Actually improve one-sided match robustness by @Cameron-Low in #800
• Rework import mechanism by @strub in #683
• extend results on ceil 'for free' by @fdupress in #781
• depext -> confirm level = unsafe-yes by @strub in #798
• remove alt-ergo from EasyCrypt TCB by @fdupress in #724
• EcRegexp: PCRE -> PCRE2 by @strub in #797
• Introduce a system-wide, parts-oriented configuration file by @strub in #801
• OCaml 5 memory blowup workaround by @strub in #802
• Rework stdlib clones. by @strub in #694
• Give a proof to witness_support by @fdupress in #803
• add mu_has_le in rewrite Pr by @bgregoir in #804
• List: new lemmas: subseq_catR, subseq_catL, subseq_consI, subseq_take, subseq_drop, subseq_drop_congr by @namasikanam in #807
• Exit --help with non-error status by @MM45 in #808
• New result: List.sorted_range by @strub in #815
• More results on List.zip by @strub in #813
• More results on BitEncoding.int2bs by @strub in #814

New Contributors

• @namasikanam made their first contribution in #796

Full Changelog: r2025.08...r2025.10

Release 2025.08

What's Changed

• Keyword global for cloning theories by @loutr in #764
• Fix unexpected failure of byupto by @bgregoir in #766
• fix async while rule by @bgregoir in #776
• [Theories, SplitRO] remove requirement of axiom ofpairK by @loutr in #773
• Update README by @MM45 in #778
• Fix #761: Sim deadcode conditions not strong enough. by @Cameron-Low in #780
• Type annotated getters/setters by @strub in #730
• Fix bug in SMT translation (abstraction of non-translatable constructions) by @strub in #782
• Fix indentation TOC by @MM45 in #784
• fixes bug #785, add check that bad is only set to true once set by @bgregoir in #786
• New lemma mu1_le_eq_mu1 for Pr-rewrite. by @loutr in #788
• Add lemma Array.map_comp by @vbgl in #790
• [tactic] Fix type unification in outline by @Cameron-Low in #791
• Add tactic for lossless while by @lyonel2017 in #669

New Contributors

• @loutr made their first contribution in #764

Full Changelog: r2025.03...r2025.08

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.