| 5c9e395 | Gustavo Delerue | 08 March 2024, 19:29:32 UTC | Fixed bruteforce, added bitwuzla equivalence checking | 08 March 2024, 19:29:32 UTC |
| c86ac4e | Gustavo Delerue | 07 March 2024, 15:29:27 UTC | First polycompress circuit working | 07 March 2024, 15:29:27 UTC |
| 33cc560 | Gustavo Delerue | 06 March 2024, 18:09:34 UTC | Changed op | 06 March 2024, 18:09:34 UTC |
| 1d34cdd | Gustavo Delerue | 06 March 2024, 18:06:06 UTC | Polycompress circuit generation from op (lightly tested) | 06 March 2024, 18:06:06 UTC |
| 9a47583 | Gustavo Delerue | 06 March 2024, 12:10:18 UTC | First working example for circ from op for JWord.W16 | 06 March 2024, 12:10:18 UTC |
| 84717a8 | Gustavo Delerue | 04 March 2024, 15:02:43 UTC | Work plan 4/03 | 04 March 2024, 15:02:43 UTC |
| 7b4144b | Gustavo Delerue | 01 March 2024, 17:18:54 UTC | Bruteforce testing | 01 March 2024, 17:18:54 UTC |
| 84757c2 | Pierre-Yves Strub | 01 March 2024, 16:09:40 UTC | . | 01 March 2024, 16:09:40 UTC |
| f478ae8 | Gustavo Delerue | 01 March 2024, 10:33:08 UTC | Output | 01 March 2024, 10:33:08 UTC |
| 695565a | Gustavo Delerue | 27 February 2024, 19:30:28 UTC | Added automatic processing based on return variables | 27 February 2024, 19:30:28 UTC |
| 6851152 | Gustavo Delerue | 27 February 2024, 18:58:00 UTC | Added block equivalence checking | 27 February 2024, 18:58:00 UTC |
| 39ebe72 | Gustavo Delerue | 27 February 2024, 13:27:59 UTC | Env doesnt update from rhs, inputs are parsed from EC | 27 February 2024, 13:27:59 UTC |
| 549530a | Pierre-Yves Strub | 27 February 2024, 13:02:57 UTC | aig equiv | 27 February 2024, 13:02:57 UTC |
| 1706c3d | Pierre-Yves Strub | 27 February 2024, 12:51:36 UTC | refactoring | 27 February 2024, 12:51:36 UTC |
| 3f58808 | Gustavo Delerue | 15 February 2024, 22:11:41 UTC | Tentative step 2 | 15 February 2024, 22:11:41 UTC |
| e614964 | Gustavo Delerue | 15 February 2024, 18:57:16 UTC | Step one: Semi-tested version | 15 February 2024, 18:57:16 UTC |
| ca124ab | Gustavo Delerue | 14 February 2024, 19:14:54 UTC | Added dep printing for generated circuits | 14 February 2024, 19:14:54 UTC |
| 04c4183 | Gustavo Delerue | 12 February 2024, 18:22:52 UTC | Tentative 1st step | 12 February 2024, 18:22:52 UTC |
| 21a3941 | Pierre-Yves Strub | 12 February 2024, 17:48:51 UTC | . | 12 February 2024, 17:48:51 UTC |
| 62fa6c8 | Gustavo Delerue | 12 February 2024, 17:44:05 UTC | Added stuff to ecBDep | 12 February 2024, 17:44:05 UTC |
| 9888e59 | Pierre-Yves Strub | 12 February 2024, 14:43:45 UTC | . | 12 February 2024, 14:43:57 UTC |
| dbaddbd | Gustavo Delerue | 06 February 2024, 19:20:13 UTC | Fully tested evaluator | 06 February 2024, 19:20:13 UTC |
| b8bdd4e | Gustavo Delerue | 05 February 2024, 17:18:53 UTC | Finished testing basic ops | 05 February 2024, 17:18:53 UTC |
| ae3022c | Gustavo Delerue | 05 February 2024, 16:55:45 UTC | Fixed smul bugs | 05 February 2024, 16:55:45 UTC |
| d860ca3 | Gustavo Delerue | 05 February 2024, 16:32:40 UTC | Testing evaluator and fixing bugs | 05 February 2024, 16:32:40 UTC |
| 71dc6b9 | Gustavo Delerue | 02 February 2024, 18:44:26 UTC | Refactored ERepeat in bitdep | 02 February 2024, 18:44:26 UTC |
| 1ec4ad3 | Gustavo Delerue | 02 February 2024, 18:36:24 UTC | Fixed concat bug on eval | 02 February 2024, 18:36:24 UTC |
| ee14d4e | Gustavo Delerue | 02 February 2024, 17:06:33 UTC | Fixed evaluator bugs and added hardcoded evaluation to lospecs_test | 02 February 2024, 17:06:33 UTC |
| 07f1b27 | Gustavo Delerue | 01 February 2024, 16:25:53 UTC | Added first version of AST BW evaluator (untested) | 01 February 2024, 16:25:53 UTC |
| e0fdcfb | Gustavo Delerue | 31 January 2024, 16:42:40 UTC | Added temp function context to evaluator | 31 January 2024, 16:42:40 UTC |
| f3e09c0 | Gustavo Delerue | 29 January 2024, 21:18:35 UTC | evaluator first commit with Zarith | 29 January 2024, 21:18:35 UTC |
| 9003cc3 | Gustavo Delerue | 24 January 2024, 00:08:49 UTC | fixed more bugs | 24 January 2024, 00:08:49 UTC |
| 9446f1b | Gustavo Delerue | 23 January 2024, 23:14:39 UTC | Fixed bugs in dependency generator | 23 January 2024, 23:14:39 UTC |
| c6a59eb | Gustavo Delerue | 22 January 2024, 21:42:18 UTC | Changed deps datastructure, fixed bugs in dep generation, added circuit dep printing for spec/avx2 directly | 22 January 2024, 21:42:18 UTC |
| 25a11ce | Gustavo Delerue | 20 January 2024, 23:11:18 UTC | Bit dependency for new AST, untested | 20 January 2024, 23:11:18 UTC |
| aa212e0 | Gustavo Delerue | 17 January 2024, 15:18:45 UTC | Added functions to bitdep | 17 January 2024, 15:18:45 UTC |
| 525c5e0 | Pierre-Yves Strub | 12 January 2024, 15:41:53 UTC | Merge branch 'rewrite-in-stmt-assign-2' into bdep | 12 January 2024, 15:41:53 UTC |
| 670355c | Pierre-Yves Strub | 12 January 2024, 15:24:54 UTC | TEMP: idassign | 12 January 2024, 15:24:54 UTC |
| 1819d2f | Pierre-Yves Strub | 11 January 2024, 15:07:18 UTC | lospec: example | 11 January 2024, 15:07:23 UTC |
| bf0cb8f | Pierre-Yves Strub | 10 January 2024, 19:13:38 UTC | lospec: vpermq | 10 January 2024, 19:13:38 UTC |
| 25c36da | Pierre-Yves Strub | 10 January 2024, 17:27:51 UTC | lospec: all VP instructions of Kyber`s sampling | 10 January 2024, 17:27:51 UTC |
| 17912f1 | Pierre-Yves Strub | 10 January 2024, 10:34:58 UTC | drop AVX512 | 10 January 2024, 10:34:58 UTC |
| fc6bb8b | Pierre-Yves Strub | 10 January 2024, 09:32:08 UTC | typo | 10 January 2024, 09:32:08 UTC |
| 666e569 | Pierre-Yves Strub | 09 January 2024, 17:36:24 UTC | lospec: display source on error | 09 January 2024, 17:36:59 UTC |
| aeb16ee | Pierre-Yves Strub | 09 January 2024, 16:45:40 UTC | lospec: localized typing errors | 09 January 2024, 16:45:40 UTC |
| e0a819e | Pierre-Yves Strub | 09 January 2024, 15:19:14 UTC | lospec: positions in ptree | 09 January 2024, 15:19:14 UTC |
| 2afe1e6 | Pierre-Yves Strub | 09 January 2024, 14:39:46 UTC | lospec: factor out AST | 09 January 2024, 14:39:46 UTC |
| a1ea92a | Pierre-Yves Strub | 09 January 2024, 14:05:47 UTC | build | 09 January 2024, 14:05:47 UTC |
| 9109c98 | Pierre-Yves Strub | 09 January 2024, 13:48:39 UTC | lospec: CLI | 09 January 2024, 13:48:39 UTC |
| 801f5ee | Pierre-Yves Strub | 09 January 2024, 11:24:37 UTC | lospec: circuit generation | 09 January 2024, 11:24:37 UTC |
| 8bfc103 | Pierre-Yves Strub | 08 January 2024, 17:07:47 UTC | progress on circuit generation from specs | 08 January 2024, 17:07:47 UTC |
| 94808be | Pierre-Yves Strub | 08 January 2024, 16:36:21 UTC | circuits: code refactoring | 08 January 2024, 16:36:21 UTC |
| ba9f44f | Pierre-Yves Strub | 08 January 2024, 16:06:56 UTC | fix | 08 January 2024, 16:06:56 UTC |
| e720652 | Pierre-Yves Strub | 08 January 2024, 15:52:20 UTC | rework spec languages + AVX2 runtime | 08 January 2024, 16:04:02 UTC |
| bcc6bed | Gustavo Delerue | 23 December 2023, 19:32:18 UTC | Fixed shift semantics in bitdep | 23 December 2023, 19:32:18 UTC |
| e0f6e76 | Gustavo Delerue | 23 December 2023, 19:27:17 UTC | Fixed map bit dep offsets | 23 December 2023, 19:27:17 UTC |
| 9f71846 | Gustavo Delerue | 23 December 2023, 18:42:32 UTC | bitdep gen now works on examples/spec.txt | 23 December 2023, 18:42:32 UTC |
| 1fb4d8b | Gustavo Delerue | 20 December 2023, 00:34:19 UTC | WIP: Bitdep Gen from AST - Fixed slice and other things for bitdep | 20 December 2023, 00:34:19 UTC |
| 2da55f4 | Gustavo Delerue | 20 December 2023, 00:01:06 UTC | Added bitdep temp var propagation and map dependency generation | 20 December 2023, 00:01:06 UTC |
| d5a9816 | Gustavo Delerue | 19 December 2023, 15:05:06 UTC | WIP: Push commit for bitdependency generator from AST | 19 December 2023, 15:05:06 UTC |
| 7a1302c | Gustavo Delerue | 19 December 2023, 15:03:32 UTC | Fixed add dependency and added mult | 19 December 2023, 15:03:32 UTC |
| 19e0367 | Gustavo Delerue | 19 December 2023, 13:20:49 UTC | WIP: Bit dependency generator from AST | 19 December 2023, 13:20:49 UTC |
| 2c53d48 | Pierre-Yves Strub | 15 December 2023, 18:53:57 UTC | Merge remote-tracking branch 'origin/main' into bdep | 15 December 2023, 18:53:57 UTC |
| cd369bd | Pierre-Yves Strub | 15 December 2023, 18:27:32 UTC | remove bck | 15 December 2023, 18:27:39 UTC |
| d295a03 | Pierre-Yves Strub | 15 December 2023, 18:18:27 UTC | nix | 15 December 2023, 18:18:27 UTC |
| fa77ddf | Pierre-Yves Strub | 15 December 2023, 15:58:49 UTC | lospec: improve hash-consing | 15 December 2023, 15:58:49 UTC |
| 629278f | Pierre-Yves Strub | 15 December 2023, 15:02:58 UTC | lospec: remove warnings | 15 December 2023, 15:02:58 UTC |
| c5fddee | Pierre-Yves Strub | 15 December 2023, 15:01:59 UTC | lospec: compiles on all arch | 15 December 2023, 15:01:59 UTC |
| 75cf839 | Pierre-Yves Strub | 15 December 2023, 14:45:34 UTC | lospec: fuzzer | 15 December 2023, 14:45:34 UTC |
| 12af606 | Cameron Low | 15 December 2023, 10:45:02 UTC | New tactic: `outline` (#473) The main idea is to provide an inverse to inline when proving an equiv. Currently, it supports basic procedure unification that requires manual selection of the program slice to unify with, as well as, requiring near exact matches on program structure. An optional return value can be supplied for situations where the return expression is just a program variable and needs to be renamed/deconstructed. There is also support for statement outlining although, this is more of a transitivity * with program slicing so may require change. Syntax and variants: - Procedure outlining: outline {m} [s - e] lv? <@ M.foo - Statement outlining: outline {m} [s - e] { s1; s2; ... } with - m: 1 or 2 - s,e: code position - M.foo: path to procedure - lv: a left-value when `s = e`, one can use `[s]` instead of `[s-s]` For example usage see: tests/outline.ec | 15 December 2023, 10:45:02 UTC |
| d444d78 | Pierre-Yves Strub | 14 December 2023, 15:46:08 UTC | lospec: circuits | 14 December 2023, 15:46:18 UTC |
| 82f0cce | Gustavo Delerue | 13 December 2023, 21:13:22 UTC | Fixed issues with spec, added more mult variants and differentiated add w/wo carry | 13 December 2023, 21:13:22 UTC |
| 3c4d22f | Gustavo Delerue | 13 December 2023, 17:02:48 UTC | Updated docs | 13 December 2023, 17:02:48 UTC |
| 7782bc4 | Gustavo Delerue | 13 December 2023, 16:47:22 UTC | Typing AST *should* be done | 13 December 2023, 16:47:22 UTC |
| 4f5ed12 | Gustavo Delerue | 13 December 2023, 16:20:26 UTC | Type AST should be done | 13 December 2023, 16:20:26 UTC |
| 971b279 | Gustavo Delerue | 12 December 2023, 19:31:44 UTC | Change typing to return AST (In progress, map not done) | 12 December 2023, 19:31:44 UTC |
| 806998c | Pierre-Yves Strub | 12 December 2023, 17:36:45 UTC | lospec: ast | 12 December 2023, 17:38:11 UTC |
| 9b51d23 | Pierre-Yves Strub | 12 December 2023, 17:01:58 UTC | refactoring | 12 December 2023, 17:01:58 UTC |
| 1733c19 | Pierre-Yves Strub | 12 December 2023, 11:36:40 UTC | Docker: bump OCaml to 5.1.0 | 12 December 2023, 14:58:32 UTC |
| 943fc84 | François Dupressoir | 12 December 2023, 10:46:03 UTC | Bump provers to latest that succeeds, drop CVC4 Only Alt-Ergo needs kept back. | 12 December 2023, 13:46:57 UTC |
| 98139b7 | Pierre-Yves Strub | 12 December 2023, 10:54:24 UTC | nix-shell: remove why3 pin | 12 December 2023, 12:58:20 UTC |
| 736e322 | Francois Dupressoir | 12 December 2023, 12:18:17 UTC | remove a global axiom warning from the UC example (#502) | 12 December 2023, 12:18:17 UTC |
| 277cc28 | Pierre-Yves Strub | 12 December 2023, 11:32:56 UTC | lospec: formatting | 12 December 2023, 11:32:56 UTC |
| 9ef1dc2 | Pierre-Yves Strub | 12 December 2023, 11:32:28 UTC | lospec: kill warnings | 12 December 2023, 11:32:28 UTC |
| 7fb4bc8 | Pierre-Yves Strub | 12 December 2023, 11:31:54 UTC | lospec: failwith -> TypingError | 12 December 2023, 11:31:54 UTC |
| c31a5e4 | Pierre-Yves Strub | 12 December 2023, 11:10:39 UTC | lospec: automated formatting | 12 December 2023, 11:10:39 UTC |
| 308aab1 | Pierre-Yves Strub | 12 December 2023, 10:50:27 UTC | nix | 12 December 2023, 10:57:29 UTC |
| 1cfd9f2 | Pierre-Yves Strub | 12 December 2023, 10:46:55 UTC | Merge branch 'main' into bdep | 12 December 2023, 10:46:55 UTC |
| 708f9a1 | Pierre-Yves Strub | 12 December 2023, 10:45:02 UTC | lospec: move doc + Makefile | 12 December 2023, 10:45:02 UTC |
| be9fc09 | Gustavo Delerue | 11 December 2023, 22:16:39 UTC | Added spec language documentation | 11 December 2023, 22:16:39 UTC |
| 4c564f5 | Pierre-Yves Strub | 06 December 2023, 10:56:36 UTC | Internal API: process_Xhl_* This family of functions type-check a formula w.r.t. a memory that is infered from the program logic goal. The commit changes two things: - for prhl, its uses the same memory name as the one used in the program logic goal. (Previously, it was using `mhr`) - its returns the memory that has been used for the type-checking | 11 December 2023, 12:52:51 UTC |
| e508c48 | Pierre-Yves Strub | 08 December 2023, 07:20:01 UTC | New tactic: "proc rewrite" (DRAFT) This tactic allows to rewrite an expression in a statement. The syntax is: proc rewrite <side?> <codepos> <proof-term> This tactic does not aim to be in the TCB and its final version should rely on "proc change". Test plan: - unit test (tests/procrewrite.ec) | 11 December 2023, 11:03:48 UTC |
| e0d9613 | Pierre-Yves Strub | 11 December 2023, 10:58:49 UTC | New tactic: "proc change" This tactic allows to change an expression in a statement by some other expression. When applied, the user has to prove that the two expressions are equal (generalizing over all the program variables) This tactic applies to any program logic. The syntax is: proc change <side?> <codepos> : <form> This tactic is in the TCB. Test plan: - unit test (tests/prochange.ec) | 11 December 2023, 11:02:52 UTC |
| 38c8bce | Pierre-Yves Strub | 11 December 2023, 10:54:25 UTC | Internal: minor additions to EcLowPhlGoal & EcMatching modules - EcMatching.Zipper.map - EcLowPhlGoal.{is_program_logic,hl_set_stmt} | 11 December 2023, 11:01:24 UTC |
| bbca483 | Pierre-Yves Strub | 06 December 2023, 10:56:36 UTC | Internal API: process_Xhl_* This family of functions type-check a formula w.r.t. a memory that is infered from the program logic goal. The commit changes two things: - for prhl, its uses the same memory name as the one used in the program logic goal. (Previously, it was using `mhr`) - its returns the memory that has been used for the type-checking | 11 December 2023, 10:53:19 UTC |
| 4f02829 | Pierre-Yves Strub | 11 December 2023, 07:03:04 UTC | New command prefix: `fail` This prefix indicates that the following command should fail and that the error has to be ignored. It is an actual error if the command does not fail. In interactive mode, the error is printed (at [info] level). The main purpose of `fail` is to allow to write more precise unit tests where one can indicate which command shoud actually fail. | 11 December 2023, 10:07:50 UTC |
| 530a354 | Pierre-Yves Strub | 11 December 2023, 09:40:46 UTC | CI: do not skip successful duplicates If so, we can end with PR to protected branches that are blocked. | 11 December 2023, 09:50:22 UTC |
| bbe5e6d | Pierre-Yves Strub | 11 December 2023, 06:12:54 UTC | CI: unit tests In the automated tests, add a section `unit`for unit tests. The unit tests are checked by the CI. They can be run using `make unit`. | 11 December 2023, 09:11:50 UTC |
| 9c1ec6b | Pierre-Yves Strub | 07 December 2023, 13:30:49 UTC | CI: skip duplicated jobs | 07 December 2023, 15:57:05 UTC |
| 1d3dcaa | Benjamin Gregoire | 07 December 2023, 15:38:16 UTC | extend weakmem to hoare/choare/ehoare/equiv | 07 December 2023, 15:56:27 UTC |
