https://gitlab.com/nomadic-labs/mi-cho-coq
Name Target Message Date
HEAD f6a9666 talk_18_01_2021_cpp_lightning_talk 19 January 2021, 14:54:50 UTC
refs/heads/51-verify-dexter-2-dexter-fa1-2lqt-dexter-1-5 eb5a0b4 [build] sort and remove duplicates in the opam dependencies 22 June 2020, 13:14:49 UTC
refs/heads/Julien@adding_contracts 52f92a6 Adding Mutually calling contracts 15 March 2019, 13:20:40 UTC
refs/heads/arvid@ci-build-refactor-cache 9749d15 [ci] add cache opam directory 07 April 2021, 19:39:52 UTC
refs/heads/arvid@ci-rethinking 401e2f7 [ci] split out linting 12 February 2021, 19:32:23 UTC
refs/heads/arvid@cpmm-verification 10d93ac tmp: remove dexter to make pipeline leaner 02 February 2021, 18:38:48 UTC
refs/heads/arvid@cpmm2-verification 5e26350 Proof of xtzToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 28 April 2021, 19:06:18 UTC
refs/heads/arvid@dexter-lemmas-and-refactorings 1916f18 [mi-cho-coq] add compare_gt_lt to comparable.v 09 October 2020, 16:44:52 UTC
refs/heads/arvid@dexter-verification-parsing-test 41c95a7 [Dexter parsing] Minor modif to debug the storage type difference 04 June 2020, 13:35:59 UTC
refs/heads/arvid@dexter-verification-stringfix 70173e1 [dexter] wip: try fix notation error 21 September 2020, 06:44:50 UTC
refs/heads/arvid@dexter-verification-updates-20200928-coq8.08 08edb74 [dexter] update proof for exchange entrypoints 28 September 2020, 21:46:43 UTC
refs/heads/arvid@dexter_fa12lqt-verification__addLiquidity 0ff13fc Dexter2/Proof: addLiquidity 02 March 2021, 17:52:07 UTC
refs/heads/arvid@dexter_fa12lqt-verification__removeLiquidity 58f6197 Dexter2: Coq 8.8.0 fixes 08 March 2021, 13:44:55 UTC
refs/heads/arvid@fragment_typer_and_ott_typing 4f48fcc semantics equivalence for fragment assuming injectivity of untyper 26 August 2019, 08:38:06 UTC
refs/heads/arvid@guillaume-claret@dexter_fa12lqt-verification 9eed601 Dexter2/Proof: prove tokenToToken 08 March 2021, 20:16:48 UTC
refs/heads/arvid@guillaume-claret@dexter_fa12lqt-verification-bis 94c4e4d Dexter2/Proof: prove tokenToToken 08 March 2021, 20:16:48 UTC
refs/heads/arvid@opaque-tez-experiments 8c110f0 Opacity attempt 04 March 2021, 20:49:39 UTC
refs/heads/arvid@rafoo@simplify-eval_precond-rebased 5796046 Simplification of the formula produced by eval_precond The following simplifications are applied: - eval_seq_precond immediately returns `False` on instruction sequences ending with a `FAILWITH` (it does so by looking at the tail-fail flag) - `match x with C1 y => phi y | C2 y => False` becomes `exists y, x = C1 y /\ phi y` - the code produced for `IF_ f` depends on the if-family `f` to avoid the previous double pattern matching: for example for options it produces `match o with | Some x -> ... | None -> ... end` instead of `match (match o with Some x -> inl x | None -> inr tt end) with inl x -> ... | inr y -> ... end`. Thanks to these simplifications, the proofs in the contract_coq directory are simpler. 31 May 2020, 13:08:41 UTC
refs/heads/arvid@re-organize-contracts_coq 54e84d6 silly me 08 April 2021, 19:02:15 UTC
refs/heads/backport-opam-package-changes-from-upstream 5833769 PAPAIR and UNPAPAIR macros 18 October 2019, 14:00:51 UTC
refs/heads/bb@dexter-verification ccf5f78 [dexter] proof for ep_setBaker_correct 07 September 2020, 08:49:03 UTC
refs/heads/chain-modelisation-guestbook 1b25d13 Prove functional spec of guestbook contract and simple lifetime prop 10 March 2020, 17:36:01 UTC
refs/heads/colin-dexter_fa12lqt-verification e8f74df Proof for updateTokenPool 05 March 2021, 14:06:39 UTC
refs/heads/contract_spend 40a3ee2 [coq|spend]add proof 16 July 2019, 13:12:04 UTC
refs/heads/dev 6406bf3 [Mi-Cho-Coq] add a function to invoke a particular entrypoint 07 May 2021, 08:03:06 UTC
refs/heads/dexter-dfs-compat 936d209 Dexter DFS compat: always call trusted contracts first There are 3 cases where Dexter emits more than an operation at once. In two of them, a potential attacker is called first. If this attacker can produce DFS calls it may be able to access Dextex before the FA1.2 is updated so some invariants might be broken. We haven't managed to use DFS calls to attack Dexter but always calling uncontrolled contracts last in the operation list is always safer. 06 February 2021, 22:41:46 UTC
refs/heads/dexter-fa2-verification-hackish 54cba5c [dexter/fa2] update proofs 12 February 2021, 17:51:37 UTC
refs/heads/dexter-verification 4f96fe5 [dexter] functional certification of Dexter Dexter version: 4e24123. The formal specification is based on the informal specification dated September 31, 2020. This is a joint work by: - Arvid Jakobsson, Nomadic Labs - Kristina Sojakova, INRIA - Colin González, Nomadic Labs 10 October 2020, 14:23:15 UTC
refs/heads/dexter-verification-approve d2f3f7c experiments 01 June 2020, 17:35:47 UTC
refs/heads/dexter-verification-cleanup-lemmas 24e1381 [dexter] clean up lemmas wip 2 wip 3 temp 09 October 2020, 13:09:26 UTC
refs/heads/dexter-verification-rebase 0df29e8 [dexter] updates for new contract/address formalization 15 September 2020, 12:45:46 UTC
refs/heads/dexter_fa12lqt-verification 7ccb336 Use the fuel-free WP in Dexter proofs 18 March 2021, 11:08:58 UTC
refs/heads/entrypoints a1eb552 disallow SELF in lambdas 19 July 2019, 12:58:11 UTC
refs/heads/guillaume-claret-add-entrypoint-to-self 447c99f Add an entrypoint to SELF 09 March 2020, 17:44:44 UTC
refs/heads/guillaume-claret-full-eval-function ad13642 WIP 03 January 2020, 17:01:17 UTC
refs/heads/guillaume-claret-gadts-without-annotations 9ed92e0 Add beginning of equivalence of the interpreters 17 December 2019, 14:31:02 UTC
refs/heads/guillaume-claret-integrate-coq-of-ocaml-output a5c0f3c [of_ocaml] Add generated Coq code from the Tezos protocol with some proofs 18 February 2020, 14:19:28 UTC
refs/heads/guillaume-claret-semantics-injection d8e3789 WIP 17 March 2020, 21:14:03 UTC
refs/heads/guillaume-claret@dexter_fa12lqt-verification 7a18337 WIP 08 March 2021, 20:16:48 UTC
refs/heads/guillaume-claret@dexter_fa12lqt-verification-benchmark-token-to-token 49b0bb6 Benchmark after cleaning 12 March 2021, 15:42:11 UTC
refs/heads/guillaume-claret@dexter_fa12lqt-verification-experiments c944fe4 WIP 12 March 2021, 10:37:39 UTC
refs/heads/guillaume-claret@dexter_fa12lqt-verification-string-eqb d7b21f4 [mi-cho-coq] Replace String.string_dec by String.eqb 12 March 2021, 11:19:43 UTC
refs/heads/improve_multisig f78585b [presentation|multisig]Add presentation about multisig's modification 11 June 2019, 12:46:36 UTC
refs/heads/internship_report 0bb78dd update 17 September 2019, 14:54:51 UTC
refs/heads/intership_presentation 8f17689 Commentaires préliminaires sur la présentation 18 September 2019, 11:19:31 UTC
refs/heads/julien@entrypoint_notations b2cd050 [Michocoq|Syntax] or notation 13 March 2020, 06:33:08 UTC
refs/heads/julien@gasoline_inconsistent_universe e696fe1 WIP 22 May 2019, 09:29:19 UTC
refs/heads/julien@mutually_calling_contracts 4a816a3 [contracts|insurance] weather insurance using simple dedicated oracle 27 June 2019, 21:13:54 UTC
refs/heads/kristina-fa12-verification-rebase d116674 Added README 11 May 2021, 09:41:59 UTC
refs/heads/kristina@fa12-verification-rebase 904c90c Using entrypoint trees instead of parameters. 03 June 2021, 09:41:17 UTC
refs/heads/kristina@fa2 b2d12f9 Initial commit. 20 May 2021, 14:48:24 UTC
refs/heads/manager-contract-do-entry 89f04ee Remove redundant entrypoints 10 July 2019, 22:37:18 UTC
refs/heads/master f6a9666 talk_18_01_2021_cpp_lightning_talk 19 January 2021, 14:54:50 UTC
refs/heads/merge-contract 2096672 Rename "contract constants" into addresses 21 July 2019, 13:38:36 UTC
refs/heads/merge-contract_multithreaded_simpl 04dbeb9 clear spec, 09 July 2019, 14:55:14 UTC
refs/heads/merge_with_shared_storage bda8d8b [merge_with_shared_storage]add code and proof 29 July 2019, 13:13:46 UTC
refs/heads/michelson_fragment b95225e Experiment with gas and fuel. 05 July 2019, 13:20:29 UTC
refs/heads/miguelito c1a9d0b Miguelito some progress 28 March 2019, 16:48:02 UTC
refs/heads/old_merge_with_shared_storage 6b65a39 [merge_with_shared_storage]add code and proof 29 July 2019, 13:13:46 UTC
refs/heads/old_merge_with_shared_storage_WIP 1f8e2cf tmp 10 August 2019, 15:50:24 UTC
refs/heads/old_merge_with_shared_storage_use eeb953e add contract_id 09 August 2019, 13:11:04 UTC
refs/heads/old_resiliable_contract_ b5a01c9 [enable_pause_spec]en cours 30 July 2019, 15:44:25 UTC
refs/heads/proto-proposal c4ef17b [Michocoq] Add GET_AND_UPDATE 12 January 2021, 20:18:17 UTC
refs/heads/rafoo@concert_integration 97d11c9 Move data_aux outside of the semantics functor 31 May 2021, 20:11:50 UTC
refs/heads/rafoo@dexter_fa12lqt-verification cfc357c Use the fuel-free WP in Dexter proofs 18 March 2021, 11:08:58 UTC
refs/heads/rafoo@dexter_perf_experiment 927aa34 Dexter proof: delay computation of the typed scripts and use vm_compute 17 March 2021, 09:24:12 UTC
refs/heads/rafoo@map_extra_lemmas 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/heads/rafoo@mutez_opacity f8ed4ec WIP: mutez opacity This hides the definition of the tez.mutez type behind an opacity layer defined by an opaque dependent record (containing the type, conversion functions from and to Z and lemmas about them). TODO: fix the proof of the vesting_tez contract. It is currently commented because calling any computation command on the parsed file takes forever. 08 March 2021, 21:45:10 UTC
refs/heads/rafoo@primitives 317fda5 [Skip-ci] WIP: primitive and macro lexing and pretty-printing 06 February 2021, 14:51:40 UTC
refs/heads/rafoo@semantics-projections 75aba35 WIP: redefine the evaluator to use fst and snd instead of pattern-matching on pairs 11 March 2021, 14:59:19 UTC
refs/heads/rafoo@slides_inria_day 6e53f26 Adapt to Bruno's template 19 September 2020, 19:17:41 UTC
refs/heads/rafoo@talk_nl_seminar 8ed2906 Final fixes 10 November 2020, 13:31:44 UTC
refs/heads/rafoo@tpbc 4eabc12 [doc] Slides TPBC 23 June 2020, 21:40:11 UTC
refs/heads/rafoo@transparent_set_remove 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/heads/rafoo@tzt 6410e49 WIP: self and param 06 May 2020, 11:24:39 UTC
refs/heads/raphael@precond_iter 116ac0b WIP: precond_iter 29 November 2019, 09:22:33 UTC
refs/heads/raphael@tuto e22bd2c Michocott: add coqdoc.sty in .gitignore 18 March 2019, 09:13:59 UTC
refs/heads/return2sender 729a333 rename contract 07 June 2019, 12:26:49 UTC
refs/heads/self_in_origination 59419d4 Remove unused module dependencies 03 October 2019, 14:10:15 UTC
refs/heads/specialised-multisig b9a0809 Mi-Cho-Coq/Contracts: formal proof of the specialised multisig 19 May 2020, 14:51:03 UTC
refs/heads/stateful 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/heads/yrg@cpmm2-economic-properties bac4a6e Add a report about CPMM proofs Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 03 June 2021, 05:48:24 UTC
refs/heads/yrg@cpmm2-new-version 466c12e Update code and proof of CPMM2 Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 12 May 2021, 07:52:52 UTC
refs/heads/yrg@dexter_fa12lqt-verification-XtzToToken 59555da Dexter2/Proof: Verify XtzToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 05 March 2021, 10:10:33 UTC
refs/heads/yrg@dexter_fa12lqt-verification-set-manager e1f3217 Proof of setManager correctness Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 03 March 2021, 13:21:05 UTC
refs/heads/yrg@dexter_fa12lqt-verification-tokenToXtz 31d8f0b Proof of correctness for TokenToXtz Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 03 March 2021, 13:45:27 UTC
refs/heads/yrg@dexter_fa12lqt-verification-update-spec 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/heads/yrg@make-mutez-more-readable 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/heads/yrg@optimize-micheline-lexer 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/heads/yrg@optimize-micheline-lexical-analysis 92c0f63 Micheline_lexer: Remove unused argument in range_aux Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 23 March 2021, 08:13:23 UTC
refs/heads/yrg@refactor-make-mutez-more-readable 8d7ecbe 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/heads/yrg@verify-vesting 57f6eb8 Verify a vesting contract Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> Almost done Almost finished verification of a vesting contract Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> Rename source file for vesting. Remove last admits. Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> 26 February 2021, 13:49:29 UTC
refs/heads/yrg@wip-cpmm2-economic-properties 0a2d979 WIP 27 May 2021, 05:36:23 UTC
refs/heads/zhenlei@cancellable_contract d33836b [util]simpl_fuel can apply on hypothesis 30 September 2019, 13:17:11 UTC
refs/heads/zhenlei@internship_report d5d8e4e [zhenlei]add presentation about the internship 26 September 2019, 09:13:06 UTC
refs/heads/zhenlei@merge_shared_tree cc3d995 [merge_shared_tree|Coq]WIP: add the generator of contract 30 September 2019, 09:35:04 UTC
refs/merge-requests/1/head 9fa0d6f OTT now compiles 14 March 2019, 16:03:27 UTC
refs/merge-requests/100/head 7ccb336 Use the fuel-free WP in Dexter proofs 18 March 2021, 11:08:58 UTC
refs/merge-requests/100/merge 6406bf3 [Mi-Cho-Coq] add a function to invoke a particular entrypoint 07 May 2021, 08:03:06 UTC
refs/merge-requests/101/head eb5a0b4 [build] sort and remove duplicates in the opam dependencies 22 June 2020, 13:14:49 UTC
back to top