diff options
Diffstat (limited to 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 1d713010..9dfe9b6e 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -886,7 +886,17 @@ Theorem eval_select: eval_expr ge sp e m le a v /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v. Proof. - unfold select; intros; discriminate. + unfold select; intros. + destruct ty; cbn in *; try discriminate. + inv H. + TrivialExists. + - cbn. constructor. + { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. } + constructor. eassumption. constructor. eassumption. constructor. + - cbn. f_equal. rewrite ExtValues.normalize_select01. + destruct b. + + rewrite ExtValues.select01_long_true. reflexivity. + + rewrite ExtValues.select01_long_false. reflexivity. Qed. Theorem eval_addressing: |