| ff23f9a | François Dupressoir | 06 May 2016, 08:39:52 UTC | argmin: remove existentials in premises. | 06 May 2016, 08:39:52 UTC |
| 22578b4 | Pierre-Yves Strub | 06 May 2016, 07:38:09 UTC | `argmin` operator `argmin p` returns the smaller natural `i` s.t. `p i` or 0 if not such witness exists. | 06 May 2016, 07:38:09 UTC |
| fa61550 | Pierre-Yves Strub | 05 May 2016, 19:31:40 UTC | Add negative filters for `clone ... proof * [...]` Filters now have the following syntax: `[-?tag ... -?tag]` Negative tags are of the form `-tag`. Other ones are named positive. An axiom is selected by a filter if: - none of its tags are rejected by a negative filters - one of its tags is accepted by a positive filter or no positive filters exists | 05 May 2016, 19:31:40 UTC |
| 6c9dfe5 | Pierre-Yves Strub | 05 May 2016, 09:28:49 UTC | Properly equip zmod with a ring structure. The inverse is currently not linked to gcd. | 05 May 2016, 09:29:36 UTC |
| bf94ca4 | François Dupressoir | 04 May 2016, 11:21:37 UTC | Moving Word away from Arrays. Updating MEE functional spec accordingly. | 04 May 2016, 11:21:45 UTC |
| 0670411 | François Dupressoir | 04 May 2016, 11:19:46 UTC | Stabilize smt in MEE instantiation. | 04 May 2016, 11:19:46 UTC |
| ccd68ba | Pierre-Yves Strub | 30 April 2016, 13:47:02 UTC | In `clone`: when renaming, don't forget to prepend sub-theorie path as a prefix. [fix #17312] | 30 April 2016, 13:47:02 UTC |
| aa6ee8e | Pierre-Yves Strub | 30 April 2016, 11:30:50 UTC | Homogenise module & module type parameters syntax. [fix #17314] | 30 April 2016, 11:30:50 UTC |
| 6bd35fb | Pierre-Yves Strub | 30 April 2016, 10:53:33 UTC | In mod-typing: clean-up dead code, remove internal exn., fix various bugs. [fix #17313] | 30 April 2016, 10:53:33 UTC |
| dff9911 | Pierre-Yves Strub | 29 April 2016, 19:32:49 UTC | bigop: partition | 29 April 2016, 19:33:12 UTC |
| 0014c65 | François Dupressoir | 27 April 2016, 13:20:53 UTC | Using (semi-)modern libs for MEE-CBC functional spec. Some discussion need to be had: - Should we bring everything back to bitstrings? octetstrings? - Should we get rid of those blasted Arrays? (Yes) | 27 April 2016, 15:06:22 UTC |
| 8db4a56 | François Dupressoir | 25 April 2016, 16:55:16 UTC | Stabilizing some smt calls and fixing a proof. | 25 April 2016, 16:55:16 UTC |
| 4702c81 | François Dupressoir | 22 April 2016, 17:58:46 UTC | More systematic construction for the partitioning of final states. | 22 April 2016, 17:58:46 UTC |
| 4bfe658 | François Dupressoir | 22 April 2016, 15:15:56 UTC | Starting cleanup in Dice_sampling and associated example. | 22 April 2016, 15:15:56 UTC |
| 179af54 | François Dupressoir | 22 April 2016, 14:34:11 UTC | Preliminary generic argument for event partitioning. This kind of argument is currently difficult to use, but formalizing and using them should give us hints as to what we can and should do to support them more cleanly. This one will be used, once generalized further and cleaned up, to simplify Dice_sampling. | 22 April 2016, 14:44:11 UTC |
| db89cbe | François Dupressoir | 22 April 2016, 13:18:48 UTC | Generalizing dscale into DScalar with backwards comp. | 22 April 2016, 14:44:11 UTC |
| 85d276d | Pierre-Yves Strub | 19 April 2016, 21:00:33 UTC | do generalization modulo alpha-eq, not conv | 19 April 2016, 21:00:42 UTC |
| ac9b6e7 | François Dupressoir | 07 April 2016, 16:14:04 UTC | Cleaning up and 'documenting' Benjamin's general Eager argument. | 07 April 2016, 16:14:04 UTC |
| 7fe5299 | François Dupressoir | 07 April 2016, 15:41:06 UTC | Very minor on NewFMap. | 07 April 2016, 15:41:06 UTC |
| 2318135 | François Dupressoir | 05 April 2016, 16:49:49 UTC | Expanding set of operators on relations. | 05 April 2016, 16:49:49 UTC |
| 5e9884e | François Dupressoir | 05 April 2016, 14:28:07 UTC | PRG example: some major changes. Switch to using explicit distributions and probability; Switch to preferred proof engine setup (newip, implicits); Switch to inductives for bad event and invariant; More stability fixes. | 05 April 2016, 14:28:07 UTC |
| 77d2c90 | François Dupressoir | 05 April 2016, 12:29:33 UTC | PG keywords | 05 April 2016, 12:29:38 UTC |
| 6e1520f | François Dupressoir | 05 April 2016, 08:16:28 UTC | Minor cleanup in PRG. | 05 April 2016, 08:16:28 UTC |
| 0778000 | François Dupressoir | 28 March 2016, 16:51:55 UTC | MEE-CBC: cleanup and smt stabilization (in CBC). | 04 April 2016, 08:58:29 UTC |
| c770168 | Pierre-Yves Strub | 02 April 2016, 08:12:48 UTC | build-linux: do not force toolchain version anymore | 02 April 2016, 08:12:48 UTC |
| ce05896 | Pierre-Yves Strub | 02 April 2016, 08:11:52 UTC | README: add ZArith in deps. | 02 April 2016, 08:11:52 UTC |
| 8204617 | Pierre-Yves Strub | 02 April 2016, 08:09:32 UTC | Why3: => 0.87 | 02 April 2016, 08:09:32 UTC |
| 9d80a0e | Pierre-Yves Strub | 28 March 2016, 19:24:26 UTC | fix packaging for linux-32 | 28 March 2016, 19:24:47 UTC |
| 250b54f | François Dupressoir | 28 March 2016, 13:19:31 UTC | MEE-CBC: making further use of new standard libraries. | 28 March 2016, 13:19:43 UTC |
| d597a68 | Pierre-Yves Strub | 25 March 2016, 07:43:56 UTC | Update README.md | 25 March 2016, 07:43:56 UTC |
| d1bbeb2 | Pierre-Yves Strub | 16 March 2016, 20:20:10 UTC | linux packaging: fix PG conf | 16 March 2016, 20:20:20 UTC |
| 9330f1e | Pierre-Yves Strub | 11 March 2016, 14:49:04 UTC | dbhints can now be empty. For example, `smt()` is `smt w=()` which implies `smt ml=0`. | 11 March 2016, 14:49:04 UTC |
| 85cdb3f | Pierre-Yves Strub | 10 March 2016, 21:52:44 UTC | smt(...) is now an alias for smt w=(...) | 10 March 2016, 21:52:44 UTC |
| 34aab04 | François Dupressoir | 10 March 2016, 10:30:11 UTC | Updating a few examples. | 10 March 2016, 10:30:11 UTC |
| 9df4dd0 | François Dupressoir | 10 March 2016, 10:13:28 UTC | Removing obsolete PRP-PRF example. An up-to-date and maintained version can be found in theories/crypto/prp_prf/RP_RF.eca | 10 March 2016, 10:13:33 UTC |
| 12a4465 | François Dupressoir | 09 March 2016, 15:54:32 UTC | Quick and Dirty fix for Hashed ElGamal. | 09 March 2016, 15:54:32 UTC |
| e365fbf | François Dupressoir | 07 March 2016, 13:48:39 UTC | PRG example: some update and stabilization. | 07 March 2016, 13:48:39 UTC |
| 123baa8 | Pierre-Yves Strub | 05 March 2016, 16:18:17 UTC | Distribute ecVersion.ml.in, not ecVersion.ml | 05 March 2016, 16:18:17 UTC |
| 1b99c89 | Pierre-Yves Strub | 04 March 2016, 19:14:32 UTC | easycrypt config now displays the git hash | 04 March 2016, 19:15:00 UTC |
| b31f19f | Pierre-Yves Strub | 04 March 2016, 15:07:52 UTC | remove stalled examples (now in stdlib) | 04 March 2016, 15:07:52 UTC |
| cc6f725 | Pierre-Yves Strub | 26 February 2016, 16:03:19 UTC | Bind local modules when pretty-printing quantifiers [fix #17304] | 26 February 2016, 16:03:19 UTC |
| 535a27e | Pierre-Yves Strub | 26 February 2016, 11:38:40 UTC | exclude `oldlibs` from tests | 26 February 2016, 11:38:47 UTC |
| 29d815d | François Dupressoir | 26 February 2016, 11:36:38 UTC | Stabilize smt call in LazyEager | 26 February 2016, 11:36:38 UTC |
| 83edf64 | François Dupressoir | 26 February 2016, 11:32:29 UTC | Fixing RP_RF after Benjamin's changes to Birthday. Further extending Birthday to allow 0 queries. | 26 February 2016, 11:32:29 UTC |
| 87b373a | Benjamin Gregoire | 25 February 2016, 15:29:40 UTC | simplify the proof using advantage of the new fel. | 25 February 2016, 15:29:40 UTC |
| 5a66208 | Benjamin Gregoire | 25 February 2016, 12:32:12 UTC | Improve conditions for fel tactics. fix the corresponding proof. | 25 February 2016, 12:32:12 UTC |
| 33cc6c2 | Benjamin Gregoire | 25 February 2016, 10:00:54 UTC | fix commit fe97e0e2ebbb35a7fcdc77b022b19cadac8f7cf5. remove eprintf | 25 February 2016, 10:00:54 UTC |
| 784ba2c | Benjamin Gregoire | 25 February 2016, 09:19:01 UTC | [fix #17303] [fix #16416] fix bug in fel. | 25 February 2016, 09:19:01 UTC |
| 532c138 | Benjamin Gregoire | 25 February 2016, 06:04:17 UTC | Fix #17302. | 25 February 2016, 06:04:17 UTC |
| fe97e0e | Benjamin Gregoire | 24 February 2016, 17:33:43 UTC | bind NewMap with smt. Should be improved | 24 February 2016, 17:33:56 UTC |
| 20ebcf5 | Benjamin Gregoire | 24 February 2016, 15:20:43 UTC | add the constant function in NewMap | 24 February 2016, 17:33:56 UTC |
| ac1e46b | Pierre-Yves Strub | 24 February 2016, 15:25:01 UTC | Stdlib: sumidE (for reals). | 24 February 2016, 15:25:08 UTC |
| e35704b | Benjamin Gregoire | 24 February 2016, 15:05:11 UTC | Fix NewMap theory. Should make the link with smt. | 24 February 2016, 15:05:11 UTC |
| 4028dec | Benjamin Gregoire | 24 February 2016, 14:46:37 UTC | Fix smt call in Real.ec | 24 February 2016, 14:46:37 UTC |
| 0f9e6ab | Benjamin Gregoire | 24 February 2016, 13:11:16 UTC | Fix theories. | 24 February 2016, 13:12:12 UTC |
| dac6d8a | Benjamin Gregoire | 24 February 2016, 13:10:35 UTC | Fix bound in Fel. | 24 February 2016, 13:12:12 UTC |
| 590cf44 | Pierre-Yves Strub | 24 February 2016, 10:13:44 UTC | Revert "FEL: fix bug related to the move from felsum to bigi" This reverts commit 6162a495cfddd16a77873d3b63f82fb7040b9c62. | 24 February 2016, 10:13:44 UTC |
| 16a7d54 | Pierre-Yves Strub | 24 February 2016, 10:13:32 UTC | Revert "Fix stdlib w.r.t new FEL" This reverts commit 24a050a0586a0ccd9c9a04e49ee2904425861c85. | 24 February 2016, 10:13:32 UTC |
| 24a050a | Pierre-Yves Strub | 24 February 2016, 09:18:25 UTC | Fix stdlib w.r.t new FEL | 24 February 2016, 09:18:25 UTC |
| 6162a49 | Pierre-Yves Strub | 24 February 2016, 09:14:07 UTC | FEL: fix bug related to the move from felsum to bigi | 24 February 2016, 09:14:07 UTC |
| 11eccbe | Pierre-Yves Strub | 23 February 2016, 09:49:06 UTC | Abstract PCRE in the EcRegexp module | 23 February 2016, 09:50:36 UTC |
| ba9bd74 | Benjamin Gregoire | 22 February 2016, 08:34:13 UTC | improve error messages | 22 February 2016, 08:34:13 UTC |
| d9dbd96 | Benjamin Gregoire | 20 February 2016, 06:42:31 UTC | fix theories for the new module syntax | 20 February 2016, 06:42:31 UTC |
| 806353c | Benjamin Gregoire | 19 February 2016, 18:37:14 UTC | Improve typing of module and modify the syntax for declaration: module type T = { proc f() : unit }. module A (T : T) = {}. module type S0 = {}. module type S = { proc f() : unit }. module type C(X : S0) = { proc f() : unit }. module type C1(X : S) = { proc f() : unit }. module type C2(X1:S, X2:S0) = { proc f() : unit }. (* D takes an S, not just an S0 but D isn't a C, in the sense that it needs not just an S0 but an actual S to provide f() : unit *) module D (X : S) : T = { proc f() : unit = { X.f(); } }. module (D1:C1) (X : S) : T = { proc f() : unit = { X.f(); } }. (* (* This one raise an error *) module (D1':C) (X : S) : T = { proc f() : unit = { X.f(); } }. this module does not meet its interface: for argument X: S0 is not a subtype of S because procedure `f' is missing *) (* (* This one raise an error *) module (D4:C2)(X : S) = { proc f() : unit = { X.f(); } }. this module does not meet its interface: not the same number of module arguments *) (* (* This one raise an error *) module D3 (X : S) : C1 = { proc f() : unit = { X.f(); } }. this module does not meet its interface: not the same number of module arguments *) module (D2 : C,C1) (X : S0) = { proc f() : unit = { } }. | 19 February 2016, 18:37:14 UTC |
| 37ac8d8 | Pierre-Yves Strub | 18 February 2016, 08:18:40 UTC | `congr` now handles `if ... then ... else ...`. | 18 February 2016, 08:18:40 UTC |
| 6dc4662 | Pierre-Yves Strub | 17 February 2016, 19:43:18 UTC | In `apply`, try `iffRL` view before `iffLR`. | 17 February 2016, 19:43:18 UTC |
| ba7b059 | Pierre-Yves Strub | 17 February 2016, 17:39:04 UTC | fix bug in clear intro-pattern (was using H internally) | 17 February 2016, 17:39:04 UTC |
| f4c24e2 | Pierre-Yves Strub | 17 February 2016, 15:41:00 UTC | make use of new parsing rules for %r | 17 February 2016, 15:41:00 UTC |
| 78a448c | Pierre-Yves Strub | 17 February 2016, 15:40:12 UTC | fix parsing/printing of %r | 17 February 2016, 15:40:19 UTC |
| b80a21e | Benjamin Gregoire | 17 February 2016, 15:39:24 UTC | add missing trivial lemmas | 17 February 2016, 15:39:43 UTC |
| c468532 | Pierre-Yves Strub | 16 February 2016, 14:14:28 UTC | Change `rewrite` behaviour w.r.t. boolean rewriting. `rewrite` now tries to rewrite the equation `e = true` where `e` is the rewrite term before `rewrite` does its first operator unfolding. | 16 February 2016, 14:14:28 UTC |
| c3588f2 | Pierre-Yves Strub | 16 February 2016, 14:13:18 UTC | Tweaking vagrant GUI box. | 16 February 2016, 14:13:18 UTC |
| 19abbdd | Pierre-Yves Strub | 11 February 2016, 13:07:07 UTC | vagrant (GUI version) | 11 February 2016, 13:07:07 UTC |
| 09966ad | Pierre-Yves Strub | 10 February 2016, 07:46:11 UTC | removing old & unused Dmulti lib. | 10 February 2016, 07:46:11 UTC |
| a00a536 | François Dupressoir | 04 February 2016, 22:38:20 UTC | Random permutation some proofs. | 04 February 2016, 22:38:20 UTC |
| a858224 | François Dupressoir | 03 February 2016, 18:33:40 UTC | Strong PRP-PRF switching lemma works for 0 queries. | 03 February 2016, 18:33:40 UTC |
| e025b20 | François Dupressoir | 03 February 2016, 17:37:45 UTC | Adding library lemmas. | 03 February 2016, 17:38:07 UTC |
| d99c749 | Pierre-Yves Strub | 03 February 2016, 05:31:56 UTC | Fix casing of some filenames | 03 February 2016, 05:31:56 UTC |
| 3b2ac49 | Pierre-Yves Strub | 03 February 2016, 05:29:59 UTC | .gitignore: *smt, *.why (at root) | 03 February 2016, 05:29:59 UTC |
| 0be3935 | Pierre-Yves Strub | 03 February 2016, 05:28:47 UTC | Add missing copyright headers. | 03 February 2016, 05:28:47 UTC |
| 3f4f1e2 | Pierre-Yves Strub | 03 February 2016, 05:27:17 UTC | Add ProofGeneral mode in the auto-license targer. | 03 February 2016, 05:27:53 UTC |
| 2cbc445 | Pierre-Yves Strub | 03 February 2016, 05:27:06 UTC | Add a copyright to ProofGeneral mode. | 03 February 2016, 05:27:52 UTC |
| 96d7862 | Pierre-Yves Strub | 03 February 2016, 05:26:48 UTC | licensing script: support for elisp-style comments | 03 February 2016, 05:26:48 UTC |
| a47cd02 | Pierre-Yves Strub | 02 February 2016, 14:22:30 UTC | kill all axioms of Number | 02 February 2016, 14:22:30 UTC |
| 9331c08 | Pierre-Yves Strub | 02 February 2016, 13:32:40 UTC | killing some admits in NewDistr | 02 February 2016, 13:32:40 UTC |
| a6b0c38 | Pierre-Yves Strub | 02 February 2016, 13:23:39 UTC | Fixing admits in uniform distributions | 02 February 2016, 13:23:39 UTC |
| 20599b8 | Pierre-Yves Strub | 02 February 2016, 13:18:44 UTC | fix. mrat_eqP statement and prove it | 02 February 2016, 13:21:05 UTC |
| 71b03bd | François Dupressoir | 02 February 2016, 10:49:47 UTC | NewDistr: fixing drat spec. Also marking one place where a lemma from Distr is used and needs to be ported over. | 02 February 2016, 10:49:47 UTC |
| e71af98 | François Dupressoir | 02 February 2016, 10:04:35 UTC | NewDistr: taking over dmap/dapply from Distr. | 02 February 2016, 10:05:00 UTC |
| e3bed45 | François Dupressoir | 02 February 2016, 09:59:46 UTC | RealSeries: sum0 | 02 February 2016, 09:59:46 UTC |
| f8394a1 | Pierre-Yves Strub | 31 January 2016, 19:47:20 UTC | Vagrant: define 2 machines - easycrypt: shared folder, not X11, public base box - easycrypt-gui: cloned easycrypt, X11 (unity), home-made base box | 31 January 2016, 19:47:20 UTC |
| 74d19dd | Pierre-Yves Strub | 29 January 2016, 09:20:18 UTC | make von Neumann an abstract theory | 29 January 2016, 13:27:23 UTC |
| 09e92e3 | Pierre-Yves Strub | 29 January 2016, 07:40:57 UTC | Simplifying von Neumann example. | 29 January 2016, 13:27:23 UTC |
| acd25c7 | François Dupressoir | 28 January 2016, 10:40:01 UTC | Filling in an admit. This is to get familiar with summability. The proof needs looked at. | 28 January 2016, 10:40:01 UTC |
| f21ba4c | Pierre-Yves Strub | 27 January 2016, 16:17:20 UTC | internal API change for checking formula in *hl goals | 27 January 2016, 16:17:27 UTC |
| e379fcf | François Dupressoir | 27 January 2016, 09:41:04 UTC | Modernizing dinter and updating stdlib. | 27 January 2016, 09:41:04 UTC |
| 729da1a | Pierre-Yves Strub | 27 January 2016, 00:16:58 UTC | Cleaning a bit br93. (nothing deep) | 27 January 2016, 00:16:58 UTC |
| 60dffa8 | Pierre-Yves Strub | 27 January 2016, 00:10:32 UTC | BR93 is back- but still ugly. | 27 January 2016, 00:10:39 UTC |
| 4cafb1e | François Dupressoir | 26 January 2016, 18:48:48 UTC | One more example re-established. | 26 January 2016, 18:48:48 UTC |
| f4d55f0 | François Dupressoir | 26 January 2016, 18:43:59 UTC | Nits in DProd. | 26 January 2016, 18:43:59 UTC |
