| 4391b04 | Pierre-Yves Strub | 12 November 2020, 11:00:16 UTC | basic results about minr | 12 November 2020, 11:00:16 UTC |
| 61de4b9 | Pierre-Yves Strub | 12 November 2020, 08:24:07 UTC | Fix "smt debug" | 12 November 2020, 08:24:20 UTC |
| b360fa8 | Benjamin Gregoire | 11 November 2020, 05:55:58 UTC | Fix bug in conseq | 11 November 2020, 05:56:42 UTC |
| ffad375 | Pierre-Yves Strub | 03 November 2020, 09:04:00 UTC | New option for SMT: "debug" | 03 November 2020, 09:04:00 UTC |
| 4ef4286 | Pierre-Yves Strub | 21 October 2020, 08:49:24 UTC | Fix dfold s.t. the functor takes the index | 21 October 2020, 08:49:24 UTC |
| 19c7285 | Pierre-Yves Strub | 20 October 2020, 09:34:40 UTC | New operator: dfold | 20 October 2020, 09:40:14 UTC |
| fa3853d | Pierre-Yves Strub | 15 October 2020, 10:30:04 UTC | README (nix) | 15 October 2020, 10:30:04 UTC |
| bc4f6df | Pierre-Yves Strub | 15 October 2020, 08:39:16 UTC | "={_}" now supports the construction "glob M \ { p1, p2, ... }" It stands for "glob M" without "p1, p2, ..." | 15 October 2020, 08:39:16 UTC |
| 22a8b51 | Pierre-Yves Strub | 14 October 2020, 09:10:10 UTC | better printing of modules bodies w.r.t. "import var" | 14 October 2020, 09:10:10 UTC |
| ca1f0d2 | Pierre-Yves Strub | 14 October 2020, 07:08:46 UTC | The command "import var" is now allowed at top-level | 14 October 2020, 07:08:46 UTC |
| b34c174 | Pierre-Yves Strub | 14 October 2020, 06:55:56 UTC | add alias "include var" that stands for "include" then "import var" | 14 October 2020, 06:55:56 UTC |
| c3114bd | Pierre-Yves Strub | 14 October 2020, 06:52:22 UTC | "import var" now takes a space-separated list of modules | 14 October 2020, 06:52:22 UTC |
| 4268b0f | Pierre-Yves Strub | 14 October 2020, 06:33:40 UTC | New command in modules: import var M This imports the variables of M in the active module scope. | 14 October 2020, 06:34:14 UTC |
| 7ba9ba4 | Pierre-Yves Strub | 11 October 2020, 07:27:44 UTC | Docker image: bump provers versions | 11 October 2020, 07:27:44 UTC |
| 7d8a513 | François Dupressoir | 10 October 2020, 11:22:49 UTC | Help smt along in brittle proofs These SMT fail when using: - Why3 1.3.1 - Z3 4.8.9 - CVC4 1.9 - Alt-Ergo 1.3.3 This appears to be bad interplay between the provers and this version of Why3: the proofs work with Why3 1.2 | 10 October 2020, 12:08:14 UTC |
| 469a12a | François Dupressoir | 09 October 2020, 16:20:54 UTC | easycrypt why3config uses --full-config | 09 October 2020, 16:20:54 UTC |
| ef6f0ba | Pierre-Yves Strub | 09 October 2020, 15:44:59 UTC | README: add --full-config option (why3 config) | 09 October 2020, 15:44:59 UTC |
| 6d31cc5 | Pierre-Yves Strub | 09 October 2020, 15:44:32 UTC | Update Dockerfile w.r.t new EasyCrypt repo layout | 09 October 2020, 15:44:32 UTC |
| e664da3 | Pierre-Yves Strub | 09 October 2020, 11:02:44 UTC | Docker: do not use easycrypt remote anymore | 09 October 2020, 11:02:44 UTC |
| ce70fa4 | Pierre-Yves Strub | 09 October 2020, 10:23:24 UTC | opam: change post-install message | 09 October 2020, 10:23:24 UTC |
| 6c03840 | Pierre-Yves Strub | 09 October 2020, 10:21:16 UTC | Fix travis configuration file w.r.t recent changes | 09 October 2020, 10:21:16 UTC |
| 44a728a | Pierre-Yves Strub | 09 October 2020, 10:16:24 UTC | Update README (no more external opam repo) & add missing opam fields | 09 October 2020, 10:16:58 UTC |
| e37a10c | Pierre-Yves Strub | 09 October 2020, 08:12:15 UTC | Import opam file s.t. travis can use it to update its dependencies | 09 October 2020, 08:41:05 UTC |
| c436fd4 | Pierre-Yves Strub | 09 October 2020, 07:16:05 UTC | Travis: update EasyCrypt dependencies before running tests | 09 October 2020, 08:41:05 UTC |
| 730f329 | Pierre-Yves Strub | 09 October 2020, 08:02:28 UTC | default.nix: remove restriction on Why3 version | 09 October 2020, 08:41:05 UTC |
| 8f33b95 | Stephane Graham-Lengrand | 07 October 2020, 23:19:47 UTC | First attempt at handling Why3 1.3.X | 09 October 2020, 08:41:05 UTC |
| 3007982 | Benjamin Gregoire | 14 September 2020, 13:36:41 UTC | fix default.nix | 14 September 2020, 13:36:41 UTC |
| d750dc3 | François Dupressoir | 15 June 2020, 15:10:39 UTC | Fix merge problem | 15 June 2020, 15:10:39 UTC |
| 66c830f | François Dupressoir | 15 June 2020, 14:55:33 UTC | Clean up the ROM libraries Now reduced to PROM as core, with ROM as a simpler interface. PROM is concrete to allow reuse of its flag type. Its internal theories, and ROM, are abstract to avoid growing forests of clones when using eager arguments. ROM now aligns with PROM in cloning interface: additional types `d_in_t` and `d_out_t` specify the distinguisher's interface. (This simplifies instantiation.) Some changes to type and oracle names to make them more explicit. Notably: - `from` is now `in_t`, - `to` is now `out_t`, (with associated change on name of distribution). | 15 June 2020, 14:55:33 UTC |
| 734e5bb | Pierre-Yves Strub | 10 June 2020, 17:03:25 UTC | Do no search for rewriting patterns modulo conversion. | 10 June 2020, 17:03:25 UTC |
| 41d0d08 | Pierre-Yves Strub | 10 June 2020, 14:44:03 UTC | Theory on square matrices (up to ring structure) `unit` predicate is still abstract. The link with the determinant has still to be done. | 10 June 2020, 14:44:03 UTC |
| 4b965ee | Pierre-Yves Strub | 10 June 2020, 14:13:50 UTC | Fix compilation | 10 June 2020, 14:13:50 UTC |
| c9641e4 | Pierre-Yves Strub | 10 June 2020, 09:53:25 UTC | Revert "Add user reductions for iteri" This reverts commit f693233ec9a7b33ba350d7b17e1d223f33d7fb56. | 10 June 2020, 09:53:35 UTC |
| bacb90b | Benjamin Gregoire | 10 June 2020, 08:02:11 UTC | in rewrite find occurences using alpha conversion first. | 10 June 2020, 09:41:40 UTC |
| ab61883 | Benjamin Gregoire | 10 June 2020, 07:46:56 UTC | add reduction for -i = i' | 10 June 2020, 07:47:46 UTC |
| 19c6c50 | Benjamin Gregoire | 10 June 2020, 07:45:48 UTC | remove duplicate declaration | 10 June 2020, 07:47:46 UTC |
| 6965ea6 | Pierre-Yves Strub | 10 June 2020, 07:46:26 UTC | binomial law + basic lemmas (full / support) | 10 June 2020, 07:46:26 UTC |
| 2064617 | Pierre-Yves Strub | 10 June 2020, 07:28:45 UTC | "search" now works with notations [fix #17317] | 10 June 2020, 07:28:49 UTC |
| 763732a | Benjamin Gregoire | 09 June 2020, 15:43:37 UTC | smt: do not filter wanted lemma | 09 June 2020, 15:43:43 UTC |
| f693233 | Pierre-Yves Strub | 09 June 2020, 15:39:58 UTC | Add user reductions for iteri | 09 June 2020, 15:39:58 UTC |
| 23b938a | Pierre-Yves Strub | 09 June 2020, 11:32:57 UTC | Refactor & merge min/max & integer/real pow. Co-Authored-By: Benjamin Gregoire <benjamin.gregoire@inria.fr> Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu> | 09 June 2020, 11:33:32 UTC |
| f71bd6c | Pierre-Yves Strub | 08 June 2020, 17:14:32 UTC | Some extra lemmas on Ring.expr Co-Authored-By: Benjamin Gregoire <benjamin.gregoire@inria.fr> Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu> | 08 June 2020, 17:14:32 UTC |
| 00ffc11 | Benjamin Gregoire | 27 May 2020, 13:08:56 UTC | add lemmas on bigi | 27 May 2020, 13:11:27 UTC |
| 53ed919 | Alley Stoughton | 22 May 2020, 22:12:19 UTC | Allows nosmt with all operators other than pure, abstract ones - i.e., with plain, axiomatized (including : {t | phi} as ax) and cases operators. When cloning, [op nosmt x = ...] is allowed, but nosmt can't be used with inlining mode. | 26 May 2020, 08:38:14 UTC |
| 170c443 | Benjamin Gregoire | 27 April 2020, 12:23:05 UTC | fix default.nix | 27 April 2020, 12:23:05 UTC |
| 58aaed4 | AntoineSere | 20 April 2020, 17:02:04 UTC | Merge pull request #42 from AntoineSere/eqvquo Added two useful lemmas to Quotient.ec | 20 April 2020, 17:02:04 UTC |
| ce4d827 | Antoine Séré | 20 April 2020, 15:04:39 UTC | Added two useful lemmas to Quotient.ec | 20 April 2020, 15:04:39 UTC |
| acfd4ea | Pierre-Yves Strub | 16 April 2020, 14:56:46 UTC | Definition of quotient types w.r.t. a equivalence relation | 16 April 2020, 14:56:46 UTC |
| 60a7d34 | Pierre-Yves Strub | 16 April 2020, 13:19:34 UTC | Finite groups, cyclic groups, Bezout. | 16 April 2020, 13:19:53 UTC |
| cdb2e6f | François Dupressoir | 16 April 2020, 10:45:54 UTC | Use arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '=' | 16 April 2020, 10:45:54 UTC |
| f44260c | Pierre-Yves Strub | 16 April 2020, 09:41:06 UTC | stdlib: distributions: dmap1E_can | 16 April 2020, 09:41:06 UTC |
| 94786bc | Pierre-Yves Strub | 16 April 2020, 09:40:44 UTC | stdlib: List: nth_default | 16 April 2020, 09:40:44 UTC |
| 136b237 | Pierre-Yves Strub | 15 April 2020, 09:39:30 UTC | lemma: fun_ext2 | 15 April 2020, 09:39:30 UTC |
| 5eba66b | Pierre-Yves Strub | 15 April 2020, 09:31:23 UTC | allow writing m.[i, j] in place of m.[(i, j)] | 15 April 2020, 09:31:23 UTC |
| 4882379 | Pierre-Yves Strub | 15 April 2020, 08:28:48 UTC | views: allow application of induction principle as a view | 15 April 2020, 08:28:48 UTC |
| 64d592d | Pierre-Yves Strub | 15 April 2020, 08:19:44 UTC | elim: search quantifier modulo reduction | 15 April 2020, 08:19:54 UTC |
| 3b8b038 | Adrien Koutsos | 14 April 2020, 15:08:58 UTC | Fixed unclosed box. (#41) Co-authored-by: Adrien Koutsos <akoutsos@users.noreply.github.com> | 14 April 2020, 15:08:58 UTC |
| f3581d5 | Pierre-Yves Strub | 10 April 2020, 09:56:42 UTC | binomial coefficients | 10 April 2020, 09:56:42 UTC |
| 21e8fce | Pierre-Yves Strub | 09 April 2020, 16:21:20 UTC | CI: move to slack notification | 09 April 2020, 16:21:20 UTC |
| d41a34d | Pierre-Yves Strub | 09 April 2020, 13:43:45 UTC | Matching for *hoareF & Pr | 09 April 2020, 13:44:05 UTC |
| 4062085 | bgregoir | 09 April 2020, 13:39:11 UTC | Merge pull request #40 from CohenCyril/nixfix default.nix: adding installFlags | 09 April 2020, 13:39:11 UTC |
| 21354f7 | Cyril Cohen | 08 April 2020, 15:21:04 UTC | default.nix: adding installFlags | 08 April 2020, 15:23:25 UTC |
| 149b09f | Pierre-Yves Strub | 28 March 2020, 08:13:02 UTC | User error message for map-style lvalue on unsupported assignment [fix #17412] | 28 March 2020, 08:13:21 UTC |
| b1b35e6 | Pierre-Yves Strub | 26 March 2020, 19:52:54 UTC | Internal: remove LvMap lvalue. | 26 March 2020, 19:52:54 UTC |
| 1a8d60a | Pierre-Yves Strub | 26 March 2020, 18:26:21 UTC | Revert "better conversion + simplify reduction algorithm." This reverts commit 11a875951d0f94381b22b362ddf8b0cc18f77886. | 26 March 2020, 18:26:21 UTC |
| 2a5b4f6 | Pierre-Yves Strub | 26 March 2020, 07:42:17 UTC | Only accepts Alt-Ergo from version 2.3.1 | 26 March 2020, 07:42:17 UTC |
| 22799f1 | Pierre-Yves Strub | 28 February 2020, 06:49:27 UTC | In `rewrite`, use a keyed matching algorithm for finding occurences. | 28 February 2020, 06:49:27 UTC |
| 10b9097 | Pierre-Yves Strub | 15 February 2020, 09:20:51 UTC | drop python2 support | 15 February 2020, 09:20:51 UTC |
| 44b23b5 | Pierre-Yves Strub | 15 February 2020, 07:19:25 UTC | Allow operators of the form 'n where n is a *fixed* natural number | 15 February 2020, 07:19:25 UTC |
| 11a8759 | Benjamin Gregoire | 14 February 2020, 08:36:31 UTC | better conversion + simplify reduction algorithm. | 14 February 2020, 08:36:31 UTC |
| 4f587f3 | Pierre-Yves Strub | 13 February 2020, 09:06:03 UTC | "hint simplify [reduce]" does one head reduction for finding the quantifers | 13 February 2020, 09:06:03 UTC |
| 2bbf3d3 | Pierre-Yves Strub | 13 February 2020, 08:38:38 UTC | Add new options to 'hint simplify': - reduce: equations are found up-to reduction - eqtrue: if no equations can be found, add a equation of the form (e = true) | 13 February 2020, 08:38:38 UTC |
| 2efb9e7 | François Dupressoir | 10 February 2020, 09:50:13 UTC | Consolidate PRP and PRF libraries Including weak PRP-PRF switching lemma, but not its strong version Squashed commit of the following: commit 005342f19a55b0ae01c88c0c729fdbad3f2519ff Merge: 5407570b 7325ae6d Author: François Dupressoir <fdupress@gmail.com> Date: Mon Feb 10 09:48:54 2020 +0000 Merge branch '1.0' into deploy-simpler-rp commit 5407570bbdeaee7b725f57fcdbbf764ff301ac9e Author: François Dupressoir <fdupress@gmail.com> Date: Fri Jan 24 12:00:21 2020 +0000 move towards merging PRF and RO also clean assignment notation commit 65e0c4eb8c702729500148e34900dc5971e583a7 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 14:14:29 2020 +0000 Integrate PRP-PRF switching lemma into PRP lib Not done for the strong version yet commit 456a7c96e40fa6827d92fbc36d8cd75fdd8abab1 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:40:25 2020 +0000 Simplifying the PRF interface No keys are needed for the ideal RP, The raw interface can be defined separately as needed. commit e7dea73e6eae21f192efc45f42e9cdc9e5ec4eb8 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:19:04 2020 +0000 Some nits commit 8bb90549b6084ea8189e3a4067a155f977ccd34a Author: François Dupressoir <fdupress@gmail.com> Date: Mon Jan 20 16:38:30 2020 +0000 Cleanup PRP/PRF and PRP-PRF | 10 February 2020, 09:50:13 UTC |
| 7325ae6 | Pierre-Yves Strub | 10 February 2020, 09:43:29 UTC | Refactor PlugAndPray | 10 February 2020, 09:45:08 UTC |
| 9e11412 | François Dupressoir | 16 January 2020, 20:48:25 UTC | Generalize arguments about sampling in dexcepted This pushes several complex low-level arguments related to sampling in restricted distributions into the related distribution file. This also generalizes these arguments, so that: - TwoStepSampling no longer requires a full distribution, - WhileSampling takes distributions and tests as procedure arguments rather than clone parameters. Specialized versions of theories and lemmas that reproduce the old behaviours are also included. The Dice_Sampling theory is removed, replaced with Dexcepted.WhileSamplingFixedTest (an abstract theory). Squashed commit of the following: commit e4bf1725f2a327bc58dda51d0079acb8dbb8fb1a Author: François Dupressoir <fdupress@gmail.com> Date: Thu Jan 16 20:40:23 2020 +0000 trailing white space in modified files commit 12d5ff0ae8607be10f7e925d1f0d44dd8e78dbde Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 15:49:41 2019 +0000 minor cleanup commit 7921a24e13e9f6d19ad02c0a22e8efb49bc37184 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 13:47:19 2019 +0000 More general ways of sampling out of a predicate TwoStep no longer requires losslessness. More sharing of proof could be obtained commit 393700f85b47b9d373be983b1451b08ae3d3be94 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:40:16 2019 +0000 PRP<->PRF uses generic resampling commit 74b9aef924cc313e358510ab9f83bc7410489db4 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:27:12 2019 +0000 Slight generalization: no longer need a full distribution commit 0853fc0e313bb6adac0ad956417480ebd70f512f Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 18:34:43 2019 +0000 Dexcepted: equivalence between two ways of sampling used in PRP<->PRF, but also in a current proof TODO: make PRP<->PRF use this | 16 January 2020, 20:48:25 UTC |
| cd341ca | Pierre-Yves Strub | 18 December 2019, 09:41:43 UTC | [done] solves context of the form [false |- G] [fix 17270] | 18 December 2019, 09:52:45 UTC |
| 050cada | Pierre-Yves Strub | 18 December 2019, 09:13:35 UTC | Remove dead code in 't_solve' | 18 December 2019, 09:52:45 UTC |
| 1ec24f8 | Benjamin Gregoire | 18 December 2019, 07:21:50 UTC | Improve />. Be sure that tactic crush (|>, />) does not transform the goal into umprovable one. | 18 December 2019, 07:48:19 UTC |
| eb9d7e3 | Benjamin Gregoire | 10 December 2019, 17:19:16 UTC | fix DHIES | 10 December 2019, 17:19:16 UTC |
| 7c400bd | Benjamin Gregoire | 10 December 2019, 15:36:45 UTC | fixing examples | 10 December 2019, 15:36:45 UTC |
| 943b847 | Benjamin Gregoire | 10 December 2019, 14:36:33 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-simple-stuff | 10 December 2019, 14:36:33 UTC |
| 3acf93f | Benjamin Gregoire | 10 December 2019, 14:35:50 UTC | fixing some examples | 10 December 2019, 14:35:50 UTC |
| 47c0851 | Pierre-Yves Strub | 10 December 2019, 14:34:52 UTC | Fix parser | 10 December 2019, 14:34:52 UTC |
| 0d33668 | Pierre-Yves Strub | 10 December 2019, 11:37:32 UTC | Printers for rewrite & solve databases | 10 December 2019, 14:00:13 UTC |
| 0b1128e | Benjamin Gregoire | 10 December 2019, 12:38:29 UTC | add lemma in "random" database | 10 December 2019, 12:38:29 UTC |
| babbac3 | Benjamin Gregoire | 10 December 2019, 12:33:05 UTC | Rename internal tactic t_auto into t_solve | 10 December 2019, 12:33:05 UTC |
| e6c9905 | Benjamin Gregoire | 10 December 2019, 12:29:05 UTC | improve automatic simplification of rnd rule for equiv | 10 December 2019, 12:29:05 UTC |
| 5d09cc2 | Benjamin Gregoire | 10 December 2019, 12:28:10 UTC | improve t_auto internal tactic | 10 December 2019, 12:28:10 UTC |
| 2b2b5b8 | Benjamin Gregoire | 09 December 2019, 15:43:32 UTC | automatically remove lossless condition in rnd{i} | 09 December 2019, 15:43:32 UTC |
| fa8b38b | Benjamin Gregoire | 07 December 2019, 09:46:33 UTC | add simplification rule for oget_some, oget_none | 07 December 2019, 09:46:33 UTC |
| 89e35d1 | Pierre-Yves Strub | 05 December 2019, 19:54:02 UTC | Compiles with OCaml 4.07 -> 4.09 (tested) | 05 December 2019, 19:54:02 UTC |
| 132968e | Pierre-Yves Strub | 02 December 2019, 10:06:01 UTC | remove failing SMT | 02 December 2019, 10:06:01 UTC |
| 60cfeb4 | Pierre-Yves Strub | 02 December 2019, 09:16:55 UTC | More results on dlet / dprod | 02 December 2019, 09:16:55 UTC |
| de1d4dc | Benjamin Gregoire | 27 November 2019, 21:10:03 UTC | Fix bug in eager if | 29 November 2019, 07:56:52 UTC |
| 78e8f6e | Pierre-Yves Strub | 26 November 2019, 13:30:43 UTC | Work of Roberto Metere on Sigma Protocols: - formalisation of the discrete logarithm assumption - formalisation of generic commitment schemes - formal verification of the Pedersen commitment scheme - formalisation of generic Sigma protocols - Sigma Protocol example: the Schnorr proof of knowledge Co-authored-by: Roberto Metere <r.metere2@ncl.ac.uk> | 26 November 2019, 13:31:58 UTC |
| add72dc | Pierre-Yves Strub | 14 November 2019, 10:15:31 UTC | Squashed commit of the following: [closes #17403] commit 55d4c60f675f8baf509682dd12e817377ba682e9 Author: Pierre-Yves Strub <pierre-yves@strub.nu> Date: Thu Nov 14 10:30:54 2019 +0100 Regeneralization of unspecified arguments in applicative views | 14 November 2019, 10:15:31 UTC |
| e58c36a | Francois Dupressoir | 07 November 2019, 16:19:02 UTC | add the full PRG tutorial from FOSAD (#35) | 07 November 2019, 16:19:02 UTC |
| e53aab7 | Pierre-Yves Strub | 25 October 2019, 15:59:30 UTC | Check .eco after the loader has been configured [fix #17400] | 25 October 2019, 15:59:33 UTC |
| 6489ade | Pierre-Yves Strub | 25 October 2019, 06:45:59 UTC | Make ECO handling more robust - do not fail when an .eco file is invalid - fix the reading of the `version' flag - erase staled .eco file - do not accept to compile files not handing with .ec or .eca - API: .mli file for EcEco [fix #17398] | 25 October 2019, 06:46:13 UTC |
| 10b2ab0 | Pierre-Yves Strub | 18 October 2019, 08:36:08 UTC | Add EC hash to .eco | 18 October 2019, 08:36:08 UTC |
