| 6410e49 | Raphaël Cauderlier | 06 May 2020, 11:24:39 UTC | WIP: self and param | 18 June 2020, 14:01:55 UTC |
| a3dc02e | Raphaël Cauderlier | 22 April 2020, 14:00:45 UTC | Support for some of the optional fields of TZT The following fields are now supported: - amount - balance - chain_id - now - sender - source | 18 June 2020, 14:01:08 UTC |
| 77f9135 | Raphaël Cauderlier | 22 April 2020, 13:59:16 UTC | General-purpose error named Debug | 08 June 2020, 14:01:01 UTC |
| d05ad76 | Raphaël Cauderlier | 22 April 2020, 12:07:41 UTC | Complete the decidability proof for instructions, data, and stacks | 08 June 2020, 14:00:27 UTC |
| 3552535 | Raphaël Cauderlier | 19 April 2020, 12:47:27 UTC | [Michocoq|TZT] Fix parsing of lambdas in stacks | 08 June 2020, 12:49:55 UTC |
| cf50b15 | Raphaël Cauderlier | 18 April 2020, 11:29:31 UTC | Improve error message for failed unit tests | 08 June 2020, 12:49:55 UTC |
| b1a8aca | Raphaël Cauderlier | 18 April 2020, 11:28:24 UTC | Add "KO" in expected error messages | 08 June 2020, 12:49:55 UTC |
| 1deb5cd | Raphaël Cauderlier | 18 April 2020, 11:27:44 UTC | Fix traces for fixed typing bugs | 08 June 2020, 12:49:55 UTC |
| bb87657 | Raphaël Cauderlier | 16 April 2020, 19:25:07 UTC | Prefix all error messages by KO to ease counting | 08 June 2020, 12:49:54 UTC |
| 75d0a35 | Raphaël Cauderlier | 16 April 2020, 09:43:12 UTC | Monadic notation for the option monad | 08 June 2020, 12:49:54 UTC |
| f8a0c31 | Raphaël Cauderlier | 16 April 2020, 09:42:33 UTC | Partial pretty-printing of stacks in unit test error messages | 08 June 2020, 12:49:54 UTC |
| a8a2d23 | Raphaël Cauderlier | 15 April 2020, 20:01:30 UTC | Improve name of the conversion function from concrete data to Micheline | 08 June 2020, 12:49:54 UTC |
| 30f80c0 | Raphaël Cauderlier | 15 April 2020, 19:44:30 UTC | Fixup more informational message | 08 June 2020, 12:49:54 UTC |
| 1cd48a2 | Raphaël Cauderlier | 14 April 2020, 20:26:58 UTC | More imformational error message at expansion | 08 June 2020, 12:49:52 UTC |
| 33aaa9a | Raphaël Cauderlier | 14 April 2020, 14:43:52 UTC | [michocoq] TZT format support This adds a `michocoq-tzt.native` binary that can be used to run unit tests. The format is very partially supported and comparison of stacks containing lambdas is buggy. | 08 June 2020, 12:48:53 UTC |
| b191aa2 | Raphaël Cauderlier | 14 April 2020, 14:38:09 UTC | [michocoq]] Add a file about decidable types A type is said to be decidable if equality on this type is a decidable relation. The type A is decidable if we have forall x y : A, {x = y} + {x <> y}. Decidability is an important notion for unit tests of the eval function because we need to compare stacks. | 08 June 2020, 12:46:25 UTC |
| d450095 | Raphaël Cauderlier | 22 April 2020, 14:00:01 UTC | Fix typing of chain_id constants (bytes instead of strings) | 04 June 2020, 20:19:08 UTC |
| cbd29fd | Raphaël Cauderlier | 16 April 2020, 09:43:55 UTC | Bytes | 04 June 2020, 20:15:38 UTC |
| c4eb2d6 | Raphaël Cauderlier | 17 April 2020, 21:22:21 UTC | Override extraction of ediv | 04 June 2020, 20:10:37 UTC |
| c375c1f | Raphaël Cauderlier | 16 April 2020, 09:43:32 UTC | Export of Zarith div and modulo; seems to have no effect for now | 04 June 2020, 20:02:55 UTC |
| f9e5a88 | Raphaël Cauderlier | 15 April 2020, 13:43:50 UTC | Fix the semantics of EDIV | 04 June 2020, 20:02:55 UTC |
| 6cdd5d6 | Raphaël Cauderlier | 15 April 2020, 14:01:33 UTC | Big map litterals | 04 June 2020, 20:02:23 UTC |
| c8200ce | Raphaël Cauderlier | 14 April 2020, 20:29:53 UTC | Add missing case for the `chain_id` type in the Micheline2michelson parser | 04 June 2020, 19:55:21 UTC |
| d6a0cf0 | Raphaël Cauderlier | 14 April 2020, 20:13:21 UTC | [Michocoq] Add the missing case ADD :: int : nat : 'S -> nat : 'S | 04 June 2020, 19:54:39 UTC |
| 0512b49 | Raphaël Cauderlier | 08 April 2020, 10:10:55 UTC | [michocoq] Formalize the relation between key_hash, addresses and contracts | 04 June 2020, 19:45:55 UTC |
| f797bb5 | Raphaël Cauderlier | 08 April 2020, 10:02:49 UTC | [michocoq] remove an unused file | 04 June 2020, 14:02:32 UTC |
| 2e8d5a3 | Raphaël Cauderlier | 16 December 2019, 08:18:47 UTC | [optimizer] Define and certify a Michelson optimizer The optimizer was initially designed for the backend of the Albert compiler, it has been slightly generalized and certified. The main theorem is the last one in file typed_optimizer.v: If the untyped instruction sequence i can be typechecked from stack type A to stack type B and then run successfully on stack sA, then (optimizer.optimize i) can also be typechecked from stack type A to stack type B and run successfully on stack sA yielding the same result. | 19 May 2020, 13:55:03 UTC |
| 11de7d7 | Raphaël Cauderlier | 10 May 2020, 14:48:32 UTC | Untyped macros in `instruction` | 19 May 2020, 13:55:02 UTC |
| 2415691 | Raphaël Cauderlier | 26 April 2020, 20:07:01 UTC | [michocoq] Simplification of tez.v This uses `Bool.Is_true (negb ...)` instead of `... = false` in the definition of the `mutez` type which simplifies a bit reasoning about the implementation of mutez. | 14 May 2020, 19:39:36 UTC |
| 93912f6 | Raphaël Cauderlier | 21 December 2019, 22:12:06 UTC | [michocoq] Prove second half of typer correctness This completes the correctness proof of the typer in Optimized mode. Before this, only the typed -> untyped -> typed round-trip was certified. | 14 May 2020, 19:39:36 UTC |
| daec052 | Raphaël Cauderlier | 25 April 2020, 13:33:49 UTC | [michocoq] Typing and untyping mode (Readable or Optimized) Since the introduction of timestamp literals, the typer is not injective anymore so the converse of untyper.untype_type is not true. By introducing a typing and an untyping mode, we get back injectivity at least in optimized mode. | 14 May 2020, 19:39:36 UTC |
| 8591d76 | Raphaël Cauderlier | 21 December 2019, 21:53:16 UTC | [michocoq] Fix a bug in the typer Type-checking a mutez literal now fails in case of overflow. | 14 May 2020, 19:39:36 UTC |
| ac659ab | Raphaël Cauderlier | 07 May 2020, 19:22:44 UTC | [build|ignore] Also ignore the cache of the `nia` tactic | 14 May 2020, 19:39:35 UTC |
| 34a1022 | Raphaël Cauderlier | 05 December 2019, 11:08:19 UTC | [michocoq] Use frienly notations in all verified scripts | 14 May 2020, 19:37:32 UTC |
| 5bd8859 | Raphaël Cauderlier | 03 December 2019, 12:19:06 UTC | [michocoq] Add a distinction between instructions and instruction sequences | 14 May 2020, 19:37:32 UTC |
| 980a820 | Raphaël Cauderlier | 29 November 2019, 14:27:04 UTC | [michocoq] Also separate IF_ and LOOP_ instructions from the other ones | 07 May 2020, 21:55:22 UTC |
| 95b18b8 | Raphaël Cauderlier | 17 March 2020, 17:40:39 UTC | [michocoq] Stratify opcodes and instructions. We call opcodes the instructions that do not take subprograms as argument nor have special treatment in the type-checker or evaluator. Most of the instructions in Michelson fall into this category, putting them aside makes the number of constructors of the instruction ASTs much smaller which is needed when reasoning on the syntax. In particular, many optimisations at the Michelson level require to reason about several terms in these ASTs by nesting destructs which was not tractable with more than 80 constructors. | 07 May 2020, 21:55:12 UTC |
| ab60300 | Raphaël Cauderlier | 07 May 2020, 21:15:25 UTC | Remove syntax_equiv.v This is incomplete and broken. | 07 May 2020, 21:54:55 UTC |
| ba48cdf | Raphaël Cauderlier | 24 January 2020, 10:26:23 UTC | Remove the return_to_sender contract This is a duplicate of the boomerang contract. | 07 May 2020, 21:54:42 UTC |
| 30ec384 | Guillaume Claret | 10 March 2020, 21:16:49 UTC | [Michocoq] Add parsing of timestamps | 18 April 2020, 12:34:45 UTC |
| 75ba1ed | Raphaël Cauderlier | 13 March 2020, 16:48:52 UTC | [CI|Tests] Run the tests in the CI | 18 April 2020, 12:34:45 UTC |
| b6d740a | Raphaël Cauderlier | 13 March 2020, 16:46:47 UTC | [Build|Tests]: add a build-test target for Opam | 18 April 2020, 12:34:45 UTC |
| 2eeac09 | Raphaël Cauderlier | 13 March 2020, 16:35:42 UTC | [Tests] Regression traces | 18 April 2020, 12:34:44 UTC |
| 123c097 | Raphaël Cauderlier | 13 March 2020, 16:48:13 UTC | [Tests] Regression testing Tests are run with `make test` and regression traces are reset with `make RESET_REGRESSION=true test`. | 18 April 2020, 12:34:44 UTC |
| 3ae9aaf | Raphaël Cauderlier | 13 March 2020, 15:54:06 UTC | [Tests] Update the test suite | 18 April 2020, 12:34:44 UTC |
| 1c4fb62 | Raphaël Cauderlier | 16 July 2019, 08:57:17 UTC | [Michocoq] Formalize %-annotations and entrypoints Annotations are still ignored at lexing time but the semantically meaningful ones are supported in the untyped syntax. | 18 April 2020, 12:34:44 UTC |
| c578eba | Guillaume Claret | 27 February 2020, 17:45:18 UTC | [build] Add support for Coq 8.11 | 18 April 2020, 12:03:13 UTC |
| 94071da | Guillaume Claret | 06 December 2019, 18:59:32 UTC | [of_ocaml] Add a README for the of_ocaml folder | 18 April 2020, 12:03:13 UTC |
| a35ea8c | Guillaume Claret | 06 December 2019, 18:04:18 UTC | [of_ocaml] Beginning of injection of the syntax of Mi-Cho-Coq to OCaml | 18 April 2020, 12:03:13 UTC |
| 41fed52 | Guillaume Claret | 03 December 2019, 15:35:40 UTC | [of_ocaml] Bijection for the comparable types | 18 April 2020, 12:03:13 UTC |
| e94f138 | Guillaume Claret | 02 December 2019, 14:54:09 UTC | [of_ocaml] Explicit definition of coq_to_ocaml_typ | 18 April 2020, 12:03:13 UTC |
| bbb0057 | Guillaume Claret | 16 November 2019, 16:28:49 UTC | [of_ocaml] Extend one side on the equivalence of the types with comparable types | 18 April 2020, 12:03:13 UTC |
| e432e03 | Guillaume Claret | 16 November 2019, 13:29:15 UTC | [of_ocaml] Add one side of the equivalence with the Coq AST | 18 April 2020, 12:03:12 UTC |
| 80978ee | Guillaume Claret | 16 November 2019, 13:28:16 UTC | [of_ocaml] Add imported syntax definition from the OCaml code | 18 April 2020, 12:03:12 UTC |
| fdfa10d | Raphaël Cauderlier | 04 December 2019, 20:50:34 UTC | [Michocoq] Remove superfluous functors | 18 April 2020, 12:03:12 UTC |
| ae11043 | Raphaël Cauderlier | 04 December 2019, 14:19:10 UTC | [Michocoq] Remove contract literals | 18 April 2020, 11:49:22 UTC |
| 5b40d03 | Raphaël Cauderlier | 18 April 2020, 11:40:18 UTC | [CI] fix shellcheck URL | 18 April 2020, 11:43:19 UTC |
| 3fb4ceb | Arvid Jakobsson | 10 March 2020, 14:23:46 UTC | [generic_multisig] Add CHAIN_ID to signature Related to #21 | 11 March 2020, 13:52:45 UTC |
| 00e403d | Raphaël Cauderlier | 13 February 2020, 17:07:39 UTC | [SC verif] Deposit contract | 13 February 2020, 17:07:39 UTC |
| 90abcb0 | Raphaël Cauderlier | 23 January 2020, 22:29:22 UTC | [build] Add missing dependency to ocamlbuild | 13 February 2020, 10:07:44 UTC |
| 9b308f4 | Raphaël Cauderlier | 12 February 2020, 13:15:58 UTC | [doc] slides for WTSC | 12 February 2020, 13:23:16 UTC |
| 949a7a4 | Raphaël Cauderlier | 12 February 2020, 13:15:36 UTC | [doc] slides of past talks | 12 February 2020, 13:23:16 UTC |
| a0ebbfd | Raphaël Cauderlier | 27 January 2020, 09:47:43 UTC | [doc] More explicit names for the talk directories | 27 January 2020, 09:48:13 UTC |
| f65e22e | Raphaël Cauderlier | 13 January 2020, 12:33:51 UTC | [doc] slides for the workshop at Cobra in Aarhus | 13 January 2020, 12:34:38 UTC |
| dc275c8 | Guillaume Claret | 04 December 2019, 09:27:10 UTC | Fix the install of the michocoq binary | 04 December 2019, 09:39:27 UTC |
| 9aa10a2 | Arvid Jakobsson | 29 November 2019, 14:39:11 UTC | [ott] remove the original michocott formalization | 29 November 2019, 14:39:11 UTC |
| ceb487e | Raphaël Cauderlier | 11 September 2019, 07:54:20 UTC | Michocott: Update michelson.ott to ease documentation generation | 29 November 2019, 13:41:28 UTC |
| 8733671 | Basile Pesin | 31 May 2019, 13:43:15 UTC | Corrected the 'a's that were changed in 'ty2's | 29 November 2019, 13:41:24 UTC |
| 3098cf5 | Basile Pesin | 30 May 2019, 17:27:17 UTC | All the way to extraction | 29 November 2019, 13:41:11 UTC |
| f2939c1 | Basile Pesin | 30 May 2019, 16:01:51 UTC | Removed ambiguity by adding explicit annotations | 29 November 2019, 13:40:31 UTC |
| eb1c38f | Basile Pesin | 29 May 2019, 23:02:55 UTC | Every rule is good with doc but multiple parses on compilation to coq for list set map | 29 November 2019, 13:40:31 UTC |
| 609a9c5 | Basile Pesin | 29 May 2019, 19:06:58 UTC | ott spec OK except for list and map | 29 November 2019, 13:40:31 UTC |
| 218ee17 | Basile Pesin | 29 May 2019, 13:09:06 UTC | Changed symbol for typing to '::' and symbol for cons to ':' in michelson_typing | 29 November 2019, 13:40:31 UTC |
| a7ba07f | Raphaël Cauderlier | 29 May 2019, 09:23:37 UTC | [Michocott] Formalize the typing rules of Michelson in OTT TOFIX: Currently the syntax of Michelson is not shared with michelson.ott. Moreover I used `:` for the typing relation and `::` for stack consing whereas the documentation (and michelson.ott) use `:` for consing and `::` for typing. | 29 November 2019, 13:40:31 UTC |
| cdc97c1 | Raphaël Cauderlier | 28 November 2019, 15:06:48 UTC | [CI] Add Coq v8.10 | 28 November 2019, 15:06:48 UTC |
| ac14acd | Raphaël Cauderlier | 28 November 2019, 10:00:56 UTC | Add the IF_RIGHT macro at the typed syntax level | 28 November 2019, 10:00:56 UTC |
| e729117 | Raphaël Cauderlier | 26 November 2019, 21:09:02 UTC | Remove IF_RIGHT The `IF_RIGHT` macro was incorrectly documented as an instruction when the Mi-Cho-Coq effort started. The macro expanser correctly converted ot to its expanded form so all handling of `IF_RIGHT` as an instruction was basically dead code. | 26 November 2019, 21:09:02 UTC |
| a7655d8 | Raphaël Cauderlier | 23 November 2019, 08:33:21 UTC | Formatting | 25 November 2019, 10:24:17 UTC |
| 48f957f | Raphaël Cauderlier | 20 November 2019, 08:13:43 UTC | Printer: simplify Michelson -> Micheline and the Micheline printer | 25 November 2019, 10:23:25 UTC |
| 474723b | Raphaël Cauderlier | 14 November 2019, 17:33:09 UTC | Make the type argument of error.Return implicit | 14 November 2019, 17:33:09 UTC |
| 3bebfc4 | Raphaël Cauderlier | 14 November 2019, 17:13:23 UTC | Swap arguments of bind | 14 November 2019, 17:19:07 UTC |
| 085c7d7 | Guillaume Claret | 23 October 2019, 14:48:57 UTC | Remove all remaining binds without let! notation | 14 November 2019, 17:19:07 UTC |
| f7efb6f | Guillaume Claret | 23 October 2019, 13:43:29 UTC | Use the let! notation | 14 November 2019, 17:11:20 UTC |
| a0ad40f | Guillaume Claret | 23 October 2019, 13:48:45 UTC | Add a module to namespace the let! notation | 14 November 2019, 17:10:51 UTC |
| 3993c1c | Guillaume Claret | 23 October 2019, 12:45:53 UTC | Add a let! notation for the bind | 06 November 2019, 15:48:00 UTC |
| d18aeba | Guillaume Claret | 23 October 2019, 12:44:24 UTC | Remove unused Eval | 06 November 2019, 15:48:00 UTC |
| d45b391 | Guillaume Claret | 23 October 2019, 12:37:56 UTC | Ignore .lia.cache files | 06 November 2019, 15:48:00 UTC |
| edb58ee | Arvid Jakobsson | 06 November 2019, 15:08:13 UTC | Update coq-mi-cho-coq.opam: remove duplicate synpopsis | 06 November 2019, 15:08:13 UTC |
| ec3f4a8 | Guillaume Claret | 23 October 2019, 15:13:34 UTC | Backport upstream changes to the opam package | 01 November 2019, 16:31:58 UTC |
| ab8c856 | Arvid Jakobsson | 23 October 2019, 08:52:16 UTC | Make sure that make clean removes files generated by extraction | 23 October 2019, 08:52:16 UTC |
| 61e2773 | Raphaël Cauderlier | 18 October 2019, 14:00:51 UTC | PAPAIR and UNPAPAIR macros | 22 October 2019, 14:18:33 UTC |
| 1b89f58 | Raphaël Cauderlier | 10 October 2019, 11:14:44 UTC | Fix expansion of the DUUUP macro | 22 October 2019, 14:18:33 UTC |
| 3b920a5 | Raphaël Cauderlier | 10 October 2019, 11:04:30 UTC | Expansion of CADR, SET_CADR, and MAP_CADR macros | 22 October 2019, 14:18:33 UTC |
| e81432c | Raphaël Cauderlier | 09 October 2019, 16:13:37 UTC | Simplify the WP calculus | 22 October 2019, 14:18:33 UTC |
| cadc05e | Raphaël Cauderlier | 10 October 2019, 10:26:52 UTC | The regular simpl tactic can now be used instead of our custom simplify_intruction | 22 October 2019, 14:18:33 UTC |
| 064f96c | Raphaël Cauderlier | 08 October 2019, 23:21:24 UTC | Simplify a bit the code of the evaluator | 22 October 2019, 14:18:33 UTC |
| f6bfa3b | Raphaël Cauderlier | 07 October 2019, 20:30:11 UTC | Install the extracted binary | 22 October 2019, 14:18:33 UTC |
| d7b66ee | Raphaël Cauderlier | 07 October 2019, 00:17:39 UTC | [Extraction] Extract the type-checker and fix many bugs | 22 October 2019, 14:18:32 UTC |
| b42ae25 | Raphaël Cauderlier | 28 June 2019, 13:31:40 UTC | Fix a typing bug occurring when SELF was used in a Michelson origination When type-checking the code literal of a smart contract originated from Michelson, we have to be cautious to use the self type of the contract being originated instead of the contract doing the origination. For this reason, we cannot have `self_type` as a parameter of the inductive type for instructions but it needs to be an index. However, SELF is forbidden inside lambdas in Michelson so we do not have to care about typing the SELF instruction in lambdas. | 22 October 2019, 14:18:32 UTC |
| 4b53f52 | Raphaël Cauderlier | 02 October 2019, 07:04:52 UTC | [/!\ Interface breaking change] Almost complete the implementation of the lexer, parser, and typer Some macros are still missing. Extracting a standalone tool would help writing more tests. | 22 October 2019, 14:18:32 UTC |
