| 24e1381 | Arvid Jakobsson | 09 October 2020, 13:09:26 UTC | [dexter] clean up lemmas wip 2 wip 3 temp | 09 October 2020, 16:45:35 UTC |
| 5bd5324 | Arvid Jakobsson | 09 October 2020, 16:44:52 UTC | [mi-cho-coq] add compare_gt_lt to comparable.v | 09 October 2020, 16:45:29 UTC |
| f5addb1 | Arvid Jakobsson | 09 October 2020, 16:17:51 UTC | [mi-cho-coq] move fold_eval_precond to semantics.v | 09 October 2020, 16:45:29 UTC |
| 3a640c9 | Arvid Jakobsson | 28 September 2020, 21:46:43 UTC | [dexter] update proof for exchange entrypoints | 28 September 2020, 21:48:12 UTC |
| e27ce6c | Arvid Jakobsson | 28 September 2020, 21:46:28 UTC | [dexter] update spec exchange entrypoints | 28 September 2020, 21:48:12 UTC |
| a3ba9dc | Arvid Jakobsson | 28 September 2020, 17:12:59 UTC | [dexter] refactorise proof of removeLiquidity | 28 September 2020, 21:48:12 UTC |
| f8a1dce | Arvid Jakobsson | 28 September 2020, 16:40:15 UTC | [dexter] update spec and proofs for addLiquidity | 28 September 2020, 21:48:12 UTC |
| f00a1db | Arvid Jakobsson | 28 September 2020, 13:06:35 UTC | [dexter] update contract to 4e24123 | 28 September 2020, 21:48:12 UTC |
| 8a2402e | Arvid Jakobsson | 28 September 2020, 09:52:25 UTC | [dexter] Prove ep_[tokenToXtz|xtzToToken|tokenToToken]_correct | 28 September 2020, 13:12:58 UTC |
| 38efb61 | Arvid Jakobsson | 28 September 2020, 09:31:19 UTC | [dexter] Add and re-organize lemmas | 28 September 2020, 13:12:58 UTC |
| 2bdaa67 | Arvid Jakobsson | 28 September 2020, 09:00:09 UTC | [dexter] Fix spec for ep_tokenToXtz, ep_xtzToToken and ep_tokenToToken | 28 September 2020, 13:12:58 UTC |
| b459984 | Arvid Jakobsson | 25 September 2020, 16:25:10 UTC | [dexter] prove removeLiquidity_correct | 28 September 2020, 13:12:58 UTC |
| 532a73f | Arvid Jakobsson | 25 September 2020, 12:46:16 UTC | [dexter] fix removeLqt specification Errors fixed in the formalization w.r.t. informal specification: - the allowance was never updated in set_allowance - allowance check should be performed in owners account - allowance check should fail if the owner has no allowances for owner - order of emitted operations - require that 0 < lqt_burned <= lqt_total | 28 September 2020, 13:12:58 UTC |
| b7e9a40 | Arvid Jakobsson | 25 September 2020, 16:24:56 UTC | [dexter] refactorise addLiquidity_correct | 28 September 2020, 13:12:58 UTC |
| b029a55 | Arvid Jakobsson | 22 September 2020, 09:24:31 UTC | [dexter] prove ep_approve_correct | 28 September 2020, 13:12:58 UTC |
| 04e1d5a | Arvid Jakobsson | 22 September 2020, 09:20:41 UTC | [dexter] move up all auxiliary lemmas | 28 September 2020, 13:12:58 UTC |
| 67a04e1 | Arvid Jakobsson | 22 September 2020, 08:27:47 UTC | [dexter] prove cmp_mutez_lt_zero | 28 September 2020, 13:12:58 UTC |
| b070580 | Arvid Jakobsson | 18 September 2020, 08:59:56 UTC | [dexter] prove ep_addLiquidity_correct | 28 September 2020, 13:12:58 UTC |
| 0ec93d3 | Arvid Jakobsson | 21 September 2020, 19:36:05 UTC | [dexter] prove injectivity of tez.to_Z | 28 September 2020, 13:12:58 UTC |
| 9c3387f | Arvid Jakobsson | 18 September 2020, 13:30:41 UTC | [dexter] prove lower bound on tez.to_Z | 28 September 2020, 13:12:58 UTC |
| 3660a5a | Colin González | 09 September 2020, 12:29:17 UTC | [dexter] proof for ep_updateTokenPoolInternal_correct | 28 September 2020, 13:12:58 UTC |
| 9b9796d | Colin González | 09 September 2020, 10:22:46 UTC | [dexter] proof for ep_updateTokenPool_correct | 28 September 2020, 13:12:58 UTC |
| bed2d35 | Arvid Jakobsson | 25 September 2020, 13:42:39 UTC | [dexter] refactor proofs for default, setBaker, setManager | 28 September 2020, 13:12:58 UTC |
| 8b0671c | Colin González | 09 September 2020, 14:22:04 UTC | [dexter] move generic lemmas out of the entry_points section | 28 September 2020, 13:12:58 UTC |
| 84e78b1 | Arvid Jakobsson | 25 September 2020, 13:46:25 UTC | [dexter] update contract to 05a3088 | 28 September 2020, 13:12:58 UTC |
| 36e8d88 | Arvid Jakobsson | 23 September 2020, 13:08:27 UTC | [dexter] update contract to 24e701a Fixes problem deadline checks | 28 September 2020, 13:12:58 UTC |
| 4ed9363 | Arvid Jakobsson | 22 September 2020, 07:53:49 UTC | [dexter] fix spec: no /0 in remLqt, tokenToXtz, tokenToToken | 28 September 2020, 13:12:58 UTC |
| 4e95dc3 | Arvid Jakobsson | 22 September 2020, 07:29:20 UTC | [dexter] fix spec: tokenToToken requires min_tokens_bought <> 0 | 28 September 2020, 13:12:58 UTC |
| 4cef434 | Arvid Jakobsson | 22 September 2020, 07:27:24 UTC | [dexter] fix spec: tokenToToken does not require that to exists | 28 September 2020, 13:12:58 UTC |
| 0dcfb18 | Arvid Jakobsson | 21 September 2020, 19:36:43 UTC | [dexter] updates to the spec of addLiquidity - xtz_pool must be larger than zero (o/w divisiion by zero) - token_deposited must be larger than zero - min_lqt_minted should be lt or eq to lqt_created | 28 September 2020, 13:12:58 UTC |
| 2745656 | Arvid Jakobsson | 21 September 2020, 06:44:50 UTC | [dexter] Fix List notation error Works better with older versions of Coq | 28 September 2020, 13:12:58 UTC |
| 0dbb5e8 | Arvid Jakobsson | 21 September 2020, 06:21:19 UTC | [dexter] Replace String.eqb with String.string_dec For compability reasons with older versions of Coq | 28 September 2020, 13:12:58 UTC |
| f093f80 | Arvid Jakobsson | 18 September 2020, 14:00:23 UTC | [dexter] fix spec: lqt_created is rounded down, token_dep rounded up | 28 September 2020, 13:12:58 UTC |
| 6ec12a3 | Arvid Jakobsson | 18 September 2020, 14:00:07 UTC | fixup! [dexter] fix spec: amount required for first liquidity provider | 28 September 2020, 13:12:58 UTC |
| 0f342f1 | Arvid Jakobsson | 18 September 2020, 13:57:52 UTC | [dexter] fix spec: owner is credited with added liquidity | 28 September 2020, 13:12:58 UTC |
| 9937c18 | Arvid Jakobsson | 18 September 2020, 08:59:20 UTC | [dexter] update to new informal spec of check_deadline | 28 September 2020, 13:12:58 UTC |
| 30c13e5 | Arvid Jakobsson | 18 September 2020, 12:21:06 UTC | [dexter] fix spec: amount required for first liquidity provider | 28 September 2020, 13:12:58 UTC |
| 3fe2f0a | Arvid Jakobsson | 18 September 2020, 12:20:52 UTC | [dexter] fix spec: percentage in fa1.2 annotations | 28 September 2020, 13:12:58 UTC |
| 3313689 | Arvid Jakobsson | 18 September 2020, 07:16:32 UTC | [dexter] fix check_deadline | 28 September 2020, 13:12:58 UTC |
| 8f7cd98 | Arvid Jakobsson | 17 September 2020, 12:49:47 UTC | [dexter] split-addLqt: split proofs | 28 September 2020, 13:12:58 UTC |
| 54b20fb | Arvid Jakobsson | 17 September 2020, 11:15:19 UTC | [dexter] split-addLqt: add split spec | 28 September 2020, 13:12:58 UTC |
| f64a288 | Arvid Jakobsson | 17 September 2020, 10:40:11 UTC | [dexter] split-addLqt: add definition | 28 September 2020, 13:12:58 UTC |
| f424b38 | Arvid Jakobsson | 15 September 2020, 12:45:46 UTC | [dexter] updates for new contract/address formalization | 28 September 2020, 13:12:58 UTC |
| 606ca11 | Arvid Jakobsson | 11 September 2020, 09:58:44 UTC | [dexter] update contract to 325f021b | 28 September 2020, 13:12:58 UTC |
| 57a7178 | Arvid Jakobsson | 11 September 2020, 09:04:12 UTC | [dexter] conform coq spec informal spec dated [September 10, 5:16 PM] | 28 September 2020, 13:12:58 UTC |
| 37e98af | Arvid Jakobsson | 08 September 2020, 12:00:43 UTC | [dexter] conform coq spec informal spec dated [August 31, 4:20 PM] | 28 September 2020, 13:12:58 UTC |
| 0887c40 | Arvid Jakobsson | 08 September 2020, 11:50:17 UTC | [dexter] add version e8e7096c of Dexter from branch develop | 28 September 2020, 13:12:58 UTC |
| 802414c | Colin González | 07 September 2020, 08:49:03 UTC | [dexter] proof for ep_setBaker_correct | 28 September 2020, 13:12:58 UTC |
| cc0dbb4 | Colin González | 07 September 2020, 08:39:04 UTC | [dexter] proof for ep_default_correct | 28 September 2020, 13:12:58 UTC |
| bb81c4a | Colin González | 01 September 2020, 14:39:35 UTC | [dexter] proof for ep_setManager_correct | 28 September 2020, 13:12:58 UTC |
| 375887e | 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 | 28 September 2020, 13:12:58 UTC |
| 09ccea6 | 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 | 28 September 2020, 13:12:58 UTC |
| 7c5515d | Arvid Jakobsson | 12 August 2020, 12:19:59 UTC | [dexter] conform coq spec informal spec dated [August 12, 2:16 PM] | 28 September 2020, 13:12:58 UTC |
| f40ab3d | Arvid Jakobsson | 11 August 2020, 14:37:58 UTC | [dexter] add version ad6ddd89 of Dexter from branch develop, update | 28 September 2020, 13:12:58 UTC |
| 5f7bcb3 | Arvid Jakobsson | 10 August 2020, 06:29:32 UTC | [dexter] Fixes to ep_approve due to Kristina | 28 September 2020, 13:12:58 UTC |
| 10c48fc | Arvid Jakobsson | 19 July 2020, 16:27:47 UTC | [dexter] Conform coq spec informal spec dated [July 17, 12:39 AM] | 28 September 2020, 13:12:58 UTC |
| 42653f7 | Arvid Jakobsson | 17 July 2020, 08:52:17 UTC | [dexter] take a stab at proving derived properties from full spec | 28 September 2020, 13:12:58 UTC |
| 5b8b7bb | Arvid Jakobsson | 16 July 2020, 20:25:01 UTC | [dexter] add tentative specification of tokenToToken entrypoint | 28 September 2020, 13:12:58 UTC |
| 4acb18d | Arvid Jakobsson | 16 July 2020, 19:26:51 UTC | [dexter] conform coq spec informal spec dated [July 13, 10:31 AM] | 28 September 2020, 13:12:58 UTC |
| d092477 | Arvid Jakobsson | 10 July 2020, 15:57:53 UTC | [dexter] update contract to 26a6dd13 | 28 September 2020, 13:12:58 UTC |
| 4d21328 | Arvid Jakobsson | 09 July 2020, 14:12:12 UTC | Adapt proofs to simplified formulas from eval_precond | 28 September 2020, 13:12:58 UTC |
| 1c25b39 | Arvid Jakobsson | 30 June 2020, 18:30:47 UTC | [dexter] Removing sender <> spender check in approve As per trail of bits security issue 6. | 28 September 2020, 13:12:58 UTC |
| 1d2aa8e | 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 | 28 September 2020, 13:12:58 UTC |
| f0b4cff | Arvid Jakobsson | 30 June 2020, 18:13:00 UTC | [dexter] add spec for updateTokenPool & updateTokenPoolInternal | 28 September 2020, 13:12:58 UTC |
| e496495 | 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. | 28 September 2020, 13:12:58 UTC |
| 01ad2a3 | Colin González | 22 May 2020, 09:55:21 UTC | [dexter] prove ep_update_TokenPool_correct. | 28 September 2020, 13:12:58 UTC |
| 2ff53fe | Colin González | 22 May 2020, 09:26:19 UTC | [dexter] prove ep_setBaker_correct. | 28 September 2020, 13:12:58 UTC |
| 5daade9 | Arvid Jakobsson | 27 May 2020, 09:27:01 UTC | [dexter] add the addLiquidity entrypoint definition | 28 September 2020, 13:12:58 UTC |
| 3da9b45 | Arvid Jakobsson | 27 May 2020, 09:18:24 UTC | [dexter] add lqt_total to storage and update affected EPs | 28 September 2020, 13:12:58 UTC |
| ba5abce | Arvid Jakobsson | 22 May 2020, 07:00:38 UTC | [dexter] replace iff w/ and in setBaker, default spec | 28 September 2020, 13:12:58 UTC |
| 0aeb0ce | Arvid Jakobsson | 22 May 2020, 06:55:19 UTC | [dexter] use same semantics module in spec and verification | 28 September 2020, 13:12:58 UTC |
| e44022c | Arvid Jakobsson | 15 May 2020, 13:49:00 UTC | [dexter] boilerplate to verify main | 28 September 2020, 13:12:58 UTC |
| 356da2f | Arvid Jakobsson | 15 May 2020, 13:14:41 UTC | [dexter] specify xtzToToken and tokenToXtz | 28 September 2020, 13:12:58 UTC |
| 42a55e9 | Arvid Jakobsson | 15 May 2020, 07:23:44 UTC | [dexter] specify removeLiquidity | 28 September 2020, 13:12:58 UTC |
| b268b8f | Arvid Jakobsson | 13 May 2020, 15:02:05 UTC | parse wip | 28 September 2020, 13:12:58 UTC |
| 4dd558f | Arvid Jakobsson | 13 May 2020, 14:55:07 UTC | [dexter] rebase on dev, spec addLiquidity entry point | 28 September 2020, 13:12:58 UTC |
| 63f6386 | Arvid Jakobsson | 13 May 2020, 13:27:20 UTC | [dexter] specify ep_addLiquidity | 28 September 2020, 13:12:58 UTC |
| 1cfeb5b | Arvid Jakobsson | 13 May 2020, 11:56:27 UTC | [dexter] add morley contract | 28 September 2020, 13:12:58 UTC |
| dcf4d74 | Arvid Jakobsson | 13 May 2020, 11:56:10 UTC | [dexter] update contract definition from wip morley contract | 28 September 2020, 13:12:58 UTC |
| a5c3ed2 | Arvid Jakobsson | 12 May 2020, 07:41:45 UTC | [dexter] update parameter and main with new morley definition | 28 September 2020, 13:12:58 UTC |
| c2a8459 | Arvid Jakobsson | 11 May 2020, 14:10:56 UTC | [dexter] add wip spec for approve | 28 September 2020, 13:12:58 UTC |
| 023acf3 | Arvid Jakobsson | 11 May 2020, 13:02:53 UTC | [dexter] use shorthands in parameter type declaration | 28 September 2020, 13:12:58 UTC |
| 68bd203 | Arvid Jakobsson | 11 May 2020, 13:02:44 UTC | [dexter] clarify fuel comment | 28 September 2020, 13:12:58 UTC |
| 7e77296 | Arvid Jakobsson | 11 May 2020, 12:18:10 UTC | [dexter] stubs for spec/def/verification of each entrypoint | 28 September 2020, 13:12:58 UTC |
| 0c0f575 | Arvid Jakobsson | 11 May 2020, 10:02:24 UTC | [dexter] add setBaker formal specification | 28 September 2020, 13:12:58 UTC |
| 4b697bd | Arvid Jakobsson | 11 May 2020, 09:24:30 UTC | [dexter] add stubs for all entrypoints and main | 28 September 2020, 13:12:58 UTC |
| bb6bc22 | Arvid Jakobsson | 11 May 2020, 07:53:40 UTC | test | 28 September 2020, 13:12:58 UTC |
| c287b4c | Arvid Jakobsson | 11 May 2020, 06:40:04 UTC | rename | 28 September 2020, 13:12:58 UTC |
| c1bc44b | Arvid Jakobsson | 24 January 2020, 18:13:32 UTC | [dexter] Specify entrypoints vote | 28 September 2020, 13:12:58 UTC |
| 3d30375 | Arvid Jakobsson | 24 January 2020, 17:24:09 UTC | [dexter] Specify entrypoints xtzToToken and tokenToXtz | 28 September 2020, 13:12:58 UTC |
| 1a25e53 | Arvid Jakobsson | 24 January 2020, 15:54:57 UTC | [dexter] Specify entrypoint removeLiquidity | 28 September 2020, 13:12:58 UTC |
| cf79373 | Arvid Jakobsson | 23 January 2020, 16:04:15 UTC | [dexter] Specify baker election (provisional version) | 28 September 2020, 13:12:58 UTC |
| 7a66b03 | Arvid Jakobsson | 21 January 2020, 16:27:58 UTC | [dexter] Relational input-output specification of entrypoint add_liquidity | 28 September 2020, 13:12:58 UTC |
| 5314b5c | Arvid Jakobsson | 21 January 2020, 10:19:18 UTC | A more "classic relational" specification of the add_liquidity entrypoint | 28 September 2020, 13:12:58 UTC |
| dd3dc15 | 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. | 28 September 2020, 13:12:58 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 |
