43d84a5 | Pierre-Yves Strub | 16 April 2020, 09:53:57 UTC | Matrix.eca: kill admits | 16 April 2020, 09:53:57 UTC |
09eb21d | Pierre-Yves Strub | 16 April 2020, 09:52:51 UTC | Merge branch '1.0' into deploy-theory-matrix-ring | 16 April 2020, 09:52:51 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 |
05e3caf | Pierre-Yves Strub | 16 April 2020, 06:34:14 UTC | Merge branch 'deploy-theory-matrix-ring' into 1.0-preview | 16 April 2020, 06:34:14 UTC |
f21502a | Pierre-Yves Strub | 16 April 2020, 06:33:53 UTC | vector/matrix & matrix/vector multiplication + L/R-module lemmas | 16 April 2020, 06:33:53 UTC |
e71f5fe | Pierre-Yves Strub | 15 April 2020, 19:08:08 UTC | Merge branch 'deploy-theory-matrix-ring' into 1.0-preview | 15 April 2020, 19:08:08 UTC |
40ed14d | Pierre-Yves Strub | 15 April 2020, 19:07:39 UTC | dmatrix | 15 April 2020, 19:07:39 UTC |
557fc21 | Pierre-Yves Strub | 15 April 2020, 12:39:10 UTC | square matrices from a non-commutative ring | 15 April 2020, 12:39:10 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 |
88814a4 | Pierre-Yves Strub | 10 April 2020, 09:57:07 UTC | Merge branch '1.0' into 1.0-preview | 10 April 2020, 09:57:07 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 |
bafcc56 | Pierre-Yves Strub | 08 April 2020, 07:28:44 UTC | Merge branch '1.0' into 1.0-preview | 08 April 2020, 07:28:44 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 |
527749b | Pierre-Yves Strub | 27 March 2020, 08:11:36 UTC | fix SecureChannel | 27 March 2020, 08:11:36 UTC |
f7f2a54 | Pierre-Yves Strub | 27 March 2020, 08:10:49 UTC | kill admits | 27 March 2020, 08:10:49 UTC |
13eeceb | Pierre-Yves Strub | 26 March 2020, 19:56:08 UTC | Merge branch '1.0' into 1.0-preview | 26 March 2020, 19:56:08 UTC |
b1b35e6 | Pierre-Yves Strub | 26 March 2020, 19:52:54 UTC | Internal: remove LvMap lvalue. | 26 March 2020, 19:52:54 UTC |
0d3cc8c | Pierre-Yves Strub | 26 March 2020, 19:44:25 UTC | Merge branch '1.0' into 1.0-preview | 26 March 2020, 19:44:25 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 |
762c088 | François Dupressoir | 11 February 2020, 19:18:33 UTC | Merge branch 'deploy-assign' into 1.0-preview | 11 February 2020, 19:18:33 UTC |
04b9a83 | François Dupressoir | 11 February 2020, 18:27:33 UTC | fix examples after rebase | 11 February 2020, 18:29:12 UTC |
bd9d006 | François Dupressoir | 27 January 2020, 17:36:46 UTC | clean up parser; $ is now an opchar | 11 February 2020, 18:19:38 UTC |
b40f781 | François Dupressoir | 21 January 2020, 16:13:44 UTC | forbid use of '=' for pWhile assignment | 11 February 2020, 18:19: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 |
f28d407 | François Dupressoir | 10 February 2020, 09:49:32 UTC | Merge branch 'deploy-simpler-rp' into 1.0-preview | 10 February 2020, 09:49:32 UTC |
005342f | François Dupressoir | 10 February 2020, 09:48:54 UTC | Merge branch '1.0' into deploy-simpler-rp | 10 February 2020, 09:48:54 UTC |
7325ae6 | Pierre-Yves Strub | 10 February 2020, 09:43:29 UTC | Refactor PlugAndPray | 10 February 2020, 09:45:08 UTC |
70ace4b | François Dupressoir | 31 January 2020, 20:42:02 UTC | Merge branch 'deploy-simpler-rp' into 1.0-preview | 31 January 2020, 20:42:02 UTC |
c3517dd | François Dupressoir | 31 January 2020, 20:40:57 UTC | Merge branch '1.0' into 1.0-preview | 31 January 2020, 20:40:57 UTC |
b12cc70 | François Dupressoir | 31 January 2020, 20:35:20 UTC | Merge branch 'deploy-dexcepted-sampling' into 1.0-preview Merge cleanup commit so 1.0 merges cleanly | 31 January 2020, 20:35:20 UTC |
5407570 | François Dupressoir | 24 January 2020, 12:00:21 UTC | move towards merging PRF and RO also clean assignment notation | 24 January 2020, 12:08:43 UTC |
65e0c4e | François Dupressoir | 21 January 2020, 14:14:29 UTC | Integrate PRP-PRF switching lemma into PRP lib Not done for the strong version yet | 21 January 2020, 15:06:07 UTC |
456a7c9 | François Dupressoir | 21 January 2020, 09:40:25 UTC | Simplifying the PRF interface No keys are needed for the ideal RP, The raw interface can be defined separately as needed. | 21 January 2020, 11:46:06 UTC |
e7dea73 | François Dupressoir | 21 January 2020, 09:19:04 UTC | Some nits | 21 January 2020, 09:19:04 UTC |
8bb9054 | François Dupressoir | 20 January 2020, 16:38:30 UTC | Cleanup PRP/PRF and PRP-PRF | 20 January 2020, 18:10:56 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 |
e4bf172 | François Dupressoir | 16 January 2020, 20:40:23 UTC | trailing white space in modified files | 16 January 2020, 20:40:34 UTC |
2b544f1 | François Dupressoir | 14 January 2020, 13:48:56 UTC | Merge branch 'deploy-dexcepted-sampling' into 1.0-preview | 14 January 2020, 13:48:56 UTC |
12d5ff0 | François Dupressoir | 19 December 2019, 15:49:41 UTC | minor cleanup | 19 December 2019, 15:55:02 UTC |
7921a24 | François Dupressoir | 19 December 2019, 13:47:19 UTC | More general ways of sampling out of a predicate TwoStep no longer requires losslessness. More sharing of proof could be obtained | 19 December 2019, 14:08:20 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 |
8b5dad5 | Pierre-Yves Strub | 18 December 2019, 09:14:26 UTC | Merge remote-tracking branch 'origin/1.0' into 1.0-preview | 18 December 2019, 09:14:26 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 |
40adf60 | Pierre-Yves Strub | 12 December 2019, 10:14:23 UTC | Merge branch '1.0' into 1.0-preview | 12 December 2019, 10:14:23 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 |
b9caec6 | Pierre-Yves Strub | 09 December 2019, 09:03:00 UTC | Merge branch '1.0' into 1.0-preview | 09 December 2019, 09:03:00 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 |
393700f | François Dupressoir | 05 December 2019, 21:40:16 UTC | PRP<->PRF uses generic resampling | 05 December 2019, 21:40:16 UTC |
74b9aef | François Dupressoir | 05 December 2019, 21:27:12 UTC | Slight generalization: no longer need a full distribution | 05 December 2019, 21:27:12 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 |
0853fc0 | François Dupressoir | 05 December 2019, 18:34:43 UTC | Dexcepted: equivalence between two ways of sampling used in PRP<->PRF, but also in a current proof TODO: make PRP<->PRF use this | 05 December 2019, 18:34:43 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 |
51f8ab0 | Pierre-Yves Strub | 18 October 2019, 08:11:34 UTC | .gitignore: .eco | 18 October 2019, 08:11:34 UTC |
d406e66 | Pierre-Yves Strub | 17 October 2019, 10:15:26 UTC | Merge branch '1.0' into 1.0-preview | 17 October 2019, 10:15:26 UTC |
f38226c | Pierre-Yves Strub | 17 October 2019, 10:08:11 UTC | Generate and use .eco files. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr> | 17 October 2019, 10:08:11 UTC |
5dd2bf6 | Pierre-Yves Strub | 16 October 2019, 09:10:34 UTC | Merge branch '1.0' into 1.0-preview | 16 October 2019, 09:10:34 UTC |
1c35db0 | Pierre-Yves Strub | 16 October 2019, 09:09:32 UTC | Fix t_auto. (was pruning opened goals) | 16 October 2019, 09:09:32 UTC |
97318f2 | Pierre-Yves Strub | 15 October 2019, 08:39:19 UTC | Merge branch 'deploy-wp-kw' into 1.0-preview | 15 October 2019, 08:39:19 UTC |
eb414fd | Pierre-Yves Strub | 15 October 2019, 08:39:00 UTC | Merge branch '1.0' into deploy-wp-kw | 15 October 2019, 08:39:00 UTC |
92a1a3d | Pierre-Yves Strub | 15 October 2019, 08:36:26 UTC | Merge branch 'deploy-match-in-stmt' into 1.0-preview | 15 October 2019, 08:36:26 UTC |
c9b3b96 | Pierre-Yves Strub | 15 October 2019, 08:29:21 UTC | match red in cbv | 15 October 2019, 08:29:21 UTC |
e318a15 | Pierre-Yves Strub | 15 October 2019, 07:59:36 UTC | Fix compilation after merge | 15 October 2019, 07:59:36 UTC |
f4a3767 | Pierre-Yves Strub | 15 October 2019, 07:54:08 UTC | Merge branch '1.0' into deploy-match-in-stmt | 15 October 2019, 07:54:08 UTC |
2139beb | Pierre-Yves Strub | 15 October 2019, 07:46:58 UTC | CI: test 1.0-preview | 15 October 2019, 07:46:58 UTC |
2f6587f | Pierre-Yves Strub | 15 October 2019, 07:09:54 UTC | In `case`, normalized 'glob' when searching for an inductive type. [fix #17391] | 15 October 2019, 07:09:54 UTC |