diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:45:34 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:45:34 +0100 |
| commit | 0892b99d00aac6ad9f7467f1383fe5dc1b45e94f (patch) | |
| tree | f3415a55149b8ab2af86c08b2c9bfee699b835ab /backend/CSE3analysisproof.v | |
| parent | 9cf4ca7760982b40e5721b2d6510eae0ced248a8 (diff) | |
| download | compcert-kvx-0892b99d00aac6ad9f7467f1383fe5dc1b45e94f.tar.gz compcert-kvx-0892b99d00aac6ad9f7467f1383fe5dc1b45e94f.zip | |
eq_find_sound
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 027a874a..4fa093c6 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -373,4 +373,20 @@ Section SOUNDNESS. Qed. Hint Resolve kill_mem_sound : cse3. + + Theorem eq_find_sound: + forall no eq id, + eq_find (ctx := ctx) no eq = Some id -> + eq_catalog ctx id = Some eq. + Proof. + unfold eq_find. + intros. + destruct (eq_find_oracle ctx no eq) as [ id' | ]. + 2: discriminate. + destruct (eq_catalog ctx id') as [eq' |] eqn:CATALOG. + 2: discriminate. + destruct (eq_dec_equation eq eq'). + 2: discriminate. + congruence. + Qed. End SOUNDNESS. |