| b983c92 | Yann Regis-Gianas | 29 April 2021, 08:15:33 UTC | New spec and proof for TokenToToken Signed-off-by: Yann Regis-Gianas <yann@nomadic-labs.com> | 29 April 2021, 15:38:38 UTC |
| 61ad095 | Arvid Jakobsson | 20 April 2021, 08:06:23 UTC | WIP: update spec and proof for tokenToToken | 29 April 2021, 07:39:43 UTC |
| 2c36f1e | Arvid Jakobsson | 09 April 2021, 15:47:28 UTC | CPMM2: Update proof for xtzToToken | 29 April 2021, 07:39:42 UTC |
| cbd1275 | Arvid Jakobsson | 09 April 2021, 15:47:19 UTC | CPMM2: Update spec for xtzToToken | 29 April 2021, 07:39:42 UTC |
| 1058bb2 | Yann Regis-Gianas | 26 April 2021, 15:01:51 UTC | [cpmm2] importing contracts liquidity_baking#29e51e9 | 26 April 2021, 15:01:51 UTC |
| abaa034 | Yann Regis-Gianas | 26 April 2021, 14:39:00 UTC | [cpmm2] Importing contracts liquidity_baking#29e51e9b72a | 26 April 2021, 14:39:14 UTC |
| 45c51b7 | Arvid Jakobsson | 22 April 2021, 14:49:06 UTC | [cpmm2] add updating script | 22 April 2021, 14:49:06 UTC |
| 7b297e4 | Arvid Jakobsson | 21 April 2021, 18:37:02 UTC | [cpmm2] importing contracts liquidity_baking#60220a2 | 21 April 2021, 18:38:09 UTC |
| 0945675 | Arvid Jakobsson | 20 April 2021, 14:12:01 UTC | Importing CPMM2 contracts liquidity_baking#399fd25 | 20 April 2021, 14:24:21 UTC |
| 8aa5a1a | Arvid Jakobsson | 09 April 2021, 14:38:58 UTC | CPMM2: Fix proofs for add/remLqt + default | 20 April 2021, 14:01:01 UTC |
| 5a16749 | Arvid Jakobsson | 09 April 2021, 14:37:33 UTC | CPMM2: Abstract out fee | 20 April 2021, 13:56:33 UTC |
| ecc0a6d | Arvid Jakobsson | 09 April 2021, 14:12:25 UTC | CPMM2: Remove references to removed entrypoints | 20 April 2021, 13:54:20 UTC |
| 8a23a27 | Arvid Jakobsson | 09 April 2021, 13:20:22 UTC | Refactor: move out storage helpers | 20 April 2021, 13:49:09 UTC |
| 43a808d | Arvid Jakobsson | 09 April 2021, 13:05:45 UTC | Refactor: move out definition helpers | 20 April 2021, 13:49:09 UTC |
| ecd0945 | Arvid Jakobsson | 09 April 2021, 13:01:26 UTC | Importing CPMM2 contracts liquidity_baking#6ca2d45 | 20 April 2021, 13:49:09 UTC |
| 3a2e6c5 | Arvid Jakobsson | 15 April 2021, 12:22:04 UTC | CPMM2: Add lemmas on N.div | 20 April 2021, 13:48:52 UTC |
| 7ccb336 | Raphaël Cauderlier | 18 March 2021, 11:08:58 UTC | Use the fuel-free WP in Dexter proofs | 20 April 2021, 13:45:45 UTC |
| 2551e5f | Raphaël Cauderlier | 17 March 2021, 09:24:12 UTC | [dexter2] delay computation of the typed scripts and use vm_compute | 20 April 2021, 13:45:45 UTC |
| a3245a8 | Arvid Jakobsson | 11 March 2021, 18:59:32 UTC | [dexter2] add functional correctness proof The proof is a joint effort of: - Arvid Jakobsson <arvid.jakobsson@nomadic-labs.com> - Yann-Regis Gianas <yann@nomadic-labs.com> - Colin González <colin@nomadic-labs.com> - Guillaume Claret <guillaume.claret@nomadic-labs.com> | 20 April 2021, 13:45:45 UTC |
| 3b66534 | Arvid Jakobsson | 11 March 2021, 18:58:39 UTC | [dexter2] add specification utility lemmas for Dexter2 These lemmas are related to the specification of Dexter 2 and unlikely to be useful in other developments. | 20 April 2021, 13:38:56 UTC |
| 1efed64 | Arvid Jakobsson | 11 March 2021, 18:56:49 UTC | [dexter2] add Dexter2 wip#adf8140: source, definition and spec | 20 April 2021, 13:38:56 UTC |
| 5813f65 | Arvid Jakobsson | 11 March 2021, 18:58:05 UTC | [dexter2] add utility lemmas These lemmas are potentially of general utility in other smart contract developments. | 20 April 2021, 08:25:01 UTC |
| 3144def | Arvid Jakobsson | 09 October 2020, 16:44:52 UTC | [mi-cho-coq] add compare_gt_lt to comparable.v | 20 April 2021, 08:25:01 UTC |
| f598c93 | Arvid Jakobsson | 21 September 2020, 19:36:05 UTC | [mi-cho-coq] prove injectivity of tez.to_Z | 20 April 2021, 08:25:01 UTC |
| 15a1a06 | Arvid Jakobsson | 18 September 2020, 13:30:41 UTC | [mi-cho-coq] prove lower bound on tez.to_Z | 20 April 2021, 08:25:01 UTC |
| 72bd425 | Raphaël Cauderlier | 18 March 2021, 10:30:36 UTC | [michocoq] Fuel-free WP in the LOOP-free case | 20 April 2021, 08:08:59 UTC |
| 478cb5a | Arvid Jakobsson | 09 October 2020, 16:17:51 UTC | [michocoq] move fold_eval_precond to semantics.v | 20 April 2021, 08:08:59 UTC |
| 3b7f66d | Raphaël Cauderlier | 18 March 2021, 10:29:59 UTC | [michocoq] Add some type annots in semantics to get prettier goals | 20 April 2021, 08:08:59 UTC |
| 8d3834d | Raphaël Cauderlier | 18 March 2021, 10:28:55 UTC | [michocoq] Move option monad definitions, notation, lemmas to error.v This is to enable using them in semantics.v | 20 April 2021, 08:08:59 UTC |
| 2690e7d | Raphaël Cauderlier | 11 April 2021, 14:59:11 UTC | [michocoq] Avoid redefining `False` in `util.v` The name of the Michelson data constructor `False` clashes with the Coq proposition for contradiction. To avoid qualifying the Coq proposition, `util.v` redefines it so `util.False` is defined as `Logic.False`. This has unpleasant side effects (see https://gitlab.com/nomadic-labs/mi-cho-coq/-/issues/53) so we remove this definition and qualify the name in the few places where it is used instead. Closes #53. | 11 April 2021, 14:59:11 UTC |
| d30f3ab | Arvid Jakobsson | 08 April 2021, 17:09:50 UTC | [build] configure should recreate the src/_CoqProject file on each run | 08 April 2021, 17:09:50 UTC |
| bcce564 | Arvid Jakobsson | 08 April 2021, 16:33:30 UTC | [build] fix the behaviour of ./configure with no arguments | 08 April 2021, 16:34:40 UTC |
| 59e5be5 | Arvid Jakobsson | 07 April 2021, 15:59:42 UTC | [ci] add contracts job | 08 April 2021, 16:11:22 UTC |
| e689a8e | Arvid Jakobsson | 07 April 2021, 14:35:54 UTC | [ci] extract michocoq | 08 April 2021, 13:45:39 UTC |
| ee5330b | Arvid Jakobsson | 07 April 2021, 12:39:30 UTC | [ci/lint] run linting in a separate stage | 07 April 2021, 13:03:43 UTC |
| 905b528 | Arvid Jakobsson | 07 April 2021, 12:39:04 UTC | [ci/lint] print linting errors if any | 07 April 2021, 12:44:26 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 |
| 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 |
