From 99361117f320bb809964818ca3fc85d5951df9a2 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Tue, 18 May 2021 22:02:02 +0100 Subject: Add axiom that only the main contains stores This is true due to the inlining pass. It should be checked in the translation and be added in the translation spec. --- src/hls/HTLgenproof.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'src/hls/HTLgenproof.v') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 7d71819..31d24bb 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -447,6 +447,11 @@ Section CORRECTNESS. match_states ge (RTL.Callstate rtl_stk (AST.Internal f) args mem) S -> (RTL.fn_stacksize f) = 0 \/ rtl_stk = nil. + Axiom only_main_stores : forall rtl_stk f sp pc pc' rs mem htl_stk mid m asr asa a b c d, + match_states ge (RTL.State rtl_stk f sp pc rs mem) (HTL.State htl_stk mid m pc asr asa) -> + (RTL.fn_code f) ! pc = Some (RTL.Istore a b c d pc') -> + (rtl_stk = nil /\ htl_stk = nil). + Lemma mem_free_zero : forall mem blk, Mem.free mem blk 0 0 = Some mem. Admitted. @@ -2043,7 +2048,7 @@ Section CORRECTNESS. unfold_merge. apply AssocMap.gss. - match goal with |- context[match_frames] => admit end. + edestruct only_main_stores; eauto; subst; constructor. (** Equality proof *) @@ -2325,7 +2330,7 @@ Section CORRECTNESS. unfold_merge. apply AssocMap.gss. - match goal with |- context[match_frames] => admit end. + edestruct only_main_stores; eauto; subst; constructor. (** Equality proof *) assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. @@ -2575,7 +2580,8 @@ Section CORRECTNESS. unfold_merge. apply AssocMap.gss. - match goal with |- context[match_frames] => admit end. + (** Match frames *) + edestruct only_main_stores; eauto; subst; constructor. (** Equality proof *) @@ -2754,7 +2760,7 @@ Section CORRECTNESS. Unshelve. all: try (exact tt); auto. - Admitted. + Qed. Hint Resolve transl_istore_correct : htlproof. Lemma transl_icond_correct: -- cgit