EasyCrypt has adopted a rolling release strategy, with updates every six weeks, starting with the r2025.02 release.

What’s Changed

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

New Contributors

  • @cassiersg made their first contribution in https://github.com/EasyCrypt/easycrypt/pull/667
  • @aubertc made their first contribution in https://github.com/EasyCrypt/easycrypt/pull/673

Full Changelog: https://github.com/EasyCrypt/easycrypt/compare/r2024.09…r2025.02