| HEAD | c8d3d6c | [theories]: Add scalar-vector multiplication | 18 July 2022, 17:11:20 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/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-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-oldmonoid | 1313a7d | Merge remote-tracking branch 'origin/1.0' into deploy-clean-oldmonoid | 14 April 2021, 18:20:13 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-cv2ec | 787383f | [C/G]DH-RSR: adapt to changes on main branch | 27 June 2022, 15:50:50 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 | 278876c | Saving work. Won't compile. | 28 June 2022, 20:41:19 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-eqv-quotient | acfd4ea | Definition of quotient types w.r.t. a equivalence relation | 16 April 2020, 14:56:46 UTC |
| refs/heads/deploy-expected-cost | 8f9d979 | add more rules | 31 August 2021, 06:39:31 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-142 | 8aa82ea | [matching]: when crossing a binder, update the env. accordingly fix #142 | 29 March 2022, 10:28:41 UTC |
| refs/heads/deploy-fix-154 | 3176e77 | force delta on convertibility checks This resolves #154, but might require some more finesse. In particular, perhaps we only want to force delta for top-level symbols? | 21 March 2022, 16:15:38 UTC |
| refs/heads/deploy-fix-17390 | bf76f88 | [fix #17390] | 24 November 2020, 16:20:22 UTC |
| refs/heads/deploy-fix-186 | 3e3f90f | Kill Stream related warnings Fix #186 | 19 June 2022, 20:07:48 UTC |
| refs/heads/deploy-fix-212 | 3cd9c5d | fix phl while rule | 15 July 2022, 09:50:10 UTC |
| refs/heads/deploy-fix-233 | 3d4f1e5 | port Dexcepted to dresrict and deprecate Dfilter fixes #233 | 28 July 2022, 14:55:15 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 | 97fe4df | 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-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-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 | 8f0c487 | Cost Hoare logic v2 Second version of the cost Hoare logic. Here are the objectives of this new version (some are still [WIP]): - 1) removed the "flattened" semantics of cost vectors - 2) [WIP] less boilerplate, better user interaction - 3) [WIP] use cost information in other Hoare logics 1) No flattened semantics: - the previous semantics flattened the cost vectors, i.e. `{42, A.f: 2}` was to be understood as the integer `42 + 2 * intr_A.f` where `intr_A.f` is the intrinsic cost of `A.f`. This flattened semantics prevent from ignoring the concrete cost of a procedure (setting it to be at most +infinity), while still bounding the number of calls to some specific module parameters or abstract modules. - previous point necessary to use cost information in other Hoare logics (especially to remove counting wrappers), while ignoring the concrete cost. - in some settings (e.g. quantum, information theoretic arguments, rejection samplings), the worst-case concrete cost may be unbounded. It is therefore crucial to get rid of the flattened semantics to apply the cost logic in these settings 2) Less boilerplate (still [WIP]): - w.r.t. the old approach, which requires to write, for every pair of procedure and oracle procedure, the number of times the former can call the latter => somehow quadratic number of constants to introduce/write - no new boilerplate added even though we prove more. Indeed, if we remove the flattened semantics and kept the old style for stating lemmas, then we also need to anticipate and state that some procedure will call some abstract module (not a functor parameter) some number of times. Issues: * this is heavy; * if we use many times the lemma, in ≠ contexts with ≠ abstract modules, then we need to anticipate *each* usage in the lemma statement. 3) use cost information in Hoare logics (still [WIP]): - remove wrappers with little overhead. | 13 June 2022, 10:01:08 UTC |
| refs/heads/deploy-new-nix | d5aee44 | workflow to compile with nix | 22 July 2022, 14:34:38 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-opsem | c954ae0 | Hakyber jasmin eclib | 25 April 2022, 14:53:39 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 | 5489c23 | Dependent version of the multi-rnd tactic | 29 June 2022, 16:01:28 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-equiv | 6a16de3 | Fiddling with goal generation And getting a proper-ish example through. | 13 June 2022, 15:46:00 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-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-crush | 6e01910 | WIP | 11 January 2021, 17:49:21 UTC |
| refs/heads/deploy-subst-refactoring | 8f8c231 | Internal: EcSubst does not rely anymore on the low-level substitutions | 19 July 2022, 13:48:12 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 | bc83128 | nits | 12 May 2022, 08:58:52 UTC |
| refs/heads/deploy-theory-matrix | d61ce8f | | 20 December 2017, 14:08:50 UTC |
| refs/heads/deploy-theory-matrix-ring | 74142f2 | Merge branch '1.0' into deploy-theory-matrix-ring | 10 June 2020, 14:14:07 UTC |
| refs/heads/deploy-theory-monalg | 879d842 | ax. for polynomials | 03 May 2020, 22:02:33 UTC |
| refs/heads/deploy-theory-symmetric-group | acfd4ea | Definition of quotient types w.r.t. a equivalence relation | 16 April 2020, 14:56:46 UTC |
| refs/heads/deploy-tighter-birthday | 645a397 | tighter Birhtday bound + coarse lemmas | 18 December 2019, 14:29:51 UTC |
