From 646a21fc7271316880edc4e627923e7bdd93065b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 13 Nov 2016 17:00:44 -0500 Subject: Add SpecificGen/GF* For bounds analysis --- .../GF41417_32Reflective/CommonUnOpFEToZ.v | 44 ++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v (limited to 'src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v') diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v new file mode 100644 index 000000000..6d991dbb4 --- /dev/null +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v @@ -0,0 +1,44 @@ +Require Export Crypto.SpecificGen.GF41417_32Reflective.Common. +Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOpFEToZ_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe41417_32W x) + (Hx : is_bounded (fe41417_32WToZ x) = true), + let args := unop_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_fe41417_32W x) + (Hx : is_bounded (fe41417_32WToZ x) = true), + let args := unop_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unopFEToZ_bounds_good bounds = true + | None => False + end) + : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unop_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. -- cgit v1.2.3