wip strCmp

LiveVerif/src/LiveVerif/LiveProgramLogic.v

@@ -255,11 +255,9 @@ Ltac2 filtered_bottom_up_simpl_in_hyp_of_type(h: ident)(t: constr): unit :=
     | _ => bottom_up_simpl_in_hyp_of_type silent_if_no_progress h t
     end.
 
-Ltac2 default_simpl_in_hyps () :=
-  repeat (foreach_hyp filtered_bottom_up_simpl_in_hyp_of_type);
-  try record.simp_hyps ().
+Ltac bsimpl_in_hyps := ltac2:(foreach_hyp filtered_bottom_up_simpl_in_hyp_of_type).
 
-Ltac default_simpl_in_hyps := ltac2:(default_simpl_in_hyps ()).
+Ltac default_simpl_in_hyps := bsimpl_in_hyps; try record.simp_hyps.
 
 Ltac default_simpl_in_all :=
   default_simpl_in_hyps; bottom_up_simpl_in_goal_nop_ok; try record.simp_goal.

LiveVerif/src/LiveVerifExamples/nt_uint8_string.v

@@ -160,6 +160,8 @@ Derive strCmp SuchThat (fun_correct! strCmp) As strCmp_ok.
   set (p2_pre := p2) in *. change p2_pre with p2 at 1. move p2_pre before p1_pre.
   prove (\[p1 ^- p1_pre] <= len s1).
   prove (\[p2 ^- p2_pre] <= len s2).
+  prove (\[p1 ^- p1_pre] = \[p2 ^- p2_pre]).
+  prove (s1[:\[p1 ^- p1_pre]] = s2[:\[p2 ^- p2_pre]]).
   clearbody p1_pre p2_pre.
 
   move p1 after c2. move p2 after p1.
@@ -171,26 +173,23 @@ Derive strCmp SuchThat (fun_correct! strCmp) As strCmp_ok.
     p2 = p2 + 1;                                                           /**. .**/
   } while (c1 == c2 && c1 != 0);                                           /**.
 
-
-  1-3: assert (\[p1' ^- p1_pre] <> len s1)
-         by (zify_goal; intro; bottom_up_simpl_in_hyps; congruence).
-  1-3: assert (\[p2' ^- p2_pre] <> len s2)
-         by (zify_goal; intro; bottom_up_simpl_in_hyps; congruence).
+  1-4: assert (\[p1' ^- p1_pre] <> len s1)
+         by (zify_goal; intro; bsimpl_in_hyps; congruence).
+  1-4: assert (\[p2' ^- p2_pre] <> len s2)
+         by (zify_goal; intro; bsimpl_in_hyps; congruence).
   1: solve [steps].
   1: solve [zify_hyps; steps].
 
-  unzify.
-  subst v.
-  subst p1.
-  zify_hyps.
-  split.
-
-  steps.
   (* TODO include in purification of array? *)
-  assert (len s1 < 2^32) by admit.
-  assert (len s2 < 2^32) by admit.
+  all: assert (len s1 < 2^32) by admit.
+  all: assert (len s2 < 2^32) by admit.
 
-  step.
+  { rewrite (List.split_at_index (s1[:\[p1 ^- p1_pre]]) (\[p1' ^- p1_pre])).
+    step. step. congruence.
+    (* TODO diff between slice start and end is 1 *)
+    admit. }
+
+  solve [step].
 
                                                                                 .**/
   uintptr_t res = c1 - c2;                                                 /**. .**/
@@ -215,9 +214,18 @@ Derive strCmp SuchThat (fun_correct! strCmp) As strCmp_ok.
 
   destr (\[p1' ^- p1_pre] =? len s1);
   destr (\[p2' ^- p2_pre] =? len s2);
-  fwd; zify_hyps; bottom_up_simpl_in_hyps.
-
-  (* TODO add clause to invariant that says "same up to (p1' ^- p1_pre)" *)
+  fwd; zify_hyps; bsimpl_in_hyps.
+  - subst s1. admit. (* List.compare_refl *)
+  - unzify. rewrite (List.split_at_index s2 \[p2' ^- p2_pre]).
+    let h := constr:(#(s1 = ??)) in rewrite <- h.
+    admit. (* List.compare_l_is_prefix *)
+  - unzify. rewrite (List.split_at_index s1 \[p1' ^- p1_pre]).
+    let h := constr:(#(?? = s2)) in rewrite h.
+    admit. (* List.compare_r_is_prefix *)
+  - unzify.
+    rewrite (List.split_at_index s2 \[p2' ^- p2_pre]).
+    rewrite (List.split_at_index s1 \[p1' ^- p1_pre]).
+    admit. (* List.compare_common_prefix *)
 Abort.
 
 #[export] Instance strcmp_spec: fnspec :=                                       .**/
@@ -256,8 +264,8 @@ Derive strcmp SuchThat (fun_correct! strcmp) As strcmp_ok.
 
     new_ghosts(s1[1:], s2[1:], p1, p2, _).
 
-    assert (len s1 <> 0) by (intro; bottom_up_simpl_in_hyps; congruence).
-    assert (len s2 <> 0) by (intro; bottom_up_simpl_in_hyps; congruence).
+    assert (len s1 <> 0) by (intro; bsimpl_in_hyps; congruence).
+    assert (len s2 <> 0) by (intro; bsimpl_in_hyps; congruence).
 
     steps.
 
@@ -267,7 +275,7 @@ Derive strcmp SuchThat (fun_correct! strcmp) As strcmp_ok.
                eapply array1_to_elem' in H;
                [ new_mem_hyp H | zify_goal; xlia zchecker ]
            end.
-    bottom_up_simpl_in_hyps.
+    bsimpl_in_hyps.
     steps.
 
                                                                                 .**/
@@ -283,7 +291,7 @@ Derive strcmp SuchThat (fun_correct! strcmp) As strcmp_ok.
         bottom_up_simpl_in_hyp A;
         specialize (A ltac:(lia))).
 
-  destruct s1; destruct s2; simpl; symmetry; fwd; bottom_up_simpl_in_hyps;
+  destruct s1; destruct s2; simpl; symmetry; fwd; bsimpl_in_hyps;
     zify_hyps; steps.
   destruct_one_match; zify_hyps; steps.
 Qed.

bedrock2/src/bedrock2/bottom_up_simpl_perf.v

@@ -0,0 +1,62 @@
+Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+Require Import Ltac2.Ltac2. Set Default Proof Mode "Classic".
+Require Import Ltac2.Printf.
+Require Import coqutil.Tactics.foreach_hyp.
+Require Import coqutil.Word.Interface coqutil.Word.Properties.
+Require Import bedrock2.bottom_up_simpl.
+Require Import bedrock2.unzify.
+
+Ltac2 filtered_bottom_up_simpl_in_hyp_of_type'(h: ident)(t: constr): unit :=
+  if Ident.starts_with @__ h then ()
+  else (printf "<infomsg>%I</infomsg>" h;
+        Control.time None
+          (fun _ => bottom_up_simpl_in_hyp_of_type silent_if_no_progress h t)).
+
+Ltac2 filtered_bottom_up_simpl_in_hyp_of_type(h: ident)(t: constr): unit :=
+  if Ident.starts_with @__ h then ()
+  else bottom_up_simpl_in_hyp_of_type silent_if_no_progress h t.
+
+Ltac2 simpl_in_hyps () := foreach_hyp filtered_bottom_up_simpl_in_hyp_of_type.
+
+Ltac simpl_in_hyps := ltac2:(simpl_in_hyps ()).
+
+Section Tests.
+
+  Context {word: word.word 32} {word_ok: word.ok word}.
+  Context {mem: Type}.
+  Hypothesis bytearray : Z -> list Z -> word -> mem -> Prop.
+
+  Add Ring wring : (Properties.word.ring_theory (word := word))
+      ((* too expensive: preprocess [autorewrite with rew_word_morphism], *)
+       morphism (Properties.word.ring_morph (word := word)),
+       constants [Properties.word_cst]).
+
+  Import ZList.List.ZIndexNotations. Local Open Scope zlist_scope.
+  Import bedrock2.WordNotations. Local Open Scope word_scope.
+
+  Goal forall (s1 s2 : list Z) (p1_pre p2_pre : word) (v : Z) (m0 m2 : mem)
+              (p1' p2' c1 c2 p1 p2 : word),
+      v = len s1 - \[p1' ^- p1_pre] ->
+      bytearray (len s1 + 1) (s1 ++ [|0|]) p1_pre m0 ->
+      bytearray (len s2 + 1) (s2 ++ [|0|]) p2_pre m2 ->
+      \[p1' ^- p1_pre] <= len s1 ->
+      \[p2' ^- p2_pre] <= len s2 ->
+      \[p1' ^- p1_pre] = \[p2' ^- p2_pre] ->
+      s1[:\[p1' ^- p1_pre]] = s2[:\[p2' ^- p2_pre]] ->
+      c1 = /[(s1 ++ [|0|])[\[p1' ^- p1_pre]]] ->
+      c2 = /[(s2 ++ [|0|])[\[p2' ^- p2_pre]]] ->
+      p1 = p1' ^+ /[1] ->
+      p2 = p2' ^+ /[1] ->
+      c1 = c2 ->
+      c1 <> /[0] ->
+      \[p1' ^- p1_pre] <> len s1 ->
+      \[p2' ^- p2_pre] = len s2 ->
+      False.
+  Proof.
+    intros.
+    zify_hyps.
+    Time simpl_in_hyps. (* 0.748 secs *)
+    (* Time bottom_up_simpl_in_hyps. 3.653 secs because it also simplifies __Z hyps *)
+    unzify.
+  Abort.
+End Tests.