Add negative edge reasoning to HTLgenproof

2 files changed, 109 insertions, 12 deletions

diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index e3b0147..3b5496f 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1736,11 +1736,21 @@ Section CORRECTNESS.
       crush.
       unfold Verilog.merge_arrs.
 
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
+      erewrite Verilog.merge_arr_empty2.
       unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
+      setoid_rewrite H7.
+      reflexivity.
+
+      rewrite AssocMap.gcombine by reflexivity.
+      unfold Verilog.merge_arr.
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       setoid_rewrite H7.
       reflexivity.
@@ -1748,12 +1758,23 @@ Section CORRECTNESS.
       rewrite combine_length.
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
+      symmetry.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite H4.
+      apply list_repeat_len.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
+      rewrite H4.
+      apply list_repeat_len.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
@@ -2015,11 +2036,21 @@ Section CORRECTNESS.
       crush.
       unfold Verilog.merge_arrs.
 
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
+      erewrite Verilog.merge_arr_empty2.
       unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
+      setoid_rewrite H7.
+      reflexivity.
+
+      rewrite AssocMap.gcombine by reflexivity.
+      unfold Verilog.merge_arr.
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       setoid_rewrite H7.
       reflexivity.
@@ -2027,12 +2058,23 @@ Section CORRECTNESS.
       rewrite combine_length.
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
+      symmetry.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
+      rewrite H4.
+      apply list_repeat_len.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite H4.
+      apply list_repeat_len.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int
@@ -2264,11 +2306,21 @@ Section CORRECTNESS.
       crush.
       unfold Verilog.merge_arrs.
 
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
+      erewrite Verilog.merge_arr_empty2.
       unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gcombine by reflexivity.
       rewrite AssocMap.gss.
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H7.
+      reflexivity.
+
+      rewrite AssocMap.gcombine by reflexivity.
       unfold Verilog.merge_arr.
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       setoid_rewrite H7.
       reflexivity.
@@ -2276,12 +2328,23 @@ Section CORRECTNESS.
       rewrite combine_length.
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
+      symmetry.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
+      rewrite H4.
+      apply list_repeat_len.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite H4.
+      apply list_repeat_len.
 
       remember i0 as OFFSET.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
@@ -2576,6 +2639,7 @@ Section CORRECTNESS.
       apply HTL.step_finish.
       unfold Verilog.merge_regs.
       unfold_merge.
+      unfold_merge.
       rewrite AssocMap.gso.
       apply AssocMap.gss. simpl; lia.
       apply AssocMap.gss.
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 8e14267..48f3084 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -76,6 +76,39 @@ Definition merge_arr (new : option arr) (old : option arr) : option arr :=
 Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
   AssocMap.combine merge_arr new old.
 
+Lemma merge_arr_empty':
+  forall l,
+  merge_arr (Some (arr_repeat None (length l))) (Some (make_array l)) = Some (make_array l).
+Proof.
+  induction l; auto.
+  unfold merge_arr.
+  unfold combine, make_array. simplify. rewrite H0.
+  rewrite list_repeat_cons. simplify.
+  rewrite H0; auto.
+Qed.
+
+Lemma merge_arr_empty:
+  forall v l,
+  v = Some (make_array l) ->
+  merge_arr (Some (arr_repeat None (length l))) v = v.
+Proof. intros. rewrite H. apply merge_arr_empty'. Qed.
+
+Lemma merge_arr_empty2:
+  forall v l v',
+  v = Some v' ->
+  l = arr_length v' ->
+  merge_arr (Some (arr_repeat None l)) v = v.
+Proof.
+  intros. subst. destruct v'. simplify.
+  generalize dependent arr_wf. generalize dependent arr_length.
+  induction arr_contents.
+  - simplify; subst; auto.
+  - unfold combine, make_array in *; simplify; subst.
+    rewrite list_repeat_cons; simplify.
+    specialize (IHarr_contents (Datatypes.length arr_contents) eq_refl).
+    inv IHarr_contents. rewrite H0. rewrite H0. auto.
+Qed.
+
 Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
   | None => None