Fixes required for Mi-Cho-Coq dev branch and its certified optimizer

.gitlab-ci.yml

@@ -6,6 +6,7 @@ stages:
   - sudo chown -R coq:coq "$CI_PROJECT_DIR"
   - opam switch ${COMPILER_EDGE}
   - opam pin add -k git -y -j ${NJOBS} coq-ott https://github.com/ott-lang/ott.git
+  - opam pin add -k git -y --no-action coq-mi-cho-coq https://gitlab.com/nomadic-labs/mi-cho-coq.git#dev
   - opam repository add coq-extra-dev https://coq.inria.fr/opam/extra-dev
   - opam depext -y coq-albert
   - opam pin add -k git -y -j ${NJOBS} --inplace-build --with-test coq-albert ./
@@ -49,6 +50,7 @@ test:docker:
     - docker build --pull -t "$CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG" .
   except:
     - master
+    - /dev/
 
 publish:docker:master:
   # :latest image

coq/compiler_correctness.v

@@ -11,41 +11,41 @@ Require Import List String Bool Ascii ZArith Permutation.
 Require Import Coq.Program.Equality.
 Require Import michocomp.
 
-Module Proofs (C : syntax.ContractContext).
-  Module syntax := syntax.Syntax C.
-  Module mtyper := typer.Typer C.
+Module Proofs.
 
 
 
-  Parameter self_type : Datatypes.option type.
-  Definition type_data := mtyper.type_data.
-  Definition type_instruction := mtyper.type_instruction (self_type := self_type).
-  Definition type_check_instruction := mtyper.type_check_instruction (self_type := self_type).
+  Parameter self_type : syntax.self_info.
+  Definition type_data := typer.type_data.
+  Definition type_instruction := typer.type_instruction (self_type := self_type).
+  Definition type_instruction_seq := typer.type_instruction_seq (self_type := self_type).
+  Definition type_check_instruction := typer.type_check_instruction (self_type := self_type).
+  Definition type_check_instruction_seq := typer.type_check_instruction_seq (self_type := self_type).
 
-  Lemma type_check_instruction_type_instruction : forall ins A B ins',
-      type_check_instruction type_instruction ins A B = Michocoq.error.Return ins' ->
-      exists r, type_instruction ins A = Michocoq.error.Return r.
+  Lemma type_check_instruction_type_instruction : forall ins A B ins' m,
+      type_check_instruction (type_instruction m) ins A B = Michocoq.error.Return ins' ->
+      exists r, type_instruction m ins A = Michocoq.error.Return r.
   Proof.
-    intros ins A B ins' Hcheck.
-    unfold type_check_instruction, mtyper.type_check_instruction in Hcheck.
+    intros ins A B ins' m Hcheck.
+    unfold type_check_instruction, typer.type_check_instruction in Hcheck.
     apply error.success_eq_return_rev.
     apply error.success_eq_return in Hcheck.
     apply error.success_bind_arg in Hcheck.
     assumption.
   Qed.
 
-  Lemma data_type_correct: forall v d ty mty,
+  Lemma data_type_correct: forall v d ty mty m,
       michelson_data_of_val v = Return _ d ->
       type_value v = Return _ ty ->
       michelson_type_of_type ty = Return _ mty ->
-      exists td, type_data d mty = Michocoq.error.Return td.
+      exists td, type_data m d mty = Michocoq.error.Return td.
   Proof.
     (* induction v using val_ind; intros d ty' mty Hd Hty Hmty; simpl in *. *)
     (* - (* numval *) *)
     (*   admit. *)
     (*   (* AJ: this blocks coq. *)
     (*    * destruct v; invert Hd; invert Hty; invert Hmty; simpl; *)
-    (*    *   unfold type_data, mtyper.type_data; eexists; eauto. *)
+    (*    *   unfold type_data, typer.type_data; eexists; eauto. *)
     (*    *) *)
     (* - (* bool *) *)
     (*   invert Hty; invert Hmty. *)
@@ -76,12 +76,12 @@ Module Proofs (C : syntax.ContractContext).
   (*     reflexivity. *)
   (* Qed. *)
 
-  Lemma compute_dig_typing: forall var ty' lt lt' ll ll' ins mty sty sty',
+  Lemma compute_dig_typing: forall var ty' lt lt' ll ll' ins mty sty sty' m,
       type_and_remove var lt = Return _ (ty', lt') ->
       compute_dig var ll = Return _ (ins, ll') ->
       michelson_type_of_type ty' = Return _ mty ->
       michelson_stack_type_of_rty lt = Return _ sty -> michelson_stack_type_of_rty lt' = Return _ sty' ->
-      exists tins, type_instruction ins sty = Michocoq.error.Return (mtyper.Inferred_type sty (mty::sty') tins).
+      exists tins, type_instruction m ins sty = Michocoq.error.Return (typer.Inferred_type sty (mty::sty') tins).
   Proof.
     (* TODO when the DIG typer is formally specified in michelson *)
     (* We could possibly give this tins explicitely instead of "exists" ? *)
@@ -118,22 +118,17 @@ Module Proofs (C : syntax.ContractContext).
     (* - admit. *)
   Admitted.
 
-  Ltac unfold_check :=
-    unfold type_check_instruction, mtyper.type_check_instruction; simpl;
-    try (unfold mtyper.type_check_instruction_no_tail_fail,
-         mtyper.type_instruction_no_tail_fail); simpl.
-
   Ltac unfold_cast :=
-    unfold mtyper.instruction_cast_range, mtyper.instruction_cast;
+    unfold typer.instruction_cast_range, typer.instruction_cast;
     simpl; repeat rewrite stype_dec_same; simpl.
 
   (** Arg adds a single element to the stack *)
-  Lemma compile_arg_type_correct : forall arg ins ty' lt lt' ll ll' mty sty sty',
+  Lemma compile_arg_type_correct : forall arg ins ty' lt lt' ll ll' mty sty sty' m,
       type_arg arg (rty_record lt) = Return _ (ty', rty_record lt') ->
       compile_arg arg ll = Return _ (ins, ll') ->
       michelson_type_of_type ty' = Return _ mty ->
       michelson_stack_type_of_rty lt = Return _ sty -> michelson_stack_type_of_rty lt' = Return _ sty' ->
-      exists res, type_check_instruction type_instruction ins sty (mty::sty') = Michocoq.error.Return res.
+      exists res, type_check_instruction_seq (type_instruction_seq m) ins sty (mty::sty') = Michocoq.error.Return res.
   Proof.
     (* induction arg; intros ins ty' lt lt' ll ll' mty sty sty' Hty Hcomp Hmty Hsty Hsty'; simpl in *. *)
     (* - (* var *) *)
@@ -160,11 +155,11 @@ Module Proofs (C : syntax.ContractContext).
     (* - (* record *) admit. *)
   Admitted.
 
-  Lemma compile_funct_type_correct : forall funct defs ins ty ty' mty mty' sty,
+  Lemma compile_funct_type_correct : forall funct defs ins ty ty' mty mty' sty m,
       type_funct funct ty g_empty = Return _ ty' ->
       compile_funct funct defs = Return _ ins ->
       michelson_type_of_type ty = Return _ mty -> michelson_type_of_type ty' = Return _ mty' ->
-      exists res, type_check_instruction type_instruction ins (mty::sty) (mty'::sty) = Michocoq.error.Return res.
+      exists res, type_check_instruction_seq (type_instruction_seq m) ins (mty::sty) (mty'::sty) = Michocoq.error.Return res.
   Proof.
     (* intros funct defs ins ty ty' mty mty' sty Hty Hcomp Hmty Hmty'. *)
     (* induction funct; invert Hty; invert Hcomp; simpl in *. *)
@@ -187,12 +182,12 @@ Module Proofs (C : syntax.ContractContext).
   Admitted.
 
   (** Rhs adds a single element to the stack *)
-  Lemma compile_rhs_type_correct : forall rhs defs ins ty' lt lt' ll ll' mty sty sty',
+  Lemma compile_rhs_type_correct : forall rhs defs ins ty' lt lt' ll ll' mty sty sty' m,
       type_rhs rhs (rty_record lt) g_empty = Return _ (ty', rty_record lt') ->
       compile_rhs rhs ll lt defs = Return _ (ins, ll') ->
       michelson_type_of_type ty' = Return _ mty ->
       michelson_stack_type_of_rty lt = Return _ sty -> michelson_stack_type_of_rty lt' = Return _ sty' ->
-      exists res, type_check_instruction type_instruction ins sty (mty::sty') = Michocoq.error.Return res.
+      exists res, type_check_instruction_seq (type_instruction_seq m) ins sty (mty::sty') = Michocoq.error.Return res.
   Proof.
     (* induction rhs; intros defs ins ty' lt lt' ll ll' mty sty sty' Hty Hcomp Hmty Hsty Hsty'; simpl in *. *)
     (* - (* arg *) *)
@@ -220,12 +215,12 @@ Module Proofs (C : syntax.ContractContext).
     (* - (* match *) admit. *)
   Admitted.
 
-  Lemma compile_instr_type_correct : forall ins defs lt lt' unins ll ll' sty sty',
+  Lemma compile_instr_type_correct : forall ins defs lt lt' unins ll ll' sty sty' m,
       type_instr ins (rty_record lt) g_empty = Return _ (Inferred (rty_record lt')) ->
       type_and_compile ins (rty_record lt) ll defs = Return _ (unins, ll') ->
       michelson_stack_type_of_rty lt = Return _ sty ->
       michelson_stack_type_of_rty lt' = Return _ sty' ->
-      exists res, type_check_instruction type_instruction unins sty sty' = Michocoq.error.Return res.
+      exists res, type_check_instruction_seq (type_instruction_seq m) unins sty sty' = Michocoq.error.Return res.
   Proof.
     (* induction ins; intros defs lt lt' unins ll ll' sty sty' Hty Hcomp Hsty Hsty'; *)
     (*   invert Hty; invert Hcomp; simpl in *. *)

coq/michocomp_tests.v

@@ -3,6 +3,9 @@
 Require Michocoq.untyped_syntax Michocoq.syntax Michocoq.syntax_type Michocoq.typer Michocoq.untyper.
 Require aux albert error label_lexico lexico_sort typer Michocoq.syntax_type.
 
+Import untyped_syntax.notations.
+Open Scope michelson_untyped_scope.
+
 Import aux error.
 Import albert typer  label_lexico lexico_sort.
 Import Michocoq.untyped_syntax Michocoq.syntax_type.
@@ -45,17 +48,17 @@ Goal michelson_of_nil_rty = Return type unit.
 Qed.
 
 Definition michelson_of_rty := Eval compute in (michelson_type_of_type (ty_rty (rty_record (("c", ty_nat)::("b", ty_mutez)::("a", ty_int)::nil)))).
-Goal michelson_of_rty = Return type (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type int))).
+Goal michelson_of_rty = Return type (pair nat (pair mutez int)).
         reflexivity.
 Qed.
 
 Definition michelson_of_vty_option := Eval compute in (michelson_type_of_type (ty_vty (vty_variant (("None", ty_unit)::("Some", ty_nat)::nil)))).
-Goal michelson_of_vty_option = Return type (option (Comparable_type nat)).
+Goal michelson_of_vty_option = Return type (option nat).
         reflexivity.
 Qed.
 
 Definition michelson_of_vty := Eval compute in (michelson_type_of_type (ty_vty (vty_variant (("A", ty_unit)::("B", ty_nat)::nil)))).
-Goal michelson_of_vty = Return type (or unit (Comparable_type nat)).
+Goal michelson_of_vty = Return type (or unit None nat None).
         reflexivity.
 Qed.
 
@@ -76,61 +79,70 @@ Notation "UNPAIR%" := (SEQ DUP (SEQ CAR (DIP CDR))).
 Definition type_and_compile ins rt ll := type_and_compile ins rt ll nil.
 
 Definition assign_add := Eval compute in (type_and_compile (instr_assign (lhs_var "r") (rhs_add "x" "y")) startType startStack).
-Goal assign_add = Return (instruction * Datatypes.list string) (SEQ (SEQ (SEQ (DIG 5) (DIG 5)) ADD) (DUG 3), "b" :: "m" :: "or" :: "r" :: "v" :: "z" :: nil).
+Goal assign_add =
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 5; DIG 5; ADD; DUG 3}, "b" :: "m" :: "or" :: "r" :: "v" :: "z" :: nil).
   reflexivity.
 Qed.
 
 Definition assign_projection := Eval compute in (type_and_compile (instr_assign (lhs_var "p") (rhs_projection "z" "b")) startType startStack).
-Goal assign_projection = Return (instruction * Datatypes.list string) (SEQ (SEQ (DIG 6) (SEQ CDR CAR)) (DUG 3), "b" :: "m" :: "or" :: "p" :: "v" :: "x" :: "y" :: nil).
+Goal assign_projection =
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 6; CDR; CAR; DUG 3}, "b" :: "m" :: "or" :: "p" :: "v" :: "x" :: "y" :: nil).
   reflexivity.
 Qed.
 
 Definition assign_update := Eval compute in (type_and_compile (instr_assign (lhs_var "p") (rhs_update "z" (("b", "m")::("c","x")::nil))) startType startStack).
 Goal assign_update =
-Return (instruction * Datatypes.list string)
-  (SEQ
-     (SEQ (DIG 6)
-        (SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR)))
-           (SEQ (DIP 1 (SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR))) (SEQ (DROP 1) (SEQ (DIG 2) (SEQ (DIP 1 (SEQ (DROP 1) (DIG 3))) PAIR))))) PAIR)))
-     (DUG 2), "b" :: "or" :: "p" :: "v" :: "y" :: nil).
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 6; Instruction_seq {DUP; CAR; DIP 1 {CDR}};
+         DIP 1
+             {Instruction_seq {DUP; CAR; DIP 1 {CDR}}; DROP 1;
+              DIG 2; DIP 1 {DROP 1; DIG 3}; PAIR}; PAIR; DUG 2},
+        "b" :: "or" :: "p" :: "v" :: "y" :: nil).
   reflexivity.
 Qed.
 
 Definition assign_lhs_record := Eval compute in (type_and_compile (instr_assign (lhs_record (("b","d")::("a", "c")::nil)) (rhs_arg (arg_var "z"))) startType startStack).
 Goal assign_lhs_record =
-Return (instruction * Datatypes.list string)
-  (SEQ (DIG 6) (SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR))) (SEQ (DUG 2) (DUG 1))), "b" :: "c" :: "d" :: "m" :: "or" :: "v" :: "x" :: "y" :: nil).
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 6; Instruction_seq {DUP; CAR; DIP 1 {CDR}}; DUG 2; DUG 1},
+        "b" :: "c" :: "d" :: "m" :: "or" :: "v" :: "x" :: "y" :: nil).
   reflexivity.
 Qed.
 
 Definition assign_rhs_record:= Eval compute in (type_and_compile (instr_assign (lhs_var "r") (rhs_arg (arg_record (("a1", "x")::("a2","z")::nil)))) startType startStack).
 Goal assign_rhs_record =
-Return (instruction * Datatypes.list string) (SEQ (SEQ (SEQ (DIG 6) (DIG 5)) PAIR) (DUG 3), "b" :: "m" :: "or" :: "r" :: "v" :: "y" :: nil).
-        reflexivity.
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 6; DIG 5; PAIR; DUG 3}, "b" :: "m" :: "or" :: "r" :: "v" :: "y" :: nil).
+  reflexivity.
 Qed.
 
 Definition drop := Eval compute in (type_and_compile (instr_drop "y") startType startStack).
 Goal drop =
-Return (instruction * Datatypes.list string) (SEQ (DIG 5) (DROP 1), "b" :: "m" :: "or" :: "v" :: "x" :: "z" :: nil).
-        reflexivity.
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 5; DROP 1}, "b" :: "m" :: "or" :: "v" :: "x" :: "z" :: nil).
+  reflexivity.
 Qed.
 
 Definition assign_dup:= Eval compute in (type_and_compile (instr_assign (lhs_var "v2") (rhs_app fun_dup (arg_var "y"))) startType startStack).
 Goal assign_dup =
-Return (instruction * Datatypes.list string) (SEQ (SEQ (DIG 5) (SEQ DUP PAIR)) (DUG 4), "b" :: "m" :: "or" :: "v" :: "v2" :: "x" :: "z" :: nil).
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 5; DUP; PAIR; DUG 4}, "b" :: "m" :: "or" :: "v" :: "v2" :: "x" :: "z" :: nil).
         reflexivity.
 Qed.
 
 Definition assign_fun_app := Eval compute in (type_and_compile (instr_assign (lhs_var "v2") (rhs_app (fun_constr "B" (vty_variant (("A", ty_int)::("B", ty_int)::("C", ty_int)::nil))) (arg_var "x"))) startType startStack).
 Goal assign_fun_app =
-Return (instruction * Datatypes.list string)
-  (SEQ (SEQ (DIG 4) (SEQ (LEFT (Comparable_type int)) (RIGHT (Comparable_type int)))) (DUG 4), "b" :: "m" :: "or" :: "v" :: "v2" :: "y" :: "z" :: nil).
+Return (instruction_seq * Datatypes.list string)
+  ({DIG 4; LEFT int; RIGHT int; DUG 4}, "b" :: "m" :: "or" :: "v" :: "v2" :: "y" :: "z" :: nil).
         reflexivity.
 Qed.
 
 Definition assign_option := Eval compute in (type_and_compile (instr_assign (lhs_var "opt") (rhs_app (fun_constr "Some" (vty_variant (("None", ty_unit)::("Some", ty_int)::nil))) (arg_var "x"))) startType startStack).
 Goal assign_option =
-Return (instruction * Datatypes.list string) (SEQ (SEQ (DIG 4) SOME) (DUG 2), "b" :: "m" :: "opt" :: "or" :: "v" :: "y" :: "z" :: nil).
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 4; SOME; DUG 2}, "b" :: "m" :: "opt" :: "or" :: "v" :: "y" :: "z" :: nil).
         reflexivity.
 Qed.
 
@@ -142,8 +154,8 @@ Definition assign_match_variant := Eval compute in (type_and_compile
                                                                     ::(pattern_variant  "C" "i", (rhs_arg (arg_var "i")))::nil))))
                                  startType startStack).
 Goal assign_match_variant =
-Return (instruction * Datatypes.list string)
-  (SEQ (SEQ (DIG 3) (IF_LEFT (DIG 0) (SEQ (DIG 3) (IF_LEFT (DIG 0) (DIG 0))))) (DUG 3), "b" :: "m" :: "or" :: "res" :: "x" :: "y" :: "z" :: nil).
+Return (instruction_seq * Datatypes.list string)
+  ({DIG 3; IF_LEFT {DIG 0} {DIG 3; IF_LEFT {DIG 0}{DIG 0}}; DUG 3}, "b" :: "m" :: "or" :: "res" :: "x" :: "y" :: "z" :: nil).
         reflexivity.
 Qed.
 
@@ -155,13 +167,14 @@ Definition match_variant := Eval compute in
                                   ::(pattern_variant "C" "i", (instr_seq (instr_drop "x")(instr_assign (lhs_var "r") (rhs_arg (arg_var "i")))))::nil)))
          startType startStack).
 Goal match_variant =
-Return (instruction * Datatypes.list string)
-  (SEQ (DIG 3)
-     (IF_LEFT (SEQ (DUG 1) (SEQ (SEQ (DIG 4) (DROP 1)) (SEQ (DIG 1) (DUG 3))))
-        (SEQ (DIG 3)
-           (IF_LEFT (SEQ (DUG 1) (SEQ (SEQ (DIG 1) (DROP 1)) (SEQ (DIG 3) (DUG 3)))) (SEQ (DUG 1) (SEQ (SEQ (DIG 4) (DROP 1)) (SEQ (DIG 1) (DUG 3))))))),
-  "b" :: "m" :: "or" :: "r" :: "y" :: "z" :: nil).
-        reflexivity.
+Return (instruction_seq * Datatypes.list string)
+  ({DIG 3;
+     IF_LEFT {DUG 1; DIG 4; DROP 1; DIG 1; DUG 3}
+       {DIG 3;
+       IF_LEFT {DUG 1; DIG 1; DROP 1; DIG 3; DUG 3}
+         {DUG 1; DIG 4; DROP 1; DIG 1; DUG 3}}},
+   "b" :: "m" :: "or" :: "r" :: "y" :: "z" :: nil).
+  reflexivity.
 Qed.
 
 Definition loop_left := Eval compute in
@@ -171,8 +184,8 @@ Definition loop_left := Eval compute in
                                                           (arg_var "o"))))
          startType startStack).
 Goal loop_left =
-Return (instruction * Datatypes.list string)
-  (SEQ (SEQ (DIG 2) (LOOP_LEFT (SEQ (DUG 2) (SEQ (SEQ (SEQ (DIG 2) (LEFT (Comparable_type nat))) (DUG 2)) (DIG 2))))) (DROP 1),
+Return (instruction_seq * Datatypes.list string)
+  ({DIG 2; LOOP_LEFT {DUG 2; DIG 2; LEFT nat; DUG 2; DIG 2}; DROP 1},
    "b" :: "m" :: "v" :: "x" :: "y" :: "z" :: nil).
   reflexivity.
 Qed.
@@ -184,8 +197,8 @@ Definition loop_bool := Eval compute in
                                                 (arg_value (val_rval (rval_record nil))))))
          startType startStack).
 Goal loop_bool =
-Return (instruction * Datatypes.list string)
-       (SEQ (DIG 0) (LOOP (SEQ (SEQ (SEQ (PUSH unit Unit) (SEQ (DROP 1) (PUSH (Comparable_type bool) True_))) (DUG 0)) (DIG 0))),
+Return (instruction_seq * Datatypes.list string)
+       ({DIG 0; LOOP {PUSH unit Unit; DROP 1; PUSH bool True_; DUG 0; DIG 0}},
         "m" :: "or" :: "v" :: "x" :: "y" :: "z" :: nil).
   reflexivity.
 Qed.
@@ -203,11 +216,12 @@ Definition type_and_fun_def := Eval compute in
         )))))).
 Goal type_and_fun_def =
 Return (Datatypes.list (string * type * instruction * type))
-  (("f0", Comparable_type int, LEFT (Comparable_type nat), or (Comparable_type int) (Comparable_type nat))
-   :: ("f1", pair (Comparable_type int) (Comparable_type int),
-      SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR))) (SEQ (SEQ (DIG 1) (LEFT (Comparable_type nat))) (SEQ (DIG 1) PAIR)),
-      pair (Comparable_type int) (or (Comparable_type int) (Comparable_type nat))) :: nil).
-        reflexivity.
+  (("f0", (int : type), Instruction_seq {LEFT nat}, or int None nat None)
+     :: ("f1", pair int int,
+         Instruction_seq {DUP; CAR; DIP 1 {CDR}; DIP 1 NOOP; SWAP; LEFT nat; SWAP; PAIR},
+      pair int (or int None nat None)) :: nil).
+  unfold type_and_fun_def.
+    reflexivity.
 Qed.
 
 End Tests.