https://github.com/EasyCrypt/easycrypt
Name Target Message Date
HEAD c5f30c8 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
refs/heads/PKEROM 959f978 Moving PKEROM from ROM to PROM 30 April 2023, 09:34:04 UTC
refs/heads/aprhl f7b8664 Added Above Threshold and Report Noisy Max examples, which check with current version of branch. 30 June 2021, 15:32:30 UTC
refs/heads/bdep 5c9e395 Fixed bruteforce, added bitwuzla equivalence checking 08 March 2024, 19:29:32 UTC
refs/heads/csidh-group-action dab7c47 Merge pull request #81 from Cameron-Low/csidh-group-action Csidh group action 11 October 2021, 09:55:19 UTC
refs/heads/deploy-annotations f89ce07 Bug equal and hash fixed 17 March 2023, 14:32:04 UTC
refs/heads/deploy-axiom-clone-subcommand aa6dc07 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
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:47 UTC
refs/heads/deploy-better-int-red 7b972a4 Merge branch '1.0' into deploy-better-int-red 14 October 2019, 12:20:46 UTC
refs/heads/deploy-better-print 7ce03dc WIP: fix printing of modules 25 February 2022, 17:12:21 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:50 UTC
refs/heads/deploy-binomial-law 82cc4d7 binomial law + basic lemmas (full / support) 09 June 2020, 19:55:20 UTC
refs/heads/deploy-cdh-rsr 328c028 proof of the reduction for GDH_RSR 18 January 2022, 18:21:42 UTC
refs/heads/deploy-chachapoly 4e84f9c Make CI useful again 14 May 2020, 11:59:26 UTC
refs/heads/deploy-chernoff ce4d674 make things compile 30 September 2019, 15:35:43 UTC
refs/heads/deploy-clean-pow fd8edc1 refactor & merge min/max 09 June 2020, 10:27:13 UTC
refs/heads/deploy-codepos-fix c997f51 fix parsing of codeposition Syntax for offset is now: &+n and &-n. 12 September 2018, 11:42:14 UTC
refs/heads/deploy-crt d583086 CRT prooved modulo some easy admits 01 March 2021, 09:56:16 UTC
refs/heads/deploy-cyclic ea6c7da Move "monogenous" to Group. 16 April 2020, 13:06:48 UTC
refs/heads/deploy-debug-mark 3a2ef0e Add debug mark 11 January 2021, 14:04:57 UTC
refs/heads/deploy-deep-match 29bfa6a Saving work. 02 July 2022, 09:50:09 UTC
refs/heads/deploy-default-nosmt f6574ff make axiomatized operators `nosmt` by default 16 May 2022, 11:48:54 UTC
refs/heads/deploy-derandomize 0e36974 Merge branch '1.0' into deploy-derandomize 15 October 2019, 08:38:08 UTC
refs/heads/deploy-dexcepted-sampling e4bf172 trailing white space in modified files 16 January 2020, 20:40:23 UTC
refs/heads/deploy-djoin-dlist 70662a7 Unfold non-transparent operators in `case` & `elim`. When `case` or `elim` search for a redex, allows the reduction to unfold non-transparent operators. This does not affect tactics that does case/elim internally (e.g., />). fix #132 18 February 2022, 22:18:29 UTC
refs/heads/deploy-docker 56a393d [github-action]: push docker images 06 May 2022, 06:44:04 UTC
refs/heads/deploy-dword-is-dlist 452ec9f Lemma stating equality of word and list distributions 14 December 2021, 12:22:51 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:55 UTC
refs/heads/deploy-easyPQC 544680e fix and simplify parser 28 October 2023, 05:36:58 UTC
refs/heads/deploy-eqv-quotient acfd4ea Definition of quotient types w.r.t. a equivalence relation 16 April 2020, 14:56:46 UTC
refs/heads/deploy-extended-tests 9db28d5 script for testing EasyCrypt on various external devs 27 January 2020, 13:46:58 UTC
refs/heads/deploy-feature-127 058022c Add rdirs option in config file closes #127 19 January 2022, 19:29:05 UTC
refs/heads/deploy-fingroup 67ea95f Merge branch '1.0' into deploy-fingroup 15 October 2019, 10:19:46 UTC
refs/heads/deploy-fix-#154 9d08a76 fix #154 24 November 2022, 16:10:02 UTC
refs/heads/deploy-fix-142 8aa82ea [matching]: when crossing a binder, update the env. accordingly fix #142 29 March 2022, 10:28:41 UTC
refs/heads/deploy-fix-17390 bf76f88 [fix #17390] 24 November 2020, 16:20:22 UTC
refs/heads/deploy-fix-292 2b54cca add local module during conversion 29 October 2022, 06:29:51 UTC
refs/heads/deploy-fmatch f47fb53 better with the files 26 November 2019, 07:51:24 UTC
refs/heads/deploy-for abd5db4 For loop temporarly removed 09 September 2021, 15:27:29 UTC
refs/heads/deploy-general-prf-distinguisher 0afb971 Clean some SMT calls in PRP-PRF 06 July 2021, 09:30:36 UTC
refs/heads/deploy-genhave 374dae6 parser: fix precedence issue 12 October 2021, 13:09:21 UTC
refs/heads/deploy-global-union 2b7b58c Merge branch '1.0' into deploy-global-union 15 October 2019, 07:02:30 UTC
refs/heads/deploy-hybrid0 a16dcf5 Apply suggestions from code review Co-authored-by: Francois Dupressoir <fdupress@gmail.com> 14 December 2021, 09:43:58 UTC
refs/heads/deploy-implicit-arguments 3671d46 Travis -> CircleCI 18 December 2020, 20:07:48 UTC
refs/heads/deploy-improve-matching 60b76e8 Try to remove exponential behavior 05 September 2019, 09:05:32 UTC
refs/heads/deploy-indexed-types b37b762 Prototype implementation of a match statement. 23 November 2021, 16:58:42 UTC
refs/heads/deploy-instance-adv 8bceccd . 13 December 2017, 16:30:02 UTC
refs/heads/deploy-lamport 9b906a3 Merge branch '1.0' into deploy-lamport 10 February 2020, 09:45:49 UTC
refs/heads/deploy-license fc07a36 License change: CeCILL B/C -> MIT 29 March 2022, 08:01:08 UTC
refs/heads/deploy-log 8e47fe3 Fix bug that prevents `rewrite //= in h` to simplify in `h` Fix #68 03 December 2021, 16:11:39 UTC
refs/heads/deploy-match 6c34461 Merge branch '1.0' into deploy-match 26 November 2018, 09:45:25 UTC
refs/heads/deploy-match-in-stmt 7f86943 02 June 2020, 13:57:30 UTC
refs/heads/deploy-match-in=prog-logic-houra e56737b matching for Pr 08 April 2020, 13:58:49 UTC
refs/heads/deploy-mem e6cc4a0 . 30 January 2024, 10:07:36 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:18 UTC
refs/heads/deploy-minr-maxr 4391b04 basic results about minr 12 November 2020, 11:00:16 UTC
refs/heads/deploy-momemtum 0659058 Merge branch '1.0' into deploy-momemtum 05 February 2020, 15:19:33 UTC
refs/heads/deploy-multi-apply 644ddc2 Fix a typing annotation bug in distribution tags' axioms fix #241 09 August 2022, 07:51:07 UTC
refs/heads/deploy-mutual-inductives 6890aca fix small bug in reduction of projection 04 February 2023, 10:56:31 UTC
refs/heads/deploy-named-goals e7ae2d3 First implementation of named goals 18 May 2023, 11:16:48 UTC
refs/heads/deploy-nested-tuples 5bab2b5 Bug fix: created too many fresh names 06 February 2023, 14:43:04 UTC
refs/heads/deploy-new-cost 3f4a0bd 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
refs/heads/deploy-new-cost2 32f0ee5 [cost v2] printing of full mpath + first wrapped mpath in the parser 25 August 2023, 16:20:56 UTC
refs/heads/deploy-new-rom e8a5cb0 Fix merge problem 15 June 2020, 15:10:39 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:19 UTC
refs/heads/deploy-oaep e3d8bd1 Merge branch '1.0' into draft-oaep 15 October 2019, 07:31:07 UTC
refs/heads/deploy-oracle-pke 14a56f1 add lemma RO_LRO and generalize RO_FinRO_D 08 December 2021, 12:53:47 UTC
refs/heads/deploy-packaging 3798b1a CI 28 September 2021, 13:50:14 UTC
refs/heads/deploy-pattern-in-rewrite d893b83 Merge branch '1.0' into deploy-pattern-in-rewrite 19 October 2021, 10:22:51 UTC
refs/heads/deploy-poly-record ad258e9 no need for List.sort for maps 27 March 2018, 12:38:51 UTC
refs/heads/deploy-poly-reduce 9e2f905 Theory for R[X]/<X^n+1> 23 January 2022, 15:46:16 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:07 UTC
refs/heads/deploy-ppe-with-full-path 4c419f4 07 June 2021, 10:12:13 UTC
refs/heads/deploy-prod-fintype ec03a3c 29 November 2019, 13:19:00 UTC
refs/heads/deploy-project-file 3f7727c easycrypt.opam 23 November 2021, 09:37:12 UTC
refs/heads/deploy-quantum d317924 Merge branch 'main' into deploy-quantum 14 December 2022, 09:56:45 UTC
refs/heads/deploy-quantum-upgrade 3cef12a Making this branch work with same Why3 version as main 10 October 2023, 09:38:20 UTC
refs/heads/deploy-reduce-decimal 93748b3 Decimal numbers are now translated to irreducible fractions 01 December 2020, 09:41:56 UTC
refs/heads/deploy-reduction ce71c7f More reduction for le/lt (real) 07 November 2017, 08:25:14 UTC
refs/heads/deploy-refine-birthday 2075873 Birthday refinements Allows prameterised sampling and bounding of collisions up to a function The query bound is now provided as a lemma parameter unless the oracles enforce the query bound. 10 May 2022, 11:31:18 UTC
refs/heads/deploy-remove-cut a8d02dd remove deprecated "cut" tactic 04 January 2021, 13:15:49 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:25 UTC
refs/heads/deploy-rigid-auto-rewrite 86266ae rigid auto rewrite 12 February 2020, 17:00:54 UTC
refs/heads/deploy-rigid-opt f27fcaa add a "rigid" meta-tactic for forcing rigid unification 16 February 2019, 06:08:09 UTC
refs/heads/deploy-ring-ideal 723d459 def. of ring quotients 17 March 2020, 21:17:33 UTC
refs/heads/deploy-ring-with-dfl-inv cd974a7 [theories]: ring with generic (choice based) inverse 23 January 2023, 10:23:53 UTC
refs/heads/deploy-rmap 1e4e582 Variant of FMap where get samples randomly 14 June 2023, 14:00:26 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:30 UTC
refs/heads/deploy-search e422fcb Improve search command - search for substrings in the lemma's name: search /"foo"/ - searching inside a specific theory search ... in T1, T2, ... Ref #71 24 July 2021, 17:58:50 UTC
refs/heads/deploy-sem 63acd50 prelude 21 November 2020, 08:36:44 UTC
refs/heads/deploy-sigmaprotocols c22ac63 more lemmas on div 10 February 2020, 09:30:24 UTC
refs/heads/deploy-simpler-rp 005342f Merge branch '1.0' into deploy-simpler-rp 10 February 2020, 09:48:54 UTC
refs/heads/deploy-simpler-xpaths 180d323 Merge branch 'deploy-extended-tests' into deploy-simpler-xpaths 27 January 2020, 13:48:30 UTC
refs/heads/deploy-solveeq ac9827a rnd auto dans cramer shoup 08 March 2019, 14:00:31 UTC
refs/heads/deploy-subst cb3771c use coresubst everywhere 29 November 2023, 14:26:28 UTC
refs/heads/deploy-subst-crush 6e01910 WIP 11 January 2021, 17:49:21 UTC
refs/heads/deploy-tactic-in-rewrite ea7db00 tactics in rewrite 04 December 2019, 09:53:07 UTC
refs/heads/deploy-taylor ff9ce64 Merge remote-tracking branch 'origin/1.0' into deploy-taylor 03 December 2019, 06:15:32 UTC
refs/heads/deploy-tc bede2b2 Merge branch 'main' into deploy-tc 16 January 2024, 15:35:30 UTC
refs/heads/deploy-theory-matrix d61ce8f 20 December 2017, 14:08:50 UTC
back to top