diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 13:33:43 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 13:33:43 +0100 |
| commit | a47d709fd9251f58032444fde27a3ad7e947c26d (patch) | |
| tree | 8270330b3037657d5b5b28bb722ed4dd283ae0cf /riscV/SelectOpproof.v | |
| parent | 7afc85c95aaec5cc0935733cac487e13f114cc46 (diff) | |
| download | compcert-kvx-a47d709fd9251f58032444fde27a3ad7e947c26d.tar.gz compcert-kvx-a47d709fd9251f58032444fde27a3ad7e947c26d.zip | |
Pselectd
Diffstat (limited to 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 7f7474b6..c313fbaf 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -962,6 +962,25 @@ Proof. * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption. - inv H. TrivialExists. + cbn. constructor. + { econstructor. + { constructor. + { econstructor. eassumption. cbn. rewrite H3. reflexivity. } + constructor. econstructor. constructor. eassumption. + constructor. cbn. reflexivity. + constructor. econstructor. constructor. eassumption. constructor. + cbn. reflexivity. constructor. + } + constructor. + } + constructor. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + destruct b. + * rewrite ExtValues.select01_long_true. + apply ExtValues.float_bits_normalize. + * rewrite ExtValues.select01_long_false. + apply ExtValues.float_bits_normalize. + - inv H. TrivialExists. + + cbn. constructor. { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. } constructor. eassumption. constructor. eassumption. constructor. + cbn. f_equal. rewrite ExtValues.normalize_select01. |