diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-09-03 15:29:31 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-09-03 15:29:31 +0200 |
| commit | 642e5873b55877be08a24e201e0aad56d3ffc3bb (patch) | |
| tree | 01420e7d486b4d755938880b15d7a21b87d9947c /kvx | |
| parent | 0fef148ea767281afc3fb8248bee0420f431f9aa (diff) | |
| download | compcert-kvx-642e5873b55877be08a24e201e0aad56d3ffc3bb.tar.gz compcert-kvx-642e5873b55877be08a24e201e0aad56d3ffc3bb.zip | |
Proof of hsilocal_simu_core_correct junk
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 342c9f30..8cb45c55 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -684,8 +684,7 @@ Proof. ++ unfold seval_sval_partial. assert (seval_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). { unfold hsi_sreg_eval. rewrite HST2. reflexivity. } - rewrite H. clear H. (*assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. - destruct TODO as (hv & HGET2). rewrite hsi_sreg_eval_correct; [|eassumption].*) + rewrite H. clear H. unfold hsi_sreg_eval. rewrite HST2. erewrite hseval_preserved; [| eapply GFS]. unfold hsi_sreg_eval in B. @@ -694,11 +693,8 @@ Proof. rewrite HST2 in B. rewrite B, RSEQ. reflexivity. - ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. admit. (* FIXME *) -(* assert (TODO: exists hv, hsi_sreg_get hst1 r ~~> hv) by admit. - destruct TODO as (hv & HGET1). rewrite hsi_sreg_eval_correct; [|eassumption]. - rewrite <- C in HGET1; [|assumption]. rewrite <- hsi_sreg_eval_correct; [|eassumption]. - unfold hsi_sreg_eval. rewrite HST2. reflexivity. *) + ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. + unfold hsi_sreg_eval. rewrite <- C; [|assumption]. rewrite HST2. reflexivity. - constructor; [|constructor]. + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _). @@ -706,13 +702,19 @@ Proof. rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. erewrite hsmem_eval_preserved; [| eapply GFS]. rewrite MEMEQ1; auto. + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _). - destruct CORE as (_ & C & _). rewrite <- A; auto. admit. (* FIXME *) -(* assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. destruct TODO as (hv & HGET2). - rewrite hsi_sreg_eval_correct; [|eassumption]. - rewrite C in HGET2; [|auto]. erewrite hseval_preserved; [| eapply GFS]. - rewrite <- hsi_sreg_eval_correct; [|eassumption]. - rewrite B; auto. - *)Admitted. (** FIXME - requires to add some hypothesis that hsi_sreg_get may return something *) + destruct CORE as (_ & C & _). rewrite <- A; auto. + unfold hsi_sreg_eval. destruct (hst2 ! r) eqn:HST2. + ++ assert (seval_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). { + unfold hsi_sreg_eval. rewrite HST2. reflexivity. } + rewrite H. clear H. + unfold hsi_sreg_eval. rewrite HST2. + erewrite hseval_preserved; [| eapply GFS]. + unfold hsi_sreg_eval in B. + generalize (B HOK1 r); clear B; intro B. + rewrite <- C in B; eauto. rewrite HST2 in B. rewrite B, RSEQ. reflexivity. + ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. + unfold hsi_sreg_eval. rewrite <- C; [|auto]. rewrite HST2. reflexivity. +Qed. Definition hsilocal_simu_check hst1 hst2 : ?? unit := phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";; |