HEAD | 782eb5c | Apply cloning substitution to datatype ctor types | 22 January 2025, 14:45:44 UTC |
refs/heads/PKEROM | 959f978 | Moving PKEROM from ROM to PROM | 30 April 2023, 09:34:04 UTC |
refs/heads/PolyMicro | b5050a9 | Added eq_mod precondition and more general forms, slight refactoring and fq_mul file | 15 May 2024, 16:00:00 UTC |
refs/heads/PolynomialEncoding | d60b796 | Refactoring and added more translations | 28 April 2024, 20:45:40 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 | 6ba7634 | Merge branch 'main' into bdep | 17 January 2025, 10:46:46 UTC |
refs/heads/bdep_MLKEM_avx2_equivs | 16ff945 | Fixes | 09 October 2024, 16:49:43 UTC |
refs/heads/ci-external-projects-in-file | ea464f2 | [ci] external projects description outside of the workflow file | 08 April 2024, 13:05:47 UTC |
refs/heads/comm-algebra | ee462d5 | stdlib: basic commutative algebra | 21 August 2024, 09:37:01 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 | 7ad0928 | Merge branch 'main' into easypqc | 23 May 2024, 06:45:39 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-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 |