| 31ae2ac | Benjamin Gregoire | 03 April 2024, 03:20:04 UTC | Merge branch 'main' into deploy-easyPQC | 03 April 2024, 03:20:04 UTC |
| 41c2667 | Pierre-Yves Strub | 29 March 2024, 21:31:04 UTC | This diff removes the cost logic. The cost logic suffers the following: - it does not implement what is needed, and is then barely used, - its implementation is invasive and duplicates some internal mechanisms The latter point slows down the development of new features. In conclusion, it has been decided not to wait for the new cost logic before removing the current implementation. | 02 April 2024, 15:42:03 UTC |
| 6ef627e | Pierre-Yves Strub | 02 April 2024, 15:41:24 UTC | Merge branch 'main' into easypqc | 02 April 2024, 15:41:24 UTC |
| c96ddd7 | Pierre-Yves Strub | 29 March 2024, 12:00:26 UTC | In cbn, restart reduction after a beta-reduction beta-reduction might have introduced a head-redex. | 29 March 2024, 12:31:44 UTC |
| 7bc148b | Pierre-Yves Strub | 31 December 2023, 10:11:31 UTC | Unify the behavior of simplify & /= w.r.t. auto-unfolding. Before this commit, `simplify` was not configured to unfold symbols marked for auto-unfolding. | 29 March 2024, 12:31:44 UTC |
| 5b48ec4 | Pierre-Yves Strub | 26 March 2024, 16:10:21 UTC | Stdlib: more results on `coprime` + modular equality | 26 March 2024, 18:01:44 UTC |
| 45f111d | Pierre-Yves Strub | 05 March 2024, 09:05:56 UTC | flake+opam-nix | 23 March 2024, 14:14:55 UTC |
| a7d2b01 | Pierre-Yves Strub | 05 March 2024, 09:05:21 UTC | Use dune-site to find resources (when installed) | 23 March 2024, 14:14:55 UTC |
| c5f30c8 | Alley Stoughton | 08 March 2024, 23:54:43 UTC | Added example usage of well-founded recursion and induction (#518) to examples directory. Cleaned up various things in WF.ec, including standardizing some terminology. | 08 March 2024, 23:54:43 UTC |
| a8274fe | Pierre-Yves Strub | 07 February 2024, 09:08:55 UTC | Optimize pretty-printing of notations The printer now does a eager filtering of notations (only notations that share the same head symbol as the printed formula are considered) The does not change the behavior of the pretty-printer, but greatly improves performance. | 07 February 2024, 16:39:46 UTC |
| f7992e1 | Cameron Low | 30 January 2024, 16:41:48 UTC | Remove module overriding when cloning a theory. (#458) | 30 January 2024, 16:41:48 UTC |
| ed61f01 | Pierre-Yves Strub | 11 December 2023, 11:05:03 UTC | New tactic: "case <-" This tactic "inlines" tuple assignments, i.e. it transforms ``` (lv1,...,lvn) <- (e1,...,en); ``` in ``` lv1 <- e1; ... lvn <- en; ``` | 30 January 2024, 15:30:11 UTC |
| 5903e1f | Pierre-Yves Strub | 11 December 2023, 10:54:25 UTC | Internal: minor additions to EcLowPhlGoal & EcMatching modules - EcMatching.Zipper.map - EcLowPhlGoal.{is_program_logic,hl_set_stmt} | 30 January 2024, 13:29:18 UTC |
| ff7b195 | Cameron Low | 19 January 2024, 12:29:44 UTC | New tactic: `rewrite equiv` The main idea is to provide a way to rewrite a procedure call, somewhere in a program, into a different procedure call, using an equiv. There is a variant provided to handle cases where the function to be rewritten to has different arguments and/or left-value than the instance provided. Syntax and variants: - Same arguments: `rewrite equiv[{m} p d lem]` - Different arguments: `rewrite equiv[{m} p d lem (a1, a2, ... :@ lv?)]` with - `m`: 1 or 2 - `p`: code position - `d`: direction, either `-` or nothing - `lem`: equiv for the rewrite - `ai`: an expression representing a function argument - `lv`: a left-value For example usage see: `tests/rwequiv.ec` or instances in the stdlib. | 29 January 2024, 14:29:12 UTC |
| 4401490 | Benjamin Grégoire | 29 January 2024, 13:23:41 UTC | Refactoring & simplfication of the low-level substitution. The low-level substitution is now in `EcCoreSubst` Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 29 January 2024, 13:31:44 UTC |
| 2b3bbad | Pierre-Yves Strub | 15 December 2023, 19:16:51 UTC | docker: fix opam init CL | 15 December 2023, 19:16:51 UTC |
| 12af606 | Cameron Low | 15 December 2023, 10:45:02 UTC | New tactic: `outline` (#473) The main idea is to provide an inverse to inline when proving an equiv. Currently, it supports basic procedure unification that requires manual selection of the program slice to unify with, as well as, requiring near exact matches on program structure. An optional return value can be supplied for situations where the return expression is just a program variable and needs to be renamed/deconstructed. There is also support for statement outlining although, this is more of a transitivity * with program slicing so may require change. Syntax and variants: - Procedure outlining: outline {m} [s - e] lv? <@ M.foo - Statement outlining: outline {m} [s - e] { s1; s2; ... } with - m: 1 or 2 - s,e: code position - M.foo: path to procedure - lv: a left-value when `s = e`, one can use `[s]` instead of `[s-s]` For example usage see: tests/outline.ec | 15 December 2023, 10:45:02 UTC |
| 1733c19 | Pierre-Yves Strub | 12 December 2023, 11:36:40 UTC | Docker: bump OCaml to 5.1.0 | 12 December 2023, 14:58:32 UTC |
| 943fc84 | François Dupressoir | 12 December 2023, 10:46:03 UTC | Bump provers to latest that succeeds, drop CVC4 Only Alt-Ergo needs kept back. | 12 December 2023, 13:46:57 UTC |
| 98139b7 | Pierre-Yves Strub | 12 December 2023, 10:54:24 UTC | nix-shell: remove why3 pin | 12 December 2023, 12:58:20 UTC |
| 736e322 | Francois Dupressoir | 12 December 2023, 12:18:17 UTC | remove a global axiom warning from the UC example (#502) | 12 December 2023, 12:18:17 UTC |
| 4c564f5 | Pierre-Yves Strub | 06 December 2023, 10:56:36 UTC | Internal API: process_Xhl_* This family of functions type-check a formula w.r.t. a memory that is infered from the program logic goal. The commit changes two things: - for prhl, its uses the same memory name as the one used in the program logic goal. (Previously, it was using `mhr`) - its returns the memory that has been used for the type-checking | 11 December 2023, 12:52:51 UTC |
| 4f02829 | Pierre-Yves Strub | 11 December 2023, 07:03:04 UTC | New command prefix: `fail` This prefix indicates that the following command should fail and that the error has to be ignored. It is an actual error if the command does not fail. In interactive mode, the error is printed (at [info]Â level). The main purpose of `fail` is to allow to write more precise unit tests where one can indicate which command shoud actually fail. | 11 December 2023, 10:07:50 UTC |
| 530a354 | Pierre-Yves Strub | 11 December 2023, 09:40:46 UTC | CI: do not skip successful duplicates If so, we can end with PR to protected branches that are blocked. | 11 December 2023, 09:50:22 UTC |
| bbe5e6d | Pierre-Yves Strub | 11 December 2023, 06:12:54 UTC | CI: unit tests In the automated tests, add a section `unit`for unit tests. The unit tests are checked by the CI. They can be run using `make unit`. | 11 December 2023, 09:11:50 UTC |
| 9c1ec6b | Pierre-Yves Strub | 07 December 2023, 13:30:49 UTC | CI: skip duplicated jobs | 07 December 2023, 15:57:05 UTC |
| 1d3dcaa | Benjamin Gregoire | 07 December 2023, 15:38:16 UTC | extend weakmem to hoare/choare/ehoare/equiv | 07 December 2023, 15:56:27 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 |
| 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 |
| 9275a29 | Pierre-Yves Strub | 19 October 2023, 13:35:01 UTC | Nits: choiceb induction principle | 19 October 2023, 14:57:04 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 |
