| HEAD | 236979f | feat: configurable warnings (uninit locals, unused unfold) Add per-warning enable/disable flags Warn:uninit and Warn:unused_unfold (on by default). Toggle in-script via pragma, on the CLI via -pragmas, or project-wide via a new pragmas key in easycrypt.project. | 10 July 2026, 16:53:40 UTC |
| refs/heads/aprhl | f7b8664 | Added Above Threshold and Report Noisy Max examples, which check with current version of branch. | 30 June 2021, 15:32:30 UTC |
| refs/heads/arrays | f7e7d63 | Formulas and typing for primitive arrays Mostly straightforward changes to get rid of compiler warnings about non-exhaustive pattern matches. Main points of note: - The various array constructors alternate between lists and arrays for the elements of the array. Those constructors are left unchanged, and sometimes we have to move between the two representations. - Tuple processing is rather similar to array processing, to the point that one closely mirrors the other. - Empty arrays, if supported, require additional processing to determine the type of their elements. | 18 February 2026, 13:16:48 UTC |
| refs/heads/bdep-bak | edab98c | tests/circuits: give example tests descriptive names | 17 June 2026, 08:13:36 UTC |
| refs/heads/bdep_ecCircuitsRefactor_zqcentered | a131fcd | Add centered representation: ZModPCentered + PolyReduce extensions ZModPCentered.ec introduces ZpCentered / ZpCenteredField with the canonical centered representative (crepr) on Z/pZ, supporting distributions, absolute value, triangle / product / monotonicity inequalities, and prime-only negation symmetry. PolyReduce.ec adds PolyReduceZpCentered / PolyReduceZpCenteredField: centered-representation infinity-norm machinery on polyXnD1, plus a DynMatrix-based vector/matrix layer with predicate-style _le / _lt bound checks and computed inf_norm soundness lemmas. | 13 May 2026, 18:06:23 UTC |
| refs/heads/claude_contributions | bf34c5c | contribution | 17 April 2026, 22:48:13 UTC |
| refs/heads/comm-algebra | ee462d5 | stdlib: basic commutative algebra | 21 August 2024, 09:37:01 UTC |
| refs/heads/coupling-rnd-tactics | 43fd769 | coupling rule: one-sided and two-sided | 03 October 2025, 13:22:59 UTC |
| refs/heads/delayed-couplings | 3a030af | sim: deadcode should check program variable isn't part of any memory of globals in the current eq. | 04 April 2025, 16:03:29 UTC |
| refs/heads/delayed-couplings-2 | a165587 | remove wp; add exfalso; alter indep | 12 May 2026, 14:21:08 UTC |
| refs/heads/deploy-fix-#154 | 9d08a76 | fix #154 | 24 November 2022, 16:10:02 UTC |
| refs/heads/deploy-flake | 097065e | flake: update toolchain and dev shells Bumps prover/toolchain pins (z3 4.12.6->4.14.1, cvc5 1.0.9->1.3.0, alt-ergo 2.4.3->2.4.2, nixpkgs 24.05->24.11) and reworks the dev shells (barebones / noProvers / withDevTools, with an emacs+proof-general setup, difftastic, perf-tools), plus conf-zlib/conf-git/alt-ergo/frama-c build overrides. Extracted from bdep_ecCircuitsRefactor; unrelated to the circuit feature. | 31 May 2026, 09:32:06 UTC |
| refs/heads/deploy-quantum-upgrade | 3cef12a | Making this branch work with same Why3 version as main | 10 October 2023, 09:38:20 UTC |
| refs/heads/deploy-tc | c8b896a | TcPoly: register ['c poly : idomain] when ['c : idomain] Phase 8 instance registration: backport stdlib [Poly.ec:850-974]'s [abstract theory Poly] (the IDomain coefficient phase). Re-emits the comring obligations (resolved verbatim from the same [polyD_*]/[polyM_*] lemmas as the Phase 5 comring instance) plus [mulf_eq0] discharged via [polyM_mulf_eq0] (already in TcPoly's idomain section). Required the bridging-lift fix in [scope/env] (parent commit) to get past the tparam-context mismatch the obligation form would otherwise have when the idomain chain reuses the existing comring/addgroup/addmonoid/monoid chain entries on the same carrier. | 21 May 2026, 05:33:20 UTC |
| refs/heads/dilithium | 77802af | Merge remote-tracking branch 'origin/main' into deploy-expected-cost | 16 February 2023, 15:28:03 UTC |
| refs/heads/distr-matrix | e48bd56 | DistrMatrix | 15 July 2024, 13:11:48 UTC |
| refs/heads/doc-fold-tutorial | 34fd8da | [doc] start folding the tutorial in | 18 June 2026, 08:26:50 UTC |
| refs/heads/doc-language | 7e5a8c4 | Add tentative auto-generated EasyCrypt language documentation This is a first draft covering: types, operators, predicates, expressions, formulas, programs, modules, module types, theories, sections, cloning, hints, printing, and standard library tour. | 12 April 2026, 21:31:51 UTC |
| refs/heads/doc-seq-tactic | fc2f6be | Fix formatting in seq.rst documentation | 04 February 2026, 16:21:29 UTC |
| refs/heads/doc-types | c996dd8 | Refman skeleton. Uses Sphinx + an extension that generates proofs viewable and navigable directly in the browser. | 14 January 2026, 21:19:49 UTC |
| refs/heads/doc-while-tactic | a2f41f8 | document pHL variants of while tactic | 16 March 2026, 18:43:33 UTC |
| refs/heads/docgen-revamp | f8a9e66 | First basic MD renderer and further abstraction/separation | 03 June 2026, 16:40:35 UTC |
| refs/heads/dynmatrix-stability | 0edbf95 | Merge branch 'main' into dynmatrix-stability | 22 February 2026, 19:21:29 UTC |
| refs/heads/eval-pwhile | 4bc1c67 | New vernacular command: eval Target: evaluation of pWhile programs. | 24 June 2024, 20:09:35 UTC |
| refs/heads/example-truncated-rejection | 3215fcd | [example] add a truncated rejection sampling This proof is uncommonly done in practice, and requires some out-of-logic reasoning plus an unreasonable amount of glue. Keeping it handy should help. (Also making sure we have a logic that can deal with this more elegantly should help.) | 13 June 2026, 21:04:11 UTC |
| refs/heads/expr-fold | 782de3b | some fixes and adding tuple destructuring | 25 March 2025, 09:19:58 UTC |
| refs/heads/feature-zqcentered | f382698 | Add centered representation: ZModPCentered + PolyReduce extensions ZModPCentered.ec introduces ZpCentered / ZpCenteredField with the canonical centered representative (crepr) on Z/pZ, supporting distributions, absolute value, triangle / product / monotonicity inequalities, and prime-only negation symmetry. PolyReduce.ec adds PolyReduceZpCentered / PolyReduceZpCenteredField: centered-representation infinity-norm machinery on polyXnD1, plus a DynMatrix-based vector/matrix layer with predicate-style _le / _lt bound checks and computed inf_norm soundness lemmas. | 13 May 2026, 18:06:23 UTC |
| refs/heads/feature_conseq_metavars | ab9125e | PR: #Pre/#Post meta vars in conseq | 13 March 2026, 23:49:40 UTC |
| refs/heads/feature_procchange_framing | 286de65 | PR: Add framing to proc change | 25 February 2026, 16:45:39 UTC |
| refs/heads/feature_signed_modP | 57701f6 | signed_modP | 29 September 2025, 14:40:46 UTC |
| refs/heads/fix-142 | 6fd85e8 | [matching]: when crossing a binder, update the env. accordingly | 29 March 2022, 10:28:41 UTC |
| refs/heads/fix-729 | 2ccf39e | In substitution, fix handling of bound variable in Pr | 10 March 2025, 08:00:58 UTC |
| refs/heads/fix_opsel_error_printing | ef9ce8e | PR: Fixing operator selection error messages | 17 November 2025, 10:55:15 UTC |
| refs/heads/fmap-fold | 34b6208 | Merge branch 'main' into fmap-fold | 22 February 2026, 19:22:10 UTC |
| refs/heads/gen-rewrite-pr | 45897e1 | WIP | 21 March 2026, 11:41:10 UTC |
| refs/heads/improve_nix_flake | 6133c09 | PR: Improve flake.nix | 27 March 2026, 16:44:11 UTC |
| refs/heads/improve_smt | a642c61 | Smtlib integration | 01 April 2026, 13:50:30 UTC |
| refs/heads/indexed-types | a52b88b | indexed-types: word numeric layer — arithmetic, comparisons, shifts Develop theories/datatypes/IWord.ec into a Tier-1 machine-word surface: - bitwise `orw` + simp lemmas; - arithmetic ℤ/2ⁿ ring: ops `(+)`/`oppa`/`(*)`, the `to_uint` homomorphism laws (to_uintD/M/N), the `of_int` laws, and a `ComRingDflInv` clone `WRingA` over `word<:n+1>`; - unsigned/signed comparisons `\ule`/`\ult`/`\sle`/`\slt` + Ngt/Nge; - shifts/rotates `>>>`/`<<<`/`sar`/`ror`/`rol` with bit-laws; - shift <-> arithmetic: `int_bitMP`/`int_bitDP` (reusable pure-integer bit-shift lemmas), `shlMP`/`shrDP`, and `to_uint_shl`/`to_uint_shr`. Tests: iword_num (numeric round-trips, smt-through-symbolic-index), iword_arith (arithmetic/comparison/shift surface), iword_ring (boolean ring tactic at symbolic/concrete widths); drop the superseded iword_ring64. | 07 July 2026, 04:58:39 UTC |
| refs/heads/jasmin-in-ci | b110239 | REVERT ME This forces the use of the EasyCrypt+Jasmin docker image to measure CI performance impact. It should be reverted if and when we decide to include Jasmin in the main docker image. | 06 August 2025, 16:06:19 UTC |
| refs/heads/latest | 1c7e6d7 | [chore] fix unused unfold warnings | 11 June 2026, 18:11:27 UTC |
| refs/heads/library_renyi_divergence | abd5301 | Rényi-∞ divergence machinery for oracle-bounded reductions The Rényi-∞ (max-divergence / dominance) machinery for bounded-query reductions: - RDiv.ec: Rényi-∞ / max-divergence (rdiv_inf, dominated) with probability preservation (dominated_pr / rdiv_inf_pr), structural composition (dmap/dlet/dprod/dlist/dexcepted/dcond/djoin/dfold/dfun), and a distinguisher layer (Sample, adv_rdiv_inf, adv_rdiv_inf_dlist). - BoundedPreSample.ec: fresh-sampling = presampling-a-list equivalence (eq_pr_fresh_ref) for bounded-query adversaries; admit-free. - RDivOracle.ec: parametric bounded-query advantage bound rdiv_bound_sampler (Pr[Game1] <= M^N * Pr[Game2]) via BoundedPreSample + dlist tensorization. | 17 June 2026, 14:01:44 UTC |
| refs/heads/llm-format | a84428d | [llm] add -trace LINE[:COL] for single-sentence before/after goals Runs every sentence before the target, prints the goal state, runs the target sentence, prints the state again. Output uses stable === BEFORE / TACTIC / AFTER === delimiters so callers can split. Exit codes: 0 ok, 1 if the target sentence failed, 2 if no sentence at or after the target. Mutually exclusive with -upto. | 26 May 2026, 11:06:16 UTC |
| refs/heads/llm-interactive | b1890de | [llm] update CLAUDE.md with current workflow status Add two workflow sections that were missing or stale: 4. Inspect and navigate nested subgoals with TREE and FOCUS Documents the dotted-path syntax (FOCUS 1.2.3), the [focus: k/N] reply tag, and the fact that TREE labels are dynamic (focus-first, not stable across focus changes). 5. Build a +strict_bullets-friendly proof with COMMIT Documents how COMMIT replays the recorded transcript and inserts bullets, plus the cycle (-, +, *, --, ++, **, ...) and the prior- bullet collision avoidance. Re-number the existing QUIET and SEARCH sections from 4/5 to 6/7. Fix one outdated pitfall ("subgoals must be closed in order") -- FOCUS path now lets the agent address them in any order. Reflects what's live in EcLlm; the protocol/meta-command table was already up to date. | 31 May 2026, 17:51:21 UTC |
| refs/heads/main | 236979f | feat: configurable warnings (uninit locals, unused unfold) Add per-warning enable/disable flags Warn:uninit and Warn:unused_unfold (on by default). Toggle in-script via pragma, on the CLI via -pragmas, or project-wide via a new pragmas key in easycrypt.project. | 10 July 2026, 16:53:40 UTC |
| refs/heads/mldsa | 83ce337 | bullets: focusing operators behind +strict_bullets pragma When `pragma +strict_bullets` is set, the bullet tokens `-`, `+`, `*` (and their repeated forms `--`, `++`, `**`, ...) become Coq-style focusing operators: each phrase's bullet is checked against a per-proof stack so that a subgoal must be discharged before its sibling is addressed, and so that bullet characters identify nesting levels. The default behavior is unchanged: without the pragma, bullets remain pure decoration, preserving every existing proof script. Repeated bullet characters are emitted by the lexer as single PLUSn/MINUSn/STARn tokens (carrying their literal), which makes them usable both as deeper bullet levels and as user-defined binary operators (`op (--) ...`). The final sibling of a split point can be continued at the parent level without a bullet: when the previous sibling is closed and exactly one sibling remains, the inner frame pops automatically (and cascades through nested last-sibling frames). This keeps the standard phl idiom of long `seq N : <post>' chains flat instead of forcing ever-deeper indentation under a `+' for each continuation. Multi-way splits keep their enumeration discipline for all but the last subgoal. | 26 May 2026, 06:14:09 UTC |
| refs/heads/new-ehoare | 55e5d3f | starting point | 10 March 2026, 18:02:02 UTC |
| refs/heads/notations | 421a078 | feat(notations): add user-extensible notations Adds a `notation` construct that lets users declare `#`-prefixed syntactic sugar for formulas, with template-based parsing and typing-time expansion. Notations are stored as operators (sharing abbreviation infrastructure), so they work uniformly with import/export, clone, locality, sections, qualified lookup, and `rewrite /#foo` unfolds. Declarations: notation #big ['a] #< i : 'a > (r : 'a list) (P : i ==> bool = predT) (F : i ==> t) "[" i " : " r ("| " P)? "] " F = big P F r. Uses: lemma L (d : 'a distr) (f : 'a -> real) J : uniq J => BRA.#big [ x : J ] (mu1 d x * f x).`1 <= 1%r. lemma M &m (bs : out_t list) : Dst.#big [ b : bs ] (Pr[A.guess() @ &m : res = b]) <= 1%r. (* slot placeholders work as pose / rewrite patterns *) pose c := #big [ _ : _ | _ ] _. Expansions round-trip back to template syntax in the pretty-printer. Includes a stdlib port: `#big` / `#bigi` are declared in Bigop.eca and used across algebra, analysis, distributions, modules, and crypto files. Tests under tests/notations/ (wired into `make unit`) and reference documentation under doc/notation.rst. | 24 April 2026, 09:17:29 UTC |
| refs/heads/ocaml-5 | 527d9ae | Force OCaml >= 5.3 This is to check the CI with the last version of OCaml. | 06 March 2025, 18:49:21 UTC |
| refs/heads/ois-refactoring | e5c82e7 | WIP: local option for function read/write and minor tweak to memory restriction solving. | 05 September 2025, 14:07:00 UTC |
| refs/heads/opt-warnings-gc-tuning | 02e5680 | perf: relax OCaml 5.x GC pacing for custom blocks, warn on 5.0–5.3 EasyCrypt hash-conses its AST and allocates zarith/GMP custom blocks heavily. On OCaml 5.x the default custom_major_ratio paces the major GC far too aggressively over that external memory (OCaml issue #14533, pronounced on 5.5), costing large amounts of CPU for no memory benefit: compiling a large file (NTTAlgebra.ec) measured ~5x slower than on 4.14 (1255s vs 339s), with the same ~1GB working set. Set custom_major_ratio to 250 on OCaml >= 5, which restores 4.14-class performance (5.5: 1255s -> 233s). This is a no-op on 5.4, whose default pacing is already fine, and harmless there. Additionally, warn at startup on OCaml 5.0–5.3, whose minor GC over-promotes values reachable from ephemeron/weak-table keys (OCaml issue #13643), causing severe memory blowup with EasyCrypt's weak-table hash-consing. Fixed upstream in OCaml 5.4; recommend upgrading. | 12 July 2026, 08:20:31 UTC |
| refs/heads/oram-new-lemmas-list | e221166 | new lemmas for List; four new operators: isprefix, prefixes, interval, rfind | 10 July 2026, 13:28:49 UTC |
| refs/heads/perms-group | b60d701 | Permutations as a group + uniform distr | 23 January 2026, 22:10:09 UTC |
| refs/heads/polydiv | 503d035 | Polynomial division | 19 March 2024, 10:29:37 UTC |
| refs/heads/pose-match-fix | 50319ad | Merge branch 'main' into pose-match-fix | 09 March 2026, 08:03:33 UTC |
| refs/heads/prf-generalise | 422787c | [cryptolib] generalize PRF definitions, PRP<->PRF This takes a swipe at cleaning up the PRF and PRP theories, as well as the associated switching lemmas. This should bring them more in line with modern EasyCrypt practice while also making them better examples of modern EasyCrypt development themselves—perhaps serving as advanced tutorials. | 03 June 2026, 14:30:49 UTC |
| refs/heads/quotation-preprocessor | fe1fbfb | Add black-box quotation preprocessor Introduce {% name body %} quotations, expanded during lexing by an external tool over stdin/stdout. A quotation expands to a sentence fragment that is spliced into the surrounding sentence, so it may replace only part of a sentence (and several may appear in one). The terminating '.' is always written by the user. Locations in the expansion are remapped back to the original source, so errors point at the original quoted text. Usage Write a quotation as {% name body %}, where name selects a handler and body is arbitrary text (the {% %} delimiters nest). The expansion is a fragment, so the surrounding sentence and its '.' are written outside the quotation: op forty_two = {% calc 6 * 7 %}. Quotations compose with ordinary source and with each other in one sentence: op mixed = {% calc 6 * 7 %} + ({% calc 2 + 3 %} * 10). Enabling quotations Quotations run external programs, so the feature is OFF by default and a quotation encountered while it is off is a hard error (never a silent skip or a silent execution). Enable it for a run in one of two ways: easycrypt -enable-quotations compile foo.ec EC_ENABLE_QUOTATIONS=1 easycrypt compile foo.ec It cannot be enabled from easycrypt.project, which ships inside a checked-out tree -- letting it turn the feature on would defeat the safeguard. Only enable quotations for sources you trust. Binding handlers Once enabled, a name is resolved to a shell command in order: a 'quote = name:command' entry in the [general] section of easycrypt.project (relative paths resolved against the project directory); then EC_QUOTE_<NAME>; then EC_QUOTE_CMD; then an executable handlers/<name> (also .py/.sh) next to the source file. Handler protocol The handler reads the body (after a header line) on stdin and writes a single JSON object on stdout: { "expanded": <source>, "segments": [...] }, where segments is the source map used for error-location remapping. A non-zero exit reports an error at the quotation. See doc/quotations.rst for the full reference. | 29 May 2026, 10:10:22 UTC |
| refs/heads/quotation-preprocessor-alt | f53bbe5 | Use lexbuf trick to ensure error exception in EcIO.expand_quotation doesn't result in Proof General getting stuck. | 19 June 2026, 15:48:15 UTC |
| refs/heads/r2022.04-01 | b765395 | [nix] force Why3 1.4.1 | 16 June 2022, 07:41:17 UTC |
| refs/heads/refactor-pl | 13273e4 | phl: keep code resolution out of the seq checker's TCB The checker is trusted re-validation, so it must not redo elaboration work the rule already did. The hoare-seq checker was re-resolving the symbolic code gap (via s_split), pulling all of code-position normalization into its trust boundary. Split the parameters into two records: the high-level rule arguments (hoare_seq_rule, with a symbolic codegap1) that the canonical rule takes, and the low-level node payload (hoare_seq_node, with the resolved nm_codegap1 integer index) that is recorded and rechecked. The rule resolves the gap once (new EcLowPhlGoal.s_split_index = normalize_cgap1 with the s_split error), records the resolved node, and builds subgoals through a pure low-level core that splits at the integer (split_at_nmcgap1, no env). The checker reruns only that core, so normalize_cgap1 stays out of its TCB; faithfulness is by construction since the rule builds its subgoals through the same core. Docs: new REFACTORING 7c ("the checker is post-resolution; the node records resolved data") + rule of thumb to record the lowest-level value that still determines the subgoals; 7b lists both records; recipe and README spine updated. Build clean; pilot + 23 seq files pass under EC_RECHECK=1. | 11 June 2026, 14:23:55 UTC |
| refs/heads/release | 1c7e6d7 | [chore] fix unused unfold warnings | 11 June 2026, 18:11:27 UTC |
| refs/heads/setoidrw | f9deb8d | setoid rewrite | 05 March 2025, 18:02:57 UTC |
| refs/heads/subtypes | e8a2fe4 | preparing for alternate operator application | 11 October 2024, 18:56:52 UTC |
| refs/heads/theory_finite_field | 3787dc9 | scaled_monicM is provable for polynomials over fields but not over any integral domain | 02 June 2023, 13:47:12 UTC |
| refs/heads/update-eclistings.sty | a2232a4 | Add custom dollar commands and math substitutions | 15 May 2026, 07:50:19 UTC |
| refs/heads/uptobad_warnings | 3ba2e8e | improved warnings for uptobad | 02 April 2025, 21:45:30 UTC |
| refs/heads/vscode | e7c3fd7 | LSP | 21 January 2026, 12:58:01 UTC |
| refs/heads/yaeasypqc | 524ffa4 | compiles | 23 January 2026, 11:03:33 UTC |
| refs/tags/r2024.09 | 7270f8c | remove some edgy SMTs in Xreal and related These might enable a version bump on some provers. | 27 August 2024, 11:44:02 UTC |
