diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-30 14:32:22 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-30 14:32:22 +0100 |
| commit | 583f1e12247bbb3c5ede02e04020036e50464636 (patch) | |
| tree | e4d93c99e37515ab9fb6fef933a02778a0e4d5ca /src | |
| parent | 0ab8ac00f15373b02487f8988da1b0828ba02801 (diff) | |
| download | vericert-583f1e12247bbb3c5ede02e04020036e50464636.tar.gz vericert-583f1e12247bbb3c5ede02e04020036e50464636.zip | |
Prove match_arrs_empty
Diffstat (limited to 'src')
| -rw-r--r-- | src/hls/HTLgenproof.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 195937c..f320ce0 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -658,9 +658,27 @@ Section CORRECTNESS. Qed. Lemma match_arrs_empty : forall m f sp mem asa, + HTL.mod_stk_len m = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> match_arrs m f sp mem asa -> match_arrs m f sp mem (Verilog.merge_arrs (HTL.empty_stack m) asa). - Admitted. + Proof. + intros * Hstklen [? ? [Hstk [Hstklen' Hstkval]]]. + econstructor; repeat split. + - unfold Verilog.merge_arrs, HTL.empty_stack. + rewrite AssocMap.gcombine by trivial. + rewrite AssocMap.gss. + replace (_ ! _) with (Some stack). + crush. + - unfold combine, make_array. simpl. + rewrite list_combine_length, list_repeat_len, arr_wf, Hstklen, Hstklen'. + lia. + - simplify. + rewrite combine_lookup_first; eauto. + + rewrite arr_repeat_length. congruence. + + unfold arr_repeat, make_array, array_get_error. simpl. + apply list_repeat_lookup. + lia. + Qed. Lemma TRANSL' : Linking.match_program (fun cu f tf => transl_fundef prog f = Errors.OK tf) eq prog tprog. |