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 |