| 520e1cb | Antoine Séré | 12 August 2022, 17:30:24 UTC | Existence of a generator of the multiplicative group of a finite field proven | 12 August 2022, 17:30:24 UTC |
| 3bb6c06 | Antoine Séré | 11 August 2022, 20:52:17 UTC | Generator existence almost done | 11 August 2022, 20:52:17 UTC |
| cf153d9 | Antoine Séré | 11 August 2022, 11:37:20 UTC | Working on the generator existence proof | 11 August 2022, 11:37:20 UTC |
| 1d3343c | Antoine Séré | 10 August 2022, 21:26:04 UTC | Most admits done in Counting | 10 August 2022, 21:26:04 UTC |
| 14cc583 | Antoine Séré | 10 August 2022, 15:52:41 UTC | lcm added to IntDiv | 10 August 2022, 15:52:41 UTC |
| 189500a | Antoine Séré | 05 August 2022, 12:50:21 UTC | added coprimes stuff | 05 August 2022, 12:50:21 UTC |
| 6eda8b8 | Antoine Séré | 29 July 2022, 18:53:19 UTC | Fixed RingModule | 29 July 2022, 18:53:19 UTC |
| 441d28c | Antoine Séré | 29 July 2022, 18:32:22 UTC | Added to IntDiv, smt issue in one of the tests | 29 July 2022, 18:32:22 UTC |
| e22503c | Antoine Séré | 29 July 2022, 11:46:54 UTC | List lemmas done | 29 July 2022, 11:46:54 UTC |
| 5e518dd | Antoine Séré | 28 July 2022, 23:00:05 UTC | Many List lemmas added | 28 July 2022, 23:00:05 UTC |
| 678ff0c | Antoine Séré | 27 July 2022, 21:49:30 UTC | Many Counting lemmas | 27 July 2022, 21:49:30 UTC |
| 03fbf7a | Antoine Séré | 26 July 2022, 23:14:45 UTC | Added counting results | 26 July 2022, 23:14:45 UTC |
| 4d338d3 | Antoine Séré | 25 July 2022, 18:22:22 UTC | Number of roots of a polynomial bounded | 25 July 2022, 18:22:22 UTC |
| a11ce19 | Antoine Séré | 22 July 2022, 16:25:35 UTC | Added properties of polynomial evaluation | 22 July 2022, 16:25:35 UTC |
| bd0f6df | Antoine Séré | 22 July 2022, 14:21:50 UTC | SubType proofs done in FiniteRing | 22 July 2022, 14:21:50 UTC |
| 4d96403 | Antoine Séré | 21 July 2022, 15:10:32 UTC | Tests passed with unit modification | 21 July 2022, 15:10:32 UTC |
| 3f61c9b | Antoine Séré | 21 July 2022, 14:49:34 UTC | Fixed unit in Field | 21 July 2022, 14:49:34 UTC |
| cd2c663 | Antoine Séré | 18 July 2022, 18:19:35 UTC | order divides cardinal | 18 July 2022, 18:19:35 UTC |
| 35cccf9 | Antoine Séré | 18 July 2022, 11:49:59 UTC | Some admits fixed | 18 July 2022, 11:49:59 UTC |
| fdb98e4 | Antoine Séré | 18 July 2022, 11:23:34 UTC | Prime binomial coefficient lemmas proved | 18 July 2022, 11:23:34 UTC |
| e7a8875 | Antoine Séré | 13 July 2022, 12:02:52 UTC | Fixed checks | 13 July 2022, 12:02:52 UTC |
| e5850a0 | Antoine Séré | 13 July 2022, 11:48:44 UTC | Merged | 13 July 2022, 11:48:44 UTC |
| e377649 | Antoine Séré | 13 July 2022, 11:43:28 UTC | Merging with main | 13 July 2022, 11:43:28 UTC |
| 53f3e84 | François Dupressoir | 11 July 2022, 09:31:07 UTC | slightly reduce reliance on trivial SMT calls | 12 July 2022, 16:44:15 UTC |
| bef5649 | François Dupressoir | 12 May 2022, 13:34:34 UTC | unify meaning of `by []` `lemma ... by [].` is now short for `lemma ... by (by []).` (instead of `by smt.`) Fixes #191. | 12 July 2022, 16:44:15 UTC |
| 57be028 | François Dupressoir | 02 July 2022, 08:57:59 UTC | strip out code related to proc * | 12 July 2022, 16:38:49 UTC |
| df8a2f9 | François Dupressoir | 30 June 2022, 20:39:24 UTC | Remove parser support for `proc *` in module sigs A deeper removal is still needed to fully address #206. | 12 July 2022, 16:38:43 UTC |
| c954ae0 | Antoine Séré | 25 April 2022, 14:53:39 UTC | Hakyber jasmin eclib | 12 July 2022, 09:10:25 UTC |
| 5524b72 | Pierre-Yves Strub | 09 July 2022, 05:54:47 UTC | Fix ordering of variables in `rndsem` The chosen ordering is the order of appearance as a left-value in the program. fix #220 | 09 July 2022, 06:08:59 UTC |
| ca3d10a | Pierre-Yves Strub | 09 July 2022, 05:15:03 UTC | Fix naming issue for the [#] intro-pattern When having a conclusion of the form "forall x, E[x]", the intro-pattern [#] was renaming `x` as `_`. Internal: low-level intro tactic that returns the generated intro name fix #221 | 09 July 2022, 05:29:53 UTC |
| bccee8e | Antoine Séré | 01 July 2022, 11:01:29 UTC | Basis existence in finite fields done up to clone issue | 01 July 2022, 11:01:29 UTC |
| b0183c4 | Antoine Séré | 30 June 2022, 22:26:44 UTC | make check succeeds again | 30 June 2022, 22:26:44 UTC |
| 8ed8cfa | Antoine Séré | 30 June 2022, 22:15:13 UTC | Lemmas missing in List to complete proof of existence of a finite basis in finite fields | 30 June 2022, 22:15:13 UTC |
| e993546 | Antoine Séré | 30 June 2022, 16:23:51 UTC | RingModule lemmas are done | 30 June 2022, 16:23:51 UTC |
| f705062 | Antoine Séré | 30 June 2022, 11:26:41 UTC | RingModule hard proof done | 30 June 2022, 11:26:41 UTC |
| 5638ba0 | Antoine Séré | 29 June 2022, 23:07:58 UTC | RingModule free lemmas done up to one admit | 29 June 2022, 23:07:58 UTC |
| 878cd49 | Pierre-Yves Strub | 29 June 2022, 16:01:28 UTC | Dependent version of the multi-rnd tactic | 29 June 2022, 16:17:08 UTC |
| 9d00961 | Pierre-Yves Strub | 29 June 2022, 14:02:08 UTC | Extend `rnd` tactic s.t. it can handle multiple samplings / assignments Syntax is `rnd ... : pos1 pos2` and is only evailable for the pRHL variant. The tactic will first collapse all the instructions after `pos1` / `pos2` (in the left/right programs) before applying the `rnd` tactic. It is also possible to access this collapse phase with the new `rndsem` tactic. The syntax is: `rndsem side? codepos` | 29 June 2022, 14:12:18 UTC |
| f6ca7bf | Pierre-Yves Strub | 29 June 2022, 09:13:11 UTC | remove "rnd := f" syntax | 29 June 2022, 14:12:18 UTC |
| b953df7 | Antoine Séré | 29 June 2022, 10:02:49 UTC | RingModule free, gen and basis lemmas in progress | 29 June 2022, 10:02:49 UTC |
| dafa224 | Alley Stoughton | 28 June 2022, 16:48:30 UTC | Switched from x <> y being expanded by the parser to ! (x = y), and consequently having several explicit parsing rules (including one involving using it as a constructor in a match, which was buggy) to removing the special parsing treatment and adding it as an abbreviation. fixes #217 | 28 June 2022, 17:03:43 UTC |
| 1259339 | Antoine Séré | 23 June 2022, 19:39:10 UTC | Attack of the clones | 23 June 2022, 19:39:10 UTC |
| b266172 | Antoine Séré | 21 June 2022, 17:21:32 UTC | SubRing reformated | 21 June 2022, 17:21:32 UTC |
| b9dab00 | Antoine Séré | 21 June 2022, 13:14:49 UTC | Merged | 21 June 2022, 13:14:49 UTC |
| d492836 | Antoine Séré | 21 June 2022, 13:03:42 UTC | Prime decomposition lemmas done | 21 June 2022, 13:03:42 UTC |
| 445de07 | Pierre-Yves Strub | 21 June 2022, 09:24:33 UTC | SubRing/RingModule: refactoring | 21 June 2022, 09:24:33 UTC |
| bbfd949 | Antoine Séré | 20 June 2022, 08:03:59 UTC | clone issue in SubRing and RingModule | 21 June 2022, 08:08:09 UTC |
| b7d5480 | Antoine Séré | 19 June 2022, 17:47:30 UTC | SubRing and SubFiniteField separated, it all works, up to a lot of admits | 21 June 2022, 08:08:09 UTC |
| 15d3e27 | Antoine Séré | 18 June 2022, 20:51:10 UTC | FiniteField broken | 21 June 2022, 08:08:09 UTC |
| 51cce36 | Antoine Séré | 08 June 2022, 10:46:24 UTC | Proved some admits in Ideal, eqvX weakened because false | 21 June 2022, 08:08:09 UTC |
| ccfa6e1 | Antoine Séré | 08 June 2022, 07:17:56 UTC | Added the skeleton in Perms.ec | 21 June 2022, 08:08:09 UTC |
| 70b38fa | Antoine Séré | 03 June 2022, 17:23:57 UTC | Outline of the first steps of the finite field existence proof | 21 June 2022, 08:08:09 UTC |
| 547ffbf | Antoine Séré | 20 June 2022, 22:09:02 UTC | Prime decomposition done up to one admit. | 20 June 2022, 22:09:02 UTC |
| a2847c3 | Antoine Séré | 20 June 2022, 08:03:59 UTC | clone issue in SubRing and RingModule | 20 June 2022, 08:03:59 UTC |
| 721c491 | Antoine Séré | 19 June 2022, 17:47:30 UTC | SubRing and SubFiniteField separated, it all works, up to a lot of admits | 19 June 2022, 17:47:30 UTC |
| cbbee20 | Antoine Séré | 18 June 2022, 20:51:10 UTC | FiniteField broken | 18 June 2022, 20:51:10 UTC |
| 5aebad5 | Antoine Séré | 14 June 2022, 13:14:10 UTC | Merge branch 'main' into theory_finite_field | 14 June 2022, 13:14:10 UTC |
| cec6716 | Pierre-Yves Strub | 11 June 2022, 06:10:21 UTC | In loop fusion/fission, add more constraints on the epilog Loops' epilogs must now be deterministic and loop/calls-free. This forbids the following unsoundness: ``` require import AllCore DBool. module E = { var i,j : int proc foo () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; j <- j + 1; c <$ {0,1}; } return i = j; } proc bar () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; c <$ {0,1}; } c <- false; while (!c) { j <- j + 1; c <$ {0,1}; } return i = j; } }. equiv bad : E.foo ~ E.bar : true ==> ={res}. proof. proc. fission{1} 4!1 @1,2. by sim. qed. ``` Fix #210 | 11 June 2022, 06:10:21 UTC |
| 1f8da33 | Pierre-Yves Strub | 11 June 2022, 06:01:44 UTC | Add an option that allows EasyCrypt to connect to an external Why3 server The option is -why3server and takes the unix domain socket path as argument. | 11 June 2022, 06:02:38 UTC |
| 38c4947 | Pierre-Yves Strub | 10 June 2022, 09:40:59 UTC | Clear the blocked signals mask on startup. In some circumstances, the inherited mask disturbs Why3 server. | 10 June 2022, 09:40:59 UTC |
| 6afdf81 | Antoine Séré | 08 June 2022, 10:46:24 UTC | Proved some admits in Ideal, eqvX weakened because false | 08 June 2022, 10:46:24 UTC |
| 4da2e4f | Antoine Séré | 08 June 2022, 07:17:56 UTC | Added the skeleton in Perms.ec | 08 June 2022, 07:17:56 UTC |
| 7fed186 | Pierre-Yves Strub | 04 June 2022, 11:20:29 UTC | new command: exit (stops EasyCrypt) | 04 June 2022, 11:20:29 UTC |
| 2a444f9 | Antoine Séré | 03 June 2022, 17:23:57 UTC | Outline of the first steps of the finite field existence proof | 03 June 2022, 17:23:57 UTC |
| 4e97480 | Pierre-Yves Strub | 03 June 2022, 12:06:31 UTC | [runtest]: use all cores by default | 03 June 2022, 12:06:38 UTC |
| 0ea3d99 | Quentin Carbonneaux | 02 June 2022, 08:54:48 UTC | rename depext to opam-depext The `depext` package fails to install with recent versions of opam. The fix suggested in the package information is to use the renamed package `opam-depext` instead. | 02 June 2022, 11:26:56 UTC |
| d083fc5 | Pierre-Yves Strub | 01 June 2022, 06:32:41 UTC | [dune]: (re)-codesign promoted binaries Dune substitution breaks the initial code-signing. The problem has been acknowledge by the dune team and should be fixed on their side at some point. | 01 June 2022, 06:32:41 UTC |
| e45a54c | Adrien Koutsos | 20 May 2022, 13:26:31 UTC | smt option to dump a smt query to a file | 20 May 2022, 14:00:39 UTC |
| 90826b1 | Vincent Laporte | 18 May 2022, 22:23:30 UTC | default.nix: use why3 1.5.0 | 19 May 2022, 08:16:49 UTC |
| b44893a | Pierre-Yves Strub | 17 May 2022, 15:17:18 UTC | [runtest]: exit with a non-zero exit status in case of failure. | 18 May 2022, 05:22:28 UTC |
| 168c6d7 | Pierre-Yves Strub | 17 May 2022, 15:16:35 UTC | [runtest]: do not display warnings/infos as errors Fix #198 | 18 May 2022, 05:22:28 UTC |
| 3c1476b | Alley Stoughton | 17 May 2022, 13:54:38 UTC | Fix pretty-printing of projections. Former printer was using an invalid priority for projections. Fixes #200 | 17 May 2022, 14:43:37 UTC |
| 24b0ce7 | Alley Stoughton | 16 May 2022, 17:16:29 UTC | Updating README for current why3 requirements. | 17 May 2022, 08:36:55 UTC |
| 762988d | François Dupressoir | 16 May 2022, 09:27:43 UTC | mark `transpose` as parse-only We have suffered long enough | 16 May 2022, 09:27:43 UTC |
| b44bcba | Pierre-Yves Strub | 14 May 2022, 21:49:26 UTC | [stdlib]: more lemmas around dfun. Main result is the equivalence between sampling a function and sampling a function in the same function space, but for one point that is sample a posteriori. | 14 May 2022, 21:58:53 UTC |
| 2e5cc0e | Pierre-Yves Strub | 14 May 2022, 21:39:35 UTC | [stdlib] new lemmas around dscalar & dlet. | 14 May 2022, 21:58:53 UTC |
| b66eb5c | Pierre-Yves Strub | 14 May 2022, 21:38:13 UTC | [stdlib]: new operator for updating a function at one point. Notation is "f.[x <- v]" for the function that is equal to "f" but at value "x" where it returns "v". | 14 May 2022, 21:58:45 UTC |
| b6f7335 | Pierre-Yves Strub | 09 May 2022, 12:13:47 UTC | New `runtest` script - more readable output (for tty / no-tty) - more readable report | 14 May 2022, 21:49:14 UTC |
| c629679 | Pierre-Yves Strub | 14 May 2022, 21:32:09 UTC | Fix pretty-printing of mixfix notations. The notation was not printed when the operators was over-applied. E.g., f.[x <- v] y was printed "_.[_<-_]" f x v y. | 14 May 2022, 21:32:09 UTC |
| 164a167 | Pierre-Yves Strub | 13 May 2022, 07:23:39 UTC | README: remove "make PREFIX=" | 13 May 2022, 07:23:39 UTC |
| a76ddc7 | Pierre-Yves Strub | 13 May 2022, 07:23:18 UTC | README: configuration Why3 using EasyCrypt | 13 May 2022, 07:23:18 UTC |
| 5ff9d70 | Pierre-Yves Strub | 13 May 2022, 07:18:32 UTC | When configuring Why3, create the configuration file destination directory first | 13 May 2022, 07:18:32 UTC |
| 92941b1 | Pierre-Yves Strub | 12 May 2022, 06:59:09 UTC | [stdlib]: link Finite & FinType. | 12 May 2022, 07:12:12 UTC |
| 1e12363 | François Dupressoir | 11 May 2022, 13:32:14 UTC | error on potential procedure call in RHS of <- If the RHS of a <- fails to typecheck as an expression but could be a procedure call, mention <@ as an alternative | 12 May 2022, 06:49:18 UTC |
| 5d030a1 | François Dupressoir | 12 May 2022, 06:47:58 UTC | Enforce separation between <- and <@ more strictly This removes the error message when the RHS is a procedure call. This allows us to accept things that were rejected before, when a procedure and operator share their name. A follow-up may re-enable it. Fix #189 | 12 May 2022, 06:49:18 UTC |
| cdc065e | Christian Doczkal | 11 May 2022, 08:47:50 UTC | [stdlib]: add various small lemmas (Logic, FSet, Distr, DInterval, Bigop) - #non-backward-compatible: this commits generalizes `Bigop.reindex` to restrict the cancellation property to the index list. | 12 May 2022, 06:43:29 UTC |
| de42d06 | Pierre-Yves Strub | 10 May 2022, 12:14:09 UTC | Change configuration file resolution Do not consider locations that point to non-existing files. The configuration file location is now printing by the `config` command. | 10 May 2022, 12:14:09 UTC |
| f1ce5ae | Pierre-Yves Strub | 09 May 2022, 10:46:10 UTC | Finite.to_seq: now have a body based on choiceb Co-authored-by: Christian Doczkal <christian.doczkal@mpi-sp.org> | 09 May 2022, 11:54:13 UTC |
| a49a0ac | Pierre-Yves Strub | 05 May 2022, 06:55:44 UTC | Bump Why3 version from 1.4.x to 1.5.0 fix #184 | 05 May 2022, 13:58:12 UTC |
| a1eeaf0 | Pierre-Yves Strub | 05 May 2022, 08:02:38 UTC | [github-action]: do not start as root This requires a modification of the docker image s.t. the user UID is compatible with the one used by Github Action | 05 May 2022, 13:14:49 UTC |
| aab2ca4 | Pierre-Yves Strub | 27 April 2022, 12:46:45 UTC | Use local configuration file in priority | 27 April 2022, 12:46:45 UTC |
| dbdca26 | Pierre-Yves Strub | 27 April 2022, 12:46:13 UTC | Fic computation of source root for local builds | 27 April 2022, 12:46:13 UTC |
| 577c882 | Pierre-Yves Strub | 27 April 2022, 09:41:00 UTC | Fix the license announced in the banner | 27 April 2022, 09:48:51 UTC |
| 8f314e4 | Pierre-Yves Strub | 26 April 2022, 08:49:07 UTC | Makefile | 26 April 2022, 08:49:07 UTC |
| 89df8ee | Adrien Koutsos | 25 April 2022, 15:42:10 UTC | move cost axioms in abstract theories (fix #175) | 26 April 2022, 08:43:31 UTC |
| 9c03562 | François Dupressoir | 11 January 2022, 16:03:51 UTC | Reject `x <- RHS` when `RHS` is a procedure call | 22 April 2022, 11:13:38 UTC |
| 7b70089 | François Dupressoir | 14 December 2021, 15:43:15 UTC | Improve parser for anonymous proc parameters Anonymous and named parameters can be mixed for abstract procedures. Corner cases are not exercised by test suites and may crop up. Resolves #108. | 22 April 2022, 10:53:46 UTC |
| 74a4d02 | Pierre-Yves Strub | 30 March 2022, 09:20:02 UTC | Fixing list of authors | 22 April 2022, 06:59:36 UTC |
| 2c53183 | Pierre-Yves Strub | 07 April 2022, 16:12:18 UTC | [env]: fully head-norm the type before fetching its top-level decl. This commit involves a lot of code motion. partially address #121 | 22 April 2022, 06:59:22 UTC |
| bfd4f84 | Pierre-Yves Strub | 07 April 2022, 15:11:17 UTC | [reduction]: in cbv, fix handling of stack arguments The API was s.t. it was possibly to detect a non-empty stack as an empty one. Partially address #121 | 22 April 2022, 06:59:22 UTC |
