| 4f48fcc | Arvid Jakobsson | 26 August 2019, 08:38:06 UTC | semantics equivalence for fragment assuming injectivity of untyper | 26 August 2019, 08:38:06 UTC |
| 16a78ef | Arvid Jakobsson | 23 August 2019, 12:59:36 UTC | WIP semantics equivalence for fragment | 23 August 2019, 12:59:36 UTC |
| cf414b6 | Arvid Jakobsson | 21 August 2019, 09:25:48 UTC | equivalence for dynamic semantics in one direction | 21 August 2019, 09:25:48 UTC |
| 08a61ba | Arvid Jakobsson | 20 August 2019, 13:49:36 UTC | typing equivalence for fragment | 20 August 2019, 13:49:36 UTC |
| 5fc0ae5 | Arvid Jakobsson | 19 August 2019, 09:21:53 UTC | WIP : partial typing equivalence | 19 August 2019, 09:21:53 UTC |
| 4244362 | Arvid Jakobsson | 14 August 2019, 18:44:36 UTC | WIP3 : typing equivalence (almost) done | 14 August 2019, 18:44:36 UTC |
| 068e942 | Arvid Jakobsson | 14 August 2019, 13:51:06 UTC | WIP 2 | 14 August 2019, 13:51:06 UTC |
| 3d35778 | Arvid Jakobsson | 14 August 2019, 09:25:18 UTC | equivalence WIP | 14 August 2019, 09:25:18 UTC |
| 535718d | Arvid Jakobsson | 14 August 2019, 07:21:37 UTC | fragment with more sharing between coq and ott data (untyped syntax, type) | 14 August 2019, 07:21:37 UTC |
| 2993ed3 | Arvid Jakobsson | 13 August 2019, 10:13:18 UTC | Equivalence type data | 13 August 2019, 10:13:18 UTC |
| 670a9a4 | Arvid Jakobsson | 13 August 2019, 10:11:57 UTC | Remove NIL instruction from fragment Since there is no concrete_data for lists, it does not make sense IMO to have this instruction | 13 August 2019, 10:11:57 UTC |
| 2a2a86f | Arvid Jakobsson | 13 August 2019, 10:11:17 UTC | Use N instead of nat in fragment_ott | 13 August 2019, 10:11:17 UTC |
| a61285b | Arvid Jakobsson | 12 August 2019, 14:19:11 UTC | WIP fragment of ott with typing rules with compiling coq extraction | 12 August 2019, 14:19:11 UTC |
| 15d1a9f | Arvid Jakobsson | 12 August 2019, 12:58:19 UTC | Fix string problem | 12 August 2019, 12:58:19 UTC |
| 74d41ee | Arvid Jakobsson | 12 August 2019, 12:52:41 UTC | Merge branch 'michocott_typing' into arvid@fragment_typer_and_ott_typing | 12 August 2019, 12:52:41 UTC |
| d31b443 | Arvid Jakobsson | 12 August 2019, 12:50:06 UTC | Rebase on master | 12 August 2019, 12:50:06 UTC |
| 11d4066 | Arvid Jakobsson | 12 August 2019, 12:19:16 UTC | Port certified typer to fragment | 12 August 2019, 12:26:05 UTC |
| 22c447d | Raphaël Cauderlier | 24 April 2019, 14:35:24 UTC | Extract a fragment of the Michelson language for testing ideas | 12 August 2019, 12:26:05 UTC |
| a6f49bd | Basile Pesin | 26 July 2019, 09:49:19 UTC | Added INT and IS_NAT | 12 August 2019, 12:26:05 UTC |
| 56170e9 | Basile Pesin | 25 July 2019, 16:18:34 UTC | Dig and Dug type-checking | 12 August 2019, 12:26:05 UTC |
| 234383b | Basile Pesin | 22 July 2019, 09:12:03 UTC | Added a specific case for PUSH _ Concrete_seq, to avoid bad line feeds | 12 August 2019, 12:25:09 UTC |
| 8f0d392 | Basile Pesin | 19 July 2019, 09:02:03 UTC | Fixed pretty printer | 12 August 2019, 12:25:09 UTC |
| 8d53f81 | Basile Pesin | 18 July 2019, 13:47:51 UTC | Flattening sequences and slightly improved the pretty-printer | 12 August 2019, 12:25:09 UTC |
| 3db6033 | Basile Pesin | 18 July 2019, 11:16:42 UTC | Added micheline2michelson converter | 12 August 2019, 12:25:09 UTC |
| 4ce70f4 | Basile Pesin | 15 July 2019, 16:32:37 UTC | Updated menhir to 20190626 | 12 August 2019, 12:25:09 UTC |
| 924154e | Basile Pesin | 15 July 2019, 15:06:21 UTC | UNPAIR macro and extracting untyped_syntax and typer | 12 August 2019, 12:25:09 UTC |
| c857970 | Basile Pesin | 12 July 2019, 17:01:33 UTC | Refactor sections into modules after rebase, missing DIG and DUG typers | 12 August 2019, 12:25:09 UTC |
| 0389bd6 | Raphaël Cauderlier | 23 June 2019, 21:29:08 UTC | Also fix the proofs of the new smart contracts | 12 August 2019, 12:25:09 UTC |
| da675f1 | Raphaël Cauderlier | 23 June 2019, 21:06:12 UTC | Fix a proof in map.v | 12 August 2019, 12:25:09 UTC |
| 9574a80 | Basile Pesin | 07 June 2019, 14:56:26 UTC | Added a lemma on string lexing | 12 August 2019, 12:25:09 UTC |
| 540786a | Basile Pesin | 06 June 2019, 20:06:32 UTC | Added pretty-printer function for micheline | 12 August 2019, 12:25:09 UTC |
| dba987e | Basile Pesin | 06 June 2019, 09:44:25 UTC | Fixed eqb for coq 8.8.2 | 12 August 2019, 12:25:09 UTC |
| 1df33a4 | 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. | 12 August 2019, 12:25:09 UTC |
| 6aba875 | Raphael Cauderlier | 22 March 2019, 10:01:18 UTC | [Michocott] Untrack and ignore the .v file generated by OTT | 12 August 2019, 12:20:53 UTC |
| f17ad38 | Raphael Cauderlier | 20 March 2019, 14:42:05 UTC | [Micheline] Micheline parser | 12 August 2019, 12:20:53 UTC |
| 0c8b5ec | Raphael Cauderlier | 18 March 2019, 09:12:44 UTC | [Micheline] Micheline lexer | 12 August 2019, 12:20:53 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 |
| 3fdbc74 | Basile Pesin | 31 May 2019, 13:43:15 UTC | Corrected the 'a's that were changed in 'ty2's | 03 June 2019, 07:30:20 UTC |
| 8462865 | Basile Pesin | 30 May 2019, 18:38:34 UTC | Fixed for coq v8.9 | 03 June 2019, 07:30:20 UTC |
| 2ce84b2 | Basile Pesin | 30 May 2019, 17:27:17 UTC | All the way to extraction | 03 June 2019, 07:30:19 UTC |
| bb8a3e7 | Basile Pesin | 30 May 2019, 16:01:51 UTC | Removed ambiguity by adding explicit annotations | 03 June 2019, 07:30:18 UTC |
| 78588f7 | 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 | 03 June 2019, 07:30:18 UTC |
| f685007 | Basile Pesin | 29 May 2019, 19:06:58 UTC | ott spec OK except for list and map | 03 June 2019, 07:30:17 UTC |
| 5112e40 | Basile Pesin | 29 May 2019, 13:09:06 UTC | Changed symbol for typing to '::' and symbol for cons to ':' in michelson_typing | 03 June 2019, 07:30:17 UTC |
| cf3768b | 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. | 03 June 2019, 07:29:26 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 |
| 398d4a6 | Raphaël Cauderlier | 17 May 2019, 15:22:18 UTC | New proven smart contract: manager.tz This contract can be used as a replacement of scriptless KT1s. | 17 May 2019, 15:22:18 UTC |
| 59f1f4b | Raphael Cauderlier | 05 April 2019, 08:53:13 UTC | [FIX] Makes the `address` type comparable. Contrary to what the documentation of Michelson claims, the `address` type is comparable in the OCaml implementation. This commit makes it comparable in Mi-Cho-Coq too. | 17 May 2019, 13:53:30 UTC |
| 53f7fcd | b | 18 March 2019, 09:56:01 UTC | [Michocoq] list_ -> list, option_ -> option, set_ -> set | 09 April 2019, 08:42:33 UTC |
| 65729a8 | Raphaël Cauderlier | 05 April 2019, 14:14:45 UTC | [CI] Install a recent version of `shellcheck` | 09 April 2019, 07:23:48 UTC |
| b4b5e0e | Brian Guo | 04 April 2019, 16:39:17 UTC | [fix] configure files in src subdirectories should now also work for mac | 09 April 2019, 07:23:48 UTC |
| 044efcc | Brian Guo | 05 April 2019, 20:18:13 UTC | [add] moved important tactics to util file; used tactics in multisig | 05 April 2019, 20:18:13 UTC |
| e2e399c | Raphael Cauderlier | 03 April 2019, 14:03:44 UTC | [CI] Continuous integration The CI script does the following: - lint the `configure` shell scripts using `shellcheck` - lint the file `README.org` using `org-lint` - compile the project with Coq v8.8 and Coq v8.9. | 03 April 2019, 14:03:44 UTC |
| baa2a13 | Raphael Cauderlier | 03 April 2019, 14:01:28 UTC | [multisig] Replace `injection; discriminate` by `discriminate`. Some versions of Coq fail at useless calls to `injection`. | 03 April 2019, 14:01:28 UTC |
| 9019629 | Raphael Cauderlier | 03 April 2019, 14:00:31 UTC | [build] By default, do not build the documentation | 03 April 2019, 14:00:31 UTC |
| 029eead | Raphael Cauderlier | 23 March 2019, 05:57:26 UTC | [Build] Drop support for Coq < 8.8 | 03 April 2019, 13:56:13 UTC |
| 0b1a985 | Raphael Cauderlier | 22 March 2019, 16:15:53 UTC | [build] Ignore shellcheck false alarms | 03 April 2019, 13:54:29 UTC |
| 4f5d906 | Raphael Cauderlier | 03 April 2019, 13:32:35 UTC | [License] Add License headers to all files | 03 April 2019, 13:49:51 UTC |
| a9a08d3 | Raphael Cauderlier | 03 April 2019, 13:31:22 UTC | [License] Assign copyright to Nomadic Labs | 03 April 2019, 13:45:54 UTC |
