diff options
Diffstat (limited to 'src/hls/HTLgenproof.v')
-rw-r--r-- | src/hls/HTLgenproof.v | 100 |
1 files changed, 82 insertions, 18 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index c1298c1..c2cbbf8 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1,4 +1,4 @@ - (* +(* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * 2020 James Pollard <j@mes.dev> @@ -1131,6 +1131,7 @@ Section CORRECTNESS. Ltac tac0 := match goal with + | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge @@ -2248,7 +2249,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2284,11 +2285,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. @@ -2296,12 +2307,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 (Integers.Int.repr z))) as OFFSET. @@ -2530,7 +2552,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2565,11 +2587,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. @@ -2577,12 +2609,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 @@ -2780,7 +2823,7 @@ Section CORRECTNESS. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2817,11 +2860,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. @@ -2829,12 +2882,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 i as OFFSET. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). @@ -3014,7 +3078,7 @@ Section CORRECTNESS. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. eauto. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -3034,7 +3098,7 @@ Section CORRECTNESS. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. eauto. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. |