Release 2026.03

What's Changed

• Make abstract phoare proc use a >= 1 by @oskgo in #887
• document the proc tactic by @oskgo in #884
• [external-ci] use formosa-xmss security proof by @fdupress in #893
• Exposed in the API for EcScope.Theory functions for manually beginning and finishing requires by @alleystoughton in #896
• Fix spurious line breaks in pretty-printing of qualified module paths by @JNC4 in #898
• document clear tactic by @oskgo in #895
• document proc* by @oskgo in #894
• Internal: correctly preserve match statements when constructing a zipper by @Cameron-Low in #899
• Eager: match on last statement and use EqTest by @Cameron-Low in #900
• Tactic: add hoare split by @strub in #888
• In clone, allow applying renamings pre-emptively by @strub in #903
• In hidden theories, remove all hints by @strub in #904
• Fix issue #905, improve error message on missing two sided memory by @Gustavo2622 in #906
• Fix printing of hypothesis about abstract statements by @Gustavo2622 in #910
• feat(unroll-for): propagate constants after unrolling by @strub in #909
• [docker]: bump provers versions by @strub in #911
• [ci] use the main build box in CI by @fdupress in #913
• [runtest] fail when a dir fails to match by @fdupress in #912
• PR: Allow symbolic assignments for cfold by @Gustavo2622 in #892
• documentation for rnd by @mbbarbosa in #890
• [parser]: support for hex literals by @strub in #919
• Add proper error message on digest mismatch in require by @Gustavo2622 in #915
• Feature exception by @lyonel2017 in #806
• Added lemmas proving consequences of a list concatenation being []. by @alleystoughton in #924
• Add check to prevent swapping of exception raises by @lyonel2017 in #927
• Allow memory preserving destruction of formulas to yield distinct types by @oskgo in #933
• Fixing two issues with the pretty printing of operators that are not applied to arguments by @alleystoughton in #929
• check for memory independence of list in rewrite Pr[mu_has_le] by @oskgo in #932
• Fix English grammar in matching error messages. by @alleystoughton in #936
• Rewriting in the pre-condition of PL logics by @strub in #940
• Fix upper bound on non-strict while by @oskgo in #941
• New lemmas for stdlib. BitChunking: chunk_nil, chun_exact; List: mkseq2; DList: dmap_dlist_partial_perm. by @namasikanam in #942
• Build docker test containers on release by @fdupress in #943

New Contributors

• @JNC4 made their first contribution in #898

Full Changelog: r2026.02...r2026.03