add cancel tactic which cancels everything which is definitely safe t…

…o cancel and

leaves the remaining formula as an open goal, which is useful for debugging.
Also add cancel_emp_l and cancel_emp_r tactics, which seem to work in Array.v,
but do not yet work in FlatToRiscv.v.

bedrock2/src/Array.v

@@ -24,8 +24,7 @@ Section Array.
     { (* TODO(lemma): skipn_all *)
       pose proof (firstn_skipn n xs) as H0.
       rewrite firstn_all2 in * by assumption.
-      rewrite <-app_nil_r in H0; apply app_inv_head in H0; rewrite H0; cbn.
-      (* FIXME *) ecancel. rewrite sep_emp_True_l. ecancel. }
+      rewrite <-app_nil_r in H0; apply app_inv_head in H0; rewrite H0; cbn. ecancel. }
     rewrite <-(firstn_skipn n xs) at 1.
     replace a with (word.add start (word.mul (word.of_Z (Z.of_nat (length (firstn n xs)))) size)); cycle 1.
     { subst a. rewrite firstn_length_le by Lia.lia. trivial. }

bedrock2/src/Map/SeparationLogic.v

@@ -153,6 +153,21 @@ Section SepProperties.
     rewrite <-(seps_nth_to_head i xs), <-(seps_nth_to_head j ys), Hij, Hrest.
     exact (reflexivity _).
   Qed.
+  Lemma cancel_emp_at_index_l i xs ys
+        (Hi : iff1 (nth i xs) (emp True))
+        (Hrest : iff1 (seps (remove_nth i xs)) (seps ys))
+    : iff1 (seps xs) (seps ys).
+  Proof.
+    rewrite <-(seps_nth_to_head i xs), Hi, Hrest. exact (sep_emp_True_l _).
+  Qed.
+  Lemma cancel_emp_at_index_r j xs ys
+        (Hj : iff1 (nth j ys) (emp True))
+        (Hrest : iff1 (seps xs) (seps (remove_nth j ys)))
+    : iff1 (seps xs) (seps ys).
+  Proof.
+    rewrite <-(seps_nth_to_head j ys), Hj, Hrest, sep_emp_True_l.
+    exact (reflexivity _).
+  Qed.
 End SepProperties.
 
 Require Import coqutil.Tactics.syntactic_unify.
@@ -204,9 +219,43 @@ Ltac find_syntactic_unify xs y :=
   | cons _ ?xs => let i := find_syntactic_unify xs y in constr:(S i)
   end.
 
-Ltac ecancel :=
-  reify_goal;
-  repeat (
+Ltac find_constr_eq xs y :=
+  multimatch xs with
+  | cons ?x _ => constr:(ltac:(constr_eq x y; exact 0%nat))
+  | cons _ ?xs => let i := find_constr_eq xs y in constr:(S i)
+  end.
+
+Ltac cancel_emp_l :=
+  let LHS := lazymatch goal with |- Lift1Prop.iff1 (seps ?LHS) _ => LHS end in
+  let RHS := lazymatch goal with |- Lift1Prop.iff1 _ (seps ?RHS) => RHS end in
+  let i := find_constr_eq LHS constr:(emp True) in
+  simple refine (cancel_emp_at_index_l i LHS RHS _ _);
+  cbn [List.firstn List.skipn List.app List.hd List.tl];
+  [exact (RelationClasses.reflexivity _)|].
+
+Ltac cancel_emp_r :=
+  let LHS := lazymatch goal with |- Lift1Prop.iff1 (seps ?LHS) _ => LHS end in
+  let RHS := lazymatch goal with |- Lift1Prop.iff1 _ (seps ?RHS) => RHS end in
+  let j := find_constr_eq RHS constr:(emp True) in
+  simple refine (cancel_emp_at_index_r j LHS RHS _ _);
+  cbn [List.firstn List.skipn List.app List.hd List.tl];
+  [exact (RelationClasses.reflexivity _)|].
+
+Ltac cancel_step :=
+      let RHS := lazymatch goal with |- Lift1Prop.iff1 _ (seps ?RHS) => RHS end in
+      let jy := index_and_element_of RHS in
+      let j := lazymatch jy with (?i, _) => i end in
+      let y := lazymatch jy with (_, ?y) => y end in
+      assert_fails (has_evar y); (* <-- different from ecancel_step *)
+
+      let LHS := lazymatch goal with |- Lift1Prop.iff1 (seps ?LHS) _ => LHS end in
+      let i := find_constr_eq LHS y in (* <-- different from ecancel_step *)
+
+      simple refine (cancel_seps_at_indices i j LHS RHS _ _);
+      cbn [List.firstn List.skipn List.app List.hd List.tl];
+      [exact (RelationClasses.reflexivity _)|].
+
+Ltac ecancel_step :=
       let RHS := lazymatch goal with |- Lift1Prop.iff1 _ (seps ?RHS) => RHS end in
       let jy := index_and_element_of RHS in
       let j := lazymatch jy with (?i, _) => i end in
@@ -218,8 +267,20 @@ Ltac ecancel :=
 
       simple refine (cancel_seps_at_indices i j LHS RHS _ _);
       cbn [List.firstn List.skipn List.app List.hd List.tl];
-      [exact (RelationClasses.reflexivity _)|]);
-  cbn [seps]; try exact (RelationClasses.reflexivity _).
+      [exact (RelationClasses.reflexivity _)|].
+
+Ltac cancel :=
+  reify_goal;
+  repeat cancel_step;
+  repeat cancel_emp_l;
+  repeat cancel_emp_r;
+  try solve [ cbn [seps]; exact (RelationClasses.reflexivity _) ].
+
+Ltac ecancel :=
+  cancel;
+  repeat ecancel_step;
+  cbn [seps];
+  exact (RelationClasses.reflexivity _).
 
 Ltac ecancel_assumption :=
   multimatch goal with
@@ -231,6 +292,17 @@ Ltac ecancel_assumption :=
     end
   end.
 
+Ltac seplog :=
+  match goal with
+  | |- _ ?m =>
+    match goal with
+    | H: _ ?m |- _ =>
+      refine (Lift1Prop.subrelation_iff1_impl1 _ _ _ _ _ H); clear H;
+      cancel;
+      try solve [ repeat ecancel_step; cbn [seps]; exact (RelationClasses.reflexivity _) ]
+    end
+  end.
+
 Ltac seprewrite0_in Hrw H :=
   let lemma_lhs := lazymatch type of Hrw with @Lift1Prop.iff1 _ ?lhs _ => lhs end in
   let Psep := lazymatch type of H with ?P _ => P end in

compiler/src/FlatToRiscv.v

@@ -917,10 +917,11 @@ Section FlatToRiscv1.
 
     - (* SLit *)
       remember (compile_lit x v) as insts.
-      eapply compile_lit_correct_full; [sidecondition..|]; cycle 1.
-      + eassumption.
-      + simpl. run1done.
+      eapply compile_lit_correct_full.
+      + sidecondition.
       + unfold compile_stmt. unfold getPc, getMem. subst insts. ecancel_assumption.
+      + sidecondition.
+      + simpl. run1done.
 
       (* SOp *)
     - admit.
@@ -940,8 +941,23 @@ Section FlatToRiscv1.
     - (* SSet *)
       run1det. run1done.
 
-    - (* SIf/Then *) (*
+    - (* SIf/Then *)
       (* branch if cond = false (will not branch *)
+      eapply det_step.
+      {
+        simulate'.
+        {
+          simpl in *.
+          seplog.
+          Fail cancel_emp_r. (* TODO should not fail *)
+
+          admit.
+        }
+        admit.
+      }
+      admit.
+
+      (*
       eapply runsToStep; simpl in *; subst *.
       + fetch_inst.
         destruct cond; [destruct op | ]; simpl in *;
@@ -956,8 +972,9 @@ Section FlatToRiscv1.
         destruct_everything.
         run1step.
         run1done.
+       *)
 
-    - (* SIf/Else *)
+    - (* SIf/Else *) (*
       (* branch if cond = 0 (will  branch) *)
       eapply runsToStep; simpl in *; subst *.
       + fetch_inst.