| 544680e | Benjamin Gregoire | 28 October 2023, 05:36:58 UTC | fix and simplify parser | 28 October 2023, 05:36:58 UTC |
| ed52616 | Benjamin Gregoire | 28 October 2023, 05:07:43 UTC | while + seq + fix conflict | 28 October 2023, 05:07:43 UTC |
| 90adafa | Benjamin Gregoire | 27 October 2023, 19:54:06 UTC | more syntax examples | 27 October 2023, 19:54:06 UTC |
| d3abcb4 | Benjamin Gregoire | 27 October 2023, 17:35:35 UTC | add rcond rule | 27 October 2023, 17:35:35 UTC |
| 943f268 | Benjamin Gregoire | 27 October 2023, 14:44:56 UTC | case + elim * + exists * + exlim + inlining | 27 October 2023, 14:44:56 UTC |
| 6d0f434 | Benjamin Gregoire | 27 October 2023, 05:05:52 UTC | fix equiv_init | 27 October 2023, 05:05:52 UTC |
| 20ed0f4 | Benjamin Gregoire | 27 October 2023, 04:48:22 UTC | add inlining | 27 October 2023, 04:48:22 UTC |
| e7f2fc5 | Benjamin Gregoire | 27 October 2023, 04:47:45 UTC | fix bugs in printing | 27 October 2023, 04:47:45 UTC |
| f8b6eeb | Benjamin Gregoire | 26 October 2023, 17:36:06 UTC | one sided rule for measure | 26 October 2023, 17:36:06 UTC |
| 05acd84 | Benjamin Gregoire | 26 October 2023, 13:36:59 UTC | rule for qinit and unitary | 26 October 2023, 13:36:59 UTC |
| e641397 | Benjamin Gregoire | 24 October 2023, 16:47:00 UTC | add mores rule for conseq, like P => q1 = q2 | P, r1 = r2 |=> P, r1, q1 = r2, q2 | 24 October 2023, 16:47:00 UTC |
| b8ebff0 | Benjamin Gregoire | 23 October 2023, 12:24:00 UTC | more on conseq and swap | 23 October 2023, 12:24:00 UTC |
| 7467f96 | Benjamin Gregoire | 16 October 2023, 06:30:27 UTC | read/write, need to be checked | 16 October 2023, 06:30:36 UTC |
| 2eb1694 | Benjamin Gregoire | 15 October 2023, 08:19:41 UTC | conseq for equivF and equivS | 16 October 2023, 06:30:36 UTC |
| 2558845 | Pierre-Yves Strub | 15 October 2023, 08:28:02 UTC | more unitary syntax | 15 October 2023, 08:28:02 UTC |
| 1a3e910 | Pierre-Yves Strub | 14 October 2023, 07:22:52 UTC | fix typing for unitary/measure | 14 October 2023, 07:22:52 UTC |
| 66d01e6 | Pierre-Yves Strub | 14 October 2023, 06:50:57 UTC | fix stdlib + parser | 14 October 2023, 06:51:07 UTC |
| 2468c5e | Benjamin Gregoire | 14 October 2023, 05:28:24 UTC | simplify printing | 14 October 2023, 05:28:24 UTC |
| f71b530 | Benjamin Gregoire | 14 October 2023, 05:12:04 UTC | equiv skip | 14 October 2023, 05:12:04 UTC |
| 8ea7241 | Benjamin Gregoire | 13 October 2023, 20:42:19 UTC | proc rule for defined function | 13 October 2023, 20:42:39 UTC |
| 1ceab33 | Pierre-Yves Strub | 13 October 2023, 19:57:27 UTC | WIP | 13 October 2023, 19:57:27 UTC |
| 56a5c6e | Pierre-Yves Strub | 13 October 2023, 16:30:53 UTC | WIP | 13 October 2023, 16:30:53 UTC |
| 6e71e4f | Pierre-Yves Strub | 13 October 2023, 15:44:56 UTC | WIP | 13 October 2023, 15:44:56 UTC |
| f5d5b47 | Pierre-Yves Strub | 13 October 2023, 14:08:15 UTC | PP | 13 October 2023, 14:08:15 UTC |
| ce19b24 | Benjamin Gregoire | 13 October 2023, 12:56:48 UTC | parser | 13 October 2023, 12:56:48 UTC |
| 3740f78 | Benjamin Gregoire | 13 October 2023, 06:29:59 UTC | WIP | 13 October 2023, 06:29:59 UTC |
| ecc6e3c | Benjamin Gregoire | 12 October 2023, 20:13:42 UTC | WIP | 12 October 2023, 20:13:42 UTC |
| 499e2cd | Benjamin Gregoire | 12 October 2023, 19:42:26 UTC | qequivF + qequivS : compilation work | 12 October 2023, 19:42:26 UTC |
| 1204364 | Benjamin Gregoire | 12 October 2023, 16:52:49 UTC | WIP | 12 October 2023, 16:52:49 UTC |
| 013e103 | Benjamin Gregoire | 12 October 2023, 13:54:58 UTC | WIP | 12 October 2023, 13:55:08 UTC |
| 2c9224e | Pierre-Yves Strub | 12 October 2023, 13:46:49 UTC | WIP (stdlib) | 12 October 2023, 13:46:49 UTC |
| 725ace9 | Pierre-Yves Strub | 12 October 2023, 13:28:01 UTC | WIP | 12 October 2023, 13:28:01 UTC |
| 5a6b4d9 | Pierre-Yves Strub | 12 October 2023, 10:04:42 UTC | Qinit @decl | 12 October 2023, 10:04:42 UTC |
| 2640590 | Pierre-Yves Strub | 12 October 2023, 09:51:47 UTC | Qinit | 12 October 2023, 09:51:47 UTC |
| 78b6f3b | Pierre-Yves Strub | 12 October 2023, 09:23:28 UTC | typing of calls | 12 October 2023, 09:23:28 UTC |
| f95a71e | Pierre-Yves Strub | 12 October 2023, 07:36:29 UTC | WIP (typing) | 12 October 2023, 07:36:29 UTC |
| c0b09e8 | Pierre-Yves Strub | 12 October 2023, 07:07:02 UTC | WIP (typing) | 12 October 2023, 07:07:02 UTC |
| 3c33782 | Pierre-Yves Strub | 12 October 2023, 06:00:08 UTC | WIP (typing + parser) | 12 October 2023, 06:00:17 UTC |
| cb5be7c | Benjamin Gregoire | 12 October 2023, 05:25:06 UTC | syntax example | 12 October 2023, 05:26:27 UTC |
| 59b32a7 | Pierre-Yves Strub | 12 October 2023, 05:09:51 UTC | parser | 12 October 2023, 05:09:51 UTC |
| dac67db | Pierre-Yves Strub | 12 October 2023, 05:05:22 UTC | typing of measure (missing disjointness) | 12 October 2023, 05:05:22 UTC |
| e1eb22f | Pierre-Yves Strub | 12 October 2023, 04:18:36 UTC | typing compiles | 12 October 2023, 04:18:36 UTC |
| d2453c4 | Pierre-Yves Strub | 11 October 2023, 08:45:36 UTC | WIP | 11 October 2023, 08:45:36 UTC |
| 01cf00a | Benjamin Gregoire | 11 October 2023, 07:27:42 UTC | WIP | 11 October 2023, 07:27:42 UTC |
| ecb9c18 | Pierre-Yves Strub | 10 October 2023, 20:49:41 UTC | fix prefix conflict check | 10 October 2023, 20:49:41 UTC |
| 2537c1a | Pierre-Yves Strub | 10 October 2023, 20:24:09 UTC | tentative implem of quantum_valid | 10 October 2023, 20:36:57 UTC |
| d3f2d83 | Benjamin Gregoire | 10 October 2023, 17:17:30 UTC | change Scall, add Squantum and Smeasure, compilation works | 10 October 2023, 17:17:46 UTC |
| ef58462 | Pierre-Yves Strub | 10 October 2023, 15:40:59 UTC | WIP (memory) | 10 October 2023, 15:41:11 UTC |
| c072e04 | Benjamin Gregoire | 10 October 2023, 09:37:09 UTC | WIP | 10 October 2023, 09:37:09 UTC |
| bd45a42 | Benjamin Gregoire | 10 October 2023, 09:18:33 UTC | WIP | 10 October 2023, 09:18:33 UTC |
| a214a56 | Pierre-Yves Strub | 11 September 2023, 14:24:03 UTC | opsem: generate spec lemmas | 26 September 2023, 11:14:56 UTC |
| 5e383f5 | Pierre-Yves Strub | 26 September 2023, 07:14:15 UTC | Internal: do not consider an applied abstract module as a non-functor abstract module fix #455 | 26 September 2023, 07:28:36 UTC |
| 13296e5 | Pierre-Yves Strub | 25 September 2023, 15:06:03 UTC | In subst, when crossing a binding, remove the bound variable. If not, the substitution can lead to name captures. | 25 September 2023, 18:44:32 UTC |
| 8fa2f94 | Pierre-Yves Strub | 22 September 2023, 15:07:33 UTC | op: fix creation of refined operators Do the operator substitution and then close the formula. | 22 September 2023, 19:27:28 UTC |
| 50bcef7 | Cameron Low | 18 September 2023, 12:05:16 UTC | Remove references | 22 September 2023, 11:49:02 UTC |
| ef42e9d | Cameron Low | 04 September 2023, 10:49:01 UTC | Fixed glob unsoundess through eager normalization of globs when type checking and substituting modules. | 22 September 2023, 11:49:02 UTC |
| 755fe93 | Benjamin Gregoire | 22 September 2023, 06:00:25 UTC | stdlib: new lemma on summable | 22 September 2023, 08:09:07 UTC |
| d5a04f5 | Vincent Laporte | 21 September 2023, 10:04:15 UTC | Read library paths from the EC_IDIRS/EC_RDIRS env. vars. Library paths can be specified using the environment variables EC_IDIRS and EC_RDIRS. They contain each a list of specifications separated by semicolumns (;). Each said specification is a path, optionally qualified (when present, the qualifier is followed by a colon (:)). Specifications given in the EC_IDIRS variable behave the same as the ones given in the idirs configuration entry or on the command line following a -I argument. Specifications given in the EC_RDIRS variable behave the same as the ones given in the rdirs configuration entry or on the command line following a -R argument. | 21 September 2023, 11:27:48 UTC |
| a9ae1ae | Benjamin Gregoire | 21 September 2023, 09:15:54 UTC | add more lemmas on converto | 21 September 2023, 09:32:44 UTC |
| c410d3c | Benjamin Gregoire | 21 September 2023, 09:04:50 UTC | remove hyp in normrV | 21 September 2023, 09:32:15 UTC |
| c60092d | Pierre-Yves Strub | 21 September 2023, 08:47:31 UTC | stdlib: limit of the inverse of a sequence | 21 September 2023, 09:08:56 UTC |
| eb00ea4 | Pierre-Yves Strub | 15 September 2023, 11:50:03 UTC | Fix the printing of operator bodies fix #442 | 15 September 2023, 12:25:39 UTC |
| 8746da3 | Pierre-Yves Strub | 14 September 2023, 09:18:37 UTC | cloning: fix regression bug in operators convertibilty check The check should use the full conversion. fix #437 | 14 September 2023, 10:51:55 UTC |
| 287106a | François Dupressoir | 30 August 2023, 15:12:52 UTC | [nix] vendor prover derivations | 13 September 2023, 20:57:12 UTC |
| 480c0ea | Pierre-Yves Strub | 28 August 2023, 15:37:04 UTC | Operator unfolding when applied to enough arguments When declaring an operator, it is now possible to specify which arguments are mandatory before an operator application is automtically unfolded during simplification. Syntax is: ``` op name (x1 : t1) (xp : tp) / (x_p+1 : t_p+1) ... = ... ``` where the optional `/` indicated that the operator `name` will be automatically unfolded when applied to at least `p` arguments. | 06 September 2023, 13:42:47 UTC |
| 8243791 | Pierre-Yves Strub | 05 September 2023, 15:52:17 UTC | [runtest]: new CLI argument --bin This argument tells `runtest` which binary to use for EasyCrypt. It takes precedence over what is found in the INI file (in default/bin). Moreover, `easycrypt runtest` automatically set --bin to itself. This allows to select the correct version of EasyCrypt without having to tweak the INI file accordingly. | 06 September 2023, 11:44:57 UTC |
| 7d59877 | Pierre-Yves Strub | 05 September 2023, 09:00:37 UTC | hint simplify now extracts rewriting rules from <=> | 05 September 2023, 12:52:06 UTC |
| bcdb9cb | Cameron Low | 04 September 2023, 13:10:46 UTC | Fixed the type given to a constructor when matching directly. | 04 September 2023, 16:43:08 UTC |
| 46d6948 | Pierre-Yves Strub | 28 August 2023, 14:00:06 UTC | Operators body can now be formulas When cloning a theory, inlined operator definitions must be expressions s.t. their substitution can be done in procedures bodies. | 04 September 2023, 08:59:09 UTC |
| 35e3849 | Oskar Goldhahn | 23 August 2023, 18:24:43 UTC | get rid of axiom in `Birthday` | 30 August 2023, 11:43:29 UTC |
| faedf01 | mm | 11 July 2023, 14:20:07 UTC | Additional List lemmas. Additional lemmas in StdBigop and RealSeries. | 29 August 2023, 12:08:44 UTC |
| c13b549 | Cameron Low | 19 July 2022, 13:48:12 UTC | [internal] EcSubst does not rely anymore on the low-level substitutions Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> | 28 August 2023, 10:36:37 UTC |
| 6a203df | François Dupressoir | 07 August 2023, 17:23:25 UTC | fix smt that regressed with z3 bump to 4.12.2 all else being equal, works with 4.12.1, fails with 4.12.2 fails with all other solvers | 12 August 2023, 08:57:48 UTC |
| ae29508 | François Dupressoir | 07 August 2023, 16:24:22 UTC | pin alt-ergo, z3 | 12 August 2023, 08:57:48 UTC |
| 705bafe | François Dupressoir | 07 August 2023, 16:20:33 UTC | refactor nix to avoid repetition | 12 August 2023, 08:57:48 UTC |
| 95cabb9 | François Dupressoir | 04 August 2023, 10:31:26 UTC | add support for test config 'report' option there is currently no way of asking for a report with 'easycrypt runtest' | 07 August 2023, 17:56:12 UTC |
| da3be5c | François Dupressoir | 04 August 2023, 10:30:36 UTC | [chore] whitespace | 07 August 2023, 17:56:12 UTC |
| a72dada | Yi Lee | 01 August 2023, 03:48:35 UTC | Propagate subtype changes to Word | 02 August 2023, 00:47:04 UTC |
| 917bba2 | Pierre Boutry | 20 July 2023, 13:30:54 UTC | Ring/field tactics available as soon as an instance is found. | 20 July 2023, 13:49:02 UTC |
| e75a7cf | Oskar Goldhahn | 12 July 2023, 22:38:59 UTC | get rid of unbounded smt calls outside examples | 20 July 2023, 13:22:13 UTC |
| 1bb2e2d | mm | 19 July 2023, 07:20:20 UTC | Additonal lemmas on fset equality establishing an equivalence, and additional lemma on perm_eq and undup (making the oflist_perm_eq lemma redundant). | 19 July 2023, 08:46:42 UTC |
| 6e066e6 | Pierre-Yves Strub | 13 July 2023, 11:06:46 UTC | Fix wording of error messages "function" -> "procedure" fix #417 | 13 July 2023, 11:07:33 UTC |
| add9232 | Christian Doczkal | 30 June 2023, 09:48:34 UTC | [chore] fix more raw smt calls | 11 July 2023, 20:01:13 UTC |
| 0c60516 | Christian Doczkal | 29 June 2023, 12:13:30 UTC | [chore] fix raw smt calls (theories/distributions) | 11 July 2023, 20:01:13 UTC |
| 757ec09 | François Dupressoir | 26 June 2023, 13:52:42 UTC | [chore] remove more raw smt calls | 29 June 2023, 13:20:43 UTC |
| 85d03a2 | Christian Doczkal | 29 June 2023, 11:18:26 UTC | [chore] fix some warnings and flaky smt calls (#408) | 29 June 2023, 11:18:26 UTC |
| cddd7d9 | Christian Doczkal | 28 June 2023, 14:58:53 UTC | [theories] define product using allpairs (#411) | 28 June 2023, 14:58:53 UTC |
| 60c3179 | Romain Tetley | 28 June 2023, 12:25:32 UTC | Renaming the easycrypt lib (making it easyier for external imports) (#410) | 28 June 2023, 12:25:32 UTC |
| 73ac095 | Pierre-Yves Strub | 27 June 2023, 06:47:59 UTC | proc op: add support for the "local" modifier | 27 June 2023, 13:55:48 UTC |
| 3693e61 | Christian Doczkal | 22 June 2023, 13:18:15 UTC | [theories] additional elimination rules for finite sums (#401) | 22 June 2023, 13:18:15 UTC |
| c0eeee4 | Pierre-Yves Strub | 21 June 2023, 10:19:54 UTC | Refactor out Fermat's little theorem from ZModP to IntDiv | 21 June 2023, 10:34:00 UTC |
| 4965377 | Yi Lee | 21 June 2023, 01:49:39 UTC | Prove Fermat's little theorem | 21 June 2023, 10:34:00 UTC |
| e38fac3 | Cameron Low | 13 June 2023, 20:55:00 UTC | Keep f_let_simp | 16 June 2023, 10:40:43 UTC |
| d1858f6 | Alley Stoughton | 05 June 2023, 14:42:45 UTC | Remove dead code relating to substitution; instead, the f_subst mechanism should be used. (And this is in fact done for simplification of let formulas in EcReduction.) | 16 June 2023, 10:40:43 UTC |
| 341cc08 | Benjamin Gregoire | 26 October 2022, 18:18:55 UTC | New inline tactic We realized that sometimes we want to inline everything besides one procedure and found that it is cumbersome to have to list everything that has to be inlined instead of listing what should remain as is. So we decided to add this to the current inline. We should have kept the previous use cases identical as supported by the fact that nothing broke while not touching any old ec files. In doing so, we also added the possibility to provide the name of a module leading to inlining all the procedure in this module. Finally, one can now provide the name of a procedure and it will inline all the procedures with that name regardless of the module in which they belong. As already mentioned, one can find examples at the following link. https://github.com/EasyCrypt/easycrypt/blob/deploy-inline/examples/tactics/inline.ec start with parsing pattern matching on inline add some examples fix | 16 June 2023, 10:39:43 UTC |
| f0e15c2 | Romain Tetley | 15 June 2023, 14:57:04 UTC | Turned the files in src into a lib called Core. (#397) * Turned the files in src into a lib called core. * Removed reference to dead code in dune file The file ecCoreHiPhl was removed as dead code, no need to exclude it in the dune file anymore. --------- Co-authored-by: Romain Tetley <rtetley@inria.fr> | 15 June 2023, 14:57:04 UTC |
| 8232d04 | Romain Tetley | 15 June 2023, 14:19:31 UTC | Remove dead code (#398) The file ecCoreHiPhl.ml seems to be dead code because: - It contains an open EcLogic which was deleted in 2014 (commit 6fe0ea944a53ffc89bdde9bb70f81629ff764c97) - The last time it was modified (apart from licence headers) was in 2013 (commit f2e05e2688ab1894daf760ed255060253839286c) | 15 June 2023, 14:19:31 UTC |
| b0eeedc | Yi Lee | 10 June 2023, 12:55:36 UTC | Take PolyReduce theory from Kyber project Add choice-based inverses and fix broken proofs from subtype changes Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 13 June 2023, 09:09:31 UTC |
| dfec6be | François Dupressoir | 27 March 2023, 08:59:03 UTC | restore name | 13 June 2023, 07:53:12 UTC |
| a4a0332 | François Dupressoir | 24 March 2022, 15:55:56 UTC | Tighten the ROM bad call results | 13 June 2023, 07:53:12 UTC |
