Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (hashed in ra rf) (#28)

Fix flatten hashing in the wrong table

veriT now has a happy ending

added a debug_coq file

5 files changed, 122 insertions, 48 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 58793b6..43365ef 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -683,9 +683,9 @@ let get_arguments concl =
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
-let make_proof call_solver env rt ro ra' rf' l' ls_smtc =
-  let root = SmtTrace.mkRootV [l'] in
-  call_solver env rt ro ra' rf' (root,l') ls_smtc
+let make_proof call_solver env rt ro ra' rf' l ls_smtc =
+  let root = SmtTrace.mkRootV [l] in
+  call_solver env rt ro ra' rf' (root,l) ls_smtc
 (* TODO: not generic anymore, the "lemma" part is currently specific to veriT *)
 
 (* <of_coq_lemma> reifies the coq lemma given, we can then easily print it in a
@@ -755,21 +755,22 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
     if ((Term.eq_constr b (Lazy.force ctrue)) ||
         (Term.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
-      let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
-      let l' =
-        if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
-      let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+      let nl = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
+      let lsmt = Form.flatten rf nl :: lsmt in
+      let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
       build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma)
     else
       let l1 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
+      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
       let l2 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf b in
-      let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
-      let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
-      let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' b in
-      let l' = Form.neg (Form.get rf' (Fapp(Fiff,[|l1';l2'|]))) in
-      let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+      let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' b in
+      let l = Form.get rf (Fapp(Fiff,[|l1;l2|])) in
+      let nl = Form.neg l in
+      let lsmt = Form.flatten rf nl :: lsmt in
+      let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
       build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2)
-        (Form.to_coq l) max_id_confl (vm_cast env) (Some find_lemma) in
+        (Form.to_coq nl) max_id_confl (vm_cast env) (Some find_lemma) in
 
       let cuts = (SmtBtype.get_cuts rt) @ cuts in
 
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 6406500..32f76f1 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -94,9 +94,9 @@ let import_trace ra' rf' filename first lsmt =
           let to_add =
             (match first, !cfirst.value with
              | Some (root, l), Some [fl] when init_index fl = 1 && not (Form.equal l (re_hash fl)) ->
-                let cfirst_value = !cfirst.value in
-                !cfirst.value <- root.value;
-                [Other (ImmFlatten (root, fl)), cfirst_value, !cfirst]
+                 let cfirst_value = !cfirst.value in
+                 !cfirst.value <- root.value;
+                 [Other (ImmFlatten (root, fl)), cfirst_value, !cfirst]
              | _ -> []) @ to_add in
        match to_add with
        | [] -> ()
@@ -171,11 +171,9 @@ let export out_channel rt ro lsmt =
 
   Format.fprintf fmt "(check-sat)\n(exit)@."
 
+exception Non_empty_warnings
 
 let call_verit _ rt ro ra' rf' first lsmt =
-  let (_, l') = first in
-  let fl' = Form.flatten rf' l' in
-  let lsmt = fl'::lsmt in
   let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
   export outchan rt ro lsmt;
   close_out outchan;
@@ -189,23 +187,25 @@ let call_verit _ rt ro ra' rf' first lsmt =
   let t1 = Sys.time () in
   Format.eprintf "Verit = %.5f@." (t1-.t0);
 
-  (* TODO: improve readability: remove the three nested try *)
   let win = open_in wname in
+
+  let assert_empty_warnings () =
+    try let _ = input_line win in raise Non_empty_warnings
+    with End_of_file -> () in
+
   try
-    if exit_code <> 0 then
-      failwith ("Verit.call_verit: command " ^ command ^
-	          " exited with code " ^ string_of_int exit_code);
-
-    try let _ = input_line win in
-        Structures.error "veriT returns 'unknown'"
-    with End_of_file ->
-          try
-            let res = import_trace ra' rf' logfilename (Some first) lsmt in
-            close_in win; Sys.remove wname; res
-          with
+    assert (exit_code = 0);
+    assert_empty_warnings ();
+    let res = import_trace ra' rf' logfilename (Some first) lsmt in
+    close_in win; Sys.remove wname; res
+  with x -> close_in win; Sys.remove wname;
+            match x with
+            | Assert_failure _ ->
+                failwith ("Verit.call_verit: command " ^ command ^
+	                    " exited with code " ^ string_of_int exit_code)
+            | Non_empty_warnings -> Structures.error "veriT returns 'unknown'"
             | VeritSyntax.Sat -> Structures.error "veriT found a counter-example"
-  with x -> close_in win; Sys.remove wname; raise x
-
+            | _ -> raise x
 
 let verit_logic =
   SL.of_list [LUF; LLia]
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index c4427b7..32e03f8 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -575,7 +575,7 @@ let init_index lsmt re_hash =
   let find = Hashtbl.find form_index_init_rank in
   let rec walk rank = function
     | [] -> ()
-    | h::t -> add (Form.to_lit h) rank;
+    | h::t -> add (Form.to_lit (re_hash h)) rank;
               walk (rank+1) t in
   walk 1 lsmt;
   fun hf -> let re_hf = re_hash hf in
@@ -584,7 +584,7 @@ let init_index lsmt re_hash =
               let oc = open_out "/tmp/input_not_found.log" in
               let fmt = Format.formatter_of_out_channel oc in
               List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt h) lsmt;
-              Format.fprintf fmt "\n%a\n" hform_to_smt re_hf;
+              Format.fprintf fmt "\n%a\n@." hform_to_smt re_hf;
               flush oc; close_out oc;
               failwith "not found: log available"
 
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index cfb8f16..9117864 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -1040,12 +1040,12 @@ Lemma taut4 :
   forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0.
 Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed.
 
-(* Lemma test_eq_sym a b : implb (a =? b) (b =? a). *)
-(* Proof. verit. *)
+Lemma test_eq_sym a b : implb (a =? b) (b =? a).
+Proof. verit. Qed.
 
-(* Lemma taut5 : *)
-(*   forall f, 0 =? f 2 -> f 2 =? 0. *)
-(* Proof. intros f p. verit_bool_base p; vauto. Qed. *)
+Lemma taut5 :
+  forall f, 0 =? f 2 -> f 2 =? 0.
+Proof. intros f p. verit_bool_base p; vauto. Qed.
 
 Lemma fun_const_Z :
   forall f , (forall x, f x =? 2) ->
@@ -1101,14 +1101,14 @@ Proof. intros x H. verit_bool_base H; vauto. Qed.
 Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x).
 Proof. intros x H. verit_bool_base H; vauto. Qed.
 
-(* Lemma un_menteur (a b c d : Z) dit: *)
-(*   dit a =? c -> *)
-(*   dit b =? d -> *)
-(*   (d =? a) || (b =? c) -> *)
-(*   (a =? c) || (a =? d) -> *)
-(*   (b =? c) || (b =? d) -> *)
-(*   a =? d. *)
-(* Proof. intros H1 H2 H3 H4 H5. verit_bool_base H1 H2 H3 H4 H5; vauto. Qed. *)
+Lemma un_menteur (a b c d : Z) dit:
+  dit a =? c ->
+  dit b =? d ->
+  (d =? a) || (b =? c) ->
+  (a =? c) || (a =? d) ->
+  (b =? c) || (b =? d) ->
+  a =? d.
+Proof. intros H1 H2 H3 H4 H5. verit_bool_base H1 H2 H3 H4 H5; vauto. Qed.
 
 Lemma const_fun_is_eq_val_0 :
   forall f : Z -> Z,
diff --git a/unit-tests/debug_coq b/unit-tests/debug_coq
new file mode 100644
index 0000000..61b9fd9
--- /dev/null
+++ b/unit-tests/debug_coq
@@ -0,0 +1,73 @@
+(* This file is useful when the tactic goes through but not hte Qed *)
+(* It is works as is for standard-coq and checker_b but can be adapted for native-coq and/or checker_eq *)
+(* Paste the environment and the following code : *)
+
+
+Definition l := TO_FILL. (* find l in the expression <checker_b l b c> *)
+Definition nclauses := let (nclauses, _, _) := c in nclauses. (* different in native-coq *)
+Definition confl := let (_, _, confl) := c in confl. (* different in native-coq *)
+Definition t := let (_, t, _) := c in t. (* different in native-coq *)
+
+
+Definition nl := Lit.neg l.
+Definition d := PArray.make nclauses nl.
+Definition s := add_roots (S.make nclauses) d None.
+
+Compute (checker_b l true c).
+Compute (checker (PArray.make nclauses nl) None c).
+
+Compute (Form.check_form t_form).
+Compute (Atom.check_atom t_atom).
+Compute (Atom.wt t_i t_func t_atom).
+Compute (euf_checker (* t_atom t_form *) C.is_false s t confl).
+
+(* Check where the false comes from, if its the last one it means the certificate is wring *)
+(* To find what rule is causing this, use : *)
+
+
+
+Definition flatten {A : Type} (trace : _trace_ A) :=
+  let (t0, _) := t in t0.
+
+(* INSTEAD in native-coq, use : *)
+(* Definition flatten {A : Type} (trace : _trace_ A) := *)
+(*   PArray.fold_left (fun l_step arr_step => l_step ++ PArray.to_list arr_step) *)
+(*                    nil trace. *)
+
+Import ListNotations.
+Fixpoint firsts {A : Type} (n : nat) (l : list A) :=
+  match n with
+  | O => []
+  | S n => match l with
+           | [] => []
+           | he :: ta => he :: firsts n ta end end.
+
+Definition step_euf := @step_checker t_i t_func t_atom t_form.
+Definition l_t := flatten t.
+
+
+Definition up_to n := List.fold_left step_euf (firsts n l_t) s.
+Definition nth n := List.nth (n-1) l_t (ImmBuildProj t_func t_atom t_form 99 99 99).
+
+Compute (List.length l_t).
+
+
+Compute (up_to 0).
+Compute (up_to 1).
+Compute (up_to 2).
+
+Compute (up_to 3).
+Compute (up_to 4).
+Compute (up_to 5).
+Compute (up_to 6).
+Compute (nth 6).
+
+Compute (up_to 7).
+Compute (up_to 8).
+Compute (up_to 9).
+Compute (nth 9).
+Compute (up_to 10).
+Compute (nth 10).
+
+Compute (Zpos (xO (xO (xI xH)))).
+