| d116674 | kristinas | 11 May 2021, 09:41:59 UTC | Added README | 11 May 2021, 09:41:59 UTC |
| f70493e | kristinas | 11 May 2021, 09:35:06 UTC | Creating a folder fa1.2 | 11 May 2021, 09:35:06 UTC |
| ee7fd9e | kristinas | 11 May 2021, 09:29:30 UTC | Renaming some files. | 11 May 2021, 09:29:30 UTC |
| 4cf31f6 | kristinas | 11 May 2021, 09:22:17 UTC | Added .tz files for FA1.2 contracts. | 11 May 2021, 09:22:17 UTC |
| 03f7b7b | kristinas | 03 May 2021, 21:00:17 UTC | Removing variable shadowing in match. | 03 May 2021, 21:00:17 UTC |
| df27e8a | kristinas | 30 April 2021, 22:37:54 UTC | Renaming Archetype to Edukera. | 30 April 2021, 22:37:54 UTC |
| 78b79d4 | kristinas | 23 March 2021, 16:21:33 UTC | Finished proving that Dexter FA1.2 preserves validity of storage. | 23 March 2021, 16:21:33 UTC |
| fd7dcce | kristinas | 17 March 2021, 10:49:42 UTC | Attempting to fix a compilation error in fa12_dexter_verification.v | 17 March 2021, 10:49:42 UTC |
| e67f299 | kristinas | 16 March 2021, 22:45:05 UTC | stack_dig issue | 16 March 2021, 22:45:05 UTC |
| 1241840 | kristinas | 15 March 2021, 20:22:15 UTC | FA1.2 correctness rebase. | 15 March 2021, 20:22:15 UTC |
| 4d6f57a | kristinas | 11 March 2021, 19:46:19 UTC | Bitvectors issue. | 11 March 2021, 19:46:19 UTC |
| a3ffc51 | Raphaël Cauderlier | 11 March 2021, 10:44:27 UTC | Fixup opacity | 11 March 2021, 10:44:27 UTC |
| 6c60364 | Raphaël Cauderlier | 11 March 2021, 10:23:56 UTC | !fixup: wip: fix fuel problem | 11 March 2021, 10:23:56 UTC |
| 2b1c2df | Raphaël Cauderlier | 10 March 2021, 23:24:50 UTC | !fixup: rebase | 11 March 2021, 10:23:13 UTC |
| 0edc082 | kristinas | 10 March 2021, 11:39:30 UTC | fuel problem | 10 March 2021, 21:41:48 UTC |
| d3b9e0d | kristinas | 16 February 2021, 21:56:13 UTC | Renaming some files. | 10 March 2021, 21:41:48 UTC |
| 6c06989 | kristinas | 11 February 2021, 10:07:38 UTC | Finalized FA1.2 verification for merging. | 10 March 2021, 21:41:48 UTC |
| 52caad3 | kristinas | 22 December 2020, 20:25:35 UTC | Updated the CamlCase implementation of FA1.2. | 10 March 2021, 21:41:48 UTC |
| 0d0e471 | kristinas | 30 November 2020, 00:57:08 UTC | Rebasing on dev. | 10 March 2021, 21:41:48 UTC |
| bcdf9ff | Raphaël Cauderlier | 10 March 2021, 20:40:12 UTC | [extraction] Hack to support the old OCaml version used in the CI | 10 March 2021, 21:40:48 UTC |
| 45ea169 | Raphaël Cauderlier | 10 March 2021, 16:47:22 UTC | [michocoq] Represent mutez using the builtin int63 type In Coq 8.10, builtin support for int63 has been added. This is exactly the type needed to represent mutez. This commits: - changes the representation of mutez - removes the now unused module "int64bv" - drops support for Coq < 8.10 - adapts the contract proofs for the new implementation. In particular the proof of vesting_tez has been rewritten. | 10 March 2021, 16:48:37 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 |
| 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 |
