diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-09-07 14:44:37 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-09-07 14:44:37 +0200 |
| commit | 7fa462ec791789cfec4327e03531efed56252937 (patch) | |
| tree | 33af2b28154aa197bd7b686eedc17d42355af437 /kvx | |
| parent | 656a2950e39a4b1dca26fce9559b19139e56cd90 (diff) | |
| download | compcert-kvx-7fa462ec791789cfec4327e03531efed56252937.tar.gz compcert-kvx-7fa462ec791789cfec4327e03531efed56252937.zip | |
hsexec_final_correct progress
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 1edfa53d..1831b3fc 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -1500,15 +1500,42 @@ Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := | _ => RET (HSnone) end. +Lemma sval_refines_local_get ge sp rs0 m0 hsl sl r: + hsok_local ge sp rs0 m0 hsl -> + hsilocal_refines ge sp rs0 m0 hsl sl -> + WHEN hsi_sreg_get hsl r ~> hsv THEN + sval_refines ge sp rs0 m0 hsv (si_sreg sl r). +Proof. + intros HOK HREF. wlp_intros hsv HSV. unfold sval_refines. + erewrite <- hsi_sreg_eval_correct; eauto. + destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption]. + reflexivity. +Qed. + +Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros: + hsok_local ge sp rs0 m0 hsl -> + hsilocal_refines ge sp rs0 m0 hsl sl -> + WHEN hsum_left hsl ros ~> svos THEN + sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros). +Proof. + intros HOK HREF. destruct ros; [| wlp_simplify]. + wlp_step_bind hr HGET. wlp_simplify. unfold sval_refines. + rewrite sval_refines_local_get; eauto. +Qed. + Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i: + hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> WHEN hsexec_final i hsl ~> hsf THEN hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl). Proof. -(* destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone). + intro HOK. + destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone). (* Scall *) - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_intros hsf HSF. - apply mayRet_ret in HSF. subst. unfold hfinal_refines. simpl. *) + apply mayRet_ret in HSF. subst. constructor. + + eapply hsum_left_correct; eauto. + + Search list_refines. admit. (* + intro. inv H. constructor; auto. @@ -1527,6 +1554,7 @@ Proof. - admit. *)Admitted. + Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit := match ln, ln' with | nil, nil => RET tt |