| refs/merge-requests/102/head | e8f74df | Proof for updateTokenPool | 05 March 2021, 14:06:39 UTC |
| refs/merge-requests/102/merge | b411636 | Dexter2/Proof: Proof for updateTokenPool | 05 March 2021, 14:06:39 UTC |
| refs/merge-requests/103/head | a47a2c0 | Fix missed occurrences of loc_micheline in Menhir file Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 24 March 2021, 07:53:54 UTC |
| refs/merge-requests/103/merge | 6ba8c47 | [Readme] Remove a TODO item | 25 April 2021, 12:26:44 UTC |
| refs/merge-requests/104/head | fac88a2 | Avoid parsing several times in main Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 02 March 2021, 16:36:26 UTC |
| refs/merge-requests/104/merge | 9fcea4f | Merge branch 'yrg@optimize-main' into 'dev' Avoid parsing 3 three times source file See merge request nomadic-labs/mi-cho-coq!104 | 02 March 2021, 17:23:30 UTC |
| refs/merge-requests/105/head | e1f3217 | Proof of setManager correctness Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 03 March 2021, 13:21:05 UTC |
| refs/merge-requests/105/merge | d258529 | Merge branch 'yrg@dexter_fa12lqt-verification-set-manager' into 'dexter_fa12lqt-verification' Proof of setManager correctness See merge request nomadic-labs/mi-cho-coq!105 | 05 March 2021, 12:19:06 UTC |
| refs/merge-requests/106/head | 6ba8ea5 | Make mutez more readable by keeping the proof implicit Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 03 March 2021, 13:20:01 UTC |
| refs/merge-requests/106/merge | db3fcd7 | Merge branch 'yrg@make-mutez-more-readable' into 'dev' Make mutez more readable by keeping the proof implicit See merge request nomadic-labs/mi-cho-coq!106 | 03 March 2021, 13:29:53 UTC |
| refs/merge-requests/107/head | 31d8f0b | Proof of correctness for TokenToXtz Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 03 March 2021, 13:45:27 UTC |
| refs/merge-requests/107/merge | ab14244 | Merge branch 'yrg@dexter_fa12lqt-verification-tokenToXtz' into 'dexter_fa12lqt-verification' Dexter2: Proof of ep_tokenToXTZ See merge request nomadic-labs/mi-cho-coq!107 | 10 March 2021, 16:44:43 UTC |
| refs/merge-requests/108/head | 58f6197 | Dexter2: Coq 8.8.0 fixes | 08 March 2021, 13:44:55 UTC |
| refs/merge-requests/108/merge | eb5c204 | Merge branch 'arvid@dexter_fa12lqt-verification__removeLiquidity' into 'dexter_fa12lqt-verification' Dexter2: Proof for add/removeLiquidity See merge request nomadic-labs/mi-cho-coq!108 | 08 March 2021, 19:00:10 UTC |
| refs/merge-requests/109/head | 416793b | Dexter2/Spec: Take care of division by zero Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 08 March 2021, 10:11:49 UTC |
| refs/merge-requests/109/merge | 6ef49ae | Merge branch 'yrg@dexter_fa12lqt-verification-update-spec' into 'dexter_fa12lqt-verification' Take division by zero into account in the specification See merge request nomadic-labs/mi-cho-coq!109 | 09 March 2021, 17:13:19 UTC |
| refs/merge-requests/11/head | c631a79 | [oracle_insurance|paper] add specification | 20 May 2019, 09:16:21 UTC |
| refs/merge-requests/11/merge | 45d99d6 | Merge branch 'prove_orcle_insurance' into 'master' WIP: Prove orcle insurance See merge request nomadic-labs/mi-cho-coq!11 | 16 March 2020, 16:57:54 UTC |
| refs/merge-requests/110/head | 59555da | Dexter2/Proof: Verify XtzToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 05 March 2021, 10:10:33 UTC |
| refs/merge-requests/110/merge | b04206f | Merge branch 'yrg@dexter_fa12lqt-verification-XtzToToken' into 'dexter_fa12lqt-verification' Dexter2: Verify XtzToToken See merge request nomadic-labs/mi-cho-coq!110 | 09 March 2021, 10:26:47 UTC |
| refs/merge-requests/111/head | 94c4e4d | Dexter2/Proof: prove tokenToToken | 08 March 2021, 20:16:48 UTC |
| refs/merge-requests/111/merge | fc0c014 | Merge branch 'arvid@guillaume-claret@dexter_fa12lqt-verification-bis' into 'dexter_fa12lqt-verification' Dexter: token_to_token entry-point See merge request nomadic-labs/mi-cho-coq!111 | 10 March 2021, 15:52:25 UTC |
| refs/merge-requests/112/head | b555744 | [extraction] Hack to support the old OCaml version used in the CI | 10 March 2021, 20:40:12 UTC |
| refs/merge-requests/112/merge | 7dcd422 | Merge branch 'rafoo@builtin_mutez' into 'dev' Represent mutez using the builtin int63 type See merge request nomadic-labs/mi-cho-coq!112 | 25 April 2021, 09:08:31 UTC |
| refs/merge-requests/113/head | d7b21f4 | [mi-cho-coq] Replace String.string_dec by String.eqb | 12 March 2021, 11:19:43 UTC |
| refs/merge-requests/113/merge | 7ccb336 | Use the fuel-free WP in Dexter proofs | 18 March 2021, 11:08:58 UTC |
| refs/merge-requests/114/head | 3ce377e | [Mi-Cho-Coq] Use the ascii boolean equality from the stdlib | 10 April 2021, 09:33:09 UTC |
| refs/merge-requests/114/merge | b1c8f8b | Merge branch 'guillaume-claret@use-string-eqb' into 'dev' Replace String.string_dec by String.eqb See merge request nomadic-labs/mi-cho-coq!114 | 25 April 2021, 10:55:29 UTC |
| refs/merge-requests/115/head | ee5330b | [ci/lint] run linting in a separate stage | 07 April 2021, 12:39:30 UTC |
| refs/merge-requests/115/merge | 9dd125a | Merge branch 'arvid@ci-lint-refactor' into 'dev' CI/Lint: refactor See merge request nomadic-labs/mi-cho-coq!115 | 07 April 2021, 13:06:55 UTC |
| refs/merge-requests/116/head | 59e5be5 | [ci] add contracts job | 07 April 2021, 15:59:42 UTC |
| refs/merge-requests/116/merge | a295b00 | Merge branch 'arvid@ci-build-refactor' into 'dev' CI: Refactor build by extracting contracts See merge request nomadic-labs/mi-cho-coq!116 | 08 April 2021, 16:15:06 UTC |
| refs/merge-requests/117/head | d30f3ab | [build] configure should recreate the src/_CoqProject file on each run | 08 April 2021, 17:09:50 UTC |
| refs/merge-requests/117/merge | 08f40b3 | Merge branch 'arvid@fix-root-configure-default' into 'dev' Fix the behaviour of `./configure` with no arguments See merge request nomadic-labs/mi-cho-coq!117 | 08 April 2021, 17:13:29 UTC |
| refs/merge-requests/118/head | 1916f18 | [mi-cho-coq] add compare_gt_lt to comparable.v | 09 October 2020, 16:44:52 UTC |
| refs/merge-requests/118/merge | 6ba8c47 | [Readme] Remove a TODO item | 25 April 2021, 12:26:44 UTC |
| refs/merge-requests/119/head | 9749d15 | [ci] add cache opam directory | 07 April 2021, 19:39:52 UTC |
| refs/merge-requests/119/merge | 8f57f12 | Merge branch 'arvid@ci-build-refactor-cache' into 'dev' Draft: [ci] add cache opam directory See merge request nomadic-labs/mi-cho-coq!119 | 10 May 2021, 07:35:53 UTC |
| refs/merge-requests/12/head | 877a6f2 | Corrected typo | 27 May 2019, 13:13:29 UTC |
| refs/merge-requests/120/head | 0617440 | [michocoq] Fuel-free WP in the LOOP-free case | 18 March 2021, 10:30:36 UTC |
| refs/merge-requests/120/merge | 6f7815a | Merge branch 'arvid@rafoo@fuelfree-wp' into 'dev' [Michocoq] Fuel-free WP for loop/lambda-free programs See merge request nomadic-labs/mi-cho-coq!120 | 25 April 2021, 12:22:00 UTC |
| refs/merge-requests/121/head | 54e84d6 | silly me | 08 April 2021, 19:02:15 UTC |
| refs/merge-requests/121/merge | 904746e | Merge branch 'arvid@re-organize-contracts_coq' into 'dev' Draft: Arvid@re organize contracts coq See merge request nomadic-labs/mi-cho-coq!121 | 10 May 2021, 07:35:53 UTC |
| refs/merge-requests/122/head | 71dac82 | [Michocoq] ignore annotations on sum types everywhere but in parameter Fixes #49. | 09 April 2021, 16:15:04 UTC |
| refs/merge-requests/122/merge | 82c7148 | Merge branch 'rafoo@issue_49' into 'dev' [Michocoq] ignore annotations on sum types everywhere but in parameter See merge request nomadic-labs/mi-cho-coq!122 | 25 April 2021, 08:55:57 UTC |
| refs/merge-requests/123/head | 2690e7d | [michocoq] Avoid redefining `False` in `util.v` The name of the Michelson data constructor `False` clashes with the Coq proposition for contradiction. To avoid qualifying the Coq proposition, `util.v` redefines it so `util.False` is defined as `Logic.False`. This has unpleasant side effects (see https://gitlab.com/nomadic-labs/mi-cho-coq/-/issues/53) so we remove this definition and qualify the name in the few places where it is used instead. Closes #53. | 11 April 2021, 14:59:11 UTC |
| refs/merge-requests/123/merge | 8c4bba1 | Merge branch 'rafoo@False_shadowing' into 'dev' [michocoq] Avoid redefining `False` in `util.v` See merge request nomadic-labs/mi-cho-coq!123 | 11 April 2021, 15:05:20 UTC |
| refs/merge-requests/124/head | 5e26350 | Proof of xtzToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 28 April 2021, 19:06:18 UTC |
| refs/merge-requests/124/merge | 1bbce76 | Merge branch 'arvid@cpmm2-verification' into 'dexter_fa12lqt-verification' Draft: Adapt Dexter2 proofs for CPMM2 See merge request nomadic-labs/mi-cho-coq!124 | 30 April 2021, 11:11:23 UTC |
| refs/merge-requests/125/head | 5e26350 | Proof of xtzToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 28 April 2021, 19:06:18 UTC |
| refs/merge-requests/125/merge | 10366a2 | Merge branch 'cpmm2-verification--xtzToToken' into 'arvid@cpmm2-verification' [cpmm2] verification xtz to token See merge request nomadic-labs/mi-cho-coq!125 | 30 April 2021, 10:24:31 UTC |
| refs/merge-requests/126/head | d4f5295 | Update manager.tz tz1YzL2mw23UWbzN4C1JKXCWM3eJDh3KZRnf | 23 April 2021, 01:48:54 UTC |
| refs/merge-requests/126/merge | b0c90bc | Merge branch 'nmm5055-master-patch-57340' into 'master' Update manager.tz See merge request nomadic-labs/mi-cho-coq!126 | 23 April 2021, 01:50:42 UTC |
| refs/merge-requests/127/head | 6406bf3 | [Mi-Cho-Coq] add a function to invoke a particular entrypoint | 07 May 2021, 08:03:06 UTC |
| refs/merge-requests/127/merge | b3c57b5 | Merge branch 'rafoo@entrypoint_call' into 'dev' Entrypoint calls See merge request nomadic-labs/mi-cho-coq!127 | 07 May 2021, 21:08:14 UTC |
| refs/merge-requests/128/head | 6ba8c47 | [Readme] Remove a TODO item | 25 April 2021, 12:26:44 UTC |
| refs/merge-requests/128/merge | a4e70ad | Merge branch 'rafoo@unaxiomatize_operations' into 'dev' Don't axiomatize operations See merge request nomadic-labs/mi-cho-coq!128 | 25 April 2021, 13:09:08 UTC |
| refs/merge-requests/129/head | 1f0c097 | Functional specification and proof for TokenToXTZ Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 16 April 2021, 14:03:14 UTC |
| refs/merge-requests/129/merge | bc22dd2 | Merge branch 'cpmm2-verification--tokenToXtz' into 'arvid@cpmm2-verification' Cpmm2 verification token to xtz See merge request nomadic-labs/mi-cho-coq!129 | 30 April 2021, 10:01:48 UTC |
| refs/merge-requests/13/head | a0d465c | Removed duplicate rule | 29 May 2019, 09:23:15 UTC |
| refs/merge-requests/130/head | b983c92 | New spec and proof for TokenToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 29 April 2021, 08:15:33 UTC |
| refs/merge-requests/130/merge | 18d7952 | Merge branch 'cpmm2-verification--tokenToToken' into 'arvid@cpmm2-verification' New spec and proof for TokenToToken See merge request nomadic-labs/mi-cho-coq!130 | 30 April 2021, 09:32:40 UTC |
| refs/merge-requests/131/head | af302e2 | [michocoq] generalize map.remove_present_untouched We don't assume anymore that the first key is associated with something in the map. | 31 May 2021, 20:24:21 UTC |
| refs/merge-requests/131/merge | 6b573da | Merge branch 'rafoo@map_extra_lemmas' into 'dev' [michocoq] generalize map.remove_present_untouched See merge request nomadic-labs/mi-cho-coq!131 | 31 May 2021, 20:28:27 UTC |
| refs/merge-requests/132/head | 7a7a1aa | [michocoq] Redefine set.remove so that it computes Before this commit, set.remove uses List.remove which only computes when its decide_equality argument does. We passed it an opaque lemma so it did not compute. Moreover, it always scanned the whole list but since we only apply it on sorted lists it could stop as soon as it encounters a value larger than the one to remove. This commit redefines set.remove so that it does not depend on decidability of equality anymore and returns as soon as it can. | 31 May 2021, 22:11:03 UTC |
| refs/merge-requests/132/merge | cc4240c | Merge branch 'rafoo@transparent_set_remove' into 'dev' [michocoq] Redefine set.remove so that it computes See merge request nomadic-labs/mi-cho-coq!132 | 31 May 2021, 22:19:06 UTC |
| refs/merge-requests/15/head | 044b7be | Proofs of extensionality for sets and maps | 30 May 2019, 22:17:41 UTC |
| refs/merge-requests/16/head | fcd4f10 | Simplified proof in comparable.v | 05 June 2019, 09:37:19 UTC |
| refs/merge-requests/17/head | 5c561bf | return to sender | 07 June 2019, 10:49:34 UTC |
| refs/merge-requests/18/head | 729a333 | rename contract | 07 June 2019, 12:26:49 UTC |
| refs/merge-requests/19/head | 0adf5ed | add boomerang | 07 June 2019, 15:46:10 UTC |
| refs/merge-requests/2/head | 52f92a6 | Adding Mutually calling contracts | 15 March 2019, 13:20:40 UTC |
| refs/merge-requests/21/head | 2b4e968 | Install Coq libraries | 20 June 2019, 16:39:23 UTC |
| refs/merge-requests/22/head | 66fe957 | Apply suggestion to src/contracts_coq/generic_multisig.v | 01 July 2019, 12:42:49 UTC |
| refs/merge-requests/23/head | 481dcf4 | [Mi-Cho-Coq|Multisig]: light cleaning | 28 June 2019, 07:23:22 UTC |
| refs/merge-requests/25/head | 3b312a4 | Type SELF in lambda correctly | 28 June 2019, 14:53:19 UTC |
| refs/merge-requests/26/head | efefd74 | Changed some Qed to Defined | 02 July 2019, 10:47:24 UTC |
| refs/merge-requests/27/head | c45ad1c | Mi-Cho-Coq: fix typo | 12 July 2019, 10:05:17 UTC |
| refs/merge-requests/27/merge | 4dbed10 | Merge branch 'section-refactor' into 'master' Section refactor See merge request nomadic-labs/mi-cho-coq!27 | 12 July 2019, 10:04:47 UTC |
| refs/merge-requests/28/head | fe7bd91 | Stateful evaluation Evaluating a Michelson instruction is not totally stateless. In particular there are a few cases where I; I; ASSERT_CMPEQ actually fails: - I = STEPS_TO_QUOTA because the second one has less gas available - instructions producing operations because operations are signed with a cryptographic nonce that changes at each operation This commit axiomatizes a notion of evaluation state that is preserved by all instructions but those. | 08 July 2019, 15:54:13 UTC |
| refs/merge-requests/28/merge | 6ba8c47 | [Readme] Remove a TODO item | 25 April 2021, 12:26:44 UTC |
| refs/merge-requests/3/head | 1a00281 | Make `./configure` more reliable | 22 March 2019, 13:49:12 UTC |
| refs/merge-requests/32/head | 40a3ee2 | [coq|spend]add proof | 16 July 2019, 13:12:04 UTC |
| refs/merge-requests/32/merge | 507e275 | Merge branch 'contract_spend' into 'master' WIP: Contract spend See merge request nomadic-labs/mi-cho-coq!32 | 16 March 2020, 17:00:38 UTC |
| refs/merge-requests/33/head | 90bcdb9 | Added IS_NAT and INT instruction | 26 July 2019, 09:49:19 UTC |
| refs/merge-requests/35/head | e538b10 | Use the stable version of coq-ott | 20 September 2019, 09:06:06 UTC |
| refs/merge-requests/35/merge | 5b23511 | Merge branch 'guillaume.claret-prepare-public-opam-package' into 'master' Prepare public opam package See merge request nomadic-labs/mi-cho-coq!35 | 20 September 2019, 09:12:35 UTC |
| refs/merge-requests/4/head | e2e399c | [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 |
| refs/merge-requests/40/head | ab8c856 | Make sure that make clean removes files generated by extraction | 23 October 2019, 08:52:16 UTC |
| refs/merge-requests/40/merge | 08f3bd6 | Merge branch 'arvid@fix-clean-extraction' into 'master' Make sure that make clean removes files generated by extraction See merge request nomadic-labs/mi-cho-coq!40 | 23 October 2019, 08:54:20 UTC |
| refs/merge-requests/43/head | edb58ee | Update coq-mi-cho-coq.opam: remove duplicate synpopsis | 06 November 2019, 15:08:13 UTC |
| refs/merge-requests/43/merge | b3f5581 | Merge branch 'patch-1-duplicate-synopsis' into 'master' Update coq-mi-cho-coq.opam: remove duplicate synpopsis See merge request nomadic-labs/mi-cho-coq!43 | 06 November 2019, 15:08:25 UTC |
| refs/merge-requests/45/head | a7655d8 | Formatting | 23 November 2019, 08:33:21 UTC |
| refs/merge-requests/45/merge | 4c97469 | Merge branch 'raphael@fix_printer' into 'master' Printer: simplify Michelson -> Micheline and hopefully fix printing of DIP See merge request nomadic-labs/mi-cho-coq!45 | 25 November 2019, 10:24:40 UTC |
| refs/merge-requests/47/head | ac14acd | Add the IF_RIGHT macro at the typed syntax level | 28 November 2019, 10:00:56 UTC |
| refs/merge-requests/47/merge | c1d827c | Merge branch 'raphael@remove_if_right' into 'master' Remove IF_RIGHT See merge request nomadic-labs/mi-cho-coq!47 | 28 November 2019, 10:03:17 UTC |
| refs/merge-requests/49/head | cdc97c1 | [CI] Add Coq v8.10 | 28 November 2019, 15:06:48 UTC |
| refs/merge-requests/49/merge | 5cfc679 | Merge branch 'raphael@ci-coq8.10' into 'master' [CI] Add Coq v8.10 See merge request nomadic-labs/mi-cho-coq!49 | 28 November 2019, 15:09:09 UTC |
| refs/merge-requests/50/head | dc275c8 | Fix the install of the michocoq binary | 04 December 2019, 09:27:10 UTC |
| refs/merge-requests/50/merge | bc1c08e | Merge branch 'fix-opam-install' into 'master' Fix install of the michocoq binary See merge request nomadic-labs/mi-cho-coq!50 | 04 December 2019, 09:40:10 UTC |
