From 0ab8ac00f15373b02487f8988da1b0828ba02801 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Thu, 30 Sep 2021 13:37:34 +0100 Subject: Complete alloc/free zero proofs --- src/hls/HTLgenproof.v | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'src/hls') diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 97b7227..195937c 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -489,11 +489,15 @@ Lemma mem_alloc_zero_load : forall mem mem' blk chunk sp ptr, Mem.alloc mem 0 0 = (mem', blk) -> Mem.load chunk mem sp ptr = Mem.load chunk mem' sp ptr. Proof. + Transparent Mem.load. intros. - destruct (Mem.load chunk mem sp ptr) eqn:E; symmetry. - - eauto using Mem.load_alloc_other. - - admit. -Admitted. + destruct (Mem.load chunk mem sp ptr) eqn:E. + - hauto lq: on use: Mem.load_alloc_other. + - unfold Mem.load in *. + destruct (Mem.valid_access_dec mem _ _ _ _), (Mem.valid_access_dec mem' _ _ _ _); crush. + eapply Mem.valid_access_alloc_inv in H; eauto. + destruct (Values.eq_block _ _), chunk; crush. +Qed. Lemma mem_alloc_zero_loadv : forall mem mem' blk chunk ptr, Mem.alloc mem 0 0 = (mem', blk) -> @@ -510,11 +514,14 @@ Lemma mem_alloc_zero_store : forall mem mem' blk chunk sp ofs v, Mem.store chunk mem sp ofs v = None -> Mem.store chunk mem' sp ofs v = None. Proof. - Transparent Mem.alloc. + Transparent Mem.store. intros. - unfold Mem.alloc in *. - inv H. -Admitted. + unfold Mem.store in *. + destruct (Mem.valid_access_dec mem _ _ _ _), (Mem.valid_access_dec mem' _ _ _ _); crush. + exfalso. + eapply Mem.valid_access_alloc_inv in H; eauto. + destruct (Values.eq_block _ _), chunk; crush. +Qed. Lemma mem_alloc_zero_storev : forall mem mem' blk chunk ptr v, Mem.alloc mem 0 0 = (mem', blk) -> -- cgit