Custom query (531 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 531)

1 2 3 4 5 6

Status: accepted (11 matches)

Ticket Summary Owner Type Priority Component Version
#16113 <top> in printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17024 Pattern matching should try to infer memory and module parameters Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17034 Generalizing loop fusion Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17040 Syntactic sugar for nested if-then-else statements. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17042 Pattern matching in non-normal form. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17070 better error message when difference between goal and lemma is tiny Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17195 Swap with 2 args move as far down as possible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17250 off-by-one error in swap Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17309 `rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17378 Proof of false using smt and Eprover. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x

Status: assigned (28 matches)

Ticket Summary Owner Type Priority Component Version
#17117 Warning when restrictions over an adversary are empty Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17160 Call SMT in parallels. Pierre-Yves Strub enhancement 2 Internals pre-1.x
#17181 slow rewriting for large expressions Pierre-Yves Strub 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
#17253 EasyCrypt should fail gracefully when applying a tactic on a solved goal. Pierre-Yves Strub defect 2 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
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 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
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 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
#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
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17364 Internals: use Batteries maps instead of Why3 ones. Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17319 Anomaly triggered by `smt` defect 3 EasyCrypt pre-1.x

Status: closed (61 matches)

Ticket Summary Owner Type Priority Component Version
#17252 The `seq` variant documented as pHL is in fact the HL tactic. Alley Stoughton defect 3 Documentation 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
#15842 Bug in lambda translation Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#15919 [case] tactic for bd_hoare is useless Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 EasyCrypt pre-1.x
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15974 The following example generates an anomaly Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15980 inconsistency due to choosing from empty distribution Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15981 "delta cpEq" causes an untypable goal to be produced Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15982 Printer bug for partially applied infix operators in prefix form Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16000 repeated instantiation and losslessness of 3-argument fun don't work well together Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16137 universal elimination doesn't enforce { ... } restriction on module Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16138 assertion failure when call tactic not given { ... } module restriction Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16228 glob M computation problem with functors and inner modules for {*} Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16231 General issues with computation of globals for nested modules Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16306 Bug in cloning ? Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16362 Assertion failure when cloning a theory with let expressions Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#16723 Subtyping for abstract modules and functors Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16727 bd_hoare should work on >=, rather than forcing us to swap arguments Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16729 Tactic swap causes inconsistent dependencies Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16732 Problem with functor aliases when outermost module is a parameter Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16751 hoare should work on fun. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16787 new conseq issues Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16849 Broken proc (in branch 1.0) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16965 Non-termination when expanding a procedure whose body contains a generic projector (.`n) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17021 Some judgment-combining variants of conseq do not apply to procedures Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17089 anomaly in [sim] Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17114 Unsoundness of module system Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17128 assert false in rnd. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17129 bug in alias, the introduced variable has not the good type. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17133 seq for phoare do not check the type of the arguments. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17142 Anomaly (related to SMT and memories) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17300 Module type checks have wrong variance when dealing with some functor configurations Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17302 fel can generate subgoal with undefined memory Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17303 more fel peculiarities Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#15872 fun stopped working ckunz defect 5 EasyCrypt pre-1.x
#15879 While one sided ckunz enhancement 3 EasyCrypt pre-1.x
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 EasyCrypt pre-1.x
#16174 Bug in bdhoare call ckunz defect 3 EasyCrypt pre-1.x
#16292 Side-conditions for the rnd rule in pHL should be proved under some precondition ckunz defect 3 EasyCrypt pre-1.x
#16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 EasyCrypt pre-1.x
#16986 "while >=" generates invalid goals ckunz defect 3 EasyCrypt pre-1.x
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#17278 [eta] reduction is not full on multi-ary functions github <noreply@…> defect 3 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
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 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
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.