All issues

Search results

proc rewrite /= ignores the proof-local simplify hint configuration (named databases, local lemma adds)

Status: Open.

#1116 In EasyCrypt/easycrypt;

· strub opened on Sep 4, 2026

out t_change from the TCB

Status: Open.

#1115 In EasyCrypt/easycrypt;

· bgregoir opened on Sep 4, 2026

New intro-pattern: n+

feature

good-to-have

Status: Open.

Feature

#1114 In EasyCrypt/easycrypt;

· fdupress opened on Sep 4, 2026

hint simplify: warn or fail on binders a conjunct does not mention

Status: Open.

#1112 In EasyCrypt/easycrypt;

· strub opened on Sep 4, 2026

Docs CI does not fail on broken ecproof examples

Status: Open.

#1111 In EasyCrypt/easycrypt;

· strub opened on Sep 4, 2026

pHL while with strict variant fails to handle cases where the loop invariant is not satisfied

Status: Open.

#1103 In EasyCrypt/easycrypt;

· oskgo opened on Aug 25, 2026

pHL while permits negative probabilities

Status: Open.

#1102 In EasyCrypt/easycrypt;

· oskgo opened on Aug 25, 2026

pHL call permits negative probabilities

Status: Open.

#1101 In EasyCrypt/easycrypt;

· oskgo opened on Aug 25, 2026

pHL seq permits negative probabilities

Status: Open.

#1100 In EasyCrypt/easycrypt;

· oskgo opened on Aug 25, 2026

circuit: Assert_failure anomaly when a context-local definition is a function-valued bitvector operator (e.g. \bitsN applied only to its value)

Status: Open.

Bug

#1078 In EasyCrypt/easycrypt;

· strub opened on Jul 15, 2026

Coding style for standard libraries

good-to-have

Status: Open.

#1074 In EasyCrypt/easycrypt;

· namasikanam opened on Jul 10, 2026

Libraries of cryptographic results; issues with query counting as done currently

library

Status: Open.

#1070 In EasyCrypt/easycrypt;

· fdupress opened on Jul 9, 2026