diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-18 22:02:02 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-18 22:03:16 +0100 |
| commit | 99361117f320bb809964818ca3fc85d5951df9a2 (patch) | |
| tree | a00eca067e97664a3fcd7fb42e57ec18a3069919 /src/hls/HTLgenproof.v | |
| parent | deb5fabefb2b67d46f1df6efc08c217c5197338a (diff) | |
| download | vericert-99361117f320bb809964818ca3fc85d5951df9a2.tar.gz vericert-99361117f320bb809964818ca3fc85d5951df9a2.zip | |
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.
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 14 |
1 files changed, 10 insertions, 4 deletions
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: |