| 058aeeb | Adrien Koutsos | 12 May 2022, 17:14:27 UTC | progress in composition cost | 12 May 2022, 17:14:27 UTC |
| 1f7d4a7 | Adrien Koutsos | 12 May 2022, 16:19:56 UTC | cleaned-up various cost (in particular epoch-related) todos | 12 May 2022, 16:19:56 UTC |
| e8473ba | Adrien Koutsos | 12 May 2022, 10:08:50 UTC | simplification rules of cost comparison based on epochs | 12 May 2022, 10:19:49 UTC |
| f4b4c0f | Adrien Koutsos | 11 May 2022, 17:11:58 UTC | [WIP] cost simplification using epochs | 11 May 2022, 17:11:58 UTC |
| af6a0ed | Adrien Koutsos | 11 May 2022, 16:03:59 UTC | fix subtyping bug | 11 May 2022, 16:03:59 UTC |
| 2fdc6e1 | Adrien Koutsos | 11 May 2022, 15:45:31 UTC | fixed: refresh module instead of module substitution | 11 May 2022, 15:45:31 UTC |
| 0853556 | Adrien Koutsos | 11 May 2022, 15:08:17 UTC | check that CHoare is loaded before generating proof obligation. | 11 May 2022, 15:08:17 UTC |
| 163c0a0 | Adrien Koutsos | 11 May 2022, 10:05:32 UTC | added epoch in local declarations | 11 May 2022, 10:05:32 UTC |
| b6602ec | Pierre-Yves Strub | 10 May 2022, 12:14:09 UTC | Change configuration file resolution Do not consider locations that point to non-existing files. The configuration file location is now printing by the `config` command. | 10 May 2022, 13:34:29 UTC |
| eedf9d2 | Pierre-Yves Strub | 09 May 2022, 10:46:10 UTC | Finite.to_seq: now have a body based on choiceb Co-authored-by: Christian Doczkal <christian.doczkal@mpi-sp.org> | 10 May 2022, 13:34:29 UTC |
| c7851aa | Pierre-Yves Strub | 05 May 2022, 06:55:44 UTC | Bump Why3 version from 1.4.x to 1.5.0 fix #184 | 10 May 2022, 13:34:29 UTC |
| b753c9f | Pierre-Yves Strub | 05 May 2022, 08:02:38 UTC | [github-action]: do not start as root This requires a modification of the docker image s.t. the user UID is compatible with the one used by Github Action | 10 May 2022, 13:34:29 UTC |
| f1093b8 | Pierre-Yves Strub | 27 April 2022, 12:46:45 UTC | Use local configuration file in priority | 10 May 2022, 13:34:29 UTC |
| 260f326 | Pierre-Yves Strub | 27 April 2022, 12:46:13 UTC | Fic computation of source root for local builds | 10 May 2022, 13:34:29 UTC |
| 1368273 | Pierre-Yves Strub | 27 April 2022, 09:41:00 UTC | Fix the license announced in the banner | 10 May 2022, 13:34:29 UTC |
| f3071a1 | Adrien Koutsos | 09 May 2022, 16:45:49 UTC | refactoring: local declarations are now records | 09 May 2022, 16:45:49 UTC |
| 65e3be8 | Adrien Koutsos | 05 May 2022, 16:44:46 UTC | tentative new technique to make complexity proof obligation still work in progress | 05 May 2022, 16:44:46 UTC |
| 8352f49 | Adrien Koutsos | 05 May 2022, 14:49:26 UTC | add test file for cost | 05 May 2022, 14:49:26 UTC |
| 28c4bf8 | Adrien Koutsos | 05 May 2022, 14:46:47 UTC | destruct_cost using hypothesis | 05 May 2022, 14:46:47 UTC |
| d411922 | Adrien Koutsos | 05 May 2022, 13:39:01 UTC | started to adapt the composition cost proof | 05 May 2022, 13:39:01 UTC |
| 4335cc5 | Adrien Koutsos | 05 May 2022, 13:06:40 UTC | fixed bad implicit arguments for cost call rule | 05 May 2022, 13:06:40 UTC |
| 94dcd47 | Adrien Koutsos | 05 May 2022, 11:36:12 UTC | fixed issue with infinite intrinsic cost infinite intrinsic cost was absorbing oracle call constraints | 05 May 2022, 11:36:12 UTC |
| c13099e | Adrien Koutsos | 04 May 2022, 10:18:31 UTC | rules to prove subcond side-conditions | 04 May 2022, 11:30:55 UTC |
| 2312419 | Adrien Koutsos | 04 May 2022, 09:19:19 UTC | removed projection over concrete cost, which is unsound. | 04 May 2022, 09:22:07 UTC |
| 29b926f | Adrien Koutsos | 04 May 2022, 07:49:37 UTC | added additional opacity check in LowGoal | 04 May 2022, 07:49:37 UTC |
| 4015176 | Adrien Koutsos | 03 May 2022, 15:22:13 UTC | abstract module now have an opacity, giving their cost when called The opacity of a module is either Opaque (default) or Open. Essentially, the opacity tells what is the intrinsic cost of an abstract module when it is called. If `A` has type `M[f : [c, ...]]` then: - if A module type is opaque, then calling A.f costs `[A.f : '1]` - if A module type is open, then calling A.f costs `c` Opacity is denoted by adding the `open` or `opaque` keyword in a module complexity restriction, e.g. `M[open f : ...]`. No explicit opacity means Opaque. | 03 May 2022, 15:22:13 UTC |
| 17ae2d3 | Adrien Koutsos | 29 April 2022, 15:32:59 UTC | better printing + work on costs | 29 April 2022, 15:32:59 UTC |
| f37b697 | Adrien Koutsos | 29 April 2022, 12:35:53 UTC | bigcost morphism rule added to reduce_logic | 29 April 2022, 12:41:50 UTC |
| 163abd8 | Adrien Koutsos | 29 April 2022, 09:31:14 UTC | printing: better alignement in cost vectors | 29 April 2022, 09:31:14 UTC |
| 6ab4890 | Adrien Koutsos | 29 April 2022, 08:43:58 UTC | simplifications of choare statements | 29 April 2022, 08:43:58 UTC |
| 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 |
