| 9e556cc | nashpotato | 15 April 2020, 15:14:16 UTC | Resolved bug in multi-parameter instance declaration | 15 April 2020, 15:14:16 UTC |
| fed096f | nashpotato | 30 March 2020, 13:32:44 UTC | Minor changes | 30 March 2020, 13:32:44 UTC |
| a49837a | nashpotato | 30 March 2020, 13:21:06 UTC | Added illustrative type class example | 30 March 2020, 13:21:06 UTC |
| 66b3785 | nashpotato | 30 March 2020, 13:08:29 UTC | Minor changes | 30 March 2020, 13:08:29 UTC |
| a349ce7 | nashpotato | 30 March 2020, 12:50:07 UTC | Deprecating extends and error messages in parser | 30 March 2020, 12:50:07 UTC |
| 4da7be0 | nashpotato | 27 March 2020, 19:20:43 UTC | typeclass lemma name tagging | 27 March 2020, 19:20:43 UTC |
| 67ddb54 | nashpotato | 27 March 2020, 14:28:03 UTC | checking of lemmas for type classes and assigned operators | 27 March 2020, 14:28:03 UTC |
| 0c8155f | nashpotato | 26 March 2020, 13:19:54 UTC | Resolved parsing error, and terser syntax for type class instances | 26 March 2020, 13:19:54 UTC |
| 33e9a33 | nashpotato | 26 March 2020, 12:29:17 UTC | Synctactic changes to instance declaration | 26 March 2020, 12:29:17 UTC |
| 7339cba | nashpotato | 25 March 2020, 15:13:57 UTC | Modified the scoping of type class instance functions. Working towards checking that assigned axioms in instances are correct. | 25 March 2020, 15:13:57 UTC |
| e84f84f | nashpotato | 24 March 2020, 18:34:52 UTC | modified environment lookups of tc axioms and ops | 24 March 2020, 18:34:52 UTC |
| ec70a34 | nashpotato | 23 March 2020, 19:45:14 UTC | changes to axiom resolution. Still can't use axioms in proofs | 23 March 2020, 19:45:14 UTC |
| be9bf76 | nashpotato | 20 March 2020, 18:24:56 UTC | initial attempts at axiom parameter replacing | 20 March 2020, 18:24:56 UTC |
| 3e9e7dc | nash | 16 March 2020, 18:36:50 UTC | type class axiom resolution | 16 March 2020, 18:36:50 UTC |
| 0382ef9 | nash | 13 March 2020, 16:29:41 UTC | Deleted buffer file | 13 March 2020, 16:29:41 UTC |
| 5088e14 | nash | 13 March 2020, 16:29:02 UTC | Rewriting op declaration in type class definition | 13 March 2020, 16:29:02 UTC |
| da5f2ac | nash | 10 March 2020, 17:51:31 UTC | Location of type instance functions when referenced | 10 March 2020, 17:51:31 UTC |
| 7f6d8f8 | nash | 09 March 2020, 15:36:55 UTC | Phasing out of abstract/field/ring type class code. Working towards operator resolution | 09 March 2020, 15:36:55 UTC |
| e4a76e3 | nash | 06 March 2020, 20:18:08 UTC | Correct scoping modification with adding new operators in type class instance | 06 March 2020, 20:18:08 UTC |
| 7df2592 | nash | 06 March 2020, 15:57:48 UTC | Linking type class information into operator definition | 06 March 2020, 15:57:48 UTC |
| fbe2793 | nash | 06 March 2020, 14:02:40 UTC | Type class instance scoping | 06 March 2020, 14:02:40 UTC |
| 837984d | nash | 03 March 2020, 17:24:55 UTC | Testable type-class instantiation | 03 March 2020, 17:24:55 UTC |
| 7a72b63 | nash | 02 March 2020, 20:15:15 UTC | Typeclass instantiation with operator checking | 02 March 2020, 20:15:15 UTC |
| 3c8dde1 | nash | 29 February 2020, 21:28:25 UTC | Modifications towards instantiating typeclasses | 29 February 2020, 21:28:25 UTC |
| acf495e | nash | 21 February 2020, 11:22:29 UTC | Axiom support within type class declaration | 21 February 2020, 11:22:29 UTC |
| ffede89 | nash | 20 February 2020, 18:26:56 UTC | Compiler supports unbounded parameters in typeclass definitions | 20 February 2020, 18:26:56 UTC |
| b419a8a | nash | 20 February 2020, 17:18:07 UTC | Refactoring of handling construction of typeclasses in compiler | 20 February 2020, 17:18:07 UTC |
| 3d1e8fb | nash | 18 February 2020, 18:45:59 UTC | Initial steps towards unbounded parameters in type class declaration | 18 February 2020, 18:45:59 UTC |
| beb9e16 | nash | 18 February 2020, 17:35:28 UTC | Parser support for typeclass declaration with unbound type parameters | 18 February 2020, 17:35:28 UTC |
| 406260d | nash | 18 February 2020, 12:29:35 UTC | Initial type-class implementation that relies on bundling on record types | 18 February 2020, 12:29:35 UTC |
| 2287cf3 | nash | 14 February 2020, 20:58:35 UTC | Minor changes to typeclass use-case and goals | 14 February 2020, 20:58:35 UTC |
| 1d5059e | nash | 14 February 2020, 16:44:24 UTC | A few more descriptions of the typeclass use-case | 14 February 2020, 16:44:24 UTC |
| 74a85cf | nash | 14 February 2020, 15:18:56 UTC | Alternative dexample use case syntax, and typo | 14 February 2020, 15:18:56 UTC |
| 1a48afb | nash | 14 February 2020, 15:04:28 UTC | Example use case of ideal typeclass behaviour | 14 February 2020, 15:04:28 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 |
| 51f8ab0 | Pierre-Yves Strub | 18 October 2019, 08:11:34 UTC | .gitignore: .eco | 18 October 2019, 08:11:34 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 |
| 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 |
| 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 |
| 74207ab | Pierre-Yves Strub | 14 October 2019, 15:22:16 UTC | Remove debugging infos | 14 October 2019, 15:22:16 UTC |
| e023995 | Benjamin Gregoire | 14 October 2019, 12:09:21 UTC | New option from inline: [tuple]. Allows no to not use tuple assignments. | 14 October 2019, 12:27:51 UTC |
| a38b2e9 | Pierre-Yves Strub | 14 October 2019, 12:05:09 UTC | Fix handling of abstract theories imports. | 14 October 2019, 12:05:09 UTC |
| e12e2c2 | Pierre-Yves Strub | 14 October 2019, 08:38:48 UTC | This commit introduces two major features. - call by value reduction strategy. - user defined reduction rules. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr> | 14 October 2019, 08:39:46 UTC |
| 651df3f | Pierre-Yves Strub | 14 October 2019, 08:24:30 UTC | Solve tactic: apply is now done modulo delta | 14 October 2019, 08:24:30 UTC |
| e77d659 | Pierre-Yves Strub | 14 October 2019, 07:45:06 UTC | Misc. in SmtMap.ec | 14 October 2019, 07:45:06 UTC |
| 297f528 | Benjamin Gregoire | 14 October 2019, 07:09:06 UTC | Add interleave tactic | 14 October 2019, 07:10:05 UTC |
| ce9380d | Benjamin Gregoire | 14 October 2019, 06:41:25 UTC | Add transitivity * (transivity with generation of VC) | 14 October 2019, 06:42:35 UTC |
| 3b9667b | Pierre-Yves Strub | 14 October 2019, 06:27:33 UTC | Pragmas for printing pre/post as a list of their resp. conjunctions Pragmas are: PrPo:{pr,po}:{raw,ands} (Pragma system has been revamped by this commit) | 14 October 2019, 06:27:33 UTC |
| 66e7f99 | Pierre-Yves Strub | 14 October 2019, 05:55:05 UTC | Add decimal literals | 14 October 2019, 05:55:27 UTC |
| 115229e | Pierre-Yves Strub | 14 October 2019, 05:19:52 UTC | New intro pattern: [#|]. [#|] is a multi-case i-p (like [#]) that works also on on disjunctions. | 14 October 2019, 05:19:52 UTC |
| 1f45fde | Alley Stoughton | 10 October 2019, 11:50:05 UTC | refactor flagged map && PROM (#22) | 10 October 2019, 11:50:05 UTC |
| da0b25a | Francois Dupressoir | 10 October 2019, 07:49:06 UTC | Some extra lemmas on nseq (#26) | 10 October 2019, 07:49:06 UTC |
| 408d1b0 | Asif Mallik | 10 October 2019, 07:19:29 UTC | Add a more general version of dmap_uni (#30, #33) | 10 October 2019, 07:19:29 UTC |
| e9598be | Asif Mallik | 10 October 2019, 06:50:06 UTC | Add lemmas to filter noncontributing list items in bigops (#29) | 10 October 2019, 06:50:06 UTC |
| 8eb2491 | nitrogl | 09 October 2019, 19:14:57 UTC | Critical bugfix on dot-product (#34) * Critical bugfix on dot-product * CauchySchwarz is now an abstract theory | 09 October 2019, 19:14:57 UTC |
| c8257d3 | Pierre-Yves Strub | 02 October 2019, 06:23:52 UTC | Namespace for libraries and th. renaming | 02 October 2019, 06:23:52 UTC |
| f2bcd42 | Pierre-Yves Strub | 01 October 2019, 20:12:36 UTC | README: add a note about installing external deps for provers | 01 October 2019, 20:12:36 UTC |
| b6a4d3a | Pierre-Yves Strub | 01 October 2019, 14:26:02 UTC | Docker: bump Z3 version | 01 October 2019, 19:49:59 UTC |
| 4860685 | Pierre-Yves Strub | 01 October 2019, 10:54:42 UTC | Fetch more up-to-date smt binaries & compress unnecessary layers | 01 October 2019, 10:54:42 UTC |
| 88ded1b | Pierre-Yves Strub | 17 September 2019, 11:28:41 UTC | Fix "n?" intro pattern. | 17 September 2019, 11:28:41 UTC |
| 67392e1 | Cécile BARITEL-RUET | 16 September 2019, 12:54:52 UTC | RndProd : random oracle of a dprod | 16 September 2019, 12:56:20 UTC |
| a8e2f10 | Pierre-Yves Strub | 15 September 2019, 12:05:31 UTC | Fix defered start of provers | 15 September 2019, 16:59:56 UTC |
| 7641f4a | Benjamin Gregoire | 13 September 2019, 14:21:19 UTC | merge RndO and PROM | 13 September 2019, 14:21:19 UTC |
| 3d66517 | Benjamin Gregoire | 13 September 2019, 11:17:04 UTC | import DHIES | 13 September 2019, 11:17:04 UTC |
| 2c5203d | Pierre-Yves Strub | 13 September 2019, 11:01:05 UTC | more on lists (assoc, onth) + some facts on fmap/assoc | 13 September 2019, 11:01:20 UTC |
| 13b7bdd | Benjamin Gregoire | 13 September 2019, 09:49:36 UTC | add PKSMK | 13 September 2019, 09:49:36 UTC |
| 3bbc09b | Benjamin Gregoire | 13 September 2019, 09:39:56 UTC | add AEAD | 13 September 2019, 09:39:56 UTC |
| 746d64c | Pierre-Yves Strub | 13 September 2019, 08:30:58 UTC | Revert "remove duplicate lemma get_none -> domNE" This reverts commit 60d29c1f11f6c79824022608f9f83503d983ce61. | 13 September 2019, 08:30:58 UTC |
| 0344765 | Pierre-Yves Strub | 13 September 2019, 08:20:36 UTC | djoin and al | 13 September 2019, 08:20:36 UTC |
| 60d29c1 | Benjamin Gregoire | 13 September 2019, 06:39:19 UTC | remove duplicate lemma get_none -> domNE | 13 September 2019, 06:39:19 UTC |
| 0e717db | Pierre-Yves Strub | 12 September 2019, 21:17:28 UTC | pre/post selector Syntax if #rg?name where `name` is either `pre` or `post` and `rg` is a list of filters. | 12 September 2019, 21:18:52 UTC |
| 806fa6b | Pierre-Yves Strub | 12 September 2019, 20:57:15 UTC | Fix compilation | 12 September 2019, 20:57:15 UTC |
