| 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 |
| 3bfd628 | Basile Pesin | 26 July 2019, 09:49:19 UTC | Added INT and IS_NAT | 22 October 2019, 14:18:32 UTC |
| 0233856 | Basile Pesin | 25 July 2019, 16:18:34 UTC | Dig and Dug type-checking | 22 October 2019, 14:18:32 UTC |
| a87cc8f | Basile Pesin | 22 July 2019, 09:12:03 UTC | Added a specific case for PUSH _ Concrete_seq, to avoid bad line feeds | 22 October 2019, 14:18:32 UTC |
| f421eb8 | Basile Pesin | 19 July 2019, 09:02:03 UTC | Fixed pretty printer | 22 October 2019, 14:18:32 UTC |
| 4b33d51 | Basile Pesin | 18 July 2019, 13:47:51 UTC | Flattening sequences and slightly improved the pretty-printer | 22 October 2019, 14:18:31 UTC |
| a98c884 | Basile Pesin | 18 July 2019, 11:16:42 UTC | Added micheline2michelson converter | 22 October 2019, 14:18:31 UTC |
| f4cdd12 | Basile Pesin | 15 July 2019, 16:32:37 UTC | Updated menhir to 20190626 | 22 October 2019, 14:18:31 UTC |
| 88dd857 | Basile Pesin | 15 July 2019, 15:06:21 UTC | UNPAIR macro and extracting untyped_syntax and typer | 22 October 2019, 14:18:31 UTC |
| 7f1a76f | Basile Pesin | 12 July 2019, 17:01:33 UTC | Refactor sections into modules after rebase, missing DIG and DUG typers | 22 October 2019, 14:18:31 UTC |
| aec321b | Basile Pesin | 07 June 2019, 14:56:26 UTC | Added a lemma on string lexing | 22 October 2019, 14:18:31 UTC |
| 124eb4c | Basile Pesin | 06 June 2019, 20:06:32 UTC | Added pretty-printer function for micheline | 22 October 2019, 14:18:31 UTC |
| 248bad4 | Basile Pesin | 06 June 2019, 09:44:25 UTC | Fixed eqb for coq 8.8.2 | 22 October 2019, 14:18:31 UTC |
| bb2ba61 | Raphael Cauderlier | 25 March 2019, 22:21:14 UTC | [typer] Certified Michelson type-checker/type-inferrer We essentially proved forall i, typer.type_instruction (untyper.untype_instruction i) A = Return _ i but this result can only be true if instructions like {FAIL; FAIL} are forbidden in the typed world (the type inferrer cannot guess the type of the stack between the two FAILs). For this reason, we introduced a new boolean flag in the syntax.instruction inductive that is true iff the instruction is a sequence whose last element is FAIL. | 22 October 2019, 14:18:31 UTC |
| d266382 | Raphael Cauderlier | 22 March 2019, 10:01:18 UTC | [Michocott] Untrack and ignore the .v file generated by OTT | 22 October 2019, 14:18:30 UTC |
| ed6bdd9 | Raphael Cauderlier | 20 March 2019, 14:42:05 UTC | [Micheline] Micheline parser | 22 October 2019, 14:18:30 UTC |
| 1cfd656 | Raphael Cauderlier | 18 March 2019, 09:12:44 UTC | [Micheline] Micheline lexer | 22 October 2019, 14:18:30 UTC |
| 2a4adc7 | Raphaël Cauderlier | 27 September 2019, 15:33:01 UTC | Comparable pairs | 22 October 2019, 14:18:30 UTC |
| baa0a09 | Raphaël Cauderlier | 27 September 2019, 10:14:07 UTC | Remove deprecated instructions | 22 October 2019, 14:18:30 UTC |
| be95036 | Raphaël Cauderlier | 27 September 2019, 10:06:52 UTC | Update the multisig contract and its proof to use CHAIN_ID | 22 October 2019, 14:18:30 UTC |
| fc16081 | Raphaël Cauderlier | 27 September 2019, 10:05:21 UTC | CHAIN_ID | 22 October 2019, 14:18:30 UTC |
| bd3e077 | Raphaël Cauderlier | 27 September 2019, 09:44:33 UTC | DROP n | 22 October 2019, 14:18:30 UTC |
| 3c9bf7b | Raphaël Cauderlier | 27 September 2019, 09:36:08 UTC | DIP n | 22 October 2019, 14:18:29 UTC |
| 98871cc | Raphaël Cauderlier | 27 September 2019, 08:40:05 UTC | APPLY | 22 October 2019, 14:18:29 UTC |
| a5e296c | Raphaël Cauderlier | 27 September 2019, 08:39:25 UTC | Packable types, for which data_to_concrete_data is defined | 22 October 2019, 14:18:29 UTC |
| 069c46d | Basile Pesin | 02 July 2019, 15:36:27 UTC | DIG and DUG Add the (future) DIG and DUG instructions to Mi-Cho-Coq. See tezos/tezos!1031 for reference. | 22 October 2019, 14:18:29 UTC |
| a4d6612 | Raphaël Cauderlier | 15 October 2019, 20:43:52 UTC | Doc: Fix a talk subtitle (PDF version) | 15 October 2019, 20:43:52 UTC |
| f1fbadf | Raphaël Cauderlier | 14 October 2019, 12:32:22 UTC | [Doc] Add slides for the Ledger - Tezos Meetup | 14 October 2019, 12:32:22 UTC |
| 46ffce5 | Raphaël Cauderlier | 10 October 2019, 13:50:55 UTC | Doc: FMBC slides | 10 October 2019, 13:50:55 UTC |
| 7b0cc2b | b | 09 October 2019, 17:25:42 UTC | Doc: add coq workshop | 09 October 2019, 17:25:42 UTC |
| e538b10 | Guillaume Claret | 20 September 2019, 09:06:06 UTC | Use the stable version of coq-ott | 20 September 2019, 09:06:17 UTC |
| db5f2d4 | Guillaume Claret | 20 September 2019, 09:05:12 UTC | Prepare the opam package for a public release | 20 September 2019, 09:05:12 UTC |
| 90bcdb9 | Basile Pesin | 26 July 2019, 09:49:19 UTC | Added IS_NAT and INT instruction | 26 July 2019, 13:28:37 UTC |
| 59f35ec | Basile Pesin | 26 July 2019, 09:48:59 UTC | Corrected an error in manager.v after refactor | 26 July 2019, 09:48:59 UTC |
| de76b7d | Raphaël Cauderlier | 15 July 2019, 18:04:30 UTC | Manager: Update proof | 25 July 2019, 16:47:52 UTC |
| 8e3a0e6 | b | 11 July 2019, 11:01:29 UTC | Manager: also remove the set_manager entrypoint in the Coq proof | 25 July 2019, 16:47:33 UTC |
| 0818b71 | Tomáš Zemanovič | 15 July 2019, 07:38:26 UTC | Manager: use 'assert' instead of 'failwith', only accept tokens on 'default' entry | 25 July 2019, 16:47:11 UTC |
| 6241f44 | Tomáš Zemanovič | 11 July 2019, 10:26:09 UTC | Manager: add entrypoint annotations in script | 25 July 2019, 16:47:00 UTC |
| 1291249 | Tomáš Zemanovič | 11 July 2019, 10:25:31 UTC | Manager: remove set_manager entrypoint in script | 25 July 2019, 16:46:47 UTC |
| 68ad926 | Raphaël Cauderlier | 10 July 2019, 21:58:44 UTC | Manager: Update script and proof to use the %do entrypoint | 25 July 2019, 16:46:37 UTC |
| 820abb7 | Raphaël Cauderlier | 16 July 2019, 11:33:57 UTC | Revert "DIG and DUG" This reverts commit 4b0092d5076627335861f888855bfd8d8fe7b37e. | 16 July 2019, 11:33:57 UTC |
| c45ad1c | b | 12 July 2019, 10:05:17 UTC | Mi-Cho-Coq: fix typo | 12 July 2019, 10:05:17 UTC |
| 33f5d2a | b | 12 July 2019, 10:04:31 UTC | Mi-Cho-Coq: inline instr definition | 12 July 2019, 10:04:31 UTC |
| 3e34215 | Raphaël Cauderlier | 08 July 2019, 16:55:10 UTC | Re-impose matching self-type with the contract parameter type. | 08 July 2019, 16:55:10 UTC |
| 2c21e57 | Basile Pesin | 05 July 2019, 16:00:18 UTC | Corrected the extraction problem | 05 July 2019, 16:00:18 UTC |
| 32711ba | Basile Pesin | 05 July 2019, 15:17:57 UTC | Passing Env to functors from toplevel. Still an issue with extraction | 05 July 2019, 15:17:57 UTC |
| aac403e | Basile Pesin | 05 July 2019, 13:00:11 UTC | Corrected the proved contracts to reflect changes | 05 July 2019, 13:00:11 UTC |
| ebf535a | Basile Pesin | 05 July 2019, 12:26:21 UTC | Refactor sections into functors | 05 July 2019, 12:28:14 UTC |
| 2b4e968 | Tom Jack | 20 June 2019, 16:39:23 UTC | Install Coq libraries | 03 July 2019, 17:02:01 UTC |
| 66fe957 | Raphaël Cauderlier | 01 July 2019, 12:42:49 UTC | Apply suggestion to src/contracts_coq/generic_multisig.v | 02 July 2019, 16:33:26 UTC |
| ea614ac | Raphaël Cauderlier | 01 July 2019, 12:41:54 UTC | Apply suggestion to src/michocoq/util.v | 02 July 2019, 16:33:26 UTC |
| 8b65f33 | Raphaël Cauderlier | 26 June 2019, 11:30:15 UTC | Prove a new version of the multisig contract With this new generic version of the multisig contract, the signers can sign several operations at once (to be run atomically) and send parameters to other smart contracts. | 02 July 2019, 16:33:26 UTC |
| 26a10ea | Raphaël Cauderlier | 23 June 2019, 20:09:26 UTC | New macros: PAPAIR and UNPAPAIR | 02 July 2019, 16:33:26 UTC |
| c564b07 | Raphaël Cauderlier | 23 June 2019, 20:08:41 UTC | Move general lemmas out of the multisig.v file. | 02 July 2019, 16:33:26 UTC |
| 4b0092d | Basile Pesin | 02 July 2019, 15:36:27 UTC | DIG and DUG Add the (future) DIG and DUG instructions to Mi-Cho-Coq. See tezos/tezos!1031 for reference. | 02 July 2019, 15:36:27 UTC |
| 481dcf4 | b | 28 June 2019, 07:23:22 UTC | [Mi-Cho-Coq|Multisig]: light cleaning | 30 June 2019, 12:28:26 UTC |
| 9b8fb39 | Raphaël Cauderlier | 28 June 2019, 12:54:58 UTC | [doc] Fix talk subtitle | 28 June 2019, 12:54:58 UTC |
| f0ea122 | Raphaël Cauderlier | 27 June 2019, 06:08:47 UTC | [Doc] New talk | 27 June 2019, 06:08:47 UTC |
| 99679e1 | Raphaël Cauderlier | 11 June 2019, 16:22:35 UTC | [Contracts|Boomerang] Fix contract indentation | 11 June 2019, 16:22:35 UTC |
| 03007a6 | Raphaël Cauderlier | 10 June 2019, 13:48:41 UTC | Update boomerang The following version is proved: https://github.com/murbard/smart-contracts/commit/fb495fa4af3858fb258154074b10d1bcd666b838 | 10 June 2019, 13:48:41 UTC |
| 0adf5ed | b | 07 June 2019, 15:46:10 UTC | add boomerang | 07 June 2019, 15:46:10 UTC |
| 5c561bf | b | 07 June 2019, 10:49:34 UTC | return to sender | 07 June 2019, 10:50:37 UTC |
| c0b89f6 | Basile Pesin | 05 June 2019, 10:03:10 UTC | New proven smart-contract: vote.tz | 05 June 2019, 10:03:10 UTC |
| a0d465c | Basile Pesin | 29 May 2019, 09:23:15 UTC | Removed duplicate rule | 31 May 2019, 15:44:47 UTC |
| 443304c | Basile Pesin | 29 May 2019, 09:05:34 UTC | Updated michocott README | 31 May 2019, 15:44:46 UTC |
| 721313e | Basile Pesin | 29 May 2019, 09:01:49 UTC | Fixed michocott pdf generation | 31 May 2019, 15:44:16 UTC |
| 1018b2d | Raphaël Cauderlier | 31 May 2019, 11:56:31 UTC | Proofs of extensionality for sets and maps | 31 May 2019, 11:56:31 UTC |
| 877a6f2 | Basile Pesin | 27 May 2019, 13:13:29 UTC | Corrected typo | 27 May 2019, 13:13:29 UTC |
| 50b434e | Raphaël Cauderlier | 23 May 2019, 11:45:27 UTC | Add a tikz version of the Tezos logo | 23 May 2019, 11:45:27 UTC |
| 38f7ba5 | Raphaël Cauderlier | 20 May 2019, 15:40:27 UTC | [Doc] Add missing tezos logo | 20 May 2019, 15:40:27 UTC |
| 7adba0e | Raphaël Cauderlier | 20 May 2019, 15:38:19 UTC | [Doc] Update the Irif seminar slides | 20 May 2019, 15:38:19 UTC |
| f23ea6e | Raphaël Cauderlier | 18 May 2019, 14:35:01 UTC | [Doc] Add a logo for Mi-Cho-Coq | 18 May 2019, 14:35:34 UTC |
| 2a7d174 | Raphaël Cauderlier | 18 May 2019, 10:46:46 UTC | [Doc] Add a "singing battery" logo This logo is a pun in french, - "la pie qui chante" (literally "the singing magpie") is a french brand producing the Mi-Cho-Ko candies - "pile" in french means both "stack" and "battery" | 18 May 2019, 10:46:46 UTC |
| 0851734 | Raphaël Cauderlier | 17 May 2019, 22:38:03 UTC | [Doc] Slides for the seminar of the verification team of Irif | 17 May 2019, 22:39:50 UTC |
| b479da0 | Raphaël Cauderlier | 17 May 2019, 18:00:27 UTC | [Manager contract] Add the possiblity to send tokens to the contract without being the manager | 17 May 2019, 18:00:27 UTC |
