#17181 |
slow rewriting for large expressions
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17194 |
anomaly: EcHiGoal.LowApply.NoInstance (in byequiv)
|
Benjamin Grégoire
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17207 |
Applicative view
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17222 |
local clones do not disappear from the environment on section end
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17240 |
Syntactic sugar for proc. that reduces to a call to an external proc.
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17255 |
Missing unification in `clone...with...`
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17256 |
apply/rewrite should work modulo zeta-reduction.
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17261 |
`rewrite -/(f _)` should not match its own unfoldings.
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17262 |
Add the possibility to add rewrite hints to rewrite hint databases.
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17263 |
Multiple incompleteness in `apply`
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17265 |
`goal` vernacular command
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17268 |
Add a tactical that fails when no progress is done.
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17269 |
Add notations for >/>=
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17270 |
`done` should close a goal when `false` is a local hyp.
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17271 |
Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn`
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17308 |
`rewrite !(A,B)` loops when `B` is not known about
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17319 |
Anomaly triggered by `smt`
|
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#17334 |
this message need more information: cannot infer all placeholders
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17335 |
the formula contains free type variables
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#17402 |
Automatically package and publish up-to-date tutorial proofs
|
Pierre-Yves Strub
|
enhancement
|
3
|
Documentation
|
pre-1.x
|
#17117 |
Warning when restrictions over an adversary are empty
|
Benjamin Grégoire
|
enhancement
|
2
|
EasyCrypt
|
pre-1.x
|
#17160 |
Call SMT in parallels.
|
Pierre-Yves Strub
|
enhancement
|
2
|
Internals
|
pre-1.x
|
#17253 |
EasyCrypt should fail gracefully when applying a tactic on a solved goal.
|
Pierre-Yves Strub
|
defect
|
2
|
EasyCrypt
|
pre-1.x
|
#17264 |
Add the possibility to clear lemmas when closing a theory.
|
Pierre-Yves Strub
|
defect
|
2
|
EasyCrypt
|
pre-1.x
|
#17310 |
Top-level command to print various databases (exact, rewrite, ...)
|
Pierre-Yves Strub
|
defect
|
2
|
EasyCrypt
|
pre-1.x
|
#17347 |
Search with notations is broken.
|
Pierre-Yves Strub
|
defect
|
2
|
EasyCrypt
|
pre-1.x
|
#17343 |
(Optional) warning for old syntax
|
Pierre-Yves Strub
|
enhancement
|
1
|
EasyCrypt
|
pre-1.x
|
#17345 |
Bad printing
|
Pierre-Yves Strub
|
defect
|
1
|
EasyCrypt
|
pre-1.x
|
#17364 |
Internals: use Batteries maps instead of Why3 ones.
|
Pierre-Yves Strub
|
enhancement
|
1
|
EasyCrypt
|
pre-1.x
|
#15872 |
fun stopped working
|
ckunz
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#16306 |
Bug in cloning ?
|
Benjamin Grégoire
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#16787 |
new conseq issues
|
Benjamin Grégoire
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17013 |
EasyCrypt toolchain does not compile anymore on OSX
|
Pierre-Yves Strub
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17027 |
[Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition
|
Pierre-Yves Strub
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17068 |
Possible bug in the union-find algorithm
|
Pierre-Yves Strub
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17079 |
Make the test-suite pass.
|
Pierre-Yves Strub
|
defect
|
5
|
Libraries
|
pre-1.x
|
#17109 |
Hoare adversary rule introducess references to non-existent memories in postconditions
|
Benjamin Grégoire
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17112 |
`unknown symbol Top.o` when importing a theory including objects referring to `Top.o`
|
Pierre-Yves Strub
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17114 |
Unsoundness of module system
|
Benjamin Grégoire
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17132 |
Unsoundness in definition of "glob M"
|
Pierre-Yves Strub
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17365 |
Proof of false using Ring and Reals.
|
Pierre-Yves Strub
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17379 |
Proving unreasonable/false lemmas through Alt-Ergo
|
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#17380 |
Internal "seq" of pHL tactics is unsound
|
Benjamin Grégoire
|
defect
|
5
|
EasyCrypt
|
pre-1.x
|
#15702 |
Error with multiple require if they contain the same game
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#15891 |
Instantiating axioms and sub-theories when cloning theories
|
Pierre-Yves Strub
|
enhancement
|
4
|
EasyCrypt
|
pre-1.x
|
#15893 |
Call in adversary call is not working properly
|
Benjamin Grégoire
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#15950 |
tactics for fundamental lemma
|
Benjamin Grégoire
|
enhancement
|
4
|
EasyCrypt
|
pre-1.x
|
#16692 |
bug in apply.
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17012 |
pr_false is badly implemented (unsoundness)
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17035 |
Alt-Ergo succeeds on false obligations in weird circumstances
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17080 |
`t_generalize_hyps` does not work when given a non-singleton list.
|
Pierre-Yves Strub
|
defect
|
4
|
Internals
|
pre-1.x
|
#17087 |
[conseq*] should be the default behaviour of [conseq]
|
Pierre-Yves Strub
|
enhancement
|
4
|
EasyCrypt
|
pre-1.x
|
#17089 |
anomaly in [sim]
|
Benjamin Grégoire
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17098 |
Add a search facility
|
Pierre-Yves Strub
|
enhancement
|
4
|
Documentation
|
pre-1.x
|
#17120 |
[rnd] allows to prove false
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17127 |
Bug in typing of instruction x.[y] = e;
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17148 |
Operators should be subject to section restrictions
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17155 |
Fix stdlib w.r.t. why3 import
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17162 |
Bad interaction between abstract theories and local modules
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17329 |
EasyCrypt output (goals order e.g.) is not stable
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#17339 |
`anomaly: EcLowGoal.InvalidProofTerm.` on `/>`
|
Pierre-Yves Strub
|
defect
|
4
|
EasyCrypt
|
pre-1.x
|
#15502 |
"Ident <top>_[...] is not yet declared" when cloning a theory with operators
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15506 |
Issues when cloning theories
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15520 |
request for more loop manipulation tactics
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#15647 |
Can't extract easily function from tuple
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15651 |
lambda in operator doesn't work
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15676 |
Zeta tactics takes too much time to end(infinite loop ?)
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15715 |
Can't access a variable from a functor in probability formula
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15716 |
Problem with introduction of Module in Proof
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15737 |
Type-soundness issue when implementing module signatures
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15738 |
Typing functor applications inside modules
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15742 |
Strange error raised during a call to trivial
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15744 |
require import causes name collisions in sub theories
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15762 |
Tactic to transform a tuple equality into a conjonction
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#15764 |
Result not introduce after call in hoare logic
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15768 |
Inlining with functor and cloning doesn't work
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15769 |
ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error
|
Pierre-Yves Strub
|
defect
|
3
|
ProofGeneral
|
pre-1.x
|
#15779 |
Inference during apply
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#15781 |
Bug into env insertion of a specific axiom Pr[]
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15786 |
Swap with call to the adversary
|
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15791 |
import doesn't import function from module
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15794 |
Operator not found
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15808 |
Declaring/defining mixfix operators, using them when not in scope
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#15809 |
Parsing/Printing scope for operator overloading "(x op y)%Scope"
|
Pierre-Yves Strub
|
enhancement
|
3
|
EasyCrypt
|
pre-1.x
|
#15813 |
call tactic signals an "unknown symbol" error
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15814 |
call tactic accepts variable defined in left game ({1}) defined for right game
|
Pierre-Yves Strub
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15827 |
memory restriction for adversary does not take inner modules into account
|
Benjamin Grégoire
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
#15841 |
No explicit binding in equiv creates problems
|
Benjamin Grégoire
|
defect
|
3
|
EasyCrypt
|
pre-1.x
|
(more results for this group on next page)
|