Merge pull request #88 from CertiCoq/certicoq-eval

Certicoq Eval command and tactic

.gitignore

@@ -130,3 +130,5 @@ bootstrap/certicoqc/META
 bootstrap/certicoqchk/META
 bootstrap/certicoqc*/glue.c
 bootstrap/certicoqc*/glue.h
+plugin/.merlin
+_build

.vscode/CertiCoq.code-workspace

@@ -6,6 +6,10 @@
  ],
  "settings": {
  "coqtop.binPath": "_opam/bin",
- "coqtop.args": []
+ "coqtop.args": [],
+ "ocaml.sandbox": {
+ "kind": "opam",
+ "switch": "coq817"
+ }
  }
 }

benchmarks/certicoq_eval.v

@@ -0,0 +1,97 @@
+From Equations Require Import Equations.
+From Coq Require Import Uint63 Wf_nat ZArith Lia Arith.
+From CertiCoq Require Import CertiCoq.
+
+(* This warns about uses of primitive operations, but we compile them fine *)
+Set Warnings "-primitive-turned-into-axiom".
+
+
+Definition inspect {A} (a : A) : {b | a = b} :=
+ exist _ a eq_refl.
+Notation " x 'eqn:' H " := (exist _ x H) (at level 20, only parsing).
+
+Section FactPrim.
+ Local Open Scope Z_scope.
+
+ Equations fact (n : int) : int 
+ by wf (Z.to_nat (to_Z n)) lt :=
+ | n with inspect (Uint63.eqb n 0) := 
+ | true eqn:_ => 1
+ | false eqn:heq => n * fact (pred n).
+ Next Obligation.
+ pose proof (to_Z_bounded n).
+ pose proof (to_Z_bounded (pred n)).
+ red.
+ eapply Uint63.eqb_false_spec in heq.
+ rewrite <- Z2Nat.inj_succ.
+ assert (φ (n)%uint63 <> 0). intros hq.
+ pose proof (of_to_Z n). rewrite hq in H1. cbn in H1. congruence.
+ 2:lia.
+ rewrite pred_spec in H0 |- *.
+ assert (to_Z n - 1 < wB)%Z. lia.
+ eapply Z2Nat.inj_le. lia. lia.
+ rewrite Z.mod_small. 2:lia. lia.
+ Qed.
+End FactPrim.
+From CertiCoq.Benchmarks Require Import sha256.
+From Coq Require Import String.
+Definition test := "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching."%string.
+
+Definition sha := sha256.SHA_256 (sha256.str_to_bytes test).
+
+Definition sha_fast := sha256.SHA_256' (sha256.str_to_bytes test).
+
+Definition sha_fast_noproofs := let x := sha_fast in tt.
+
+Time Eval vm_compute in sha_fast_noproofs.
+(* Executed in 0.004 sec *)
+
+CertiCoq Eval -time sha_fast_noproofs.
+(* Executed in 0.037175 sec *)
+
+Time CertiCoq Eval sha_fast_noproofs.
+(* Finished transaction in 0.06 sec *)
+
+CertiCoq Eval -time sha_fast_noproofs.
+(* Executed in 0.045 sec *)
+CertiCoq Eval -time sha_fast_noproofs.
+
+
+From CertiCoq.Benchmarks Require Import Color.
+
+Time Eval vm_compute in Color.main.
+
+From CertiCoq.Benchmarks Require Import vs.
+Import VeriStar.
+
+Definition vs_easy :=
+ (fix loop (n : nat) (res : veristar_result) :=
+ match n with
+ | 0%nat =>
+ match res with
+ | Valid => true
+ | _ => false
+ end
+ | S n =>
+ let res := check_entailment example_ent in
+ loop n res
+ end) 100 Valid.
+
+Definition vs_hard :=
+ match vs.main_h with
+ | vs.VeriStar.Valid => true
+ | _ => false
+ end.
+
+(* 
+(* Blows up *) Time Eval vm_compute in vs_easy.
+(* Blows up *) Time Eval vm_compute in vs_hard.
+*)
+
+CertiCoq Eval -time vs_hard.
+(* Executed in 0.06s *)
+CertiCoq Eval -time vs_hard.
+
+CertiCoq Eval -time vs_easy.
+(* Executed in 0.007s *)
+

benchmarks/certicoq_eval_issue.v

@@ -0,0 +1,45 @@
+
+From Coq Require Import List Arith Extraction Lia.
+Notation "( x ; p )" := (exist _ x p).
+Example nth {A} (l : list A) : {n : nat | n < length l} -> A.
+Proof.
+ intros n.
+ induction l as [|l' Hl'].
+ - destruct n as [n Hn].
+ simpl in Hn.
+ apply False_rect.
+ inversion Hn.
+ Set Printing Notations.
+ - destruct n as [n Hn].
+ destruct n as [|n'].
+ + (* 0 *)
+ exact l'.
+ + (* S n' *)
+ apply IHHl'.
+ exists n'.
+ simpl in Hn.
+ apply Nat.succ_lt_mono. apply Hn.
+Defined.
+
+Print nth.
+
+Extraction nth.
+
+From CertiCoq.Plugin Require Import CertiCoq.
+
+Import ListNotations.
+Definition l : list nat := map (fun x => x * x) (repeat 3 45000).
+
+Lemma nth_l : 30000 < length l.
+Proof. unfold l. rewrite map_length. rewrite repeat_length. Admitted.
+
+Definition test : nat := (nth l (30000; nth_l)).
+(* Time Eval vm_compute in test. *)
+(* 30 seconds, includes cost of building the intermediate n < length proofs *)
+(* Stack overflowing? *)
+(* CertiCoq Eval -debug -time test. *)
+Definition largenat := 45000.
+(* Stack overflowing? *)
+
+Definition llength := length l.
+CertiCoq Eval -debug -time llength.

benchmarks/test_primfloat.v

@@ -1,6 +1,6 @@
 
 From CertiCoq.Plugin Require Import CertiCoq.
-From MetaCoq Require Import utils.
+From MetaCoq.Utils Require Import utils.
 From CertiCoq.Common Require Import Pipeline_utils.
 
 Open Scope bs_scope.
@@ -14,7 +14,7 @@ Definition string_of_bool b :=
 #[export] Instance bool_show : Show bool := string_of_bool.
 
 #[export] Instance list_show {A} {SA : Show A} : Show (list A) := string_of_list show.
-From MetaCoq Require Import Primitive.
+From MetaCoq.Common Require Import Primitive.
 From Coq Require Import PrimFloat PrimInt63.
 #[export] Instance float_show : Show PrimFloat.float := string_of_float.
 #[export] Instance prim_int_show : Show PrimInt63.int := string_of_prim_int.
@@ -39,4 +39,6 @@ Definition certicoqc2 :=
  coq_msg_info (show (0%float == (-0)%float)).
 
 Time Eval compute in certicoqc2.
+
+Set Warnings "-primitive-turned-into-axiom".
 Time CertiCoq Run certicoqc2.

benchmarks/test_primitive.v

@@ -1,4 +1,5 @@
-From MetaCoq Require Import bytestring MCString Primitive.
+From MetaCoq.Utils Require Import bytestring MCString. 
+From MetaCoq.Common Require Import Primitive.
 From CertiCoq.Plugin Require Import CertiCoq.
 From Coq Require Import Uint63 ZArith.
 Open Scope bs.

cplugin/_CoqProject

@@ -468,5 +468,3 @@ extraction/zbool.ml
 extraction/zbool.mli
 extraction/zpower.ml
 extraction/zpower.mli
-extraction/optionMonad.mli
-extraction/optionMonad.ml

cplugin/certicoq.ml

@@ -280,8 +280,9 @@ let make_pipeline_options (opts : options) =
  let dev = coq_nat_of_int opts.dev in
  let prefix = bytestring_of_string opts.prefix in
  let prims = get_global_prims () @ opts.prims in
+ let name = bytestring_of_string "body" in
  (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *)
- Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix prims
+ Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix name prims
 
 
 (** Main Compilation Functions *)

plugin/CoqMsgFFI.v

@@ -11,4 +11,4 @@ CertiCoq Register [
  coq_msg_notice => "coq_msg_notice",
  coq_msg_debug => "coq_msg_debug",
  coq_user_error => "coq_user_error" ]
-Include [ "coq_c_ffi.h" as library ].
+Include [ "coq_ffi.h" as library ].

plugin/Makefile.local

@@ -8,8 +8,16 @@ CAMLFLAGS+=-w -39 # Unused rec flagss
 CAMLFLAGS+=-w -20 # Unused arguments
 CAMLFLAGS+=-w -60 # Unused functor arguments
 CAMLFLAGS+=-w -8 # Non-exhaustive matches produced by extraction
+CAMLFLAGS+=-w -37 # Unused constructor
 
 CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims
 
+CC=$(shell which gcc || which clang-11)
+
 merlin-hook::
- $(HIDE)echo 'FLG $(OPENS)' >> .merlin
+ $(HIDE)echo 'FLG $(OPENS)' >> .merlin
+
+get_ordinal.o: get_ordinal.c
+ $(CC) -c -o $@ -I runtime $<
+
+certicoq_plugin.cmxs: get_ordinal.o

plugin/Makefile.local-late

@@ -0,0 +1,4 @@
+# CAMLOPTLINK = "$(OCAMLFIND)" opt -linkall get_ordinal.o
+
+certicoq_plugin.cmxa: certicoq_plugin.cmx
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $<