From cdb48111d4baff50d8708b979f8b31ef21505247 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 21 Sep 2020 22:48:45 +0200 Subject: risc-V now without trapping instructions --- riscV/SelectLongproof.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'riscV/SelectLongproof.v') diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index f5e8edf8..0fc578bf 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -558,6 +558,7 @@ Proof. unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longoffloat; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat. @@ -565,6 +566,7 @@ Proof. unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longuoffloat; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong. @@ -572,6 +574,7 @@ Proof. unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_floatoflong; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu. @@ -579,6 +582,7 @@ Proof. unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_floatoflongu; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. @@ -586,6 +590,7 @@ Proof. unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longofsingle; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle. @@ -593,6 +598,7 @@ Proof. unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longuofsingle; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. @@ -600,6 +606,7 @@ Proof. unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_singleoflong; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. @@ -607,6 +614,7 @@ Proof. unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_singleoflongu; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. End CMCONSTR. -- cgit