ffe0656 | Pierre-Yves Strub | 18 November 2021, 14:23:49 UTC | New command: locate [partial-qualid] This command allows to locate and print the fullname & shortest name of an operator, a lemma or a type declaration. fix #82 | 18 November 2021, 14:23:49 UTC |
92f23db | Pierre-Yves Strub | 18 November 2021, 12:06:18 UTC | Add the project name in dune-project This is needed by "dune subst" ref #99 | 18 November 2021, 12:06:45 UTC |
5e3929a | Pierre-Yves Strub | 18 November 2021, 12:06:09 UTC | remove debugging code | 18 November 2021, 12:06:09 UTC |
17e143c | Pierre-Yves Strub | 17 November 2021, 15:41:35 UTC | | 17 November 2021, 15:41:35 UTC |
b38a5aa | Pierre-Yves Strub | 17 November 2021, 15:39:37 UTC | | 17 November 2021, 15:39:37 UTC |
dfb413d | Pierre-Yves Strub | 17 November 2021, 15:35:07 UTC | fix opam package (do not do "dune subst") | 17 November 2021, 15:35:07 UTC |
0a2d4ad | Pierre-Yves Strub | 17 November 2021, 07:42:42 UTC | [build] use dune to install & find resources | 17 November 2021, 08:23:14 UTC |
31ce231 | François Dupressoir | 06 November 2019, 20:46:14 UTC | [SmtMap] add has, find and some lemmas these are focused on a specific proof and deserve expanding, fleshing out and cleaning up | 17 November 2021, 07:51:50 UTC |
229ac7a | Pierre-Yves Strub | 17 November 2021, 06:24:47 UTC | Remove EcFortune | 17 November 2021, 06:24:47 UTC |
02082bd | Pierre-Yves Strub | 17 November 2021, 06:22:22 UTC | Update copyright | 17 November 2021, 06:22:22 UTC |
e7d401f | Pierre-Yves Strub | 17 November 2021, 05:59:48 UTC | remove the script for creating tarballs | 17 November 2021, 06:01:10 UTC |
e46ef74 | Pierre-Yves Strub | 17 November 2021, 05:57:03 UTC | disable warning as errors | 17 November 2021, 05:57:03 UTC |
a54cec2 | Pierre-Yves Strub | 17 November 2021, 05:52:23 UTC | remove deprecated functions and reenable warning 3 | 17 November 2021, 05:52:23 UTC |
b7a2ee2 | Pierre-Yves Strub | 17 November 2021, 05:43:59 UTC | reenable warning 39 | 17 November 2021, 05:43:59 UTC |
4217836 | Pierre-Yves Strub | 17 November 2021, 05:41:36 UTC | reenable warning 38 | 17 November 2021, 05:41:36 UTC |
061e164 | Pierre-Yves Strub | 17 November 2021, 05:40:28 UTC | reenable warning 35 | 17 November 2021, 05:40:28 UTC |
43a1b9f | Pierre-Yves Strub | 17 November 2021, 05:39:00 UTC | reenable warning 34 | 17 November 2021, 05:39:17 UTC |
5b09921 | Pierre-Yves Strub | 17 November 2021, 05:34:48 UTC | reenable warning 6 | 17 November 2021, 05:34:48 UTC |
003fc41 | Pierre-Yves Strub | 17 November 2021, 05:34:23 UTC | [build] only consider src/theories/examples are deps | 17 November 2021, 05:34:23 UTC |
df78b65 | Pierre-Yves Strub | 17 November 2021, 05:34:13 UTC | .gitignore (.eca at root) | 17 November 2021, 05:34:13 UTC |
f8d5b79 | Pierre-Yves Strub | 16 November 2021, 18:32:37 UTC | Merge pull request #31 from ejgallego/1.0+dune [build] Add basic dune support | 16 November 2021, 18:32:37 UTC |
e39463d | Pierre-Yves Strub | 16 November 2021, 17:37:59 UTC | .gitignore: cleanup | 16 November 2021, 17:37:59 UTC |
68bbd4b | Pierre-Yves Strub | 16 November 2021, 14:59:38 UTC | [nix] update dependencies | 16 November 2021, 17:35:05 UTC |
f7c671c | Pierre-Yves Strub | 16 November 2021, 14:14:36 UTC | [build] use dune in Makefile | 16 November 2021, 17:35:05 UTC |
5334126 | Pierre-Yves Strub | 16 November 2021, 13:38:29 UTC | [build] do not create an internal EC library we do not currently expose any stable API. | 16 November 2021, 17:35:05 UTC |
3f13dec | Pierre-Yves Strub | 16 November 2021, 13:29:42 UTC | Use the old build system in opam. | 16 November 2021, 17:35:04 UTC |
fd804d6 | Emilio Jesus Gallego Arias | 22 August 2019, 15:33:19 UTC | [build] Add basic dune support Add experimental support for buidling `ec` using dune. Use ``` dune build ``` We don't add support for building the stdlib yet. | 16 November 2021, 17:35:04 UTC |
743a247 | Pierre-Yves Strub | 16 November 2021, 16:53:15 UTC | [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t | 16 November 2021, 17:35:04 UTC |
4b604bf | Christian Doczkal | 04 November 2021, 14:52:23 UTC | renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE | 16 November 2021, 17:35:04 UTC |
ab62416 | Christian Doczkal | 24 October 2021, 10:45:16 UTC | adapt to consistent use of mu1 | 16 November 2021, 17:35:04 UTC |
15946aa | Christian Doczkal | 24 October 2021, 09:36:02 UTC | use mu1 instead of mass in in Distr | 16 November 2021, 17:35:04 UTC |
5a0238b | Pierre-Yves Strub | 16 November 2021, 16:53:15 UTC | [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t | 16 November 2021, 16:56:20 UTC |
ec1f979 | Pierre-Yves Strub | 09 November 2021, 16:32:05 UTC | Merge pull request #88 from EasyCrypt/deploy-mu1 Consistently use `mu1` instead of `mass`. | 09 November 2021, 16:32:05 UTC |
e770f0f | Pierre-Yves Strub | 09 November 2021, 15:36:49 UTC | Refactor & generalize the section mechanism the section mechanism has been refactored s.t. it provides a more uniform interface where any kind of declaration can be marked as local / declared and erased / generalized when the section is closed. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 09 November 2021, 15:36:49 UTC |
b0e609d | Pierre-Yves Strub | 05 November 2021, 15:07:43 UTC | Fix the pretty printing of \ as a binop fix #93 | 05 November 2021, 15:08:07 UTC |
b37085c | Christian Doczkal | 04 November 2021, 14:52:23 UTC | renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE | 04 November 2021, 14:56:36 UTC |
d5d3d94 | Christian Doczkal | 24 October 2021, 10:45:16 UTC | adapt to consistent use of mu1 | 04 November 2021, 12:09:30 UTC |
6676710 | Christian Doczkal | 24 October 2021, 09:36:02 UTC | use mu1 instead of mass in in Distr | 04 November 2021, 12:06:45 UTC |
b9c7685 | Christian Doczkal | 03 November 2021, 15:28:23 UTC | comments, renaming, proof* | 04 November 2021, 10:00:49 UTC |
4da60d2 | Christian Doczkal | 03 November 2021, 15:06:57 UTC | allow sdist-distinguishers for ROs to call sample and set | 04 November 2021, 10:00:49 UTC |
8a26fe5 | Christian Doczkal | 03 November 2021, 12:25:10 UTC | some more simplifications | 04 November 2021, 10:00:49 UTC |
6851729 | Christian Doczkal | 01 November 2021, 10:09:10 UTC | remove weight equality side conditions | 04 November 2021, 10:00:49 UTC |
a21c135 | Christian Doczkal | 22 October 2021, 14:33:38 UTC | implement feedback from review | 04 November 2021, 10:00:49 UTC |
570f090 | Christian Doczkal | 21 October 2021, 15:48:19 UTC | fix compilation | 04 November 2021, 10:00:49 UTC |
7fcfa1d | Christian Doczkal | 21 October 2021, 14:21:07 UTC | move lemmas from SDist to RealSeries and Distr, rename summableM | 04 November 2021, 10:00:49 UTC |
f1d2f19 | Christian Doczkal | 21 October 2021, 09:05:24 UTC | use PROM rather than ROM | 04 November 2021, 10:00:49 UTC |
051cb1d | Christian Doczkal | 20 October 2021, 15:24:05 UTC | sdist for ROM distinguishers and N distinct queries | 04 November 2021, 10:00:49 UTC |
f5d072e | Christian Doczkal | 19 October 2021, 17:49:56 UTC | reduction from N to 1 oracle call for sdist distinguisher | 04 November 2021, 10:00:49 UTC |
3adc9c8 | Christian Doczkal | 18 October 2021, 16:11:21 UTC | sdist distinguisher for single oracle call + reduction to single sampling | 04 November 2021, 10:00:49 UTC |
62e1ce7 | Christian Doczkal | 14 October 2021, 12:55:45 UTC | connection between sdist and distinguisher procedures | 04 November 2021, 10:00:49 UTC |
4529cfc | Christian Doczkal | 12 October 2021, 12:10:25 UTC | statitical distance and some lemmas | 04 November 2021, 10:00:49 UTC |
aa6dc07 | Pierre-Yves Strub | 19 October 2021, 10:19:36 UTC | Add a simple form of pattern selection in rewrite rules Syntax is: `rewrite [pattern]rule` In this form, `pattern` is first searched against the current goal and rule LHS is then matched against the instanciated pattern. E.g. `rewrite [y+_]addrC` will instantiate `addrC` to `y` and `z` assuming that the first match of `y+_` in the current goal is `y+z`. This syntax is compatible with other variants: `rewrite -{2}[y+_]addrC` | 19 October 2021, 10:19:36 UTC |
4afdfe9 | Pierre-Yves Strub | 18 October 2021, 12:51:49 UTC | change "smt in rewrite" syntax New syntax is: - rewrite #smt - rewrite #smt:(db) - rewrite #smt:[options] | 18 October 2021, 12:52:42 UTC |
7b8aa43 | Pierre-Yves Strub | 18 October 2021, 08:03:55 UTC | Compute free program variables in *hoare statements. Fix #83 | 18 October 2021, 08:03:55 UTC |
c854989 | Pierre-Yves Strub | 12 October 2021, 13:39:31 UTC | Implement "gen have" & "wlog suff" Fix #77 | 12 October 2021, 13:39:31 UTC |
c132a25 | Pierre-Yves Strub | 08 October 2021, 12:09:27 UTC | StdLib: summability of partitioning | 08 October 2021, 12:09:35 UTC |
3ffc3be | Alley Stoughton | 06 October 2021, 15:00:49 UTC | Some lemmas for floor and ceil, in particular letting one rewrite floor x and ceil x. | 07 October 2021, 06:39:26 UTC |
0656ac7 | Alley Stoughton | 01 October 2021, 17:11:23 UTC | Added disjoint xs ys as an abbreviation for xs `&` ys = fset0. Added lemma disjointP (xs ys : 'a fset): disjoint xs ys <=> forall (x : 'a), x \in xs => ! x \in ys. | 04 October 2021, 07:24:14 UTC |
c07e880 | Pierre-Yves Strub | 06 September 2021, 09:47:40 UTC | Fix global positions reporting | 06 September 2021, 09:47:40 UTC |
512f0f2 | François Dupressoir | 30 June 2021, 14:43:29 UTC | [docker] get CVC4 from a more stable URL | 30 June 2021, 14:43:36 UTC |
489ff17 | Benjamin Gregoire | 30 June 2021, 09:54:24 UTC | default.nix | 30 June 2021, 10:01:04 UTC |
410f882 | Benjamin Gregoire | 28 June 2021, 10:11:24 UTC | improve default.nix | 28 June 2021, 10:11:24 UTC |
692a017 | Benjamin Gregoire | 09 June 2021, 06:26:11 UTC | remove duplicate eq_in_count/eq_count_in, keep eq_in_count | 09 June 2021, 06:26:37 UTC |
1890ad1 | Pierre Boutry | 08 June 2021, 19:43:54 UTC | Update README.md | 08 June 2021, 19:43:54 UTC |
73afe4f | Benjamin Gregoire | 04 June 2021, 05:35:25 UTC | improve error msg for proc | 04 June 2021, 05:35:25 UTC |
aeac2d4 | Pierre-Yves Strub | 27 May 2021, 10:03:02 UTC | Fix: cleanup exact hint DB after clone | 27 May 2021, 10:03:14 UTC |
eb6ce7c | François Dupressoir | 26 May 2021, 15:07:59 UTC | [stdlib] Array: fix set_set_swap | 26 May 2021, 15:07:59 UTC |
4dbdb88 | Pierre-Yves Strub | 26 May 2021, 07:20:22 UTC | Extend cloning with - inline but keep override (<=) - override theories | 26 May 2021, 07:20:22 UTC |
16e5d3b | Pierre-Yves Strub | 25 May 2021, 12:40:30 UTC | remove 'search' commands | 25 May 2021, 12:40:30 UTC |
aae9601 | Francois Dupressoir | 20 May 2021, 16:48:40 UTC | Merge pull request #67 from EasyCrypt/merge-chachapoly Soft-merge chachapoly proof and its stdlib changes We'll want to consider shifting the generic arguments on SKE (EUF-CMA + IND-CPA ⇒ IND-CCA) into standard libraries. | 20 May 2021, 16:48:40 UTC |
f30e424 | François Dupressoir | 20 May 2021, 14:32:30 UTC | Some nits in the new SmtMap lemmas | 20 May 2021, 16:31:22 UTC |
c750a58 | François Dupressoir | 20 May 2021, 09:59:20 UTC | FinType.FinType → FinType | 20 May 2021, 09:59:20 UTC |
82fd774 | François Dupressoir | 20 May 2021, 09:26:40 UTC | Shift some results to SmtMap Shift specific map-merging strategies from SplitRO to SmtMap. The `pair` strategy now does a product (with None as zero). | 20 May 2021, 09:26:40 UTC |
edd02d0 | François Dupressoir | 18 May 2021, 22:22:35 UTC | ChaCha-Poly x Easter He has risen! Authored by Benjamin Grégoire and Cécile Baritel-Ruet. Co-Authored-By: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-Authored-By: Cécile Baritel-Ruet <cecile.baritel-ruet@inria.fr> | 18 May 2021, 22:22:47 UTC |
8774376 | François Dupressoir | 18 May 2021, 13:15:43 UTC | Library work towards soft-merge of ChaCha-Poly | 18 May 2021, 22:17:02 UTC |
ba45bb5 | Francois Dupressoir | 26 April 2021, 12:10:43 UTC | Merge pull request #63 from EasyCrypt/deploy-clean-oldmonoid StdLib: Remove old Monoid dependency, port Hybrid argument to Bigops | 26 April 2021, 12:10:43 UTC |
14216cb | Benjamin Gregoire | 18 April 2021, 14:12:06 UTC | fix default.nix | 18 April 2021, 14:12:06 UTC |
1313a7d | François Dupressoir | 14 April 2021, 18:20:13 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-clean-oldmonoid | 14 April 2021, 18:20:13 UTC |
49d7ad3 | François Dupressoir | 14 April 2021, 15:32:51 UTC | 'Cleanup' but it's mostly shifting things around | 14 April 2021, 15:32:51 UTC |
2afb775 | Pierre-Yves Strub | 14 April 2021, 15:27:25 UTC | StdLib: funi + same weight => eq | 14 April 2021, 15:27:25 UTC |
d809ef8 | François Dupressoir | 13 April 2021, 15:50:46 UTC | StdLib: use bigops in generic Hybrid This instantiates BigOp for Booleans (with xor, or, and and) and gets rid of the old Monoid library, which Hybrid arguments relied upon. Some proof cleaning left to do in Hybrid, Indist, and PKE_Hybrid. | 13 April 2021, 15:50:46 UTC |
5df6a6f | Pierre-Yves Strub | 13 April 2021, 13:34:33 UTC | StdLib: basic facts on distributions | 13 April 2021, 13:34:33 UTC |
1b25ed4 | Pierre-Yves Strub | 12 April 2021, 09:31:13 UTC | Fix bug in theory renamings | 12 April 2021, 09:31:13 UTC |
40d1950 | Pierre-Yves Strub | 12 April 2021, 06:10:36 UTC | StdLib: ZModP: finite + uniform distribution | 12 April 2021, 06:10:36 UTC |
7ad9727 | Pierre-Yves Strub | 11 April 2021, 13:06:28 UTC | StdLib: linking sampling in Z/pZ and Z/qZ when q|p | 11 April 2021, 13:06:28 UTC |
c6ad4b1 | Pierre-Yves Strub | 10 April 2021, 14:05:38 UTC | StdLib: Poly: killing last admits | 10 April 2021, 14:05:38 UTC |
81f358d | Pierre-Yves Strub | 10 April 2021, 10:47:47 UTC | StdLib: polynomials distributions | 10 April 2021, 10:47:47 UTC |
639a76e | Pierre-Yves Strub | 09 April 2021, 20:10:53 UTC | StdLib: lead coeff. and degree of X^n+1 | 09 April 2021, 20:10:53 UTC |
8e6dd9a | Pierre-Yves Strub | 09 April 2021, 18:16:22 UTC | StdLib: ring quotient for non-integral domains | 09 April 2021, 18:16:22 UTC |
6a4bbab | Pierre-Yves Strub | 09 April 2021, 16:55:55 UTC | StdLib: ring regular element + poly over non integral domains | 09 April 2021, 16:55:55 UTC |
9e43d2c | Pierre-Yves Strub | 09 April 2021, 15:30:53 UTC | StdLib: more results on pmin | 09 April 2021, 15:30:53 UTC |
7fbcff7 | Pierre-Yves Strub | 08 April 2021, 16:42:07 UTC | StdLib: few lemmas about polynomials | 08 April 2021, 16:42:07 UTC |
84c2618 | Pierre-Yves Strub | 08 April 2021, 13:48:16 UTC | Fix stdlib | 08 April 2021, 13:48:16 UTC |
a014668 | Pierre-Yves Strub | 08 April 2021, 13:14:10 UTC | StdLib: enumerating polynomials of a given degree | 08 April 2021, 13:14:10 UTC |
0a6485a | Pierre-Yves Strub | 08 April 2021, 13:13:54 UTC | StdLib: Finite: explicit witnesses for finitness + related lemmas on lists | 08 April 2021, 13:13:54 UTC |
81cd929 | Pierre-Yves Strub | 08 April 2021, 13:13:27 UTC | Stdlib: IntDiv - add a few lemmas | 08 April 2021, 13:13:27 UTC |
18e7bf4 | Pierre-Yves Strub | 08 April 2021, 07:15:49 UTC | Stdlib: more results on polynomials & ring ideals | 08 April 2021, 07:15:49 UTC |
83e39fd | Pierre-Yves Strub | 07 April 2021, 14:44:27 UTC | Prove that polynomials form an integral domain | 07 April 2021, 14:44:27 UTC |
6ce66c7 | Pierre-Yves Strub | 07 April 2021, 14:44:12 UTC | Include ring quotients th. in ideals th. | 07 April 2021, 14:44:12 UTC |
de2158b | Pierre-Yves Strub | 07 April 2021, 12:32:34 UTC | Poly.ec -> Poly.eca | 07 April 2021, 12:32:34 UTC |