| a430e75 | Adrien Koutsos | 20 February 2020, 17:02:20 UTC | Optional type in cost statement, when necessary. | 20 February 2020, 17:02:20 UTC |
| 04a6445 | Adrien Koutsos | 20 February 2020, 15:14:45 UTC | Eop are not free. | 20 February 2020, 15:14:45 UTC |
| 17c2f3c | Adrien Koutsos | 20 February 2020, 15:08:33 UTC | Slight printing improvement. | 20 February 2020, 15:08:33 UTC |
| 822f85b | Adrien Koutsos | 20 February 2020, 11:39:45 UTC | Subst error | 20 February 2020, 11:39:45 UTC |
| 8bca1a6 | Adrien Koutsos | 20 February 2020, 10:36:33 UTC | Cost is polymorphic. | 20 February 2020, 10:36:33 UTC |
| 32cb9d9 | Adrien Koutsos | 20 February 2020, 10:19:08 UTC | Bug fix in alpha-equality checking. | 20 February 2020, 10:19:08 UTC |
| ea55f42 | Adrien Koutsos | 20 February 2020, 09:19:12 UTC | Bug fix for the parser, with memories in cost statements. | 20 February 2020, 09:19:12 UTC |
| d443c0d | Adrien Koutsos | 19 February 2020, 16:58:38 UTC | Started to add instantiation of schemas. | 19 February 2020, 16:58:38 UTC |
| 10b9097 | Pierre-Yves Strub | 15 February 2020, 09:20:51 UTC | drop python2 support | 15 February 2020, 09:20:51 UTC |
| 44b23b5 | Pierre-Yves Strub | 15 February 2020, 07:19:25 UTC | Allow operators of the form 'n where n is a *fixed* natural number | 15 February 2020, 07:19:25 UTC |
| 6db51b8 | Adrien Koutsos | 14 February 2020, 17:11:18 UTC | Added schemata, and cost judgement to the parser and type-checker. | 14 February 2020, 17:11:18 UTC |
| 11a8759 | Benjamin Gregoire | 14 February 2020, 08:36:31 UTC | better conversion + simplify reduction algorithm. | 14 February 2020, 08:36:31 UTC |
| e30318c | Adrien Koutsos | 13 February 2020, 17:02:48 UTC | minors | 13 February 2020, 17:02:48 UTC |
| 0a14a28 | Adrien Koutsos | 13 February 2020, 09:45:32 UTC | Do not add cost of free expressions, + extended example. | 13 February 2020, 09:45:32 UTC |
| 4f587f3 | Pierre-Yves Strub | 13 February 2020, 09:06:03 UTC | "hint simplify [reduce]" does one head reduction for finding the quantifers | 13 February 2020, 09:06:03 UTC |
| 2bbf3d3 | Pierre-Yves Strub | 13 February 2020, 08:38:38 UTC | Add new options to 'hint simplify': - reduce: equations are found up-to reduction - eqtrue: if no equations can be found, add a equation of the form (e = true) | 13 February 2020, 08:38:38 UTC |
| e40e1c5 | Adrien Koutsos | 12 February 2020, 17:37:54 UTC | Improved syntax for restrictions. | 12 February 2020, 17:37:54 UTC |
| 2674137 | Adrien Koutsos | 12 February 2020, 16:20:31 UTC | Extended example. | 12 February 2020, 16:20:31 UTC |
| ff0921c | Adrien Koutsos | 12 February 2020, 16:19:20 UTC | Fix in while tactic (in sums). | 12 February 2020, 16:19:20 UTC |
| 850c717 | Adrien Koutsos | 12 February 2020, 16:18:47 UTC | Fix call tactic + improved printing for call. | 12 February 2020, 16:18:47 UTC |
| 28a547a | Adrien Koutsos | 12 February 2020, 16:18:30 UTC | Fix for conseq tactic. | 12 February 2020, 16:18:30 UTC |
| 1efcb37 | Adrien Koutsos | 12 February 2020, 12:51:48 UTC | Improved call rule | 12 February 2020, 12:51:48 UTC |
| 21d2ca8 | Adrien Koutsos | 12 February 2020, 12:51:41 UTC | Minor fix | 12 February 2020, 12:51:41 UTC |
| 0d79b94 | Adrien Koutsos | 12 February 2020, 10:53:34 UTC | Example. | 12 February 2020, 10:53:34 UTC |
| a04a396 | Adrien Koutsos | 12 February 2020, 10:52:49 UTC | Improved call rule application (smaller premises). | 12 February 2020, 10:52:49 UTC |
| 44b80c0 | Adrien Koutsos | 12 February 2020, 10:52:37 UTC | improved parser for call tactic. | 12 February 2020, 10:52:37 UTC |
| 8540969 | Adrien Koutsos | 12 February 2020, 10:26:05 UTC | Fix for substitutions in coe | 12 February 2020, 10:26:05 UTC |
| a055a3e | Adrien Koutsos | 12 February 2020, 09:45:11 UTC | The same xfun could be added twice to the cost, causing errors. | 12 February 2020, 09:45:11 UTC |
| b648778 | Adrien Koutsos | 11 February 2020, 17:22:03 UTC | Bug fix, or how not to trust too much the type system. | 11 February 2020, 17:22:03 UTC |
| 1992d9c | Adrien Koutsos | 11 February 2020, 16:24:00 UTC | Bug fix | 11 February 2020, 16:24:00 UTC |
| 2efb9e7 | François Dupressoir | 10 February 2020, 09:50:13 UTC | Consolidate PRP and PRF libraries Including weak PRP-PRF switching lemma, but not its strong version Squashed commit of the following: commit 005342f19a55b0ae01c88c0c729fdbad3f2519ff Merge: 5407570b 7325ae6d Author: François Dupressoir <fdupress@gmail.com> Date: Mon Feb 10 09:48:54 2020 +0000 Merge branch '1.0' into deploy-simpler-rp commit 5407570bbdeaee7b725f57fcdbbf764ff301ac9e Author: François Dupressoir <fdupress@gmail.com> Date: Fri Jan 24 12:00:21 2020 +0000 move towards merging PRF and RO also clean assignment notation commit 65e0c4eb8c702729500148e34900dc5971e583a7 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 14:14:29 2020 +0000 Integrate PRP-PRF switching lemma into PRP lib Not done for the strong version yet commit 456a7c96e40fa6827d92fbc36d8cd75fdd8abab1 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:40:25 2020 +0000 Simplifying the PRF interface No keys are needed for the ideal RP, The raw interface can be defined separately as needed. commit e7dea73e6eae21f192efc45f42e9cdc9e5ec4eb8 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:19:04 2020 +0000 Some nits commit 8bb90549b6084ea8189e3a4067a155f977ccd34a Author: François Dupressoir <fdupress@gmail.com> Date: Mon Jan 20 16:38:30 2020 +0000 Cleanup PRP/PRF and PRP-PRF | 10 February 2020, 09:50:13 UTC |
| 7325ae6 | Pierre-Yves Strub | 10 February 2020, 09:43:29 UTC | Refactor PlugAndPray | 10 February 2020, 09:45:08 UTC |
| 3137e16 | Adrien Koutsos | 07 February 2020, 16:47:17 UTC | Bug fix. | 07 February 2020, 16:47:17 UTC |
| fb4a0fd | Adrien Koutsos | 07 February 2020, 14:47:27 UTC | Two printing fixes. | 07 February 2020, 14:47:27 UTC |
| 06bfaf4 | Adrien Koutsos | 06 February 2020, 13:28:22 UTC | Restriction syntax small simplification. No need to provide the name of the functor to refer to its (maybe implicit) parameters. | 06 February 2020, 13:28:22 UTC |
| e25ee11 | Adrien Koutsos | 06 February 2020, 13:24:07 UTC | Small fixes. | 06 February 2020, 13:24:07 UTC |
| 7d42518 | Adrien Koutsos | 06 February 2020, 11:30:16 UTC | Can have extended restr. in quantification and loc. declarations. | 06 February 2020, 11:30:16 UTC |
| c179aad | Adrien Koutsos | 05 February 2020, 16:47:47 UTC | Mutually recursion in typing, to deal with dependent types. I only moved code around, and made everybody mutually recursive. | 05 February 2020, 16:47:47 UTC |
| 7c6da58 | Adrien Koutsos | 05 February 2020, 16:47:32 UTC | Typing of formulas in restrictions | 05 February 2020, 16:47:32 UTC |
| c57b77a | Adrien Koutsos | 05 February 2020, 16:44:03 UTC | Fixed parser | 05 February 2020, 16:44:03 UTC |
| a5e4020 | Adrien Koutsos | 05 February 2020, 15:36:28 UTC | Restrictions can be partially supplied. | 05 February 2020, 15:36:28 UTC |
| eff1631 | Adrien Koutsos | 04 February 2020, 16:26:44 UTC | Updated example. | 04 February 2020, 16:26:44 UTC |
| 78f237e | Adrien Koutsos | 04 February 2020, 16:26:09 UTC | Allow for complexity restrictions in function declarations. Typing of these restrictions is not yet done. | 04 February 2020, 16:26:09 UTC |
| 00c8584 | Adrien Koutsos | 04 February 2020, 14:30:16 UTC | Same syntax for printing and parsing. | 04 February 2020, 14:30:16 UTC |
| d536224 | Adrien Koutsos | 04 February 2020, 14:03:33 UTC | Improved printing. | 04 February 2020, 14:03:33 UTC |
| 35ff228 | Adrien Koutsos | 04 February 2020, 12:47:50 UTC | Removed self intrisinc cost from module restrictions. | 04 February 2020, 12:47:50 UTC |
| 63f5a17 | Adrien Koutsos | 04 February 2020, 10:44:06 UTC | Merge branch 'deploy-simpler-xpaths' into deploy-cost | 04 February 2020, 10:44:06 UTC |
| ed1db7c | Adrien Koutsos | 03 February 2020, 15:56:52 UTC | Updated the examples. | 03 February 2020, 15:56:52 UTC |
| 58d252a | Adrien Koutsos | 03 February 2020, 15:37:41 UTC | Updated the theories. | 03 February 2020, 15:41:29 UTC |
| 688ec58 | Adrien Koutsos | 03 February 2020, 15:17:14 UTC | Parsing for improved memory restrictions. | 03 February 2020, 15:17:14 UTC |
| 180d323 | Pierre-Yves Strub | 27 January 2020, 13:48:30 UTC | Merge branch 'deploy-extended-tests' into deploy-simpler-xpaths | 27 January 2020, 13:48:30 UTC |
| 9db28d5 | Pierre-Yves Strub | 27 January 2020, 13:46:58 UTC | script for testing EasyCrypt on various external devs | 27 January 2020, 13:46:58 UTC |
| 2e7d1e6 | Benjamin Gregoire | 27 January 2020, 09:31:49 UTC | First version that seems to work | 27 January 2020, 09:31:49 UTC |
| 74084f2 | Benjamin Gregoire | 26 January 2020, 10:21:17 UTC | WIP | 26 January 2020, 10:21:17 UTC |
| 0c7d992 | Benjamin Gregoire | 24 January 2020, 16:03:55 UTC | remove a remaining TODO A | 24 January 2020, 16:03:55 UTC |
| d940c4c | Benjamin Gregoire | 24 January 2020, 15:50:37 UTC | first version that compile | 24 January 2020, 15:50:37 UTC |
| fd37de4 | Adrien Koutsos | 24 January 2020, 14:30:13 UTC | Improved memory restrictions. Allow for variable in memory restrictions. Allow for positive and negative restrictions. Not fully done. | 24 January 2020, 14:30:13 UTC |
| fdc80db | Adrien Koutsos | 23 January 2020, 18:21:32 UTC | Added modules restrictions to the parser. The parser's output is not yet processed, and the module typing does not yet check the restriction. | 23 January 2020, 18:21:32 UTC |
| 6770045 | Adrien Koutsos | 23 January 2020, 15:29:59 UTC | Minor. New while example + printing. | 23 January 2020, 15:31:29 UTC |
| f91eb9b | Adrien Koutsos | 23 January 2020, 15:10:28 UTC | Fix the substitution in coe predicate. | 23 January 2020, 15:23:19 UTC |
| a6e66c9 | Adrien Koutsos | 23 January 2020, 15:09:59 UTC | Revert the previous commit. Except for the printing changes. This reverts commit a701153ac01419f4f6d5f1c558b8c36cf9f81014. | 23 January 2020, 15:09:59 UTC |
| a701153 | Adrien Koutsos | 23 January 2020, 13:48:54 UTC | Changed the coe predicate to use a memtype instead of a full memenv. This is to avoid problems with substitutions, that were catching the memenv name even thoug it is never used. | 23 January 2020, 13:48:54 UTC |
| e4ab48b | Adrien Koutsos | 22 January 2020, 15:27:50 UTC | Added the CHoareTactic theory. | 22 January 2020, 15:27:50 UTC |
| 5ee8edc | Adrien Koutsos | 22 January 2020, 15:07:06 UTC | Implemented the inline tactic for choare. | 22 January 2020, 15:07:06 UTC |
| cd2f29b | Adrien Koutsos | 22 January 2020, 15:00:47 UTC | Added the Coe formula. The parser is not yet updated, we need to merge deploy-simpler-xpaths first for it. | 22 January 2020, 15:00:47 UTC |
| 60e1e9d | Adrien Koutsos | 21 January 2020, 17:09:35 UTC | Started to add the cost_of_expr predicate. | 21 January 2020, 17:09:35 UTC |
| bcd669f | Adrien Koutsos | 21 January 2020, 15:42:25 UTC | Hashing memenv in formulas. | 21 January 2020, 15:42:25 UTC |
| 4e7efec | Adrien Koutsos | 21 January 2020, 15:14:05 UTC | Started changing the memory types, xpath shapes, and pvar shapes. Far from finished. | 21 January 2020, 15:14:05 UTC |
| 951932a | Adrien Koutsos | 21 January 2020, 09:30:33 UTC | Minor. | 21 January 2020, 09:30:33 UTC |
| 61f7bb1 | Adrien Koutsos | 17 January 2020, 17:12:30 UTC | Added an example file, to be completed. | 17 January 2020, 17:12:30 UTC |
| 85dd8df | Adrien Koutsos | 17 January 2020, 17:11:53 UTC | minor improvements. | 17 January 2020, 17:11:53 UTC |
| f6d2dcb | Adrien Koutsos | 17 January 2020, 17:11:39 UTC | bug fix for wp. | 17 January 2020, 17:11:39 UTC |
| 61226a8 | Adrien Koutsos | 17 January 2020, 15:59:15 UTC | Renamed back hoare constructors and fields to original names. | 17 January 2020, 15:59:15 UTC |
| 50ed0b8 | Adrien Koutsos | 17 January 2020, 15:53:07 UTC | Rule for abstract calls. | 17 January 2020, 15:53:07 UTC |
| 9e11412 | François Dupressoir | 16 January 2020, 20:48:25 UTC | 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 |
| 4414cab | Adrien Koutsos | 16 January 2020, 17:46:44 UTC | Started implementing the [proc] tactic for abstract procedures. | 16 January 2020, 17:46:44 UTC |
| 16fc2b3 | Adrien Koutsos | 16 January 2020, 15:30:12 UTC | creation of choare formulas and costs from EcParsetree types. | 16 January 2020, 15:30:12 UTC |
| 308792e | Adrien Koutsos | 16 January 2020, 15:14:16 UTC | Removed warnings. | 16 January 2020, 15:14:16 UTC |
| a2e41d8 | Adrien Koutsos | 16 January 2020, 13:06:35 UTC | Cost counting self cost + bounds on number of calls to the oracles. | 16 January 2020, 13:06:35 UTC |
| 1aeed31 | Adrien Koutsos | 15 January 2020, 17:49:25 UTC | Started extending costs to included bounds on oracle calls. | 15 January 2020, 17:49:25 UTC |
| 73d8b75 | Adrien Koutsos | 15 January 2020, 14:18:54 UTC | Type-checking now verifies that complexity resticitions are valid. | 15 January 2020, 14:18:54 UTC |
| 258e25e | Adrien Koutsos | 15 January 2020, 12:36:35 UTC | cleanup | 15 January 2020, 12:36:35 UTC |
| b79fe3b | Adrien Koutsos | 15 January 2020, 11:00:47 UTC | pretty printer | 15 January 2020, 11:00:47 UTC |
| 72847a9 | Adrien Koutsos | 15 January 2020, 10:16:12 UTC | pretty printer | 15 January 2020, 10:16:12 UTC |
| e01e01d | Adrien Koutsos | 14 January 2020, 17:52:04 UTC | some cleaning, plus pretty printers | 14 January 2020, 17:52:04 UTC |
| a56336a | Adrien Koutsos | 14 January 2020, 16:54:43 UTC | Some cleanup | 14 January 2020, 16:54:43 UTC |
| 76fa43a | Adrien Koutsos | 14 January 2020, 15:35:52 UTC | Added some type dependencies between module types and formulas. | 14 January 2020, 15:35:52 UTC |
| 7009577 | Adrien Koutsos | 14 January 2020, 12:05:09 UTC | Started adding some type dependencies between modules and formulas. | 14 January 2020, 12:05:09 UTC |
| ba6ed2b | Adrien Koutsos | 14 January 2020, 09:21:09 UTC | interface for oracle calls | 14 January 2020, 09:21:09 UTC |
| 7e1f524 | Adrien Koutsos | 13 January 2020, 15:10:03 UTC | Minor | 13 January 2020, 15:10:03 UTC |
| 21e7b33 | Adrien Koutsos | 13 January 2020, 13:53:04 UTC | Part of the conseq and call tactics for cost judgement. | 13 January 2020, 13:53:04 UTC |
| 80c2289 | Adrien Koutsos | 13 January 2020, 09:36:05 UTC | Minor correction in while tactic for cost. | 13 January 2020, 09:36:05 UTC |
| d35c807 | Adrien Koutsos | 10 January 2020, 17:21:41 UTC | Fix the call tactic. It was not checking independence of the cost correctly. | 10 January 2020, 17:21:41 UTC |
| 8c0a3c2 | Adrien Koutsos | 10 January 2020, 16:57:07 UTC | cleanup | 10 January 2020, 16:57:07 UTC |
| c6aa095 | Adrien Koutsos | 10 January 2020, 16:54:05 UTC | While tactic for cost judgement. | 10 January 2020, 16:54:05 UTC |
| 6d5eca6 | Adrien Koutsos | 10 January 2020, 16:15:22 UTC | cleanup | 10 January 2020, 16:15:22 UTC |
| 1f7bdd2 | Adrien Koutsos | 10 January 2020, 13:26:16 UTC | removed mli entry for inline_choare. | 10 January 2020, 13:26:16 UTC |
| dc2bcab | Adrien Koutsos | 10 January 2020, 13:26:07 UTC | removed warnings. | 10 January 2020, 13:26:07 UTC |
| b46db7e | Adrien Koutsos | 10 January 2020, 13:23:54 UTC | App (seq) tactic for cost judgement. | 10 January 2020, 13:23:54 UTC |
| e9cf816 | Adrien Koutsos | 10 January 2020, 13:23:45 UTC | Typo | 10 January 2020, 13:23:45 UTC |
