https://github.com/EasyCrypt/easycrypt
Name Revision Message Date
HEAD 7ad9727 StdLib: linking sampling in Z/pZ and Z/qZ when q|p 11 April 2021, 13:06 UTC
refs/heads/1.0 7ad9727 StdLib: linking sampling in Z/pZ and Z/qZ when q|p 11 April 2021, 13:06 UTC
refs/heads/1.0-preview 7a4c6d1 Stdlib: ring quotients 05 April 2021, 09:08 UTC
refs/heads/aprhl 0d55fac Merge branch '1.0' into aprhl 04 April 2021, 17:25 UTC
refs/heads/deploy-assign 04b9a83 fix examples after rebase 11 February 2020, 18:27 UTC
refs/heads/deploy-better-dlet b081035 Masking the default dletE lemma more meaningful This is a quick and dirty attempt and requires iteration. 17 January 2020, 11:01 UTC
refs/heads/deploy-better-int-red 7b972a4 Merge branch '1.0' into deploy-better-int-red 14 October 2019, 12:20 UTC
refs/heads/deploy-better-printing 92c2f2a Pragmas for printing pre/post as a list of their resp. conjunctions Pragmas are: PrPo:{pr,po}:{raw,ands} 09 May 2018, 11:25 UTC
refs/heads/deploy-binomial-law 82cc4d7 binomial law + basic lemmas (full / support) 09 June 2020, 19:55 UTC
refs/heads/deploy-chachapoly 4e84f9c Make CI useful again 14 May 2020, 11:59 UTC
refs/heads/deploy-chernoff ce4d674 make things compile 30 September 2019, 15:35 UTC
refs/heads/deploy-clean-pow fd8edc1 refactor & merge min/max 09 June 2020, 10:27 UTC
refs/heads/deploy-cloning-with-theories 12d8680 WIP 04 December 2020, 15:31 UTC
refs/heads/deploy-codepos-fix c997f51 fix parsing of codeposition Syntax for offset is now: &+n and &-n. 12 September 2018, 11:42 UTC
refs/heads/deploy-cost ce01988 allow cost precondition in rcondf, rcondt and if tactics 19 June 2020, 11:54 UTC
refs/heads/deploy-cost-1.0-preview bab83fc simplify syntaxe of call rule 30 March 2021, 10:25 UTC
refs/heads/deploy-cost-submitted 555d19a Travis -> CircleCI 18 December 2020, 20:07 UTC
refs/heads/deploy-crt d583086 CRT prooved modulo some easy admits 01 March 2021, 09:56 UTC
refs/heads/deploy-cyclic ea6c7da Move "monogenous" to Group. 16 April 2020, 13:06 UTC
refs/heads/deploy-debug-mark 3a2ef0e Add debug mark 11 January 2021, 14:04 UTC
refs/heads/deploy-derandomize 0e36974 Merge branch '1.0' into deploy-derandomize 15 October 2019, 08:38 UTC
refs/heads/deploy-dexcepted-sampling e4bf172 trailing white space in modified files 16 January 2020, 20:40 UTC
refs/heads/deploy-eager-rp 0dd57f7 OneMap-PRP: a PRP with a single map and lemmas to switch This is to later support sampling the map eagerly, possibly with programming queries as well. 06 December 2019, 09:55 UTC
refs/heads/deploy-eco2 714c8e6 Add EC hash to .eco 18 October 2019, 08:18 UTC
refs/heads/deploy-eqv-quotient acfd4ea Definition of quotient types w.r.t. a equivalence relation 16 April 2020, 14:56 UTC
refs/heads/deploy-extended-tests 9db28d5 script for testing EasyCrypt on various external devs 27 January 2020, 13:46 UTC
refs/heads/deploy-fingroup 67ea95f Merge branch '1.0' into deploy-fingroup 15 October 2019, 10:19 UTC
refs/heads/deploy-fix-17390 bf76f88 [fix #17390] 24 November 2020, 16:20 UTC
refs/heads/deploy-fmatch f47fb53 better with the files 26 November 2019, 07:51 UTC
refs/heads/deploy-for 99d5c85 Free variable propagation in sp tuned down 06 April 2021, 16:31 UTC
refs/heads/deploy-global-union 2b7b58c Merge branch '1.0' into deploy-global-union 15 October 2019, 07:02 UTC
refs/heads/deploy-implicit-arguments 3671d46 Travis -> CircleCI 18 December 2020, 20:07 UTC
refs/heads/deploy-improve-matching 60b76e8 Try to remove exponential behavior 05 September 2019, 09:05 UTC
refs/heads/deploy-instance-adv 8bceccd . 13 December 2017, 16:30 UTC
refs/heads/deploy-lamport 9b906a3 Merge branch '1.0' into deploy-lamport 10 February 2020, 09:45 UTC
refs/heads/deploy-map-find eaa7592 Fix bug in eager if 27 November 2019, 21:10 UTC
refs/heads/deploy-match 6c34461 Merge branch '1.0' into deploy-match 26 November 2018, 09:45 UTC
refs/heads/deploy-match-in-stmt 7f86943 02 June 2020, 13:57 UTC
refs/heads/deploy-match-in=prog-logic-houra e56737b matching for Pr 08 April 2020, 13:58 UTC
refs/heads/deploy-mathml fcdfcbd Core theory for univariate polynomials 21 November 2020, 12:11 UTC
refs/heads/deploy-mem-in-types 88a87da Merge branch '1.0' of https://github.com/EasyCrypt/easycrypt into 1.0 17 December 2018, 14:33 UTC
refs/heads/deploy-minr-maxr 4391b04 basic results about minr 12 November 2020, 11:00 UTC
refs/heads/deploy-momemtum 0659058 Merge branch '1.0' into deploy-momemtum 05 February 2020, 15:19 UTC
refs/heads/deploy-new-rom e8a5cb0 Fix merge problem 15 June 2020, 15:10 UTC
refs/heads/deploy-no-eco 3a626d5 Add a -no-eco option to disable .eco generation Existing .eco cached results are used, but new ones are not generated 30 March 2021, 13:09 UTC
refs/heads/deploy-nosmt-ops da719f0 Allows nosmt with all operators other than pure, abstract ones - i.e., with plain, axiomatized (including : {t | phi} as ax) and cases operators. When cloning, [op nosmt x = ...] is allowed, but nosmt can't be used with inlining mode. 22 May 2020, 22:12 UTC
refs/heads/deploy-oaep e3d8bd1 Merge branch '1.0' into draft-oaep 15 October 2019, 07:31 UTC
refs/heads/deploy-opaque-op bd8615e 13 January 2021, 15:01 UTC
refs/heads/deploy-poly-record ad258e9 no need for List.sort for maps 27 March 2018, 12:38 UTC
refs/heads/deploy-polymorphic-module 846710a Start restructuration of the code to be able to avant mutual dependency between type and mpath 14 July 2019, 06:50 UTC
refs/heads/deploy-prod-fintype ec03a3c 29 November 2019, 13:19 UTC
refs/heads/deploy-quantum ff849a2 Fundamental lemma 10 April 2021, 14:20 UTC
refs/heads/deploy-reduce-decimal 93748b3 Decimal numbers are now translated to irreducible fractions 01 December 2020, 09:41 UTC
refs/heads/deploy-reduction ce71c7f More reduction for le/lt (real) 07 November 2017, 08:25 UTC
refs/heads/deploy-remove-cut a8d02dd remove deprecated "cut" tactic 04 January 2021, 13:15 UTC
refs/heads/deploy-rewrite-patterns 9e11412 Generalize arguments about sampling in dexcepted This pushes several complex low-level arguments related to sampling in restricted distributions into the related distribution file. This also generalizes these arguments, so that: - TwoStepSampling no longer requires a full distribution, - WhileSampling takes distributions and tests as procedure arguments rather than clone parameters. Specialized versions of theories and lemmas that reproduce the old behaviours are also included. The Dice_Sampling theory is removed, replaced with Dexcepted.WhileSamplingFixedTest (an abstract theory). Squashed commit of the following: commit e4bf1725f2a327bc58dda51d0079acb8dbb8fb1a Author: François Dupressoir <fdupress@gmail.com> Date: Thu Jan 16 20:40:23 2020 +0000 trailing white space in modified files commit 12d5ff0ae8607be10f7e925d1f0d44dd8e78dbde Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 15:49:41 2019 +0000 minor cleanup commit 7921a24e13e9f6d19ad02c0a22e8efb49bc37184 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 13:47:19 2019 +0000 More general ways of sampling out of a predicate TwoStep no longer requires losslessness. More sharing of proof could be obtained commit 393700f85b47b9d373be983b1451b08ae3d3be94 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:40:16 2019 +0000 PRP<->PRF uses generic resampling commit 74b9aef924cc313e358510ab9f83bc7410489db4 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:27:12 2019 +0000 Slight generalization: no longer need a full distribution commit 0853fc0e313bb6adac0ad956417480ebd70f512f Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 18:34:43 2019 +0000 Dexcepted: equivalence between two ways of sampling used in PRP<->PRF, but also in a current proof TODO: make PRP<->PRF use this 16 January 2020, 20:48 UTC
refs/heads/deploy-rigid-auto-rewrite 86266ae rigid auto rewrite 12 February 2020, 17:00 UTC
refs/heads/deploy-rigid-opt f27fcaa add a "rigid" meta-tactic for forcing rigid unification 16 February 2019, 06:08 UTC
refs/heads/deploy-ring-ideal 723d459 def. of ring quotients 17 March 2020, 21:17 UTC
refs/heads/deploy-rom-nobranching 27c52db Try out a non-branching version of core ROM This makes post-skip proofs a lot smoother (avoiding a lot of duplication in proofs). However, it requires some mental gymnastics to deal with no-op updates. 07 July 2020, 16:39 UTC
refs/heads/deploy-section 0935e74 restructure code 21 December 2020, 06:45 UTC
refs/heads/deploy-sem 63acd50 prelude 21 November 2020, 08:36 UTC
refs/heads/deploy-sigmaprotocols c22ac63 more lemmas on div 10 February 2020, 09:30 UTC
refs/heads/deploy-simpler-rp 005342f Merge branch '1.0' into deploy-simpler-rp 10 February 2020, 09:48 UTC
refs/heads/deploy-simpler-xpaths 180d323 Merge branch 'deploy-extended-tests' into deploy-simpler-xpaths 27 January 2020, 13:48 UTC
refs/heads/deploy-solveeq ac9827a rnd auto dans cramer shoup 08 March 2019, 14:00 UTC
refs/heads/deploy-subst-crush 6e01910 WIP 11 January 2021, 17:49 UTC
refs/heads/deploy-tactic-in-rewrite ea7db00 tactics in rewrite 04 December 2019, 09:53 UTC
refs/heads/deploy-taylor ff9ce64 Merge remote-tracking branch 'origin/1.0' into deploy-taylor 03 December 2019, 06:15 UTC
refs/heads/deploy-test-script 51f8ab0 .gitignore: .eco 18 October 2019, 08:11 UTC
refs/heads/deploy-theory-matrix d61ce8f 20 December 2017, 14:08 UTC
refs/heads/deploy-theory-matrix-ring 74142f2 Merge branch '1.0' into deploy-theory-matrix-ring 10 June 2020, 14:14 UTC
refs/heads/deploy-theory-monalg 879d842 ax. for polynomials 03 May 2020, 22:02 UTC
refs/heads/deploy-theory-symmetric-group acfd4ea Definition of quotient types w.r.t. a equivalence relation 16 April 2020, 14:56 UTC
refs/heads/deploy-tighter-birthday 645a397 tighter Birhtday bound + coarse lemmas 18 December 2019, 14:29 UTC
refs/heads/deploy-transeq e15c19f Merge branch '1.0' into deploy-transeq 10 July 2019, 05:57 UTC
refs/heads/deploy-trivial-in-low-api 5e06824 Merge branch '1.0' into deploy-trivial-in-low-api 27 April 2018, 12:07 UTC
refs/heads/deploy-tutorial 0c0796c fixing file names priorities in include paths? such luxury! 07 November 2019, 14:40 UTC
refs/heads/deploy-weak-dep-types 6590f1e wdep 05 August 2019, 10:06 UTC
refs/heads/deploy-wf b529da0 An axiom-free formalization of well-founded relations, induction and recursion. 29 March 2021, 13:09 UTC
refs/heads/deploy-why3-1.4 4a45b36 Why3 1.4: CI 04 April 2021, 06:10 UTC
refs/heads/deploy-wp-kw eb414fd Merge branch '1.0' into deploy-wp-kw 15 October 2019, 08:39 UTC
refs/heads/draft-typeclass 1977833 Make interface uniform 12 August 2020, 20:15 UTC
refs/heads/ellora 03fd7f2 compile with up-to-date toolchain 10 October 2017, 09:04 UTC
refs/heads/typeclass-draft 9e556cc Resolved bug in multi-parameter instance declaration 15 April 2020, 15:14 UTC
refs/tags/ccs14-sfe a79f9ae Fix bug w.r.t. _tools presence detection. 08 July 2014, 09:43 UTC
refs/tags/doc 863066b Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec` [fix #17249] 23 September 2015, 08:28 UTC
refs/tags/evoting 955e909 NewList: last_ -> last. 30 July 2015, 08:20 UTC
back to top