diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:05:03 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:05:03 +0200 |
| commit | 3d87236deffbcbfd8d56a9080482071602f9ea01 (patch) | |
| tree | a869f7cb9f385a16b1aedd95ad3b4f66b6921025 /backend/Injectproof.v | |
| parent | e4c053f3ddfb8fbea125ba5100293e013900d0b1 (diff) | |
| download | compcert-kvx-3d87236deffbcbfd8d56a9080482071602f9ea01.tar.gz compcert-kvx-3d87236deffbcbfd8d56a9080482071602f9ea01.zip | |
fewer admits
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 0a53dc9f..7ba4b9f7 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1214,6 +1214,15 @@ Section INJECTOR. trivial. Qed. + Lemma match_regs_setres: + forall f res rs trs vres + (MATCH : match_regs f rs trs), + match_regs f (regmap_setres res vres rs) (regmap_setres res vres trs). + Proof. + induction res; simpl; intros; trivial. + apply match_regs_write; auto. + Qed. + Lemma transf_function_preserves_ros: forall f tf pc rs trs ros args res fd pc' sig (FUN : transf_function gen_injections f = OK tf) @@ -1594,7 +1603,8 @@ Section INJECTOR. ** symmetry. apply E0_right. * constructor; trivial. apply match_regs_trans with (rs2 := (regmap_setres res vres trs)); trivial. - admit. + apply match_regs_setres. + assumption. + econstructor; split. * eapply Smallstep.plus_one. apply exec_Ibuiltin with (ef := ef) (args := args) (res := res) (vargs := vargs). |