| f37eff5 | Adrien Koutsos | 28 April 2022, 16:54:57 UTC | removed projection over abstract procedures, which is unsound | 28 April 2022, 16:54:57 UTC |
| e399dc5 | Adrien Koutsos | 27 April 2022, 23:09:11 UTC | new cost axiom | 27 April 2022, 23:09:11 UTC |
| 2055e8f | Adrien Koutsos | 27 April 2022, 17:08:08 UTC | minor | 27 April 2022, 17:08:08 UTC |
| c3146c2 | Adrien Koutsos | 27 April 2022, 17:08:03 UTC | cleanup | 27 April 2022, 17:08:03 UTC |
| 3a46371 | Adrien Koutsos | 27 April 2022, 17:07:53 UTC | fixed cost librairies | 27 April 2022, 17:07:53 UTC |
| db88428 | Adrien Koutsos | 27 April 2022, 14:27:46 UTC | fix projection printing | 27 April 2022, 14:27:46 UTC |
| 89f954e | Adrien Koutsos | 27 April 2022, 14:05:40 UTC | can parse projections | 27 April 2022, 14:05:40 UTC |
| 753f746 | Adrien Koutsos | 27 April 2022, 09:59:18 UTC | fixed `hint simplify` usage for cost theory also moved axiom out of pervasive | 27 April 2022, 09:59:18 UTC |
| 91761d1 | Adrien Koutsos | 27 April 2022, 09:49:14 UTC | better form dumping | 27 April 2022, 09:49:14 UTC |
| 324ba73 | Pierre-Yves Strub | 26 April 2022, 08:49:07 UTC | Makefile | 26 April 2022, 16:46:37 UTC |
| 2dabde1 | Adrien Koutsos | 25 April 2022, 15:42:10 UTC | move cost axioms in abstract theories (fix #175) | 26 April 2022, 16:46:15 UTC |
| 5d283f2 | François Dupressoir | 11 January 2022, 16:03:51 UTC | Reject `x <- RHS` when `RHS` is a procedure call | 26 April 2022, 16:42:47 UTC |
| 7e0f6ba | François Dupressoir | 14 December 2021, 15:43:15 UTC | Improve parser for anonymous proc parameters Anonymous and named parameters can be mixed for abstract procedures. Corner cases are not exercised by test suites and may crop up. Resolves #108. | 26 April 2022, 16:42:12 UTC |
| 20564b5 | Pierre-Yves Strub | 30 March 2022, 09:20:02 UTC | Fixing list of authors | 26 April 2022, 16:35:39 UTC |
| 716f354 | Pierre-Yves Strub | 07 April 2022, 16:12:18 UTC | [env]: fully head-norm the type before fetching its top-level decl. This commit involves a lot of code motion. partially address #121 | 26 April 2022, 16:35:39 UTC |
| 8abdc7d | Pierre-Yves Strub | 07 April 2022, 15:11:17 UTC | [reduction]: in cbv, fix handling of stack arguments The API was s.t. it was possibly to detect a non-empty stack as an empty one. Partially address #121 | 26 April 2022, 16:35:39 UTC |
| 3aee866 | Adrien Koutsos | 08 April 2022, 08:53:32 UTC | error message if cost information are missing in the call tactic | 26 April 2022, 16:35:18 UTC |
| 44a632c | Adrien Koutsos | 07 April 2022, 09:18:51 UTC | Fix typing of modules expressions fix #171 | 26 April 2022, 16:33:30 UTC |
| a5de7bc | Pierre-Yves Strub | 05 April 2022, 10:25:31 UTC | [reduction]: use symmetric "and" when reducing tuples equality fix #171 | 26 April 2022, 16:33:30 UTC |
| 1c52e78 | Adrien Koutsos | 31 March 2022, 13:49:34 UTC | pretty printer improvements for module restrs + local memtypes | 26 April 2022, 16:33:17 UTC |
| 75f6941 | Alley Stoughton | 31 March 2022, 13:16:44 UTC | Remove superflous renamings fixes #146 | 26 April 2022, 16:30:56 UTC |
| 312ac25 | Pierre-Yves Strub | 31 March 2022, 06:36:38 UTC | [tactic]: [proc*]: fix procedure's arguments substitution Instead of introduce a single variable for the arguments tuple, introduce all the procedure's arguments as single program variables. Fix #166 | 26 April 2022, 16:30:56 UTC |
| 86b62e5 | François Dupressoir | 30 March 2022, 12:32:24 UTC | [chore] update theories/dune | 26 April 2022, 16:30:56 UTC |
| 7dbdbe0 | Pierre-Yves Strub | 29 March 2022, 18:47:14 UTC | [tactic]: [rewrite]: support for multi-rules `rewrite h` with `h : eq1 /\ eq2 /\ ... /\ eqn` is equivalent to `rewrite ?(h1, h2, ..., hn)` with `hi : eqi` address #155 | 26 April 2022, 16:30:56 UTC |
| 32578da | Pierre-Yves Strub | 29 March 2022, 08:01:08 UTC | License change: CeCILL B/C -> MIT | 26 April 2022, 16:30:22 UTC |
| a307890 | Christian Doczkal | 24 March 2022, 12:11:19 UTC | dopt: extend subdistribution to lossless distributions on options | 26 April 2022, 16:29:04 UTC |
| 47a2f63 | Pierre-Yves Strub | 29 March 2022, 08:23:24 UTC | [tactic]: in `apply... in...`, check that all variables are instantiated fix #149 | 26 April 2022, 16:29:04 UTC |
| 53651e1 | Pierre-Yves Strub | 28 March 2022, 16:59:08 UTC | [build]: [dune]: auto-generation of theories/dune | 26 April 2022, 16:29:04 UTC |
| 5dd9a9c | Adrien Koutsos | 11 April 2022, 09:12:40 UTC | improved substitution API for module idents | 11 April 2022, 09:12:40 UTC |
| 50961c7 | Adrien Koutsos | 08 April 2022, 09:39:43 UTC | fix: use the functor to retrieve the cost information and not the applied module | 08 April 2022, 09:41:52 UTC |
| 6cabd84 | Adrien Koutsos | 16 March 2022, 09:45:03 UTC | comments + assert | 16 March 2022, 09:45:03 UTC |
| 3466266 | Adrien Koutsos | 15 March 2022, 17:44:34 UTC | minor | 15 March 2022, 17:44:34 UTC |
| 905023b | Adrien Koutsos | 15 March 2022, 17:09:54 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-new-cost | 15 March 2022, 17:09:54 UTC |
| 45559bb | Adrien Koutsos | 15 March 2022, 15:38:15 UTC | [WIP] | 15 March 2022, 15:43:37 UTC |
| 9108d72 | Adrien Koutsos | 15 March 2022, 15:12:18 UTC | [WIP] | 15 March 2022, 15:12:18 UTC |
| c3be289 | Adrien Koutsos | 15 March 2022, 12:49:19 UTC | [WIP] | 15 March 2022, 12:49:19 UTC |
| a0fed93 | Adrien Koutsos | 14 March 2022, 18:57:39 UTC | [WIP] | 14 March 2022, 18:57:39 UTC |
| 928152b | Adrien Koutsos | 14 March 2022, 17:18:57 UTC | subst: distinguish between refreshing module and instantiating | 14 March 2022, 17:18:57 UTC |
| b93754a | Adrien Koutsos | 14 March 2022, 15:02:48 UTC | fixed hashed elgamal | 14 March 2022, 15:02:48 UTC |
| aa86882 | Oskar Goldhahn | 11 March 2022, 21:20:30 UTC | changed name of lemma | 14 March 2022, 13:40:02 UTC |
| c502b6b | Oskar Goldhahn | 11 March 2022, 18:14:23 UTC | added stronger version of dmap1E_can | 14 March 2022, 13:40:02 UTC |
| 6f177e1 | Adrien Koutsos | 14 March 2022, 13:38:34 UTC | pragma to retrieve the old behaviour on memory restrictions | 14 March 2022, 13:40:02 UTC |
| 2a9c1a7 | Adrien Koutsos | 13 March 2022, 07:40:36 UTC | smart constructors for module type and module sigs | 13 March 2022, 07:40:36 UTC |
| 15d9859 | Adrien Koutsos | 10 March 2022, 14:38:50 UTC | [WIP] substitution in module types | 10 March 2022, 14:38:50 UTC |
| d5f5cfd | Adrien Koutsos | 08 March 2022, 14:12:19 UTC | misc | 08 March 2022, 14:12:19 UTC |
| 5134807 | Adrien Koutsos | 08 March 2022, 10:19:57 UTC | fixed typing bug for module cost | 08 March 2022, 10:45:18 UTC |
| 1f5557e | Adrien Koutsos | 07 March 2022, 17:13:29 UTC | cleanup | 07 March 2022, 17:13:29 UTC |
| ddea5f0 | Adrien Koutsos | 07 March 2022, 16:37:29 UTC | fixed reduction issue because `zero` cost was not reduced | 07 March 2022, 16:37:29 UTC |
| 3457885 | Adrien Koutsos | 07 March 2022, 16:24:32 UTC | fixed fv computation in EcFol | 07 March 2022, 16:24:32 UTC |
| 954698e | Adrien Koutsos | 07 March 2022, 14:20:12 UTC | minor | 07 March 2022, 14:20:12 UTC |
| 64a96b2 | Adrien Koutsos | 07 March 2022, 11:24:16 UTC | fixed cost comparison + added hint simplify | 07 March 2022, 11:24:16 UTC |
| 0cfa98f | Adrien Koutsos | 07 March 2022, 10:49:58 UTC | fixed finiteness check in abstract call rule | 07 March 2022, 10:49:58 UTC |
| 1a360c7 | Pierre-Yves Strub | 04 March 2022, 13:18:40 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-cost-1.0-preview | 04 March 2022, 13:18:40 UTC |
| c98b014 | Kai-Chun Ning | 03 March 2022, 15:26:36 UTC | Extend standard library (IntDiv) with core results. | 03 March 2022, 18:13:54 UTC |
| 6be28ea | Adrien Koutsos | 03 March 2022, 15:12:50 UTC | fixed hash-el-gamal | 03 March 2022, 15:12:50 UTC |
| e22c918 | MM | 13 January 2022, 20:10:45 UTC | Added definition and lemmas for 'put' operator in List.ec. | 03 March 2022, 12:53:02 UTC |
| 982ef1d | Adrien Koutsos | 03 March 2022, 12:50:28 UTC | dh_enc_cost goes through. Still needs cleanup | 03 March 2022, 12:50:28 UTC |
| 086df70 | Adrien Koutsos | 03 March 2022, 12:23:15 UTC | progress dh_enc_cost | 03 March 2022, 12:23:15 UTC |
| c0247d3 | Adrien Koutsos | 03 March 2022, 12:22:56 UTC | finished sections | 03 March 2022, 12:22:56 UTC |
| 8cfa32b | Alley Stoughton | 29 March 2021, 13:09:27 UTC | An axiom-free formalization of well-founded relations, induction and recursion. | 03 March 2022, 09:50:40 UTC |
| 6199997 | Morten Solberg | 01 March 2022, 09:53:41 UTC | Generalize `LorR` theory Generalize the `LorR` theory to make it possible to give some input to `L.main` and `R.main`. Using the theory for procedures without input is still possible by cloning the theory with type `input <- unit`. | 03 March 2022, 09:50:19 UTC |
| c4f950f | Adrien Koutsos | 03 March 2022, 08:15:39 UTC | pushed not-working file. | 03 March 2022, 08:15:39 UTC |
| b06e700 | Pierre-Yves Strub | 02 March 2022, 16:27:38 UTC | Stdlib: more results on integer division & exponentiation | 02 March 2022, 16:28:09 UTC |
| c7cc569 | Adrien Koutsos | 01 March 2022, 14:26:07 UTC | fixed examples | 01 March 2022, 14:26:07 UTC |
| c316eff | Alley Stoughton | 01 March 2022, 14:04:58 UTC | Removed redundant "rec" in function declaration. | 01 March 2022, 14:04:58 UTC |
| f4a46ec | Adrien Koutsos | 01 March 2022, 13:45:11 UTC | section, first pass | 01 March 2022, 13:45:11 UTC |
| bd2af62 | Adrien Koutsos | 01 March 2022, 13:45:02 UTC | fixing examples | 01 March 2022, 13:45:02 UTC |
| 50452c5 | Adrien Koutsos | 01 March 2022, 11:03:03 UTC | fixed SplitRO | 01 March 2022, 11:03:03 UTC |
| 9a6a3ac | Adrien Koutsos | 01 March 2022, 11:00:24 UTC | do not print local memories in quantifiers | 01 March 2022, 11:00:24 UTC |
| a62441e | Adrien Koutsos | 01 March 2022, 10:36:18 UTC | use crush instead of progress in chacha_poly | 01 March 2022, 10:36:18 UTC |
| 2807d6e | Adrien Koutsos | 01 March 2022, 10:28:59 UTC | fixed chacha | 01 March 2022, 10:28:59 UTC |
| b56e8d0 | Adrien Koutsos | 28 February 2022, 15:59:38 UTC | allow explicit memory types in gbindings | 01 March 2022, 10:20:27 UTC |
| 77aac4b | Pierre-Yves Strub | 24 February 2022, 07:02:59 UTC | Revert "Unfold non-transparent operators in `case` & `elim`." This reverts commit 70662a755d2121ca1c809cf2eef68462bd720d72. | 24 February 2022, 07:02:59 UTC |
| 559910b | Benjamin Gregoire | 22 February 2022, 05:52:41 UTC | Partially fix memory capture in substitutions closes #130 | 22 February 2022, 09:41:14 UTC |
| ce4d8ca | François Dupressoir | 21 February 2022, 17:58:38 UTC | [dune+opam] fix git hash versioning widget | 21 February 2022, 18:24:12 UTC |
| 28c60b4 | Pierre-Yves Strub | 21 February 2022, 08:25:03 UTC | Merge branch '1.0' into deploy-cost-1.0-preview | 21 February 2022, 08:25:03 UTC |
| f278e3c | François Dupressoir | 14 December 2021, 12:22:51 UTC | Lemma stating equality of word and list distributions | 18 February 2022, 22:51:52 UTC |
| 70662a7 | Pierre-Yves Strub | 18 February 2022, 22:18:29 UTC | 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 |
| 03a3fe8 | Pierre-Yves Strub | 18 February 2022, 22:18:29 UTC | Fails gracefully when applying a tactic on a completed proof. fix #133 | 18 February 2022, 22:18:29 UTC |
| b71782f | Adrien Koutsos | 18 February 2022, 10:27:03 UTC | minor | 18 February 2022, 10:27:03 UTC |
| c3251b6 | Adrien Koutsos | 18 February 2022, 08:59:35 UTC | fixed example | 18 February 2022, 08:59:35 UTC |
| 53150bb | Adrien Koutsos | 17 February 2022, 17:15:48 UTC | fixed parser | 17 February 2022, 17:15:48 UTC |
| 7be9ac6 | Adrien Koutsos | 17 February 2022, 15:06:23 UTC | [WIP] | 17 February 2022, 15:59:32 UTC |
| d5a9f2b | Adrien Koutsos | 17 February 2022, 13:46:25 UTC | [WIP] | 17 February 2022, 13:46:25 UTC |
| 39b2562 | Pierre-Yves Strub | 16 February 2022, 06:38:28 UTC | Get rid of dune-site dune-site is currently in a very alpha-state and not stable enough. fix #99 fix #115 | 16 February 2022, 06:38:37 UTC |
| 4da7a10 | Adrien Koutsos | 15 February 2022, 17:51:24 UTC | [WIP] | 15 February 2022, 17:51:30 UTC |
| 01e6aee | Adrien Koutsos | 15 February 2022, 17:38:50 UTC | reduction rules for cost | 15 February 2022, 17:38:50 UTC |
| 1c0e36f | Adrien Koutsos | 15 February 2022, 16:59:38 UTC | fixes | 15 February 2022, 16:59:38 UTC |
| 76d410e | Adrien Koutsos | 14 February 2022, 17:35:58 UTC | 1.0 version of SDist with fixed syntax | 14 February 2022, 17:35:58 UTC |
| 222efc5 | Adrien Koutsos | 14 February 2022, 16:49:04 UTC | 1.0 versions of Hybird.ec and Indist.ec, with updated syntax | 14 February 2022, 16:49:04 UTC |
| 5532145 | Adrien Koutsos | 14 February 2022, 16:37:06 UTC | new syntax | 14 February 2022, 16:37:06 UTC |
| 56084f8 | Adrien Koutsos | 14 February 2022, 16:32:50 UTC | change Ideal.ec to the version in 1.0 | 14 February 2022, 16:32:50 UTC |
| ec7f718 | Adrien Koutsos | 14 February 2022, 16:27:02 UTC | [WIP] merge | 14 February 2022, 16:27:02 UTC |
| f933dd7 | Adrien Koutsos | 11 February 2022, 16:18:14 UTC | minor | 11 February 2022, 16:18:14 UTC |
| d123580 | Adrien Koutsos | 11 February 2022, 15:43:31 UTC | [WIP] fixing examples and theories | 11 February 2022, 15:43:31 UTC |
| ce56b10 | François Dupressoir | 19 January 2022, 19:29:05 UTC | Add rdirs option in config file closes #127 | 19 January 2022, 22:45:29 UTC |
| 46ba308 | Christian Doczkal | 14 December 2021, 09:43:58 UTC | Apply suggestions from code review Co-authored-by: Francois Dupressoir <fdupress@gmail.com> | 05 January 2022, 13:39:35 UTC |
| 49e768e | Christian Doczkal | 10 November 2021, 11:05:22 UTC | fix theories | 05 January 2022, 13:39:35 UTC |
| e77248a | Christian Doczkal | 09 November 2021, 15:40:12 UTC | allow zero queries in Hybrid and SDist | 05 January 2022, 13:39:35 UTC |
| 49aec58 | Christian Doczkal | 10 December 2021, 15:21:46 UTC | lemmas on FSet, List, and DList | 10 December 2021, 17:02:37 UTC |
