| 8f57f12 | Arvid Jakobsson | 10 May 2021, 07:35:53 UTC | Merge branch 'arvid@ci-build-refactor-cache' into 'dev' Draft: [ci] add cache opam directory See merge request nomadic-labs/mi-cho-coq!119 | 10 May 2021, 07:35:53 UTC |
| 6ba8c47 | Raphaël Cauderlier | 25 April 2021, 12:26:44 UTC | [Readme] Remove a TODO item | 25 April 2021, 13:02:07 UTC |
| 1f25be1 | Raphaël Cauderlier | 22 April 2021, 15:13:43 UTC | [michocoq] Don't axiomatize operations To break the dependency cycle between the interpretation of operations and the definition of the semantics of Michelson types, we rely on the following stratification observation: data appearing inside operations cannot contain operations because the operation type is neither passable nor storable. | 25 April 2021, 13:02:07 UTC |
| eb663d9 | Raphaël Cauderlier | 25 April 2021, 12:15:12 UTC | [test] regenerate the regression traces The non-packability of `contract _` and `operation` are now taken into account in the type checker. | 25 April 2021, 12:50:22 UTC |
| 6197a02 | Raphaël Cauderlier | 25 April 2021, 12:14:49 UTC | [test] Document how to regenerate the regression traces | 25 April 2021, 12:50:21 UTC |
| 1fc3c6b | Raphaël Cauderlier | 22 April 2021, 14:38:48 UTC | [michocoq] model Michelson typeclasses This commit enforces that types appearing in some instructions are constrained by some type classes: - EMPTY_BIG_MAP k v: v can contain big map values - TRANSFER_TOKENS and CONTRACT: parameter type is passable - PACK and UNPACK: packed type is packable - FAILWITH: thrown values is packable - CREATE_CONTRACT and whole script: parameter type is passable and storage type is storable | 25 April 2021, 12:49:45 UTC |
| c4559c5 | Raphaël Cauderlier | 21 April 2021, 10:16:14 UTC | [michocoq] Use an inductive type for interpreting contracts Same motivation than the previous commit. | 25 April 2021, 12:41:48 UTC |
| 06a7ea4 | Raphaël Cauderlier | 21 April 2021, 08:00:47 UTC | [michocoq] Use an inductive type for interpreting lambdas This replaces the type "sigT (fun tff : Datatypes.bool => instruction_seq None tff (a ::: nil) (b ::: nil)" by a new inductive type to simplify Coq error messages. | 25 April 2021, 12:41:47 UTC |
| 8506507 | Raphaël Cauderlier | 21 April 2021, 07:35:51 UTC | [michocoq] Rename is_packable into is_pushable This predicate, used to constrain the APPLY opcode, is named "pushable" in the documentation and in the Tezos source code. | 25 April 2021, 12:41:47 UTC |
| 63f7a56 | Raphaël Cauderlier | 21 April 2021, 07:32:13 UTC | [michocoq] Remove unused "tez_constant" type This remains from the formalization of mutez arith. | 25 April 2021, 12:41:47 UTC |
| c0f0ffb | Raphaël Cauderlier | 21 April 2021, 07:21:37 UTC | [michocoq] simplify the elaboration of APPLY | 25 April 2021, 12:41:47 UTC |
| 9b1d3d5 | Raphaël Cauderlier | 21 April 2021, 06:46:46 UTC | [michocoq] avoid reasoning on dependent if The dependent if construction error.dif wasn't very convenient because Coq was rarely able to infer the implicit type predicate parameter. This commit drops it in favor of a simpler construction error.assume that can be used while working inside the error monad to check that a boolean is true and obtain a witness of this fact. | 25 April 2021, 12:41:32 UTC |
| 0617440 | Raphaël Cauderlier | 18 March 2021, 10:30:36 UTC | [michocoq] Fuel-free WP in the LOOP-free case | 25 April 2021, 12:21:28 UTC |
| 4f2fb8a | Arvid Jakobsson | 09 October 2020, 16:17:51 UTC | [michocoq] move fold_eval_precond to semantics.v | 25 April 2021, 12:21:28 UTC |
| 28ab3ae | Raphaël Cauderlier | 18 March 2021, 10:29:59 UTC | [michocoq] Add some type annots in semantics to get prettier goals | 25 April 2021, 12:21:28 UTC |
| 3848255 | 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 | 25 April 2021, 12:21:28 UTC |
| 3ce377e | Raphaël Cauderlier | 10 April 2021, 09:33:09 UTC | [Mi-Cho-Coq] Use the ascii boolean equality from the stdlib | 25 April 2021, 10:55:07 UTC |
| f7e378a | Guillaume Claret | 12 March 2021, 12:42:17 UTC | [mi-cho-coq] Replace String.string_dec by String.eqb | 25 April 2021, 10:55:07 UTC |
| b555744 | Raphaël Cauderlier | 10 March 2021, 20:40:12 UTC | [extraction] Hack to support the old OCaml version used in the CI | 25 April 2021, 08:57:22 UTC |
| f9f30b9 | 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. | 25 April 2021, 08:57:22 UTC |
| 71dac82 | Raphaël Cauderlier | 09 April 2021, 16:15:04 UTC | [Michocoq] ignore annotations on sum types everywhere but in parameter Fixes #49. | 25 April 2021, 08:55:21 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 |
| 9749d15 | Arvid Jakobsson | 07 April 2021, 19:39:52 UTC | [ci] add cache opam directory | 08 April 2021, 16:50:07 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 |
| 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 |
