| HEAD | 30bfa95 | New tactic: "proc change" This tactic allows to change an expression in a statement by some other expression. When applied, the user has to prove that the two expressions are equal (generalizing over all the program variables) This tactic applies to any program logic. The syntax is: proc change <side?> <codepos> : <form> This tactic is in the TCB. Test plan: - unit test (tests/prochange.ec) | 11 December 2023, 10:58:49 UTC |
| refs/heads/PKEROM | 959f978 | Moving PKEROM from ROM to PROM | 30 April 2023, 09:34:04 UTC |
| refs/heads/PolynomialEncoding | ac3cc65 | Add zify tactic | 05 April 2024, 13:22:05 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 | a14e0e6 | Converted precondition to circuit (working for polycompress) | 20 March 2024, 18:19: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 | 31ae2ac | Merge branch 'main' into deploy-easyPQC | 03 April 2024, 03:20:04 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 | 03f5769 | Merge remote-tracking branch 'origin/main' into deploy-tc | 05 April 2024, 15:16:41 UTC |
