diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/HTLgenproof.v | 88 | ||||
-rw-r--r-- | src/hls/Verilog.v | 33 |
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 |