| 32f0ee5 | Adrien Koutsos | 25 August 2023, 16:20:56 UTC | [cost v2] printing of full mpath + first wrapped mpath in the parser | 25 August 2023, 16:20:56 UTC |
| f688844 | Adrien Koutsos | 25 August 2023, 14:05:00 UTC | [cost v2] wrapped module path in CHoare | 25 August 2023, 14:05:00 UTC |
| e5e946c | Adrien Koutsos | 25 August 2023, 13:50:05 UTC | [cost v2] minor | 25 August 2023, 13:50:05 UTC |
| 237f245 | Adrien Koutsos | 25 August 2023, 13:33:20 UTC | [cost v2] minor | 25 August 2023, 13:33:20 UTC |
| 15804c7 | Adrien Koutsos | 25 August 2023, 13:02:46 UTC | [cost v2] typing of module paths | 25 August 2023, 13:08:49 UTC |
| 9809974 | Adrien Koutsos | 25 August 2023, 12:50:17 UTC | [cost v2] resolution of parsed module path, typing unfinished | 25 August 2023, 12:50:17 UTC |
| 9211dcb | Adrien Koutsos | 24 August 2023, 16:52:35 UTC | [cost v2] parsing rules for module path, typing remains to be done | 24 August 2023, 16:52:35 UTC |
| a6a0195 | Adrien Koutsos | 24 August 2023, 14:22:51 UTC | [cost v2] removed quantification over agents in formulas | 24 August 2023, 14:22:51 UTC |
| fb5e115 | Adrien Koutsos | 24 August 2023, 14:05:38 UTC | [cost v2] fixed a bug where conversion was stronger than it should | 24 August 2023, 14:10:34 UTC |
| 358ec8f | Adrien Koutsos | 24 August 2023, 14:05:12 UTC | [cost v2] various changes to help debugging | 24 August 2023, 14:05:12 UTC |
| 5e7284a | Adrien Koutsos | 24 August 2023, 11:32:10 UTC | [cost v2] various small changes disable some checks in EcEnv.Agent, as it is unused for now minor fix in EcLowGoal sub-hyp check printing of agent names in sequents cost simplification + somes tests | 24 August 2023, 11:32:10 UTC |
| dd9ed5b | Adrien Koutsos | 24 August 2023, 09:44:09 UTC | [cost v2] cost simplification + somes tests | 24 August 2023, 09:44:09 UTC |
| 3b2e441 | Adrien Koutsos | 24 August 2023, 08:44:14 UTC | [cost v2] a few test files | 24 August 2023, 08:44:14 UTC |
| 01adbed | Adrien Koutsos | 24 August 2023, 08:41:01 UTC | [cost v2] commented-out some more cost-related examples | 24 August 2023, 08:42:01 UTC |
| 8d1c9d1 | Adrien Koutsos | 24 August 2023, 08:39:14 UTC | [cost v2] fixed Cramer Shoup: desambiguate ZModE.zero from Cost.zero | 24 August 2023, 08:39:14 UTC |
| 9f10127 | Adrien Koutsos | 24 August 2023, 08:38:48 UTC | [cost v2] moved functions that need to be globally available to Pervasive | 24 August 2023, 08:38:48 UTC |
| f76a5a2 | Adrien Koutsos | 24 August 2023, 08:38:28 UTC | [cost v2] commented-out some cost-related examples for now | 24 August 2023, 08:38:41 UTC |
| ddd405e | Adrien Koutsos | 23 August 2023, 13:47:30 UTC | [cost v2] fix compilation | 23 August 2023, 14:13:23 UTC |
| fe23a65 | Adrien Koutsos | 23 August 2023, 12:11:17 UTC | Merge remote-tracking branch 'origin/main' into deploy-new-cost2 | 23 August 2023, 12:11:17 UTC |
| 6a203df | François Dupressoir | 07 August 2023, 17:23:25 UTC | fix smt that regressed with z3 bump to 4.12.2 all else being equal, works with 4.12.1, fails with 4.12.2 fails with all other solvers | 12 August 2023, 08:57:48 UTC |
| ae29508 | François Dupressoir | 07 August 2023, 16:24:22 UTC | pin alt-ergo, z3 | 12 August 2023, 08:57:48 UTC |
| 705bafe | François Dupressoir | 07 August 2023, 16:20:33 UTC | refactor nix to avoid repetition | 12 August 2023, 08:57:48 UTC |
| 95cabb9 | François Dupressoir | 04 August 2023, 10:31:26 UTC | add support for test config 'report' option there is currently no way of asking for a report with 'easycrypt runtest' | 07 August 2023, 17:56:12 UTC |
| da3be5c | François Dupressoir | 04 August 2023, 10:30:36 UTC | [chore] whitespace | 07 August 2023, 17:56:12 UTC |
| a72dada | Yi Lee | 01 August 2023, 03:48:35 UTC | Propagate subtype changes to Word | 02 August 2023, 00:47:04 UTC |
| 917bba2 | Pierre Boutry | 20 July 2023, 13:30:54 UTC | Ring/field tactics available as soon as an instance is found. | 20 July 2023, 13:49:02 UTC |
| e75a7cf | Oskar Goldhahn | 12 July 2023, 22:38:59 UTC | get rid of unbounded smt calls outside examples | 20 July 2023, 13:22:13 UTC |
| 1bb2e2d | mm | 19 July 2023, 07:20:20 UTC | Additonal lemmas on fset equality establishing an equivalence, and additional lemma on perm_eq and undup (making the oflist_perm_eq lemma redundant). | 19 July 2023, 08:46:42 UTC |
| 6e066e6 | Pierre-Yves Strub | 13 July 2023, 11:06:46 UTC | Fix wording of error messages "function" -> "procedure" fix #417 | 13 July 2023, 11:07:33 UTC |
| add9232 | Christian Doczkal | 30 June 2023, 09:48:34 UTC | [chore] fix more raw smt calls | 11 July 2023, 20:01:13 UTC |
| 0c60516 | Christian Doczkal | 29 June 2023, 12:13:30 UTC | [chore] fix raw smt calls (theories/distributions) | 11 July 2023, 20:01:13 UTC |
| 757ec09 | François Dupressoir | 26 June 2023, 13:52:42 UTC | [chore] remove more raw smt calls | 29 June 2023, 13:20:43 UTC |
| 85d03a2 | Christian Doczkal | 29 June 2023, 11:18:26 UTC | [chore] fix some warnings and flaky smt calls (#408) | 29 June 2023, 11:18:26 UTC |
| cddd7d9 | Christian Doczkal | 28 June 2023, 14:58:53 UTC | [theories] define product using allpairs (#411) | 28 June 2023, 14:58:53 UTC |
| 60c3179 | Romain Tetley | 28 June 2023, 12:25:32 UTC | Renaming the easycrypt lib (making it easyier for external imports) (#410) | 28 June 2023, 12:25:32 UTC |
| 73ac095 | Pierre-Yves Strub | 27 June 2023, 06:47:59 UTC | proc op: add support for the "local" modifier | 27 June 2023, 13:55:48 UTC |
| 3693e61 | Christian Doczkal | 22 June 2023, 13:18:15 UTC | [theories] additional elimination rules for finite sums (#401) | 22 June 2023, 13:18:15 UTC |
| c0eeee4 | Pierre-Yves Strub | 21 June 2023, 10:19:54 UTC | Refactor out Fermat's little theorem from ZModP to IntDiv | 21 June 2023, 10:34:00 UTC |
| 4965377 | Yi Lee | 21 June 2023, 01:49:39 UTC | Prove Fermat's little theorem | 21 June 2023, 10:34:00 UTC |
| e38fac3 | Cameron Low | 13 June 2023, 20:55:00 UTC | Keep f_let_simp | 16 June 2023, 10:40:43 UTC |
| d1858f6 | Alley Stoughton | 05 June 2023, 14:42:45 UTC | Remove dead code relating to substitution; instead, the f_subst mechanism should be used. (And this is in fact done for simplification of let formulas in EcReduction.) | 16 June 2023, 10:40:43 UTC |
| 341cc08 | Benjamin Gregoire | 26 October 2022, 18:18:55 UTC | New inline tactic We realized that sometimes we want to inline everything besides one procedure and found that it is cumbersome to have to list everything that has to be inlined instead of listing what should remain as is. So we decided to add this to the current inline. We should have kept the previous use cases identical as supported by the fact that nothing broke while not touching any old ec files. In doing so, we also added the possibility to provide the name of a module leading to inlining all the procedure in this module. Finally, one can now provide the name of a procedure and it will inline all the procedures with that name regardless of the module in which they belong. As already mentioned, one can find examples at the following link. https://github.com/EasyCrypt/easycrypt/blob/deploy-inline/examples/tactics/inline.ec start with parsing pattern matching on inline add some examples fix | 16 June 2023, 10:39:43 UTC |
| f0e15c2 | Romain Tetley | 15 June 2023, 14:57:04 UTC | Turned the files in src into a lib called Core. (#397) * Turned the files in src into a lib called core. * Removed reference to dead code in dune file The file ecCoreHiPhl was removed as dead code, no need to exclude it in the dune file anymore. --------- Co-authored-by: Romain Tetley <rtetley@inria.fr> | 15 June 2023, 14:57:04 UTC |
| 8232d04 | Romain Tetley | 15 June 2023, 14:19:31 UTC | Remove dead code (#398) The file ecCoreHiPhl.ml seems to be dead code because: - It contains an open EcLogic which was deleted in 2014 (commit 6fe0ea944a53ffc89bdde9bb70f81629ff764c97) - The last time it was modified (apart from licence headers) was in 2013 (commit f2e05e2688ab1894daf760ed255060253839286c) | 15 June 2023, 14:19:31 UTC |
| b0eeedc | Yi Lee | 10 June 2023, 12:55:36 UTC | Take PolyReduce theory from Kyber project Add choice-based inverses and fix broken proofs from subtype changes Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> | 13 June 2023, 09:09:31 UTC |
| dfec6be | François Dupressoir | 27 March 2023, 08:59:03 UTC | restore name | 13 June 2023, 07:53:12 UTC |
| a4a0332 | François Dupressoir | 24 March 2022, 15:55:56 UTC | Tighten the ROM bad call results | 13 June 2023, 07:53:12 UTC |
| d481338 | François Dupressoir | 05 June 2023, 14:21:42 UTC | [lib] FSet: fcard_eq1 Co-authored-by: Christian Doczkal <christian.doczkal@mpi-sp.org> | 13 June 2023, 07:30:41 UTC |
| c73033b | François Dupressoir | 05 June 2023, 21:54:01 UTC | [lib] List: remove all raw smt calls | 13 June 2023, 07:14:59 UTC |
| ab21d3a | Pierre-Yves Strub | 12 June 2023, 11:53:09 UTC | New rewrite-pr lemma: Pr[muE] Transform a Pr[...] statement into its pointwise summation. | 12 June 2023, 12:22:39 UTC |
| 16747c7 | François Dupressoir | 04 May 2023, 10:24:24 UTC | properly fail early if one SMT returns `Invalid` This was seemingly intended, but racy | 10 June 2023, 22:35:56 UTC |
| cf55a7c | François Dupressoir | 04 May 2023, 10:22:26 UTC | warn on `Invalid` SMT results | 10 June 2023, 22:35:56 UTC |
| eaba09c | Christian Doczkal | 24 February 2023, 16:42:30 UTC | [theories]: p_max (maximum probability for atomic events) Co-authored-by: Ethan Lee <ylee1228@umd.edu> | 05 June 2023, 14:39:42 UTC |
| 4650947 | Cameron Low | 19 May 2023, 10:58:37 UTC | Removed Smart constructors for types, expressions, formulae, paths, and statements. | 05 June 2023, 06:53:24 UTC |
| dc50f44 | Pierre-Yves Strub | 26 May 2023, 09:54:58 UTC | Forbid the usage of [declare] for concrete modules. Fix #328 | 26 May 2023, 12:06:42 UTC |
| 8f15fcb | Pierre-Yves Strub | 25 May 2023, 14:14:03 UTC | Fix datatype comparisons for theory replays We do not need to check the inductive schemas: - if the constructors are compatible, so are the schemas, - anyway, they are going to be checked right after, and - at that point, they are not convertible because they come from incomaptible enclosing theories. Fix #381 | 25 May 2023, 14:30:11 UTC |
| 926927a | Pierre-Yves Strub | 25 May 2023, 14:06:49 UTC | Accept non-printed variable only abbreviations. fix #382 | 25 May 2023, 14:23:31 UTC |
| 242e996 | Pierre-Yves Strub | 25 May 2023, 13:58:07 UTC | New command: proc op. This command generates an operator that computes the output distribution of a stateless proc. The command is in beta-mode. It misses: - a support for a larger set of instructions, - better error messages, - a registry of generated proc ops, and - a hoare/phoare statement that links the operator to the procedure. | 25 May 2023, 14:16:01 UTC |
| cf79f50 | Christian Doczkal | 26 April 2023, 13:15:46 UTC | [theories] FunRO: RO for FinType using dfun for init | 23 May 2023, 10:49:03 UTC |
| 860dc3f | Christian Doczkal | 16 May 2023, 10:13:08 UTC | use polymorpic wrapper to enable theory cloning | 17 May 2023, 04:25:30 UTC |
| d77676c | Christian Doczkal | 15 May 2023, 15:27:15 UTC | clean up SubType theory | 17 May 2023, 04:25:30 UTC |
| a672c38 | Dominique Unruh | 14 May 2023, 15:50:01 UTC | Updated examples to match new Subtype. | 17 May 2023, 04:25:30 UTC |
| 957afc7 | Dominique Unruh | 14 May 2023, 15:20:56 UTC | New Subtype theory. Updated stdlib to match. | 17 May 2023, 04:25:30 UTC |
| ee26cc5 | Alley Stoughton | 15 May 2023, 19:51:42 UTC | Commit b2106aa suppressed additional parentheses around match ... end in all circumstances, even though on the left and right of applications the parser requires parentheses, the theory being this makes it easier for humans to scan. So this commit inserts parentheses around matches in applications, but not elsewhere (e.g., not in infix operators). See below for examples. [The pretty printer needs a major redesign, so this is another stopgap measure.] require import AllCore List. type t = [ A of int | B of bool]. (* the following formulas now parse and pretty-print the same *) lemma foo1 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo2 : (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo3 (f : (int -> int) -> (int -> int)) : f (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo4 (f : int -> bool) : f (1 + match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo5 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort. lemma foo6 (f : int -> bool) : f (3 + match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort. | 16 May 2023, 07:04:10 UTC |
| 38e63de | Adrien Koutsos | 12 May 2023, 16:37:35 UTC | [cost v2] WIP, adding module wrappers in module paths | 12 May 2023, 16:37:35 UTC |
| 19b32c9 | Adrien Koutsos | 10 May 2023, 09:42:51 UTC | [cost v2] finished adding module path wrappers in EcPath Remains to add them in the rest of the code | 10 May 2023, 09:42:51 UTC |
| f7cba73 | Adrien Koutsos | 10 May 2023, 09:31:00 UTC | [cost v2] started to add wrappers in module paths | 10 May 2023, 09:31:00 UTC |
| d80bc3a | Adrien Koutsos | 04 May 2023, 14:33:20 UTC | commented debug printing which caused the test script to crash | 04 May 2023, 14:33:46 UTC |
| 94538c5 | François Dupressoir | 16 March 2023, 19:08:33 UTC | [ci] update actions to avoid node deprecation | 02 May 2023, 09:38:51 UTC |
| bde8af8 | Cameron Low | 28 March 2023, 16:09:16 UTC | Track the argument variables as well. Also update ROM proof. | 02 May 2023, 09:38:19 UTC |
| dc7ea88 | Adrien Koutsos | 28 April 2023, 16:43:56 UTC | [cost v2] changed internal representation of module path Preparing adding agent (for wrapped modules) in module paths | 28 April 2023, 16:43:56 UTC |
| d9e0b37 | Adrien Koutsos | 28 April 2023, 10:05:25 UTC | [cost v2] made type mpath private | 28 April 2023, 10:05:25 UTC |
| b90a0b8 | Adrien Koutsos | 28 April 2023, 09:38:12 UTC | [cost v2] replaced all access to field m_top by function calls | 28 April 2023, 09:38:12 UTC |
| 354ea9b | Adrien Koutsos | 27 April 2023, 13:10:28 UTC | [cost v2] minor | 27 April 2023, 13:10:28 UTC |
| 18dd603 | Adrien Koutsos | 26 April 2023, 13:02:53 UTC | [cost v2] wip | 26 April 2023, 13:02:53 UTC |
| a862304 | Adrien Koutsos | 26 April 2023, 12:18:53 UTC | [cost v2] wip | 26 April 2023, 12:18:53 UTC |
| 0163d0d | Adrien Koutsos | 26 April 2023, 09:26:40 UTC | [cost v2] printing agent names parameters in lemmas | 26 April 2023, 09:26:40 UTC |
| 4cded5c | Adrien Koutsos | 26 April 2023, 09:07:12 UTC | [cost v2] added missing agent files | 26 April 2023, 09:07:12 UTC |
| 2a1bbd4 | Adrien Koutsos | 26 April 2023, 09:06:41 UTC | [cost v2] fixed bug in proof-term construction (cut) | 26 April 2023, 09:06:41 UTC |
| 4788a8c | Adrien Koutsos | 25 April 2023, 15:30:14 UTC | [cost v2] constraint checker for agent name disjointness | 25 April 2023, 15:30:31 UTC |
| a82e428 | Adrien Koutsos | 25 April 2023, 12:58:57 UTC | [cost v2] agent names handled in a parametrized fashion (similarly to type parameters) | 25 April 2023, 12:58:57 UTC |
| 993c4e3 | Adrien Koutsos | 14 April 2023, 15:37:34 UTC | [cost v2] fixed printing bug | 14 April 2023, 15:37:34 UTC |
| 236a7c7 | Adrien Koutsos | 14 April 2023, 15:24:55 UTC | [cost v2] fixed substitution bug | 14 April 2023, 15:24:55 UTC |
| 3dc5e47 | Adrien Koutsos | 14 April 2023, 12:02:28 UTC | [cost v2] fixed error | 14 April 2023, 12:02:37 UTC |
| 0070bc6 | Adrien Koutsos | 14 April 2023, 09:14:09 UTC | [cost v2] conversion of agent binders | 14 April 2023, 09:18:28 UTC |
| 69fdb31 | Adrien Koutsos | 14 April 2023, 08:44:15 UTC | [cost v2] agents in proof-terms | 14 April 2023, 08:44:15 UTC |
| 5b443c0 | Adrien Koutsos | 13 April 2023, 16:22:54 UTC | Merge remote-tracking branch 'origin/main' into deploy-new-cost2 | 13 April 2023, 16:22:54 UTC |
| 34e68a8 | Adrien Koutsos | 13 April 2023, 16:20:35 UTC | Merge remote-tracking branch 'origin/main' into deploy-new-cost2 | 13 April 2023, 16:20:35 UTC |
| f7af981 | Adrien Koutsos | 13 April 2023, 16:20:10 UTC | [cost v2] wip | 13 April 2023, 16:20:10 UTC |
| 08d696b | Adrien Koutsos | 12 April 2023, 16:58:02 UTC | [cost v2] record module information in the environment | 12 April 2023, 16:58:02 UTC |
| 8fedd0c | Adrien Koutsos | 12 April 2023, 15:17:15 UTC | [cost v2] use agent names in cost records | 12 April 2023, 15:17:15 UTC |
| 863309b | Adrien Koutsos | 12 April 2023, 12:35:51 UTC | [cost v2] parser for external agents | 12 April 2023, 12:35:51 UTC |
| 1b95ad4 | Adrien Koutsos | 29 March 2023, 07:46:24 UTC | [cost v2] removed module opacity | 29 March 2023, 07:46:24 UTC |
| b0a1c6e | Adrien Koutsos | 29 March 2023, 07:20:22 UTC | [cost v2] wip | 29 March 2023, 07:33:17 UTC |
| f626259 | Cameron Low | 21 March 2023, 14:35:30 UTC | [tactic] Rewrite Equiv | 24 March 2023, 13:44:07 UTC |
| b2106aa | Alley Stoughton | 08 March 2023, 00:26:51 UTC | An attempt at fixing pretty printing bugs in which formulas that end with implications, conditionals or quantifiers and appear to the left of binary operators have their scopes extended to include those following binary operators. E.g., (3 :: 4 :: let x = 1 in [x]) = ys. incorrectly pretty prints as 3 :: 4 :: let x = 1 in [x] = ys | 21 March 2023, 10:59:33 UTC |
| ee4c20e | François Dupressoir | 16 March 2023, 20:56:12 UTC | [chore] update dependency versions in README | 20 March 2023, 16:28:35 UTC |
| ed96ecf | François Dupressoir | 16 March 2023, 16:21:06 UTC | fix a failing proof in MEE-CBC this aligns the top-level proof with earlier changes to a leaf theory | 20 March 2023, 16:28:35 UTC |
| ad96b3d | Pierre-Yves Strub | 16 March 2023, 15:39:37 UTC | simplify some smt calls | 20 March 2023, 16:28:35 UTC |
| 7a00b11 | François Dupressoir | 16 March 2023, 15:21:40 UTC | Remove raw smt in MEE-CBC | 20 March 2023, 16:28:35 UTC |
