All pull requests

Pull requests

• fix(fixpoint): matchfix termination check must descend into all call arguments

  #1144·namasikanam opened Sep 18, 2026·

  ·

• fix(sim): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

  #1143·namasikanam opened Sep 18, 2026·

  ·

• fix(fel): count the lvalue of a call to an excepted oracle as a write

  #1140·strub opened Sep 11, 2026·

  ·
  1

• Fix swap when exception are in call

  #1137·lyonel2017 opened Sep 11, 2026·

  ·

• Add support of exception in Hoare logic for command rnd

  #1136·lyonel2017 opened Sep 11, 2026·

  ·

• fix(phl): emit the non-negativity of the bound as a separate goal in rnd (on #1105)

  #1135·Yiping106283 opened Sep 11, 2026·

  ·
  1

  3

• fix(phl): require the invariant on loop entry in the while variant rule

  #1132·Yiping106283 opened Sep 11, 2026·

  ·
  1

• fix(phl): reject a bound written by the prefix in the upper-bound while rule

  #1131·Yiping106283 opened Sep 11, 2026·

  ·

• fix(phl): check the bound of the upper-bound while rule on all memories (on #1105)

  #1130·Yiping106283 opened Sep 11, 2026·

  ·
  1

• Speed up requiring large machine-generated theories

  #1118·bgregoir opened Sep 7, 2026·

  ·

• fix(fel): require per-step weights non-negative over the counter range

  #1096·namasikanam opened Aug 24, 2026·

  ·
  3

• replay: redirect datatype constructors in match bodies too

  #1089·MavenRain opened Jul 31, 2026·

  ·
  1

• Documentation for incremental module definitions

  documentation
  #1087·Gustavo2622 opened Jul 24, 2026·

  ·
  1

  

• Rényi-∞ divergence machinery for oracle-bounded reductions

  library
  #1076·Gustavo2622 opened Jul 13, 2026·

  ·
  3

  

• Integer-indexed types

  #1065·strub opened Jul 2, 2026·

  ·
  16

• [doc] start folding the tutorial in

  #1051·fdupress opened Jun 18, 2026·

  ·
  2

• phl: reorganize the program logic into a recheckable four-layer structure

  #1041·strub opened Jun 10, 2026·

  ·

• [cryptolib] generalize PRF definitions, PRP<->PRF

  breaking changelibrary
  #1028·fdupress opened Jun 3, 2026·

  ·
  10

  

• Add black-box quotation preprocessor

  #1020·strub opened May 29, 2026·

  ·
  9

• [llm] agent-facing interfaces: interactive REPL and in-binary MCP server

  #1019·strub opened May 27, 2026·

  ·

• Adds theories/algebra/ZqCentered.ec providing the centered (signed) i…

  #995·mbbarbosa opened May 7, 2026·

  ·

• feat(notations): add user-extensible notations

  enhancementfeature
  #985·strub opened Apr 23, 2026·

  ·
  

• contributions from Claude experiments

  #982·mbbarbosa opened Apr 17, 2026·

  ·

• Add tentative auto-generated EasyCrypt language documentation

  #976·strub opened Apr 12, 2026·

  ·
  11

• Rewrite PR

  #946·strub opened Mar 21, 2026·

  ·