| ec65ae2 | Benjamin Gregoire | 30 January 2024, 10:16:11 UTC | . | 30 January 2024, 10:16:11 UTC |
| 8b5d405 | Benjamin Gregoire | 30 January 2024, 10:09:44 UTC | . | 30 January 2024, 10:09:44 UTC |
| 0b5fe57 | Benjamin Gregoire | 11 December 2023, 09:43:18 UTC | remove unecessary assert | 11 December 2023, 09:43:18 UTC |
| bf70e2c | Benjamin Gregoire | 09 December 2023, 07:47:32 UTC | add small remarks | 09 December 2023, 07:47:32 UTC |
| 648f621 | Benjamin Gregoire | 08 December 2023, 06:48:38 UTC | make the use of freshen explicite, we should inspect when freshen is really necessary | 08 December 2023, 06:48:38 UTC |
| df768b5 | Benjamin Gregoire | 07 December 2023, 15:46:34 UTC | remove deadcode, try to use ecCoreSubst as much as possible in ecReduction | 07 December 2023, 15:46:34 UTC |
| 7814666 | Benjamin Gregoire | 07 December 2023, 13:07:48 UTC | refresh memory binding in hoare judgment when necessary | 07 December 2023, 13:07:48 UTC |
| db28551 | Benjamin Gregoire | 06 December 2023, 06:01:10 UTC | fix last rebase | 07 December 2023, 12:56:12 UTC |
| 2e5c61a | Benjamin Gregoire | 05 December 2023, 20:27:55 UTC | fix rebase | 07 December 2023, 12:56:11 UTC |
| af51c86 | Benjamin Gregoire | 05 December 2023, 16:32:56 UTC | fix rebase | 07 December 2023, 12:56:11 UTC |
| 5cd0e48 | Benjamin Gregoire | 05 December 2023, 16:31:54 UTC | fix rebase | 07 December 2023, 12:56:10 UTC |
| 90c7b86 | Benjamin Gregoire | 05 December 2023, 07:23:49 UTC | remove option in f_subst_tvar | 07 December 2023, 12:56:10 UTC |
| e010664 | Benjamin Gregoire | 05 December 2023, 03:58:48 UTC | remove unused function | 07 December 2023, 12:56:10 UTC |
| 85974e7 | Benjamin Gregoire | 05 December 2023, 03:39:26 UTC | introduce fs_fv | 07 December 2023, 12:56:09 UTC |
| 3e4b2fb | Benjamin Gregoire | 04 December 2023, 13:27:23 UTC | small internal refactoring for mod subst | 07 December 2023, 12:56:09 UTC |
| 8e9c440 | Benjamin Gregoire | 04 December 2023, 07:19:39 UTC | simplify instantiation of schema | 07 December 2023, 12:56:08 UTC |
| 6388953 | Benjamin Gregoire | 03 December 2023, 08:03:32 UTC | small refactoring | 07 December 2023, 12:56:08 UTC |
| 95ff65f | Benjamin Gregoire | 03 December 2023, 06:26:42 UTC | introduce Tvar.f_subst | 07 December 2023, 12:56:07 UTC |
| e550dfd | Benjamin Gregoire | 03 December 2023, 06:11:04 UTC | small cleanup | 07 December 2023, 12:56:07 UTC |
| 4bc4c4d | Benjamin Gregoire | 03 December 2023, 05:17:25 UTC | rename subst_xpath into x_subst | 07 December 2023, 12:56:06 UTC |
| 1e2f70a | Benjamin Gregoire | 03 December 2023, 05:10:08 UTC | rename subst_me into me_subst | 07 December 2023, 12:56:06 UTC |
| 3f1365f | Benjamin Gregoire | 02 December 2023, 21:53:51 UTC | rename subst_gty into gty_subst | 07 December 2023, 12:56:05 UTC |
| 5bfdf05 | Benjamin Gregoire | 02 December 2023, 21:42:55 UTC | rename subst_oi into oi_subst | 07 December 2023, 12:56:05 UTC |
| 9b4ade2 | Benjamin Gregoire | 02 December 2023, 21:36:04 UTC | rename subst_ty into ty_subst | 07 December 2023, 12:56:04 UTC |
| 32890d0 | Benjamin Gregoire | 02 December 2023, 21:26:45 UTC | rename subst_m into m_subst | 07 December 2023, 12:56:04 UTC |
| 57158af | Benjamin Gregoire | 02 December 2023, 20:50:15 UTC | rename subst_e into e_subst | 07 December 2023, 12:56:03 UTC |
| 7ee880f | Benjamin Gregoire | 02 December 2023, 20:04:21 UTC | rename subst_stmt into s_subst | 07 December 2023, 12:56:03 UTC |
| 43982dd | Benjamin Gregoire | 02 December 2023, 19:53:28 UTC | rename subst_lpattern into lp_subst | 07 December 2023, 12:56:03 UTC |
| d12d925 | Benjamin Gregoire | 02 December 2023, 19:30:44 UTC | small cleanup | 07 December 2023, 12:56:02 UTC |
| 6aba0e8 | Benjamin Gregoire | 02 December 2023, 17:57:50 UTC | remove f_subst_init_rm | 07 December 2023, 12:56:02 UTC |
| 7f7ce50 | Benjamin Gregoire | 02 December 2023, 17:10:47 UTC | start removing use of f_subst_init_rm | 07 December 2023, 12:56:01 UTC |
| 6841edb | Benjamin Gregoire | 02 December 2023, 16:49:47 UTC | remove e_subst_init | 07 December 2023, 12:56:00 UTC |
| 4e8b595 | Benjamin Gregoire | 02 December 2023, 16:04:03 UTC | new interface to f_subst_init | 07 December 2023, 12:56:00 UTC |
| e6e7023 | Benjamin Gregoire | 02 December 2023, 15:32:34 UTC | remove type ty_subst and e_subst | 07 December 2023, 12:55:59 UTC |
| b98d6b8 | Benjamin Gregoire | 02 December 2023, 13:09:30 UTC | merge all subst types | 07 December 2023, 12:55:59 UTC |
| 03b81a6 | Benjamin Gregoire | 02 December 2023, 12:14:55 UTC | type f_subst become abstract | 07 December 2023, 12:55:58 UTC |
| 9acb9b0 | Benjamin Gregoire | 02 December 2023, 10:20:08 UTC | type e_subst become abstract | 07 December 2023, 12:55:58 UTC |
| e7995db | Benjamin Gregoire | 02 December 2023, 09:45:28 UTC | add missing files ... | 07 December 2023, 12:55:57 UTC |
| b45b94a | Benjamin Gregoire | 02 December 2023, 09:39:38 UTC | ty_subst is abstract | 07 December 2023, 12:55:57 UTC |
| febb46d | Benjamin Gregoire | 02 December 2023, 09:24:42 UTC | move substitution function to EcCoreSubst | 07 December 2023, 12:55:56 UTC |
| 6576223 | Benjamin Gregoire | 06 December 2023, 15:12:04 UTC | Fix reduction w.r.t. memory types. This commit fixes two bugs: - the memory types (in all hoare logic constructor) were not taken into account in conversion. - the bounded memories where not substituted for alpha conversion. | 07 December 2023, 10:35:52 UTC |
| 9e85ab1 | Benjamin Gregoire | 06 December 2023, 17:00:18 UTC | Add tactic `weakmem` This tactic allows to weaken the memory of a phoare hypothesis by adding new variables to it. This tactic is needed in the while rule for phoare, when one wants to apply the induction hypothesis & the memories are not compatible. Currently, the convertibility check does not enforce that memories are equal, but a to-come PR is going to fix that point. | 07 December 2023, 10:21:48 UTC |
| d248e73 | Pierre-Yves Strub | 06 December 2023, 05:52:29 UTC | rndsem: new version that only computes the distribution for used variables This version was already available internally. This commits only add the needed syntax for accessing it. The syntax is: `rndsem* <options>`. closes #415 | 06 December 2023, 15:25:53 UTC |
| 7c0adea | Pierre-Yves Strub | 05 December 2023, 16:20:13 UTC | In substitutions, lazyly refresh the codomain of the univar map This map is allowed to do name capture and is hence sensitive to bound variables renaming. | 05 December 2023, 16:33:38 UTC |
| dd02a37 | Pierre-Yves Strub | 05 December 2023, 10:08:59 UTC | In view application, close cut formula after substitution If not, we are creating a capture. The bug is hidden because we are not using a refreshing substitution in this case. | 05 December 2023, 14:03:35 UTC |
| 0de7f16 | Pierre-Yves Strub | 04 December 2023, 14:17:14 UTC | Compile in `dev` mode by default. Until now, `make` was building EasyCrypt in release mode. The set of warning flags in release mode is weaker then in development mode. Switching to dev mode caused the apparition of some warnings. This commit fixes them. | 04 December 2023, 15:39:51 UTC |
| 068fdd9 | Pierre-Yves Strub | 01 December 2023, 21:49:53 UTC | nix: do not pin provers versions nix-flake should be used to pin provers to a given version. | 02 December 2023, 11:10:24 UTC |
| c0376b7 | Pierre-Yves Strub | 02 December 2023, 08:00:15 UTC | Bump the minimal version of Why to 1.7 This allows us to use more recent versions of the provers. The docker images have been updated accordingly. Docker now comes with the following provers: - Z3 4.12.2 - CVC4 1.8 - CVC5 1.0.6 - Alt-Ergo 2.5.2 | 02 December 2023, 08:24:16 UTC |
| 14a397c | Pierre-Yves Strub | 01 December 2023, 17:16:43 UTC | runtest: new option: why3 (why3 configuration file location) | 01 December 2023, 21:44:34 UTC |
| 23e603e | Pierre-Yves Strub | 01 December 2023, 20:13:32 UTC | runtest: allows to specify provers from the CLI | 01 December 2023, 21:27:04 UTC |
| 42a7841 | Pierre-Yves Strub | 01 December 2023, 16:42:37 UTC | runtest: do not try to load pyyaml when reporting is disabled | 01 December 2023, 16:53:46 UTC |
| 15f0751 | Pierre-Yves Strub | 01 December 2023, 15:12:27 UTC | Allows selecting a prover by its version number. Syntax is name@version. The selected prover is the prover with name `name` and with the lowest version that is greater (or equal) than `version`. For example, if Z3 4.8.0, Z3 4.8.2 & Z3 4.12.2 are installed, Z3@4.8 selects Z3 4.8.2. | 01 December 2023, 16:15:50 UTC |
| 27edb8a | Pierre-Yves Strub | 30 November 2023, 07:12:31 UTC | opam: allow Why3 1.7.x | 30 November 2023, 08:37:08 UTC |
| d9d7bcf | Alley Stoughton | 28 November 2023, 18:44:30 UTC | Removed two unused type declarations. | 28 November 2023, 20:14:47 UTC |
| d43887b | Benjamin Gregoire | 25 November 2023, 09:48:25 UTC | Share the definition of the datatypes in EcAst.ml | 25 November 2023, 10:05:04 UTC |
| b79290f | Pierre-Yves Strub | 24 November 2023, 14:35:35 UTC | SMT timeout can now be configured in INI files The configuration key is "timeout" | 24 November 2023, 17:30:52 UTC |
| 3be7cb9 | Pierre-Yves Strub | 24 November 2023, 14:20:34 UTC | Support project-local ini files EasyCrypt now reads project-local files for getting its configuration settings. This configuration file takes precedence over the system-level configuration file. The project-local configuration file is named 'easycrypt.project'. It is identical to the system-level configuration file. When compiling a file, the configuration file is searched upward from the target file directory. When ran in interactive mode, the configuration file is searched upward from the current working directory. Note that when ProofGeneral starts EasyCrypt, the working directory is set to the directory of the focused file. | 24 November 2023, 17:25:58 UTC |
| 9fd429a | Pierre-Yves Strub | 06 November 2023, 14:12:01 UTC | When rewriting in the local env, do not fail on identity rewriting fix #463 | 08 November 2023, 17:06:32 UTC |
| ff7b698 | AVANZINI Martin | 26 October 2023, 17:56:30 UTC | added adversary and qselect examples | 08 November 2023, 11:03:26 UTC |
| 99ec9f4 | Benjamin Gregoire | 11 October 2023, 11:29:39 UTC | ehoare Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Martin Avanzini <martin.avanzini@inria.fr> | 08 November 2023, 11:03:26 UTC |
| 9275a29 | Pierre-Yves Strub | 19 October 2023, 13:35:01 UTC | Nits: choiceb induction principle | 19 October 2023, 14:57:04 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 |
