| c944fe4 | Guillaume Claret | 12 March 2021, 10:37:39 UTC | WIP | 12 March 2021, 14:06:33 UTC |
| 31d8f0b | Yann Regis-Gianas | 03 March 2021, 13:45:27 UTC | Proof of correctness for TokenToXtz Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 10 March 2021, 16:40:19 UTC |
| 3b5fb39 | Yann Regis-Gianas | 09 March 2021, 08:07:35 UTC | More helper lemmas about mutez comparison Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 10 March 2021, 16:40:14 UTC |
| 94c4e4d | Guillaume Claret | 08 March 2021, 20:16:48 UTC | Dexter2/Proof: prove tokenToToken | 10 March 2021, 15:34:57 UTC |
| bf32c6a | Arvid Jakobsson | 09 March 2021, 20:23:53 UTC | Dexter2/Lemmas: some utilities for tokenToToken | 10 March 2021, 15:34:57 UTC |
| 0d4f64e | Arvid Jakobsson | 09 March 2021, 18:18:42 UTC | Dexter2/Util: Fix fold_mutez_goal | 10 March 2021, 15:34:57 UTC |
| 54c0037 | Arvid Jakobsson | 10 March 2021, 15:31:30 UTC | Revert "Dexter2/Spec: debit before credit in ep_tokenToXtz" This reverts commit 562b501a99683b870f9f221de844bfc2d1a40a78. I made this specification change by error. It was the implementation that should've been changed, and that was done in : 5d23761 * Importing Dexter2 contracts wip#22a69ba | 10 March 2021, 15:31:34 UTC |
| e66a03e | Arvid Jakobsson | 09 March 2021, 20:27:21 UTC | Importing Dexter2 contracts wip#adf8140 | 09 March 2021, 20:27:21 UTC |
| fd831d7 | Arvid Jakobsson | 09 March 2021, 11:31:24 UTC | Dexter2: Show the parsed and hand-written definitions equal | 09 March 2021, 17:54:41 UTC |
| 5d23761 | Arvid Jakobsson | 09 March 2021, 17:38:56 UTC | Importing Dexter2 contracts wip#22a69ba | 09 March 2021, 17:38:56 UTC |
| 562b501 | Arvid Jakobsson | 09 March 2021, 17:19:59 UTC | Dexter2/Spec: debit before credit in ep_tokenToXtz Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 09 March 2021, 17:19:59 UTC |
| 59555da | Yann Regis-Gianas | 05 March 2021, 10:10:33 UTC | Dexter2/Proof: Verify XtzToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 09 March 2021, 10:24:30 UTC |
| 0d73918 | Arvid Jakobsson | 09 March 2021, 09:59:35 UTC | Dexter2/Util: Tactics for XtzToToken | 09 March 2021, 10:24:30 UTC |
| 390a74e | Yann Regis-Gianas | 08 March 2021, 13:32:16 UTC | Dexter2/Util: Add new lemmas about comparisons Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 09 March 2021, 10:24:30 UTC |
| ea2c090 | Yann Regis-Gianas | 08 March 2021, 10:11:49 UTC | Dexter2/Spec: Update Dexter specification to account for division by zero Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 09 March 2021, 10:24:30 UTC |
| e6a4e9e | Arvid Jakobsson | 09 March 2021, 10:23:31 UTC | fixup! Dexter2/Proof: addLiquidity | 09 March 2021, 10:23:31 UTC |
| 728c8c4 | Arvid Jakobsson | 09 March 2021, 10:07:09 UTC | TMP: do not merge, reduce parallelism | 09 March 2021, 10:07:09 UTC |
| 58f6197 | Arvid Jakobsson | 08 March 2021, 13:44:55 UTC | Dexter2: Coq 8.8.0 fixes | 08 March 2021, 18:59:10 UTC |
| 2759b39 | Arvid Jakobsson | 04 March 2021, 17:44:11 UTC | Dexter2/Proofs: dirty proof for removeLiquidity | 08 March 2021, 18:59:10 UTC |
| b920e9f | Arvid Jakobsson | 04 March 2021, 17:43:52 UTC | Dexter2/Lemmas: add lemmas from removeLiquidity | 08 March 2021, 18:59:10 UTC |
| 1fa7276 | Arvid Jakobsson | 04 March 2021, 17:41:28 UTC | Dexter2/Definition: evaluate in self_type Hopefully, this will lead to less need for unfolding. | 08 March 2021, 18:59:10 UTC |
| 09284b3 | Arvid Jakobsson | 02 March 2021, 17:52:07 UTC | Dexter2/Proof: addLiquidity | 08 March 2021, 18:59:10 UTC |
| d1babf2 | Arvid Jakobsson | 02 March 2021, 17:52:42 UTC | Dexter2/Spec: order of operations in addLiquidity | 08 March 2021, 18:59:10 UTC |
| 0a36a4e | Arvid Jakobsson | 03 March 2021, 16:34:02 UTC | Dexter2/Lemmas: simplify Spec_Nceiling_mod & Spec_Nceiling_rem | 08 March 2021, 18:59:10 UTC |
| f2aeade | Arvid Jakobsson | 03 March 2021, 16:33:44 UTC | Dexter2/Lemmas: lemmas for addLiquidity | 08 March 2021, 18:59:10 UTC |
| b411636 | Colin González | 05 March 2021, 14:06:39 UTC | Dexter2/Proof: Proof for updateTokenPool | 08 March 2021, 18:03:48 UTC |
| 9264a80 | Colin González | 05 March 2021, 13:38:00 UTC | Dexter2/Proof: Proof for updateTokenPoolInternal | 08 March 2021, 18:03:48 UTC |
| 27ec437 | Colin González | 05 March 2021, 13:14:06 UTC | Dexter2/Proof: Proof setLqtAddresss correct | 08 March 2021, 18:03:48 UTC |
| e5f0e42 | Colin González | 04 March 2021, 10:13:27 UTC | Dexter2/Proof: Proof for setManager correct. | 08 March 2021, 18:03:48 UTC |
| ae27612 | Colin González | 04 March 2021, 09:40:26 UTC | Dexter2/Proof: Proof of correction for setBaker | 08 March 2021, 18:03:48 UTC |
| 7ddd228 | Colin González | 26 February 2021, 15:04:31 UTC | Dexter2/Proof: proof ep_default correct | 08 March 2021, 18:03:48 UTC |
| da03549 | Arvid Jakobsson | 08 March 2021, 15:56:49 UTC | TMP: only run CI for Coq 8.11 | 08 March 2021, 17:52:27 UTC |
| 5370d2f | Yann Regis-Gianas | 03 March 2021, 13:20:01 UTC | Make mutez more readable by keeping the proof implicit Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 05 March 2021, 12:50:43 UTC |
| 1ac3607 | Arvid Jakobsson | 05 March 2021, 11:57:29 UTC | Dexter2/Spec: updates in updateTokenPool, setLqtAddress - updateTokenPool: remove unnecessary `param = tt` check, relic from Dexter1 spec - updateTokenPool: check `sender = source` - setLqtAddress: change so that the lqt address can only be changed from tz1 zero | 05 March 2021, 11:57:29 UTC |
| 5364d48 | Arvid Jakobsson | 05 March 2021, 11:07:34 UTC | Dexter2/Lemmas: Logic.False dexter_util.v fixes | 05 March 2021, 11:11:09 UTC |
| e958d3f | Arvid Jakobsson | 04 March 2021, 17:57:37 UTC | Importing Dexter2 contracts d5ec303 | 04 March 2021, 18:03:58 UTC |
| 030768c | Arvid Jakobsson | 02 March 2021, 17:52:29 UTC | Dexter2: add step tactic | 03 March 2021, 15:14:00 UTC |
| 830db17 | Arvid Jakobsson | 03 March 2021, 15:13:13 UTC | Dexter/Lemmas: replace tez.compare with compare mutez | 03 March 2021, 15:14:00 UTC |
| a777889 | Arvid Jakobsson | 03 March 2021, 14:39:52 UTC | Dexter/Lemmas: add comparison_to_int_tez_compare_le_zero | 03 March 2021, 14:40:42 UTC |
| b77dd82 | Arvid Jakobsson | 02 March 2021, 19:44:22 UTC | Dexter2: Weird Coq 8.11.2 fixes | 02 March 2021, 19:44:22 UTC |
| 3ffa9a0 | Tom Jack | 26 February 2021, 14:00:29 UTC | Dexter contract: swap op order in token_to_token, recompile | 02 March 2021, 19:44:17 UTC |
| 0c78577 | Tom Jack | 26 February 2021, 13:59:55 UTC | Dexter contract: (noop) remove TODO, add some comments | 02 March 2021, 19:44:17 UTC |
| 9b5bb14 | Tom Jack | 24 February 2021, 23:01:47 UTC | Add back #if FA2 in dexter_fa12lqt.mligo | 02 March 2021, 19:44:17 UTC |
| 022b3c4 | Arvid Jakobsson | 24 February 2021, 19:25:54 UTC | One file per entrypoint | 02 March 2021, 19:44:17 UTC |
| 45171ea | Arvid Jakobsson | 24 February 2021, 12:23:10 UTC | Move Dexter Michelson/mligo contracts to src/contracts/tomjack | 02 March 2021, 19:44:17 UTC |
| 51ef246 | Arvid Jakobsson | 24 February 2021, 12:11:30 UTC | Defunctorize Dexter | 02 March 2021, 19:44:17 UTC |
| 9218b58 | Arvid Jakobsson | 23 February 2021, 18:47:18 UTC | Setup proof boilerplate. | 02 March 2021, 18:13:44 UTC |
| c1a9c22 | Arvid Jakobsson | 23 February 2021, 14:12:00 UTC | Refactor spec utilities | 02 March 2021, 18:13:44 UTC |
| e1ea8aa | Tom Jack | 16 February 2021, 13:59:37 UTC | Use records for fa12/lqt | 02 March 2021, 18:13:44 UTC |
| 737daea | Tom Jack | 16 February 2021, 10:57:51 UTC | Remove more irrelevant #ifdefs | 02 March 2021, 18:13:44 UTC |
| 3dcdb9f | Tom Jack | 16 February 2021, 09:51:41 UTC | Update code & spec | 02 March 2021, 18:13:44 UTC |
| 1046106 | Tom Jack | 12 February 2021, 20:13:12 UTC | fix mintOrBurn case & force layout | 02 March 2021, 18:13:44 UTC |
| 57b5217 | Tom Jack | 12 February 2021, 20:06:06 UTC | Revert "Add %safeApprove to FA1.2 under #define" This reverts commit baf7a1ea740114b512d50793ce65fd3da22605e0. | 02 March 2021, 18:13:44 UTC |
| 935ca71 | Tom Jack | 12 February 2021, 18:16:02 UTC | Add %safeApprove to FA1.2 under #define | 02 March 2021, 18:13:44 UTC |
| ece64fa | Tom Jack | 12 February 2021, 18:10:04 UTC | Rewrite FA1.2 draft | 02 March 2021, 18:13:44 UTC |
| 106a809 | Tom Jack | 09 February 2021, 21:36:15 UTC | Update dexter_string with draft, get to first broken proof | 02 March 2021, 18:13:44 UTC |
| f3c2835 | Tom Jack | 09 February 2021, 18:40:38 UTC | Fix wrong .tz | 02 March 2021, 18:13:44 UTC |
| 1683e98 | Tom Jack | 09 February 2021, 18:33:21 UTC | Add draft dexter_fa12lqt | 02 March 2021, 18:13:44 UTC |
| b1fe58e | Raphaël Cauderlier | 06 February 2021, 22:41:46 UTC | 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. | 02 March 2021, 18:13:44 UTC |
| 16eec8a | Raphaël Cauderlier | 06 February 2021, 22:05:50 UTC | Dexter DFS compat: assert that `to` and `owner` args are always implicit accounts In order to reduce the attack surface of Dexter in the presence of both BFS and DFS calls, we add assertions that guarantee that: - Dexter is not called by a smart-contract so no BFS operations can be injected before the operations emitted by Dexter. This is checked by (SOURCE = SENDER) which can never hold in internal transactions. - uncontrolled addresses (the `to` and `owner` parameters) are prevented to do any call (DFS or BFS) by requesting them to be implicit accounts. There is unfortunately no instruction in Michelson to check that an address is implicit (see https://gitlab.com/nomadic-labs/tezos/-/merge_requests/93) but we know that the transaction source is always implicit (since Babylon) so we use the over approximation (to = SOURCE) and (owner = SOURCE). | 02 March 2021, 18:13:44 UTC |
| 027833e | Raphaël Cauderlier | 07 February 2021, 15:48:49 UTC | Debug: output the Dexter script on stdout A very small edit of the script is still needed to: - remove some garbage before and after the script - replace "" by " - ask Emacs to reindent everything | 02 March 2021, 18:13:44 UTC |
| f47c9a2 | Raphaël Cauderlier | 07 February 2021, 15:47:56 UTC | Dexter string: Add newlines to help Emacs indent the script correctly | 02 March 2021, 18:13:44 UTC |
| 50228cc | Raphaël Cauderlier | 07 February 2021, 15:46:00 UTC | Dexter string: Edo compat In Edo FAILWITH cannot raise a big map anymore. This commit adds UNIT before the FAILWITHs that don't typecheck in Edo. | 02 March 2021, 18:13:44 UTC |
| 569ef67 | Arvid Jakobsson | 10 October 2020, 14:23:15 UTC | [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 | 02 March 2021, 18:13:44 UTC |
| 42fb2cb | Arvid Jakobsson | 10 October 2020, 14:21:50 UTC | [dexter] add utility lemmas for Dexter | 02 March 2021, 18:13:44 UTC |
| b0a8b04 | Arvid Jakobsson | 09 October 2020, 16:44:52 UTC | [mi-cho-coq] add compare_gt_lt to comparable.v | 02 March 2021, 18:13:42 UTC |
| 2508590 | Arvid Jakobsson | 09 October 2020, 16:17:51 UTC | [mi-cho-coq] move fold_eval_precond to semantics.v | 02 March 2021, 17:57:31 UTC |
| 90a0d08 | Arvid Jakobsson | 21 September 2020, 19:36:05 UTC | [mi-cho-coq] prove injectivity of tez.to_Z | 02 March 2021, 17:57:31 UTC |
| 25510be | Arvid Jakobsson | 18 September 2020, 13:30:41 UTC | [mi-cho-coq] prove lower bound on tez.to_Z | 02 March 2021, 17:57:31 UTC |
| fac88a2 | Yann Regis-Gianas | 02 March 2021, 16:36:26 UTC | Avoid parsing several times in main Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 02 March 2021, 16:36:26 UTC |
| 762928b | Michael J. Klein | 27 January 2021, 23:24:44 UTC | cleanup, add case_compare_Eq, add key descriptions | 02 February 2021, 18:09:35 UTC |
| 45b7c5d | Michael J. Klein | 10 January 2021, 23:22:17 UTC | add tez vesting contract source add vesting_tez coq definition, add _spec and _correct proof sans details for vesting wip: backup before rebasing on dev WIP: update to dev improvements fix spec, finish proof, first pass cleanup add vesting_tez.v to README.org rebase readme to dev add comparison_to_int_leb for N, IT_eq_iff, and simplification for to_flush constraints refactor spec, begin relocating utils refactor and reorganize distribute lemmas and cleanup move contract definition into vesting_tez_string.v, using match goal to minimize differences make vesting_tez_string.v easier to diff with vesting_tez.v | 02 February 2021, 18:09:35 UTC |
| b392c47 | Michael J. Klein | 10 January 2021, 23:08:03 UTC | add _opam to .gitignore, add lemmas and utils for vesting_tez.v | 02 February 2021, 18:09:35 UTC |
| 4c83fa8 | Raphaël Cauderlier | 15 September 2020, 21:49:43 UTC | [michocoq] Enforce concrete maps and big maps to be sorted by construction Solves #28. | 19 November 2020, 13:19:49 UTC |
| fe8c6f0 | Raphaël Cauderlier | 24 August 2020, 20:44:04 UTC | [michocoq] Enforce ordering of concrete sets | 19 November 2020, 13:15:43 UTC |
| 1df3192 | Raphaël Cauderlier | 24 August 2020, 20:11:30 UTC | [michocoq] Use simple_comparable_data to simplify concrete_data | 19 November 2020, 13:15:43 UTC |
| 760fbfe | Raphaël Cauderlier | 24 August 2020, 19:41:20 UTC | [michocoq] Reverse dependency between syntax.v and comparable.v Allowing syntax to depend on comparable is needed to talk about the compare function when defining the syntax of sets and maps. | 19 November 2020, 13:15:43 UTC |
| d89caaf | Raphaël Cauderlier | 24 August 2020, 19:38:52 UTC | [michocoq|extraction] fix a typo | 19 November 2020, 13:15:43 UTC |
| 5a01c81 | Michael J. Klein | 17 November 2020, 22:52:09 UTC | add constraint "coq" { < "8.12.0" } | 17 November 2020, 22:52:09 UTC |
| a4d37fa | Raphaël Cauderlier | 24 August 2020, 10:33:05 UTC | [Michocoq] Allow FAILWITH in LOOP, LOOP_LEFT, and ITER Fixes #27. | 17 September 2020, 11:45:12 UTC |
| 5796046 | Raphaël Cauderlier | 31 May 2020, 13:08:41 UTC | 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. | 15 September 2020, 12:28:46 UTC |
| 1f739de | Raphaël Cauderlier | 08 July 2020, 08:49:35 UTC | [Michocoq] Improve checking time of the SLC proof On my machine, it is now checked in 16s instead of 56s. | 29 August 2020, 15:21:54 UTC |
| 02388f8 | Raphaël Cauderlier | 22 April 2020, 14:00:01 UTC | [michocoq] Fix typing of chain_id constants (bytes instead of strings) | 24 August 2020, 12:51:55 UTC |
| d7cd730 | Raphaël Cauderlier | 16 April 2020, 09:43:55 UTC | [michocoq] Foramlise byte sequences | 24 August 2020, 12:51:55 UTC |
| 5bf0775 | Raphaël Cauderlier | 15 April 2020, 13:43:50 UTC | [michocoq] Fix the semantics of EDIV | 24 August 2020, 12:51:55 UTC |
| 83d1e37 | Raphaël Cauderlier | 15 April 2020, 14:01:33 UTC | [michocoq] Big map litterals | 24 August 2020, 12:51:55 UTC |
| 03244f9 | Raphaël Cauderlier | 14 April 2020, 20:29:53 UTC | [michocoq] Add missing case for the `chain_id` type in the Micheline2michelson parser | 24 August 2020, 12:51:55 UTC |
| 411a3d3 | Raphaël Cauderlier | 14 April 2020, 20:13:21 UTC | [michocoq] Add the missing case AND :: int : nat : 'S -> nat : 'S | 24 August 2020, 12:51:55 UTC |
| 13b317b | Raphaël Cauderlier | 08 April 2020, 10:10:55 UTC | [michocoq] Formalize the relation between key_hash, addresses and contracts | 24 August 2020, 12:51:55 UTC |
| 99b67eb | Raphaël Cauderlier | 08 April 2020, 10:02:49 UTC | [michocoq] remove an unused file | 24 August 2020, 12:51:55 UTC |
| 3ffee65 | Raphaël Cauderlier | 24 August 2020, 12:01:25 UTC | [SLC] remove unused imports | 24 August 2020, 12:51:54 UTC |
| c8a57c8 | Raphaël Cauderlier | 17 July 2020, 12:04:38 UTC | [Optimizer] Optimize `PAIR; UNPAIR` | 17 July 2020, 12:05:04 UTC |
| a403a4f | Raphaël Cauderlier | 16 July 2020, 15:19:10 UTC | Optimize `DIP n {}` | 16 July 2020, 15:19:10 UTC |
| 55af1d7 | Raphaël Cauderlier | 06 July 2020, 19:58:50 UTC | [Michocoq] Improve doc and arg names for precond_iter_bounded | 07 July 2020, 08:25:41 UTC |
| 12ee2ad | Raphaël Cauderlier | 16 June 2020, 13:12:01 UTC | [SLC] fuel minimization | 07 July 2020, 08:25:41 UTC |
| b6580c5 | Raphaël Cauderlier | 09 June 2020, 14:07:28 UTC | [michocoq] Fix curly-brace wrapping of macros | 07 July 2020, 08:25:41 UTC |
| 8cdd957 | Arvid Jakobsson | 29 November 2019, 14:36:45 UTC | [SLC] Proof of the Spending Limit Contract This is joint work with Zaynah Dargaye <zaynah.dargaye@nomadic-labs.com>. See https://blog.nomadic-labs.com/formally-verifying-a-critical-smart-contract.html | 07 July 2020, 08:25:41 UTC |
| 98cd2c9 | Raphaël Cauderlier | 10 March 2020, 15:16:23 UTC | Add a lemma precond_iter on precond for ITER | 06 July 2020, 19:17:24 UTC |
| 50b5400 | Raphaël Cauderlier | 18 June 2020, 20:27:29 UTC | [michocoq] Propagation of annotations | 22 June 2020, 09:30:53 UTC |
| 83f6208 | Arvid Jakobsson | 18 June 2020, 13:35:44 UTC | [michocoq] WIP lexing and parsing of micheline annotations This does not compile because the definition of the syntax of Micheline nodes has been changed without changing the Micheline pretty-printer nor the converter from and to Michelson. | 22 June 2020, 09:30:36 UTC |
