0ff13fc | Arvid Jakobsson | 02 March 2021, 17:52:07 UTC | Dexter2/Proof: addLiquidity | 05 March 2021, 12:31:21 UTC |
011424e | Arvid Jakobsson | 02 March 2021, 17:52:42 UTC | Dexter2/Spec: order of operations in addLiquidity | 05 March 2021, 12:31:21 UTC |
f16dfe4 | Arvid Jakobsson | 03 March 2021, 16:34:02 UTC | Dexter2/Lemmas: simplify Spec_Nceiling_mod & Spec_Nceiling_rem | 05 March 2021, 12:31:21 UTC |
d583241 | Arvid Jakobsson | 03 March 2021, 16:33:44 UTC | Dexter2/Lemmas: lemmas for addLiquidity | 05 March 2021, 12:31:21 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 |
5d3d290 | Arvid Jakobsson | 18 June 2020, 13:35:44 UTC | [michocoq] Avoid using `Check` for unit tests Writing unit tests as `Check (eq_refl : f x = y).` works but dumps unnecessary output on stdout that can be confusing when compiling the project. The equivalent `Goal (f x = y). reflexivity. Qed.` does the same check without producing any output. | 19 June 2020, 20:08:22 UTC |
9eaab97 | Raphaël Cauderlier | 19 June 2020, 13:38:54 UTC | [michocoq] Fix the behaviour of `get_entrypoint_opt (Some "%default")` | 19 June 2020, 20:08:15 UTC |
2e8d5a3 | Raphaël Cauderlier | 16 December 2019, 08:18:47 UTC | [optimizer] Define and certify a Michelson optimizer The optimizer was initially designed for the backend of the Albert compiler, it has been slightly generalized and certified. The main theorem is the last one in file typed_optimizer.v: If the untyped instruction sequence i can be typechecked from stack type A to stack type B and then run successfully on stack sA, then (optimizer.optimize i) can also be typechecked from stack type A to stack type B and run successfully on stack sA yielding the same result. | 19 May 2020, 13:55:03 UTC |
11de7d7 | Raphaël Cauderlier | 10 May 2020, 14:48:32 UTC | Untyped macros in `instruction` | 19 May 2020, 13:55:02 UTC |
2415691 | Raphaël Cauderlier | 26 April 2020, 20:07:01 UTC | [michocoq] Simplification of tez.v This uses `Bool.Is_true (negb ...)` instead of `... = false` in the definition of the `mutez` type which simplifies a bit reasoning about the implementation of mutez. | 14 May 2020, 19:39:36 UTC |
93912f6 | Raphaël Cauderlier | 21 December 2019, 22:12:06 UTC | [michocoq] Prove second half of typer correctness This completes the correctness proof of the typer in Optimized mode. Before this, only the typed -> untyped -> typed round-trip was certified. | 14 May 2020, 19:39:36 UTC |
daec052 | Raphaël Cauderlier | 25 April 2020, 13:33:49 UTC | [michocoq] Typing and untyping mode (Readable or Optimized) Since the introduction of timestamp literals, the typer is not injective anymore so the converse of untyper.untype_type is not true. By introducing a typing and an untyping mode, we get back injectivity at least in optimized mode. | 14 May 2020, 19:39:36 UTC |
8591d76 | Raphaël Cauderlier | 21 December 2019, 21:53:16 UTC | [michocoq] Fix a bug in the typer Type-checking a mutez literal now fails in case of overflow. | 14 May 2020, 19:39:36 UTC |
ac659ab | Raphaël Cauderlier | 07 May 2020, 19:22:44 UTC | [build|ignore] Also ignore the cache of the `nia` tactic | 14 May 2020, 19:39:35 UTC |
34a1022 | Raphaël Cauderlier | 05 December 2019, 11:08:19 UTC | [michocoq] Use frienly notations in all verified scripts | 14 May 2020, 19:37:32 UTC |
5bd8859 | Raphaël Cauderlier | 03 December 2019, 12:19:06 UTC | [michocoq] Add a distinction between instructions and instruction sequences | 14 May 2020, 19:37:32 UTC |
980a820 | Raphaël Cauderlier | 29 November 2019, 14:27:04 UTC | [michocoq] Also separate IF_ and LOOP_ instructions from the other ones | 07 May 2020, 21:55:22 UTC |
95b18b8 | Raphaël Cauderlier | 17 March 2020, 17:40:39 UTC | [michocoq] Stratify opcodes and instructions. We call opcodes the instructions that do not take subprograms as argument nor have special treatment in the type-checker or evaluator. Most of the instructions in Michelson fall into this category, putting them aside makes the number of constructors of the instruction ASTs much smaller which is needed when reasoning on the syntax. In particular, many optimisations at the Michelson level require to reason about several terms in these ASTs by nesting destructs which was not tractable with more than 80 constructors. | 07 May 2020, 21:55:12 UTC |
ab60300 | Raphaël Cauderlier | 07 May 2020, 21:15:25 UTC | Remove syntax_equiv.v This is incomplete and broken. | 07 May 2020, 21:54:55 UTC |
ba48cdf | Raphaël Cauderlier | 24 January 2020, 10:26:23 UTC | Remove the return_to_sender contract This is a duplicate of the boomerang contract. | 07 May 2020, 21:54:42 UTC |
30ec384 | Guillaume Claret | 10 March 2020, 21:16:49 UTC | [Michocoq] Add parsing of timestamps | 18 April 2020, 12:34:45 UTC |
75ba1ed | Raphaël Cauderlier | 13 March 2020, 16:48:52 UTC | [CI|Tests] Run the tests in the CI | 18 April 2020, 12:34:45 UTC |
b6d740a | Raphaël Cauderlier | 13 March 2020, 16:46:47 UTC | [Build|Tests]: add a build-test target for Opam | 18 April 2020, 12:34:45 UTC |
2eeac09 | Raphaël Cauderlier | 13 March 2020, 16:35:42 UTC | [Tests] Regression traces | 18 April 2020, 12:34:44 UTC |
123c097 | Raphaël Cauderlier | 13 March 2020, 16:48:13 UTC | [Tests] Regression testing Tests are run with `make test` and regression traces are reset with `make RESET_REGRESSION=true test`. | 18 April 2020, 12:34:44 UTC |
3ae9aaf | Raphaël Cauderlier | 13 March 2020, 15:54:06 UTC | [Tests] Update the test suite | 18 April 2020, 12:34:44 UTC |
1c4fb62 | Raphaël Cauderlier | 16 July 2019, 08:57:17 UTC | [Michocoq] Formalize %-annotations and entrypoints Annotations are still ignored at lexing time but the semantically meaningful ones are supported in the untyped syntax. | 18 April 2020, 12:34:44 UTC |
c578eba | Guillaume Claret | 27 February 2020, 17:45:18 UTC | [build] Add support for Coq 8.11 | 18 April 2020, 12:03:13 UTC |
94071da | Guillaume Claret | 06 December 2019, 18:59:32 UTC | [of_ocaml] Add a README for the of_ocaml folder | 18 April 2020, 12:03:13 UTC |
a35ea8c | Guillaume Claret | 06 December 2019, 18:04:18 UTC | [of_ocaml] Beginning of injection of the syntax of Mi-Cho-Coq to OCaml | 18 April 2020, 12:03:13 UTC |
41fed52 | Guillaume Claret | 03 December 2019, 15:35:40 UTC | [of_ocaml] Bijection for the comparable types | 18 April 2020, 12:03:13 UTC |
e94f138 | Guillaume Claret | 02 December 2019, 14:54:09 UTC | [of_ocaml] Explicit definition of coq_to_ocaml_typ | 18 April 2020, 12:03:13 UTC |
bbb0057 | Guillaume Claret | 16 November 2019, 16:28:49 UTC | [of_ocaml] Extend one side on the equivalence of the types with comparable types | 18 April 2020, 12:03:13 UTC |
e432e03 | Guillaume Claret | 16 November 2019, 13:29:15 UTC | [of_ocaml] Add one side of the equivalence with the Coq AST | 18 April 2020, 12:03:12 UTC |