| 69d5154 | Pierre-Yves Strub | 21 August 2024, 09:37:01 UTC | stdlib: basic commutative algebra | 22 August 2024, 15:52:38 UTC |
| 791bfa7 | Matthias | 21 August 2024, 11:27:14 UTC | [External CI] Add XMSS and SPHINCS+ (#601) Co-authored-by: François Dupressoir <fdupress@gmail.com> | 21 August 2024, 11:27:14 UTC |
| 3a56e18 | Pierre-Yves Strub | 19 August 2024, 06:30:44 UTC | pretty printer: better handling of long module paths | 21 August 2024, 09:42:52 UTC |
| 352f3d8 | Pierre-Yves Strub | 20 August 2024, 06:45:02 UTC | Change default pp width from 20 to 80 | 20 August 2024, 17:47:52 UTC |
| 3928a0c | Pierre-Yves Strub | 02 August 2024, 08:33:45 UTC | Optimization hack for checking operator compatibility in clones The conversion check has a strategy to unfold the LHS before the RHS when checking that two maybe applied different operators are convertible. When cloning a theory with the "theory T <- U" stanza, the RHS of the conversion is an alias to the RHS. By swapping the two arguments, the convertibility check is immediate, while on the other case, both hands will be normalized. A proper way to solve this problem would be to have a more advanced unfold heuristic (by using a generation ID per operators or having more meta-information on the operators bodies) | 02 August 2024, 08:54:52 UTC |
| 65ac0be | Pierre-Yves Strub | 01 August 2024, 17:35:18 UTC | More results on lists (take/drop) and bit-encoding (bs2int/chunk) | 01 August 2024, 18:36:29 UTC |
| 5775739 | Pierre-Yves Strub | 21 July 2024, 19:26:40 UTC | runtest: display number of parallel jobs | 21 July 2024, 19:50:35 UTC |
| e4f28da | Pierre-Yves Strub | 20 July 2024, 08:52:54 UTC | Update docker image Simplify docker files + more provers | 20 July 2024, 18:11:48 UTC |
| fa96e87 | Pierre-Yves Strub | 19 July 2024, 19:51:42 UTC | [smt]: proper selection of SMT variant Why3 can define several variants (e.g. counterexamples, noBV). Currently, EasyCrypt select the first variant that comes in the prover list. From now on, the default variant (= empty name) is selected by default. It is also possible to provide the desired in the prover name (syntax = "prover[variant]", e.g. "Z3[noBV]"). This is compatible with the version selection (e.g. "Z3[noBV]@4.8") | 20 July 2024, 06:50:03 UTC |
| 6a29c79 | Pierre-Yves Strub | 19 July 2024, 18:24:48 UTC | [build]: configure the provers via easycrypt.project | 19 July 2024, 18:31:45 UTC |
| cf68b25 | Pierre-Yves Strub | 18 July 2024, 06:24:16 UTC | [stdlib]: more lemmas on distributions over lists dlist_dlist, dlist_insert | 19 July 2024, 18:05:16 UTC |
| c54ae97 | Pierre-Yves Strub | 18 July 2024, 06:32:34 UTC | [stdlib]: extra lemmas on dprod. dprod_dunit, dprod_marginal{L,R}, dprod_dmap_cross, dprod_dmap | 19 July 2024, 18:01:53 UTC |
| 72d8266 | Pierre-Yves Strub | 18 July 2024, 08:13:34 UTC | Fully check external project that compiles in <10 minutes. | 19 July 2024, 17:18:39 UTC |
| d5ccbf3 | Pierre-Yves Strub | 08 July 2024, 15:53:32 UTC | new vernacular: print axiom | 17 July 2024, 19:49:23 UTC |
| f7db115 | Pierre-Yves Strub | 17 July 2024, 18:55:59 UTC | [stdlib]: remove axioms (int + inductive schemes) | 17 July 2024, 19:40:53 UTC |
| b8fb10b | Pierre-Yves Strub | 17 July 2024, 14:47:56 UTC | [stdlib]: List: more lemmas on insert and related | 17 July 2024, 19:13:04 UTC |
| f1ddd44 | Pierre-Yves Strub | 17 July 2024, 08:14:11 UTC | Fixing bug in elim* when a bound is given. When a bound is given to elim*, do not try to destruct internal existentials. | 17 July 2024, 11:51:16 UTC |
| 6210a32 | Pierre-Yves Strub | 17 July 2024, 09:28:25 UTC | [stdlib]: iftrue / iffalse Very simple lemmas that allow to reduce if-expression. | 17 July 2024, 11:51:01 UTC |
| 2bb54a6 | Pierre-Yves Strub | 17 July 2024, 07:29:31 UTC | Fix spacing issues in pretty-printer | 17 July 2024, 07:29:31 UTC |
| f4beed3 | Pierre-Yves Strub | 16 July 2024, 12:53:06 UTC | New tags for operators: smt_opaque Operators' body are not sent to SMT solvers when tagged with "smt_opaque" | 16 July 2024, 18:10:57 UTC |
| 242e850 | Pierre-Yves Strub | 16 July 2024, 08:31:18 UTC | Remove the "nosmt" mechanism | 16 July 2024, 17:11:53 UTC |
| 9dee629 | François Dupressoir | 15 July 2024, 19:24:59 UTC | make dapply a parsing-only abbreviation | 15 July 2024, 19:34:37 UTC |
| a9e31ff | Pierre-Yves Strub | 05 July 2024, 08:07:13 UTC | [internal]: fix filtering as saved theory-related environments The bug takes its root in a poorly document API (EcPath.isprefix). The function now takes named arguments to make things clearer. | 05 July 2024, 08:39:20 UTC |
| 009198b | Pierre-Yves Strub | 17 June 2024, 14:56:43 UTC | [pretty-printing]: pretty-print in the theory environment of the target object The theory environment is the environment obtained just before the theory is closed. This environment is now saved when a theory is closed (regardless of the theory being abstract or not). This fixes two bugs: - hard failures when printing an abstract theory - long-object names | 03 July 2024, 19:19:11 UTC |
| b532306 | bgregoir | 03 July 2024, 04:56:17 UTC | simplify representation of memory restriction (#569) * simplify representation of memory restriction * fix typos in comments | 03 July 2024, 04:56:17 UTC |
| 86e8fc8 | Alley Stoughton | 20 June 2024, 17:30:31 UTC | [internal]: make public some functions needed by external projects | 21 June 2024, 12:00:14 UTC |
| d5d977d | Pierre-Yves Strub | 21 June 2024, 11:41:45 UTC | [ci]: never skips fetching external projects matrix | 21 June 2024, 11:45:06 UTC |
| e405758 | Pierre-Yves Strub | 20 June 2024, 09:23:50 UTC | [pretty-printing]: fix construction application display in match patterns | 20 June 2024, 15:00:49 UTC |
| e80ff3e | Pierre-Yves Strub | 17 June 2024, 19:51:05 UTC | [ci]: do not update opam This slows down the CI and brings little benefits. | 17 June 2024, 20:58:20 UTC |
| 9b940b4 | Pierre-Yves Strub | 23 May 2024, 07:30:10 UTC | Simplify/clean up memory/call restrictions. Memory restrictions can now only be decorators of modules types in top-level abstract module declarations / quantifications. Call restrictions can now only be decorators of procedure declarations in module types. | 17 June 2024, 20:23:03 UTC |
| 26689ed | Pierre-Yves Strub | 17 June 2024, 16:55:50 UTC | [ci]: remove ML-KEM ML-KEM is hard-failing on Github Actions for an obscure reason. Moreover, ML-KEM checking time, even in weak-check mode, is uterly long to check. While it is investigate & ML-KEM proofs are updated using the map-reduce tactics, I am removing it from the CI. It will be reintegrated ASAP. | 17 June 2024, 18:57:05 UTC |
| a8d385a | Pierre-Yves Strub | 12 June 2024, 07:33:29 UTC | More unit tests for `proc change` / `proc rewrite` | 14 June 2024, 20:06:59 UTC |
| 4631a0e | Pierre-Yves Strub | 10 June 2024, 19:19:04 UTC | proc change/rewrite: can be applied to if/while/match conditions/targets | 12 June 2024, 07:10:50 UTC |
| ddcc091 | Pierre-Yves Strub | 30 May 2024, 19:12:12 UTC | Reduce equalities between record literals. The reduction follows the current behavior for tuples. | 31 May 2024, 18:25:07 UTC |
| 2d87cff | Pierre-Yves Strub | 25 May 2024, 16:10:08 UTC | runtest: when EC is killed, display an error message | 25 May 2024, 16:10:08 UTC |
| 945c4e0 | Pierre-Yves Strub | 25 May 2024, 09:11:32 UTC | (undocumented) option to pass EC arguments via runtest | 25 May 2024, 09:16:23 UTC |
| 3c9a7e0 | Pierre-Yves Strub | 25 May 2024, 09:07:32 UTC | (undocumented) option that runs the GC compaction every `n` commands | 25 May 2024, 09:15:31 UTC |
| 3952606 | Pierre-Yves Strub | 25 May 2024, 07:47:25 UTC | Do not compute GC stats twice when printing memory statistics | 25 May 2024, 08:54:41 UTC |
| 0df8511 | Pierre-Yves Strub | 16 May 2024, 08:26:12 UTC | Remove non-strict proof mode. Non-strict proof-mode allows SMT failures to be catchable with `try` and affiliated. This tends to lead to hardly maintainable proofs and is not used anymore. The commits remove the internal handling of non-strict proof scripts, removing the `proof strict` / `proof -strict` syntax. The only leftover is the `try!` tactical that allows to catch SMT failures. It is useful for debugging purpose but should not remain in final scripts. | 16 May 2024, 08:49:52 UTC |
| 554909c | François Dupressoir | 15 May 2024, 13:09:15 UTC | [runtest] fix TTY detection so we might get useful CI logs! | 15 May 2024, 16:04:25 UTC |
| bde8207 | Yi Lee | 30 April 2024, 00:38:08 UTC | Change `axiom eq_choice` to lemma | 15 May 2024, 08:47:02 UTC |
| 0429a14 | Pierre-Yves Strub | 14 May 2024, 15:05:26 UTC | runtest: all to control the number of files checked in parallel For that purpose, a new CLI argument (-jobs) has been added to the `runtest` command. | 14 May 2024, 19:56:38 UTC |
| 11948bd | Pierre-Yves Strub | 03 May 2024, 15:17:19 UTC | [subst]: fix name capture When crossing a let-binding, remove the bound variables from the substitution in *all* situation. Fix #544 | 03 May 2024, 22:36:45 UTC |
| 28a9270 | François Dupressoir | 19 April 2024, 12:26:31 UTC | [external ci] add xsalsa security | 23 April 2024, 07:42:27 UTC |
| 66c2deb | Pierre-Yves Strub | 22 April 2024, 12:27:42 UTC | [ci] dump & upload errors | 22 April 2024, 20:00:46 UTC |
| 00cb1a4 | Pierre-Yves Strub | 15 April 2024, 06:51:47 UTC | tactic: match: out of TCB | 19 April 2024, 14:46:15 UTC |
| 3cfeb39 | François Dupressoir | 16 April 2024, 14:33:48 UTC | add cryptobox to the external CI | 19 April 2024, 12:27:16 UTC |
| 81926bc | François Dupressoir | 16 April 2024, 14:33:38 UTC | whitespace | 19 April 2024, 12:27:16 UTC |
| e2e4efb | Pierre-Yves Strub | 13 April 2024, 15:46:26 UTC | [ci] separate status for all external projects | 15 April 2024, 06:55:11 UTC |
| 51b60df | Pierre-Yves Strub | 12 April 2024, 12:49:37 UTC | [ci] add ML-KEM Check is done in weak-check mode. | 13 April 2024, 17:19:56 UTC |
| c0e1455 | Pierre-Yves Strub | 13 April 2024, 12:18:29 UTC | Fix HO matching HO matching was sometimes wrongly triggered | 13 April 2024, 12:44:07 UTC |
| 120f52c | Pierre-Yves Strub | 12 April 2024, 13:35:49 UTC | [ci] do not use set-output anymore Command has been marked as deprecated | 12 April 2024, 13:49:59 UTC |
| 3a0f7f0 | Pierre-Yves Strub | 12 April 2024, 13:15:18 UTC | [ci] upgrade actions - actions/checkout: v3 -> v4 - actions/upload-artifact: v3 -> v4 - cachix/install-nix-action: v20 -> v26 - cachix/cachix-action: v12 -> v14 | 12 April 2024, 13:41:58 UTC |
| b20b207 | Pierre-Yves Strub | 12 April 2024, 13:00:34 UTC | [ci] clone sub-modules when cloning external projects | 12 April 2024, 13:15:25 UTC |
| 9fa531e | François Dupressoir | 12 April 2024, 10:28:24 UTC | [ci] add SHA3 to external CI Proofs are checked in weak-mode. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 12 April 2024, 12:44:51 UTC |
| 1b24e75 | François Dupressoir | 12 April 2024, 10:26:31 UTC | [ci] external CI supports non-github repos Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 12 April 2024, 12:44:51 UTC |
| c9304d4 | Pierre-Yves Strub | 08 April 2024, 13:05:47 UTC | [ci] external projects description outside of the workflow file | 12 April 2024, 12:44:51 UTC |
| 8006327 | Pierre-Yves Strub | 12 April 2024, 12:26:44 UTC | Docker: fix CVC4 URL | 12 April 2024, 12:26:44 UTC |
| 08376c6 | Pierre-Yves Strub | 11 April 2024, 06:56:47 UTC | stdlib: bigop: split sums between even- and odd- indices | 11 April 2024, 07:07:14 UTC |
| 4201fdd | Pierre-Yves Strub | 05 April 2024, 11:57:25 UTC | Allow patterns in cut-rewrite. It is now possible to use pattern variables in cut-rewrite: ``` rewrite (_ : pattern = term) ``` See tests/rw_explicit_eq_with_pattern.ec for examples. | 08 April 2024, 12:44:57 UTC |
| 90e97e5 | Pierre-Yves Strub | 08 April 2024, 11:50:22 UTC | Internal: refactoring of matching algorithm This diff removes all the corner cases of the matching algorithm. The matching algorithm is now full-duplex (before, only the pattern was allowed to contain match variables) Matching performance is identical (test done on the examples & the standard library) Previous implementation was missing some trivial matching and the refactoring solves this issue. Some proofs might have to be fixed. | 08 April 2024, 12:27:49 UTC |
| 782f0a9 | Pierre-Yves Strub | 08 December 2023, 07:20:01 UTC | New tactic: "proc rewrite" This tactic allows to rewrite an expression in a statement. The syntax is: proc rewrite <side?> <codepos> <proof-term> This tactic relies on "proc change" and does not modify the TCB. Test plan: - unit test (tests/procrewrite.ec) | 08 April 2024, 12:10:15 UTC |
| b2d4cd7 | Pierre-Yves Strub | 05 April 2024, 14:34:09 UTC | Internal change: primitive notion of forall-bindings in proof terms | 08 April 2024, 11:48:29 UTC |
| e563f6c | Pierre-Yves Strub | 08 April 2024, 11:41:08 UTC | CI: add support for merge queue | 08 April 2024, 11:41:08 UTC |
| f27823e | Pierre-Yves Strub | 07 April 2024, 08:17:49 UTC | runtest: accept all options from the prover/loader group Fix #506 | 08 April 2024, 06:22:26 UTC |
| 30bfa95 | Pierre-Yves Strub | 11 December 2023, 10:58:49 UTC | New tactic: "proc change" This tactic allows to change an expression in a statement by some other expression. When applied, the user has to prove that the two expressions are equal (generalizing over all the program variables) This tactic applies to any program logic. The syntax is: proc change <side?> <codepos> : <form> This tactic is in the TCB. Test plan: - unit test (tests/prochange.ec) | 05 April 2024, 12:45:45 UTC |
| 4ccf645 | Pierre-Yves Strub | 05 April 2024, 11:39:43 UTC | runtest: fix regexp escapes + deprecation warnings | 05 April 2024, 12:31:27 UTC |
| ad79306 | mm | 14 July 2023, 13:12:24 UTC | DigitalSignatures.eca library | 05 April 2024, 12:21:31 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 |
| 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 |
