#15872 
fun stopped working

ckunz

defect

5

EasyCrypt

pre1.x

#16306 
Bug in cloning ?

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#16787 
new conseq issues

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#17013 
EasyCrypt toolchain does not compile anymore on OSX

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17027 
[Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17068 
Possible bug in the unionfind algorithm

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17079 
Make the testsuite pass.

PierreYves Strub

defect

5

Libraries

pre1.x

#17109 
Hoare adversary rule introducess references to nonexistent memories in postconditions

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#17112 
`unknown symbol Top.o` when importing a theory including objects referring to `Top.o`

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17114 
Unsoundness of module system

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#17132 
Unsoundness in definition of "glob M"

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17270 
`done` should close a goal when `false` is a local hyp.

PierreYves Strub

enhancement

5

EasyCrypt

pre1.x

#17365 
Proof of false using Ring and Reals.

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17379 
Proving unreasonable/false lemmas through AltErgo


defect

5

EasyCrypt

pre1.x

#17380 
Internal "seq" of pHL tactics is unsound

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#15702 
Error with multiple require if they contain the same game

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#15893 
Call in adversary call is not working properly

Benjamin Grégoire

defect

4

EasyCrypt

pre1.x

#15950 
tactics for fundamental lemma

Benjamin Grégoire

enhancement

4

EasyCrypt

pre1.x

#16692 
bug in apply.

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17012 
pr_false is badly implemented (unsoundness)

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17035 
AltErgo succeeds on false obligations in weird circumstances

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17080 
`t_generalize_hyps` does not work when given a nonsingleton list.

PierreYves Strub

defect

4

Internals

pre1.x

#17082 
SMT tactic should be interruptable.

PierreYves Strub

enhancement

4

EasyCrypt

pre1.x

#17087 
[conseq*] should be the default behaviour of [conseq]

PierreYves Strub

enhancement

4

EasyCrypt

pre1.x

#17089 
anomaly in [sim]

Benjamin Grégoire

defect

4

EasyCrypt

pre1.x

#17098 
Add a search facility

PierreYves Strub

enhancement

4

Documentation

pre1.x

#17120 
[rnd] allows to prove false

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17127 
Bug in typing of instruction x.[y] = e;

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17148 
Operators should be subject to section restrictions

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17162 
Bad interaction between abstract theories and local modules

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17329 
EasyCrypt output (goals order e.g.) is not stable

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17339 
`anomaly: EcLowGoal.InvalidProofTerm.` on `/>`

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#15506 
Issues when cloning theories

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15647 
Can't extract easily function from tuple

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15651 
lambda in operator doesn't work

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15676 
Zeta tactics takes too much time to end(infinite loop ?)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15715 
Can't access a variable from a functor in probability formula

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15737 
Typesoundness issue when implementing module signatures

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15738 
Typing functor applications inside modules

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15742 
Strange error raised during a call to trivial

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15744 
require import causes name collisions in sub theories

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15764 
Result not introduce after call in hoare logic

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15768 
Inlining with functor and cloning doesn't work

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15769 
ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#15781 
Bug into env insertion of a specific axiom Pr[]

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15786 
Swap with call to the adversary


defect

3

EasyCrypt

pre1.x

#15791 
import doesn't import function from module

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15794 
Operator not found

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15813 
call tactic signals an "unknown symbol" error

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15827 
memory restriction for adversary does not take inner modules into account

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15841 
No explicit binding in equiv creates problems

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15842 
Bug in lambda translation

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15851 
[rnd] for map update produces confusing postconditions

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15853 
timeout and prover settings are not undone

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#15871 
Stack Overflow

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15877 
Apply is not working when trying to use it to instantiate a lemma that is quantified on modules

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15881 
Complete path for local variable in printer

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15882 
tuple and memory misprinted

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15892 
It should not be possible to close a theory where not all proofs are finished

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15908 
Unification variables appear

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15909 
firstlast tactical do not have the right precedence w.r.t tactics chaining (t1; t2)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15919 
[case] tactic for bd_hoare is useless

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15920 
[conseq (_ : pre => _)] tactic for bd_hoare doesn't work

Santiago ZanellaBéguelin

defect

3

EasyCrypt

pre1.x

#15924 
Assertion failed in otherwise provable goal

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15962 
Rewrite Fails because it didn't manage to infer type whereas it could

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15965 
Assertion failure in EcEnv

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15966 
Something wrong with installation script?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15974 
The following example generates an anomaly

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15975 
Cfold bug with notation x.[a] =

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15980 
inconsistency due to choosing from empty distribution

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15981 
"delta cpEq" causes an untypable goal to be produced

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15982 
Printer bug for partially applied infix operators in prefix form

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15998 
Problem in cloning

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16000 
repeated instantiation and losslessness of 3argument fun don't work well together

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16001 
Instantiating an internal theory when cloning fails

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16013 
Bug in theory realization

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16015 
lack of dot in map subscripting leads to assertion failure

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16054 
Bug in theory cloning with theory instanciation and export

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16055 
confusion of x{1} and x{2} with x in cut

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16104 
naming issues


enhancement

3

EasyCrypt

pre1.x

#16111 
Strange bug in require

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16112 
Rnd on different type possible

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16115 
Subst failed

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16137 
universal elimination doesn't enforce { ... } restriction on module

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16138 
assertion failure when call tactic not given { ... } module restriction

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16140 
Strange error in typing

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16141 
Not catched error in split

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16149 
printer bug: parentheses in types

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16174 
Bug in bdhoare call

ckunz

defect

3

EasyCrypt

pre1.x

#16222 
Functor application circumvents sectionlocality

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16228 
glob M computation problem with functors and inner modules for {*}

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16231 
General issues with computation of globals for nested modules

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16264 
Bug in rewrite with let

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16288 
uncatched exception with functor inside functor

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16362 
Assertion failure when cloning a theory with let expressions

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16399 
Bug in congr?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16416 
FEL completeness  initialization

Benjamin Grégoire

enhancement

3

EasyCrypt

pre1.x

#16468 
try fails to catch some callrelated exceptions


defect

3

EasyCrypt

pre1.x

#16620 
Failure to patternmatch functional terms when they are applied in the goal.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

(more results for this group on next page)
