| ccf5f78 | Colin González | 07 September 2020, 08:49:03 UTC | [dexter] proof for ep_setBaker_correct | 07 September 2020, 08:49:03 UTC |
| 0cad4fe | Colin González | 07 September 2020, 08:39:04 UTC | [dexter] proof for ep_default_correct | 07 September 2020, 08:39:04 UTC |
| 355f24e | Colin González | 01 September 2020, 14:39:35 UTC | [dexter] proof for ep_setManager_correct | 01 September 2020, 14:40:59 UTC |
| e3e28ca | Arvid Jakobsson | 01 September 2020, 08:17:25 UTC | [dexter] add version 6d1798cb of Dexter from branch develop https://gitlab.com/camlcase-dev/dexter/-/blob/6d1798cbb6c926db608a9ba473cc9f215b647b1f/morley/dexter.tz | 01 September 2020, 08:17:25 UTC |
| 3784c44 | Arvid Jakobsson | 31 August 2020, 11:06:38 UTC | [dexter] conform coq spec informal spec dated [August 26, 1:02 PM] Remove resolved TODOs from the specification: - the behavior of approve when allowance[spender] is undefined has been confirmed by james - as there is nothing that suggests that dexter verifies that token_bought <= token_pool, i'm removing that comment - the operations emitted by tokentotoken has been clarified by james | 31 August 2020, 11:08:48 UTC |
| 30f1ab4 | Arvid Jakobsson | 12 August 2020, 12:19:59 UTC | [dexter] conform coq spec informal spec dated [August 12, 2:16 PM] | 12 August 2020, 12:19:59 UTC |
| 99be45a | Arvid Jakobsson | 11 August 2020, 14:37:58 UTC | [dexter] add version ad6ddd89 of Dexter from branch develop, update | 11 August 2020, 14:37:58 UTC |
| 82aef18 | Arvid Jakobsson | 10 August 2020, 06:29:32 UTC | [dexter] Fixes to ep_approve due to Kristina | 11 August 2020, 14:01:02 UTC |
| 3a4fea4 | Arvid Jakobsson | 19 July 2020, 16:27:47 UTC | [dexter] Conform coq spec informal spec dated [July 17, 12:39 AM] | 11 August 2020, 14:00:35 UTC |
| fb6334e | Arvid Jakobsson | 17 July 2020, 08:52:17 UTC | [dexter] take a stab at proving derived properties from full spec | 17 July 2020, 08:52:17 UTC |
| bbefbf2 | Arvid Jakobsson | 16 July 2020, 20:25:01 UTC | [dexter] add tentative specification of tokenToToken entrypoint | 16 July 2020, 20:39:21 UTC |
| e4f128c | Arvid Jakobsson | 16 July 2020, 19:26:51 UTC | [dexter] conform coq spec informal spec dated [July 13, 10:31 AM] | 16 July 2020, 20:39:21 UTC |
| d377019 | Arvid Jakobsson | 10 July 2020, 15:57:53 UTC | [dexter] update contract to 26a6dd13 | 16 July 2020, 18:14:42 UTC |
| 92461d6 | Arvid Jakobsson | 09 July 2020, 14:12:12 UTC | Adapt proofs to simplified formulas from eval_precond | 09 July 2020, 14:12:12 UTC |
| 3f39afb | Arvid Jakobsson | 30 June 2020, 18:30:47 UTC | [dexter] Removing sender <> spender check in approve As per trail of bits security issue 6. | 09 July 2020, 14:01:50 UTC |
| d1ca600 | Arvid Jakobsson | 30 June 2020, 18:13:34 UTC | [dexter] Fix the spec for entrypoint approve - I had forgotten the allowance = current_allowance check - Added the case where there is no account for sender, as per the discussion with James in the informal spec | 09 July 2020, 14:01:50 UTC |
| 3410de9 | Arvid Jakobsson | 30 June 2020, 18:13:00 UTC | [dexter] add spec for updateTokenPool & updateTokenPoolInternal | 09 July 2020, 14:01:50 UTC |
| 38a5b2b | Arvid Jakobsson | 09 June 2020, 21:40:51 UTC | [dexter] add version 333cfb87 of dexter, update as follows From James: "There have been a few changes in the morley version to fix bugs. - The storage reorganized a bit so that the bigmap is at the top (pair (bigmap) ...) , that way we can still use the old POST big map rpc (just used in development with tezos-client, it is much easier, production uses the newer GET rpc which has a few more steps). The pair structure changed, the data is all the same. - There were one or two errors with transfer. to_ sending to owner instead of the other way around. init liquidity in addLiquidity was not setting the tokenPool. Fixed that." Also add some tactics for robustness: - use destruct_sto to destruct contract - use autofuel instead of "do X more_fuel; simpl". hopefully, this will be more robust." Also, this include the latest changes in updateTokenPool that fixes the issue brought up in the trail of bits security report. | 09 July 2020, 14:01:50 UTC |
| 8977774 | Colin González | 22 May 2020, 09:55:21 UTC | [dexter] prove ep_update_TokenPool_correct. | 09 July 2020, 14:01:50 UTC |
| c10441d | Colin González | 22 May 2020, 09:26:19 UTC | [dexter] prove ep_setBaker_correct. | 09 July 2020, 14:01:50 UTC |
| 2884b1f | Arvid Jakobsson | 27 May 2020, 09:27:01 UTC | [dexter] add the addLiquidity entrypoint definition | 09 July 2020, 14:01:50 UTC |
| 5e87ca2 | Arvid Jakobsson | 27 May 2020, 09:18:24 UTC | [dexter] add lqt_total to storage and update affected EPs | 09 July 2020, 14:01:50 UTC |
| 5d33722 | Arvid Jakobsson | 22 May 2020, 07:00:38 UTC | [dexter] replace iff w/ and in setBaker, default spec | 09 July 2020, 14:01:50 UTC |
| 011a574 | Arvid Jakobsson | 22 May 2020, 06:55:19 UTC | [dexter] use same semantics module in spec and verification | 09 July 2020, 14:01:50 UTC |
| 628284e | Arvid Jakobsson | 15 May 2020, 13:49:00 UTC | [dexter] boilerplate to verify main | 09 July 2020, 14:01:50 UTC |
| 7de8cc1 | Arvid Jakobsson | 15 May 2020, 13:14:41 UTC | [dexter] specify xtzToToken and tokenToXtz | 09 July 2020, 14:01:50 UTC |
| d03a220 | Arvid Jakobsson | 15 May 2020, 07:23:44 UTC | [dexter] specify removeLiquidity | 09 July 2020, 14:01:50 UTC |
| 9569a93 | Arvid Jakobsson | 13 May 2020, 15:02:05 UTC | parse wip | 09 July 2020, 14:01:50 UTC |
| b4d5be9 | Arvid Jakobsson | 13 May 2020, 14:55:07 UTC | [dexter] rebase on dev, spec addLiquidity entry point | 09 July 2020, 14:01:50 UTC |
| a0b95a7 | Arvid Jakobsson | 13 May 2020, 13:27:20 UTC | [dexter] specify ep_addLiquidity | 09 July 2020, 14:01:50 UTC |
| 72369ef | Arvid Jakobsson | 13 May 2020, 11:56:27 UTC | [dexter] add morley contract | 09 July 2020, 14:01:50 UTC |
| c07faad | Arvid Jakobsson | 13 May 2020, 11:56:10 UTC | [dexter] update contract definition from wip morley contract | 09 July 2020, 14:01:50 UTC |
| 4322bdd | Arvid Jakobsson | 12 May 2020, 07:41:45 UTC | [dexter] update parameter and main with new morley definition | 09 July 2020, 14:01:50 UTC |
| 7816d6a | Arvid Jakobsson | 11 May 2020, 14:10:56 UTC | [dexter] add wip spec for approve | 09 July 2020, 14:01:50 UTC |
| a1acfe1 | Arvid Jakobsson | 11 May 2020, 13:02:53 UTC | [dexter] use shorthands in parameter type declaration | 09 July 2020, 14:01:50 UTC |
| 0629ab7 | Arvid Jakobsson | 11 May 2020, 13:02:44 UTC | [dexter] clarify fuel comment | 09 July 2020, 14:01:50 UTC |
| 955be9f | Arvid Jakobsson | 11 May 2020, 12:18:10 UTC | [dexter] stubs for spec/def/verification of each entrypoint | 09 July 2020, 14:01:50 UTC |
| bc60f8d | Arvid Jakobsson | 11 May 2020, 10:02:24 UTC | [dexter] add setBaker formal specification | 09 July 2020, 14:01:50 UTC |
| 4f3ee7a | Arvid Jakobsson | 11 May 2020, 09:24:30 UTC | [dexter] add stubs for all entrypoints and main | 09 July 2020, 14:01:50 UTC |
| 34a310d | Arvid Jakobsson | 11 May 2020, 07:53:40 UTC | test | 09 July 2020, 14:01:50 UTC |
| 471b4e4 | Arvid Jakobsson | 11 May 2020, 06:40:04 UTC | rename | 09 July 2020, 14:01:50 UTC |
| 6471af0 | Arvid Jakobsson | 24 January 2020, 18:13:32 UTC | [dexter] Specify entrypoints vote | 09 July 2020, 14:01:50 UTC |
| d5004df | Arvid Jakobsson | 24 January 2020, 17:24:09 UTC | [dexter] Specify entrypoints xtzToToken and tokenToXtz | 09 July 2020, 14:01:50 UTC |
| cff25ae | Arvid Jakobsson | 24 January 2020, 15:54:57 UTC | [dexter] Specify entrypoint removeLiquidity | 09 July 2020, 14:01:50 UTC |
| 3aa08fb | Arvid Jakobsson | 23 January 2020, 16:04:15 UTC | [dexter] Specify baker election (provisional version) | 09 July 2020, 14:01:50 UTC |
| d2f943b | Arvid Jakobsson | 21 January 2020, 16:27:58 UTC | [dexter] Relational input-output specification of entrypoint add_liquidity | 09 July 2020, 14:01:50 UTC |
| abb65d2 | Arvid Jakobsson | 21 January 2020, 10:19:18 UTC | A more "classic relational" specification of the add_liquidity entrypoint | 09 July 2020, 14:01:50 UTC |
| 500c6dc | Arvid Jakobsson | 20 January 2020, 10:35:13 UTC | Monadic specification -- dead end? to handle errors, i would have to make the specicification monad very close to the error monad... then what is the point of the specificiation monad ? maybe more point if I rewrite it as a reader / writer. For the moment, i will rather try to make a more simple specification DSL and go from there. | 09 July 2020, 14:01:50 UTC |
| ccfd693 | 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. | 05 July 2020, 12:47:33 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 |
| 80978ee | Guillaume Claret | 16 November 2019, 13:28:16 UTC | [of_ocaml] Add imported syntax definition from the OCaml code | 18 April 2020, 12:03:12 UTC |
| fdfa10d | Raphaël Cauderlier | 04 December 2019, 20:50:34 UTC | [Michocoq] Remove superfluous functors | 18 April 2020, 12:03:12 UTC |
| ae11043 | Raphaël Cauderlier | 04 December 2019, 14:19:10 UTC | [Michocoq] Remove contract literals | 18 April 2020, 11:49:22 UTC |
| 5b40d03 | Raphaël Cauderlier | 18 April 2020, 11:40:18 UTC | [CI] fix shellcheck URL | 18 April 2020, 11:43:19 UTC |
| 3fb4ceb | Arvid Jakobsson | 10 March 2020, 14:23:46 UTC | [generic_multisig] Add CHAIN_ID to signature Related to #21 | 11 March 2020, 13:52:45 UTC |
| 00e403d | Raphaël Cauderlier | 13 February 2020, 17:07:39 UTC | [SC verif] Deposit contract | 13 February 2020, 17:07:39 UTC |
| 90abcb0 | Raphaël Cauderlier | 23 January 2020, 22:29:22 UTC | [build] Add missing dependency to ocamlbuild | 13 February 2020, 10:07:44 UTC |
| 9b308f4 | Raphaël Cauderlier | 12 February 2020, 13:15:58 UTC | [doc] slides for WTSC | 12 February 2020, 13:23:16 UTC |
| 949a7a4 | Raphaël Cauderlier | 12 February 2020, 13:15:36 UTC | [doc] slides of past talks | 12 February 2020, 13:23:16 UTC |
| a0ebbfd | Raphaël Cauderlier | 27 January 2020, 09:47:43 UTC | [doc] More explicit names for the talk directories | 27 January 2020, 09:48:13 UTC |
| f65e22e | Raphaël Cauderlier | 13 January 2020, 12:33:51 UTC | [doc] slides for the workshop at Cobra in Aarhus | 13 January 2020, 12:34:38 UTC |
| dc275c8 | Guillaume Claret | 04 December 2019, 09:27:10 UTC | Fix the install of the michocoq binary | 04 December 2019, 09:39:27 UTC |
| 9aa10a2 | Arvid Jakobsson | 29 November 2019, 14:39:11 UTC | [ott] remove the original michocott formalization | 29 November 2019, 14:39:11 UTC |
| ceb487e | Raphaël Cauderlier | 11 September 2019, 07:54:20 UTC | Michocott: Update michelson.ott to ease documentation generation | 29 November 2019, 13:41:28 UTC |
| 8733671 | Basile Pesin | 31 May 2019, 13:43:15 UTC | Corrected the 'a's that were changed in 'ty2's | 29 November 2019, 13:41:24 UTC |
| 3098cf5 | Basile Pesin | 30 May 2019, 17:27:17 UTC | All the way to extraction | 29 November 2019, 13:41:11 UTC |
| f2939c1 | Basile Pesin | 30 May 2019, 16:01:51 UTC | Removed ambiguity by adding explicit annotations | 29 November 2019, 13:40:31 UTC |
| eb1c38f | Basile Pesin | 29 May 2019, 23:02:55 UTC | Every rule is good with doc but multiple parses on compilation to coq for list set map | 29 November 2019, 13:40:31 UTC |
| 609a9c5 | Basile Pesin | 29 May 2019, 19:06:58 UTC | ott spec OK except for list and map | 29 November 2019, 13:40:31 UTC |
| 218ee17 | Basile Pesin | 29 May 2019, 13:09:06 UTC | Changed symbol for typing to '::' and symbol for cons to ':' in michelson_typing | 29 November 2019, 13:40:31 UTC |
